java - 如何从Java程序中正确调用Z3？

Question

我想将 Z3 集成到我用 Java 开发的安全工具中。目前，我正在输出公式以 checkin 文件，然后调用 Z3。请问Ja​​va API稳定性如何？

当我查看随 Z3 分发的 Java API 示例时，似乎有两种方法可以解决公式。第一个是创建一个求解器:

Solver solver = ctx.MkSolver();

for (BoolExpr a : g.Formulas())
    solver.Assert(a);

if (solver.Check() != Status.SATISFIABLE)
    throw new TestFailedException();

另一种方法是使用战术。有使用策略“simplify”和“smt”的示例

ApplyResult ar = ApplyTactic(ctx, ctx.MkTactic("simplify"), g);
if (ar.NumSubgoals() == 1
        && (ar.Subgoals()[0].IsDecidedSat() || ar.Subgoals()[0]
                .IsDecidedUnsat()))
    throw new TestFailedException();

我的问题是:调用 z3 哪种方法更有效？第一个或第二个。哪种策略适合哪个问题？策略“smt”适用于 SMT-LIB1 还是 SMT-LIB2？

谢谢。

Answer 1

Z3 Java API 是稳定的，因为它在下一个版本之前不会更改任何函数/结构名称。当然可能会有错误修复，也许还有一些附加功能。

使用求解器或策略是否更有意义完全取决于应用程序。但是，由于您当前使用基于文件的接口(interface)，因此使用基于求解器的接口(interface)可能就足够了。使用此功能时，solver.Check() 将使用默认策略(可能取决于所使用的逻辑)来解决问题。

有关策略的更多信息，请参阅strategies tutorial ，它展示了如何使用基于 SMT-LIB 文件的界面中的目标和策略。这同样适用于 Java API，并且策略的名称是相同的。 “smt”策略是封装在策略中的 SMT 求解器；这与输入语言(SMT1 或 SMT2)无关，本质上与使用通过 ctx.MkSolver() 构造的默认 Solver 对象相同。