DatatypeSortRef Class Reference

Inheritance diagram for DatatypeSortRef:

Public Member Functions
def	num_constructors
def	constructor
def	recognizer
def	accessor
Public Member Functions inherited from SortRef
def	as_ast
def	get_id
def	kind
def	subsort
def	cast
def	name
def	__eq__
def	__ne__
Public Member Functions inherited from AstRef
def	__init__
def	__del__
def	__str__
def	__repr__
def	sexpr
def	as_ast
def	get_id
def	ctx_ref
def	eq
def	translate
def	hash
Public Member Functions inherited from Z3PPObject
def	use_pp

Additional Inherited Members
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

Datatype sorts.

Definition at line 4361 of file z3py.py.

Member Function Documentation

def accessor	(		self,
			i,
			j
	)

In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.

>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> List.num_constructors()
2
>>> List.constructor(0)
cons
>>> num_accs = List.constructor(0).arity()
>>> num_accs
2
>>> List.accessor(0, 0)
car
>>> List.accessor(0, 1)
cdr
>>> List.constructor(1)
nil
>>> num_accs = List.constructor(1).arity()
>>> num_accs
0

Definition at line 4423 of file z3py.py.

    def accessor(self, i, j):
        """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
        
        >>> List = Datatype('List')
        >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
        >>> List.declare('nil')
        >>> List = List.create()
        >>> List.num_constructors()
        2
        >>> List.constructor(0)
        cons
        >>> num_accs = List.constructor(0).arity()
        >>> num_accs
        2
        >>> List.accessor(0, 0)
        car
        >>> List.accessor(0, 1)
        cdr
        >>> List.constructor(1)
        nil
        >>> num_accs = List.constructor(1).arity()
        >>> num_accs
        0
        """
        if __debug__:
            _z3_assert(i < self.num_constructors(), "Invalid constructor index")
            _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
        return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)