package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

val fp : (int * int) -> t

Floating point literal.

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.

val abs : (int * int) -> t

Absolute value.

val neg : (int * int) -> t

Floating point negation.

val add : (int * int) -> t

Floating point addition.

val sub : (int * int) -> t

Floating point subtraction.

val mul : (int * int) -> t

Floating point multiplication.

val div : (int * int) -> t

Floating point division.

val fma : (int * int) -> t

Floating point fused multiplication and addition.

val sqrt : (int * int) -> t

Floating point square root.

val rem : (int * int) -> t

Floating point division remainder.

val roundToIntegral : (int * int) -> t

Floating point rounding to integral.

val min : (int * int) -> t

Floating point minimum.

val max : (int * int) -> t

Floating point maximum.

val lt : (int * int) -> t

Floating point "less than" comparison.

val leq : (int * int) -> t

Floating point "less or equal" comparison.

val gt : (int * int) -> t

Floating point "greater than" comparison.

val geq : (int * int) -> t

Floating point "greater or equal" comparison.

val eq : (int * int) -> t

Floating point equality.

val isNormal : (int * int) -> t

Test if a value is a normal floating point.

val isSubnormal : (int * int) -> t

Test if a value is a subnormal floating point.

val isZero : (int * int) -> t

Test if a value is a zero.

val isInfinite : (int * int) -> t

Test if a value is an infinite.

val isNaN : (int * int) -> t

Test if a value is NaN.

val isNegative : (int * int) -> t

Test if a value is a negative floating point.

val isPositive : (int * int) -> t

Test if a value is a positive floating point.

val to_real : (int * int) -> t

Convert a floating point to a real.

val ieee_format_to_fp : (int * int) -> t

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

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

Convert from one floating point format to another.

val real_to_fp : (int * int) -> t

Convert a real to a floating point.

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

Convert a signed bitvector to a floating point.

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

Convert an unsigned bitvector to a floating point.

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

Convert an floating point to an unsigned bitvector.

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

Convert an floating point to an signed bitvector.