Module AltErgoLib.Fp_value

Literal floating-point values.

type t =
  1. | Plus_infinity
  2. | Minus_infinity
  3. | Plus_zero
  4. | Minus_zero
  5. | NaN
  6. | Finite of {
    1. neg : bool;
    2. biased_exp : int;
    3. significand : Z.t;
    }
val compare : t -> t -> int
val pp : t Fmt.t

pp ppf v prints the concrete FP value v in the Alt-Ergo native format.

val pp_smtlib : int -> int -> t Fmt.t

pp_smtlib eb sb ppf v prints the concrete FP value v of precision (eb, sb) in the SMT-LIB format.

val mk_fp_literal : neg:bool -> biased_exp:int -> mantissa:Z.t -> int -> t

mk_fp_literal neg biased_exp mantissa e creates a floating-point literal with the geiven parameters, where neg is the sign bit, biased_exp is the biased exponent, mantissa is the mantissa bits (without the hidden bit), e is the exponent width.