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

Class FPSortRef

lean_py/z3/core.py:3119–3133  ·  view source on GitHub ↗

Floating-point sort (IEEE 754).

Source from the content-addressed store, hash-verified

3117
3118
3119class FPSortRef(SortRef):
3120 """Floating-point sort (IEEE 754)."""
3121
3122 __slots__ = ("_ebits", "_sbits")
3123
3124 def __init__(self, ebits: int, sbits: int) -> None:
3125 super().__init__(FpASTSort(ebits, sbits))
3126 self._ebits = ebits
3127 self._sbits = sbits
3128
3129 def ebits(self) -> int:
3130 return self._ebits
3131
3132 def sbits(self) -> int:
3133 return self._sbits
3134
3135
3136class FPRef(ExprRef):

Callers 2

sortMethod · 0.85
FPSortFunction · 0.85

Calls

no outgoing calls

Tested by

no test coverage detected