Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions
BitVecRef Class Reference
+ Inheritance diagram for BitVecRef:

Public Member Functions

def sort
 
def size
 
def __add__
 
def __radd__
 
def __mul__
 
def __rmul__
 
def __sub__
 
def __rsub__
 
def __or__
 
def __ror__
 
def __and__
 
def __rand__
 
def __xor__
 
def __rxor__
 
def __pos__
 
def __neg__
 
def __invert__
 
def __div__
 
def __truediv__
 
def __rdiv__
 
def __rtruediv__
 
def __mod__
 
def __rmod__
 
def __le__
 
def __lt__
 
def __gt__
 
def __ge__
 
def __rshift__
 
def __lshift__
 
def __rrshift__
 
def __rlshift__
 
- Public Member Functions inherited from ExprRef
def as_ast
 
def get_id
 
def sort
 
def sort_kind
 
def __eq__
 
def __hash__
 
def __ne__
 
def params
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
def hash
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Bit-vector expressions.

Definition at line 3215 of file z3py.py.

Member Function Documentation

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

3241  def __add__(self, other):
3242  """Create the Z3 expression `self + other`.
3243 
3244  >>> x = BitVec('x', 32)
3245  >>> y = BitVec('y', 32)
3246  >>> x + y
3247  x + y
3248  >>> (x + y).sort()
3249  BitVec(32)
3250  """
3251  a, b = _coerce_exprs(self, other)
3252  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __add__
Definition: z3py.py:3240
def ctx_ref
Definition: z3py.py:352
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
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 3332 of file z3py.py.

3333  def __and__(self, other):
3334  """Create the Z3 expression bitwise-and `self & other`.
3335 
3336  >>> x = BitVec('x', 32)
3337  >>> y = BitVec('y', 32)
3338  >>> x & y
3339  x & y
3340  >>> (x & y).sort()
3341  BitVec(32)
3342  """
3343  a, b = _coerce_exprs(self, other)
3344  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __and__
Definition: z3py.py:3332
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
def ctx_ref
Definition: z3py.py:352
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 3409 of file z3py.py.

3410  def __div__(self, other):
3411  """Create the Z3 expression (signed) division `self / other`.
3412 
3413  Use the function UDiv() for unsigned division.
3414 
3415  >>> x = BitVec('x', 32)
3416  >>> y = BitVec('y', 32)
3417  >>> x / y
3418  x/y
3419  >>> (x / y).sort()
3420  BitVec(32)
3421  >>> (x / y).sexpr()
3422  '(bvsdiv x y)'
3423  >>> UDiv(x, y).sexpr()
3424  '(bvudiv x y)'
3425  """
3426  a, b = _coerce_exprs(self, other)
3427  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __div__
Definition: z3py.py:3409
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
def ctx_ref
Definition: z3py.py:352
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 3539 of file z3py.py.

3540  def __ge__(self, other):
3541  """Create the Z3 expression (signed) `other >= self`.
3542 
3543  Use the function UGE() for unsigned greater than or equal to.
3544 
3545  >>> x, y = BitVecs('x y', 32)
3546  >>> x >= y
3547  x >= y
3548  >>> (x >= y).sexpr()
3549  '(bvsge x y)'
3550  >>> UGE(x, y).sexpr()
3551  '(bvuge x y)'
3552  """
3553  a, b = _coerce_exprs(self, other)
3554  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.
def ctx_ref
Definition: z3py.py:352
def __ge__
Definition: z3py.py:3539
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 3523 of file z3py.py.

3524  def __gt__(self, other):
3525  """Create the Z3 expression (signed) `other > self`.
3526 
3527  Use the function UGT() for unsigned greater than.
3528 
3529  >>> x, y = BitVecs('x y', 32)
3530  >>> x > y
3531  x > y
3532  >>> (x > y).sexpr()
3533  '(bvsgt x y)'
3534  >>> UGT(x, y).sexpr()
3535  '(bvugt x y)'
3536  """
3537  a, b = _coerce_exprs(self, other)
3538  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.
def __gt__
Definition: z3py.py:3523
def ctx_ref
Definition: z3py.py:352
def __invert__ (   self)
Create the Z3 expression bitwise-not `~self`.

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

Definition at line 3398 of file z3py.py.

3399  def __invert__(self):
3400  """Create the Z3 expression bitwise-not `~self`.
3401 
3402  >>> x = BitVec('x', 32)
3403  >>> ~x
3404  ~x
3405  >>> simplify(~(~x))
3406  x
3407  """
3408  return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)
def __invert__
Definition: z3py.py:3398
def as_ast
Definition: z3py.py:344
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
def ctx_ref
Definition: z3py.py:352
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 3491 of file z3py.py.

