Undocumented
Class | FPV |
Undocumented |
Class |
|
Undocumented |
Class | RM |
Undocumented |
Function | compare |
Undocumented |
Function | fp |
Returns the absolute value of the floating point `x`. So: |
Function | fp |
Returns the addition of two floating point numbers, `a` and `b`. |
Function | fp |
Returns the division of the floating point `a` by the floating point `b`. |
Function | fp |
Checks if floating point `a` is equal to floating point `b`. |
Function | fp |
Concatenates the bitvectors `sgn`, `exp` and `mantissa` and returns the corresponding IEEE754 floating point number. |
Function | fp |
Checks if floating point `a` is greater than or equal to floating point `b`. |
Function | fp |
Checks if floating point `a` is greater than floating point `b`. |
Function | fp |
Checks whether the argument is a floating point infinity. |
Function | fp |
Checks whether the argument is a floating point NaN. |
Function | fp |
Checks if floating point `a` is less than or equal to floating point `b`. |
Function | fp |
Checks if floating point `a` is less than floating point `b`. |
Function | fp |
Returns the multiplication of two floating point numbers, `a` and `b`. |
Function | fp |
Checks if floating point `a` is not equal to floating point `b`. |
Function | fp |
Returns the additive inverse of the floating point `x`. So: |
Function | fp |
Returns the subtraction of the floating point `a` by the floating point `b`. |
Function | fp |
Returns a FP AST and has three signatures: |
Function | fp |
Returns a FP AST whose value is the same as the unsigned BVV `thing` and whose sort is `sort`. |
Function | fp |
Interprets the bit-pattern of the IEEE754 floating point number `fpv` as a bitvector. |
Function | fp |
Undocumented |
Function | fp |
Undocumented |
Function | normalize |
Undocumented |
Constant | FSORT |
Undocumented |
Constant | FSORT |
Undocumented |
Returns the absolute value of the floating point `x`. So: a = FPV(-3.2, FSORT_DOUBLE) b = fpAbs(a) b is FPV(3.2, FSORT_DOUBLE)
Concatenates the bitvectors `sgn`, `exp` and `mantissa` and returns the corresponding IEEE754 floating point number. :return: A FP AST whose bit-pattern is the same as the concatenated bitvector
Returns the additive inverse of the floating point `x`. So: a = FPV(3.2, FSORT_DOUBLE) b = fpAbs(a) b is FPV(-3.2, FSORT_DOUBLE)
Returns a FP AST and has three signatures: fpToFP(ubvv, sort) Returns a FP AST whose value is the same as the unsigned BVV `a1` and whose sort is `a2`. fpToFP(rm, fpv, sort) Returns a FP AST whose value is the same as the floating point `a2` and whose sort is `a3`. fpToTP(rm, sbvv, sort) Returns a FP AST whose value is the same as the signed BVV `a2` and whose sort is `a3`.