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 regular expressions.
11 : : */
12 : :
13 : : #include "theory/strings/regexp_entail.h"
14 : :
15 : : #include "theory/rewriter.h"
16 : : #include "theory/strings/regexp_eval.h"
17 : : #include "theory/strings/theory_strings_utils.h"
18 : : #include "theory/strings/word.h"
19 : : #include "util/rational.h"
20 : : #include "util/string.h"
21 : :
22 : : using namespace std;
23 : : using namespace cvc5::internal::kind;
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace strings {
28 : :
29 : 109958 : RegExpEntail::RegExpEntail(NodeManager* nm, Rewriter* r) : d_aent(nm, r)
30 : : {
31 : 109958 : d_zero = nm->mkConstInt(Rational(0));
32 : 109958 : d_one = nm->mkConstInt(Rational(1));
33 : 109958 : }
34 : :
35 : 39013 : Node RegExpEntail::simpleRegexpConsume(NodeManager* nm,
36 : : std::vector<Node>& mchildren,
37 : : std::vector<Node>& children,
38 : : int dir)
39 : : {
40 [ + - ]: 78026 : Trace("regexp-ext-rewrite-debug")
41 : 39013 : << "Simple reg exp consume, dir=" << dir << ":" << std::endl;
42 : 39013 : unsigned tmin = dir < 0 ? 0 : dir;
43 [ + + ]: 39013 : unsigned tmax = dir < 0 ? 1 : dir;
44 : : // try to remove off front and back
45 [ + + ]: 106824 : for (unsigned t = 0; t < 2; t++)
46 : : {
47 [ + + ][ + + ]: 74503 : if (tmin <= t && t <= tmax)
48 : : {
49 [ + - ]: 97222 : Trace("regexp-ext-rewrite-debug")
50 : 48611 : << "Run consume, direction is " << t << " with:" << std::endl;
51 [ + - ]: 97222 : Trace("regexp-ext-rewrite-debug")
52 : 48611 : << " mchildren : " << mchildren << std::endl;
53 [ + - ]: 97222 : Trace("regexp-ext-rewrite-debug")
54 : 48611 : << " children : " << children << std::endl;
55 : 48611 : bool do_next = true;
56 [ + + ][ + + ]: 94735 : while (!children.empty() && !mchildren.empty() && do_next)
[ + + ][ + + ]
57 : : {
58 : 52824 : do_next = false;
59 : 52824 : Node xc = mchildren[mchildren.size() - 1];
60 : 52824 : Node rc = children[children.size() - 1];
61 [ + - ]: 105648 : Trace("regexp-ext-rewrite-debug")
62 : 52824 : << "* " << xc << " in " << rc << std::endl;
63 [ - + ][ - + ]: 52824 : Assert(rc.getKind() != Kind::REGEXP_CONCAT);
[ - - ]
64 [ - + ][ - + ]: 52824 : Assert(xc.getKind() != Kind::STRING_CONCAT);
[ - - ]
65 [ + + ]: 52824 : if (rc.getKind() == Kind::STRING_TO_REGEXP)
66 : : {
67 : 23324 : std::vector<Node> childrenc;
68 : 23324 : utils::getConcat(rc[0], childrenc);
69 [ + + ]: 23324 : size_t cindex = t == 1 ? 0 : childrenc.size() - 1;
70 : 23324 : Node rcc = childrenc[cindex];
71 : 23324 : Node remStr;
72 [ + + ]: 23324 : if (xc == rcc)
73 : : {
74 : 2167 : mchildren.pop_back();
75 : 2167 : do_next = true;
76 [ + - ]: 2167 : Trace("regexp-ext-rewrite-debug") << "- strip equal" << std::endl;
77 : : }
78 [ + + ][ + + ]: 21157 : else if (rcc.isConst() && Word::isEmpty(rcc))
[ + + ][ + + ]
[ - - ]
79 : : {
80 [ + - ]: 1052 : Trace("regexp-ext-rewrite-debug")
81 : 526 : << "- ignore empty RE" << std::endl;
82 : : // ignore and continue
83 : 526 : do_next = true;
84 : : }
85 [ + + ][ + + ]: 20631 : else if (xc.isConst() && rcc.isConst())
[ + + ]
86 : : {
87 : : // split the constant
88 : : size_t index;
89 : 7539 : remStr = Word::splitConstant(xc, rcc, index, t == 0);
90 [ + - ]: 15078 : Trace("regexp-ext-rewrite-debug")
91 : 0 : << "- CRE: Regexp const split : " << xc << " " << rcc << " -> "
92 : 7539 : << remStr << " " << index << " " << t << std::endl;
93 [ + + ]: 7539 : if (remStr.isNull())
94 : : {
95 [ + - ]: 11320 : Trace("regexp-ext-rewrite-debug")
96 : 5660 : << "...return false" << std::endl;
97 : 11320 : return nm->mkConst(false);
98 : : }
99 : : else
100 : : {
101 [ + - ]: 3758 : Trace("regexp-ext-rewrite-debug")
102 : 1879 : << "- strip equal const" << std::endl;
103 : 1879 : mchildren.pop_back();
104 [ + + ]: 1879 : if (index == 0)
105 : : {
106 : 1553 : mchildren.push_back(remStr);
107 : : // we've processed the remainder as leftover for the LHS
108 : : // string, clear it now
109 : 1553 : remStr = Node::null();
110 : : }
111 : : // otherwise remStr is processed below
112 : : }
113 [ + - ]: 1879 : Trace("regexp-ext-rewrite-debug") << "- split const" << std::endl;
114 : 1879 : do_next = true;
115 : : }
116 [ + + ]: 17664 : if (do_next)
117 : : {
118 [ + + ]: 4572 : if (remStr.isNull())
119 : : {
120 : : // we have fully processed the component
121 : 4246 : childrenc.erase(childrenc.begin() + cindex);
122 : : }
123 : : else
124 : : {
125 : : // we have a remainder
126 : 326 : childrenc[cindex] = remStr;
127 : : }
128 [ + + ]: 4572 : if (childrenc.empty())
129 : : {
130 : : // if childrenc is empty, we are done with the current str.to_re
131 : 4148 : children.pop_back();
132 : : }
133 : : else
134 : : {
135 : : // otherwise we reconstruct it
136 : 424 : TypeNode stype = nm->stringType();
137 : 848 : children[children.size() - 1] = nm->mkNode(
138 : 1272 : Kind::STRING_TO_REGEXP, utils::mkConcat(childrenc, stype));
139 : 424 : }
140 : : }
141 [ + + ][ + + ]: 34644 : }
[ + + ]
142 [ + + ]: 29500 : else if (xc.isConst())
143 : : {
144 : : // check for constants
145 : 9763 : cvc5::internal::String s = xc.getConst<String>();
146 [ + + ]: 9763 : if (Word::isEmpty(xc))
147 : : {
148 [ + - ]: 469 : Trace("regexp-ext-rewrite-debug") << "- ignore empty" << std::endl;
149 : : // ignore and continue
150 : 469 : mchildren.pop_back();
151 : 469 : do_next = true;
152 : : }
153 : 9294 : else if (rc.getKind() == Kind::REGEXP_RANGE
154 [ + + ][ + + ]: 9294 : || rc.getKind() == Kind::REGEXP_ALLCHAR)
[ + + ]
155 : : {
156 [ + + ]: 1665 : if (!isConstRegExp(rc))
157 : : {
158 : : // if a non-standard re.range term, abort
159 : 8 : break;
160 : : }
161 : 1657 : std::vector<unsigned> ssVec;
162 [ + + ]: 1657 : ssVec.push_back(t == 0 ? s.back() : s.front());
163 : 1657 : cvc5::internal::String ss(ssVec);
164 [ + + ]: 1657 : if (testConstStringInRegExp(ss, rc))
165 : : {
166 : : // strip off one character
167 : 1136 : mchildren.pop_back();
168 [ + + ]: 1136 : if (s.size() > 1)
169 : : {
170 [ + + ]: 833 : if (t == 0)
171 : : {
172 : 572 : mchildren.push_back(nm->mkConst(s.substr(0, s.size() - 1)));
173 : : }
174 : : else
175 : : {
176 : 261 : mchildren.push_back(nm->mkConst(s.substr(1)));
177 : : }
178 : : }
179 : 1136 : children.pop_back();
180 : 1136 : do_next = true;
181 : : }
182 : : else
183 : : {
184 [ + - ]: 1042 : Trace("regexp-ext-rewrite-debug")
185 : 521 : << "...return false" << std::endl;
186 : 1042 : return nm->mkConst(false);
187 : : }
188 [ + + ][ + + ]: 2178 : }
189 : 7629 : else if (rc.getKind() == Kind::REGEXP_INTER
190 [ + + ][ + + ]: 7629 : || rc.getKind() == Kind::REGEXP_UNION)
[ + + ]
191 : : {
192 : : // see if any/each child does not work
193 : 2733 : bool result_valid = true;
194 : 2733 : Node result;
195 : 2733 : Node emp_s = nm->mkConst(String(""));
196 [ + + ]: 8942 : for (unsigned i = 0; i < rc.getNumChildren(); i++)
197 : : {
198 : 6209 : std::vector<Node> mchildren_s;
199 : 6209 : std::vector<Node> children_s;
200 : 6209 : mchildren_s.push_back(xc);
201 : 6209 : utils::getConcat(rc[i], children_s);
202 [ + - ]: 6209 : Trace("regexp-ext-rewrite-debug") << push;
203 : 6209 : Node ret = simpleRegexpConsume(nm, mchildren_s, children_s, t);
204 [ + - ]: 6209 : Trace("regexp-ext-rewrite-debug") << pop;
205 [ + + ]: 6209 : if (!ret.isNull())
206 : : {
207 : : // one conjunct cannot be satisfied, return false
208 [ - + ]: 3371 : if (rc.getKind() == Kind::REGEXP_INTER)
209 : : {
210 [ - - ]: 0 : Trace("regexp-ext-rewrite-debug")
211 : 0 : << "...return " << ret << std::endl;
212 : 0 : return ret;
213 : : }
214 : : }
215 : : else
216 : : {
217 [ + + ]: 2838 : if (children_s.empty())
218 : : {
219 : : // if we were able to fully consume, store the result
220 [ - + ][ - + ]: 1976 : Assert(mchildren_s.size() <= 1);
[ - - ]
221 [ + + ]: 1976 : if (mchildren_s.empty())
222 : : {
223 : 332 : mchildren_s.push_back(emp_s);
224 : : }
225 [ + + ]: 1976 : if (result.isNull())
226 : : {
227 : 1682 : result = mchildren_s[0];
228 : : }
229 [ + + ]: 294 : else if (result != mchildren_s[0])
230 : : {
231 : 14 : result_valid = false;
232 : : }
233 : : }
234 : : else
235 : : {
236 : 862 : result_valid = false;
237 : : }
238 : : }
239 [ + - ][ + - ]: 6209 : }
[ + - ]
240 [ + + ]: 2733 : if (result_valid)
241 : : {
242 [ + + ]: 2059 : if (result.isNull())
243 : : {
244 : : // all disjuncts cannot be satisfied, return false
245 [ - + ][ - + ]: 511 : Assert(rc.getKind() == Kind::REGEXP_UNION);
[ - - ]
246 [ + - ]: 1022 : Trace("regexp-ext-rewrite-debug")
247 : 511 : << "...return false" << std::endl;
248 : 1022 : return nm->mkConst(false);
249 : : }
250 : : else
251 : : {
252 [ + - ]: 3096 : Trace("regexp-ext-rewrite-debug")
253 : 0 : << "- same result, try again, children now " << children
254 : 1548 : << std::endl;
255 : : // all branches led to the same result
256 : 1548 : children.pop_back();
257 : 1548 : mchildren.pop_back();
258 [ + + ]: 1548 : if (result != emp_s)
259 : : {
260 : 1242 : mchildren.push_back(result);
261 : : }
262 : 1548 : do_next = true;
263 : : }
264 : : }
265 [ + + ][ + + ]: 3244 : }
266 [ + + ]: 4896 : else if (rc.getKind() == Kind::REGEXP_STAR)
267 : : {
268 : : // check if there is no way that this star can be unrolled even once
269 : 4695 : std::vector<Node> mchildren_s;
270 : 9390 : mchildren_s.insert(
271 : 4695 : mchildren_s.end(), mchildren.begin(), mchildren.end());
272 [ + + ]: 4695 : if (t == 1)
273 : : {
274 : 1949 : std::reverse(mchildren_s.begin(), mchildren_s.end());
275 : : }
276 : 4695 : std::vector<Node> children_s;
277 : 4695 : utils::getConcat(rc[0], children_s);
278 [ + - ]: 9390 : Trace("regexp-ext-rewrite-debug")
279 : 4695 : << "- recursive call on body of star" << std::endl;
280 [ + - ]: 4695 : Trace("regexp-ext-rewrite-debug") << push;
281 : 4695 : Node ret = simpleRegexpConsume(nm, mchildren_s, children_s, t);
282 [ + - ]: 4695 : Trace("regexp-ext-rewrite-debug") << pop;
283 [ + + ]: 4695 : if (!ret.isNull())
284 : : {
285 [ + - ]: 3950 : Trace("regexp-ext-rewrite-debug")
286 : 0 : << "- CRE : regexp star infeasable " << xc << " " << rc
287 : 1975 : << std::endl;
288 : 1975 : children.pop_back();
289 [ + + ]: 1975 : if (!children.empty())
290 : : {
291 [ + - ]: 1297 : Trace("regexp-ext-rewrite-debug") << "- continue" << std::endl;
292 : 1297 : do_next = true;
293 : : }
294 : : }
295 : : else
296 : : {
297 [ + + ]: 2720 : if (children_s.empty())
298 : : {
299 : : // Check if beyond this, we hit a conflict. In this case, we
300 : : // must repeat. Notice that we do not treat the case where
301 : : // there are no more strings to consume as a failure, since
302 : : // we may be within a recursive call, see issue #5510.
303 : 2223 : bool can_skip = true;
304 [ + + ]: 2223 : if (children.size() > 1)
305 : : {
306 : 1808 : std::vector<Node> mchildren_ss;
307 : 3616 : mchildren_ss.insert(
308 : 1808 : mchildren_ss.end(), mchildren.begin(), mchildren.end());
309 : 1808 : std::vector<Node> children_ss;
310 : 3616 : children_ss.insert(
311 : 3616 : children_ss.end(), children.begin(), children.end() - 1);
312 [ + + ]: 1808 : if (t == 1)
313 : : {
314 : 678 : std::reverse(mchildren_ss.begin(), mchildren_ss.end());
315 : 678 : std::reverse(children_ss.begin(), children_ss.end());
316 : : }
317 [ + - ]: 3616 : Trace("regexp-ext-rewrite-debug")
318 : 1808 : << "- recursive call required repeat star" << std::endl;
319 [ + - ]: 1808 : Trace("regexp-ext-rewrite-debug") << push;
320 : : Node rets =
321 : 1808 : simpleRegexpConsume(nm, mchildren_ss, children_ss, t);
322 [ + - ]: 1808 : Trace("regexp-ext-rewrite-debug") << pop;
323 [ + + ]: 1808 : if (!rets.isNull())
324 : : {
325 : 851 : can_skip = false;
326 : : }
327 : 1808 : }
328 [ + + ]: 2223 : if (!can_skip)
329 : : {
330 : 851 : TypeNode stype = nm->stringType();
331 : 851 : Node prev = utils::mkConcat(mchildren, stype);
332 [ + - ]: 1702 : Trace("regexp-ext-rewrite-debug")
333 : 851 : << "- can't skip" << std::endl;
334 : : // take the result of fully consuming once
335 [ + + ]: 851 : if (t == 1)
336 : : {
337 : 415 : std::reverse(mchildren_s.begin(), mchildren_s.end());
338 : : }
339 : 851 : mchildren.clear();
340 : 1702 : mchildren.insert(
341 : 851 : mchildren.end(), mchildren_s.begin(), mchildren_s.end());
342 : 851 : Node curr = utils::mkConcat(mchildren, stype);
343 : 851 : do_next = (prev != curr);
344 [ + - ]: 1702 : Trace("regexp-ext-rewrite-debug")
345 : 851 : << "- do_next = " << do_next << std::endl;
346 : 851 : }
347 : : else
348 : : {
349 [ + - ]: 2744 : Trace("regexp-ext-rewrite-debug")
350 : 1372 : << "- can skip " << rc << " from " << xc << std::endl;
351 : : }
352 : : }
353 : : }
354 : 4695 : }
355 [ + + ][ + ]: 9763 : }
356 [ + + ]: 46124 : if (!do_next)
357 : : {
358 [ + - ]: 72502 : Trace("regexp-ext-rewrite")
359 : 36251 : << "- cannot consume : " << xc << " " << rc << std::endl;
360 : : }
361 [ + + ][ + + ]: 59524 : }
[ + + ]
362 : : }
363 [ + + ]: 67811 : if (dir != 0)
364 : : {
365 : 44555 : std::reverse(children.begin(), children.end());
366 : 44555 : std::reverse(mchildren.begin(), mchildren.end());
367 : : }
368 : : }
369 [ + - ]: 32321 : Trace("regexp-ext-rewrite-debug") << "...finished, return null" << std::endl;
370 : 32321 : return Node::null();
371 : : }
372 : :
373 : 28538 : bool RegExpEntail::isConstRegExp(TNode t)
374 : : {
375 : 28538 : std::unordered_set<TNode> visited;
376 : 28538 : std::vector<TNode> visit;
377 : 28538 : TNode cur;
378 : 28538 : visit.push_back(t);
379 : : do
380 : : {
381 : 89096 : cur = visit.back();
382 : 89096 : visit.pop_back();
383 [ + + ]: 89096 : if (visited.find(cur) == visited.end())
384 : : {
385 : 69981 : visited.insert(cur);
386 : 69981 : Kind ck = cur.getKind();
387 [ + + ]: 69981 : if (ck == Kind::STRING_TO_REGEXP)
388 : : {
389 [ + + ]: 26148 : if (!cur[0].isConst())
390 : : {
391 : 3040 : return false;
392 : : }
393 : : }
394 [ - + ]: 43833 : else if (ck == Kind::REGEXP_RV)
395 : : {
396 : 0 : return false;
397 : : }
398 [ + + ]: 43833 : else if (ck == Kind::REGEXP_RANGE)
399 : : {
400 [ + + ]: 5486 : if (!utils::isCharacterRange(cur))
401 : : {
402 : 16 : return false;
403 : : }
404 : : }
405 [ + + ]: 38347 : else if (!utils::isRegExpKind(ck))
406 : : {
407 : 364 : return false;
408 : : }
409 : : else
410 : : {
411 [ + + ]: 100718 : for (const Node& cn : cur)
412 : : {
413 : 62735 : visit.push_back(cn);
414 : 62735 : }
415 : : }
416 : : }
417 [ + + ]: 85676 : } while (!visit.empty());
418 : 25118 : return true;
419 : 28538 : }
420 : :
421 : 22593 : bool RegExpEntail::testConstStringInRegExp(String& s, TNode r)
422 : : {
423 : 22593 : Kind k = r.getKind();
424 [ + + ][ + + ]: 22593 : if (k == Kind::REGEXP_CONCAT || k == Kind::REGEXP_STAR
425 [ + + ]: 9160 : || k == Kind::REGEXP_UNION)
426 : : {
427 : : // If we can evaluate it via NFA construction, do so. We only do this
428 : : // for compound regular expressions (re.++, re.*, re.union) which may
429 : : // have non-trivial NFA constructions, otherwise the check below will
430 : : // be simpler.
431 [ + + ]: 14249 : if (RegExpEval::canEvaluate(r))
432 : : {
433 : 13081 : return RegExpEval::evaluate(s, r);
434 : : }
435 : : }
436 : 9512 : return testConstStringInRegExpInternal(s, 0, r);
437 : : }
438 : :
439 : 52631 : bool RegExpEntail::testConstStringInRegExpInternal(String& s,
440 : : unsigned index_start,
441 : : TNode r)
442 : : {
443 [ - + ][ - + ]: 52631 : Assert(index_start <= s.size());
[ - - ]
444 [ + - ]: 105262 : Trace("regexp-debug") << "Checking " << s << " in " << r << ", starting at "
445 : 52631 : << index_start << std::endl;
446 [ - + ][ - + ]: 52631 : Assert(!r.isVar());
[ - - ]
447 : 52631 : Kind k = r.getKind();
448 [ + + ][ + + ]: 52631 : switch (k)
[ + + ][ + + ]
[ - + ][ - ]
449 : : {
450 : 21178 : case Kind::STRING_TO_REGEXP:
451 : : {
452 : 21178 : String s2 = s.substr(index_start, s.size() - index_start);
453 [ + - ]: 21178 : if (r[0].isConst())
454 : : {
455 : 21178 : return (s2 == r[0].getConst<String>());
456 : : }
457 : 0 : DebugUnhandled() << "RegExp contains variables";
458 : : return false;
459 : 21178 : }
460 : 3834 : case Kind::REGEXP_CONCAT:
461 : : {
462 [ + + ]: 3834 : if (s.size() != index_start)
463 : : {
464 : 3038 : std::vector<int> vec_k(r.getNumChildren(), -1);
465 : 3038 : int start = 0;
466 : 3038 : int left = (int)s.size() - index_start;
467 : 3038 : int i = 0;
468 [ + - ]: 9365 : while (i < (int)r.getNumChildren())
469 : : {
470 : 9365 : bool flag = true;
471 [ + + ]: 9365 : if (i == (int)r.getNumChildren() - 1)
472 : : {
473 [ + + ]: 1204 : if (testConstStringInRegExpInternal(s, index_start + start, r[i]))
474 : : {
475 : 955 : return true;
476 : : }
477 : : }
478 [ + + ]: 8161 : else if (i == -1)
479 : : {
480 : 2083 : return false;
481 : : }
482 : : else
483 : : {
484 [ + + ]: 21782 : for (vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i])
485 : : {
486 : : cvc5::internal::String t =
487 : 18338 : s.substr(index_start + start, vec_k[i]);
488 [ + + ]: 18338 : if (testConstStringInRegExpInternal(t, 0, r[i]))
489 : : {
490 : 2634 : start += vec_k[i];
491 : 2634 : left -= vec_k[i];
492 : 2634 : flag = false;
493 : 2634 : ++i;
494 : 2634 : vec_k[i] = -1;
495 : 2634 : break;
496 : : }
497 [ + + ]: 18338 : }
498 : : }
499 : :
500 [ + + ]: 6327 : if (flag)
501 : : {
502 : 3693 : --i;
503 [ + + ]: 3693 : if (i >= 0)
504 : : {
505 : 1610 : start -= vec_k[i];
506 : 1610 : left += vec_k[i];
507 : : }
508 : : }
509 : : }
510 : 0 : return false;
511 : 3038 : }
512 : : else
513 : : {
514 [ + - ]: 1074 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
515 : : {
516 [ + + ]: 1074 : if (!testConstStringInRegExpInternal(s, index_start, r[i]))
517 : : {
518 : 796 : return false;
519 : : }
520 : : }
521 : 0 : return true;
522 : : }
523 : : }
524 : 12 : case Kind::REGEXP_UNION:
525 : : {
526 [ + + ]: 33 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
527 : : {
528 [ + + ]: 24 : if (testConstStringInRegExpInternal(s, index_start, r[i]))
529 : : {
530 : 3 : return true;
531 : : }
532 : : }
533 : 9 : return false;
534 : : }
535 : 5189 : case Kind::REGEXP_INTER:
536 : : {
537 [ + + ]: 7388 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
538 : : {
539 [ + + ]: 6529 : if (!testConstStringInRegExpInternal(s, index_start, r[i]))
540 : : {
541 : 4330 : return false;
542 : : }
543 : : }
544 : 859 : return true;
545 : : }
546 : 6020 : case Kind::REGEXP_STAR:
547 : : {
548 [ + + ]: 6020 : if (s.size() != index_start)
549 : : {
550 [ + + ]: 11636 : for (unsigned i = s.size() - index_start; i > 0; --i)
551 : : {
552 : 11548 : cvc5::internal::String t = s.substr(index_start, i);
553 [ + + ]: 11548 : if (testConstStringInRegExpInternal(t, 0, r[0]))
554 : : {
555 : 8718 : if (index_start + i == s.size()
556 [ + + ][ + - ]: 4359 : || testConstStringInRegExpInternal(s, index_start + i, r))
[ + + ][ + - ]
[ - - ]
557 : : {
558 : 4359 : return true;
559 : : }
560 : : }
561 [ + + ]: 11548 : }
562 : 88 : return false;
563 : : }
564 : : else
565 : : {
566 : 1573 : return true;
567 : : }
568 : : }
569 : 64 : case Kind::REGEXP_NONE:
570 : : {
571 : 64 : return false;
572 : : }
573 : 13569 : case Kind::REGEXP_ALLCHAR:
574 : : {
575 [ + + ]: 13569 : if (s.size() == index_start + 1)
576 : : {
577 : 5640 : return true;
578 : : }
579 : : else
580 : : {
581 : 7929 : return false;
582 : : }
583 : : }
584 : 1109 : case Kind::REGEXP_RANGE:
585 : : {
586 [ + + ]: 1109 : if (s.size() == index_start + 1)
587 : : {
588 : 927 : unsigned a = r[0].getConst<String>().front();
589 : 927 : unsigned b = r[1].getConst<String>().front();
590 : 927 : unsigned c = s.back();
591 [ + + ][ + + ]: 927 : return (a <= c && c <= b);
592 : : }
593 : : else
594 : : {
595 : 182 : return false;
596 : : }
597 : : }
598 : 0 : case Kind::REGEXP_LOOP:
599 : : {
600 : 0 : NodeManager* nm = r.getNodeManager();
601 : 0 : uint32_t l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
602 [ - - ]: 0 : if (s.size() == index_start)
603 : : {
604 : 0 : return l == 0 || testConstStringInRegExpInternal(s, index_start, r[0]);
605 : : }
606 : 0 : else if (l == 0 && r[1] == r[2])
607 : : {
608 : 0 : return false;
609 : : }
610 : : else
611 : : {
612 : 0 : Assert(r.getNumChildren() == 3)
613 : 0 : << "String rewriter error: LOOP has 2 children";
614 [ - - ]: 0 : if (l == 0)
615 : : {
616 : : // R{0,u}
617 : 0 : uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
618 [ - - ]: 0 : for (unsigned len = s.size() - index_start; len >= 1; len--)
619 : : {
620 : 0 : cvc5::internal::String t = s.substr(index_start, len);
621 [ - - ]: 0 : if (testConstStringInRegExpInternal(t, 0, r[0]))
622 : : {
623 [ - - ]: 0 : if (len + index_start == s.size())
624 : : {
625 : 0 : return true;
626 : : }
627 : : else
628 : : {
629 : 0 : Node num2 = nm->mkConstInt(cvc5::internal::Rational(u - 1));
630 : 0 : Node r2 = nm->mkNode(Kind::REGEXP_LOOP, r[0], r[1], num2);
631 [ - - ]: 0 : if (testConstStringInRegExpInternal(s, index_start + len, r2))
632 : : {
633 : 0 : return true;
634 : : }
635 [ - - ][ - - ]: 0 : }
636 : : }
637 [ - - ]: 0 : }
638 : 0 : return false;
639 : : }
640 : : else
641 : : {
642 : : // R{l,l}
643 : 0 : Assert(r[1] == r[2])
644 : 0 : << "String rewriter error: LOOP nums are not equal";
645 [ - - ]: 0 : if (l > s.size() - index_start)
646 : : {
647 [ - - ]: 0 : if (testConstStringInRegExpInternal(s, s.size(), r[0]))
648 : : {
649 : 0 : l = s.size() - index_start;
650 : : }
651 : : else
652 : : {
653 : 0 : return false;
654 : : }
655 : : }
656 [ - - ]: 0 : for (unsigned len = 1; len <= s.size() - index_start; len++)
657 : : {
658 : 0 : cvc5::internal::String t = s.substr(index_start, len);
659 [ - - ]: 0 : if (testConstStringInRegExpInternal(t, 0, r[0]))
660 : : {
661 : 0 : Node num2 = nm->mkConstInt(cvc5::internal::Rational(l - 1));
662 : 0 : Node r2 = nm->mkNode(Kind::REGEXP_LOOP, r[0], num2, num2);
663 [ - - ]: 0 : if (testConstStringInRegExpInternal(s, index_start + len, r2))
664 : : {
665 : 0 : return true;
666 : : }
667 [ - - ][ - - ]: 0 : }
668 [ - - ]: 0 : }
669 : 0 : return false;
670 : : }
671 : : }
672 : : }
673 : 1656 : case Kind::REGEXP_COMPLEMENT:
674 : : {
675 : 1656 : return !testConstStringInRegExpInternal(s, index_start, r[0]);
676 : : break;
677 : : }
678 : 0 : default:
679 : : {
680 : 0 : Assert(!utils::isRegExpKind(k));
681 : 0 : return false;
682 : : }
683 : : }
684 : : }
685 : :
686 : 676 : bool RegExpEntail::hasEpsilonNode(TNode node)
687 : : {
688 [ + + ]: 2252 : for (const Node& nc : node)
689 : : {
690 : 1602 : if (nc.getKind() == Kind::STRING_TO_REGEXP && Word::isEmpty(nc[0]))
691 : : {
692 : 26 : return true;
693 : : }
694 [ + + ]: 1602 : }
695 : 650 : return false;
696 : : }
697 : :
698 : 12507 : Node RegExpEntail::getFixedLengthForRegexp(TNode n)
699 : : {
700 : 12507 : NodeManager* nm = n.getNodeManager();
701 : 12507 : Kind k = n.getKind();
702 [ + + ]: 12507 : if (k == Kind::STRING_TO_REGEXP)
703 : : {
704 [ + + ]: 3825 : if (n[0].isConst())
705 : : {
706 : 7366 : return nm->mkConstInt(Rational(Word::getLength(n[0])));
707 : : }
708 : : }
709 [ + + ][ + + ]: 8682 : else if (k == Kind::REGEXP_ALLCHAR || k == Kind::REGEXP_RANGE)
710 : : {
711 : 3662 : return nm->mkConstInt(Rational(1));
712 : : }
713 [ + + ][ + + ]: 6851 : else if (k == Kind::REGEXP_UNION || k == Kind::REGEXP_INTER)
714 : : {
715 : 1169 : Node ret;
716 [ + + ]: 3005 : for (const Node& nc : n)
717 : : {
718 : 2530 : Node flc = getFixedLengthForRegexp(nc);
719 [ + + ][ + + ]: 2530 : if (flc.isNull() || (!ret.isNull() && ret != flc))
[ + + ][ + + ]
720 : : {
721 : 694 : return Node::null();
722 : : }
723 [ + + ]: 1836 : else if (ret.isNull())
724 : : {
725 : : // first time
726 : 1044 : ret = flc;
727 : : }
728 [ + + ][ + + ]: 3224 : }
729 : 475 : return ret;
730 : 1169 : }
731 [ + + ]: 5682 : else if (k == Kind::REGEXP_CONCAT)
732 : : {
733 : 2335 : Rational sum(0);
734 [ + + ]: 4878 : for (const Node& nc : n)
735 : : {
736 : 4304 : Node flc = getFixedLengthForRegexp(nc);
737 [ + + ]: 4304 : if (flc.isNull())
738 : : {
739 : 1761 : return flc;
740 : : }
741 : 2543 : Assert(flc.isConst() && flc.getType().isInteger());
742 : 2543 : sum += flc.getConst<Rational>();
743 [ + + ][ + + ]: 6065 : }
744 : 574 : return nm->mkConstInt(sum);
745 : 2335 : }
746 : 3489 : return Node::null();
747 : : }
748 : :
749 : 83 : Node RegExpEntail::getConstantBoundLengthForRegexp(TNode n, bool isLower) const
750 : : {
751 [ - + ][ - + ]: 83 : Assert(n.getType().isRegExp());
[ - - ]
752 : 83 : Node ret;
753 [ + + ]: 83 : if (getConstantBoundCache(n, isLower, ret))
754 : : {
755 : 27 : return ret;
756 : : }
757 : 56 : Kind k = n.getKind();
758 : 56 : NodeManager* nm = n.getNodeManager();
759 [ + + ]: 56 : if (k == Kind::STRING_TO_REGEXP)
760 : : {
761 : 24 : ret = d_aent.getConstantBoundLength(n[0], isLower);
762 : : }
763 [ + - ][ - + ]: 32 : else if (k == Kind::REGEXP_ALLCHAR || k == Kind::REGEXP_RANGE)
764 : : {
765 : 0 : ret = d_one;
766 : : }
767 [ + + ][ + - ]: 32 : else if (k == Kind::REGEXP_UNION || k == Kind::REGEXP_INTER
768 [ + + ]: 28 : || k == Kind::REGEXP_CONCAT)
769 : : {
770 : 20 : bool success = true;
771 : 20 : bool firstTime = true;
772 : 20 : Rational rr(0);
773 [ + + ]: 54 : for (const Node& nc : n)
774 : : {
775 : 40 : Node bc = getConstantBoundLengthForRegexp(nc, isLower);
776 [ + + ]: 40 : if (bc.isNull())
777 : : {
778 [ + - ][ + - ]: 6 : if (k == Kind::REGEXP_UNION || (k == Kind::REGEXP_CONCAT && !isLower))
[ + - ]
779 : : {
780 : : // since the bound could not be determined on the component, the
781 : : // overall bound is undetermined.
782 : 6 : success = false;
783 : 6 : break;
784 : : }
785 : : else
786 : : {
787 : : // if intersection, or we are computing lower bound for concat
788 : : // and the component cannot be determined, ignore it
789 : 0 : continue;
790 : : }
791 : : }
792 : 34 : Assert(bc.isConst() && bc.getType().isInteger());
793 : 34 : Rational r = bc.getConst<Rational>();
794 [ + + ]: 34 : if (k == Kind::REGEXP_CONCAT)
795 : : {
796 : 26 : rr += r;
797 : : }
798 [ + + ]: 8 : else if (firstTime)
799 : : {
800 : 4 : rr = r;
801 : : }
802 [ + + ]: 4 : else if ((k == Kind::REGEXP_UNION) == isLower)
803 : : {
804 : 2 : rr = std::min(r, rr);
805 : : }
806 : : else
807 : : {
808 : 2 : rr = std::max(r, rr);
809 : : }
810 : 34 : firstTime = false;
811 [ + + ][ - + ]: 46 : }
[ + - ]
812 : : // if we were successful and didn't ignore all components
813 [ + + ][ + - ]: 20 : if (success && !firstTime)
814 : : {
815 : 14 : ret = nm->mkConstInt(rr);
816 : : }
817 : 20 : }
818 [ + + ][ + + ]: 56 : if (ret.isNull() && isLower)
[ + + ]
819 : : {
820 : 6 : ret = d_zero;
821 : : }
822 [ + - ]: 112 : Trace("strings-rentail") << "getConstantBoundLengthForRegexp: " << n
823 : 0 : << ", isLower=" << isLower << " returns " << ret
824 : 56 : << std::endl;
825 : 56 : setConstantBoundCache(n, ret, isLower);
826 : 56 : return ret;
827 : 0 : }
828 : :
829 : 26374 : bool RegExpEntail::regExpIncludes(Node r1,
830 : : Node r2,
831 : : std::map<std::pair<Node, Node>, bool>& cache)
832 : : {
833 [ + + ]: 26374 : if (r1 == r2)
834 : : {
835 : 3598 : return true;
836 : : }
837 : 22776 : std::pair<Node, Node> key = std::make_pair(r1, r2);
838 : 22776 : const auto& it = cache.find(key);
839 [ + + ]: 22776 : if (it != cache.end())
840 : : {
841 : 5940 : return (*it).second;
842 : : }
843 : : // first, check some basic inclusions
844 : 16836 : bool ret = false;
845 : 16836 : Kind k2 = r2.getKind();
846 : : // if the right hand side is a constant string, this is a membership test
847 [ + + ]: 16836 : if (k2 == Kind::STRING_TO_REGEXP)
848 : : {
849 : : // only check if r1 is a constant regular expression
850 : 4906 : if (r2[0].isConst() && isConstRegExp(r1))
851 : : {
852 : 4136 : String s = r2[0].getConst<String>();
853 : 4136 : ret = testConstStringInRegExp(s, r1);
854 : 4136 : }
855 : 4906 : cache[key] = ret;
856 : 4906 : return ret;
857 : : }
858 : 11930 : Kind k1 = r1.getKind();
859 : 11930 : bool retSet = false;
860 [ + + ]: 11930 : if (k1 == Kind::REGEXP_UNION)
861 : : {
862 : 1181 : retSet = true;
863 : : // if any component of r1 includes r2, return true
864 [ + + ]: 4085 : for (const Node& r : r1)
865 : : {
866 [ + + ]: 2948 : if (regExpIncludes(r, r2, cache))
867 : : {
868 : 44 : ret = true;
869 : 44 : break;
870 : : }
871 [ + + ]: 2948 : }
872 : : }
873 [ + + ][ + - ]: 11930 : if (k2 == Kind::REGEXP_INTER && !ret)
874 : : {
875 : 23 : retSet = true;
876 : : // if r1 includes any component of r2, return true
877 [ + + ]: 63 : for (const Node& r : r2)
878 : : {
879 [ + + ]: 43 : if (regExpIncludes(r1, r, cache))
880 : : {
881 : 3 : ret = true;
882 : 3 : break;
883 : : }
884 [ + + ]: 43 : }
885 : : }
886 [ + + ]: 11930 : if (k1 == Kind::REGEXP_STAR)
887 : : {
888 : 2491 : retSet = true;
889 : : // inclusion if r1 is (re.* re.allchar), or if the body of r1 includes r2
890 : : // (or the body of r2 if it is also a star).
891 [ + + ]: 2491 : if (r1[0].getKind() == Kind::REGEXP_ALLCHAR)
892 : : {
893 : 239 : ret = true;
894 : : }
895 : : else
896 : : {
897 [ + + ]: 2252 : ret = regExpIncludes(r1[0], k2 == Kind::REGEXP_STAR ? r2[0] : r2, cache);
898 : : }
899 : : }
900 [ + + ]: 9439 : else if (k1 == Kind::STRING_TO_REGEXP)
901 : : {
902 : : // only way to include is if equal, which was already checked
903 : 4102 : retSet = true;
904 : : }
905 [ + + ][ + - ]: 5337 : else if (k1 == Kind::REGEXP_RANGE && utils::isCharacterRange(r1))
[ + + ][ + + ]
[ - - ]
906 : : {
907 : 281 : retSet = true;
908 : : // if comparing subranges, we check inclusion of interval
909 [ + + ][ + - ]: 281 : if (k2 == Kind::REGEXP_RANGE && utils::isCharacterRange(r2))
[ + + ][ + + ]
[ - - ]
910 : : {
911 : 40 : unsigned l1 = r1[0].getConst<String>().front();
912 : 40 : unsigned u1 = r1[1].getConst<String>().front();
913 : 40 : unsigned l2 = r2[0].getConst<String>().front();
914 : 40 : unsigned u2 = r2[1].getConst<String>().front();
915 [ + - ][ + - ]: 40 : ret = l1 <= l2 && l2 <= u1 && l1 <= u2 && u2 <= u1;
[ + - ][ + + ]
916 : : }
917 : : }
918 [ + + ]: 11930 : if (retSet)
919 : : {
920 : 8055 : cache[key] = ret;
921 : 8055 : return ret;
922 : : }
923 : : // avoid infinite loop
924 : 3875 : cache[key] = false;
925 : 3875 : NodeManager* nm = r1.getNodeManager();
926 : 3875 : Node sigma = nm->mkNode(Kind::REGEXP_ALLCHAR, std::vector<Node>{});
927 : 3875 : Node sigmaStar = nm->mkNode(Kind::REGEXP_STAR, sigma);
928 : :
929 : 3875 : std::vector<Node> v1, v2;
930 : 3875 : utils::getRegexpComponents(r1, v1);
931 : 3875 : utils::getRegexpComponents(r2, v2);
932 : :
933 : : // In the following, we iterate over `r2` (the "includee") and try to
934 : : // match it with `r1`. `idxs`/`newIdxs` keep track of all the possible
935 : : // positions in `r1` that we could currently be at.
936 : 3875 : std::unordered_set<size_t> newIdxs = {0};
937 : 3875 : std::unordered_set<size_t> idxs;
938 [ + + ]: 8875 : for (const Node& n2 : v2)
939 : : {
940 : : // Transfer elements from `newIdxs` to `idxs`. Out-of-bound indices are
941 : : // removed and for (re.* re.allchar), we additionally include the option of
942 : : // skipping it. Indices must be smaller than the size of `v1`.
943 : 8118 : idxs.clear();
944 [ + + ]: 23339 : for (size_t idx : newIdxs)
945 : : {
946 [ + + ]: 15221 : if (idx < v1.size())
947 : : {
948 : 14995 : idxs.insert(idx);
949 [ + + ][ + + ]: 14995 : if (idx + 1 < v1.size() && v1[idx] == sigmaStar)
[ + + ]
950 : : {
951 [ + - ][ + - ]: 4240 : Assert(idx + 1 == v1.size() || v1[idx + 1] != sigmaStar);
[ - + ][ - + ]
[ - - ]
952 : 4240 : idxs.insert(idx + 1);
953 : : }
954 : : }
955 : : }
956 : 8118 : newIdxs.clear();
957 : :
958 [ + + ]: 23948 : for (size_t idx : idxs)
959 : : {
960 [ + + ]: 15830 : if (regExpIncludes(v1[idx], n2, cache))
961 : : {
962 : : // If this component includes n2, then we can consume it.
963 : 8578 : newIdxs.insert(idx + 1);
964 : : }
965 [ + + ]: 15830 : if (v1[idx] == sigmaStar)
966 : : {
967 : : // (re.* re.allchar) can match an arbitrary amount of `r2`
968 : 4505 : newIdxs.insert(idx);
969 : : }
970 [ + + ]: 11325 : else if (utils::isUnboundedWildcard(v1, idx))
971 : : {
972 : : // If a series of re.allchar is followed by (re.* re.allchar), we
973 : : // can decide not to "waste" the re.allchar because the order of
974 : : // the two wildcards is not observable (i.e. it does not change
975 : : // the sequences matched by the regular expression)
976 : 2188 : newIdxs.insert(idx);
977 : : }
978 : : }
979 : :
980 [ + + ]: 8118 : if (newIdxs.empty())
981 : : {
982 : : // If there are no candidates, we can't match the remainder of r2
983 : 3118 : break;
984 : : }
985 : : }
986 : :
987 : : // We have processed all of `r2`. We are now looking if there was also a
988 : : // path to the end in `r1`. This makes sure that we don't have leftover
989 : : // bits in `r1` that don't match anything in `r2`.
990 : 3875 : bool result = false;
991 [ + + ]: 6132 : for (size_t idx : newIdxs)
992 : : {
993 [ + + ][ + + ]: 2567 : if (idx == v1.size() || (idx == v1.size() - 1 && v1[idx] == sigmaStar))
[ + + ][ + + ]
994 : : {
995 : 310 : result = true;
996 : 310 : break;
997 : : }
998 : : }
999 : 3875 : cache[key] = result;
1000 : 3875 : return result;
1001 : 22776 : }
1002 : :
1003 : 3566 : bool RegExpEntail::regExpIncludes(Node r1, Node r2)
1004 : : {
1005 : 3566 : std::map<std::pair<Node, Node>, bool> cache;
1006 : 7132 : return regExpIncludes(r1, r2, cache);
1007 : 3566 : }
1008 : :
1009 : 58870 : Node RegExpEntail::getGeneralizedConstRegExp(const Node& n)
1010 : : {
1011 [ - + ][ - + ]: 58870 : Assert(n.getType().isString());
[ - - ]
1012 : 58870 : NodeManager* nm = n.getNodeManager();
1013 : 58870 : std::vector<Node> ncs;
1014 [ + + ]: 58870 : if (n.getKind() == Kind::STRING_CONCAT)
1015 : : {
1016 : 7675 : ncs.insert(ncs.end(), n.begin(), n.end());
1017 : : }
1018 : : else
1019 : : {
1020 : 51195 : ncs.push_back(n);
1021 : : }
1022 : 58870 : bool nonTrivial = false;
1023 : : Node sigmaStar =
1024 : 117740 : nm->mkNode(Kind::REGEXP_STAR, nm->mkNode(Kind::REGEXP_ALLCHAR));
1025 : 58870 : std::vector<Node> rs;
1026 [ + + ]: 135219 : for (const Node& nc : ncs)
1027 : : {
1028 : 76349 : Node re = sigmaStar;
1029 [ + + ]: 76349 : if (nc.isConst())
1030 : : {
1031 : 9335 : nonTrivial = true;
1032 : 9335 : re = nm->mkNode(Kind::STRING_TO_REGEXP, nc);
1033 : : }
1034 [ + + ]: 67014 : else if (nc.getKind() == Kind::STRING_ITOS)
1035 : : {
1036 : 1171 : nonTrivial = true;
1037 : : Node digRange =
1038 : 3513 : nm->mkNode(Kind::REGEXP_RANGE,
1039 : 2342 : {nm->mkConst(String("0")), nm->mkConst(String("9"))});
1040 : 1171 : re = nm->mkNode(Kind::REGEXP_STAR, digRange);
1041 : : // maybe non-empty digit range?
1042 : : // relies on RARE rule str-in-re-from-int-dig-range to prove
1043 [ + + ]: 1171 : if (d_aent.check(nc[0]))
1044 : : {
1045 : 389 : re = nm->mkNode(Kind::REGEXP_CONCAT, digRange, re);
1046 : : }
1047 : 1171 : }
1048 : 76349 : rs.push_back(re);
1049 : 76349 : }
1050 [ + + ]: 58870 : if (nonTrivial)
1051 : : {
1052 [ + + ]: 7704 : return rs.size() == 1 ? rs[0] : nm->mkNode(Kind::REGEXP_CONCAT, rs);
1053 : : }
1054 : 51166 : return Node::null();
1055 : 58870 : }
1056 : :
1057 : : struct RegExpEntailConstantBoundLowerId
1058 : : {
1059 : : };
1060 : : typedef expr::Attribute<RegExpEntailConstantBoundLowerId, Node>
1061 : : RegExpEntailConstantBoundLower;
1062 : :
1063 : : struct RegExpEntailConstantBoundUpperId
1064 : : {
1065 : : };
1066 : : typedef expr::Attribute<RegExpEntailConstantBoundUpperId, Node>
1067 : : RegExpEntailConstantBoundUpper;
1068 : :
1069 : 56 : void RegExpEntail::setConstantBoundCache(TNode n, Node ret, bool isLower)
1070 : : {
1071 [ + + ]: 56 : if (isLower)
1072 : : {
1073 : : RegExpEntailConstantBoundLower rcbl;
1074 : 28 : n.setAttribute(rcbl, ret);
1075 : : }
1076 : : else
1077 : : {
1078 : : RegExpEntailConstantBoundUpper rcbu;
1079 : 28 : n.setAttribute(rcbu, ret);
1080 : : }
1081 : 56 : }
1082 : :
1083 : 83 : bool RegExpEntail::getConstantBoundCache(TNode n, bool isLower, Node& c)
1084 : : {
1085 [ + + ]: 83 : if (isLower)
1086 : : {
1087 : : RegExpEntailConstantBoundLower rcbl;
1088 [ + + ]: 52 : if (n.hasAttribute(rcbl))
1089 : : {
1090 : 24 : c = n.getAttribute(rcbl);
1091 : 24 : return true;
1092 : : }
1093 : : }
1094 : : else
1095 : : {
1096 : : RegExpEntailConstantBoundUpper rcbu;
1097 [ + + ]: 31 : if (n.hasAttribute(rcbu))
1098 : : {
1099 : 3 : c = n.getAttribute(rcbu);
1100 : 3 : return true;
1101 : : }
1102 : : }
1103 : 56 : return false;
1104 : : }
1105 : :
1106 : : } // namespace strings
1107 : : } // namespace theory
1108 : : } // namespace cvc5::internal
|
