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 entailment tests involving strings.
11 : : */
12 : :
13 : : #include "theory/strings/strings_entail.h"
14 : :
15 : : #include "expr/node_builder.h"
16 : : #include "theory/rewriter.h"
17 : : #include "theory/strings/arith_entail.h"
18 : : #include "theory/strings/sequences_rewriter.h"
19 : : #include "theory/strings/theory_strings_utils.h"
20 : : #include "theory/strings/word.h"
21 : : #include "util/rational.h"
22 : : #include "util/string.h"
23 : :
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace strings {
29 : :
30 : 70235 : StringsEntail::StringsEntail(Rewriter* r, ArithEntail& aent)
31 : 70235 : : d_rr(r), d_arithEntail(aent)
32 : : {
33 : 70235 : }
34 : :
35 : 0 : bool StringsEntail::canConstantContainConcat(Node c,
36 : : Node n,
37 : : int& firstc,
38 : : int& lastc)
39 : : {
40 : 0 : Assert(c.isConst());
41 : 0 : Assert(n.getKind() == Kind::STRING_CONCAT);
42 : : // must find constant components in order
43 : 0 : size_t pos = 0;
44 : 0 : firstc = -1;
45 : 0 : lastc = -1;
46 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
47 : : {
48 [ - - ]: 0 : if (n[i].isConst())
49 : : {
50 [ - - ]: 0 : firstc = firstc == -1 ? i : firstc;
51 : 0 : lastc = i;
52 : 0 : size_t new_pos = Word::find(c, n[i], pos);
53 [ - - ]: 0 : if (new_pos == std::string::npos)
54 : : {
55 : 0 : return false;
56 : : }
57 : : else
58 : : {
59 : 0 : pos = new_pos + Word::getLength(n[i]);
60 : : }
61 : : }
62 [ - - ][ - - ]: 0 : else if (n[i].getKind() == Kind::STRING_ITOS
63 : 0 : && d_arithEntail.check(n[i][0]))
64 : : {
65 : 0 : Assert(c.getType().isString()); // string-only
66 : 0 : const std::vector<unsigned>& tvec = c.getConst<String>().getVec();
67 : : // find the first occurrence of a digit starting at pos
68 [ - - ][ - - ]: 0 : while (pos < tvec.size() && !String::isDigit(tvec[pos]))
[ - - ]
69 : : {
70 : 0 : pos++;
71 : : }
72 [ - - ]: 0 : if (pos == tvec.size())
73 : : {
74 : 0 : return false;
75 : : }
76 : : // must consume at least one digit here
77 : 0 : pos++;
78 : : }
79 : : }
80 : 0 : return true;
81 : : }
82 : :
83 : 42815 : bool StringsEntail::canConstantContainList(Node c,
84 : : std::vector<Node>& l,
85 : : int& firstc,
86 : : int& lastc)
87 : : {
88 [ - + ][ - + ]: 42815 : Assert(c.isConst());
[ - - ]
89 : : // must find constant components in order
90 : 42815 : size_t pos = 0;
91 : 42815 : firstc = -1;
92 : 42815 : lastc = -1;
93 [ + + ]: 125841 : for (unsigned i = 0; i < l.size(); i++)
94 : : {
95 [ + + ]: 84079 : if (l[i].isConst())
96 : : {
97 [ + + ]: 70887 : firstc = firstc == -1 ? i : firstc;
98 : 70887 : lastc = i;
99 : 70887 : size_t new_pos = Word::find(c, l[i], pos);
100 [ + + ]: 70887 : if (new_pos == std::string::npos)
101 : : {
102 : 1053 : return false;
103 : : }
104 : : else
105 : : {
106 : 69834 : pos = new_pos + Word::getLength(l[i]);
107 : : }
108 : : }
109 : : }
110 : 41762 : return true;
111 : : }
112 : :
113 : 238632 : bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
114 : : std::vector<Node>& nr,
115 : : int dir,
116 : : Node& curr,
117 : : bool strict)
118 : : {
119 [ + + ][ + - ]: 238632 : Assert(dir == 1 || dir == -1);
[ - + ][ - + ]
[ - - ]
120 [ - + ][ - + ]: 238632 : Assert(nr.empty());
[ - - ]
121 : 238632 : NodeManager* nm = curr.getNodeManager();
122 : 238632 : Node zero = nm->mkConstInt(cvc5::internal::Rational(0));
123 : 238632 : bool ret = false;
124 : 238632 : bool success = true;
125 : 238632 : unsigned sindex = 0;
126 [ + + ][ + + ]: 441989 : while (success && curr != zero && sindex < n1.size())
[ + + ][ + + ]
127 : : {
128 [ - + ][ - + ]: 203357 : Assert(!curr.isNull());
[ - - ]
129 : 203357 : success = false;
130 [ + + ]: 203357 : unsigned sindex_use = dir == 1 ? sindex : ((n1.size() - 1) - sindex);
131 [ + + ]: 203357 : if (n1[sindex_use].isConst())
132 : : {
133 : : // could strip part of a constant
134 : : Node lowerBound =
135 : 90134 : d_arithEntail.getConstantBound(d_arithEntail.rewriteArith(curr));
136 [ + + ]: 45067 : if (!lowerBound.isNull())
137 : : {
138 [ - + ][ - + ]: 9454 : Assert(lowerBound.isConst());
[ - - ]
139 : 9454 : Rational lbr = lowerBound.getConst<Rational>();
140 [ + + ]: 9454 : if (lbr.sgn() > 0)
141 : : {
142 [ - + ][ - + ]: 3882 : Assert(d_arithEntail.check(curr, true));
[ - - ]
143 : 3882 : Node s = n1[sindex_use];
144 : 3882 : size_t slen = Word::getLength(s);
145 : 3882 : Node ncl = nm->mkConstInt(cvc5::internal::Rational(slen));
146 : 7764 : Node next_s = nm->mkNode(Kind::SUB, lowerBound, ncl);
147 : 3882 : next_s = d_arithEntail.rewriteArith(next_s);
148 [ - + ][ - + ]: 3882 : Assert(next_s.isConst());
[ - - ]
149 : : // we can remove the entire constant
150 [ + + ]: 3882 : if (next_s.getConst<Rational>().sgn() >= 0)
151 : : {
152 : 1807 : curr = d_arithEntail.rewriteArith(nm->mkNode(Kind::SUB, curr, ncl));
153 : 1807 : success = true;
154 : 1807 : sindex++;
155 : : }
156 : : else
157 : : {
158 : : // we can remove part of the constant
159 : : // lower bound minus the length of a concrete string is negative,
160 : : // hence lowerBound cannot be larger than long max
161 [ - + ][ - + ]: 2075 : Assert(lbr < Rational(String::maxSize()));
[ - - ]
162 : 4150 : curr = d_arithEntail.rewriteArith(
163 : 6225 : nm->mkNode(Kind::SUB, curr, lowerBound));
164 : 2075 : uint32_t lbsize = lbr.getNumerator().toUnsignedInt();
165 [ - + ][ - + ]: 2075 : Assert(lbsize < slen);
[ - - ]
166 [ + + ]: 2075 : if (dir == 1)
167 : : {
168 : : // strip partially from the front
169 : 1845 : nr.push_back(Word::prefix(s, lbsize));
170 : 1845 : n1[sindex_use] = Word::suffix(s, slen - lbsize);
171 : : }
172 : : else
173 : : {
174 : : // strip partially from the back
175 : 230 : nr.push_back(Word::suffix(s, lbsize));
176 : 230 : n1[sindex_use] = Word::prefix(s, slen - lbsize);
177 : : }
178 : 2075 : ret = true;
179 : : }
180 [ - + ][ - + ]: 3882 : Assert(d_arithEntail.check(curr));
[ - - ]
181 : 3882 : }
182 : : else
183 : : {
184 : : // we cannot remove the constant
185 : : }
186 : 9454 : }
187 : 45067 : }
188 : : else
189 : : {
190 : : Node next_s = NodeManager::mkNode(
191 : : Kind::SUB,
192 : : curr,
193 : 316580 : NodeManager::mkNode(Kind::STRING_LENGTH, n1[sindex_use]));
194 : 158290 : next_s = d_arithEntail.rewriteArith(next_s);
195 [ + + ]: 158290 : if (d_arithEntail.check(next_s))
196 : : {
197 : 1993 : success = true;
198 : 1993 : curr = next_s;
199 : 1993 : sindex++;
200 : : }
201 : 158290 : }
202 : : }
203 [ + + ][ + + ]: 238632 : if (strict && curr != zero)
[ + + ]
204 : : {
205 : : // return false if we did not strip the entire length
206 : 10309 : ret = false;
207 : : }
208 [ + + ]: 228323 : else if (sindex > 0)
209 : : {
210 [ + + ]: 3378 : if (dir == 1)
211 : : {
212 : 3046 : nr.insert(nr.begin(), n1.begin(), n1.begin() + sindex);
213 : 3046 : n1.erase(n1.begin(), n1.begin() + sindex);
214 : : }
215 : : else
216 : : {
217 : 332 : nr.insert(nr.end(), n1.end() - sindex, n1.end());
218 : 332 : n1.erase(n1.end() - sindex, n1.end());
219 : : }
220 : 3378 : ret = true;
221 : : }
222 : 238632 : return ret;
223 : 238632 : }
224 : :
225 : 222090 : int StringsEntail::componentContains(std::vector<Node>& n1,
226 : : std::vector<Node>& n2,
227 : : std::vector<Node>& nb,
228 : : std::vector<Node>& ne,
229 : : bool computeRemainder,
230 : : int remainderDir)
231 : : {
232 : 222090 : return componentContainsInternal(
233 : 222090 : false, n1, n2, nb, ne, computeRemainder, remainderDir);
234 : : }
235 : :
236 : 5099 : int StringsEntail::componentContainsExt(std::vector<Node>& n1,
237 : : std::vector<Node>& n2,
238 : : std::vector<Node>& nb,
239 : : std::vector<Node>& ne,
240 : : bool computeRemainder,
241 : : int remainderDir)
242 : : {
243 : 5099 : return componentContainsInternal(
244 : 5099 : true, n1, n2, nb, ne, computeRemainder, remainderDir);
245 : : }
246 : :
247 : 227189 : int StringsEntail::componentContainsInternal(bool isExt,
248 : : std::vector<Node>& n1,
249 : : std::vector<Node>& n2,
250 : : std::vector<Node>& nb,
251 : : std::vector<Node>& ne,
252 : : bool computeRemainder,
253 : : int remainderDir)
254 : : {
255 [ - + ][ - + ]: 227189 : Assert(nb.empty());
[ - - ]
256 [ - + ][ - + ]: 227189 : Assert(ne.empty());
[ - - ]
257 [ + - ]: 227189 : Trace("strings-entail") << "Component contains: " << std::endl;
258 [ + - ]: 227189 : Trace("strings-entail") << "isExt = " << isExt << std::endl;
259 [ + - ]: 227189 : Trace("strings-entail") << "n1 = " << n1 << std::endl;
260 [ + - ]: 227189 : Trace("strings-entail") << "n2 = " << n2 << std::endl;
261 : : // if n2 is a singleton, we can do optimized version here
262 [ + + ]: 227189 : if (n2.size() == 1)
263 : : {
264 [ + + ]: 462941 : for (unsigned i = 0; i < n1.size(); i++)
265 : : {
266 : 273459 : Node n1rb;
267 : 273459 : Node n1re;
268 [ + + ]: 546918 : if (componentContainsBase(
269 : 546918 : isExt, n1[i], n2[0], n1rb, n1re, 0, computeRemainder))
270 : : {
271 [ + + ]: 20759 : if (computeRemainder)
272 : : {
273 : 4057 : n1[i] = n2[0];
274 [ + - ]: 4057 : if (remainderDir != -1)
275 : : {
276 [ + + ]: 4057 : if (!n1re.isNull())
277 : : {
278 : 281 : ne.push_back(n1re);
279 : : }
280 : 4057 : ne.insert(ne.end(), n1.begin() + i + 1, n1.end());
281 : 4057 : n1.erase(n1.begin() + i + 1, n1.end());
282 : : }
283 [ - - ]: 0 : else if (!n1re.isNull())
284 : : {
285 : 0 : n1[i] = NodeManager::mkNode(Kind::STRING_CONCAT, n1[i], n1re);
286 : : }
287 [ - + ]: 4057 : if (remainderDir != 1)
288 : : {
289 : 0 : nb.insert(nb.end(), n1.begin(), n1.begin() + i);
290 : 0 : n1.erase(n1.begin(), n1.begin() + i);
291 [ - - ]: 0 : if (!n1rb.isNull())
292 : : {
293 : 0 : nb.push_back(n1rb);
294 : : }
295 : : }
296 [ + + ]: 4057 : else if (!n1rb.isNull())
297 : : {
298 : 459 : n1[i] = NodeManager::mkNode(Kind::STRING_CONCAT, n1rb, n1[i]);
299 : : }
300 : : }
301 : 20759 : return i;
302 : : }
303 [ + + ][ + + ]: 294218 : }
304 : : }
305 [ + + ]: 16948 : else if (n1.size() >= n2.size())
306 : : {
307 : 7754 : unsigned diff = n1.size() - n2.size();
308 [ + + ]: 19379 : for (unsigned i = 0; i <= diff; i++)
309 : : {
310 : 13213 : Node n1rb_first;
311 : 13213 : Node n1re_first;
312 : : // first component of n2 must be a suffix
313 [ + + ]: 26426 : if (componentContainsBase(isExt,
314 : 13213 : n1[i],
315 : 13213 : n2[0],
316 : : n1rb_first,
317 : : n1re_first,
318 : : 1,
319 [ + + ][ + + ]: 13213 : computeRemainder && remainderDir != 1))
320 : : {
321 [ - + ][ - + ]: 2878 : Assert(n1re_first.isNull());
[ - - ]
322 [ + - ]: 4522 : for (unsigned j = 1; j < n2.size(); j++)
323 : : {
324 : : // are we in the last component?
325 [ + + ]: 4522 : if (j + 1 == n2.size())
326 : : {
327 : 2368 : Node n1rb_last;
328 : 2368 : Node n1re_last;
329 : : // last component of n2 must be a prefix
330 [ + + ]: 4736 : if (componentContainsBase(isExt,
331 : 2368 : n1[i + j],
332 : 2368 : n2[j],
333 : : n1rb_last,
334 : : n1re_last,
335 : : -1,
336 [ + + ][ + - ]: 2368 : computeRemainder && remainderDir != -1))
337 : : {
338 [ + - ]: 3176 : Trace("strings-entail-debug")
339 : 1588 : << "Last remainder begin is " << n1rb_last << std::endl;
340 [ + - ]: 3176 : Trace("strings-entail-debug")
341 : 1588 : << "Last remainder end is " << n1re_last << std::endl;
342 [ - + ][ - + ]: 1588 : Assert(n1rb_last.isNull());
[ - - ]
343 [ + + ]: 1588 : if (computeRemainder)
344 : : {
345 [ + - ]: 530 : if (remainderDir != -1)
346 : : {
347 [ + + ]: 530 : if (!n1re_last.isNull())
348 : : {
349 : 6 : ne.push_back(n1re_last);
350 : : }
351 : 530 : ne.insert(ne.end(), n1.begin() + i + j + 1, n1.end());
352 : 530 : n1.erase(n1.begin() + i + j + 1, n1.end());
353 : 530 : n1[i + j] = n2[j];
354 : : }
355 [ + + ]: 530 : if (remainderDir != 1)
356 : : {
357 : 9 : n1[i] = n2[0];
358 : 9 : nb.insert(nb.end(), n1.begin(), n1.begin() + i);
359 : 9 : n1.erase(n1.begin(), n1.begin() + i);
360 [ + + ]: 9 : if (!n1rb_first.isNull())
361 : : {
362 : 3 : nb.push_back(n1rb_first);
363 : : }
364 : : }
365 : : }
366 [ + - ]: 1588 : Trace("strings-entail-debug") << "ne = " << ne << std::endl;
367 [ + - ]: 1588 : Trace("strings-entail-debug") << "nb = " << nb << std::endl;
368 [ + - ]: 1588 : Trace("strings-entail-debug") << "...return " << i << std::endl;
369 : 1588 : return i;
370 : : }
371 : : else
372 : : {
373 : 780 : break;
374 : : }
375 [ + + ][ + + ]: 4736 : }
376 [ + + ]: 2154 : else if (n1[i + j] != n2[j])
377 : : {
378 : 510 : break;
379 : : }
380 : : }
381 : : }
382 [ + + ][ + + ]: 14801 : }
383 : : }
384 : 204842 : return -1;
385 : : }
386 : :
387 : 289040 : bool StringsEntail::componentContainsBase(bool isExt,
388 : : Node n1,
389 : : Node n2,
390 : : Node& n1rb,
391 : : Node& n1re,
392 : : int dir,
393 : : bool computeRemainder)
394 : : {
395 [ - + ][ - + ]: 289040 : Assert(n1rb.isNull());
[ - - ]
396 [ - + ][ - + ]: 289040 : Assert(n1re.isNull());
[ - - ]
397 : :
398 [ + + ]: 289040 : if (n1 == n2)
399 : : {
400 : 21344 : return true;
401 : : }
402 : : else
403 : : {
404 [ + + ][ + + ]: 267696 : if (n1.isConst() && n2.isConst())
[ + + ]
405 : : {
406 : 12306 : size_t len1 = Word::getLength(n1);
407 : 12306 : size_t len2 = Word::getLength(n2);
408 [ + + ]: 12306 : if (len2 < len1)
409 : : {
410 [ + + ]: 4900 : if (dir == 1)
411 : : {
412 [ + + ]: 414 : if (Word::suffix(n1, len2) == n2)
413 : : {
414 [ + + ]: 299 : if (computeRemainder)
415 : : {
416 : 3 : n1rb = Word::prefix(n1, len1 - len2);
417 : : }
418 : 299 : return true;
419 : : }
420 : : }
421 [ + + ]: 4486 : else if (dir == -1)
422 : : {
423 [ + - ]: 314 : if (Word::prefix(n1, len2) == n2)
424 : : {
425 [ + + ]: 314 : if (computeRemainder)
426 : : {
427 : 6 : n1re = Word::suffix(n1, len1 - len2);
428 : : }
429 : 314 : return true;
430 : : }
431 : : }
432 : : else
433 : : {
434 : 4172 : size_t f = Word::find(n1, n2);
435 [ + + ]: 4172 : if (f != std::string::npos)
436 : : {
437 [ + + ]: 3254 : if (computeRemainder)
438 : : {
439 [ + + ]: 691 : if (f > 0)
440 : : {
441 : 459 : n1rb = Word::prefix(n1, f);
442 : : }
443 [ + + ]: 691 : if (len1 > f + len2)
444 : : {
445 : 281 : n1re = Word::suffix(n1, len1 - (f + len2));
446 : : }
447 : : }
448 : 3254 : return true;
449 : : }
450 : : }
451 : : }
452 : : }
453 [ + + ][ - + ]: 255390 : else if (!isExt || computeRemainder)
454 : : {
455 : : // Note the cases below would require constructing new terms
456 : : // as part of the remainder components. Thus, this is only checked
457 : : // when computeRemainder is false.
458 : 250286 : return false;
459 : : }
460 : : else
461 : : {
462 : : // cases for:
463 : : // n1 = x containing n2 = substr( x, n2[1], n2[2] )
464 [ + + ]: 5104 : if (n2.getKind() == Kind::STRING_SUBSTR)
465 : : {
466 [ + + ]: 4719 : if (n2[0] == n1)
467 : : {
468 : 12 : bool success = true;
469 : 12 : Node start_pos = n2[1];
470 : 24 : Node end_pos = NodeManager::mkNode(Kind::ADD, n2[1], n2[2]);
471 : 24 : Node len_n2s = NodeManager::mkNode(Kind::STRING_LENGTH, n2[0]);
472 [ + + ]: 12 : if (dir == 1)
473 : : {
474 : : // To be a suffix, start + length must be greater than
475 : : // or equal to the length of the string.
476 : 6 : success = d_arithEntail.check(end_pos, len_n2s);
477 : : }
478 [ + - ]: 6 : else if (dir == -1)
479 : : {
480 : : // To be a prefix, must literally start at 0, since
481 : : // if we knew it started at <0, it should be rewritten to "",
482 : : // if we knew it started at 0, then n2[1] should be rewritten to
483 : : // 0.
484 : 12 : success = start_pos.isConst()
485 [ + - ][ + - ]: 6 : && start_pos.getConst<Rational>().sgn() == 0;
486 : : }
487 [ + - ]: 12 : if (success)
488 : : {
489 : 12 : return true;
490 : : }
491 [ - + ][ - + ]: 36 : }
[ - + ]
492 : : }
493 : :
494 [ + + ]: 5092 : if (dir == 0)
495 : : {
496 [ + + ]: 5086 : if (n1.getKind() == Kind::STRING_REPLACE)
497 : : {
498 : : // (str.contains (str.replace x y z) w) ---> true
499 : : // if (str.contains x w) --> true and (str.contains z w) ---> true
500 : 16 : Node xCtnW = checkContains(n1[0], n2);
501 [ + + ][ + + ]: 8 : if (!xCtnW.isNull() && xCtnW.getConst<bool>())
[ + + ]
502 : : {
503 : 6 : Node zCtnW = checkContains(n1[2], n2);
504 [ + + ][ + - ]: 3 : if (!zCtnW.isNull() && zCtnW.getConst<bool>())
[ + + ]
505 : : {
506 : 2 : return true;
507 : : }
508 [ + + ]: 3 : }
509 [ + + ]: 8 : }
510 : : }
511 : : }
512 : : }
513 : 13529 : return false;
514 : : }
515 : :
516 : 277015 : bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
517 : : std::vector<Node>& n2,
518 : : std::vector<Node>& nb,
519 : : std::vector<Node>& ne,
520 : : int dir)
521 : : {
522 [ - + ][ - + ]: 277015 : Assert(nb.empty());
[ - - ]
523 [ - + ][ - + ]: 277015 : Assert(ne.empty());
[ - - ]
524 : 277015 : bool changed = false;
525 : : // for ( forwards, backwards ) direction
526 [ + + ]: 727079 : for (unsigned r = 0; r < 2; r++)
527 : : {
528 [ + + ][ + + ]: 502167 : if (dir == 0 || (r == 0 && dir == 1) || (r == 1 && dir == -1))
[ + + ][ + + ]
[ + + ]
529 : : {
530 [ + + ]: 360353 : unsigned index0 = r == 0 ? 0 : n1.size() - 1;
531 [ + + ]: 360353 : unsigned index1 = r == 0 ? 0 : n2.size() - 1;
532 : 360353 : bool removeComponent = false;
533 : 360353 : Node n1cmp = n1[index0];
534 : :
535 [ + + ][ + + ]: 360353 : if (n1cmp.isConst() && Word::isEmpty(n1cmp))
[ + + ][ + + ]
[ - - ]
536 : : {
537 : 51993 : return false;
538 : : }
539 : :
540 : 308360 : std::vector<Node> sss;
541 : 308360 : std::vector<Node> sls;
542 : 308360 : n1cmp = utils::decomposeSubstrChain(n1cmp, sss, sls);
543 [ + - ]: 616720 : Trace("strings-rewrite-debug2")
544 : 0 : << "stripConstantEndpoints : Compare " << n1cmp << " " << n2[index1]
545 : 308360 : << ", dir = " << r << ", sss/sls=" << sss << "/" << sls << std::endl;
546 [ + + ]: 308360 : if (n1cmp.isConst())
547 : : {
548 : 110515 : Node s = n1cmp;
549 : 110515 : size_t slen = Word::getLength(s);
550 : : // overlap is an overapproximation of the number of characters
551 : : // n2[index1] can match in s
552 : 110515 : unsigned overlap = Word::getLength(s);
553 [ + + ]: 110515 : if (n2[index1].isConst())
554 : : {
555 : 23133 : Node t = n2[index1];
556 : 23133 : std::size_t ret = r == 0 ? Word::find(s, t) : Word::rfind(s, t);
557 [ + + ]: 23133 : if (ret == std::string::npos)
558 : : {
559 [ + + ]: 6015 : if (n1.size() == 1)
560 : : {
561 : : // can remove everything
562 : : // e.g. str.contains( "abc", str.++( "ba", x ) ) -->
563 : : // str.contains( "", str.++( "ba", x ) )
564 : : // or std.contains( str.substr( "abc", x, y ), "d" ) --->
565 : : // str.contains( "", "d" )
566 : 31 : removeComponent = true;
567 : : }
568 [ + + ]: 5984 : else if (sss.empty()) // only if not substr
569 : : {
570 : : // check how much overlap there is
571 : : // This is used to partially strip off the endpoint
572 : : // e.g. str.contains( str.++( "abc", x ), str.++( "cd", y ) ) -->
573 : : // str.contains( str.++( "c", x ), str.++( "cd", y ) )
574 : 5981 : overlap = r == 0 ? Word::overlap(s, t) : Word::overlap(t, s);
575 : : }
576 : : // note that we cannot process substring here, since t may
577 : : // match only part of s. Consider:
578 : : // (str.++ "C" (str.substr "AB" x y)), "CB"
579 : : // where "AB" and "CB" have no overlap, but "C" is not part of what
580 : : // is matched with "AB".
581 : : }
582 [ + + ]: 17118 : else if (sss.empty()) // only if not substr
583 : : {
584 [ - + ][ - + ]: 6054 : Assert(ret < slen);
[ - - ]
585 : : // can strip off up to the find position, e.g.
586 : : // str.contains( str.++( "abc", x ), str.++( "b", y ) ) -->
587 : : // str.contains( str.++( "bc", x ), str.++( "b", y ) ),
588 : : // and
589 : : // str.contains( str.++( x, "abbd" ), str.++( y, "b" ) ) -->
590 : : // str.contains( str.++( x, "abb" ), str.++( y, "b" ) )
591 : 6054 : overlap = slen - ret;
592 : : }
593 : 23133 : }
594 : : else
595 : : {
596 : : // inconclusive
597 : : }
598 [ + - ]: 221030 : Trace("strings-rewrite-debug2")
599 : 0 : << "rem = " << removeComponent << ", overlap = " << overlap
600 : 110515 : << std::endl;
601 : : // process the overlap
602 [ + + ]: 110515 : if (overlap < slen)
603 : : {
604 : 4181 : changed = true;
605 [ + + ]: 4181 : if (overlap == 0)
606 : : {
607 : 3753 : removeComponent = true;
608 : : }
609 : : else
610 : : {
611 : : // can drop the prefix (resp. suffix) from the first (resp. last)
612 : : // component
613 [ + + ]: 428 : if (r == 0)
614 : : {
615 : 144 : nb.push_back(Word::prefix(s, slen - overlap));
616 : 144 : n1[index0] = Word::suffix(s, overlap);
617 : : }
618 : : else
619 : : {
620 : 284 : ne.push_back(Word::suffix(s, slen - overlap));
621 : 284 : n1[index0] = Word::prefix(s, overlap);
622 : : }
623 : : }
624 : : }
625 : 110515 : }
626 [ + + ]: 197845 : else if (n1cmp.getKind() == Kind::STRING_ITOS)
627 : : {
628 [ + + ]: 1543 : if (n2[index1].isConst())
629 : : {
630 [ - + ][ - + ]: 978 : Assert(n2[index1].getType().isString()); // string-only
[ - - ]
631 : 978 : cvc5::internal::String t = n2[index1].getConst<String>();
632 [ + + ]: 978 : if (n1.size() == 1)
633 : : {
634 : : // if n1.size()==1, then if n2[index1] is not a number, we can drop
635 : : // the entire component
636 : : // e.g. str.contains( int.to.str(x), "123a45") --> false
637 [ + + ]: 858 : if (!t.isNumber())
638 : : {
639 : 79 : removeComponent = true;
640 : : }
641 : : }
642 : : else
643 : : {
644 : 120 : const std::vector<unsigned>& tvec = t.getVec();
645 [ - + ][ - + ]: 120 : Assert(tvec.size() > 0);
[ - - ]
646 : :
647 : : // if n1.size()>1, then if the first (resp. last) character of
648 : : // n2[index1]
649 : : // is not a digit, we can drop the entire component, e.g.:
650 : : // str.contains( str.++( int.to.str(x), y ), "a12") -->
651 : : // str.contains( y, "a12" )
652 : : // str.contains( str.++( y, int.to.str(x) ), "a0b") -->
653 : : // str.contains( y, "a0b" )
654 [ + + ]: 120 : unsigned i = r == 0 ? 0 : (tvec.size() - 1);
655 [ + + ]: 120 : if (!String::isDigit(tvec[i]))
656 : : {
657 : 47 : removeComponent = true;
658 : : }
659 : : }
660 : 978 : }
661 : : }
662 [ + + ]: 308360 : if (removeComponent)
663 : : {
664 [ + - ]: 3910 : Trace("strings-rewrite-debug2") << "...remove component" << std::endl;
665 : : // can drop entire first (resp. last) component
666 [ + + ]: 3910 : if (r == 0)
667 : : {
668 : 1432 : nb.push_back(n1[index0]);
669 : 1432 : n1.erase(n1.begin(), n1.begin() + 1);
670 : : }
671 : : else
672 : : {
673 : 2478 : ne.push_back(n1[index0]);
674 : 2478 : n1.pop_back();
675 : : }
676 [ + + ]: 3910 : if (n1.empty())
677 : : {
678 : : // if we've removed everything, just return (we will rewrite to false)
679 : 110 : return true;
680 : : }
681 : : else
682 : : {
683 : 3800 : changed = true;
684 : : }
685 : : }
686 [ + + ][ + + ]: 360573 : }
[ + + ]
687 : : }
688 : : // TODO (#1180) : computing the maximal overlap in this function may be
689 : : // important.
690 : : // str.contains( str.++( str.to.int(x), str.substr(y,0,3) ), "2aaaa" ) --->
691 : : // false
692 : : // ...since str.to.int(x) can contain at most 1 character from "2aaaa",
693 : : // leaving 4 characters
694 : : // which is larger that the upper bound for length of str.substr(y,0,3),
695 : : // which is 3.
696 : 224912 : return changed;
697 : : }
698 : :
699 : 102866 : Node StringsEntail::checkContains(Node a, Node b)
700 : : {
701 : 205732 : Node ctn = NodeManager::mkNode(Kind::STRING_CONTAINS, a, b);
702 : :
703 [ + - ]: 102866 : if (d_rr != nullptr)
704 : : {
705 : 102866 : ctn = d_rr->rewrite(ctn);
706 : : }
707 : : else
708 : : {
709 [ - - ]: 0 : if (d_rewriter == nullptr)
710 : : {
711 : 0 : return Node::null();
712 : : }
713 : 0 : Node prev;
714 : : do
715 : : {
716 : 0 : prev = ctn;
717 : 0 : ctn = d_rewriter->rewriteContains(ctn);
718 : 0 : } while (prev != ctn && ctn.getKind() == Kind::STRING_CONTAINS);
719 : 0 : }
720 : :
721 [ - + ][ - + ]: 102866 : Assert(ctn.getType().isBoolean());
[ - - ]
722 [ + + ]: 102866 : return ctn.isConst() ? ctn : Node::null();
723 : 102866 : }
724 : :
725 : 64197 : bool StringsEntail::checkNonEmpty(Node a)
726 : : {
727 [ + + ]: 64197 : if (a.isConst())
728 : : {
729 : 25576 : return Word::getLength(a) != 0;
730 : : }
731 : 38621 : Node len = NodeManager::mkNode(Kind::STRING_LENGTH, a);
732 : 38621 : len = d_arithEntail.rewriteArith(len);
733 : 38621 : return d_arithEntail.check(len, true);
734 : 38621 : }
735 : :
736 : 78707 : bool StringsEntail::checkLengthOne(Node s, bool strict)
737 : : {
738 [ + + ]: 78707 : if (s.isConst())
739 : : {
740 : 7814 : size_t len = Word::getLength(s);
741 [ + + ]: 7814 : return strict ? (len == 1) : (len <= 1);
742 : : }
743 : 70893 : NodeManager* nm = s.getNodeManager();
744 : 70893 : Node one = nm->mkConstInt(Rational(1));
745 : 70893 : Node len = nm->mkNode(Kind::STRING_LENGTH, s);
746 : 70893 : len = d_arithEntail.rewriteArith(len);
747 [ + - ][ - - ]: 70893 : return d_arithEntail.check(one, len)
[ - - ]
748 [ + + ][ + + ]: 70893 : && (!strict || d_arithEntail.check(len, true));
[ + + ][ + + ]
[ + - ][ - - ]
749 : 70893 : }
750 : :
751 : 200168 : bool StringsEntail::checkMultisetSubset(Node a, Node b)
752 : : {
753 : 200168 : std::vector<Node> avec;
754 : 200168 : utils::getConcat(getMultisetApproximation(a), avec);
755 : 200168 : std::vector<Node> bvec;
756 : 200168 : utils::getConcat(b, bvec);
757 : :
758 [ + + ]: 1201008 : std::map<Node, unsigned> num_nconst[2];
759 [ + + ]: 1201008 : std::map<Node, unsigned> num_const[2];
760 [ + + ]: 600504 : for (unsigned j = 0; j < 2; j++)
761 : : {
762 [ + + ]: 400336 : std::vector<Node>& jvec = j == 0 ? avec : bvec;
763 [ + + ]: 933893 : for (const Node& cc : jvec)
764 : : {
765 [ + + ]: 533557 : if (cc.isConst())
766 : : {
767 : 235605 : num_const[j][cc]++;
768 : : }
769 : : else
770 : : {
771 : 297952 : num_nconst[j][cc]++;
772 : : }
773 : : }
774 : : }
775 : 200168 : bool ms_success = true;
776 [ + + ]: 206103 : for (std::pair<const Node, unsigned>& nncp : num_nconst[0])
777 : : {
778 [ + + ]: 104234 : if (nncp.second > num_nconst[1][nncp.first])
779 : : {
780 : 98299 : ms_success = false;
781 : 98299 : break;
782 : : }
783 : : }
784 [ + + ]: 200168 : if (ms_success)
785 : : {
786 : : // count the number of constant characters in the first argument
787 [ + + ]: 611214 : std::map<Node, unsigned> count_const[2];
788 : 101869 : std::vector<Node> chars;
789 [ + + ]: 305607 : for (unsigned j = 0; j < 2; j++)
790 : : {
791 [ + + ]: 316964 : for (std::pair<const Node, unsigned>& ncp : num_const[j])
792 : : {
793 : 113226 : Node cn = ncp.first;
794 [ - + ][ - + ]: 113226 : Assert(cn.isConst());
[ - - ]
795 : 113226 : std::vector<Node> cnChars = Word::getChars(cn);
796 [ + + ]: 269950 : for (const Node& ch : cnChars)
797 : : {
798 : 156724 : count_const[j][ch] += ncp.second;
799 [ + + ]: 156724 : if (std::find(chars.begin(), chars.end(), ch) == chars.end())
800 : : {
801 : 117231 : chars.push_back(ch);
802 : : }
803 : : }
804 : 113226 : }
805 : : }
806 [ + - ]: 203738 : Trace("strings-entail-ms-ss")
807 : 101869 : << "For " << a << " and " << b << " : " << std::endl;
808 [ + + ]: 217555 : for (const Node& ch : chars)
809 : : {
810 [ + - ]: 116630 : Trace("strings-entail-ms-ss") << " # occurrences of substring ";
811 [ + - ]: 116630 : Trace("strings-entail-ms-ss") << ch << " in arguments is ";
812 [ + - ]: 233260 : Trace("strings-entail-ms-ss")
813 : 116630 : << count_const[0][ch] << " / " << count_const[1][ch] << std::endl;
814 [ + + ]: 116630 : if (count_const[0][ch] < count_const[1][ch])
815 : : {
816 : 944 : return true;
817 : : }
818 : : }
819 : :
820 : : // TODO (#1180): count the number of 2,3,4,.. character substrings
821 : : // for example:
822 : : // str.contains( str.++( x, "cbabc" ), str.++( "cabbc", x ) ) ---> false
823 : : // since the second argument contains more occurrences of "bb".
824 : : // note this is orthogonal reasoning to inductive reasoning
825 : : // via regular membership reduction in Liang et al CAV 2015.
826 [ + + ][ + + ]: 407476 : }
[ - - ]
827 : 199224 : return false;
828 [ + + ][ + + ]: 1401176 : }
[ - - ][ - - ]
829 : :
830 : 6770 : Node StringsEntail::checkHomogeneousString(Node a)
831 : : {
832 : 6770 : std::vector<Node> avec;
833 : 6770 : utils::getConcat(getMultisetApproximation(a), avec);
834 : :
835 : 6770 : bool cValid = false;
836 : 6770 : Node c;
837 [ + + ]: 8870 : for (const Node& ac : avec)
838 : : {
839 [ + + ]: 6811 : if (ac.isConst())
840 : : {
841 : 4416 : std::vector<Node> acv = Word::getChars(ac);
842 [ + + ]: 9073 : for (const Node& cc : acv)
843 : : {
844 [ + + ]: 6973 : if (!cValid)
845 : : {
846 : 3881 : cValid = true;
847 : 3881 : c = cc;
848 : : }
849 [ + + ]: 3092 : else if (c != cc)
850 : : {
851 : : // Found a different character
852 : 2316 : return Node::null();
853 : : }
854 : : }
855 [ + + ]: 4416 : }
856 : : else
857 : : {
858 : : // Could produce a different character
859 : 2395 : return Node::null();
860 : : }
861 : : }
862 : :
863 [ + + ]: 2059 : if (!cValid)
864 : : {
865 : 1056 : return Word::mkEmptyWord(a.getType());
866 : : }
867 : :
868 : 1531 : return c;
869 : 6770 : }
870 : :
871 : 418973 : Node StringsEntail::getMultisetApproximation(Node a)
872 : : {
873 : 418973 : NodeManager* nm = a.getNodeManager();
874 [ + + ]: 472853 : while (a.getKind() == Kind::STRING_SUBSTR)
875 : : {
876 : 53880 : a = a[0];
877 : : }
878 [ + + ]: 418973 : if (a.getKind() == Kind::STRING_REPLACE)
879 : : {
880 : : return getMultisetApproximation(
881 : 47178 : nm->mkNode(Kind::STRING_CONCAT, a[0], a[2]));
882 : : }
883 [ + + ]: 395384 : else if (a.getKind() == Kind::STRING_CONCAT)
884 : : {
885 : 69510 : NodeBuilder nb(nm, Kind::STRING_CONCAT);
886 [ + + ]: 257956 : for (const Node& ac : a)
887 : : {
888 : 188446 : nb << getMultisetApproximation(ac);
889 : 188446 : }
890 : 69510 : return nb.constructNode();
891 : 69510 : }
892 : : else
893 : : {
894 : 325874 : return a;
895 : : }
896 : : }
897 : :
898 : 1364 : Node StringsEntail::getStringOrEmpty(Node n)
899 : : {
900 : 1364 : Node res;
901 [ + + ]: 2733 : while (res.isNull())
902 : : {
903 [ + + ][ + ]: 1369 : switch (n.getKind())
904 : : {
905 : 16 : case Kind::STRING_REPLACE:
906 : : {
907 [ + + ]: 16 : if (Word::isEmpty(n[0]))
908 : : {
909 : : // (str.replace "" x y) --> y
910 : 5 : n = n[2];
911 : 5 : break;
912 : : }
913 : 11 : if (checkLengthOne(n[0]) && Word::isEmpty(n[2]))
914 : : {
915 : : // (str.replace "A" x "") --> "A"
916 : 7 : res = n[0];
917 : 7 : break;
918 : : }
919 : :
920 : 4 : res = n;
921 : 4 : break;
922 : : }
923 : 34 : case Kind::STRING_SUBSTR:
924 : : {
925 [ + + ]: 34 : if (checkLengthOne(n[0]))
926 : : {
927 : : // (str.substr "A" x y) --> "A"
928 : 12 : res = n[0];
929 : 12 : break;
930 : : }
931 : 22 : res = n;
932 : 22 : break;
933 : : }
934 : 1319 : default:
935 : : {
936 : 1319 : res = n;
937 : 1319 : break;
938 : : }
939 : : }
940 : : }
941 : 1364 : return res;
942 : 0 : }
943 : :
944 : 2098 : Node StringsEntail::inferEqsFromContains(Node x, Node y)
945 : : {
946 : 2098 : NodeManager* nm = x.getNodeManager();
947 : 2098 : Node emp = Word::mkEmptyWord(x.getType());
948 [ - + ][ - + ]: 6294 : AssertEqual(x.getType(), y.getType());
[ - - ]
949 : 2098 : TypeNode stype = x.getType();
950 : :
951 : 2098 : Node xLen = nm->mkNode(Kind::STRING_LENGTH, x);
952 : 2098 : std::vector<Node> yLens;
953 [ + + ]: 2098 : if (y.getKind() != Kind::STRING_CONCAT)
954 : : {
955 : 10 : yLens.push_back(nm->mkNode(Kind::STRING_LENGTH, y));
956 : : }
957 : : else
958 : : {
959 [ + + ]: 7961 : for (const Node& yi : y)
960 : : {
961 : 5873 : yLens.push_back(nm->mkNode(Kind::STRING_LENGTH, yi));
962 : 5873 : }
963 : : }
964 : :
965 : 2098 : std::vector<Node> zeroLens;
966 [ + + ]: 2098 : if (x == emp)
967 : : {
968 : : // If x is the empty string, then all ys must be empty, too, and we can
969 : : // skip the expensive checks. Note that this is just a performance
970 : : // optimization.
971 : 199 : zeroLens.swap(yLens);
972 : : }
973 : : else
974 : : {
975 : : // Check if we can infer that str.len(x) <= str.len(y). If that is the
976 : : // case, try to minimize the sum in str.len(x) <= str.len(y1) + ... +
977 : : // str.len(yn) (where y = y1 ++ ... ++ yn) while keeping the inequality
978 : : // true. The terms that can have length zero without making the inequality
979 : : // false must be all be empty if (str.contains x y) is true.
980 [ + + ]: 1899 : if (!d_arithEntail.inferZerosInSumGeq(xLen, yLens, zeroLens))
981 : : {
982 : : // We could not prove that the inequality holds
983 : 1707 : return Node::null();
984 : : }
985 [ + + ]: 192 : else if (yLens.size() == y.getNumChildren())
986 : : {
987 : : // We could only prove that the inequality holds but not that any of the
988 : : // ys must be empty
989 : 136 : return nm->mkNode(Kind::EQUAL, x, y);
990 : : }
991 : : }
992 : :
993 [ + + ]: 255 : if (y.getKind() != Kind::STRING_CONCAT)
994 : : {
995 [ - + ]: 3 : if (zeroLens.size() == 1)
996 : : {
997 : : // y is not a concatenation and we found that it must be empty, so just
998 : : // return (= y "")
999 : 0 : Assert(zeroLens[0][0] == y);
1000 : 0 : return nm->mkNode(Kind::EQUAL, y, emp);
1001 : : }
1002 : : else
1003 : : {
1004 : 3 : Assert(yLens.size() == 1 && yLens[0][0] == y);
1005 : 3 : return nm->mkNode(Kind::EQUAL, x, y);
1006 : : }
1007 : : }
1008 : :
1009 : 252 : std::vector<Node> cs;
1010 [ + + ]: 324 : for (const Node& yiLen : yLens)
1011 : : {
1012 [ - + ][ - + ]: 72 : Assert(std::find(y.begin(), y.end(), yiLen[0]) != y.end());
[ - - ]
1013 : 72 : cs.push_back(yiLen[0]);
1014 : : }
1015 : :
1016 : : // (= x (str.++ y1' ... ym'))
1017 : 252 : std::vector<Node> eqs;
1018 : 504 : Node mainEq = nm->mkNode(Kind::EQUAL, x, utils::mkConcat(cs, stype));
1019 : 252 : eqs.push_back(mainEq);
1020 : : // (= y1'' "") ... (= yk'' "")
1021 [ + + ]: 871 : for (const Node& zeroLen : zeroLens)
1022 : : {
1023 [ - + ][ - + ]: 619 : Assert(std::find(y.begin(), y.end(), zeroLen[0]) != y.end());
[ - - ]
1024 : 619 : eqs.push_back(nm->mkNode(Kind::EQUAL, zeroLen[0], emp));
1025 : : }
1026 : : // (and (= x (str.++ y1' ... ym')) (= y1'' "") ... (= yk'' ""))
1027 : 252 : return nm->mkAnd(eqs);
1028 : 2098 : }
1029 : :
1030 : 111827 : Node StringsEntail::rewriteViaMacroSubstrStripSymLength(const Node& node,
1031 : : Rewrite& rule,
1032 : : std::vector<Node>& ch1,
1033 : : std::vector<Node>& ch2)
1034 : : {
1035 [ - + ][ - + ]: 111827 : Assert(node.getKind() == Kind::STRING_SUBSTR);
[ - - ]
1036 : 111827 : NodeManager* nm = node.getNodeManager();
1037 : 111827 : utils::getConcat(node[0], ch1);
1038 : 111827 : TypeNode stype = node[0].getType();
1039 : 111827 : Node zero = nm->mkConstInt(Rational(0));
1040 : : // definite inclusion
1041 [ + + ]: 111827 : if (node[1] == zero)
1042 : : {
1043 : 49151 : Node curr = node[2];
1044 [ + + ]: 49151 : if (stripSymbolicLength(ch1, ch2, 1, curr))
1045 : : {
1046 : 1906 : std::vector<Node> chr = ch2;
1047 [ + + ][ + + ]: 1906 : if (curr != zero && !ch1.empty())
[ + + ]
1048 : : {
1049 : : // make the length explicitly, which helps proof reconstruction
1050 : 377 : Node cpulled = utils::mkConcat(ch2, stype);
1051 : : Node resultLen = nm->mkNode(
1052 : 754 : Kind::SUB, node[2], nm->mkNode(Kind::STRING_LENGTH, cpulled));
1053 : 1131 : chr.push_back(nm->mkNode(Kind::STRING_SUBSTR,
1054 : 754 : utils::mkConcat(ch1, stype),
1055 : : node[1],
1056 : : resultLen));
1057 : 377 : }
1058 : 1906 : Node ret = utils::mkConcat(chr, stype);
1059 : 1906 : rule = Rewrite::SS_LEN_INCLUDE;
1060 : 1906 : return ret;
1061 : 1906 : }
1062 [ + + ]: 49151 : }
1063 [ + + ]: 324424 : for (unsigned r = 0; r < 2; r++)
1064 : : {
1065 : : // the amount of characters we can strip
1066 : 217398 : Node curr;
1067 [ + + ]: 217398 : if (r == 0)
1068 : : {
1069 [ + + ]: 109921 : if (node[1] != zero)
1070 : : {
1071 : : // strip up to start point off the start of the string
1072 : 62676 : curr = node[1];
1073 : : }
1074 : : }
1075 [ + - ]: 107477 : else if (r == 1)
1076 : : {
1077 : 214954 : Node tot_len = nm->mkNode(Kind::STRING_LENGTH, node[0]);
1078 [ + + ]: 107477 : if (node[2] != tot_len)
1079 : : {
1080 : 210894 : Node end_pt = nm->mkNode(Kind::ADD, node[1], node[2]);
1081 : : // strip up to ( str.len(node[0]) - end_pt ) off the end of the string
1082 : 105447 : curr = nm->mkNode(Kind::SUB, tot_len, end_pt);
1083 : 105447 : curr = d_arithEntail.rewriteArith(curr);
1084 : 105447 : }
1085 : 107477 : }
1086 [ + + ]: 217398 : if (!curr.isNull())
1087 : : {
1088 : : // strip off components while quantity is entailed positive
1089 [ + + ]: 168123 : int dir = r == 0 ? 1 : -1;
1090 : 168123 : ch2.clear();
1091 [ + + ]: 168123 : if (stripSymbolicLength(ch1, ch2, dir, curr))
1092 : : {
1093 [ + + ]: 2895 : if (r == 0)
1094 : : {
1095 : : // make the length explicitly, which helps proof reconstruction
1096 : 2444 : Node cskipped = utils::mkConcat(ch2, stype);
1097 : : Node resultStart = nm->mkNode(
1098 : 4888 : Kind::SUB, node[1], nm->mkNode(Kind::STRING_LENGTH, cskipped));
1099 : : Node ret = nm->mkNode(Kind::STRING_SUBSTR,
1100 : 4888 : utils::mkConcat(ch1, stype),
1101 : : resultStart,
1102 : 9776 : node[2]);
1103 : 2444 : rule = Rewrite::SS_STRIP_START_PT;
1104 : 2444 : return ret;
1105 : 2444 : }
1106 : : else
1107 : : {
1108 : : Node ret = nm->mkNode(Kind::STRING_SUBSTR,
1109 : 902 : utils::mkConcat(ch1, stype),
1110 : : node[1],
1111 : 1804 : node[2]);
1112 : 451 : rule = Rewrite::SS_STRIP_END_PT;
1113 : 451 : return ret;
1114 : 451 : }
1115 : : }
1116 : : }
1117 [ + + ]: 217398 : }
1118 : :
1119 : 107026 : return Node::null();
1120 : 111827 : }
1121 : :
1122 : : } // namespace strings
1123 : : } // namespace theory
1124 : : } // namespace cvc5::internal
|
