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, #func_decl, #initialize, #sexpr, #simplify, #to_s

Constructor Details

This class inherits a constructor from Z3::Expr

Class Method Details

.Add(a, b, m) ⇒ Object 



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

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:



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

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:



103
104
105
106
107
 
# File 'lib/z3/expr/float_expr.rb', line 103

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 



161
162
163
164
165
 
# File 'lib/z3/expr/float_expr.rb', line 161

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 



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

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 



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

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 



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

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 



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

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 



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

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



174
175
176
177
 
# File 'lib/z3/expr/float_expr.rb', line 174

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 



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

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 



155
156
157
158
159
 
# File 'lib/z3/expr/float_expr.rb', line 155

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 



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

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

.Rem(a, b) ⇒ Object 



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

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 



149
150
151
152
153
 
# File 'lib/z3/expr/float_expr.rb', line 149

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 



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

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 



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

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

#min(other) ⇒ Object 



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

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

#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 



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

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