From f348dcd5ae65aafc226f395f5d50b1791bec1734 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 29 Jan 2016 14:40:43 +0100
Subject: [PATCH] expose dummy theory in a functor

---
 sat/sat.ml            | 44 +++++++++----------------------------------
 solver/solver.ml      | 25 ++++++++++++++++++++++++
 solver/solver.mli     |  4 ++++
 solver/theory_intf.ml |  7 +++++++
 4 files changed, 45 insertions(+), 35 deletions(-)

diff --git a/sat/sat.ml b/sat/sat.ml
index 227ffcec..6c68d8e0 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -57,45 +57,13 @@ module Fsat = struct
       (if a < 0 then "~" else "")
       (if a mod 2 = 0 then "v" else "f")
       ((abs a) / 2)
-
 end
 
 module Tseitin = Tseitin.Make(Fsat)
 
-module Tsat = struct
-  (* We don't have anything to do since the SAT Solver already
-   * does propagation and conflict detection *)
-
-  type formula = Fsat.t
-  type proof = unit
-  type level = unit
-
-  type slice = {
-    start : int;
-    length : int;
-    get : int -> formula;
-    push : formula list -> proof -> unit;
-  }
-
-  type res =
-    | Sat of level
-    | Unsat of formula list * proof
-
-  let dummy = ()
-  let current_level () = ()
-  let assume _ = Sat ()
-  let backtrack _ = ()
-
-end
-
 module Make(Dummy : sig end) = struct
-
+  module Tsat = Solver.DummyTheory(Fsat)
   module SatSolver = Solver.Make(Fsat)(Tsat)
-  module Dot = Dot.Make(SatSolver.Proof)(struct
-      let clause_name c = SatSolver.St.(c.name)
-      let print_atom = SatSolver.St.print_atom
-      let lemma_info () = "()", None, []
-    end)
 
   exception Bad_atom
 
@@ -158,6 +126,12 @@ module Make(Dummy : sig end) = struct
 
   let print_atom = Fsat.print
   let print_clause = SatSolver.St.print_clause
-  let print_proof = Dot.print
-
+  let print_proof out p =
+    let module Dot = Dot.Make(SatSolver.Proof)(struct
+        let clause_name c = SatSolver.St.(c.name)
+        let print_atom = SatSolver.St.print_atom
+        let lemma_info () = "()", None, []
+      end)
+    in
+    Dot.print out p
 end
diff --git a/solver/solver.ml b/solver/solver.ml
index 020ba371..c71e07c7 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -10,6 +10,31 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module DummyTheory(F : Formula_intf.S with type proof = unit) = struct
+  (* We don't have anything to do since the SAT Solver already
+   * does propagation and conflict detection *)
+
+  type formula = F.t
+  type proof = unit
+  type level = unit
+
+  type slice = {
+    start : int;
+    length : int;
+    get : int -> formula;
+    push : formula list -> proof -> unit;
+  }
+
+  type res =
+    | Sat of level
+    | Unsat of formula list * proof
+
+  let dummy = ()
+  let current_level () = ()
+  let assume _ = Sat ()
+  let backtrack _ = ()
+end
+
 module Make (E : Formula_intf.S)
     (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct
 
diff --git a/solver/solver.mli b/solver/solver.mli
index a6ab67e5..56bd14ad 100644
--- a/solver/solver.mli
+++ b/solver/solver.mli
@@ -11,6 +11,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Simple case where the proof type is [unit] and the theory is empty *)
+module DummyTheory(F : Formula_intf.S with type proof = unit) :
+  Theory_intf.S with type formula = F.t and type proof = unit
+
 module Make (F : Formula_intf.S)
     (Th : Theory_intf.S with type formula = F.t and type proof = F.proof) : sig
   (** Functor to create a SMT Solver parametrised by the atomic
diff --git a/solver/theory_intf.ml b/solver/theory_intf.ml
index 3923ff0e..527b73b1 100644
--- a/solver/theory_intf.ml
+++ b/solver/theory_intf.ml
@@ -12,6 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+type ('form, 'proof) slice = {
+  start : int;
+  length : int;
+  get : int -> 'form;
+  push : 'form list -> 'proof -> unit;
+}
+
 module type S = sig
   (** Signature for theories to be given to the Solver. *)