make state explicit and add type t state-wrapper in most modules

src/backend/Coq.ml

@@ -127,21 +127,18 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
     | S.Lemma _ ->
       A.prove_lemma fmt (name clause) clause
     | S.Duplicate (p, l) ->
-      let p' = S.expand p in
+      let c = S.conclusion p in
-      let c = p'.S.conclusion in
       let () = elim_duplicate fmt clause c l in
       clean t fmt [c]
     | S.Resolution (p1, p2, a) ->
-      let c1 = (S.expand p1).S.conclusion in
+      let c1 = S.conclusion p1 in
-      let c2 = (S.expand p2).S.conclusion in
+      let c2 = S.conclusion p2 in
       if resolution fmt clause c1 c2 a then clean t fmt [c1; c2]
 
   let count_uses p =
     let h = S.H.create 4013 in
     let aux () node =
-      List.iter (fun p' ->
+      List.iter (fun p' -> incr_use h S.(conclusion p')) (S.parents node.S.step)
-          incr_use h S.((expand p').conclusion))
-        (S.parents node.S.step)
     in
     let () = S.fold aux () p in
     h

src/backend/Dimacs.ml

@@ -7,18 +7,18 @@ Copyright 2014 Simon Cruanes
 open Msat
 
 module type S = sig
+  type st
 
   type clause
+  (** The type of clauses *)
 
   val export :
+    st ->
     Format.formatter ->
     hyps:clause Vec.t ->
     history:clause Vec.t ->
     local:clause Vec.t ->
     unit
-  (** Export the given clause vectors to the dimacs format.
-      The arguments should be transmitted directly from the corresponding
-      function of the {Internal} module. *)
 
   val export_icnf :
     Format.formatter ->
@@ -26,13 +26,11 @@ module type S = sig
     history:clause Vec.t ->
     local:clause Vec.t ->
     unit
-  (** Export the given clause vectors to the dimacs format.
-      The arguments should be transmitted directly from the corresponding
-      function of the {Internal} module. *)
 
 end
 
-module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
+module Make(St : Solver_types_intf.S) = struct
+  type st = St.t
 
   (* Dimacs & iCNF export *)
   let export_vec name fmt vec =
@@ -76,7 +74,7 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
       ) learnt;
     lemmas
 
-  let export fmt ~hyps ~history ~local =
+  let export st fmt ~hyps ~history ~local =
     assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);
     (* Learnt clauses, then filtered to only keep only
        the theory lemmas; all other learnt clauses should be logical
@@ -85,7 +83,7 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
     (* Local assertions *)
     assert (Vec.for_all (fun c -> St.Local = St.Clause.premise c) local);
     (* Number of atoms and clauses *)
-    let n = St.nb_elt () in
+    let n = St.nb_elt st in
     let m = Vec.size local + Vec.size hyps + Vec.size lemmas in
     Format.fprintf fmt
       "@[<v>p cnf %d %d@,%a%a%a@]@." n m

src/backend/Dimacs.mli

@@ -13,11 +13,13 @@ Copyright 2014 Simon Cruanes
 open Msat
 
 module type S = sig
+  type st
 
   type clause
   (** The type of clauses *)
 
   val export :
+    st ->
     Format.formatter ->
     hyps:clause Vec.t ->
     history:clause Vec.t ->
@@ -42,6 +44,6 @@ module type S = sig
 
 end
 
-module Make(St: Solver_types_intf.S)(Dummy: sig end) : S with type clause := St.clause
+module Make(St: Solver_types_intf.S) : S with type clause := St.clause and type st = St.t
 (** Functor to create a module for exporting probems to the dimacs (& iCNF) formats. *)
 

src/core/Internal.mli

@@ -14,8 +14,8 @@ Copyright 2014 Simon Cruanes
 
 module Make
   (St : Solver_types.S)
-  (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
+  (Th : Plugin_intf.S with type term = St.term
-  (Dummy: sig end)
+                       and type formula = St.formula and type proof = St.proof)
 : sig
   (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
 
@@ -24,55 +24,63 @@ module Make
   exception Unsat
   exception UndecidedLit
 
-  val solve : unit -> unit
+  type t
+  (** Solver *)
+
+  val create : ?st:St.t -> unit -> t
+
+  val st : t -> St.t
+  (** Underlying state *)
+
+  val solve : t -> unit
   (** Try and solves the current set of assumptions.
       @return () if the current set of clauses is satisfiable
       @raise Unsat if a toplevel conflict is found *)
 
-  val assume : ?tag:int -> St.formula list list -> unit
+  val assume : t -> ?tag:int -> St.formula list list -> unit
   (** Add the list of clauses to the current set of assumptions.
       Modifies the sat solver state in place. *)
 
-  val new_lit : St.term -> unit
+  val new_lit : t -> St.term -> unit
   (** Add a new litteral (i.e term) to the solver. This term will
       be decided on at some point during solving, wether it appears
       in clauses or not. *)
 
-  val new_atom : St.formula -> unit
+  val new_atom : t -> St.formula -> unit
   (** Add a new atom (i.e propositional formula) to the solver.
       This formula will be decided on at some point during solving,
       wether it appears in clauses or not. *)
 
-  val push : unit -> unit
+  val push : t -> unit
   (** Create a decision level for local assumptions.
       @raise Unsat if a conflict is detected in the current state. *)
 
-  val pop : unit -> unit
+  val pop : t -> unit
   (** Pop a decision level for local assumptions. *)
 
-  val local : St.formula list -> unit
+  val local : t -> St.formula list -> unit
   (** Add local assumptions
       @param assumptions list of additional local assumptions to make,
         removed after the callback returns a value *)
 
   (** {2 Propositional models} *)
 
-  val eval : St.formula -> bool
+  val eval : t -> St.formula -> bool
   (** Returns the valuation of a formula in the current state
       of the sat solver.
       @raise UndecidedLit if the literal is not decided *)
 
-  val eval_level : St.formula -> bool * int
+  val eval_level : t -> St.formula -> bool * int
   (** Return the current assignement of the literals, as well as its
       decision level. If the level is 0, then it is necessary for
       the atom to have this value; otherwise it is due to choices
       that can potentially be backtracked.
       @raise UndecidedLit if the literal is not decided *)
 
-  val model : unit -> (St.term * St.term) list
+  val model : t -> (St.term * St.term) list
   (** Returns the model found if the formula is satisfiable. *)
 
-  val check : unit -> bool
+  val check : t -> bool
   (** Check the satisfiability of the current model. Only has meaning
       if the solver finished proof search and has returned [Sat]. *)
 
@@ -80,11 +88,11 @@ module Make
 
   module Proof : Res.S with module St = St
 
-  val unsat_conflict : unit -> St.clause option
+  val unsat_conflict : t -> St.clause option
   (** Returns the unsat clause found at the toplevel, if it exists (i.e if
       [solve] has raised [Unsat]) *)
 
-  val full_slice : unit -> (St.term, St.formula, St.proof) Plugin_intf.slice
+  val full_slice : t -> (St.term, St.formula, St.proof) Plugin_intf.slice
   (** View the current state of the trail as a slice. Mainly useful when the
       solver has reached a SAT conclusion. *)
 
@@ -92,21 +100,21 @@ module Make
       These functions expose some internal data stored by the solver, as such
       great care should be taken to ensure not to mess with the values returned. *)
 
-  val trail : unit -> St.trail_elt Vec.t
+  val trail : t -> St.trail_elt Vec.t
   (** Returns the current trail.
       *DO NOT MUTATE* *)
 
-  val hyps : unit -> St.clause Vec.t
+  val hyps : t -> St.clause Vec.t
   (** Returns the vector of assumptions used by the solver. May be slightly different
       from the clauses assumed because of top-level simplification of clauses.
       *DO NOT MUTATE* *)
 
-  val temp : unit -> St.clause Vec.t
+  val temp : t -> St.clause Vec.t
   (** Returns the clauses coreesponding to the local assumptions.
       All clauses in this vec are assured to be unit clauses.
       *DO NOT MUTATE* *)
 
-  val history : unit -> St.clause Vec.t
+  val history : t -> St.clause Vec.t
   (** Returns the history of learnt clauses, with no guarantees on order.
       *DO NOT MUTATE* *)
 

src/core/Res.ml

@@ -178,12 +178,15 @@ module Make(St : Solver_types.S) = struct
           end
         | _ ->
           Log.debugf error
-            (fun k -> k "While resolving clauses:@[<hov>%a@\n%a@]" St.Clause.debug c St.Clause.debug d);
+            (fun k -> k "While resolving clauses:@[<hov>%a@\n%a@]"
+                St.Clause.debug c St.Clause.debug d);
           raise (Resolution_error "Clause mismatch")
       end
     | _ ->
       raise (Resolution_error "Bad history")
 
+  let[@inline] conclusion (p:proof) : clause = p
+
   let expand conclusion =
     Log.debugf debug (fun k -> k "Expanding : @[%a@]" St.Clause.debug conclusion);
     match conclusion.St.cpremise with

src/core/Res_intf.ml

@@ -95,6 +95,8 @@ module type S = sig
   val expand : proof -> proof_node
   (** Return the proof step at the root of a given proof. *)
 
+  val conclusion : proof -> clause
+
   val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> 'a
   (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that
       [f] is executed exactly once on each proof node in the tree, and that the execution of

src/core/Solver.ml

@@ -13,12 +13,11 @@ module Make
     (Th : Plugin_intf.S with type term = St.term
                          and type formula = St.formula
                          and type proof = St.proof)
-    ()
 = struct
 
   module St = St
 
-  module S = Internal.Make(St)(Th)(struct end)
+  module S = Internal.Make(St)(Th)
 
   module Proof = S.Proof
 
@@ -26,25 +25,30 @@ module Make
 
   type atom = St.formula
 
+  type t = S.t
+
+  let create = S.create
+
   (* Result type *)
   type res =
     | Sat of (St.term,St.formula) sat_state
     | Unsat of (St.clause,Proof.proof) unsat_state
 
-  let pp_all lvl status =
+  let pp_all st lvl status =
     Log.debugf lvl
       (fun k -> k
-        "@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
+          "@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,\
+           @[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
           status
-          (Vec.print ~sep:"" St.Trail_elt.debug) (S.trail ())
+          (Vec.print ~sep:"" St.Trail_elt.debug) (S.trail st)
-          (Vec.print ~sep:"" St.Clause.debug) (S.temp ())
+          (Vec.print ~sep:"" St.Clause.debug) (S.temp st)
-          (Vec.print ~sep:"" St.Clause.debug) (S.hyps ())
+          (Vec.print ~sep:"" St.Clause.debug) (S.hyps st)
-          (Vec.print ~sep:"" St.Clause.debug) (S.history ())
+          (Vec.print ~sep:"" St.Clause.debug) (S.history st)
       )
 
-  let mk_sat () : (_,_) sat_state =
+  let mk_sat (st:S.t) : (_,_) sat_state =
-    pp_all 99 "SAT";
+    pp_all st 99 "SAT";
-    let t = S.trail () in
+    let t = S.trail st in
     let iter f f' =
       Vec.iter (function
           | St.Atom a -> f a.St.lit
@@ -52,16 +56,16 @@ module Make
         t
     in
     {
-      eval = S.eval;
+      eval = S.eval st;
-      eval_level = S.eval_level;
+      eval_level = S.eval_level st;
       iter_trail = iter;
-      model = S.model;
+      model = (fun () -> S.model st);
     }
 
-  let mk_unsat () : (_,_) unsat_state =
+  let mk_unsat (st:S.t) : (_,_) unsat_state =
-    pp_all 99 "UNSAT";
+    pp_all st 99 "UNSAT";
     let unsat_conflict () =
-      match S.unsat_conflict () with
+      match S.unsat_conflict st with
       | None -> assert false
       | Some c -> c
     in
@@ -74,21 +78,21 @@ module Make
   (* Wrappers around internal functions*)
   let assume = S.assume
 
-  let solve ?(assumptions=[]) () =
+  let solve (st:t) ?(assumptions=[]) () =
     try
-      S.pop (); (* FIXME: what?! *)
+      S.pop st; (* FIXME: what?! *)
-      S.push ();
+      S.push st;
-      S.local assumptions;
+      S.local st assumptions;
-      S.solve ();
+      S.solve st;
-      Sat (mk_sat())
+      Sat (mk_sat st)
     with S.Unsat ->
-      Unsat (mk_unsat())
+      Unsat (mk_unsat st)
 
   let unsat_core = S.Proof.unsat_core
 
-  let true_at_level0 a =
+  let true_at_level0 st a =
     try
-      let b, lev = S.eval_level a in
+      let b, lev = S.eval_level st a in
       b && lev = 0
     with S.UndecidedLit -> false
 
@@ -97,9 +101,9 @@ module Make
   let new_lit = S.new_lit
   let new_atom = S.new_atom
 
-  let export () : St.clause export =
+  let export (st:t) : St.clause export =
-    let hyps = S.hyps () in
+    let hyps = S.hyps st in
-    let history = S.history () in
+    let history = S.history st in
-    let local = S.temp () in
+    let local = S.temp st in
     {hyps; history; local}
 end

src/core/Solver.mli

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

src/core/Solver_intf.ml

@@ -61,6 +61,13 @@ module type S = sig
   module Proof : Res.S with module St = St
   (** A module to manipulate proofs. *)
 
+  type t
+  (** Main solver type, containing all state *)
+
+  val create : ?st:St.t -> unit -> t
+  (** Create new solver *)
+  (* TODO: add size hint, callbacks, etc. *)
+
   (** {2 Types} *)
 
   type atom = St.formula
@@ -77,19 +84,19 @@ module type S = sig
 
   (** {2 Base operations} *)
 
-  val assume : ?tag:int -> atom list list -> unit
+  val assume : t -> ?tag:int -> atom list list -> unit
   (** Add the list of clauses to the current set of assumptions.
       Modifies the sat solver state in place. *)
 
-  val solve : ?assumptions:atom list -> unit -> res
+  val solve : t -> ?assumptions:atom list -> unit -> res
   (** Try and solves the current set of assumptions. *)
 
-  val new_lit : St.term -> unit
+  val new_lit : t -> St.term -> unit
   (** Add a new litteral (i.e term) to the solver. This term will
       be decided on at some point during solving, wether it appears
       in clauses or not. *)
 
-  val new_atom : atom -> unit
+  val new_atom : t -> atom -> unit
   (** Add a new atom (i.e propositional formula) to the solver.
       This formula will be decided on at some point during solving,
       wether it appears in clauses or not. *)
@@ -97,13 +104,13 @@ module type S = sig
   val unsat_core : Proof.proof -> St.clause list
   (** Returns the unsat core of a given proof. *)
 
-  val true_at_level0 : atom -> bool
+  val true_at_level0 : t -> atom -> bool
   (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
       it must hold in all models *)
 
   val get_tag : St.clause -> int option
   (** Recover tag from a clause, if any *)
 
-  val export : unit -> St.clause export
+  val export : t -> St.clause export
 end
 

src/core/Solver_types.ml

@@ -27,7 +27,7 @@ let () = Var_fields.freeze()
 (* Solver types for McSat Solving *)
 (* ************************************************************************ *)
 
-module McMake (E : Expr_intf.S)() = struct
+module McMake (E : Expr_intf.S) = struct
 
   (* Flag for Mcsat v.s Pure Sat *)
   let mcsat = true
@@ -36,6 +36,8 @@ module McMake (E : Expr_intf.S)() = struct
   type formula = E.Formula.t
   type proof = E.proof
 
+  let pp_form = E.Formula.dummy
+
   type seen =
     | Nope
     | Both
@@ -136,16 +138,29 @@ module McMake (E : Expr_intf.S)() = struct
   module MF = Hashtbl.Make(E.Formula)
   module MT = Hashtbl.Make(E.Term)
 
+  type t = {
+    t_map: lit MT.t;
+    f_map: var MF.t;
+    vars: elt Vec.t;
+    mutable cpt_mk_var: int;
+    mutable cpt_mk_clause: int;
+  }
+
+  type state = t
+
+  let create() : t = {
+    f_map = MF.create 4096;
+    t_map = MT.create 4096;
+    vars = Vec.make 107 (E_var dummy_var);
+    cpt_mk_var = 0;
+    cpt_mk_clause = 0;
+  }
+
   (* TODO: embed a state `t` with these inside *)
-  let f_map = MF.create 4096
-  let t_map = MT.create 4096
 
-  let vars = Vec.make 107 (E_var dummy_var)
+  let nb_elt st = Vec.size st.vars
-  let nb_elt () = Vec.size vars
+  let get_elt st i = Vec.get st.vars i
-  let get_elt i = Vec.get vars i
+  let iter_elt st f = Vec.iter f st.vars
-  let iter_elt f = Vec.iter f vars
-
-  let cpt_mk_var = ref 0
 
   let name_of_clause c = match c.cpremise with
     | Hyp -> "H" ^ string_of_int c.name
@@ -165,20 +180,20 @@ module McMake (E : Expr_intf.S)() = struct
     let[@inline] weight l = l.l_weight
     let[@inline] set_weight l w = l.l_weight <- w
 
-    let make t =
+    let make (st:state) (t:term) : t =
-      try MT.find t_map t
+      try MT.find st.t_map t
       with Not_found ->
         let res = {
-          lid = !cpt_mk_var;
+          lid = st.cpt_mk_var;
           term = t;
           l_weight = 1.;
           l_idx= -1;
           l_level = -1;
           assigned = None;
         } in
-        incr cpt_mk_var;
+        st.cpt_mk_var <- st.cpt_mk_var + 1;
-        MT.add t_map t res;
+        MT.add st.t_map t res;
-        Vec.push vars (E_lit res);
+        Vec.push st.vars (E_lit res);
         res
 
     let debug_assign fmt v =
@@ -208,15 +223,14 @@ module McMake (E : Expr_intf.S)() = struct
     let[@inline] weight v = v.v_weight
     let[@inline] set_weight v w = v.v_weight <- w
 
-    let make : formula -> var * Expr_intf.negated =
+    let make (st:state) (t:formula) : var * Expr_intf.negated =
-      fun t ->
       let lit, negated = E.Formula.norm t in
       try
-          MF.find f_map lit, negated
+        MF.find st.f_map lit, negated
       with Not_found ->
-          let cpt_fois_2 = !cpt_mk_var lsl 1 in
+        let cpt_double = st.cpt_mk_var lsl 1 in
         let rec var  =
-            { vid = !cpt_mk_var;
+          { vid = st.cpt_mk_var;
             pa = pa;
             na = na;
             v_fields = Var_fields.empty;
@@ -232,17 +246,17 @@ module McMake (E : Expr_intf.S)() = struct
             watched = Vec.make 10 dummy_clause;
             neg = na;
             is_true = false;
-              aid = cpt_fois_2 (* aid = vid*2 *) }
+            aid = cpt_double (* aid = vid*2 *) }
         and na =
           { var = var;
             lit = E.Formula.neg lit;
             watched = Vec.make 10 dummy_clause;
             neg = pa;
             is_true = false;
-              aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
+            aid = cpt_double + 1 (* aid = vid*2+1 *) } in
-          MF.add f_map lit var;
+        MF.add st.f_map lit var;
-          incr cpt_mk_var;
+        st.cpt_mk_var <- st.cpt_mk_var + 1;
-          Vec.push vars (E_var var);
+        Vec.push st.vars (E_var var);
         var, negated
 
     (* Marking helpers *)
@@ -281,8 +295,8 @@ module McMake (E : Expr_intf.S)() = struct
       then a.var.v_fields <- Var_fields.set v_field_seen_pos true a.var.v_fields
       else a.var.v_fields <- Var_fields.set v_field_seen_neg true a.var.v_fields
 
-    let[@inline] make lit =
+    let[@inline] make st lit =
-      let var, negated = Var.make lit in
+      let var, negated = Var.make st lit in
       match negated with
       | Formula_intf.Negated -> var.na
       | Formula_intf.Same_sign -> var.pa
@@ -427,19 +441,29 @@ module McMake (E : Expr_intf.S)() = struct
       in
       Format.fprintf fmt "%a0" aux atoms
   end
+
+  module Term = struct
+    include E.Term
+    let pp = print
   end
 
+  module Formula = struct
+    include E.Formula
+    let pp = print
+  end
+end[@@inline]
+
 
 (* Solver types for pure SAT Solving *)
 (* ************************************************************************ *)
 
-module SatMake (E : Formula_intf.S)() = struct
+module SatMake (E : Formula_intf.S) = struct
   include McMake(struct
       include E
       module Term = E
       module Formula = E
-    end)(struct end)
+    end)
 
   let mcsat = false
-end
+end[@@inline]
 

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)():
+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)():
+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

@@ -32,6 +32,12 @@ module type S = sig
   val mcsat : bool
   (** TODO:deprecate. *)
 
+  type t
+  (** State for creating new terms, literals, clauses *)
+
+  (* TODO: add size hint *)
+  val create: unit -> t
+
   (** {2 Type definitions} *)
 
   type term
@@ -138,17 +144,19 @@ module type S = sig
     | E_var of var (**)
   (** Either a lit of a var *)
 
-  val nb_elt : unit -> int
+  val nb_elt : t -> int
-  val get_elt : int -> elt
+  val get_elt : t -> int -> elt
-  val iter_elt : (elt -> unit) -> unit
+  val iter_elt : t -> (elt -> unit) -> unit
   (** Read access to the vector of variables created *)
 
   (** {2 Variables, Literals & Clauses } *)
 
+  type state = t
+
   module Lit : sig
     type t = lit
     val term : t -> term
-    val make : term -> t
+    val make : state -> term -> t
     (** Returns the variable associated with the term *)
 
     val level : t -> int
@@ -167,7 +175,6 @@ module type S = sig
     type t = var
     val dummy : t
 
-
     val pos : t -> atom
     val neg : t -> atom
 
@@ -180,7 +187,7 @@ module type S = sig
     val weight : t -> float
     val set_weight : t -> float -> unit
 
-    val make : formula -> t * Formula_intf.negated
+    val make : state -> formula -> t * Formula_intf.negated
     (** Returns the variable linked with the given formula,
         and whether the atom associated with the formula
         is [var.pa] or [var.na] *)
@@ -207,7 +214,7 @@ module type S = sig
     val is_true : t -> bool
     val is_false : t -> bool
 
-    val make : formula -> t
+    val make : state -> formula -> t
     (** Returns the atom associated with the given formula *)
 
     val mark : t -> unit
@@ -274,5 +281,19 @@ module type S = sig
     (** Constructors and destructors *)
     val debug : t printer
   end
+
+  module Term : sig
+    type t = term
+    val equal : t -> t -> bool
+    val hash : t -> int
+    val pp : t printer
+  end
+
+  module Formula : sig
+    type t = formula
+    val equal : t -> t -> bool
+    val hash : t -> int
+    val pp : t printer
+  end
 end
 

src/main/main.ml

@@ -37,19 +37,21 @@ module Make
 
   let hyps = ref []
 
-  let check_model state =
+  let st = S.create()
+
+  let check_model sat =
     let check_clause c =
       let l = List.map (function a ->
           Log.debugf 99
-            (fun k -> k "Checking value of %a" S.St.Atom.debug (S.St.Atom.make a));
+            (fun k -> k "Checking value of %a" S.St.Formula.pp a);
-          state.Msat.eval a) c in
+          sat.Msat.eval a) c in
       List.exists (fun x -> x) l
     in
     let l = List.map check_clause !hyps in
     List.for_all (fun x -> x) l
 
