From 97aab34e466d5e8c65f400b19bb88a58a385fe59 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 19 Jul 2021 09:56:51 -0400
Subject: [PATCH] statistics for pure sat solver

---
 src/main/main.ml            | 18 ++++++++++++++++--
 src/main/pure_sat_solver.ml |  1 +
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/main/main.ml b/src/main/main.ml
index 15a7eae7..0c10a6fd 100644
--- a/src/main/main.ml
+++ b/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 () =
 
diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml
index 14f79638..da8e094d 100644
--- a/src/main/pure_sat_solver.ml
+++ b/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 ()
+