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

[Leonardo de Moura]

Hi Silvio,


>> - Use bvadd, bvsub, bvuminus, bvmul, bvle, bvge, bvlt, bvgt  
>> instead of
>>    +, -, *, <=, >=, <, >.
>
> Why? :-) After all, it is easy to support a slight form of overloading
> (as we argue in the proposal) to re-use the standard arithmetic  
> symbols
> without complicating the parsing... So, why are you suggesting to  
> use a
> different set of symbols?  Is there something I am missing?

I was trying to limit overloading to bitvector operators. I didn't  
want to
deal with them in other theories. :-)
That is also the motivation for my other comment:

>> - Use overloading only for "theory" functions and predicates. I mean,
>> one should not be able to overload uninterpreted functions/ 
>> predicates.

Actually, I don't think overloading is appropriate for an  
intermediate format such
as SMT-LIB. In my point of view, SMT-LIB benchmarks/formulas are  
automatically
generated by other tools, and not manually written by a person.
So, overloading adds an unnecessary level of complexity.
We could avoid overloading by using the indexed function
symbols. In this way, we would have:

(bvadd[1] BitVec[1] BitVec[1] BitVec[1])
(bvadd[2] BitVec[2] BitVec[2] BitVec[2])
(bvadd[3] BitVec[3] BitVec[3] BitVec[3])
(bvadd[4] BitVec[4] BitVec[4] BitVec[4])

instead of:

(+ BitVec[1] BitVec[1] BitVec[1])
(+ BitVec[2] BitVec[2] BitVec[2])
(+ BitVec[3] BitVec[3] BitVec[3])
(+ BitVec[4] BitVec[4] BitVec[4])

What do you think?


>> - I think it would be nice to include bv2nat and nat2bv.  For  
>> instance,
>> nat2bv is useful for specifying bitvector constants. I guess nat2bv
>> needs to be indexed with the size of the resulting bitvector.
>
> To tell the truth, in a previous version, we have included the two  
> functions
> in the signatures and not only in the semantics.  Then, we decided  
> not to do
> so, since it make the theory of fixed-size bit-vectors even more  
> complex since
> it forces us to see it as a non-disjoint combination of the theory of
> bit-vectors as defined in the actual proposal and Presburger  
> arithmetic
> with the two functions bv2nat and nat2bv as bridges between the  
> theories.

I see.


> To define the theory of bit-vectors this is not necessary... To be  
> strict,
> it is not even necessary to introduce the two functions in the  
> semantics.

I agree.

> Regarding bitvector constants, notice that in the logic we have  
> introduced
> a suitable set of abbreviations which denotes exactly bitvector  
> constants.

Sorry, I thought you had only bv0 and bv1.
I read your proposal again, and I found the bvN abbreviations. :-)

Cheers,
Leonardo