-  let prove ~assumptions =
+  let prove ~assumptions () =
-    let res = S.solve ~assumptions () in
+    let res = S.solve st ~assumptions () in
     let t = Sys.time () in
     begin match res with
       | S.Sat state ->
@@ -78,15 +80,15 @@ module Make
     | Dolmen.Statement.Clause l ->
       let cnf = T.antecedent (Dolmen.Term.or_ l) in
       hyps := cnf @ !hyps;
-      S.assume cnf
+      S.assume st cnf
     | Dolmen.Statement.Consequent t ->
       let cnf = T.consequent t in
       hyps := cnf @ !hyps;
-      S.assume cnf
+      S.assume st cnf
     | Dolmen.Statement.Antecedent t ->
       let cnf = T.antecedent t in
       hyps := cnf @ !hyps;
-      S.assume cnf
+      S.assume st cnf
     | Dolmen.Statement.Pack [
         { Dolmen.Statement.descr = Dolmen.Statement.Push 1;_ };
         { Dolmen.Statement.descr = Dolmen.Statement.Antecedent f;_ };
@@ -94,9 +96,9 @@ module Make
         { Dolmen.Statement.descr = Dolmen.Statement.Pop 1;_ };
       ] ->
       let assumptions = T.assumptions f in
-      prove ~assumptions
+      prove ~assumptions ()
     | Dolmen.Statement.Prove ->
