add a flag to print the solver statistics

[zapashcanon]

the quick&dirty way to do it for reference:

diff --git a/src/symbolic_choice.ml b/src/symbolic_choice.ml
index e799358..534a023 100644
--- a/src/symbolic_choice.ml
+++ b/src/symbolic_choice.ml
@@ -19,7 +19,10 @@ let check sym_bool thread (S (solver_module, solver)) =
   | _ ->
     let check = no :: pc in
     let module Solver = (val solver_module) in
+
     let r = Solver.check solver check in
+        Solver.pp_statistics Stdlib.Format.std_formatter solver;
+        Stdlib.Format.pp_print_flush Stdlib.Format.std_formatter ();
     not r

 let list_select b ({ Thread.pc; _ } as thread) (S (solver_module, s)) =
@@ -34,6 +37,9 @@ let list_select b ({ Thread.pc; _ } as thread) (S (solver_module, s)) =
     let with_not_v = Bool.not v :: pc in
     let sat_true = Solver.check s with_v in
     let sat_false = Solver.check s with_not_v in
+
+        Solver.pp_statistics Stdlib.Format.std_formatter s;
+        Stdlib.Format.pp_print_flush Stdlib.Format.std_formatter ();
     match (sat_true, sat_false) with
     | false, false -> []
     | true, false | false, true -> [ (sat_true, thread) ]
@@ -78,6 +84,8 @@ let list_select_i32 sym_int thread (S (solver_module, solver)) =
       if not (Solver.check solver (additionnal @ pc)) then []
       else begin
         let model = Solver.model ~symbols:[ symbol ] solver in
+        Solver.pp_statistics Stdlib.Format.std_formatter solver;
+        Stdlib.Format.pp_print_flush Stdlib.Format.std_formatter ();
         match model with
         | None -> assert false (* ? *)
         | Some model -> (

[filipeom]

Where would printing the solver statistics make more sense? In this example you're doing it after each solver interaction. I was thinking it might be more appropriate at the end of the analysis, with all the stats accumulated. However, considering that the solver is part of the multi-threaded choice monad, gathering the statistics of every spawned solver may not be straightforward. What do you think?

[epatrizio]

For now, statistics are displayed after Solver.get_model call.

[zapashcanon]

I believe we should start by trying to have a proper type of solver statistics into Smt.ml and then have a way to "add" two of them, WDYT @filipeom ?

[filipeom]

This is already available in smtml. We would just need to collect solver statistics and merge them at the end

[zapashcanon]

Oh, I didn't know that!

[filipeom]

I'll take a look into this, if it's quick I can make a PR to address this