Z3 for Java 中 check() 的性能

Question

我正在使用 Z3 for Java 来检查具有未解释函数的术语的可满足性，例如 (type(o)>1 或 type(p)2 and type(o)=1）运行solver.check() 需要6 ms。

        FuncDecl typeFun = ctx.MkFuncDecl("type", ctx.IntSort(), ctx.IntSort());        
        Expr o = ctx.MkConst("o", ctx.IntSort());
        //type(o)
        IntExpr to = (IntExpr)typeFun.Apply(o);
        //type(o)=1
        BoolExpr subExpr1 = ctx.MkEq(to, ctx.MkInt("1"));   
        //type(o)>2    
        BoolExpr subExpr2 = ctx.MkGt(to, ctx.MkInt("2"));  
        //type(o)>2 and type(o)=1
        BoolExpr expr = ctx.MkAnd(new BoolExpr[] { subExpr1, subExpr2 });

        solver.Assert(expr);
        //this step will take 6 ms.
        solver.check();

鉴于我的项目中实际约束的大小比这个例子大得多（但每个术语都非常简单，例如 type(o1)=1, type(o2)>1 等）并且有数十亿个这样的例子约束需要解决：
1、check()的表现应该是这样的吗？ 2. 如果 1 的答案是肯定的，是否有其他替代方法可以绕过性能问题？

提前致谢。

@ChristophWintersteiger： 我认为我系统中的很大一部分约束应该是 SAT。我正在为 Java 实现指针分析，并且我正在使用 Z3 以自下而上的方式解决虚拟调用的潜在目标。假设我有一个虚拟调用点 v.foo()，这个调用点可能会根据 v 的动态类型调用不同的方法。所以对于每个被调用者 foo()，我将引入一个约束 type(o) = T，其中 o 是点- 接收者 v 和 T 的集合是声明 foo 的类。约束意味着当 v.foo() 的一个动态指向集的类型为 T 时，v.foo() 可以在 T 中调用方法 foo()。我当前系统中的所有约束都是一些线性算术，只有一个未解释的函数“类型” (o)"。但是由于我是以自下而上的方式分析调用图，因此可以扩展与每个虚拟调用点相关的约束，直到分析到达根级别并且已经解决了接收器的所有指向目标。

Answer 1

6ms 对我来说听起来相当快。为什么这太慢了？

solver.check() 调用本机 .dll/.so，因此在执行调用之前涉及相当多的开销。一旦.check() 返回，在检查结果是否有错误时会产生另外一点开销。因此，很可能仅仅因为应用程序正在使用 Java API 而需要 6 毫秒。

如果应用程序对性能的要求如此之高，那么可能无法使用 C API，因为所有其他 API 都会产生一些非零开销。

附录：我做了以下简单类型的分析：

long startTime = System.nanoTime();
int i = 0;
for (; i < 10000; i++) {                                
    status = solver.check();
}
long elapsedTime = System.nanoTime() - startTime;

运行大约需要 22 秒。此处调用的默认求解器确实在此特定实例上表现出次优性能。我们可以通过添加 ignore_solver1 选项（或使用 push/pop 命令）强制 Z3 回退到较旧的求解器，即如下设置：

Solver solver = ctx.mkSolver();
Params solver_params = ctx.mkParams();
solver_params.add("ignore_solver1", true);
solver.setParameters(solver_params);

现在解决同样的问题 10k 次大约需要 100ms（我得到 9us/check）。

在这些命令上调用的求解器也支持增量求解，因此我们几乎可以免费添加推送/弹出命令：

for (; i < 10000; i++) {
    solver.push();
    status = solver.check();
    solver.pop();
}

这会将 10k 检查的运行时间增加到 ~120ms。现在，将solver.add(expr) 移动到这个循环中会大大增加运行时间，即，对于这个：

for (; i < 10000; i++) {
    solver.push();
    solver.add(expr);
    status = solver.check();
    solver.pop();
}

我的运行时间约为 275 毫秒，即接近我们之前的两倍。因此，此时，表达式构建/添加所需的时间与求解时间处于同一数量级。此时，瓶颈确实是Java API。

我也许应该补充一点，我只尝试了问题中提供的示例。在稍微不同的示例中，求解器的行为很可能会有所不同，添加 ignore_solver1 选项的行为会更糟。

Answer 2

您可以尝试使用自定义策略。默认求解器使用相当广泛的算法组合（我相信）。尝试使用不经过预处理的简单策略，例如 MkTactic("smt")。