RoundingMode ¶

enum
cvc5
::
RoundingMode
¶

Rounding modes for floatingpoint numbers.
For many floatingpoint 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 floatingpoint numbers.
These rounding modes directly follow the SMTLIB theory for floatingpoint 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 floatingpoint 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 (SMTLIB:
+oo
).The result shall be the format’s floatingpoint 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 floatingpoint 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 floatingpoint 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 floatingpoint numbers bracketing an unrepresentable infinitely precise result are equally near, the one with larger magnitude will be selected.

enumerator
ROUND_NEAREST_TIES_TO_EVEN
¶