From 7bead748a6d5e1804360c7eec389cd85d41bda18 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 17 Aug 2021 23:59:02 -0400 Subject: [PATCH] refactor: move SAT_PROOF into sidekick.core SAT proofs are part of bigger proofs, now. And we expect them to work on the literals of CDCL(T) directly, bypassing the low level boolean atoms --- src/core/Sidekick_core.ml | 95 ++++++++++-------- src/sat/Solver.ml | 200 ++++++++++++++------------------------ src/sat/Solver.mli | 10 +- src/sat/Solver_intf.ml | 111 ++++++--------------- src/sat/dune | 2 +- 5 files changed, 169 insertions(+), 249 deletions(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 8a7a5eb0..df32bdc3 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -155,6 +155,35 @@ module type CC_PROOF = sig of uninterpreted functions. *) end +(** Signature for SAT-solver proof emission, using DRUP. + + We do not store the resolution steps, just the stream of clauses deduced. + See {!Sidekick_drup} for checking these proofs. *) +module type SAT_PROOF = sig + type t + (** The stored proof (possibly nil, possibly on disk, possibly in memory) *) + + type lit + (** A boolean literal for the proof trace *) + + type dproof = t -> unit + (** A delayed proof, used to produce proofs on demand from theories. *) + + val enabled : t -> bool + (** Do we emit proofs at all? *) + + val emit_input_clause : t -> lit Iter.t -> unit + (** Emit an input clause. *) + + val emit_redundant_clause : t -> lit Iter.t -> unit + (** Emit a clause deduced by the SAT solver, redundant wrt axioms. + The clause must be RUP wrt previous clauses. *) + + val del_clause : t -> lit Iter.t -> unit + (** Forget a clause. Only useful for performance considerations. *) + (* TODO: replace with something index-based? *) +end + (** Proofs of unsatisfiability. We use DRUP(T)-style traces where we simply emit clauses as we go, @@ -173,19 +202,26 @@ module type PROOF = sig with type t := t and type lit := lit + include SAT_PROOF + with type t := t + and type lit := lit + val begin_subproof : t -> unit (** Begins a subproof. The result of this will only be the clause with which {!end_subproof} is called; all other intermediate steps will be discarded. *) - val end_subproof : t -> lit Iter.t -> unit - (** [end_subproof p lits] ends the current active subproof, which {b must} - prove the clause [lits] by RUP. *) + val end_subproof : t -> unit + (** [end_subproof p] ends the current active subproof, the last result + of which is kept. *) val define_term : t -> term -> term -> unit (** [define_term p cst u] defines the new constant [cst] as being equal to [u]. *) + val lemma_true : t -> term -> unit + (** [lemma_true p (true)] asserts the clause [(true)] *) + val lemma_preprocess : t -> term -> term -> unit (** [lemma_preprocess p t u] asserts that [t = u] is a tautology and that [t] has been preprocessed into [u]. @@ -223,6 +259,17 @@ module type LIT = sig (** [abs lit] is like [lit] but always positive, i.e. [sign (abs lit) = true] *) val signed_term : t -> T.Term.t * bool + (** Return the atom and the sign *) + + val atom : T.Term.store -> ?sign:bool -> T.Term.t -> t + (** [atom store t] makes a literal out of a term, possibly normalizing + its sign in the process. + @param sign if provided, and [sign=false], negate the resulting lit. *) + + val norm_sign : t -> t * bool + (** [norm_sign (+t)] is [+t, true], + and [norm_sign (-t)] is [+t, false]. + In both cases the term is positive, and the boolean reflects the initial sign. *) val equal : t -> t -> bool val hash : t -> int @@ -594,6 +641,7 @@ end new lemmas, propagate literals, access the congruence closure, etc. *) module type SOLVER_INTERNAL = sig module T : TERM + module Lit : LIT with module T = T type ty = T.Ty.t type term = T.Term.t @@ -603,13 +651,6 @@ module type SOLVER_INTERNAL = sig type dproof = proof -> unit (** Delayed proof. This is used to build a proof step on demand. *) - (** {3 Literals} - - A literal is a (preprocessed) term along with its sign. - It is directly manipulated by the SAT solver. - *) - module Lit : LIT with module T = T - (** {3 Proofs} *) module P : PROOF with type lit = Lit.t and type term = term and type t = proof @@ -726,7 +767,7 @@ module type SOLVER_INTERNAL = sig (** Create a literal. This automatically preprocesses the term. *) val preprocess_term : - t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * dproof + t -> add_clause:(Lit.t list -> dproof -> unit) -> term -> term * dproof (** Preprocess a term. *) val add_lit : t -> actions -> lit -> unit @@ -989,7 +1030,7 @@ module type SOLVER = sig ?stat:Stat.t -> ?size:[`Big | `Tiny | `Small] -> (* TODO? ?config:Config.t -> *) - ?store_proof:bool -> + proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> @@ -1018,7 +1059,7 @@ module type SOLVER = sig val add_theory_l : t -> theory list -> unit - val mk_atom_lit : t -> lit -> Atom.t + val mk_atom_lit : t -> lit -> Atom.t * dproof (** [mk_atom_lit _ lit] returns [atom, pr] where [atom] is an internal atom for the solver, and [pr] is a proof of [|- lit = atom] *) @@ -1026,7 +1067,7 @@ module type SOLVER = sig val mk_atom_lit' : t -> lit -> Atom.t (** Like {!mk_atom_t} but skips the proof *) - val mk_atom_t : t -> ?sign:bool -> term -> Atom.t + val mk_atom_t : t -> ?sign:bool -> term -> Atom.t * dproof (** [mk_atom_t _ ~sign t] returns [atom, pr] where [atom] is an internal representation of [± t], and [pr] is a proof of [|- atom = (± t)] *) @@ -1034,11 +1075,11 @@ module type SOLVER = sig val mk_atom_t' : t -> ?sign:bool -> term -> Atom.t (** Like {!mk_atom_t} but skips the proof *) - val add_clause : t -> Atom.t IArray.t -> P.t -> unit + val add_clause : t -> Atom.t IArray.t -> dproof -> unit (** [add_clause solver cs] adds a boolean clause to the solver. Subsequent calls to {!solve} will need to satisfy this clause. *) - val add_clause_l : t -> Atom.t list -> P.t -> unit + val add_clause_l : t -> Atom.t list -> dproof -> unit (** Add a clause to the solver, given as a list. *) val assert_terms : t -> term list -> unit @@ -1049,32 +1090,10 @@ module type SOLVER = sig (** Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion *) - (** {2 Internal representation of proofs} - - A type or state convertible into {!P.t} *) - module Pre_proof : sig - type t - - val output : out_channel -> t -> unit - (** Output onto a channel, efficiently *) - - val pp_debug : t Fmt.printer - - val pp_dot : t Fmt.printer option - (** Optional printer into DOT/graphviz *) - - val check : t -> unit - (** Check the proof (to an unspecified level of confidence; - this can be a no-op). May fail. *) - - val to_proof : t -> P.t - end - (** Result of solving for the current set of clauses *) type res = | Sat of Model.t (** Satisfiable *) | Unsat of { - proof: Pre_proof.t option lazy_t; (** proof of unsat *) unsat_core: Atom.t list lazy_t; (** subset of assumptions responsible for unsat *) } (** Unsatisfiable *) | Unknown of Unknown.t diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 0c119711..abe763f4 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -33,14 +33,14 @@ end module Make(Plugin : PLUGIN) = struct + type formula = Plugin.formula + type theory = Plugin.t + type proof = Plugin.proof + type dproof = proof -> unit + module Formula = Plugin.Formula module Proof = Plugin.Proof - type formula = Formula.t - type theory = Plugin.t - type lemma = Plugin.lemma - type proof = Plugin.proof - (* ### types ### *) (* a boolean variable (positive int) *) @@ -88,27 +88,11 @@ module Make(Plugin : PLUGIN) end type clause = Clause0.t - (* TODO: remove, replace with user-provided proof trackng device? - for pure SAT, [reason] is sufficient *) - type premise = - | Hyp of lemma - | Local - | Lemma of lemma - | History of clause list - | Empty_premise - and reason = | Decision | Bcp of clause | Bcp_lazy of clause lazy_t - let kind_of_premise p = match p with - | Hyp _ -> "H" - | Lemma _ -> "T" - | Local -> "L" - | History _ -> "C" - | Empty_premise -> "" - (* ### stores ### *) module Form_tbl = Hashtbl.Make(Formula) @@ -118,7 +102,6 @@ module Make(Plugin : PLUGIN) type cstore = { c_lits: atom array Vec.t; (* storage for clause content *) c_activity: Vec_float.t; - c_premise: premise Vec.t; c_recycle_idx: VecI32.t; (* recycle clause numbers that were GC'd *) c_attached: Bitvec.t; c_marked: Bitvec.t; (* TODO : remove *) @@ -170,7 +153,6 @@ module Make(Plugin : PLUGIN) c_store={ c_lits=Vec.create(); c_activity=Vec_float.create(); - c_premise=Vec.create(); c_recycle_idx=VecI32.create ~cap:0 (); c_dead=Bitvec.create(); c_attached=Bitvec.create(); @@ -245,8 +227,7 @@ module Make(Plugin : PLUGIN) | n, None -> Format.fprintf out "%d" n | n, Some Decision -> Format.fprintf out "@@%d" n | n, Some Bcp c -> - let premise = Vec.get self.c_store.c_premise (c:>int) in - Format.fprintf out "->%d/%s/%d" n (kind_of_premise premise) (c:>int) + Format.fprintf out "->%d/%d" n (c:>int) | n, Some (Bcp_lazy _) -> Format.fprintf out "->%d/" n let pp_level self out a = @@ -274,11 +255,9 @@ module Make(Plugin : PLUGIN) (** Make a clause with the given atoms *) - val make_a : store -> removable:bool -> atom array -> premise -> t - val make_l : store -> removable:bool -> atom list -> premise -> t - val make_vec : store -> removable:bool -> atom Vec.t -> premise -> t - - val premise : store -> t -> premise + val make_a : store -> removable:bool -> atom array -> t + val make_l : store -> removable:bool -> atom list -> t + val make_vec : store -> removable:bool -> atom Vec.t -> t val n_atoms : store -> t -> int @@ -314,9 +293,9 @@ module Make(Plugin : PLUGIN) (* TODO: store watch lists inside clauses *) - let make_a (store:store) ~removable (atoms:atom array) premise : t = + let make_a (store:store) ~removable (atoms:atom array) : t = let { - c_recycle_idx; c_lits; c_activity; c_premise; + c_recycle_idx; c_lits; c_activity; c_attached; c_dead; c_removable; c_marked; } = store.c_store in (* allocate new ID *) @@ -330,7 +309,6 @@ module Make(Plugin : PLUGIN) begin let new_len = cid + 1 in Vec.ensure_size c_lits [||] new_len; - Vec.ensure_size c_premise Empty_premise new_len; Vec_float.ensure_size c_activity new_len; Bitvec.ensure_size c_attached new_len; Bitvec.ensure_size c_dead new_len; @@ -341,16 +319,15 @@ module Make(Plugin : PLUGIN) end; Vec.set c_lits cid atoms; - Vec.set c_premise cid premise; let c = of_int_unsafe cid in c - let make_l store ~removable atoms premise : t = - make_a store ~removable (Array.of_list atoms) premise + let make_l store ~removable atoms : t = + make_a store ~removable (Array.of_list atoms) - let make_vec store ~removable atoms premise : t = - make_a store ~removable (Vec.to_array atoms) premise + let make_vec store ~removable atoms : t = + make_a store ~removable (Vec.to_array atoms) let[@inline] n_atoms (store:store) (c:t) : int = Array.length (Vec.get store.c_store.c_lits (c:t:>int)) @@ -377,7 +354,6 @@ module Make(Plugin : PLUGIN) let {c_lits; _} = store.c_store in Array.fold_left f acc (Vec.get c_lits (c:t:>int)) - let[@inline] premise store c = Vec.get store.c_store.c_premise (c:t:>int) let[@inline] marked store c = Bitvec.get store.c_store.c_marked (c:t:>int) let[@inline] set_marked store c b = Bitvec.set store.c_store.c_marked (c:t:>int) b let[@inline] attached store c = Bitvec.get store.c_store.c_attached (c:t:>int) @@ -389,7 +365,7 @@ module Make(Plugin : PLUGIN) let dealloc store c : unit = assert (dead store c); - let {c_lits; c_premise; c_recycle_idx; c_activity; + let {c_lits; c_recycle_idx; c_activity; c_dead; c_removable; c_attached; c_marked; } = store.c_store in (* clear data *) @@ -399,7 +375,6 @@ module Make(Plugin : PLUGIN) Bitvec.set c_removable cid false; Bitvec.set c_marked cid false; Vec.set c_lits cid [||]; - Vec.set c_premise cid Empty_premise; Vec_float.set c_activity cid 0.; VecI32.push c_recycle_idx cid; (* recycle idx *) @@ -412,14 +387,14 @@ module Make(Plugin : PLUGIN) let[@inline] activity store c = Vec_float.get store.c_store.c_activity (c:t:>int) let[@inline] set_activity store c f = Vec_float.set store.c_store.c_activity (c:t:>int) f - let[@inline] make_removable store l premise = - make_l store ~removable:true l premise + let[@inline] make_removable store l = + make_l store ~removable:true l - let[@inline] make_removable_a store a premise = - make_a store ~removable:true a premise + let[@inline] make_removable_a store a = + make_a store ~removable:true a - let[@inline] make_permanent store l premise = - let c = make_l store ~removable:false l premise in + let[@inline] make_permanent store l = + let c = make_l store ~removable:false l in assert (not (removable store c)); (* permanent by default *) c @@ -428,32 +403,18 @@ module Make(Plugin : PLUGIN) let atoms_l store c : _ list = Array.to_list (atoms_a store c) let atoms_iter store c = fun k -> iter store c ~f:k - let short_name store c = - let p = premise store c in - Printf.sprintf "%s%d" (kind_of_premise p) (c:t:>int) + let short_name _store c = Printf.sprintf "cl[%d]" (c:t:>int) let pp store fmt c = - let p = premise store c in - Format.fprintf fmt "(cl[%s%d] : %a" (kind_of_premise p) (c:t:>int) + Format.fprintf fmt "(cl[%d] : %a" (c:t:>int) (Atom.pp_a store) (atoms_a store c) - let debug_premise out = function - | Hyp _ -> Format.fprintf out "hyp" - | Lemma _ -> Format.fprintf out "th_lemma" - | Local -> Format.fprintf out "local" - | History v as p -> - Format.fprintf out "(@[res"; - List.iter (fun c -> Format.fprintf out "@ %s%d," (kind_of_premise p) (c:t:>int)) v; - Format.fprintf out "@])" - | Empty_premise -> Format.fprintf out "none" - let debug store out c = let atoms = atoms_a store c in - let p = premise store c in Format.fprintf out - "(@[cl[%s%d]@ {@[%a@]}@ :premise %a@])" - (kind_of_premise p) (c:t:>int) - (Atom.debug_a store) atoms debug_premise p + "(@[cl[%d]@ {@[%a@]}@])" + (c:t:>int) + (Atom.debug_a store) atoms end (* allocate new variable *) @@ -557,7 +518,7 @@ module Make(Plugin : PLUGIN) th: theory; (* user defined theory *) - store_proof: bool; (* do we store proofs? *) + proof: Proof.t; (* the proof object *) (* Clauses are simplified for efficiency purposes. In the following vectors, the comments actually refer to the original non-simplified @@ -647,7 +608,7 @@ module Make(Plugin : PLUGIN) let _nop_on_conflict (_:atom array) = () (* Starting environment. *) - let create_ ~store ~store_proof (th:theory) : t = { + let create_ ~store ~proof (th:theory) : t = { store; th; unsat_at_0=None; next_decisions = []; @@ -671,7 +632,8 @@ module Make(Plugin : PLUGIN) var_incr = 1.; clause_incr = 1.; - store_proof; + + proof; n_conflicts = 0; n_decisions = 0; @@ -687,10 +649,10 @@ module Make(Plugin : PLUGIN) let create ?on_conflict ?on_decision ?on_new_atom ?on_learnt ?on_gc - ?(store_proof=true) ?(size=`Big) + ?(size=`Big) ~proof (th:theory) : t = let store = Store.create ~size () in - let self = create_ ~store ~store_proof th in + let self = create_ ~store ~proof th in self.on_new_atom <- on_new_atom; self.on_decision <- on_decision; self.on_conflict <- on_conflict; @@ -806,7 +768,7 @@ module Make(Plugin : PLUGIN) clause ) else ( let removable = Clause.removable store clause in - Clause.make_l store ~removable !res (History [clause]) + Clause.make_l store ~removable !res ) (* TODO: do it in place in a vec? *) @@ -948,7 +910,6 @@ module Make(Plugin : PLUGIN) Log.debugf 3 (fun k -> k "(@[sat.unsat-conflict@ %a@])" (pp_unsat_cause self) us); let us = match us with | US_false c -> - let c = if self.store_proof then Proof.prove_unsat self.store c else c in self.unsat_at_0 <- Some c; (match self.on_learnt with Some f -> f self (Clause.atoms_a self.store c) | None -> ()); US_false c @@ -979,9 +940,7 @@ module Make(Plugin : PLUGIN) and set it as the cause for the propagation of [a], that way we can rebuild the whole resolution tree when we want to prove [a]. *) let removable = Clause.removable self.store cl in - let c' = - Clause.make_l self.store ~removable l (History (cl :: history)) - in + let c' = Clause.make_l self.store ~removable l in Log.debugf 3 (fun k -> k "(@[sat.simplified-reason@ %a@ %a@])" (Clause.debug self.store) cl (Clause.debug self.store) c'); @@ -1208,10 +1167,6 @@ module Make(Plugin : PLUGIN) (* 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 - let proof = - if self.store_proof - then History (Array.to_list cr.cr_history) - else Empty_premise in begin match cr.cr_learnt with | [| |] -> assert false | [|fuip|] -> @@ -1221,14 +1176,14 @@ module Make(Plugin : PLUGIN) report_unsat self (US_false confl) ) else ( let uclause = - Clause.make_a store ~removable:true cr.cr_learnt proof in + Clause.make_a store ~removable:true cr.cr_learnt in (match self.on_learnt with Some f -> f self cr.cr_learnt | None -> ()); (* no need to attach [uclause], it is true at level 0 *) enqueue_bool self fuip ~level:0 (Bcp uclause) ) | _ -> let fuip = cr.cr_learnt.(0) in - let lclause = Clause.make_a store ~removable:true cr.cr_learnt proof 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 *) ); @@ -1287,9 +1242,8 @@ module Make(Plugin : PLUGIN) List.iteri (fun i a -> c_atoms.(i) <- a) atoms; c ) else ( - let proof = if self.store_proof then History (c::history) else Empty_premise in let removable = Clause.removable store c in - Clause.make_l store ~removable atoms proof + Clause.make_l store ~removable atoms ) in assert (Clause.removable store clause = Clause.removable store init); @@ -1420,10 +1374,11 @@ module Make(Plugin : PLUGIN) let[@inline] slice_get st i = Vec.get st.trail i - let acts_add_clause self ?(keep=false) (l:formula list) (lemma:lemma): unit = + let acts_add_clause self ?(keep=false) (l:formula list) (dp:dproof): 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 (Lemma lemma) in + let c = Clause.make_l self.store ~removable atoms in + if Proof.enabled self.proof then dp self.proof; Log.debugf 5 (fun k->k "(@[sat.th.add-clause@ %a@])" (Clause.debug self.store) c); Vec.push self.clauses_to_add c @@ -1436,10 +1391,11 @@ module Make(Plugin : PLUGIN) self.next_decisions <- a :: self.next_decisions ) - let acts_raise self (l:formula list) proof : 'a = + let acts_raise self (l:formula list) (pr:dproof) : '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 (Lemma proof) in + let c = Clause.make_l self.store ~removable:true atoms in + if Proof.enabled self.proof then pr self.proof; Log.debugf 5 (fun k->k "(@[@{sat.th.raise-conflict@}@ %a@])" (Clause.debug self.store) c); raise_notrace (Th_conflict c) @@ -1460,15 +1416,16 @@ module Make(Plugin : PLUGIN) let p = make_atom self f in if Atom.is_true store p then () else if Atom.is_false store p then ( - let lits, proof = mk_expl() in + let lits, dp = mk_expl() in let l = List.rev_map (fun f -> Atom.neg @@ make_atom self f) lits in check_consequence_lits_false_ self l; - let c = Clause.make_l store ~removable:true (p :: l) (Lemma proof) in + let c = Clause.make_l store ~removable:true (p :: l) in + if Proof.enabled self.proof then dp self.proof; raise_notrace (Th_conflict c) ) else ( insert_var_order self (Atom.var p); let c = lazy ( - let lits, proof = mk_expl () in + let lits, dp = mk_expl () in let l = List.rev_map (fun f -> Atom.neg @@ make_atom self f) lits in (* note: we can check that invariant here in the [lazy] block, as conflict analysis will run in an environment where @@ -1477,7 +1434,8 @@ module Make(Plugin : PLUGIN) (otherwise the propagated lit would have been backtracked and discarded already.) *) check_consequence_lits_false_ self l; - Clause.make_l store ~removable:true (p :: l) (Lemma proof) + if Proof.enabled self.proof then dp self.proof; + Clause.make_l store ~removable:true (p :: l) ) in let level = decision_level self in self.n_propagations <- 1 + self.n_propagations; @@ -1505,7 +1463,7 @@ module Make(Plugin : PLUGIN) let[@inline] current_slice st : _ Solver_intf.acts = let module M = struct type nonrec proof = proof - type nonrec lemma = lemma + type dproof = proof -> unit type nonrec formula = formula let iter_assumptions=acts_iter st ~full:false st.th_head let eval_lit= acts_eval_lit st @@ -1521,7 +1479,7 @@ module Make(Plugin : PLUGIN) let[@inline] full_slice st : _ Solver_intf.acts = let module M = struct type nonrec proof = proof - type nonrec lemma = lemma + type dproof = proof -> unit type nonrec formula = formula let iter_assumptions=acts_iter st ~full:true st.th_head let eval_lit= acts_eval_lit st @@ -1842,11 +1800,12 @@ module Make(Plugin : PLUGIN) done with E_sat -> () - let assume self cnf lemma : unit = + let assume self cnf dp : unit = List.iter (fun l -> let atoms = List.rev_map (make_atom self) l in - let c = Clause.make_l self.store ~removable:false atoms (Hyp lemma) in + let c = Clause.make_l self.store ~removable:false atoms in + if Proof.enabled self.proof then dp self.proof; Log.debugf 10 (fun k -> k "(@[sat.assume-clause@ @[%a@]@])" (Clause.debug self.store) c); Vec.push self.clauses_to_add c) @@ -1875,7 +1834,7 @@ module Make(Plugin : PLUGIN) (* Result type *) type res = | Sat of Formula.t Solver_intf.sat_state - | Unsat of (atom,clause,Proof.t) Solver_intf.unsat_state + | Unsat of (atom,clause) Solver_intf.unsat_state let pp_all self lvl status = Log.debugf lvl @@ -1911,45 +1870,32 @@ module Make(Plugin : PLUGIN) let c = lazy ( let core = List.rev core in (* increasing trail order *) assert (Atom.equal first @@ List.hd core); - let proof_of (a:atom) = match Atom.reason self.store a with - | Some Decision -> Clause.make_l self.store ~removable:true [a] Local - | Some (Bcp c | Bcp_lazy (lazy c)) -> c - | None -> assert false - in - let other_lits = List.filter (fun a -> not (Atom.equal a first)) core in - let hist = - Clause.make_l self.store ~removable:false [first] Local :: - proof_of first :: - List.map proof_of other_lits in - Clause.make_l self.store ~removable:false [] (History hist) + Clause.make_l self.store ~removable:false [] ) in fun () -> Lazy.force c in - let get_proof () : Proof.t = - let c = unsat_conflict () in - Proof.prove self.store c - in let module M = struct type nonrec atom = atom type clause = Clause.t type proof = Proof.t - let get_proof = get_proof let unsat_conflict = unsat_conflict let unsat_assumptions = unsat_assumptions end in (module M) - let add_clause_a self c lemma : unit = + let add_clause_a self c dp : unit = try - let c = Clause.make_a self.store ~removable:false c (Hyp lemma) in + let c = Clause.make_a self.store ~removable:false c in + if Proof.enabled self.proof then dp self.proof; add_clause_ self c with | E_unsat (US_false c) -> self.unsat_at_0 <- Some c - let add_clause self c lemma : unit = + let add_clause self c dp : unit = try - let c = Clause.make_l self.store ~removable:false c (Hyp lemma) in + let c = Clause.make_l self.store ~removable:false c in + if Proof.enabled self.proof then dp self.proof; add_clause_ self c with | E_unsat (US_false c) -> @@ -1985,14 +1931,16 @@ module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) = module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) = Make(struct - module Formula = Plugin.Formula - type t = unit - type proof = Plugin.proof - let push_level () = () - let pop_levels _ _ = () - let partial_check () _ = () - let final_check () _ = () - let has_theory = false -end) + type formula = Plugin.formula + type proof = Plugin.proof + module Formula = Plugin.Formula + module Proof = Plugin.Proof + type t = unit + let push_level () = () + let pop_levels _ _ = () + let partial_check () _ = () + let final_check () _ = () + let has_theory = false + end) [@@inline][@@specialise] diff --git a/src/sat/Solver.mli b/src/sat/Solver.mli index 1af4efd8..4c959519 100644 --- a/src/sat/Solver.mli +++ b/src/sat/Solver.mli @@ -3,13 +3,15 @@ module type S = Solver_intf.S (** Safe external interface of solvers. *) module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT) - : S with module Formula = Th.Formula - and type lemma = Th.lemma + : S with type formula = Th.formula + and module Formula = Th.Formula and type proof = Th.proof + and module Proof = Th.Proof and type theory = unit module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T) - : S with module Formula = Th.Formula - and type lemma = Th.lemma + : S with type formula = Th.formula + and module Formula = Th.Formula and type proof = Th.proof + and module Proof = Th.Proof and type theory = Th.t diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index cccd5f90..f7363669 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -39,22 +39,17 @@ type 'form sat_state = (module SAT_STATE with type formula = 'form) module type UNSAT_STATE = sig type atom type clause - type proof val unsat_conflict : unit -> clause (** Returns the unsat clause found at the toplevel *) - val get_proof : unit -> proof - (** returns a persistent proof of the empty clause from the Unsat result. *) - val unsat_assumptions: unit -> atom list (** Subset of assumptions responsible for "unsat" *) end -type ('atom, 'clause, 'proof) unsat_state = +type ('atom, 'clause) unsat_state = (module UNSAT_STATE with type atom = 'atom - and type clause = 'clause - and type proof = 'proof) + and type clause = 'clause) (** The type of values returned when the solver reaches an UNSAT state. *) type negated = @@ -64,8 +59,8 @@ type negated = See {!val:Expr_intf.S.norm} for more details. *) (** The type of reasons for propagations of a formula [f]. *) -type ('formula, 'lemma) reason = - | Consequence of (unit -> 'formula list * 'lemma) [@@unboxed] +type ('formula, 'proof) reason = + | Consequence of (unit -> 'formula list * 'proof) [@@unboxed] (** [Consequence (l, p)] means that the formulas in [l] imply the propagated formula [f]. The proof should be a proof of the clause "[l] implies [f]". @@ -90,7 +85,8 @@ type lbool = L_true | L_false | L_undefined module type ACTS = sig type formula - type lemma + type proof + type dproof = proof -> unit val iter_assumptions: (formula -> unit) -> unit (** Traverse the new assumptions on the boolean trail. *) @@ -102,19 +98,19 @@ module type ACTS = sig (** Map the given formula to a literal, which will be decided by the SAT solver. *) - val add_clause: ?keep:bool -> formula list -> lemma -> unit + val add_clause: ?keep:bool -> formula list -> dproof -> 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 partial model again. *) - val raise_conflict: formula list -> lemma -> 'b + val raise_conflict: formula 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 current trail. *) - val propagate: formula -> (formula, lemma) reason -> unit + val propagate: formula -> (formula, dproof) reason -> unit (** Propagate a formula, i.e. the theory can evaluate the formula to be true (see the definition of {!type:eval_res} *) @@ -124,9 +120,9 @@ module type ACTS = sig Useful for theory combination. This will be undone on backtracking. *) end -type ('formula, 'lemma) acts = +type ('formula, 'proof) acts = (module ACTS with type formula = 'formula - and type lemma = 'lemma) + and type proof = 'proof) (** The type for a slice of assertions to assume/propagate in the theory. *) exception No_proof @@ -157,61 +153,22 @@ module type FORMULA = sig but one returns [Negated] and the other [Same_sign]. *) end -(** Signature for proof emission, using DRUP. - - We do not store the resolution steps, just the stream of clauses deduced. - See {!Sidekick_drup} for checking these proofs. *) -module type PROOF = sig - type t - (** The stored proof (possibly nil, possibly on disk, possibly in memory) *) - - type atom - (** A boolean atom for the proof trace *) - - type lemma - (** A theory lemma *) - - module Atom : sig - type t = atom - val sign : t -> bool - val var_int : t -> int - val make : sign:bool -> int -> t - val pp : t Fmt.printer - end - - val enabled : t -> bool - (** Do we emit proofs at all? *) - - val emit_input_clause : t -> atom Iter.t -> unit - (** Emit an input clause. *) - - val emit_lemma : t -> atom Iter.t -> lemma -> unit - (** Emit a theory lemma *) - - val emit_redundant_clause : t -> atom Iter.t -> unit - (** Emit a clause deduced by the SAT solver, redundant wrt axioms. - The clause must be RUP wrt previous clauses. *) - - val del_clause : t -> atom Iter.t -> unit - (** Forget a clause. Only useful for performance considerations. *) -end +module type PROOF = Sidekick_core.SAT_PROOF (** Signature for theories to be given to the CDCL(T) solver *) module type PLUGIN_CDCL_T = sig type t (** The plugin state itself *) - module Formula : FORMULA + type formula + module Formula : FORMULA with type t = formula type proof (** Proof storage/recording *) - type lemma - (* Theory lemmas *) - module Proof : PROOF with type t = proof - and type lemma = lemma + and type lit = formula val push_level : t -> unit (** Create a new backtrack level *) @@ -219,12 +176,12 @@ module type PLUGIN_CDCL_T = sig val pop_levels : t -> int -> unit (** Pop [n] levels of the theory *) - val partial_check : t -> (Formula.t, lemma) acts -> unit + val partial_check : t -> (Formula.t, proof) acts -> unit (** Assume the formulas in the slice, possibly using the [slice] to push new formulas to be propagated or to raising a conflict or to add new lemmas. *) - val final_check : t -> (Formula.t, lemma) acts -> unit + val final_check : t -> (Formula.t, proof) 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; @@ -233,14 +190,11 @@ end (** Signature for pure SAT solvers *) module type PLUGIN_SAT = sig - module Formula : FORMULA + type formula + module Formula : FORMULA with type t = formula - type lemma = unit type proof - - module Proof : PROOF - with type t = proof - and type lemma = lemma + module Proof : PROOF with type t = proof and type lit = formula end (** The external interface implemented by safe solvers, such as the one @@ -250,9 +204,9 @@ module type S = sig These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT. *) - module Formula : FORMULA + type formula (** user formulas *) - type formula = Formula.t (** user formulas *) + module Formula : FORMULA with type t = formula type atom (** The type of atoms given by the module argument for formulas. @@ -263,12 +217,11 @@ module type S = sig type theory - type lemma - (** A theory lemma or an input axiom. *) - type proof (** A representation of a full proof *) + type dproof = proof -> unit + type solver (** The main solver type. *) @@ -317,8 +270,7 @@ module type S = sig end module Proof : PROOF - with type atom = atom - and type lemma = lemma + with type lit = formula and type t = proof (** A module to manipulate proofs. *) @@ -331,14 +283,13 @@ module type S = sig ?on_new_atom:(t -> atom -> unit) -> ?on_learnt:(t -> atom array -> unit) -> ?on_gc:(t -> atom array -> unit) -> - ?store_proof:bool -> ?size:[`Tiny|`Small|`Big] -> + proof:Proof.t -> theory -> t (** Create new solver @param theory the theory - @param store_proof if true, stores proof (default [true]). Otherwise - the functions that return proofs will fail with [No_proof] + @param the proof @param size the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses. *) @@ -353,7 +304,7 @@ module type S = sig (** Result type for the solver *) type res = | Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *) - | Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) + | Unsat of (atom,clause) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) exception UndecidedLit (** Exception raised by the evaluating functions when a literal @@ -361,14 +312,14 @@ module type S = sig (** {2 Base operations} *) - val assume : t -> formula list list -> lemma -> unit + val assume : t -> formula list list -> dproof -> unit (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *) - val add_clause : t -> atom list -> lemma -> unit + val add_clause : t -> atom list -> dproof -> unit (** Lower level addition of clauses *) - val add_clause_a : t -> atom array -> lemma -> unit + val add_clause_a : t -> atom array -> dproof -> unit (** Lower level addition of clauses *) val solve : diff --git a/src/sat/dune b/src/sat/dune index 8b762d67..69b53c12 100644 --- a/src/sat/dune +++ b/src/sat/dune @@ -2,7 +2,7 @@ (library (name sidekick_sat) (public_name sidekick.sat) - (libraries iter sidekick.util) + (libraries iter sidekick.util sidekick.core) (synopsis "Pure OCaml SAT solver implementation for sidekick") (flags :standard -warn-error -a+8 -open Sidekick_util) (ocamlopt_flags :standard -O3 -bin-annot