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

Method test_fp_predicates

tests/test_z3_ported.py:3919–3927  ·  view source on GitHub ↗
(self)

Source from the content-addressed store, hash-verified

3917 assert isinstance(fpEQ(x, y), BoolRef)
3918
3919 def test_fp_predicates(self):
3920 x = FP("x", Float32())
3921 assert isinstance(fpIsNaN(x), BoolRef)
3922 assert isinstance(fpIsInf(x), BoolRef)
3923 assert isinstance(fpIsZero(x), BoolRef)
3924 assert isinstance(fpIsNormal(x), BoolRef)
3925 assert isinstance(fpIsSubnormal(x), BoolRef)
3926 assert isinstance(fpIsNegative(x), BoolRef)
3927 assert isinstance(fpIsPositive(x), BoolRef)
3928
3929 def test_fp_to_real(self):
3930 x = FP("x", Float32())

Callers

nothing calls this directly

Calls 9

FPFunction · 0.90
Float32Function · 0.90
fpIsNaNFunction · 0.90
fpIsInfFunction · 0.90
fpIsZeroFunction · 0.90
fpIsNormalFunction · 0.90
fpIsSubnormalFunction · 0.90
fpIsNegativeFunction · 0.90
fpIsPositiveFunction · 0.90

Tested by

no test coverage detected