FP Expressions.
Floating-point expressions.
Definition at line 8852 of file z3py.py.
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 8898 of file z3py.py.
8898 def __add__(self, other):
8899 """Create the Z3 expression `self + other`.
8901 >>> x = FP('x', FPSort(8, 24))
8902 >>> y = FP('y', FPSort(8, 24))
8908 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8909 return fpAdd(_dflt_rm(), a, b, self.ctx)
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 8985 of file z3py.py.
8985 def __div__(self, other):
8986 """Create the Z3 expression `self / other`.
8988 >>> x = FP('x', FPSort(8, 24))
8989 >>> y = FP('y', FPSort(8, 24))
8997 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8998 return fpDiv(_dflt_rm(), a, b, self.ctx)
Referenced by FPRef.__truediv__().
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 8944 of file z3py.py.
8944 def __mul__(self, other):
8945 """Create the Z3 expression `self * other`.
8947 >>> x = FP('x', FPSort(8, 24))
8948 >>> y = FP('y', FPSort(8, 24))
8956 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8957 return fpMul(_dflt_rm(), a, b, self.ctx)
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 9000 of file z3py.py.
9000 def __rdiv__(self, other):
9001 """Create the Z3 expression `other / self`.
9003 >>> x = FP('x', FPSort(8, 24))
9004 >>> y = FP('y', FPSort(8, 24))
9010 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9011 return fpDiv(_dflt_rm(), a, b, self.ctx)
Referenced by FPRef.__rtruediv__().
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 8921 of file z3py.py.
8921 def __sub__(self, other):
8922 """Create the Z3 expression `self - other`.
8924 >>> x = FP('x', FPSort(8, 24))
8925 >>> y = FP('y', FPSort(8, 24))
8931 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8932 return fpSub(_dflt_rm(), a, b, self.ctx)
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 8855 of file z3py.py.
8856 """Return the sort of the floating-point expression `self`.
8858 >>> x = FP('1.0', FPSort(8, 24))
8861 >>> x.sort() == FPSort(8, 24)
8864 return FPSortRef(
Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)