From 8f1c24c1a6ff3a5b73f82911f3caddc588e8ba26 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 26 Jan 2019 11:23:45 -0600
Subject: [PATCH] refactor: change API to `{final,partial}_check`

---
 src/core/Internal.ml       |  8 ++++----
 src/core/Solver_intf.ml    | 22 ++++++++++++----------
 src/sudoku/sudoku_solve.ml |  8 ++++----
 3 files changed, 20 insertions(+), 18 deletions(-)

diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 2eb2695f..74c89bb7 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -1690,7 +1690,7 @@ module Make(Plugin : PLUGIN)
     ) else (
       let slice = current_slice st in
       st.th_head <- st.elt_head; (* catch up *)
-      match Plugin.assume st.th slice with
+      match Plugin.partial_check st.th slice with
       | () ->
         flush_clauses st;
         propagate st
@@ -1914,7 +1914,7 @@ module Make(Plugin : PLUGIN)
             n_of_learnts   := !n_of_learnts *. learntsize_inc
           | E_sat ->
             assert (st.elt_head = Vec.size st.trail);
-            begin match Plugin.if_sat st.th (full_slice st) with
+            begin match Plugin.final_check st.th (full_slice st) with
               | () ->
                 if st.elt_head = Vec.size st.trail &&
                    Vec.is_empty st.clauses_to_add then (
@@ -2113,8 +2113,8 @@ module Make_pure_sat(F: Solver_intf.FORMULA) =
   type proof = Solver_intf.void
   let push_level () = ()
   let pop_levels _ _ = ()
-  let assume () _ = ()
-  let if_sat () _ = ()
+  let partial_check () _ = ()
+  let final_check () _ = ()
   let eval () _ = Solver_intf.Unknown
   let assign () t = t
   let mcsat = false
diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml
index f4059814..fdb7675a 100644
--- a/src/core/Solver_intf.ml
+++ b/src/core/Solver_intf.ml
@@ -174,13 +174,14 @@ module type PLUGIN_CDCL_T = sig
   val pop_levels : t -> int -> unit
   (** Pop [n] levels of the theory *)
 
-  val assume : t -> (void, Formula.t, proof) slice -> unit
-  (** Assume the formulas in the slice, possibly pushing new formulas to be
-      propagated or raising a conflict. *)
+  val partial_check : t -> (void, Formula.t, proof) slice -> unit
+  (** Assume the formulas in the slice, possibly using the [slice]
+      to push new formulas to be propagated or to raising a conflict or to add
+      new lemmas. *)
 
-  val if_sat : t -> (void, Formula.t, proof) slice -> unit
+  val final_check : 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 pushed, then proof search ends and 'sat' is returned;
+      If no new clause is pushed, then proof search ends and "sat" is returned;
       if lemmas are added, search is resumed;
       if a conflict clause is added, search backtracks and then resumes. *)
 end
@@ -199,13 +200,14 @@ module type PLUGIN_MCSAT = sig
   val pop_levels : t -> int -> unit
   (** Pop [n] levels of the theory *)
 
-  val assume : t -> (Term.t, Formula.t, proof) slice -> unit
-  (** Assume the formulas in the slice, possibly pushing new formulas to be
-      propagated or raising a conflict. *)
+  val partial_check : t -> (Term.t, Formula.t, proof) slice -> unit
+  (** Assume the formulas in the slice, possibly using the [slice]
+      to push new formulas to be propagated or to raising a conflict or to add
+      new lemmas. *)
 
-  val if_sat : t -> (Term.t, Formula.t, proof) slice -> unit
+  val final_check : 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 pushed, then proof search ends and 'sat' is returned;
+      If no new clause is pushed, then proof search ends and "sat" is returned;
       if lemmas are added, search is resumed;
       if a conflict clause is added, search backtracks and then resumes. *)
 
diff --git a/src/sudoku/sudoku_solve.ml b/src/sudoku/sudoku_solve.ml
index 8269ac2d..72dc1e6b 100644
--- a/src/sudoku/sudoku_solve.ml
+++ b/src/sudoku/sudoku_solve.ml
@@ -261,14 +261,14 @@ end = struct
             )
         )
 
-    let assume (self:t) acts : unit =
+    let partial_check (self:t) acts : unit =
       Log.debugf 4
-        (fun k->k "(@[sudoku.assume@ :trail [@[%a@]]@])" (Fmt.seq F.pp) (trail_ acts));
+        (fun k->k "(@[sudoku.partial-check@ :trail [@[%a@]]@])" (Fmt.seq F.pp) (trail_ acts));
       add_slice self acts;
       check_ self acts
 
-    let if_sat (self:t) acts : unit =
-      Log.debugf 4 (fun k->k "(@[sudoku.if-sat@])");
+    let final_check (self:t) acts : unit =
+      Log.debugf 4 (fun k->k "(@[sudoku.final-check@])");
       check_full_ self acts;
       check_ self acts