use generative functors, remove a layer of nesting for SMT libs

src/core/BitField.ml

@@ -107,7 +107,7 @@ let get_then_incr n =
   incr n;
   x
 
-module Make(X : sig end) : S = struct
+module Make() : S = struct
   type t = int
 
   let empty = 0

src/core/BitField.mli

@@ -62,7 +62,7 @@ module type S = sig
 end
 
 (** Create a new bitfield type *)
-module Make(X : sig end) : S
+module Make() : S
 
 (**/**)
 val all_bits_ : int -> int -> int

src/core/External.ml

@@ -42,7 +42,8 @@ module Make
     (Th : Plugin_intf.S with type term = St.term
                          and type formula = St.formula
                          and type proof = St.proof)
-    (Dummy : sig end) = struct
+    ()
+= struct
 
   module St = St
 

src/core/External.mli

@@ -18,7 +18,7 @@ module Make
     (Th : Plugin_intf.S with type term = St.term
                          and type formula = St.formula
                          and type proof = St.proof)
-    (Dummy : sig end) :
+    () :
   S with module St = St
 (** Functor to make a safe external interface. *)
 

src/core/Solver_types.ml

@@ -27,7 +27,7 @@ let () = Var_fields.freeze()
 (* Solver types for McSat Solving *)
 (* ************************************************************************ *)
 
-module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
+module McMake (E : Expr_intf.S)() = struct
 
   (* Flag for Mcsat v.s Pure Sat *)
   let mcsat = true
@@ -375,7 +375,7 @@ end
 (* Solver types for pure SAT Solving *)
 (* ************************************************************************ *)
 
-module SatMake (E : Formula_intf.S)(Dummy : sig end) = struct
+module SatMake (E : Formula_intf.S)() = struct
   include McMake(struct
       include E
       module Term = E

src/core/Solver_types.mli

@@ -30,11 +30,11 @@ module type S = Solver_types_intf.S
 
 module Var_fields = Solver_types_intf.Var_fields
 
-module McMake (E : Expr_intf.S)(Dummy : sig end):
+module McMake (E : Expr_intf.S)():
     S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof
 (** Functor to instantiate the types of clauses for a solver. *)
 
-module SatMake (E : Formula_intf.S)(Dummy : sig end):
+module SatMake (E : Formula_intf.S)():
     S with type term = E.t and type formula = E.t and type proof = E.proof
 (** Functor to instantiate the types of clauses for a solver. *)
 

src/core/Solver_types_intf.ml

@@ -22,7 +22,7 @@ Copyright 2016 Simon Cruanes
     used in the core solver.
 *)
 
-module Var_fields = BitField.Make(struct end)
+module Var_fields = BitField.Make()
 
 module type S = sig
   (** The signatures of clauses used in the Solver. *)

src/main/main.ml

@@ -105,9 +105,9 @@ module Make
         Dolmen.Statement.print s
 end
 
-module Sat = Make(Msat_sat.Sat.Make(struct end))(Msat_sat.Type_sat)
+module Sat = Make(Msat_sat.Make(struct end))(Msat_sat.Type)
-module Smt = Make(Msat_smt.Smt.Make(struct end))(Msat_smt.Type_smt)
+module Smt = Make(Msat_smt.Make(struct end))(Msat_smt.Type)
-module Mcsat = Make(Msat_mcsat.Mcsat.Make(struct end))(Msat_smt.Type_smt)
+module Mcsat = Make(Msat_mcsat.Make(struct end))(Msat_smt.Type)
 
 let solver = ref (module Sat : S)
 let solver_list = [
@@ -226,8 +226,8 @@ let () =
   | Incorrect_model ->
     Format.printf "Internal error : incorrect *sat* model@.";
     exit 4
-  | Msat_sat.Type_sat.Typing_error (msg, t)
+  | Msat_sat.Type.Typing_error (msg, t)
-  | Msat_smt.Type_smt.Typing_error (msg, t) ->
+  | Msat_smt.Type.Typing_error (msg, t) ->
     let b = Printexc.get_backtrace () in
     let loc = match t.Dolmen.Term.loc with
       | Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0

src/mcsat/Msat_mcsat.ml

@@ -4,10 +4,10 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make(Dummy:sig end) =
+module Make() =
   Msat_solver.Mcsolver.Make(struct
     type proof = unit
-    module Term = Msat_smt.Expr_smt.Term
+    module Term = Msat_smt.Expr.Term
-    module Formula = Msat_smt.Expr_smt.Atom
+    module Formula = Msat_smt.Expr.Atom
-  end)(Plugin_mcsat)(struct end)
+  end)(Plugin_mcsat)()
 

src/mcsat/Msat_mcsat.mli

@@ -4,5 +4,5 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make(Dummy: sig end) : Msat_solver.Solver.S with type St.formula = Expr_smt.atom
+module Make() : Msat_solver.Solver.S with type St.formula = Msat_smt.Expr.atom
 

src/mcsat/plugin_mcsat.ml

@@ -1,7 +1,7 @@
 
 (* Module initialization *)
 
-open Msat_smt
+module Expr_smt = Msat_smt.Expr
 
 module E = Eclosure.Make(Expr_smt.Term)
 module H = Backtrack.Hashtbl(Expr_smt.Term)

src/sat/Expr_sat.ml

@@ -0,0 +1,70 @@
+
+exception Bad_atom
+(** Exception raised if an atom cannot be created *)
+
+type proof
+(** A empty type for proofs *)
+
+type t = int
+(** Atoms are represented as integers. [-i] begin the negation of [i].
+    Additionally, since we nee dot be able to create fresh atoms, we
+    use even integers for user-created atoms, and odd integers for the
+    fresh atoms. *)
+
+let max_lit = max_int
+
+(* Counters *)
+let max_index = ref 0
+let max_fresh = ref (-1)
+
+(** Internal function for creating atoms.
+    Updates the internal counters *)
+let _make i =
+  if i <> 0 && (abs i) < max_lit then begin
+    max_index := max !max_index (abs i);
+    i
+  end else
+    raise Bad_atom
+
+(** A dummy atom *)
+let dummy = 0
+
+(** *)
+let neg a = - a
+
+let norm a =
+  abs a, if a < 0 then
+    Formula_intf.Negated
+  else
+    Formula_intf.Same_sign
+
+let abs = abs
+
+let sign i = i > 0
+
+let apply_sign b i = if b then i else neg i
+
+let set_sign b i = if b then abs i else neg (abs i)
+
+let hash (a:int) = a land max_int
+let equal (a:int) b = a=b
+let compare (a:int) b = Pervasives.compare a b
+
+let make i = _make (2 * i)
+
+let fresh () =
+  incr max_fresh;
+  _make (2 * !max_fresh + 1)
+
+(*
+let iter: (t -> unit) -> unit = fun f ->
+  for j = 1 to !max_index do
+    f j
+  done
+*)
+
+let print fmt a =
+  Format.fprintf fmt "%s%s%d"
+    (if a < 0 then "~" else "")
+    (if a mod 2 = 0 then "v" else "f")
+    ((abs a) / 2)

src/sat/Expr_sat.mli

@@ -0,0 +1,31 @@
+
+(** The module defining formulas *)
+
+(** SAT Formulas
+
+    This modules implements formuals adequate for use in a pure SAT Solver.
+    Atomic formuals are represented using integers, that should allow
+    near optimal efficiency (both in terms of space and time).
+*)
+
+include Formula_intf.S
+(** This modules implements the requirements for implementing an SAT Solver. *)
+
+val make : int -> t
+(** Make a proposition from an integer. *)
+
+val fresh : unit -> t
+(** Make a fresh atom *)
+
+val compare : t -> t -> int
+(** Compare atoms *)
+
+val sign : t -> bool
+(** Is the given atom positive ? *)
+
+val apply_sign : bool -> t -> t
+(** [apply_sign b] is the identity if [b] is [true], and the negation
+    function if [b] is [false]. *)
+
+val set_sign : bool -> t -> t
+(** Return the atom with the sign set. *)

src/sat/Msat_sat.ml

@@ -0,0 +1,11 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+*)
+
+module Expr = Expr_sat
+module Type = Type_sat
+
+module Make() =
+  Msat_solver.Solver.Make(Expr)(Msat_solver.Solver.DummyTheory(Expr))()
+

src/sat/Msat_sat.mli

@@ -0,0 +1,17 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+*)
+
+(** Sat solver
+
+    This modules instanciates a pure sat solver using integers to represent
+    atomic propositions.
+*)
+
+module Expr = Expr_sat
+module Type = Type_sat
+
+module Make() : Msat_solver.Solver.S with type St.formula = Expr.t
+(** A functor that can generate as many solvers as needed. *)
+

src/sat/sat.ml

@@ -1,82 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2016 Guillaume Bury
-*)
-
-module Expr = struct
-
-  exception Bad_atom
-  (** Exception raised if an atom cannot be created *)
-
-  type proof
-  (** A empty type for proofs *)
-
-  type t = int
-  (** Atoms are represented as integers. [-i] begin the negation of [i].
-      Additionally, since we nee dot be able to create fresh atoms, we
-      use even integers for user-created atoms, and odd integers for the
-      fresh atoms. *)
-
-  let max_lit = max_int
-
-  (* Counters *)
-  let max_index = ref 0
-  let max_fresh = ref (-1)
-
-  (** Internal function for creating atoms.
-      Updates the internal counters *)
-  let _make i =
-    if i <> 0 && (abs i) < max_lit then begin
-      max_index := max !max_index (abs i);
-      i
-    end else
-      raise Bad_atom
-
-  (** A dummy atom *)
-  let dummy = 0
-
-  (** *)
-  let neg a = - a
-
-  let norm a =
-    abs a, if a < 0 then
-      Formula_intf.Negated
-    else
-      Formula_intf.Same_sign
-
-  let abs = abs
-
-  let sign i = i > 0
-
-  let apply_sign b i = if b then i else neg i
-
-  let set_sign b i = if b then abs i else neg (abs i)
-
-  let hash (a:int) = a land max_int
-  let equal (a:int) b = a=b
-  let compare (a:int) b = Pervasives.compare a b
-
-  let make i = _make (2 * i)
-
-  let fresh () =
-    incr max_fresh;
-    _make (2 * !max_fresh + 1)
-
-  (*
-  let iter: (t -> unit) -> unit = fun f ->
-    for j = 1 to !max_index do
-      f j
-    done
-  *)
-
-  let print fmt a =
-    Format.fprintf fmt "%s%s%d"
-      (if a < 0 then "~" else "")
-      (if a mod 2 = 0 then "v" else "f")
-      ((abs a) / 2)
-
-end
-
-module Make(Dummy : sig end) =
-  Msat_solver.Solver.Make(Expr)(Msat_solver.Solver.DummyTheory(Expr))(struct end)
-

src/sat/sat.mli

@@ -1,47 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2016 Guillaume Bury
-*)
-
-(** Sat solver
-
-    This modules instanciates a pure sat solver using integers to represent
-    atomic propositions.
-*)
-
-module Expr : sig
-  (** SAT Formulas
-
-      This modules implements formuals adequate for use in a pure SAT Solver.
-      Atomic formuals are represented using integers, that should allow
-      near optimal efficiency (both in terms of space and time).
-  *)
-
-  include Formula_intf.S
-  (** This modules implements the requirements for implementing an SAT Solver. *)
-
-  val make : int -> t
-  (** Make a proposition from an integer. *)
-
-  val fresh : unit -> t
-  (** Make a fresh atom *)
-
-  val compare : t -> t -> int
-  (** Compare atoms *)
-
-  val sign : t -> bool
-  (** Is the given atom positive ? *)
-
-  val apply_sign : bool -> t -> t
-  (** [apply_sign b] is the identity if [b] is [true], and the negation
-      function if [b] is [false]. *)
-
-  val set_sign : bool -> t -> t
-  (** Return the atom with the sign set. *)
-
-end
-(** The module defining formulas *)
-
-module Make(Dummy : sig end) : Msat_solver.Solver.S with type St.formula = Expr.t
-(** A functor that can generate as many solvers as needed. *)
-

src/sat/type_sat.ml

@@ -10,7 +10,7 @@ Copyright 2014 Simon Cruanes
 module Id = Dolmen.Id
 module Ast = Dolmen.Term
 module H = Hashtbl.Make(Id)
-module Formula = Msat_tseitin.Make(Sat.Expr)
+module Formula = Msat_tseitin.Make(Expr_sat)
 
 (* Exceptions *)
 (* ************************************************************************ *)
@@ -26,7 +26,7 @@ let find_id id =
   try
     H.find symbols id
   with Not_found ->
-    let res = Sat.Expr.fresh () in
+    let res = Expr_sat.fresh () in
     H.add symbols id res;
     res
 

src/sat/type_sat.mli

@@ -8,5 +8,5 @@ Copyright 2014 Simon Cruanes
     This module provides functions to parse terms from the untyped syntax tree
     defined in Dolmen, and generate formulas as defined in the Expr_sat module. *)
 
-include Msat_solver.Type.S with type atom := Sat.Expr.t
+include Msat_solver.Type.S with type atom := Expr_sat.t
 

src/smt/Msat_smt.ml

@@ -4,8 +4,11 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+module Expr = Expr_smt
+module Type = Type_smt
+
 module Th = Msat_solver.Solver.DummyTheory(Expr_smt.Atom)
 
-module Make(Dummy:sig end) =
+module Make() =
-  Msat_solver.Solver.Make(Expr_smt.Atom)(Th)(struct end)
+  Msat_solver.Solver.Make(Expr_smt.Atom)(Th)()
 

src/smt/Msat_smt.mli

@@ -4,5 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make(Dummy: sig end) : Msat_solver.Solver.S with type St.formula = Msat_smt.Expr_smt.atom
+module Expr = Expr_smt
+module Type = Type_smt
+
+module Make() : Msat_solver.Solver.S with type St.formula = Expr_smt.atom
 

src/solver/mcsolver.ml

@@ -10,10 +10,10 @@ module Make (E : Expr_intf.S)
     (Th : Plugin_intf.S with type term = E.Term.t
                          and type formula = E.Formula.t
                          and type proof = E.proof)
-    (Dummy: sig end) =
+    () =
   External.Make
     (Solver_types.McMake(E)(struct end))
     (Th)
-    (struct end)
+    ()
 
 

src/solver/mcsolver.mli

@@ -16,7 +16,7 @@ module Make (E : Expr_intf.S)
     (Th : Plugin_intf.S with type term = E.Term.t
                          and type formula = E.Formula.t
                          and type proof = E.proof)
-    (Dummy: sig end) :
+    () :
   S with type St.term = E.Term.t
      and type St.formula = E.Formula.t
      and type St.proof = E.proof

src/solver/solver.ml

@@ -76,10 +76,10 @@ end
 
 module Make (E : Formula_intf.S)
     (Th : Theory_intf.S with type formula = E.t and type proof = E.proof)
-    (Dummy: sig end) =
+    () =
   External.Make
     (Solver_types.SatMake(E)(struct end))
     (Plugin(E)(Th))
-    (struct end)
+    ()
 
 

src/solver/solver.mli

@@ -23,7 +23,7 @@ module DummyTheory(F : Formula_intf.S) :
 module Make (F : Formula_intf.S)
     (Th : Theory_intf.S with type formula = F.t
                          and type proof = F.proof)
-    (Dummy: sig end) :
+    () :
   S with type St.formula = F.t
      and type St.proof = F.proof
 (** Functor to create a SMT Solver parametrised by the atomic

tests/test_api.ml

@@ -7,9 +7,8 @@ Copyright 2014 Simon Cruanes
 (* Tests that require the API *)
 
 open Msat
-open Msat_sat
 
-module F = Sat.Expr
+module F = Msat_sat.Expr
 module T = Msat_tseitin.Make(F)
 
 let (|>) x f = f x
@@ -47,7 +46,7 @@ end
 
 let mk_solver (): (module BASIC_SOLVER) =
   let module S = struct
-    include Sat.Make(struct end)
+    include Msat_sat.Make(struct end)
     let solve ?assumptions ()= match solve ?assumptions() with
       | Sat _ ->
         R_sat