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 and Cesare,
>
> I'm still having problems with my QPQ account. So, I'm sending my
> comments direct to you.

Uhmm, I have also experienced some problems with my accounts...
We should ask the people handling the site to check things out...

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

>
> - Use overloading only for "theory" functions and predicates. I mean,
> one should not be able to overload uninterpreted functions/predicates.
>
> - 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.
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.
In fact, it would be possible to define the semantics of the various arithmetic
operations on bit-vectors by specifying simple circuits to implement
addition, subtraction, and so on.  Indeed, this would be unnecessarely
long and far too detailed, while by introducing nat2bv and bv2nat the definition
of the semantics becomes much more compact.

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

Thanks a lot for your feedback.

Cheers,

Silvio.


>
> Cheers,
> Leonardo.
>
>
>