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

9574  def __add__(self, other):
9575  """Create the Z3 expression `self + other`.
9576 
9577  >>> x = FP('x', FPSort(8, 24))
9578  >>> y = FP('y', FPSort(8, 24))
9579  >>> x + y
9580  x + y
9581  >>> (x + y).sort()
9582  FPSort(8, 24)
9583  """
9584  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9585  return fpAdd(_dflt_rm(), a, b, self.ctx)
9586 
def __add__(self, other)
Definition: z3py.py:9574
def fpAdd
Definition: z3py.py:10254
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 9661 of file z3py.py.

9661  def __div__(self, other):
9662  """Create the Z3 expression `self / other`.
9663 
9664  >>> x = FP('x', FPSort(8, 24))
9665  >>> y = FP('y', FPSort(8, 24))
9666  >>> x / y
9667  x / y
9668  >>> (x / y).sort()
9669  FPSort(8, 24)
9670  >>> 10 / y
9671  1.25*(2**3) / y
9672  """
9673  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9674  return fpDiv(_dflt_rm(), a, b, self.ctx)
9675 
def __div__(self, other)
Definition: z3py.py:9661
def fpDiv
Definition: z3py.py:10301
def __ge__ (   self,
  other 
)

Definition at line 9568 of file z3py.py.

9568  def __ge__(self, other):
9569  return fpGEQ(self, other, self.ctx)
9570 
def fpGEQ
Definition: z3py.py:10472
def __ge__(self, other)
Definition: z3py.py:9568
def __gt__ (   self,
  other 
)

Definition at line 9571 of file z3py.py.

9571  def __gt__(self, other):
9572  return fpGT(self, other, self.ctx)
9573 
def __gt__(self, other)
Definition: z3py.py:9571
def fpGT
Definition: z3py.py:10460
def __le__ (   self,
  other 
)

Definition at line 9562 of file z3py.py.

9562  def __le__(self, other):
9563  return fpLEQ(self, other, self.ctx)
9564 
def __le__(self, other)
Definition: z3py.py:9562
def fpLEQ
Definition: z3py.py:10448
def __lt__ (   self,
  other 
)

Definition at line 9565 of file z3py.py.

9565  def __lt__(self, other):
9566  return fpLT(self, other, self.ctx)
9567 
def fpLT
Definition: z3py.py:10436
def __lt__(self, other)
Definition: z3py.py:9565
def __mod__ (   self,
  other 
)
Create the Z3 expression mod `self % other`.

Definition at line 9697 of file z3py.py.

9697  def __mod__(self, other):
9698  """Create the Z3 expression mod `self % other`."""
9699  return fpRem(self, other)
9700 
def fpRem
Definition: z3py.py:10316
def __mod__(self, other)
Definition: z3py.py:9697
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 9620 of file z3py.py.

9620  def __mul__(self, other):
9621  """Create the Z3 expression `self * other`.
9622 
9623  >>> x = FP('x', FPSort(8, 24))
9624  >>> y = FP('y', FPSort(8, 24))
9625  >>> x * y
9626  x * y
9627  >>> (x * y).sort()
9628  FPSort(8, 24)
9629  >>> 10 * y
9630  1.25*(2**3) * y
9631  """
9632  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9633  return fpMul(_dflt_rm(), a, b, self.ctx)
9634 
def fpMul
Definition: z3py.py:10286
def __mul__(self, other)
Definition: z3py.py:9620
def __neg__ (   self)
Create the Z3 expression `-self`.

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

Definition at line 9652 of file z3py.py.

9652  def __neg__(self):
9653  """Create the Z3 expression `-self`.
9654 
9655  >>> x = FP('x', Float32())
9656  >>> -x
9657  -x
9658  """
9659  return fpNeg(self)
9660 
def __neg__(self)
Definition: z3py.py:9652
def fpNeg
Definition: z3py.py:10186
def __pos__ (   self)
Create the Z3 expression `+self`.

Definition at line 9648 of file z3py.py.

9648  def __pos__(self):
9649  """Create the Z3 expression `+self`."""
9650  return self
9651 
def __pos__(self)
Definition: z3py.py:9648
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 9587 of file z3py.py.

9587  def __radd__(self, other):
9588  """Create the Z3 expression `other + self`.
9589 
9590  >>> x = FP('x', FPSort(8, 24))
9591  >>> 10 + x
9592  1.25*(2**3) + x
9593  """
9594  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9595  return fpAdd(_dflt_rm(), a, b, self.ctx)
9596 
def fpAdd
Definition: z3py.py:10254
def __radd__(self, other)
Definition: z3py.py:9587
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 9676 of file z3py.py.

