如何将z3py表达式转换为smtlib 2格式

Question

我的问题和这个有关： Z3：如何将Z3py表达式转换为SMT-LIB2？

我正在尝试将z3py表达式转换成smtlib2格式。我使用了以下脚本，但在转换后，当我把结果输入到z3或其他SMT工具时，出现了：

“语法错误，意外的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")   

这是输出结果：

(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(let (($x35 (and $x10 $x31 $x34)))
(assert $x35)))))
(check-sat)

Answer 1

这段内容也和另一个问题有关，具体可以查看这里。

很可能，这个问题是因为你使用的Z3版本太旧了。其实，Z3有很多修复bug的更新，但这些更新还没有合并到主版本中。如果你使用不太稳定的版本（或者是这里的预编译夜间版本），我得到的输出就会不同，而且Z3会接受这个输出，没有错误：

(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(assert
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(and $x10 $x31 $x34)))))
(check-sat)