20 #ifndef __CVC4__REGEXP_H 21 #define __CVC4__REGEXP_H 38 return (
unsigned int)(i<0 ? i+256 : i);
42 return (
char)(ii>=256 ? ii-256 : ii);
45 char c = convertUnsignedIntToChar( i );
46 return isprint( (
int)c );
50 std::vector<unsigned int> d_str;
52 bool isVecSame(
const std::vector<unsigned int> &a,
const std::vector<unsigned int> &b)
const {
53 if(a.size() != b.size())
return false;
55 for(
unsigned int i=0; i<a.size(); ++i)
56 if(a[i] != b[i])
return false;
62 char hexToDec(
char c) {
65 }
else if (c >=
'a' && c <=
'f') {
73 void toInternal(
const std::string &s);
88 d_str.push_back( convertCharToUnsignedInt(c) );
91 String(
const std::vector<unsigned int> &s) : d_str(s) { }
96 if(
this != &y) d_str = y.d_str;
101 return isVecSame(d_str, y.d_str);
105 return ! ( isVecSame(d_str, y.d_str) );
109 std::vector<unsigned int> ret_vec(d_str);
110 ret_vec.insert( ret_vec.end(), other.d_str.begin(), other.d_str.end() );
115 if(d_str.size() != y.d_str.size())
return d_str.size() < y.d_str.size();
117 for(
unsigned int i=0; i<d_str.size(); ++i)
118 if(d_str[i] != y.d_str[i])
return d_str[i] < y.d_str[i];
125 if(d_str.size() != y.d_str.size())
return d_str.size() > y.d_str.size();
127 for(
unsigned int i=0; i<d_str.size(); ++i)
128 if(d_str[i] != y.d_str[i])
return d_str[i] > y.d_str[i];
134 bool operator <=(
const String& y)
const {
135 if(d_str.size() != y.d_str.size())
return d_str.size() < y.d_str.size();
137 for(
unsigned int i=0; i<d_str.size(); ++i)
138 if(d_str[i] != y.d_str[i])
return d_str[i] < y.d_str[i];
144 bool operator >=(
const String& y)
const {
145 if(d_str.size() != y.d_str.size())
return d_str.size() > y.d_str.size();
147 for(
unsigned int i=0; i<d_str.size(); ++i)
148 if(d_str[i] != y.d_str[i])
return d_str[i] > y.d_str[i];
155 for(
unsigned int i=0; i<n; ++i)
156 if(d_str[i] != y.d_str[i])
return false;
161 for(
unsigned int i=0; i<n; ++i)
162 if(d_str[d_str.size() - i - 1] != y.d_str[y.d_str.size() - i - 1])
return false;
167 return ( d_str.size() == 0 );
170 unsigned int operator[] (
const unsigned int i)
const {
177 std::string toString()
const;
184 return convertUnsignedIntToChar( d_str[0] );
188 if(d_str.size() > 1) {
189 unsigned int f = d_str[0];
190 for(
unsigned i=1; i<d_str.size(); ++i) {
191 if(f != d_str[i])
return false;
198 int id_x = d_str.size() - 1;
199 int id_y = y.d_str.size() - 1;
200 while(id_x>=0 && id_y>=0) {
201 if(d_str[id_x] != y.d_str[id_y]) {
207 c = id_x == -1 ? ( - (id_y+1) ) : (id_x + 1);
211 std::size_t
find(
const String &y,
const int start = 0)
const {
212 if(d_str.size() < y.d_str.size() + (std::size_t) start)
return std::string::npos;
213 if(y.d_str.size() == 0)
return (std::size_t) start;
214 if(d_str.size() == 0)
return std::string::npos;
215 std::size_t ret = std::string::npos;
216 for(
int i = start; i <= (int) d_str.size() - (int) y.d_str.size(); i++) {
217 if(d_str[i] == y.d_str[0]) {
219 for(; j<y.d_str.size(); j++) {
220 if(d_str[i+j] != y.d_str[j])
break;
222 if(j == y.d_str.size()) {
223 ret = (std::size_t) i;
232 std::size_t ret = find(s);
233 if( ret != std::string::npos ) {
234 std::vector<unsigned int> vec;
235 vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret);
236 vec.insert(vec.end(), t.d_str.begin(), t.d_str.end());
237 vec.insert(vec.end(), d_str.begin() + ret + s.d_str.size(), d_str.end());
245 std::vector<unsigned int> ret_vec;
246 std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
247 ret_vec.insert(ret_vec.end(), itr, d_str.end());
251 std::vector<unsigned int> ret_vec;
252 std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
253 ret_vec.insert( ret_vec.end(), itr, itr + j );
261 return substr(d_str.size() - i, i);
263 std::size_t overlap(
String &y)
const;
266 if(d_str.size() == 0)
return false;
267 for(
unsigned int i=0; i<d_str.size(); ++i) {
268 char c = convertUnsignedIntToChar( d_str[i] );
278 for(
unsigned int i=0; i<d_str.size(); ++i) {
279 char c = convertUnsignedIntToChar( d_str[i] );
280 ret = ret * 10 + (int)c - (
int)
'0';
287 void getCharSet(std::set<unsigned int> &cset)
const;
313 return d_type == y.
d_type ;
317 return d_type != y.
d_type ;
325 return d_type > y.
d_type ;
328 bool operator <=(
const RegExp& y)
const {
329 return d_type <= y.
d_type;
332 bool operator >=(
const RegExp& y)
const {
333 return d_type >= y.
d_type ;
std::size_t find(const String &y, const int start=0) const
bool strncmp(const String &y, unsigned int n) const
[[ Add one-line brief description here ]]
CVC4's exception base class and some associated utilities.
String concat(const String &other) const
size_t operator()(const RegExp &s) const
String replace(const String &s, const String &t) const
size_t operator()(const ::CVC4::String &s) const
Macros that should be defined everywhere during the building of the libraries and driver binary...
String substr(unsigned i, unsigned j) const
String prefix(unsigned i) const
Hash function for the RegExp constants.
String(const std::vector< unsigned int > &s)
static bool isPrintable(unsigned int i)
std::ostream & operator<<(std::ostream &out, SimplificationMode mode)
static char convertUnsignedIntToChar(unsigned int i)
bool operator!=(enum Result::Sat s, const Result &r)
bool tailcmp(const String &y, int &c) const
bool operator==(enum Result::Sat s, const Result &r)
String substr(unsigned i) const
String(const std::string &s)
static unsigned int convertCharToUnsignedInt(char c)
String suffix(unsigned i) const
bool rstrncmp(const String &y, unsigned int n) const
bool isEmptyString() const
char getFirstChar() const