Module Expr.FP

Constructors from the smtlib theory of floating-point numbers.

https://smt-lib.org/theories-FloatingPoint.shtml

module Names : sig ... end
val fp : t -> t -> t -> int -> int -> t
val ieee_format_to_fp : t -> int -> int -> t

Arithmetic with rounding mode

val add : eb:int -> sb:int -> mode:t -> t -> t -> t
val sub : eb:int -> sb:int -> mode:t -> t -> t -> t
val mul : eb:int -> sb:int -> mode:t -> t -> t -> t
val div : eb:int -> sb:int -> mode:t -> t -> t -> t
val fma : eb:int -> sb:int -> mode:t -> t -> t -> t -> t
val sqrt : eb:int -> sb:int -> mode:t -> t -> t
val round_to_integral : eb:int -> sb:int -> mode:t -> t -> t
val of_real : eb:int -> sb:int -> mode:t -> t -> t

Arithmetic without rounding mode

val abs : eb:int -> sb:int -> t -> t
val neg : eb:int -> sb:int -> t -> t
val min : eb:int -> sb:int -> t -> t -> t
val max : eb:int -> sb:int -> t -> t -> t

Comparisons

val le : eb:int -> sb:int -> t -> t -> t
val lt : eb:int -> sb:int -> t -> t -> t
val ge : eb:int -> sb:int -> t -> t -> t
val gt : eb:int -> sb:int -> t -> t -> t
val eq : eb:int -> sb:int -> t -> t -> t

Predicates

val is_normal : eb:int -> sb:int -> t -> t
val is_subnormal : eb:int -> sb:int -> t -> t
val is_zero : eb:int -> sb:int -> t -> t
val is_infinite : eb:int -> sb:int -> t -> t
val is_nan : eb:int -> sb:int -> t -> t
val is_negative : eb:int -> sb:int -> t -> t
val is_positive : eb:int -> sb:int -> t -> t
val is_finite : eb:int -> sb:int -> t -> t

Real conversion

val to_real : eb:int -> sb:int -> t -> t