Better interface for Msat.Internal

src/core/external.ml

@@ -48,12 +48,11 @@ module Make
   type clause = St.clause
   type proof = Proof.proof
 
+  (* Result type *)
   type res =
     | Sat of (St.term,St.formula) sat_state
     | Unsat of (St.clause,Proof.proof) unsat_state
 
-  let assume ?tag l = S.assume ?tag l
-
   let mk_sat () : (_,_) sat_state =
     { model=S.model; eval=S.eval; eval_level=S.eval_level }
 
@@ -68,9 +67,18 @@ module Make
     in
     { unsat_conflict; get_proof; }
 
-  let solve ?assumptions () =
+  (* Wrappers around internal functions*)
+  let assume ?tag l =
     try
-      S.solve ?assumptions ();
+      S.assume ?tag l
+    with S.Unsat -> ()
+
+  let solve ?(assumptions=[]) () =
+    try
+      S.pop ();
+      S.push ();
+      S.local assumptions;
+      S.solve ();
       Sat (mk_sat())
     with S.Unsat ->
       Unsat (mk_unsat())

src/core/internal.ml

@@ -1064,52 +1064,13 @@ module Make
          | Atom _ -> acc)
       [] env.elt_queue
 
-  (* push a series of assumptions to the stack *)
-  let push_assumptions =
-    List.iter
-      (fun lit ->
-         let a = atom lit in
-         Log.debugf 10 "push assumption %a" (fun k->k pp_atom a);
-         if a.is_true then ()
-         else if a.neg.is_true then (
-           (* conflict between assumptions: UNSAT *)
-           let c = make_clause (fresh_hname ()) [a] Hyp in
-           report_unsat c;
-         ) else (
-           (* make a decision, propagate *)
-           new_decision_level();
-           let level = decision_level() in
-           assert (env.base_level = level-1);
-           env.base_level <- level;
-           let c = make_clause (fresh_hname ()) [a] Hyp in
-           enqueue_bool a ~level (Bcp c);
-           match propagate () with
-           | Some confl -> (* Conflict *)
-             report_unsat confl;
-           | None -> ()
-         ))
-
-  (* clear assumptions *)
-  let pop_assumptions (): unit =
-    env.base_level <- 0; (* before the [cancel_until]! *)
-    cancel_until 0;
-    ()
-
   (* fixpoint of propagation and decisions until a model is found, or a
      conflict is reached *)
-  let solve ?(assumptions=[]) (): unit =
+  let solve (): unit =
     Log.debug 5 "solve";
-    if env.base_level > 0 then (
-      pop_assumptions();
-      env.unsat_conflict <- None;
-    );
     if is_unsat () then raise Unsat;
     let n_of_conflicts = ref (to_float env.restart_first) in
     let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in
-    (* return to level 0 before pushing assumptions *)
-    cancel_until 0;
-    push_assumptions assumptions;
-    assert (env.base_level <= List.length assumptions);
     try
       while true do
         begin try
@@ -1132,10 +1093,6 @@ module Make
     with Sat -> ()
 
   let assume ?tag cnf =
-    if env.base_level > 0 then (
-      pop_assumptions ();
-      env.unsat_conflict <- None;
-    );
     List.iter
       (fun l ->
          let atoms = List.rev_map atom l in
@@ -1143,6 +1100,52 @@ module Make
          Stack.push c env.clauses_to_add)
       cnf
 
+  (* create a factice decision level for local assumptions *)
+  let push (): unit =
+    cancel_until env.base_level;
+    begin match propagate () with
+      | Some confl -> report_unsat confl
+      | None ->
+        new_decision_level ();
+        env.base_level <- env.base_level + 1;
+        assert (decision_level () = env.base_level)
+    end
+
+  (* pop the last factice decision level *)
+  let pop (): unit =
+    if env.base_level = 0 then ()
+    else begin
+      assert (env.base_level > 0);
+      env.unsat_conflict <- None;
+      env.base_level <- env.base_level - 1; (* before the [cancel_until]! *)
+      cancel_until env.base_level
+    end
+
+  (* Add local hyps to the current decision level *)
+  let local l =
+    let aux lit =
+      let a = atom lit in
+      Log.debugf 10 "local assumption: @[%a@]" (fun k->k pp_atom a);
+      assert (decision_level () = env.base_level);
+      if a.is_true then ()
+      else if a.neg.is_true then begin
+        (* conflict between assumptions: UNSAT *)
+        let c = make_clause (fresh_hname ()) [a] Hyp in
+        report_unsat c;
+      end else begin
+        (* make a decision, propagate *)
+        let level = decision_level() in
+        let c = make_clause (fresh_hname ()) [a] Hyp in
+        enqueue_bool a ~level (Bcp c);
+      end
+    in
+    assert (env.base_level > 0);
+    match env.unsat_conflict with
+    | None ->
+      cancel_until env.base_level;
+      List.iter aux l
+    | Some _ -> ()
+
   let hyps () = env.clauses_hyps
 
   let history () = env.clauses_learnt

src/core/internal.mli

@@ -18,14 +18,9 @@ module Make
 
   module Proof : Res.S with module St = St
 
-  val solve :
-    ?assumptions:St.formula list ->
-    unit ->
-    unit
+  val solve : unit -> unit
   (** Try and solves the current set of assumptions.
       @return () if the current set of clauses is satisfiable
-      @param assumptions list of additional local assumptions to make,
-        removed after the callback returns a value
       @raise Unsat if a toplevel conflict is found *)
 
   val assume : ?tag:int -> St.formula list list -> unit
@@ -33,6 +28,18 @@ module Make
       Modifies the sat solver state in place.
       @raise Unsat if a conflict is detect when adding the clauses *)
 
+  val push : unit -> unit
+  (** Create a decision level for local assumptions.
+      @raise Unsat if a conflict is detected in the current state. *)
+
+  val pop : unit -> unit
+  (** Pop a decision level for local assumptions. *)
+
+  val local : St.formula list -> unit
+    (** Add local assumptions
+      @param assumptions list of additional local assumptions to make,
+        removed after the callback returns a value *)
+
   val eval : St.formula -> bool
   (** Returns the valuation of a formula in the current state
       of the sat solver.