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 4075 of file z3py.py.
4075 def as_long(self):
4076 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
4077
4078 >>> v = BitVecVal(0xbadc0de, 32)
4079 >>> v
4080 195936478
4081 >>> print("0x%.8x" % v.as_long())
4082 0x0badc0de
4083 """
4084 return int(self.as_string())
4085
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 4086 of file z3py.py.
4086 def as_signed_long(self):
4087 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
4088 The most significant bit is assumed to be the sign.
4089
4090 >>> BitVecVal(4, 3).as_signed_long()
4091 -4
4092 >>> BitVecVal(7, 3).as_signed_long()
4093 -1
4094 >>> BitVecVal(3, 3).as_signed_long()
4095 3
4096 >>> BitVecVal(2**32 - 1, 32).as_signed_long()
4097 -1
4098 >>> BitVecVal(2**64 - 1, 64).as_signed_long()
4099 -1
4100 """
4101 sz = self.size()
4102 val = self.as_long()
4103 if val >= 2**(sz - 1):
4104 val = val - 2**sz
4105 if val < -2**(sz - 1):
4106 val = val + 2**sz
4107 return int(val)
4108
◆ as_string()
| as_string | ( | self | ) |
◆ py_value()
Generated by
1.18.0