Z3
Loading...
Searching...
No Matches
FPRef Class Reference
Inheritance diagram for FPRef:

Public Member Functions

 sort (self)
 ebits (self)
 sbits (self)
 as_string (self)
 __le__ (self, other)
 __lt__ (self, other)
 __ge__ (self, other)
 __gt__ (self, other)
 __add__ (self, other)
 __radd__ (self, other)
 __sub__ (self, other)
 __rsub__ (self, other)
 __mul__ (self, other)
 __rmul__ (self, other)
 __pos__ (self)
 __neg__ (self)
 __div__ (self, other)
 __rdiv__ (self, other)
 __truediv__ (self, other)
 __rtruediv__ (self, other)
 __mod__ (self, other)
 __rmod__ (self, other)
Public Member Functions inherited from ExprRef
 as_ast (self)
 get_id (self)
 sort_kind (self)
 __eq__ (self, other)
 __hash__ (self)
 __ne__ (self, other)
 params (self)
 decl (self)
 kind (self)
 num_args (self)
 arg (self, idx)
 children (self)
 from_string (self, s)
 serialize (self)
Public Member Functions inherited from AstRef
 __init__ (self, ast, ctx=None)
 __del__ (self)
 __deepcopy__ (self, memo={})
 __str__ (self)
 __repr__ (self)
 __eq__ (self, other)
 __hash__ (self)
 __nonzero__ (self)
 __bool__ (self)
 sexpr (self)
 ctx_ref (self)
 eq (self, other)
 translate (self, target)
 __copy__ (self)
 hash (self)
 py_value (self)
Public Member Functions inherited from Z3PPObject
 use_pp (self)

Additional Inherited Members

Data Fields inherited from AstRef
 ast = ast
 ctx = _get_ctx(ctx)
Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)

Detailed Description

Floating-point expressions.

Definition at line 9715 of file z3py.py.

Member Function Documentation

◆ __add__()

__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 9761 of file z3py.py.

9761 def __add__(self, other):
9762 """Create the Z3 expression `self + other`.
9763
9764 >>> x = FP('x', FPSort(8, 24))
9765 >>> y = FP('y', FPSort(8, 24))
9766 >>> x + y
9767 x + y
9768 >>> (x + y).sort()
9769 FPSort(8, 24)
9770 """
9771 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9772 return fpAdd(_dflt_rm(), a, b, self.ctx)
9773

◆ __div__()

__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 9848 of file z3py.py.

9848 def __div__(self, other):
9849 """Create the Z3 expression `self / other`.
9850
9851 >>> x = FP('x', FPSort(8, 24))
9852 >>> y = FP('y', FPSort(8, 24))
9853 >>> x / y
9854 x / y
9855 >>> (x / y).sort()
9856 FPSort(8, 24)
9857 >>> 10 / y
9858 1.25*(2**3) / y
9859 """
9860 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9861 return fpDiv(_dflt_rm(), a, b, self.ctx)
9862

◆ __ge__()

__ge__ ( self,
other )

Definition at line 9755 of file z3py.py.

9755 def __ge__(self, other):
9756 return fpGEQ(self, other, self.ctx)
9757

◆ __gt__()

__gt__ ( self,
other )

Definition at line 9758 of file z3py.py.

9758 def __gt__(self, other):
9759 return fpGT(self, other, self.ctx)
9760

◆ __le__()

__le__ ( self,
other )

Definition at line 9749 of file z3py.py.

9749 def __le__(self, other):
9750 return fpLEQ(self, other, self.ctx)
9751

◆ __lt__()

__lt__ ( self,
other )

Definition at line 9752 of file z3py.py.

9752 def __lt__(self, other):
9753 return fpLT(self, other, self.ctx)
9754

◆ __mod__()

__mod__ ( self,
other )
Create the Z3 expression mod `self % other`.

Definition at line 9884 of file z3py.py.

9884 def __mod__(self, other):
9885 """Create the Z3 expression mod `self % other`."""
9886 return fpRem(self, other)
9887

◆ __mul__()

__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 9807 of file z3py.py.

9807 def __mul__(self, other):
9808 """Create the Z3 expression `self * other`.
9809
9810 >>> x = FP('x', FPSort(8, 24))
9811 >>> y = FP('y', FPSort(8, 24))
9812 >>> x * y
9813 x * y
9814 >>> (x * y).sort()
9815 FPSort(8, 24)
9816 >>> 10 * y
9817 1.25*(2**3) * y
9818 """
9819 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9820 return fpMul(_dflt_rm(), a, b, self.ctx)
9821

◆ __neg__()

__neg__ ( self)
Create the Z3 expression `-self`.

>>> x = FP('x', Float32())
>>> -x
-x

Definition at line 9839 of file z3py.py.

