sig
  module type S = Res_intf.S
  module Make :
    functor (St : Solver_types.S) ->
      sig
        module St :
          sig
            val mcsat : bool
            type term = St.term
            type formula = St.formula
            type proof = St.proof
            type seen = St.seen = Nope | Both | Positive | Negative
            type lit =
              St.lit = {
              lid : int;
              term : term;
              mutable l_level : int;
              mutable l_weight : float;
              mutable assigned : term option;
            }
            type var =
              St.var = {
              vid : int;
              pa : atom;
              na : atom;
              mutable used : int;
              mutable seen : seen;
              mutable v_level : int;
              mutable v_weight : float;
              mutable v_assignable : lit list option;
              mutable reason : reason option;
            }
            and atom =
              St.atom = {
              aid : int;
              var : var;
              neg : atom;
              lit : formula;
              mutable is_true : bool;
              mutable watched : clause Vec.t;
            }
            and clause =
              St.clause = {
              name : string;
              tag : int option;
              atoms : atom array;
              mutable cpremise : premise;
              mutable activity : float;
              mutable attached : bool;
              mutable visited : bool;
            }
            and reason = St.reason = Decision | Bcp of clause | Semantic
            and premise =
              St.premise =
                Hyp
              | Local
              | Lemma of proof
              | History of clause list
            type t = St.t = Lit of lit | Atom of atom
            val of_lit : lit -> t
            val of_atom : atom -> t
            type elt = St.elt = E_lit of lit | E_var of var
            val nb_elt : unit -> int
            val get_elt : int -> elt
            val iter_elt : (elt -> unit) -> unit
            val elt_of_lit : lit -> elt
            val elt_of_var : var -> elt
            val get_elt_id : elt -> int
            val get_elt_level : elt -> int
            val get_elt_weight : elt -> float
            val set_elt_level : elt -> int -> unit
            val set_elt_weight : elt -> float -> unit
            val dummy_var : var
            val dummy_atom : atom
            val dummy_clause : clause
            val add_term : term -> lit
            val add_atom : formula -> atom
            val make_boolean_var : formula -> var * Formula_intf.negated
            val empty_clause : clause
            val make_clause :
              ?tag:int -> string -> atom list -> premise -> clause
            val mark : atom -> unit
            val seen : atom -> bool
            val clear : var -> unit
            val fresh_name : unit -> string
            val fresh_lname : unit -> string
            val fresh_tname : unit -> string
            val fresh_hname : unit -> string
            val print_lit : Format.formatter -> lit -> unit
            val print_atom : Format.formatter -> atom -> unit
            val print_clause : Format.formatter -> clause -> unit
            val pp : Format.formatter -> t -> unit
            val pp_lit : Format.formatter -> lit -> unit
            val pp_atom : Format.formatter -> atom -> unit
            val pp_clause : Format.formatter -> clause -> unit
            val pp_dimacs : Format.formatter -> clause -> unit
            val pp_reason : Format.formatter -> int * reason option -> unit
          end
        exception Insuficient_hyps
        type atom = St.atom
        type lemma = St.proof
        type clause = St.clause
        type proof
        and proof_node = { conclusion : clause; step : step; }
        and step =
            Hypothesis
          | Assumption
          | Lemma of lemma
          | Duplicate of proof * atom list
          | Resolution of proof * proof * atom
        val to_list : clause -> atom list
        val merge : atom list -> atom list -> atom list
        val resolve : atom list -> atom list * atom list
        val prove : clause -> proof
        val prove_unsat : clause -> proof
        val prove_atom : atom -> proof option
        val parents : step -> proof list
        val is_leaf : step -> bool
        val expl : step -> string
        val expand : proof -> proof_node
        val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> 'a
        val unsat_core : proof -> clause list
        val check : proof -> unit
        val print_clause : Format.formatter -> clause -> unit
        module H :
          sig
            type key = clause
            type 'a t
            val create : int -> 'a t
            val clear : 'a t -> unit
            val reset : 'a t -> unit
            val copy : 'a t -> 'a t
            val add : 'a t -> key -> 'a -> unit
            val remove : 'a t -> key -> unit
            val find : 'a t -> key -> 'a
            val find_opt : 'a t -> key -> 'a option
            val find_all : 'a t -> key -> 'a list
            val replace : 'a t -> key -> 'a -> unit
            val mem : 'a t -> key -> bool
            val iter : (key -> 'a -> unit) -> 'a t -> unit
            val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
            val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
            val length : 'a t -> int
            val stats : 'a t -> Hashtbl.statistics
          end
      end
end