Module Z3.Set

module Set: sig .. end

Functions to manipulate Set expressions

val mk_sort : context -> Sort.sort -> Sort.sort

Create a set type.

val is_union : Expr.expr -> bool

Indicates whether the term is set union

val is_intersect : Expr.expr -> bool

Indicates whether the term is set intersection

val is_difference : Expr.expr -> bool

Indicates whether the term is set difference

val is_complement : Expr.expr -> bool

Indicates whether the term is set complement

val is_subset : Expr.expr -> bool

Indicates whether the term is set subset

val mk_empty : context -> Sort.sort -> Expr.expr

Create an empty set.

val mk_full : context -> Sort.sort -> Expr.expr

Create the full set.

val mk_set_add : context -> Expr.expr -> Expr.expr -> Expr.expr

Add an element to the set.

val mk_del : context -> Expr.expr -> Expr.expr -> Expr.expr

Remove an element from a set.

val mk_union : context -> Expr.expr list -> Expr.expr

Take the union of a list of sets.

val mk_intersection : context -> Expr.expr list -> Expr.expr

Take the intersection of a list of sets.

val mk_difference : context -> Expr.expr -> Expr.expr -> Expr.expr

Take the difference between two sets.

val mk_complement : context -> Expr.expr -> Expr.expr

Take the complement of a set.

val mk_membership : context -> Expr.expr -> Expr.expr -> Expr.expr

Check for set membership.

val mk_subset : context -> Expr.expr -> Expr.expr -> Expr.expr

Check for subsetness of sets.