Module AltErgoLib.Fpa_rounding

module DE = Dolmen.Std.Expr
type rounding_mode = Dolmen.Std.Builtin.Float.rounding_mode

We reuse Dolmen's own representation of the rounding modes.

val compare_rounding_mode : rounding_mode -> rounding_mode -> int
val fpa_rounding_mode_type_name : string

Equal to "RoundingMode", the SMT2 type of rounding modes.

val fpa_rounding_mode_ae_type_name : string

Equal to "fpa_rounding_mode", the Alt-Ergo native rounding mode type.

val fpa_rounding_mode_dty : Dolmen.Std.Expr.Ty.t

The Dolmen rounding mode type.

val d_constrs : DE.term_cst list

The Dolmen constructors of rounding_mode.

val fpa_rounding_mode : Ty.t

The rounding mode type.

val rounding_mode_of_smt : string -> rounding_mode

Transforms the string 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 : string -> rounding_mode

Same, but for legacy's rounding_mode equivalent.

val translate_smt_rounding_mode : string -> string option

Same, but from AE modes to SMT2 modes.

val string_of_rounding_mode : rounding_mode -> string

Returns the string representation of the rounding_mode (SMT2 standard)

val term_cst_of_rounding_mode : rounding_mode -> Dolmen.Std.Expr.term_cst

Returns the Dolmen constructor associated with the rounding mode.

val integer_log_2 : Numbers.Q.t -> int

Integer part of binary logarithm for NON-ZERO POSITIVE number *

val mult_x_by_2_pow_n : Numbers.Q.t -> int -> Numbers.Q.t

mult_x_by_2_pow_n x n is x * 2^n.

val float_of_rational : int -> int -> rounding_mode -> 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 : int -> int -> rounding_mode -> Numbers.Q.t -> Numbers.Q.t

round prec exp mode x is the first component of float_of_rational prec exp mode x.

val succ : int -> int -> Numbers.Q.t -> Numbers.Q.t

succ prec exp x is the next float of the format after x, which must be a float of the format.

val pred : int -> int -> Numbers.Q.t -> Numbers.Q.t

pred prec exp x is the float of the format before x, which must be a float of the format.

val round_to_integer : rounding_mode -> Numbers.Q.t -> Numbers.Q.t

round_to_integer mode x rounds the rational x to an integer depending on the rounding mode mode

val empty_cache : unit -> unit

Empties the module's inner cache