BitwuzlaRoundingMode
-
enum BitwuzlaRoundingMode
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 BITWUZLA_RM_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 BITWUZLA_RM_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 BITWUZLA_RM_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 BITWUZLA_RM_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 BITWUZLA_RM_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
-
enumerator BITWUZLA_RM_RNE
-
const char *bitwuzla_rm_to_string(BitwuzlaRoundingMode rm)
Get the string representation of a rounding mode.
Note
The returned char* pointer is only valid until the next
bitwuzla_rm_to_string
call.- Returns:
A string representation of the rounding mode.