Z3 statistics meaning

1
votes

I was wondering if somebody could tell me what the following Z3 statistics mean.

(:add-rows        2
 :arith-conflicts 1
 :assert-lower    2
 :assert-upper    1
 :conflicts       1
 :max-memory      0.43
 :memory          0.43
 :mk-bool-var     4
 :num-allocs      6961
 :num-checks      1
 :pivots          2
 :rlimit-count    115
 :time            0.00)

Thanks.

1
statisticsz3

1 Answers

0
votes

I don't believe the meaning of these statistics is well documented. Your best bet would be to actually read through the source code if you want to study them in any detail. You can start here: https://github.com/Z3Prover/z3/blob/ca498e20d17457b4baa32578a94923cf8e3e105c/src/smt/theory_lra.cpp#L3527-L3554

Some of these are well known "statistics" in the SMT-literature, like conflicts. (Essentially a measure of how many times the solver had to backtrack.) Others are entirely solver specific, like mk-bool-var.

SMTLib itself specifies some statistics; see Section 3.9.2 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf But the actual meaning is largely left to implementations and can vary from solver to solver.

If you're curious about a particular one, I'd recommend asking about it directly at the z3 github repo: https://github.com/Z3Prover/z3