关于Z3 for Java的性能问题

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

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

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

如果我通过相同的ctx实例生成expr数十亿次，那是否会出现问题？ 何时是调用ctx.Dispose()的最佳时机，或者，管理c​​tx的最佳方法是什么？

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

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

Answer 1

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

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