Class FPRMRef

lean_py/z3/core.py:3222–3232

Floating-point rounding mode.

class FPRMRef(ExprRef):
    """Floating-point rounding mode."""

    __slots__ = ()

    def __init__(self, name: str) -> None:
        super().__init__(
            _AstVar(name),
            SortRef(_rm_ast_sort),
            frozenset(),
        )


def FPSort(ebits: int, sbits: int, ctx: Context | None = None) -> FPSortRef: