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