Add statistics output for long-running computations

[konnov]

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.