Z3：隐蔽INT排序成位向量

Question

：变量x由 定义为int排序（声明const的X智力）

是否有任何与x转换为位向量的排序方法？因为有时x涉及位操作，例如&，|，^ int理论无法处理。

我不想在开始时将变量x定义为位向量，因为我认为int理论支持的操作（例如，+， - ，*，/），除了位操作运行速度远远快于支持的操作bitvectors。

所以实际上，我想要将int转换为bitvector sort或vise vesa。

谢谢。

陈婷

Answer 1

是的，你可以使用之类的东西bv2int和int2bv。注意位向量长度很重要，int2bv是参数（需要位向量长度）。

下面是一个小例子（rise4fun链接：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)) 

另一个例子是在这里：

Z3: an exception with int2bv

它看起来像有可能与目前这些功能的一些问题： Check overflow with Z3

这些也可能被其他求解器中的不同名称调用（bv2nat和nat2bv）：http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2