Function FPVal

lean_py/z3/core.py:3263–3272

(
    val: float | int | str,
    sort: FPSortRef | None = None,
    ctx: Context | None = None,
)

def FPVal(
    val: float | int | str,
    sort: FPSortRef | None = None,
    ctx: Context | None = None,
) -> FPNumRef:
    if sort is None:
        sort = Float64()
    val = float(val) if isinstance(val, (int, str)) else val
    bits = struct.unpack("<Q", struct.pack("<d", val))[0]
    return FPNumRef(FpLitNode(bits, sort.ebits(), sort.sbits()), sort, frozenset())


def fpNaN(sort: FPSortRef, ctx: Context | None = None) -> FPNumRef: