RetroSearch Browse

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

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

Z3: BitVecRef Class Reference

def sort (self) def size (self) def __add__ (self, other) def __radd__ (self, other) def __mul__ (self, other) def __rmul__ (self, other) def __sub__ (self, other) def __rsub__ (self, other) def __or__ (self, other) def __ror__ (self, other) def __and__ (self, other) def __rand__ (self, other) def __xor__ (self, other) def __rxor__ (self, other) def __pos__ (self) def __neg__ (self) def __invert__ (self) def __div__ (self, other) def __truediv__ (self, other) def __rdiv__ (self, other) def __rtruediv__ (self, other) def __mod__ (self, other) def __rmod__ (self, other) def __le__ (self, other) def __lt__ (self, other) def __gt__ (self, other) def __ge__ (self, other) def __rshift__ (self, other) def __lshift__ (self, other) def __rrshift__ (self, other) def __rlshift__ (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)

Bit-vector expressions.

Definition at line 3533 of file z3py.py.

◆ __add__() def __add__ ( self, other )

Create the Z3 expression `self + other`.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x + y
x + y
>>> (x + y).sort()
BitVec(32)

Definition at line 3558 of file z3py.py.

3558 def

__add__(self, other):

3559 """Create the Z3 expression `self + other`. 3561 >>> x = BitVec('x', 32) 3562 >>> y = BitVec('y', 32) 3568

a, b = _coerce_exprs(self, other)

3569 return

BitVecRef(

Z3_mk_bvadd

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

Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)

Standard two's complement addition.

◆ __and__() def __and__ ( self, other )

Create the Z3 expression bitwise-and `self & other`.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x & y
x & y
>>> (x & y).sort()
BitVec(32)

Definition at line 3650 of file z3py.py.

3650 def

__and__(self, other):

3651 """Create the Z3 expression bitwise-and `self & other`. 3653 >>> x = BitVec('x', 32) 3654 >>> y = BitVec('y', 32) 3660

a, b = _coerce_exprs(self, other)

3661 return

