sig
  val mk_sort : Z3.context -> Z3.Sort.sort -> Z3.Sort.sort
  val is_union : Z3.Expr.expr -> bool
  val is_intersect : Z3.Expr.expr -> bool
  val is_difference : Z3.Expr.expr -> bool
  val is_complement : Z3.Expr.expr -> bool
  val is_subset : Z3.Expr.expr -> bool
  val mk_empty : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_full : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_set_add : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_del : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_union : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_intersection : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_difference :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_complement : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_membership :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_subset : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
end