Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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 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 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 2831 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 2856 of file z3py.py.

2857  def __add__(self, other):
2858  """Create the Z3 expression `self + other`.
2859 
2860  >>> x = BitVec('x', 32)
2861  >>> y = BitVec('y', 32)
2862  >>> x + y
2863  x + y
2864  >>> (x + y).sort()
2865  BitVec(32)
2866  """
2867  a, b = _coerce_exprs(self, other)
2868  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 2948 of file z3py.py.

2949  def __and__(self, other):
2950  """Create the Z3 expression bitwise-and `self & other`.
2951 
2952  >>> x = BitVec('x', 32)
2953  >>> y = BitVec('y', 32)
2954  >>> x & y
2955  x & y
2956  >>> (x & y).sort()
2957  BitVec(32)
2958  """
2959  a, b = _coerce_exprs(self, other)
2960  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 3025 of file z3py.py.

3026  def __div__(self, other):
3027  """Create the Z3 expression (signed) division `self / other`.
3028 
3029  Use the function UDiv() for unsigned division.
3030 
3031  >>> x = BitVec('x', 32)
3032  >>> y = BitVec('y', 32)
3033  >>> x / y
3034  x/y
3035  >>> (x / y).sort()
3036  BitVec(32)
3037  >>> (x / y).sexpr()
3038  '(bvsdiv x y)'
3039  >>> UDiv(x, y).sexpr()
3040  '(bvudiv x y)'
3041  """
3042  a, b = _coerce_exprs(self, other)
3043  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 3155 of file z3py.py.

3156  def __ge__(self, other):
3157  """Create the Z3 expression (signed) `other >= self`.
3158 
3159  Use the function UGE() for unsigned greater than or equal to.
3160 
3161  >>> x, y = BitVecs('x y', 32)
3162  >>> x >= y
3163  x >= y
3164  >>> (x >= y).sexpr()
3165  '(bvsge x y)'
3166  >>> UGE(x, y).sexpr()
3167  '(bvuge x y)'
3168  """
3169  a, b = _coerce_exprs(self, other)
3170  return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 3139 of file z3py.py.

3140  def __gt__(self, other):
3141  """Create the Z3 expression (signed) `other > self`.
3142 
3143  Use the function UGT() for unsigned greater than.
3144 
3145  >>> x, y = BitVecs('x y', 32)
3146  >>> x > y
3147  x > y
3148  >>> (x > y).sexpr()
3149  '(bvsgt x y)'
3150  >>> UGT(x, y).sexpr()
3151  '(bvugt x y)'
3152  """
3153  a, b = _coerce_exprs(self, other)
3154  return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __invert__ (   self)
Create the Z3 expression bitwise-not `~self`.

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

Definition at line 3014 of file z3py.py.

3015  def __invert__(self):
3016  """Create the Z3 expression bitwise-not `~self`.
3017 
3018  >>> x = BitVec('x', 32)
3019  >>> ~x
3020  ~x
3021  >>> simplify(~(~x))
3022  x
3023  """
3024  return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)
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 3107 of file z3py.py.

3108  def __le__(self, other):
3109  """Create the Z3 expression (signed) `other <= self`.
3110 
3111  Use the function ULE() for unsigned less than or equal to.
3112 
3113  >>> x, y = BitVecs('x y', 32)
3114  >>> x <= y
3115  x <= y
3116  >>> (x <= y).sexpr()
3117  '(bvsle x y)'
3118  >>> ULE(x, y).sexpr()
3119  '(bvule x y)'
3120  """
3121  a, b = _coerce_exprs(self, other)
3122  return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 3201 of file z3py.py.

3202  def __lshift__(self, other):
3203  """Create the Z3 expression left shift `self << other`
3204 
3205  >>> x, y = BitVecs('x y', 32)
3206  >>> x << y
3207  x << y
3208  >>> (x << y).sexpr()
3209  '(bvshl x y)'
3210  >>> simplify(BitVecVal(2, 3) << 1)
3211  4
3212  """
3213  a, b = _coerce_exprs(self, other)
3214  return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 3123 of file z3py.py.

3124  def __lt__(self, other):
3125  """Create the Z3 expression (signed) `other < self`.
3126 
3127  Use the function ULT() for unsigned less than.
3128 
3129  >>> x, y = BitVecs('x y', 32)
3130  >>> x < y
3131  x < y
3132  >>> (x < y).sexpr()
3133  '(bvslt x y)'
3134  >>> ULT(x, y).sexpr()
3135  '(bvult x y)'
3136  """
3137  a, b = _coerce_exprs(self, other)
3138  return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 3068 of file z3py.py.

