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) | |
| update (self, *args) | |
| 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 4065 of file z3py.py.
4065 def as_long(self):
4066 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
4067
4068 >>> v = BitVecVal(0xbadc0de, 32)
4069 >>> v
4070 195936478
4071 >>> print("0x%.8x" % v.as_long())
4072 0x0badc0de
4073 """
4074 return int(self.as_string())
4075
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 4076 of file z3py.py.
4076 def as_signed_long(self):
4077 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
4078 The most significant bit is assumed to be the sign.
4079
4080 >>> BitVecVal(4, 3).as_signed_long()
4081 -4
4082 >>> BitVecVal(7, 3).as_signed_long()
4083 -1
4084 >>> BitVecVal(3, 3).as_signed_long()
4085 3
4086 >>> BitVecVal(2**32 - 1, 32).as_signed_long()
4087 -1
4088 >>> BitVecVal(2**64 - 1, 64).as_signed_long()
4089 -1
4090 """
4091 sz = self.size()
4092 val = self.as_long()
4093 if val >= 2**(sz - 1):
4094 val = val - 2**sz
4095 if val < -2**(sz - 1):
4096 val = val + 2**sz
4097 return int(val)
4098
◆ as_string()
| as_string | ( | self | ) |
◆ py_value()
Generated by
1.16.1