Floating-point expressions.
Definition at line 9317 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 9450 of file z3py.py.
9450 def __div__(self, other):
9451 """Create the Z3 expression `self / other`.
9453 >>> x = FP('x', FPSort(8, 24))
9454 >>> y = FP('y', FPSort(8, 24))
9462 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9463 return fpDiv(_dflt_rm(), a, b, self.ctx)
def fpDiv(rm, a, b, ctx=None)
Referenced by ArithRef.__truediv__(), BitVecRef.__truediv__(), and FPRef.__truediv__().
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 9465 of file z3py.py.
9465 def __rdiv__(self, other):
9466 """Create the Z3 expression `other / self`.
9468 >>> x = FP('x', FPSort(8, 24))
9469 >>> y = FP('y', FPSort(8, 24))
9475 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9476 return fpDiv(_dflt_rm(), a, b, self.ctx)
Referenced by ArithRef.__rtruediv__(), BitVecRef.__rtruediv__(), and 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 9386 of file z3py.py.
9386 def __sub__(self, other):
9387 """Create the Z3 expression `self - other`.
9389 >>> x = FP('x', FPSort(8, 24))
9390 >>> y = FP('y', FPSort(8, 24))
9396 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9397 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 9320 of file z3py.py.
9321 """Return the sort of the floating-point expression `self`.
9323 >>> x = FP('1.0', FPSort(8, 24))
9326 >>> x.sort() == FPSort(8, 24)
9329 return FPSortRef(
Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Referenced by QuantifierRef.__getitem__(), FPNumRef.as_string(), ArrayRef.domain(), FPRef.ebits(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), FPRef.sbits(), BitVecRef.size(), and ExprRef.sort_kind().