SMT.Enumeration
include SMT_sig.EQUALITY with type t := t
val mk_eq : t list -> t
val mk_distinct : t list -> t
val mk_var : string -> Sort.t -> t
val mk_fresh_var : string -> Sort.t -> t
val mk_sort : string -> string list -> Sort.t
val mk_const : Sort.t -> string -> t
val get_constants : Sort.t -> Constant.t list
val get_constants_terms : Sort.t -> t list