3492  def __le__(self, other):
3493  """Create the Z3 expression (signed) `other <= self`.
3494 
3495  Use the function ULE() for unsigned less than or equal to.
3496 
3497  >>> x, y = BitVecs('x y', 32)
3498  >>> x <= y
3499  x <= y
3500  >>> (x <= y).sexpr()
3501  '(bvsle x y)'
3502  >>> ULE(x, y).sexpr()
3503  '(bvule x y)'
3504  """
3505  a, b = _coerce_exprs(self, other)
3506  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.
def __le__
Definition: z3py.py:3491
def ctx_ref
Definition: z3py.py:352
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 3585 of file z3py.py.

3586  def __lshift__(self, other):
3587  """Create the Z3 expression left shift `self << other`
3588 
3589  >>> x, y = BitVecs('x y', 32)
3590  >>> x << y
3591  x << y
3592  >>> (x << y).sexpr()
3593  '(bvshl x y)'
3594  >>> simplify(BitVecVal(2, 3) << 1)
3595  4
3596  """
3597  a, b = _coerce_exprs(self, other)
3598  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.
def __lshift__
Definition: z3py.py:3585
def ctx_ref
Definition: z3py.py:352
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 3507 of file z3py.py.

3508  def __lt__(self, other):
3509  """Create the Z3 expression (signed) `other < self`.
3510 
3511  Use the function ULT() for unsigned less than.
3512 
3513  >>> x, y = BitVecs('x y', 32)
3514  >>> x < y
3515  x < y
3516  >>> (x < y).sexpr()
3517  '(bvslt x y)'
3518  >>> ULT(x, y).sexpr()
3519  '(bvult x y)'
3520  """
3521  a, b = _coerce_exprs(self, other)
3522  return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __lt__
Definition: z3py.py:3507
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
def ctx_ref
Definition: z3py.py:352
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 3452 of file z3py.py.

3453  def __mod__(self, other):
3454  """Create the Z3 expression (signed) mod `self % other`.
3455 
3456  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3457 
3458  >>> x = BitVec('x', 32)
3459  >>> y = BitVec('y', 32)
3460  >>> x % y
3461  x%y
3462  >>> (x % y).sort()
3463  BitVec(32)
3464  >>> (x % y).sexpr()
3465  '(bvsmod x y)'
3466  >>> URem(x, y).sexpr()
3467  '(bvurem x y)'
3468  >>> SRem(x, y).sexpr()
3469  '(bvsrem x y)'
3470  """
3471  a, b = _coerce_exprs(self, other)
3472  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).
def ctx_ref
Definition: z3py.py:352
def __mod__
Definition: z3py.py:3452
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 3263 of file z3py.py.

3264  def __mul__(self, other):
3265  """Create the Z3 expression `self * other`.
3266 
3267  >>> x = BitVec('x', 32)
3268  >>> y = BitVec('y', 32)
3269  >>> x * y
3270  x*y
3271  >>> (x * y).sort()
3272  BitVec(32)
3273  """
3274  a, b = _coerce_exprs(self, other)
3275  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __mul__
Definition: z3py.py:3263
def ctx_ref
Definition: z3py.py:352
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
def __neg__ (   self)
Return an expression representing `-self`.

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

Definition at line 3387 of file z3py.py.

3388  def __neg__(self):
3389  """Return an expression representing `-self`.
3390 
3391  >>> x = BitVec('x', 32)
3392  >>> -x
3393  -x
3394  >>> simplify(-(-x))
3395  x
3396  """
3397  return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
def __neg__
Definition: z3py.py:3387
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 3309 of file z3py.py.

3310  def __or__(self, other):
3311  """Create the Z3 expression bitwise-or `self | other`.
3312 
3313  >>> x = BitVec('x', 32)
3314  >>> y = BitVec('y', 32)
3315  >>> x | y
3316  x | y
3317  >>> (x | y).sort()
3318  BitVec(32)
3319  """
3320  a, b = _coerce_exprs(self, other)
3321  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.
def ctx_ref
Definition: z3py.py:352
def __or__
Definition: z3py.py:3309
def __pos__ (   self)
Return `self`.

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

Definition at line 3378 of file z3py.py.

3379  def __pos__(self):
3380  """Return `self`.
3381 
3382  >>> x = BitVec('x', 32)
3383  >>> +x
3384  x
3385  """
3386  return self
def __pos__
Definition: z3py.py:3378
def __radd__ (   self,
  other 
)
Create the Z3 expression `other + self`.

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

Definition at line 3253 of file z3py.py.

