From 9024b0f0a90f30fdf23bfd19a16824a676638326 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 23 Jan 2019 08:36:07 -0600 Subject: [PATCH] refactor: change theory API to be simpler and more imperative --- src/core/Internal.ml | 87 ++++++++++++++++++++++++++--------------- src/core/Msat.ml | 18 +++++++-- src/core/Solver_intf.ml | 82 +++++++++++++++++++------------------- 3 files changed, 112 insertions(+), 75 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index b02b1af3..673e47a3 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -1440,10 +1440,7 @@ module Make(Plugin : PLUGIN) (* Get the correct vector to insert a clause in. *) let clause_vector st c = - match c.cpremise with - | Hyp | Lemma _ -> st.clauses_hyps - | History _ -> st.clauses_learnt - | Local -> assert false (* never added directly *) + if Clause.learnt c then st.clauses_learnt else st.clauses_hyps (* Add a new clause, simplifying, propagating, and backtracking if the clause is false in the current trail *) @@ -1598,6 +1595,8 @@ module Make(Plugin : PLUGIN) ignore (th_eval st a); a + exception Th_conflict of Clause.t + let slice_get st i = match Vec.get st.trail i with | Atom a -> @@ -1606,12 +1605,18 @@ module Make(Plugin : PLUGIN) Solver_intf.Assign (term, v) | Lit _ -> assert false - let slice_push st (l:formula list) (lemma:lemma): unit = + let slice_push st ?(keep=false) (l:formula list) (lemma:lemma): unit = let atoms = List.rev_map (create_atom st) l in let c = Clause.make atoms (Lemma lemma) in + if not keep then Clause.set_learnt c true; Log.debugf info (fun k->k "Pushing clause %a" Clause.debug c); Stack.push c st.clauses_to_add + let slice_raise st (l:formula list) proof : 'a = + let atoms = List.rev_map (create_atom st) l in + let c = Clause.make atoms (Lemma proof) in + raise_notrace (Th_conflict c) + let slice_propagate (st:t) f = function | Solver_intf.Eval l -> let a = mk_atom st f in @@ -1633,23 +1638,44 @@ module Make(Plugin : PLUGIN) invalid_arg "Msat.Internal.slice_propagate" ) - let current_slice st : (_,_,_) Solver_intf.slice = { - Solver_intf.start = st.th_head; - length = Vec.size st.trail - st.th_head; - get = slice_get st; + let[@specialise] slice_iter st ~full f : unit = + for i = (if full then 0 else st.th_head) to Vec.size st.trail-1 do + let e = match Vec.get st.trail i with + | Atom a -> + Solver_intf.Lit a.lit + | Lit {term; assigned = Some v; _} -> + Solver_intf.Assign (term, v) + | Lit _ -> assert false + in + f e + done + + let[@inline] current_slice st : (_,_,_) Solver_intf.slice = { + Solver_intf. + iter_assumptions=slice_iter st ~full:false; push = slice_push st; propagate = slice_propagate st; + raise_conflict=slice_raise st; } (* full slice, for [if_sat] final check *) - let full_slice st : (_,_,_) Solver_intf.slice = { - Solver_intf.start = 0; - length = Vec.size st.trail; - get = slice_get st; + let[@inline] full_slice st : (_,_,_) Solver_intf.slice = { + Solver_intf. + iter_assumptions=slice_iter st ~full:true; push = slice_push st; - propagate = (fun _ -> assert false); + propagate = slice_propagate st; + raise_conflict=slice_raise st; } + (* Assert that the conflict is indeeed a conflict *) + let check_is_conflict_ (c:Clause.t) : unit = + if not @@ Array.for_all (Atom.is_false) c.atoms then ( + let msg = + Format.asprintf "msat:core/internal: invalid conflict %a" Clause.debug c + in + raise (Invalid_argument msg); + ) + (* some boolean literals were decided/propagated within Msat. Now we need to inform the theory of those assumptions, so it can do its job. @return the conflict clause, if the theory detects unsatisfiability *) @@ -1662,18 +1688,11 @@ module Make(Plugin : PLUGIN) let slice = current_slice st in st.th_head <- st.elt_head; (* catch up *) match Plugin.assume st.th slice with - | Solver_intf.Th_sat -> + | () -> propagate st - | Solver_intf.Th_unsat (l, p) -> - (* conflict *) - let l = List.rev_map (create_atom st) l in - (* Assert that the conflcit is indeeed a conflict *) - if not @@ List.for_all (fun a -> a.neg.is_true) l then ( - raise (Invalid_argument "msat:core/internal: invalid conflict"); - ); - List.iter (fun a -> insert_var_order st (Elt.of_var a.var)) l; - (* Create the clause and return it. *) - let c = Clause.make l (Lemma p) in + | exception Th_conflict c -> + check_is_conflict_ c; + Array.iter (fun a -> insert_var_order st (Elt.of_var a.var)) c.atoms; Some c ) @@ -1892,14 +1911,18 @@ module Make(Plugin : PLUGIN) | E_sat -> assert (st.elt_head = Vec.size st.trail); begin match Plugin.if_sat st.th (full_slice st) with - | Solver_intf.Th_sat -> () - | Solver_intf.Th_unsat (l, p) -> - let atoms = List.rev_map (create_atom st) l in - let c = Clause.make atoms (Lemma p) in + | () -> + if st.elt_head = Vec.size st.trail && + Stack.is_empty st.clauses_to_add then ( + raise_notrace E_sat + ); + (* otherwise, keep on *) + | exception Th_conflict c -> + check_is_conflict_ c; + Array.iter (fun a -> insert_var_order st (Elt.of_var a.var)) c.atoms; Log.debugf info (fun k -> k "Theory conflict clause: %a" Clause.debug c); Stack.push c st.clauses_to_add end; - if Stack.is_empty st.clauses_to_add then raise_notrace E_sat end done with E_sat -> () @@ -2082,8 +2105,8 @@ module Make_pure_sat(F: Solver_intf.FORMULA) = type proof = Solver_intf.void type level = unit let current_level () = () - let assume () _ = Solver_intf.Th_sat - let if_sat () _ = Solver_intf.Th_sat + let assume () _ = () + let if_sat () _ = () let backtrack () _ = () let eval () _ = Solver_intf.Unknown let assign () t = t diff --git a/src/core/Msat.ml b/src/core/Msat.ml index daee1b7c..1dbd99a3 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -27,9 +27,21 @@ type 'clause export = 'clause Solver_intf.export = { hyps : 'clause Vec.t; history : 'clause Vec.t; } -type ('formula, 'proof) th_res = ('formula, 'proof) Solver_intf.th_res = - | Th_sat - | Th_unsat of 'formula list * 'proof + +type ('term, 'formula) assumption = ('term, 'formula) Solver_intf.assumption = + | Lit of 'formula + | Assign of 'term * 'term (** The first term is assigned to the second *) + +type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.reason = + | Eval of 'term list + | Consequence of 'formula list * 'proof + +type ('term, 'formula, 'proof) slice = ('term, 'formula, 'proof) Solver_intf.slice = { + iter_assumptions: (('term,'formula) assumption -> unit) -> unit; + push : ?keep:bool -> 'formula list -> 'proof -> unit; + raise_conflict: 'b. 'formula list -> 'proof -> 'b; + propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; +} type negated = Solver_intf.negated = Negated | Same_sign diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index 354e9f6c..5f209785 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -68,39 +68,40 @@ type 'term eval_res = - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number) *) -type ('formula, 'proof) th_res = - | Th_sat - (** The current set of assumptions is satisfiable. *) - | Th_unsat of 'formula list * 'proof - (** The current set of assumptions is *NOT* satisfiable, and here is a - theory tautology (with its proof), for which every litteral is false - under the current assumptions. *) -(** Type returned by the theory. Formulas in the unsat clause must come from the - current set of assumptions, i.e must have been encountered in a slice. *) - type ('term, 'formula) assumption = - | Lit of 'formula (** The given formula is asserted true by the solver *) + | Lit of 'formula (** The given formula is asserted true by the solver *) | Assign of 'term * 'term (** The first term is assigned to the second *) (** Asusmptions made by the core SAT solver. *) type ('term, 'formula, 'proof) reason = - | Eval of 'term list (** The formula can be evalutaed using the terms in the list *) - | Consequence of 'formula list * 'proof (** [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]". *) + | Eval of 'term list + (** The formula can be evalutaed using the terms in the list *) + | Consequence of 'formula list * 'proof + (** [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]". + *) (** The type of reasons for propagations of a formula [f]. *) +(* TODO: find a way to use atoms instead of formulas here *) type ('term, 'formula, 'proof) slice = { - start : int; (** Start of the slice *) - length : int; (** Length of the slice *) - get : int -> ('term, 'formula) assumption; (** Accessor for the assertions in the slice. - Should only be called on integers [i] s.t. - [start <= i < start + length] *) - push : 'formula list -> 'proof -> unit; (** Add a clause to the solver. *) - propagate : 'formula -> - ('term, 'formula, 'proof) reason -> unit; (** Propagate a formula, i.e. the theory can - evaluate the formula to be true (see the - definition of {!type:eval_res} *) + iter_assumptions: (('term,'formula) assumption -> unit) -> unit; + (** Traverse the new assumptions on the boolean trail. *) + + push : ?keep:bool -> 'formula list -> 'proof -> 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. + *) + + raise_conflict: 'b. 'formula list -> 'proof -> '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. *) + + propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; + (** Propagate a formula, i.e. the theory can evaluate the formula to be true + (see the definition of {!type:eval_res} *) } (** The type for a slice of assertions to assume/propagate in the theory. *) @@ -174,19 +175,19 @@ module type PLUGIN_CDCL_T = sig (** Return the current level of the theory (either the empty/beginning state, or the last level returned by the [assume] function). *) - val assume : t -> (void, Formula.t, proof) slice -> (Formula.t, proof) th_res - (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, - and returns the result of the new assumptions. *) + val assume : t -> (void, Formula.t, proof) slice -> unit + (** Assume the formulas in the slice, possibly pushing new formulas to be + propagated or raising a conflict. *) - val if_sat : t -> (void, Formula.t, proof) slice -> (Formula.t, proof) th_res - (** Called at the end of the search in case a model has been found. If no new clause is - pushed and the function returns [Sat], then proof search ends and 'sat' is returned, - else search is resumed. *) + val if_sat : t -> (void, Formula.t, proof) slice -> 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. *) val backtrack : t -> level -> unit (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the same state as when it returned the value [l], *) - end (** Signature for theories to be given to the Model Constructing Solver. *) @@ -203,14 +204,15 @@ module type PLUGIN_MCSAT = sig (** Return the current level of the theory (either the empty/beginning state, or the last level returned by the [assume] function). *) - val assume : t -> (Term.t, Formula.t, proof) slice -> (Formula.t, proof) th_res - (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, - and returns the result of the new assumptions. *) + val assume : t -> (Term.t, Formula.t, proof) slice -> unit + (** Assume the formulas in the slice, possibly pushing new formulas to be + propagated or raising a conflict. *) - val if_sat : t -> (Term.t, Formula.t, proof) slice -> (Formula.t, proof) th_res - (** Called at the end of the search in case a model has been found. If no new clause is - pushed and the function returns [Sat], then proof search ends and 'sat' is returned, - else search is resumed. *) + val if_sat : t -> (Term.t, Formula.t, proof) slice -> 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. *) val backtrack : t -> level -> unit (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the