Class SeqRef

lean_py/z3/core.py:3873–3913

Sequence expression.

class SeqRef(ExprRef):
    """Sequence expression."""

    __slots__ = ()

    def __init__(
        self,
        ast: ASTNode,
        sort: SeqSortRef,
        vars: frozenset[tuple[str, ASTSort]] = frozenset(),
    ) -> None:
        super().__init__(ast, sort, vars)

    def __add__(self, other: SeqRef) -> SeqRef:
        if not isinstance(other, SeqRef):
            return NotImplemented
        return SeqRef(
            SeqConcatNode(self._ast, other._ast),
            self._sort,  # type: ignore[arg-type]
            _merge(self._vars, other._vars),
        )

    def __getitem__(self, idx: ArithRef | int) -> ExprRef:
        if isinstance(idx, int):
            idx = IntVal(idx)
        sort = self._sort
        elem_sort = sort._elem if isinstance(sort, SeqSortRef) else IntSort()
        return ExprRef(
            SeqNthNode(self._ast, idx._ast),
            elem_sort,
            _merge(self._vars, idx._vars),
        )

    def at(self, idx: ArithRef | int) -> ExprRef:
        """Return a unit sequence at the given index."""
        elem = self[idx]
        return Unit(elem)

    def is_string(self) -> bool:
        sort = self._sort
        return isinstance(sort, SeqSortRef) and sort.is_string()


def SeqSort(s: SortRef) -> SeqSortRef | StringSortRef: