More cleanup in strings (#2138)

2 files changed, 13 insertions, 13 deletions

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 8589c6993..93178b948 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -421,18 +421,11 @@ size_t String::maxSize()
 {
   return std::numeric_limits<size_t>::max();
 }
-
-int String::toNumber() const {
-  if (isNumber()) {
-    int ret = 0;
-    for (unsigned int i = 0; i < size(); ++i) {
-      unsigned char c = convertUnsignedIntToChar(d_str[i]);
-      ret = ret * 10 + (int)c - (int)'0';
-    }
-    return ret;
-  } else {
-    return -1;
-  }
+Rational String::toNumber() const
+{
+  // when smt2 standard for strings is set, this may change, based on the
+  // semantics of str.from.int for leading zeros
+  return Rational(toString());
 }
 
 unsigned char String::hexToDec(unsigned char c) {
diff --git a/src/util/regexp.h b/src/util/regexp.h
index e2d07111d..e91ca61e2 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -25,6 +25,7 @@
 #include <ostream>
 #include <string>
 #include <vector>
+#include "util/rational.h"
 
 namespace CVC4 {
 
@@ -178,8 +179,14 @@ class CVC4_PUBLIC String {
   */
   std::size_t roverlap(const String& y) const;
 
+  /**
+   * Returns true if this string corresponds in text to a number, for example
+   * this returns true for strings "7", "12", "004", "0" and false for strings
+   * "abc", "4a", "-4", "".
+   */
   bool isNumber() const;
-  int toNumber() const;
+  /** Returns the corresponding rational for the text of this string. */
+  Rational toNumber() const;
 
   const std::vector<unsigned>& getVec() const { return d_str; }
   /** is the unsigned a digit?