diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/regexp.cpp | 80 | ||||
-rw-r--r-- | src/util/regexp.h | 74 |
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) { |