refactor: change theory API to be simpler and more imperative

src/core/Internal.ml

@@ -1440,10 +1440,7 @@ module Make(Plugin : PLUGIN)
 
   (* Get the correct vector to insert a clause in. *)
   let clause_vector st c =
-    match c.cpremise with
+    if Clause.learnt c then st.clauses_learnt else st.clauses_hyps
-    | Hyp | Lemma _ -> st.clauses_hyps
-    | History _ -> st.clauses_learnt
-    | Local -> assert false (* never added directly *)
 
   (* Add a new clause, simplifying, propagating, and backtracking if
      the clause is false in the current trail *)
@@ -1598,6 +1595,8 @@ module Make(Plugin : PLUGIN)
     ignore (th_eval st a);
     a
 
+  exception Th_conflict of Clause.t
+
   let slice_get st i =
     match Vec.get st.trail i with
     | Atom a ->
@@ -1606,12 +1605,18 @@ module Make(Plugin : PLUGIN)
       Solver_intf.Assign (term, v)
     | Lit _ -> assert false
 
-  let slice_push st (l:formula list) (lemma:lemma): unit =
+  let slice_push st ?(keep=false) (l:formula list) (lemma:lemma): unit =
     let atoms = List.rev_map (create_atom st) l in
     let c = Clause.make atoms (Lemma lemma) in
+    if not keep then Clause.set_learnt c true;
     Log.debugf info (fun k->k "Pushing clause %a" Clause.debug c);
     Stack.push c st.clauses_to_add
 
+  let slice_raise st (l:formula list) proof : 'a =
+    let atoms = List.rev_map (create_atom st) l in
+    let c = Clause.make atoms (Lemma proof) in
+    raise_notrace (Th_conflict c)
+
   let slice_propagate (st:t) f = function
     | Solver_intf.Eval l ->
       let a = mk_atom st f in
@@ -1633,23 +1638,44 @@ module Make(Plugin : PLUGIN)
         invalid_arg "Msat.Internal.slice_propagate"
       )
 
