From d265cc611581c1d5da16283008d4fcb95eab74dd Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 7 Jun 2021 23:42:59 -0700 Subject: [PATCH] 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. --- src/api/python/cvc5.pxi | 19 +++++++++++++++- test/python/unit/api/test_term.py | 26 +++++++++++++++++----- test/python/unit/api/test_to_python_obj.py | 6 ++--- 3 files changed, 42 insertions(+), 9 deletions(-) diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 3339543f3..258005207 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -740,6 +740,21 @@ cdef class Solver: return term def mkReal(self, val, den=None): + ''' + Make a real number term. + + Really, makes a rational term. + + Can be used in various forms. + * Given a string "N/D" constructs the corresponding rational. + * Given a string "W.D" constructs the reduction of (W * P + D)/P, where + P is the appropriate power of 10. + * Given a float f, constructs the rational matching f's string + representation. This means that mkReal(0.3) gives 3/10 and not the + IEEE-754 approximation of 3/10. + * Given a string "W" or an integer, constructs that integer. + * Given two strings and/or integers N and D, constructs N/D. + ''' cdef Term term = Term(self) if den is None: term.cterm = self.csolver.mkReal(str(val).encode()) @@ -1766,12 +1781,14 @@ cdef class Term: return self.cterm.isRealValue() def getRealValue(self): - return float(Fraction(self.cterm.getRealValue().decode())) + '''Returns the value of a real term as a Fraction''' + return Fraction(self.cterm.getRealValue().decode()) def isBitVectorValue(self): return self.cterm.isBitVectorValue() def getBitVectorValue(self, base = 2): + '''Returns the value of a bit-vector term as a 0/1 string''' return self.cterm.getBitVectorValue(base).decode() def toPythonObj(self): 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") -- 2.30.2