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 __ne__ (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 __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 __ne__ (self, other)
 
def decl (self)
 
def num_args (self)
 
def arg (self, idx)
 
def children (self)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __str__ (self)
 
def __repr__ (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 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 7601 of file z3py.py.

Member Function Documentation

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

7651  def __add__(self, other):
7652  """Create the Z3 expression `self + other`.
7653 
7654  >>> x = FP('x', FPSort(8, 24))
7655  >>> y = FP('y', FPSort(8, 24))
7656  >>> x + y
7657  x + y
7658  >>> (x + y).sort()
7659  FPSort(8, 24)
7660  """
7661  a, b = z3._coerce_exprs(self, other)
7662  return fpAdd(_dflt_rm(), self, other)
7663 
def fpAdd(rm, a, b)
Definition: z3py.py:8099
def __add__(self, other)
Definition: z3py.py:7651
def __ge__ (   self,
  other 
)

Definition at line 7641 of file z3py.py.

7641  def __ge__(self, other):
7642  return fpGEQ(self, other)
7643 
def __ge__(self, other)
Definition: z3py.py:7641
def fpGEQ(a, b)
Definition: z3py.py:8353
def __gt__ (   self,
  other 
)

Definition at line 7644 of file z3py.py.

7644  def __gt__(self, other):
7645  return fpGT(self, other)
7646 
def __gt__(self, other)
Definition: z3py.py:7644
def fpGT(a, b)
Definition: z3py.py:8339
def __le__ (   self,
  other 
)

Definition at line 7635 of file z3py.py.

7635  def __le__(self, other):
7636  return fpLEQ(self, other)
7637 
def fpLEQ(a, b)
Definition: z3py.py:8326
def __le__(self, other)
Definition: z3py.py:7635
def __lt__ (   self,
  other 
)

Definition at line 7638 of file z3py.py.

7638  def __lt__(self, other):
7639  return fpLEQ(self, other)
7640 
def fpLEQ(a, b)
Definition: z3py.py:8326
def __lt__(self, other)
Definition: z3py.py:7638
def __mod__ (   self,
  other 
)
Create the Z3 expression mod `self % other`.

Definition at line 7741 of file z3py.py.

7741  def __mod__(self, other):
7742  """Create the Z3 expression mod `self % other`."""
7743  return fpRem(self, other)
7744 
def fpRem(a, b)
Definition: z3py.py:8171
def __mod__(self, other)
Definition: z3py.py:7741
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 7697 of file z3py.py.

7697  def __mul__(self, other):
7698  """Create the Z3 expression `self * other`.
7699 
7700  >>> x = FP('x', FPSort(8, 24))
7701  >>> y = FP('y', FPSort(8, 24))
7702  >>> x * y
7703  x * y
7704  >>> (x * y).sort()
7705  FPSort(8, 24)
7706  >>> 10 * y
7707  1.25*(2**3) * y
7708  """
7709  a, b = z3._coerce_exprs(self, other)
7710  return fpMul(_dflt_rm(), self, other)
7711 
def fpMul(rm, a, b)
Definition: z3py.py:8135
def __mul__(self, other)
Definition: z3py.py:7697
def __ne__ (   self,
  other 
)

Definition at line 7647 of file z3py.py.

7647  def __ne__(self, other):
7648  return fpNEQ(self, other)
7649 
7650 
def fpNEQ(a, b)
Definition: z3py.py:8381
def __ne__(self, other)
Definition: z3py.py:7647
def __neg__ (   self)
Create the Z3 expression `-self`.

Definition at line 7729 of file z3py.py.

7729  def __neg__(self):
7730  """Create the Z3 expression `-self`."""
7731  return FPRef(fpNeg(self))
7732 
FP Expressions.
Definition: z3py.py:7601
def __neg__(self)
Definition: z3py.py:7729
def fpNeg(a)
Definition: z3py.py:8077
def __pos__ (   self)
Create the Z3 expression `+self`.

Definition at line 7725 of file z3py.py.

7725  def __pos__(self):
7726  """Create the Z3 expression `+self`."""
7727  return self
7728 
def __pos__(self)
Definition: z3py.py:7725
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 7664 of file z3py.py.

7664  def __radd__(self, other):
7665  """Create the Z3 expression `other + self`.
7666 
7667  >>> x = FP('x', FPSort(8, 24))
7668  >>> 10 + x
7669  1.25*(2**3) + x
7670  """
7671  a, b = _coerce_exprs(self, other)
7672  return fpAdd(_dflt_rm(), other, self)
7673 
def fpAdd(rm, a, b)
Definition: z3py.py:8099
def __radd__(self, other)
Definition: z3py.py:7664
def __rmod__ (   self,
  other 
)
Create the Z3 expression mod `other % self`.

Definition at line 7745 of file z3py.py.

7745  def __rmod__(self, other):
7746  """Create the Z3 expression mod `other % self`."""
7747  return fpRem(other, self)
7748 
def fpRem(a, b)
Definition: z3py.py:8171
def __rmod__(self, other)
Definition: z3py.py:7745
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 7712 of file z3py.py.

7712  def __rmul__(self, other):
7713  """Create the Z3 expression `other * self`.
7714 
7715  >>> x = FP('x', FPSort(8, 24))
7716  >>> y = FP('y', FPSort(8, 24))
7717  >>> x * y
7718  x * y
7719  >>> x * 10
7720  x * 1.25*(2**3)
7721  """
7722  a, b = _coerce_exprs(self, other)
7723  return fpMul(_dflt_rm(), other, self)
7724 
def __rmul__(self, other)
Definition: z3py.py:7712
def fpMul(rm, a, b)
Definition: z3py.py:8135
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 7687 of file z3py.py.

7687  def __rsub__(self, other):
7688  """Create the Z3 expression `other - self`.
7689 
7690  >>> x = FP('x', FPSort(8, 24))
7691  >>> 10 - x
7692  1.25*(2**3) - x
7693  """
7694  a, b = _coerce_exprs(self, other)
7695  return fpSub(_dflt_rm(), other, self)
7696 
def fpSub(rm, a, b)
Definition: z3py.py:8117
def __rsub__(self, other)
Definition: z3py.py:7687
def __rtruediv__ (   self,
  other 
)
Create the Z3 expression division `other / self`.

Definition at line 7737 of file z3py.py.

7737  def __rtruediv__(self, other):
7738  """Create the Z3 expression division `other / self`."""
7739  return self.__rdiv__(other)
7740 
def __rtruediv__(self, other)
Definition: z3py.py:7737
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 7674 of file z3py.py.

7674  def __sub__(self, other):
7675  """Create the Z3 expression `self - other`.
7676 
7677  >>> x = FP('x', FPSort(8, 24))
7678  >>> y = FP('y', FPSort(8, 24))
7679  >>> x - y
7680  x - y
7681  >>> (x - y).sort()
7682  FPSort(8, 24)
7683  """
7684  a, b = z3._coerce_exprs(self, other)
7685  return fpSub(_dflt_rm(), self, other)
7686 
def fpSub(rm, a, b)
Definition: z3py.py:8117
def __sub__(self, other)
Definition: z3py.py:7674
def __truediv__ (   self,
  other 
)
Create the Z3 expression division `self / other`.

Definition at line 7733 of file z3py.py.

7733  def __truediv__(self, other):
7734  """Create the Z3 expression division `self / other`."""
7735  return self.__div__(other)
7736 
def __truediv__(self, other)
Definition: z3py.py:7733
def as_string (   self)
Return a Z3 floating point expression as a Python string.

Definition at line 7631 of file z3py.py.

7631  def as_string(self):
7632  """Return a Z3 floating point expression as a Python string."""
7633  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
7634 
def as_ast(self)
Definition: z3py.py:296
Z3_string Z3_API Z3_ast_to_string(__in Z3_context c, __in Z3_ast a)
Convert the given AST node into a string.
def ctx_ref(self)
Definition: z3py.py:305
def as_string(self)
Definition: z3py.py:7631
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 7615 of file z3py.py.

7615  def ebits(self):
7616  """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
7617  >>> b = FPSort(8, 24)
7618  >>> b.ebits()
7619  8
7620  """
7621  return self.sort().ebits();
7622 
def sort(self)
Definition: z3py.py:752
def ebits(self)
Definition: z3py.py:7615
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 7623 of file z3py.py.

7623  def sbits(self):
7624  """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
7625  >>> b = FPSort(8, 24)
7626  >>> b.sbits()
7627  24
7628  """
7629  return self.sort().sbits();
7630 
def sbits(self)
Definition: z3py.py:7623
def sort(self)
Definition: z3py.py:752
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 7604 of file z3py.py.

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

7604  def sort(self):
7605  """Return the sort of the floating-point expression `self`.
7606 
7607  >>> x = FP('1.0', FPSort(8, 24))
7608  >>> x.sort()
7609  FPSort(8, 24)
7610  >>> x.sort() == FPSort(8, 24)
7611  True
7612  """
7613  return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
7614 
def as_ast(self)
Definition: z3py.py:296
Z3_sort Z3_API Z3_get_sort(__in Z3_context c, __in Z3_ast a)
Return the sort of an AST node.
def sort(self)
Definition: z3py.py:7604
FP Sorts.
Definition: z3py.py:7499
def ctx_ref(self)
Definition: z3py.py:305