From 79b15858047eb1c8cc9b1d69b51034a0e616d494 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 29 Oct 2019 14:21:25 -0500 Subject: [PATCH 1/5] feat: allow the theory to ask for some literals to be decided on it's part of the actions provided to the theory. close #19 --- src/core/Internal.ml | 30 ++++++++++++++++++++---------- src/core/Msat.ml | 2 +- src/core/Solver_intf.ml | 5 +++++ 3 files changed, 26 insertions(+), 11 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index bda30191..6f71d5e3 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -787,9 +787,11 @@ module Make(Plugin : PLUGIN) mutable unsat_at_0: clause option; (* conflict at level 0, if any *) - mutable next_decision : atom option; + mutable next_decisions : atom list; (* When the last conflict was a semantic one (mcsat), - this stores the next decision to make *) + this stores the next decision to make; + if some theory wants atoms to be decided on (for theory combination), + store them here. *) trail : trail_elt Vec.t; (* decision stack + propagated elements (atoms or assignments). *) @@ -841,7 +843,7 @@ module Make(Plugin : PLUGIN) let create_ ~st ~store_proof (th:theory) : t = { st; th; unsat_at_0=None; - next_decision = None; + next_decisions = []; clauses_hyps = Vec.create(); clauses_learnt = Vec.create(); @@ -1175,6 +1177,7 @@ module Make(Plugin : PLUGIN) Vec.shrink st.trail !head; Vec.shrink st.elt_levels lvl; Plugin.pop_levels st.th n; + st.next_decisions <- []; ); () @@ -1489,7 +1492,7 @@ module Make(Plugin : PLUGIN) enqueue_bool st fuip ~level:cr.cr_backtrack_lvl (Bcp lclause) ) else ( assert Plugin.mcsat; - st.next_decision <- Some fuip.neg + st.next_decisions <- [fuip.neg]; ) end; var_decay_activity st; @@ -1502,7 +1505,7 @@ module Make(Plugin : PLUGIN) *) let add_boolean_conflict st (confl:clause): unit = Log.debugf info (fun k -> k "(@[sat.add-bool-conflict@ %a@])" Clause.debug confl); - st.next_decision <- None; + st.next_decisions <- []; assert (decision_level st >= 0); if decision_level st = 0 || Array.for_all (fun a -> a.var.v_level <= 0) confl.atoms then ( @@ -1695,6 +1698,11 @@ module Make(Plugin : PLUGIN) Log.debugf info (fun k->k "(@[sat.th.add-clause@ %a@])" Clause.debug c); Vec.push st.clauses_to_add c + let acts_add_decision_lit (st:t) (f:formula) : unit = + let a = create_atom st f in + Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); + st.next_decisions <- a :: st.next_decisions + let acts_raise st (l:formula list) proof : 'a = let atoms = List.rev_map (create_atom st) l in (* conflicts can be removed *) @@ -1776,6 +1784,7 @@ module Make(Plugin : PLUGIN) acts_add_clause = acts_add_clause st; acts_propagate = acts_propagate st; acts_raise_conflict=acts_raise st; + acts_add_decision_lit=acts_add_decision_lit st; } (* full slice, for [if_sat] final check *) @@ -1788,6 +1797,7 @@ module Make(Plugin : PLUGIN) acts_add_clause = acts_add_clause st; acts_propagate = acts_propagate st; acts_raise_conflict=acts_raise st; + acts_add_decision_lit=acts_add_decision_lit st; } (* Assert that the conflict is indeeed a conflict *) @@ -1914,12 +1924,12 @@ module Make(Plugin : PLUGIN) ) and pick_branch_lit st = - match st.next_decision with - | Some atom -> + match st.next_decisions with + | atom :: tl -> assert Plugin.mcsat; - st.next_decision <- None; + st.next_decisions <- tl; pick_branch_aux st atom - | None when decision_level st < Vec.size st.assumptions -> + | [] when decision_level st < Vec.size st.assumptions -> (* use an assumption *) let a = Vec.get st.assumptions (decision_level st) in if Atom.is_true a then ( @@ -1932,7 +1942,7 @@ module Make(Plugin : PLUGIN) ) else ( pick_branch_aux st a ) - | None -> + | [] -> begin match H.remove_min st.order with | E_lit l -> if Lit.level l >= 0 then ( diff --git a/src/core/Msat.ml b/src/core/Msat.ml index 6de87bec..07ea45c3 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -1,4 +1,3 @@ - (** Main API *) @@ -49,6 +48,7 @@ type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof) acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit; acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b; acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; + acts_add_decision_lit: 'formula -> unit; } type negated = Solver_intf.negated = Negated | Same_sign diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index 351850c7..cbf909c0 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -131,6 +131,11 @@ type ('term, 'formula, 'value, 'proof) acts = { acts_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} *) + + acts_add_decision_lit: 'formula -> unit; + (** Ask the SAT solver to decide on the given formula before it can + answer [SAT]. This will be removed on backtrack. + Useful for theory combination. *) } (** The type for a slice of assertions to assume/propagate in the theory. *) From 2286a72437de8f59426bb802c0da1194a1212cfd Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 29 Oct 2019 14:34:13 -0500 Subject: [PATCH 2/5] fix: in final-check, resume if there are new decisions to do --- src/core/Internal.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 6f71d5e3..749626d2 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -2041,7 +2041,9 @@ module Make(Plugin : PLUGIN) begin match Plugin.final_check st.th (full_slice st) with | () -> if st.elt_head = Vec.size st.trail && - Vec.is_empty st.clauses_to_add then ( + Vec.is_empty st.clauses_to_add && + st.next_decisions = [] + then ( raise_notrace E_sat ); (* otherwise, keep on *) From 919c1e60117fc21acdb66b869a72e44c54c1aaf3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 29 Oct 2019 14:35:26 -0500 Subject: [PATCH 3/5] fix: only push atoms that don't have a value into `next_decisions` --- src/core/Internal.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 749626d2..36d9c24d 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -246,6 +246,7 @@ module Make(Plugin : PLUGIN) let[@inline] id a = a.aid let[@inline] is_true a = a.is_true let[@inline] is_false a = a.neg.is_true + let has_value a = is_true a || is_false a let[@inline] seen a = if sign a @@ -1700,8 +1701,10 @@ module Make(Plugin : PLUGIN) let acts_add_decision_lit (st:t) (f:formula) : unit = let a = create_atom st f in - Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); - st.next_decisions <- a :: st.next_decisions + if not (Atom.has_value a) then ( + Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); + st.next_decisions <- a :: st.next_decisions + ) let acts_raise st (l:formula list) proof : 'a = let atoms = List.rev_map (create_atom st) l in From 4097ed9dc2fd7236deed35ddf96026b54ceefad4 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 07:47:53 -0600 Subject: [PATCH 4/5] refactor: account for @gbury's review --- src/core/Internal.ml | 2 +- src/core/Solver_intf.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 36d9c24d..82c1b036 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -1493,6 +1493,7 @@ module Make(Plugin : PLUGIN) enqueue_bool st fuip ~level:cr.cr_backtrack_lvl (Bcp lclause) ) else ( assert Plugin.mcsat; + assert (st.next_decisions = []); st.next_decisions <- [fuip.neg]; ) end; @@ -1929,7 +1930,6 @@ module Make(Plugin : PLUGIN) and pick_branch_lit st = match st.next_decisions with | atom :: tl -> - assert Plugin.mcsat; st.next_decisions <- tl; pick_branch_aux st atom | [] when decision_level st < Vec.size st.assumptions -> diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index cbf909c0..5f1b7d44 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -134,7 +134,7 @@ type ('term, 'formula, 'value, 'proof) acts = { acts_add_decision_lit: 'formula -> unit; (** Ask the SAT solver to decide on the given formula before it can - answer [SAT]. This will be removed on backtrack. + answer [SAT]. The order of decisions is still unspecified. Useful for theory combination. *) } (** The type for a slice of assertions to assume/propagate in the theory. *) From 764695bb6568c40dd5dbd23e1f9d15a2d25c7422 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 14 Nov 2020 18:58:40 -0500 Subject: [PATCH 5/5] feat: pass a sign along with the formula in `acts_add_decision_lit` --- src/core/Internal.ml | 3 ++- src/core/Msat.ml | 2 +- src/core/Solver_intf.ml | 10 +++++----- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 82c1b036..4076ae6f 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -1700,8 +1700,9 @@ module Make(Plugin : PLUGIN) Log.debugf info (fun k->k "(@[sat.th.add-clause@ %a@])" Clause.debug c); Vec.push st.clauses_to_add c - let acts_add_decision_lit (st:t) (f:formula) : unit = + let acts_add_decision_lit (st:t) (f:formula) (sign:bool) : unit = let a = create_atom st f in + let a = if sign then a else Atom.neg a in if not (Atom.has_value a) then ( Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); st.next_decisions <- a :: st.next_decisions diff --git a/src/core/Msat.ml b/src/core/Msat.ml index 07ea45c3..fb049615 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -48,7 +48,7 @@ type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof) acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit; acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b; acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; - acts_add_decision_lit: 'formula -> unit; + acts_add_decision_lit: 'formula -> bool -> unit; } type negated = Solver_intf.negated = Negated | Same_sign diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index 5f1b7d44..e144df1a 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -120,7 +120,7 @@ type ('term, 'formula, 'value, 'proof) acts = { (** 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. + partial model again. *) acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b; @@ -132,10 +132,10 @@ type ('term, 'formula, 'value, 'proof) acts = { (** Propagate a formula, i.e. the theory can evaluate the formula to be true (see the definition of {!type:eval_res} *) - acts_add_decision_lit: 'formula -> unit; - (** Ask the SAT solver to decide on the given formula before it can - answer [SAT]. The order of decisions is still unspecified. - Useful for theory combination. *) + acts_add_decision_lit: 'formula -> bool -> unit; + (** Ask the SAT solver to decide on the given formula 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. *) } (** The type for a slice of assertions to assume/propagate in the theory. *)