3069  def __mod__(self, other):
3070  """Create the Z3 expression (signed) mod `self % other`.
3071 
3072  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3073 
3074  >>> x = BitVec('x', 32)
3075  >>> y = BitVec('y', 32)
3076  >>> x % y
3077  x%y
3078  >>> (x % y).sort()
3079  BitVec(32)
3080  >>> (x % y).sexpr()
3081  '(bvsmod x y)'
3082  >>> URem(x, y).sexpr()
3083  '(bvurem x y)'
3084  >>> SRem(x, y).sexpr()
3085  '(bvsrem x y)'
3086  """
3087  a, b = _coerce_exprs(self, other)
3088  return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 2879 of file z3py.py.

2880  def __mul__(self, other):
2881  """Create the Z3 expression `self * other`.
2882 
2883  >>> x = BitVec('x', 32)
2884  >>> y = BitVec('y', 32)
2885  >>> x * y
2886  x*y
2887  >>> (x * y).sort()
2888  BitVec(32)
2889  """
2890  a, b = _coerce_exprs(self, other)
2891  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __neg__ (   self)
Return an expression representing `-self`.

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

Definition at line 3003 of file z3py.py.

3004  def __neg__(self):
3005  """Return an expression representing `-self`.
3006 
3007  >>> x = BitVec('x', 32)
3008  >>> -x
3009  -x
3010  >>> simplify(-(-x))
3011  x
3012  """
3013  return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)
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 2925 of file z3py.py.

2926  def __or__(self, other):
2927  """Create the Z3 expression bitwise-or `self | other`.
2928 
2929  >>> x = BitVec('x', 32)
2930  >>> y = BitVec('y', 32)
2931  >>> x | y
2932  x | y
2933  >>> (x | y).sort()
2934  BitVec(32)
2935  """
2936  a, b = _coerce_exprs(self, other)
2937  return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __pos__ (   self)
Return `self`.

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

Definition at line 2994 of file z3py.py.

2995  def __pos__(self):
2996  """Return `self`.
2997 
2998  >>> x = BitVec('x', 32)
2999  >>> +x
3000  x
3001  """
3002  return self
def __radd__ (   self,
  other 
)
Create the Z3 expression `other + self`.

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

Definition at line 2869 of file z3py.py.

2870  def __radd__(self, other):
2871  """Create the Z3 expression `other + self`.
2872 
2873  >>> x = BitVec('x', 32)
2874  >>> 10 + x
2875  10 + x
2876  """
2877  a, b = _coerce_exprs(self, other)
2878  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rand__ (   self,
  other 
)
Create the Z3 expression bitwise-or `other & self`.

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

Definition at line 2961 of file z3py.py.

2962  def __rand__(self, other):
2963  """Create the Z3 expression bitwise-or `other & self`.
2964 
2965  >>> x = BitVec('x', 32)
2966  >>> 10 & x
2967  10 & x
2968  """
2969  a, b = _coerce_exprs(self, other)
2970  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
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 3048 of file z3py.py.

3049  def __rdiv__(self, other):
3050  """Create the Z3 expression (signed) division `other / self`.
3051 
3052  Use the function UDiv() for unsigned division.
3053 
3054  >>> x = BitVec('x', 32)
3055  >>> 10 / x
3056  10/x
3057  >>> (10 / x).sexpr()
3058  '(bvsdiv #x0000000a x)'
3059  >>> UDiv(10, x).sexpr()
3060  '(bvudiv #x0000000a x)'
3061  """
3062  a, b = _coerce_exprs(self, other)
3063  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
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 3229 of file z3py.py.

3230  def __rlshift__(self, other):
3231  """Create the Z3 expression left shift `other << self`.
3232 
3233  Use the function LShR() for the right logical shift
3234 
3235  >>> x = BitVec('x', 32)
3236  >>> 10 << x
3237  10 << x
3238  >>> (10 << x).sexpr()
3239  '(bvshl #x0000000a x)'
3240  """
3241  a, b = _coerce_exprs(self, other)
3242  return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
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 3089 of file z3py.py.

3090  def __rmod__(self, other):
3091  """Create the Z3 expression (signed) mod `other % self`.
3092 
3093  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3094 
3095  >>> x = BitVec('x', 32)
3096  >>> 10 % x
3097  10%x
3098  >>> (10 % x).sexpr()
3099  '(bvsmod #x0000000a x)'
3100  >>> URem(10, x).sexpr()
3101  '(bvurem #x0000000a x)'
3102  >>> SRem(10, x).sexpr()
3103  '(bvsrem #x0000000a x)'
3104  """
3105  a, b = _coerce_exprs(self, other)
3106  return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rmul__ (   self,
  other 
)
Create the Z3 expression `other * self`.

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

Definition at line 2892 of file z3py.py.

2893  def __rmul__(self, other):
2894  """Create the Z3 expression `other * self`.
2895 
2896  >>> x = BitVec('x', 32)
2897  >>> 10 * x
2898  10*x
2899  """
2900  a, b = _coerce_exprs(self, other)
2901  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __ror__ (   self,
  other 
)
Create the Z3 expression bitwise-or `other | self`.

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