9839 def __neg__(self):
9840 """Create the Z3 expression `-self`.
9841
9842 >>> x = FP('x', Float32())
9843 >>> -x
9844 -x
9845 """
9846 return fpNeg(self)
9847

◆ __pos__()

__pos__ ( self)
Create the Z3 expression `+self`.

Definition at line 9835 of file z3py.py.

9835 def __pos__(self):
9836 """Create the Z3 expression `+self`."""
9837 return self
9838

◆ __radd__()

__radd__ ( self,
other )
Create the Z3 expression `other + self`.

>>> x = FP('x', FPSort(8, 24))
>>> 10 + x
1.25*(2**3) + x

Definition at line 9774 of file z3py.py.

9774 def __radd__(self, other):
9775 """Create the Z3 expression `other + self`.
9776
9777 >>> x = FP('x', FPSort(8, 24))
9778 >>> 10 + x
9779 1.25*(2**3) + x
9780 """
9781 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9782 return fpAdd(_dflt_rm(), a, b, self.ctx)
9783

◆ __rdiv__()

__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 9863 of file z3py.py.

9863 def __rdiv__(self, other):
9864 """Create the Z3 expression `other / self`.
9865
9866 >>> x = FP('x', FPSort(8, 24))
9867 >>> y = FP('y', FPSort(8, 24))
9868 >>> x / y
9869 x / y
9870 >>> x / 10
9871 x / 1.25*(2**3)
9872 """
9873 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9874 return fpDiv(_dflt_rm(), a, b, self.ctx)
9875

◆ __rmod__()

__rmod__ ( self,
other )
Create the Z3 expression mod `other % self`.

Definition at line 9888 of file z3py.py.

9888 def __rmod__(self, other):
9889 """Create the Z3 expression mod `other % self`."""
9890 return fpRem(other, self)
9891
9892

◆ __rmul__()

__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 9822 of file z3py.py.

9822 def __rmul__(self, other):
9823 """Create the Z3 expression `other * self`.
9824
9825 >>> x = FP('x', FPSort(8, 24))
9826 >>> y = FP('y', FPSort(8, 24))
9827 >>> x * y
9828 x * y
9829 >>> x * 10
9830 x * 1.25*(2**3)
9831 """
9832 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9833 return fpMul(_dflt_rm(), a, b, self.ctx)
9834

◆ __rsub__()

__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 9797 of file z3py.py.

9797 def __rsub__(self, other):
9798 """Create the Z3 expression `other - self`.
9799
9800 >>> x = FP('x', FPSort(8, 24))
9801 >>> 10 - x
9802 1.25*(2**3) - x
9803 """
9804 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9805 return fpSub(_dflt_rm(), a, b, self.ctx)
9806

◆ __rtruediv__()

__rtruediv__ ( self,
other )
Create the Z3 expression division `other / self`.

Definition at line 9880 of file z3py.py.

9880 def __rtruediv__(self, other):
9881 """Create the Z3 expression division `other / self`."""
9882 return self.__rdiv__(other)
9883

◆ __sub__()

__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 9784 of file z3py.py.

9784 def __sub__(self, other):
9785 """Create the Z3 expression `self - other`.
9786
9787 >>> x = FP('x', FPSort(8, 24))
9788 >>> y = FP('y', FPSort(8, 24))
9789 >>> x - y
9790 x - y
9791 >>> (x - y).sort()
9792 FPSort(8, 24)
9793 """
9794 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9795 return fpSub(_dflt_rm(), a, b, self.ctx)
9796

◆ __truediv__()

__truediv__ ( self,
other )
Create the Z3 expression division `self / other`.

Definition at line 9876 of file z3py.py.

9876 def __truediv__(self, other):
9877 """Create the Z3 expression division `self / other`."""
9878 return self.__div__(other)
9879

◆ as_string()

as_string ( self)
Return a Z3 floating point expression as a Python string.

Reimplemented in FPNumRef.

Definition at line 9745 of file z3py.py.

9745 def as_string(self):
9746 """Return a Z3 floating point expression as a Python string."""
9747 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
9748
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.

◆ ebits()

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 9729 of file z3py.py.

9729 def ebits(self):
9730 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
9731 >>> b = FPSort(8, 24)
9732 >>> b.ebits()
9733 8
9734 """
9735 return self.sort().ebits()
9736

◆ sbits()

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 9737 of file z3py.py.

9737 def sbits(self):
9738 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
9739 >>> b = FPSort(8, 24)
9740 >>> b.sbits()
9741 24
9742 """
9743 return self.sort().sbits()
9744

◆ sort()

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 9718 of file z3py.py.

9718 def sort(self):
9719 """Return the sort of the floating-point expression `self`.
9720
9721 >>> x = FP('1.0', FPSort(8, 24))
9722 >>> x.sort()
9723 FPSort(8, 24)
9724 >>> x.sort() == FPSort(8, 24)
9725 True
9726 """
9727 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
9728
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.