mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
SAT: remove clause pools
This commit is contained in:
Simon Cruanes
parent
00dec7ced8
commit
679b35012b
3 changed files with 20 additions and 88 deletions
|
|
@ -9,8 +9,6 @@ end
|
|||
module type S = Solver_intf.S
|
||||
module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
|
||||
|
||||
module Clause_pool_id = Solver_intf.Clause_pool_id
|
||||
|
||||
let invalid_argf fmt =
|
||||
Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) fmt
|
||||
|
||||
|
|
@ -19,7 +17,16 @@ module Make (Plugin : PLUGIN) = struct
|
|||
type theory = Plugin.t
|
||||
type proof = Plugin.proof
|
||||
type proof_step = Plugin.proof_step
|
||||
type clause_pool_id = Clause_pool_id.t
|
||||
|
||||
module Clause_pool_id : sig
|
||||
type t = private int
|
||||
|
||||
val _unsafe_of_int : int -> t
|
||||
end = struct
|
||||
type t = int
|
||||
|
||||
let _unsafe_of_int x = x
|
||||
end
|
||||
|
||||
module Lit = Plugin.Lit
|
||||
module Proof = Plugin.Proof
|
||||
|
|
@ -951,10 +958,6 @@ module Make (Plugin : PLUGIN) = struct
|
|||
let[@inline] nb_clauses st = CVec.size st.clauses_hyps
|
||||
let stat self = self.stat
|
||||
|
||||
let clause_pool_descr self (p : clause_pool_id) =
|
||||
let pool = Vec.get self.clause_pools (p :> int) in
|
||||
cp_descr_ pool
|
||||
|
||||
(* Do we have a level-0 empty clause? *)
|
||||
let[@inline] check_unsat_ st =
|
||||
match st.unsat_at_0 with
|
||||
|
|
@ -1855,7 +1858,7 @@ module Make (Plugin : PLUGIN) = struct
|
|||
let atoms = List.rev_map (make_atom_ self) l in
|
||||
let removable = true in
|
||||
let c = Clause.make_l self.store ~removable atoms p in
|
||||
let pool = Vec.get self.clause_pools (pool : clause_pool_id :> int) in
|
||||
let pool = Vec.get self.clause_pools (pool : Clause_pool_id.t :> int) in
|
||||
Log.debugf 5 (fun k ->
|
||||
k "(@[sat.th.add-clause-in-pool@ %a@ :pool %s@])"
|
||||
(Clause.debug self.store) c (cp_descr_ pool));
|
||||
|
|
@ -2003,7 +2006,6 @@ module Make (Plugin : PLUGIN) = struct
|
|||
let module M = struct
|
||||
type nonrec proof = proof
|
||||
type nonrec proof_step = proof_step
|
||||
type nonrec clause_pool_id = clause_pool_id
|
||||
type nonrec lit = lit
|
||||
|
||||
let proof = st.proof
|
||||
|
|
@ -2011,7 +2013,6 @@ module Make (Plugin : PLUGIN) = struct
|
|||
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
|
||||
|
|
@ -2023,7 +2024,6 @@ module Make (Plugin : PLUGIN) = struct
|
|||
let module M = struct
|
||||
type nonrec proof = proof
|
||||
type nonrec proof_step = proof_step
|
||||
type nonrec clause_pool_id = clause_pool_id
|
||||
type nonrec lit = lit
|
||||
|
||||
let proof = st.proof
|
||||
|
|
@ -2031,7 +2031,6 @@ module Make (Plugin : PLUGIN) = struct
|
|||
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
|
||||
|
|
@ -2615,16 +2614,6 @@ module Make (Plugin : PLUGIN) = struct
|
|||
let c = Util.array_of_list_map (make_atom_ self) c in
|
||||
add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c pr
|
||||
|
||||
let add_clause_a_in_pool self ~pool c (pr : proof_step) : unit =
|
||||
let c = Array.map (make_atom_ self) c in
|
||||
let pool = Vec.get self.clause_pools (pool : clause_pool_id :> int) in
|
||||
add_clause_atoms_ ~pool ~removable:true self c pr
|
||||
|
||||
let add_clause_in_pool self ~pool (c : lit list) dp : unit =
|
||||
let c = Util.array_of_list_map (make_atom_ self) c in
|
||||
let pool = Vec.get self.clause_pools (pool : clause_pool_id :> int) in
|
||||
add_clause_atoms_ ~pool ~removable:true self c dp
|
||||
|
||||
let add_input_clause self (c : lit list) =
|
||||
let pr = Proof.emit_input_clause (Iter.of_list c) self.proof in
|
||||
add_clause self c pr
|
||||
|
|
@ -2633,14 +2622,6 @@ module Make (Plugin : PLUGIN) = struct
|
|||
let pr = Proof.emit_input_clause (Iter.of_array c) self.proof in
|
||||
add_clause_a self c pr
|
||||
|
||||
let new_clause_pool_gc_fixed_size ~descr ~size (self : t) : clause_pool_id =
|
||||
let p =
|
||||
make_gc_clause_pool_ ~descr:(fun () -> descr) ~max_size:(ref size) ()
|
||||
in
|
||||
let id = Vec.size self.clause_pools in
|
||||
Vec.push self.clause_pools p;
|
||||
Clause_pool_id._unsafe_of_int id
|
||||
|
||||
(* run [f()] with additional assumptions *)
|
||||
let with_local_assumptions_ (self : t) (assumptions : lit list) f =
|
||||
let old_assm_lvl = AVec.size self.assumptions in
|
||||
|
|
|
|||
|
|
@ -1,18 +1,19 @@
|
|||
(** Interface for Solvers
|
||||
|
||||
This modules defines the safe external interface for solvers.
|
||||
Solvers that implements this interface can be obtained using the [Make]
|
||||
functor.
|
||||
*)
|
||||
|
||||
(*
|
||||
MSAT is free software, using the Apache license, see file LICENSE
|
||||
Copyright 2016 Guillaume Bury
|
||||
Copyright 2016 Simon Cruanes
|
||||
*)
|
||||
|
||||
(** Interface for Solvers
|
||||
|
||||
This modules defines the safe external interface for solvers.
|
||||
Solvers that implements this interface can be obtained using the [Make]
|
||||
functor in {!Solver} or {!Mcsolver}.
|
||||
*)
|
||||
|
||||
type 'a printer = Format.formatter -> 'a -> unit
|
||||
|
||||
(** Solver in a "SATISFIABLE" state *)
|
||||
module type SAT_STATE = sig
|
||||
type lit
|
||||
(** Literals (signed boolean atoms) *)
|
||||
|
|
@ -37,6 +38,7 @@ end
|
|||
type 'form sat_state = (module SAT_STATE with type lit = 'form)
|
||||
(** The type of values returned when the solver reaches a SAT state. *)
|
||||
|
||||
(** Solver in an "UNSATISFIABLE" state *)
|
||||
module type UNSAT_STATE = sig
|
||||
type lit
|
||||
type clause
|
||||
|
|
@ -86,16 +88,6 @@ type ('lit, 'proof) reason = Consequence of (unit -> 'lit list * 'proof)
|
|||
|
||||
type lbool = L_true | L_false | L_undefined (** Valuation of an atom *)
|
||||
|
||||
module Clause_pool_id : sig
|
||||
type t = private int
|
||||
|
||||
val _unsafe_of_int : int -> t
|
||||
end = struct
|
||||
type t = int
|
||||
|
||||
let _unsafe_of_int x = x
|
||||
end
|
||||
|
||||
(** Actions available to the Plugin
|
||||
|
||||
The plugin provides callbacks for the SAT solver to use. These callbacks
|
||||
|
|
@ -105,7 +97,6 @@ module type ACTS = sig
|
|||
type lit
|
||||
type proof
|
||||
type proof_step
|
||||
type clause_pool_id = Clause_pool_id.t
|
||||
|
||||
val proof : proof
|
||||
|
||||
|
|
@ -127,10 +118,6 @@ module type ACTS = sig
|
|||
- [C_use_allocator alloc] puts the clause in the given allocator.
|
||||
*)
|
||||
|
||||
val add_clause_in_pool : pool:clause_pool_id -> lit list -> proof_step -> unit
|
||||
(** Like {!add_clause} but uses a custom clause pool for the clause,
|
||||
with its own lifetime. *)
|
||||
|
||||
val raise_conflict : lit list -> proof_step -> '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
|
||||
|
|
@ -254,10 +241,6 @@ module type S = sig
|
|||
module Lit : LIT with type t = lit
|
||||
|
||||
type clause
|
||||
|
||||
type clause_pool_id
|
||||
(** Pool of clauses, with its own lifetime management *)
|
||||
|
||||
type theory
|
||||
|
||||
type proof
|
||||
|
|
@ -332,24 +315,6 @@ 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.
|
||||
We only expose an id, not a private type. *)
|
||||
|
||||
val clause_pool_descr : t -> clause_pool_id -> string
|
||||
|
||||
val new_clause_pool_gc_fixed_size :
|
||||
descr:string -> size:int -> t -> clause_pool_id
|
||||
(** Allocate a new clause pool that GC's its clauses when its size
|
||||
goes above [size]. It keeps half of the clauses. *)
|
||||
|
||||
(* TODO: scoped clause pool, which removes clauses automatically
|
||||
on backtrack. *)
|
||||
|
||||
(** {2 Types} *)
|
||||
|
||||
(** Result type for the solver *)
|
||||
|
|
@ -381,14 +346,6 @@ module type S = sig
|
|||
val add_input_clause_a : t -> lit array -> unit
|
||||
(** Like {!add_clause_a} but with justification of being an input clause *)
|
||||
|
||||
val add_clause_in_pool :
|
||||
t -> pool:clause_pool_id -> lit list -> proof_step -> unit
|
||||
(** Like {!add_clause} but using a specific clause pool *)
|
||||
|
||||
val add_clause_a_in_pool :
|
||||
t -> pool:clause_pool_id -> lit array -> proof_step -> unit
|
||||
(** Like {!add_clause_a} but using a specific clause pool *)
|
||||
|
||||
(** {2 Solving} *)
|
||||
|
||||
val solve : ?on_progress:(unit -> unit) -> ?assumptions:lit list -> t -> res
|
||||
|
|
|
|||
|
|
@ -387,12 +387,6 @@ module Make (A : ARG) :
|
|||
Stat.incr self.count_axiom;
|
||||
A.add_clause ~keep lits proof
|
||||
|
||||
let add_sat_clause_pool_ self (acts : theory_actions) ~pool lits
|
||||
(proof : proof_step) : unit =
|
||||
let (module A) = acts in
|
||||
Stat.incr self.count_axiom;
|
||||
A.add_clause_in_pool ~pool lits proof
|
||||
|
||||
let add_sat_lit_ _self ?default_pol (acts : theory_actions) (lit : Lit.t) :
|
||||
unit =
|
||||
let (module A) = acts in
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue