class Z3::FloatSort
Public Class Methods
new(e, s=nil)
click to toggle source
Calls superclass method
# 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
Public Instance Methods
>(other)
click to toggle source
# 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
ebits()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 54 def ebits LowLevel.fpa_get_ebits(self) end
expr_class()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 30 def expr_class FloatExpr end
from_const(val)
click to toggle source
# 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
inspect()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 66 def inspect "FloatSort(#{ebits}, #{sbits})" end
nan()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 70 def nan new LowLevel.mk_fpa_nan(self) end
negative_infinity()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 78 def negative_infinity new LowLevel.mk_fpa_inf(self, true) end
negative_zero()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 86 def negative_zero new LowLevel.mk_fpa_zero(self, true) end
positive_infinity()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 74 def positive_infinity new LowLevel.mk_fpa_inf(self, false) end
positive_zero()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 82 def positive_zero new LowLevel.mk_fpa_zero(self, false) end
sbits()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 58 def sbits LowLevel.fpa_get_sbits(self) end
to_s()
click to toggle source
# File lib/z3/sort/float_sort.rb, line 62 def to_s "Float(#{ebits}, #{sbits})" end