-      prove ~assumptions:[]
+      prove ~assumptions:[] ()
     | Dolmen.Statement.Set_info _
     | Dolmen.Statement.Set_logic _ -> ()
     | Dolmen.Statement.Exit -> exit 0
@@ -105,9 +107,9 @@ module Make
         Dolmen.Statement.print s
 end
 
-module Sat = Make(Minismt_sat.Make(struct end))(Minismt_sat.Type)
+module Sat = Make(Minismt_sat)(Minismt_sat.Type)
-module Smt = Make(Minismt_smt.Make(struct end))(Minismt_smt.Type)
+module Smt = Make(Minismt_smt)(Minismt_smt.Type)
-module Mcsat = Make(Minismt_mcsat.Make(struct end))(Minismt_smt.Type)
+module Mcsat = Make(Minismt_mcsat)(Minismt_smt.Type)
 
 let solver = ref (module Sat : S)
 let solver_list = [

src/mcsat/Minismt_mcsat.ml

@@ -4,10 +4,10 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make() =
+include
   Minismt.Mcsolver.Make(struct
     type proof = unit
     module Term = Minismt_smt.Expr.Term
     module Formula = Minismt_smt.Expr.Atom
-  end)(Plugin_mcsat)()
+  end)(Plugin_mcsat)
 

