OCamlPro
add a flag to print the solver statistics
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 -> (
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?
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 ?
This is already available in smtml. We would just need to collect solver statistics and merge them at the end