add strings-opt2 for regular splitting

2 files changed, 45 insertions, 48 deletions

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 3bc17b050..3e2fa948c 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -96,10 +96,7 @@ void String::getCharSet(std::set<unsigned int> &cset) const {
 }

 

 bool String::overlap(String &y) const {

-	unsigned n = y.size();

-	if(d_str.size() < y.size()) {

-		n = d_str.size();

-	}

+	unsigned n = d_str.size() < y.size() ? d_str.size() : y.size();

 	for(unsigned i=1; i<n; i++) {

 		String s = suffix(i);

 		String p = y.prefix(i);

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 2bb2b5c4c..1ae01343d 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -34,29 +34,29 @@ namespace CVC4 {
 class CVC4_PUBLIC String {
 public:
   static unsigned int convertCharToUnsignedInt( char c ) {
-	int i = (int)c;
-	i = i-65;
-	return (unsigned int)(i<0 ? i+256 : i);
+    int i = (int)c;
+    i = i-65;
+    return (unsigned int)(i<0 ? i+256 : i);
   }
   static char convertUnsignedIntToChar( unsigned int i ){
-	int ii = i+65;
-	return (char)(ii>=256 ? ii-256 : ii);
+    int ii = i+65;
+    return (char)(ii>=256 ? ii-256 : ii);
   }
   static bool isPrintable( unsigned int i ){
-	char c = convertUnsignedIntToChar( i );
-	return isprint( (int)c );
+    char c = convertUnsignedIntToChar( i );
+    return isprint( (int)c );
   }
 
 private:
   std::vector<unsigned int> d_str;
 
   bool isVecSame(const std::vector<unsigned int> &a, const std::vector<unsigned int> &b) const {
-      if(a.size() != b.size()) return false;
-      else {
-          for(unsigned int i=0; i<a.size(); ++i)
-              if(a[i] != b[i]) return false;
-          return true;
-      }
+    if(a.size() != b.size()) return false;
+    else {
+      for(unsigned int i=0; i<a.size(); ++i)
+        if(a[i] != b[i]) return false;
+      return true;
+    }
   }
 
   //guarded
@@ -76,12 +76,12 @@ public:
   String() {}
 
   String(const std::string &s) {
-	toInternal(s);
+    toInternal(s);
   }
 
   String(const char* s) {
-	std::string stmp(s);
-	toInternal(stmp);
+    std::string stmp(s);
+    toInternal(stmp);
   }
 
   String(const char c) {
@@ -114,53 +114,53 @@ public:
   bool operator <(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
 
-        return false;
+      return false;
     }
   }
 
   bool operator >(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
 
-        return false;
+      return false;
     }
   }
 
   bool operator <=(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
 
-        return true;
+      return true;
     }
   }
 
   bool operator >=(const String& y) const {
     if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
     else {
-        for(unsigned int i=0; i<d_str.size(); ++i)
-            if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+      for(unsigned int i=0; i<d_str.size(); ++i)
+        if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
 
-        return true;
+      return true;
     }
   }
 
   bool strncmp(const String &y, unsigned int n) const {
-      for(unsigned int i=0; i<n; ++i)
-          if(d_str[i] != y.d_str[i]) return false;
-      return true;
+    for(unsigned int i=0; i<n; ++i)
+      if(d_str[i] != y.d_str[i]) return false;
+    return true;
   }
 
   bool rstrncmp(const String &y, unsigned int n) const {
-      for(unsigned int i=0; i<n; ++i)
-          if(d_str[d_str.size() - i - 1] != y.d_str[y.d_str.size() - i - 1]) return false;
-      return true;
+    for(unsigned int i=0; i<n; ++i)
+      if(d_str[d_str.size() - i - 1] != y.d_str[y.d_str.size() - i - 1]) return false;
+    return true;
   }
 
   bool isEmptyString() const {
@@ -229,16 +229,16 @@ public:
   }
 
   String replace(const String &s, const String &t) const {
-	std::size_t ret = find(s);
-	if( ret != std::string::npos ) {
-		std::vector<unsigned int> vec;
-		vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret); 
-		vec.insert(vec.end(), t.d_str.begin(), t.d_str.end());
-		vec.insert(vec.end(), d_str.begin() + ret + s.d_str.size(), d_str.end());
-		return String(vec);
-	} else {
-		return *this;
-	}
+    std::size_t ret = find(s);
+    if( ret != std::string::npos ) {
+      std::vector<unsigned int> vec;
+      vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret); 
+      vec.insert(vec.end(), t.d_str.begin(), t.d_str.end());
+      vec.insert(vec.end(), d_str.begin() + ret + s.d_str.size(), d_str.end());
+      return String(vec);
+    } else {
+      return *this;
+    }
   }
 
   String substr(unsigned i) const {