Module Term.Float

Satisfy the required interface for typing smtlib floating points.

include Dolmen_intf.Term.Smtlib_Float_Float with type t := t and type cst := term_cst
val fp : t -> t -> t -> t

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

val abs : t -> t

absolute value

val neg : t -> t

negation

val add : t -> t -> t -> t

add rm f1 f2 addition

val sub : t -> t -> t -> t

sub rm f1 f2 subtraction

val mul : t -> t -> t -> t

mul rm f1 f2 multiplication

val div : t -> t -> t -> t

mul rm f1 f2 division

val fma : t -> t -> t -> t -> t

mul rm f1 f2 fused multiplication and addition

val sqrt : t -> t -> t

sqrt rm f square root

val rem : t -> t -> t

rem f1 f2 remainder

val roundToIntegral : t -> t -> t

roundToIntegral rm f rounding to integral

val min : t -> t -> t

min f1 f2 minimum

val min' : (int * int) -> term_cst

Constant for float min.

val max : t -> t -> t

max f1 f2 maximum

val max' : (int * int) -> term_cst

Constant for float max.

val leq : t -> t -> t

leq f1 f2 less or equal floating point comparison

val lt : t -> t -> t

lt f1 f2 less than floating point comparison

val geq : t -> t -> t

geq f1 f2 greater or equal floating point comparison

val gt : t -> t -> t

lt f1 f2 greater than floating point comparison

val eq : t -> t -> t

eq f1 f2 floating point equality

val isNormal : t -> t

isNormal f test if it is a normal floating point

val isSubnormal : t -> t

isSubnormal f test if it is a subnormal floating point

val isZero : t -> t

isZero f test if it is a zero

val isInfinite : t -> t

isInfinite f test if it is an infinite

val isNaN : t -> t

isNaN f test if it is NaN

val isNegative : t -> t

isNegative f test if it is a negative floating point

val isPositive : t -> t

isPositive f test if it is a positive floating point

val ieee_format_to_fp : int -> int -> 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 -> t -> t -> t

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

val real_to_fp : int -> int -> t -> t -> t

real_to_fp e s rm r convert from a real

val sbv_to_fp : int -> int -> t -> t -> t

sbv_to_fp e s rm bv convert from a signed integer

val ubv_to_fp : int -> int -> t -> t -> t

ubv_to_fp e s rm bv convert from an unsigned integer

val to_ubv : int -> t -> t -> t

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

val to_ubv' : int -> (int * int) -> term_cst

constant for to_ubv

val to_sbv : int -> t -> t -> t

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

val to_sbv' : int -> (int * int) -> term_cst

constant for to_sbv

val to_real : t -> t

to_real f convert to a real