From d4ba4602a421d0270dadaa0a99e951374978ada5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 29 Jul 2022 22:28:21 -0400 Subject: [PATCH] refactor(sat): simplify interface a lot - pure_sat is not a functor anymore - make_cdcl_t is only functorized over theory - both use standard `Lit.t` and proofs --- src/sat/Proof_dummy.ml | 31 --------- src/sat/Sidekick_sat.ml | 19 ++---- src/sat/Solver.ml | 135 ++++++++++++++++-------------------- src/sat/Solver.mli | 15 +--- src/sat/Solver_intf.ml | 148 ++++++++++++---------------------------- src/sat/dune | 5 +- 6 files changed, 111 insertions(+), 242 deletions(-) delete mode 100644 src/sat/Proof_dummy.ml diff --git a/src/sat/Proof_dummy.ml b/src/sat/Proof_dummy.ml deleted file mode 100644 index 947be4b4..00000000 --- a/src/sat/Proof_dummy.ml +++ /dev/null @@ -1,31 +0,0 @@ -(** Dummy proof module using rule=[unit]. - - These proof traces will not record anything. *) - -module Make (Lit : sig - type t -end) : sig - module Proof_trace : - Sidekick_sigs_proof_trace.S - with type A.rule = unit - and type A.step_id = unit - and type t = unit - - module Proof_rules : - Solver_intf.PROOF_RULES - with type lit = Lit.t - and type rule = unit - and type step_id = unit -end = struct - module Proof_trace = Sidekick_proof_trace_dummy.Unit - - module Proof_rules = struct - type lit = Lit.t - type rule = unit - type step_id = unit - - let sat_input_clause _ = () - let sat_redundant_clause _ ~hyps:_ = () - let sat_unsat_core _ = () - end -end diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml index 2210b271..bbbb6089 100644 --- a/src/sat/Sidekick_sat.ml +++ b/src/sat/Sidekick_sat.ml @@ -1,29 +1,25 @@ (** Main API *) +open Sidekick_core module Solver_intf = Solver_intf module type S = Solver_intf.S module type LIT = Solver_intf.LIT module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T -module type PLUGIN_SAT = Solver_intf.PLUGIN_SAT -module type PROOF_RULES = Solver_intf.PROOF_RULES type lbool = Solver_intf.lbool = L_true | L_false | L_undefined module type SAT_STATE = Solver_intf.SAT_STATE -type 'form sat_state = 'form Solver_intf.sat_state +type sat_state = Solver_intf.sat_state -type ('lit, 'proof) reason = ('lit, 'proof) Solver_intf.reason = - | Consequence of (unit -> 'lit list * 'proof) +type reason = Solver_intf.reason = + | Consequence of (unit -> Lit.t list * Proof_step.id) [@@unboxed] module type ACTS = Solver_intf.ACTS -type ('lit, 'proof, 'proof_step) acts = - ('lit, 'proof, 'proof_step) Solver_intf.acts - -type negated = bool +type acts = (module ACTS) (** Print {!lbool} values *) let pp_lbool out = function @@ -36,7 +32,4 @@ exception Resource_exhausted = Solver_intf.Resource_exhausted module Solver = Solver module Make_cdcl_t = Solver.Make_cdcl_t -module Make_pure_sat = Solver.Make_pure_sat - -module Proof_dummy = Proof_dummy -(** Module for dummy proofs based on unit *) +module Pure_sat = Solver.Pure_sat diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 1d33c63c..58a9a986 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -1,3 +1,5 @@ +open Sidekick_core + module type PLUGIN = sig val has_theory : bool (** [true] iff the solver is parametrized by a theory, not just @@ -13,16 +15,9 @@ let invalid_argf fmt = Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) fmt module Make (Plugin : PLUGIN) = struct - module Lit = Plugin.Lit - module Proof_trace = Plugin.Proof_trace - module Proof_rules = Plugin.Proof_rules - module Step_vec = Proof_trace.A.Step_vec + module Step_vec = Proof_trace.Step_vec - type lit = Plugin.Lit.t type theory = Plugin.t - type proof_rule = Proof_trace.A.rule - type proof_step = Proof_trace.A.step_id - type proof_trace = Proof_trace.t module Clause_pool_id : sig type t = private int @@ -128,10 +123,10 @@ module Make (Plugin : PLUGIN) = struct (* atoms *) a_is_true: Bitvec.t; a_seen: Bitvec.t; - a_form: lit Vec.t; + a_form: Lit.t Vec.t; (* TODO: store watches in clauses instead *) a_watched: Clause0.CVec.t Vec.t; - a_proof_lvl0: proof_step ATbl.t; + a_proof_lvl0: Proof_step.id ATbl.t; (* atom -> proof for it to be true at level 0 *) stat_n_atoms: int Stat.counter; (* clauses *) @@ -296,9 +291,9 @@ module Make (Plugin : PLUGIN) = struct (** Make a clause with the given atoms *) - val make_a : store -> removable:bool -> atom array -> proof_step -> t - val make_l : store -> removable:bool -> atom list -> proof_step -> t - val make_vec : store -> removable:bool -> atom Vec.t -> proof_step -> t + val make_a : store -> removable:bool -> atom array -> Proof_step.id -> t + val make_l : store -> removable:bool -> atom list -> Proof_step.id -> t + val make_vec : store -> removable:bool -> atom Vec.t -> Proof_step.id -> t val n_atoms : store -> t -> int val marked : store -> t -> bool val set_marked : store -> t -> bool -> unit @@ -312,8 +307,8 @@ module Make (Plugin : PLUGIN) = struct val dealloc : store -> t -> unit (** Delete the clause *) - val set_proof_step : store -> t -> proof_step -> unit - val proof_step : store -> t -> proof_step + val set_proof_step : store -> t -> Proof_step.id -> unit + val proof_step : store -> t -> Proof_step.id val activity : store -> t -> float val set_activity : store -> t -> float -> unit val iter : store -> f:(atom -> unit) -> t -> unit @@ -321,9 +316,9 @@ module Make (Plugin : PLUGIN) = struct val for_all : store -> f:(atom -> bool) -> t -> bool val exists : store -> f:(atom -> bool) -> t -> bool val atoms_a : store -> t -> atom array - val lits_l : store -> t -> lit list - val lits_a : store -> t -> lit array - val lits_iter : store -> t -> lit Iter.t + val lits_l : store -> t -> Lit.t list + val lits_a : store -> t -> Lit.t array + val lits_iter : store -> t -> Lit.t Iter.t val short_name : store -> t -> string val pp : store -> Format.formatter -> t -> unit val debug : store -> Format.formatter -> t -> unit @@ -485,15 +480,15 @@ module Make (Plugin : PLUGIN) = struct let[@inline] atoms_a store c : atom array = Vec.get store.c_store.c_lits (c : t :> int) - let lits_l store c : lit list = + let lits_l store c : Lit.t list = let arr = atoms_a store c in Util.array_to_list_map (Atom.lit store) arr - let lits_a store c : lit array = + let lits_a store c : Lit.t array = let arr = atoms_a store c in Array.map (Atom.lit store) arr - let lits_iter store c : lit Iter.t = + let lits_iter store c : Lit.t Iter.t = let arr = atoms_a store c in Iter.of_array arr |> Iter.map (Atom.lit store) @@ -512,7 +507,8 @@ module Make (Plugin : PLUGIN) = struct end (* allocate new variable *) - let alloc_var_uncached_ ?default_pol:(pol = true) self (form : lit) : var = + let alloc_var_uncached_ ?default_pol:(pol = true) self (form : Lit.t) : var + = let { v_count; v_of_lit; @@ -560,7 +556,7 @@ module Make (Plugin : PLUGIN) = struct v (* create new variable *) - let alloc_var (self : t) ?default_pol (lit : lit) : + let alloc_var (self : t) ?default_pol (lit : Lit.t) : var * Solver_intf.same_sign = let lit, same_sign = Lit.norm_sign lit in try Lit_tbl.find self.v_of_lit lit, same_sign @@ -882,9 +878,9 @@ module Make (Plugin : PLUGIN) = struct mutable clause_incr: float; (* increment for clauses' activity *) (* FIXME: use event *) on_conflict: (Clause.t, unit) Event.Emitter.t; - on_decision: (lit, unit) Event.Emitter.t; + on_decision: (Lit.t, unit) Event.Emitter.t; on_learnt: (Clause.t, unit) Event.Emitter.t; - on_gc: (lit array, unit) Event.Emitter.t; + on_gc: (Lit.t array, unit) Event.Emitter.t; stat: Stat.t; n_conflicts: int Stat.counter; n_propagations: int Stat.counter; @@ -975,11 +971,11 @@ module Make (Plugin : PLUGIN) = struct let[@inline] insert_var_order st (v : var) : unit = H.insert st.order v (* find atom for the lit, if any *) - let[@inline] find_atom_ (self : t) (p : lit) : atom option = + let[@inline] find_atom_ (self : t) (p : Lit.t) : atom option = Store.find_atom self.store p (* create a new atom, pushing it into the decision queue if needed *) - let make_atom_ (self : t) ?default_pol (p : lit) : atom = + let make_atom_ (self : t) ?default_pol (p : Lit.t) : atom = let a = Store.alloc_atom self.store ?default_pol p in if Atom.level self.store a < 0 then insert_var_order self (Atom.var a) @@ -1041,7 +1037,7 @@ module Make (Plugin : PLUGIN) = struct (* get/build the proof for [a], which must be an atom true at level 0. This uses a global cache to avoid repeated computations, as many clauses might resolve against a given 0-level atom. *) - let rec proof_of_atom_lvl0_ (self : t) (a : atom) : proof_step = + let rec proof_of_atom_lvl0_ (self : t) (a : atom) : Proof_step.id = assert (Atom.is_true self.store a && Atom.level self.store a = 0); match Atom.proof_lvl0 self.store a with @@ -1075,7 +1071,7 @@ module Make (Plugin : PLUGIN) = struct proof_c2 else Proof_trace.add_step self.proof - @@ Proof_rules.sat_redundant_clause + @@ Proof_sat.sat_redundant_clause (Iter.return (Atom.lit self.store a)) ~hyps:Iter.(cons proof_c2 (of_list !steps)) in @@ -1168,7 +1164,7 @@ module Make (Plugin : PLUGIN) = struct let proof = let lits = Iter.of_array atoms |> Iter.map (Atom.lit store) in Proof_trace.add_step self.proof - @@ Proof_rules.sat_redundant_clause lits + @@ Proof_sat.sat_redundant_clause lits ~hyps: Iter.( cons (Clause.proof_step self.store c) (of_list !res0_proofs)) @@ -1282,7 +1278,7 @@ module Make (Plugin : PLUGIN) = struct let p_empty = Proof_trace.add_step self.proof - @@ Proof_rules.sat_redundant_clause Iter.empty + @@ Proof_sat.sat_redundant_clause Iter.empty ~hyps:(Step_vec.to_iter pvec) in Step_vec.clear pvec; @@ -1643,7 +1639,7 @@ module Make (Plugin : PLUGIN) = struct let p = Proof_trace.add_step self.proof - @@ Proof_rules.sat_redundant_clause + @@ Proof_sat.sat_redundant_clause (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store)) ~hyps:(Step_vec.to_iter cr.cr_steps) in @@ -1660,7 +1656,7 @@ module Make (Plugin : PLUGIN) = struct let fuip = cr.cr_learnt.(0) in let p = Proof_trace.add_step self.proof - @@ Proof_rules.sat_redundant_clause + @@ Proof_sat.sat_redundant_clause (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store)) ~hyps:(Step_vec.to_iter cr.cr_steps) in @@ -1842,8 +1838,8 @@ module Make (Plugin : PLUGIN) = struct let[@inline] slice_get st i = AVec.get st.trail i - let acts_add_clause self ?(keep = false) (l : lit list) (p : proof_step) : - unit = + let acts_add_clause self ?(keep = false) (l : Lit.t list) (p : Proof_step.id) + : unit = let atoms = List.rev_map (make_atom_ self) l in let removable = not keep in let c = Clause.make_l self.store ~removable atoms p in @@ -1852,8 +1848,8 @@ module Make (Plugin : PLUGIN) = struct (* will be added later, even if we backtrack *) Delayed_actions.add_clause_learnt self.delayed_actions c - let acts_add_clause_in_pool self ~pool (l : lit list) (p : proof_step) : unit - = + let acts_add_clause_in_pool self ~pool (l : Lit.t list) (p : Proof_step.id) : + unit = 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 @@ -1864,7 +1860,7 @@ module Make (Plugin : PLUGIN) = struct (* will be added later, even if we backtrack *) Delayed_actions.add_clause_pool self.delayed_actions c pool - let acts_add_decision_lit (self : t) (f : lit) (sign : bool) : unit = + let acts_add_decision_lit (self : t) (f : Lit.t) (sign : bool) : unit = let store = self.store in let a = make_atom_ self f in let a = @@ -1879,7 +1875,7 @@ module Make (Plugin : PLUGIN) = struct Delayed_actions.add_decision self.delayed_actions a ) - let acts_raise self (l : lit list) (p : proof_step) : 'a = + let acts_raise self (l : Lit.t list) (p : Proof_step.id) : 'a = let atoms = List.rev_map (make_atom_ self) l in (* conflicts can be removed *) let c = Clause.make_l self.store ~removable:true atoms p in @@ -1903,7 +1899,7 @@ module Make (Plugin : PLUGIN) = struct (Atom.debug store) (Atom.neg a) | exception Not_found -> () - let acts_propagate (self : t) f (expl : (_, proof_step) Solver_intf.reason) = + let acts_propagate (self : t) f (expl : Solver_intf.reason) = let store = self.store in match expl with | Solver_intf.Consequence mk_expl -> @@ -1994,19 +1990,15 @@ module Make (Plugin : PLUGIN) = struct else Solver_intf.L_undefined - let[@inline] acts_eval_lit self (f : lit) : Solver_intf.lbool = + let[@inline] acts_eval_lit self (f : Lit.t) : Solver_intf.lbool = let a = make_atom_ self f in eval_atom_ self a let[@inline] acts_add_lit self ?default_pol f : unit = ignore (make_atom_ ?default_pol self f : atom) - let[@inline] current_slice st : _ Solver_intf.acts = + let[@inline] current_slice st : Solver_intf.acts = let module M = struct - type nonrec proof = Proof_trace.t - type nonrec proof_step = proof_step - type nonrec lit = lit - let proof = st.proof let iter_assumptions = acts_iter st ~full:false st.th_head let eval_lit = acts_eval_lit st @@ -2019,12 +2011,8 @@ module Make (Plugin : PLUGIN) = struct (module M) (* full slice, for [if_sat] final check *) - let[@inline] full_slice st : _ Solver_intf.acts = + let[@inline] full_slice st : Solver_intf.acts = let module M = struct - type nonrec proof = Proof_trace.t - type nonrec proof_step = proof_step - type nonrec lit = lit - let proof = st.proof let iter_assumptions = acts_iter st ~full:true st.th_head let eval_lit = acts_eval_lit st @@ -2403,7 +2391,7 @@ module Make (Plugin : PLUGIN) = struct let atoms = Util.array_of_list_map (make_atom_ self) l in let proof = Proof_trace.add_step self.proof - @@ Proof_rules.sat_input_clause (Iter.of_list l) + @@ Proof_sat.sat_input_clause (Iter.of_list l) in let c = Clause.make_a self.store ~removable:false atoms proof in Log.debugf 10 (fun k -> @@ -2419,14 +2407,14 @@ module Make (Plugin : PLUGIN) = struct let[@inline] add_lit self ?default_pol lit = ignore (make_atom_ self lit ?default_pol : atom) - let[@inline] set_default_pol (self : t) (lit : lit) (pol : bool) : unit = + let[@inline] set_default_pol (self : t) (lit : Lit.t) (pol : bool) : unit = let a = make_atom_ self lit ~default_pol:pol in Var.set_default_pol self.store (Atom.var a) pol (* Result type *) type res = - | Sat of Lit.t Solver_intf.sat_state - | Unsat of (lit, clause, proof_step) Solver_intf.unsat_state + | Sat of Solver_intf.sat_state + | Unsat of clause Solver_intf.unsat_state let pp_all self lvl status = Log.debugf lvl (fun k -> @@ -2447,7 +2435,7 @@ module Make (Plugin : PLUGIN) = struct (Util.pp_iter @@ Clause.debug self.store) (cp_to_iter_ self.clauses_learnt)) - let mk_sat (self : t) : Lit.t Solver_intf.sat_state = + let mk_sat (self : t) : Solver_intf.sat_state = pp_all self 99 "SAT"; let t = self.trail in let module M = struct @@ -2495,7 +2483,7 @@ module Make (Plugin : PLUGIN) = struct let lits = Iter.of_list !res |> Iter.map (Atom.lit self.store) in let hyps = Iter.of_list (Clause.proof_step self.store c :: !lvl0) in Proof_trace.add_step self.proof - @@ Proof_rules.sat_redundant_clause lits ~hyps + @@ Proof_sat.sat_redundant_clause lits ~hyps in Clause.make_l self.store ~removable:false !res proof ) @@ -2530,16 +2518,13 @@ module Make (Plugin : PLUGIN) = struct assert (Atom.equal first @@ List.hd core); let proof = let lits = Iter.of_list core |> Iter.map (Atom.lit self.store) in - Proof_trace.add_step self.proof - @@ Proof_rules.sat_unsat_core lits + Proof_trace.add_step self.proof @@ Proof_sat.sat_unsat_core lits in Clause.make_l self.store ~removable:false [] proof) in fun () -> Lazy.force c in let module M = struct - type nonrec lit = lit - type nonrec proof_step = proof_step type clause = Clause.t let unsat_conflict = unsat_conflict @@ -2554,7 +2539,7 @@ module Make (Plugin : PLUGIN) = struct type propagation_result = | PR_sat | PR_conflict of { backtracked: int } - | PR_unsat of (lit, clause, proof_step) Solver_intf.unsat_state + | PR_unsat of clause Solver_intf.unsat_state (* decide on assumptions, and do propagations, but no other kind of decision *) let propagate_under_assumptions (self : t) : propagation_result = @@ -2591,8 +2576,8 @@ module Make (Plugin : PLUGIN) = struct assert false with Exit -> !result - let add_clause_atoms_ self ~pool ~removable (c : atom array) (pr : proof_step) - : unit = + let add_clause_atoms_ self ~pool ~removable (c : atom array) + (pr : Proof_step.id) : unit = try let c = Clause.make_a self.store ~removable c pr in add_clause_ ~pool self c @@ -2602,26 +2587,26 @@ module Make (Plugin : PLUGIN) = struct let c = Array.map (make_atom_ self) c in add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c pr - let add_clause self (c : lit list) (pr : proof_step) : unit = + let add_clause self (c : Lit.t list) (pr : Proof_step.id) : unit = 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_input_clause self (c : lit list) = + let add_input_clause self (c : Lit.t list) = let pr = Proof_trace.add_step self.proof - @@ Proof_rules.sat_input_clause (Iter.of_list c) + @@ Proof_sat.sat_input_clause (Iter.of_list c) in add_clause self c pr let add_input_clause_a self c = let pr = Proof_trace.add_step self.proof - @@ Proof_rules.sat_input_clause (Iter.of_array c) + @@ Proof_sat.sat_input_clause (Iter.of_array c) in add_clause_a self c pr (* run [f()] with additional assumptions *) - let with_local_assumptions_ (self : t) (assumptions : lit list) f = + let with_local_assumptions_ (self : t) (assumptions : Lit.t list) f = let old_assm_lvl = AVec.size self.assumptions in List.iter (fun lit -> @@ -2645,7 +2630,7 @@ module Make (Plugin : PLUGIN) = struct Sat (mk_sat self) with E_unsat us -> Unsat (mk_unsat self us) - let push_assumption (self : t) (lit : lit) : unit = + let push_assumption (self : t) (lit : Lit.t) : unit = let a = make_atom_ self lit in AVec.push self.assumptions a @@ -2667,7 +2652,7 @@ module Make (Plugin : PLUGIN) = struct let us = mk_unsat self us in PR_unsat us - let true_at_level0 (self : t) (lit : lit) : bool = + let true_at_level0 (self : t) (lit : Lit.t) : bool = match find_atom_ self lit with | None -> false | Some a -> @@ -2676,7 +2661,7 @@ module Make (Plugin : PLUGIN) = struct b && lev = 0 with UndecidedLit -> false) - let[@inline] eval_lit self (lit : lit) : Solver_intf.lbool = + let[@inline] eval_lit self (lit : Lit.t) : Solver_intf.lbool = match find_atom_ self lit with | Some a -> eval_atom_ self a | None -> Solver_intf.L_undefined @@ -2690,11 +2675,7 @@ module Make_cdcl_t (Plugin : Solver_intf.PLUGIN_CDCL_T) = Make (struct end) [@@inline] [@@specialise] -module Make_pure_sat (Plugin : Solver_intf.PLUGIN_SAT) = Make (struct - module Lit = Plugin.Lit - module Proof_trace = Plugin.Proof_trace - module Proof_rules = Plugin.Proof_rules - +module Pure_sat = Make (struct type t = unit let push_level () = () diff --git a/src/sat/Solver.mli b/src/sat/Solver.mli index 3a0858d0..499e94ee 100644 --- a/src/sat/Solver.mli +++ b/src/sat/Solver.mli @@ -1,16 +1,5 @@ module type S = Solver_intf.S (** Safe external interface of solvers. *) -module Make_pure_sat (Th : Solver_intf.PLUGIN_SAT) : - S - with module Lit = Th.Lit - and module Proof_trace = Th.Proof_trace - and module Proof_rules = Th.Proof_rules - and type theory = unit - -module Make_cdcl_t (Th : Solver_intf.PLUGIN_CDCL_T) : - S - with module Lit = Th.Lit - and module Proof_trace = Th.Proof_trace - and module Proof_rules = Th.Proof_rules - and type theory = Th.t +module Pure_sat : S with type theory = unit +module Make_cdcl_t (Th : Solver_intf.PLUGIN_CDCL_T) : S with type theory = Th.t diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index a0797607..f3630ba0 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -11,53 +11,46 @@ Copyright 2016 Guillaume Bury Copyright 2016 Simon Cruanes *) +open Sidekick_core + type 'a printer = Format.formatter -> 'a -> unit (** Solver in a "SATISFIABLE" state *) module type SAT_STATE = sig - type lit - (** Literals (signed boolean atoms) *) - - val eval : lit -> bool + val eval : Lit.t -> bool (** Returns the valuation of a lit in the current state of the sat solver. @raise UndecidedLit if the literal is not decided *) - val eval_level : lit -> bool * int + val eval_level : Lit.t -> bool * int (** Return the current assignement of the literals, as well as its decision level. If the level is 0, then it is necessary for the literal to have this value; otherwise it is due to choices that can potentially be backtracked. @raise UndecidedLit if the literal is not decided *) - val iter_trail : (lit -> unit) -> unit + val iter_trail : (Lit.t -> unit) -> unit (** Iter through the lits in order of decision/propagation (starting from the first propagation, to the last propagation). *) end -type 'form sat_state = (module SAT_STATE with type lit = 'form) +type sat_state = (module SAT_STATE) (** 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 - type proof_step val unsat_conflict : unit -> clause (** Returns the unsat clause found at the toplevel *) - val unsat_assumptions : unit -> lit Iter.t + val unsat_assumptions : unit -> Lit.t Iter.t (** Subset of assumptions responsible for "unsat" *) - val unsat_proof : unit -> proof_step + val unsat_proof : unit -> Proof_term.step_id end -type ('lit, 'clause, 'proof_step) unsat_state = - (module UNSAT_STATE - with type lit = 'lit - and type clause = 'clause - and type proof_step = 'proof_step) +type 'clause unsat_state = (module UNSAT_STATE with type clause = 'clause) (** The type of values returned when the solver reaches an UNSAT state. *) type same_sign = bool @@ -65,9 +58,7 @@ type same_sign = bool [true] means the literal stayed the same, [false] that its sign was flipped. *) (** The type of reasons for propagations of a lit [f]. *) -type ('lit, 'proof_step) reason = - | Consequence of (unit -> 'lit list * 'proof_step) -[@@unboxed] +type reason = Consequence of (unit -> Lit.t list * Proof_step.id) [@@unboxed] (** [Consequence (l, p)] means that the lits in [l] imply the propagated lit [f]. The proof should be a proof of the clause "[l] implies [f]". @@ -95,23 +86,19 @@ type lbool = L_true | L_false | L_undefined (** Valuation of an atom *) are provided with a [(module ACTS)] so they can modify the SAT solver by adding new lemmas, raise conflicts, etc. *) module type ACTS = sig - type lit - type proof - type proof_step + val proof : Proof_trace.t - val proof : proof - - val iter_assumptions : (lit -> unit) -> unit + val iter_assumptions : (Lit.t -> unit) -> unit (** Traverse the new assumptions on the boolean trail. *) - val eval_lit : lit -> lbool + val eval_lit : Lit.t -> lbool (** Obtain current value of the given literal *) - val add_lit : ?default_pol:bool -> lit -> unit + val add_lit : ?default_pol:bool -> Lit.t -> unit (** Map the given lit to an internal atom, which will be decided by the SAT solver. *) - val add_clause : ?keep:bool -> lit list -> proof_step -> unit + val add_clause : ?keep:bool -> Lit.t list -> Proof_step.id -> unit (** Add a clause to the solver. @param keep if true, the clause will be kept by the solver. Otherwise the solver is allowed to GC the clause and propose this @@ -119,26 +106,22 @@ module type ACTS = sig - [C_use_allocator alloc] puts the clause in the given allocator. *) - val raise_conflict : lit list -> proof_step -> 'b + val raise_conflict : Lit.t list -> Proof_step.id -> '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 current trail. *) - val propagate : lit -> (lit, proof_step) reason -> unit + val propagate : Lit.t -> reason -> unit (** Propagate a lit, i.e. the theory can evaluate the lit to be true (see the definition of {!type:eval_res} *) - val add_decision_lit : lit -> bool -> unit + val add_decision_lit : Lit.t -> bool -> unit (** Ask the SAT solver to decide on the given lit with given sign before it can answer [SAT]. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking. *) end -type ('lit, 'proof, 'proof_step) acts = - (module ACTS - with type lit = 'lit - and type proof = 'proof - and type proof_step = 'proof_step) +type acts = (module ACTS) (** The type for a slice of assertions to assume/propagate in the theory. *) exception No_proof @@ -169,77 +152,39 @@ module type LIT = sig but one returns [false] and the other [true]. *) end -module type PROOF_RULES = Sidekick_sigs_proof_sat.S - (** Signature for theories to be given to the CDCL(T) solver *) module type PLUGIN_CDCL_T = sig type t (** The plugin state itself *) - module Lit : LIT - module Proof_trace : Sidekick_sigs_proof_trace.S - - module Proof_rules : - PROOF_RULES - with type lit = Lit.t - and type rule = Proof_trace.A.rule - and type step_id = Proof_trace.A.step_id - val push_level : t -> unit (** Create a new backtrack level *) val pop_levels : t -> int -> unit (** Pop [n] levels of the theory *) - val partial_check : - t -> (Lit.t, Proof_trace.t, Proof_trace.A.step_id) acts -> unit + val partial_check : t -> acts -> unit (** Assume the lits in the slice, possibly using the [slice] to push new lits to be propagated or to raising a conflict or to add new lemmas. *) - val final_check : - t -> (Lit.t, Proof_trace.t, Proof_trace.A.step_id) acts -> unit + val final_check : t -> acts -> unit (** Called at the end of the search in case a model has been found. If no new clause is pushed, then proof search ends and "sat" is returned; if lemmas are added, search is resumed; if a conflict clause is added, search backtracks and then resumes. *) end -(** Signature for pure SAT solvers *) -module type PLUGIN_SAT = sig - module Lit : LIT - module Proof_trace : Sidekick_sigs_proof_trace.S - - module Proof_rules : - PROOF_RULES - with type lit = Lit.t - and type rule = Proof_trace.A.rule - and type step_id = Proof_trace.A.step_id -end - exception Resource_exhausted (** Can be raised in a progress handler *) (** The external interface implemented by safe solvers, such as the one created by the {!Solver.Make} and {!Mcsolver.Make} functors. *) module type S = sig - (** {2 Internal modules} - These are the internal modules used, you should probably not use them - if you're not familiar with the internals of mSAT. *) - - module Lit : LIT - module Proof_trace : Sidekick_sigs_proof_trace.S - - type lit = Lit.t (** literals *) type clause type theory - type proof_rule = Proof_trace.A.rule - type proof_step = Proof_trace.A.step_id - - type proof_trace = Proof_trace.t - (** A representation of a full proof *) type solver (** The main solver type. *) @@ -262,23 +207,16 @@ module type S = sig val n_atoms : store -> t -> int - val lits_iter : store -> t -> lit Iter.t + val lits_iter : store -> t -> Lit.t Iter.t (** Literals of a clause *) - val lits_a : store -> t -> lit array + val lits_a : store -> t -> Lit.t array (** Atoms of a clause *) - val lits_l : store -> t -> lit list + val lits_l : store -> t -> Lit.t list (** List of atoms of a clause *) end - (** Proof rules for SAT solving *) - module Proof_rules : - PROOF_RULES - with type lit = lit - and type rule = proof_rule - and type step_id = proof_step - (** {2 Main Solver Type} *) type t = solver @@ -287,7 +225,7 @@ module type S = sig val create : ?stat:Stat.t -> ?size:[ `Tiny | `Small | `Big ] -> - proof:proof_trace -> + proof:Proof_trace.t -> theory -> t (** Create new solver @@ -305,21 +243,21 @@ module type S = sig val stat : t -> Stat.t (** Statistics *) - val proof : t -> proof_trace + val proof : t -> Proof_trace.t (** Access the inner proof *) val on_conflict : t -> (Clause.t, unit) Event.t - val on_decision : t -> (lit, unit) Event.t + val on_decision : t -> (Lit.t, unit) Event.t val on_learnt : t -> (Clause.t, unit) Event.t - val on_gc : t -> (lit array, unit) Event.t + val on_gc : t -> (Lit.t array, unit) Event.t (** {2 Types} *) (** Result type for the solver *) type res = - | Sat of lit sat_state + | Sat of sat_state (** Returned when the solver reaches SAT, with a model *) - | Unsat of (lit, clause, proof_step) unsat_state + | Unsat of clause unsat_state (** Returned when the solver reaches UNSAT, with a proof *) exception UndecidedLit @@ -328,25 +266,25 @@ module type S = sig (** {2 Base operations} *) - val assume : t -> lit list list -> unit + val assume : t -> Lit.t list list -> unit (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *) - val add_clause : t -> lit list -> proof_step -> unit + val add_clause : t -> Lit.t list -> Proof_step.id -> unit (** Lower level addition of clauses *) - val add_clause_a : t -> lit array -> proof_step -> unit + val add_clause_a : t -> Lit.t array -> Proof_step.id -> unit (** Lower level addition of clauses *) - val add_input_clause : t -> lit list -> unit + val add_input_clause : t -> Lit.t list -> unit (** Like {!add_clause} but with the justification of being an input clause *) - val add_input_clause_a : t -> lit array -> unit + val add_input_clause_a : t -> Lit.t array -> unit (** Like {!add_clause_a} but with justification of being an input clause *) (** {2 Solving} *) - val solve : ?on_progress:(unit -> unit) -> ?assumptions:lit list -> t -> res + val solve : ?on_progress:(unit -> unit) -> ?assumptions:Lit.t list -> t -> res (** Try and solves the current set of clauses. @param assumptions additional atomic assumptions to be temporarily added. The assumptions are just used for this call to [solve], they are @@ -360,24 +298,24 @@ module type S = sig (** {2 Evaluating and adding literals} *) - val add_lit : t -> ?default_pol:bool -> lit -> unit + val add_lit : t -> ?default_pol:bool -> Lit.t -> unit (** Ensure the SAT solver handles this particular literal, ie add a boolean variable for it if it's not already there. *) - val set_default_pol : t -> lit -> bool -> unit + val set_default_pol : t -> Lit.t -> bool -> unit (** Set default polarity for the given boolean variable. Sign of the literal is ignored. *) - val true_at_level0 : t -> lit -> bool + val true_at_level0 : t -> Lit.t -> bool (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e. it must hold in all models *) - val eval_lit : t -> lit -> lbool + val eval_lit : t -> Lit.t -> lbool (** Evaluate atom in current state *) (** {2 Assumption stack} *) - val push_assumption : t -> lit -> unit + val push_assumption : t -> Lit.t -> unit (** Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by {!pop_assumptions}. *) @@ -390,10 +328,10 @@ module type S = sig type propagation_result = | PR_sat | PR_conflict of { backtracked: int } - | PR_unsat of (lit, clause, proof_step) unsat_state + | PR_unsat of clause unsat_state val check_sat_propagations_only : - ?assumptions:lit list -> t -> propagation_result + ?assumptions:Lit.t list -> t -> propagation_result (** [check_sat_propagations_only solver] uses the added clauses and local assumptions (using {!push_assumptions} and [assumptions]) to quickly assess whether the context is satisfiable. diff --git a/src/sat/dune b/src/sat/dune index b912a7b6..56fdf8e7 100644 --- a/src/sat/dune +++ b/src/sat/dune @@ -1,7 +1,6 @@ (library (name sidekick_sat) (public_name sidekick.sat) - (libraries iter sidekick.util sidekick.core sidekick.sigs.proof-trace - sidekick.proof-trace.dummy) (synopsis "Pure OCaml SAT solver implementation for sidekick") - (flags :standard -open Sidekick_util)) + (libraries iter sidekick.util sidekick.core) + (flags :standard -w +32 -open Sidekick_util))