add a flag to print the solver statistics

[epatrizio]

fixes #184

[epatrizio]

Command line example :

dune exec owi -- sym ./test/sym/table.wat --no-stop-at-failure --print-solver-statistics

Display :

(decisions 3)                          
(propagations 62)
(final checks 1)
(mk clause 98)
(num checks 1)
(mk bool var 66)
(arith-make-feasible 1)
(arith-max-columns 4)
(num allocs 149343)
(rlimit count 240)
(max memory 84.94)
(memory 68.2)(decisions 3)
(propagations 129)
(final checks 2)
(added eqs 5)
(mk clause 199)
(del clause 98)
(num checks 2)
(mk bool var 169)
(arith-make-feasible 2)
(arith-max-columns 4)
(bv bit2core 32)
(num allocs 153416)
(rlimit count 665)
(max memory 84.94)
(memory 68.3)(decisions 34)
(propagations 197)
(final checks 3)
(added eqs 8)
(mk clause 302)
(del clause 199)
(num checks 3)
(mk bool var 272)
(arith-make-feasible 3)
(arith-max-columns 4)
(bv dynamic diseqs 2)
(bv bit2core 32)
(bv->core eq 1)
(num allocs 153416)
(rlimit count 1350)
(max memory 84.94)
(memory 68.3)Trap: unreachable
Model:
  (model
    (symbol_0 (i32 0))
    (symbol_1 (i32 0)))
Trap: undefined element
Model:
  (model
    (symbol_0 (i32 0))
    (symbol_1 (i32 -2147483648)))
Reached 2 problems!

Does the Owi.Solver.pp_statistics function need to be improved?

let pp_statistics solver =
  Z3Batch.pp_statistics Stdlib.Format.std_formatter solver;
  Stdlib.Format.pp_print_flush Stdlib.Format.std_formatter ()

[krtab]

Thanks!

Before merging, I think we must check and clarify what statistics are displayed exactly. If there is n worker threads, then there is a total of n+1 solver objects. One for each worker thread and one in the main thread (the one you're using). I don't know whether the statistics are computed by z3 for all solver objects combined or only for each one (my guess is that it is only for each one). If it is only for each one, the meaningful thing to do would be combining all these statistics as one, and display that.

[krtab]

Could you rebase on #199?

[zapashcanon]

I'm wondering if we would like to merge this with the --profiling flag ?

[filipeom]

I don't know whether the statistics are computed by z3 for all solver objects combined or only for each one (my guess is that it is only for each one).

To clarify, what pp_statistics does is print the statistics related to each solver object (Your guess is correct). You can confirm this looking at the number of solver checks printed in the output Eric gave. The maximum is (num checks 3) which only represents the checks done for by the solver in the main thread.

If it is only for each one, the meaningful thing to do would be combining all these statistics as one, and display that.

It doesn't seem trivial to do here because a solver object allocated in a thread will be collected when the thread finishes (correct me if I'm wrong). Therefore, we would need to incrementally combine solver statistics as threads finish.

[epatrizio]

I'm wondering if we would like to merge this with the --profiling flag ?

dune exec owi -- sym ./test/sym/table.wat --no-stop-at-failure --profiling

displays :

Exec module anonymous                  
enter 1
intrs 5
Exec module anonymous
enter 1
intrs 1
calls
  id 0 start
    enter 1
    intrs 3
    calls
      id 1 f
        enter 1
        intrs 3
Trap: undefined element
Model:
  (model
    (symbol_0 (i32 0))
    (symbol_1 (i32 -2147483648)))
Trap: unreachable
Model:
  (model
    (symbol_0 (i32 0))
    (symbol_1 (i32 0)))
(decisions 34)
(propagations 197)
(final checks 3)
(added eqs 8)
(mk clause 302)
(del clause 201)
(num checks 3)
(mk bool var 272)
(arith-make-feasible 3)
(arith-max-columns 4)
(bv dynamic diseqs 2)
(bv bit2core 32)
(bv->core eq 1)
(num allocs 153329)
(rlimit count 1350)
(max memory 85.6)
(memory 68.3)
Reached 2 problems!%

[krtab]

It doesn't seem trivial to do here because a solver object allocated in a thread will be collected when the thread finishes (correct me if I'm wrong). Therefore, we would need to incrementally combine solver statistics as threads finish.

Though not trivial, it shouldn't be too hard either. There is one solver per worker, and a defined number of workers. At least in the nominal case where no worker encounters an unrecoverable error, it should be doable for each worker too record its own solver's statistics somewhere and for the main thread to collect these aggregated statistics once every worker is finished.

This depends of formalsec/encoding#85 to be done but there is always the possibility of doing it "dirty" by simply parsing the output so we should manage to get something that works anyway.

[zapashcanon]

I would be for merging as this is clearly a clear improvement when used with -w1. It may give weird/hard to understand results in a parallel run but we could fix this later if we end up needing it, what do you think @krtab ?

@epatrizio, could you rebase please?

[krtab]

I think that even with -w1 the results are meaningless. -w1 doesn't deactivate the multicore monad, it simply spans only one worker iirc.

[zapashcanon]

Oh so, even inside a single worker, the Z3 statistics are not shared? If that's the case, yes indeed, we should probably wait before merging.

[zapashcanon]

I'm closing this one. We'll need to gather all solver statistics and merge them somehow.