FP Expressions.
Floating-point expressions.
Definition at line 8211 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 8344 of file z3py.py.
8344 def __div__(self, other):
8345 """Create the Z3 expression `self / other`. 8347 >>> x = FP('x', FPSort(8, 24)) 8348 >>> y = FP('y', FPSort(8, 24)) 8356 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8357 return fpDiv(_dflt_rm(), a, b, self.ctx)
def fpDiv(rm, a, b, ctx=None)
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 8303 of file z3py.py.
8303 def __mul__(self, other):
8304 """Create the Z3 expression `self * other`. 8306 >>> x = FP('x', FPSort(8, 24)) 8307 >>> y = FP('y', FPSort(8, 24)) 8315 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8316 return fpMul(_dflt_rm(), a, b, self.ctx)
def fpMul(rm, a, b, ctx=None)
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
Definition at line 8214 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), and FPRef.__sub__().
8215 """Return the sort of the floating-point expression `self`. 8217 >>> x = FP('1.0', FPSort(8, 24)) 8220 >>> x.sort() == FPSort(8, 24) 8223 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)