Function fpMinusInfinity

lean_py/z3/core.py:3285–3287

(sort: FPSortRef, ctx: Context | None = None)

def fpMinusInfinity(sort: FPSortRef, ctx: Context | None = None) -> FPNumRef:
    bits = struct.unpack("<Q", struct.pack("<d", float("-inf")))[0]
    return FPNumRef(FpLitNode(bits, sort.ebits(), sort.sbits()), sort, frozenset())


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