来自 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 文件可能需要以一种或另一种方式进行调整。

这是我的代码。我正在使用 Ubuntu 16.04 LTS 和 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 人员会如何解决这个问题，因为默认求解器会很快处理查询。请报告您的发现！