Class BitVecRef

lean_py/z3/core.py:621–748

Bit-vector expression, maps to Lean's ``BitVec n``.

class BitVecRef(ExprRef):
    """Bit-vector expression, maps to Lean's ``BitVec n``."""

    __slots__ = ()

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

    def _binop(self, op: str, other: BitVecRef | int) -> BitVecRef:
        other = _coerce_bv(other, self._sort)
        return BitVecRef(
            BinOpNode(op, self._ast, other._ast),
            self._sort,  # type: ignore[arg-type]
            _merge(self._vars, other._vars),
        )

    # Arithmetic
    def __add__(self, other: BitVecRef | int) -> BitVecRef:
        return self._binop(BinOp.ADD, other)

    def __radd__(self, other: int) -> BitVecRef:
        return _coerce_bv(other, self._sort)._binop(BinOp.ADD, self)

    def __sub__(self, other: BitVecRef | int) -> BitVecRef:
        return self._binop(BinOp.SUB, other)

    def __rsub__(self, other: int) -> BitVecRef:
        return _coerce_bv(other, self._sort)._binop(BinOp.SUB, self)

    def __mul__(self, other: BitVecRef | int) -> BitVecRef:
        return self._binop(BinOp.MUL, other)

    def __rmul__(self, other: int) -> BitVecRef:
        return _coerce_bv(other, self._sort)._binop(BinOp.MUL, self)

    def __neg__(self) -> BitVecRef:
        return BitVecRef(
            UnOpNode(UnOp.NEG, self._ast),
            self._sort,  # type: ignore[arg-type]
            self._vars,
        )

    # Bitwise
    def __and__(self, other: BitVecRef | int) -> BitVecRef:
        return self._binop(BinOp.BAND, other)

    def __rand__(self, other: int) -> BitVecRef:
        return _coerce_bv(other, self._sort)._binop(BinOp.BAND, self)

    def __or__(self, other: BitVecRef | int) -> BitVecRef:
        return self._binop(BinOp.BOR, other)

    def __ror__(self, other: int) -> BitVecRef: