【发布时间】：2012-06-27 13:10:08
【问题描述】：
如何以 SMT-LIB2 格式输出 z3py 的断言？我在文档中找不到任何提及。我找到了一个标志Z3_PRINT_SMTLIB_FULL，但我不知道如何设置它。
【问题讨论】：
【发布时间】：2012-06-27 13:10:08
【问题描述】：
您可以使用方法 sexpr()。 例如： http://rise4fun.com/Z3Py/9t
x, y = Reals('x y')
print (x + y * 3).sexpr()
有 Python API 的在线文档。 例如，sexpr() 方法记录在：
http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#ExprRef
【讨论】：
-
您想要一个有效的 SMT 2.0 脚本的输出吗？
-
我们将在未来的版本中添加此功能。我同意它非常有用。
-
@LeonardodeMoura：这是最终添加的吗？