鉴于Z3py的表情，我可以转换到SMT-LIB2语言？ （因此，我可以喂这个SMT-LIB2表达于其他SMT求解器支持SMT-LIB2）
如果这是可能的，请举一个例子。
非常感谢。
Answer 1:
我们可以使用C API Z3_benchmark_to_smtlib_string 。 在C API中的每个函数Z3Py可用。 此功能最初是用于转储在SMT 1.0格式的基准，它早于SMT 2.0。 这就是为什么它有一些参数可能似乎是不必要的。 现在，在默认情况下，它会显示在SMT 2.0格式的基准。 输出不意味着是人类可读的。 我们可以写出下面的Python功能，使其更加方便使用：
def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""):
v = (Ast * 0)()
return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())
下面是使用它的一个小例子（也可在网上点击这里 ）
a = Int('a')
b = Int('b')
f = And(Or(a > If(b > 0, -b, b) + 1, a <= 0), b > 0)
print toSMT2Benchmark(f, logic="QF_LIA")
文章来源: Z3: convert Z3py expression to SMT-LIB2?
