python - z3 (py) smt-lib2 输出

Question

如何以 SMT-LIB2 格式输出使用 z3py 所做的断言？我在文档中找不到任何提及。我找到了一个标志Z3_PRINT_SMTLIB_FULL，但我不知道如何设置它。

Answer 1

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