RoundingMode ¶

class cvc5. RoundingMode ( value ) ¶

The RoundingMode enum

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.

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.

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.

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.

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.