DatatypeRef Class Reference

Inheritance diagram for DatatypeRef:

Public Member Functions
def	sort (self)
Public Member Functions inherited from ExprRef
def	as_ast (self)
def	get_id (self)
def	sort (self)
def	sort_kind (self)
def	__eq__ (self, other)
def	__ne__ (self, other)
def	decl (self)
def	num_args (self)
def	arg (self, idx)
def	children (self)
Public Member Functions inherited from AstRef
def	__init__
def	__del__ (self)
def	__str__ (self)
def	__repr__ (self)
def	sexpr (self)
def	as_ast (self)
def	get_id (self)
def	ctx_ref (self)
def	eq (self, other)
def	translate (self, target)
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

Datatype expressions.

Definition at line 4392 of file z3py.py.

Member Function Documentation

def sort

(

self

)

Return the datatype sort of the datatype expression `self`.

Definition at line 4394 of file z3py.py.

    def sort(self):
        """Return the datatype sort of the datatype expression `self`."""
        return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)