sig
  val d_interp : Term.t -> Sym.propset * Term.t list
  val is_empty : Term.t -> bool
  val is_full : Term.t -> bool
  val is_diseq : Term.t -> Term.t -> bool
  val is_const : Term.t -> bool
  val mk_empty : unit -> Term.t
  val mk_full : unit -> Term.t
  val mk_ite : Term.t -> Term.t -> Term.t -> Term.t
  val mk_inter : Term.t -> Term.t -> Term.t
  val mk_union : Term.t -> Term.t -> Term.t
  val mk_compl : Term.t -> Term.t
  val sigma : Sym.propset -> Term.t list -> Term.t
  val map : (Term.t -> Term.t) -> Term.t -> Term.t
  val solve : Term.Equal.t -> Term.Equal.t list
end