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

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

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

Solver solver = ctx.MkSolver();

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

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

另一种方法是使用战术。有使用战术“简化”和“ 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？

谢谢。

最佳答案

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

使用求解器还是使用战术更有意义，这完全取决于应用程序。但是，由于您当前使用的是基于文件的界面，因此使用基于求解器的界面可能就足够了。使用此方法时，solver.Check（）将使用默认策略（可能取决于所使用的逻辑）来解决问题。

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