do not expose St in solver, but only expose a restricted API.

src/backend/Coq.ml

@@ -22,11 +22,12 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
                                 and type lemma := S.clause
                                 and type assumption := S.clause) = struct
 
-  module Atom = S.St.Atom
+  module Atom = S.Atom
-  module Clause = S.St.Clause
+  module Clause = S.Clause
-  module M = Map.Make(S.St.Atom)
+  module M = Map.Make(S.Atom)
+  module C_tbl = S.Clause.Tbl
 
-  let name = S.St.Clause.name
+  let name = Clause.name
 
   let clause_map c =
     let rec aux acc a i =
@@ -36,11 +37,11 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
         aux (M.add a.(i) name acc) a (i + 1)
       end
     in
-    aux M.empty c.S.St.atoms 0
+    aux M.empty (Clause.atoms c) 0
 
   let clause_iter m format fmt clause =
     let aux atom = Format.fprintf fmt format (M.find atom m) in
-    Array.iter aux clause.S.St.atoms
+    Array.iter aux (Clause.atoms clause)
 
   let elim_duplicate fmt goal hyp _ =
     (** Printing info comment in coq *)
@@ -59,27 +60,30 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
            if b == a then begin
              Format.fprintf fmt "@ (fun p =>@ %s%a)"
                (name h2) (fun fmt -> (Array.iter (fun c ->
-                   if c == a.S.St.neg then
+                   if Atom.equal c (Atom.neg a) then
                      Format.fprintf fmt "@ (fun np => np p)"
                    else
                      Format.fprintf fmt "@ %s" (M.find c m)))
-                 ) h2.S.St.atoms
+                 ) (Clause.atoms h2)
            end else
              Format.fprintf fmt "@ %s" (M.find b m)
-         )) h1.S.St.atoms
+         )) (Clause.atoms h1)
 
   let resolution fmt goal hyp1 hyp2 atom =
     let a = Atom.abs atom in
     let h1, h2 =
-      if Array.exists (Atom.equal a) hyp1.S.St.atoms then hyp1, hyp2
+      if Array.exists (Atom.equal a) (Clause.atoms hyp1) then hyp1, hyp2
-      else (assert (Array.exists (Atom.equal a) hyp2.S.St.atoms); hyp2, hyp1)
+      else (
+        assert (Array.exists (Atom.equal a) (Clause.atoms hyp2));
+        hyp2, hyp1
+      )
     in
     (** Print some debug info *)
     Format.fprintf fmt
       "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n"
       (name goal) (name h1) (name h2);
     (** Prove the goal: intro the axioms, then perform resolution *)
