class
Z3::FloatExpr
- Z3::FloatExpr
- Reference
- Object
Overview
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.
Defined in:
z3/float_expr.crConstructors
Instance Method Summary
-
#!=(other)
fp.eqhas no negation of its own, and Z3'sdistinctis term inequality - which answers differently for the zeroes and for NaN - #%(other)
- #*(other)
- #+(other)
- #-(other)
- #-
- #/(other)
- #<(other)
- #<=(other)
-
#==(other)
Returns
false(other can only be aValuehere). - #>(other)
- #>=(other)
- #abs
-
#add(other, mode : RoundingModeExpr)
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
-
#const?
Every float literal is an application, NaN and the infinities included, so this can't be the
AstKindquestion it is on Int and Bitvec - Z3 has a separate call for it - #div(other, mode : RoundingModeExpr)
- #ebits
- #exponent_bv(biased : Bool)
- #exponent_string(biased : Bool)
-
#fused_multiply_add(other, addend, mode : RoundingModeExpr)
(self * other) + addend, rounded once at the end rather than after the multiply and again after the add - #infinite?
- #inspect(io)
- #max(other)
- #min(other)
- #mul(other, mode : RoundingModeExpr)
-
#nan?
Z3 Bools, like every other sort's predicates, not Crystal ones.
- #negative?
-
#nonzero?
Neither zero nor NaN, so this is not
~zero?- the two zeroes and NaN are the three values which are neither positive nor negative - #normal?
- #positive?
-
#rem(other)
The IEEE remainder, which is exact and so takes no rounding mode
-
#round_to_integral(mode : RoundingModeExpr)
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 -
#same_term?(other : AnyExpr)
Whether this is the same term as
other. - #sbits
-
#sign_bv
The three IEEE fields as Bitvec expressions, and as Crystal Strings.
- #significand_bv
- #significand_string
- #simplify
- #sort : Z3::FloatSort
- #sqrt(mode : RoundingModeExpr)
- #sub(other, mode : RoundingModeExpr)
- #subnormal?
- #to_bv(size, mode)
- #to_f : Float64
-
#to_ieee_bv
The IEEE 754 bits of this float, as one Bitvec of the sort's full width.
-
#to_real
Exact - a Real can hold every float value, where the other direction rounds.
- #to_s(io)
-
#to_signed_bv(size : Int, mode : RoundingModeExpr)
Rounds to an integer, unlike #to_ieee_bv which reinterprets the same bits.
- #to_unsafe : LibZ3::Ast
- #to_unsigned_bv(size : Int, mode : RoundingModeExpr)
-
#value : Float64
Leaves Z3 for a Crystal Float64, where #to_real and #to_ieee_bv build expressions.
- #zero?
Constructor Detail
Instance Method Detail
fp.eq has no negation of its own, and Z3's distinct is term inequality -
which answers differently for the zeroes and for NaN
Returns false (other can only be a Value here).
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.