module DE = Dolmen.Std.ExprThe rounding modes for the Floating Point Arithmetic theory. In the legacy frontend, the rounding mode type was `fpa_rounding_mode` and defined 5 rounding modes (see the rounding_mode type below). The SMT2 standard defines the exact same rounding modes, but with different identifiers.
val compare_rounding_mode :
rounding_mode ->
rounding_mode ->
Ppx_deriving_runtime.intEqual to "fpa_rounding_mode", the Alt-Ergo native rounding mode type.
val fpa_rounding_mode_dty : Dolmen.Std.Expr.Ty.tThe Dolmen rounding mode type.
val d_constrs :
(AltErgoLib.Uid.DE.term_cst
* (AltErgoLib.Uid.DE.ty * AltErgoLib.Uid.DE.term_cst option) list)
listThe Dolmen constructors of rounding_mode.
val fpa_rounding_mode : Ty.tThe rounding mode type.
val rounding_mode_of_smt_hs : Hstring.t -> rounding_modeTransforms the Hstring corresponding to a RoundingMode element into the rounding_mode equivalent. Raises 'Failure' if the string does not correspond to a valid rounding mode.
val rounding_mode_of_ae_hs : Hstring.t -> rounding_modeSame, but for legacy's rounding_mode equivalent.
Same, but from AE modes to SMT2 modes.
val string_of_rounding_mode : rounding_mode -> stringReturns the string representation of the rounding_mode (SMT2 standard)
val integer_log_2 : Numbers.Q.t -> intInteger part of binary logarithm for NON-ZERO POSITIVE number *
val float_of_rational :
int ->
int ->
rounding_mode ->
Numbers.Q.t ->
Numbers.Q.t * Numbers.Z.t * intfloat_of_rational prec exp mode x float approx of a rational constant. The function also returns the mantissa and the exponent. i.e. if res, m, e = float_of_rational prec exp mode x, then res = m * 2^e *
val round_to_integer : rounding_mode -> Numbers.Q.t -> Numbers.Q.tround_to_integer mode x rounds the rational x to an integer depending on the rounding mode mode