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

wip: clauses pools

Browse source
This commit is contained in:
Simon Cruanes 2021-08-30 09:32:32 -04:00
parent 81caf4824e
commit 1877c00c02
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 165 additions and 82 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

145
src/sat/Solver.ml
View file

@ -87,7 +87,7 @@ module Make(Plugin : PLUGIN)
c_activity: Vec_float.t;
c_recycle_idx: VecI32.t; (* recycle clause numbers that were GC'd *)
c_attached: Bitvec.t;
c_marked: Bitvec.t; (* TODO : remove *)
c_marked: Bitvec.t;
c_removable: Bitvec.t;
c_dead: Bitvec.t;
}
@ -532,16 +532,23 @@ module Make(Plugin : PLUGIN)
vectors, the comments actually refer to the original non-simplified
clause. *)
(* TODO: this should be a veci32 *)
clauses_hyps : clause Vec.t;
(* clauses added by the user *)
clauses_hyps : CVec.t;
(* clauses added by the user, never removed *)
clauses_learnt : clause Vec.t;
(* learnt clauses (tautologies true at any time, whatever the user level) *)
clauses_learnt : CVec.t;
(* learnt clauses (tautologies true at any time, whatever the user level).
GC'd regularly. *)
clauses_to_add : clause Vec.t;
clauses_to_add : CVec.t;
(* Clauses either assumed or pushed by the theory, waiting to be added. *)
clauses_dead : CVec.t;
(* dead clauses, to be removed at next GC.
invariant: all satisfy [Clause.dead store c]. *)
clause_pools : clause_pool Vec.t;
(* custom clause pools *)
mutable unsat_at_0: clause option;
(* conflict at level 0, if any *)
@ -604,6 +611,18 @@ module Make(Plugin : PLUGIN)
n_decisions : int Stat.counter;
n_restarts : int Stat.counter;
}
and clause_pool =
| CP_gc of {
size: int;
clauses: CVec.t;
descr: string;
}
| CP_scoped of {
clauses: CVec.t;
levels: VecI32.t; (* backtracking levels for clauses *)
descr: string;
}
type solver = t
(* intial restart limit *)
@ -621,10 +640,13 @@ module Make(Plugin : PLUGIN)
unsat_at_0=None;
next_decisions = [];
clauses_hyps = Vec.create();
clauses_learnt = Vec.create();
clauses_hyps = CVec.create();
clauses_learnt = CVec.create();
clauses_to_add = CVec.create ();
clauses_dead = CVec.create();
clause_pools = Vec.create();
clauses_to_add = Vec.create ();
to_clear=Vec.create();
temp_clause_vec=Vec.create();
temp_atom_vec=Vec.create();
@ -667,8 +689,65 @@ module Make(Plugin : PLUGIN)
self.on_gc <- on_gc;
self
module Clause_pool : sig
type t = clause_pool
val descr : t -> string
val add : solver -> t -> clause -> unit
val gc : solver -> t -> unit
val push_level : solver -> t -> unit
val cancel_until : solver -> t -> int -> unit
val iter : t -> f:(clause -> unit) -> unit
end = struct
type t = clause_pool
let descr = function
| CP_gc {descr; _} | CP_scoped {descr; _} -> descr
let gc (solver:solver) (self:t) : unit =
match self with
| CP_gc {clauses; size; descr} ->
Log.debugf 10 (fun k->k"(@[clause-pool.gc@ %s@])" descr);
() (* FIXME *)
| CP_scoped _ -> ()
let push_level (_:solver) (self:t) =
match self with
| CP_gc _ -> ()
| CP_scoped {clauses; levels; descr=_} ->
VecI32.push levels (CVec.size clauses)
let cancel_until (solver:solver) (self:t) (lvl: int) : unit =
match self with
| CP_gc _ -> ()
| CP_scoped {clauses; levels; descr} ->
Log.debugf 10 (fun k->k"(@[clause-pool.gc@ %s@])" descr);
let old_size = VecI32.get levels lvl in
VecI32.shrink levels lvl;
while CVec.size clauses > old_size do
let c = CVec.pop clauses in
Log.debugf 50 (fun k->k"(@[clause-pool.gc.remove@ :in %s@ %a"
descr (Clause.pp solver.store) c);
Clause.set_dead solver.store c true;
CVec.push solver.clauses_dead c;
done
let add solver (self:t) (c:clause) =
match self with
| CP_gc { clauses; size; descr=_} ->
if CVec.size clauses >= size then (
gc solver self;
);
CVec.push clauses c
| CP_scoped {clauses; _} ->
CVec.push clauses c
let iter self ~f = match self with
| CP_gc {clauses; _} | CP_scoped {clauses; _} ->
CVec.iter clauses ~f
end
let[@inline] decision_level st = Vec.size st.var_levels
let[@inline] nb_clauses st = Vec.size st.clauses_hyps
let[@inline] nb_clauses st = CVec.size st.clauses_hyps
let stat self = self.stat
(* Do we have a level-0 empty clause? *)
@ -722,14 +801,21 @@ module Make(Plugin : PLUGIN)
H.decrease self.order v
)
(* iterate on all learnt clauses, pool included *)
let iter_clauses_learnt_ (self:t) ~f : unit =
CVec.iter self.clauses_learnt ~f;
Vec.iter (fun pool -> Clause_pool.iter pool ~f) self.clause_pools;
()
(* increase activity of clause [c] *)
let clause_bump_activity self (c:clause) : unit =
let store = self.store in
Clause.set_activity store c (Clause.activity store c +. self.clause_incr);
if Clause.activity store c > 1e20 then (
Vec.iter
(fun c -> Clause.set_activity store c (Clause.activity store c *. 1e-20))
self.clauses_learnt;
let update_clause c =
Clause.set_activity store c (Clause.activity store c *. 1e-20)
in
iter_clauses_learnt_ self ~f:update_clause;
self.clause_incr <- self.clause_incr *. 1e-20
)
@ -899,6 +985,7 @@ module Make(Plugin : PLUGIN)
Vec.shrink self.trail !head;
Vec.shrink self.var_levels lvl;
Plugin.pop_levels self.th n;
(* TODO: for scoped clause pools, backtrack them *)
self.next_decisions <- [];
);
()
@ -1172,6 +1259,7 @@ module Make(Plugin : PLUGIN)
cr_is_uip = is_uip;
}
(* FIXME: take clause pool *)
(* add the learnt clause to the clause database, propagate, etc. *)
let record_learnt_clause (self:t) (confl:clause) (cr:conflict_res): unit =
let store = self.store in
@ -1195,7 +1283,7 @@ module Make(Plugin : PLUGIN)
let fuip = cr.cr_learnt.(0) in
let lclause = Clause.make_a store ~removable:true cr.cr_learnt in
if Clause.n_atoms store lclause > 2 then (
Vec.push self.clauses_learnt lclause; (* potentially gc'able *)
CVec.push self.clauses_learnt lclause; (* potentially gc'able *)
);
attach_clause self lclause;
clause_bump_activity self lclause;
@ -1299,13 +1387,13 @@ module Make(Plugin : PLUGIN)
(fun k->k "(@[sat.add-clause@ :ignore-trivial @[%a@]@])" (Clause.debug store) init)
let[@inline never] flush_clauses_ st =
while not @@ Vec.is_empty st.clauses_to_add do
let c = Vec.pop_exn st.clauses_to_add in
while not @@ CVec.is_empty st.clauses_to_add do
let c = CVec.pop st.clauses_to_add in
add_clause_ st c
done
let[@inline] flush_clauses st =
if not @@ Vec.is_empty st.clauses_to_add then flush_clauses_ st
if not @@ CVec.is_empty st.clauses_to_add then flush_clauses_ st
type watch_res =
| Watch_kept
@ -1371,11 +1459,14 @@ module Make(Plugin : PLUGIN)
else (
let c = CVec.get watched i in
assert (Clause.attached store c);
assert (not (Clause.dead store c));
let j =
match propagate_in_clause self a c i with
| Watch_kept -> i+1
| Watch_removed -> i (* clause at this index changed *)
if Clause.dead store c then (
i (* remove on the fly *)
) else (
match propagate_in_clause self a c i with
| Watch_kept -> i+1
| Watch_removed -> i (* clause at this index changed *)
)
in
aux j
)
@ -1394,6 +1485,15 @@ module Make(Plugin : PLUGIN)
Log.debugf 5 (fun k->k "(@[sat.th.add-clause@ %a@])" (Clause.debug self.store) c);
Vec.push self.clauses_to_add c
let acts_add_clause_in_pool self ~pool (l:lit list) (dp:dproof): unit =
let atoms = List.rev_map (make_atom_ self) l in
let removable = true in
let c = Clause.make_l self.store ~removable atoms in
Proof.with_proof self.proof dp;
Log.debugf 5 (fun k->k "(@[sat.th.add-clause-in-pool@ %a@ :pool %s@])"
(Clause.debug self.store) c (Clause_pool.descr pool));
Clause_pool.add pool c
let acts_add_decision_lit (self:t) (f:lit) (sign:bool) : unit =
let store = self.store in
let a = make_atom_ self f in
@ -1481,6 +1581,7 @@ module Make(Plugin : PLUGIN)
let eval_lit= acts_eval_lit st
let add_lit=acts_add_lit st
let add_clause = acts_add_clause st
let add_clause_in_pool = acts_add_clause_in_pool st
let propagate = acts_propagate st
let raise_conflict c pr=acts_raise st c pr
let add_decision_lit=acts_add_decision_lit st

102
src/sat/Solver_intf.ml
View file

@ -37,21 +37,6 @@ end
type 'form sat_state = (module SAT_STATE with type lit = 'form)
(** The type of values returned when the solver reaches a SAT state. *)
(** Lifetime for clauses added with {!add_clause}.
See {!CLAUSE_ALLOCATOR} to see what allocators are
(here they are referred to by their index). *)
type clause_lifetime =
| CL_keep
| CL_can_gc
| CL_use_allocator of {
allocator_idx: int;
}
let pp_clause_lifetime out = function
| CL_keep -> Fmt.string out "keep"
| CL_can_gc -> Fmt.string out "can-gc"
| CL_use_allocator {allocator_idx=idx} -> Fmt.fprintf out "(custom %d)" idx
module type UNSAT_STATE = sig
type lit
type clause
@ -97,26 +82,6 @@ type ('lit, 'proof) reason =
type lbool = L_true | L_false | L_undefined
(** Valuation of an atom *)
(** {2 Clause Allocators}
A clause allocator holds a set of clauses. Each clause lives in
exactly one clause allocator.
Each allocator is responsible for the lifetime of its clause: some will
keep the clauses forever (e.g. for axioms), some will GC the clauses
after reaching a maximum size, etc. *)
module type CLAUSE_ALLOCATOR = sig
type t
type behavior
(** Behavior for the clause allocator *)
val gc_fixed_size : int -> behavior
(** GC clauses when the allocator reaches the given size *)
(* TODO: scoped allocator? different GCs? *)
end
(** Actions available to the Plugin
The plugin provides callbacks for the SAT solver to use. These callbacks
@ -125,6 +90,7 @@ end
module type ACTS = sig
type lit
type proof
type clause_pool
type dproof = proof -> unit
val iter_assumptions: (lit -> unit) -> unit
@ -137,20 +103,18 @@ module type ACTS = sig
(** Map the given lit to an internal atom, which will be decided by the
SAT solver. *)
val add_clause:
?lifetime:clause_lifetime ->
lit list ->
dproof ->
unit
val add_clause: ?keep:bool -> lit list -> dproof -> unit
(** Add a clause to the solver.
@param lifetime lifetime to use for the clause.
- [C_keep] will make the clause unremovable
- [C_can_gc] the solver is allowed to GC the clause and propose this
@param keep if true, the clause will be kept by the solver.
Otherwise the solver is allowed to GC the clause and propose this
partial model again.
- [C_use_allocator alloc] puts the clause in the given allocator.
*)
val add_clause_in_pool : pool:clause_pool -> lit list -> dproof -> unit
(** Like {!add_clause} but uses a custom clause pool for the clause,
with its own lifetime. *)
val raise_conflict: lit list -> dproof -> 'b
(** Raise a conflict, yielding control back to the solver.
The list of atoms must be a valid theory lemma that is false in the
@ -256,6 +220,9 @@ module type S = sig
type clause
type clause_pool
(** Pool of clauses, with its own lifetime management *)
type theory
type proof
@ -329,6 +296,31 @@ module type S = sig
val proof : t -> proof
(** Access the inner proof *)
(** {2 Clause Pools} *)
(** Clause pools.
A clause pool holds/owns a set of clauses, and is responsible for
managing their lifetime. *)
module Clause_pool : sig
type t = clause_pool
val descr : t -> string
end
val new_clause_pool_gc_fixed_size :
descr:string ->
size:int ->
t -> clause_pool
(** Allocate a new clause pool that GC's its clauses when its size
goes above [size]. It keeps half of the clauses. *)
val new_clause_pool_scoped :
descr:string ->
t -> clause_pool
(** Allocate a new clause pool that holds local clauses
goes above [size]. It keeps half of the clauses. *)
(** {2 Types} *)
(** Result type for the solver *)
@ -340,22 +332,6 @@ module type S = sig
(** Exception raised by the evaluating functions when a literal
has not yet been assigned a value. *)
module Clause_allocator : CLAUSE_ALLOCATOR
type clause_allocator = Clause_allocator.t
val add_clause_allocator :
descr:string ->
behavior:Clause_allocator.behavior ->
t ->
clause_allocator
(** Make a new clause allocator for this solver.
@param descr short description of this allocator and what it contains
@param behavior controls the behavior of the allocator, i.e. whether
it collects clauses, which clauses are kept, what its maximum size
is, etc.
*)
(** {2 Base operations} *)
val assume : t -> lit list list -> unit
@ -371,6 +347,12 @@ module type S = sig
val add_clause_a : t -> lit array -> dproof -> unit
(** Lower level addition of clauses *)
val add_clause_in_pool : t -> pool:clause_pool -> lit list -> unit
(** Like {!add_clause} but using a specific clause pool *)
val add_clause_a_in_pool : t -> pool:clause_pool -> lit array -> unit
(** Like {!add_clause_a} but using a specific clause pool *)
val add_input_clause_a : t -> lit array -> unit
(** Like {!add_clause_a} but with justification of being an input clause *)