[SMT-LIB] Proposal for a theory of fixed-size bit-vectors in SMT-LIB format

[Cesare Tinelli]

Hi Clark,

thanks again for the feedback below. Yesterday we sent a new proposal 
taking your feedback into account. Here is a more specific reply.


QPQ wrote:
> 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.
>
Good point. We have switched the order as you suggest.


> 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.  
 >
We agree on this too. So we have introduced the "_description" variants 
of the :funs, :preds, and :sorts operators, which take a text value.
We

> 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.
> 
We do not think it would be a good idea to add include directives to the 
format, at least at this stage of development, because they complicate 
managing and parsing of the specifications.
Note, however, that we can take advantage of the fact that the SMT-LIB 
format is order independent, so a simple solution can be to write the 
specification so that the informal descriptions come first and the long 
formal ones come at the end of the file, the way we have done it in the 
bitvector definition sent earlier today.


> 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 <= 4.
 >
We have removed this attribute altogether because it is actually 
redundant. With the kind of overloading we propose, well-sortedness and 
sort inference are defined exactly as in the SMT-LIB format 
specification. SO there is not need to discuss them in the theory 
definition.


 > In the "ASSUMPTION" section, you use the terminology "well-formed". I
 > think ou mean well-sorted as defined above.
 >
This is gone too. All formulas and terms in SMT-LIB expressions are 
supposed to be well-sorted.


 > In the ":definition" section:
 >
 > Several times, BVec is used when it should be BitVec
 >
 > Variable symbols: it should be 0 < i <= 4 (not 0 <= i < 4).
 >
 > Function symbols for extraction should read:
 > [[(extract[j:i] s)]] := \lambda x : [0...i-j+1). [[s]](x+j)
 > where s is of sort BitVec[l], 0 <= j <= i < l <= 4.
 >
 > The definition of bv2nat should be:
 > bv2nat(s) := \sum x : [0..4).s(x)*2^x
 >
All of the about should ahve been fixed. Could you please double check.


 > In the definition of the arithmetic operators, things are not
 > well-defined in
 > the case of negative numbers. For example:
 >
 > [[(-s)]] := nat2bv[m](-bv2nat(s))
 >
                        ^^^^^^^^^^^ This is a misprint.
The intended expression was (2^m - bv2nat(s)), which should give the 
right semantics, according to our understanding.
Is that correct?



 > bv2nat returns an integer in the range [0...2^{4}), so after negation it
 > will be in the range (-2^{4}...0]. But nat2bv[m] takes as input an
 > integer in the range [0...2^{4}), so there is a type mismatch in the
 > definition here.
 >


 > bv4.logic comments:
 >
 > In the definition of bvN, it looks like you are expecting N to be given
 > in base ten. This should be made explicit.
 >
We added a comment to that respect.

 > Also, you may want to
 > consider allowing constants specified in base 2, 8, and 16.
 >
How crucial is this? Is it really a big deal to have to use base 10 only?


 > In the line beginning "Below, let m denote":
 > "and integer" -> "an integer"
 > "|exp| denotes" -> "|exp| denote"
 >
Fixed.


 > In the definitions of the various shift operators, m seems to be being
 > used for both the bit-width and the number of bits to shift. This makes
 > the definitions ambiguous at best. Using a different variable for one of
 > the two should solve the problem.
 >
Done.


 > I look forward to the next revision!
 >
Sent in the previous two messages to this list.

Cheers,


Silvio & Cesare



 > -Clark