Function FiniteDomainSize

lean_py/z3/core.py:4021–4025

Return size of finite domain sort.

(sort: SortRef, ctx: Context | None = None)

def FiniteDomainSize(sort: SortRef, ctx: Context | None = None) -> int:
    """Return size of finite domain sort."""
    if isinstance(sort, _FiniteDomainSortRef):
        return sort.size()
    raise TypeError("Expected FiniteDomainSort")


# ---------------------------------------------------------------------------