-    if Array.length goal.S.St.atoms = 0 then (
+    if Array.length (Clause.atoms goal) = 0 then (
       let m = M.empty in
       Format.fprintf fmt "exact @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) ();
       false
@@ -92,13 +96,13 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
 
   (* Count uses of hypotheses *)
   let incr_use h c =
-    let i = try S.H.find h c with Not_found -> 0 in
+    let i = try C_tbl.find h c with Not_found -> 0 in
-    S.H.add h c (i + 1)
+    C_tbl.add h c (i + 1)
 
   let decr_use h c =
-    let i = S.H.find h c - 1 in
+    let i = C_tbl.find h c - 1 in
     assert (i >= 0);
-    let () = S.H.add h c i in
+    let () = C_tbl.add h c i in
     i <= 0
 
   let clear fmt c =
@@ -136,7 +140,7 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
       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 h = C_tbl.create 128 in
     let aux () node =
       List.iter (fun p' -> incr_use h S.(conclusion p')) (S.parents node.S.step)
     in
@@ -157,13 +161,13 @@ end
 
 
 module Simple(S : Res.S)
-    (A : Arg with type hyp = S.St.formula list
+    (A : Arg with type hyp = S.formula list
               and type lemma := S.lemma
-              and type assumption := S.St.formula) =
+              and type assumption := S.formula) =
   Make(S)(struct
 
     (* Some helpers *)
-    let lit a = a.S.St.lit
+    let lit = S.Atom.lit
 
     let get_assumption c =
       match S.to_list c with
@@ -171,8 +175,8 @@ module Simple(S : Res.S)
       | _ -> assert false
 
     let get_lemma c =
-      match c.S.St.cpremise with
+      match S.expand (S.prove c) with
-      | S.St.Lemma p -> p
+      | {S.step=S.Lemma p; _} -> p
       | _ -> assert false
 
     let prove_hyp fmt name c =

src/backend/Coq.mli

@@ -40,8 +40,8 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
 (** Base functor to output Coq proofs *)
 
 
-module Simple(S : Res.S)(A : Arg with type hyp = S.St.formula list
+module Simple(S : Res.S)(A : Arg with type hyp = S.formula list
                                   and type lemma := S.lemma
-                                  and type assumption := S.St.formula) : S with type t := S.proof
+                                  and type assumption := S.formula) : S with type t := S.proof
 (** Simple functo to output Coq proofs *)
 

src/backend/Dedukti.ml

@@ -18,22 +18,24 @@ module type Arg = sig
   val context : Format.formatter -> proof -> unit
 end
 
-module Make(S : Res.S)(A : Arg with type formula := S.St.formula and type lemma := S.lemma and type proof := S.proof) = struct
+module Make(S : Res.S)(A : Arg with type formula := S.formula
+                                and type lemma := S.lemma
+                                and type proof := S.proof) = struct
 
   let pp_nl fmt = Format.fprintf fmt "@\n"
   let fprintf fmt format = Format.kfprintf pp_nl fmt format
 
-  let _clause_name c = S.St.(c.name)
+  let _clause_name = S.Clause.name
 
   let _pp_clause fmt c =
     let rec aux fmt = function
       | [] -> ()
       | a :: r ->
         let f, pos =
-          if S.St.(a.var.pa == a) then
+          if S.Atom.is_pos a then
-            S.St.(a.lit), true
+            S.Atom.lit a, true
           else
-            S.St.(a.neg.lit), false
+            S.Atom.lit (S.Atom.neg a), false
         in
         fprintf fmt "%s _b %a ->@ %a"
           (if pos then "_pos" else "_neg") A.print f aux r

src/backend/Dedukti.mli

@@ -27,7 +27,7 @@ end
 module Make :
   functor(S : Res.S) ->
   functor(A : Arg
-          with type formula := S.St.formula
+          with type formula := S.formula
            and type lemma := S.lemma
            and type proof := S.proof) ->
     S with type t := S.proof

src/backend/Dot.ml

@@ -31,8 +31,8 @@ module type Arg = sig
 end
 
 module Default(S : Res.S) = struct
-  module Atom = S.St.Atom
+  module Atom = S.Atom
-  module Clause = S.St.Clause
+  module Clause = S.Clause
 
   let print_atom = Atom.pp
 
@@ -55,8 +55,8 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
                                 and type hyp := S.clause
                                 and type lemma := S.clause
                                 and type assumption := S.clause) = struct
-  module Atom = S.St.Atom
+  module Atom = S.Atom
-  module Clause = S.St.Clause
+  module Clause = S.Clause
 
   let node_id n = Clause.name n.S.conclusion
 
@@ -148,13 +148,13 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
 end
 
 module Simple(S : Res.S)
-    (A : Arg with type atom := S.St.formula
+    (A : Arg with type atom := S.formula
-              and type hyp = S.St.formula list
+              and type hyp = S.formula list
               and type lemma := S.lemma
-              and type assumption = S.St.formula) =
+              and type assumption = S.formula) =
   Make(S)(struct
-    module Atom = S.St.Atom
+    module Atom = S.Atom
-    module Clause = S.St.Clause
+    module Clause = S.Clause
 
     (* Some helpers *)
     let lit = Atom.lit
@@ -165,8 +165,8 @@ module Simple(S : Res.S)
       | _ -> assert false
 
     let get_lemma c =
-      match Clause.premise c with
+      match S.expand (S.prove c) with
-      | S.St.Lemma p -> p
+      | {S.step=S.Lemma p;_} -> p
       | _ -> assert false
 
     (* Actual functions *)

src/backend/Dot.mli

@@ -61,10 +61,10 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
                                 and type assumption := S.clause) : S with type t := S.proof
 (** Functor for making a module to export proofs to the DOT format. *)
 
-module Simple(S : Res.S)(A : Arg with type atom := S.St.formula
+module Simple(S : Res.S)(A : Arg with type atom := S.formula
-                                  and type hyp = S.St.formula list
+                                  and type hyp = S.formula list
                                   and type lemma := S.lemma
-                                  and type assumption = S.St.formula) : S with type t := S.proof
+                                  and type assumption = S.formula) : S with type t := S.proof
 (** Functor for making a module to export proofs to the DOT format.
     The substitution of the hyp type is non-destructive due to a restriction
     of destructive substitutions on earlier versions of ocaml. *)

src/core/Internal.ml

@@ -228,7 +228,7 @@ module Make
     let l = Lit.make st.st t in
     insert_var_order st (E_lit l)
 
-  let new_atom st p =
+  let new_atom st (p:formula) : unit =
     let a = mk_atom st p in
     insert_var_order st (E_var a.var)
 
@@ -294,7 +294,7 @@ module Make
      literals (which are the first two lits of the clause) are appropriate.
      Indeed, it is better to watch true literals, and then unassigned literals.
      Watching false literals should be a last resort, and come with constraints
-     (see add_clause).
+     (see {!add_clause}).
   *)
   exception Trivial
 

