0

我想将 Z3 集成到我用 Java 开发的安全工具中。目前，我正在输出公式以签入文件，然后调用 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();

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

谢谢。

4

1 回答 1

1

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

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

有关策略的更多信息，请参阅策略教程，该教程展示了如何从基于 SMT-LIB 文件的界面使用目标和策略。Java API 也是如此，战术的名称也是一样的。“smt”策略是包裹在策略中的 SMT 求解器；这与输入语言（SMT1 或 SMT2）无关，本质上与使用通过 ctx.MkSolver() 构造的默认 Solver 对象相同。

于 2013-10-28T12:44:03.810 回答