class Z3::SetExpr

# File lib/z3/expr/set_expr.rb, line 60
def Difference(a, b)
  a, b = coerce_to_same_set_sort(a, b)
  a.sort.new(LowLevel.mk_set_difference(a, b))
end

# File lib/z3/expr/set_expr.rb, line 55
def Intersection(*args)
  args = coerce_to_same_set_sort(*args)
  args[0].sort.new(LowLevel.mk_set_intersect(args))
end

# File lib/z3/expr/set_expr.rb, line 45
def Subset(a, b)
  a, b = coerce_to_same_set_sort(a, b)
  BoolSort.new.new(LowLevel.mk_set_subset(a, b))
end

# File lib/z3/expr/set_expr.rb, line 50
def Union(*args)
  args = coerce_to_same_set_sort(*args)
  args[0].sort.new(LowLevel.mk_set_union(args))
end

# File lib/z3/expr/set_expr.rb, line 39
def coerce_to_same_set_sort(*args)
  args = coerce_to_same_sort(*args)
  raise Z3::Exception, "Set value with same element sort expected" unless args[0].is_a?(SetExpr)
  args
end

# File lib/z3/expr/expr.rb, line 5
def initialize(_ast, sort)
  super(_ast)
  @sort = sort
  raise Z3::Exception, "Values must have AST kind numeral, app, or quantifier" unless [:numeral, :app, :quantifier].include?(ast_kind)
end

# File lib/z3/expr/set_expr.rb, line 17
def complement
  sort.new(LowLevel.mk_set_complement(self))
end

# File lib/z3/expr/set_expr.rb, line 29
def difference(other)
  SetExpr.Difference(self, other)
end

# File lib/z3/expr/set_expr.rb, line 5
def element_sort
  sort.element_sort
end

# File lib/z3/expr/set_expr.rb, line 33
def include?(element)
  element = element_sort.cast(element)
  BoolSort.new.new(LowLevel.mk_set_member(element, self))
end

# File lib/z3/expr/set_expr.rb, line 25
def intersection(other)
  SetExpr.Union(self, other)
end

# File lib/z3/expr/set_expr.rb, line 13
def is_subset_of(other)
  SetExpr.Subset(self, other)
end

# File lib/z3/expr/set_expr.rb, line 9
def is_superset_of(other)
  SetExpr.Subset(other, self)
end

# File lib/z3/expr/set_expr.rb, line 21
def union(other)
  SetExpr.Union(self, other)
end