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 : 103886 : RegExpEntail::RegExpEntail(NodeManager* nm, Rewriter* r) : d_aent(nm, r)
30 : : {
31 : 103886 : d_zero = nm->mkConstInt(Rational(0));
32 : 103886 : d_one = nm->mkConstInt(Rational(1));
33 : 103886 : }
34 : :
35 : 32768 : Node RegExpEntail::simpleRegexpConsume(NodeManager* nm,
36 : : std::vector<Node>& mchildren,
37 : : std::vector<Node>& children,
38 : : int dir)
39 : : {
40 [ + - ]: 65536 : Trace("regexp-ext-rewrite-debug")
41 : 32768 : << "Simple reg exp consume, dir=" << dir << ":" << std::endl;
42 : 32768 : unsigned tmin = dir < 0 ? 0 : dir;
43 [ + + ]: 32768 : unsigned tmax = dir < 0 ? 1 : dir;
44 : : // try to remove off front and back
45 [ + + ]: 89187 : for (unsigned t = 0; t < 2; t++)
46 : : {
47 [ + + ][ + + ]: 62415 : if (tmin <= t && t <= tmax)
48 : : {
49 [ + - ]: 82540 : Trace("regexp-ext-rewrite-debug")
50 : 41270 : << "Run consume, direction is " << t << " with:" << std::endl;
51 [ + - ]: 82540 : Trace("regexp-ext-rewrite-debug")
52 : 41270 : << " mchildren : " << mchildren << std::endl;
53 [ + - ]: 82540 : Trace("regexp-ext-rewrite-debug")
54 : 41270 : << " children : " << children << std::endl;
55 : 41270 : bool do_next = true;
56 [ + + ][ + + ]: 80109 : while (!children.empty() && !mchildren.empty() && do_next)
[ + + ][ + + ]
57 : : {
58 : 44843 : do_next = false;
59 : 44843 : Node xc = mchildren[mchildren.size() - 1];
60 : 44843 : Node rc = children[children.size() - 1];
61 [ + - ]: 89686 : Trace("regexp-ext-rewrite-debug")
62 : 44843 : << "* " << xc << " in " << rc << std::endl;
63 [ - + ][ - + ]: 44843 : Assert(rc.getKind() != Kind::REGEXP_CONCAT);
[ - - ]
64 [ - + ][ - + ]: 44843 : Assert(xc.getKind() != Kind::STRING_CONCAT);
[ - - ]
65 [ + + ]: 44843 : if (rc.getKind() == Kind::STRING_TO_REGEXP)
66 : : {
67 : 19176 : std::vector<Node> childrenc;
68 : 19176 : utils::getConcat(rc[0], childrenc);
69 [ + + ]: 19176 : size_t cindex = t == 1 ? 0 : childrenc.size() - 1;
70 : 19176 : Node rcc = childrenc[cindex];
71 : 19176 : Node remStr;
72 [ + + ]: 19176 : if (xc == rcc)
73 : : {
74 : 1970 : mchildren.pop_back();
75 : 1970 : do_next = true;
76 [ + - ]: 1970 : Trace("regexp-ext-rewrite-debug") << "- strip equal" << std::endl;
77 : : }
78 [ + + ][ + + ]: 17206 : else if (rcc.isConst() && Word::isEmpty(rcc))
[ + + ][ + + ]
[ - - ]
79 : : {
80 [ + - ]: 816 : Trace("regexp-ext-rewrite-debug")
81 : 408 : << "- ignore empty RE" << std::endl;
82 : : // ignore and continue
83 : 408 : do_next = true;
84 : : }
85 [ + + ][ + + ]: 16798 : else if (xc.isConst() && rcc.isConst())
[ + + ]
86 : : {
87 : : // split the constant
88 : : size_t index;
89 : 6461 : remStr = Word::splitConstant(xc, rcc, index, t == 0);
90 [ + - ]: 12922 : Trace("regexp-ext-rewrite-debug")
91 : 0 : << "- CRE: Regexp const split : " << xc << " " << rcc << " -> "
92 : 6461 : << remStr << " " << index << " " << t << std::endl;
93 [ + + ]: 6461 : if (remStr.isNull())
94 : : {
95 [ + - ]: 10182 : Trace("regexp-ext-rewrite-debug")
96 : 5091 : << "...return false" << std::endl;
97 : 10182 : return nm->mkConst(false);
98 : : }
99 : : else
100 : : {
101 [ + - ]: 2740 : Trace("regexp-ext-rewrite-debug")
102 : 1370 : << "- strip equal const" << std::endl;
103 : 1370 : mchildren.pop_back();
104 [ + + ]: 1370 : if (index == 0)
105 : : {
106 : 1142 : mchildren.push_back(remStr);
107 : : // we've processed the remainder as leftover for the LHS
108 : : // string, clear it now
109 : 1142 : remStr = Node::null();
110 : : }
111 : : // otherwise remStr is processed below
112 : : }
113 [ + - ]: 1370 : Trace("regexp-ext-rewrite-debug") << "- split const" << std::endl;
114 : 1370 : do_next = true;
115 : : }
116 [ + + ]: 14085 : if (do_next)
117 : : {
118 [ + + ]: 3748 : if (remStr.isNull())
119 : : {
120 : : // we have fully processed the component
121 : 3520 : childrenc.erase(childrenc.begin() + cindex);
122 : : }
123 : : else
124 : : {
125 : : // we have a remainder
126 : 228 : childrenc[cindex] = remStr;
127 : : }
128 [ + + ]: 3748 : if (childrenc.empty())
129 : : {
130 : : // if childrenc is empty, we are done with the current str.to_re
131 : 3449 : children.pop_back();
132 : : }
133 : : else
134 : : {
135 : : // otherwise we reconstruct it
136 : 299 : TypeNode stype = nm->stringType();
137 : 598 : children[children.size() - 1] = nm->mkNode(
138 : 897 : Kind::STRING_TO_REGEXP, utils::mkConcat(childrenc, stype));
139 : 299 : }
140 : : }
141 [ + + ][ + + ]: 29358 : }
[ + + ]
142 [ + + ]: 25667 : else if (xc.isConst())
143 : : {
144 : : // check for constants
145 : 8683 : cvc5::internal::String s = xc.getConst<String>();
146 [ + + ]: 8683 : if (Word::isEmpty(xc))
147 : : {
148 [ + - ]: 454 : Trace("regexp-ext-rewrite-debug") << "- ignore empty" << std::endl;
149 : : // ignore and continue
150 : 454 : mchildren.pop_back();
151 : 454 : do_next = true;
152 : : }
153 : 8229 : else if (rc.getKind() == Kind::REGEXP_RANGE
154 [ + + ][ + + ]: 8229 : || rc.getKind() == Kind::REGEXP_ALLCHAR)
[ + + ]
155 : : {
156 [ + + ]: 1440 : if (!isConstRegExp(rc))
157 : : {
158 : : // if a non-standard re.range term, abort
159 : 8 : break;
160 : : }
161 : 1432 : std::vector<unsigned> ssVec;
162 [ + + ]: 1432 : ssVec.push_back(t == 0 ? s.back() : s.front());
163 : 1432 : cvc5::internal::String ss(ssVec);
164 [ + + ]: 1432 : if (testConstStringInRegExp(ss, rc))
165 : : {
166 : : // strip off one character
167 : 968 : mchildren.pop_back();
168 [ + + ]: 968 : if (s.size() > 1)
169 : : {
170 [ + + ]: 721 : if (t == 0)
171 : : {
172 : 472 : mchildren.push_back(nm->mkConst(s.substr(0, s.size() - 1)));
173 : : }
174 : : else
175 : : {
176 : 249 : mchildren.push_back(nm->mkConst(s.substr(1)));
177 : : }
178 : : }
179 : 968 : children.pop_back();
180 : 968 : do_next = true;
181 : : }
182 : : else
183 : : {
184 [ + - ]: 928 : Trace("regexp-ext-rewrite-debug")
185 : 464 : << "...return false" << std::endl;
186 : 928 : return nm->mkConst(false);
187 : : }
188 [ + + ][ + + ]: 1896 : }
189 : 6789 : else if (rc.getKind() == Kind::REGEXP_INTER
190 [ + + ][ + + ]: 6789 : || rc.getKind() == Kind::REGEXP_UNION)
[ + + ]
191 : : {
192 : : // see if any/each child does not work
193 : 2416 : bool result_valid = true;
194 : 2416 : Node result;
195 : 2416 : Node emp_s = nm->mkConst(String(""));
196 [ + + ]: 8007 : for (unsigned i = 0; i < rc.getNumChildren(); i++)
197 : : {
198 : 5591 : std::vector<Node> mchildren_s;
199 : 5591 : std::vector<Node> children_s;
200 : 5591 : mchildren_s.push_back(xc);
201 : 5591 : utils::getConcat(rc[i], children_s);
202 [ + - ]: 5591 : Trace("regexp-ext-rewrite-debug") << push;
203 : 5591 : Node ret = simpleRegexpConsume(nm, mchildren_s, children_s, t);
204 [ + - ]: 5591 : Trace("regexp-ext-rewrite-debug") << pop;
205 [ + + ]: 5591 : if (!ret.isNull())
206 : : {
207 : : // one conjunct cannot be satisfied, return false
208 [ - + ]: 2991 : 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 [ + + ]: 2600 : if (children_s.empty())
218 : : {
219 : : // if we were able to fully consume, store the result
220 [ - + ][ - + ]: 1706 : Assert(mchildren_s.size() <= 1);
[ - - ]
221 [ + + ]: 1706 : if (mchildren_s.empty())
222 : : {
223 : 306 : mchildren_s.push_back(emp_s);
224 : : }
225 [ + + ]: 1706 : if (result.isNull())
226 : : {
227 : 1404 : result = mchildren_s[0];
228 : : }
229 [ + + ]: 302 : else if (result != mchildren_s[0])
230 : : {
231 : 22 : result_valid = false;
232 : : }
233 : : }
234 : : else
235 : : {
236 : 894 : result_valid = false;
237 : : }
238 : : }
239 [ + - ][ + - ]: 5591 : }
[ + - ]
240 [ + + ]: 2416 : if (result_valid)
241 : : {
242 [ + + ]: 1699 : if (result.isNull())
243 : : {
244 : : // all disjuncts cannot be satisfied, return false
245 [ - + ][ - + ]: 441 : Assert(rc.getKind() == Kind::REGEXP_UNION);
[ - - ]
246 [ + - ]: 882 : Trace("regexp-ext-rewrite-debug")
247 : 441 : << "...return false" << std::endl;
248 : 882 : return nm->mkConst(false);
249 : : }
250 : : else
251 : : {
252 [ + - ]: 2516 : Trace("regexp-ext-rewrite-debug")
253 : 0 : << "- same result, try again, children now " << children
254 : 1258 : << std::endl;
255 : : // all branches led to the same result
256 : 1258 : children.pop_back();
257 : 1258 : mchildren.pop_back();
258 [ + + ]: 1258 : if (result != emp_s)
259 : : {
260 : 978 : mchildren.push_back(result);
261 : : }
262 : 1258 : do_next = true;
263 : : }
264 : : }
265 [ + + ][ + + ]: 2857 : }
266 [ + + ]: 4373 : else if (rc.getKind() == Kind::REGEXP_STAR)
267 : : {
268 : : // check if there is no way that this star can be unrolled even once
269 : 4173 : std::vector<Node> mchildren_s;
270 : 8346 : mchildren_s.insert(
271 : 4173 : mchildren_s.end(), mchildren.begin(), mchildren.end());
272 [ + + ]: 4173 : if (t == 1)
273 : : {
274 : 1744 : std::reverse(mchildren_s.begin(), mchildren_s.end());
275 : : }
276 : 4173 : std::vector<Node> children_s;
277 : 4173 : utils::getConcat(rc[0], children_s);
278 [ + - ]: 8346 : Trace("regexp-ext-rewrite-debug")
279 : 4173 : << "- recursive call on body of star" << std::endl;
280 [ + - ]: 4173 : Trace("regexp-ext-rewrite-debug") << push;
281 : 4173 : Node ret = simpleRegexpConsume(nm, mchildren_s, children_s, t);
282 [ + - ]: 4173 : Trace("regexp-ext-rewrite-debug") << pop;
283 [ + + ]: 4173 : if (!ret.isNull())
284 : : {
285 [ + - ]: 3732 : Trace("regexp-ext-rewrite-debug")
286 : 0 : << "- CRE : regexp star infeasable " << xc << " " << rc
287 : 1866 : << std::endl;
288 : 1866 : children.pop_back();
289 [ + + ]: 1866 : if (!children.empty())
290 : : {
291 [ + - ]: 1219 : Trace("regexp-ext-rewrite-debug") << "- continue" << std::endl;
292 : 1219 : do_next = true;
293 : : }
294 : : }
295 : : else
296 : : {
297 [ + + ]: 2307 : 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 : 1800 : bool can_skip = true;
304 [ + + ]: 1800 : if (children.size() > 1)
305 : : {
306 : 1426 : std::vector<Node> mchildren_ss;
307 : 2852 : mchildren_ss.insert(
308 : 1426 : mchildren_ss.end(), mchildren.begin(), mchildren.end());
309 : 1426 : std::vector<Node> children_ss;
310 : 2852 : children_ss.insert(
311 : 2852 : children_ss.end(), children.begin(), children.end() - 1);
312 [ + + ]: 1426 : if (t == 1)
313 : : {
314 : 561 : std::reverse(mchildren_ss.begin(), mchildren_ss.end());
315 : 561 : std::reverse(children_ss.begin(), children_ss.end());
316 : : }
317 [ + - ]: 2852 : Trace("regexp-ext-rewrite-debug")
318 : 1426 : << "- recursive call required repeat star" << std::endl;
319 [ + - ]: 1426 : Trace("regexp-ext-rewrite-debug") << push;
320 : : Node rets =
321 : 1426 : simpleRegexpConsume(nm, mchildren_ss, children_ss, t);
322 [ + - ]: 1426 : Trace("regexp-ext-rewrite-debug") << pop;
323 [ + + ]: 1426 : if (!rets.isNull())
324 : : {
325 : 702 : can_skip = false;
326 : : }
327 : 1426 : }
328 [ + + ]: 1800 : if (!can_skip)
329 : : {
330 : 702 : TypeNode stype = nm->stringType();
331 : 702 : Node prev = utils::mkConcat(mchildren, stype);
332 [ + - ]: 1404 : Trace("regexp-ext-rewrite-debug")
333 : 702 : << "- can't skip" << std::endl;
334 : : // take the result of fully consuming once
335 [ + + ]: 702 : if (t == 1)
336 : : {
337 : 353 : std::reverse(mchildren_s.begin(), mchildren_s.end());
338 : : }
339 : 702 : mchildren.clear();
340 : 1404 : mchildren.insert(
341 : 702 : mchildren.end(), mchildren_s.begin(), mchildren_s.end());
342 : 702 : Node curr = utils::mkConcat(mchildren, stype);
343 : 702 : do_next = (prev != curr);
344 [ + - ]: 1404 : Trace("regexp-ext-rewrite-debug")
345 : 702 : << "- do_next = " << do_next << std::endl;
346 : 702 : }
347 : : else
348 : : {
349 [ + - ]: 2196 : Trace("regexp-ext-rewrite-debug")
350 : 1098 : << "- can skip " << rc << " from " << xc << std::endl;
351 : : }
352 : : }
353 : : }
354 : 4173 : }
355 [ + + ][ + ]: 8683 : }
356 [ + + ]: 38839 : if (!do_next)
357 : : {
358 [ + - ]: 60980 : Trace("regexp-ext-rewrite")
359 : 30490 : << "- cannot consume : " << xc << " " << rc << std::endl;
360 : : }
361 [ + + ][ + + ]: 50847 : }
[ + + ]
362 : : }
363 [ + + ]: 56419 : if (dir != 0)
364 : : {
365 : 38011 : std::reverse(children.begin(), children.end());
366 : 38011 : std::reverse(mchildren.begin(), mchildren.end());
367 : : }
368 : : }
369 [ + - ]: 26772 : Trace("regexp-ext-rewrite-debug") << "...finished, return null" << std::endl;
370 : 26772 : return Node::null();
371 : : }
372 : :
373 : 24156 : bool RegExpEntail::isConstRegExp(TNode t)
374 : : {
375 : 24156 : std::unordered_set<TNode> visited;
376 : 24156 : std::vector<TNode> visit;
377 : 24156 : TNode cur;
378 : 24156 : visit.push_back(t);
379 : : do
380 : : {
381 : 74455 : cur = visit.back();
382 : 74455 : visit.pop_back();
383 [ + + ]: 74455 : if (visited.find(cur) == visited.end())
384 : : {
385 : 61226 : visited.insert(cur);
386 : 61226 : Kind ck = cur.getKind();
387 [ + + ]: 61226 : if (ck == Kind::STRING_TO_REGEXP)
388 : : {
389 [ + + ]: 23592 : if (!cur[0].isConst())
390 : : {
391 : 2710 : return false;
392 : : }
393 : : }
394 [ - + ]: 37634 : else if (ck == Kind::REGEXP_RV)
395 : : {
396 : 0 : return false;
397 : : }
398 [ + + ]: 37634 : else if (ck == Kind::REGEXP_RANGE)
399 : : {
400 [ + + ]: 4593 : if (!utils::isCharacterRange(cur))
401 : : {
402 : 16 : return false;
403 : : }
404 : : }
405 [ + + ]: 33041 : else if (!utils::isRegExpKind(ck))
406 : : {
407 : 326 : return false;
408 : : }
409 : : else
410 : : {
411 [ + + ]: 85079 : for (const Node& cn : cur)
412 : : {
413 : 52364 : visit.push_back(cn);
414 : 52364 : }
415 : : }
416 : : }
417 [ + + ]: 71403 : } while (!visit.empty());
418 : 21104 : return true;
419 : 24156 : }
420 : :
421 : 19814 : bool RegExpEntail::testConstStringInRegExp(String& s, TNode r)
422 : : {
423 : 19814 : Kind k = r.getKind();
424 [ + + ][ + + ]: 19814 : if (k == Kind::REGEXP_CONCAT || k == Kind::REGEXP_STAR
425 [ + + ]: 7833 : || 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 [ + + ]: 12724 : if (RegExpEval::canEvaluate(r))
432 : : {
433 : 11631 : return RegExpEval::evaluate(s, r);
434 : : }
435 : : }
436 : 8183 : return testConstStringInRegExpInternal(s, 0, r);
437 : : }
438 : :
439 : 47970 : bool RegExpEntail::testConstStringInRegExpInternal(String& s,
440 : : unsigned index_start,
441 : : TNode r)
442 : : {
443 [ - + ][ - + ]: 47970 : Assert(index_start <= s.size());
[ - - ]
444 [ + - ]: 95940 : Trace("regexp-debug") << "Checking " << s << " in " << r << ", starting at "
445 : 47970 : << index_start << std::endl;
446 [ - + ][ - + ]: 47970 : Assert(!r.isVar());
[ - - ]
447 : 47970 : Kind k = r.getKind();
448 [ + + ][ + + ]: 47970 : switch (k)
[ + + ][ + + ]
[ - + ][ - ]
449 : : {
450 : 19229 : case Kind::STRING_TO_REGEXP:
451 : : {
452 : 19229 : String s2 = s.substr(index_start, s.size() - index_start);
453 [ + - ]: 19229 : if (r[0].isConst())
454 : : {
455 : 19229 : return (s2 == r[0].getConst<String>());
456 : : }
457 : 0 : DebugUnhandled() << "RegExp contains variables";
458 : : return false;
459 : 19229 : }
460 : 3427 : case Kind::REGEXP_CONCAT:
461 : : {
462 [ + + ]: 3427 : if (s.size() != index_start)
463 : : {
464 : 2711 : std::vector<int> vec_k(r.getNumChildren(), -1);
465 : 2711 : int start = 0;
466 : 2711 : int left = (int)s.size() - index_start;
467 : 2711 : int i = 0;
468 [ + - ]: 8663 : while (i < (int)r.getNumChildren())
469 : : {
470 : 8663 : bool flag = true;
471 [ + + ]: 8663 : if (i == (int)r.getNumChildren() - 1)
472 : : {
473 [ + + ]: 1043 : if (testConstStringInRegExpInternal(s, index_start + start, r[i]))
474 : : {
475 : 818 : return true;
476 : : }
477 : : }
478 [ + + ]: 7620 : else if (i == -1)
479 : : {
480 : 1893 : return false;
481 : : }
482 : : else
483 : : {
484 [ + + ]: 20020 : for (vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i])
485 : : {
486 : 16766 : cvc5::internal::String t = s.substr(index_start + start, vec_k[i]);
487 [ + + ]: 16766 : if (testConstStringInRegExpInternal(t, 0, r[i]))
488 : : {
489 : 2473 : start += vec_k[i];
490 : 2473 : left -= vec_k[i];
491 : 2473 : flag = false;
492 : 2473 : ++i;
493 : 2473 : vec_k[i] = -1;
494 : 2473 : break;
495 : : }
496 [ + + ]: 16766 : }
497 : : }
498 : :
499 [ + + ]: 5952 : if (flag)
500 : : {
501 : 3479 : --i;
502 [ + + ]: 3479 : if (i >= 0)
503 : : {
504 : 1586 : start -= vec_k[i];
505 : 1586 : left += vec_k[i];
506 : : }
507 : : }
508 : : }
509 : 0 : return false;
510 : 2711 : }
511 : : else
512 : : {
513 [ + - ]: 998 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
514 : : {
515 [ + + ]: 998 : if (!testConstStringInRegExpInternal(s, index_start, r[i]))
516 : : {
517 : 716 : return false;
518 : : }
519 : : }
520 : 0 : return true;
521 : : }
522 : : }
523 : 12 : case Kind::REGEXP_UNION:
524 : : {
525 [ + + ]: 33 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
526 : : {
527 [ + + ]: 24 : if (testConstStringInRegExpInternal(s, index_start, r[i]))
528 : : {
529 : 3 : return true;
530 : : }
531 : : }
532 : 9 : return false;
533 : : }
534 : 4858 : case Kind::REGEXP_INTER:
535 : : {
536 [ + + ]: 6786 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
537 : : {
538 [ + + ]: 6047 : if (!testConstStringInRegExpInternal(s, index_start, r[i]))
539 : : {
540 : 4119 : return false;
541 : : }
542 : : }
543 : 739 : return true;
544 : : }
545 : 5663 : case Kind::REGEXP_STAR:
546 : : {
547 [ + + ]: 5663 : if (s.size() != index_start)
548 : : {
549 [ + + ]: 10896 : for (unsigned i = s.size() - index_start; i > 0; --i)
550 : : {
551 : 10821 : cvc5::internal::String t = s.substr(index_start, i);
552 [ + + ]: 10821 : if (testConstStringInRegExpInternal(t, 0, r[0]))
553 : : {
554 : 8274 : if (index_start + i == s.size()
555 [ + + ][ + - ]: 4137 : || testConstStringInRegExpInternal(s, index_start + i, r))
[ + + ][ + - ]
[ - - ]
556 : : {
557 : 4137 : return true;
558 : : }
559 : : }
560 [ + + ]: 10821 : }
561 : 75 : return false;
562 : : }
563 : : else
564 : : {
565 : 1451 : return true;
566 : : }
567 : : }
568 : 59 : case Kind::REGEXP_NONE:
569 : : {
570 : 59 : return false;
571 : : }
572 : 12312 : case Kind::REGEXP_ALLCHAR:
573 : : {
574 [ + + ]: 12312 : if (s.size() == index_start + 1)
575 : : {
576 : 5223 : return true;
577 : : }
578 : : else
579 : : {
580 : 7089 : return false;
581 : : }
582 : : }
583 : 924 : case Kind::REGEXP_RANGE:
584 : : {
585 [ + + ]: 924 : if (s.size() == index_start + 1)
586 : : {
587 : 818 : unsigned a = r[0].getConst<String>().front();
588 : 818 : unsigned b = r[1].getConst<String>().front();
589 : 818 : unsigned c = s.back();
590 [ + + ][ + + ]: 818 : return (a <= c && c <= b);
591 : : }
592 : : else
593 : : {
594 : 106 : return false;
595 : : }
596 : : }
597 : 0 : case Kind::REGEXP_LOOP:
598 : : {
599 : 0 : NodeManager* nm = r.getNodeManager();
600 : 0 : uint32_t l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
601 [ - - ]: 0 : if (s.size() == index_start)
602 : : {
603 : 0 : return l == 0 || testConstStringInRegExpInternal(s, index_start, r[0]);
604 : : }
605 : 0 : else if (l == 0 && r[1] == r[2])
606 : : {
607 : 0 : return false;
608 : : }
609 : : else
610 : : {
611 : 0 : Assert(r.getNumChildren() == 3)
612 : 0 : << "String rewriter error: LOOP has 2 children";
613 [ - - ]: 0 : if (l == 0)
614 : : {
615 : : // R{0,u}
616 : 0 : uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
617 [ - - ]: 0 : for (unsigned len = s.size() - index_start; len >= 1; len--)
618 : : {
619 : 0 : cvc5::internal::String t = s.substr(index_start, len);
620 [ - - ]: 0 : if (testConstStringInRegExpInternal(t, 0, r[0]))
621 : : {
622 [ - - ]: 0 : if (len + index_start == s.size())
623 : : {
624 : 0 : return true;
625 : : }
626 : : else
627 : : {
628 : 0 : Node num2 = nm->mkConstInt(cvc5::internal::Rational(u - 1));
629 : 0 : Node r2 = nm->mkNode(Kind::REGEXP_LOOP, r[0], r[1], num2);
630 [ - - ]: 0 : if (testConstStringInRegExpInternal(s, index_start + len, r2))
631 : : {
632 : 0 : return true;
633 : : }
634 [ - - ][ - - ]: 0 : }
635 : : }
636 [ - - ]: 0 : }
637 : 0 : return false;
638 : : }
639 : : else
640 : : {
641 : : // R{l,l}
642 : 0 : Assert(r[1] == r[2])
643 : 0 : << "String rewriter error: LOOP nums are not equal";
644 [ - - ]: 0 : if (l > s.size() - index_start)
645 : : {
646 [ - - ]: 0 : if (testConstStringInRegExpInternal(s, s.size(), r[0]))
647 : : {
648 : 0 : l = s.size() - index_start;
649 : : }
650 : : else
651 : : {
652 : 0 : return false;
653 : : }
654 : : }
655 [ - - ]: 0 : for (unsigned len = 1; len <= s.size() - index_start; len++)
656 : : {
657 : 0 : cvc5::internal::String t = s.substr(index_start, len);
658 [ - - ]: 0 : if (testConstStringInRegExpInternal(t, 0, r[0]))
659 : : {
660 : 0 : Node num2 = nm->mkConstInt(cvc5::internal::Rational(l - 1));
661 : 0 : Node r2 = nm->mkNode(Kind::REGEXP_LOOP, r[0], num2, num2);
662 [ - - ]: 0 : if (testConstStringInRegExpInternal(s, index_start + len, r2))
663 : : {
664 : 0 : return true;
665 : : }
666 [ - - ][ - - ]: 0 : }
667 [ - - ]: 0 : }
668 : 0 : return false;
669 : : }
670 : : }
671 : : }
672 : 1486 : case Kind::REGEXP_COMPLEMENT:
673 : : {
674 : 1486 : return !testConstStringInRegExpInternal(s, index_start, r[0]);
675 : : break;
676 : : }
677 : 0 : default:
678 : : {
679 : 0 : Assert(!utils::isRegExpKind(k));
680 : 0 : return false;
681 : : }
682 : : }
683 : : }
684 : :
685 : 623 : bool RegExpEntail::hasEpsilonNode(TNode node)
686 : : {
687 [ + + ]: 2055 : for (const Node& nc : node)
688 : : {
689 : 1457 : if (nc.getKind() == Kind::STRING_TO_REGEXP && Word::isEmpty(nc[0]))
690 : : {
691 : 25 : return true;
692 : : }
693 [ + + ]: 1457 : }
694 : 598 : return false;
695 : : }
696 : :
697 : 11970 : Node RegExpEntail::getFixedLengthForRegexp(TNode n)
698 : : {
699 : 11970 : NodeManager* nm = n.getNodeManager();
700 : 11970 : Kind k = n.getKind();
701 [ + + ]: 11970 : if (k == Kind::STRING_TO_REGEXP)
702 : : {
703 [ + + ]: 3562 : if (n[0].isConst())
704 : : {
705 : 6856 : return nm->mkConstInt(Rational(Word::getLength(n[0])));
706 : : }
707 : : }
708 [ + + ][ + + ]: 8408 : else if (k == Kind::REGEXP_ALLCHAR || k == Kind::REGEXP_RANGE)
709 : : {
710 : 3638 : return nm->mkConstInt(Rational(1));
711 : : }
712 [ + + ][ + + ]: 6589 : else if (k == Kind::REGEXP_UNION || k == Kind::REGEXP_INTER)
713 : : {
714 : 1089 : Node ret;
715 [ + + ]: 2855 : for (const Node& nc : n)
716 : : {
717 : 2362 : Node flc = getFixedLengthForRegexp(nc);
718 [ + + ][ + + ]: 2362 : if (flc.isNull() || (!ret.isNull() && ret != flc))
[ + + ][ + + ]
719 : : {
720 : 596 : return Node::null();
721 : : }
722 [ + + ]: 1766 : else if (ret.isNull())
723 : : {
724 : : // first time
725 : 960 : ret = flc;
726 : : }
727 [ + + ][ + + ]: 2958 : }
728 : 493 : return ret;
729 : 1089 : }
730 [ + + ]: 5500 : else if (k == Kind::REGEXP_CONCAT)
731 : : {
732 : 2223 : Rational sum(0);
733 [ + + ]: 4696 : for (const Node& nc : n)
734 : : {
735 : 4122 : Node flc = getFixedLengthForRegexp(nc);
736 [ + + ]: 4122 : if (flc.isNull())
737 : : {
738 : 1649 : return flc;
739 : : }
740 : 2473 : Assert(flc.isConst() && flc.getType().isInteger());
741 : 2473 : sum += flc.getConst<Rational>();
742 [ + + ][ + + ]: 5771 : }
743 : 574 : return nm->mkConstInt(sum);
744 : 2223 : }
745 : 3411 : return Node::null();
746 : : }
747 : :
748 : 83 : Node RegExpEntail::getConstantBoundLengthForRegexp(TNode n, bool isLower) const
749 : : {
750 [ - + ][ - + ]: 83 : Assert(n.getType().isRegExp());
[ - - ]
751 : 83 : Node ret;
752 [ + + ]: 83 : if (getConstantBoundCache(n, isLower, ret))
753 : : {
754 : 27 : return ret;
755 : : }
756 : 56 : Kind k = n.getKind();
757 : 56 : NodeManager* nm = n.getNodeManager();
758 [ + + ]: 56 : if (k == Kind::STRING_TO_REGEXP)
759 : : {
760 : 24 : ret = d_aent.getConstantBoundLength(n[0], isLower);
761 : : }
762 [ + - ][ - + ]: 32 : else if (k == Kind::REGEXP_ALLCHAR || k == Kind::REGEXP_RANGE)
763 : : {
764 : 0 : ret = d_one;
765 : : }
766 [ + + ][ + - ]: 32 : else if (k == Kind::REGEXP_UNION || k == Kind::REGEXP_INTER
767 [ + + ]: 28 : || k == Kind::REGEXP_CONCAT)
768 : : {
769 : 20 : bool success = true;
770 : 20 : bool firstTime = true;
771 : 20 : Rational rr(0);
772 [ + + ]: 54 : for (const Node& nc : n)
773 : : {
774 : 40 : Node bc = getConstantBoundLengthForRegexp(nc, isLower);
775 [ + + ]: 40 : if (bc.isNull())
776 : : {
777 [ + - ][ + - ]: 6 : if (k == Kind::REGEXP_UNION || (k == Kind::REGEXP_CONCAT && !isLower))
[ + - ]
778 : : {
779 : : // since the bound could not be determined on the component, the
780 : : // overall bound is undetermined.
781 : 6 : success = false;
782 : 6 : break;
783 : : }
784 : : else
785 : : {
786 : : // if intersection, or we are computing lower bound for concat
787 : : // and the component cannot be determined, ignore it
788 : 0 : continue;
789 : : }
790 : : }
791 : 34 : Assert(bc.isConst() && bc.getType().isInteger());
792 : 34 : Rational r = bc.getConst<Rational>();
793 [ + + ]: 34 : if (k == Kind::REGEXP_CONCAT)
794 : : {
795 : 26 : rr += r;
796 : : }
797 [ + + ]: 8 : else if (firstTime)
798 : : {
799 : 4 : rr = r;
800 : : }
801 [ + + ]: 4 : else if ((k == Kind::REGEXP_UNION) == isLower)
802 : : {
803 : 2 : rr = std::min(r, rr);
804 : : }
805 : : else
806 : : {
807 : 2 : rr = std::max(r, rr);
808 : : }
809 : 34 : firstTime = false;
810 [ + + ][ - + ]: 46 : }
[ + - ]
811 : : // if we were successful and didn't ignore all components
812 [ + + ][ + - ]: 20 : if (success && !firstTime)
813 : : {
814 : 14 : ret = nm->mkConstInt(rr);
815 : : }
816 : 20 : }
817 [ + + ][ + + ]: 56 : if (ret.isNull() && isLower)
[ + + ]
818 : : {
819 : 6 : ret = d_zero;
820 : : }
821 [ + - ]: 112 : Trace("strings-rentail") << "getConstantBoundLengthForRegexp: " << n
822 : 0 : << ", isLower=" << isLower << " returns " << ret
823 : 56 : << std::endl;
824 : 56 : setConstantBoundCache(n, ret, isLower);
825 : 56 : return ret;
826 : 0 : }
827 : :
828 : 23617 : bool RegExpEntail::regExpIncludes(Node r1,
829 : : Node r2,
830 : : std::map<std::pair<Node, Node>, bool>& cache)
831 : : {
832 [ + + ]: 23617 : if (r1 == r2)
833 : : {
834 : 3260 : return true;
835 : : }
836 : 20357 : std::pair<Node, Node> key = std::make_pair(r1, r2);
837 : 20357 : const auto& it = cache.find(key);
838 [ + + ]: 20357 : if (it != cache.end())
839 : : {
840 : 5479 : return (*it).second;
841 : : }
842 : : // first, check some basic inclusions
843 : 14878 : bool ret = false;
844 : 14878 : Kind k2 = r2.getKind();
845 : : // if the right hand side is a constant string, this is a membership test
846 [ + + ]: 14878 : if (k2 == Kind::STRING_TO_REGEXP)
847 : : {
848 : : // only check if r1 is a constant regular expression
849 : 4393 : if (r2[0].isConst() && isConstRegExp(r1))
850 : : {
851 : 3681 : String s = r2[0].getConst<String>();
852 : 3681 : ret = testConstStringInRegExp(s, r1);
853 : 3681 : }
854 : 4393 : cache[key] = ret;
855 : 4393 : return ret;
856 : : }
857 : 10485 : Kind k1 = r1.getKind();
858 : 10485 : bool retSet = false;
859 [ + + ]: 10485 : if (k1 == Kind::REGEXP_UNION)
860 : : {
861 : 1035 : retSet = true;
862 : : // if any component of r1 includes r2, return true
863 [ + + ]: 3615 : for (const Node& r : r1)
864 : : {
865 [ + + ]: 2621 : if (regExpIncludes(r, r2, cache))
866 : : {
867 : 41 : ret = true;
868 : 41 : break;
869 : : }
870 [ + + ]: 2621 : }
871 : : }
872 [ + + ][ + - ]: 10485 : if (k2 == Kind::REGEXP_INTER && !ret)
873 : : {
874 : 20 : retSet = true;
875 : : // if r1 includes any component of r2, return true
876 [ + + ]: 56 : for (const Node& r : r2)
877 : : {
878 [ + + ]: 38 : if (regExpIncludes(r1, r, cache))
879 : : {
880 : 2 : ret = true;
881 : 2 : break;
882 : : }
883 [ + + ]: 38 : }
884 : : }
885 [ + + ]: 10485 : if (k1 == Kind::REGEXP_STAR)
886 : : {
887 : 2194 : retSet = true;
888 : : // inclusion if r1 is (re.* re.allchar), or if the body of r1 includes r2
889 : : // (or the body of r2 if it is also a star).
890 [ + + ]: 2194 : if (r1[0].getKind() == Kind::REGEXP_ALLCHAR)
891 : : {
892 : 218 : ret = true;
893 : : }
894 : : else
895 : : {
896 [ + + ]: 1976 : ret = regExpIncludes(r1[0], k2 == Kind::REGEXP_STAR ? r2[0] : r2, cache);
897 : : }
898 : : }
899 [ + + ]: 8291 : else if (k1 == Kind::STRING_TO_REGEXP)
900 : : {
901 : : // only way to include is if equal, which was already checked
902 : 3557 : retSet = true;
903 : : }
904 [ + + ][ + - ]: 4734 : else if (k1 == Kind::REGEXP_RANGE && utils::isCharacterRange(r1))
[ + + ][ + + ]
[ - - ]
905 : : {
906 : 253 : retSet = true;
907 : : // if comparing subranges, we check inclusion of interval
908 [ + + ][ + - ]: 253 : if (k2 == Kind::REGEXP_RANGE && utils::isCharacterRange(r2))
[ + + ][ + + ]
[ - - ]
909 : : {
910 : 37 : unsigned l1 = r1[0].getConst<String>().front();
911 : 37 : unsigned u1 = r1[1].getConst<String>().front();
912 : 37 : unsigned l2 = r2[0].getConst<String>().front();
913 : 37 : unsigned u2 = r2[1].getConst<String>().front();
914 [ + - ][ + - ]: 37 : ret = l1 <= l2 && l2 <= u1 && l1 <= u2 && u2 <= u1;
[ + - ][ + + ]
915 : : }
916 : : }
917 [ + + ]: 10485 : if (retSet)
918 : : {
919 : 7039 : cache[key] = ret;
920 : 7039 : return ret;
921 : : }
922 : : // avoid infinite loop
923 : 3446 : cache[key] = false;
924 : 3446 : NodeManager* nm = r1.getNodeManager();
925 : 3446 : Node sigma = nm->mkNode(Kind::REGEXP_ALLCHAR, std::vector<Node>{});
926 : 3446 : Node sigmaStar = nm->mkNode(Kind::REGEXP_STAR, sigma);
927 : :
928 : 3446 : std::vector<Node> v1, v2;
929 : 3446 : utils::getRegexpComponents(r1, v1);
930 : 3446 : utils::getRegexpComponents(r2, v2);
931 : :
932 : : // In the following, we iterate over `r2` (the "includee") and try to
933 : : // match it with `r1`. `idxs`/`newIdxs` keep track of all the possible
934 : : // positions in `r1` that we could currently be at.
935 : 3446 : std::unordered_set<size_t> newIdxs = {0};
936 : 3446 : std::unordered_set<size_t> idxs;
937 [ + + ]: 7953 : for (const Node& n2 : v2)
938 : : {
939 : : // Transfer elements from `newIdxs` to `idxs`. Out-of-bound indices are
940 : : // removed and for (re.* re.allchar), we additionally include the option of
941 : : // skipping it. Indices must be smaller than the size of `v1`.
942 : 7297 : idxs.clear();
943 [ + + ]: 21039 : for (size_t idx : newIdxs)
944 : : {
945 [ + + ]: 13742 : if (idx < v1.size())
946 : : {
947 : 13537 : idxs.insert(idx);
948 [ + + ][ + + ]: 13537 : if (idx + 1 < v1.size() && v1[idx] == sigmaStar)
[ + + ]
949 : : {
950 [ + - ][ + - ]: 3808 : Assert(idx + 1 == v1.size() || v1[idx + 1] != sigmaStar);
[ - + ][ - + ]
[ - - ]
951 : 3808 : idxs.insert(idx + 1);
952 : : }
953 : : }
954 : : }
955 : 7297 : newIdxs.clear();
956 : :
957 [ + + ]: 21563 : for (size_t idx : idxs)
958 : : {
959 [ + + ]: 14266 : if (regExpIncludes(v1[idx], n2, cache))
960 : : {
961 : : // If this component includes n2, then we can consume it.
962 : 7765 : newIdxs.insert(idx + 1);
963 : : }
964 [ + + ]: 14266 : if (v1[idx] == sigmaStar)
965 : : {
966 : : // (re.* re.allchar) can match an arbitrary amount of `r2`
967 : 4049 : newIdxs.insert(idx);
968 : : }
969 [ + + ]: 10217 : else if (utils::isUnboundedWildcard(v1, idx))
970 : : {
971 : : // If a series of re.allchar is followed by (re.* re.allchar), we
972 : : // can decide not to "waste" the re.allchar because the order of
973 : : // the two wildcards is not observable (i.e. it does not change
974 : : // the sequences matched by the regular expression)
975 : 1922 : newIdxs.insert(idx);
976 : : }
977 : : }
978 : :
979 [ + + ]: 7297 : if (newIdxs.empty())
980 : : {
981 : : // If there are no candidates, we can't match the remainder of r2
982 : 2790 : break;
983 : : }
984 : : }
985 : :
986 : : // We have processed all of `r2`. We are now looking if there was also a
987 : : // path to the end in `r1`. This makes sure that we don't have leftover
988 : : // bits in `r1` that don't match anything in `r2`.
989 : 3446 : bool result = false;
990 [ + + ]: 5403 : for (size_t idx : newIdxs)
991 : : {
992 [ + + ][ + + ]: 2234 : if (idx == v1.size() || (idx == v1.size() - 1 && v1[idx] == sigmaStar))
[ + + ][ + + ]
993 : : {
994 : 277 : result = true;
995 : 277 : break;
996 : : }
997 : : }
998 : 3446 : cache[key] = result;
999 : 3446 : return result;
1000 : 20357 : }
1001 : :
1002 : 2981 : bool RegExpEntail::regExpIncludes(Node r1, Node r2)
1003 : : {
1004 : 2981 : std::map<std::pair<Node, Node>, bool> cache;
1005 : 5962 : return regExpIncludes(r1, r2, cache);
1006 : 2981 : }
1007 : :
1008 : 53933 : Node RegExpEntail::getGeneralizedConstRegExp(const Node& n)
1009 : : {
1010 [ - + ][ - + ]: 53933 : Assert(n.getType().isString());
[ - - ]
1011 : 53933 : NodeManager* nm = n.getNodeManager();
1012 : 53933 : std::vector<Node> ncs;
1013 [ + + ]: 53933 : if (n.getKind() == Kind::STRING_CONCAT)
1014 : : {
1015 : 6660 : ncs.insert(ncs.end(), n.begin(), n.end());
1016 : : }
1017 : : else
1018 : : {
1019 : 47273 : ncs.push_back(n);
1020 : : }
1021 : 53933 : bool nonTrivial = false;
1022 : : Node sigmaStar =
1023 : 107866 : nm->mkNode(Kind::REGEXP_STAR, nm->mkNode(Kind::REGEXP_ALLCHAR));
1024 : 53933 : std::vector<Node> rs;
1025 [ + + ]: 123361 : for (const Node& nc : ncs)
1026 : : {
1027 : 69428 : Node re = sigmaStar;
1028 [ + + ]: 69428 : if (nc.isConst())
1029 : : {
1030 : 8290 : nonTrivial = true;
1031 : 8290 : re = nm->mkNode(Kind::STRING_TO_REGEXP, nc);
1032 : : }
1033 [ + + ]: 61138 : else if (nc.getKind() == Kind::STRING_ITOS)
1034 : : {
1035 : 999 : nonTrivial = true;
1036 : : Node digRange = nm->mkNode(Kind::REGEXP_RANGE,
1037 : 1998 : nm->mkConst(String("0")),
1038 : 3996 : nm->mkConst(String("9")));
1039 : 999 : re = nm->mkNode(Kind::REGEXP_STAR, digRange);
1040 : : // maybe non-empty digit range?
1041 : : // relies on RARE rule str-in-re-from-int-dig-range to prove
1042 [ + + ]: 999 : if (d_aent.check(nc[0]))
1043 : : {
1044 : 227 : re = nm->mkNode(Kind::REGEXP_CONCAT, digRange, re);
1045 : : }
1046 : 999 : }
1047 : 69428 : rs.push_back(re);
1048 : 69428 : }
1049 [ + + ]: 53933 : if (nonTrivial)
1050 : : {
1051 [ + + ]: 6821 : return rs.size() == 1 ? rs[0] : nm->mkNode(Kind::REGEXP_CONCAT, rs);
1052 : : }
1053 : 47112 : return Node::null();
1054 : 53933 : }
1055 : :
1056 : : struct RegExpEntailConstantBoundLowerId
1057 : : {
1058 : : };
1059 : : typedef expr::Attribute<RegExpEntailConstantBoundLowerId, Node>
1060 : : RegExpEntailConstantBoundLower;
1061 : :
1062 : : struct RegExpEntailConstantBoundUpperId
1063 : : {
1064 : : };
1065 : : typedef expr::Attribute<RegExpEntailConstantBoundUpperId, Node>
1066 : : RegExpEntailConstantBoundUpper;
1067 : :
1068 : 56 : void RegExpEntail::setConstantBoundCache(TNode n, Node ret, bool isLower)
1069 : : {
1070 [ + + ]: 56 : if (isLower)
1071 : : {
1072 : : RegExpEntailConstantBoundLower rcbl;
1073 : 28 : n.setAttribute(rcbl, ret);
1074 : : }
1075 : : else
1076 : : {
1077 : : RegExpEntailConstantBoundUpper rcbu;
1078 : 28 : n.setAttribute(rcbu, ret);
1079 : : }
1080 : 56 : }
1081 : :
1082 : 83 : bool RegExpEntail::getConstantBoundCache(TNode n, bool isLower, Node& c)
1083 : : {
1084 [ + + ]: 83 : if (isLower)
1085 : : {
1086 : : RegExpEntailConstantBoundLower rcbl;
1087 [ + + ]: 52 : if (n.hasAttribute(rcbl))
1088 : : {
1089 : 24 : c = n.getAttribute(rcbl);
1090 : 24 : return true;
1091 : : }
1092 : : }
1093 : : else
1094 : : {
1095 : : RegExpEntailConstantBoundUpper rcbu;
1096 [ + + ]: 31 : if (n.hasAttribute(rcbu))
1097 : : {
1098 : 3 : c = n.getAttribute(rcbu);
1099 : 3 : return true;
1100 : : }
1101 : : }
1102 : 56 : return false;
1103 : : }
1104 : :
1105 : : } // namespace strings
1106 : : } // namespace theory
1107 : : } // namespace cvc5::internal
|
