Z3py：在约束中求解整数和位向量

Question

我正在尝试在 python 中使用 Z3 SMT 求解器来求解约束。约束涉及整数和位向量。我正在使用 Z3_mk_bv2int 将 BitVec 转换为 Int。我相信以下约束是不可满足的，但我从 Z3 求解器获得了 SAT。我不确定我是否正确转换它。但是，如果我用受约束的整数变量替换 BitVecs 变量，则不需要转换，我会得到预期的结果。

例子：

def get_int(var):

ctx = var.ctx

    return ArithRef(Z3_mk_bv2int(ctx.ref(), var.as_ast(), 0), ctx)

def main():

    var1 = BitVec('var1', 6)
    var2 = Int('var2')
    solve(var2 == get_int(var1)- var2, var2 > 32)

if __name__ == "__main__": main()

结果： [var1 = 0, var2 = 33]

我是 SMT 求解器的新手。请帮我找出错误或替代解决方案。

Answer 1

请看一下这个问题： https://z3.codeplex.com/workitem/187

本质上，问题在于默认情况下不导入 Z3_mk_bv2int。尝试添加
from z3 import *

在程序的开头。