From 9ddce6a186188f2a30595caad022dbf6cf3ae0f8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 30 Oct 2019 13:31:04 -0500 Subject: [PATCH] feat(check-cc): add statistics --- src/core/Sidekick_core.ml | 1 + src/msat-solver/Sidekick_msat_solver.ml | 1 + src/smtlib/Process.ml | 6 +++++- 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 4ceea0b0..eda7ceaa 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -328,6 +328,7 @@ module type SOLVER_INTERNAL = sig type solver = t val tst : t -> term_state + val stats : t -> Stat.t (** {3 Literals} diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index b72aadee..2d2492d0 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -193,6 +193,7 @@ module Make(A : ARG) let[@inline] cc (t:t) = Lazy.force t.cc let[@inline] tst t = t.tst + let stats t = t.stat let simplifier self = self.simp let simp_t self (t:Term.t) : Term.t = Simplify.normalize self.simp t diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index d3846cef..b38e3a6a 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -458,7 +458,11 @@ module Check_cc = struct let theory = Solver.mk_theory ~name:"cc-check" ~create_and_setup:(fun si -> - Solver.Solver_internal.on_cc_conflict si (check_conflict si)) + let n_calls = Stat.mk_int (Solver.Solver_internal.stats si) "check-cc.call" in + Solver.Solver_internal.on_cc_conflict si + (fun c -> + Stat.incr n_calls; + check_conflict si c)) () end