class Z3::FloatExpr
Public Class Methods
Add(a, b, m)
click to toggle source
# 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
Div(a, b, m)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
In older versons, this dies when trying to calll Z3_get_ast_kind, min works on same call Works in 4.6
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 123 def Ne(a, b) ~Eq(a,b) end
Rem(a, b)
click to toggle source
# 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)
click to toggle source
# 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
coerce_to_mode_sort(m)
click to toggle source
# 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)
click to toggle source
# 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
new(_ast, sort)
click to toggle source
Calls superclass method
Z3::Expr::new
# File lib/z3/expr/expr.rb, line 5 def initialize(_ast, sort) super(_ast) @sort = sort raise Z3::Exception, "Values must have AST kind numeral, app, or quantifier" unless [:numeral, :app, :quantifier].include?(ast_kind) end
Public Instance Methods
!=(other)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 8 def !=(other) FloatExpr.Ne(self, other) end
-@()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 52 def -@ sort.new LowLevel.mk_fpa_neg(self) end
<(other)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 12 def <(other) FloatExpr.Lt(self, other) end
<=(other)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 16 def <=(other) FloatExpr.Le(self, other) end
==(other)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 4 def ==(other) FloatExpr.Eq(self, other) end
>(other)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 20 def >(other) FloatExpr.Gt(self, other) end
>=(other)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 24 def >=(other) FloatExpr.Ge(self, other) end
abs()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 48 def abs sort.new LowLevel.mk_fpa_abs(self) end
add(other, mode)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 28 def add(other, mode) FloatExpr.Add(self, other, mode) end
div(other, mode)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 40 def div(other, mode) FloatExpr.Div(self, other, mode) end
exponent_string(biased)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 96 def exponent_string(biased) LowLevel.fpa_get_numeral_exponent_string(self, biased) end
infinite?()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 56 def infinite? BoolSort.new.new LowLevel.mk_fpa_is_infinite(self) end
max(other)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 88 def max(other) FloatExpr.Max(self, other) end
min(other)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 92 def min(other) FloatExpr.Min(self, other) end
mul(other, mode)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 36 def mul(other, mode) FloatExpr.Mul(self, other, mode) end
nan?()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 60 def nan? BoolSort.new.new LowLevel.mk_fpa_is_nan(self) end
negative?()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 64 def negative? BoolSort.new.new LowLevel.mk_fpa_is_negative(self) end
nonzero?()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 84 def nonzero? Z3.And(~zero?, ~nan?) end
normal?()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 68 def normal? BoolSort.new.new LowLevel.mk_fpa_is_normal(self) end
positive?()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 72 def positive? BoolSort.new.new LowLevel.mk_fpa_is_positive(self) end
rem(other)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 44 def rem(other) FloatExpr.Rem(self, other) end
significand_string()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 100 def significand_string LowLevel.fpa_get_numeral_significand_string(self) end
sub(other, mode)
click to toggle source
# File lib/z3/expr/float_expr.rb, line 32 def sub(other, mode) FloatExpr.Sub(self, other, mode) end
subnormal?()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 76 def subnormal? BoolSort.new.new LowLevel.mk_fpa_is_subnormal(self) end
zero?()
click to toggle source
# File lib/z3/expr/float_expr.rb, line 80 def zero? BoolSort.new.new LowLevel.mk_fpa_is_zero(self) end