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
std::ostream & operator<<(std::ostream &out, const SubrangeBound &bound)
String prefix(unsigned i) const
Hash function for the RegExp constants.
String(const std::vector< unsigned int > &s)
static bool isPrintable(unsigned int i)
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