3254  def __radd__(self, other):
3255  """Create the Z3 expression `other + self`.
3256 
3257  >>> x = BitVec('x', 32)
3258  >>> 10 + x
3259  10 + x
3260  """
3261  a, b = _coerce_exprs(self, other)
3262  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __radd__
Definition: z3py.py:3253
def ctx_ref
Definition: z3py.py:352
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
def __rand__ (   self,
  other 
)
Create the Z3 expression bitwise-or `other & self`.

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

Definition at line 3345 of file z3py.py.

3346  def __rand__(self, other):
3347  """Create the Z3 expression bitwise-or `other & self`.
3348 
3349  >>> x = BitVec('x', 32)
3350  >>> 10 & x
3351  10 & x
3352  """
3353  a, b = _coerce_exprs(self, other)
3354  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rand__
Definition: z3py.py:3345
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
def ctx_ref
Definition: z3py.py:352
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 3432 of file z3py.py.

3433  def __rdiv__(self, other):
3434  """Create the Z3 expression (signed) division `other / self`.
3435 
3436  Use the function UDiv() for unsigned division.
3437 
3438  >>> x = BitVec('x', 32)
3439  >>> 10 / x
3440  10/x
3441  >>> (10 / x).sexpr()
3442  '(bvsdiv #x0000000a x)'
3443  >>> UDiv(10, x).sexpr()
3444  '(bvudiv #x0000000a x)'
3445  """
3446  a, b = _coerce_exprs(self, other)
3447  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.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.
def __rdiv__
Definition: z3py.py:3432
def ctx_ref
Definition: z3py.py:352
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 3613 of file z3py.py.

3614  def __rlshift__(self, other):
3615  """Create the Z3 expression left shift `other << self`.
3616 
3617  Use the function LShR() for the right logical shift
3618 
3619  >>> x = BitVec('x', 32)
3620  >>> 10 << x
3621  10 << x
3622  >>> (10 << x).sexpr()
3623  '(bvshl #x0000000a x)'
3624  """
3625  a, b = _coerce_exprs(self, other)
3626  return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
def __rlshift__
Definition: z3py.py:3613
def ctx_ref
Definition: z3py.py:352
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 3473 of file z3py.py.

3474  def __rmod__(self, other):
3475  """Create the Z3 expression (signed) mod `other % self`.
3476 
3477  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3478 
3479  >>> x = BitVec('x', 32)
3480  >>> 10 % x
3481  10%x
3482  >>> (10 % x).sexpr()
3483  '(bvsmod #x0000000a x)'
3484  >>> URem(10, x).sexpr()
3485  '(bvurem #x0000000a x)'
3486  >>> SRem(10, x).sexpr()
3487  '(bvsrem #x0000000a x)'
3488  """
3489  a, b = _coerce_exprs(self, other)
3490  return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rmod__
Definition: z3py.py:3473
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
def ctx_ref
Definition: z3py.py:352
def __rmul__ (   self,
  other 
)
Create the Z3 expression `other * self`.

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

Definition at line 3276 of file z3py.py.

3277  def __rmul__(self, other):
3278  """Create the Z3 expression `other * self`.
3279 
3280  >>> x = BitVec('x', 32)
3281  >>> 10 * x
3282  10*x
3283  """
3284  a, b = _coerce_exprs(self, other)
3285  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rmul__
Definition: z3py.py:3276
def ctx_ref
Definition: z3py.py:352
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
def __ror__ (   self,
  other 
)
Create the Z3 expression bitwise-or `other | self`.

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

Definition at line 3322 of file z3py.py.

3323  def __ror__(self, other):
3324  """Create the Z3 expression bitwise-or `other | self`.
3325 
3326  >>> x = BitVec('x', 32)
3327  >>> 10 | x
3328  10 | x
3329  """
3330  a, b = _coerce_exprs(self, other)
3331  return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __ror__
Definition: z3py.py:3322
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
def ctx_ref
Definition: z3py.py:352
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 3599 of file z3py.py.

3600  def __rrshift__(self, other):
3601  """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3602 
3603  Use the function LShR() for the right logical shift
3604 
3605  >>> x = BitVec('x', 32)
3606  >>> 10 >> x
3607  10 >> x
3608  >>> (10 >> x).sexpr()
3609  '(bvashr #x0000000a x)'
3610  """
3611  a, b = _coerce_exprs(self, other)
3612  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.
def ctx_ref
Definition: z3py.py:352
def __rrshift__
Definition: z3py.py:3599
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 3555 of file z3py.py.

