Z3
Public Member Functions
FPRef Class Reference

FP Expressions. More...

+ Inheritance diagram for FPRef:

Public Member Functions

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

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

FP Expressions.

Floating-point expressions.

Definition at line 8693 of file z3py.py.

Member Function Documentation

◆ __add__()

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

8739  def __add__(self, other):
8740  """Create the Z3 expression `self + other`.
8741 
8742  >>> x = FP('x', FPSort(8, 24))
8743  >>> y = FP('y', FPSort(8, 24))
8744  >>> x + y
8745  x + y
8746  >>> (x + y).sort()
8747  FPSort(8, 24)
8748  """
8749  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8750  return fpAdd(_dflt_rm(), a, b, self.ctx)
8751 
def fpAdd(rm, a, b, ctx=None)
Definition: z3py.py:9373

◆ __div__()

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

8826  def __div__(self, other):
8827  """Create the Z3 expression `self / other`.
8828 
8829  >>> x = FP('x', FPSort(8, 24))
8830  >>> y = FP('y', FPSort(8, 24))
8831  >>> x / y
8832  x / y
8833  >>> (x / y).sort()
8834  FPSort(8, 24)
8835  >>> 10 / y
8836  1.25*(2**3) / y
8837  """
8838  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8839  return fpDiv(_dflt_rm(), a, b, self.ctx)
8840 
def fpDiv(rm, a, b, ctx=None)
Definition: z3py.py:9417

◆ __ge__()

def __ge__ (   self,
  other 
)

Definition at line 8733 of file z3py.py.

8733  def __ge__(self, other):
8734  return fpGEQ(self, other, self.ctx)
8735 
def fpGEQ(a, b, ctx=None)
Definition: z3py.py:9571

◆ __gt__()

def __gt__ (   self,
  other 
)

Definition at line 8736 of file z3py.py.

8736  def __gt__(self, other):
8737  return fpGT(self, other, self.ctx)
8738 
def fpGT(a, b, ctx=None)
Definition: z3py.py:9560

◆ __le__()

def __le__ (   self,
  other 
)

Definition at line 8727 of file z3py.py.

8727  def __le__(self, other):
8728  return fpLEQ(self, other, self.ctx)
8729 
def fpLEQ(a, b, ctx=None)
Definition: z3py.py:9549

◆ __lt__()

def __lt__ (   self,
  other 
)

Definition at line 8730 of file z3py.py.

8730  def __lt__(self, other):
8731  return fpLT(self, other, self.ctx)
8732 
def fpLT(a, b, ctx=None)
Definition: z3py.py:9538

◆ __mod__()

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

Definition at line 8863 of file z3py.py.

8863  def __mod__(self, other):
8864  """Create the Z3 expression mod `self % other`."""
8865  return fpRem(self, other)
8866 
def fpRem(a, b, ctx=None)
Definition: z3py.py:9431

◆ __mul__()

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

8785  def __mul__(self, other):
8786  """Create the Z3 expression `self * other`.
8787 
8788  >>> x = FP('x', FPSort(8, 24))
8789  >>> y = FP('y', FPSort(8, 24))
8790  >>> x * y
8791  x * y
8792  >>> (x * y).sort()
8793  FPSort(8, 24)
8794  >>> 10 * y
8795  1.25*(2**3) * y
8796  """
8797  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8798  return fpMul(_dflt_rm(), a, b, self.ctx)
8799 
def fpMul(rm, a, b, ctx=None)
Definition: z3py.py:9403

◆ __neg__()

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

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

Definition at line 8817 of file z3py.py.

8817  def __neg__(self):
8818  """Create the Z3 expression `-self`.
8819 
8820  >>> x = FP('x', Float32())
8821  >>> -x
8822  -x
8823  """
8824  return fpNeg(self)
8825 
def fpNeg(a, ctx=None)
Definition: z3py.py:9306

◆ __pos__()

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

Definition at line 8813 of file z3py.py.

8813  def __pos__(self):
8814  """Create the Z3 expression `+self`."""
8815  return self
8816 

◆ __radd__()

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

