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 "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 47
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 54
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 34
def from_const(val)
  if val.is_a?(Float)
    new LowLevel.mk_fpa_numeral_double(val, self)
  elsif val.is_a?(Integer)
    val_f = val.to_f
    # FIXME, there are other constructors
    raise Z3::Exception, "Out of range" unless val_f == val
    new LowLevel.mk_fpa_numeral_double(val_f, self)
  else
    raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}"
  end
end

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

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

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

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

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

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

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

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