What conversion operators are available in Z3 and CVC4 for Bit-Vectors?

Question

I am writing a BV encoding of a problem which requires converting some Int to BitVec and viceversa.

In mathsat/optimathsat one can use:

((_ to_bv BITS) <int_term>) ; Int => BitVec
(sbv_to_int <bv_term>)      ; Signed BitVec => Int
(ubv_to_int <bv_term>)      ; Unsigned BitVec => Int

In z3 one can use:

((_ int2bv BITS) <int_term>) ; Int => BitVec
???                          ; Signed BitVec => Int   
(bv2int <bv_term>)           ; Unsigned BitVec => Int

In CVC4 one can use:

((_ int2bv BITS) <int_term>) ; Int => BitVec
???                          ; Signed BitVec => Int   
???                          ; Unsigned BitVec => Int

---

Q:

• does z3's have a bv2int function for Signed BitVec? (It appears no.)
• does CVC4 have any bv2int function at all? (I have no clue.)
• is there some place where these conversion functions are documented? (The SMT-LIB webpage about Logics/Theories does not appear to have any information about them.)

note: I am limited by the text-based SMT-LIB interface (no API solution).

Answer 1

SMTLib does define bv2nat and nat2bv:

bv2nat, which takes a bitvector b: [0, m) → {0, 1} with 0 < m, and returns an integer in the range [0, 2^m), and is defined as follows:

   bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ⋯ + b(0)*2^0

o nat2bv[m], with 0 < m, which takes a non-negative integer n and returns the (unique) bitvector b: [0, m) → {0, 1} such that

   b(m-1)*2^{m-1} + ⋯ + b(0)*2^0 = n rem 2^m

See here: http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml

Both CVC4 and z3 should support these two operations. (If not, you should report it to them!)

For everything else, you'll have to do the math yourself. SMTLib is decidedly agnostic about "sign" of a bit-vector; it attributes no sign to a given vector, but instead it provides signed and unsigned version of arithmetic operators when they are different. (For instance, there's only one version of addition since it doesn't matter if you have signed or unsigned bit-vectors for that operation, but for comparisons we get bvult, bvslt etc.)

From these two functions, you can define your other variants. For instance, to do signed-bitvector x of length 8 to integer, I'd go:

(ite (= ((_ extract 7 7) x) #b0)
           (bv2nat ((_ extract 6 0) x))
        (- (bv2nat ((_ extract 6 0) x)) 128)))

That is, you check the top bit of x:

• If it's 0, then you just convert it using bv2nat. (You can skip the top bit as you know it's 0, as a small optimization.)

• If the top bit is 1, then the value is what you converted by skipping the top bit, and you subtract 128 (= 2^(8-1)), from it. In general, you'll subtract 2^(m-1) where m is the size of the bitvector.

One gotcha: You cannot make an SMTLib function that does this for you for all bit-vector sizes. This is because SMTLib does not allow users to define size-polymorphic functions. You can, however, generate as many of such functions as you want by declaring them on the fly, or simply generate the corresponding expressions whenever needed.

Other operations are similarly encodable using similar tricks. Please ask specific questions if you run into issues.