Z3 |

Public Member Functions
FiniteDomainSortRef Class Reference
Inheritance diagram for FiniteDomainSortRef:

## Public Member Functions
def | size (self)
Public Member Functions inherited from SortRef
def | as_ast (self)
def | get_id (self)
def | kind (self)
def | subsort (self, other)
def | cast (self, val)
def | name (self)
def | __eq__ (self, other)
def | __ne__ (self, other)
def | __hash__ (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 | __eq__ (self, other)
def | __hash__ (self)
def | __nonzero__ (self)
def | __bool__ (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 | __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

    Finite domain sort.

Definition at line 7578 of file z3py.py.

## Member Function Documentation

## ◆ size()

def size | ( |  | self | ) |

    Return the size of the finite domain sort

Definition at line 7581 of file z3py.py.

7581 def size(self):
7582 """Return the size of the finite domain sort"""
7583 r = (ctypes.c_ulonglong * 1)()
7584 if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast, r):
7585 return r[0]
7586 else:
7587 raise Z3Exception("Failed to retrieve finite domain sort size")
7588
7589
Z3_get_finite_domain_sort_size
Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t *r)
Store the size of the sort in r. Return false if the call failed. That is, Z3_get_sort_kind(s) == Z3_...

Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), and BitVecSortRef.subsort().