z3 - 监控 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。该方法在每次重启后执行。