From 698f5a09b1c0177abfd2eaa2b110de100fd108ef Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 24 Apr 2014 17:30:15 -0500
Subject: minor change: add a heuristic for preventing constant splitting.

---
 src/util/regexp.h | 74 ++++++++-----------------------------------------------
 1 file changed, 10 insertions(+), 64 deletions(-)

(limited to 'src/util/regexp.h')

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 8c4a3922d..2bb2b5c4c 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -70,70 +70,7 @@ private:
 	  }
   }
 
-  void toInternal(const std::string &s) {
-	  d_str.clear();
-	  unsigned i=0;
-	  while(i < s.size()) {
-		  if(s[i] == '\\') {
-			  i++;
-			  if(i < s.size()) {
-				  switch(s[i]) {
-					  case 'n':  {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break;
-					  case 't':  {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break;
-					  case 'v':  {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break;
-					  case 'b':  {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break;
-					  case 'r':  {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break;
-					  case 'f':  {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break;
-					  case 'a':  {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break;
-					  case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break;
-					  case 'x': {
-						  if(i + 2 < s.size()) {
-							if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) &&
-							   (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) {
-								d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );
-								i += 3;
-							} else {
-								throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
-							}
-						  } else {
-							throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
-						  }
-					  }
-					  break;
-					  default: {
-						  if(isdigit(s[i])) {
-							  int num = (int)s[i] - (int)'0';
-							  bool flag = num < 4;
-							  if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') {
-								  num = num * 8 + (int)s[i+1] - (int)'0';
-								  if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') {
-									  num = num * 8 + (int)s[i+2] - (int)'0';
-									  d_str.push_back( convertCharToUnsignedInt((char)num) );
-									  i += 3;
-								  } else {
-									  d_str.push_back( convertCharToUnsignedInt((char)num) );
-									  i += 2;
-								  }
-							  } else {
-								  d_str.push_back( convertCharToUnsignedInt((char)num) );
-								  i++;
-							  }
-						  } else {
-							  d_str.push_back( convertCharToUnsignedInt(s[i]) );
-							  i++;
-						  }
-					  }
-				  }
-			  } else {
-				  throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" );
-				  //d_str.push_back( convertCharToUnsignedInt('\\') );
-			  }
-		  } else {
-			  d_str.push_back( convertCharToUnsignedInt(s[i]) );
-			  i++;
-		  }
-	  }
-  }
+  void toInternal(const std::string &s);
 
 public:
   String() {}
@@ -316,6 +253,15 @@ public:
     ret_vec.insert( ret_vec.end(), itr, itr + j );
     return String(ret_vec);
   }
+
+  String prefix(unsigned i) const {
+	  return substr(0, i);
+  }
+  String suffix(unsigned i) const {
+	  return substr(d_str.size() - i, i);
+  }
+  bool overlap(String &y) const;
+
   bool isNumber() const {
 	 if(d_str.size() == 0) return false;
 	 for(unsigned int i=0; i<d_str.size(); ++i) {
-- 
cgit v1.2.3