simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(stat): improve printing api

Browse source
This commit is contained in:
Simon Cruanes 2022-08-13 13:45:21 -04:00
parent eddbf139fc
commit 63802fe3d6
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
4 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/main/main.ml
View file

@ -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 () ->

2
src/smt/solver.ml
View file

@ -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 =

3
src/util/Stat.ml
View file

@ -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 ()

3
src/util/Stat.mli
View file

@ -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 *)