Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties 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 __ne__
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __str__
 
def __repr__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
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 2939 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 2964 of file z3py.py.

2965  def __add__(self, other):
2966  """Create the Z3 expression `self + other`.
2967 
2968  >>> x = BitVec('x', 32)
2969  >>> y = BitVec('y', 32)
2970  >>> x + y
2971  x + y
2972  >>> (x + y).sort()
2973  BitVec(32)
2974  """
2975  a, b = _coerce_exprs(self, other)
2976  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvadd(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement addition.
def __add__
Definition: z3py.py:2964
def ctx_ref
Definition: z3py.py:305
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 3056 of file z3py.py.

3057  def __and__(self, other):
3058  """Create the Z3 expression bitwise-and `self & other`.
3059 
3060  >>> x = BitVec('x', 32)
3061  >>> y = BitVec('y', 32)
3062  >>> x & y
3063  x & y
3064  >>> (x & y).sort()
3065  BitVec(32)
3066  """
3067  a, b = _coerce_exprs(self, other)
3068  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __and__
Definition: z3py.py:3056
Z3_ast Z3_API Z3_mk_bvand(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise and.
def ctx_ref
Definition: z3py.py:305
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 3133 of file z3py.py.

3134  def __div__(self, other):
3135  """Create the Z3 expression (signed) division `self / other`.
3136 
3137  Use the function UDiv() for unsigned division.
3138 
3139  >>> x = BitVec('x', 32)
3140  >>> y = BitVec('y', 32)
3141  >>> x / y
3142  x/y
3143  >>> (x / y).sort()
3144  BitVec(32)
3145  >>> (x / y).sexpr()
3146  '(bvsdiv x y)'
3147  >>> UDiv(x, y).sexpr()
3148  '(bvudiv x y)'
3149  """
3150  a, b = _coerce_exprs(self, other)
3151  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __div__
Definition: z3py.py:3133
Z3_ast Z3_API Z3_mk_bvsdiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed division.
def ctx_ref
Definition: z3py.py:305
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 3263 of file z3py.py.

3264  def __ge__(self, other):
3265  """Create the Z3 expression (signed) `other >= self`.
3266 
3267  Use the function UGE() for unsigned greater than or equal to.
3268 
3269  >>> x, y = BitVecs('x y', 32)
3270  >>> x >= y
3271  x >= y
3272  >>> (x >= y).sexpr()
3273  '(bvsge x y)'
3274  >>> UGE(x, y).sexpr()
3275  '(bvuge x y)'
3276  """
3277  a, b = _coerce_exprs(self, other)
3278  return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvsge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than or equal to.
def ctx_ref
Definition: z3py.py:305
def __ge__
Definition: z3py.py:3263
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 3247 of file z3py.py.

3248  def __gt__(self, other):
3249  """Create the Z3 expression (signed) `other > self`.
3250 
3251  Use the function UGT() for unsigned greater than.
3252 
3253  >>> x, y = BitVecs('x y', 32)
3254  >>> x > y
3255  x > y
3256  >>> (x > y).sexpr()
3257  '(bvsgt x y)'
3258  >>> UGT(x, y).sexpr()
3259  '(bvugt x y)'
3260  """
3261  a, b = _coerce_exprs(self, other)
3262  return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __gt__
Definition: z3py.py:3247
Z3_ast Z3_API Z3_mk_bvsgt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than.
def ctx_ref
Definition: z3py.py:305
def __invert__ (   self)
Create the Z3 expression bitwise-not `~self`.

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

Definition at line 3122 of file z3py.py.

3123  def __invert__(self):
3124  """Create the Z3 expression bitwise-not `~self`.
3125 
3126  >>> x = BitVec('x', 32)
3127  >>> ~x
3128  ~x
3129  >>> simplify(~(~x))
3130  x
3131  """
3132  return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)
def __invert__
Definition: z3py.py:3122
Z3_ast Z3_API Z3_mk_bvnot(__in Z3_context c, __in Z3_ast t1)
Bitwise negation.
def as_ast
Definition: z3py.py:296
def ctx_ref
Definition: z3py.py:305
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 3215 of file z3py.py.

3216  def __le__(self, other):
3217  """Create the Z3 expression (signed) `other <= self`.
3218 
3219  Use the function ULE() for unsigned less than or equal to.
3220 
3221  >>> x, y = BitVecs('x y', 32)
3222  >>> x <= y
3223  x <= y
3224  >>> (x <= y).sexpr()
3225  '(bvsle x y)'
3226  >>> ULE(x, y).sexpr()
3227  '(bvule x y)'
3228  """
3229  a, b = _coerce_exprs(self, other)
3230  return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvsle(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than or equal to.
def __le__
Definition: z3py.py:3215
def ctx_ref
Definition: z3py.py:305
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 3309 of file z3py.py.

3310  def __lshift__(self, other):
3311  """Create the Z3 expression left shift `self << other`
3312 
3313  >>> x, y = BitVecs('x y', 32)
3314  >>> x << y
3315  x << y
3316  >>> (x << y).sexpr()
3317  '(bvshl x y)'
3318  >>> simplify(BitVecVal(2, 3) << 1)
3319  4
3320  """
3321  a, b = _coerce_exprs(self, other)
3322  return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvshl(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Shift left.
def __lshift__
Definition: z3py.py:3309
def ctx_ref
Definition: z3py.py:305
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 3231 of file z3py.py.

3232  def __lt__(self, other):
3233  """Create the Z3 expression (signed) `other < self`.
3234 
3235  Use the function ULT() for unsigned less than.
3236 
3237  >>> x, y = BitVecs('x y', 32)
3238  >>> x < y
3239  x < y
3240  >>> (x < y).sexpr()
3241  '(bvslt x y)'
3242  >>> ULT(x, y).sexpr()
3243  '(bvult x y)'
3244  """
3245  a, b = _coerce_exprs(self, other)
3246  return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __lt__
Definition: z3py.py:3231
Z3_ast Z3_API Z3_mk_bvslt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than.
def ctx_ref
Definition: z3py.py:305
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 3176 of file z3py.py.

3177  def __mod__(self, other):
3178  """Create the Z3 expression (signed) mod `self % other`.
3179 
3180  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3181 
3182  >>> x = BitVec('x', 32)
3183  >>> y = BitVec('y', 32)
3184  >>> x % y
3185  x%y
3186  >>> (x % y).sort()
3187  BitVec(32)
3188  >>> (x % y).sexpr()
3189  '(bvsmod x y)'
3190  >>> URem(x, y).sexpr()
3191  '(bvurem x y)'
3192  >>> SRem(x, y).sexpr()
3193  '(bvsrem x y)'
3194  """
3195  a, b = _coerce_exprs(self, other)
3196  return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvsmod(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
def ctx_ref
Definition: z3py.py:305
def __mod__
Definition: z3py.py:3176
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 2987 of file z3py.py.

2988  def __mul__(self, other):
2989  """Create the Z3 expression `self * other`.
2990 
2991  >>> x = BitVec('x', 32)
2992  >>> y = BitVec('y', 32)
2993  >>> x * y
2994  x*y
2995  >>> (x * y).sort()
2996  BitVec(32)
2997  """
2998  a, b = _coerce_exprs(self, other)
2999  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __mul__
Definition: z3py.py:2987
Z3_ast Z3_API Z3_mk_bvmul(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement multiplication.
def ctx_ref
Definition: z3py.py:305
def __neg__ (   self)
Return an expression representing `-self`.

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

Definition at line 3111 of file z3py.py.

3112  def __neg__(self):
3113  """Return an expression representing `-self`.
3114 
3115  >>> x = BitVec('x', 32)
3116  >>> -x
3117  -x
3118  >>> simplify(-(-x))
3119  x
3120  """
3121  return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvneg(__in Z3_context c, __in Z3_ast t1)
Standard two's complement unary minus.
def as_ast
Definition: z3py.py:296
def ctx_ref
Definition: z3py.py:305
def __neg__
Definition: z3py.py:3111
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 3033 of file z3py.py.

3034  def __or__(self, other):
3035  """Create the Z3 expression bitwise-or `self | other`.
3036 
3037  >>> x = BitVec('x', 32)
3038  >>> y = BitVec('y', 32)
3039  >>> x | y
3040  x | y
3041  >>> (x | y).sort()
3042  BitVec(32)
3043  """
3044  a, b = _coerce_exprs(self, other)
3045  return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise or.
def ctx_ref
Definition: z3py.py:305
def __or__
Definition: z3py.py:3033
def __pos__ (   self)
Return `self`.

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

Definition at line 3102 of file z3py.py.

3103  def __pos__(self):
3104  """Return `self`.
3105 
3106  >>> x = BitVec('x', 32)
3107  >>> +x
3108  x
3109  """
3110  return self
def __pos__
Definition: z3py.py:3102
def __radd__ (   self,
  other 
)
Create the Z3 expression `other + self`.

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

Definition at line 2977 of file z3py.py.

2978  def __radd__(self, other):
2979  """Create the Z3 expression `other + self`.
2980 
2981  >>> x = BitVec('x', 32)
2982  >>> 10 + x
2983  10 + x
2984  """
2985  a, b = _coerce_exprs(self, other)
2986  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvadd(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement addition.
def __radd__
Definition: z3py.py:2977
def ctx_ref
Definition: z3py.py:305
def __rand__ (   self,
  other 
)
Create the Z3 expression bitwise-or `other & self`.

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

Definition at line 3069 of file z3py.py.

3070  def __rand__(self, other):
3071  """Create the Z3 expression bitwise-or `other & self`.
3072 
3073  >>> x = BitVec('x', 32)
3074  >>> 10 & x
3075  10 & x
3076  """
3077  a, b = _coerce_exprs(self, other)
3078  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvand(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise and.
def __rand__
Definition: z3py.py:3069
def ctx_ref
Definition: z3py.py:305
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 3156 of file z3py.py.

3157  def __rdiv__(self, other):
3158  """Create the Z3 expression (signed) division `other / self`.
3159 
3160  Use the function UDiv() for unsigned division.
3161 
3162  >>> x = BitVec('x', 32)
3163  >>> 10 / x
3164  10/x
3165  >>> (10 / x).sexpr()
3166  '(bvsdiv #x0000000a x)'
3167  >>> UDiv(10, x).sexpr()
3168  '(bvudiv #x0000000a x)'
3169  """
3170  a, b = _coerce_exprs(self, other)
3171  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvsdiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed division.
def __rdiv__
Definition: z3py.py:3156
def ctx_ref
Definition: z3py.py:305
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 3337 of file z3py.py.

3338  def __rlshift__(self, other):
3339  """Create the Z3 expression left shift `other << self`.
3340 
3341  Use the function LShR() for the right logical shift
3342 
3343  >>> x = BitVec('x', 32)
3344  >>> 10 << x
3345  10 << x
3346  >>> (10 << x).sexpr()
3347  '(bvshl #x0000000a x)'
3348  """
3349  a, b = _coerce_exprs(self, other)
3350  return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvshl(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Shift left.
def __rlshift__
Definition: z3py.py:3337
def ctx_ref
Definition: z3py.py:305
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 3197 of file z3py.py.

3198  def __rmod__(self, other):
3199  """Create the Z3 expression (signed) mod `other % self`.
3200 
3201  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3202 
3203  >>> x = BitVec('x', 32)
3204  >>> 10 % x
3205  10%x
3206  >>> (10 % x).sexpr()
3207  '(bvsmod #x0000000a x)'
3208  >>> URem(10, x).sexpr()
3209  '(bvurem #x0000000a x)'
3210  >>> SRem(10, x).sexpr()
3211  '(bvsrem #x0000000a x)'
3212  """
3213  a, b = _coerce_exprs(self, other)
3214  return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvsmod(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
def __rmod__
Definition: z3py.py:3197
def ctx_ref
Definition: z3py.py:305
def __rmul__ (   self,
  other 
)
Create the Z3 expression `other * self`.

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

Definition at line 3000 of file z3py.py.

3001  def __rmul__(self, other):
3002  """Create the Z3 expression `other * self`.
3003 
3004  >>> x = BitVec('x', 32)
3005  >>> 10 * x
3006  10*x
3007  """
3008  a, b = _coerce_exprs(self, other)
3009  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rmul__
Definition: z3py.py:3000
Z3_ast Z3_API Z3_mk_bvmul(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement multiplication.
def ctx_ref
Definition: z3py.py:305
def __ror__ (   self,
  other 
)
Create the Z3 expression bitwise-or `other | self`.

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

Definition at line 3046 of file z3py.py.

3047  def __ror__(self, other):
3048  """Create the Z3 expression bitwise-or `other | self`.
3049 
3050  >>> x = BitVec('x', 32)
3051  >>> 10 | x
3052  10 | x
3053  """
3054  a, b = _coerce_exprs(self, other)
3055  return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __ror__
Definition: z3py.py:3046
Z3_ast Z3_API Z3_mk_bvor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise or.
def ctx_ref
Definition: z3py.py:305
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 3323 of file z3py.py.

3324  def __rrshift__(self, other):
3325  """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3326 
3327  Use the function LShR() for the right logical shift
3328 
3329  >>> x = BitVec('x', 32)
3330  >>> 10 >> x
3331  10 >> x
3332  >>> (10 >> x).sexpr()
3333  '(bvashr #x0000000a x)'
3334  """
3335  a, b = _coerce_exprs(self, other)
3336  return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvashr(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Arithmetic shift right.
def ctx_ref
Definition: z3py.py:305
def __rrshift__
Definition: z3py.py:3323
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 3279 of file z3py.py.

3280  def __rshift__(self, other):
3281  """Create the Z3 expression (arithmetical) right shift `self >> other`
3282 
3283  Use the function LShR() for the right logical shift
3284 
3285  >>> x, y = BitVecs('x y', 32)
3286  >>> x >> y
3287  x >> y
3288  >>> (x >> y).sexpr()
3289  '(bvashr x y)'
3290  >>> LShR(x, y).sexpr()
3291  '(bvlshr x y)'
3292  >>> BitVecVal(4, 3)
3293  4
3294  >>> BitVecVal(4, 3).as_signed_long()
3295  -4
3296  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3297  -2
3298  >>> simplify(BitVecVal(4, 3) >> 1)
3299  6
3300  >>> simplify(LShR(BitVecVal(4, 3), 1))
3301  2
3302  >>> simplify(BitVecVal(2, 3) >> 1)
3303  1
3304  >>> simplify(LShR(BitVecVal(2, 3), 1))
3305  1
3306  """
3307  a, b = _coerce_exprs(self, other)
3308  return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __rshift__
Definition: z3py.py:3279
Z3_ast Z3_API Z3_mk_bvashr(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Arithmetic shift right.
def ctx_ref
Definition: z3py.py:305
def __rsub__ (   self,
  other 
)
Create the Z3 expression `other - self`.

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

Definition at line 3023 of file z3py.py.

3024  def __rsub__(self, other):
3025  """Create the Z3 expression `other - self`.
3026 
3027  >>> x = BitVec('x', 32)
3028  >>> 10 - x
3029  10 - x
3030  """
3031  a, b = _coerce_exprs(self, other)
3032  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rsub__
Definition: z3py.py:3023
Z3_ast Z3_API Z3_mk_bvsub(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement subtraction.
def ctx_ref
Definition: z3py.py:305
def __rtruediv__ (   self,
  other 
)
Create the Z3 expression (signed) division `other / self`.

Definition at line 3172 of file z3py.py.

3173  def __rtruediv__(self, other):
3174  """Create the Z3 expression (signed) division `other / self`."""
3175  return self.__rdiv__(other)
def __rtruediv__
Definition: z3py.py:3172
def __rdiv__
Definition: z3py.py:3156
def __rxor__ (   self,
  other 
)
Create the Z3 expression bitwise-xor `other ^ self`.

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

Definition at line 3092 of file z3py.py.

3093  def __rxor__(self, other):
3094  """Create the Z3 expression bitwise-xor `other ^ self`.
3095 
3096  >>> x = BitVec('x', 32)
3097  >>> 10 ^ x
3098  10 ^ x
3099  """
3100  a, b = _coerce_exprs(self, other)
3101  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rxor__
Definition: z3py.py:3092
Z3_ast Z3_API Z3_mk_bvxor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise exclusive-or.
def ctx_ref
Definition: z3py.py:305
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 3010 of file z3py.py.

3011  def __sub__(self, other):
3012  """Create the Z3 expression `self - other`.
3013 
3014  >>> x = BitVec('x', 32)
3015  >>> y = BitVec('y', 32)
3016  >>> x - y
3017  x - y
3018  >>> (x - y).sort()
3019  BitVec(32)
3020  """
3021  a, b = _coerce_exprs(self, other)
3022  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvsub(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement subtraction.
def ctx_ref
Definition: z3py.py:305
def __sub__
Definition: z3py.py:3010
def __truediv__ (   self,
  other 
)
Create the Z3 expression (signed) division `self / other`.

Definition at line 3152 of file z3py.py.

3153  def __truediv__(self, other):
3154  """Create the Z3 expression (signed) division `self / other`."""
3155  return self.__div__(other)
def __truediv__
Definition: z3py.py:3152
def __div__
Definition: z3py.py:3133
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 3079 of file z3py.py.

3080  def __xor__(self, other):
3081  """Create the Z3 expression bitwise-xor `self ^ other`.
3082 
3083  >>> x = BitVec('x', 32)
3084  >>> y = BitVec('y', 32)
3085  >>> x ^ y
3086  x ^ y
3087  >>> (x ^ y).sort()
3088  BitVec(32)
3089  """
3090  a, b = _coerce_exprs(self, other)
3091  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_bvxor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise exclusive-or.
def ctx_ref
Definition: z3py.py:305
def __xor__
Definition: z3py.py:3079
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 2953 of file z3py.py.

Referenced by BitVecNumRef.as_signed_long().

2954  def size(self):
2955  """Return the number of bits of the bit-vector expression `self`.
2956 
2957  >>> x = BitVec('x', 32)
2958  >>> (x + 1).size()
2959  32
2960  >>> Concat(x, x).size()
2961  64
2962  """
2963  return self.sort().size()
def sort
Definition: z3py.py:748
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 2942 of file z3py.py.

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

2943  def sort(self):
2944  """Return the sort of the bit-vector expression `self`.
2945 
2946  >>> x = BitVec('x', 32)
2947  >>> x.sort()
2948  BitVec(32)
2949  >>> x.sort() == BitVecSort(32)
2950  True
2951  """
2952  return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
Bit-Vectors.
Definition: z3py.py:2897
Z3_sort Z3_API Z3_get_sort(__in Z3_context c, __in Z3_ast a)
Return the sort of an AST node.
def as_ast
Definition: z3py.py:296
def ctx_ref
Definition: z3py.py:305