关于Z3 for Java的性能问题 [英] Performance issues about Z3 for Java

问题描述

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

I am running into some performance issues in my current project with Z3 for Java: Basically most of my current constraints are pretty simple: e.g: (f(x) = 2 && f(y) <= 3) || f(x) <=5

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

1. I am using static context and solver instances shared by the whole project:

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

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

If I generate expr by the same instance of ctx for billions of times, is that going to an issue? When is the best time to invoke ctx.Dispose(), or, what's the best way to manage ctx?

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

1. I invoked expr.Simplify() to simplify some constraints like: f(x)=3 && f(x)<=2. But this API turned out to be very slow. Especially the length of constraint increased. Is this a known issue or is that because I used it incorrectly?

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

I am using expr.substitute(expr1, expr2), but I notice that z3 will turn the expr into a let-binding form after substitution. Is this for making the formula more compact?

推荐答案

1. 简化执行简单的代数简化。在某些情况下，您可以控制其行为。例如*分配超过+，但这可能导致实际开销，并且可以关闭这种简化。使用z3 -pm：从命令行简化以检查参数。 （另一方面，Z3不太可能解决这种简化过于昂贵的公式。）


2. let-bindings由打印机提供。在内部，术语表示为共享节点的有向非循环图。将DAG作为树打印可能非常昂贵（在最坏的情况下呈指数）。因此，当打印机确定这样可以缩短打印长度时，它会引入let表达式。

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

The .NET and Java APIs use the garbage collector to manage lifetimes of terms. They get recycled at the discretion of the GC. For top performance you can manage reference counts on your own, but then you have to bypass the supported API. The released source code contains the JNI/pinvoke relevant to do this. Note that rolling your own low level API is a lot of work and the low level reference counting is also not as easy to program with as the supported API.

这篇关于关于Z3 for Java的性能问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！