src/mcsat/Minismt_mcsat.mli

@@ -4,5 +4,5 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make() : Minismt.Solver.S with type St.formula = Minismt_smt.Expr.atom
+include Minismt.Solver.S with type St.formula = Minismt_smt.Expr.atom
 

src/sat/Minismt_sat.ml

@@ -6,6 +6,5 @@ Copyright 2016 Guillaume Bury
 module Expr = Expr_sat
 module Type = Type_sat
 
-module Make() =
+include Minismt.Solver.Make(Expr)(Minismt.Solver.DummyTheory(Expr))
-  Minismt.Solver.Make(Expr)(Minismt.Solver.DummyTheory(Expr))()
 

src/sat/Minismt_sat.mli

@@ -12,6 +12,6 @@ Copyright 2016 Guillaume Bury
 module Expr = Expr_sat
 module Type = Type_sat
 
-module Make() : Minismt.Solver.S with type St.formula = Expr.t
+include Minismt.Solver.S with type St.formula = Expr.t
 (** A functor that can generate as many solvers as needed. *)
 

src/smt/Minismt_smt.ml

@@ -9,5 +9,5 @@ module Type = Type_smt
 
 module Th = Minismt.Solver.DummyTheory(Expr.Atom)
 
-module Make() = Minismt.Solver.Make(Expr.Atom)(Th)()
+include Minismt.Solver.Make(Expr.Atom)(Th)
 

