Class: Z3::FloatExpr

Inherits:
Expr show all
Defined in:
lib/z3/expr/float_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

And, Distinct, Or, 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

.Add(a, b, m) ⇒ Object



147
148
149
150
151
# File 'lib/z3/expr/float_expr.rb', line 147

def Add(a, b, m)
  a, b = coerce_to_same_float_sort(a, b)
  m = coerce_to_mode_sort(m)
  a.sort.new(LowLevel.mk_fpa_add(m, a, b))
end

.coerce_to_mode_sort(m) ⇒ Object

Raises:



113
114
115
116
# File 'lib/z3/expr/float_expr.rb', line 113

def coerce_to_mode_sort(m)
  raise Z3::Exception, "Mode expected" unless m.is_a?(RoundingModeExpr)
  m
end

.coerce_to_same_float_sort(*args) ⇒ Object

Raises:



107
108
109
110
111
# File 'lib/z3/expr/float_expr.rb', line 107

def coerce_to_same_float_sort(*args)
  args = coerce_to_same_sort(*args)
  raise Z3::Exception, "Float value with same sizes expected" unless args[0].is_a?(FloatExpr)
  args
end

.Div(a, b, m) ⇒ Object



165
166
167
168
169
# File 'lib/z3/expr/float_expr.rb', line 165

def Div(a, b, m)
  a, b = coerce_to_same_float_sort(a, b)
  m = coerce_to_mode_sort(m)
  a.sort.new(LowLevel.mk_fpa_div(m, a, b))
end

.Eq(a, b) ⇒ Object



118
119
120
121
# File 'lib/z3/expr/float_expr.rb', line 118

def Eq(a, b)
  a, b = coerce_to_same_float_sort(a, b)
  BoolSort.new.new(LowLevel.mk_fpa_eq(a, b))
end

.Ge(a, b) ⇒ Object



137
138
139
140
# File 'lib/z3/expr/float_expr.rb', line 137

def Ge(a, b)
  a, b = coerce_to_same_float_sort(a, b)
  BoolSort.new.new(LowLevel.mk_fpa_geq(a, b))
end

.Gt(a, b) ⇒ Object



127
128
129
130
# File 'lib/z3/expr/float_expr.rb', line 127

def Gt(a, b)
  a, b = coerce_to_same_float_sort(a, b)
  BoolSort.new.new(LowLevel.mk_fpa_gt(a, b))
end

.Le(a, b) ⇒ Object



142
143
144
145
# File 'lib/z3/expr/float_expr.rb', line 142

def Le(a, b)
  a, b = coerce_to_same_float_sort(a, b)
  BoolSort.new.new(LowLevel.mk_fpa_leq(a, b))
end

.Lt(a, b) ⇒ Object



132
133
134
135
# File 'lib/z3/expr/float_expr.rb', line 132

def Lt(a, b)
  a, b = coerce_to_same_float_sort(a, b)
  BoolSort.new.new(LowLevel.mk_fpa_lt(a, b))
end

.Max(a, b) ⇒ Object

In older versons, this dies when trying to calll Z3_get_ast_kind, min works on same call Works in 4.6



178
179
180
181
# File 'lib/z3/expr/float_expr.rb', line 178

def Max(a, b)
  a, b = coerce_to_same_float_sort(a, b)
  a.sort.new(LowLevel.mk_fpa_max(a, b))
end

.Min(a, b) ⇒ Object



183
184
185
186
# File 'lib/z3/expr/float_expr.rb', line 183

def Min(a, b)
  a, b = coerce_to_same_float_sort(a, b)
  a.sort.new(LowLevel.mk_fpa_min(a, b))
end

.Mul(a, b, m) ⇒ Object



159
160
161
162
163
# File 'lib/z3/expr/float_expr.rb', line 159

def Mul(a, b, m)
  a, b = coerce_to_same_float_sort(a, b)
  m = coerce_to_mode_sort(m)
  a.sort.new(LowLevel.mk_fpa_mul(m, a, b))
end

.Ne(a, b) ⇒ Object



123
124
125
# File 'lib/z3/expr/float_expr.rb', line 123

def Ne(a, b)
  ~Eq(a,b)
end

.Rem(a, b) ⇒ Object



171
172
173
174
# File 'lib/z3/expr/float_expr.rb', line 171

def Rem(a, b)
  a, b = coerce_to_same_float_sort(a, b)
  a.sort.new(LowLevel.mk_fpa_rem(a, b))
end

.Sub(a, b, m) ⇒ Object



153
154
155
156
157
# File 'lib/z3/expr/float_expr.rb', line 153

def Sub(a, b, m)
  a, b = coerce_to_same_float_sort(a, b)
  m = coerce_to_mode_sort(m)
  a.sort.new(LowLevel.mk_fpa_sub(m, a, b))
end

Instance Method Details

