Z3: hidden int sort in bitvector
: variable x is defined to be of type int by (declare-const x Int)
Is there any method for converting x to bitvector sort? Because sometimes x includes bitwise operations like &, |, ^, which int theory can't handle.
I don't want to define the variable x as a bitvector at the beginning, because I believe that the operations (e.g. +, -, *, /) supported by int theory other than bit-operations are much faster than the operations supported by bitvectors.
So, actually, I want to hide int sort in bitvector sort or vise vesa is in demand.
Thank.
Ting Chen
source to share
Yes, you can use things like bv2int
and int2bv
. Note that the length of the bitvector matters and that int2bv is parametric (the length of the bitvector is required).
Here's a minimal example (link: 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:
It looks like there may be some problems with these functions at the moment: Check for overflow with Z3
They can also be called by different names in other solvers ( bv2nat
and nat2bv
): http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2
source to share