Z3统计中的内存使用单位是什么？答案

【问题标题】：What is the unit of memory usage in Z3 statistics?Z3统计中的内存使用单位是什么？
【发布时间】：2014-07-29 03:28:28
【问题描述】：

在 z3 统计中测量内存使用的单位是什么？是 MB 还是 KB？

记忆究竟意味着什么？是执行期间的最大内存使用量还是所有分配的总和？

【问题讨论】：

标签： z3 smt

【解决方案1】：

它是执行期间最大堆大小的近似值，并通过 cmd_context.cpp 中的以下函数添加到统计对象中：

void cmd_context::display_statistics(...) {
    statistics st;
    ...
    unsigned long long mem = memory::get_max_used_memory();
    ...
    st.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
    ...
}

因此它以 MB 为单位。但这只是一个近似值，因为计数器不会在每次分配时更新；请参阅 memory_manager.cpp 中的以下注释：

// We only integrate the local thread counters with the global one
// when the local counter > SYNCH_THRESHOLD 
#define SYNCH_THRESHOLD 100000

【讨论】：

感谢您的回复。我实际上试图探索代码以找出将其添加到统计信息中的确切位置，但找不到。
截至今天，我认为相关代码位于github.com/Z3Prover/z3/blob/… 另外，请注意，这些不是兆字节 (MB)，而是兆字节（MiB，过去含糊不清也是 MB）。