DOMAINS :: SMT-LIB :: Proposal for a theory of fixed-size bit-vectors in SMT-LIB format

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. Proposal for a theory of fixed-size bit-vectors in SMT-LIB format

barrett wrote at Apr 07, 2006 - 04:17 PM
---------------------------------------------------------------------
I would like to thank Silvio and Cesare for working hard to put together the
bit-vector theory.  Since we are planning to use it in this year's SMT-COMP, I
have read through it carefully and have a lot of comments.

bv4.theory comments:

First, one high-level comment.  The theory seems designed to think of
bit-vectors with their least significant bit (LSB) on the left and most
significant bit (MSB) on the right.  I would like to make a case that it should
be the other way around.  Hardware people typically think of bit-vectors with
the MSB on the left and LSB on the right.  This is reflected in hardware
description languages such as verilog.  The particular operators that are
affected are extract and concat.  I really want to emphasize the importance of
having the same semantics as hardware languages.  Otherwise, I think it will be
more difficult (and error-prone) to persuade hardware people to produce smt-lib
format.

Another high-level comment: as the number of bits grows, the size of the theory
is going to grow significantly, especially for the different variants of the
extract operator.  I wonder if it wouldn't be worth introducing some
meta-notation that would make the theory more readable.  For example, the
":funs" section could have a comment describing the general pattern of the
functions and then a pointer to the more formal description (or perhaps an
"include" directive).  That way, someone reading the theory doesn't have to
deal with an inordinately large file.

Now, some specific commentary (this commentary does not address the first point
above which would require more substantial changes throughout):

The ":type-constraints" section is problematic: half way through the list of
items, a switch is made from "or" to "and".  Also a switch is made from the
constraints on s to constraints on sub-terms of s.  There should be an easier
formulation using a standard inductive definition: i.e. "s is well-sorted if s
is of the form extract[i:j] t where t is well-sorted and..."
In item 4 (concat), the bounds are wrong: it should be 0 < i,j 
---------------------------------------------------------------------

Reply to this message:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=179&forum=46

Browse thread:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=179

You are receiving this Email because you are subscribed to be notified of events in forums at: http://www.qpq.org/