FiniteDomainNumRef Class Reference

Inheritance diagram for FiniteDomainNumRef:

Public Member Functions
	as_long (self)
	as_string (self)
Public Member Functions inherited from FiniteDomainRef
	sort (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)
	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)
	py_value (self)
Public Member Functions inherited from Z3PPObject
	use_pp (self)

Additional Inherited Members
Data Fields inherited from FiniteDomainRef
	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 7974 of file z3py.py.

Member Function Documentation

as_long()

as_long

(

self

)

Return a Z3 finite-domain numeral as a Python long (bignum) numeral.

>>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(3, s)
>>> v
3
>>> v.as_long() + 1
4

Definition at line 7977 of file z3py.py.

    def as_long(self):
        """Return a Z3 finite-domain numeral as a Python long (bignum) numeral.
 
        >>> s = FiniteDomainSort('S', 100)
        >>> v = FiniteDomainVal(3, s)
        >>> v
        3
        >>> v.as_long() + 1
        4
        """
        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 finite-domain numeral as a Python string.

>>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(42, s)
>>> v.as_string()
'42'

Reimplemented from FiniteDomainRef.

Definition at line 7989 of file z3py.py.

    def as_string(self):
        """Return a Z3 finite-domain numeral as a Python string.
 
        >>> s = FiniteDomainSort('S', 100)
        >>> v = FiniteDomainVal(42, s)
        >>> v.as_string()
        '42'
        """
        return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
 
 

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