From 764695bb6568c40dd5dbd23e1f9d15a2d25c7422 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 14 Nov 2020 18:58:40 -0500 Subject: [PATCH] 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. *)