package smtml

Rounding modes for floating-point operations.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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.

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.

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

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

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.

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