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 4009 of file z3py.py.
4009 def as_long(self):
4010 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
4011
4012 >>> v = BitVecVal(0xbadc0de, 32)
4013 >>> v
4014 195936478
4015 >>> print("0x%.8x" % v.as_long())
4016 0x0badc0de
4017 """
4018 return int(self.as_string())
4019
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 4020 of file z3py.py.
4020 def as_signed_long(self):
4021 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
4022 The most significant bit is assumed to be the sign.
4023
4024 >>> BitVecVal(4, 3).as_signed_long()
4025 -4
4026 >>> BitVecVal(7, 3).as_signed_long()
4027 -1
4028 >>> BitVecVal(3, 3).as_signed_long()
4029 3
4030 >>> BitVecVal(2**32 - 1, 32).as_signed_long()
4031 -1
4032 >>> BitVecVal(2**64 - 1, 64).as_signed_long()
4033 -1
4034 """
4035 sz = self.size()
4036 val = self.as_long()
4037 if val >= 2**(sz - 1):
4038 val = val - 2**sz
4039 if val < -2**(sz - 1):
4040 val = val + 2**sz
4041 return int(val)
4042
◆ as_string()
| as_string | ( | self | ) |
◆ py_value()
Generated on for Z3 by
1.15.0