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.

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)