Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of utility functions for words.
14 : : */
15 : :
16 : : #include "theory/strings/word.h"
17 : :
18 : : #include "expr/sequence.h"
19 : : #include "util/string.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace strings {
26 : :
27 : 2185770 : Node Word::mkEmptyWord(TypeNode tn)
28 : : {
29 [ + + ]: 2185770 : if (tn.isString())
30 : : {
31 : 2096970 : std::vector<unsigned> vec;
32 : 4193940 : return NodeManager::currentNM()->mkConst(String(vec));
33 : : }
34 [ + - ]: 88801 : else if (tn.isSequence())
35 : : {
36 : 88801 : std::vector<Node> seq;
37 : : return NodeManager::currentNM()->mkConst(
38 : 177602 : Sequence(tn.getSequenceElementType(), seq));
39 : : }
40 : 0 : Unimplemented();
41 : : return Node::null();
42 : : }
43 : :
44 : 82025 : Node Word::mkWordFlatten(const std::vector<Node>& xs)
45 : : {
46 [ - + ][ - + ]: 82025 : Assert(!xs.empty());
[ - - ]
47 : 82025 : NodeManager* nm = NodeManager::currentNM();
48 : 82025 : Kind k = xs[0].getKind();
49 [ + + ]: 82025 : if (k == Kind::CONST_STRING)
50 : : {
51 : 80400 : std::vector<unsigned> vec;
52 [ + + ]: 222129 : for (TNode x : xs)
53 : : {
54 [ - + ][ - + ]: 141729 : Assert(x.getKind() == Kind::CONST_STRING);
[ - - ]
55 : 141729 : String sx = x.getConst<String>();
56 : 141729 : const std::vector<unsigned>& vecc = sx.getVec();
57 : 141729 : vec.insert(vec.end(), vecc.begin(), vecc.end());
58 : : }
59 : 160800 : return nm->mkConst(String(vec));
60 : : }
61 [ + - ]: 1625 : else if (k == Kind::CONST_SEQUENCE)
62 : : {
63 : 3250 : std::vector<Node> seq;
64 : 1625 : TypeNode tn = xs[0].getType();
65 [ + + ]: 4295 : for (TNode x : xs)
66 : : {
67 [ - + ][ - + ]: 2670 : Assert(x.getType() == tn);
[ - - ]
68 : 2670 : const Sequence& sx = x.getConst<Sequence>();
69 : 2670 : const std::vector<Node>& vecc = sx.getVec();
70 : 2670 : seq.insert(seq.end(), vecc.begin(), vecc.end());
71 : : }
72 : : return NodeManager::currentNM()->mkConst(
73 : 3250 : Sequence(tn.getSequenceElementType(), seq));
74 : : }
75 : 0 : Unimplemented();
76 : : return Node::null();
77 : : }
78 : :
79 : 1395120 : size_t Word::getLength(TNode x)
80 : : {
81 : 1395120 : Kind k = x.getKind();
82 [ + + ]: 1395120 : if (k == Kind::CONST_STRING)
83 : : {
84 : 1372850 : return x.getConst<String>().size();
85 : : }
86 [ + - ]: 22266 : else if (k == Kind::CONST_SEQUENCE)
87 : : {
88 : 22266 : return x.getConst<Sequence>().size();
89 : : }
90 : 0 : Unimplemented() << "Word::getLength on " << x;
91 : : return 0;
92 : : }
93 : :
94 : 196461 : std::vector<Node> Word::getChars(TNode x)
95 : : {
96 : 196461 : Kind k = x.getKind();
97 : 196461 : std::vector<Node> ret;
98 : 196461 : NodeManager* nm = NodeManager::currentNM();
99 [ + + ]: 196461 : if (k == Kind::CONST_STRING)
100 : : {
101 : 384460 : std::vector<unsigned> ccVec;
102 : 192230 : const std::vector<unsigned>& cvec = x.getConst<String>().getVec();
103 [ + + ]: 501912 : for (unsigned chVal : cvec)
104 : : {
105 : 309682 : ccVec.clear();
106 : 309682 : ccVec.push_back(chVal);
107 : 619364 : Node ch = nm->mkConst(String(ccVec));
108 : 309682 : ret.push_back(ch);
109 : : }
110 : 192230 : return ret;
111 : : }
112 [ + - ]: 4231 : else if (k == Kind::CONST_SEQUENCE)
113 : : {
114 : 8462 : TypeNode t = x.getConst<Sequence>().getType();
115 : 4231 : const Sequence& sx = x.getConst<Sequence>();
116 : 4231 : const std::vector<Node>& vec = sx.getVec();
117 [ + + ]: 8211 : for (const Node& v : vec)
118 : : {
119 : 7960 : ret.push_back(nm->mkConst(Sequence(t, {v})));
120 : : }
121 : 4231 : return ret;
122 : : }
123 : 0 : Unimplemented();
124 : : return ret;
125 : : }
126 : :
127 : 1194 : Node Word::getNth(TNode x, size_t n)
128 : : {
129 : 1194 : Kind k = x.getKind();
130 [ + + ]: 1194 : if (k == Kind::CONST_STRING)
131 : : {
132 : 92 : const std::vector<unsigned>& vec = x.getConst<String>().getVec();
133 [ - + ][ - + ]: 92 : Assert(n < vec.size());
[ - - ]
134 : 92 : return NodeManager::currentNM()->mkConstInt(vec[n]);
135 : : }
136 [ + - ]: 1102 : else if (k == Kind::CONST_SEQUENCE)
137 : : {
138 : 1102 : const std::vector<Node>& vec = x.getConst<Sequence>().getVec();
139 [ - + ][ - + ]: 1102 : Assert(n < vec.size());
[ - - ]
140 : 1102 : return vec[n];
141 : : }
142 : 0 : Unimplemented();
143 : : return Node::null();
144 : : }
145 : :
146 [ + + ][ + + ]: 414414 : bool Word::isEmpty(TNode x) { return x.isConst() && getLength(x) == 0; }
[ + + ][ - - ]
147 : :
148 : 27480 : bool Word::strncmp(TNode x, TNode y, std::size_t n)
149 : : {
150 : 27480 : Kind k = x.getKind();
151 [ + + ]: 27480 : if (k == Kind::CONST_STRING)
152 : : {
153 [ - + ][ - + ]: 27441 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
154 : 54882 : String sx = x.getConst<String>();
155 : 54882 : String sy = y.getConst<String>();
156 : 27441 : return sx.strncmp(sy, n);
157 : : }
158 [ + - ]: 39 : else if (k == Kind::CONST_SEQUENCE)
159 : : {
160 [ - + ][ - + ]: 39 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
161 : 39 : const Sequence& sx = x.getConst<Sequence>();
162 : 39 : const Sequence& sy = y.getConst<Sequence>();
163 : 39 : return sx.strncmp(sy, n);
164 : : }
165 : 0 : Unimplemented();
166 : : return false;
167 : : }
168 : :
169 : 26199 : bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
170 : : {
171 : 26199 : Kind k = x.getKind();
172 [ + + ]: 26199 : if (k == Kind::CONST_STRING)
173 : : {
174 [ - + ][ - + ]: 26054 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
175 : 52108 : String sx = x.getConst<String>();
176 : 52108 : String sy = y.getConst<String>();
177 : 26054 : return sx.rstrncmp(sy, n);
178 : : }
179 [ + - ]: 145 : else if (k == Kind::CONST_SEQUENCE)
180 : : {
181 [ - + ][ - + ]: 145 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
182 : 145 : const Sequence& sx = x.getConst<Sequence>();
183 : 145 : const Sequence& sy = y.getConst<Sequence>();
184 : 145 : return sx.rstrncmp(sy, n);
185 : : }
186 : 0 : Unimplemented();
187 : : return false;
188 : : }
189 : :
190 : 85518 : std::size_t Word::find(TNode x, TNode y, std::size_t start)
191 : : {
192 : 85518 : Kind k = x.getKind();
193 [ + + ]: 85518 : if (k == Kind::CONST_STRING)
194 : : {
195 [ - + ][ - + ]: 83485 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
196 : 166970 : String sx = x.getConst<String>();
197 : 166970 : String sy = y.getConst<String>();
198 : 83485 : return sx.find(sy, start);
199 : : }
200 [ + - ]: 2033 : else if (k == Kind::CONST_SEQUENCE)
201 : : {
202 [ - + ][ - + ]: 2033 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
203 : 2033 : const Sequence& sx = x.getConst<Sequence>();
204 : 2033 : const Sequence& sy = y.getConst<Sequence>();
205 : 2033 : return sx.find(sy, start);
206 : : }
207 : 0 : Unimplemented();
208 : : return 0;
209 : : }
210 : :
211 : 12414 : std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
212 : : {
213 : 12414 : Kind k = x.getKind();
214 [ + + ]: 12414 : if (k == Kind::CONST_STRING)
215 : : {
216 [ - + ][ - + ]: 12176 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
217 : 24352 : String sx = x.getConst<String>();
218 : 24352 : String sy = y.getConst<String>();
219 : 12176 : return sx.rfind(sy, start);
220 : : }
221 [ + - ]: 238 : else if (k == Kind::CONST_SEQUENCE)
222 : : {
223 [ - + ][ - + ]: 238 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
224 : 238 : const Sequence& sx = x.getConst<Sequence>();
225 : 238 : const Sequence& sy = y.getConst<Sequence>();
226 : 238 : return sx.rfind(sy, start);
227 : : }
228 : 0 : Unimplemented();
229 : : return 0;
230 : : }
231 : :
232 : 5456 : bool Word::hasPrefix(TNode x, TNode y)
233 : : {
234 : 5456 : Kind k = x.getKind();
235 [ + + ]: 5456 : if (k == Kind::CONST_STRING)
236 : : {
237 [ - + ][ - + ]: 5448 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
238 : 10896 : String sx = x.getConst<String>();
239 : 10896 : String sy = y.getConst<String>();
240 : 5448 : return sx.hasPrefix(sy);
241 : : }
242 [ + - ]: 8 : else if (k == Kind::CONST_SEQUENCE)
243 : : {
244 [ - + ][ - + ]: 8 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
245 : 8 : const Sequence& sx = x.getConst<Sequence>();
246 : 8 : const Sequence& sy = y.getConst<Sequence>();
247 : 8 : return sx.hasPrefix(sy);
248 : : }
249 : 0 : Unimplemented();
250 : : return false;
251 : : }
252 : :
253 : 17788 : bool Word::hasSuffix(TNode x, TNode y)
254 : : {
255 : 17788 : Kind k = x.getKind();
256 [ + + ]: 17788 : if (k == Kind::CONST_STRING)
257 : : {
258 [ - + ][ - + ]: 17556 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
259 : 35112 : String sx = x.getConst<String>();
260 : 35112 : String sy = y.getConst<String>();
261 : 17556 : return sx.hasSuffix(sy);
262 : : }
263 [ + - ]: 232 : else if (k == Kind::CONST_SEQUENCE)
264 : : {
265 [ - + ][ - + ]: 232 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
266 : 232 : const Sequence& sx = x.getConst<Sequence>();
267 : 232 : const Sequence& sy = y.getConst<Sequence>();
268 : 232 : return sx.hasSuffix(sy);
269 : : }
270 : 0 : Unimplemented();
271 : : return false;
272 : : }
273 : :
274 : 153 : Node Word::update(TNode x, std::size_t i, TNode t)
275 : : {
276 : 153 : NodeManager* nm = NodeManager::currentNM();
277 : 153 : Kind k = x.getKind();
278 [ + + ]: 153 : if (k == Kind::CONST_STRING)
279 : : {
280 [ - + ][ - + ]: 111 : Assert(t.getKind() == Kind::CONST_STRING);
[ - - ]
281 : 222 : String sx = x.getConst<String>();
282 : 111 : String st = t.getConst<String>();
283 : 222 : return nm->mkConst(String(sx.update(i, st)));
284 : : }
285 [ + - ]: 42 : else if (k == Kind::CONST_SEQUENCE)
286 : : {
287 [ - + ][ - + ]: 42 : Assert(t.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
288 : 42 : const Sequence& sx = x.getConst<Sequence>();
289 : 42 : const Sequence& st = t.getConst<Sequence>();
290 : 84 : Sequence res = sx.update(i, st);
291 : 42 : return nm->mkConst(res);
292 : : }
293 : 0 : Unimplemented();
294 : : return Node::null();
295 : : }
296 : 3 : Node Word::replace(TNode x, TNode y, TNode t)
297 : : {
298 : 3 : NodeManager* nm = NodeManager::currentNM();
299 : 3 : Kind k = x.getKind();
300 [ + - ]: 3 : if (k == Kind::CONST_STRING)
301 : : {
302 [ - + ][ - + ]: 3 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
303 [ - + ][ - + ]: 3 : Assert(t.getKind() == Kind::CONST_STRING);
[ - - ]
304 : 6 : String sx = x.getConst<String>();
305 : 6 : String sy = y.getConst<String>();
306 : 3 : String st = t.getConst<String>();
307 : 6 : return nm->mkConst(String(sx.replace(sy, st)));
308 : : }
309 [ - - ]: 0 : else if (k == Kind::CONST_SEQUENCE)
310 : : {
311 : 0 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
312 : 0 : Assert(t.getKind() == Kind::CONST_SEQUENCE);
313 : 0 : const Sequence& sx = x.getConst<Sequence>();
314 : 0 : const Sequence& sy = y.getConst<Sequence>();
315 : 0 : const Sequence& st = t.getConst<Sequence>();
316 : 0 : Sequence res = sx.replace(sy, st);
317 : 0 : return nm->mkConst(res);
318 : : }
319 : 0 : Unimplemented();
320 : : return Node::null();
321 : : }
322 : 9174 : Node Word::substr(TNode x, std::size_t i)
323 : : {
324 : 9174 : NodeManager* nm = NodeManager::currentNM();
325 : 9174 : Kind k = x.getKind();
326 [ + + ]: 9174 : if (k == Kind::CONST_STRING)
327 : : {
328 : 9129 : String sx = x.getConst<String>();
329 : 18258 : return nm->mkConst(String(sx.substr(i)));
330 : : }
331 [ + - ]: 45 : else if (k == Kind::CONST_SEQUENCE)
332 : : {
333 : 45 : const Sequence& sx = x.getConst<Sequence>();
334 : 90 : Sequence res = sx.substr(i);
335 : 45 : return nm->mkConst(res);
336 : : }
337 : 0 : Unimplemented();
338 : : return Node::null();
339 : : }
340 : 57533 : Node Word::substr(TNode x, std::size_t i, std::size_t j)
341 : : {
342 : 57533 : NodeManager* nm = NodeManager::currentNM();
343 : 57533 : Kind k = x.getKind();
344 [ + + ]: 57533 : if (k == Kind::CONST_STRING)
345 : : {
346 : 57238 : String sx = x.getConst<String>();
347 : 114476 : return nm->mkConst(String(sx.substr(i, j)));
348 : : }
349 [ + - ]: 295 : else if (k == Kind::CONST_SEQUENCE)
350 : : {
351 : 295 : const Sequence& sx = x.getConst<Sequence>();
352 : 590 : Sequence res = sx.substr(i, j);
353 : 295 : return nm->mkConst(res);
354 : : }
355 : 0 : Unimplemented();
356 : : return Node::null();
357 : : }
358 : :
359 : 20281 : Node Word::prefix(TNode x, std::size_t i) { return substr(x, 0, i); }
360 : :
361 : 27733 : Node Word::suffix(TNode x, std::size_t i)
362 : : {
363 : 27733 : NodeManager* nm = NodeManager::currentNM();
364 : 27733 : Kind k = x.getKind();
365 [ + + ]: 27733 : if (k == Kind::CONST_STRING)
366 : : {
367 : 27687 : String sx = x.getConst<String>();
368 : 55374 : return nm->mkConst(String(sx.suffix(i)));
369 : : }
370 [ + - ]: 46 : else if (k == Kind::CONST_SEQUENCE)
371 : : {
372 : 46 : const Sequence& sx = x.getConst<Sequence>();
373 : 92 : Sequence res = sx.suffix(i);
374 : 46 : return nm->mkConst(res);
375 : : }
376 : 0 : Unimplemented();
377 : : return Node::null();
378 : : }
379 : :
380 : 2191 : bool Word::noOverlapWith(TNode x, TNode y)
381 : : {
382 : 2191 : Kind k = x.getKind();
383 [ + + ]: 2191 : if (k == Kind::CONST_STRING)
384 : : {
385 [ - + ][ - + ]: 2183 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
386 : 4366 : String sx = x.getConst<String>();
387 : 4366 : String sy = y.getConst<String>();
388 : 2183 : return sx.noOverlapWith(sy);
389 : : }
390 [ + - ]: 8 : else if (k == Kind::CONST_SEQUENCE)
391 : : {
392 [ - + ][ - + ]: 8 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
393 : 8 : const Sequence& sx = x.getConst<Sequence>();
394 : 8 : const Sequence& sy = y.getConst<Sequence>();
395 : 8 : return sx.noOverlapWith(sy);
396 : : }
397 : 0 : Unimplemented();
398 : : return false;
399 : : }
400 : :
401 : 5127 : std::size_t Word::overlap(TNode x, TNode y)
402 : : {
403 : 5127 : Kind k = x.getKind();
404 [ + + ]: 5127 : if (k == Kind::CONST_STRING)
405 : : {
406 [ - + ][ - + ]: 5074 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
407 : 10148 : String sx = x.getConst<String>();
408 : 10148 : String sy = y.getConst<String>();
409 : 5074 : return sx.overlap(sy);
410 : : }
411 [ + - ]: 53 : else if (k == Kind::CONST_SEQUENCE)
412 : : {
413 [ - + ][ - + ]: 53 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
414 : 53 : const Sequence& sx = x.getConst<Sequence>();
415 : 53 : const Sequence& sy = y.getConst<Sequence>();
416 : 53 : return sx.overlap(sy);
417 : : }
418 : 0 : Unimplemented();
419 : : return 0;
420 : : }
421 : :
422 : 3164 : std::size_t Word::roverlap(TNode x, TNode y)
423 : : {
424 : 3164 : Kind k = x.getKind();
425 [ + + ]: 3164 : if (k == Kind::CONST_STRING)
426 : : {
427 [ - + ][ - + ]: 3142 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
428 : 6284 : String sx = x.getConst<String>();
429 : 6284 : String sy = y.getConst<String>();
430 : 3142 : return sx.roverlap(sy);
431 : : }
432 [ + - ]: 22 : else if (k == Kind::CONST_SEQUENCE)
433 : : {
434 [ - + ][ - + ]: 22 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
435 : 22 : const Sequence& sx = x.getConst<Sequence>();
436 : 22 : const Sequence& sy = y.getConst<Sequence>();
437 : 22 : return sx.roverlap(sy);
438 : : }
439 : 0 : Unimplemented();
440 : : return 0;
441 : : }
442 : :
443 : 0 : bool Word::isRepeated(TNode x)
444 : : {
445 : 0 : Kind k = x.getKind();
446 [ - - ]: 0 : if (k == Kind::CONST_STRING)
447 : : {
448 : 0 : return x.getConst<String>().isRepeated();
449 : : }
450 [ - - ]: 0 : else if (k == Kind::CONST_SEQUENCE)
451 : : {
452 : 0 : return x.getConst<Sequence>().isRepeated();
453 : : }
454 : 0 : Unimplemented();
455 : : return false;
456 : : }
457 : :
458 : 14804 : Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
459 : : {
460 [ + - ][ + - ]: 29608 : Assert(x.isConst() && y.isConst());
[ - + ][ - - ]
461 : 14804 : size_t lenA = getLength(x);
462 : 14804 : size_t lenB = getLength(y);
463 [ + + ]: 14804 : index = lenA <= lenB ? 1 : 0;
464 [ + + ]: 14804 : size_t lenShort = index == 1 ? lenA : lenB;
465 : 14804 : bool cmp = isRev ? rstrncmp(x, y, lenShort) : strncmp(x, y, lenShort);
466 [ + + ]: 14804 : if (cmp)
467 : : {
468 [ + + ]: 19356 : Node l = index == 0 ? x : y;
469 [ + + ]: 9678 : if (isRev)
470 : : {
471 : 5440 : size_t new_len = getLength(l) - lenShort;
472 : 5440 : return substr(l, 0, new_len);
473 : : }
474 : : else
475 : : {
476 : 4238 : return substr(l, lenShort);
477 : : }
478 : : }
479 : : // not the same prefix/suffix
480 : 5126 : return Node::null();
481 : : }
482 : :
483 : 162 : Node Word::reverse(TNode x)
484 : : {
485 : 162 : NodeManager* nm = NodeManager::currentNM();
486 : 162 : Kind k = x.getKind();
487 [ + + ]: 162 : if (k == Kind::CONST_STRING)
488 : : {
489 : 258 : String sx = x.getConst<String>();
490 : 129 : std::vector<unsigned> nvec = sx.getVec();
491 : 129 : std::reverse(nvec.begin(), nvec.end());
492 : 258 : return nm->mkConst(String(nvec));
493 : : }
494 [ + - ]: 33 : else if (k == Kind::CONST_SEQUENCE)
495 : : {
496 : 33 : const Sequence& sx = x.getConst<Sequence>();
497 : 33 : const std::vector<Node>& vecc = sx.getVec();
498 : 66 : std::vector<Node> vecr(vecc.begin(), vecc.end());
499 : 33 : std::reverse(vecr.begin(), vecr.end());
500 : 66 : Sequence res(sx.getType(), vecr);
501 : 33 : return nm->mkConst(res);
502 : : }
503 : 0 : Unimplemented();
504 : : return Node::null();
505 : : }
506 : :
507 : : } // namespace strings
508 : : } // namespace theory
509 : : } // namespace cvc5::internal
|
