feat: pass a sign along with the formula in acts_add_decision_lit

Gbury · Nov 14, 2020 · 764695b · 764695b
1 parent 4097ed9
commit 764695b
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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. *)