From 9b733851c69b09d4d77f3c823832a2b45ece2acf Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 11 Nov 2014 15:34:10 +0100
Subject: [PATCH] Removed useless argument to Th.assume

---
 sat/sat.ml         | 2 +-
 sat/solver.ml      | 6 +++++-
 sat/theory_intf.ml | 3 +--
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/sat/sat.ml b/sat/sat.ml
index 83a3a505..9dbb0f21 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -72,7 +72,7 @@ module Tsat = struct
 
   let dummy = ()
   let empty () = ()
-  let assume ~cs:_ _ _ _ = ()
+  let assume _ _ _ = ()
 end
 
 module Make(Dummy : sig end) = struct
diff --git a/sat/solver.ml b/sat/solver.ml
index a80ac63e..2cd3f665 100644
--- a/sat/solver.ml
+++ b/sat/solver.ml
@@ -381,7 +381,7 @@ module Make (F : Formula_intf.S)
       let full_model = nb_assigns() = env.nb_init_vars in
       env.tenv <-
         List.fold_left
-          (fun t (a,ex) -> let t = Th.assume ~cs:true a ex t in t)
+          (fun t (a,ex) -> let t = Th.assume a ex t in t)
           env.tenv !facts;
       if full_model then expensive_theory_propagate ()
       else None
@@ -561,6 +561,7 @@ module Make (F : Formula_intf.S)
     var_decay_activity ();
     clause_decay_activity ()
 
+  (*
   let check_inconsistency_of dep =
     try
       let env = ref (Th.empty()) in ();
@@ -572,6 +573,7 @@ module Make (F : Formula_intf.S)
       (* ignore (Th.expensive_processing !env); *)
       assert false
     with Th.Inconsistent _ -> ()
+  *)
 
   let theory_analyze dep =
     let atoms, sz, max_lvl, c_hist =
@@ -701,9 +703,11 @@ module Make (F : Formula_intf.S)
   let check_vec vec =
     for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done
 
+  (*
   let check_model () =
     check_vec env.clauses;
     check_vec env.learnts
+  *)
 
   (* fixpoint of propagation and decisions until a model is found, or a
      conflict is reached *)
diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml
index 1dce23ab..3707ca43 100644
--- a/sat/theory_intf.ml
+++ b/sat/theory_intf.ml
@@ -37,10 +37,9 @@ module type S = sig
   val empty : unit -> t
   (** A function to create an empty theory. *)
 
-  val assume : cs:bool -> formula -> explanation -> t -> t
+  val assume : formula -> explanation -> t -> t
   (** Return a new theory state with the formula as assumption.
       @raise Inconsistent if the new state would be inconsistent. *)
-  (* TODO: remove (apparently) useless [cs] parameter *)
 
 end