我在当前使用 Z3 for Java 的项目中遇到了一些性能问题：
基本上我当前的大多数限制都非常简单：
例如：(f(x) = 2 && f(y) <= 3) || f(x) <=5
-
我正在使用整个项目共享的静态上下文和解算器实例：
public class ConstraintManager {
static Context ctx;
static Solver solver;
...
}
如果我通过同一个 ctx 实例生成 expr 数十亿次，这会出现问题吗？什么时候是调用的最佳时间ctx.Dispose()，或者，管理 ctx 的最佳方式是什么？
我调用了expr.Simplify()简化一些约束，例如：f(x)=3 && f(x)<=2。
但这个 API 结果非常慢。特别是约束长度增加。这是一个已知问题还是因为我使用不当？
我在用expr.substitute(expr1, expr2)，但我注意到 z3 在替换后会将 expr 转换为 let 绑定形式。这是为了让公式更紧凑吗？
- Simplify 执行简单的代数简化。在某些情况下您可以控制其行为。例如，* 分布在 + 上，但这可能会导致真正的开销，并且可以关闭这种简化。从命令行使用 z3 -pm:simplify 来检查参数。 （另一方面，Z3 不太可能解决这种简化成本太高的公式）。
- “let-bounds”由打印机提供。在内部，术语表示为共享节点的有向无环图。将 DAG 打印为树可能非常昂贵（在最坏的情况下是指数级的）。因此，当打印机确定这会给出较短的打印长度时，它会引入 let 表达式。
.NET 和 Java API 使用垃圾收集器来管理术语的生命周期。它们由 GC 自行决定回收。为了获得最佳性能，您可以自行管理引用计数，但随后您必须绕过支持的 API。已发布的源代码包含与执行此操作相关的 JNI/pinvoke。请注意，滚动您自己的低级 API 需要大量工作，而且低级引用计数也不像受支持的 API 那样易于编程。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
