Function EnumSort

lean_py/z3/core.py:1277–1287

Create an enumeration sort. Returns (sort, list_of_enum_constants).

(name: str, values: list[str] | tuple[str, ...])

def EnumSort(name: str, values: list[str] | tuple[str, ...]) -> tuple:
    """Create an enumeration sort.

    Returns (sort, list_of_enum_constants).
    """
    b = _DatatypeBuilder(name)
    for v in values:
        b.declare(v)
    sort = b.create()
    consts = [getattr(sort, v) for v in values]
    return sort, consts


def TupleSort(name: str, sorts: list[SortRef] | tuple[SortRef, ...]) -> tuple: