Z3
Public Member Functions
BitVecRef Class Reference
+ Inheritance diagram for BitVecRef:

Public Member Functions

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)
 
- 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)
 
- Public Member Functions inherited from AstRef
def __init__ (self, ast, ctx=None)
 
def __del__ (self)
 
def __deepcopy__ (self, memo={})
 
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

Bit-vector expressions.

Definition at line 3198 of file z3py.py.

Member Function Documentation

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

3223  def __add__(self, other):
3224  """Create the Z3 expression `self + other`.
3225 
3226  >>> x = BitVec('x', 32)
3227  >>> y = BitVec('y', 32)
3228  >>> x + y
3229  x + y
3230  >>> (x + y).sort()
3231  BitVec(32)
3232  """
3233  a, b = _coerce_exprs(self, other)
3234  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3235 
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 3315 of file z3py.py.

3315  def __and__(self, other):
3316  """Create the Z3 expression bitwise-and `self & other`.
3317 
3318  >>> x = BitVec('x', 32)
3319  >>> y = BitVec('y', 32)
3320  >>> x & y
3321  x & y
3322  >>> (x & y).sort()
3323  BitVec(32)
3324  """
3325  a, b = _coerce_exprs(self, other)
3326  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3327 
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 3392 of file z3py.py.

3392  def __div__(self, other):
3393  """Create the Z3 expression (signed) division `self / other`.
3394 
3395  Use the function UDiv() for unsigned division.
3396 
3397  >>> x = BitVec('x', 32)
3398  >>> y = BitVec('y', 32)
3399  >>> x / y
3400  x/y
3401  >>> (x / y).sort()
3402  BitVec(32)
3403  >>> (x / y).sexpr()
3404  '(bvsdiv x y)'
3405  >>> UDiv(x, y).sexpr()
3406  '(bvudiv x y)'
3407  """
3408  a, b = _coerce_exprs(self, other)
3409  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3410 
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.

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

3522  def __ge__(self, other):
3523  """Create the Z3 expression (signed) `other >= self`.
3524 
3525  Use the function UGE() for unsigned greater than or equal to.
3526 
3527  >>> x, y = BitVecs('x y', 32)
3528  >>> x >= y
3529  x >= y
3530  >>> (x >= y).sexpr()
3531  '(bvsge x y)'
3532  >>> UGE(x, y).sexpr()
3533  '(bvuge x y)'
3534  """
3535  a, b = _coerce_exprs(self, other)
3536  return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3537 
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 3506 of file z3py.py.

3506  def __gt__(self, other):
3507  """Create the Z3 expression (signed) `other > self`.
3508 
3509  Use the function UGT() for unsigned greater than.
3510 
3511  >>> x, y = BitVecs('x y', 32)
3512  >>> x > y
3513  x > y
3514  >>> (x > y).sexpr()
3515  '(bvsgt x y)'
3516  >>> UGT(x, y).sexpr()
3517  '(bvugt x y)'
3518  """
3519  a, b = _coerce_exprs(self, other)
3520  return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3521 
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.

◆ __invert__()

def __invert__ (   self)
Create the Z3 expression bitwise-not `~self`.

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

Definition at line 3381 of file z3py.py.

3381  def __invert__(self):
3382  """Create the Z3 expression bitwise-not `~self`.
3383 
3384  >>> x = BitVec('x', 32)
3385  >>> ~x
3386  ~x
3387  >>> simplify(~(~x))
3388  x
3389  """
3390  return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)
3391 
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 3474 of file z3py.py.

3474  def __le__(self, other):
3475  """Create the Z3 expression (signed) `other <= self`.
3476 
3477  Use the function ULE() for unsigned less than or equal to.
3478 
3479  >>> x, y = BitVecs('x y', 32)
3480  >>> x <= y
3481  x <= y
3482  >>> (x <= y).sexpr()
3483  '(bvsle x y)'
3484  >>> ULE(x, y).sexpr()
3485  '(bvule x y)'
3486  """
3487  a, b = _coerce_exprs(self, other)
3488  return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3489 
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;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 3568 of file z3py.py.

