sig
  type var = {
    vid : int;
    pa : Solver_types.atom;
    na : Solver_types.atom;
    mutable weight : float;
    mutable seen : bool;
    mutable level : int;
    mutable reason : Solver_types.reason;
    mutable vpremise : Solver_types.premise;
  }
  and atom = {
    var : Solver_types.var;
    lit : Literal.LT.t;
    neg : Solver_types.atom;
    mutable watched : Solver_types.clause Vec.t;
    mutable is_true : bool;
    aid : int;
  }
  and clause = {
    name : string;
    mutable atoms : Solver_types.atom Vec.t;
    mutable activity : float;
    mutable removed : bool;
    learnt : bool;
    cpremise : Solver_types.premise;
  }
  and reason = Solver_types.clause option
  and premise = Solver_types.clause list
  val cpt_mk_var : int Pervasives.ref
  val ma : Solver_types.var Literal.LT.Map.t Pervasives.ref
  val dummy_var : Solver_types.var
  val dummy_atom : Solver_types.atom
  val dummy_clause : Solver_types.clause
  val make_var : Literal.LT.t -> Solver_types.var * bool
  val add_atom : Literal.LT.t -> Solver_types.atom
  val make_clause :
    string ->
    Solver_types.atom list ->
    int -> bool -> Solver_types.premise -> Solver_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 * Solver_types.var list
  val clear : unit -> unit
  module Debug :
    sig
      val atom : Format.formatter -> Solver_types.atom -> unit
      val clause : Format.formatter -> Solver_types.clause -> unit
    end
end