RoundingMode

namespace bitwuzla {

enum class bitwuzla::RoundingMode

Rounding mode for floating-point operations.

For some floating-point operations, infinitely precise results may not be representable in a given format. Hence, they are rounded modulo one of five rounding modes to a representable floating-point number.

The following rounding modes 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 RNE

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.

SMT-LIB: RNE roundNearestTiesToEven

enumerator RNA

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.

SMT-LIB: RNA roundNearestTiesToAway

enumerator RTN

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.

SMT-LIB: RTN roundTowardNegative

enumerator RTP

Round towards positive infinity (+oo). The result shall be the format’s floating-point number (possibly +oo) closest to and no less than the infinitely precise result.

SMT-LIB: RTP roundTowardPositive

enumerator RTZ

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.

SMT-LIB: RTZ roundTowardZero

std::ostream &bitwuzla::operator<<(std::ostream &out, RoundingMode rm)

Print rounding mode to output stream.

Parameters:

  • out – The output stream.

  • rm – The rounding mode.

Returns:

The output stream.

}

namespace std {

std::string std::to_string(bitwuzla::RoundingMode rm)

Get string representation of given rounding mode.

Parameters:

rm – The roundingmode.

Returns:

The string representation.

}