package smtml

  1. Overview
  2. Docs
package smtml
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Make.FloatSource

Sourcemodule Rounding_mode : sig ... end

Rounding modes for floating-point operations.

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

Sourceval neg : term -> term

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

Sourceval abs : term -> term

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

Sourceval sqrt : rm:term -> term -> term

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

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

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

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

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

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

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

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

Sourceval min : term -> term -> term

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

Sourceval max : term -> term -> term

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

Sourceval fma : rm:term -> term -> term -> term -> term

fma ~rm a b c

Sourceval rem : term -> term -> term

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

Sourceval eq : term -> term -> term

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

Sourceval lt : term -> term -> term

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

Sourceval le : term -> term -> term

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

Sourceval gt : term -> term -> term

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

Sourceval ge : term -> term -> term

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

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

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

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

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

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

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

Sourceval to_ieee_bv : (term -> term) option

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