8752  def __radd__(self, other):
8753  """Create the Z3 expression `other + self`.
8754 
8755  >>> x = FP('x', FPSort(8, 24))
8756  >>> 10 + x
8757  1.25*(2**3) + x
8758  """
8759  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
8760  return fpAdd(_dflt_rm(), a, b, self.ctx)
8761 
def fpAdd(rm, a, b, ctx=None)
Definition: z3py.py:9373

◆ __rdiv__()

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

8841  def __rdiv__(self, other):
8842  """Create the Z3 expression `other / self`.
8843 
8844  >>> x = FP('x', FPSort(8, 24))
8845  >>> y = FP('y', FPSort(8, 24))
8846  >>> x / y
8847  x / y
8848  >>> x / 10
8849  x / 1.25*(2**3)
8850  """
8851  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
8852  return fpDiv(_dflt_rm(), a, b, self.ctx)
8853 
def fpDiv(rm, a, b, ctx=None)
Definition: z3py.py:9417

◆ __rmod__()

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

Definition at line 8867 of file z3py.py.

8867  def __rmod__(self, other):
8868  """Create the Z3 expression mod `other % self`."""
8869  return fpRem(other, self)
8870 
def fpRem(a, b, ctx=None)
Definition: z3py.py:9431

◆ __rmul__()

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

8800  def __rmul__(self, other):
8801  """Create the Z3 expression `other * self`.
8802 
8803  >>> x = FP('x', FPSort(8, 24))
8804  >>> y = FP('y', FPSort(8, 24))
8805  >>> x * y
8806  x * y
8807  >>> x * 10
8808  x * 1.25*(2**3)
8809  """
8810  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
8811  return fpMul(_dflt_rm(), a, b, self.ctx)
8812 
def fpMul(rm, a, b, ctx=None)
Definition: z3py.py:9403

◆ __rsub__()

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

8775  def __rsub__(self, other):
8776  """Create the Z3 expression `other - self`.
8777 
8778  >>> x = FP('x', FPSort(8, 24))
8779  >>> 10 - x
8780  1.25*(2**3) - x
8781  """
8782  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
8783  return fpSub(_dflt_rm(), a, b, self.ctx)
8784 
def fpSub(rm, a, b, ctx=None)
Definition: z3py.py:9389

◆ __rtruediv__()

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

Definition at line 8859 of file z3py.py.

8859  def __rtruediv__(self, other):
8860  """Create the Z3 expression division `other / self`."""
8861  return self.__rdiv__(other)
8862 

◆ __sub__()

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

8762  def __sub__(self, other):
8763  """Create the Z3 expression `self - other`.
8764 
8765  >>> x = FP('x', FPSort(8, 24))
8766  >>> y = FP('y', FPSort(8, 24))
8767  >>> x - y
8768  x - y
8769  >>> (x - y).sort()
8770  FPSort(8, 24)
8771  """
8772  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
8773  return fpSub(_dflt_rm(), a, b, self.ctx)
8774 
def fpSub(rm, a, b, ctx=None)
Definition: z3py.py:9389

◆ __truediv__()

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

Definition at line 8855 of file z3py.py.

8855  def __truediv__(self, other):
8856  """Create the Z3 expression division `self / other`."""
8857  return self.__div__(other)
8858 

◆ as_string()

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

Definition at line 8723 of file z3py.py.

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

◆ ebits()

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

8707  def ebits(self):
8708  """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
8709  >>> b = FPSort(8, 24)
8710  >>> b.ebits()
8711  8
8712  """
8713  return self.sort().ebits();
8714 

◆ sbits()

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

8715  def sbits(self):
8716  """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
8717  >>> b = FPSort(8, 24)
8718  >>> b.sbits()
8719  24
8720  """
8721  return self.sort().sbits();
8722 

◆ sort()

def 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

Definition at line 8696 of file z3py.py.

Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), and FPRef.__sub__().

8696  def sort(self):
8697  """Return the sort of the floating-point expression `self`.
8698 
8699  >>> x = FP('1.0', FPSort(8, 24))
8700  >>> x.sort()
8701  FPSort(8, 24)
8702  >>> x.sort() == FPSort(8, 24)
8703  True
8704  """
8705  return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
8706 
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.