Class: Z3::SetExpr

Inherits:
Expr show all
Defined in:
lib/z3/expr/set_expr.rb

Instance Attribute Summary

Attributes inherited from Expr

#sort

Attributes inherited from AST

#_ast

Class Method Summary collapse

Instance Method Summary collapse

Methods inherited from Expr

#!=, #==, Add, And, Distinct, Eq, Ge, Gt, Le, Lt, Mul, Or, Sub, Xor, coerce_to_same_sort, #initialize, #inspect, new_from_pointer, sort_for_const

Methods inherited from AST

#arguments, #ast_kind, #eql?, #func_decl, #hash, #initialize, #sexpr, #simplify, #to_s

Constructor Details

This class inherits a constructor from Z3::Expr

Class Method Details

.coerce_to_same_set_sort(*args) ⇒ Object

Raises:



39
40
41
42
43
 
# 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

.Difference(a, b) ⇒ Object 



60
61
62
63
 
# 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) ⇒ Object 



55
56
57
58
 
# 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) ⇒ Object 



45
46
47
48
 
# 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) ⇒ Object 



50
51
52
53
 
# 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

Instance Method Details

#complement ⇒ Object 



17
18
19
 
# File 'lib/z3/expr/set_expr.rb', line 17

def complement
  sort.new(LowLevel.mk_set_complement(self))
end

#difference(other) ⇒ Object 



29
30
31
 
# File 'lib/z3/expr/set_expr.rb', line 29

def difference(other)
  SetExpr.Difference(self, other)
end

#element_sort ⇒ Object 



5
6
7
 
# File 'lib/z3/expr/set_expr.rb', line 5

def element_sort
  sort.element_sort
end

#include?(element) ⇒ Boolean

Returns:

  • (Boolean) 


33
34
35
36
 
# 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) ⇒ Object 



25
26
27
 
# File 'lib/z3/expr/set_expr.rb', line 25

def intersection(other)
  SetExpr.Union(self, other)
end

#is_subset_of(other) ⇒ Object 



13
14
15
 
# File 'lib/z3/expr/set_expr.rb', line 13

def is_subset_of(other)
  SetExpr.Subset(self, other)
end

#is_superset_of(other) ⇒ Object 



9
10
11
 
# File 'lib/z3/expr/set_expr.rb', line 9

def is_superset_of(other)
  SetExpr.Subset(other, self)
end

#union(other) ⇒ Object 



21
22
23
 
# File 'lib/z3/expr/set_expr.rb', line 21

def union(other)
  SetExpr.Union(self, other)
end