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