Class: Z3::Sort

Inherits:
AST
  • Object
show all
Includes:
Comparable
Defined in:
lib/z3/sort/sort.rb

Instance Attribute Summary

Attributes inherited from AST

#_ast

Class Method Summary collapse

Instance Method Summary collapse

Methods inherited from AST

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

Constructor Details

#initialize(_ast) ⇒ Sort

Returns a new instance of Sort.

Raises:



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

def initialize(_ast)
  super(_ast)
  raise Z3::Exception, "Sorts must have AST kind sort" unless ast_kind == :sort
end

Class Method Details

.from_pointer(_sort) ⇒ Object 



98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
 
# File 'lib/z3/sort/sort.rb', line 98

def self.from_pointer(_sort)
  kind = VeryLowLevel.Z3_get_sort_kind(LowLevel._ctx_pointer, _sort)
  case kind
  when 1
    BoolSort.new
  when 2
    IntSort.new
  when 3
    RealSort.new
  when 4
    n = VeryLowLevel.Z3_get_bv_sort_size(LowLevel._ctx_pointer, _sort)
    BitvecSort.new(n)
  when 5
    domain = from_pointer(VeryLowLevel.Z3_get_array_sort_domain(LowLevel._ctx_pointer, _sort))
    range = from_pointer(VeryLowLevel.Z3_get_array_sort_range(LowLevel._ctx_pointer, _sort))
    if range == BoolSort.new
      SetSort.new(domain)
    else
      ArraySort.new(domain, range)
    end
  when 9
    e = VeryLowLevel.Z3_fpa_get_ebits(LowLevel._ctx_pointer, _sort)
    s = VeryLowLevel.Z3_fpa_get_sbits(LowLevel._ctx_pointer, _sort)
    FloatSort.new(e, s)
  when 10
    RoundingModeSort.new
  else
    raise "Unknown sort kind #{kind}"
  end
end

Instance Method Details

#<(other) ⇒ Object

Reimplementing Comparable Check if it can handle partial orders OK

Raises:

  • (ArgumentError) 


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

def <(other)
  raise ArgumentError unless other.is_a?(Sort)
  other > self
end

#<=(other) ⇒ Object

Raises:

  • (ArgumentError) 


30
31
32
33
 
# File 'lib/z3/sort/sort.rb', line 30

def <=(other)
  raise ArgumentError unless other.is_a?(Sort)
  other >= self
end

#<=>(other) ⇒ Object

Raises:

  • (ArgumentError) 


35
36
37
38
39
40
41
 
# File 'lib/z3/sort/sort.rb', line 35

def <=>(other)
  raise ArgumentError unless other.is_a?(Sort)
  return 0 if self == other
  return 1 if self > other
  return -1 if other > self
  nil
end

#==(other) ⇒ Object 



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

def ==(other)
  other.is_a?(Sort) and @_ast == other._ast
end

#>(other) ⇒ Object

Raises:

  • (ArgumentError) 


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

def >(other)
  raise ArgumentError unless other.is_a?(Sort)
  false
end

#>=(other) ⇒ Object

Raises:

  • (ArgumentError) 


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

def >=(other)
  raise ArgumentError unless other.is_a?(Sort)
  self == other or self > other
end

#cast(a) ⇒ Object 



86
87
88
89
90
91
92
93
94
95
96
 
# File 'lib/z3/sort/sort.rb', line 86

def cast(a)
  if a.is_a?(Expr)
    if  a.sort == self
      a
    else
      from_value(a)
    end
  else
    from_const(a)
  end
end

#eql?(other) ⇒ Boolean

Returns:

  • (Boolean) 


47
48
49
 
# File 'lib/z3/sort/sort.rb', line 47

def eql?(other)
  self == other
end

#from_value(v) ⇒ Object

Raises:



81
82
83
84
 
# File 'lib/z3/sort/sort.rb', line 81

def from_value(v)
  return v if v.sort == self
  raise Z3::Exception, "Can't convert #{v.sort} into #{self}"
end

#hash ⇒ Object 



51
52
53
 
# File 'lib/z3/sort/sort.rb', line 51

def hash
  self.class.hash
end

#inspect ⇒ Object 



55
56
57
 
# File 'lib/z3/sort/sort.rb', line 55

def inspect
  "#{self}Sort"
end

#new(_ast) ⇒ Object

We pretend to be a class, sort of



73
74
75
 
# File 'lib/z3/sort/sort.rb', line 73

def new(_ast)
  expr_class.new(_ast, self)
end

#to_s ⇒ Object 



43
44
45
 
# File 'lib/z3/sort/sort.rb', line 43

def to_s
  LowLevel.ast_to_string(self)
end

#value_class ⇒ Object 



77
78
79
 
# File 'lib/z3/sort/sort.rb', line 77

def value_class
  raise "SubclassResponsibility"
end

#var(name) ⇒ Object 



59
60
61
62
63
64
65
66
67
68
69
70
 
# File 'lib/z3/sort/sort.rb', line 59

def var(name)
  if name.is_a?(Enumerable)
    name.map{|v| var(v)}
  else
    new(
      LowLevel.mk_const(
        LowLevel.mk_string_symbol(name),
        self,
      )
    )
  end
end