Smt solver with dummy theory now builds

src/main.ml

@@ -6,8 +6,8 @@ Copyright 2014 Simon Cruanes
 
 module Sat = Sat.Make(struct end)
 module Dummy = Sat
-  (*
 module Smt = Smt.Make(struct end)
+  (*
 module Mcsat = Mcsat.Make(struct end)
     *)
 

src/smt/smt.ml

@@ -4,8 +4,9 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Tsmt = struct
+module Th = Solver.DummyTheory(Expr_smt.Atom)
 
+  (* struct
   module CC = Cc.Make(String)
 
   type formula = Fsmt.t
@@ -49,22 +50,7 @@ module Tsmt = struct
   let if_sat _ = ()
 
 end
+  *)
 
-module Make(Dummy:sig end) = struct
+module Make(Dummy:sig end) =
-
+  Solver.Make(Expr_smt.Atom)(Th)(struct end)
-  include Solver.Make(Fsmt)(Tsmt)(struct end)
-  module Dot = Dot.Make(Proof)(struct
-      let print_atom = St.print_atom
-      let lemma_info () = "Proof", Some "PURPLE", []
-    end)
-  module Dedukti = Dedukti.Make(Proof)(struct
-      let print _ _ = ()
-      let prove _ _ = ()
-      let context _ _ = ()
-    end)
-
-  let print_clause = St.print_clause
-  let print_dot = Dot.print
-  let print_dedukti = Dedukti.print
-
-end

src/smt/smt.mli

@@ -4,19 +4,5 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make(Dummy: sig end) : sig
+module Make(Dummy: sig end) : Solver.S with type St.formula = Expr_smt.atom
-  (** Fonctor to make a SMT Solver module with built-in literals. *)
-
-  include Solver.S with type St.formula = Expr.t
-
-  val print_clause : Format.formatter -> St.clause -> unit
-  (** Print the clause on the given formatter. *)
-
-  val print_dot : Format.formatter -> Proof.proof -> unit
-  (** Print the given proof in dot format. *)
-
-  val print_dedukti : Format.formatter -> Proof.proof -> unit
-  (** Print the given proof in dot format. *)
-
-end