MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / fpPlusInfinity

Function fpPlusInfinity

lean_py/z3/core.py:3280–3282  ·  view source on GitHub ↗
(sort: FPSortRef, ctx: Context | None = None)

Source from the content-addressed store, hash-verified

3278
3279
3280def fpPlusInfinity(sort: FPSortRef, ctx: Context | None = None) -> FPNumRef:
3281 bits = struct.unpack("<Q", struct.pack("<d", float("inf")))[0]
3282 return FPNumRef(FpLitNode(bits, sort.ebits(), sort.sbits()), sort, frozenset())
3283
3284
3285def fpMinusInfinity(sort: FPSortRef, ctx: Context | None = None) -> FPNumRef:

Callers 5

test_fp_plus_infinityMethod · 0.90
test_fp_infinityMethod · 0.90
test_all_lt_pos_infinityMethod · 0.90
test_inf_is_infMethod · 0.90
fpInfinityFunction · 0.85

Calls 4

FpLitNodeClass · 0.90
FPNumRefClass · 0.85
ebitsMethod · 0.45
sbitsMethod · 0.45

Tested by 4

test_fp_plus_infinityMethod · 0.72
test_fp_infinityMethod · 0.72
test_all_lt_pos_infinityMethod · 0.72
test_inf_is_infMethod · 0.72