From 2f78ed85a8263d7ad632e679034e662091511670 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 6 Oct 2021 17:37:08 -0700 Subject: [PATCH] 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). --- src/api/cpp/cvc5.cpp | 2 +- src/api/cpp/cvc5.h | 2 +- test/unit/api/term_black.cpp | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) 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(0, 1)), real1.getReal32Value()); ASSERT_EQ((std::pair(0, 1)), real1.getReal64Value()); - ASSERT_EQ("0.0", real1.getRealValue()); + ASSERT_EQ("0/1", real1.getRealValue()); ASSERT_EQ((std::pair(0, 1)), real2.getReal32Value()); ASSERT_EQ((std::pair(0, 1)), real2.getReal64Value()); - ASSERT_EQ("0.0", real2.getRealValue()); + ASSERT_EQ("0/1", real2.getRealValue()); ASSERT_EQ((std::pair(-17, 1)), real3.getReal32Value()); ASSERT_EQ((std::pair(-17, 1)), real3.getReal64Value()); - ASSERT_EQ("-17.0", real3.getRealValue()); + ASSERT_EQ("-17/1", real3.getRealValue()); ASSERT_EQ((std::pair(-3, 5)), real4.getReal32Value()); ASSERT_EQ((std::pair(-3, 5)), real4.getReal64Value()); @@ -811,11 +811,11 @@ TEST_F(TestApiBlackTerm, getReal) ASSERT_EQ("1/4294967297", real6.getRealValue()); ASSERT_EQ((std::pair(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()); } -- 2.30.2