FiniteDomainSortRef Class Reference

Inheritance diagram for FiniteDomainSortRef:

Public Member Functions
def	size
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

Finite domain sort.

Definition at line 6378 of file z3py.py.

Member Function Documentation

def size

(

self

)

Return the size of the finite domain sort

Definition at line 6381 of file z3py.py.

    def size(self):
        """Return the size of the finite domain sort"""
        r = (ctype.c_ulonglong * 1)()
        if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast(), r):
            return r[0]
        else:
            raise Z3Exception("Failed to retrieve finite domain sort size")