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 Numbers.Q.t
val compare : t -> t -> int
val equal : t -> t -> bool
val pp : t Fmt.t

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

val pp_smtlib : eb:int -> sb: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 -> eb:int -> sb:int -> t

mk_fp_literal ~neg ~biased_exp ~mantissa ~eb ~sb creates a floating-point literal where neg is the sign bit, biased_exp is the biased exponent, mantissa is the significand bits (without the hidden bit), eb is the exponent width, and sb is the significand width (including the hidden bit).

val max_finite_q : eb:int -> sb:int -> Numbers.Q.t

max_finite_q ~eb ~sb is the largest finite value of the format (eb, sb).

val min_normal_q : eb:int -> Numbers.Q.t

min_normal_q ~eb is the smallest positive normal value of the formats with eb exponent bits.

val is_normal : eb:int -> t -> bool

is_normal ~eb v holds if v is a normal value of a format with eb exponent bits.

val is_subnormal : eb:int -> t -> bool

is_subnormal ~eb v holds if v is a subnormal value of a format with eb exponent bits.