Remove is_unsat function

src/lib/reasoners/fun_sat_frontend.ml

@@ -71,6 +71,4 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     raise (Util.Not_implemented "optimization is not supported by FunSAT.")
 
   let supports_optimization = false
-
-  let is_unsat _env = assert false
 end

src/lib/reasoners/sat_solver_sig.ml

@@ -159,7 +159,6 @@ module type S = sig
 
   val supports_optimization : bool
   (** Returns whether the solver supports optimization. *)
-  val is_unsat : t -> bool
 end
 
 

src/lib/reasoners/sat_solver_sig.mli

@@ -139,7 +139,6 @@ module type S = sig
 
   val supports_optimization : bool
   (** Returns whether the solver supports optimization. *)
-  val is_unsat : t -> bool
 end
 
 

src/lib/reasoners/satml.ml

@@ -140,8 +140,6 @@ module type SAT_ML = sig
   val pop : t -> unit
 
   val optimize : t -> Objective.Function.t -> unit
-
-  val is_unsat : t -> bool
 end
 
 module MFF = FF.Map
@@ -2291,5 +2289,4 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       Vec.replace (fun fns -> fn :: fns) env.objectives
         (Vec.size env.objectives - 1)
 
-  let is_unsat env = env.is_unsat
 end

src/lib/reasoners/satml.mli

@@ -98,7 +98,6 @@ module type SAT_ML = sig
 
       @raise invalid_argurment if the decision level of [env] is not zero. *)
 
-  val is_unsat : t -> bool
 end
 
 module Make (Th : Theory.S) : SAT_ML with type th = Th.t

src/lib/reasoners/satml_frontend.ml

@@ -1478,7 +1478,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     Shostak.Combine.save_cache ();
     Uf.save_cache ()
 
-  let is_unsat env = SAT.is_unsat env.satml
 end
 
 (*