RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3py_1_1_f_p_ref.html below:

Z3: FPRef Class Reference

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) def as_ast (self) def get_id (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) def __init__ (self, ast, ctx=None) def __del__ (self) def __deepcopy__ (self, memo={}) def __str__ (self) def __repr__ (self) def __nonzero__ (self) def __bool__ (self) def sexpr (self) def ctx_ref (self) def eq (self, other) def translate (self, target) def __copy__ (self) def hash (self) def use_pp (self)

Floating-point expressions.

Definition at line 9613 of file z3py.py.

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

9659 def

__add__(self, other):

9660 """Create the Z3 expression `self + other`. 9662 >>> x = FP('x', FPSort(8, 24)) 9663 >>> y = FP('y', FPSort(8, 24)) 9669

[a, b] = _coerce_fp_expr_list([self, other], self.ctx)

9670 return fpAdd

(_dflt_rm(), a, b, self.ctx)

def fpAdd(rm, a, b, ctx=None)

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

9746 def

__div__(self, other):

9747 """Create the Z3 expression `self / other`. 9749 >>> x = FP('x', FPSort(8, 24)) 9750 >>> y = FP('y', FPSort(8, 24)) 9758

[a, b] = _coerce_fp_expr_list([self, other], self.ctx)

9759 return fpDiv

(_dflt_rm(), a, b, self.ctx)

def fpDiv(rm, a, b, ctx=None)

Referenced by ArithRef.__truediv__(), BitVecRef.__truediv__(), and FPRef.__truediv__().

◆ __ge__() def __ge__ ( self, other )

Definition at line 9653 of file z3py.py.

9653 def

__ge__(self, other):

9654 return fpGEQ

(self, other, self.ctx)

def fpGEQ(a, b, ctx=None)

◆ __gt__() def __gt__ ( self, other )

Definition at line 9656 of file z3py.py.

9656 def

__gt__(self, other):

9657 return fpGT

(self, other, self.ctx)

◆ __le__() def __le__ ( self, other )

Definition at line 9647 of file z3py.py.

9647 def

__le__(self, other):

9648 return fpLEQ

(self, other, self.ctx)

def fpLEQ(a, b, ctx=None)

◆ __lt__() def __lt__ ( self, other )

Definition at line 9650 of file z3py.py.

9650 def

__lt__(self, other):

9651 return fpLT

(self, other, self.ctx)

◆ __mod__() def __mod__ ( self, other )

Create the Z3 expression mod `self % other`.

Definition at line 9782 of file z3py.py.

9782 def

__mod__(self, other):

9783 """Create the Z3 expression mod `self % other`.""" 9784 return fpRem

(self, other)

def fpRem(a, b, ctx=None)

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

9705 def

__mul__(self, other):

9706 """Create the Z3 expression `self * other`. 9708 >>> x = FP('x', FPSort(8, 24)) 9709 >>> y = FP('y', FPSort(8, 24)) 9717

[a, b] = _coerce_fp_expr_list([self, other], self.ctx)

9718 return fpMul

(_dflt_rm(), a, b, self.ctx)

def fpMul(rm, a, b, ctx=None)

◆ __neg__()

Create the Z3 expression `-self`.

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

Definition at line 9737 of file z3py.py.

9738 """Create the Z3 expression `-self`. 9740 >>> x = FP('x', Float32()) ◆ __pos__()

Create the Z3 expression `+self`.

Definition at line 9733 of file z3py.py.

9734 """Create the Z3 expression `+self`.""" ◆ __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 9672 of file z3py.py.

9672 def

__radd__(self, other):

9673 """Create the Z3 expression `other + self`. 9675 >>> x = FP('x', FPSort(8, 24)) 9679

[a, b] = _coerce_fp_expr_list([other, self], self.ctx)

9680 return fpAdd

(_dflt_rm(), a, b, self.ctx)

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

9761 def

__rdiv__(self, other):

9762 """Create the Z3 expression `other / self`. 9764 >>> x = FP('x', FPSort(8, 24)) 9765 >>> y = FP('y', FPSort(8, 24)) 9771

[a, b] = _coerce_fp_expr_list([other, self], self.ctx)

9772 return fpDiv

(_dflt_rm(), a, b, self.ctx)

Referenced by ArithRef.__rtruediv__(), BitVecRef.__rtruediv__(), and FPRef.__rtruediv__().

◆ __rmod__() def __rmod__ ( self, other )

Create the Z3 expression mod `other % self`.

Definition at line 9786 of file z3py.py.

9786 def

__rmod__(self, other):

9787 """Create the Z3 expression mod `other % self`.""" 9788 return fpRem

(other, self)

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

9720 def

__rmul__(self, other):

9721 """Create the Z3 expression `other * self`. 9723 >>> x = FP('x', FPSort(8, 24)) 9724 >>> y = FP('y', FPSort(8, 24)) 9730

[a, b] = _coerce_fp_expr_list([other, self], self.ctx)

9731 return fpMul

(_dflt_rm(), a, b, self.ctx)

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

9695 def

__rsub__(self, other):

9696 """Create the Z3 expression `other - self`. 9698 >>> x = FP('x', FPSort(8, 24)) 9702

[a, b] = _coerce_fp_expr_list([other, self], self.ctx)

9703 return fpSub

(_dflt_rm(), a, b, self.ctx)

def fpSub(rm, a, b, ctx=None)

◆ __rtruediv__() def __rtruediv__ ( self, other )

Create the Z3 expression division `other / self`.

Definition at line 9778 of file z3py.py.

9778 def

__rtruediv__(self, other):

9779 """Create the Z3 expression division `other / self`.""" 9780 return

self.__rdiv__(other)

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

9682 def

__sub__(self, other):

9683 """Create the Z3 expression `self - other`. 9685 >>> x = FP('x', FPSort(8, 24)) 9686 >>> y = FP('y', FPSort(8, 24)) 9692

[a, b] = _coerce_fp_expr_list([self, other], self.ctx)

9693 return fpSub

(_dflt_rm(), a, b, self.ctx)

◆ __truediv__() def __truediv__ ( self, other )

Create the Z3 expression division `self / other`.

Definition at line 9774 of file z3py.py.

9774 def

__truediv__(self, other):

9775 """Create the Z3 expression division `self / other`.""" 9776 return

self.__div__(other)

◆ as_string() ◆ ebits()

Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
>>> b = FPSort(8, 24)
>>> b.ebits()
8

Definition at line 9627 of file z3py.py.

9628 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. 9629 >>> b = FPSort(8, 24) 9633 return

self.sort().ebits()

◆ sbits()

Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
>>> b = FPSort(8, 24)
>>> b.sbits()
24

Definition at line 9635 of file z3py.py.

9636 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. 9637 >>> b = FPSort(8, 24) 9641 return

self.sort().sbits()

◆ sort()

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

9617 """Return the sort of the floating-point expression `self`. 9619 >>> x = FP('1.0', FPSort(8, 24)) 9622 >>> x.sort() == FPSort(8, 24) 9625 return

FPSortRef(

Z3_get_sort

(self.ctx_ref(), self.as_ast()), self.ctx)

Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)

Return the sort of an AST node.

Referenced by FPNumRef.as_string(), ArrayRef.domain(), ArrayRef.domain_n(), FPRef.ebits(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), FPRef.sbits(), BitVecRef.size(), and ExprRef.sort_kind().

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4