sig
  val mcsat : bool
  type term
  type formula
  type proof
  type seen = Nope | Both | Positive | Negative
  type lit = {
    lid : int;
    term : Solver_types_intf.S.term;
    mutable l_level : int;
    mutable l_weight : float;
    mutable assigned : Solver_types_intf.S.term option;
  }
  type var = {
    vid : int;
    pa : Solver_types_intf.S.atom;
    na : Solver_types_intf.S.atom;
    mutable used : int;
    mutable seen : Solver_types_intf.S.seen;
    mutable v_level : int;
    mutable v_weight : float;
    mutable v_assignable : Solver_types_intf.S.lit list option;
    mutable reason : Solver_types_intf.S.reason option;
  }
  and atom = {
    aid : int;
    var : Solver_types_intf.S.var;
    neg : Solver_types_intf.S.atom;
    lit : Solver_types_intf.S.formula;
    mutable is_true : bool;
    mutable watched : Solver_types_intf.S.clause Vec.t;
  }
  and clause = {
    name : string;
    tag : int option;
    atoms : Solver_types_intf.S.atom array;
    mutable cpremise : Solver_types_intf.S.premise;
    mutable activity : float;
    mutable attached : bool;
    mutable visited : bool;
  }
  and reason = Decision | Bcp of Solver_types_intf.S.clause | Semantic
  and premise =
      Hyp
    | Local
    | Lemma of Solver_types_intf.S.proof
    | History of Solver_types_intf.S.clause list
  type t = Lit of Solver_types_intf.S.lit | Atom of Solver_types_intf.S.atom
  val of_lit : Solver_types_intf.S.lit -> Solver_types_intf.S.t
  val of_atom : Solver_types_intf.S.atom -> Solver_types_intf.S.t
  type elt =
      E_lit of Solver_types_intf.S.lit
    | E_var of Solver_types_intf.S.var
  val nb_elt : unit -> int
  val get_elt : int -> Solver_types_intf.S.elt
  val iter_elt : (Solver_types_intf.S.elt -> unit) -> unit
  val elt_of_lit : Solver_types_intf.S.lit -> Solver_types_intf.S.elt
  val elt_of_var : Solver_types_intf.S.var -> Solver_types_intf.S.elt
  val get_elt_id : Solver_types_intf.S.elt -> int
  val get_elt_level : Solver_types_intf.S.elt -> int
  val get_elt_weight : Solver_types_intf.S.elt -> float
  val set_elt_level : Solver_types_intf.S.elt -> int -> unit
  val set_elt_weight : Solver_types_intf.S.elt -> float -> unit
  val dummy_var : Solver_types_intf.S.var
  val dummy_atom : Solver_types_intf.S.atom
  val dummy_clause : Solver_types_intf.S.clause
  val add_term : Solver_types_intf.S.term -> Solver_types_intf.S.lit
  val add_atom : Solver_types_intf.S.formula -> Solver_types_intf.S.atom
  val make_boolean_var :
    Solver_types_intf.S.formula ->
    Solver_types_intf.S.var * Formula_intf.negated
  val empty_clause : Solver_types_intf.S.clause
  val make_clause :
    ?tag:int ->
    string ->
    Solver_types_intf.S.atom list ->
    Solver_types_intf.S.premise -> Solver_types_intf.S.clause
  val mark : Solver_types_intf.S.atom -> unit
  val seen : Solver_types_intf.S.atom -> bool
  val clear : Solver_types_intf.S.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 -> Solver_types_intf.S.lit -> unit
  val print_atom : Format.formatter -> Solver_types_intf.S.atom -> unit
  val print_clause : Format.formatter -> Solver_types_intf.S.clause -> unit
  val pp : Format.formatter -> Solver_types_intf.S.t -> unit
  val pp_lit : Format.formatter -> Solver_types_intf.S.lit -> unit
  val pp_atom : Format.formatter -> Solver_types_intf.S.atom -> unit
  val pp_clause : Format.formatter -> Solver_types_intf.S.clause -> unit
  val pp_dimacs : Format.formatter -> Solver_types_intf.S.clause -> unit
  val pp_reason :
    Format.formatter -> int * Solver_types_intf.S.reason option -> unit
end