:A 变量 x 被定义为一个 int sort by
(declare-const x Int)
有什么方法可以将 x 转换为位向量排序?因为有时 x 涉及到 int 理论无法处理的位操作,例如 &、|、^。
我不想在开始时将变量 x 定义为位向量,因为我认为 int 理论支持的操作(例如,+、-、*、/)除了位操作的运行速度比位向量中支持的操作快得多。
所以实际上,我想根据需要将 int sort 转换为 bitvector sort 或 vise vesa 。
谢谢。
陈婷
最佳答案
是的,您可以使用 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
关于int - Z3:将整数排序转换为位向量,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/27273728/