diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-11-19 10:50:06 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-19 18:50:06 +0000 |
commit | e67777928ed8c73f6dfc802b5844c95d135c5127 (patch) | |
tree | ad60a1f35bfd73ddf7580390774707cc64712749 /src/util | |
parent | 2d2e2568403ea3d16c6480e57f88b7ba47193fd9 (diff) |
Allow negative denominator for CLN Rationals constructed from string. (#7667)
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/rational_cln_imp.cpp | 40 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 43 |
2 files changed, 44 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. |