: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 vice versa on demand.
Yes, you can use things like
bv2int
andint2bv
. 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 ):
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
andnat2bv
): http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2