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

[Leonardo de Moura]

Hi Silvio,

>> 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?
>
> Uhmmm, I do not agree on this point.  I think that for some theories
> (and the theory of bitvectors is a very appropriate example) not
> supporting overloading makes benchmarks quite difficult even to be  
> generated
> automatically.  After all, to my knowledge, all available benchmarks
> for bitvectors overloads the operations above...  Please, tell me if I
> am wrong...

I don't think it is quite difficult. I think the complexity of  
generating benchmarks
without overloading is equivalent to the one of parsing benchmarks  
with overloading.
If overloading is not supported, then the generator just needs to  
know the number of bits
in each bitvector sub-expression. In most cases, this information  
needs to be computed even
when overloading is provided. For instance, in the CVC Lite format,  
there is a function
(BVPLUS n b1 b2), but b1 and b2 can have different lengths and n is  
the resulting
number of bits and it may be different from the lengths of b1 and b2.  
So, we need
to know the number of bits of b1 and b2 even if overloading is  
provided in the
SMT-LIB format.

Anyway, I will be happy if overloading is limited to the bitvector  
theory. :-)

Cheers,
Leonardo