監視z3內存使用特徵

Question

我有一些約束z3需要很長時間才能解決。我知道打印統計數據的「-st」命令行標誌，但最終還是打印出內部數據結構值的TRACE工具。是否有一種方法可以從z3中獲取診斷信息（例如，持續監視內存使用情況），因爲它正在運行（像ps這樣的外部工具並不總是方便，並不總是用於此目的）命令行？謝謝。

Answer 1

您可以使用選項-v:100，它將詳細級別設置爲100.它可能不會仍然顯示內存使用情況。 另一種選擇是在適當的位置添加以下代碼行。

timeit tt(get_verbosity_level() >= 3, "report"); 

如果詳細級別爲>= 3，它將顯示內存使用情況。 例如，一個好的地方是在lbool context::bounded_search()的方法src/smt/smt_context.cpp的開頭。此方法在每次重新啓動後執行。