Z3
Public Member Functions
FPRef Class Reference
+ 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)
 
def from_string (self, s)
 
def serialize (self)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __deepcopy__
 
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

Floating-point expressions.

Definition at line 9596 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 9642 of file z3py.py.

9642  def __add__(self, other):
9643  """Create the Z3 expression `self + other`.
9644 
9645  >>> x = FP('x', FPSort(8, 24))
9646  >>> y = FP('y', FPSort(8, 24))
9647  >>> x + y
9648  x + y
9649  >>> (x + y).sort()
9650  FPSort(8, 24)
9651  """
9652  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9653  return fpAdd(_dflt_rm(), a, b, self.ctx)
9654 
def __add__(self, other)
Definition: z3py.py:9642
def fpAdd
Definition: z3py.py:10322
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 9729 of file z3py.py.

9729  def __div__(self, other):
9730  """Create the Z3 expression `self / other`.
9731 
9732  >>> x = FP('x', FPSort(8, 24))
9733  >>> y = FP('y', FPSort(8, 24))
9734  >>> x / y
9735  x / y
9736  >>> (x / y).sort()
9737  FPSort(8, 24)
9738  >>> 10 / y
9739  1.25*(2**3) / y
9740  """
9741  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9742  return fpDiv(_dflt_rm(), a, b, self.ctx)
9743 
def __div__(self, other)
Definition: z3py.py:9729
def fpDiv
Definition: z3py.py:10369
def __ge__ (   self,
  other 
)

Definition at line 9636 of file z3py.py.

9636  def __ge__(self, other):
9637  return fpGEQ(self, other, self.ctx)
9638 
def fpGEQ
Definition: z3py.py:10540
def __ge__(self, other)
Definition: z3py.py:9636
def __gt__ (   self,
  other 
)

Definition at line 9639 of file z3py.py.

9639  def __gt__(self, other):
9640  return fpGT(self, other, self.ctx)
9641 
def __gt__(self, other)
Definition: z3py.py:9639
def fpGT
Definition: z3py.py:10528
def __le__ (   self,
  other 
)

Definition at line 9630 of file z3py.py.

9630  def __le__(self, other):
9631  return fpLEQ(self, other, self.ctx)
9632 
def __le__(self, other)
Definition: z3py.py:9630
def fpLEQ
Definition: z3py.py:10516
def __lt__ (   self,
  other 
)

Definition at line 9633 of file z3py.py.

9633  def __lt__(self, other):
9634  return fpLT(self, other, self.ctx)
9635 
def fpLT
Definition: z3py.py:10504
def __lt__(self, other)
Definition: z3py.py:9633
def __mod__ (   self,
  other 
)
Create the Z3 expression mod `self % other`.

Definition at line 9765 of file z3py.py.

9765  def __mod__(self, other):
9766  """Create the Z3 expression mod `self % other`."""
9767  return fpRem(self, other)
9768 
def fpRem
Definition: z3py.py:10384
def __mod__(self, other)
Definition: z3py.py:9765
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 9688 of file z3py.py.

9688  def __mul__(self, other):
9689  """Create the Z3 expression `self * other`.
9690 
9691  >>> x = FP('x', FPSort(8, 24))
9692  >>> y = FP('y', FPSort(8, 24))
9693  >>> x * y
9694  x * y
9695  >>> (x * y).sort()
9696  FPSort(8, 24)
9697  >>> 10 * y
9698  1.25*(2**3) * y
9699  """
9700  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9701  return fpMul(_dflt_rm(), a, b, self.ctx)
9702 
def fpMul
Definition: z3py.py:10354
def __mul__(self, other)
Definition: z3py.py:9688
def __neg__ (   self)
Create the Z3 expression `-self`.

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

Definition at line 9720 of file z3py.py.

9720  def __neg__(self):
9721  """Create the Z3 expression `-self`.
9722 
9723  >>> x = FP('x', Float32())
9724  >>> -x
9725  -x
9726  """
9727  return fpNeg(self)
9728 
def __neg__(self)
Definition: z3py.py:9720
def fpNeg
Definition: z3py.py:10254
def __pos__ (   self)
Create the Z3 expression `+self`.

Definition at line 9716 of file z3py.py.

9716  def __pos__(self):
9717  """Create the Z3 expression `+self`."""
9718  return self
9719 
def __pos__(self)
Definition: z3py.py:9716
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 9655 of file z3py.py.

9655  def __radd__(self, other):
9656  """Create the Z3 expression `other + self`.
9657 
9658  >>> x = FP('x', FPSort(8, 24))
9659  >>> 10 + x
9660  1.25*(2**3) + x
9661  """
9662  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9663  return fpAdd(_dflt_rm(), a, b, self.ctx)
9664 
def fpAdd
Definition: z3py.py:10322
def __radd__(self, other)
Definition: z3py.py:9655
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 9744 of file z3py.py.

