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

#abs ⇒ Object 



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_string ⇒ Object 



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