BitVecNumRef Class Reference
Inheritance diagram for BitVecNumRef:
Public Member Functions | |
| as_long (self) | |
| as_signed_long (self) | |
| as_string (self) | |
| as_binary_string (self) | |
| py_value (self) | |
| Public Member Functions inherited from BitVecRef | |
| sort (self) | |
| size (self) | |
| __add__ (self, other) | |
| __radd__ (self, other) | |
| __mul__ (self, other) | |
| __rmul__ (self, other) | |
| __sub__ (self, other) | |
| __rsub__ (self, other) | |
| __or__ (self, other) | |
| __ror__ (self, other) | |
| __and__ (self, other) | |
| __rand__ (self, other) | |
| __xor__ (self, other) | |
| __rxor__ (self, other) | |
| __pos__ (self) | |
| __neg__ (self) | |
| __invert__ (self) | |
| __div__ (self, other) | |
| __truediv__ (self, other) | |
| __rdiv__ (self, other) | |
| __rtruediv__ (self, other) | |
| __mod__ (self, other) | |
| __rmod__ (self, other) | |
| __le__ (self, other) | |
| __lt__ (self, other) | |
| __gt__ (self, other) | |
| __ge__ (self, other) | |
| __rshift__ (self, other) | |
| __lshift__ (self, other) | |
| __rrshift__ (self, other) | |
| __rlshift__ (self, other) | |
| Public Member Functions inherited from ExprRef | |
| as_ast (self) | |
| get_id (self) | |
| sort_kind (self) | |
| __eq__ (self, other) | |
| __hash__ (self) | |
| __ne__ (self, other) | |
| params (self) | |
| decl (self) | |
| kind (self) | |
| num_args (self) | |
| arg (self, idx) | |
| children (self) | |
| from_string (self, s) | |
| serialize (self) | |
| Public Member Functions inherited from AstRef | |
| __init__ (self, ast, ctx=None) | |
| __del__ (self) | |
| __deepcopy__ (self, memo={}) | |
| __str__ (self) | |
| __repr__ (self) | |
| __eq__ (self, other) | |
| __hash__ (self) | |
| __nonzero__ (self) | |
| __bool__ (self) | |
| sexpr (self) | |
| ctx_ref (self) | |
| eq (self, other) | |
| translate (self, target) | |
| __copy__ (self) | |
| hash (self) | |
| Public Member Functions inherited from Z3PPObject | |
| use_pp (self) | |
Additional Inherited Members | |
| Data Fields inherited from AstRef | |
| ast = ast | |
| ctx = _get_ctx(ctx) | |
| Protected Member Functions inherited from Z3PPObject | |
| _repr_html_ (self) | |
Detailed Description
Member Function Documentation
◆ as_binary_string()
| as_binary_string | ( | self | ) |
◆ as_long()
| as_long | ( | self | ) |
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 3994 of file z3py.py.
3994 def as_long(self):
3995 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
3996
3997 >>> v = BitVecVal(0xbadc0de, 32)
3998 >>> v
3999 195936478
4000 >>> print("0x%.8x" % v.as_long())
4001 0x0badc0de
4002 """
4003 return int(self.as_string())
4004
Referenced by as_signed_long(), and py_value().
◆ as_signed_long()
| as_signed_long | ( | self | ) |
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 4005 of file z3py.py.
4005 def as_signed_long(self):
4006 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
4007 The most significant bit is assumed to be the sign.
4008
4009 >>> BitVecVal(4, 3).as_signed_long()
4010 -4
4011 >>> BitVecVal(7, 3).as_signed_long()
4012 -1
4013 >>> BitVecVal(3, 3).as_signed_long()
4014 3
4015 >>> BitVecVal(2**32 - 1, 32).as_signed_long()
4016 -1
4017 >>> BitVecVal(2**64 - 1, 64).as_signed_long()
4018 -1
4019 """
4020 sz = self.size()
4021 val = self.as_long()
4022 if val >= 2**(sz - 1):
4023 val = val - 2**sz
4024 if val < -2**(sz - 1):
4025 val = val + 2**sz
4026 return int(val)
4027
◆ as_string()
| as_string | ( | self | ) |
◆ py_value()
Generated by
1.14.0