src/smt/Minismt_smt.mli

@@ -7,5 +7,5 @@ Copyright 2014 Simon Cruanes
 module Expr = Expr_smt
 module Type = Type_smt
 
-module Make() : Minismt.Solver.S with type St.formula = Expr_smt.atom
+include Minismt.Solver.S with type St.formula = Expr_smt.atom
 

src/solver/mcsolver.ml

@@ -10,10 +10,6 @@ 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)
-    () =
+    = Msat.Make (Make_mcsat_expr(E)) (Th)
-  Msat.Make
-    (Make_mcsat_expr(E)())
-    (Th)
-    ()
 
 

src/solver/mcsolver.mli

@@ -16,8 +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)
-    () :
+  : S with type St.term = E.Term.t
-  S with type St.term = E.Term.t
        and type St.formula = E.Formula.t
        and type St.proof = E.proof
 (** Functor to create a solver parametrised by the atomic formulas and a theory. *)

src/solver/solver.ml

@@ -76,10 +76,6 @@ end
 
 module Make (E : Formula_intf.S)
     (Th : Theory_intf.S with type formula = E.t and type proof = E.proof)
-    () =
+    = Msat.Make (Make_smt_expr(E)) (Plugin(E)(Th))
-  Msat.Make
-    (Make_smt_expr(E)(struct end))
-    (Plugin(E)(Th))
-    ()
 
 

