minor change: add a heuristic for preventing constant splitting.

2 files changed, 90 insertions, 64 deletions

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index b6db624d5..3bc17b050 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -23,6 +23,71 @@ using namespace std;
 

 namespace CVC4 {

 

+void String::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 String::getCharSet(std::set<unsigned int> &cset) const {

 	for(std::vector<unsigned int>::const_iterator itr = d_str.begin();

 		itr != d_str.end(); itr++) {

@@ -30,6 +95,21 @@ 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();

+	}

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

+		String s = suffix(i);

+		String p = y.prefix(i);

+		if(s == p) {

+			return true;

+		}

+	}

+	return false;

+}

+

 std::string String::toString() const {

 	std::string str;

 	for(unsigned int i=0; i<d_str.size(); ++i) {

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) {