diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-11 16:35:17 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-11 16:42:30 -0600 |
commit | 8e83aaadc6c7a653d74a7214f4f81e6ac982c3f7 (patch) | |
tree | 87c5b09416e4f6b344f02b2d840eac6fe8bb4121 /src/util | |
parent | 8accf31d91312a35eae5b4b84dc9d1f1853b7d87 (diff) |
escaped characters, having an issue with smt-lib defintion, further repair is needed.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/regexp.h | 147 |
1 files changed, 126 insertions, 21 deletions
diff --git a/src/util/regexp.h b/src/util/regexp.h index 82b838315..4942c2652 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -22,7 +22,8 @@ #include <iostream> #include <string> -//#include "util/cvc4_assert.h" +#include <sstream> +#include "util/exception.h" //#include "util/integer.h" #include "util/hash.h" @@ -30,6 +31,21 @@ 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); + } + static char convertUnsignedIntToChar( unsigned int i ){ + 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 ); + } + private: std::vector<unsigned int> d_str; @@ -42,19 +58,99 @@ private: } } + //guarded + char hexToDec(char c) { + if(isdigit(c)) { + return c - '0'; + } else if (c >= 'a' && c >= 'f') { + return c - 'a' + 10; + } else { + return c - 'A' + 10; + } + } + + 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( "Error String Literal: \"" + s + "\"" ); + } + } else { + d_str.push_back( convertCharToUnsignedInt(s[i]) ); + i++; + } + } + } + public: String() {} String(const std::string &s) { + toInternal(s); + /* for(unsigned int i=0; i<s.size(); ++i) { d_str.push_back( convertCharToUnsignedInt(s[i]) ); - } + }*/ } String(const char* s) { + std::string stmp(s); + toInternal(stmp); + /* for(unsigned int i=0,len=strlen(s); i<len; ++i) { d_str.push_back( convertCharToUnsignedInt(s[i]) ); - } + }*/ } String(const char c) { @@ -150,8 +246,33 @@ public: std::string toString() const { std::string str; for(unsigned int i=0; i<d_str.size(); ++i) { - str += convertUnsignedIntToChar( d_str[i] ); - //TODO isPrintable: ( "\\" + (convertUnsignedIntToChar( d_str[i] ) ); + char c = convertUnsignedIntToChar( d_str[i] ); + if(isprint( c )) { + if(c == '\\') { + str += "\\"; + } else if(c == '\"') { + str += "\\\""; + } else { + str += c; + } + } else { + std::string s; + switch(c) { + case '\a': s = "\\a"; break; + case '\b': s = "\\b"; break; + case '\t': s = "\\t"; break; + case '\r': s = "\\r"; break; + case '\v': s = "\\v"; break; + case '\f': s = "\\f"; break; + case '\n': s = "\\n"; break; + case '\e': s = "\\e"; break; + default : { + std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str(); + s = "\\x" + s2; + } + } + str += s; + } } return str; } @@ -237,22 +358,6 @@ public: ret_vec.insert( ret_vec.end(), itr, itr + j ); return String(ret_vec); } - -public: - static unsigned int convertCharToUnsignedInt( char c ) { - 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); - } - static bool isPrintable( unsigned int i ){ - char c = convertUnsignedIntToChar( i ); - return isprint( (int)c ); - } - };/* class String */ namespace strings { |