Module SMT.Sets

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 : Sort.t -> Sort.t

Create set sort using given element sort.

val get_elem_sort : t -> Sort.t
val mk_empty : Sort.t -> t
val mk_singleton : t -> t
val mk_constant : Sort.t -> t list -> t
val mk_add : t -> t -> t
val mk_union : Sort.t -> t list -> t
val mk_inter : Sort.t -> t list -> t
val mk_diff : t -> t -> t
val mk_compl : t -> t
val mk_mem : t -> t -> t
val mk_subset : t -> t -> t
val mk_disjoint : t list -> t
val mk_eq_empty : t -> t
val mk_eq_singleton : t -> t -> t
val may_disjoint : t list -> bool