来自z3-4.8.9-x64-ubuntu-16.04的非终止Z3Str3

Question

在尝试使用来自z3-4.8.9-x64-ubuntu-16.04的Z3Str3时，我遇到了一个问题，特别是如果我将com.microsoft.z3.jar替换为z3-4.8.8-x64-ubuntu-16.04中的那个，我就不再有这个问题了。问题是，尽管查询很简单，但Z3进程永远不会返回结果。我注意到当我杀死我的程序时，它会返回有效的答案。当我试图在可执行文件上运行相同的查询时，我没有注意到这种行为，所以我猜使用jar文件有一些东西，我可能需要以某种方式进行调整。

这是我的代码。我使用的是Ubuntu16.04LTS和IntelliJ终极版2020.3。

非常感谢！

import com.microsoft.z3.*;
public class Z3String3Processor_reduced {
    public static void main(String[] args) {
        StringBuilder currentQuery = new StringBuilder("\n" +
                "(declare-const string0 String)\n" +
                "(assert (= (str.indexof string0 \"a\" 1) 6))\n" +
                "(check-sat)\n" +
                "(get-model)\n" +
                "\n");
        Context context1 = new Context();
        Solver solver1 = context1.mkSolver();
        Params params = context1.mkParams();
        params.add("smt.string_solver", "z3str3");
        solver1.setParameters(params);
        StringBuilder finalQuery = new StringBuilder(currentQuery.toString());

        // attempt to parse the query, if successful continue with checking satisfiability
        try {

            // throws z3 exception if malformed or unknown constant/operation
            BoolExpr[] assertions = context1.parseSMTLIB2String(finalQuery.toString(), null, null, null, null);
            solver1.add(assertions);
            // check sat, if so we can go ahead and get the model....
            if (solver1.check() == Status.SATISFIABLE) {
                System.out.println("sat");
            } else
                System.out.println("not sat");
            context1.close();
        } catch (Z3Exception e) {
            System.out.println("Z3 exception: " + e.getMessage());
        }
    }
}

Answer 1

我不认为这与Java有任何关系。让我们提取您的查询并将其放入名为a.smt2的文件中

$ cat a.smt2
(declare-const string0 String)
(assert (= (str.indexof string0 "a" 1) 6))
(check-sat)
(get-model)

现在，如果我运行：

$ z3 a.smt2
sat
(
  (define-fun string0 () String
    "FBCADEaGaa")
)

那很好。但是如果我运行：

$ z3  smt.string_solver=z3str3 a.smt2
... does not terminate ..

所以，最重要的是，您的查询(就像它看起来那么简单)给z3str3求解器带来了困难。

我看到你已经在https://github.com/Z3Prover/z3/issues/5673上报了这是一个错误

既然默认的字符串求解器可以很好地处理查询，为什么不直接使用它呢？如果您因为其他原因而不得不使用z3str3，那么您已经发现了它不能很好地处理这个查询的情况；我不确定z3人员会倾向于修复这个问题，因为查询是由默认求解器处理得相当快的。请报告您发现的情况！