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

wip: stats for msat

Browse source
This commit is contained in:
Simon Cruanes 2019-06-10 16:04:14 -05:00
parent af0635dab7
commit 7b62dbcb4d
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -375,6 +375,9 @@ module Make(A : ARG)
stat: Stat.t; stat: Stat.t;
count_clause: int Stat.counter; count_clause: int Stat.counter;
count_solve: int Stat.counter; count_solve: int Stat.counter;
count_sat_conflict: int Stat.counter;
count_sat_props: int Stat.counter;
count_sat_restarts: int Stat.counter;
(* config: Config.t *) (* config: Config.t *)
} }
type solver = t type solver = t
@ -425,6 +428,9 @@ module Make(A : ARG)
stat; stat;
count_clause=Stat.mk_int stat "solver.add-clause"; count_clause=Stat.mk_int stat "solver.add-clause";
count_solve=Stat.mk_int stat "solver.solve"; count_solve=Stat.mk_int stat "solver.solve";
count_sat_conflict=Stat.mk_int stat "sat.conflict";
count_sat_props=Stat.mk_int stat "sat.propagation";
count_sat_restarts=Stat.mk_int stat "sat.restart";
} in } in
add_theory_l self theories; add_theory_l self theories;
(* assert [true] and [not false] *) (* assert [true] and [not false] *)
@ -559,6 +565,9 @@ module Make(A : ARG)
let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res = let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
let do_on_exit () = let do_on_exit () =
(* TODO:
let stat = Sat_solver.stat self.sat in
Stat.set self.count_sat_restarts stat.n_restarts *)
List.iter (fun f->f()) on_exit; List.iter (fun f->f()) on_exit;
in in
let r = Sat_solver.solve ~assumptions (solver self) in let r = Sat_solver.solve ~assumptions (solver self) in