Improve rewriter for string indexof (#1592)

2 files changed, 10 insertions, 0 deletions

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index d93c5426e..a7e5131ec 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -371,6 +371,11 @@ bool String::isDigit(unsigned character)
   return c >= '0' && c <= '9';
 }
 
+size_t String::maxSize()
+{
+  return std::numeric_limits<size_t>::max();
+}
+
 int String::toNumber() const {
   if (isNumber()) {
     int ret = 0;
diff --git a/src/util/regexp.h b/src/util/regexp.h
index d51ef4372..efbb4579d 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -163,6 +163,11 @@ class CVC4_PUBLIC String {
   */
   static bool isDigit(unsigned character);
 
+  /**
+   * Returns the maximum length of string representable by this class.
+   * Corresponds to the maximum size of d_str.
+   */
+  static size_t maxSize();
  private:
   // guarded
   static unsigned char hexToDec(unsigned char c);