package dolmen
-
dolmen
-
dolmen_intf
-
-
dolmen_line
-
dolmen_smtlib2
-
dolmen_smtlib2_v6
-
dolmen_std
-
-
dolmen_tptp
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.