src/solver/solver.mli

@@ -23,8 +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)
-    () :
+  : S with type St.formula = F.t
-  S with type St.formula = F.t
        and type St.proof = F.proof
 (** Functor to create a SMT Solver parametrised by the atomic
     formulas and a theory. *)

tests/test_api.ml

@@ -40,14 +40,18 @@ type solver_res =
 exception Incorrect_model
 
 module type BASIC_SOLVER = sig
-  val solve : ?assumptions:F.t list -> unit -> solver_res
+  type t
-  val assume : ?tag:int -> F.t list list -> unit
+  val create : unit -> t
+  val solve : t -> ?assumptions:F.t list -> unit -> solver_res
+  val assume : t -> ?tag:int -> F.t list list -> unit
 end
 
 let mk_solver (): (module BASIC_SOLVER) =
   let module S = struct
-    include Minismt_sat.Make(struct end)
+    include Minismt_sat
-    let solve ?assumptions ()= match solve ?assumptions() with
+    let create() = create()
+    let solve st ?assumptions () =
+      match solve st ?assumptions() with
       | Sat _ ->
         R_sat
       | Unsat us ->
@@ -86,13 +90,14 @@ module Test = struct
   let run (t:t): result =
   (* Interesting stuff happening *)
     let (module S: BASIC_SOLVER) = mk_solver () in
+    let st = S.create() in
     try
       List.iter
         (function
           | A_assume cs ->
-            S.assume cs
+            S.assume st cs
           | A_solve (assumptions, expect) ->
-            match S.solve ~assumptions (), expect with
+            match S.solve st ~assumptions (), expect with
               | R_sat, `Expect_sat
               | R_unsat, `Expect_unsat -> ()
               | R_unsat, `Expect_sat ->