Add statistics output for long-running computations
konnov opened this issue · 0 comments
konnov commented
The CLI version of Z3 supports periodic statistics, e.g.,
z3 verbose=3 stats=true log0.smt
(smt.searching)
(smt.stats :restarts :decisions :clauses/bin/units :simplify :memory)
(smt.stats :conflicts :propagations :lemmas :deletions )
(smt.stats 0 0 0 0 57037/36291/2996 0 0 0 112.35)
(smt.stats 0 101 2582 59179 53338/38652/3333 4024/7 2 6060 114.77)
(smt.stats 1 203 3491 115174 53338/38652/3334 7931/8 3 6060 115.55)
(smt.stats 2 306 3871 172926 53338/38652/3334 9623/8 3 6060 115.74)
(smt.stats 3 410 4388 210481 53338/38652/3334 12109/8 3 6060 116.03)
(smt.stats 4 515 4830 302266 53339/38653/3336 15435/18 4 6060 116.53)
(smt.stats 5 621 5329 315379 53339/38653/3336 15702/23 5 6060 116.53)
(smt.stats :restarts :decisions :clauses/bin/units :simplify :memory)
(smt.stats :conflicts :propagations :lemmas :deletions )
(smt.stats 6 728 5680 322192 53339/38653/3336 15880/23 5 6060 116.53)
(smt.stats 7 836 6160 344447 53339/38653/3336 16971/23 5 6060 116.62)
(smt.stats 8 945 6641 394437 53342/38656/3336 18899/23 5 6060 116.91)We should be able to print something similar in detailed.log, e.g., when the user increases the verbosity level. Otherwise, it is impossible to get any idea about what is going on inside z3 for hours or days.