module documentation

Undocumented

Class FPV Undocumented
Class FSort Undocumented
Class RM Undocumented
Function compare_sorts Undocumented
Function fpAbs Returns the absolute value of the floating point `x`. So:
Function fpAdd Returns the addition of two floating point numbers, `a` and `b`.
Function fpDiv Returns the division of the floating point `a` by the floating point `b`.
Function fpEQ Checks if floating point `a` is equal to floating point `b`.
Function fpFP Concatenates the bitvectors `sgn`, `exp` and `mantissa` and returns the corresponding IEEE754 floating point number.
Function fpGEQ Checks if floating point `a` is greater than or equal to floating point `b`.
Function fpGT Checks if floating point `a` is greater than floating point `b`.
Function fpIsInf Checks whether the argument is a floating point infinity.
Function fpIsNaN Checks whether the argument is a floating point NaN.
Function fpLEQ Checks if floating point `a` is less than or equal to floating point `b`.
Function fpLT Checks if floating point `a` is less than floating point `b`.
Function fpMul Returns the multiplication of two floating point numbers, `a` and `b`.
Function fpNE Checks if floating point `a` is not equal to floating point `b`.
Function fpNeg Returns the additive inverse of the floating point `x`. So:
Function fpSub Returns the subtraction of the floating point `a` by the floating point `b`.
Function fpToFP Returns a FP AST and has three signatures:
Function fpToFPUnsigned Returns a FP AST whose value is the same as the unsigned BVV `thing` and whose sort is `sort`.
Function fpToIEEEBV Interprets the bit-pattern of the IEEE754 floating point number `fpv` as a bitvector.
Function fpToSBV Undocumented
Function fpToUBV Undocumented
Function normalize_types Undocumented
Constant FSORT_DOUBLE Undocumented
Constant FSORT_FLOAT Undocumented
def compare_sorts(f): (source)

Undocumented

def fpAbs(x): (source)

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)

def fpAdd(_rm, a, b): (source)

Returns the addition of two floating point numbers, `a` and `b`.

def fpDiv(_rm, a, b): (source)

Returns the division of the floating point `a` by the floating point `b`.

def fpEQ(a, b): (source)

Checks if floating point `a` is equal to floating point `b`.

def fpFP(sgn, exp, mantissa): (source)

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

def fpGEQ(a, b): (source)

Checks if floating point `a` is greater than or equal to floating point `b`.

def fpGT(a, b): (source)

Checks if floating point `a` is greater than floating point `b`.

def fpIsInf(x): (source)

Checks whether the argument is a floating point infinity.

def fpIsNaN(x): (source)

Checks whether the argument is a floating point NaN.

def fpLEQ(a, b): (source)

Checks if floating point `a` is less than or equal to floating point `b`.

def fpLT(a, b): (source)

Checks if floating point `a` is less than floating point `b`.

def fpMul(_rm, a, b): (source)

Returns the multiplication of two floating point numbers, `a` and `b`.

def fpNE(a, b): (source)

Checks if floating point `a` is not equal to floating point `b`.

def fpNeg(x): (source)

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)

def fpSub(_rm, a, b): (source)

Returns the subtraction of the floating point `a` by the floating point `b`.

def fpToFP(a1, a2, a3=None): (source)

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

def fpToFPUnsigned(_rm, thing, sort): (source)

Returns a FP AST whose value is the same as the unsigned BVV `thing` and whose sort is `sort`.

def fpToIEEEBV(fpv): (source)

Interprets the bit-pattern of the IEEE754 floating point number `fpv` as a bitvector. :return: A BV AST whose bit-pattern is the same as `fpv`

def fpToSBV(rm, fp, size): (source)

Undocumented

def fpToUBV(rm, fp, size): (source)

Undocumented

def normalize_types(f): (source)

Undocumented

FSORT_DOUBLE = (source)

Undocumented

Value
FSort('DOUBLE', 11, 53)
FSORT_FLOAT = (source)

Undocumented

Value
FSort('FLOAT', 8, 24)