api: getRealValue: Fix printing of integer values. (#6795)

diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst
index 08d25b205ba9dd7d71d2b97917a217a8f9a58b22..ba0c6fd22f0dc1a509231fdc7fad1a37a2e005e9 100644 (file)
--- a/docs/api/cpp/quickstart.rst
+++ b/docs/api/cpp/quickstart.rst
@@ -105,7 +105,7 @@ This will print the following:
 
   value for x: 1/6
   value for y: 1/6
-  value for x - y: 0
+  value for x - y: 0.0
 
 We can convert these values to C++ types using standard conversion functions.
 

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 43bb3d2dc7a8283762b9158caee5910a5f41bf34..e6de0d16238e89c9bed941af3e19dd8e1b0141d9 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -2812,7 +2812,13 @@ std::string Term::getRealValue() const
   CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node), *d_node)
       << "Term to be a rational value when calling getRealValue()";
   //////// all checks before this line
-  return detail::getRational(*d_node).toString();
+  const Rational& rat = detail::getRational(*d_node);
+  std::string res = rat.toString();
+  if (rat.isIntegral())
+  {
+    return res + ".0";
+  }
+  return res;
   ////////
   CVC5_API_TRY_CATCH_END;
 }

diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index 617f032ab7bbe4b763573b37be51bb7d57c9d72c..96ee1ba47a01d1d518201770c8379a41b0c7ce6a 100644 (file)
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -769,6 +769,7 @@ TEST_F(TestApiBlackTerm, getReal)
   Term real7 = d_solver.mkReal("4294967297");
   Term real8 = d_solver.mkReal("1/18446744073709551617");
   Term real9 = d_solver.mkReal("18446744073709551617");
+  Term real10 = d_solver.mkReal("2343.2343");
 
   ASSERT_TRUE(real1.isRealValue() && real1.isReal64Value()
               && real1.isReal32Value());
@@ -784,18 +785,19 @@ TEST_F(TestApiBlackTerm, getReal)
   ASSERT_TRUE(real7.isRealValue() && real7.isReal64Value());
   ASSERT_TRUE(real8.isRealValue());
   ASSERT_TRUE(real9.isRealValue());
+  ASSERT_TRUE(real10.isRealValue());
 
   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", real1.getRealValue());
+  ASSERT_EQ("0.0", 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", real2.getRealValue());
+  ASSERT_EQ("0.0", 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", real3.getRealValue());
+  ASSERT_EQ("-17.0", 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());
@@ -809,11 +811,13 @@ 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", real7.getRealValue());
+  ASSERT_EQ("4294967297.0", real7.getRealValue());
 
   ASSERT_EQ("1/18446744073709551617", real8.getRealValue());
 
-  ASSERT_EQ("18446744073709551617", real9.getRealValue());
+  ASSERT_EQ("18446744073709551617.0", real9.getRealValue());
+
+  ASSERT_EQ("23432343/10000", real10.getRealValue());
 }
 
 TEST_F(TestApiBlackTerm, getConstArrayBase)