class Z3::FloatSort

# File lib/z3/sort/float_sort.rb, line 3
def initialize(e, s=nil)
  if s.nil?
    case e
    when 16
      super LowLevel.mk_fpa_sort_16
    when 32
      super LowLevel.mk_fpa_sort_32
    when 64
      super LowLevel.mk_fpa_sort_64
    when 128
      super LowLevel.mk_fpa_sort_128
    when :half
      super LowLevel.mk_fpa_sort_half
    when :single
      super LowLevel.mk_fpa_sort_single
    when :double
      super LowLevel.mk_fpa_sort_double
    when :quadruple
      super LowLevel.mk_fpa_sort_quadruple
    else
      raise Z3::Exception, "Unknown float type #{e}, use FloatSort.new(exponent_bits, significant_bits)"
    end
  else
    super LowLevel.mk_fpa_sort(e, s)
  end
end

# File lib/z3/sort/float_sort.rb, line 107
def >(other)
  raise ArgumentError unless other.is_a?(Sort)
  return true if other.is_a?(IntSort) # This is nasty...
  return true if other.is_a?(RealSort) # This is nasty...
  false
end

# File lib/z3/sort/float_sort.rb, line 114
def ebits
  LowLevel.fpa_get_ebits(self)
end

# File lib/z3/sort/float_sort.rb, line 30
def expr_class
  FloatExpr
end

# File lib/z3/sort/float_sort.rb, line 68
def from_components(sign, exponent, significand)
  expect_bitvec_of_size(sign, 1, "a sign")
  expect_bitvec_of_size(exponent, ebits, "an exponent")
  expect_bitvec_of_size(significand, sbits - 1, "a significand")
  new(LowLevel.mk_fpa_fp(sign, exponent, significand))
end

# File lib/z3/sort/float_sort.rb, line 34
def from_const(val)
  if val.is_a?(Integer)
    val_f = val.to_f
    raise Z3::Exception, "Out of range" unless val_f == val
    val = val_f
  elsif !val.is_a?(Float)
    raise cant_convert(val)
  end

  # A Ruby Float is a double, so this is exact for the double sort
  double = FloatSort.new(:double)
  return new(LowLevel.mk_fpa_numeral_double(val, self)) if self == double

  # For every other sort the value has to be rounded, and Z3_mk_fpa_numeral_double
  # gets that wrong - it returns NaN on overflow and misencodes denormals. Build the
  # exact double instead, and let Z3 round it to this sort the way IEEE says to.
  exact = FloatExpr.new(LowLevel.mk_fpa_numeral_double(val, double), double)
  rounding_mode = RoundingModeSort.new.nearest_ties_even
  new(LowLevel.mk_fpa_to_fp_float(rounding_mode, exact, self)).simplify
end

# File lib/z3/sort/float_sort.rb, line 75
def from_float(float, mode)
  raise Z3::Exception, "Float expected" unless float.is_a?(FloatExpr)
  new(LowLevel.mk_fpa_to_fp_float(expect_mode(mode), float, self))
end

# File lib/z3/sort/float_sort.rb, line 60
def from_ieee_bv(bv)
  expect_bitvec_of_size(bv, ebits + sbits, "an IEEE bit pattern")
  new(LowLevel.mk_fpa_to_fp_bv(bv, self))
end

# File lib/z3/sort/float_sort.rb, line 80
def from_real(real, mode)
  new(LowLevel.mk_fpa_to_fp_real(expect_mode(mode), RealSort.new.cast(real), self))
end

# File lib/z3/sort/float_sort.rb, line 86
def from_signed_bv(bv, mode)
  raise Z3::Exception, "Bitvec expected" unless bv.is_a?(BitvecExpr)
  new(LowLevel.mk_fpa_to_fp_signed(expect_mode(mode), bv, self))
end

# File lib/z3/sort/float_sort.rb, line 98
def from_significand_and_exponent(significand, exponent, mode)
  new(LowLevel.mk_fpa_to_fp_int_real(
    expect_mode(mode),
    IntSort.new.cast(exponent),
    RealSort.new.cast(significand),
    self,
  ))
end

# File lib/z3/sort/float_sort.rb, line 91
def from_unsigned_bv(bv, mode)
  raise Z3::Exception, "Bitvec expected" unless bv.is_a?(BitvecExpr)
  new(LowLevel.mk_fpa_to_fp_unsigned(expect_mode(mode), bv, self))
end

# File lib/z3/sort/float_sort.rb, line 126
def inspect
  "FloatSort(#{ebits}, #{sbits})"
end

# File lib/z3/sort/float_sort.rb, line 130
def nan
  new LowLevel.mk_fpa_nan(self)
end

# File lib/z3/sort/float_sort.rb, line 138
def negative_infinity
  new LowLevel.mk_fpa_inf(self, true)
end

# File lib/z3/sort/float_sort.rb, line 146
def negative_zero
  new LowLevel.mk_fpa_zero(self, true)
end

# File lib/z3/sort/float_sort.rb, line 134
def positive_infinity
  new LowLevel.mk_fpa_inf(self, false)
end

# File lib/z3/sort/float_sort.rb, line 142
def positive_zero
  new LowLevel.mk_fpa_zero(self, false)
end

# File lib/z3/sort/float_sort.rb, line 118
def sbits
  LowLevel.fpa_get_sbits(self)
end

# File lib/z3/sort/float_sort.rb, line 122
def to_s
  "Float(#{ebits}, #{sbits})"
end