sig
  val mk_sort : Z3.context -> Z3.Sort.sort -> Z3.Sort.sort
  val is_finite_set_sort : Z3.context -> Z3.Sort.sort -> bool
  val get_sort_basis : Z3.context -> Z3.Sort.sort -> Z3.Sort.sort
  val mk_empty : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_singleton : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_union : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_intersect :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_difference :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_member : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_size : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_subset : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_map : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_filter : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_range : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
end