-  let current_slice st : (_,_,_) Solver_intf.slice = {
+  let[@specialise] slice_iter st ~full f : unit =
-    Solver_intf.start = st.th_head;
+    for i = (if full then 0 else st.th_head) to Vec.size st.trail-1 do
-    length = Vec.size st.trail - st.th_head;
+      let e = match Vec.get st.trail i with
-    get = slice_get st;
+        | Atom a ->
+          Solver_intf.Lit a.lit
+        | Lit {term; assigned = Some v; _} ->
+          Solver_intf.Assign (term, v)
+        | Lit _ -> assert false
+      in
+      f e
+    done
+
+  let[@inline] current_slice st : (_,_,_) Solver_intf.slice = {
+    Solver_intf.
+    iter_assumptions=slice_iter st ~full:false;
     push = slice_push st;
     propagate = slice_propagate st;
+    raise_conflict=slice_raise st;
   }
 
   (* full slice, for [if_sat] final check *)
-  let full_slice st : (_,_,_) Solver_intf.slice = {
+  let[@inline] full_slice st : (_,_,_) Solver_intf.slice = {
-    Solver_intf.start = 0;
+    Solver_intf.
-    length = Vec.size st.trail;
+    iter_assumptions=slice_iter st ~full:true;
-    get = slice_get st;
     push = slice_push st;
-    propagate = (fun _ -> assert false);
+    propagate = slice_propagate st;
+    raise_conflict=slice_raise st;
   }
 
+  (* Assert that the conflict is indeeed a conflict *)
+  let check_is_conflict_ (c:Clause.t) : unit =
+    if not @@ Array.for_all (Atom.is_false) c.atoms then (
+      let msg =
+        Format.asprintf "msat:core/internal: invalid conflict %a" Clause.debug c
+      in
+      raise (Invalid_argument msg);
+    )
+
   (* some boolean literals were decided/propagated within Msat. Now we
      need to inform the theory of those assumptions, so it can do its job.
      @return the conflict clause, if the theory detects unsatisfiability *)
@@ -1662,18 +1688,11 @@ module Make(Plugin : PLUGIN)
       let slice = current_slice st in
       st.th_head <- st.elt_head; (* catch up *)
       match Plugin.assume st.th slice with
-      | Solver_intf.Th_sat ->
+      | () ->
         propagate st
-      | Solver_intf.Th_unsat (l, p) ->
+      | exception Th_conflict c ->
-        (* conflict *)
+        check_is_conflict_ c;
-        let l = List.rev_map (create_atom st) l in
+        Array.iter (fun a -> insert_var_order st (Elt.of_var a.var)) c.atoms;
-        (* Assert that the conflcit is indeeed a conflict *)
-        if not @@ List.for_all (fun a -> a.neg.is_true) l then (
-          raise (Invalid_argument "msat:core/internal: invalid conflict");
-        );
-        List.iter (fun a -> insert_var_order st (Elt.of_var a.var)) l;
-        (* Create the clause and return it. *)
-        let c = Clause.make l (Lemma p) in
         Some c
     )
 
@@ -1892,14 +1911,18 @@ module Make(Plugin : PLUGIN)
           | E_sat ->
             assert (st.elt_head = Vec.size st.trail);
             begin match Plugin.if_sat st.th (full_slice st) with
-              | Solver_intf.Th_sat -> ()
+              | () ->
-              | Solver_intf.Th_unsat (l, p) ->
+                if st.elt_head = Vec.size st.trail &&
-                let atoms = List.rev_map (create_atom st) l in
+                   Stack.is_empty st.clauses_to_add then (
-                let c = Clause.make atoms (Lemma p) in
+                  raise_notrace E_sat
+                );
+                (* otherwise, keep on *)
+              | exception Th_conflict c ->
+                check_is_conflict_ c;
+                Array.iter (fun a -> insert_var_order st (Elt.of_var a.var)) c.atoms;
                 Log.debugf info (fun k -> k "Theory conflict clause: %a" Clause.debug c);
                 Stack.push c st.clauses_to_add
             end;
-            if Stack.is_empty st.clauses_to_add then raise_notrace E_sat
         end
       done
     with E_sat -> ()
@@ -2082,8 +2105,8 @@ module Make_pure_sat(F: Solver_intf.FORMULA) =
   type proof = Solver_intf.void
   type level = unit
   let current_level () = ()
-  let assume () _ = Solver_intf.Th_sat
+  let assume () _ = ()
-  let if_sat () _ = Solver_intf.Th_sat
+  let if_sat () _ = ()
   let backtrack () _ = ()
   let eval () _ = Solver_intf.Unknown
   let assign () t = t

src/core/Msat.ml

@@ -27,9 +27,21 @@ type 'clause export = 'clause Solver_intf.export = {
   hyps : 'clause Vec.t;
   history : 'clause Vec.t;
 }
-type ('formula, 'proof) th_res = ('formula, 'proof) Solver_intf.th_res =
+
-  | Th_sat
+type ('term, 'formula) assumption = ('term, 'formula) Solver_intf.assumption =
-  | Th_unsat of 'formula list * 'proof
+  | Lit of 'formula
+  | Assign of 'term * 'term (** The first term is assigned to the second *)
+
+type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.reason =
+  | Eval of 'term list
+  | Consequence of 'formula list * 'proof
+
+type ('term, 'formula, 'proof) slice = ('term, 'formula, 'proof) Solver_intf.slice = {
+  iter_assumptions: (('term,'formula) assumption -> unit) -> unit;
+  push : ?keep:bool -> 'formula list -> 'proof -> unit;
+  raise_conflict: 'b. 'formula list -> 'proof -> 'b;
+  propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit;
+}
 
 type negated = Solver_intf.negated = Negated | Same_sign
 

src/core/Solver_intf.ml

@@ -68,39 +68,40 @@ type 'term eval_res =
     - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number)
 *)
 
