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

Class FPRef

lean_py/z3/core.py:3136–3195  ·  view source on GitHub ↗

Floating-point expression.

Source from the content-addressed store, hash-verified

3134
3135
3136class FPRef(ExprRef):
3137 """Floating-point expression."""
3138
3139 __slots__ = ()
3140
3141 def __init__(
3142 self,
3143 ast: ASTNode,
3144 sort: SortRef,
3145 vars: frozenset[tuple[str, ASTSort]] = frozenset(),
3146 ) -> None:
3147 super().__init__(ast, sort, vars)
3148
3149 def sort(self) -> FPSortRef:
3150 s = self._sort
3151 if isinstance(s, FPSortRef):
3152 return s
3153 return FPSortRef(0, 0)
3154
3155 def ebits(self) -> int:
3156 return self.sort().ebits()
3157
3158 def sbits(self) -> int:
3159 return self.sort().sbits()
3160
3161 def __add__(self, other: Any) -> FPRef:
3162 return fpAdd(RNE(), self, other)
3163
3164 def __radd__(self, other: Any) -> FPRef:
3165 return fpAdd(RNE(), other, self)
3166
3167 def __sub__(self, other: Any) -> FPRef:
3168 return fpSub(RNE(), self, other)
3169
3170 def __mul__(self, other: Any) -> FPRef:
3171 return fpMul(RNE(), self, other)
3172
3173 def __truediv__(self, other: Any) -> FPRef:
3174 return fpDiv(RNE(), self, other)
3175
3176 def __neg__(self) -> FPRef:
3177 return fpNeg(self)
3178
3179 def __pos__(self) -> FPRef:
3180 return self
3181
3182 def __abs__(self) -> FPRef:
3183 return fpAbs(self)
3184
3185 def __lt__(self, other: Any) -> BoolRef:
3186 return fpLT(self, other)
3187
3188 def __le__(self, other: Any) -> BoolRef:
3189 return fpLEQ(self, other)
3190
3191 def __gt__(self, other: Any) -> BoolRef:
3192 return fpGT(self, other)
3193

Callers 9

FPFunction · 0.85
_fp_opFunction · 0.85
fpToFPFunction · 0.85
fpBVToFPFunction · 0.85
fpFPToFPFunction · 0.85
fpRealToFPFunction · 0.85
fpSignedToFPFunction · 0.85
fpUnsignedToFPFunction · 0.85
fpFPFunction · 0.85

Calls

no outgoing calls

Tested by

no test coverage detected