statistics for pure sat solver

src/main/main.ml

@@ -142,9 +142,23 @@ let main_smt ~dot_proof () : _ result =
   res
 
 let main_cnf () : _ result =
-  let solver = Pure_sat_solver.SAT.create ~size:`Big () in
+  let n_decision = ref 0 in
+  let n_confl = ref 0 in
+  let n_atoms = ref 0 in
+  let solver =
+    Pure_sat_solver.SAT.create
+      ~on_conflict:(fun _ -> incr n_confl)
+      ~on_decision:(fun _ -> incr n_decision)
+      ~on_new_atom:(fun _ -> incr n_atoms)
+      ~size:`Big ()
+  in
   Pure_sat_solver.Dimacs.parse_file solver !file >>= fun () ->
-  Pure_sat_solver.solve solver
+  let r = Pure_sat_solver.solve solver in
+  if !p_stat then (
+    Fmt.printf "; n-atoms: %d n-conflicts: %d n-decisions: %d@."
+      !n_atoms !n_confl !n_decision;
+  );
+  r
 
 let main () =
 

src/main/pure_sat_solver.ml

@@ -56,3 +56,4 @@ let solve (solver:SAT.t) : (unit, string) result =
       Format.printf "Unsat (%.3f/%.3f)@." t2 t3;
   end;
   Ok ()
+