Z3: Covert int sort into bitvector

问题:

:A variable x is defined as an int sort by (declare-const x Int)

Is there any method to convert the x into a bitvector sort? Because sometimes x involves bit operations such as &, |, ^ that int theory cannot handle.

I do not want to define the variable x as a bitvector in the beginning because I suppose the operations (e.g., +, -, *, /) supported by int theory except bit operations run much faster than those operations supported in bitvectors.

So actually, I want to covert int sort into bitvector sort or vise vesa in demand.

Thanks.

Ting Chen

回答1:

Yes, you can use things like bv2int and int2bv. Note the bitvector length matters and that int2bv is parametric (requires the bitvector length).

Here is a minimal example (rise4fun link: http://rise4fun.com/Z3/wxcp ):

(declare-fun x () (_ BitVec 32))
(declare-fun y () Int)
(declare-fun z () (_ BitVec 16))
(assert (= y 129))
(assert (= (bv2int x) y))
; (assert (= ((_ int2bv 32) y) x)) ; try with this uncommented
(assert (= ((_ int2bv 16) y) z))
(check-sat)
(get-model)
(get-value (x y z)) ; gives ((x #x00000000) (y 129) (z #x0081))

Another example is here:

Z3: an exception with int2bv

It looks like there may be some issues with these functions currently: Check overflow with Z3

These may also be called by different names in other solvers (bv2nat and nat2bv): http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2