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

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

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

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

◆ __ge__()

__ge__ ( self,
other )

Definition at line 9750 of file z3py.py.

9750 def __ge__(self, other):
9751 return fpGEQ(self, other, self.ctx)
9752

◆ __gt__()

__gt__ ( self,
other )

Definition at line 9753 of file z3py.py.

9753 def __gt__(self, other):
9754 return fpGT(self, other, self.ctx)
9755

◆ __le__()

__le__ ( self,
other )

Definition at line 9744 of file z3py.py.

9744 def __le__(self, other):
9745 return fpLEQ(self, other, self.ctx)
9746

◆ __lt__()

__lt__ ( self,
other )

Definition at line 9747 of file z3py.py.

9747 def __lt__(self, other):
9748 return fpLT(self, other, self.ctx)
9749

◆ __mod__()

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

Definition at line 9879 of file z3py.py.

9879 def __mod__(self, other):
9880 """Create the Z3 expression mod `self % other`."""
9881 return fpRem(self, other)
9882

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

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

◆ __neg__()

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

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

Definition at line 9834 of file z3py.py.

9834 def __neg__(self):
9835 """Create the Z3 expression `-self`.
9836
9837 >>> x = FP('x', Float32())
9838 >>> -x
9839 -x
9840 """
9841 return fpNeg(self)
9842

◆ __pos__()

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

Definition at line 9830 of file z3py.py.

9830 def __pos__(self):
9831 """Create the Z3 expression `+self`."""
9832 return self
9833

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

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

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

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

◆ __rmod__()

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

Definition at line 9883 of file z3py.py.

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

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

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

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

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

◆ __rtruediv__()

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

Definition at line 9875 of file z3py.py.

9875 def __rtruediv__(self, other):
9876 """Create the Z3 expression division `other / self`."""
9877 return self.__rdiv__(other)
9878

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

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

◆ __truediv__()

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

Definition at line 9871 of file z3py.py.

9871 def __truediv__(self, other):
9872 """Create the Z3 expression division `self / other`."""
9873 return self.__div__(other)
9874

◆ as_string()

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

Reimplemented in FPNumRef.

Definition at line 9740 of file z3py.py.

9740 def as_string(self):
9741 """Return a Z3 floating point expression as a Python string."""
9742 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
9743
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 9724 of file z3py.py.

9724 def ebits(self):
9725 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
9726 >>> b = FPSort(8, 24)
9727 >>> b.ebits()
9728 8
9729 """
9730 return self.sort().ebits()
9731

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

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

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

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