Z3 for Java 的性能问题

Question

我在当前使用 Z3 for Java 的项目中遇到了一些性能问题： 基本上我目前的大部分限制都非常简单： 例如：(f(x) = 2 && f(y) <= 3) || f(x) <=5

1. 我正在使用整个项目共享的静态上下文和求解器实例：

   public class ConstraintManager {
       static Context ctx;
       static Solver solver;
       ...
   }
   

如果我通过同一个 ctx 实例生成 expr 数十亿次，这会成为问题吗？何时是调用ctx.Dispose() 的最佳时间，或者，管理 ctx 的最佳方式是什么？

1. 我调用了expr.Simplify() 来简化一些约束，例如：f(x)=3 && f(x)<=2。 但是这个 API 结果非常慢。尤其是约束的长度增加了。这是一个已知问题还是因为我使用不正确？

2. 我正在使用expr.substitute(expr1, expr2)，但我注意到z3 在替换后会将expr 转换为let-binding 形式。这是为了让公式更紧凑吗？

Answer 1

1. Simplify 执行简单的代数化简。在某些情况下，您可以控制其行为。例如 * 分布在 + 上，但这可能会导致实际开销，并且可以关闭这种简化。从命令行使用 z3 -pm:simplify 来检查参数。 （另一方面，Z3 不太可能解决这种简化过于昂贵的公式）。
2. “let-bindings”由打印机提供。在内部，术语表示为共享节点的有向无环图。将 DAG 打印为树可能非常昂贵（在最坏的情况下是指数的）。因此，当打印机确定这会给出更短的打印长度时，它会引入 let 表达式。

.NET 和 Java API 使用垃圾收集器来管理术语的生命周期。它们由 GC 自行决定回收。为了获得最佳性能，您可以自行管理引用计数，但您必须绕过支持的 API。发布的源代码包含与此相关的 JNI/pinvoke。请注意，滚动您自己的低级 API 需要大量工作，而且低级引用计数也不像支持的 API 那样易于编程。