java - Z3 Java API : when to dispose expressions/Z3 objects?

Question

在我的 Java 代码中，我在循环中调用 Z3 来检查公式(取决于循环索引并且每次迭代都不同)，直到公式变得可满足，如以下伪代码片段所示:

int n = 0;
do {
    n += 1;

    Context ctx = new Context();
    Solver solver = ctx.mkSolver();

    // Construct large formula b(n) (depending on n)
    // with a lot of Boolean subexpressions
    BoolExpr b = ... 
    solver.add(b);

    Status result = solver.check();

    solver.dispose();
    ctx.dispose();

    if (result == Status.SATISFIABLE) {
         break;
    }

} while (true);

但是，我很快遇到了内存问题(即抛出带有“内存不足”消息的 Z3Exception)，并且我觉得我可能没有正确处理创建的 Z3Objects。

由于我没有找到这方面的信息(我刚刚找到 Z3 Java API documentation or tutorial 和 Performance issues about Z3 for Java )，我的问题是:

1. 调用 solver.dispose() 时，所有包含的 BoolExpr 也都已释放，还是我需要在某处记住它们并对其中任何一个调用 .dispose() ？
2. 将上下文和求解器的创建和处理移出循环，转而在循环内使用 solver.push() 和 solver.pop() 是否会提高性能？
3. 在给定情况下，我还应该“手动”处置哪些其他 Z3Objects？

Answer 1

当抛出带有“内存不足”消息的 Z3Exception 时，意味着 native libz3.dll 内存不足。在每次循环迭代中同时处理求解器和上下文确实是最好的选择(一些东西仍然保留在内存中，例如符号)。但请注意，Solver 和 Context 对象对于垃圾收集器来说看起来就像微小的对象(它们只是一个指针，Java 无法看到指针后面的内容)。因此，首先要尝试的是添加对 System.gc() 的调用，希望此时所有 Z3 对象都能真正被收集。另外，我似乎记得 Java 虚拟机的默认内存限制比预期的要小，但可以通过 -Xms 和 -Xmx 选项进行设置。