[SMT-LIB] BitVectors32

[Christoph M. Wintersteiger]

Thanks for your reply!

I do of course know the difference between theory and logic files - for 
some strange reason I just didn't see the bvX in there. So by now I 
solved that problem.

However, two other small things occurred to me while implementing the BV 
typechecker. I solved these, but they still seem kind of 'unclean' to 
me, that's why I mention them:

- predicates are not defined for different bitvector sizes, e.g., = is 
frequently used in the benchmarks with arguments of BitVec[8] and 
Bitvec[32]. Also, the theories predicates (bvlt, bvleq...) are only 
defined to be (pred BitVec[m] BitVec[m]), i.e., take arguments of equal 
size m. And there is no bveq (not needed, but would be nice).

- Variables of sort BitVec[1] are implicitly assumed to be boolean. 
While this is not a real problem, a typechecker still has to double 
check the function definitions in that case.

Christoph

Clark Barrett schrieb:
> Christoph,
> 
> The notation you are referring to is explained in the bit-vector *logic* file:
> QF_UFBV[32].  This is different from the *theory* file.
> 
> Every SMT-LIB benchmark references a logic, and every logic references a
> theory.  The theory explains the formal signature and semantics.  The logic is
> used to restrict the language or to offer extensions (which can be thought of
> as syntactic sugar) as is the case here.
> 
> -Clark Barrett
> 
>>
>> Hi list members!
>>
>> I have the following problem: The BitVectors32 theory defines these
>> basic functions:
>>
>> - Constant symbols bv0 and bv1 of sort BitVec[32]
>>    [[bv0]] := \lambda x : [0...32). 0
>>    [[bv1]] := \lambda x : [0...32). if x = 0 then 1 else 0
>>
>> However, some of the benchmarks seem to use this as if there was a
>> function bvX, e.g. QF_UFBV32/crafted/bb.smt wants bv7.
>>
>> >From the declaration of bv0/bv1 I guess this used to be a definition of
>> the form bvX anyways. So: should I implement this as bv0/1 and wait for
>> the benchmark files to be fixed, or should I implement bvX and ignore
>> the theory definition? 
>>
>> It would also be nice to know what does functions are supposed to do: Is
>> this kind of an ==0 as in C? or is this supposed to load a bitvector
>> with the binary representation of X?
>>
>> Thanks,
>> Christoph
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>
>