diff --git a/src/main/main.ml b/src/main/main.ml index a89f5018..ca6f432d 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -211,7 +211,7 @@ let main_cnf () : _ result = let stat = Stat.create () in let finally () = - if !p_stat then Fmt.printf "%a@." Stat.pp_all (Stat.all stat); + if !p_stat then Fmt.printf "%a@." Stat.pp stat; Proof.close proof in CCFun.protect ~finally @@ fun () -> diff --git a/src/smt/solver.ml b/src/smt/solver.ml index 4b2aa8ab..4c6be1ca 100644 --- a/src/smt/solver.ml +++ b/src/smt/solver.ml @@ -134,7 +134,7 @@ let mk_lit_t (self : t) ?sign (t : term) : lit = (** {2 Main} *) -let pp_stats out (self : t) : unit = Stat.pp_all out (Stat.all @@ stats self) +let pp_stats out (self : t) : unit = Stat.pp out (stats self) (* add [c], without preprocessing its literals *) let add_clause_nopreproc_ (self : t) (c : lit array) (proof : step_id) : unit = diff --git a/src/util/Stat.ml b/src/util/Stat.ml index d81b30c6..f024a9f0 100644 --- a/src/util/Stat.ml +++ b/src/util/Stat.ml @@ -37,11 +37,12 @@ let[@inline] incr x = x.count <- 1 + x.count let[@inline] incr_f x by = x.count <- by +. x.count let[@inline] set c x : unit = c.count <- x -let pp_all out l = +let pp_counters 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.(iter ~sep:(return "@ ") pp_w) l +let pp out (self : t) = pp_counters out @@ all self let global = create () diff --git a/src/util/Stat.mli b/src/util/Stat.mli index c3da800c..53945c43 100644 --- a/src/util/Stat.mli +++ b/src/util/Stat.mli @@ -18,7 +18,8 @@ type ex_counter (** Existential counter *) val all : t -> ex_counter Iter.t -val pp_all : ex_counter Iter.t Fmt.printer +val pp_counters : ex_counter Iter.t Fmt.printer +val pp : t Fmt.printer val global : t (** Global statistics, by default *)