functor (E : Expr_intf.S) (Dummy : sig  end) ->
  sig
    val mcsat : bool
    type term = E.Term.t
    type formula = E.Formula.t
    type proof = E.proof
    type seen = Nope | Both | Positive | Negative
    type lit = {
      lid : int;
      term : term;
      mutable l_level : int;
      mutable l_weight : float;
      mutable assigned : term option;
    }
    type 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 = {
      aid : int;
      var : var;
      neg : atom;
      lit : formula;
      mutable is_true : bool;
      mutable watched : clause Vec.t;
    }
    and clause = {
      name : string;
      tag : int option;
      atoms : atom array;
      mutable cpremise : premise;
      mutable activity : float;
      mutable attached : bool;
      mutable visited : bool;
    }
    and reason = Decision | Bcp of clause | Semantic
    and premise = Hyp | Local | Lemma of proof | History of clause list
    type t = Lit of lit | Atom of atom
    val of_lit : lit -> t
    val of_atom : atom -> t
    type 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