class
Z3::FloatSort
- Z3::FloatSort
- Reference
- Object
Overview
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 againDefined in:
z3/float_sort.crConstructors
- .new(ebits : Int, sbits : Int)
-
.new(width : Int | Symbol)
The four IEEE widths, by total size or by name.
Instance Method Summary
-
#==(other : FloatSort)
Z3 hash-conses its sorts, so two Float sorts of the same two sizes are one sort
- #[](expr : FloatExpr)
-
#[](value : Float64)
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. - #[](value : Int)
- #cast(value) : FloatExpr
- #ebits : UInt32
- #from_ast(ast : LibZ3::Ast) : FloatExpr
-
#from_components(sign : BitvecExpr, exponent : BitvecExpr, significand : BitvecExpr)
The three IEEE fields separately, which is
#sign_bv/#exponent_bv/#significand_bvbackwards. - #from_float(float : FloatExpr, mode : RoundingModeExpr)
-
#from_ieee_bv(bv : BitvecExpr)
Reinterprets the IEEE 754 bits, so it's
FloatExpr#to_ieee_bvbackwards and nothing is rounded. - #from_real(real, mode : RoundingModeExpr)
-
#from_signed_bv(bv : BitvecExpr, mode : RoundingModeExpr)
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
-
#from_significand_and_exponent(significand, exponent, mode : RoundingModeExpr)
significand * 2 ** exponent, with a Real significand and an Int exponent - the one constructor which isn't a conversion from some other representation - #from_unsigned_bv(bv : BitvecExpr, mode : RoundingModeExpr)
-
#nan
The values IEEE has and no Crystal literal spells.
- #negative_infinity
- #negative_zero
- #positive_infinity
- #positive_zero
- #sbits : UInt32
- #to_s(io)
- #to_unsafe : LibZ3::Sort
- #var(name : String)
Constructor Detail
The four IEEE widths, by total size or by name. Each is only its two bit
counts, so this is mk_fpa_sort too - Z3's mk_fpa_sort_16 and friends are
the same four sorts under their IEEE names.
Instance Method Detail
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.