我的问题与:Z3: convert Z3py expression to SMT-LIB2?
我正在尝试将z3py表达式从转换为smtlib2格式。使用以下脚本,但在转换后,当我将结果输入到z3或任何其他SMT时,我得到:
"Syntax error, unexpected let"
有没有办法可以用z3py把它转换成smtlib2格式,这样我就不用再写长表达式了。在
以下是我用于转换的代码:
def convertor(f, status="unknown", name="benchmark", logic=""):
v = (Ast * 0)()
if isinstance(f, Solver):
a = f.assertions()
if len(a) == 0:
f = BoolVal(True)
else:
f = And(*a)
return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())
x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 0)
s.add( x < 100000)
s.add(x==2*y)
print convertor(s, logic="QF_LIA")
这是输出:
^{pr2}$
这也与另一个问题here有关。在
最有可能的是,这个问题是因为Z3的过时版本。已经有很多错误修复了,但是还没有进入主分支,使用不稳定的分支(或者预编译的夜间二进制文件here)我得到了一个不同的输出,Z3没有错误地接受它:
相关问题 更多 >
编程相关推荐