1 /********************* */
4 ** Top contributors (to current version):
5 ** Tianyi Liang, Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing 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
29 #include "base/exception.h"
30 #include "util/hash.h"
34 class CVC4_PUBLIC String
{
36 static unsigned convertCharToUnsignedInt( unsigned char c
) {
39 return (i
>=256 ? i
-256 : i
);
41 static unsigned char convertUnsignedIntToChar( unsigned i
){
43 return (unsigned char)(ii
>=256 ? ii
-256 : ii
);
45 static bool isPrintable( unsigned i
){
46 unsigned char c
= convertUnsignedIntToChar( i
);
47 return (c
>=' ' && c
<='~');//isprint( (int)c );
51 std::vector
<unsigned> d_str
;
53 bool isVecSame(const std::vector
<unsigned> &a
, const std::vector
<unsigned> &b
) const {
54 if(a
.size() != b
.size()) return false;
56 return std::equal(a
.begin(), a
.end(), b
.begin());
57 //for(unsigned int i=0; i<a.size(); ++i)
58 //if(a[i] != b[i]) return false;
64 unsigned char hexToDec(unsigned char c
) {
65 if(c
>='0' && c
<='9') {
67 } else if (c
>= 'a' && c
<= 'f') {
70 assert(c
>= 'A' && c
<= 'F');
75 void toInternal(const std::string
&s
);
80 String(const std::string
&s
) {
84 String(const char* s
) {
89 String(const unsigned char c
) {
90 d_str
.push_back( convertCharToUnsignedInt(c
) );
93 String(const std::vector
<unsigned> &s
) : d_str(s
) { }
97 String
& operator =(const String
& y
) {
98 if(this != &y
) d_str
= y
.d_str
;
102 bool operator ==(const String
& y
) const {
103 return isVecSame(d_str
, y
.d_str
);
106 bool operator !=(const String
& y
) const {
107 return ! ( isVecSame(d_str
, y
.d_str
) );
110 String
concat (const String
& other
) const {
111 std::vector
<unsigned int> ret_vec(d_str
);
112 ret_vec
.insert( ret_vec
.end(), other
.d_str
.begin(), other
.d_str
.end() );
113 return String(ret_vec
);
116 bool operator <(const String
& y
) const {
117 if(d_str
.size() != y
.d_str
.size()) return d_str
.size() < y
.d_str
.size();
119 for(unsigned int i
=0; i
<d_str
.size(); ++i
)
120 if(d_str
[i
] != y
.d_str
[i
]) return convertUnsignedIntToChar(d_str
[i
]) < convertUnsignedIntToChar(y
.d_str
[i
]);
126 bool operator >(const String
& y
) const {
127 if(d_str
.size() != y
.d_str
.size()) return d_str
.size() > y
.d_str
.size();
129 for(unsigned int i
=0; i
<d_str
.size(); ++i
)
130 if(d_str
[i
] != y
.d_str
[i
]) return convertUnsignedIntToChar(d_str
[i
]) > convertUnsignedIntToChar(y
.d_str
[i
]);
136 bool operator <=(const String
& y
) const {
137 if(d_str
.size() != y
.d_str
.size()) return d_str
.size() < y
.d_str
.size();
139 for(unsigned int i
=0; i
<d_str
.size(); ++i
)
140 if(d_str
[i
] != y
.d_str
[i
]) return convertUnsignedIntToChar(d_str
[i
]) < convertUnsignedIntToChar(y
.d_str
[i
]);
146 bool operator >=(const String
& y
) const {
147 if(d_str
.size() != y
.d_str
.size()) return d_str
.size() > y
.d_str
.size();
149 for(unsigned int i
=0; i
<d_str
.size(); ++i
)
150 if(d_str
[i
] != y
.d_str
[i
]) return convertUnsignedIntToChar(d_str
[i
]) > convertUnsignedIntToChar(y
.d_str
[i
]);
156 bool strncmp(const String
&y
, const std::size_t np
) const {
158 std::size_t b
= (d_str
.size() >= y
.d_str
.size()) ? d_str
.size() : y
.d_str
.size();
159 std::size_t s
= (d_str
.size() <= y
.d_str
.size()) ? d_str
.size() : y
.d_str
.size();
167 for(std::size_t i
=0; i
<n
; ++i
)
168 if(d_str
[i
] != y
.d_str
[i
]) return false;
172 bool rstrncmp(const String
&y
, const std::size_t np
) const {
174 std::size_t b
= (d_str
.size() >= y
.d_str
.size()) ? d_str
.size() : y
.d_str
.size();
175 std::size_t s
= (d_str
.size() <= y
.d_str
.size()) ? d_str
.size() : y
.d_str
.size();
183 for(std::size_t i
=0; i
<n
; ++i
)
184 if(d_str
[d_str
.size() - i
- 1] != y
.d_str
[y
.d_str
.size() - i
- 1]) return false;
188 bool isEmptyString() const {
189 return ( d_str
.size() == 0 );
192 /*char operator[] (const std::size_t i) const {
193 assert( i < d_str.size() );
194 return convertUnsignedIntToChar(d_str[i]);
197 * Convenience functions
199 std::string
toString() const;
201 std::size_t size() const {
205 unsigned char getFirstChar() const {
206 return convertUnsignedIntToChar( d_str
[0] );
209 unsigned char getLastChar() const {
210 assert(d_str
.size() != 0);
211 return convertUnsignedIntToChar( d_str
[d_str
.size() - 1] );
214 bool isRepeated() const {
215 if(d_str
.size() > 1) {
216 unsigned int f
= d_str
[0];
217 for(unsigned i
=1; i
<d_str
.size(); ++i
) {
218 if(f
!= d_str
[i
]) return false;
224 bool tailcmp(const String
&y
, int &c
) const {
225 int id_x
= d_str
.size() - 1;
226 int id_y
= y
.d_str
.size() - 1;
227 while(id_x
>=0 && id_y
>=0) {
228 if(d_str
[id_x
] != y
.d_str
[id_y
]) {
234 c
= id_x
== -1 ? ( - (id_y
+1) ) : (id_x
+ 1);
238 std::size_t find(const String
&y
, const std::size_t start
= 0) const {
239 if(d_str
.size() < y
.d_str
.size() + start
) return std::string::npos
;
240 if(y
.d_str
.size() == 0) return start
;
241 if(d_str
.size() == 0) return std::string::npos
;
242 std::vector
<unsigned>::const_iterator itr
= std::search(d_str
.begin() + start
, d_str
.end(), y
.d_str
.begin(), y
.d_str
.end());
243 if(itr
!= d_str
.end()) {
244 return itr
- d_str
.begin();
246 return std::string::npos
;
250 std::size_t rfind( String
&y
, const std::size_t start
= 0) {
251 std::reverse( d_str
.begin(), d_str
.end() );
252 std::reverse( y
.d_str
.begin(), y
.d_str
.end() );
253 std::size_t f
= find( y
, start
);
254 std::reverse( d_str
.begin(), d_str
.end() );
255 std::reverse( y
.d_str
.begin(), y
.d_str
.end() );
256 if( f
==std::string::npos
){
257 return std::string::npos
;
263 String
replace(const String
&s
, const String
&t
) const {
264 std::size_t ret
= find(s
);
265 if( ret
!= std::string::npos
) {
266 std::vector
<unsigned int> vec
;
267 vec
.insert(vec
.begin(), d_str
.begin(), d_str
.begin() + ret
);
268 vec
.insert(vec
.end(), t
.d_str
.begin(), t
.d_str
.end());
269 vec
.insert(vec
.end(), d_str
.begin() + ret
+ s
.d_str
.size(), d_str
.end());
276 String
substr(std::size_t i
) const {
277 assert(i
<= d_str
.size());
278 std::vector
<unsigned int> ret_vec
;
279 std::vector
<unsigned int>::const_iterator itr
= d_str
.begin() + i
;
280 ret_vec
.insert(ret_vec
.end(), itr
, d_str
.end());
281 return String(ret_vec
);
283 String
substr(std::size_t i
, std::size_t j
) const {
284 assert(i
+j
<= d_str
.size());
285 std::vector
<unsigned int> ret_vec
;
286 std::vector
<unsigned int>::const_iterator itr
= d_str
.begin() + i
;
287 ret_vec
.insert( ret_vec
.end(), itr
, itr
+ j
);
288 return String(ret_vec
);
291 String
prefix(std::size_t i
) const {
294 String
suffix(std::size_t i
) const {
295 return substr(d_str
.size() - i
, i
);
297 // if y=y1...yn and overlap returns m, then this is x1...y1...ym
298 std::size_t overlap(String
&y
) const;
299 // if y=y1...yn and overlap returns m, then this is y(n+1-m)...yn...xk
300 std::size_t roverlap(String
&y
) const;
302 bool isNumber() const {
303 if(d_str
.size() == 0) return false;
304 for(unsigned int i
=0; i
<d_str
.size(); ++i
) {
305 unsigned char c
= convertUnsignedIntToChar( d_str
[i
] );
312 int toNumber() const {
315 for(unsigned int i
=0; i
<d_str
.size(); ++i
) {
316 unsigned char c
= convertUnsignedIntToChar( d_str
[i
] );
317 ret
= ret
* 10 + (int)c
- (int)'0';
325 void getCharSet(std::set
<unsigned char> &cset
) const;
327 std::vector
<unsigned> getVec() const {
334 struct CVC4_PUBLIC StringHashFunction
{
335 size_t operator()(const ::CVC4::String
& s
) const {
336 return __gnu_cxx::hash
<const char*>()(s
.toString().c_str());
338 };/* struct StringHashFunction */
340 }/* CVC4::strings namespace */
342 std::ostream
& operator <<(std::ostream
& os
, const String
& s
) CVC4_PUBLIC
;
344 class CVC4_PUBLIC RegExp
{
348 RegExp() : d_type(1) {}
350 RegExp(const int t
) : d_type(t
) {}
354 bool operator ==(const RegExp
& y
) const {
355 return d_type
== y
.d_type
;
358 bool operator !=(const RegExp
& y
) const {
359 return d_type
!= y
.d_type
;
362 bool operator <(const RegExp
& y
) const {
363 return d_type
< y
.d_type
;
366 bool operator >(const RegExp
& y
) const {
367 return d_type
> y
.d_type
;
370 bool operator <=(const RegExp
& y
) const {
371 return d_type
<= y
.d_type
;
374 bool operator >=(const RegExp
& y
) const {
375 return d_type
>= y
.d_type
;
378 int getType() const { return d_type
; }
382 * Hash function for the RegExp constants.
384 struct CVC4_PUBLIC RegExpHashFunction
{
385 inline size_t operator()(const RegExp
& s
) const {
386 return (size_t)s
.getType();
388 };/* struct RegExpHashFunction */
390 std::ostream
& operator <<(std::ostream
& os
, const RegExp
& s
) CVC4_PUBLIC
;
392 }/* CVC4 namespace */
394 #endif /* __CVC4__REGEXP_H */