BitVecRef(

Z3_mk_bvand

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

Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise and.

◆ __div__() def __div__ ( self, other )

Create the Z3 expression (signed) division `self / other`.

Use the function UDiv() for unsigned division.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x / y
x/y
>>> (x / y).sort()
BitVec(32)
>>> (x / y).sexpr()
'(bvsdiv x y)'
>>> UDiv(x, y).sexpr()
'(bvudiv x y)'

Definition at line 3727 of file z3py.py.

3727 def

__div__(self, other):

3728 """Create the Z3 expression (signed) division `self / other`. 3730 Use the function UDiv() for unsigned division. 3732 >>> x = BitVec('x', 32) 3733 >>> y = BitVec('y', 32) 3740 >>> UDiv(x, y).sexpr() 3743

a, b = _coerce_exprs(self, other)

3744 return

BitVecRef(

Z3_mk_bvsdiv

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

Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed division.

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

◆ __ge__() def __ge__ ( self, other )

Create the Z3 expression (signed) `other >= self`.

Use the function UGE() for unsigned greater than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> x >= y
x >= y
>>> (x >= y).sexpr()
'(bvsge x y)'
>>> UGE(x, y).sexpr()
'(bvuge x y)'

Definition at line 3857 of file z3py.py.

3857 def

__ge__(self, other):

3858 """Create the Z3 expression (signed) `other >= self`. 3860 Use the function UGE() for unsigned greater than or equal to. 3862 >>> x, y = BitVecs('x y', 32) 3865 >>> (x >= y).sexpr() 3867 >>> UGE(x, y).sexpr() 3870

a, b = _coerce_exprs(self, other)

3871 return

BoolRef(

Z3_mk_bvsge

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

Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed greater than or equal to.

◆ __gt__() def __gt__ ( self, other )

Create the Z3 expression (signed) `other > self`.

Use the function UGT() for unsigned greater than.

>>> x, y = BitVecs('x y', 32)
>>> x > y
x > y
>>> (x > y).sexpr()
'(bvsgt x y)'
>>> UGT(x, y).sexpr()
'(bvugt x y)'

Definition at line 3841 of file z3py.py.

3841 def

__gt__(self, other):

3842 """Create the Z3 expression (signed) `other > self`. 3844 Use the function UGT() for unsigned greater than. 3846 >>> x, y = BitVecs('x y', 32) 3851 >>> UGT(x, y).sexpr() 3854

a, b = _coerce_exprs(self, other)

3855 return

BoolRef(

Z3_mk_bvsgt

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

Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed greater than.

◆ __invert__()

Create the Z3 expression bitwise-not `~self`.

>>> x = BitVec('x', 32)
>>> ~x
~x
>>> simplify(~(~x))
x

Definition at line 3716 of file z3py.py.

3716 def

__invert__(self):

3717 """Create the Z3 expression bitwise-not `~self`. 3719 >>> x = BitVec('x', 32) 3725 return

BitVecRef(

Z3_mk_bvnot

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

Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)

Bitwise negation.

◆ __le__() def __le__ ( self, other )

Create the Z3 expression (signed) `other <= self`.

Use the function ULE() for unsigned less than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> x <= y
x <= y
>>> (x <= y).sexpr()
'(bvsle x y)'
>>> ULE(x, y).sexpr()
'(bvule x y)'

Definition at line 3809 of file z3py.py.

3809 def

__le__(self, other):

3810 """Create the Z3 expression (signed) `other <= self`. 3812 Use the function ULE() for unsigned less than or equal to. 3814 >>> x, y = BitVecs('x y', 32) 3817 >>> (x <= y).sexpr() 3819 >>> ULE(x, y).sexpr() 3822

a, b = _coerce_exprs(self, other)

3823 return

BoolRef(

Z3_mk_bvsle

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

Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed less than or equal to.

◆ __lshift__() def __lshift__ ( self, other )

Create the Z3 expression left shift `self << other`

>>> x, y = BitVecs('x y', 32)
>>> x << y
x << y
>>> (x << y).sexpr()
'(bvshl x y)'
>>> simplify(BitVecVal(2, 3) << 1)
4

Definition at line 3903 of file z3py.py.

3903 def

__lshift__(self, other):

3904 """Create the Z3 expression left shift `self << other` 3906 >>> x, y = BitVecs('x y', 32) 3909 >>> (x << y).sexpr() 3911 >>> simplify(BitVecVal(2, 3) << 1) 3914

a, b = _coerce_exprs(self, other)

3915 return

BitVecRef(

Z3_mk_bvshl

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

Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)

Shift left.

◆ __lt__() def __lt__ ( self, other )

Create the Z3 expression (signed) `other < self`.

Use the function ULT() for unsigned less than.

>>> x, y = BitVecs('x y', 32)
>>> x < y
x < y
>>> (x < y).sexpr()
'(bvslt x y)'
>>> ULT(x, y).sexpr()
'(bvult x y)'

Definition at line 3825 of file z3py.py.

3825 def

__lt__(self, other):

3826 """Create the Z3 expression (signed) `other < self`. 3828 Use the function ULT() for unsigned less than. 3830 >>> x, y = BitVecs('x y', 32) 3835 >>> ULT(x, y).sexpr() 3838

a, b = _coerce_exprs(self, other)

3839 return

BoolRef(

Z3_mk_bvslt

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

Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed less than.

◆ __mod__() def __mod__ ( self, other )

Create the Z3 expression (signed) mod `self % other`.

Use the function URem() for unsigned remainder, and SRem() for signed remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x % y
x%y
>>> (x % y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> URem(x, y).sexpr()
'(bvurem x y)'
>>> SRem(x, y).sexpr()
'(bvsrem x y)'

Definition at line 3770 of file z3py.py.

3770 def

__mod__(self, other):

3771 """Create the Z3 expression (signed) mod `self % other`. 3773 Use the function URem() for unsigned remainder, and SRem() for signed remainder. 3775 >>> x = BitVec('x', 32) 3776 >>> y = BitVec('y', 32) 3783 >>> URem(x, y).sexpr() 3785 >>> SRem(x, y).sexpr() 3788

a, b = _coerce_exprs(self, other)

3789 return

BitVecRef(

Z3_mk_bvsmod

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

Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed remainder (sign follows divisor).

◆ __mul__() def __mul__ ( self, other )

Create the Z3 expression `self * other`.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x * y
x*y
>>> (x * y).sort()
BitVec(32)

Definition at line 3581 of file z3py.py.

3581 def

__mul__(self, other):

3582 """Create the Z3 expression `self * other`. 3584 >>> x = BitVec('x', 32) 3585 >>> y = BitVec('y', 32) 3591

a, b = _coerce_exprs(self, other)

3592 return

BitVecRef(

Z3_mk_bvmul

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

Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)

Standard two's complement multiplication.

◆ __neg__()

Return an expression representing `-self`.

>>> x = BitVec('x', 32)
>>> -x
-x
>>> simplify(-(-x))
x

Definition at line 3705 of file z3py.py.

3706 """Return an expression representing `-self`. 3708 >>> x = BitVec('x', 32) 3714 return

BitVecRef(

Z3_mk_bvneg

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

Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)

Standard two's complement unary minus.

◆ __or__() def __or__ ( self, other )

Create the Z3 expression bitwise-or `self | other`.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x | y
x | y
>>> (x | y).sort()
BitVec(32)

Definition at line 3627 of file z3py.py.

3627 def

__or__(self, other):

3628 """Create the Z3 expression bitwise-or `self | other`. 3630 >>> x = BitVec('x', 32) 3631 >>> y = BitVec('y', 32) 3637

a, b = _coerce_exprs(self, other)

3638 return

BitVecRef(

Z3_mk_bvor

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

Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise or.

◆ __pos__()

Return `self`.

>>> x = BitVec('x', 32)
>>> +x
x

Definition at line 3696 of file z3py.py.

3699 >>> x = BitVec('x', 32) ◆ __radd__() def __radd__ ( self, other )

Create the Z3 expression `other + self`.

>>> x = BitVec('x', 32)
>>> 10 + x
10 + x

Definition at line 3571 of file z3py.py.

3571 def

__radd__(self, other):

3572 """Create the Z3 expression `other + self`. 3574 >>> x = BitVec('x', 32) 3578

a, b = _coerce_exprs(self, other)

3579 return

BitVecRef(

Z3_mk_bvadd

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

◆ __rand__() def __rand__ ( self, other )

Create the Z3 expression bitwise-or `other & self`.

>>> x = BitVec('x', 32)
>>> 10 & x
10 & x

Definition at line 3663 of file z3py.py.

3663 def

__rand__(self, other):

3664 """Create the Z3 expression bitwise-or `other & self`. 3666 >>> x = BitVec('x', 32) 3670

a, b = _coerce_exprs(self, other)

3671 return

BitVecRef(

Z3_mk_bvand

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

◆ __rdiv__() def __rdiv__ ( self, other )

Create the Z3 expression (signed) division `other / self`.

Use the function UDiv() for unsigned division.

>>> x = BitVec('x', 32)
>>> 10 / x
10/x
>>> (10 / x).sexpr()
'(bvsdiv #x0000000a x)'
>>> UDiv(10, x).sexpr()
'(bvudiv #x0000000a x)'

Definition at line 3750 of file z3py.py.

3750 def

__rdiv__(self, other):

3751 """Create the Z3 expression (signed) division `other / self`. 3753 Use the function UDiv() for unsigned division. 3755 >>> x = BitVec('x', 32) 3758 >>> (10 / x).sexpr() 3759 '(bvsdiv #x0000000a x)' 3760 >>> UDiv(10, x).sexpr() 3761 '(bvudiv #x0000000a x)' 3763

a, b = _coerce_exprs(self, other)

3764 return

BitVecRef(

Z3_mk_bvsdiv

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

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

◆ __rlshift__() def __rlshift__ ( self, other )

Create the Z3 expression left shift `other << self`.

Use the function LShR() for the right logical shift

>>> x = BitVec('x', 32)
>>> 10 << x
10 << x
>>> (10 << x).sexpr()
'(bvshl #x0000000a x)'

Definition at line 3931 of file z3py.py.

3931 def

__rlshift__(self, other):

3932 """Create the Z3 expression left shift `other << self`. 3934 Use the function LShR() for the right logical shift 3936 >>> x = BitVec('x', 32) 3939 >>> (10 << x).sexpr() 3940 '(bvshl #x0000000a x)' 3942

a, b = _coerce_exprs(self, other)

3943 return

BitVecRef(

Z3_mk_bvshl

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

◆ __rmod__() def __rmod__ ( self, other )

Create the Z3 expression (signed) mod `other % self`.

Use the function URem() for unsigned remainder, and SRem() for signed remainder.

>>> x = BitVec('x', 32)
>>> 10 % x
10%x
>>> (10 % x).sexpr()
'(bvsmod #x0000000a x)'
>>> URem(10, x).sexpr()
'(bvurem #x0000000a x)'
>>> SRem(10, x).sexpr()
'(bvsrem #x0000000a x)'

Definition at line 3791 of file z3py.py.

3791 def

__rmod__(self, other):

3792 """Create the Z3 expression (signed) mod `other % self`. 3794 Use the function URem() for unsigned remainder, and SRem() for signed remainder. 3796 >>> x = BitVec('x', 32) 3799 >>> (10 % x).sexpr() 3800 '(bvsmod #x0000000a x)' 3801 >>> URem(10, x).sexpr() 3802 '(bvurem #x0000000a x)' 3803 >>> SRem(10, x).sexpr() 3804 '(bvsrem #x0000000a x)' 3806

a, b = _coerce_exprs(self, other)

3807 return

BitVecRef(

Z3_mk_bvsmod

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

◆ __rmul__() def __rmul__ ( self, other )

Create the Z3 expression `other * self`.

>>> x = BitVec('x', 32)
>>> 10 * x
10*x

Definition at line 3594 of file z3py.py.

3594 def

__rmul__(self, other):

3595 """Create the Z3 expression `other * self`. 3597 >>> x = BitVec('x', 32) 3601

a, b = _coerce_exprs(self, other)

3602 return

BitVecRef(

Z3_mk_bvmul

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

◆ __ror__() def __ror__ ( self, other )

Create the Z3 expression bitwise-or `other | self`.

>>> x = BitVec('x', 32)
>>> 10 | x
10 | x

Definition at line 3640 of file z3py.py.

3640 def

__ror__(self, other):

3641 """Create the Z3 expression bitwise-or `other | self`. 3643 >>> x = BitVec('x', 32) 3647

a, b = _coerce_exprs(self, other)

3648 return

BitVecRef(

Z3_mk_bvor

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

◆ __rrshift__() def __rrshift__ ( self, other )

Create the Z3 expression (arithmetical) right shift `other` >> `self`.

Use the function LShR() for the right logical shift

>>> x = BitVec('x', 32)
>>> 10 >> x
10 >> x
>>> (10 >> x).sexpr()
'(bvashr #x0000000a x)'

Definition at line 3917 of file z3py.py.

3917 def

__rrshift__(self, other):

3918 """Create the Z3 expression (arithmetical) right shift `other` >> `self`. 3920 Use the function LShR() for the right logical shift 3922 >>> x = BitVec('x', 32) 3925 >>> (10 >> x).sexpr() 3926 '(bvashr #x0000000a x)' 3928

a, b = _coerce_exprs(self, other)

3929 return

BitVecRef(

Z3_mk_bvashr

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

Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)

Arithmetic shift right.

◆ __rshift__() def __rshift__ ( self, other )

Create the Z3 expression (arithmetical) right shift `self >> other`

Use the function LShR() for the right logical shift

>>> x, y = BitVecs('x y', 32)
>>> x >> y
x >> y
>>> (x >> y).sexpr()
'(bvashr x y)'
>>> LShR(x, y).sexpr()
'(bvlshr x y)'
>>> BitVecVal(4, 3)
4
>>> BitVecVal(4, 3).as_signed_long()
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2
>>> simplify(BitVecVal(4, 3) >> 1)
6
>>> simplify(LShR(BitVecVal(4, 3), 1))
2
>>> simplify(BitVecVal(2, 3) >> 1)
1
>>> simplify(LShR(BitVecVal(2, 3), 1))
1

Definition at line 3873 of file z3py.py.

3873 def

__rshift__(self, other):

3874 """Create the Z3 expression (arithmetical) right shift `self >> other` 3876 Use the function LShR() for the right logical shift 3878 >>> x, y = BitVecs('x y', 32) 3881 >>> (x >> y).sexpr() 3883 >>> LShR(x, y).sexpr() 3887 >>> BitVecVal(4, 3).as_signed_long() 3889 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() 3891 >>> simplify(BitVecVal(4, 3) >> 1) 3893 >>> simplify(LShR(BitVecVal(4, 3), 1)) 3895 >>> simplify(BitVecVal(2, 3) >> 1) 3897 >>> simplify(LShR(BitVecVal(2, 3), 1)) 3900

a, b = _coerce_exprs(self, other)

3901 return

BitVecRef(

Z3_mk_bvashr

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

◆ __rsub__() def __rsub__ ( self, other )

Create the Z3 expression `other - self`.

>>> x = BitVec('x', 32)
>>> 10 - x
10 - x

Definition at line 3617 of file z3py.py.

3617 def

__rsub__(self, other):

3618 """Create the Z3 expression `other - self`. 3620 >>> x = BitVec('x', 32) 3624

a, b = _coerce_exprs(self, other)

3625 return

BitVecRef(

Z3_mk_bvsub

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

Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)

Standard two's complement subtraction.

◆ __rtruediv__() def __rtruediv__ ( self, other )

Create the Z3 expression (signed) division `other / self`.

Definition at line 3766 of file z3py.py.

3766 def

__rtruediv__(self, other):

3767 """Create the Z3 expression (signed) division `other / self`.""" 3768 return

self.__rdiv__(other)

◆ __rxor__() def __rxor__ ( self, other )

Create the Z3 expression bitwise-xor `other ^ self`.

>>> x = BitVec('x', 32)
>>> 10 ^ x
10 ^ x

Definition at line 3686 of file z3py.py.

3686 def

__rxor__(self, other):

3687 """Create the Z3 expression bitwise-xor `other ^ self`. 3689 >>> x = BitVec('x', 32) 3693

a, b = _coerce_exprs(self, other)

3694 return

BitVecRef(

Z3_mk_bvxor

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

Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise exclusive-or.

◆ __sub__() def __sub__ ( self, other )

Create the Z3 expression `self - other`.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x - y
x - y
>>> (x - y).sort()
BitVec(32)

Definition at line 3604 of file z3py.py.

3604 def

__sub__(self, other):

3605 """Create the Z3 expression `self - other`. 3607 >>> x = BitVec('x', 32) 3608 >>> y = BitVec('y', 32) 3614

a, b = _coerce_exprs(self, other)

3615 return

BitVecRef(

Z3_mk_bvsub

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

◆ __truediv__() def __truediv__ ( self, other )

Create the Z3 expression (signed) division `self / other`.

Definition at line 3746 of file z3py.py.

3746 def

__truediv__(self, other):

3747 """Create the Z3 expression (signed) division `self / other`.""" 3748 return

self.__div__(other)

◆ __xor__() def __xor__ ( self, other )

Create the Z3 expression bitwise-xor `self ^ other`.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x ^ y
x ^ y
>>> (x ^ y).sort()
BitVec(32)

Definition at line 3673 of file z3py.py.

3673 def

__xor__(self, other):

3674 """Create the Z3 expression bitwise-xor `self ^ other`. 3676 >>> x = BitVec('x', 32) 3677 >>> y = BitVec('y', 32) 3683

a, b = _coerce_exprs(self, other)

3684 return

BitVecRef(

Z3_mk_bvxor

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

◆ size() ◆ sort()

Return the sort of the bit-vector expression `self`.

>>> x = BitVec('x', 32)
>>> x.sort()
BitVec(32)
>>> x.sort() == BitVecSort(32)
True

Reimplemented from ExprRef.

Definition at line 3536 of file z3py.py.

3537 """Return the sort of the bit-vector expression `self`. 3539 >>> x = BitVec('x', 32) 3542 >>> x.sort() == BitVecSort(32) 3545 return

BitVecSortRef(

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