Class ExprRef

lean_py/z3/core.py:282–386

Base expression node.

class ExprRef:
    """Base expression node."""

    __slots__ = ("_ast", "_sort", "_vars")

    def __init__(
        self,
        ast: ASTNode,
        sort: SortRef,
        vars: frozenset[tuple[str, ASTSort]] = frozenset(),
    ) -> None:
        self._ast = ast
        self._sort = sort
        self._vars = vars

    def sort(self) -> SortRef:
        return self._sort

    def __repr__(self) -> str:
        return _ast_repr(self._ast)

    def __eq__(self, other: object) -> BoolRef:  # type: ignore[override]
        if isinstance(other, (int, float)):
            other = _coerce_val(other, self._sort)
        if not isinstance(other, ExprRef):
            return NotImplemented
        # Normalize: put non-literal args on the left.  Python's reflected
        # comparison protocol can swap self/other when one type is a subclass
        # of the other (e.g. IntNumRef subclasses ArithRef), leading to
        # "5 = x + 3" instead of "x + 3 = 5".  We canonicalize by putting
        # literal/value AST nodes on the RHS so tactics see the natural order.
        lhs, rhs = self._ast, other._ast
        if _is_literal(lhs) and not _is_literal(rhs):
            lhs, rhs = rhs, lhs
        return BoolRef(
            BinOpNode(BinOp.EQ, lhs, rhs),
            _merge(self._vars, other._vars),
        )

    def __ne__(self, other: object) -> BoolRef:  # type: ignore[override]
        if isinstance(other, (int, float)):
            other = _coerce_val(other, self._sort)
        if not isinstance(other, ExprRef):
            return NotImplemented
        return BoolRef(
            BinOpNode(BinOp.NE, self._ast, other._ast),
            _merge(self._vars, other._vars),
        )

    def __hash__(self) -> int:
        return hash(self._ast)

    def __bool__(self) -> bool:
        raise TypeError("Symbolic expressions cannot be cast to concrete Boolean values")

    def num_args(self) -> int:
        """Number of arguments (children) of this expression."""
        return len(_ast_children(self._ast))