Class AstVector

lean_py/z3/core.py:3047–3078

Vector of AST nodes.

class AstVector:
    """Vector of AST nodes."""

    def __init__(self, ctx: Context | None = None) -> None:
        self._elems: list[Any] = []

    def push(self, v: Any) -> None:
        self._elems.append(v)

    def __len__(self) -> int:
        return len(self._elems)

    def __getitem__(self, i: int) -> Any:
        return self._elems[i]

    def __setitem__(self, i: int, v: Any) -> None:
        self._elems[i] = v

    def __iter__(self):
        return iter(self._elems)

    def __contains__(self, v: Any) -> bool:
        return v in self._elems

    def __repr__(self) -> str:
        return f"[{', '.join(repr(e) for e in self._elems)}]"

    def translate(self, ctx: Context) -> AstVector:
        return self

    def sexpr(self) -> str:
        return repr(self)


class AstMap: