Allow negative denominator for CLN Rationals constructed from string. (#7667)

diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 033e53e958d00c15a1d394d16b0f5ce419f6e7da..2e5097ef1d8c3b1ced593f2f877633c690f351d4 100644 (file)
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -12,6 +12,8 @@
  *
  * A multi-precision rational constant.
  */
+#include <cln/integer_io.h>
+
 #include <sstream>
 #include <string>
 
@@ -49,6 +51,44 @@ Rational Rational::fromDecimal(const std::string& dec) {
   }
 }
 
+Rational::Rational(const char* s, uint32_t base)
+{
+  try
+  {
+    cln::cl_read_flags flags;
+    flags.rational_base = base;
+    flags.lsyntax = cln::lsyntax_standard;
+
+    const char* p = strchr(s, '/');
+    /* read_rational() does not support the case where the denominator is
+     * negative.  In this case we read the numerator and denominator via
+     * read_integer() and build a rational out of two integers. */
+    if (p)
+    {
+      flags.syntax = cln::syntax_integer;
+      auto num = cln::read_integer(flags, s, p, nullptr);
+      auto den = cln::read_integer(flags, p + 1, nullptr, nullptr);
+      d_value = num / den;
+    }
+    else
+    {
+      flags.syntax = cln::syntax_rational;
+      d_value = read_rational(flags, s, NULL, NULL);
+    }
+  }
+  catch (...)
+  {
+    std::stringstream ss;
+    ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
+    throw std::invalid_argument(ss.str());
+  }
+}
+
+Rational::Rational(const std::string& s, uint32_t base)
+    : Rational(s.c_str(), base)
+{
+}
+
 int Rational::sgn() const
 {
   if (cln::zerop(d_value))

diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index f1b6022cf0fcd47062ee34a800bda6f08a6c448f..017fc3cb4af160034659aa33e6462bba081e4a5d 100644 (file)
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -74,46 +74,11 @@ class CVC5_EXPORT Rational
   /**
    * Constructs a Rational from a C string in a given base (defaults to 10).
    *
-   * Throws std::invalid_argument if the string is not a valid rational.
-   * For more information about what is a valid rational string,
-   * see CLN's documentation for read_rational.
+   * Throws std::invalid_argument if the string is not a valid rational, i.e.,
+   * if it does not match sign{digit}+/sign{digit}+.
    */
-  explicit Rational(const char* s, unsigned base = 10)
-  {
-    cln::cl_read_flags flags;
-
-    flags.syntax = cln::syntax_rational;
-    flags.lsyntax = cln::lsyntax_standard;
-    flags.rational_base = base;
-    try
-    {
-      d_value = read_rational(flags, s, NULL, NULL);
-    }
-    catch (...)
-    {
-      std::stringstream ss;
-      ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
-      throw std::invalid_argument(ss.str());
-    }
-  }
-  Rational(const std::string& s, unsigned base = 10)
-  {
-    cln::cl_read_flags flags;
-
-    flags.syntax = cln::syntax_rational;
-    flags.lsyntax = cln::lsyntax_standard;
-    flags.rational_base = base;
-    try
-    {
-      d_value = read_rational(flags, s.c_str(), NULL, NULL);
-    }
-    catch (...)
-    {
-      std::stringstream ss;
-      ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
-      throw std::invalid_argument(ss.str());
-    }
-  }
+  explicit Rational(const char* s, uint32_t base = 10);
+  Rational(const std::string& s, uint32_t base = 10);
 
   /**
    * Creates a Rational from another Rational, q, by performing a deep copy.

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index cf6b29017a0ee6bc8ae87276018d82973a9ff4b8..74910df1e8fadc6f4a91ce896ab505ac6107c8bc 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -593,6 +593,11 @@ TEST_F(TestApiBlackSolver, mkReal)
   ASSERT_NO_THROW(d_solver.mkReal(val2, val2));
   ASSERT_NO_THROW(d_solver.mkReal(val3, val3));
   ASSERT_NO_THROW(d_solver.mkReal(val4, val4));
+  ASSERT_NO_THROW(d_solver.mkReal("-1/-1"));
+  ASSERT_NO_THROW(d_solver.mkReal("1/-1"));
+  ASSERT_NO_THROW(d_solver.mkReal("-1/1"));
+  ASSERT_NO_THROW(d_solver.mkReal("1/1"));
+  ASSERT_THROW(d_solver.mkReal("/-5"), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkRegexpAll)