package dolmen
Sub-module used for namespacing the floating number part of the theory requirements
Construct a floating point from bitvector literals (sign, exponent, significand). The sign should be of size 1.
val roundNearestTiesToEven : t
constant for rounding mode RNE
val roundNearestTiesToAway : t
constant for rounding mode RNA
val roundTowardPositive : t
constant for rounding mode RTP
val roundTowardNegative : t
constant for rounding mode RTN
val roundTowardZero : t
constant for rounding mode RTZ
val plus_infinity : int -> int -> t
The constant plus infinity, it is also equivalent to a literal
val minus_infinity : int -> int -> t
The constant minus infinity, it is also equivalent to a literal
val plus_zero : int -> int -> t
The constant plus zero, it is also equivalent to a literal
val minus_zero : int -> int -> t
The constant minus zero, it is also equivalent to a literal
val nan : int -> int -> t
The constant Non-numbers, it is also equivalent to many literals which are equivalent together
ieee_format_to_fp e s bv
Convert a bitvector into a floating point using IEEE 754-2008 interchange format. (reinterpret the bitvector into floating-point)
to_fp e s rm f
convert from one floating point format to another