Change behaviour of Term::getRealValue() (#7316)

This PR modifies the API function Term::getRealValue() to always return a fraction. Beforehand, it would return rationals in fractional notation (15/2) and integers in decimal notation (2.0).

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 7ee33f14374d6f9455f3f713bd6e342c6587fd89..778f700c04d3578841501d079f3f2e393812f759 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -3011,7 +3011,7 @@ std::string Term::getRealValue() const
   std::string res = rat.toString();
   if (rat.isIntegral())
   {
-    return res + ".0";
+    return res + "/1";
   }
   return res;
   ////////

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 1c47927b7d9d806dece54ae768610f6f4e9134fe..73b3d1ee9866c48853e5e60e0ea3b24dc8955c94 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1338,7 +1338,7 @@ class CVC5_EXPORT Term
   bool isRealValue() const;
   /**
    * Asserts isRealValue().
-   * @return the representation of a rational value as a (decimal) string.
+   * @return the representation of a rational value as a (rational) string.
    */
   std::string getRealValue() const;
 

diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index fe5838cd4c34d14a14873e23bbb0d8cc20ca333b..7cfbe25272b0bc40a8cd711452e6652662006715 100644 (file)
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -789,15 +789,15 @@ TEST_F(TestApiBlackTerm, getReal)
 
   ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real1.getReal32Value());
   ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real1.getReal64Value());
-  ASSERT_EQ("0.0", real1.getRealValue());
+  ASSERT_EQ("0/1", real1.getRealValue());
 
   ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real2.getReal32Value());
   ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real2.getReal64Value());
-  ASSERT_EQ("0.0", real2.getRealValue());
+  ASSERT_EQ("0/1", real2.getRealValue());
 
   ASSERT_EQ((std::pair<int32_t, uint32_t>(-17, 1)), real3.getReal32Value());
   ASSERT_EQ((std::pair<int64_t, uint64_t>(-17, 1)), real3.getReal64Value());
-  ASSERT_EQ("-17.0", real3.getRealValue());
+  ASSERT_EQ("-17/1", real3.getRealValue());
 
   ASSERT_EQ((std::pair<int32_t, uint32_t>(-3, 5)), real4.getReal32Value());
   ASSERT_EQ((std::pair<int64_t, uint64_t>(-3, 5)), real4.getReal64Value());
@@ -811,11 +811,11 @@ TEST_F(TestApiBlackTerm, getReal)
   ASSERT_EQ("1/4294967297", real6.getRealValue());
 
   ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), real7.getReal64Value());
-  ASSERT_EQ("4294967297.0", real7.getRealValue());
+  ASSERT_EQ("4294967297/1", real7.getRealValue());
 
   ASSERT_EQ("1/18446744073709551617", real8.getRealValue());
 
-  ASSERT_EQ("18446744073709551617.0", real9.getRealValue());
+  ASSERT_EQ("18446744073709551617/1", real9.getRealValue());
 
   ASSERT_EQ("23432343/10000", real10.getRealValue());
 }