[SMT-LIB] Bitvectors

[Cesare Tinelli]

Hi Christoph,

On Feb 9, 2007, at 12:15 PM, Christoph M. Wintersteiger wrote:

>
> Hi there!
>
> Two quick questions:
>
> a) I know there were plans for a new theories/logics for sizes other
> than 32 -- are these plans still there, or did somebody define those
> theories already?
>
In view of the request and the feedback from members of this list,  
the current plan is to provide a single theory of bitvectors, with no  
bounds on the vector size. See below.


> b) Are there any plans to introduce a quantified version of the
> bitvector logics/theories?
>
Not currently. As usual, a new logic (or theories) are introduced  
only after a sizable of set of benchmarks are available for that  
logic, and the logic is of interest to the SMT community. Bitvector  
logics with quantifiers are definitely of interest, so the only thing  
that we need are the benchmarks :)


>
> I think there should also be a bitvector theory that does not  
> predefine
> the (max) size of a vector, maybe this could be based upon the array
> theory?
>
There is no need to use array if we allow a specification with an  
infinite signature (for the infinitely-many sorts BitVec(1), BitVec 
(2), ..., and the infinitely many polymorphic operators on those sorts.)

Now, the current SMT-LIB language does not allow one to specify this  
kind of infinite signature, and extending the format to do that  
properly does not seem to be worth the trouble at the moment because  
it requires extending SMT-LIB's underlying logic with dependent types.

So, as a practical solution we are going to propose that we simply  
drop for the bitvector theory the requirement that the signature be  
specified by formal SMT-LIB attributes (as opposed to free text  
ones). Specifying the signature in English, as it is now done in  
the :*_description attributes in the current theory  
Fixed_Size_BitVectors[32], should be enough for the short to medium  
term. None of the groups developing bitvector solvers seem have a  
need to parse the signature attributes anyway, or expect to need that  
in the future.

Then, the specification of the new theory becomes pretty much the  
same as that of Fixed_Size_BitVectors[32], with the difference that  
the formal attributes :sorts and :funs and :preds are absent, and the  
32 bit upper bound goes away.

Best,


Cesare





> Regards,
> cmw
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib