Class: Z3::SetSort

Inherits:
Sort show all
Defined in:
lib/z3/sort/set_sort.rb

Instance Attribute Summary collapse

Attributes inherited from AST

#_ast

Instance Method Summary collapse

Methods inherited from Sort

#<, #<=, #<=>, #==, #>, #>=, #cast, #eql?, from_pointer, #from_value, #hash, #new, #value_class, #var

Methods inherited from AST

#arguments, #ast_kind, #func_decl, #sexpr, #simplify

Constructor Details

#initialize(element_sort) ⇒ SetSort

Returns a new instance of SetSort.



4
5
6
7
 
# File 'lib/z3/sort/set_sort.rb', line 4

def initialize(element_sort)
  @element_sort = element_sort
  super LowLevel.mk_set_sort(element_sort)
end

Instance Attribute Details

#element_sort ⇒ Object (readonly)

Returns the value of attribute element_sort.



3
4
5
 
# File 'lib/z3/sort/set_sort.rb', line 3

def element_sort
  @element_sort
end

Instance Method Details

#Empty ⇒ Object 



21
22
23
 
# File 'lib/z3/sort/set_sort.rb', line 21

def Empty
  new(LowLevel.mk_empty_set(self))
end

#expr_class ⇒ Object 



9
10
11
 
# File 'lib/z3/sort/set_sort.rb', line 9

def expr_class
  SetExpr
end

#Full ⇒ Object 



25
26
27
 
# File 'lib/z3/sort/set_sort.rb', line 25

def Full
  new(LowLevel.mk_full_set(self))
end

#inspect ⇒ Object 



17
18
19
 
# File 'lib/z3/sort/set_sort.rb', line 17

def inspect
  "SetSort(#{element_sort})"
end

#to_s ⇒ Object 



13
14
15
 
# File 'lib/z3/sort/set_sort.rb', line 13

def to_s
  "Set(#{element_sort})"
end