z3统计中内存使用量的单位是什么?是MB还是KB?
内存到底是什么意思?是最大内存使用量还是执行过程中所有分配的总和?
最佳答案
它是执行期间最大堆大小的近似值,它通过 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
关于z3 - Z3统计中内存使用的单位是什么?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25007806/