Z3 Java API：何時配置表達式/ Z3對象？

在我的Java代碼中，我在循環中調用Z3來檢查公式（取決於循環索引，每次迭代都不相同），直到公式變得可滿足，如下面的僞代碼片段所示：Z3 Java API：何時配置表達式/ 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），我的問題是：

當調用solver.dispose()，都包含BoolExpr配置一樣好，甚至我需要的地方記住他們並致電.dispose()其中任何一個？
將環境和求解程序的創建和處理移出循環，而是在循環內部使用solver.push()和solver.pop()會更高效嗎？
其他Z3Objects我應該在特定情況下「手動」處理嗎？

來源

2014-12-19 Dan

當拋出「內存不足」消息的Z3Exception時，這意味着本機libz3.dll內存不足。在每個循環迭代中處理解算器和上下文實際上是可以完成的最好的（一些事情仍然留在內存中，例如符號）。但是請注意，Solver和Context對象看起來像垃圾收集器的小對象（它們只是一個指針，Java不能看到指針後面的內容）。所以，首先要嘗試的是給System.gc()添加一個電話，希望所有Z3對象都能在此時真正收集。此外，我似乎還記得，Java虛擬機的默認內存限制比預期的要小，但它們可以通過-Xms和-Xmx選項進行設置。

來源

2014-12-19 12:23:13

謝謝Christof。調用垃圾收集器可以改善這個問題。但是，當我使用context/solver的單個實例（而不是在每次迭代中創建一個實例）並調用'push' /'pop'時，程序突然顯示低內存配置文件。這似乎解決了我的問題，但它可能表明Java API泄漏？ – Dan 2014-12-20 02:37:08

不知道我明白。使用增量求解器（即使用push/pop）會影響求解器的行爲;在很多情況下，Z3切換到一個完全不同的求解器，它支持增量求解（對於一個特定的查詢通常較慢，但有時更快）。有些事情會在呼叫push/pop（例如，符號）的過程中持續存在，這就是你所說的泄漏？ – 2014-12-29 12:12:24

使用push/pop工作正常，因爲它不會耗盡內存。創建一個新的求解器並在一次查詢後處理它很快就會耗盡內存（即使調用了垃圾回收器）。 – Dan 2014-12-29 21:31:11

Z3 Java API：何時配置表達式/ Z3對象？

回答

相關問題