From 0631135bd5769e09c3226e490ddb7d93327b81c6 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 12 Sep 2016 15:43:57 +0200
Subject: [PATCH] Smt solver with dummy theory now builds

---
 src/main.ml                             |  2 +-
 src/{util/expr.ml => smt/expr_smt.ml}   |  0
 src/{util/expr.mli => smt/expr_smt.mli} |  0
 src/smt/smt.ml                          | 24 +++++-------------------
 src/smt/smt.mli                         | 16 +---------------
 src/{util => smt}/type_smt.ml           |  0
 src/{util => smt}/type_smt.mli          |  0
 7 files changed, 7 insertions(+), 35 deletions(-)
 rename src/{util/expr.ml => smt/expr_smt.ml} (100%)
 rename src/{util/expr.mli => smt/expr_smt.mli} (100%)
 rename src/{util => smt}/type_smt.ml (100%)
 rename src/{util => smt}/type_smt.mli (100%)

diff --git a/src/main.ml b/src/main.ml
index b3e0450d..521f5c6c 100644
--- a/src/main.ml
+++ b/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)
     *)
 
diff --git a/src/util/expr.ml b/src/smt/expr_smt.ml
similarity index 100%
rename from src/util/expr.ml
rename to src/smt/expr_smt.ml
diff --git a/src/util/expr.mli b/src/smt/expr_smt.mli
similarity index 100%
rename from src/util/expr.mli
rename to src/smt/expr_smt.mli
diff --git a/src/smt/smt.ml b/src/smt/smt.ml
index b42478fc..f80984fb 100644
--- a/src/smt/smt.ml
+++ b/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
-
-  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
+module Make(Dummy:sig end) =
+  Solver.Make(Expr_smt.Atom)(Th)(struct end)
diff --git a/src/smt/smt.mli b/src/smt/smt.mli
index f703efe4..edb13401 100644
--- a/src/smt/smt.mli
+++ b/src/smt/smt.mli
@@ -4,19 +4,5 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make(Dummy: sig end) : sig
-  (** 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
+module Make(Dummy: sig end) : Solver.S with type St.formula = Expr_smt.atom
 
diff --git a/src/util/type_smt.ml b/src/smt/type_smt.ml
similarity index 100%
rename from src/util/type_smt.ml
rename to src/smt/type_smt.ml
diff --git a/src/util/type_smt.mli b/src/smt/type_smt.mli
similarity index 100%
rename from src/util/type_smt.mli
rename to src/smt/type_smt.mli