class Z3::SetExpr

Public Class Methods

Difference(a, b) click to toggle source
# 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
Intersection(*args) click to toggle source
# 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
Subset(a, b) click to toggle source
# 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
Union(*args) click to toggle source
# 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
coerce_to_same_set_sort(*args) click to toggle source
# 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
new(_ast, sort) click to toggle source
Calls superclass method Z3::Expr::new
# 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

Public Instance Methods

complement() click to toggle source
# File lib/z3/expr/set_expr.rb, line 17
def complement
  sort.new(LowLevel.mk_set_complement(self))
end
difference(other) click to toggle source
# File lib/z3/expr/set_expr.rb, line 29
def difference(other)
  SetExpr.Difference(self, other)
end
element_sort() click to toggle source
# File lib/z3/expr/set_expr.rb, line 5
def element_sort
  sort.element_sort
end
include?(element) click to toggle source
# 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
intersection(other) click to toggle source
# File lib/z3/expr/set_expr.rb, line 25
def intersection(other)
  SetExpr.Union(self, other)
end
is_subset_of(other) click to toggle source
# File lib/z3/expr/set_expr.rb, line 13
def is_subset_of(other)
  SetExpr.Subset(self, other)
end
is_superset_of(other) click to toggle source
# File lib/z3/expr/set_expr.rb, line 9
def is_superset_of(other)
  SetExpr.Subset(other, self)
end
union(other) click to toggle source
# File lib/z3/expr/set_expr.rb, line 21
def union(other)
  SetExpr.Union(self, other)
end