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

Function fpToIEEEBV

lean_py/z3/core.py:3528–3535  ·  view source on GitHub ↗

Convert FP to IEEE BV representation.

(a: FPRef, ctx: Context | None = None)

Source from the content-addressed store, hash-verified

3526
3527
3528def fpToIEEEBV(a: FPRef, ctx: Context | None = None) -> BitVecRef:
3529 """Convert FP to IEEE BV representation."""
3530 sort = a._sort
3531 if isinstance(sort, FPSortRef):
3532 w = sort.ebits() + sort.sbits()
3533 else:
3534 w = 64
3535 return BitVecRef(AppNode(_AstVar("fpToIEEEBV"), (a._ast,)), BitVecSort(w), a._vars)
3536
3537
3538def fpInfinity(sort: FPSortRef, negative: bool) -> FPNumRef:

Callers

nothing calls this directly

Calls 5

AppNodeClass · 0.90
BitVecRefClass · 0.85
BitVecSortFunction · 0.85
ebitsMethod · 0.45
sbitsMethod · 0.45

Tested by

no test coverage detected