如何从 z3 求解器生成 SMTLIB2 格式的公式

Question

我使用 java API 在 z3 中构建公式。 但是，我有一些难以解决的公式，我想调查原因。因此，我想以 SMTLIB2 格式打印公式。

是否可以从 Solver 对象中获取它。目前，我能得到的只是一组断言。谢谢。

Answer 1

是的，Solver.toString() 做到了。如果您使用的是最新的 master，这还应该包括 variable/constant 声明；我认为那部分是在上次发布之后添加的。