FiniteDomainNumRef Class Reference

Inheritance diagram for FiniteDomainNumRef:

Public Member Functions
def	as_long (self)
def	as_string (self)
Public Member Functions inherited from FiniteDomainRef
def	sort (self)
Public Member Functions inherited from ExprRef
def	as_ast (self)
def	get_id (self)
def	sort_kind (self)
def	__eq__ (self, other)
def	__hash__ (self)
def	__ne__ (self, other)
def	params (self)
def	decl (self)
def	num_args (self)
def	arg (self, idx)
def	children (self)
Public Member Functions inherited from AstRef
def	__init__ (self, ast, ctx=None)
def	__del__ (self)
def	__deepcopy__ (self, memo={})
def	__str__ (self)
def	__repr__ (self)
def	__nonzero__ (self)
def	__bool__ (self)
def	sexpr (self)
def	ctx_ref (self)
def	eq (self, other)
def	translate (self, target)
def	__copy__ (self)
def	hash (self)
Public Member Functions inherited from Z3PPObject
def	use_pp (self)

Additional Inherited Members
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

Integer values.

Definition at line 7634 of file z3py.py.

Member Function Documentation

as_long()

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

Definition at line 7637 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())
 

as_string()

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'

Reimplemented from FiniteDomainRef.

Definition at line 7649 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())