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

@@ -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
+    match st.next_decisions with
-    | Some atom ->
+    | 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 (

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

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. *)