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