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

[Silvio.Ranise@loria.fr]

Hi Leonardo,


Selon Leonardo de Moura <demoura at csl.sri.com>:

> 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. :-)

I see your point... After all, it seems reasonable to limit overloading
within a theory and not globally (across 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?

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...

Thanks a lot for your comments.

Cheers,

Silvio.