监控z3内存使用特征

Question

我有一些约束，z3需要很长时间才能解决。我知道打印统计信息的"-st“命令行标志，以及打印内部数据结构值的跟踪工具。有没有办法从z3中获取诊断信息(例如，当从命令行使用它时，当它正在运行时(像ps这样的外部工具并不总是方便的，也不总是服务于目的)，是否可以持续监视内存使用情况？谢谢。

Answer 1

您可以使用选项-v:100，它会将详细级别设置为100。它可能不会像您希望的那样频繁地显示内存使用情况。另一种选择是在适当的位置添加以下代码行。

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

如果详细级别为>= 3，它将显示内存使用情况。例如，一个好的位置是在src/smt/smt_context.cpp的方法lbool context::bounded_search()的开头。此方法在每次重新启动后执行。