Class RatNumRef

lean_py/z3/core.py:571–606

Rational numeral — concrete rational value with extraction methods.

class RatNumRef(ArithRef):
    """Rational numeral — concrete rational value with extraction methods."""

    __slots__ = ("_num", "_den")

    def __init__(self, num: int, den: int) -> None:
        ast = BinOpNode(BinOp.DIV, ToRealNode(IntLit(num)), ToRealNode(IntLit(den)))
        super().__init__(ast, RealSort())
        self._num = num
        self._den = den

    def numerator(self) -> IntNumRef:
        return IntNumRef(IntLit(self._num), IntSort())

    def denominator(self) -> IntNumRef:
        return IntNumRef(IntLit(self._den), IntSort())

    def numerator_as_long(self) -> int:
        return self._num

    def denominator_as_long(self) -> int:
        return self._den

    def as_fraction(self):
        return Fraction(self._num, self._den)

    def as_decimal(self, prec: int = 10) -> str:
        ctx = getcontext()
        ctx.prec = prec
        return str(Decimal(self._num) / Decimal(self._den))

    def as_string(self) -> str:
        return f"{self._num}/{self._den}"

    def as_long(self) -> int:
        return self._num // self._den


class AlgebraicNumRef(ArithRef):