src/core/Internal.mli

@@ -1,122 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** mSAT core
-
-    This is the core of msat, containing the code doing the actual solving.
-    This module is based on mini-sat, and as such the solver heavily uses mutation,
-    which makes using it direclty kinda tricky (some exceptions can be raised
-    at surprising times, mutating is dangerous for maintaining invariants, etc...).
-*)
-
-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)
-: sig
-  (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
-
-  (** {2 Solving facilities} *)
-
-  exception Unsat
-  exception UndecidedLit
-
-  type t
-  (** Solver *)
-
-  val create : ?size:[`Tiny|`Small|`Big] -> ?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 : 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 : 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 : 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 : t -> unit
-  (** Create a decision level for local assumptions.
-      @raise Unsat if a conflict is detected in the current state. *)
-
-  val pop : t -> unit
-  (** Pop a decision level for local assumptions. *)
-
-  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 : 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 : 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 : t -> (St.term * St.term) list
-  (** Returns the model found if the formula is satisfiable. *)
-
-  val check : t -> bool
-  (** Check the satisfiability of the current model. Only has meaning
-      if the solver finished proof search and has returned [Sat]. *)
-
-  (** {2 Proofs and Models} *)
-
-  module Proof : Res.S with module St = St
-
-  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 : 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. *)
-
-  (** {2 Internal data}
-      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 : t -> St.trail_elt Vec.t
-  (** Returns the current trail.
-      *DO NOT MUTATE* *)
-
-  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 : 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 : t -> St.clause Vec.t
-  (** Returns the history of learnt clauses, with no guarantees on order.
-      *DO NOT MUTATE* *)
-
-end
-

src/core/Res.ml

@@ -5,12 +5,13 @@ Copyright 2014 Simon Cruanes
 *)
 
 module type S = Res_intf.S
+module type FULL = Res_intf.FULL
 
 module Make(St : Solver_types.S) = struct
 
   module St = St
 
-  (* Type definitions *)
+  type formula = St.formula
   type lemma = St.proof
   type clause = St.clause
   type atom = St.atom
@@ -27,7 +28,8 @@ module Make(St : Solver_types.S) = struct
   let equal_atoms a b = St.(a.aid) = St.(b.aid)
   let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
 
-  let print_clause = St.Clause.pp
+  module Clause = St.Clause
+  module Atom = St.Atom
 
   let merge = List.merge compare_atoms
 
@@ -105,7 +107,7 @@ module Make(St : Solver_types.S) = struct
     in
     aux (c, d)
 
-  let prove conclusion =
+  let[@inline] prove conclusion =
     assert St.(conclusion.cpremise <> History []);
     conclusion
 
@@ -259,13 +261,7 @@ module Make(St : Solver_types.S) = struct
     List.iter (fun c -> c.St.visited <- false) tmp;
     res
 
-  (* Iter on proofs *)
+  module Tbl = Clause.Tbl
-  module H = Hashtbl.Make(struct
-      type t = clause
-      let hash cl =
-        Array.fold_left (fun i a -> Hashtbl.hash St.(a.aid, i)) 0 cl.St.atoms
-      let equal = (==)
-    end)
 
   type task =
     | Enter of proof
@@ -277,10 +273,10 @@ module Make(St : Solver_types.S) = struct
     match spop s with
     | None -> acc
     | Some (Leaving c) ->
-      H.add h c true;
+      Tbl.add h c true;
       fold_aux s h f (f acc (expand c))
     | Some (Enter c) ->
-      if not (H.mem h c) then begin
+      if not (Tbl.mem h c) then begin
         Stack.push (Leaving c) s;
         let node = expand c in
         begin match node.step with
@@ -295,7 +291,7 @@ module Make(St : Solver_types.S) = struct
       fold_aux s h f acc
 
   let fold f acc p =
-    let h = H.create 42 in
+    let h = Tbl.create 42 in
     let s = Stack.create () in
     Stack.push (Enter p) s;
     fold_aux s h f acc

src/core/Res.mli

@@ -12,6 +12,8 @@ Copyright 2014 Simon Cruanes
 module type S = Res_intf.S
 (** Interface for a module manipulating resolution proofs. *)
 
-module Make : functor (St : Solver_types.S) -> S with module St = St
+module type FULL = Res_intf.FULL
+
+module Make : functor (St : Solver_types.S) -> FULL with module St = St
 (** Functor to create a module building proofs from a sat-solver unsat trace. *)
 

src/core/Res_intf.ml

@@ -6,25 +6,26 @@ Copyright 2014 Simon Cruanes
 
 (** Interface for proofs *)
 
+type 'a printer = Format.formatter -> 'a -> unit
+
 module type S = sig
   (** Signature for a module handling proof by resolution from sat solving traces *)
 
-  module St : Solver_types.S
-  (** Module defining atom and clauses *)
-
   (** {3 Type declarations} *)
 
   exception Insuficient_hyps
   (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *)
 
-  type atom = St.atom
+  type formula
-  type lemma = St.proof
+  type atom
-  type clause = St.clause
+  type lemma
+  type clause
   (** Abstract types for atoms, clauses and theory-specific lemmas *)
 
   type proof
   (** Lazy type for proof trees. Proofs are persistent objects, and can be
       extended to proof nodes using functions defined later. *)
+
   and proof_node = {
     conclusion : clause;  (** The conclusion of the proof *)
     step : step;          (** The reasoning step used to prove the conclusion *)
@@ -45,7 +46,6 @@ module type S = sig
         of the two given proofs. The atom on which to perform the resolution is also given. *)
   (** The type of reasoning steps allowed in a proof. *)
 
-
   (** {3 Resolution helpers} *)
 
   val to_list : clause -> atom list
@@ -73,7 +73,6 @@ module type S = sig
   val prove_atom : atom -> proof option
   (** Given an atom [a], returns a proof of the clause [\[a\]] if [a] is true at level 0 *)
 
-
   (** {3 Proof Nodes} *)
 
   val is_leaf : step -> bool
@@ -103,25 +102,46 @@ module type S = sig
       [f] on a proof node happens after the execution on the parents of the nodes. *)
 
   val unsat_core : proof -> clause list
-  (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof.
+  (** Returns the unsat_core of the given proof, i.e the lists of conclusions
-      More efficient than using the [fold] function since it has access to the internal representation of proofs *)
+      of all leafs of the proof.
-
+      More efficient than using the [fold] function since it has
+      access to the internal representation of proofs *)
 
   (** {3 Misc} *)
 
   val check : proof -> unit
   (** Check the contents of a proof. Mainly for internal use *)
 
-  val print_clause : Format.formatter -> clause -> unit
+  module Clause : sig
+    type t = clause
+    val name : t -> string
+    val atoms : t -> atom array
+    val pp : t printer
     (** A nice looking printer for clauses, which sort the atoms before printing. *)
 
-
+    module Tbl : Hashtbl.S with type key = t
-  (** {3 Unsafe} *)
+  end
-
+
-  module H : Hashtbl.S with type key = clause
+  module Atom : sig
-  (** Hashtable over proofs. Uses the details of the internal representation
+    type t = atom
-      to achieve the best performances, however hashtables from this module
+    val is_pos : t -> bool
-      become invalid when solving is restarted, so they should only be live
+    val neg : t -> t
-      during inspection of a single proof. *)
+    val abs : t -> t
-
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val lit : t -> formula
+    val pp : t printer
+  end
+
+  module Tbl : Hashtbl.S with type key = proof
+end
+
+module type FULL = sig
+  module St : Solver_types.S
+  (** Module defining atom and clauses *)
+
+  include S with type atom = St.atom
+             and type lemma = St.proof
+             and type clause = St.clause
+             and type formula = St.formula
 end

src/core/Solver.ml

@@ -23,11 +23,15 @@ module Make
 
   exception UndecidedLit = S.UndecidedLit
 
+  type formula = St.formula
+  type term = St.term
   type atom = St.formula
+  type clause = St.clause
 
   type t = S.t
+  type solver = t
 
-  let create = S.create
+  let[@inline] create ?size () = S.create ?size ()
 
   (* Result type *)
   type res =
@@ -78,6 +82,8 @@ module Make
   (* Wrappers around internal functions*)
   let assume = S.assume
 
+  let add_clause = S.add_clause
+
   let solve (st:t) ?(assumptions=[]) () =
     try
       S.pop st; (* FIXME: what?! *)
@@ -106,4 +112,17 @@ module Make
     let history = S.history st in
     let local = S.temp st in
     {hyps; history; local}
+
+  module Clause = struct
+    include St.Clause
+
+    let atoms c = St.Clause.atoms c |> Array.map (fun a -> a.St.lit)
+
+    let make st ?tag l =
+      let l = List.map (S.mk_atom st) l in
+      St.Clause.make ?tag l St.Hyp
+  end
+
+  module Formula = St.Formula
+  module Term = St.Term
 end

src/core/Solver.mli

@@ -18,7 +18,10 @@ 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 type term = St.term
+       and type formula = St.formula
+       and type clause = St.clause
+       and type Proof.lemma = St.proof
 (** Functor to make a safe external interface. *)
 
 

src/core/Solver_intf.ml

@@ -45,6 +45,8 @@ type 'clause export = {
 }
 (** Export internal state *)
 
+type 'a printer = Format.formatter -> 'a -> unit
+
 (** The external interface implemented by safe solvers, such as the one
     created by the {!Solver.Make} and {!Mcsolver.Make} functors. *)
 module type S = sig
@@ -52,30 +54,29 @@ module type S = sig
       These are the internal modules used, you should probably not use them
       if you're not familiar with the internals of mSAT. *)
 
-  (* TODO: replace {!St} with explicit modules (Expr, Var, Lit, Elt,...)
+  type term (** user terms *)
-     with carefully picked interfaces *)
-  module St : Solver_types.S
-  (** WARNING: Very dangerous module that expose the internal representation used
-      by the solver. *)
 
-  module Proof : Res.S with module St = St
+  type formula (** user formulas *)
+
+  type clause
+
+  module Proof : Res.S with type clause = clause
   (** A module to manipulate proofs. *)
 
   type t
   (** Main solver type, containing all state *)
 
-  val create : ?size:[`Tiny|`Small|`Big] -> ?st:St.t -> unit -> t
+  val create : ?size:[`Tiny|`Small|`Big] -> unit -> t
   (** Create new solver *)
-  (* TODO: add size hint, callbacks, etc. *)
 
   (** {2 Types} *)
 
-  type atom = St.formula
+  type atom = formula
   (** The type of atoms given by the module argument for formulas *)
 
   type res =
-    | Sat of (St.term,St.formula) sat_state         (** Returned when the solver reaches SAT *)
+    | Sat of (term,formula) sat_state         (** Returned when the solver reaches SAT *)
-    | Unsat of (St.clause,Proof.proof) unsat_state  (** Returned when the solver reaches UNSAT *)
+    | Unsat of (clause,Proof.proof) unsat_state  (** Returned when the solver reaches UNSAT *)
   (** Result type for the solver *)
 
   exception UndecidedLit
@@ -88,10 +89,13 @@ module type S = sig
   (** Add the list of clauses to the current set of assumptions.
       Modifies the sat solver state in place. *)
 
+  val add_clause : t -> clause -> unit
+  (** Lower level addition of clauses *)
+
   val solve : t -> ?assumptions:atom list -> unit -> res
   (** Try and solves the current set of assumptions. *)
 
-  val new_lit : t -> St.term -> unit
+  val new_lit : t -> 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. *)
@@ -101,16 +105,42 @@ module type S = sig
       This formula will be decided on at some point during solving,
       wether it appears in clauses or not. *)
 
-  val unsat_core : Proof.proof -> St.clause list
+  val unsat_core : Proof.proof -> clause list
   (** Returns the unsat core of a given proof. *)
 
   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
+  val get_tag : clause -> int option
   (** Recover tag from a clause, if any *)
 
-  val export : t -> St.clause export
+  val export : t -> clause export
+
+  (** {2 Re-export some functions} *)
+
+  type solver = t
+
+  module Clause : sig
+    type t = clause
+
+    val atoms : t -> atom array
+    val tag : t -> int option
+    val equal : t -> t -> bool
+
+    val make : solver -> ?tag:int -> atom list -> t
+
+    val pp : t printer
+  end
+
+  module Formula : sig
+    type t = formula
+    val pp : t printer
+  end
+
+  module Term : sig
+    type t = term
+    val pp : t printer
+  end
 end
 

src/core/Solver_types.ml

@@ -283,6 +283,7 @@ module McMake (E : Expr_intf.S) = struct
     let[@inline] abs a = a.var.pa
     let[@inline] lit a = a.lit
     let[@inline] equal a b = a == b
+    let[@inline] is_pos a = a == abs a
     let[@inline] compare a b = Pervasives.compare a.aid b.aid
     let[@inline] reason a = Var.reason a.var
     let[@inline] id a = a.aid
@@ -408,8 +409,10 @@ module McMake (E : Expr_intf.S) = struct
 
     let empty = make [] (History [])
     let name = name_of_clause
+    let[@inline] equal c1 c2 = c1==c2
     let[@inline] atoms c = c.atoms
     let[@inline] tag c = c.tag
+    let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.aid, i)) 0 cl.atoms
 
     let[@inline] premise c = c.cpremise
     let[@inline] set_premise c p = c.cpremise <- p
@@ -423,6 +426,12 @@ module McMake (E : Expr_intf.S) = struct
     let[@inline] activity c = c.activity
     let[@inline] set_activity c w = c.activity <- w
 
+    module Tbl = Hashtbl.Make(struct
+        type t = clause
+        let hash = hash
+        let equal = equal
+      end)
+
     let pp fmt c =
       Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms
 

src/core/Solver_types_intf.ml

@@ -210,6 +210,7 @@ module type S = sig
     val abs : t -> t (** positive atom *)
     val neg : t -> t
     val id : t -> int
+    val is_pos : t -> bool (* positive atom? *)
     val is_true : t -> bool
     val is_false : t -> bool
 
@@ -249,6 +250,8 @@ module type S = sig
     val dummy : t
 
     val name : t -> string
+    val equal : t -> t -> bool
+    val hash : t -> int
     val atoms : t -> Atom.t array
     val tag : t -> int option
     val premise : t -> premise
@@ -270,6 +273,8 @@ module type S = sig
     val pp : t printer
     val pp_dimacs : t printer
     val debug : t printer
+
+    module Tbl : Hashtbl.S with type key = t
   end
 
   module Trail_elt : sig

src/main/main.ml

@@ -43,7 +43,7 @@ module Make
     let check_clause c =
       let l = List.map (function a ->
           Log.debugf 99
-            (fun k -> k "Checking value of %a" S.St.Formula.pp a);
+            (fun k -> k "Checking value of %a" S.Formula.pp a);
           sat.Msat.eval a) c in
       List.exists (fun x -> x) l
     in

src/mcsat/Minismt_mcsat.mli

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

src/sat/Minismt_sat.mli

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

src/smt/Minismt_smt.mli

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

src/solver/mcsolver.mli

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

src/solver/solver.mli

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