1 /********************* */
4 ** Original author: Tianyi Liang
5 ** Major contributors: none
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_public.h"
20 #ifndef __CVC4__REGEXP_H
21 #define __CVC4__REGEXP_H
28 #include "util/exception.h"
29 //#include "util/integer.h"
30 #include "util/hash.h"
34 class CVC4_PUBLIC String
{
36 static unsigned int convertCharToUnsignedInt( char c
) {
39 return (unsigned int)(i
<0 ? i
+256 : i
);
41 static char convertUnsignedIntToChar( unsigned int i
){
43 return (char)(ii
>=256 ? ii
-256 : ii
);
45 static bool isPrintable( unsigned int i
){
46 char c
= convertUnsignedIntToChar( i
);
47 return isprint( (int)c
);
51 std::vector
<unsigned int> d_str
;
53 bool isVecSame(const std::vector
<unsigned int> &a
, const std::vector
<unsigned int> &b
) const {
54 if(a
.size() != b
.size()) return false;
56 for(unsigned int i
=0; i
<a
.size(); ++i
)
57 if(a
[i
] != b
[i
]) return false;
63 char hexToDec(char c
) {
66 } else if (c
>= 'a' && c
>= 'f') {
73 void toInternal(const std::string
&s
);
78 String(const std::string
&s
) {
82 String(const char* s
) {
87 String(const char c
) {
88 d_str
.push_back( convertCharToUnsignedInt(c
) );
91 String(const std::vector
<unsigned int> &s
) : d_str(s
) { }
95 String
& operator =(const String
& y
) {
96 if(this != &y
) d_str
= y
.d_str
;
100 bool operator ==(const String
& y
) const {
101 return isVecSame(d_str
, y
.d_str
);
104 bool operator !=(const String
& y
) const {
105 return ! ( isVecSame(d_str
, y
.d_str
) );
108 String
concat (const String
& other
) const {
109 std::vector
<unsigned int> ret_vec(d_str
);
110 ret_vec
.insert( ret_vec
.end(), other
.d_str
.begin(), other
.d_str
.end() );
111 return String(ret_vec
);
114 bool operator <(const String
& y
) const {
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
];
124 bool operator >(const String
& y
) const {
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
];
154 bool strncmp(const String
&y
, unsigned int n
) const {
155 for(unsigned int i
=0; i
<n
; ++i
)
156 if(d_str
[i
] != y
.d_str
[i
]) return false;
160 bool rstrncmp(const String
&y
, unsigned int n
) const {
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;
166 bool isEmptyString() const {
167 return ( d_str
.size() == 0 );
170 unsigned int operator[] (const unsigned int i
) const {
171 //Assert( i < d_str.size() && i >= 0);
175 * Convenience functions
177 std::string
toString() const;
179 unsigned size() const {
183 char getFirstChar() const {
184 return convertUnsignedIntToChar( d_str
[0] );
187 bool isRepeated() const {
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;
197 bool tailcmp(const String
&y
, int &c
) const {
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
;
231 String
replace(const String
&s
, const String
&t
) const {
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());
244 String
substr(unsigned i
) const {
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());
248 return String(ret_vec
);
250 String
substr(unsigned i
, unsigned j
) const {
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
);
254 return String(ret_vec
);
257 String
prefix(unsigned i
) const {
260 String
suffix(unsigned i
) const {
261 return substr(d_str
.size() - i
, i
);
263 bool overlap(String
&y
) const;
265 bool isNumber() 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
] );
275 int toNumber() const {
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;
292 struct CVC4_PUBLIC StringHashFunction
{
293 size_t operator()(const ::CVC4::String
& s
) const {
294 return __gnu_cxx::hash
<const char*>()(s
.toString().c_str());
296 };/* struct StringHashFunction */
298 }/* CVC4::strings namespace */
300 std::ostream
& operator <<(std::ostream
& os
, const String
& s
) CVC4_PUBLIC
;
302 class CVC4_PUBLIC RegExp
{
306 RegExp() : d_type(1) {}
308 RegExp(const int t
) : d_type(t
) {}
312 bool operator ==(const RegExp
& y
) const {
313 return d_type
== y
.d_type
;
316 bool operator !=(const RegExp
& y
) const {
317 return d_type
!= y
.d_type
;
320 bool operator <(const RegExp
& y
) const {
321 return d_type
< y
.d_type
;
324 bool operator >(const RegExp
& y
) const {
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
;
336 int getType() const { return d_type
; }
340 * Hash function for the RegExp constants.
342 struct CVC4_PUBLIC RegExpHashFunction
{
343 inline size_t operator()(const RegExp
& s
) const {
344 return (size_t)s
.getType();
346 };/* struct RegExpHashFunction */
348 std::ostream
& operator <<(std::ostream
& os
, const RegExp
& s
) CVC4_PUBLIC
;
350 }/* CVC4 namespace */
352 #endif /* __CVC4__REGEXP_H */