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