Function TupleSort

lean_py/z3/core.py:1290–1300

Create a tuple sort. Returns (sort, constructor, list_of_accessor_FuncDeclRefs). z3py compat: ctor name = sort name, accessors named project0, project1, ...

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

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

    Returns (sort, constructor, list_of_accessor_FuncDeclRefs).
    z3py compat: ctor name = sort name, accessors named project0, project1, ...
    """
    b = _DatatypeBuilder(name)
    fields = [(f"project{i}", s) for i, s in enumerate(sorts)]
    b.declare(name, *fields)
    sort = b.create()
    return sort, sort.constructor(0), [sort.accessor(0, i) for i in range(len(sorts))]


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