Inheritance diagram for IntNumRef:

Public Member Functions
	as_long (self)

	as_string (self)

	as_binary_string (self)

	py_value (self)

Public Member Functions inherited from ArithRef
	sort (self)

	is_int (self)

	is_real (self)

	__add__ (self, other)

	__radd__ (self, other)

	__mul__ (self, other)

	__rmul__ (self, other)

	__sub__ (self, other)

	__rsub__ (self, other)

	__pow__ (self, other)

	__rpow__ (self, other)

	__div__ (self, other)

	__truediv__ (self, other)

	__rdiv__ (self, other)

	__rtruediv__ (self, other)

	__mod__ (self, other)

	__rmod__ (self, other)

	__neg__ (self)

	__pos__ (self)

	__le__ (self, other)

	__lt__ (self, other)

	__gt__ (self, other)

	__ge__ (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 ArithRef
	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

Integer values.

Definition at line 3061 of file z3py.py.

Member Function Documentation

◆ as_binary_string()

as_binary_string ( self )

Return a Z3 integer numeral as a Python binary string.
>>> v = IntVal(10)
>>> v.as_binary_string()
'1010'

Definition at line 3085 of file z3py.py.

    def as_binary_string(self):
        """Return a Z3 integer numeral as a Python binary string.
        >>> v = IntVal(10)
        >>> v.as_binary_string()
        '1010'
        """
        return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
 

◆ as_long()

as_long ( self )

Return a Z3 integer numeral as a Python long (bignum) numeral.

>>> v = IntVal(1)
>>> v + 1
1 + 1
>>> v.as_long() + 1
2

Definition at line 3064 of file z3py.py.

    def as_long(self):
        """Return a Z3 integer numeral as a Python long (bignum) numeral.
 
        >>> v = IntVal(1)
        >>> v + 1
        1 + 1
        >>> v.as_long() + 1
        2
        """
        if z3_debug():
            _z3_assert(self.is_int(), "Integer value expected")
        return int(self.as_string())
 

Referenced by BitVecNumRef.as_signed_long(), IntNumRef.py_value(), and BitVecNumRef.py_value().

◆ as_string()

as_string ( self )

Return a Z3 integer numeral as a Python string.
>>> v = IntVal(100)
>>> v.as_string()
'100'

Definition at line 3077 of file z3py.py.

    def as_string(self):
        """Return a Z3 integer numeral as a Python string.
        >>> v = IntVal(100)
        >>> v.as_string()
        '100'
        """
        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 a Python value that is equivalent to `self`.

Reimplemented from AstRef.

Definition at line 3093 of file z3py.py.

    def py_value(self):
        return self.as_long()