#!=(other) ⇒ Object



8
9
10
# File 'lib/z3/expr/float_expr.rb', line 8

def !=(other)
  FloatExpr.Ne(self, other)
end

#-@Object



52
53
54
# File 'lib/z3/expr/float_expr.rb', line 52

def -@
  sort.new LowLevel.mk_fpa_neg(self)
end

#<(other) ⇒ Object



12
13
14
# File 'lib/z3/expr/float_expr.rb', line 12

def <(other)
  FloatExpr.Lt(self, other)
end

#<=(other) ⇒ Object



16
17
18
# File 'lib/z3/expr/float_expr.rb', line 16

def <=(other)
  FloatExpr.Le(self, other)
end

#==(other) ⇒ Object



4
5
6
# File 'lib/z3/expr/float_expr.rb', line 4

def ==(other)
  FloatExpr.Eq(self, other)
end

#>(other) ⇒ Object



20
21
22
# File 'lib/z3/expr/float_expr.rb', line 20

def >(other)
  FloatExpr.Gt(self, other)
end

#>=(other) ⇒ Object



24
25
26
# File 'lib/z3/expr/float_expr.rb', line 24

def >=(other)
  FloatExpr.Ge(self, other)
end

#absObject



48
49
50
# File 'lib/z3/expr/float_expr.rb', line 48

def abs
  sort.new LowLevel.mk_fpa_abs(self)
end

#add(other, mode) ⇒ Object



28
29
30
# File 'lib/z3/expr/float_expr.rb', line 28

def add(other, mode)
  FloatExpr.Add(self, other, mode)
end

#div(other, mode) ⇒ Object



40
41
42
# File 'lib/z3/expr/float_expr.rb', line 40

def div(other, mode)
  FloatExpr.Div(self, other, mode)
end

#exponent_string(biased) ⇒ Object



96
97
98
# File 'lib/z3/expr/float_expr.rb', line 96

def exponent_string(biased)
  LowLevel.fpa_get_numeral_exponent_string(self, biased)
end

#infinite?Boolean

Returns:

  • (Boolean)


56
57
58
# File 'lib/z3/expr/float_expr.rb', line 56

def infinite?
  BoolSort.new.new LowLevel.mk_fpa_is_infinite(self)
end

#max(other) ⇒ Object



88
89
90
# File 'lib/z3/expr/float_expr.rb', line 88

def max(other)
  FloatExpr.Max(self, other)
end

#min(other) ⇒ Object



92
93
94
# File 'lib/z3/expr/float_expr.rb', line 92

def min(other)
  FloatExpr.Min(self, other)
end

#mul(other, mode) ⇒ Object



36
37
38
# File 'lib/z3/expr/float_expr.rb', line 36

def mul(other, mode)
  FloatExpr.Mul(self, other, mode)
end

#nan?Boolean

Returns:

  • (Boolean)


60
61
62
# File 'lib/z3/expr/float_expr.rb', line 60

def nan?
  BoolSort.new.new LowLevel.mk_fpa_is_nan(self)
end

#negative?Boolean

Returns:

  • (Boolean)


64
65
66
# File 'lib/z3/expr/float_expr.rb', line 64

def negative?
  BoolSort.new.new LowLevel.mk_fpa_is_negative(self)
end

#nonzero?Boolean

Returns:

  • (Boolean)


84
85
86
# File 'lib/z3/expr/float_expr.rb', line 84

def nonzero?
  Z3.And(~zero?, ~nan?)
end

#normal?Boolean

Returns:

  • (Boolean)


68
69
70
# File 'lib/z3/expr/float_expr.rb', line 68

def normal?
  BoolSort.new.new LowLevel.mk_fpa_is_normal(self)
end

#positive?Boolean

Returns:

  • (Boolean)


72
73
74
# File 'lib/z3/expr/float_expr.rb', line 72

def positive?
  BoolSort.new.new LowLevel.mk_fpa_is_positive(self)
end

#rem(other) ⇒ Object



44
45
46
# File 'lib/z3/expr/float_expr.rb', line 44

def rem(other)
  FloatExpr.Rem(self, other)
end

#significand_stringObject



100
101
102
# File 'lib/z3/expr/float_expr.rb', line 100

def significand_string
  LowLevel.fpa_get_numeral_significand_string(self)
end

#sub(other, mode) ⇒ Object



32
33
34
# File 'lib/z3/expr/float_expr.rb', line 32

def sub(other, mode)
  FloatExpr.Sub(self, other, mode)
end

#subnormal?Boolean

Returns:

  • (Boolean)


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

def subnormal?
  BoolSort.new.new LowLevel.mk_fpa_is_subnormal(self)
end

#zero?Boolean

Returns:

  • (Boolean)


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

def zero?
  BoolSort.new.new LowLevel.mk_fpa_is_zero(self)
end