sig
  module St : Solver_types.S
  module Proof :
    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
  type atom = St.formula
  type res =
      Sat of (St.term, St.formula) Solver_intf.sat_state
    | Unsat of (St.clause, Solver_intf.S.Proof.proof) Solver_intf.unsat_state
  exception UndecidedLit
  val assume : ?tag:int -> Solver_intf.S.atom list list -> unit
  val solve :
    ?assumptions:Solver_intf.S.atom list -> unit -> Solver_intf.S.res
  val new_lit : St.term -> unit
  val new_atom : Solver_intf.S.atom -> unit
  val unsat_core : Solver_intf.S.Proof.proof -> St.clause list
  val true_at_level0 : Solver_intf.S.atom -> bool
  val get_tag : St.clause -> int option
  val export_dimacs : Format.formatter -> unit -> unit
  val export_icnf : Format.formatter -> unit -> unit
end