3568  def __lshift__(self, other):
3569  """Create the Z3 expression left shift `self << other`
3570 
3571  >>> x, y = BitVecs('x y', 32)
3572  >>> x << y
3573  x << y
3574  >>> (x << y).sexpr()
3575  '(bvshl x y)'
3576  >>> simplify(BitVecVal(2, 3) << 1)
3577  4
3578  """
3579  a, b = _coerce_exprs(self, other)
3580  return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3581 
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 3490 of file z3py.py.

3490  def __lt__(self, other):
3491  """Create the Z3 expression (signed) `other < self`.
3492 
3493  Use the function ULT() for unsigned less than.
3494 
3495  >>> x, y = BitVecs('x y', 32)
3496  >>> x < y
3497  x < y
3498  >>> (x < y).sexpr()
3499  '(bvslt x y)'
3500  >>> ULT(x, y).sexpr()
3501  '(bvult x y)'
3502  """
3503  a, b = _coerce_exprs(self, other)
3504  return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3505 
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;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 3435 of file z3py.py.

3435  def __mod__(self, other):
3436  """Create the Z3 expression (signed) mod `self % other`.
3437 
3438  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3439 
3440  >>> x = BitVec('x', 32)
3441  >>> y = BitVec('y', 32)
3442  >>> x % y
3443  x%y
3444  >>> (x % y).sort()
3445  BitVec(32)
3446  >>> (x % y).sexpr()
3447  '(bvsmod x y)'
3448  >>> URem(x, y).sexpr()
3449  '(bvurem x y)'
3450  >>> SRem(x, y).sexpr()
3451  '(bvsrem x y)'
3452  """
3453  a, b = _coerce_exprs(self, other)
3454  return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3455 
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;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 3246 of file z3py.py.

3246  def __mul__(self, other):
3247  """Create the Z3 expression `self * other`.
3248 
3249  >>> x = BitVec('x', 32)
3250  >>> y = BitVec('y', 32)
3251  >>> x * y
3252  x*y
3253  >>> (x * y).sort()
3254  BitVec(32)
3255  """
3256  a, b = _coerce_exprs(self, other)
3257  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3258 
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement multiplication.

◆ __neg__()

def __neg__ (   self)
Return an expression representing `-self`.

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

Definition at line 3370 of file z3py.py.

3370  def __neg__(self):
3371  """Return an expression representing `-self`.
3372 
3373  >>> x = BitVec('x', 32)
3374  >>> -x
3375  -x
3376  >>> simplify(-(-x))
3377  x
3378  """
3379  return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)
3380 
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two&#39;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 3292 of file z3py.py.

3292  def __or__(self, other):
3293  """Create the Z3 expression bitwise-or `self | other`.
3294 
3295  >>> x = BitVec('x', 32)
3296  >>> y = BitVec('y', 32)
3297  >>> x | y
3298  x | y
3299  >>> (x | y).sort()
3300  BitVec(32)
3301  """
3302  a, b = _coerce_exprs(self, other)
3303  return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3304 
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.

◆ __pos__()

def __pos__ (   self)
Return `self`.

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

Definition at line 3361 of file z3py.py.

3361  def __pos__(self):
3362  """Return `self`.
3363 
3364  >>> x = BitVec('x', 32)
3365  >>> +x
3366  x
3367  """
3368  return self
3369 

◆ __radd__()

def __radd__ (   self,
  other 
)
Create the Z3 expression `other + self`.

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

Definition at line 3236 of file z3py.py.

3236  def __radd__(self, other):
3237  """Create the Z3 expression `other + self`.
3238 
3239  >>> x = BitVec('x', 32)
3240  >>> 10 + x
3241  10 + x
3242  """
3243  a, b = _coerce_exprs(self, other)
3244  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3245 
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement addition.

◆ __rand__()

def __rand__ (   self,
  other 
)
Create the Z3 expression bitwise-or `other & self`.

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

Definition at line 3328 of file z3py.py.

