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)
	__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 BitVecRef
	ctx
Data Fields inherited from ExprRef
	ctx
	ast
Data Fields inherited from AstRef
	ast
	ctx
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

Bit-vector values.

Definition at line 4006 of file z3py.py.

Member Function Documentation

as_binary_string()

as_binary_string

(

self

)

Definition at line 4046 of file z3py.py.

    def as_binary_string(self):
        return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
 

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.

    def 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
        """
        return int(self.as_string())
 

Referenced by BitVecNumRef.as_signed_long(), IntNumRef.py_value(), and BitVecNumRef.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.

    def 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
        """
        sz = self.size()
        val = self.as_long()
        if val >= 2**(sz - 1):
            val = val - 2**sz
        if val < -2**(sz - 1):
            val = val + 2**sz
        return int(val)
 

as_string()

as_string

(

self

)

Definition at line 4043 of file z3py.py.

    def as_string(self):
        return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
 

Referenced by IntNumRef.as_long(), and BitVecNumRef.as_long().

py_value()

py_value

(

self

)

Return the Python value of a Z3 bit-vector numeral.

Reimplemented from AstRef.

Definition at line 4049 of file z3py.py.

    def py_value(self):
        """Return the Python value of a Z3 bit-vector numeral."""
        return self.as_long()