val is_rounding_mode : Expr.t -> boolval fpa_rounding_mode : Ty.tval _NearestTiesToEven__rounding_mode : Expr.tne in Gappa: to nearest, tie breaking to even mantissas
val _ToZero__rounding_mode : Expr.tzr in Gappa: toward zero
val _Up__rounding_mode : Expr.tup in Gappa: toward plus infinity
val _Down__rounding_mode : Expr.tdn in Gappa: toward minus infinity
val _NearestTiesToAway__rounding_mode : Expr.tna : to nearest, tie breaking away from zero
val _Aw__rounding_mode : Expr.taw in Gappa: away from zero *
val _Od__rounding_mode : Expr.tod in Gappa: to odd mantissas
val _No__rounding_mode : Expr.tno in Gappa: to nearest, tie breaking to odd mantissas
val _Nz__rounding_mode : Expr.tnz in Gappa: to nearest, tie breaking toward zero
val _Nd__rounding_mode : Expr.tnd in Gappa: to nearest, tie breaking toward minus infinity
val _Nu__rounding_mode : Expr.tnu in Gappa: to nearest, tie breaking toward plus infinity
val integer_log_2 : Numbers.Q.t -> intInteger 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 * 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 : Expr.t -> Numbers.Q.t -> Numbers.Q.tround_to_integer mode x rounds the rational x to an integer depending on the rounding mode mode