class Z3::FloatExpr

# File lib/z3/expr/float_expr.rb, line 205
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 223
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 176
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 256
def FusedMultiplyAdd(a, b, c, m)
  a, b, c = coerce_to_same_float_sort(a, b, c)
  m = coerce_to_mode_sort(m)
  a.sort.new(LowLevel.mk_fpa_fma(m, a, b, c))
end

# File lib/z3/expr/float_expr.rb, line 195
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 185
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 200
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 190
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 236
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 241
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 217
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 181
def Ne(a, b)
  ~Eq(a,b)
end

# File lib/z3/expr/float_expr.rb, line 229
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 251
def RoundToIntegral(a, m)
  m = coerce_to_mode_sort(m)
  a.sort.new(LowLevel.mk_fpa_round_to_integral(m, a))
end

# File lib/z3/expr/float_expr.rb, line 246
def Sqrt(a, m)
  m = coerce_to_mode_sort(m)
  a.sort.new(LowLevel.mk_fpa_sqrt(m, a))
end

# File lib/z3/expr/float_expr.rb, line 211
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 171
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 165
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 68
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 64
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 154
def exponent_bv(biased)
  BitvecSort.new(sort.ebits).new(LowLevel.fpa_get_numeral_exponent_bv(self, biased))
end

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

# File lib/z3/expr/float_expr.rb, line 60
def fused_multiply_add(other, addend, mode)
  FloatExpr.FusedMultiplyAdd(self, other, addend, mode)
end

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

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

# File lib/z3/expr/float_expr.rb, line 108
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 76
def nan?
  BoolSort.new.new LowLevel.mk_fpa_is_nan(self)
end

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

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

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

# File lib/z3/expr/float_expr.rb, line 88
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 54
def round_to_integral(mode)
  FloatExpr.RoundToIntegral(self, mode)
end

# File lib/z3/expr/float_expr.rb, line 150
def sign_bv
  BitvecSort.new(1).new(LowLevel.fpa_get_numeral_sign_bv(self))
end

# File lib/z3/expr/float_expr.rb, line 158
def significand_bv
  BitvecSort.new(sort.sbits - 1).new(LowLevel.fpa_get_numeral_significand_bv(self))
end

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

# File lib/z3/expr/float_expr.rb, line 48
def sqrt(mode)
  FloatExpr.Sqrt(self, mode)
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 92
def subnormal?
  BoolSort.new.new LowLevel.mk_fpa_is_subnormal(self)
end

# File lib/z3/expr/float_expr.rb, line 126
def to_bv(*)
  raise Z3::Exception, "Use #to_signed_bv or #to_unsigned_bv for Float, not #to_bv"
end

# File lib/z3/expr/float_expr.rb, line 120
def to_ieee_bv
  BitvecSort.new(sort.ebits + sort.sbits).new(LowLevel.mk_fpa_to_ieee_bv(self))
end

# File lib/z3/expr/float_expr.rb, line 114
def to_real
  RealSort.new.new(LowLevel.mk_fpa_to_real(self))
end

# File lib/z3/expr/float_expr.rb, line 130
def to_signed_bv(size, mode)
  BitvecSort.new(size).new(LowLevel.mk_fpa_to_sbv(FloatExpr.coerce_to_mode_sort(mode), self, size))
end

# File lib/z3/expr/float_expr.rb, line 134
def to_unsigned_bv(size, mode)
  BitvecSort.new(size).new(LowLevel.mk_fpa_to_ubv(FloatExpr.coerce_to_mode_sort(mode), self, size))
end

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