3328  def __rand__(self, other):
3329  """Create the Z3 expression bitwise-or `other & self`.
3330 
3331  >>> x = BitVec('x', 32)
3332  >>> 10 & x
3333  10 & x
3334  """
3335  a, b = _coerce_exprs(self, other)
3336  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3337 
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.

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

3415  def __rdiv__(self, other):
3416  """Create the Z3 expression (signed) division `other / self`.
3417 
3418  Use the function UDiv() for unsigned division.
3419 
3420  >>> x = BitVec('x', 32)
3421  >>> 10 / x
3422  10/x
3423  >>> (10 / x).sexpr()
3424  '(bvsdiv #x0000000a x)'
3425  >>> UDiv(10, x).sexpr()
3426  '(bvudiv #x0000000a x)'
3427  """
3428  a, b = _coerce_exprs(self, other)
3429  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3430 
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed division.

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

3596  def __rlshift__(self, other):
3597  """Create the Z3 expression left shift `other << self`.
3598 
3599  Use the function LShR() for the right logical shift
3600 
3601  >>> x = BitVec('x', 32)
3602  >>> 10 << x
3603  10 << x
3604  >>> (10 << x).sexpr()
3605  '(bvshl #x0000000a x)'
3606  """
3607  a, b = _coerce_exprs(self, other)
3608  return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3609 
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.

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

3456  def __rmod__(self, other):
3457  """Create the Z3 expression (signed) mod `other % self`.
3458 
3459  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3460 
3461  >>> x = BitVec('x', 32)
3462  >>> 10 % x
3463  10%x
3464  >>> (10 % x).sexpr()
3465  '(bvsmod #x0000000a x)'
3466  >>> URem(10, x).sexpr()
3467  '(bvurem #x0000000a x)'
3468  >>> SRem(10, x).sexpr()
3469  '(bvsrem #x0000000a x)'
3470  """
3471  a, b = _coerce_exprs(self, other)
3472  return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3473 
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed remainder (sign follows divisor).

◆ __rmul__()

def __rmul__ (   self,
  other 
)
Create the Z3 expression `other * self`.

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

Definition at line 3259 of file z3py.py.

3259  def __rmul__(self, other):
3260  """Create the Z3 expression `other * self`.
3261 
3262  >>> x = BitVec('x', 32)
3263  >>> 10 * x
3264  10*x
3265  """
3266  a, b = _coerce_exprs(self, other)
3267  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3268 
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement multiplication.

◆ __ror__()

def __ror__ (   self,
  other 
)
Create the Z3 expression bitwise-or `other | self`.

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

Definition at line 3305 of file z3py.py.

3305  def __ror__(self, other):
3306  """Create the Z3 expression bitwise-or `other | self`.
3307 
3308  >>> x = BitVec('x', 32)
3309  >>> 10 | x
3310  10 | x
3311  """
3312  a, b = _coerce_exprs(self, other)
3313  return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3314 
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.

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

3582  def __rrshift__(self, other):
3583  """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3584 
3585  Use the function LShR() for the right logical shift
3586 
3587  >>> x = BitVec('x', 32)
3588  >>> 10 >> x
3589  10 >> x
3590  >>> (10 >> x).sexpr()
3591  '(bvashr #x0000000a x)'
3592  """
3593  a, b = _coerce_exprs(self, other)
3594  return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3595 
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 3538 of file z3py.py.

3538  def __rshift__(self, other):
3539  """Create the Z3 expression (arithmetical) right shift `self >> other`
3540 
3541  Use the function LShR() for the right logical shift
3542 
3543  >>> x, y = BitVecs('x y', 32)
3544  >>> x >> y
3545  x >> y
3546  >>> (x >> y).sexpr()
3547  '(bvashr x y)'
3548  >>> LShR(x, y).sexpr()
3549  '(bvlshr x y)'
3550  >>> BitVecVal(4, 3)
3551  4
3552  >>> BitVecVal(4, 3).as_signed_long()
3553  -4
3554  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3555  -2
3556  >>> simplify(BitVecVal(4, 3) >> 1)
3557  6
3558  >>> simplify(LShR(BitVecVal(4, 3), 1))
3559  2
3560  >>> simplify(BitVecVal(2, 3) >> 1)
3561  1
3562  >>> simplify(LShR(BitVecVal(2, 3), 1))
3563  1
3564  """
3565  a, b = _coerce_exprs(self, other)
3566  return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3567 
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.

