sig
  type t
  val pp : Prop.t Pretty.printer
  val mk_true : Prop.t
  val mk_false : Prop.t
  val mk_var : Name.t -> Prop.t
  val mk_poslit : Atom.t -> Prop.t
  val mk_neglit : Atom.t -> Prop.t
  val mk_ite : Prop.t -> Prop.t -> Prop.t -> Prop.t
  val mk_conj : Prop.t list -> Prop.t
  val mk_disj : Prop.t list -> Prop.t
  val mk_iff : Prop.t -> Prop.t -> Prop.t
  val mk_neg : Prop.t -> Prop.t
  val mk_let : Name.t -> Prop.t -> Prop.t -> Prop.t
  val is_true : Prop.t -> bool
  val is_false : Prop.t -> bool
  val is_var : Prop.t -> bool
  val is_atom : Prop.t -> bool
  val is_ite : Prop.t -> bool
  val is_disj : Prop.t -> bool
  val is_iff : Prop.t -> bool
  val is_neg : Prop.t -> bool
  val is_let : Prop.t -> bool
  val d_var : Prop.t -> Name.t
  val d_atom : Prop.t -> Atom.t
  val d_disj : Prop.t -> Prop.t list
  val d_iff : Prop.t -> Prop.t * Prop.t
  val d_ite : Prop.t -> Prop.t * Prop.t * Prop.t
  val d_neg : Prop.t -> Prop.t
  val d_let : Prop.t -> Name.t * Prop.t * Prop.t
  val set_verbose : bool -> unit
  val set_assertion_frequency : int -> unit
  val set_remove_subsumed_clauses : bool -> unit
  val set_validate : bool -> unit
  val set_polarity_optimization : bool -> unit
  val set_clause_relevance : int -> unit
  val set_cleanup_period : int -> unit
  val set_num_refinements : int -> unit
  val statistics : bool Pervasives.ref
  val show_explanations : bool Pervasives.ref
  module Assignment :
    sig
      type t = { valuation : (Name.t * bool) list; literals : Atom.Set.t; } 
      val pp : Prop.Assignment.t Pretty.printer
    end
  val sat : Context.t -> Prop.t -> (Prop.Assignment.t * Context.t) option
end