From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 7 Oct 2021 00:37:08 +0000 (-0700)
Subject: Change behaviour of Term::getRealValue() (#7316)
X-Git-Tag: cvc5-1.0.0~1115
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f78ed85a8263d7ad632e679034e662091511670;p=cvc5.git

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 7ee33f143..778f700c0 100644
--- 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 1c47927b7..73b3d1ee9 100644
--- 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 fe5838cd4..7cfbe2527 100644
--- 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());
 }