diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-08-24 14:09:43 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-08-24 14:09:43 +0200 |
commit | 54e1e611ec23eaa7e39f5bffcc62c462ba0adeb4 (patch) | |
tree | 91ac124eae5002b3fc3d0955b6b767861518a400 /src | |
parent | 0ff3d2dbf187376c3a9aeeeae8d3f47e4d73c1c9 (diff) | |
parent | 26a2fcf1413a02788dc25745fac87eb610b5a55d (diff) |
Merge pull request #191 from timothy-king/cleanup-regexp
Cleaning up the CVC4::String class.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 4 | ||||
-rw-r--r-- | src/util/regexp.cpp | 367 | ||||
-rw-r--r-- | src/util/regexp.h | 391 |
3 files changed, 375 insertions, 387 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index ec788fa78..a98a2a0ef 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1326,14 +1326,14 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned char> &pcset, SetNodes &pv Node st = Rewriter::rewrite(r[0]); if(st.isConst()) { CVC4::String s = st.getConst< CVC4::String >(); - s.getCharSet( cset ); + cset.insert(s.getVec().begin(), s.getVec().end()); } else if(st.getKind() == kind::VARIABLE) { vset.insert( st ); } else { for(unsigned i=0; i<st.getNumChildren(); i++) { if(st[i].isConst()) { CVC4::String s = st[i].getConst< CVC4::String >(); - s.getCharSet( cset ); + cset.insert(s.getVec().begin(), s.getVec().end()); } else { vset.insert( st[i] ); } diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index c32b42bad..f8fc1833c 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -18,105 +18,193 @@ #include "util/regexp.h" #include <algorithm> +#include <climits> #include <iomanip> #include <iostream> +#include <sstream> + +#include "base/cvc4_assert.h" +#include "base/exception.h" 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] == '\\') { +static_assert(UCHAR_MAX == 255, "Unsigned char is assumed to have 256 values."); + +int String::cmp(const String &y) const { + if (size() != y.size()) { + return size() < y.size() ? -1 : 1; + } + for (unsigned int i = 0; i < size(); ++i) { + if (d_str[i] != y.d_str[i]) { + return getUnsignedCharAt(i) < y.getUnsignedCharAt(i) ? -1 : 1; + } + } + return 0; +} + +String String::concat(const String &other) const { + std::vector<unsigned int> ret_vec(d_str); + ret_vec.insert(ret_vec.end(), other.d_str.begin(), other.d_str.end()); + return String(ret_vec); +} + +bool String::strncmp(const String &y, const std::size_t np) const { + std::size_t n = np; + std::size_t b = (size() >= y.size()) ? size() : y.size(); + std::size_t s = (size() <= y.size()) ? size() : y.size(); + if (n > s) { + if (b == s) { + n = s; + } else { + return false; + } + } + for (std::size_t i = 0; i < n; ++i) { + if (d_str[i] != y.d_str[i]) return false; + } + return true; +} + +bool String::rstrncmp(const String &y, const std::size_t np) const { + std::size_t n = np; + std::size_t b = (size() >= y.size()) ? size() : y.size(); + std::size_t s = (size() <= y.size()) ? size() : y.size(); + if (n > s) { + if (b == s) { + n = s; + } else { + return false; + } + } + for (std::size_t i = 0; i < n; ++i) { + if (d_str[size() - i - 1] != y.d_str[y.size() - i - 1]) return false; + } + return true; +} + +std::vector<unsigned> String::toInternal(const std::string &s) { + std::vector<unsigned> str; + 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; + if (i < s.size()) { + switch (s[i]) { + case 'n': { + str.push_back(convertCharToUnsignedInt('\n')); + i++; + } break; + case 't': { + str.push_back(convertCharToUnsignedInt('\t')); + i++; + } break; + case 'v': { + str.push_back(convertCharToUnsignedInt('\v')); + i++; + } break; + case 'b': { + str.push_back(convertCharToUnsignedInt('\b')); + i++; + } break; + case 'r': { + str.push_back(convertCharToUnsignedInt('\r')); + i++; + } break; + case 'f': { + str.push_back(convertCharToUnsignedInt('\f')); + i++; + } break; + case 'a': { + str.push_back(convertCharToUnsignedInt('\a')); + i++; + } break; + case '\\': { + str.push_back(convertCharToUnsignedInt('\\')); + i++; + } break; case 'x': { - if(i + 2 < s.size()) { - if(isxdigit(s[i+1]) && isxdigit(s[i+2])) { - d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) ); + if (i + 2 < s.size()) { + if (isxdigit(s[i + 1]) && isxdigit(s[i + 2])) { + str.push_back(convertCharToUnsignedInt(hexToDec(s[i + 1]) * 16 + + hexToDec(s[i + 2]))); i += 3; } else { - throw CVC4::Exception( "Illegal String Literal: \"" + s + "\"" ); + throw CVC4::Exception("Illegal String Literal: \"" + s + "\""); } } else { - throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must have two digits after \\x" ); + throw CVC4::Exception("Illegal String Literal: \"" + s + + "\", must have two digits after \\x"); } - } - break; + } break; default: { - if(isdigit(s[i])) { + 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((unsigned char)num) ); + 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'; + str.push_back(convertCharToUnsignedInt((unsigned char)num)); i += 3; } else { - d_str.push_back( convertCharToUnsignedInt((unsigned char)num) ); + str.push_back(convertCharToUnsignedInt((unsigned char)num)); i += 2; } } else { - d_str.push_back( convertCharToUnsignedInt((unsigned char)num) ); + str.push_back(convertCharToUnsignedInt((unsigned char)num)); i++; } - } else if((unsigned)s[i] > 127) { - throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" ); + } else if ((unsigned)s[i] > 127) { + throw CVC4::Exception("Illegal String Literal: \"" + s + + "\", must use escaped sequence"); } else { - d_str.push_back( convertCharToUnsignedInt(s[i]) ); + str.push_back(convertCharToUnsignedInt(s[i])); i++; } } } } else { - throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" ); - //d_str.push_back( convertCharToUnsignedInt('\\') ); + throw CVC4::Exception("should be handled by lexer: \"" + s + "\""); + // str.push_back( convertCharToUnsignedInt('\\') ); } - } else if((unsigned)s[i] > 127) { - throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" ); + } else if ((unsigned)s[i] > 127) { + throw CVC4::Exception("Illegal String Literal: \"" + s + + "\", must use escaped sequence"); } else { - d_str.push_back( convertCharToUnsignedInt(s[i]) ); + str.push_back(convertCharToUnsignedInt(s[i])); i++; } } + return str; } -void String::getCharSet(std::set<unsigned char> &cset) const { - for(std::vector<unsigned int>::const_iterator itr = d_str.begin(); - itr != d_str.end(); itr++) { - cset.insert( convertUnsignedIntToChar(*itr) ); - } +unsigned char String::getUnsignedCharAt(size_t pos) const { + Assert(pos < size()); + return convertUnsignedIntToChar(d_str[pos]); } -std::size_t String::overlap(String &y) const { - std::size_t i = d_str.size() < y.size() ? d_str.size() : y.size(); - for(; i>0; i--) { +std::size_t String::overlap(const String &y) const { + std::size_t i = size() < y.size() ? size() : y.size(); + for (; i > 0; i--) { String s = suffix(i); String p = y.prefix(i); - if(s == p) { + if (s == p) { return i; } } return i; } -std::size_t String::roverlap(String &y) const { - std::size_t i = d_str.size() < y.size() ? d_str.size() : y.size(); - for(; i>0; i--) { + +std::size_t String::roverlap(const String &y) const { + std::size_t i = size() < y.size() ? size() : y.size(); + for (; i > 0; i--) { String s = prefix(i); String p = y.suffix(i); - if(s == p) { + if (s == p) { return i; } } @@ -125,36 +213,53 @@ std::size_t String::roverlap(String &y) const { std::string String::toString() const { std::string str; - for(unsigned int i=0; i<d_str.size(); ++i) { - unsigned char c = convertUnsignedIntToChar( d_str[i] ); - if(isprint( c )) { - if(c == '\\') { + for (unsigned int i = 0; i < size(); ++i) { + unsigned char c = convertUnsignedIntToChar(d_str[i]); + if (isprint(c)) { + if (c == '\\') { str += "\\\\"; - } - //else if(c == '\"') { + } + // 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 : { + 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::stringstream ss; - ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c); + ss << std::setfill('0') << std::setw(2) << std::hex << ((int)c); std::string t = ss.str(); - t = t.substr(t.size()-2, 2); + t = t.substr(t.size() - 2, 2); s = "\\x" + t; - //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str(); + // std::string s2 = static_cast<std::ostringstream*>( + // &(std::ostringstream() << (int)c) )->str(); } } str += s; @@ -163,12 +268,126 @@ std::string String::toString() const { return str; } -std::ostream& operator <<(std::ostream& os, const String& s) { +bool String::isRepeated() const { + if (size() > 1) { + unsigned int f = d_str[0]; + for (unsigned i = 1; i < size(); ++i) { + if (f != d_str[i]) return false; + } + } + return true; +} + +bool String::tailcmp(const String &y, int &c) const { + int id_x = size() - 1; + int id_y = y.size() - 1; + while (id_x >= 0 && id_y >= 0) { + if (d_str[id_x] != y.d_str[id_y]) { + c = id_x; + return false; + } + --id_x; + --id_y; + } + c = id_x == -1 ? (-(id_y + 1)) : (id_x + 1); + return true; +} + +std::size_t String::find(const String &y, const std::size_t start) const { + if (size() < y.size() + start) return std::string::npos; + if (y.empty()) return start; + if (empty()) return std::string::npos; + + std::vector<unsigned>::const_iterator itr = std::search( + d_str.begin() + start, d_str.end(), y.d_str.begin(), y.d_str.end()); + if (itr != d_str.end()) { + return itr - d_str.begin(); + } + return std::string::npos; +} + +std::size_t String::rfind(const String &y, const std::size_t start) const { + if (size() < y.size() + start) return std::string::npos; + if (y.empty()) return start; + if (empty()) return std::string::npos; + + std::vector<unsigned>::const_reverse_iterator itr = std::search( + d_str.rbegin() + start, d_str.rend(), y.d_str.rbegin(), y.d_str.rend()); + if (itr != d_str.rend()) { + return itr - d_str.rbegin(); + } + return std::string::npos; +} + +String 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.size(), d_str.end()); + return String(vec); + } else { + return *this; + } +} + +String String::substr(std::size_t i) const { + Assert(i <= size()); + std::vector<unsigned int> ret_vec; + std::vector<unsigned int>::const_iterator itr = d_str.begin() + i; + ret_vec.insert(ret_vec.end(), itr, d_str.end()); + return String(ret_vec); +} + +String String::substr(std::size_t i, std::size_t j) const { + Assert(i + j <= size()); + std::vector<unsigned int> ret_vec; + std::vector<unsigned int>::const_iterator itr = d_str.begin() + i; + ret_vec.insert(ret_vec.end(), itr, itr + j); + return String(ret_vec); +} + +bool String::isNumber() const { + for (unsigned character : d_str) { + unsigned char c = convertUnsignedIntToChar(character); + if (c < '0' || c > '9') { + return false; + } + } + return true; +} + +int String::toNumber() const { + if (isNumber()) { + int ret = 0; + for (unsigned int i = 0; i < size(); ++i) { + unsigned char c = convertUnsignedIntToChar(d_str[i]); + ret = ret * 10 + (int)c - (int)'0'; + } + return ret; + } else { + return -1; + } +} + +unsigned char String::hexToDec(unsigned char c) { + if (c >= '0' && c <= '9') { + return c - '0'; + } else if (c >= 'a' && c <= 'f') { + return c - 'a' + 10; + } else { + Assert(c >= 'A' && c <= 'F'); + return c - 'A' + 10; + } +} + +std::ostream &operator<<(std::ostream &os, const String &s) { return os << "\"" << s.toString() << "\""; } -std::ostream& operator<<(std::ostream& out, const RegExp& s) { +std::ostream &operator<<(std::ostream &out, const RegExp &s) { return out << "regexp(" << s.getType() << ')'; } -}/* CVC4 namespace */ +} // namespace CVC4 diff --git a/src/util/regexp.h b/src/util/regexp.h index e7c8c5806..f451a8dec 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -20,316 +20,104 @@ #ifndef __CVC4__REGEXP_H #define __CVC4__REGEXP_H -#include <algorithm> -#include <cassert> +#include <cstddef> #include <functional> -#include <set> -#include <sstream> +#include <ostream> #include <string> #include <vector> -#include "base/exception.h" -#include "util/hash.h" - namespace CVC4 { class CVC4_PUBLIC String { -public: - static unsigned convertCharToUnsignedInt( unsigned char c ) { + public: + static unsigned convertCharToUnsignedInt(unsigned char c) { unsigned i = c; i = i + 191; - return (i>=256 ? i-256 : i); + return (i >= 256 ? i - 256 : i); } - static unsigned char convertUnsignedIntToChar( unsigned i ){ - unsigned ii = i+65; - return (unsigned char)(ii>=256 ? ii-256 : ii); + static unsigned char convertUnsignedIntToChar(unsigned i) { + unsigned ii = i + 65; + return (unsigned char)(ii >= 256 ? ii - 256 : ii); } - static bool isPrintable( unsigned i ){ - unsigned char c = convertUnsignedIntToChar( i ); - return (c>=' ' && c<='~');//isprint( (int)c ); + static bool isPrintable(unsigned i) { + unsigned char c = convertUnsignedIntToChar(i); + return (c >= ' ' && c <= '~'); // isprint( (int)c ); } -private: - std::vector<unsigned> d_str; - - bool isVecSame(const std::vector<unsigned> &a, const std::vector<unsigned> &b) const { - if(a.size() != b.size()) return false; - else { - return std::equal(a.begin(), a.end(), b.begin()); - //for(unsigned int i=0; i<a.size(); ++i) - //if(a[i] != b[i]) return false; - //return true; - } - } + String() = default; + explicit String(const std::string& s) : d_str(toInternal(s)) {} + explicit String(const char* s) : d_str(toInternal(std::string(s))) {} + explicit String(const unsigned char c) + : d_str({convertCharToUnsignedInt(c)}) {} + explicit String(const std::vector<unsigned>& s) : d_str(s) {} - //guarded - unsigned char hexToDec(unsigned char c) { - if(c>='0' && c<='9') { - return c - '0'; - } else if (c >= 'a' && c <= 'f') { - return c - 'a' + 10; - } else { - assert(c >= 'A' && c <= 'F'); - return c - 'A' + 10; + String& operator=(const String& y) { + if (this != &y) { + d_str = y.d_str; } - } - - void toInternal(const std::string &s); - -public: - String() {} - - String(const std::string &s) { - toInternal(s); - } - - String(const char* s) { - std::string stmp(s); - toInternal(stmp); - } - - String(const unsigned char c) { - d_str.push_back( convertCharToUnsignedInt(c) ); - } - - String(const std::vector<unsigned> &s) : d_str(s) { } - - ~String() {} - - String& operator =(const String& y) { - if(this != &y) d_str = y.d_str; return *this; } - bool operator ==(const String& y) const { - return isVecSame(d_str, y.d_str); - } - - bool operator !=(const String& y) const { - return ! ( isVecSame(d_str, y.d_str) ); - } - - String concat (const String& other) const { - std::vector<unsigned int> ret_vec(d_str); - ret_vec.insert( ret_vec.end(), other.d_str.begin(), other.d_str.end() ); - return String(ret_vec); - } - - 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 convertUnsignedIntToChar(d_str[i]) < convertUnsignedIntToChar(y.d_str[i]); - - 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 convertUnsignedIntToChar(d_str[i]) > convertUnsignedIntToChar(y.d_str[i]); - - 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 convertUnsignedIntToChar(d_str[i]) < convertUnsignedIntToChar(y.d_str[i]); - - 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 convertUnsignedIntToChar(d_str[i]) > convertUnsignedIntToChar(y.d_str[i]); + String concat(const String& other) const; - return true; - } - } + bool operator==(const String& y) const { return cmp(y) == 0; } + bool operator!=(const String& y) const { return cmp(y) != 0; } + bool operator<(const String& y) const { return cmp(y) < 0; } + bool operator>(const String& y) const { return cmp(y) > 0; } + bool operator<=(const String& y) const { return cmp(y) <= 0; } + bool operator>=(const String& y) const { return cmp(y) >= 0; } - bool strncmp(const String &y, const std::size_t np) const { - std::size_t n = np; - std::size_t b = (d_str.size() >= y.d_str.size()) ? d_str.size() : y.d_str.size(); - std::size_t s = (d_str.size() <= y.d_str.size()) ? d_str.size() : y.d_str.size(); - if(n > s) { - if(b == s) { - n = s; - } else { - return false; - } - } - for(std::size_t i=0; i<n; ++i) - if(d_str[i] != y.d_str[i]) return false; - return true; - } - - bool rstrncmp(const String &y, const std::size_t np) const { - std::size_t n = np; - std::size_t b = (d_str.size() >= y.d_str.size()) ? d_str.size() : y.d_str.size(); - std::size_t s = (d_str.size() <= y.d_str.size()) ? d_str.size() : y.d_str.size(); - if(n > s) { - if(b == s) { - n = s; - } else { - return false; - } - } - for(std::size_t 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 { - return ( d_str.size() == 0 ); - } + bool strncmp(const String& y, const std::size_t np) const; + bool rstrncmp(const String& y, const std::size_t np) const; - /*char operator[] (const std::size_t i) const { - assert( i < d_str.size() ); - return convertUnsignedIntToChar(d_str[i]); - }*/ /* * Convenience functions */ std::string toString() const; + bool empty() const { return d_str.empty(); } + bool isEmptyString() const { return empty(); } + std::size_t size() const { return d_str.size(); } - std::size_t size() const { - return d_str.size(); - } + unsigned char getFirstChar() const { return getUnsignedCharAt(0); } + unsigned char getLastChar() const { return getUnsignedCharAt(size() - 1); } - unsigned char getFirstChar() const { - return convertUnsignedIntToChar( d_str[0] ); - } + bool isRepeated() const; + bool tailcmp(const String& y, int& c) const; - unsigned char getLastChar() const { - assert(d_str.size() != 0); - return convertUnsignedIntToChar( d_str[d_str.size() - 1] ); - } + std::size_t find(const String& y, const std::size_t start = 0) const; + std::size_t rfind(const String& y, const std::size_t start = 0) const; - bool isRepeated() const { - if(d_str.size() > 1) { - unsigned int f = d_str[0]; - for(unsigned i=1; i<d_str.size(); ++i) { - if(f != d_str[i]) return false; - } - } - return true; - } + String replace(const String& s, const String& t) const; + String substr(std::size_t i) const; + String substr(std::size_t i, std::size_t j) const; - bool tailcmp(const String &y, int &c) const { - int id_x = d_str.size() - 1; - int id_y = y.d_str.size() - 1; - while(id_x>=0 && id_y>=0) { - if(d_str[id_x] != y.d_str[id_y]) { - c = id_x; - return false; - } - --id_x; --id_y; - } - c = id_x == -1 ? ( - (id_y+1) ) : (id_x + 1); - return true; - } + String prefix(std::size_t i) const { return substr(0, i); } + String suffix(std::size_t i) const { return substr(size() - i, i); } + // if y=y1...yn and overlap returns m, then this is x1...y1...ym + std::size_t overlap(const String& y) const; + // if y=y1...yn and overlap returns m, then this is y(n+1-m)...yn...xk + std::size_t roverlap(const String& y) const; - std::size_t find(const String &y, const std::size_t start = 0) const { - if(d_str.size() < y.d_str.size() + start) return std::string::npos; - if(y.d_str.size() == 0) return start; - if(d_str.size() == 0) return std::string::npos; - std::vector<unsigned>::const_iterator itr = std::search(d_str.begin() + start, d_str.end(), y.d_str.begin(), y.d_str.end()); - if(itr != d_str.end()) { - return itr - d_str.begin(); - }else{ - return std::string::npos; - } - } - - std::size_t rfind( String &y, const std::size_t start = 0) { - std::reverse( d_str.begin(), d_str.end() ); - std::reverse( y.d_str.begin(), y.d_str.end() ); - std::size_t f = find( y, start ); - std::reverse( d_str.begin(), d_str.end() ); - std::reverse( y.d_str.begin(), y.d_str.end() ); - if( f==std::string::npos ){ - return std::string::npos; - }else{ - return f; - } - } + bool isNumber() const; + int toNumber() const; - 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; - } - } + const std::vector<unsigned>& getVec() const { return d_str; } - String substr(std::size_t i) const { - assert(i <= d_str.size()); - std::vector<unsigned int> ret_vec; - std::vector<unsigned int>::const_iterator itr = d_str.begin() + i; - ret_vec.insert(ret_vec.end(), itr, d_str.end()); - return String(ret_vec); - } - String substr(std::size_t i, std::size_t j) const { - assert(i+j <= d_str.size()); - std::vector<unsigned int> ret_vec; - std::vector<unsigned int>::const_iterator itr = d_str.begin() + i; - ret_vec.insert( ret_vec.end(), itr, itr + j ); - return String(ret_vec); - } + private: + // guarded + static unsigned char hexToDec(unsigned char c); - String prefix(std::size_t i) const { - return substr(0, i); - } - String suffix(std::size_t i) const { - return substr(d_str.size() - i, i); - } - // if y=y1...yn and overlap returns m, then this is x1...y1...ym - std::size_t overlap(String &y) const; - // if y=y1...yn and overlap returns m, then this is y(n+1-m)...yn...xk - std::size_t roverlap(String &y) const; - - bool isNumber() const { - if(d_str.size() == 0) return false; - for(unsigned int i=0; i<d_str.size(); ++i) { - unsigned char c = convertUnsignedIntToChar( d_str[i] ); - if(c<'0' || c>'9') { - return false; - } - } - return true; - } - int toNumber() const { - if(isNumber()) { - int ret=0; - for(unsigned int i=0; i<d_str.size(); ++i) { - unsigned char c = convertUnsignedIntToChar( d_str[i] ); - ret = ret * 10 + (int)c - (int)'0'; - } - return ret; - } else { - return -1; - } - } + static std::vector<unsigned> toInternal(const std::string& s); + unsigned char getUnsignedCharAt(size_t pos) const; - void getCharSet(std::set<unsigned char> &cset) const; + /** + * Returns a negative number if *this < y, 0 if *this and y are equal and a + * positive number if *this > y. + */ + int cmp(const String& y) const; - std::vector<unsigned> getVec() const { - return d_str; - } -};/* class String */ + std::vector<unsigned> d_str; +}; /* class String */ namespace strings { @@ -337,48 +125,29 @@ struct CVC4_PUBLIC StringHashFunction { size_t operator()(const ::CVC4::String& s) const { return std::hash<std::string>()(s.toString()); } -};/* struct StringHashFunction */ +}; /* struct StringHashFunction */ -}/* CVC4::strings namespace */ +} // namespace strings -std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& os, const String& s) CVC4_PUBLIC; class CVC4_PUBLIC RegExp { -protected: - int d_type; -public: + public: RegExp() : d_type(1) {} + explicit RegExp(const int t) : d_type(t) {} - RegExp(const int t) : d_type(t) {} - - ~RegExp() {} - - bool operator ==(const RegExp& y) const { - return d_type == y.d_type ; - } - - bool operator !=(const RegExp& y) const { - return d_type != y.d_type ; - } - - bool operator <(const RegExp& y) const { - return d_type < y.d_type; - } - - bool operator >(const RegExp& y) const { - return d_type > y.d_type ; - } - - bool operator <=(const RegExp& y) const { - return d_type <= y.d_type; - } - - bool operator >=(const RegExp& y) const { - return d_type >= y.d_type ; - } + bool operator==(const RegExp& y) const { return d_type == y.d_type; } + bool operator!=(const RegExp& y) const { return d_type != y.d_type; } + bool operator<(const RegExp& y) const { return d_type < y.d_type; } + bool operator>(const RegExp& y) const { return d_type > y.d_type; } + bool operator<=(const RegExp& y) const { return d_type <= y.d_type; } + bool operator>=(const RegExp& y) const { return d_type >= y.d_type; } int getType() const { return d_type; } -};/* class RegExp */ + + private: + int d_type; +}; /* class RegExp */ /** * Hash function for the RegExp constants. @@ -387,10 +156,10 @@ struct CVC4_PUBLIC RegExpHashFunction { inline size_t operator()(const RegExp& s) const { return (size_t)s.getType(); } -};/* struct RegExpHashFunction */ +}; /* struct RegExpHashFunction */ -std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& os, const RegExp& s) CVC4_PUBLIC; -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* __CVC4__REGEXP_H */ |