◆ __rsub__()

def __rsub__ (   self,
  other 
)
Create the Z3 expression `other - self`.

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

Definition at line 3282 of file z3py.py.

3282  def __rsub__(self, other):
3283  """Create the Z3 expression `other - self`.
3284 
3285  >>> x = BitVec('x', 32)
3286  >>> 10 - x
3287  10 - x
3288  """
3289  a, b = _coerce_exprs(self, other)
3290  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3291 
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement subtraction.

◆ __rtruediv__()

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

Definition at line 3431 of file z3py.py.

3431  def __rtruediv__(self, other):
3432  """Create the Z3 expression (signed) division `other / self`."""
3433  return self.__rdiv__(other)
3434 

◆ __rxor__()

def __rxor__ (   self,
  other 
)
Create the Z3 expression bitwise-xor `other ^ self`.

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

Definition at line 3351 of file z3py.py.

3351  def __rxor__(self, other):
3352  """Create the Z3 expression bitwise-xor `other ^ self`.
3353 
3354  >>> x = BitVec('x', 32)
3355  >>> 10 ^ x
3356  10 ^ x
3357  """
3358  a, b = _coerce_exprs(self, other)
3359  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3360 
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 3269 of file z3py.py.

3269  def __sub__(self, other):
3270  """Create the Z3 expression `self - other`.
3271 
3272  >>> x = BitVec('x', 32)
3273  >>> y = BitVec('y', 32)
3274  >>> x - y
3275  x - y
3276  >>> (x - y).sort()
3277  BitVec(32)
3278  """
3279  a, b = _coerce_exprs(self, other)
3280  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3281 
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement subtraction.

◆ __truediv__()

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

Definition at line 3411 of file z3py.py.

3411  def __truediv__(self, other):
3412  """Create the Z3 expression (signed) division `self / other`."""
3413  return self.__div__(other)
3414 

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

3338  def __xor__(self, other):
3339  """Create the Z3 expression bitwise-xor `self ^ other`.
3340 
3341  >>> x = BitVec('x', 32)
3342  >>> y = BitVec('y', 32)
3343  >>> x ^ y
3344  x ^ y
3345  >>> (x ^ y).sort()
3346  BitVec(32)
3347  """
3348  a, b = _coerce_exprs(self, other)
3349  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3350 
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.

◆ size()

def size (   self)
Return the number of bits of the bit-vector expression `self`.

>>> x = BitVec('x', 32)
>>> (x + 1).size()
32
>>> Concat(x, x).size()
64

Definition at line 3212 of file z3py.py.

3212  def size(self):
3213  """Return the number of bits of the bit-vector expression `self`.
3214 
3215  >>> x = BitVec('x', 32)
3216  >>> (x + 1).size()
3217  32
3218  >>> Concat(x, x).size()
3219  64
3220  """
3221  return self.sort().size()
3222 

◆ sort()

def sort (   self)
Return the sort of the bit-vector expression `self`.

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

Definition at line 3201 of file z3py.py.

Referenced by BitVecRef.__add__(), BitVecRef.__and__(), BitVecRef.__div__(), BitVecRef.__mod__(), BitVecRef.__mul__(), BitVecRef.__or__(), BitVecRef.__sub__(), and BitVecRef.__xor__().

3201  def sort(self):
3202  """Return the sort of the bit-vector expression `self`.
3203 
3204  >>> x = BitVec('x', 32)
3205  >>> x.sort()
3206  BitVec(32)
3207  >>> x.sort() == BitVecSort(32)
3208  True
3209  """
3210  return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
3211 
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.