Module Make.Float

module Rounding_mode : sig ... end

Rounding modes for floating-point operations.

val v : float -> int -> int -> term

v f e s constructs a floating-point term from the float f with exponent width e and significand width s.

val neg : term -> term

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

val abs : term -> term

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

val sqrt : rm:term -> term -> term

sqrt ~rm t constructs the square root of the floating-point term t using the rounding mode rm.

val is_normal : term -> term
val is_subnormal : term -> term
val is_negative : term -> term
val is_positive : term -> term
val is_infinite : term -> term
val is_zero : term -> term
val is_nan : term -> term

is_nan t checks if the floating-point term t is NaN.

val round_to_integral : rm:term -> term -> term

round_to_integral ~rm t rounds the floating-point term t to an integral value using the rounding mode rm.

val add : rm:term -> term -> term -> term

add ~rm t1 t2 constructs the sum of the floating-point terms t1 and t2 using the rounding mode rm.

val sub : rm:term -> term -> term -> term

sub ~rm t1 t2 constructs the difference of the floating-point terms t1 and t2 using the rounding mode rm.

val mul : rm:term -> term -> term -> term

mul ~rm t1 t2 constructs the product of the floating-point terms t1 and t2 using the rounding mode rm.

val div : rm:term -> term -> term -> term

div ~rm t1 t2 constructs the quotient of the floating-point terms t1 and t2 using the rounding mode rm.

val min : term -> term -> term

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

val max : term -> term -> term

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

val fma : rm:term -> term -> term -> term -> term

fma ~rm a b c

val rem : term -> term -> term

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

val eq : term -> term -> term

eq t1 t2 constructs the equality of the floating-point terms t1 and t2.

val lt : term -> term -> term

lt t1 t2 constructs the less-than relation between floating-point terms t1 and t2.

val le : term -> term -> term

le t1 t2 constructs the less-than-or-equal relation between floating-point terms t1 and t2.

val gt : term -> term -> term

gt t1 t2 constructs the greater-than relation between floating-point terms t1 and t2.

val ge : term -> term -> term

ge t1 t2 constructs the greater-than-or-equal relation between floating-point terms t1 and t2.

val to_fp : int -> int -> rm:term -> term -> term

to_fp e s ~rm t converts the term t to a floating-point term with exponent width e and significand width s using the rounding mode rm.

val sbv_to_fp : int -> int -> rm:term -> term -> term

sbv_to_fp e s ~rm t converts the signed bitvector term t to a floating-point term with exponent width e and significand width s using the rounding mode rm.

val ubv_to_fp : int -> int -> rm:term -> term -> term

ubv_to_fp e s ~rm t converts the unsigned bitvector term t to a floating-point term with exponent width e and significand width s using the rounding mode rm.

val to_ubv : int -> rm:term -> term -> term

to_ubv n ~rm t converts the floating-point term t to an unsigned bitvector term of width n using the rounding mode rm.

val to_sbv : int -> rm:term -> term -> term

to_sbv n ~rm t converts the floating-point term t to a signed bitvector term of width n using the rounding mode rm.

val of_ieee_bv : int -> int -> term -> term

of_ieee_bv e s t constructs a floating-point term from the IEEE bitvector term t with exponent width e and significand width s.

val to_ieee_bv : (term -> term) option

to_ieee_bv t converts the floating-point term t to an IEEE bitvector term.