feat: modular statistics aggregate

src/cc/Congruence_closure.ml

@@ -334,6 +334,9 @@ module Make(A: ARG) = struct
     (* pairs to explain *)
     true_ : node lazy_t;
     false_ : node lazy_t;
+    stat: Stat.t;
+    count_conflict: int Stat.counter;
+    count_merge: int Stat.counter;
   }
   (* TODO: an additional union-find to keep track, for each term,
      of the terms they are known to be equal to, according
@@ -459,6 +462,7 @@ module Make(A: ARG) = struct
     Vec.clear cc.pending;
     Vec.clear cc.combine;
     let c = List.rev_map A.Lit.neg e in
+    Stat.incr cc.count_conflict;
     acts.Msat.acts_raise_conflict c A.Proof.default
 
   let[@inline] all_classes cc : repr Iter.t =
@@ -717,6 +721,7 @@ module Make(A: ARG) = struct
     if not @@ N.equal ra rb then (
       assert (N.is_root ra);
       assert (N.is_root rb);
+      Stat.incr cc.count_merge;
       (* check we're not merging [true] and [false] *)
       if (N.equal ra (true_ cc) && N.equal rb (false_ cc)) ||
          (N.equal rb (true_ cc) && N.equal ra (false_ cc)) then (
@@ -1005,7 +1010,8 @@ module Make(A: ARG) = struct
 
   let on_merge cc f = cc.on_merge <- f :: cc.on_merge
 
-  let create ?th:(theories=[]) ?(on_merge=[]) ?(size=`Big) (tst:term_state) : t =
+  let create ?(stat=Stat.global)
+      ?th:(theories=[]) ?(on_merge=[]) ?(size=`Big) (tst:term_state) : t =
     let size = match size with `Small -> 128 | `Big -> 2048 in
     let rec cc = {
       tst;
@@ -1020,6 +1026,9 @@ module Make(A: ARG) = struct
       ps_queue=Vec.create();
       true_;
       false_;
+      stat;
+      count_conflict=Stat.mk_int stat "cc.conflicts";
+      count_merge=Stat.mk_int stat "cc.merges";
     } and true_ = lazy (
         add_term cc (T.bool tst true)
       ) and false_ = lazy (

src/cc/Congruence_closure_intf.ml

@@ -151,6 +151,7 @@ module type S = sig
   end
 
   val create :
+    ?stat:Stat.t ->
     ?th:Theory.t list ->
     ?on_merge:(t -> N.t -> N.t -> Expl.t -> unit) list ->
     ?size:[`Small | `Big] ->

src/main/main.ml

@@ -152,7 +152,7 @@ let main () =
       E.return()
   in
   if !p_stat then (
-    Format.printf "%a@." Sidekick_smt.Solver.pp_stats solver;
+    Format.printf "%a@." Solver.pp_stats solver;
   );
   if !p_gc_stat then (
     Printf.printf "(gc_stats\n%t)\n" Gc.print_stat;

src/smt/Solver.ml

@@ -23,6 +23,8 @@ module Proof = Sat_solver.Proof
 type t = {
   solver: Sat_solver.t;
   stat: Stat.t;
+  count_clause: int Stat.counter;
+  count_solve: int Stat.counter;
   config: Config.t
 }
 
@@ -35,14 +37,16 @@ let[@inline] tst self = Theory_combine.tst (th_combine self)
 
 let[@inline] mk_atom_lit self lit : Atom.t = Sat_solver.make_atom self.solver lit
 let[@inline] mk_atom_t self ?sign t : Atom.t =
-  let lit = Lit.atom (tst self)  ?sign t in
+  let lit = Lit.atom (tst self) ?sign t in
   mk_atom_lit self lit
 
-let create ?size ?(config=Config.empty) ?store_proof ~theories () : t =
+let create ?(stat=Stat.global) ?size ?(config=Config.empty) ?store_proof ~theories () : t =
-  let th_combine = Theory_combine.create() in
+  let th_combine = Theory_combine.create ~stat () in
   let self = {
     solver=Sat_solver.create ?store_proof ?size th_combine;
-    stat=Stat.create ();
+    stat;
+    count_clause=Stat.mk_int stat "input-clauses";
+    count_solve=Stat.mk_int stat "solve";
     config;
   } in
   (* now add the theories *)
@@ -54,17 +58,6 @@ let create ?size ?(config=Config.empty) ?store_proof ~theories () : t =
   ] Proof_default;
   self
 
-(** {2 Sat Solver} *)
-
-let print_progress (st:t) : unit =
-  Printf.printf "\r[%.2f] clauses %d | lemmas %d%!"
-    (get_time())
-    st.stat.Stat.num_clause_push
-    st.stat.Stat.num_clause_tautology
-
-let flush_progress (): unit =
-  Printf.printf "\r%-80d\r%!" 0
-
 (** {2 Toplevel Goals}
 
     List of toplevel goals to satisfy. Mainly used for checking purpose
@@ -155,16 +148,8 @@ let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Iter.t =
 let pp_term_graph _out (_:t) =
   ()
 
-let pp_stats out (s:t) : unit =
+let pp_stats out (self:t) : unit =
-  Format.fprintf out
+  Stat.pp_all out (Stat.all @@ stats self)
-    "(@[<hv1>stats@ \
-     :num_clause_push %d@ \
-     :num_clause_tautology %d@ \
-     :num_propagations %d@ \
-     @])"
-    s.stat.Stat.num_clause_push
-    s.stat.Stat.num_clause_tautology
-    s.stat.Stat.num_propagations
 
 let do_on_exit ~on_exit =
   List.iter (fun f->f()) on_exit;
@@ -187,6 +172,7 @@ let assume (self:t) (c:Lit.t IArray.t) : unit =
   let sat = solver self in
   IArray.iter (fun lit -> add_bool_subterms_ self @@ Lit.term lit) c;
   let c = IArray.to_array_map (Sat_solver.make_atom sat) c in
+  Stat.incr self.count_clause;
   Sat_solver.add_clause_a sat c Proof_default
 
 (* TODO: remove? use a special constant + micro theory instead?
@@ -205,6 +191,7 @@ let check_model (_s:t) : unit =
    (not the value depth limit) *)
 let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
   let r = Sat_solver.solve ~assumptions (solver self) in
+  Stat.incr self.count_solve;
   match r with
   | Sat_solver.Sat st ->
     Log.debugf 1 (fun k->k "SAT");

src/smt/Solver.mli

@@ -37,6 +37,7 @@ type t
 (** Solver state *)
 
 val create :
+  ?stat:Stat.t ->
   ?size:[`Big | `Tiny | `Small] ->
   ?config:Config.t ->
   ?store_proof:bool ->

src/smt/Stat.ml

@@ -1,12 +0,0 @@
-
-type t = {
-  mutable num_clause_push  : int;
-  mutable num_clause_tautology  : int;
-  mutable num_propagations  : int;
-}
-
-let create () : t = {
-  num_clause_push = 0;
-  num_clause_tautology = 0;
-  num_propagations = 0;
-}

src/smt/Theory_combine.ml

@@ -23,12 +23,13 @@ type theory_state =
 
 (* TODO: first-class module instead *)
 type t = {
-  tst: Term.state;
+  tst: Term.state; (** state for managing terms *)
-  (** state for managing terms *)
+  cc: CC.t lazy_t; (** congruence closure *)
-  cc: CC.t lazy_t;
+  stat: Stat.t;
-  (** congruence closure *)
+  count_axiom: int Stat.counter;
-  mutable theories : theory_state list;
+  count_conflict: int Stat.counter;
-  (** Set of theories *)
+  count_propagate: int Stat.counter;
+  mutable theories : theory_state list; (** Set of theories *)
 }
 
 let[@inline] cc (t:t) = Lazy.force t.cc
@@ -52,13 +53,18 @@ let assert_lits_ ~final (self:t) acts (lits:Lit.t Iter.t) : unit =
   CC.check cc acts;
   let module A = struct
     let cc = cc
-    let[@inline] raise_conflict c : 'a = acts.Msat.acts_raise_conflict c Proof_default
+    let[@inline] raise_conflict c : 'a =
+      Stat.incr self.count_conflict;
+      acts.Msat.acts_raise_conflict c Proof_default
     let[@inline] propagate p cs : unit =
+      Stat.incr self.count_propagate;
       acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), Proof_default))
     let[@inline] propagate_l p cs : unit = propagate p (fun()->cs)
     let[@inline] add_local_axiom lits : unit =
+      Stat.incr self.count_axiom;
       acts.Msat.acts_add_clause ~keep:false lits Proof_default
     let[@inline] add_persistent_axiom lits : unit =
+      Stat.incr self.count_axiom;
       acts.Msat.acts_add_clause ~keep:true lits Proof_default
     let[@inline] add_lit lit : unit = acts.Msat.acts_mk_lit lit
   end in
@@ -120,7 +126,7 @@ let mk_model (self:t) lits : Model.t =
 (** {2 Main} *)
 
 (* create a new theory combination *)
-let create () : t =
+let create ?(stat=Stat.global) () : t =
   Log.debug 5 "th_combine.create";
   let rec self = {
     tst=Term.create ~size:1024 ();
@@ -130,6 +136,10 @@ let create () : t =
       CC.create ~size:`Big self.tst;
     );
     theories = [];
+    stat;
+    count_axiom = Stat.mk_int stat "th-axioms";
+    count_propagate = Stat.mk_int stat "th-propagations";
+    count_conflict = Stat.mk_int stat "th-conflicts";
   } in
   ignore (Lazy.force @@ self.cc : CC.t);
   self

src/smt/Theory_combine.mli

@@ -11,7 +11,7 @@ include Msat.Solver_intf.PLUGIN_CDCL_T
   with module Formula = Lit
    and type proof = Proof.t
 
-val create : unit -> t
+val create : ?stat:Stat.t -> unit -> t
 
 val cc : t -> CC.t
 val tst : t -> Term.state

src/util/Sidekick_util.ml

@@ -10,3 +10,4 @@ module Error = Error
 module IArray = IArray
 module Intf = Intf
 module Bag = Bag
+module Stat = Stat

src/util/Stat.ml

@@ -0,0 +1,50 @@
+
+(** {1 Statistics} *)
+
+module Fmt = CCFormat
+module S_map = CCMap.Make(String)
+
+type 'a counter = {
+  name: string;
+  mutable count: 'a;
+}
+
+type ex_counter =
+  | C_int : int counter -> ex_counter
+  | C_float : float counter -> ex_counter
+
+type t = {
+  mutable cs: ex_counter S_map.t;
+}
+
+let create() : t = {cs=S_map.empty}
+let register_ self name c = self.cs <- S_map.add name c self.cs
+let all (self:t) = S_map.values self.cs
+
+let mk_int self name =
+  match S_map.find name self.cs with
+  | C_int s -> s
+  | _ -> Error.errorf "incompatible types for stat %S" name
+  | exception Not_found ->
+    let c = {name; count=0} in
+    register_ self name (C_int c); c
+
+let mk_float self name =
+  match S_map.find name self.cs with
+  | C_float s -> s
+  | _ -> Error.errorf "incompatible types for stat %S" name
+  | exception Not_found ->
+    let c = {name; count=0.} in
+    register_ self name (C_float c); c
+
+let[@inline] incr x = x.count <- 1 + x.count
+let[@inline] incr_f x by = x.count <- by +. x.count
+
+let pp_all out l =
+  let pp_w out = function
+    | C_int {name; count} -> Fmt.fprintf out "@[:%s %d@]" name count
+    | C_float {name; count} -> Fmt.fprintf out "@[:%s %.4f@]" name count
+  in
+  Fmt.fprintf out "(@[stats@ %a@])" Fmt.(seq ~sep:(return "@ ") pp_w) l
+
+let global = create()

src/util/Stat.mli

@@ -0,0 +1,26 @@
+
+(** {1 Statistics} *)
+
+module Fmt = CCFormat
+
+type t
+
+val create : unit -> t
+
+type 'a counter
+
+val mk_int : t -> string -> int counter
+val mk_float : t -> string -> float counter
+
+val incr : int counter -> unit
+val incr_f : float counter -> float -> unit
+
+(** Existential counter *)
+type ex_counter
+
+val all : t -> ex_counter Iter.t
+
+val pp_all : ex_counter Iter.t Fmt.printer
+
+val global : t
+(** Global statistics, by default *)