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)
	__abs__ (self)
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

Integer values.

Definition at line 3113 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 3137 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 3116 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(), BitVecNumRef.py_value(), and 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 3129 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 BitVecNumRef.as_long(), and as_long().

◆ py_value()

py_value ( self )

Return a Python value that is equivalent to `self`.

Reimplemented from AstRef.

Definition at line 3145 of file z3py.py.

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