python - z3(py)smt-lib2输出

如何以SMT-LIB2格式输出使用z3py生成的断言？我在文件里找不到任何关于那件事的记载。我发现了一个标志，但我不知道如何设置它。

最佳答案

您可以使用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