From 2000114ab48a266f6e6a1fbc3ed05bc65c74f4da Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 7 Jun 2019 13:27:03 -0500
Subject: [PATCH] feat: add more stats

---
 src/cc/Sidekick_cc.ml                   |  3 +++
 src/msat-solver/Sidekick_msat_solver.ml | 21 ++++++++++++++-------
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 4bb16b44..ff04c1e9 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -221,6 +221,7 @@ module Make(CC_A: ARG) = struct
     false_ : node lazy_t;
     stat: Stat.t;
     count_conflict: int Stat.counter;
+    count_props: int Stat.counter;
     count_merge: int Stat.counter;
   }
   (* TODO: an additional union-find to keep track, for each term,
@@ -707,6 +708,7 @@ module Make(CC_A: ARG) = struct
              let e = lazy (explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1) in
              fun () -> Lazy.force e
            in
+           Stat.incr cc.count_props;
            CC_A.Actions.propagate acts lit ~reason CC_A.A.Proof.default
          | _ -> ())
 
@@ -831,6 +833,7 @@ module Make(CC_A: ARG) = struct
       false_;
       stat;
       count_conflict=Stat.mk_int stat "cc.conflicts";
+      count_props=Stat.mk_int stat "cc.propagations";
       count_merge=Stat.mk_int stat "cc.merges";
     } and true_ = lazy (
         add_term cc (T.bool tst true)
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index 16af306b..de56191c 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -109,6 +109,7 @@ module Make(A : ARG)
       cc: CC.t lazy_t; (** congruence closure *)
       stat: Stat.t;
       count_axiom: int Stat.counter;
+      count_preprocess_clause: int Stat.counter;
       count_conflict: int Stat.counter;
       count_propagate: int Stat.counter;
       simp: Simplify.t;
@@ -182,13 +183,17 @@ module Make(A : ARG)
                   T.pp t T.pp u);
             aux u
       in
-      let t = aux (Lit.term lit) in
+      let t = Lit.term lit |> simp_t self |> aux in
+      let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
       Log.debugf 10
-        (fun k->k "(@[msat-solver.preprocess@ :lit %a@ :into %a@])" Lit.pp lit T.pp t);
-      Lit.atom self.tst ~sign:(Lit.sign lit) t
+        (fun k->k "(@[msat-solver.preprocess@ :lit %a@ :into %a@])" Lit.pp lit Lit.pp lit');
+      lit'
 
     let[@inline] mk_lit self acts ?sign t =
-      let add_clause lits = add_sat_clause_ self acts ~keep:true lits in
+      let add_clause lits =
+        Stat.incr self.count_preprocess_clause;
+        add_sat_clause_ self acts ~keep:true lits
+      in
       preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t
 
     let[@inline] add_clause_temp self acts lits : unit =
@@ -296,9 +301,10 @@ module Make(A : ARG)
         simp=Simplify.create tst;
         preprocess=[];
         preprocess_cache=T.Tbl.create 32;
-        count_axiom = Stat.mk_int stat "th-axioms";
-        count_propagate = Stat.mk_int stat "th-propagations";
-        count_conflict = Stat.mk_int stat "th-conflicts";
+        count_axiom = Stat.mk_int stat "solver.th-axioms";
+        count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause";
+        count_propagate = Stat.mk_int stat "solver.th-propagations";
+        count_conflict = Stat.mk_int stat "solver.th-conflicts";
         on_partial_check=[];
         on_final_check=[];
       } in
@@ -420,6 +426,7 @@ module Make(A : ARG)
       Solver_internal.preprocess_lit_
         ~add_clause:(fun lits ->
             (* recursively add these sub-literals, so they're also properly processed *)
+            Stat.incr self.si.count_preprocess_clause;
             let atoms = List.map (mk_atom_lit self) lits in
             Sat_solver.add_clause self.solver atoms A.Proof.default)
         self.si lit in