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.

1 files changed, 18 insertions, 1 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):