FP Expressions. More...
Public Member Functions | |
def | sort (self) |
def | ebits (self) |
def | sbits (self) |
def | as_string (self) |
def | __le__ (self, other) |
def | __lt__ (self, other) |
def | __ge__ (self, other) |
def | __gt__ (self, other) |
def | __add__ (self, other) |
def | __radd__ (self, other) |
def | __sub__ (self, other) |
def | __rsub__ (self, other) |
def | __mul__ (self, other) |
def | __rmul__ (self, other) |
def | __pos__ (self) |
def | __neg__ (self) |
def | __div__ (self, other) |
def | __rdiv__ (self, other) |
def | __truediv__ (self, other) |
def | __rtruediv__ (self, other) |
def | __mod__ (self, other) |
def | __rmod__ (self, other) |
![]() | |
def | as_ast (self) |
def | get_id (self) |
def | sort (self) |
def | sort_kind (self) |
def | __eq__ (self, other) |
def | __hash__ (self) |
def | __ne__ (self, other) |
def | params (self) |
def | decl (self) |
def | num_args (self) |
def | arg (self, idx) |
def | children (self) |
![]() | |
def | __init__ (self, ast, ctx=None) |
def | __del__ (self) |
def | __deepcopy__ (self, memo={}) |
def | __str__ (self) |
def | __repr__ (self) |
def | __eq__ (self, other) |
def | __hash__ (self) |
def | __nonzero__ (self) |
def | __bool__ (self) |
def | sexpr (self) |
def | as_ast (self) |
def | get_id (self) |
def | ctx_ref (self) |
def | eq (self, other) |
def | translate (self, target) |
def | __copy__ (self) |
def | hash (self) |
![]() | |
def | use_pp (self) |
Additional Inherited Members | |
![]() | |
ast | |
ctx | |
def __add__ | ( | self, | |
other | |||
) |
Create the Z3 expression `self + other`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x + y x + y >>> (x + y).sort() FPSort(8, 24)
Definition at line 8841 of file z3py.py.
def __div__ | ( | self, | |
other | |||
) |
Create the Z3 expression `self / other`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x / y x / y >>> (x / y).sort() FPSort(8, 24) >>> 10 / y 1.25*(2**3) / y
Definition at line 8928 of file z3py.py.
Referenced by ArithRef.__truediv__(), BitVecRef.__truediv__(), and FPRef.__truediv__().
def __ge__ | ( | self, | |
other | |||
) |
def __gt__ | ( | self, | |
other | |||
) |
def __le__ | ( | self, | |
other | |||
) |
def __lt__ | ( | self, | |
other | |||
) |
def __mod__ | ( | self, | |
other | |||
) |
def __mul__ | ( | self, | |
other | |||
) |
Create the Z3 expression `self * other`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x * y x * y >>> (x * y).sort() FPSort(8, 24) >>> 10 * y 1.25*(2**3) * y
Definition at line 8887 of file z3py.py.
def __neg__ | ( | self | ) |
def __pos__ | ( | self | ) |
def __radd__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other + self`. >>> x = FP('x', FPSort(8, 24)) >>> 10 + x 1.25*(2**3) + x
def __rdiv__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other / self`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x / y x / y >>> x / 10 x / 1.25*(2**3)
Definition at line 8943 of file z3py.py.
Referenced by ArithRef.__rtruediv__(), BitVecRef.__rtruediv__(), and FPRef.__rtruediv__().
def __rmod__ | ( | self, | |
other | |||
) |
def __rmul__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other * self`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x * y x * y >>> x * 10 x * 1.25*(2**3)
Definition at line 8902 of file z3py.py.
def __rsub__ | ( | self, | |
other | |||
) |
Create the Z3 expression `other - self`. >>> x = FP('x', FPSort(8, 24)) >>> 10 - x 1.25*(2**3) - x
Definition at line 8877 of file z3py.py.
def __rtruediv__ | ( | self, | |
other | |||
) |
def __sub__ | ( | self, | |
other | |||
) |
Create the Z3 expression `self - other`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x - y x - y >>> (x - y).sort() FPSort(8, 24)
Definition at line 8864 of file z3py.py.
def __truediv__ | ( | self, | |
other | |||
) |
def as_string | ( | self | ) |
Return a Z3 floating point expression as a Python string.
Reimplemented in FPNumRef.
Definition at line 8825 of file z3py.py.
Referenced by IntNumRef.as_long(), BitVecNumRef.as_long(), and FiniteDomainNumRef.as_long().
def ebits | ( | self | ) |
Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. >>> b = FPSort(8, 24) >>> b.ebits() 8
Definition at line 8809 of file z3py.py.
Referenced by FPRef.ebits().
def sbits | ( | self | ) |
Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. >>> b = FPSort(8, 24) >>> b.sbits() 24
Definition at line 8817 of file z3py.py.
Referenced by FPRef.sbits().
def sort | ( | self | ) |
Return the sort of the floating-point expression `self`. >>> x = FP('1.0', FPSort(8, 24)) >>> x.sort() FPSort(8, 24) >>> x.sort() == FPSort(8, 24) True
Reimplemented from ExprRef.
Definition at line 8798 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__div__(), QuantifierRef.__getitem__(), FPRef.__mul__(), FPRef.__sub__(), FPNumRef.as_string(), ArrayRef.domain(), FPRef.ebits(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), FPRef.sbits(), BitVecRef.size(), and ExprRef.sort_kind().