Module Const.FloatSource

A module for floating point constant symbols that occur in terms.

Sourceval fp : (int * int) -> t

Floating point literal.

Sourceval roundNearestTiesToEven : t

Constant for rounding mode RNE.

Sourceval roundNearestTiesToAway : t

Constant for rounding mode RNA.

Sourceval roundTowardPositive : t

Constant for rounding mode RTP.

Sourceval roundTowardNegative : t

Constant for rounding mode RTN.

Sourceval roundTowardZero : t

Constant for rounding mode RTZ.

Sourceval plus_infinity : (int * int) -> t

The constant plus infinity, it is also equivalent to a literal.

Sourceval minus_infinity : (int * int) -> t

The constant minus infinity, it is also equivalent to a literal.

Sourceval plus_zero : (int * int) -> t

The constant plus zero, it is also equivalent to a literal.

Sourceval minus_zero : (int * int) -> t

The constant minus zero, it is also equivalent to a literal.

Sourceval nan : (int * int) -> t

The constant Non-numbers, it is also equivalent to many literals which are equivalent together.

Sourceval abs : (int * int) -> t

Absolute value.

Sourceval neg : (int * int) -> t

Floating point negation.

Sourceval add : (int * int) -> t

Floating point addition.

Sourceval sub : (int * int) -> t

Floating point subtraction.

Sourceval mul : (int * int) -> t

Floating point multiplication.

Sourceval div : (int * int) -> t

Floating point division.

Sourceval fma : (int * int) -> t

Floating point fused multiplication and addition.

Sourceval sqrt : (int * int) -> t

Floating point square root.

Sourceval rem : (int * int) -> t

Floating point division remainder.

Sourceval roundToIntegral : (int * int) -> t

Floating point rounding to integral.

Sourceval min : (int * int) -> t

Floating point minimum.

Sourceval max : (int * int) -> t

Floating point maximum.

Sourceval lt : (int * int) -> t

Floating point "less than" comparison.

Sourceval leq : (int * int) -> t

Floating point "less or equal" comparison.

Sourceval gt : (int * int) -> t

Floating point "greater than" comparison.

Sourceval geq : (int * int) -> t

Floating point "greater or equal" comparison.

Sourceval eq : (int * int) -> t

Floating point equality.

Sourceval isNormal : (int * int) -> t

Test if a value is a normal floating point.

Sourceval isSubnormal : (int * int) -> t

Test if a value is a subnormal floating point.

Sourceval isZero : (int * int) -> t

Test if a value is a zero.

Sourceval isInfinite : (int * int) -> t

Test if a value is an infinite.

Sourceval isNaN : (int * int) -> t

Test if a value is NaN.

Sourceval isNegative : (int * int) -> t

Test if a value is a negative floating point.

Sourceval isPositive : (int * int) -> t

Test if a value is a positive floating point.

Sourceval to_real : (int * int) -> t

Convert a floating point to a real.

Sourceval ieee_format_to_fp : (int * int) -> t

Convert a bitvector into a floating point using IEEE 754-2008 interchange format.

Sourceval to_fp : (int * int * int * int) -> t

Convert from one floating point format to another.

Sourceval real_to_fp : (int * int) -> t

Convert a real to a floating point.

Sourceval sbv_to_fp : (int * int * int) -> t

Convert a signed bitvector to a floating point.

Sourceval ubv_to_fp : (int * int * int) -> t

Convert an unsigned bitvector to a floating point.

Sourceval to_ubv : (int * int * int) -> t

Convert an floating point to an unsigned bitvector.

Sourceval to_sbv : (int * int * int) -> t

Convert an floating point to an signed bitvector.