获取 SMT2 格式的求解器答案

【问题标题】：Getting solver in SMT2 format获取 SMT2 格式的求解器
【发布时间】：2014-08-01 18:50:28
【问题描述】：

我正在使用 java API 生成代码，但我想向用户展示 SMT2 格式的代码，有什么方法可以从 java API 获取它？

可以说我想要一些这样的生成代码...

(forall ((task Task)) (not (mustPrecede task task)))
(forall ((t1 Task) (t2 Task) (t3 Task))
(=> (and (mustPrecede t1 t2) (mustPrecede t2 t3)) (mustPrecede t1 t3)))

可以解析成这样的东西

(declare-fun TaskUser (Task User) Bool)
(declare-fun mustPrecede (Task Task) Bool)
(assert(forall((t Task)) (not (mustPrecede t t))))
(assert(forall((t1 Task)(t2 Task)(t3 Task)) (implies (and (mustPrecede t1 t2)     (mustPrecede t2 t3)) (mustPrecede t1 t3))))
(assert(forall((t Task)(u User)) (TaskUser t u)))

【问题讨论】：

标签： z3 z3py

【解决方案1】：

如果我们将 AST 的打印模式设置为相应的选项，则表达式将以 SMT2 语法打印，例如，

ctx.setPrintMode(Z3_PRINT_SMTLIB2_COMPLIANT);

每当调用 AST 或 Expr 上的 .toString() 函数时，它将符合 SMT2。

请注意，.toString() 函数只会打印表达式本身，而不是它们可能依赖的任何声明。如果需要声明，很可能在客户端代码中的某处存在它们的列表，但如果不是这种情况，则需要遍历表达式以查找它们所依赖的所有函数声明。函数声明可以通过在 Expr 上调用 .getFuncDecl() 来获得。

【讨论】：