From e67777928ed8c73f6dfc802b5844c95d135c5127 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 19 Nov 2021 10:50:06 -0800
Subject: [PATCH] Allow negative denominator for CLN Rationals constructed from
 string. (#7667)

---
 src/util/rational_cln_imp.cpp      | 40 +++++++++++++++++++++++++++
 src/util/rational_cln_imp.h        | 43 +++---------------------------
 test/unit/api/cpp/solver_black.cpp |  5 ++++
 3 files changed, 49 insertions(+), 39 deletions(-)

diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 033e53e95..2e5097ef1 100644
--- 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 f1b6022cf..017fc3cb4 100644
--- 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 cf6b29017..74910df1e 100644
--- 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)
-- 
2.30.2