-type ('formula, 'proof) th_res =
-  | Th_sat
-  (** The current set of assumptions is satisfiable. *)
-  | Th_unsat of 'formula list * 'proof
-  (** The current set of assumptions is *NOT* satisfiable, and here is a
-      theory tautology (with its proof), for which every litteral is false
-      under the current assumptions. *)
-(** Type returned by the theory. Formulas in the unsat clause must come from the
-    current set of assumptions, i.e must have been encountered in a slice. *)
-
 type ('term, 'formula) assumption =
   | Lit of 'formula  (** The given formula is asserted true by the solver *)
   | Assign of 'term * 'term (** The first term is assigned to the second *)
 (** Asusmptions made by the core SAT solver. *)
 
 type ('term, 'formula, 'proof) reason =
-  | Eval of 'term list                      (** The formula can be evalutaed using the terms in the list *)
+  | Eval of 'term list
-  | Consequence of 'formula list * 'proof   (** [Consequence (l, p)] means that the formulas in [l] imply
+  (** The formula can be evalutaed using the terms in the list *)
-                                                the propagated formula [f]. The proof should be a proof of
+  | Consequence of 'formula list * 'proof
-                                                the clause "[l] implies [f]". *)
+  (** [Consequence (l, p)] means that the formulas in [l] imply the propagated
+      formula [f]. The proof should be a proof of the clause "[l] implies [f]".
+  *)
 (** The type of reasons for propagations of a formula [f]. *)
 
+(* TODO: find a way to use atoms instead of formulas here *)
 type ('term, 'formula, 'proof) slice = {
-  start : int;                                (** Start of the slice *)
+  iter_assumptions: (('term,'formula) assumption -> unit) -> unit;
-  length : int;                               (** Length of the slice *)
+  (** Traverse the new assumptions on the boolean trail. *)
-  get : int -> ('term, 'formula) assumption;  (** Accessor for the assertions in the slice.
+
-                                                  Should only be called on integers [i] s.t.
+  push : ?keep:bool -> 'formula list -> 'proof -> unit;
-                                                  [start <= i < start + length] *)
+  (** Add a clause to the solver.
-  push : 'formula list -> 'proof -> unit;     (** Add a clause to the solver. *)
+      @param keep if true, the clause will be kept by the solver.
-  propagate : 'formula ->
+        Otherwise the solver is allowed to GC the clause and propose this
-    ('term, 'formula, 'proof) reason -> unit; (** Propagate a formula, i.e. the theory can
+        partial model again. 
-                                                  evaluate the formula to be true (see the
+  *)
-                                                  definition of {!type:eval_res} *)
+
+  raise_conflict: 'b. 'formula list -> 'proof -> 'b;
+  (** Raise a conflict, yielding control back to the solver.
+      The list of atoms must be a valid theory lemma that is false in the
+      current trail. *)
+
+  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} *)
 }
 (** The type for a slice of assertions to assume/propagate in the theory. *)
 
@@ -174,19 +175,19 @@ module type PLUGIN_CDCL_T = sig
   (** Return the current level of the theory (either the empty/beginning state, or the
       last level returned by the [assume] function). *)
 
-  val assume : t -> (void, Formula.t, proof) slice -> (Formula.t, proof) th_res
+  val assume : t -> (void, Formula.t, proof) slice -> unit
-  (** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
+  (** Assume the formulas in the slice, possibly pushing new formulas to be
-      and returns the result of the new assumptions. *)
+      propagated or raising a conflict. *)
 
-  val if_sat : t -> (void, Formula.t, proof) slice -> (Formula.t, proof) th_res
+  val if_sat : t -> (void, Formula.t, proof) slice -> unit
-  (** Called at the end of the search in case a model has been found. If no new clause is
+  (** Called at the end of the search in case a model has been found.
-      pushed and the function returns [Sat], then proof search ends and 'sat' is returned,
+      If no new clause is pushed, then proof search ends and 'sat' is returned;
-      else search is resumed. *)
+      if lemmas are added, search is resumed;
+      if a conflict clause is added, search backtracks and then resumes. *)
 
   val backtrack : t -> level -> unit
   (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the
       same state as when it returned the value [l], *)
-
 end
 
 (** Signature for theories to be given to the Model Constructing Solver. *)
@@ -203,14 +204,15 @@ module type PLUGIN_MCSAT = sig
   (** Return the current level of the theory (either the empty/beginning state, or the
       last level returned by the [assume] function). *)
 
-  val assume : t -> (Term.t, Formula.t, proof) slice -> (Formula.t, proof) th_res
+  val assume : t -> (Term.t, Formula.t, proof) slice -> unit
-  (** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
+  (** Assume the formulas in the slice, possibly pushing new formulas to be
-      and returns the result of the new assumptions. *)
+      propagated or raising a conflict. *)
 
-  val if_sat : t -> (Term.t, Formula.t, proof) slice -> (Formula.t, proof) th_res
+  val if_sat : t -> (Term.t, Formula.t, proof) slice -> unit
-  (** Called at the end of the search in case a model has been found. If no new clause is
+  (** Called at the end of the search in case a model has been found.
-      pushed and the function returns [Sat], then proof search ends and 'sat' is returned,
+      If no new clause is pushed, then proof search ends and 'sat' is returned;
-      else search is resumed. *)
+      if lemmas are added, search is resumed;
+      if a conflict clause is added, search backtracks and then resumes. *)
 
   val backtrack : t -> level -> unit
   (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the