sig
  module type S = Solver_types_intf.S
  module McMake :
    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
  module SatMake :
    functor (E : Formula_intf.S) (Dummy : sig  end) ->
      sig
        val mcsat : bool
        type term = E.t
        type formula = E.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
end