9676  def __rdiv__(self, other):
9677  """Create the Z3 expression `other / self`.
9678 
9679  >>> x = FP('x', FPSort(8, 24))
9680  >>> y = FP('y', FPSort(8, 24))
9681  >>> x / y
9682  x / y
9683  >>> x / 10
9684  x / 1.25*(2**3)
9685  """
9686  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9687  return fpDiv(_dflt_rm(), a, b, self.ctx)
9688 
def __rdiv__(self, other)
Definition: z3py.py:9676
def fpDiv
Definition: z3py.py:10301
def __rmod__ (   self,
  other 
)
Create the Z3 expression mod `other % self`.

Definition at line 9701 of file z3py.py.

9701  def __rmod__(self, other):
9702  """Create the Z3 expression mod `other % self`."""
9703  return fpRem(other, self)
9704 
9705 
def fpRem
Definition: z3py.py:10316
def __rmod__(self, other)
Definition: z3py.py:9701
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 9635 of file z3py.py.

9635  def __rmul__(self, other):
9636  """Create the Z3 expression `other * self`.
9637 
9638  >>> x = FP('x', FPSort(8, 24))
9639  >>> y = FP('y', FPSort(8, 24))
9640  >>> x * y
9641  x * y
9642  >>> x * 10
9643  x * 1.25*(2**3)
9644  """
9645  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9646  return fpMul(_dflt_rm(), a, b, self.ctx)
9647 
def __rmul__(self, other)
Definition: z3py.py:9635
def fpMul
Definition: z3py.py:10286
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 9610 of file z3py.py.

9610  def __rsub__(self, other):
9611  """Create the Z3 expression `other - self`.
9612 
9613  >>> x = FP('x', FPSort(8, 24))
9614  >>> 10 - x
9615  1.25*(2**3) - x
9616  """
9617  [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9618  return fpSub(_dflt_rm(), a, b, self.ctx)
9619 
def __rsub__(self, other)
Definition: z3py.py:9610
def fpSub
Definition: z3py.py:10271
def __rtruediv__ (   self,
  other 
)
Create the Z3 expression division `other / self`.

Definition at line 9693 of file z3py.py.

9693  def __rtruediv__(self, other):
9694  """Create the Z3 expression division `other / self`."""
9695  return self.__rdiv__(other)
9696 
def __rtruediv__(self, other)
Definition: z3py.py:9693
def __rdiv__(self, other)
Definition: z3py.py:9676
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 9597 of file z3py.py.

9597  def __sub__(self, other):
9598  """Create the Z3 expression `self - other`.
9599 
9600  >>> x = FP('x', FPSort(8, 24))
9601  >>> y = FP('y', FPSort(8, 24))
9602  >>> x - y
9603  x - y
9604  >>> (x - y).sort()
9605  FPSort(8, 24)
9606  """
9607  [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9608  return fpSub(_dflt_rm(), a, b, self.ctx)
9609 
def fpSub
Definition: z3py.py:10271
def __sub__(self, other)
Definition: z3py.py:9597
def __truediv__ (   self,
  other 
)
Create the Z3 expression division `self / other`.

Definition at line 9689 of file z3py.py.

9689  def __truediv__(self, other):
9690  """Create the Z3 expression division `self / other`."""
9691  return self.__div__(other)
9692 
def __div__(self, other)
Definition: z3py.py:9661
def __truediv__(self, other)
Definition: z3py.py:9689
def as_string (   self)
Return a Z3 floating point expression as a Python string.

Definition at line 9558 of file z3py.py.

9558  def as_string(self):
9559  """Return a Z3 floating point expression as a Python string."""
9560  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
9561 
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:9558
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 9542 of file z3py.py.

9542  def ebits(self):
9543  """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
9544  >>> b = FPSort(8, 24)
9545  >>> b.ebits()
9546  8
9547  """
9548  return self.sort().ebits()
9549 
def sort(self)
Definition: z3py.py:974
def ebits(self)
Definition: z3py.py:9542
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 9550 of file z3py.py.

9550  def sbits(self):
9551  """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
9552  >>> b = FPSort(8, 24)
9553  >>> b.sbits()
9554  24
9555  """
9556  return self.sort().sbits()
9557 
def sbits(self)
Definition: z3py.py:9550
def sort(self)
Definition: z3py.py:974
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 9531 of file z3py.py.

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

9531  def sort(self):
9532  """Return the sort of the floating-point expression `self`.
9533 
9534  >>> x = FP('1.0', FPSort(8, 24))
9535  >>> x.sort()
9536  FPSort(8, 24)
9537  >>> x.sort() == FPSort(8, 24)
9538  True
9539  """
9540  return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
9541 
def as_ast(self)
Definition: z3py.py:392
def sort(self)
Definition: z3py.py:9531
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.