Detailed Description
Definition at line 3351 of file z3py.py.
Member Function Documentation
Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
>>> v = BitVecVal(0xbadc0de, 32)
>>> v
195936478
>>> print("0x%.8x" % v.as_long())
0x0badc0de
Definition at line 3354 of file z3py.py.
03354
03355 def as_long(self):
03356 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
03357
03358 >>> v = BitVecVal(0xbadc0de, 32)
03359 >>> v
03360 195936478
03361 >>> print("0x%.8x" % v.as_long())
03362 0x0badc0de
03363 """
03364 return int(self.as_string())
Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign.
>>> BitVecVal(4, 3).as_signed_long()
-4
>>> BitVecVal(7, 3).as_signed_long()
-1
>>> BitVecVal(3, 3).as_signed_long()
3
>>> BitVecVal(2**32 - 1, 32).as_signed_long()
-1
>>> BitVecVal(2**64 - 1, 64).as_signed_long()
-1
Definition at line 3365 of file z3py.py.
03365
03366 def as_signed_long(self):
03367 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign.
03368
03369 >>> BitVecVal(4, 3).as_signed_long()
03370 -4
03371 >>> BitVecVal(7, 3).as_signed_long()
03372 -1
03373 >>> BitVecVal(3, 3).as_signed_long()
03374 3
03375 >>> BitVecVal(2**32 - 1, 32).as_signed_long()
03376 -1
03377 >>> BitVecVal(2**64 - 1, 64).as_signed_long()
03378 -1
03379 """
03380 sz = self.size()
03381 val = self.as_long()
03382 if val >= 2**(sz - 1):
03383 val = val - 2**sz
03384 if val < -2**(sz - 1):
03385 val = val + 2**sz
03386 return int(val)