diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2021-06-07 23:42:59 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-08 06:42:59 +0000 |
| commit | d265cc611581c1d5da16283008d4fcb95eab74dd (patch) | |
| tree | ef2d2b48afa3a4dca1986739e1cbcaf43bfe1a75 /test/python/unit | |
| parent | ccfe07f8daba372d2d88b249aa27fe78ad22ed54 (diff) | |
Change output of getRealValue to a fraction. (#6692)
Our documentation for `toPythonObj` says that real values are represented as Fractions. However, getRealValue yields a float approximation thereof.
We should probably stick to Fractions, since they allow us to precisely capture values in LRA. Also, that's more aligned with the C++ API, which returns a string representation of the (unapproximated) Rational.
Also, document some (potential) weirdness with calling mkReal on floating-point values.
Diffstat (limited to 'test/python/unit')
| -rw-r--r-- | test/python/unit/api/test_term.py | 26 | ||||
| -rw-r--r-- | test/python/unit/api/test_to_python_obj.py | 6 |
2 files changed, 24 insertions, 8 deletions
diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py index 32813e17f..e78188079 100644 --- a/test/python/unit/api/test_term.py +++ b/test/python/unit/api/test_term.py @@ -15,6 +15,7 @@ import pytest import pycvc5 from pycvc5 import kinds from pycvc5 import Sort, Term +from fractions import Fraction @pytest.fixture @@ -1145,12 +1146,27 @@ def test_get_real(solver): assert 0 == real1.getRealValue() assert 0 == real2.getRealValue() assert -17 == real3.getRealValue() - assert -3 / 5 == real4.getRealValue() - assert 127 / 10 == real5.getRealValue() - assert 1 / 4294967297 == real6.getRealValue() + assert Fraction(-3, 5) == real4.getRealValue() + assert Fraction(127, 10) == real5.getRealValue() + assert Fraction(1, 4294967297) == real6.getRealValue() assert 4294967297 == real7.getRealValue() - assert 1 / 18446744073709551617 == real8.getRealValue() - assert float(18446744073709551617) == real9.getRealValue() + assert Fraction(1, 18446744073709551617) == real8.getRealValue() + assert Fraction(18446744073709551617, 1) == real9.getRealValue() + + # Check denominator too large for float + num = 1 + den = 2 ** 64 + 1 + real_big = solver.mkReal(num, den) + assert real_big.isRealValue() + assert Fraction(num, den) == real_big.getRealValue() + + # Check that we're treating floats as decimal aproximations rather than + # IEEE-754-specified values. + real_decimal = solver.mkReal(0.3) + assert real_decimal.isRealValue() + assert Fraction("0.3") == real_decimal.getRealValue() + assert Fraction(0.3) == Fraction(5404319552844595, 18014398509481984) + assert Fraction(0.3) != real_decimal.getRealValue() def test_get_boolean(solver): diff --git a/test/python/unit/api/test_to_python_obj.py b/test/python/unit/api/test_to_python_obj.py index 2ba685d50..bb30fae8f 100644 --- a/test/python/unit/api/test_to_python_obj.py +++ b/test/python/unit/api/test_to_python_obj.py @@ -22,8 +22,8 @@ def testGetBool(): solver = pycvc5.Solver() t = solver.mkTrue() f = solver.mkFalse() - assert t.toPythonObj() == True - assert f.toPythonObj() == False + assert t.toPythonObj() is True + assert f.toPythonObj() is False def testGetInt(): @@ -115,4 +115,4 @@ def testGetValueReal(): xval = solver.getValue(x) yval = solver.getValue(y) assert xval.toPythonObj() == Fraction("6") - assert yval.toPythonObj() == float(Fraction("8.33")) + assert yval.toPythonObj() == Fraction("8.33") |