From aa2060556740cd2c709e2616a849913cc8e774fe Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 16 Feb 2021 19:18:45 -0500 Subject: [PATCH] feat(lra): expose some stats --- src/arith/lra/sidekick_arith_lra.ml | 9 +++++---- src/arith/lra/simplex2.ml | 16 ++++++++++++++-- 2 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml index d314898f..989c8d6e 100644 --- a/src/arith/lra/sidekick_arith_lra.ml +++ b/src/arith/lra/sidekick_arith_lra.ml @@ -74,7 +74,7 @@ module type S = sig type state - val create : A.S.T.Term.state -> state + val create : ?stat:Stat.t -> A.S.T.Term.state -> state val theory : A.S.theory end @@ -133,7 +133,7 @@ module Make(A : ARG) : S with module A = A = struct simplex: SimpSolver.t; } - let create tst : state = + let create ?stat tst : state = { tst; simps=T.Tbl.create 128; gensym=A.Gensym.create tst; @@ -141,7 +141,7 @@ module Make(A : ARG) : S with module A = A = struct needs_th_combination=T.Tbl.create 8; encoded_le=Comb_map.empty; local_eqs = Backtrack_stack.create(); - simplex=SimpSolver.create (); + simplex=SimpSolver.create ?stat (); } let push_level self = @@ -477,7 +477,8 @@ module Make(A : ARG) : S with module A = A = struct let create_and_setup si = Log.debug 2 "(th-lra.setup)"; - let st = create (SI.tst si) in + let stat = SI.stats si in + let st = create ~stat (SI.tst si) in (* TODO SI.add_simplifier si (simplify st); *) SI.add_preprocess si (preproc_lra st); SI.on_final_check si (final_check_ st); diff --git a/src/arith/lra/simplex2.ml b/src/arith/lra/simplex2.ml index ac590380..1c7ae836 100644 --- a/src/arith/lra/simplex2.ml +++ b/src/arith/lra/simplex2.ml @@ -71,7 +71,7 @@ module type S = sig type t - val create : unit -> t + val create : ?stat:Stat.t -> unit -> t (** Create a new simplex. *) val push_level : t -> unit @@ -372,6 +372,9 @@ module Make(Var: VAR) vars: var_state Vec.t; (* index -> var with this index *) mutable var_tbl: var_state V_map.t; (* var -> its state *) bound_stack: (var_state * [`Upper|`Lower] * bound option) Backtrack_stack.t; + stat_check: int Stat.counter; + stat_unsat: int Stat.counter; + stat_define: int Stat.counter; } let push_level self : unit = @@ -438,6 +441,7 @@ module Make(Var: VAR) (* define [x] as a basic variable *) let define (self:t) (x:V.t) (le:_ list) : unit = assert (not (has_var_ self x)); + Stat.incr self.stat_define; (* Log.debugf 50 (fun k->k "define-in: %a" pp self); *) let le = List.map (fun (q,v) -> q, find_var_ self v) le in @@ -685,6 +689,7 @@ module Make(Var: VAR) | _, Some upper when Erat.(new_bnd.b_val > upper.b_val) -> (* [b_val <= x <= upper], but [b_val > upper] *) let cert = Unsat_cert.bounds vs ~lower:new_bnd ~upper in + Stat.incr self.stat_unsat; raise (E_unsat cert) | Some lower, _ when Erat.(lower.b_val >= new_bnd.b_val) -> () (* subsumed by existing constraint, do nothing *) @@ -704,6 +709,7 @@ module Make(Var: VAR) | Some lower, _ when Erat.(new_bnd.b_val < lower.b_val) -> (* [lower <= x <= b_val], but [b_val < lower] *) let cert = Unsat_cert.bounds vs ~lower ~upper:new_bnd in + Stat.incr self.stat_unsat; raise (E_unsat cert) | _, Some upper when Erat.(upper.b_val <= new_bnd.b_val) -> () (* subsumed *) @@ -810,6 +816,7 @@ module Make(Var: VAR) let check_exn (self:t) : unit = let exception Stop in Log.debugf 20 (fun k->k "(@[simplex2.check@ %a@])" pp_stats self); + Stat.incr self.stat_check; let m = self.matrix in try @@ -837,6 +844,7 @@ module Make(Var: VAR) | Some x -> x | None -> let cert = cert_of_row_ self x_i bnd ~is_lower:true in + Stat.incr self.stat_unsat; raise (E_unsat cert) in assert (Var_state.is_n_basic x_j); @@ -859,6 +867,7 @@ module Make(Var: VAR) | Some x -> x | None -> let cert = cert_of_row_ self x_i bnd ~is_lower:false in + Stat.incr self.stat_unsat; raise (E_unsat cert) in assert (Var_state.is_n_basic x_j); @@ -874,12 +883,15 @@ module Make(Var: VAR) Log.debugf 50 (fun k->k "(@[simplex2.check.done@])"); () - let create () : t = + let create ?(stat=Stat.global) () : t = let self = { matrix=Matrix.create(); vars=Vec.create(); var_tbl=V_map.empty; bound_stack=Backtrack_stack.create(); + stat_check=Stat.mk_int stat "simplex.check"; + stat_unsat=Stat.mk_int stat "simplex.unsat"; + stat_define=Stat.mk_int stat "simplex.define"; } in self