RoundingMode
This enum class represents a floating-point rounding mode.
-
enum
class
cvc5
::
RoundingMode
-
Rounding modes for floating-point numbers.
For many floating-point operations, infinitely precise results may not be representable with the number of available bits. Thus, the results are rounded in a certain way to one of the representable floating-point numbers.
These rounding modes directly follow the SMT-LIB theory for floating-point arithmetic, which in turn is based on IEEE Standard 754 [ IEE19 ] . The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE Standard 754.
Values:
-
enumerator
ROUND_NEAREST_TIES_TO_EVEN
-
Round to the nearest even number.
If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near, the one with an even least significant digit will be delivered.
-
enumerator
ROUND_TOWARD_POSITIVE
-
Round towards positive infinity (SMT-LIB:
+oo
).The result shall be the format’s floating-point number (possibly
+oo
) closest to and no less than the infinitely precise result.
-
enumerator
ROUND_TOWARD_NEGATIVE
-
Round towards negative infinity (
-oo
).The result shall be the format’s floating-point number (possibly
-oo
) closest to and no less than the infinitely precise result.
-
enumerator
ROUND_TOWARD_ZERO
-
Round towards zero.
The result shall be the format’s floating-point number closest to and no greater in magnitude than the infinitely precise result.
-
enumerator
ROUND_NEAREST_TIES_TO_AWAY
-
Round to the nearest number away from zero.
If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near), the one with larger magnitude will be selected.
-
enumerator
ROUND_NEAREST_TIES_TO_EVEN
-
std
::
ostream
&
cvc5
::
operator
<<
(
std
::
ostream
&
out
,
RoundingMode
rm
)
-
Serialize a RoundingMode to given stream.
- Parameters :
-
-
out – The output stream
-
rm – The rounding mode to be serialized to the given output stream
-
- Returns :
-
The output stream
-
std
::
string
std
::
to_string
(
cvc5
::
RoundingMode
rm
)