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.

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")