Public Member Functions | |
as_long (self) | |
as_signed_long (self) | |
as_string (self) | |
as_binary_string (self) | |
![]() | |
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) | |
![]() | |
as_ast (self) | |
get_id (self) | |
sort_kind (self) | |
__eq__ (self, other) | |
__hash__ (self) | |
__ne__ (self, other) | |
params (self) | |
decl (self) | |
num_args (self) | |
arg (self, idx) | |
children (self) | |
from_string (self, s) | |
serialize (self) | |
![]() | |
__init__ (self, ast, ctx=None) | |
__del__ (self) | |
__deepcopy__ (self, memo={}) | |
__str__ (self) | |
__repr__ (self) | |
__nonzero__ (self) | |
__bool__ (self) | |
sexpr (self) | |
ctx_ref (self) | |
eq (self, other) | |
translate (self, target) | |
__copy__ (self) | |
hash (self) | |
![]() | |
use_pp (self) | |
Additional Inherited Members | |
![]() | |
ctx = _coerce_exprs(self, other) | |
![]() | |
ctx | |
![]() | |
ast = ast | |
ctx = _get_ctx(ctx) | |
![]() | |
_repr_html_ (self) | |
as_binary_string | ( | self | ) |
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 3949 of file z3py.py.
Referenced by BitVecNumRef.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 3960 of file z3py.py.
as_string | ( | self | ) |
Definition at line 3983 of file z3py.py.
Referenced by BitVecNumRef.as_long(), and IntNumRef.as_long().