simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat: add more stats

Browse source
This commit is contained in:
Simon Cruanes 2019-06-07 13:27:03 -05:00
parent 8c9590b1e8
commit 2000114ab4
2 changed files with 17 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/cc/Sidekick_cc.ml
View file

@ -221,6 +221,7 @@ module Make(CC_A: ARG) = struct
false_ : node lazy_t; false_ : node lazy_t;
stat: Stat.t; stat: Stat.t;
count_conflict: int Stat.counter; count_conflict: int Stat.counter;
count_props: int Stat.counter;
count_merge: int Stat.counter; count_merge: int Stat.counter;
} }
(* TODO: an additional union-find to keep track, for each term, (* TODO: an additional union-find to keep track, for each term,
@ -707,6 +708,7 @@ module Make(CC_A: ARG) = struct
let e = lazy (explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1) in let e = lazy (explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1) in
fun () -> Lazy.force e fun () -> Lazy.force e
in in
Stat.incr cc.count_props;
CC_A.Actions.propagate acts lit ~reason CC_A.A.Proof.default CC_A.Actions.propagate acts lit ~reason CC_A.A.Proof.default
| _ -> ()) | _ -> ())
@ -831,6 +833,7 @@ module Make(CC_A: ARG) = struct
false_; false_;
stat; stat;
count_conflict=Stat.mk_int stat "cc.conflicts"; count_conflict=Stat.mk_int stat "cc.conflicts";
count_props=Stat.mk_int stat "cc.propagations";
count_merge=Stat.mk_int stat "cc.merges"; count_merge=Stat.mk_int stat "cc.merges";
} and true_ = lazy ( } and true_ = lazy (
add_term cc (T.bool tst true) add_term cc (T.bool tst true)

21
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -109,6 +109,7 @@ module Make(A : ARG)
cc: CC.t lazy_t; (** congruence closure *) cc: CC.t lazy_t; (** congruence closure *)
stat: Stat.t; stat: Stat.t;
count_axiom: int Stat.counter; count_axiom: int Stat.counter;
count_preprocess_clause: int Stat.counter;
count_conflict: int Stat.counter; count_conflict: int Stat.counter;
count_propagate: int Stat.counter; count_propagate: int Stat.counter;
simp: Simplify.t; simp: Simplify.t;
@ -182,13 +183,17 @@ module Make(A : ARG)
T.pp t T.pp u); T.pp t T.pp u);
aux u aux u
in in
let t = aux (Lit.term lit) in let t = Lit.term lit |> simp_t self |> aux in
let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
Log.debugf 10 Log.debugf 10
(fun k->k "(@[msat-solver.preprocess@ :lit %a@ :into %a@])" Lit.pp lit T.pp t); (fun k->k "(@[msat-solver.preprocess@ :lit %a@ :into %a@])" Lit.pp lit Lit.pp lit');
Lit.atom self.tst ~sign:(Lit.sign lit) t lit'
let[@inline] mk_lit self acts ?sign t = let[@inline] mk_lit self acts ?sign t =
let add_clause lits = add_sat_clause_ self acts ~keep:true lits in let add_clause lits =
Stat.incr self.count_preprocess_clause;
add_sat_clause_ self acts ~keep:true lits
in
preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t
let[@inline] add_clause_temp self acts lits : unit = let[@inline] add_clause_temp self acts lits : unit =
@ -296,9 +301,10 @@ module Make(A : ARG)
simp=Simplify.create tst; simp=Simplify.create tst;
preprocess=[]; preprocess=[];
preprocess_cache=T.Tbl.create 32; preprocess_cache=T.Tbl.create 32;
count_axiom = Stat.mk_int stat "th-axioms"; count_axiom = Stat.mk_int stat "solver.th-axioms";
count_propagate = Stat.mk_int stat "th-propagations"; count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause";
count_conflict = Stat.mk_int stat "th-conflicts"; count_propagate = Stat.mk_int stat "solver.th-propagations";
count_conflict = Stat.mk_int stat "solver.th-conflicts";
on_partial_check=[]; on_partial_check=[];
on_final_check=[]; on_final_check=[];
} in } in
@ -420,6 +426,7 @@ module Make(A : ARG)
Solver_internal.preprocess_lit_ Solver_internal.preprocess_lit_
~add_clause:(fun lits -> ~add_clause:(fun lits ->
(* recursively add these sub-literals, so they're also properly processed *) (* recursively add these sub-literals, so they're also properly processed *)
Stat.incr self.si.count_preprocess_clause;
let atoms = List.map (mk_atom_lit self) lits in let atoms = List.map (mk_atom_lit self) lits in
Sat_solver.add_clause self.solver atoms A.Proof.default) Sat_solver.add_clause self.solver atoms A.Proof.default)
self.si lit in self.si lit in