cvc4-1.3
regexp.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__REGEXP_H
21 #define __CVC4__REGEXP_H
22 
23 #include <iostream>
24 #include <string>
25 //#include "util/cvc4_assert.h"
26 //#include "util/integer.h"
27 #include "util/hash.h"
28 
29 namespace CVC4 {
30 
32 
33 private:
34  std::vector<unsigned int> d_str;
35 
36  bool isVecSame(const std::vector<unsigned int> &a, const std::vector<unsigned int> &b) const {
37  if(a.size() != b.size()) return false;
38  else {
39  for(unsigned int i=0; i<a.size(); ++i)
40  if(a[i] != b[i]) return false;
41  return true;
42  }
43  }
44 
45 public:
46  String() {}
47 
48  String(const std::string &s) {
49  for(unsigned int i=0; i<s.size(); ++i) {
50  d_str.push_back( convertCharToUnsignedInt(s[i]) );
51  }
52  }
53 
54  String(const char* s) {
55  for(unsigned int i=0,len=strlen(s); i<len; ++i) {
56  d_str.push_back( convertCharToUnsignedInt(s[i]) );
57  }
58  }
59 
60  String(const char c) {
61  d_str.push_back( convertCharToUnsignedInt(c) );
62  }
63 
64  String(const std::vector<unsigned int> &s) : d_str(s) { }
65 
66  ~String() {}
67 
68  String& operator =(const String& y) {
69  if(this != &y) d_str = y.d_str;
70  return *this;
71  }
72 
73  bool operator ==(const String& y) const {
74  return isVecSame(d_str, y.d_str);
75  }
76 
77  bool operator !=(const String& y) const {
78  return ! ( isVecSame(d_str, y.d_str) );
79  }
80 
81  String concat (const String& other) const {
82  std::vector<unsigned int> ret_vec(d_str);
83  ret_vec.insert( ret_vec.end(), other.d_str.begin(), other.d_str.end() );
84  return String(ret_vec);
85  }
86 
87  bool operator <(const String& y) const {
88  if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
89  else {
90  for(unsigned int i=0; i<d_str.size(); ++i)
91  if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
92 
93  return false;
94  }
95  }
96 
97  bool operator >(const String& y) const {
98  if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
99  else {
100  for(unsigned int i=0; i<d_str.size(); ++i)
101  if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
102 
103  return false;
104  }
105  }
106 
107  bool operator <=(const String& y) const {
108  if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
109  else {
110  for(unsigned int i=0; i<d_str.size(); ++i)
111  if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
112 
113  return true;
114  }
115  }
116 
117  bool operator >=(const String& y) const {
118  if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
119  else {
120  for(unsigned int i=0; i<d_str.size(); ++i)
121  if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
122 
123  return true;
124  }
125  }
126 
127  bool strncmp(const String &y, unsigned int n) const {
128  for(unsigned int i=0; i<n; ++i)
129  if(d_str[i] != y.d_str[i]) return false;
130  return true;
131  }
132 
133 
134  bool isEmptyString() const {
135  return ( d_str.size() == 0 );
136  }
137 
138  unsigned int operator[] (const unsigned int i) const {
139  //Assert( i < d_str.size() && i >= 0);
140  return d_str[i];
141  }
142  /*
143  * Convenience functions
144  */
145  std::string toString() const {
146  std::string str;
147  for(unsigned int i=0; i<d_str.size(); ++i) {
148  str += convertUnsignedIntToChar( d_str[i] );
149  //TODO isPrintable: ( "\\" + (convertUnsignedIntToChar( d_str[i] ) );
150  }
151  return str;
152  }
153 
154  unsigned size() const {
155  return d_str.size();
156  }
157 
158  char getFirstChar() const {
159  return convertUnsignedIntToChar( d_str[0] );
160  }
161 
162  bool isRepeated() const {
163  if(d_str.size() > 1) {
164  unsigned int f = d_str[0];
165  for(unsigned i=1; i<d_str.size(); ++i) {
166  if(f != d_str[i]) return false;
167  }
168  }
169  return true;
170  }
171 
172  bool tailcmp(const String &y, int &c) const {
173  int id_x = d_str.size() - 1;
174  int id_y = y.d_str.size() - 1;
175  while(id_x>=0 && id_y>=0) {
176  if(d_str[id_x] != y.d_str[id_y]) {
177  c = id_x;
178  return false;
179  }
180  --id_x; --id_y;
181  }
182  c = id_x == -1 ? ( - (id_y+1) ) : (id_x + 1);
183  return true;
184  }
185 
186  String substr(unsigned i) const {
187  std::vector<unsigned int> ret_vec;
188  std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
189  //for(unsigned k=0; k<i; k++) ++itr;
190  ret_vec.insert(ret_vec.end(), itr, d_str.end());
191  return String(ret_vec);
192  }
193  String substr(unsigned i, unsigned j) const {
194  std::vector<unsigned int> ret_vec;
195  std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
196  //for(unsigned k=0; k<i; k++) ++itr;
197  //std::vector<unsigned int>::const_iterator itr2 = itr;
198  //for(unsigned k=0; k<j; k++) ++itr2;
199  ret_vec.insert( ret_vec.end(), itr, itr + j );
200  return String(ret_vec);
201  }
202 
203 public:
204  static unsigned int convertCharToUnsignedInt( char c ) {
205  int i = (int)c;
206  i = i-65;
207  return (unsigned int)(i<0 ? i+256 : i);
208  }
209  static char convertUnsignedIntToChar( unsigned int i ){
210  int ii = i+65;
211  return (char)(ii>=256 ? ii-256 : ii);
212  }
213  static bool isPrintable( unsigned int i ){
214  char c = convertUnsignedIntToChar( i );
215  return isprint( (int)c );
216  }
217 
218 };/* class String */
219 
220 namespace strings {
221 
223  size_t operator()(const ::CVC4::String& s) const {
224  return __gnu_cxx::hash<const char*>()(s.toString().c_str());
225  }
226 };/* struct StringHashFunction */
227 
228 }/* CVC4::strings namespace */
229 
230 inline std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC;
231 inline std::ostream& operator <<(std::ostream& os, const String& s) {
232  return os << "\"" << s.toString() << "\"";
233 }
234 
236 
237 private:
238  std::string d_str;
239 
240 public:
241  RegExp() {}
242 
243  RegExp(const std::string s)
244  : d_str(s) {}
245 
246  ~RegExp() {}
247 
248  RegExp& operator =(const RegExp& y) {
249  if(this != &y) d_str = y.d_str;
250  return *this;
251  }
252 
253  bool operator ==(const RegExp& y) const {
254  return d_str == y.d_str ;
255  }
256 
257  bool operator !=(const RegExp& y) const {
258  return d_str != y.d_str ;
259  }
260 
261  String concat (const RegExp& other) const {
262  return String(d_str + other.d_str);
263  }
264 
265  bool operator <(const RegExp& y) const {
266  return d_str < y.d_str;
267  }
268 
269  bool operator >(const RegExp& y) const {
270  return d_str > y.d_str ;
271  }
272 
273  bool operator <=(const RegExp& y) const {
274  return d_str <= y.d_str;
275  }
276 
277  bool operator >=(const RegExp& y) const {
278  return d_str >= y.d_str ;
279  }
280 
281  /*
282  * Convenience functions
283  */
284 
285  size_t hash() const {
286  unsigned int h = 1;
287 
288  for (size_t i = 0; i < d_str.length(); ++i) {
289  h = (h << 5) + d_str[i];
290  }
291 
292  return h;
293  }
294 
295  std::string toString() const {
296  return d_str;
297  }
298 
299 };/* class RegExp */
300 
305  inline size_t operator()(const RegExp& s) const {
306  return s.hash();
307  }
308 };/* struct RegExpHashFunction */
309 
310 inline std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC;
311 inline std::ostream& operator <<(std::ostream& os, const RegExp& s) {
312  return os << s.toString();
313 }
314 
315 }/* CVC4 namespace */
316 
317 #endif /* __CVC4__REGEXP_H */
bool strncmp(const String &y, unsigned int n) const
Definition: regexp.h:127
String(const char c)
Definition: regexp.h:60
std::string toString() const
Definition: regexp.h:295
std::string toString() const
Definition: regexp.h:145
[[ Add one-line brief description here ]]
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
unsigned size() const
Definition: regexp.h:154
String(const char *s)
Definition: regexp.h:54
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:508
String concat(const String &other) const
Definition: regexp.h:81
size_t operator()(const RegExp &s) const
Definition: regexp.h:305
RegExp(const std::string s)
Definition: regexp.h:243
size_t operator()(const ::CVC4::String &s) const
Definition: regexp.h:223
Macros that should be defined everywhere during the building of the libraries and driver binary...
String concat(const RegExp &other) const
Definition: regexp.h:261
String substr(unsigned i, unsigned j) const
Definition: regexp.h:193
size_t hash() const
Definition: regexp.h:285
Hash function for the RegExp constants.
Definition: regexp.h:304
String(const std::vector< unsigned int > &s)
Definition: regexp.h:64
static bool isPrintable(unsigned int i)
Definition: regexp.h:213
static char convertUnsignedIntToChar(unsigned int i)
Definition: regexp.h:209
bool operator!=(enum Result::Sat s, const Result &r)
bool tailcmp(const String &y, int &c) const
Definition: regexp.h:172
bool operator==(enum Result::Sat s, const Result &r)
String substr(unsigned i) const
Definition: regexp.h:186
String(const std::string &s)
Definition: regexp.h:48
static unsigned int convertCharToUnsignedInt(char c)
Definition: regexp.h:204
bool isRepeated() const
Definition: regexp.h:162
bool isEmptyString() const
Definition: regexp.h:134
char getFirstChar() const
Definition: regexp.h:158