Class StringRef

lean_py/z3/core.py:2245–2266

String expression.

class StringRef(ExprRef):
    """String expression."""

    __slots__ = ()

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

    def __add__(self, other: StringRef) -> StringRef:
        if isinstance(other, str):
            other = StringVal(other)
        return StringRef(
            StrConcatNode(self._ast, other._ast),
            _merge(self._vars, other._vars),
        )

    def __radd__(self, other: str) -> StringRef:
        return StringVal(other) + self


def StringSort() -> StringSortRef: