Z3::FloatExpr
Inherits Reference < Object
An IEEE 754 float. Arithmetic rounds, so #add and friends take a rounding
mode and there are no + / - / * / / operators - IEEE has no such thing
as an addition which doesn't say how it rounds.
The comparisons are IEEE's, not Z3's =: +zero == -zero is true, and
NaN == NaN is false. #same_term? is what asks whether two expressions are
the same term.
Constructors
Instance methods
fp.eq has no negation of its own, and Z3's distinct is term inequality -
which answers differently for the zeroes and for NaN
Arithmetic is #add / #sub / #mul / #div rather than the operators, because every one of them rounds and IEEE says the rounding has to be spelled out
Every float literal is an application, NaN and the infinities included, so
this can't be the AstKind question it is on Int and Bitvec - Z3 has a
separate call for it
(self * other) + addend, rounded once at the end rather than after the
multiply and again after the add
Z3 Bools, like every other sort's predicates, not Crystal ones. NaN answers false to all of them, itself excepted.
Neither zero nor NaN, so this is not ~zero? - the two zeroes and NaN are
the three values which are neither positive nor negative
Nearest float with no fractional part, rounded mode's way - so which of 2.0
and 3.0 you get for 2.5 is the rounding mode's business, not this method's
Whether this is the same term as other. Z3 hash-conses its expressions, so
this is structural equality - Z3.int("a") + 1 built twice is one term. It is
a named method rather than == because == builds a Z3 expression instead of
answering a Crystal Bool - see the Limitations section of the README.
It's also the only equality which tells +zero from -zero and says NaN is
NaN, both of which == answers the other way round, IEEE's way.
The three IEEE fields as Bitvec expressions, and as Crystal Strings. Like
#value, all five only work on a literal - they take the value apart rather
than building a term which would. The significand is one bit narrower than
the sort's sbits, since IEEE doesn't store the leading bit.
The IEEE 754 bits of this float, as one Bitvec of the sort's full width. NaN has many encodings and Z3 doesn't promise which one you get.
Exact - a Real can hold every float value, where the other direction rounds. Z3 leaves the answer unspecified for NaN and the infinities.
Rounds to an integer, unlike #to_ieee_bv which reinterprets the same bits.
Z3 leaves the answer unspecified when the value doesn't fit in size bits.
Leaves Z3 for a Crystal Float64, where #to_real and #to_ieee_bv build expressions. A Crystal Float64 is an IEEE double, so every Float(11, 53) or narrower value converts exactly, NaN, the infinities and the two zeroes included.
A wider sort raises whatever it holds, even when that value happens to fit - Float(15, 113)'s 1.5 is a Float64's 1.5, but a sort which can't round-trip through a Float64 doesn't get a #value which works only sometimes.