[SMT-LIB] Bool as alias for BitVec[1]

[Cesare Tinelli]

Domagoj,

On Feb 16, 2007, at 5:35 PM, Domagoj Babic wrote:

> Hi,
>
> Encoding some software verification benchmarks to Yices and new
> SMT modular arithmetic format without UIFs, I ran into a type  
> inconsistency:
>
> BitVec[1] is type-incompatible with bool, which is weird, at best.
>
This is not an inconsistency. It is a feature (not kidding).

SMT-LIB's underlying logic maintains the traditional distinction in  
first-order logic between formulas and terms: terms denote the  
individuals one wants to talk about while formulas express properties  
of these individuals. More concretely, since the logic is typed over  
terms, terms of a certain sort (i.e, type) S denote elements of that  
sort, formulas denote true or false statements about those elements.

So, writing (= a b), say, where a and b are terms of some sort S, is  
a statement about the elements denoted by a and by b---which holds or  
not depending on the interpretation of a and b.
The expression (= a b) is not a term, it does not denote any element.


> Since current QF_UFBV32 logic does not allow BitVec[1] type,

?? It does.


> I assumed
> that this is just a cosmetic modification, but Clarke B. pointed  
> out that
> this modification would require changes in the underlying logic.
>
What modification? Eliminating the difference between terms and formula?
That modification would indeed require a major change of both the  
underlying logic's syntax and semantics.

There is a plan to that in the next version of the standard,  
following the example of
the literature in higher-order logics, but notice that that will  
entail introducing a predefined Bool sort and have all formulas  
become terms of that sort.
The new Bool sort will still be distinct from BITVECTOR[1]. Booleans  
and bit vectors of size 1 really belong to two different types, the  
same way as the type of integer arrays of size 1 is different from  
the integer type (or the type of singleton sets of integers is  
different from integer type, and so on).
So, your request to identify Bool and BITVECTOR[1] cannot be  
accepted, for the same reason you might not find acceptable to  
identify integers with integer arrays of size 1, say.



> Questions:
> 1) Is it possible to modify the underlying bitvector logic to fix this
> inconsistency?

Again, change you are proposing would require a change to the whole  
SMT-LIB language and underlying  logic, not just the definition of  
bit vectors
Moreover the change is not even needed as your needed can be already  
accommodated in the current language.

> Example:
> :extrafuns ((a b c BitVec[1]))
> :extrafuns ((d BitVec[2]))
> :assumption (= a (= (bvxor b c) bv0))
> :assumption (= d (concat b c))

The first assumption contains indeed an ill-formed formula. But you  
can write what you mean by using ITE expressions, which are there in  
the language exactly to address this kind of need:

:extrafuns ( (bv0[1] BitVec[1]) (bv1[1] BitVec[1]) )
:assumption (= bv0[1] (extract[0:0] bv0)) ; zero bit vector of size 1
:assumption (= bv1[1] (extract[0:0] bv1)) ; one bit vector of size 1
:assumption (= a (ite (= (bvxor b c) bv0) bv0[1] bv1[0]))

Admittedly, this is not as concise as what you had in mind and it  
also involves the definition
of additional constants. But it requires no modification to the  
language and is rather general because it applies to any bit vector  
comparison operator, not just =.

Moreover, the planned new version of the bit vector theory and logic,  
which allows vectors of any size, will predefine bv0[1] and bv1[1],   
bv0[2] and bv1[2], and so on, denoting respectively the zero and the  
one vector for each size. So you will not need to define them yourself.


>
> 2) I'm still not clear about bit-vector sizes. The benchmarks I  
> have generated
> so far use up to 64-bits, so I added
> :notes { maxbits 64 }
> which specifies the maximum number of bits required to do all the  
> computation
> to solve the benchmark. Any other suggestions?
>
A more specific way would be to use a new user-defined attribute such as

:maxbits { 64 }



> 3) I just noticed that the new operators that were recently  
> proposed suggest
> bv(s)mod instead of bv(s)rem. That should be fixed.
>
In what way? What is the problem with bvmod?



>
> If all three suggestions are accepted, I can make the benchmarks  
> available
> today...
>
Is your offer still valid? :)

We plan to propose the new version of the theory  
Fixed_Size_BitVectors and the logic QF_UFBV in the next few days.  
With that, inserting ITEs in your benchmarks should not take a lot of  
effort.

Thanks,


Cesare




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