python - z3（py）smt-lib2出力

Question

z3pyで作成されたアサーションをSMT-LIB2形式で出力するにはどうすればよいですか？ドキュメントにそのことについての言及が見つかりません。旗を見つけました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