dolmen_type 0.7 · OCaml Package

Sub-module used for namespacing the floating number part of the theory requirements

val fp : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

Construct a floating point from bitvector literals (sign, exponent, significand). The sign should be of size 1.

val roundNearestTiesToEven : Type.T.t

constant for rounding mode RNE

val roundNearestTiesToAway : Type.T.t

constant for rounding mode RNA

val roundTowardPositive : Type.T.t

constant for rounding mode RTP

val roundTowardNegative : Type.T.t

constant for rounding mode RTN

val roundTowardZero : Type.T.t

constant for rounding mode RTZ

val plus_infinity : int -> int -> Type.T.t

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

val minus_infinity : int -> int -> Type.T.t

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

val plus_zero : int -> int -> Type.T.t

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

val minus_zero : int -> int -> Type.T.t

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

val nan : int -> int -> Type.T.t

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

val abs : Type.T.t -> Type.T.t

absolute value

val neg : Type.T.t -> Type.T.t

negation

val add : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

add rm f1 f2 addition

val sub : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

sub rm f1 f2 subtraction

val mul : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

mul rm f1 f2 multiplication

val div : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

mul rm f1 f2 division

val fma : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

mul rm f1 f2 fused multiplication and addition

val sqrt : Type.T.t -> Type.T.t -> Type.T.t

sqrt rm f square root

val rem : Type.T.t -> Type.T.t -> Type.T.t

rem f1 f2 remainder

val roundToIntegral : Type.T.t -> Type.T.t -> Type.T.t

roundToIntegral rm f rounding to integral

val min : Type.T.t -> Type.T.t -> Type.T.t

min f1 f2 minimum

val max : Type.T.t -> Type.T.t -> Type.T.t

max f1 f2 maximum

val leq : Type.T.t -> Type.T.t -> Type.T.t

leq f1 f2 less or equal floating point comparison

val lt : Type.T.t -> Type.T.t -> Type.T.t

lt f1 f2 less than floating point comparison

val geq : Type.T.t -> Type.T.t -> Type.T.t

geq f1 f2 greater or equal floating point comparison

val gt : Type.T.t -> Type.T.t -> Type.T.t

lt f1 f2 greater than floating point comparison

val eq : Type.T.t -> Type.T.t -> Type.T.t

eq f1 f2 floating point equality

val isNormal : Type.T.t -> Type.T.t

isNormal f test if it is a normal floating point

val isSubnormal : Type.T.t -> Type.T.t

isSubnormal f test if it is a subnormal floating point

val isZero : Type.T.t -> Type.T.t

isZero f test if it is a zero

val isInfinite : Type.T.t -> Type.T.t

isInfinite f test if it is an infinite

val isNaN : Type.T.t -> Type.T.t

isNaN f test if it is NaN

val isNegative : Type.T.t -> Type.T.t

isNegative f test if it is a negative floating point

val isPositive : Type.T.t -> Type.T.t

isPositive f test if it is a positive floating point

val ieee_format_to_fp : int -> int -> Type.T.t -> Type.T.t

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)

val to_fp : int -> int -> Type.T.t -> Type.T.t -> Type.T.t

to_fp e s rm f convert from one floating point format to another

val real_to_fp : int -> int -> Type.T.t -> Type.T.t -> Type.T.t

real_to_fp e s rm r convert from a real

val sbv_to_fp : int -> int -> Type.T.t -> Type.T.t -> Type.T.t

sbv_to_fp e s rm bv convert from a signed integer

val ubv_to_fp : int -> int -> Type.T.t -> Type.T.t -> Type.T.t

ubv_to_fp e s rm bv convert from an unsigned integer

val to_ubv : int -> Type.T.t -> Type.T.t -> Type.T.t

to_ubv m rm f convert to an unsigned integer (bitvector of size m)

val to_sbv : int -> Type.T.t -> Type.T.t -> Type.T.t

to_ubv m rm f convert to a signed integer (bitvector of size m)

val to_real : Type.T.t -> Type.T.t

to_real f convert to a real

package dolmen_type