Module Typed.Float32

type t = float32 expr
val zero : t
val v : int32 -> t

v bits creates a float32 from the raw integer bits.

val of_float : float -> t

of_float f creates a float32 from an OCaml float value.

val of_int32_bits : int32 -> t

of_int32_bits bits is an alias for v.

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 float32.

val convert_i32_u : bitv32 expr -> t

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

val convert_i64_s : bitv64 expr -> t

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

val convert_i64_u : bitv64 expr -> t

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

val demote_f64 : float64 expr -> t

demote_f64 t converts a float64 to float32 (may lose precision).

val reinterpret_i32 : bitv32 expr -> t

reinterpret_i32 i reinterprets the bits of a 32-bit integer as a float32.

val to_bv : t -> bitv32 expr

to_bv t reinterprets the float32 t as a raw 32-bit bitvector.

val pp : t Fmt.t