在 Java API 中使用 parseSMTLIB2String 的 Z3 一旦发现一个 UNSAT 就会提供错误的 UNSAT答案

【问题标题】：Z3 using parseSMTLIB2String in Java API delivers false UNSAT once it devilverd one UNSAT在 Java API 中使用 parseSMTLIB2String 的 Z3 一旦发现一个 UNSAT 就会提供错误的 UNSAT
【发布时间】：2018-03-26 11:48:06
【问题描述】：

我的 Z3 SMT 求解器实现很粗糙，但我发现 Java API 非常难以访问。我使用 parseSMTLIB2String，它做得很好，直到 SAT 检查返回一个 UNSATISFIABLE。然后它继续返回 UNSATISFIABLE，即使之前的值返回了 SATISFIABLE。我是不是用错了求解器？

public static Boolean checkSat(int checkMakespan, Flowshop fs) {
    String smtString = FlowShopSmtGen.generateSMTFromFlowshop(fs, checkMakespan);
    HashMap<String, String> cfg = new HashMap<>();
    Context ctx = new Context(cfg);
    BoolExpr fsresult = ctx.parseSMTLIB2String(smtString, null, null, null, null);

    Solver solver = ctx.mkSolver();
    solver.add(fsresult);
    Status s = solver.check();
    System.out.println(s);

    if (s == Status.SATISFIABLE) {
        return true;
    } else {
        return false;
    }
}

【问题讨论】：

添加 ctx.close();求解器.reset();没有做到这一点
这看起来不错，但行为取决于您在 smtString 中传递的内容。如果您认为这是一个错误，请在我们的问题跟踪器上打开一个问题，包括所有涉及的工具的所有字符串和版本号。问题跟踪器在这里：github.com/z3prover/z3/issues

标签： z3 smt

【解决方案1】：

如果您将断言添加到已经无法满足的断言集合中，则预计您会继续获得无法满足的答案。

但是，如果您在中间弹出了一些断言，那么可能会有一些可疑之处。

【讨论】：