Definition at line 2938 of file z3py.py.

2939  def __ror__(self, other):
2940  """Create the Z3 expression bitwise-or `other | self`.
2941 
2942  >>> x = BitVec('x', 32)
2943  >>> 10 | x
2944  10 | x
2945  """
2946  a, b = _coerce_exprs(self, other)
2947  return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
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 3215 of file z3py.py.

3216  def __rrshift__(self, other):
3217  """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3218 
3219  Use the function LShR() for the right logical shift
3220 
3221  >>> x = BitVec('x', 32)
3222  >>> 10 >> x
3223  10 >> x
3224  >>> (10 >> x).sexpr()
3225  '(bvashr #x0000000a x)'
3226  """
3227  a, b = _coerce_exprs(self, other)
3228  return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
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()
-4L
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2L
>>> 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 3171 of file z3py.py.

3172  def __rshift__(self, other):
3173  """Create the Z3 expression (arithmetical) right shift `self >> other`
3174 
3175  Use the function LShR() for the right logical shift
3176 
3177  >>> x, y = BitVecs('x y', 32)
3178  >>> x >> y
3179  x >> y
3180  >>> (x >> y).sexpr()
3181  '(bvashr x y)'
3182  >>> LShR(x, y).sexpr()
3183  '(bvlshr x y)'
3184  >>> BitVecVal(4, 3)
3185  4
3186  >>> BitVecVal(4, 3).as_signed_long()
3187  -4L
3188  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3189  -2L
3190  >>> simplify(BitVecVal(4, 3) >> 1)
3191  6
3192  >>> simplify(LShR(BitVecVal(4, 3), 1))
3193  2
3194  >>> simplify(BitVecVal(2, 3) >> 1)
3195  1
3196  >>> simplify(LShR(BitVecVal(2, 3), 1))
3197  1
3198  """
3199  a, b = _coerce_exprs(self, other)
3200  return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __rsub__ (   self,
  other 
)
Create the Z3 expression `other - self`.

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

Definition at line 2915 of file z3py.py.

2916  def __rsub__(self, other):
2917  """Create the Z3 expression `other - self`.
2918 
2919  >>> x = BitVec('x', 32)
2920  >>> 10 - x
2921  10 - x
2922  """
2923  a, b = _coerce_exprs(self, other)
2924  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rtruediv__ (   self,
  other 
)
Create the Z3 expression (signed) division `other / self`.

Definition at line 3064 of file z3py.py.

3065  def __rtruediv__(self, other):
3066  """Create the Z3 expression (signed) division `other / self`."""
3067  self.__rdiv__(other)
def __rxor__ (   self,
  other 
)
Create the Z3 expression bitwise-xor `other ^ self`.

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

Definition at line 2984 of file z3py.py.

2985  def __rxor__(self, other):
2986  """Create the Z3 expression bitwise-xor `other ^ self`.
2987 
2988  >>> x = BitVec('x', 32)
2989  >>> 10 ^ x
2990  10 ^ x
2991  """
2992  a, b = _coerce_exprs(self, other)
2993  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
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 2902 of file z3py.py.

2903  def __sub__(self, other):
2904  """Create the Z3 expression `self - other`.
2905 
2906  >>> x = BitVec('x', 32)
2907  >>> y = BitVec('y', 32)
2908  >>> x - y
2909  x - y
2910  >>> (x - y).sort()
2911  BitVec(32)
2912  """
2913  a, b = _coerce_exprs(self, other)
2914  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __truediv__ (   self,
  other 
)
Create the Z3 expression (signed) division `self / other`.

Definition at line 3044 of file z3py.py.

3045  def __truediv__(self, other):
3046  """Create the Z3 expression (signed) division `self / other`."""
3047  self.__div__(other)
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 2971 of file z3py.py.

2972  def __xor__(self, other):
2973  """Create the Z3 expression bitwise-xor `self ^ other`.
2974 
2975  >>> x = BitVec('x', 32)
2976  >>> y = BitVec('y', 32)
2977  >>> x ^ y
2978  x ^ y
2979  >>> (x ^ y).sort()
2980  BitVec(32)
2981  """
2982  a, b = _coerce_exprs(self, other)
2983  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
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 2845 of file z3py.py.

2846  def size(self):
2847  """Return the number of bits of the bit-vector expression `self`.
2848 
2849  >>> x = BitVec('x', 32)
2850  >>> (x + 1).size()
2851  32
2852  >>> Concat(x, x).size()
2853  64
2854  """
2855  return self.sort().size()
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 2834 of file z3py.py.

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

2835  def sort(self):
2836  """Return the sort of the bit-vector expression `self`.
2837 
2838  >>> x = BitVec('x', 32)
2839  >>> x.sort()
2840  BitVec(32)
2841  >>> x.sort() == BitVecSort(32)
2842  True
2843  """
2844  return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)