Module Typed.Float64

type t = float64 expr
val zero : t
val v : int64 -> t

v bits creates a float64 from the raw integer bits.

val of_float : float -> t

of_float f creates a float64 from an OCaml float value.

val symbol : Symbol.t -> t
val neg : t -> t

neg t constructs the negation of the floating-point term t.

val abs : t -> t

abs t constructs the absolute value of the floating-point term t.

val sqrt : t -> t

sqrt t constructs the square root of the floating-point term t.

val is_normal : t -> bool expr

is_normal t checks if t is a normal floating point number (not zero, subnormal, infinite, or NaN).

val is_subnormal : t -> bool expr

is_subnormal t checks if t is a subnormal (denormal) number.

val is_negative : t -> bool expr

is_negative t checks if the sign bit of t is set.

val is_positive : t -> bool expr

is_positive t checks if the sign bit of t is unset.

val is_infinite : t -> bool expr

is_infinite t checks if t is +Inf or -Inf.

val is_zero : t -> bool expr

is_zero t checks if t is +0.0 or -0.0.

val is_nan : t -> bool expr

is_nan t checks if t is Not-a-Number (NaN).

val ceil : t -> t

ceil t rounds t to the nearest integer towards positive infinity.

val floor : t -> t

floor t rounds t to the nearest integer towards negative infinity.

val trunc : t -> t

trunc t rounds t to the nearest integer towards zero.

val nearest : t -> t

nearest t rounds t to the nearest integer (ties to even).

val add : t -> t -> t

add t1 t2 computes t1 + t2.

val sub : t -> t -> t

sub t1 t2 computes t1 - t2.

val mul : t -> t -> t

mul t1 t2 computes t1 * t2.

val div : t -> t -> t

div t1 t2 computes t1 / t2.

val min : t -> t -> t

min t1 t2 constructs the minimum of the floating-point terms t1 and t2.

val max : t -> t -> t

max t1 t2 constructs the maximum of the floating-point terms t1 and t2.

val rem : t -> t -> t

rem t1 t2 constructs the remainder of the floating-point terms t1 and t2.

val copy_sign : t -> t -> t

copy_sign x y returns x with the sign of y.

val eq : t -> t -> bool expr

eq t1 t2 performs IEEE-754 equality comparison.

val ne : t -> t -> bool expr

ne t1 t2 performs IEEE-754 inequality comparison.

val lt : t -> t -> bool expr

lt t1 t2 performs IEEE-754 less-than comparison.

val le : t -> t -> bool expr

le t1 t2 performs IEEE-754 less-than-or-equal comparison.

val convert_i32_s : bitv32 expr -> t

convert_i32_s t converts a signed 32-bit integer to float64.

val convert_i32_u : bitv32 expr -> t

convert_i32_u t converts an unsigned 32-bit integer to float64.

val convert_i64_s : bitv64 expr -> t

convert_i64_s t converts a signed 64-bit integer to float64.

val convert_i64_u : bitv64 expr -> t

convert_i64_u t converts an unsigned 64-bit integer to float64.

val promote_f32 : float32 expr -> t

promote_f32 t converts a float32 to float64 (exact conversion).

val reinterpret_i64 : bitv64 expr -> t

reinterpret_i64 i reinterprets the bits of a 64-bit integer as a float64.

val to_bv : t -> bitv64 expr

to_bv t reinterprets the float64 t as a raw 64-bit bitvector.

val pp : t Fmt.t