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

fix some stats

Browse source
This commit is contained in:
Simon Cruanes 2022-08-21 13:53:36 -04:00
parent 7dac9781bf
commit 007fbad243
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 17 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/smt/solver.ml
View file

@ -65,8 +65,9 @@ type t = {
mutable last_res: res option; mutable last_res: res option;
stat: Stat.t; stat: Stat.t;
proof: P.t; proof: P.t;
count_clause: int Stat.counter; n_clause_input: int Stat.counter;
count_solve: int Stat.counter; (* config: Config.t *) n_clause_internal: int Stat.counter;
n_solve: int Stat.counter; (* config: Config.t *)
} }
(** {2 Main} *) (** {2 Main} *)
@ -101,8 +102,9 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
last_res = None; last_res = None;
solver = Sat_solver.create ~proof ?size ~stat (SI.to_sat_plugin si); solver = Sat_solver.create ~proof ?size ~stat (SI.to_sat_plugin si);
stat; stat;
count_clause = Stat.mk_int stat "smt.solver.add-clause"; n_clause_input = Stat.mk_int stat "smt.solver.add-clause.input";
count_solve = Stat.mk_int stat "smt.solver.solve"; n_clause_internal = Stat.mk_int stat "smt.solver.add-clause.internal";
n_solve = Stat.mk_int stat "smt.solver.solve";
} }
in in
add_theory_l self theories; add_theory_l self theories;
@ -137,8 +139,12 @@ let mk_lit_t (self : t) ?sign (t : term) : lit =
let pp_stats out (self : t) : unit = Stat.pp out (stats self) let pp_stats out (self : t) : unit = Stat.pp out (stats self)
(* add [c], without preprocessing its literals *) (* add [c], without preprocessing its literals *)
let add_clause_nopreproc_ (self : t) (c : lit array) (proof : step_id) : unit = let add_clause_nopreproc_ ~internal (self : t) (c : lit array) (proof : step_id)
Stat.incr self.count_clause; : unit =
if internal then
Stat.incr self.n_clause_internal
else
Stat.incr self.n_clause_input;
reset_last_res_ self; reset_last_res_ self;
Log.debugf 50 (fun k -> Log.debugf 50 (fun k ->
k "(@[solver.add-clause@ %a@])" (Util.pp_array Lit.pp) c); k "(@[solver.add-clause@ %a@])" (Util.pp_array Lit.pp) c);
@ -146,14 +152,14 @@ let add_clause_nopreproc_ (self : t) (c : lit array) (proof : step_id) : unit =
Sat_solver.add_clause_a self.solver (c :> lit array) proof; Sat_solver.add_clause_a self.solver (c :> lit array) proof;
Profile.exit pb Profile.exit pb
let add_clause_nopreproc_l_ self c p = let add_clause_nopreproc_l_ ~internal self c p =
add_clause_nopreproc_ self (CCArray.of_list c) p add_clause_nopreproc_ ~internal self (CCArray.of_list c) p
module Perform_delayed_ = Solver_internal.Perform_delayed (struct module Perform_delayed_ = Solver_internal.Perform_delayed (struct
type nonrec t = t type nonrec t = t
let add_clause _si solver ~keep:_ c pr : unit = let add_clause _si solver ~keep:_ c pr : unit =
add_clause_nopreproc_l_ solver c pr add_clause_nopreproc_l_ ~internal:true solver c pr
let add_lit _si solver ?default_pol lit : unit = let add_lit _si solver ?default_pol lit : unit =
Sat_solver.add_lit solver.solver ?default_pol lit Sat_solver.add_lit solver.solver ?default_pol lit
@ -161,7 +167,7 @@ end)
let add_clause (self : t) (c : lit array) (proof : step_id) : unit = let add_clause (self : t) (c : lit array) (proof : step_id) : unit =
let c, proof = preprocess_clause_ self c proof in let c, proof = preprocess_clause_ self c proof in
add_clause_nopreproc_ self c proof; add_clause_nopreproc_ ~internal:false self c proof;
Perform_delayed_.top self.si self; Perform_delayed_.top self.si self;
(* finish preproc *) (* finish preproc *)
() ()
@ -192,7 +198,7 @@ let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
let res = let res =
match match
Stat.incr self.count_solve; Stat.incr self.n_solve;
Sat_solver.solve ~on_progress ~assumptions (solver self) Sat_solver.solve ~on_progress ~assumptions (solver self)
with with
| Sat_solver.Sat _ when not (SI.is_complete self.si) -> | Sat_solver.Sat _ when not (SI.is_complete self.si) ->