Removed solver_types module in solver.Make functor

sat/res_intf.ml

@@ -16,8 +16,8 @@ module type S = sig
   (** Learn and build proofs for the clause in the vector. Clauses in the vector should be in the order they were learned. *)
 
   val assert_can_prove_unsat : clause -> unit
-  (** [prove_unsat c] tries and prove the empty clause from [c]. [c] may be a learnt clause not yet proved.
+  (** [assert_can_prove_unsat c] tries and prove the empty clause from [c]. [c] may be a learnt clause not yet proved.
-      @raise Cannot if it is impossible. *)
+      @raise Insuficient_hyps if it is impossible. *)
 
   type proof_node = {
     conclusion : clause;
@@ -30,7 +30,9 @@ module type S = sig
     | Resolution of proof * proof * atom
 
   val prove_unsat : clause -> proof
-  (** Given a conflict clause [c], returns a proof of the empty clause. *)
+  (** Given a conflict clause [c], returns a proof of the empty clause. Same as [assert_can_prove_unsat] but returns
+      the proof if it succeeds.
+      @raise Insuficient_hyps if it does not succeed. *)
 
   val unsat_core : proof -> clause list
   (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. *)

sat/sat.ml

@@ -55,8 +55,6 @@ end
 
 module Tseitin = Tseitin.Make(Fsat)
 
-module Stypes = Solver_types.Make(Fsat)
-
 module Tsat = struct
   (* We don't have anything to do since the SAT Solver already
    * does propagation and conflict detection *)
@@ -84,12 +82,12 @@ module Tsat = struct
 end
 
 module Make(Dummy : sig end) = struct
-  module SatSolver = Solver.Make(Fsat)(Stypes)(Tsat)
+  module SatSolver = Solver.Make(Fsat)(Tsat)
 
   exception Bad_atom
 
   type atom = Fsat.t
-  type clause = Stypes.clause
+  type clause = SatSolver.St.clause
   type proof = SatSolver.Proof.proof
 
   type res =
@@ -141,7 +139,7 @@ module Make(Dummy : sig end) = struct
   let unsat_core = SatSolver.Proof.unsat_core
 
   let print_atom = Fsat.print
-  let print_clause = Stypes.print_clause
+  let print_clause = SatSolver.St.print_clause
   let print_proof = SatSolver.Proof.print_dot
 
 end

sat/solver.ml

@@ -11,12 +11,13 @@
 (**************************************************************************)
 
 module Make (F : Formula_intf.S)
-    (St : Solver_types.S with type formula = F.t)
     (Th : Theory_intf.S with type formula = F.t) = struct
 
-  open St
+  module St = Solver_types.Make(F)
   module Proof = Res.Make(St)(Th)
 
+  open St
+
   exception Sat
   exception Unsat
   exception Restart

sat/solver.mli

@@ -12,18 +12,19 @@
 (**************************************************************************)
 
 module Make (F : Formula_intf.S)
-    (St : Solver_types.S with type formula = F.t)
+    (Th : Theory_intf.S with type formula = F.t) : sig
-    (Th : Theory_intf.S with type formula = F.t) :
-sig
   (** Functor to create a SMT Solver parametrised by the atomic
       formulas and a theory. *)
 
   exception Unsat
 
+  module St : Solver_types.S with
+    type formula = F.t
+
   module Proof : Res.S with
     type atom = St.atom and
-  type clause = St.clause and
+    type clause = St.clause and
-  type lemma = Th.proof
+    type lemma = Th.proof
 
   val solve : unit -> unit
   (** Try and solves the current set of assumptions.