9744  def __rdiv__(self, other):
9745  """Create the Z3 expression `other / self`.
9746 
9747  >>> x = FP('x', FPSort(8, 24))
9748  >>> y = FP('y', FPSort(8, 24))
9749  >>> x / y
9750  x / y
9751  >>> x / 10
9752  x / 1.25*(2**3)
9753  """
9754  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9755  return fpDiv(_dflt_rm(), a, b, self.ctx)
9756 
def __rdiv__(self, other)
Definition: z3py.py:9744
def fpDiv
Definition: z3py.py:10369
def __rmod__ (   self,
  other 
)
Create the Z3 expression mod `other % self`.

Definition at line 9769 of file z3py.py.

9769  def __rmod__(self, other):
9770  """Create the Z3 expression mod `other % self`."""
9771  return fpRem(other, self)
9772 
9773 
def fpRem
Definition: z3py.py:10384
def __rmod__(self, other)
Definition: z3py.py:9769
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 9703 of file z3py.py.

9703  def __rmul__(self, other):
9704  """Create the Z3 expression `other * self`.
9705 
9706  >>> x = FP('x', FPSort(8, 24))
9707  >>> y = FP('y', FPSort(8, 24))
9708  >>> x * y
9709  x * y
9710  >>> x * 10
9711  x * 1.25*(2**3)
9712  """
9713  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9714  return fpMul(_dflt_rm(), a, b, self.ctx)
9715 
def __rmul__(self, other)
Definition: z3py.py:9703
def fpMul
Definition: z3py.py:10354
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 9678 of file z3py.py.

9678  def __rsub__(self, other):
9679  """Create the Z3 expression `other - self`.
9680 
9681  >>> x = FP('x', FPSort(8, 24))
9682  >>> 10 - x
9683  1.25*(2**3) - x
9684  """
9685  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9686  return fpSub(_dflt_rm(), a, b, self.ctx)
9687 
def __rsub__(self, other)
Definition: z3py.py:9678
def fpSub
Definition: z3py.py:10339
def __rtruediv__ (   self,
  other 
)
Create the Z3 expression division `other / self`.

Definition at line 9761 of file z3py.py.

9761  def __rtruediv__(self, other):
9762  """Create the Z3 expression division `other / self`."""
9763  return self.__rdiv__(other)
9764 
def __rtruediv__(self, other)
Definition: z3py.py:9761
def __rdiv__(self, other)
Definition: z3py.py:9744
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 9665 of file z3py.py.

9665  def __sub__(self, other):
9666  """Create the Z3 expression `self - other`.
9667 
9668  >>> x = FP('x', FPSort(8, 24))
9669  >>> y = FP('y', FPSort(8, 24))
9670  >>> x - y
9671  x - y
9672  >>> (x - y).sort()
9673  FPSort(8, 24)
9674  """
9675  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9676  return fpSub(_dflt_rm(), a, b, self.ctx)
9677 
def fpSub
Definition: z3py.py:10339
def __sub__(self, other)
Definition: z3py.py:9665
def __truediv__ (   self,
  other 
)
Create the Z3 expression division `self / other`.

Definition at line 9757 of file z3py.py.

9757  def __truediv__(self, other):
9758  """Create the Z3 expression division `self / other`."""
9759  return self.__div__(other)
9760 
def __div__(self, other)
Definition: z3py.py:9729
def __truediv__(self, other)
Definition: z3py.py:9757
def as_string (   self)
Return a Z3 floating point expression as a Python string.

Definition at line 9626 of file z3py.py.

9626  def as_string(self):
9627  """Return a Z3 floating point expression as a Python string."""
9628  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
9629 
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
def as_ast(self)
Definition: z3py.py:392
def ctx_ref(self)
Definition: z3py.py:400
def as_string(self)
Definition: z3py.py:9626
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 9610 of file z3py.py.

9610  def ebits(self):
9611  """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
9612  >>> b = FPSort(8, 24)
9613  >>> b.ebits()
9614  8
9615  """
9616  return self.sort().ebits()
9617 
def sort(self)
Definition: z3py.py:996
def ebits(self)
Definition: z3py.py:9610
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 9618 of file z3py.py.

9618  def sbits(self):
9619  """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
9620  >>> b = FPSort(8, 24)
9621  >>> b.sbits()
9622  24
9623  """
9624  return self.sort().sbits()
9625 
def sbits(self)
Definition: z3py.py:9618
def sort(self)
Definition: z3py.py:996
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 9599 of file z3py.py.

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

9599  def sort(self):
9600  """Return the sort of the floating-point expression `self`.
9601 
9602  >>> x = FP('1.0', FPSort(8, 24))
9603  >>> x.sort()
9604  FPSort(8, 24)
9605  >>> x.sort() == FPSort(8, 24)
9606  True
9607  """
9608  return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
9609 
def as_ast(self)
Definition: z3py.py:392
def sort(self)
Definition: z3py.py:9599
def ctx_ref(self)
Definition: z3py.py:400
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.