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

Class FPNumRef

lean_py/z3/core.py:3198–3219  ·  view source on GitHub ↗

Floating-point numeral.

Source from the content-addressed store, hash-verified

3196
3197
3198class FPNumRef(FPRef):
3199 """Floating-point numeral."""
3200
3201 __slots__ = ()
3202
3203 def as_string(self) -> str:
3204 return repr(self)
3205
3206 def isNaN(self) -> bool:
3207 if isinstance(self._ast, FpLitNode):
3208 return math.isnan(struct.unpack("<d", struct.pack("<Q", self._ast.bits))[0])
3209 return False
3210
3211 def isInf(self) -> bool:
3212 if isinstance(self._ast, FpLitNode):
3213 return math.isinf(struct.unpack("<d", struct.pack("<Q", self._ast.bits))[0])
3214 return False
3215
3216 def isZero(self) -> bool:
3217 if isinstance(self._ast, FpLitNode):
3218 return struct.unpack("<d", struct.pack("<Q", self._ast.bits))[0] == 0.0
3219 return False
3220
3221
3222class FPRMRef(ExprRef):

Callers 6

FPValFunction · 0.85
fpNaNFunction · 0.85
fpPlusInfinityFunction · 0.85
fpMinusInfinityFunction · 0.85
fpPlusZeroFunction · 0.85
fpMinusZeroFunction · 0.85

Calls

no outgoing calls

Tested by

no test coverage detected