Module Term.FloatSource

Satisfy the required interface for typing smtlib floating points.

include Dolmen_intf.Term.Smtlib_Float_Float with type t := t
Sourceval fp : t -> t -> t -> t

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

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 : t -> t

absolute value

Sourceval neg : t -> t

negation

Sourceval add : t -> t -> t -> t

add rm f1 f2 addition

Sourceval sub : t -> t -> t -> t

sub rm f1 f2 subtraction

Sourceval mul : t -> t -> t -> t

mul rm f1 f2 multiplication

Sourceval div : t -> t -> t -> t

mul rm f1 f2 division

Sourceval fma : t -> t -> t -> t -> t

mul rm f1 f2 fused multiplication and addition

Sourceval sqrt : t -> t -> t

sqrt rm f square root

Sourceval rem : t -> t -> t

rem f1 f2 remainder

Sourceval roundToIntegral : t -> t -> t

roundToIntegral rm f rounding to integral

Sourceval min : t -> t -> t

min f1 f2 minimum

Sourceval max : t -> t -> t

max f1 f2 maximum

Sourceval leq : t -> t -> t

leq f1 f2 less or equal floating point comparison

Sourceval lt : t -> t -> t

lt f1 f2 less than floating point comparison

Sourceval geq : t -> t -> t

geq f1 f2 greater or equal floating point comparison

Sourceval gt : t -> t -> t

lt f1 f2 greater than floating point comparison

Sourceval eq : t -> t -> t

eq f1 f2 floating point equality

Sourceval isNormal : t -> t

isNormal f test if it is a normal floating point

Sourceval isSubnormal : t -> t

isSubnormal f test if it is a subnormal floating point

Sourceval isZero : t -> t

isZero f test if it is a zero

Sourceval isInfinite : t -> t

isInfinite f test if it is an infinite

Sourceval isNaN : t -> t

isNaN f test if it is NaN

Sourceval isNegative : t -> t

isNegative f test if it is a negative floating point

Sourceval isPositive : t -> t

isPositive f test if it is a positive floating point

Sourceval 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)

Sourceval to_fp : int -> int -> t -> t -> t

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

Sourceval real_to_fp : int -> int -> t -> t -> t

real_to_fp e s rm r convert from a real

Sourceval sbv_to_fp : int -> int -> t -> t -> t

sbv_to_fp e s rm bv convert from a signed integer

Sourceval ubv_to_fp : int -> int -> t -> t -> t

ubv_to_fp e s rm bv convert from an unsigned integer

Sourceval to_ubv : int -> t -> t -> t

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

Sourceval to_sbv : int -> t -> t -> t

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

Sourceval to_real : t -> t

to_real f convert to a real