Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of the string data type.
11 : : */
12 : :
13 : : #include "util/string.h"
14 : :
15 : : #include <algorithm>
16 : : #include <climits>
17 : : #include <iomanip>
18 : : #include <iostream>
19 : : #include <sstream>
20 : :
21 : : #include "base/check.h"
22 : : #include "base/exception.h"
23 : : #include "util/hash.h"
24 : :
25 : : using namespace std;
26 : :
27 : : namespace cvc5::internal {
28 : :
29 : : static_assert(UCHAR_MAX == 255, "Unsigned char is assumed to have 256 values.");
30 : :
31 : 2 : String::String(const std::wstring& s)
32 : : {
33 : 2 : d_str.resize(s.size());
34 [ - + ]: 2 : for (size_t i = 0, n = s.size(); i < n; ++i)
35 : : {
36 : 0 : unsigned u = static_cast<unsigned>(s[i]);
37 : : #ifdef CVC5_ASSERTIONS
38 : 0 : Assert(u < num_codes());
39 : : #endif
40 : 0 : d_str[i] = u;
41 : : }
42 : 2 : }
43 : :
44 : 84 : String::String(const std::u32string& s)
45 : : {
46 : 84 : d_str.resize(s.size());
47 [ + + ]: 96 : for (size_t i = 0, n = s.size(); i < n; ++i)
48 : : {
49 : 12 : d_str[i] = static_cast<unsigned>(s[i]);
50 : : }
51 : 84 : }
52 : :
53 : 5269749 : String::String(const std::vector<unsigned>& s) : d_str(s)
54 : : {
55 : : #ifdef CVC5_ASSERTIONS
56 [ + + ]: 7238676 : for (unsigned u : d_str)
57 : : {
58 [ - + ][ - + ]: 1968927 : Assert(u < num_codes());
[ - - ]
59 : : }
60 : : #endif
61 : 5269749 : }
62 : :
63 : 5594438 : int String::cmp(const String& y) const
64 : : {
65 [ + + ]: 5594438 : if (size() != y.size())
66 : : {
67 [ + + ]: 17637 : return size() < y.size() ? -1 : 1;
68 : : }
69 [ + + ]: 8101972 : for (unsigned int i = 0; i < size(); ++i)
70 : : {
71 [ + + ]: 2538888 : if (d_str[i] != y.d_str[i])
72 : : {
73 : 13717 : unsigned cp = d_str[i];
74 : 13717 : unsigned cpy = y.d_str[i];
75 [ + + ]: 13717 : return cp < cpy ? -1 : 1;
76 : : }
77 : : }
78 : 5563084 : return 0;
79 : : }
80 : :
81 : 9415 : String String::concat(const String& other) const
82 : : {
83 : 9415 : std::vector<unsigned int> ret_vec(d_str);
84 : 9415 : ret_vec.insert(ret_vec.end(), other.d_str.begin(), other.d_str.end());
85 : 18830 : return String(ret_vec);
86 : 9415 : }
87 : :
88 : 29625 : bool String::strncmp(const String& y, std::size_t n) const
89 : : {
90 [ + + ]: 29625 : std::size_t b = (size() >= y.size()) ? size() : y.size();
91 [ + + ]: 29625 : std::size_t s = (size() <= y.size()) ? size() : y.size();
92 [ - + ]: 29625 : if (n > s)
93 : : {
94 [ - - ]: 0 : if (b == s)
95 : : {
96 : 0 : n = s;
97 : : }
98 : : else
99 : : {
100 : 0 : return false;
101 : : }
102 : : }
103 [ + + ]: 110168 : for (std::size_t i = 0; i < n; ++i)
104 : : {
105 [ + + ]: 88774 : if (d_str[i] != y.d_str[i]) return false;
106 : : }
107 : 21394 : return true;
108 : : }
109 : :
110 : 27646 : bool String::rstrncmp(const String& y, std::size_t n) const
111 : : {
112 [ + + ]: 27646 : std::size_t b = (size() >= y.size()) ? size() : y.size();
113 [ + + ]: 27646 : std::size_t s = (size() <= y.size()) ? size() : y.size();
114 [ - + ]: 27646 : if (n > s)
115 : : {
116 [ - - ]: 0 : if (b == s)
117 : : {
118 : 0 : n = s;
119 : : }
120 : : else
121 : : {
122 : 0 : return false;
123 : : }
124 : : }
125 [ + + ]: 64150 : for (std::size_t i = 0; i < n; ++i)
126 : : {
127 [ + + ]: 46134 : if (d_str[size() - i - 1] != y.d_str[y.size() - i - 1]) return false;
128 : : }
129 : 18016 : return true;
130 : : }
131 : :
132 : 239635 : void String::addCharToInternal(unsigned char ch, std::vector<unsigned>& str)
133 : : {
134 : : // if not a printable character
135 [ + - ][ - + ]: 239635 : if (ch > 127 || ch < 32)
136 : : {
137 : 0 : std::stringstream serr;
138 : : serr << "Illegal string character: \"" << ch
139 : 0 : << "\", must use escape sequence";
140 : 0 : throw cvc5::internal::Exception(serr.str());
141 : 0 : }
142 : : else
143 : : {
144 : 239635 : str.push_back(static_cast<unsigned>(ch));
145 : : }
146 : 239635 : }
147 : :
148 : 145928 : std::vector<unsigned> String::toInternal(const std::string& s,
149 : : bool useEscSequences)
150 : : {
151 : 145928 : std::vector<unsigned> str;
152 : 145928 : unsigned i = 0;
153 [ + + ]: 368071 : while (i < s.size())
154 : : {
155 : : // get the current character
156 : 222143 : char si = s[i];
157 [ + + ][ + + ]: 222143 : if (si != '\\' || !useEscSequences)
158 : : {
159 : 218301 : addCharToInternal(si, str);
160 : 218301 : ++i;
161 : 218301 : continue;
162 : : }
163 : : // the vector of characters, in case we fail to read an escape sequence
164 : 3842 : std::vector<unsigned> nonEscCache;
165 : : // process the '\'
166 : 3842 : addCharToInternal(si, nonEscCache);
167 : 3842 : ++i;
168 : : // are we an escape sequence?
169 : 3842 : bool isEscapeSequence = true;
170 : : // the string corresponding to the hexadecimal code point
171 : 3842 : std::stringstream hexString;
172 : : // is the slash followed by a 'u'? Could be last character.
173 [ + - ][ + + ]: 3842 : if (i >= s.size() || s[i] != 'u')
[ + + ]
174 : : {
175 : 333 : isEscapeSequence = false;
176 : : }
177 : : else
178 : : {
179 : : // process the 'u'
180 : 3509 : addCharToInternal(s[i], nonEscCache);
181 : 3509 : ++i;
182 : 3509 : bool isStart = true;
183 : 3509 : bool isEnd = false;
184 : 3509 : bool hasBrace = false;
185 [ + + ]: 14017 : while (i < s.size())
186 : : {
187 : : // add the next character
188 : 13992 : si = s[i];
189 [ + + ]: 13992 : if (isStart)
190 : : {
191 : 3503 : isStart = false;
192 : : // possibly read '{'
193 [ + + ]: 3503 : if (si == '{')
194 : : {
195 : 3416 : hasBrace = true;
196 : 3416 : addCharToInternal(si, nonEscCache);
197 : 3416 : ++i;
198 : 3416 : continue;
199 : : }
200 : : }
201 [ + + ]: 10489 : else if (si == '}')
202 : : {
203 : : // can only end if we had an open brace and read at least one digit
204 [ + - ][ + + ]: 3391 : isEscapeSequence = hasBrace && !hexString.str().empty();
[ + - ][ - - ]
205 : 3391 : isEnd = true;
206 : 3391 : addCharToInternal(si, nonEscCache);
207 : 3391 : ++i;
208 : 3391 : break;
209 : : }
210 : : // must be a hex digit at this point
211 [ + + ]: 7185 : if (!isHexDigit(static_cast<unsigned>(si)))
212 : : {
213 : 9 : isEscapeSequence = false;
214 : 9 : break;
215 : : }
216 : 7176 : hexString << si;
217 : 7176 : addCharToInternal(si, nonEscCache);
218 : 7176 : ++i;
219 [ + + ][ + + ]: 7176 : if (!hasBrace && hexString.str().size() == 4)
[ + + ][ + + ]
[ - - ]
220 : : {
221 : : // will be finished reading \ u d_3 d_2 d_1 d_0 with no parens
222 : 81 : isEnd = true;
223 : 81 : break;
224 : : }
225 [ + + ][ + + ]: 7095 : else if (hasBrace && hexString.str().size() > 5)
[ + + ][ + + ]
[ - - ]
226 : : {
227 : : // too many digits enclosed in brace, not an escape sequence
228 : 3 : isEscapeSequence = false;
229 : 3 : break;
230 : : }
231 : : }
232 [ + + ]: 3509 : if (!isEnd)
233 : : {
234 : : // if we were interrupted before ending, then this is not a valid
235 : : // escape sequence
236 : 37 : isEscapeSequence = false;
237 : : }
238 : : }
239 [ + + ]: 3842 : if (isEscapeSequence)
240 : : {
241 : 3469 : Assert(!hexString.str().empty() && hexString.str().size() <= 5);
242 : : // Otherwise, we add the escaped character.
243 : : // This is guaranteed not to overflow due to the length of hstr.
244 : : uint32_t val;
245 : 3469 : hexString >> std::hex >> val;
246 [ + + ]: 3469 : if (val >= num_codes())
247 : : {
248 : : // Failed due to being out of range. This can happen for strings of
249 : : // the form \ u { d_4 d_3 d_2 d_1 d_0 } where d_4 is a hexadecimal not
250 : : // in the range [0-2], or the code point is exactly num_codes().
251 : 9 : isEscapeSequence = false;
252 : : }
253 : : else
254 : : {
255 : 3460 : str.push_back(val);
256 : : }
257 : : }
258 : : // if we did not successfully parse an escape sequence, we add back all
259 : : // characters that we cached
260 [ + + ]: 3842 : if (!isEscapeSequence)
261 : : {
262 : 382 : str.insert(str.end(), nonEscCache.begin(), nonEscCache.end());
263 : : }
264 : 3842 : }
265 : : #ifdef CVC5_ASSERTIONS
266 [ + + ]: 368265 : for (unsigned u : str)
267 : : {
268 [ - + ][ - + ]: 222337 : Assert(u < num_codes());
[ - - ]
269 : : }
270 : : #endif
271 : 145928 : return str;
272 : 0 : }
273 : :
274 : 100980 : unsigned String::front() const
275 : : {
276 [ - + ][ - + ]: 100980 : Assert(!d_str.empty());
[ - - ]
277 : 100980 : return d_str.front();
278 : : }
279 : :
280 : 1649 : unsigned String::back() const
281 : : {
282 [ - + ][ - + ]: 1649 : Assert(!d_str.empty());
[ - - ]
283 : 1649 : return d_str.back();
284 : : }
285 : :
286 : 9762 : std::size_t String::overlap(const String& y) const
287 : : {
288 [ + + ]: 9762 : std::size_t i = size() < y.size() ? size() : y.size();
289 [ + + ]: 18923 : for (; i > 0; i--)
290 : : {
291 : 11630 : String s = suffix(i);
292 : 11630 : String p = y.prefix(i);
293 [ + + ]: 11630 : if (s == p)
294 : : {
295 : 2469 : return i;
296 : : }
297 [ + + ][ + + ]: 14099 : }
298 : 7293 : return i;
299 : : }
300 : :
301 : 3887 : std::size_t String::roverlap(const String& y) const
302 : : {
303 [ + + ]: 3887 : std::size_t i = size() < y.size() ? size() : y.size();
304 [ + + ]: 5510 : for (; i > 0; i--)
305 : : {
306 : 2676 : String s = prefix(i);
307 : 2676 : String p = y.suffix(i);
308 [ + + ]: 2676 : if (s == p)
309 : : {
310 : 1053 : return i;
311 : : }
312 [ + + ][ + + ]: 3729 : }
313 : 2834 : return i;
314 : : }
315 : :
316 : 72415 : std::string String::toString(bool useEscSequences) const
317 : : {
318 : 72415 : std::stringstream str;
319 [ + + ]: 287080 : for (unsigned int i = 0; i < size(); ++i)
320 : : {
321 : : // we always print backslash as a code point so that it cannot be
322 : : // interpreted as specifying part of a code point, e.g. the string '\' +
323 : : // 'u' + '0' of length three.
324 [ + + ][ + + ]: 214665 : if (isPrintable(d_str[i]) && d_str[i] != '\\' && !useEscSequences)
[ + - ][ + + ]
325 : : {
326 : 213657 : str << static_cast<char>(d_str[i]);
327 : : }
328 : : else
329 : : {
330 : 1008 : std::stringstream ss;
331 : 1008 : ss << std::hex << d_str[i];
332 : 1008 : str << "\\u{" << ss.str() << "}";
333 : 1008 : }
334 : : }
335 : 144830 : return str.str();
336 : 72415 : }
337 : :
338 : 2 : std::wstring String::toWString() const
339 : : {
340 : 2 : std::wstring res(size(), static_cast<wchar_t>(0));
341 [ - + ]: 2 : for (std::size_t i = 0; i < size(); ++i)
342 : : {
343 : 0 : res[i] = static_cast<wchar_t>(d_str[i]);
344 : : }
345 : 2 : return res;
346 : 0 : }
347 : :
348 : 159 : std::u32string String::toU32String() const
349 : : {
350 : 159 : std::u32string res(size(), static_cast<char32_t>(0));
351 [ + + ]: 594 : for (std::size_t i = 0; i < size(); ++i)
352 : : {
353 : 435 : res[i] = static_cast<char32_t>(d_str[i]);
354 : : }
355 : 159 : return res;
356 : 0 : }
357 : :
358 : 391 : bool String::isLeq(const String& y) const
359 : : {
360 [ + + ]: 625 : for (unsigned i = 0; i < size(); ++i)
361 : : {
362 [ + + ]: 503 : if (i >= y.size())
363 : : {
364 : 44 : return false;
365 : : }
366 : 459 : unsigned ci = d_str[i];
367 : 459 : unsigned cyi = y.d_str[i];
368 [ + + ]: 459 : if (ci > cyi)
369 : : {
370 : 97 : return false;
371 : : }
372 [ + + ]: 362 : if (ci < cyi)
373 : : {
374 : 128 : return true;
375 : : }
376 : : }
377 : 122 : return true;
378 : : }
379 : :
380 : 20 : bool String::isRepeated() const
381 : : {
382 [ + - ]: 20 : if (size() > 1)
383 : : {
384 : 20 : unsigned int f = d_str[0];
385 [ + + ]: 34 : for (unsigned i = 1; i < size(); ++i)
386 : : {
387 [ + + ]: 20 : if (f != d_str[i]) return false;
388 : : }
389 : : }
390 : 14 : return true;
391 : : }
392 : :
393 : 18 : bool String::tailcmp(const String& y, int& c) const
394 : : {
395 : 18 : int id_x = size() - 1;
396 : 18 : int id_y = y.size() - 1;
397 [ + - ][ + + ]: 78 : while (id_x >= 0 && id_y >= 0)
398 : : {
399 [ - + ]: 60 : if (d_str[id_x] != y.d_str[id_y])
400 : : {
401 : 0 : c = id_x;
402 : 0 : return false;
403 : : }
404 : 60 : --id_x;
405 : 60 : --id_y;
406 : : }
407 [ - + ]: 18 : c = id_x == -1 ? (-(id_y + 1)) : (id_x + 1);
408 : 18 : return true;
409 : : }
410 : :
411 : 104872 : std::size_t String::find(const String& y, const std::size_t start) const
412 : : {
413 [ + + ]: 104872 : if (size() < y.size() + start) return std::string::npos;
414 [ + + ]: 96624 : if (y.empty()) return start;
415 [ - + ]: 94558 : if (empty()) return std::string::npos;
416 : :
417 : 189116 : std::vector<unsigned>::const_iterator itr = std::search(
418 : 94558 : d_str.begin() + start, d_str.end(), y.d_str.begin(), y.d_str.end());
419 [ + + ]: 94558 : if (itr != d_str.end())
420 : : {
421 : 83191 : return itr - d_str.begin();
422 : : }
423 : 11367 : return std::string::npos;
424 : : }
425 : :
426 : 16406 : std::size_t String::rfind(const String& y, const std::size_t start) const
427 : : {
428 [ + + ]: 16406 : if (size() < y.size() + start) return std::string::npos;
429 [ + + ]: 12822 : if (y.empty()) return start;
430 [ - + ]: 12821 : if (empty()) return std::string::npos;
431 : :
432 : : std::vector<unsigned>::const_reverse_iterator itr = std::search(
433 : 12821 : d_str.rbegin() + start, d_str.rend(), y.d_str.rbegin(), y.d_str.rend());
434 [ + + ]: 12821 : if (itr != d_str.rend())
435 : : {
436 : 10507 : return itr - d_str.rbegin();
437 : : }
438 : 2314 : return std::string::npos;
439 : : }
440 : :
441 : 7294 : bool String::hasPrefix(const String& y) const
442 : : {
443 : 7294 : size_t s = size();
444 : 7294 : size_t ys = y.size();
445 [ + + ]: 7294 : if (ys > s)
446 : : {
447 : 1 : return false;
448 : : }
449 [ + + ]: 20702 : for (size_t i = 0; i < ys; i++)
450 : : {
451 [ + + ]: 13486 : if (d_str[i] != y.d_str[i])
452 : : {
453 : 77 : return false;
454 : : }
455 : : }
456 : 7216 : return true;
457 : : }
458 : :
459 : 18812 : bool String::hasSuffix(const String& y) const
460 : : {
461 : 18812 : size_t s = size();
462 : 18812 : size_t ys = y.size();
463 [ + + ]: 18812 : if (ys > s)
464 : : {
465 : 1 : return false;
466 : : }
467 : 18811 : size_t idiff = s - ys;
468 [ + + ]: 48905 : for (size_t i = 0; i < ys; i++)
469 : : {
470 [ + + ]: 30239 : if (d_str[i + idiff] != y.d_str[i])
471 : : {
472 : 145 : return false;
473 : : }
474 : : }
475 : 18666 : return true;
476 : : }
477 : :
478 : 170 : String String::update(std::size_t i, const String& t) const
479 : : {
480 [ + - ]: 170 : if (i < size())
481 : : {
482 : 170 : std::vector<unsigned> vec(d_str.begin(), d_str.begin() + i);
483 : 170 : size_t remNum = size() - i;
484 : 170 : size_t tnum = t.d_str.size();
485 [ + + ]: 170 : if (tnum >= remNum)
486 : : {
487 : 61 : vec.insert(vec.end(), t.d_str.begin(), t.d_str.begin() + remNum);
488 : : }
489 : : else
490 : : {
491 : 109 : vec.insert(vec.end(), t.d_str.begin(), t.d_str.end());
492 : 109 : vec.insert(vec.end(), d_str.begin() + i + tnum, d_str.end());
493 : : }
494 : 170 : return String(vec);
495 : 170 : }
496 : 0 : return *this;
497 : : }
498 : :
499 : 275 : String String::replace(const String& s, const String& t) const
500 : : {
501 : 275 : std::size_t ret = find(s);
502 [ + + ]: 275 : if (ret != std::string::npos)
503 : : {
504 : 190 : std::vector<unsigned> vec;
505 : 190 : vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret);
506 : 190 : vec.insert(vec.end(), t.d_str.begin(), t.d_str.end());
507 : 190 : vec.insert(vec.end(), d_str.begin() + ret + s.size(), d_str.end());
508 : 190 : return String(vec);
509 : 190 : }
510 : : else
511 : : {
512 : 85 : return *this;
513 : : }
514 : : }
515 : :
516 : 16565 : String String::substr(std::size_t i) const
517 : : {
518 [ - + ][ - + ]: 16565 : Assert(i <= size());
[ - - ]
519 : 16565 : std::vector<unsigned> ret_vec;
520 : 16565 : std::vector<unsigned>::const_iterator itr = d_str.begin() + i;
521 : 16565 : ret_vec.insert(ret_vec.end(), itr, d_str.end());
522 : 33130 : return String(ret_vec);
523 : 16565 : }
524 : :
525 : 171813 : String String::substr(std::size_t i, std::size_t j) const
526 : : {
527 [ - + ][ - + ]: 171813 : Assert(i + j <= size());
[ - - ]
528 : 171813 : std::vector<unsigned> ret_vec;
529 : 171813 : std::vector<unsigned>::const_iterator itr = d_str.begin() + i;
530 : 171813 : ret_vec.insert(ret_vec.end(), itr, itr + j);
531 : 343626 : return String(ret_vec);
532 : 171813 : }
533 : :
534 : 1571 : bool String::isNumber() const
535 : : {
536 [ + + ]: 1571 : if (d_str.empty())
537 : : {
538 : 95 : return false;
539 : : }
540 [ + + ]: 3647 : for (unsigned character : d_str)
541 : : {
542 [ + + ]: 2403 : if (!isDigit(character))
543 : : {
544 : 232 : return false;
545 : : }
546 : : }
547 : 1244 : return true;
548 : : }
549 : :
550 : 9697 : bool String::isDigit(unsigned character)
551 : : {
552 : : // '0' to '9'
553 [ + + ][ + + ]: 9697 : return 48 <= character && character <= 57;
554 : : }
555 : :
556 : 7185 : bool String::isHexDigit(unsigned character)
557 : : {
558 : : // '0' to '9' or 'A' to 'F' or 'a' to 'f'
559 [ + - ][ + + ]: 8579 : return isDigit(character) || (65 <= character && character <= 70)
560 [ + + ][ + + ]: 8579 : || (97 <= character && character <= 102);
[ + + ]
561 : : }
562 : :
563 : 214665 : bool String::isPrintable(unsigned character)
564 : : {
565 : : // Unicode 0x00020 (' ') to 0x0007E ('~')
566 [ + + ][ + + ]: 214665 : return 32 <= character && character <= 126;
567 : : }
568 : :
569 : 15818 : size_t String::maxSize() { return std::numeric_limits<uint32_t>::max(); }
570 : :
571 : 252 : Rational String::toNumber() const
572 : : {
573 : : // when smt2 standard for strings is set, this may change, based on the
574 : : // semantics of str.from.int for leading zeros
575 : 504 : return Rational(toString());
576 : : }
577 : :
578 : : namespace strings {
579 : :
580 : 5809568 : size_t StringHashFunction::operator()(const cvc5::internal::String& s) const
581 : : {
582 : 5809568 : uint64_t ret = fnv1a::offsetBasis;
583 [ + + ]: 9199828 : for (unsigned c : s.d_str)
584 : : {
585 : 3390260 : ret = fnv1a::fnv1a_64(c, ret);
586 : : }
587 : 5809568 : return static_cast<size_t>(ret);
588 : : }
589 : :
590 : : } // namespace strings
591 : :
592 : 0 : std::ostream& operator<<(std::ostream& os, const String& s)
593 : : {
594 : 0 : return os << "\"" << s.toString() << "\"";
595 : : }
596 : :
597 : : } // namespace cvc5::internal
|
