3

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?

Mohammed
  • 134
  • 6

1 Answers1

2

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));
    ...
}

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
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • Thanks for your reply. I actually tried to explore the code to find out where exactly it is added to the statistics, but could not find it. – Mohammed Jul 30 '14 at 08:08
  • As of today, I think the relevant code is at https://github.com/Z3Prover/z3/blob/8a229bf684b1e2abc2276814a03182a36a8c6e96/src/util/statistics.cpp#L234-L242 Also, note that these are not megabytes (MB) but mebibytes (MiB, in the past ambiguously also MB). – Lorenz Leutgeb Jan 28 '21 at 08:49