如何找到在 Z3py 中建模/检查可满足性所消耗的内存？

Question

我正在使用 z3py。我正在尝试检查不同大小的不同问题的可满足性，并验证所提出方法的可扩展性。但是，要做到这一点，我需要知道求解器为每个问题消耗的内存。有没有办法访问内存或让 z3py 在 STATISTICS 部分打印它。非常感谢您。

2015 年 5 月 27 日更新：

我尝试使用 paython 内存分析器，但生成的内存似乎非常大。我不确定，但报告的内存类似于python应用程序消耗的内存，而不仅仅是Z3（构建z3模型并检查sat然后生成模型）。此外，我使用形式化建模检查工具已经很多年了。我期待 Z3 更高效并且具有更好的可扩展性，但是，我获得的内存比 paython 生成的内存要少得多。 我想做的是尝试使用内存以外的因素来衡量设计大小或可伸缩性。在 z3py 统计中，会生成许多详细信息来描述设计大小和复杂性。但是，我无法在教程、网页或 z3 论文中找到对这些参数的任何解释。 例如，您能帮我理解在统计中为我拥有的一种基本模型生成的以下参数吗？还有任何参数/参数可以替换内存或很好地指示 Z3 mdoel 大小/复杂性。

• ：添加-eqs 152
• :assert-lower 2
• :assert-upper 2
• ：二进制传播 59
• :冲突 6
• :datatype-accessor-ax 12
• :datatype-constructor-ax 14
• :datatype-occurs-check 19
• :datatype-splits 12
• ：决定 35
• :del-clause 2
• :eq 适配器 2
• :final-checks 1
• :mk 条款 9
• :offset-eqs 2
• :传播 61

再次感谢您的宝贵时间。

Answer 1

Z3 近似于全局最大内存使用量，但它没有用于跟踪特定 API 调用的内存使用量的工具。在全局内存使用量减少的情况下，这还不够（例如，它应该是负数吗？）。我认为像 Python memory_profiler 这样的外部工具会做得更好。

更新后的问题是一个反复出现的问题，请参阅这些较早的答案：Interpretation of Z3 Statistics、What is the unit of memory usage in Z3 statistics?、Z3 statistics: what does time measure?、Z3 real arithmetic and statistics、Statistics in Z3、How to get statistics in Z3 3.2?。

Answer 2

我在不稳定分支中添加了内存消耗统计信息。 所以现在你应该能够从统计数据中访问这些信息 由 Z3 返回。