Z3::FloatSort
Inherits Reference < Object
Real IEEE 754 floats, not Reals - Float(11, 53) is a double, with everything
that implies: two zeroes, two infinities, NaN, and rounding on every operation.
A sort is its two bit counts, the exponent's and the significand's, and the four IEEE widths can be named instead:
Z3::FloatSort.new(:double) # also :half, :single, :quadruple
Z3::FloatSort.new(64) # also 16, 32, 128
Z3::FloatSort.new(11, 53) # the same sort againConstructors
Instance methods
Z3 hash-conses its sorts, so two Float sorts of the same two sizes are one sort
A Crystal Float64 is an IEEE double, so every value converts exactly into
Float(11, 53) - NaN, the infinities and the two zeroes included - and rounds
to nearest into anything narrower.
The three IEEE fields separately, which is #sign_bv / #exponent_bv /
#significand_bv backwards. The significand excludes the leading bit IEEE
doesn't store, so it's one narrower than sbits.
Reinterprets the IEEE 754 bits, so it's FloatExpr#to_ieee_bv backwards and
nothing is rounded. The Bitvec has to be exactly as wide as this sort.
Reads the Bitvec as a number and rounds it to this sort, where #from_ieee_bv reads the very same bits as a float already
significand * 2 ** exponent, with a Real significand and an Int exponent -
the one constructor which isn't a conversion from some other representation
The values IEEE has and no Crystal literal spells. self[Float64::NAN] and
friends build the same three, since a Crystal Float64 has them too.