Class FpLitNode

lean_py/z3/_ast.py:432–437

FP value encoded as IEEE 754 bit pattern (always a non-negative int).

@dataclass(frozen=True)
class FpLitNode:
    """FP value encoded as IEEE 754 bit pattern (always a non-negative int)."""

    bits: int  # IEEE 754 bit pattern as uint64
    ebits: int
    sbits: int


@dataclass(frozen=True)