class Z3::FloatExpr

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# File lib/z3/expr/float_expr.rb, line 123
def Ne(a, b)
  ~Eq(a,b)
end

# 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

# 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

# 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

# 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

# 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

# File lib/z3/expr/float_expr.rb, line 8
def !=(other)
  FloatExpr.Ne(self, other)
end

# File lib/z3/expr/float_expr.rb, line 52
def -@
  sort.new LowLevel.mk_fpa_neg(self)
end

# File lib/z3/expr/float_expr.rb, line 12
def <(other)
  FloatExpr.Lt(self, other)
end

# File lib/z3/expr/float_expr.rb, line 16
def <=(other)
  FloatExpr.Le(self, other)
end

# File lib/z3/expr/float_expr.rb, line 4
def ==(other)
  FloatExpr.Eq(self, other)
end

# File lib/z3/expr/float_expr.rb, line 20
def >(other)
  FloatExpr.Gt(self, other)
end

# File lib/z3/expr/float_expr.rb, line 24
def >=(other)
  FloatExpr.Ge(self, other)
end

# File lib/z3/expr/float_expr.rb, line 48
def abs
  sort.new LowLevel.mk_fpa_abs(self)
end

# File lib/z3/expr/float_expr.rb, line 28
def add(other, mode)
  FloatExpr.Add(self, other, mode)
end

# File lib/z3/expr/float_expr.rb, line 40
def div(other, mode)
  FloatExpr.Div(self, other, mode)
end

# File lib/z3/expr/float_expr.rb, line 96
def exponent_string(biased)
  LowLevel.fpa_get_numeral_exponent_string(self, biased)
end

# File lib/z3/expr/float_expr.rb, line 56
def infinite?
  BoolSort.new.new LowLevel.mk_fpa_is_infinite(self)
end

# File lib/z3/expr/float_expr.rb, line 88
def max(other)
  FloatExpr.Max(self, other)
end

# File lib/z3/expr/float_expr.rb, line 92
def min(other)
  FloatExpr.Min(self, other)
end

# File lib/z3/expr/float_expr.rb, line 36
def mul(other, mode)
  FloatExpr.Mul(self, other, mode)
end

# File lib/z3/expr/float_expr.rb, line 60
def nan?
  BoolSort.new.new LowLevel.mk_fpa_is_nan(self)
end

# File lib/z3/expr/float_expr.rb, line 64
def negative?
  BoolSort.new.new LowLevel.mk_fpa_is_negative(self)
end

# File lib/z3/expr/float_expr.rb, line 84
def nonzero?
  Z3.And(~zero?, ~nan?)
end

# File lib/z3/expr/float_expr.rb, line 68
def normal?
  BoolSort.new.new LowLevel.mk_fpa_is_normal(self)
end

# File lib/z3/expr/float_expr.rb, line 72
def positive?
  BoolSort.new.new LowLevel.mk_fpa_is_positive(self)
end

# File lib/z3/expr/float_expr.rb, line 44
def rem(other)
  FloatExpr.Rem(self, other)
end

# File lib/z3/expr/float_expr.rb, line 100
def significand_string
  LowLevel.fpa_get_numeral_significand_string(self)
end

# File lib/z3/expr/float_expr.rb, line 32
def sub(other, mode)
  FloatExpr.Sub(self, other, mode)
end

# File lib/z3/expr/float_expr.rb, line 76
def subnormal?
  BoolSort.new.new LowLevel.mk_fpa_is_subnormal(self)
end

# File lib/z3/expr/float_expr.rb, line 80
def zero?
  BoolSort.new.new LowLevel.mk_fpa_is_zero(self)
end