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 



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
128
129
130
 
# File 'lib/z3/sort/sort.rb', line 101

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 Z3::Exception, "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 



89
90
91
92
93
94
95
96
97
98
99
 
# File 'lib/z3/sort/sort.rb', line 89

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:



84
85
86
87
 
# File 'lib/z3/sort/sort.rb', line 84

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

#hash ⇒ Object

Z3 hash-conses sorts, and Set(X) is really Array(X, Bool), so two sorts can be

while their Ruby classes differ. hash has to follow the pointer like eql? does,

or sorts which are eql? would end up in different Hash buckets.



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

def hash
  _ast.address
end

#inspect ⇒ Object 



58
59
60
 
# File 'lib/z3/sort/sort.rb', line 58

def inspect
  "#{self}Sort"
end

#new(_ast) ⇒ Object

We pretend to be a class, sort of



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

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 



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

def value_class
  raise "SubclassResponsibility"
end

#var(name) ⇒ Object 



62
63
64
65
66
67
68
69
70
71
72
73
 
# File 'lib/z3/sort/sort.rb', line 62

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