[SMT-LIB] BitVectors32

[Clark Barrett]

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
>