simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 20:55:39 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(sat): refactor a bit clause pools; add stats

Browse source
This commit is contained in:
Simon Cruanes 2021-09-19 13:06:53 -04:00
parent 14d2a89196
commit 156eadd9df
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 19 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/sat/Solver.ml
View file

@ -535,7 +535,7 @@ module Make(Plugin : PLUGIN)
(** A clause pool *) (** A clause pool *)
module type CLAUSE_POOL = sig module type CLAUSE_POOL = sig
val add : clause -> unit val add : clause -> unit
val descr : unit -> string val descr : string
val gc : (module GC_ARG) -> unit val gc : (module GC_ARG) -> unit
val iter : f:(clause -> unit) -> unit val iter : f:(clause -> unit) -> unit
val needs_gc : unit -> bool val needs_gc : unit -> bool
@ -547,15 +547,19 @@ module Make(Plugin : PLUGIN)
(* a pool with garbage collection determined by [P] *) (* a pool with garbage collection determined by [P] *)
module Make_gc_cp(P:sig module Make_gc_cp(P:sig
val descr : unit -> string val descr : string
val max_size : int ref val max_size : int ref
val stat : Stat.t
end)() : CLAUSE_POOL = struct end)() : CLAUSE_POOL = struct
let clauses_ : clause Vec.t = Vec.create() let clauses_ : clause Vec.t = Vec.create()
(* Use a [Vec] so we can sort it. (* Use a [Vec] so we can sort it.
TODO: when we can sort any vec, come back to that. *) TODO: when we can sort any vec, come back to that to use [CVec.t]. *)
let n_alloc : int Stat.counter = Stat.mk_int P.stat (P.descr ^ ".clauses_alloc")
let n_clauses_gc : int Stat.counter = Stat.mk_int P.stat (P.descr ^ ".clauses_gc")
let descr = P.descr let descr = P.descr
let add c = Vec.push clauses_ c let add c = Stat.incr n_alloc; Vec.push clauses_ c
let iter ~f = Vec.iter f clauses_ let iter ~f = Vec.iter f clauses_
let push_level () = () let push_level () = ()
let pop_levels _ = () let pop_levels _ = ()
@ -576,6 +580,7 @@ module Make(Plugin : PLUGIN)
if G.must_keep_clause c then ( if G.must_keep_clause c then (
CVec.push to_be_pushed_back c; (* must keep it, it's on the trail *) CVec.push to_be_pushed_back c; (* must keep it, it's on the trail *)
) else ( ) else (
Stat.incr n_clauses_gc;
G.flag_clause_for_gc c; G.flag_clause_for_gc c;
) )
done; done;
@ -584,13 +589,14 @@ module Make(Plugin : PLUGIN)
() ()
end end
let make_gc_clause_pool_ ~descr ~max_size () : clause_pool = let make_gc_clause_pool_ ~stat ~descr ~max_size () : clause_pool =
(module Make_gc_cp(struct (module Make_gc_cp(struct
let stat=stat
let descr=descr let descr=descr
let max_size=max_size let max_size=max_size
end)()) end)())
let[@inline] cp_descr_ (module P:CLAUSE_POOL) : string = P.descr() let[@inline] cp_descr_ (module P:CLAUSE_POOL) : string = P.descr
let[@inline] cp_size_ (module P:CLAUSE_POOL) : int = P.size() let[@inline] cp_size_ (module P:CLAUSE_POOL) : int = P.size()
let[@inline] cp_needs_gc_ (module P:CLAUSE_POOL) : bool = P.needs_gc() let[@inline] cp_needs_gc_ (module P:CLAUSE_POOL) : bool = P.needs_gc()
let[@inline] cp_add_ (module P:CLAUSE_POOL) c : unit = P.add c let[@inline] cp_add_ (module P:CLAUSE_POOL) c : unit = P.add c
@ -699,6 +705,7 @@ module Make(Plugin : PLUGIN)
n_decisions : int Stat.counter; n_decisions : int Stat.counter;
n_restarts : int Stat.counter; n_restarts : int Stat.counter;
n_minimized_away : int Stat.counter; n_minimized_away : int Stat.counter;
n_gc_clause : int Stat.counter;
} }
type solver = t type solver = t
@ -717,8 +724,8 @@ module Make(Plugin : PLUGIN)
max_clauses_learnt; max_clauses_learnt;
clauses_hyps = CVec.create(); clauses_hyps = CVec.create();
clauses_learnt = clauses_learnt =
make_gc_clause_pool_ make_gc_clause_pool_ ~stat
~descr:(fun () -> "cp.learnt-clauses") ~descr:"cp.learnt-clauses"
~max_size:max_clauses_learnt (); ~max_size:max_clauses_learnt ();
clauses_to_add_learnt = CVec.create (); clauses_to_add_learnt = CVec.create ();
clauses_to_add_in_pool = Vec.create(); clauses_to_add_in_pool = Vec.create();
@ -750,6 +757,7 @@ module Make(Plugin : PLUGIN)
n_propagations = Stat.mk_int stat "sat.n-propagations"; n_propagations = Stat.mk_int stat "sat.n-propagations";
n_restarts = Stat.mk_int stat "sat.n-restarts"; n_restarts = Stat.mk_int stat "sat.n-restarts";
n_minimized_away = Stat.mk_int stat "sat.n-confl-lits-minimized-away"; n_minimized_away = Stat.mk_int stat "sat.n-confl-lits-minimized-away";
n_gc_clause = Stat.mk_int stat "sat.n-gc-clause";
on_conflict = None; on_conflict = None;
on_decision= None; on_decision= None;
@ -1801,6 +1809,7 @@ module Make(Plugin : PLUGIN)
let flag_clause_for_gc c : unit = let flag_clause_for_gc c : unit =
assert (Clause.removable store c); assert (Clause.removable store c);
Log.debugf 10 (fun k->k"(@[sat.gc.will-collect@ %a@])" (Clause.debug store) c); Log.debugf 10 (fun k->k"(@[sat.gc.will-collect@ %a@])" (Clause.debug store) c);
Stat.incr self.n_gc_clause;
CVec.push to_be_gc c; CVec.push to_be_gc c;
Clause.set_dead store c true; Clause.set_dead store c true;
let atoms = Clause.atoms_a store c in let atoms = Clause.atoms_a store c in
@ -1824,7 +1833,7 @@ module Make(Plugin : PLUGIN)
(* GC a pool, if it needs it *) (* GC a pool, if it needs it *)
let gc_pool (module P:CLAUSE_POOL) : unit = let gc_pool (module P:CLAUSE_POOL) : unit =
if P.needs_gc () then ( if P.needs_gc () then (
Log.debugf 5 (fun k->k"(@[sat.gc.pool@ :descr %s@])" (P.descr())); Log.debugf 5 (fun k->k"(@[sat.gc.pool@ :descr %s@])" P.descr);
P.gc gc_arg P.gc gc_arg
) )
in in
@ -2116,11 +2125,7 @@ module Make(Plugin : PLUGIN)
add_clause_a self c dp add_clause_a self c dp
let new_clause_pool_gc_fixed_size ~descr ~size (self:t) : clause_pool_id = let new_clause_pool_gc_fixed_size ~descr ~size (self:t) : clause_pool_id =
let p = let p = make_gc_clause_pool_ ~stat:self.stat ~descr ~max_size:(ref size) () in
make_gc_clause_pool_
~descr:(fun () -> descr)
~max_size:(ref size)
() in
let id = Vec.size self.clause_pools in let id = Vec.size self.clause_pools in
Vec.push self.clause_pools p; Vec.push self.clause_pools p;
Clause_pool_id._unsafe_of_int id Clause_pool_id._unsafe_of_int id