AltErgoLib.Fpa_rounding
val is_rounding_mode : Expr.t -> bool
val fpa_rounding_mode : Ty.t
val _NearestTiesToEven__rounding_mode : Expr.t
ne in Gappa: to nearest, tie breaking to even mantissas
val _ToZero__rounding_mode : Expr.t
zr in Gappa: toward zero
val _Up__rounding_mode : Expr.t
up in Gappa: toward plus infinity
val _Down__rounding_mode : Expr.t
dn in Gappa: toward minus infinity
val _NearestTiesToAway__rounding_mode : Expr.t
na : to nearest, tie breaking away from zero
val _Aw__rounding_mode : Expr.t
aw in Gappa: away from zero *
val _Od__rounding_mode : Expr.t
od in Gappa: to odd mantissas
val _No__rounding_mode : Expr.t
no in Gappa: to nearest, tie breaking to odd mantissas
val _Nz__rounding_mode : Expr.t
nz in Gappa: to nearest, tie breaking toward zero
val _Nd__rounding_mode : Expr.t
nd in Gappa: to nearest, tie breaking toward minus infinity
val _Nu__rounding_mode : Expr.t
nu in Gappa: to nearest, tie breaking toward plus infinity
val integer_log_2 : Numbers.Q.t -> int
Integer part of binary logarithm for NON-ZERO POSITIVE number *
val float_of_rational :
Expr.t ->
Expr.t ->
Expr.t ->
Numbers.Q.t ->
Numbers.Q.t * Numbers.Z.t * int
float_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 : Expr.t -> Numbers.Q.t -> Numbers.Q.t
round_to_integer mode x
rounds the rational x
to an integer depending on the rounding mode mode