sig
  type ident = {
    iname : Hstring.t;
    mask : int;
    mutable ivalues : (Enumsolver_types.atom * int) Vec.t;
    ivars : Enumsolver_types.var Vec.t;
  }
  and var = {
    vid : int;
    ident : Enumsolver_types.ident;
    pa : Enumsolver_types.atom;
    na : Enumsolver_types.atom;
    mutable weight : float;
    mutable seen : bool;
    mutable level : int;
    mutable reason : Enumsolver_types.reason;
    mutable vpremise : Enumsolver_types.premise;
  }
  and atom = {
    aid : int;
    var : Enumsolver_types.var;
    value : int;
    neg : Enumsolver_types.atom;
    mutable is_true : bool;
    mutable watched : Enumsolver_types.clause Vec.t;
  }
  and clause = {
    name : string;
    mutable atoms : Enumsolver_types.atom Vec.t;
    mutable activity : float;
    mutable removed : bool;
    learnt : bool;
    cpremise : Enumsolver_types.premise;
  }
  and reason = Enumsolver_types.clause option
  and premise = Enumsolver_types.clause list
  val cpt_mk_var : int Pervasives.ref
  val dummy_var : Enumsolver_types.var
  val dummy_atom : Enumsolver_types.atom
  val dummy_clause : Enumsolver_types.clause
  val add_atom :
    (Enumsolver_types.atom * Enumsolver_types.clause * int) list
    Pervasives.ref -> Hstring.t * int * int -> Enumsolver_types.atom
  val make_clause :
    string ->
    Enumsolver_types.atom list ->
    int -> bool -> Enumsolver_types.premise -> Enumsolver_types.clause
  val fresh_name : unit -> string
  val fresh_lname : unit -> string
  val fresh_dname : unit -> string
  val to_float : int -> float
  val to_int : float -> int
  val made_vars_info : unit -> int * Enumsolver_types.atom list
  val clear : unit -> unit
  val same_ident : Enumsolver_types.atom -> Enumsolver_types.atom -> bool
  val is_bottom : Enumsolver_types.atom -> bool
  val enqueue_ident :
    Enumsolver_types.atom ->
    (Enumsolver_types.atom * Enumsolver_types.clause * int) list
  val pop_ident : Enumsolver_types.atom -> unit
  val check_bottom_clause :
    Enumsolver_types.atom -> Enumsolver_types.clause option
  module Debug :
    sig
      val atom : Format.formatter -> Enumsolver_types.atom -> unit
      val atoms_list : Format.formatter -> Enumsolver_types.atom list -> unit
      val clause : Format.formatter -> Enumsolver_types.clause -> unit
    end
  val is_attached : Enumsolver_types.clause -> bool
end