From 539186bfe6d89ee1211af7b71035d7244a61af2b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 22 Mar 2019 20:14:28 -0500 Subject: [PATCH] feat: modular statistics aggregate --- src/cc/Congruence_closure.ml | 11 ++++++- src/cc/Congruence_closure_intf.ml | 1 + src/main/main.ml | 2 +- src/smt/Solver.ml | 37 ++++++++--------------- src/smt/Solver.mli | 1 + src/smt/Stat.ml | 12 -------- src/smt/Theory_combine.ml | 26 +++++++++++----- src/smt/Theory_combine.mli | 2 +- src/util/Sidekick_util.ml | 1 + src/util/Stat.ml | 50 +++++++++++++++++++++++++++++++ src/util/Stat.mli | 26 ++++++++++++++++ 11 files changed, 121 insertions(+), 48 deletions(-) delete mode 100644 src/smt/Stat.ml create mode 100644 src/util/Stat.ml create mode 100644 src/util/Stat.mli diff --git a/src/cc/Congruence_closure.ml b/src/cc/Congruence_closure.ml index 33ddee83..c7993033 100644 --- a/src/cc/Congruence_closure.ml +++ b/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 ( diff --git a/src/cc/Congruence_closure_intf.ml b/src/cc/Congruence_closure_intf.ml index dc444544..02aa2418 100644 --- a/src/cc/Congruence_closure_intf.ml +++ b/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] -> diff --git a/src/main/main.ml b/src/main/main.ml index e2cb6869..7dda80f6 100644 --- a/src/main/main.ml +++ b/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; diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml index 0a50d2b0..76b5dad0 100644 --- a/src/smt/Solver.ml +++ b/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 th_combine = Theory_combine.create() in +let create ?(stat=Stat.global) ?size ?(config=Config.empty) ?store_proof ~theories () : t = + 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 = - Format.fprintf out - "(@[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 pp_stats out (self:t) : unit = + Stat.pp_all out (Stat.all @@ stats self) 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"); diff --git a/src/smt/Solver.mli b/src/smt/Solver.mli index 83adee9a..fea5cdd5 100644 --- a/src/smt/Solver.mli +++ b/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 -> diff --git a/src/smt/Stat.ml b/src/smt/Stat.ml deleted file mode 100644 index 26ef5a1a..00000000 --- a/src/smt/Stat.ml +++ /dev/null @@ -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; -} diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index 1cce41b5..cfa77267 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -23,12 +23,13 @@ type theory_state = (* TODO: first-class module instead *) type t = { - tst: Term.state; - (** state for managing terms *) - cc: CC.t lazy_t; - (** congruence closure *) - mutable theories : theory_state list; - (** Set of theories *) + tst: Term.state; (** state for managing terms *) + cc: CC.t lazy_t; (** congruence closure *) + stat: Stat.t; + count_axiom: int Stat.counter; + count_conflict: int Stat.counter; + 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 diff --git a/src/smt/Theory_combine.mli b/src/smt/Theory_combine.mli index 532f20e2..f470a3ce 100644 --- a/src/smt/Theory_combine.mli +++ b/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 diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml index 76ae82b9..7b216231 100644 --- a/src/util/Sidekick_util.ml +++ b/src/util/Sidekick_util.ml @@ -10,3 +10,4 @@ module Error = Error module IArray = IArray module Intf = Intf module Bag = Bag +module Stat = Stat diff --git a/src/util/Stat.ml b/src/util/Stat.ml new file mode 100644 index 00000000..b6d69d72 --- /dev/null +++ b/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() diff --git a/src/util/Stat.mli b/src/util/Stat.mli new file mode 100644 index 00000000..6ea3846b --- /dev/null +++ b/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 *)