Z3统计中的内存使用单位是什么? [英] What is the unit of memory usage in Z3 statistics?

问题描述

z3 统计中衡量内存使用的单位是什么?是 MB 还是 KB?

What is the unit in which memory usage is measured in z3 statistics? Is it MB or KB?

内存到底是什么意思?是最大内存使用量还是执行过程中所有分配的总和?

And what does the memory exactly means? Is it the maximum memory usage or the aggregate sum of all allocations during the execution?

推荐答案

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

It's an approximation of the maximum heap size during execution and it is added to the statistics object through the following function in 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 中的以下注释:

Thus it is in MB. It is only an approximation though, because the counters are not updated at every allocation; see the following comment in memory_manager.cpp:

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

这篇关于Z3统计中的内存使用单位是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！