Z3：隐性int排序成位向量答案

【问题标题】：Z3: Covert int sort into bitvectorZ3：隐性int排序成位向量
【发布时间】：2015-02-01 03:13:41
【问题描述】：

: 变量 x 定义为 int 排序方式 (declare-const x Int)

有什么方法可以将 x 转换为位向量排序吗？因为有时x涉及到位运算，如&、|、^，是int理论无法处理的。

我不想在开始时将变量 x 定义为位向量，因为我认为 int 理论支持的操作（例如，+、-、*、/）除了位操作之外的运行速度比位向量中支持的操作快得多.

所以实际上，我想根据需要将 int 排序转换为位向量排序或 vesa。

谢谢。

陈婷

【问题讨论】：

标签： int z3 smt bitvector

【解决方案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

【讨论】：