Added if_sat to Theory_intf

src/core/plugin_intf.ml

@@ -75,6 +75,10 @@ module type S = sig
   (** 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], *)
 
+  val if_sat : (term, formula, proof) slice -> unit
+  (** Called at the end of the search in case a model has been found. If no new clause is
+      pushed, then 'sat' is returned, else search is resumed. *)
+
   val assign : term -> term
   (** Returns an assignment value for the given term. *)
 
@@ -84,9 +88,5 @@ module type S = sig
   val eval : formula -> eval_res
   (** Returns the evaluation of the formula in the current assignment *)
 
-  val if_sat : (term, formula, proof) slice -> unit
-  (** Called at the end of the search in case a model has been found. If no new clause is
-      pushed, then 'sat' is returned, else search is resumed. *)
-
 end
 

src/core/theory_intf.ml

@@ -57,5 +57,9 @@ module type S = sig
   (** 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], *)
 
+  val if_sat : (formula, proof) slice -> unit
+  (** Called at the end of the search in case a model has been found. If no new clause is
+      pushed, then 'sat' is returned, else search is resumed. *)
+
 end
 

src/example/smt.ml

@@ -48,6 +48,8 @@ module Tsmt = struct
 
   let backtrack l = env := l
 
+  let if_sat _ = ()
+
 end
 
 module Make(Dummy:sig end) = struct

src/solver/solver.ml

@@ -24,6 +24,7 @@ module DummyTheory(F : Formula_intf.S) = struct
   let current_level () = ()
   let assume _ = Theory_intf.Sat
   let backtrack _ = ()
+  let if_sat _ = ()
 end
 
 module Plugin(E : Formula_intf.S)
@@ -43,27 +44,27 @@ module Plugin(E : Formula_intf.S)
     | Plugin_intf.Lit f -> f
     | _ -> assert false
 
-  let assume s =
+  let mk_slice s = {
-    let slice = {
       Theory_intf.start = s.Plugin_intf.start;
       length = s.Plugin_intf.length;
       get = assume_get s;
       push = s.Plugin_intf.push;
-    } in
+    }
-    Th.assume slice
+
+  let assume s = Th.assume (mk_slice s)
 
   let backtrack = Th.backtrack
 
+  let if_sat s = Th.if_sat (mk_slice s)
+
+
+  (* McSat specific functions *)
   let assign _ = assert false
 
   let iter_assignable _ _ = ()
 
   let eval _ = Plugin_intf.Unknown
 
-  let if_sat _ = ()
-
-  let proof_debug _ = assert false
-
 end