Class BoolRef

lean_py/z3/core.py:395–430

Boolean / Prop expression.

class BoolRef(ExprRef):
    """Boolean / Prop expression."""

    __slots__ = ()

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

    def __and__(self, other: BoolRef) -> BoolRef:
        return And(self, other)

    def __or__(self, other: BoolRef) -> BoolRef:
        return Or(self, other)

    def __invert__(self) -> BoolRef:
        return Not(self)

    def __xor__(self, other: BoolRef) -> BoolRef:
        return Xor(self, other)

    # Bool→Int coercion: z3py converts b + 0 to If(b, 1, 0) + 0
    def __add__(self, other: object) -> ArithRef:
        return _bool_to_int(self).__add__(_coerce_arith_any(other))

    def __radd__(self, other: object) -> ArithRef:
        return _coerce_arith_any(other).__add__(_bool_to_int(self))

    def __mul__(self, other: object) -> ArithRef:
        return _bool_to_int(self).__mul__(_coerce_arith_any(other))

    def __rmul__(self, other: object) -> ArithRef:
        return _coerce_arith_any(other).__mul__(_bool_to_int(self))


class ArithRef(ExprRef):