Module `Term.Rm`

Rounding-mode

type t = rm term: A rounding-mode term.

type 'a operator = | Rne : rm term operator 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 | Rna : rm term operator 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 | Rtn : rm term operator 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 | Rtp : rm term operator 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 | Rtz : rm term operator 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

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. The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE Standard 754.

val term : 'a operator -> 'a

term op create a rounding-mode term of given kind.

parameter op: The operator kind.

returns: A term representing an operation of given kind.

val rne : t: Same as term Rne

val rna : t: Same as term Rna

val rtn : t: Same as term Rtn

val rtp : t: Same as term Rtp

val rtz : t: Same as term Rtz

`\|` `Rne : rm term operator`	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
`\|` `Rna : rm term operator`	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
`\|` `Rtn : rm term operator`	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
`\|` `Rtp : rm term operator`	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
`\|` `Rtz : rm term operator`	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