3556  def __rshift__(self, other):
3557  """Create the Z3 expression (arithmetical) right shift `self >> other`
3558 
3559  Use the function LShR() for the right logical shift
3560 
3561  >>> x, y = BitVecs('x y', 32)
3562  >>> x >> y
3563  x >> y
3564  >>> (x >> y).sexpr()
3565  '(bvashr x y)'
3566  >>> LShR(x, y).sexpr()
3567  '(bvlshr x y)'
3568  >>> BitVecVal(4, 3)
3569  4
3570  >>> BitVecVal(4, 3).as_signed_long()
3571  -4
3572  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3573  -2
3574  >>> simplify(BitVecVal(4, 3) >> 1)
3575  6
3576  >>> simplify(LShR(BitVecVal(4, 3), 1))
3577  2
3578  >>> simplify(BitVecVal(2, 3) >> 1)
3579  1
3580  >>> simplify(LShR(BitVecVal(2, 3), 1))
3581  1
3582  """
3583  a, b = _coerce_exprs(self, other)
3584  return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
def __rshift__
Definition: z3py.py:3555
def ctx_ref
Definition: z3py.py:352
def __rsub__ (   self,
  other 
)
Create the Z3 expression `other - self`.

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

Definition at line 3299 of file z3py.py.

3300  def __rsub__(self, other):
3301  """Create the Z3 expression `other - self`.
3302 
3303  >>> x = BitVec('x', 32)
3304  >>> 10 - x
3305  10 - x
3306  """
3307  a, b = _coerce_exprs(self, other)
3308  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rsub__
Definition: z3py.py:3299
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
def ctx_ref
Definition: z3py.py:352
def __rtruediv__ (   self,
  other 
)
Create the Z3 expression (signed) division `other / self`.

Definition at line 3448 of file z3py.py.

3449  def __rtruediv__(self, other):
3450  """Create the Z3 expression (signed) division `other / self`."""
3451  return self.__rdiv__(other)
def __rtruediv__
Definition: z3py.py:3448
def __rdiv__
Definition: z3py.py:3432
def __rxor__ (   self,
  other 
)
Create the Z3 expression bitwise-xor `other ^ self`.

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

Definition at line 3368 of file z3py.py.

3369  def __rxor__(self, other):
3370  """Create the Z3 expression bitwise-xor `other ^ self`.
3371 
3372  >>> x = BitVec('x', 32)
3373  >>> 10 ^ x
3374  10 ^ x
3375  """
3376  a, b = _coerce_exprs(self, other)
3377  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rxor__
Definition: z3py.py:3368
def ctx_ref
Definition: z3py.py:352
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
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 3286 of file z3py.py.

3287  def __sub__(self, other):
3288  """Create the Z3 expression `self - other`.
3289 
3290  >>> x = BitVec('x', 32)
3291  >>> y = BitVec('y', 32)
3292  >>> x - y
3293  x - y
3294  >>> (x - y).sort()
3295  BitVec(32)
3296  """
3297  a, b = _coerce_exprs(self, other)
3298  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.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.
def ctx_ref
Definition: z3py.py:352
def __sub__
Definition: z3py.py:3286
def __truediv__ (   self,
  other 
)
Create the Z3 expression (signed) division `self / other`.

Definition at line 3428 of file z3py.py.

3429  def __truediv__(self, other):
3430  """Create the Z3 expression (signed) division `self / other`."""
3431  return self.__div__(other)
def __truediv__
Definition: z3py.py:3428
def __div__
Definition: z3py.py:3409
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 3355 of file z3py.py.

3356  def __xor__(self, other):
3357  """Create the Z3 expression bitwise-xor `self ^ other`.
3358 
3359  >>> x = BitVec('x', 32)
3360  >>> y = BitVec('y', 32)
3361  >>> x ^ y
3362  x ^ y
3363  >>> (x ^ y).sort()
3364  BitVec(32)
3365  """
3366  a, b = _coerce_exprs(self, other)
3367  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def ctx_ref
Definition: z3py.py:352
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
def __xor__
Definition: z3py.py:3355
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 3229 of file z3py.py.

Referenced by BitVecNumRef.as_signed_long().

3230  def size(self):
3231  """Return the number of bits of the bit-vector expression `self`.
3232 
3233  >>> x = BitVec('x', 32)
3234  >>> (x + 1).size()
3235  32
3236  >>> Concat(x, x).size()
3237  64
3238  """
3239  return self.sort().size()
def sort
Definition: z3py.py:879
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 3218 of file z3py.py.

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

3219  def sort(self):
3220  """Return the sort of the bit-vector expression `self`.
3221 
3222  >>> x = BitVec('x', 32)
3223  >>> x.sort()
3224  BitVec(32)
3225  >>> x.sort() == BitVecSort(32)
3226  True
3227  """
3228  return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
Bit-Vectors.
Definition: z3py.py:3173
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.