some stats for the SAT solver

src/main/main.ml

@@ -142,21 +142,19 @@ let main_smt ~dot_proof () : _ result =
   res
 
 let main_cnf () : _ result =
-  let n_decision = ref 0 in
-  let n_confl = ref 0 in
+  let module S = Pure_sat_solver 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)
+    S.SAT.create
       ~on_new_atom:(fun _ -> incr n_atoms)
       ~size:`Big ()
   in
-  Pure_sat_solver.Dimacs.parse_file solver !file >>= fun () ->
-  let r = Pure_sat_solver.solve solver in
+  S.Dimacs.parse_file solver !file >>= fun () ->
+  let r = S.solve solver in
   if !p_stat then (
-    Fmt.printf "; n-atoms: %d n-conflicts: %d n-decisions: %d@."
-      !n_atoms !n_confl !n_decision;
+    Fmt.printf "; n-conflicts: %d n-decisions: %d n-propagations: %d n-atoms: %d@."
+      (S.SAT.n_conflicts solver) (S.SAT.n_decisions solver)
+      (S.SAT.n_propagations solver) !n_atoms;
   );
   r
 

src/sat/Solver.ml

@@ -779,6 +779,10 @@ module Make(Plugin : PLUGIN)
     mutable on_conflict : (atom array -> unit) option;
     mutable on_decision : (atom -> unit) option;
     mutable on_new_atom: (atom -> unit) option;
+
+    mutable n_conflicts : int;
+    mutable n_propagations : int;
+    mutable n_decisions : int;
   }
   type solver = t
 
@@ -817,6 +821,10 @@ module Make(Plugin : PLUGIN)
     var_incr = 1.;
     clause_incr = 1.;
     store_proof;
+
+    n_conflicts = 0;
+    n_decisions = 0;
+    n_propagations = 0;
     on_conflict = None;
     on_decision= None;
     on_new_atom = None;
@@ -833,9 +841,13 @@ module Make(Plugin : PLUGIN)
     self.on_conflict <- on_conflict;
     self
 
-  let[@inline] nb_clauses st = Vec.size st.clauses_hyps
   let[@inline] decision_level st = Vec.size st.var_levels
 
+  let[@inline] nb_clauses st = Vec.size st.clauses_hyps
+  let n_propagations self = self.n_propagations
+  let n_decisions self = self.n_decisions
+  let n_conflicts self = self.n_conflicts
+
   (* Do we have a level-0 empty clause? *)
   let[@inline] check_unsat_ st =
     match st.unsat_at_0 with
@@ -1487,6 +1499,7 @@ module Make(Plugin : PLUGIN)
           self.elt_head <- Vec.size self.trail;
           raise_notrace (Conflict c)
         ) else (
+          self.n_propagations <- 1 + self.n_propagations;
           enqueue_bool self first ~level:(decision_level self) (Bcp c)
         );
         Watch_kept
@@ -1585,6 +1598,7 @@ module Make(Plugin : PLUGIN)
           Clause.make_removable (p :: l) (Lemma proof)
         ) in
         let level = decision_level self in
+        self.n_propagations <- 1 + self.n_propagations;
         enqueue_bool self p ~level (Bcp_lazy c)
       )
 
@@ -1745,6 +1759,7 @@ module Make(Plugin : PLUGIN)
       new_decision_level self;
       let current_level = decision_level self in
       enqueue_bool self atom ~level:current_level Decision;
+      self.n_decisions <- 1 + self.n_decisions;
       (match self.on_decision with Some f -> f atom | None -> ());
     )
 
@@ -1793,6 +1808,7 @@ module Make(Plugin : PLUGIN)
         ) else (
           add_clause_ st confl
         );
+        st.n_conflicts <- 1 + st.n_conflicts;
         (match st.on_conflict with Some f -> f confl.atoms | None -> ());
 
       | None -> (* No Conflict *)
@@ -1863,6 +1879,7 @@ module Make(Plugin : PLUGIN)
                 Array.iter (fun a -> insert_var_order self (Atom.var a)) c.atoms;
                 Log.debugf 5 (fun k -> k "(@[sat.theory-conflict-clause@ %a@])"
                                  (Clause.debug self.store) c);
+                self.n_conflicts <- 1 + self.n_conflicts;
                 (match self.on_conflict with Some f -> f c.atoms | None -> ());
                 Vec.push self.clauses_to_add c;
                 flush_clauses self;

src/sat/Solver_intf.ml

@@ -444,5 +444,9 @@ module type S = sig
 
   val eval_atom : t -> atom -> lbool
   (** Evaluate atom in current state *)
+
+  val n_propagations : t -> int
+  val n_decisions : t -> int
+  val n_conflicts : t -> int
 end