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 : : * Symbolic Regular Expresion Operations
11 : : */
12 : :
13 : : #include "theory/strings/regexp_operation.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "expr/node_algorithm.h"
18 : : #include "options/strings_options.h"
19 : : #include "theory/rewriter.h"
20 : : #include "theory/strings/regexp_entail.h"
21 : : #include "theory/strings/theory_strings_utils.h"
22 : : #include "theory/strings/word.h"
23 : : #include "util/regexp.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace strings {
30 : :
31 : 51092 : RegExpOpr::RegExpOpr(Env& env, SkolemCache* sc)
32 : : : EnvObj(env),
33 : 51092 : d_true(nodeManager()->mkConst(true)),
34 : 51092 : d_false(nodeManager()->mkConst(false)),
35 : 102184 : d_emptyRegexp(
36 : 102184 : nodeManager()->mkNode(Kind::REGEXP_NONE, std::vector<Node>{})),
37 : 51092 : d_zero(nodeManager()->mkConstInt(Rational(0))),
38 : 51092 : d_one(nodeManager()->mkConstInt(Rational(1))),
39 : 51092 : d_sigma(nodeManager()->mkNode(Kind::REGEXP_ALLCHAR, std::vector<Node>{})),
40 : 51092 : d_sigma_star(nodeManager()->mkNode(Kind::REGEXP_STAR, d_sigma)),
41 : 153276 : d_sc(sc)
42 : : {
43 : 51092 : d_emptyString = Word::mkEmptyWord(nodeManager()->stringType());
44 : :
45 : : d_emptySingleton =
46 : 51092 : nodeManager()->mkNode(Kind::STRING_TO_REGEXP, d_emptyString);
47 : 51092 : d_lastchar = options().strings.stringsAlphaCard - 1;
48 : 51092 : }
49 : :
50 : 50744 : RegExpOpr::~RegExpOpr() {}
51 : :
52 : 2848 : bool RegExpOpr::checkConstRegExp(Node r)
53 : : {
54 [ - + ][ - + ]: 2848 : Assert(r.getType().isRegExp());
[ - - ]
55 [ + - ]: 5696 : Trace("strings-regexp-cstre")
56 : 2848 : << "RegExpOpr::checkConstRegExp /" << mkString(r) << "/" << std::endl;
57 : 2848 : RegExpConstType rct = getRegExpConstType(r);
58 : 2848 : return rct != RE_C_VARIABLE;
59 : : }
60 : :
61 : 2857 : RegExpConstType RegExpOpr::getRegExpConstType(Node r)
62 : : {
63 [ - + ][ - + ]: 2857 : Assert(r.getType().isRegExp());
[ - - ]
64 : 2857 : std::unordered_map<Node, RegExpConstType>::iterator it;
65 : 2857 : std::vector<TNode> visit;
66 : 2857 : TNode cur;
67 : 2857 : visit.push_back(r);
68 : : do
69 : : {
70 : 8199 : cur = visit.back();
71 : 8199 : visit.pop_back();
72 : 8199 : it = d_constCache.find(cur);
73 : :
74 : 8199 : Kind ck = cur.getKind();
75 [ + + ]: 8199 : if (it == d_constCache.end())
76 : : {
77 [ + + ]: 3040 : if (ck == Kind::STRING_TO_REGEXP)
78 : : {
79 : 982 : Node tmp = rewrite(cur[0]);
80 : 982 : d_constCache[cur] =
81 [ + + ]: 982 : tmp.isConst() ? RE_C_CONCRETE_CONSTANT : RE_C_VARIABLE;
82 : 982 : }
83 [ + + ][ + + ]: 2058 : else if (ck == Kind::REGEXP_ALLCHAR || ck == Kind::REGEXP_RANGE)
84 : : {
85 : 289 : d_constCache[cur] = RE_C_CONSTANT;
86 : : }
87 [ - + ]: 1769 : else if (!utils::isRegExpKind(ck))
88 : : {
89 : : // non-regular expression applications, e.g. function applications
90 : : // with regular expression return type are treated as variables.
91 : 0 : d_constCache[cur] = RE_C_VARIABLE;
92 : : }
93 : : else
94 : : {
95 : 1769 : d_constCache[cur] = RE_C_UNKNOWN;
96 : 1769 : visit.push_back(cur);
97 : 1769 : visit.insert(visit.end(), cur.begin(), cur.end());
98 : : }
99 : : }
100 [ + + ]: 5159 : else if (it->second == RE_C_UNKNOWN)
101 : : {
102 : 1769 : RegExpConstType ret = ck == Kind::REGEXP_COMPLEMENT
103 [ + + ]: 1769 : ? RE_C_CONSTANT
104 : : : RE_C_CONCRETE_CONSTANT;
105 [ + + ]: 5342 : for (const Node& cn : cur)
106 : : {
107 : 3573 : it = d_constCache.find(cn);
108 [ - + ][ - + ]: 3573 : Assert(it != d_constCache.end());
[ - - ]
109 [ + + ]: 3573 : if (it->second > ret)
110 : : {
111 : 949 : ret = it->second;
112 : : }
113 : 3573 : }
114 : 1769 : d_constCache[cur] = ret;
115 : : }
116 [ + + ]: 8199 : } while (!visit.empty());
117 [ - + ][ - + ]: 2857 : Assert(d_constCache.find(r) != d_constCache.end());
[ - - ]
118 : 5714 : return d_constCache[r];
119 : 2857 : }
120 : :
121 : : // 0-unknown, 1-yes, 2-no
122 : 21 : int RegExpOpr::delta(Node r, Node& exp)
123 : : {
124 : : std::map<Node, std::pair<int, Node> >::const_iterator itd =
125 : 21 : d_delta_cache.find(r);
126 [ + + ]: 21 : if (itd != d_delta_cache.end())
127 : : {
128 : : // already computed
129 : 7 : exp = itd->second.second;
130 : 7 : return itd->second.first;
131 : : }
132 [ + - ]: 14 : Trace("regexp-delta") << "RegExpOpr::delta: " << r << std::endl;
133 : 14 : int ret = 0;
134 : 14 : NodeManager* nm = nodeManager();
135 : 14 : Kind k = r.getKind();
136 [ - + ][ + - ]: 14 : switch (k)
[ - - ][ - - ]
137 : : {
138 : 0 : case Kind::REGEXP_NONE:
139 : : case Kind::REGEXP_ALLCHAR:
140 : : case Kind::REGEXP_RANGE:
141 : : {
142 : : // does not contain empty string
143 : 0 : ret = 2;
144 : 0 : break;
145 : : }
146 : 7 : case Kind::STRING_TO_REGEXP:
147 : : {
148 : 14 : Node tmp = rewrite(r[0]);
149 [ + - ]: 7 : if (tmp.isConst())
150 : : {
151 [ + - ]: 7 : if (tmp == d_emptyString)
152 : : {
153 : 7 : ret = 1;
154 : : }
155 : : else
156 : : {
157 : 0 : ret = 2;
158 : : }
159 : : }
160 : : else
161 : : {
162 : 0 : ret = 0;
163 [ - - ]: 0 : if (tmp.getKind() == Kind::STRING_CONCAT)
164 : : {
165 [ - - ]: 0 : for (const Node& tmpc : tmp)
166 : : {
167 [ - - ]: 0 : if (tmpc.isConst())
168 : : {
169 : 0 : ret = 2;
170 : 0 : break;
171 : : }
172 [ - - ]: 0 : }
173 : : }
174 [ - - ]: 0 : if (ret == 0)
175 : : {
176 : 0 : exp = r[0].eqNode(d_emptyString);
177 : : }
178 : : }
179 : 7 : break;
180 : 7 : }
181 : 7 : case Kind::REGEXP_CONCAT:
182 : : case Kind::REGEXP_UNION:
183 : : case Kind::REGEXP_INTER:
184 : : {
185 : : // has there been an unknown child?
186 : 7 : bool hasUnknownChild = false;
187 : 7 : std::vector<Node> vec;
188 [ + - ]: 7 : int checkTmp = k == Kind::REGEXP_UNION ? 1 : 2;
189 [ + - ]: 7 : int retTmp = k == Kind::REGEXP_UNION ? 2 : 1;
190 [ + - ]: 7 : for (const Node& rc : r)
191 : : {
192 : 7 : Node exp2;
193 : 7 : int tmp = delta(rc, exp2);
194 [ + - ]: 7 : if (tmp == checkTmp)
195 : : {
196 : : // return is implied by the child's return value
197 : 7 : ret = checkTmp;
198 : 7 : break;
199 : : }
200 [ - - ]: 0 : else if (tmp == 0)
201 : : {
202 : : // unknown if child contains empty string
203 : 0 : Assert(!exp2.isNull());
204 : 0 : vec.push_back(exp2);
205 : 0 : hasUnknownChild = true;
206 : : }
207 [ - + ][ - + ]: 14 : }
208 [ - + ]: 7 : if (ret != checkTmp)
209 : : {
210 [ - - ]: 0 : if (!hasUnknownChild)
211 : : {
212 : 0 : ret = retTmp;
213 : : }
214 : : else
215 : : {
216 [ - - ]: 0 : Kind kr = k == Kind::REGEXP_UNION ? Kind::OR : Kind::AND;
217 [ - - ]: 0 : exp = vec.size() == 1 ? vec[0] : nm->mkNode(kr, vec);
218 : : }
219 : : }
220 : 7 : break;
221 : 7 : }
222 : 0 : case Kind::REGEXP_STAR:
223 : : case Kind::REGEXP_OPT:
224 : : {
225 : : // contains empty string
226 : 0 : ret = 1;
227 : 0 : break;
228 : : }
229 : 0 : case Kind::REGEXP_PLUS:
230 : : {
231 : 0 : ret = delta(r[0], exp);
232 : 0 : break;
233 : : }
234 : 0 : case Kind::REGEXP_LOOP:
235 : : {
236 : 0 : uint32_t lo = utils::getLoopMinOccurrences(r);
237 [ - - ]: 0 : if (lo == 0)
238 : : {
239 : 0 : ret = 1;
240 : : }
241 : : else
242 : : {
243 : 0 : ret = delta(r[0], exp);
244 : : }
245 : 0 : break;
246 : : }
247 : 0 : case Kind::REGEXP_COMPLEMENT:
248 : : {
249 : 0 : int tmp = delta(r[0], exp);
250 : : // flip the result if known
251 [ - - ]: 0 : ret = tmp == 0 ? 0 : (3 - tmp);
252 [ - - ]: 0 : exp = exp.isNull() ? exp : exp.negate();
253 : 0 : break;
254 : : }
255 : 0 : default:
256 : : {
257 : 0 : Assert(!utils::isRegExpKind(k));
258 : 0 : break;
259 : : }
260 : : }
261 [ - + ]: 14 : if (!exp.isNull())
262 : : {
263 : 0 : exp = rewrite(exp);
264 : : }
265 : 14 : std::pair<int, Node> p(ret, exp);
266 : 14 : d_delta_cache[r] = p;
267 [ + - ]: 28 : Trace("regexp-delta") << "RegExpOpr::delta returns " << ret << " for " << r
268 : 14 : << ", expr = " << exp << std::endl;
269 : 14 : return ret;
270 : : }
271 : :
272 : : // 0-unknown, 1-yes, 2-no
273 : 42 : int RegExpOpr::derivativeS(Node r, cvc5::internal::String c, Node& retNode)
274 : : {
275 [ - + ][ - + ]: 42 : Assert(c.size() < 2);
[ - - ]
276 : 84 : Trace("regexp-derive") << "RegExp-derive starts with /" << mkString(r)
277 : 42 : << "/, c=" << c << std::endl;
278 : :
279 : 42 : int ret = 1;
280 : 42 : retNode = d_emptyRegexp;
281 : 42 : NodeManager* nm = nodeManager();
282 : :
283 : 42 : PairNodeStr dv = std::make_pair(r, c);
284 [ + + ]: 42 : if (d_deriv_cache.find(dv) != d_deriv_cache.end())
285 : : {
286 : 7 : retNode = d_deriv_cache[dv].first;
287 : 7 : ret = d_deriv_cache[dv].second;
288 : : }
289 [ - + ]: 35 : else if (c.empty())
290 : : {
291 : 0 : Node expNode;
292 : 0 : ret = delta(r, expNode);
293 [ - - ]: 0 : if (ret == 0)
294 : : {
295 : 0 : retNode = nodeManager()->mkNode(Kind::ITE, expNode, r, d_emptyRegexp);
296 : : }
297 [ - - ]: 0 : else if (ret == 1)
298 : : {
299 : 0 : retNode = r;
300 : : }
301 : 0 : std::pair<Node, int> p(retNode, ret);
302 : 0 : d_deriv_cache[dv] = p;
303 : 0 : }
304 : : else
305 : : {
306 [ - - ][ - + ]: 35 : switch (r.getKind())
[ + + ][ - + ]
[ - - ][ - ]
307 : : {
308 : 0 : case Kind::REGEXP_NONE:
309 : : {
310 : 0 : ret = 2;
311 : 0 : break;
312 : : }
313 : 0 : case Kind::REGEXP_ALLCHAR:
314 : : {
315 : 0 : retNode = d_emptySingleton;
316 : 0 : break;
317 : : }
318 : 0 : case Kind::REGEXP_RANGE:
319 : : {
320 : 0 : cvc5::internal::String a = r[0].getConst<String>();
321 : 0 : cvc5::internal::String b = r[1].getConst<String>();
322 : 0 : retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp;
323 : 0 : break;
324 : 0 : }
325 : 14 : case Kind::STRING_TO_REGEXP:
326 : : {
327 : 28 : Node tmp = rewrite(r[0]);
328 [ + - ]: 14 : if (tmp.isConst())
329 : : {
330 [ + + ]: 14 : if (tmp == d_emptyString)
331 : : {
332 : 7 : ret = 2;
333 : : }
334 : : else
335 : : {
336 [ - + ]: 7 : if (tmp.getConst<String>().front() == c.front())
337 : : {
338 : : retNode =
339 : 0 : nm->mkNode(Kind::STRING_TO_REGEXP,
340 : 0 : Word::getLength(tmp) == 1 ? d_emptyString
341 : 0 : : Word::substr(tmp, 1));
342 : : }
343 : : else
344 : : {
345 : 7 : ret = 2;
346 : : }
347 : : }
348 : : }
349 : : else
350 : : {
351 : 0 : ret = 0;
352 : 0 : Node rest;
353 [ - - ]: 0 : if (tmp.getKind() == Kind::STRING_CONCAT)
354 : : {
355 : 0 : Node t2 = tmp[0];
356 [ - - ]: 0 : if (t2.isConst())
357 : : {
358 [ - - ]: 0 : if (t2.getConst<String>().front() == c.front())
359 : : {
360 : : Node n = nm->mkNode(Kind::STRING_TO_REGEXP,
361 : 0 : Word::getLength(tmp) == 1
362 : 0 : ? d_emptyString
363 : 0 : : Word::substr(tmp, 1));
364 : 0 : std::vector<Node> vec_nodes;
365 : 0 : vec_nodes.push_back(n);
366 [ - - ]: 0 : for (unsigned i = 1; i < tmp.getNumChildren(); i++)
367 : : {
368 : 0 : vec_nodes.push_back(tmp[i]);
369 : : }
370 : 0 : retNode = nm->mkNode(Kind::REGEXP_CONCAT, vec_nodes);
371 : 0 : ret = 1;
372 : 0 : }
373 : : else
374 : : {
375 : 0 : ret = 2;
376 : : }
377 : : }
378 : : else
379 : : {
380 : 0 : tmp = tmp[0];
381 : 0 : std::vector<Node> vec_nodes;
382 [ - - ]: 0 : for (unsigned i = 1; i < tmp.getNumChildren(); i++)
383 : : {
384 : 0 : vec_nodes.push_back(tmp[i]);
385 : : }
386 : 0 : rest = nm->mkNode(Kind::REGEXP_CONCAT, vec_nodes);
387 : 0 : }
388 : 0 : }
389 [ - - ]: 0 : if (ret == 0)
390 : : {
391 : 0 : Node sk = NodeManager::mkDummySkolem("rsp", nm->stringType());
392 : 0 : retNode = nm->mkNode(Kind::STRING_TO_REGEXP, sk);
393 [ - - ]: 0 : if (!rest.isNull())
394 : : {
395 : 0 : retNode = rewrite(nm->mkNode(Kind::REGEXP_CONCAT, retNode, rest));
396 : : }
397 : : Node exp =
398 : 0 : tmp.eqNode(nm->mkNode(Kind::STRING_CONCAT, nm->mkConst(c), sk));
399 : : retNode =
400 : 0 : rewrite(nm->mkNode(Kind::ITE, exp, retNode, d_emptyRegexp));
401 : 0 : }
402 : 0 : }
403 : 14 : break;
404 : 14 : }
405 : 7 : case Kind::REGEXP_CONCAT:
406 : : {
407 : 7 : std::vector<Node> vec_nodes;
408 : 7 : std::vector<Node> delta_nodes;
409 : 7 : Node dnode = d_true;
410 [ + + ]: 21 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
411 : : {
412 : 14 : Node dc;
413 : 14 : Node exp2;
414 : 14 : int rt = derivativeS(r[i], c, dc);
415 [ - + ]: 14 : if (rt != 2)
416 : : {
417 [ - - ]: 0 : if (rt == 0)
418 : : {
419 : 0 : ret = 0;
420 : : }
421 : 0 : std::vector<Node> vec_nodes2;
422 [ - - ]: 0 : if (dc != d_emptySingleton)
423 : : {
424 : 0 : vec_nodes2.push_back(dc);
425 : : }
426 [ - - ]: 0 : for (unsigned j = i + 1; j < r.getNumChildren(); ++j)
427 : : {
428 [ - - ]: 0 : if (r[j] != d_emptySingleton)
429 : : {
430 : 0 : vec_nodes2.push_back(r[j]);
431 : : }
432 : : }
433 : : Node tmp =
434 : 0 : vec_nodes2.size() == 0 ? d_emptySingleton
435 : 0 : : vec_nodes2.size() == 1
436 : 0 : ? vec_nodes2[0]
437 : 0 : : nodeManager()->mkNode(Kind::REGEXP_CONCAT, vec_nodes2);
438 [ - - ]: 0 : if (dnode != d_true)
439 : : {
440 : 0 : tmp = rewrite(nm->mkNode(Kind::ITE, dnode, tmp, d_emptyRegexp));
441 : 0 : ret = 0;
442 : : }
443 : 0 : if (std::find(vec_nodes.begin(), vec_nodes.end(), tmp)
444 [ - - ]: 0 : == vec_nodes.end())
445 : : {
446 : 0 : vec_nodes.push_back(tmp);
447 : : }
448 : 0 : }
449 : 14 : Node exp3;
450 : 14 : int rt2 = delta(r[i], exp3);
451 [ - + ]: 14 : if (rt2 == 0)
452 : : {
453 : 0 : dnode = rewrite(nm->mkNode(Kind::AND, dnode, exp3));
454 : : }
455 [ - + ]: 14 : else if (rt2 == 2)
456 : : {
457 : 0 : break;
458 : : }
459 [ + - ][ + - ]: 14 : }
[ + - ]
460 : : retNode =
461 : 7 : vec_nodes.size() == 0
462 [ + - ][ - - ]: 14 : ? d_emptyRegexp
463 : 0 : : (vec_nodes.size() == 1
464 : 0 : ? vec_nodes[0]
465 : 7 : : nodeManager()->mkNode(Kind::REGEXP_UNION, vec_nodes));
466 [ + - ]: 7 : if (retNode == d_emptyRegexp)
467 : : {
468 : 7 : ret = 2;
469 : : }
470 : 7 : break;
471 : 7 : }
472 : 7 : case Kind::REGEXP_UNION:
473 : : {
474 : 7 : std::vector<Node> vec_nodes;
475 [ + + ]: 21 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
476 : : {
477 : 14 : Node dc;
478 : 14 : int rt = derivativeS(r[i], c, dc);
479 [ - + ]: 14 : if (rt == 0)
480 : : {
481 : 0 : ret = 0;
482 : : }
483 [ - + ]: 14 : if (rt != 2)
484 : : {
485 : 0 : if (std::find(vec_nodes.begin(), vec_nodes.end(), dc)
486 [ - - ]: 0 : == vec_nodes.end())
487 : : {
488 : 0 : vec_nodes.push_back(dc);
489 : : }
490 : : }
491 : : // Trace("regexp-derive") << "RegExp-derive OR R[" << i << "] " <<
492 : : // mkString(r[i]) << " returns " << mkString(dc) << std::endl;
493 : 14 : }
494 : : retNode =
495 : 7 : vec_nodes.size() == 0
496 [ + - ][ - - ]: 14 : ? d_emptyRegexp
497 : 0 : : (vec_nodes.size() == 1
498 : 0 : ? vec_nodes[0]
499 : 7 : : nodeManager()->mkNode(Kind::REGEXP_UNION, vec_nodes));
500 [ + - ]: 7 : if (retNode == d_emptyRegexp)
501 : : {
502 : 7 : ret = 2;
503 : : }
504 : 7 : break;
505 : 7 : }
506 : 0 : case Kind::REGEXP_INTER:
507 : : {
508 : 0 : bool flag = true;
509 : 0 : bool flag_sg = false;
510 : 0 : std::vector<Node> vec_nodes;
511 [ - - ]: 0 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
512 : : {
513 : 0 : Node dc;
514 : 0 : int rt = derivativeS(r[i], c, dc);
515 [ - - ]: 0 : if (rt == 0)
516 : : {
517 : 0 : ret = 0;
518 : : }
519 [ - - ]: 0 : else if (rt == 2)
520 : : {
521 : 0 : flag = false;
522 : 0 : break;
523 : : }
524 [ - - ]: 0 : if (dc == d_sigma_star)
525 : : {
526 : 0 : flag_sg = true;
527 : : }
528 : : else
529 : : {
530 : 0 : if (std::find(vec_nodes.begin(), vec_nodes.end(), dc)
531 [ - - ]: 0 : == vec_nodes.end())
532 : : {
533 : 0 : vec_nodes.push_back(dc);
534 : : }
535 : : }
536 [ - - ]: 0 : }
537 [ - - ]: 0 : if (flag)
538 : : {
539 [ - - ][ - - ]: 0 : if (vec_nodes.size() == 0 && flag_sg)
[ - - ]
540 : : {
541 : 0 : retNode = d_sigma_star;
542 : : }
543 : : else
544 : : {
545 : 0 : retNode = vec_nodes.size() == 0
546 : 0 : ? d_emptyRegexp
547 : 0 : : (vec_nodes.size() == 1
548 : 0 : ? vec_nodes[0]
549 : : : nodeManager()->mkNode(Kind::REGEXP_INTER,
550 : 0 : vec_nodes));
551 [ - - ]: 0 : if (retNode == d_emptyRegexp)
552 : : {
553 : 0 : ret = 2;
554 : : }
555 : : }
556 : : }
557 : : else
558 : : {
559 : 0 : retNode = d_emptyRegexp;
560 : 0 : ret = 2;
561 : : }
562 : 0 : break;
563 : 0 : }
564 : 7 : case Kind::REGEXP_STAR:
565 : : {
566 : 7 : Node dc;
567 : 7 : ret = derivativeS(r[0], c, dc);
568 : : retNode =
569 : 7 : dc == d_emptyRegexp
570 : 14 : ? dc
571 [ - - ]: 0 : : (dc == d_emptySingleton
572 : : ? r
573 : 7 : : nodeManager()->mkNode(Kind::REGEXP_CONCAT, dc, r));
574 : 7 : break;
575 : 7 : }
576 : 0 : case Kind::REGEXP_LOOP:
577 : : {
578 : 0 : uint32_t l = utils::getLoopMinOccurrences(r);
579 : 0 : uint32_t u = utils::getLoopMaxOccurrences(r);
580 [ - - ][ - - ]: 0 : if (l == u && l == 0)
581 : : {
582 : 0 : ret = 2;
583 : : // retNode = d_emptyRegexp;
584 : : }
585 : : else
586 : : {
587 : 0 : Node dc;
588 : 0 : ret = derivativeS(r[0], c, dc);
589 [ - - ]: 0 : if (dc == d_emptyRegexp)
590 : : {
591 [ - - ]: 0 : Node lop = nm->mkConst(RegExpLoop(l == 0 ? 0 : (l - 1), u - 1));
592 : 0 : Node r2 = nm->mkNode(Kind::REGEXP_LOOP, lop, r[0]);
593 : 0 : retNode = dc == d_emptySingleton
594 : 0 : ? r2
595 : 0 : : nodeManager()->mkNode(Kind::REGEXP_CONCAT, dc, r2);
596 : 0 : }
597 : : else
598 : : {
599 : 0 : retNode = d_emptyRegexp;
600 : : }
601 : 0 : }
602 : 0 : break;
603 : : }
604 : 0 : case Kind::REGEXP_COMPLEMENT:
605 : : {
606 : : // don't know result
607 : 0 : return 0;
608 : : break;
609 : : }
610 : 0 : default:
611 : : {
612 : 0 : Assert(!utils::isRegExpKind(r.getKind()));
613 : 0 : return 0;
614 : : break;
615 : : }
616 : : }
617 [ - + ]: 35 : if (retNode != d_emptyRegexp)
618 : : {
619 : 0 : retNode = rewrite(retNode);
620 : : }
621 : 70 : std::pair<Node, int> p(retNode, ret);
622 : 35 : d_deriv_cache[dv] = p;
623 : : }
624 : :
625 : 84 : Trace("regexp-derive") << "RegExp-derive returns : /" << mkString(retNode)
626 : 42 : << "/" << std::endl;
627 : 42 : return ret;
628 : 42 : }
629 : :
630 : 0 : Node RegExpOpr::derivativeSingle(Node r, cvc5::internal::String c)
631 : : {
632 : 0 : Assert(c.size() < 2);
633 : 0 : Trace("regexp-derive") << "RegExp-derive starts with /" << mkString(r)
634 : 0 : << "/, c=" << c << std::endl;
635 : 0 : Node retNode = d_emptyRegexp;
636 : 0 : PairNodeStr dv = std::make_pair(r, c);
637 : 0 : NodeManager* nm = nodeManager();
638 [ - - ]: 0 : if (d_dv_cache.find(dv) != d_dv_cache.end())
639 : : {
640 : 0 : retNode = d_dv_cache[dv];
641 : : }
642 [ - - ]: 0 : else if (c.empty())
643 : : {
644 : 0 : Node exp;
645 : 0 : int tmp = delta(r, exp);
646 [ - - ]: 0 : if (tmp == 0)
647 : : {
648 : : // TODO variable
649 : 0 : retNode = d_emptyRegexp;
650 : : }
651 [ - - ]: 0 : else if (tmp == 1)
652 : : {
653 : 0 : retNode = r;
654 : : }
655 : : else
656 : : {
657 : 0 : retNode = d_emptyRegexp;
658 : : }
659 : 0 : }
660 : : else
661 : : {
662 : 0 : Kind k = r.getKind();
663 [ - - ][ - - ]: 0 : switch (k)
[ - - ][ - - ]
[ - - ]
664 : : {
665 : 0 : case Kind::REGEXP_NONE:
666 : : {
667 : 0 : retNode = d_emptyRegexp;
668 : 0 : break;
669 : : }
670 : 0 : case Kind::REGEXP_ALLCHAR:
671 : : {
672 : 0 : retNode = nodeManager()->mkNode(Kind::STRING_TO_REGEXP, d_emptyString);
673 : 0 : break;
674 : : }
675 : 0 : case Kind::REGEXP_RANGE:
676 : : {
677 : 0 : cvc5::internal::String a = r[0].getConst<String>();
678 : 0 : cvc5::internal::String b = r[1].getConst<String>();
679 : 0 : retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp;
680 : 0 : break;
681 : 0 : }
682 : 0 : case Kind::STRING_TO_REGEXP:
683 : : {
684 [ - - ]: 0 : if (r[0].isConst())
685 : : {
686 [ - - ]: 0 : if (r[0] == d_emptyString)
687 : : {
688 : 0 : retNode = d_emptyRegexp;
689 : : }
690 : : else
691 : : {
692 [ - - ]: 0 : if (r[0].getConst<String>().front() == c.front())
693 : : {
694 : 0 : retNode = nm->mkNode(Kind::STRING_TO_REGEXP,
695 : 0 : Word::getLength(r[0]) == 1
696 : 0 : ? d_emptyString
697 : 0 : : Word::substr(r[0], 1));
698 : : }
699 : : else
700 : : {
701 : 0 : retNode = d_emptyRegexp;
702 : : }
703 : : }
704 : : }
705 : : else
706 : : {
707 : : // TODO variable
708 : 0 : retNode = d_emptyRegexp;
709 : : }
710 : 0 : break;
711 : : }
712 : 0 : case Kind::REGEXP_CONCAT:
713 : : {
714 : : Node rees =
715 : 0 : nodeManager()->mkNode(Kind::STRING_TO_REGEXP, d_emptyString);
716 : 0 : std::vector<Node> vec_nodes;
717 [ - - ]: 0 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
718 : : {
719 : 0 : Node dc = derivativeSingle(r[i], c);
720 [ - - ]: 0 : if (dc != d_emptyRegexp)
721 : : {
722 : 0 : std::vector<Node> vec_nodes2;
723 [ - - ]: 0 : if (dc != rees)
724 : : {
725 : 0 : vec_nodes2.push_back(dc);
726 : : }
727 [ - - ]: 0 : for (unsigned j = i + 1; j < r.getNumChildren(); ++j)
728 : : {
729 [ - - ]: 0 : if (r[j] != rees)
730 : : {
731 : 0 : vec_nodes2.push_back(r[j]);
732 : : }
733 : : }
734 : : Node tmp =
735 : 0 : vec_nodes2.size() == 0 ? rees
736 : 0 : : vec_nodes2.size() == 1
737 : 0 : ? vec_nodes2[0]
738 : 0 : : nodeManager()->mkNode(Kind::REGEXP_CONCAT, vec_nodes2);
739 : 0 : if (std::find(vec_nodes.begin(), vec_nodes.end(), tmp)
740 [ - - ]: 0 : == vec_nodes.end())
741 : : {
742 : 0 : vec_nodes.push_back(tmp);
743 : : }
744 : 0 : }
745 : 0 : Node exp;
746 [ - - ]: 0 : if (delta(r[i], exp) != 1)
747 : : {
748 : 0 : break;
749 : : }
750 [ - - ][ - - ]: 0 : }
751 : : retNode =
752 : 0 : vec_nodes.size() == 0
753 : 0 : ? d_emptyRegexp
754 : 0 : : (vec_nodes.size() == 1
755 : 0 : ? vec_nodes[0]
756 : 0 : : nodeManager()->mkNode(Kind::REGEXP_UNION, vec_nodes));
757 : 0 : break;
758 : 0 : }
759 : 0 : case Kind::REGEXP_UNION:
760 : : {
761 : 0 : std::vector<Node> vec_nodes;
762 [ - - ]: 0 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
763 : : {
764 : 0 : Node dc = derivativeSingle(r[i], c);
765 [ - - ]: 0 : if (dc != d_emptyRegexp)
766 : : {
767 : 0 : if (std::find(vec_nodes.begin(), vec_nodes.end(), dc)
768 [ - - ]: 0 : == vec_nodes.end())
769 : : {
770 : 0 : vec_nodes.push_back(dc);
771 : : }
772 : : }
773 : : // Trace("regexp-derive") << "RegExp-derive OR R[" << i << "] /" <<
774 : : // mkString(r[i]) << "/ returns /" << mkString(dc) << "/" <<
775 : : // std::endl;
776 : 0 : }
777 : : retNode =
778 : 0 : vec_nodes.size() == 0
779 : 0 : ? d_emptyRegexp
780 : 0 : : (vec_nodes.size() == 1
781 : 0 : ? vec_nodes[0]
782 : 0 : : nodeManager()->mkNode(Kind::REGEXP_UNION, vec_nodes));
783 : 0 : break;
784 : 0 : }
785 : 0 : case Kind::REGEXP_INTER:
786 : : {
787 : 0 : bool flag = true;
788 : 0 : bool flag_sg = false;
789 : 0 : std::vector<Node> vec_nodes;
790 [ - - ]: 0 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
791 : : {
792 : 0 : Node dc = derivativeSingle(r[i], c);
793 [ - - ]: 0 : if (dc != d_emptyRegexp)
794 : : {
795 [ - - ]: 0 : if (dc == d_sigma_star)
796 : : {
797 : 0 : flag_sg = true;
798 : : }
799 : : else
800 : : {
801 : 0 : if (std::find(vec_nodes.begin(), vec_nodes.end(), dc)
802 [ - - ]: 0 : == vec_nodes.end())
803 : : {
804 : 0 : vec_nodes.push_back(dc);
805 : : }
806 : : }
807 : : }
808 : : else
809 : : {
810 : 0 : flag = false;
811 : 0 : break;
812 : : }
813 [ - - ]: 0 : }
814 [ - - ]: 0 : if (flag)
815 : : {
816 [ - - ][ - - ]: 0 : if (vec_nodes.size() == 0 && flag_sg)
[ - - ]
817 : : {
818 : 0 : retNode = d_sigma_star;
819 : : }
820 : : else
821 : : {
822 : 0 : retNode = vec_nodes.size() == 0
823 : 0 : ? d_emptyRegexp
824 : 0 : : (vec_nodes.size() == 1
825 : 0 : ? vec_nodes[0]
826 : : : nodeManager()->mkNode(Kind::REGEXP_INTER,
827 : 0 : vec_nodes));
828 : : }
829 : : }
830 : : else
831 : : {
832 : 0 : retNode = d_emptyRegexp;
833 : : }
834 : 0 : break;
835 : 0 : }
836 : 0 : case Kind::REGEXP_STAR:
837 : : {
838 : 0 : Node dc = derivativeSingle(r[0], c);
839 [ - - ]: 0 : if (dc != d_emptyRegexp)
840 : : {
841 : 0 : retNode = dc == d_emptySingleton
842 : 0 : ? r
843 : 0 : : nodeManager()->mkNode(Kind::REGEXP_CONCAT, dc, r);
844 : : }
845 : : else
846 : : {
847 : 0 : retNode = d_emptyRegexp;
848 : : }
849 : 0 : break;
850 : 0 : }
851 : 0 : case Kind::REGEXP_LOOP:
852 : : {
853 : 0 : uint32_t l = utils::getLoopMinOccurrences(r);
854 : 0 : uint32_t u = utils::getLoopMaxOccurrences(r);
855 [ - - ][ - - ]: 0 : if (l == u || l == 0)
856 : : {
857 : 0 : retNode = d_emptyRegexp;
858 : : }
859 : : else
860 : : {
861 : 0 : Node dc = derivativeSingle(r[0], c);
862 [ - - ]: 0 : if (dc != d_emptyRegexp)
863 : : {
864 [ - - ]: 0 : Node lop = nm->mkConst(RegExpLoop(l == 0 ? 0 : (l - 1), u - 1));
865 : 0 : Node r2 = nm->mkNode(Kind::REGEXP_LOOP, lop, r[0]);
866 : 0 : retNode = dc == d_emptySingleton
867 : 0 : ? r2
868 : 0 : : nodeManager()->mkNode(Kind::REGEXP_CONCAT, dc, r2);
869 : 0 : }
870 : : else
871 : : {
872 : 0 : retNode = d_emptyRegexp;
873 : : }
874 : 0 : }
875 : : // Trace("regexp-derive") << "RegExp-derive : REGEXP_LOOP returns /" <<
876 : : // mkString(retNode) << "/" << std::endl;
877 : 0 : break;
878 : : }
879 : 0 : case Kind::REGEXP_COMPLEMENT:
880 : : default:
881 : : {
882 : 0 : Trace("strings-error") << "Unsupported term: " << mkString(r)
883 : 0 : << " in derivative of RegExp." << std::endl;
884 : 0 : Unreachable();
885 : : break;
886 : : }
887 : : }
888 [ - - ]: 0 : if (retNode != d_emptyRegexp)
889 : : {
890 : 0 : retNode = rewrite(retNode);
891 : : }
892 : 0 : d_dv_cache[dv] = retNode;
893 : : }
894 : 0 : Trace("regexp-derive") << "RegExp-derive returns : /" << mkString(retNode)
895 : 0 : << "/" << std::endl;
896 : 0 : return retNode;
897 : 0 : }
898 : :
899 : 0 : void RegExpOpr::firstChars(Node r, std::set<unsigned>& pcset, SetNodes& pvset)
900 : : {
901 : 0 : Trace("regexp-fset") << "Start FSET(" << mkString(r) << ")" << std::endl;
902 : : std::map<Node, std::pair<std::set<unsigned>, SetNodes> >::const_iterator itr =
903 : 0 : d_fset_cache.find(r);
904 [ - - ]: 0 : if (itr != d_fset_cache.end())
905 : : {
906 : 0 : pcset.insert((itr->second).first.begin(), (itr->second).first.end());
907 : 0 : pvset.insert((itr->second).second.begin(), (itr->second).second.end());
908 : : }
909 : : else
910 : : {
911 : : // cset is code points
912 : 0 : std::set<unsigned> cset;
913 : 0 : SetNodes vset;
914 : 0 : Kind k = r.getKind();
915 [ - - ][ - - ]: 0 : switch (k)
[ - - ][ - - ]
[ - ]
916 : : {
917 : 0 : case Kind::REGEXP_NONE:
918 : : {
919 : 0 : break;
920 : : }
921 : 0 : case Kind::REGEXP_RANGE:
922 : : {
923 : 0 : unsigned a = r[0].getConst<String>().front();
924 : 0 : unsigned b = r[1].getConst<String>().front();
925 : 0 : Assert(a < b);
926 : 0 : Assert(b < std::numeric_limits<unsigned>::max());
927 [ - - ]: 0 : for (unsigned c = a; c <= b; c++)
928 : : {
929 : 0 : cset.insert(c);
930 : : }
931 : 0 : break;
932 : : }
933 : 0 : case Kind::STRING_TO_REGEXP:
934 : : {
935 : 0 : Node st = rewrite(r[0]);
936 [ - - ]: 0 : if (st.isConst())
937 : : {
938 : 0 : String s = st.getConst<String>();
939 [ - - ]: 0 : if (s.size() != 0)
940 : : {
941 : 0 : unsigned sc = s.front();
942 : 0 : cset.insert(sc);
943 : : }
944 : 0 : }
945 [ - - ]: 0 : else if (st.getKind() == Kind::STRING_CONCAT)
946 : : {
947 [ - - ]: 0 : if (st[0].isConst())
948 : : {
949 : 0 : String s = st[0].getConst<String>();
950 : 0 : unsigned sc = s.front();
951 : 0 : cset.insert(sc);
952 : 0 : }
953 : : else
954 : : {
955 : 0 : vset.insert(st[0]);
956 : : }
957 : : }
958 : : else
959 : : {
960 : 0 : vset.insert(st);
961 : : }
962 : 0 : break;
963 : 0 : }
964 : 0 : case Kind::REGEXP_CONCAT:
965 : : {
966 [ - - ]: 0 : for (unsigned i = 0; i < r.getNumChildren(); i++)
967 : : {
968 : 0 : firstChars(r[i], cset, vset);
969 : 0 : Node n = r[i];
970 : 0 : Node exp;
971 [ - - ]: 0 : if (delta(n, exp) != 1)
972 : : {
973 : 0 : break;
974 : : }
975 [ - - ][ - - ]: 0 : }
976 : 0 : break;
977 : : }
978 : 0 : case Kind::REGEXP_UNION:
979 : : {
980 [ - - ]: 0 : for (unsigned i = 0; i < r.getNumChildren(); i++)
981 : : {
982 : 0 : firstChars(r[i], cset, vset);
983 : : }
984 : 0 : break;
985 : : }
986 : 0 : case Kind::REGEXP_INTER:
987 : : {
988 : : // TODO: Overapproximation for now
989 : : // for(unsigned i=0; i<r.getNumChildren(); i++) {
990 : : // firstChars(r[i], cset, vset);
991 : : // }
992 : 0 : firstChars(r[0], cset, vset);
993 : 0 : break;
994 : : }
995 : 0 : case Kind::REGEXP_STAR:
996 : : {
997 : 0 : firstChars(r[0], cset, vset);
998 : 0 : break;
999 : : }
1000 : 0 : case Kind::REGEXP_LOOP:
1001 : : {
1002 : 0 : firstChars(r[0], cset, vset);
1003 : 0 : break;
1004 : : }
1005 : 0 : case Kind::REGEXP_ALLCHAR:
1006 : : case Kind::REGEXP_COMPLEMENT:
1007 : : default:
1008 : : {
1009 : : // we do not expect to call this function on regular expressions that
1010 : : // aren't a standard regular expression kind. However, if we do, then
1011 : : // the following code is conservative and says that the current
1012 : : // regular expression can begin with any character.
1013 : 0 : Assert(utils::isRegExpKind(k));
1014 : : // can start with any character
1015 : 0 : Assert(d_lastchar < std::numeric_limits<unsigned>::max());
1016 [ - - ]: 0 : for (unsigned i = 0; i <= d_lastchar; i++)
1017 : : {
1018 : 0 : cset.insert(i);
1019 : : }
1020 : 0 : break;
1021 : : }
1022 : : }
1023 : 0 : pcset.insert(cset.begin(), cset.end());
1024 : 0 : pvset.insert(vset.begin(), vset.end());
1025 : 0 : std::pair<std::set<unsigned>, SetNodes> p(cset, vset);
1026 : 0 : d_fset_cache[r] = p;
1027 : 0 : }
1028 : :
1029 [ - - ]: 0 : if (TraceIsOn("regexp-fset"))
1030 : : {
1031 : 0 : Trace("regexp-fset") << "END FSET(" << mkString(r) << ") = {";
1032 : 0 : for (std::set<unsigned>::const_iterator it = pcset.begin();
1033 [ - - ]: 0 : it != pcset.end();
1034 : 0 : ++it)
1035 : : {
1036 [ - - ]: 0 : if (it != pcset.begin())
1037 : : {
1038 [ - - ]: 0 : Trace("regexp-fset") << ",";
1039 : : }
1040 [ - - ]: 0 : Trace("regexp-fset") << (*it);
1041 : : }
1042 [ - - ]: 0 : Trace("regexp-fset") << "}" << std::endl;
1043 : : }
1044 : 0 : }
1045 : :
1046 : 880 : Node RegExpOpr::simplify(Node t, bool polarity)
1047 : : {
1048 [ + - ]: 1760 : Trace("strings-regexp-simpl")
1049 : 880 : << "RegExpOpr::simplify: " << t << ", polarity=" << polarity << std::endl;
1050 [ - + ][ - + ]: 880 : Assert(t.getKind() == Kind::STRING_IN_REGEXP);
[ - - ]
1051 [ + + ]: 880 : Node tlit = polarity ? t : t.notNode();
1052 : 880 : Node conc;
1053 : 880 : std::map<Node, Node>::const_iterator itr = d_simpCache.find(tlit);
1054 [ + + ]: 880 : if (itr != d_simpCache.end())
1055 : : {
1056 : 8 : return itr->second;
1057 : : }
1058 [ + + ]: 872 : if (polarity)
1059 : : {
1060 : 801 : std::vector<Node> newSkolems;
1061 : 801 : conc = reduceRegExpPos(nodeManager(), tlit, d_sc, newSkolems);
1062 : 801 : }
1063 : : else
1064 : : {
1065 : : // see if we can use an optimized version of the reduction for re.++.
1066 : 71 : Node r = t[1];
1067 [ + + ]: 71 : if (r.getKind() == Kind::REGEXP_CONCAT)
1068 : : {
1069 : : // the index we are removing from the RE concatenation
1070 : : bool isRev;
1071 : : // As an optimization to the reduction, if we can determine that
1072 : : // all strings in the language of R1 have the same length, say n,
1073 : : // then the conclusion of the reduction is quantifier-free:
1074 : : // ~( substr(s,0,n) in R1 ) OR ~( substr(s,len(s)-n,n) in R2)
1075 : 65 : Node reLen = getRegExpConcatFixed(r, isRev);
1076 [ + + ]: 65 : if (!reLen.isNull())
1077 : : {
1078 : 59 : conc = reduceRegExpNegConcatFixed(nodeManager(), tlit, reLen, isRev);
1079 : : }
1080 : 65 : }
1081 [ + + ]: 71 : if (conc.isNull())
1082 : : {
1083 : 12 : conc = reduceRegExpNeg(nodeManager(), tlit);
1084 : : }
1085 : 71 : }
1086 : 872 : d_simpCache[tlit] = conc;
1087 [ + - ]: 1744 : Trace("strings-regexp-simpl")
1088 : 872 : << "RegExpOpr::simplify: returns " << conc << std::endl;
1089 : 872 : return conc;
1090 : 880 : }
1091 : :
1092 : 93 : Node RegExpOpr::getRegExpConcatFixed(Node r, bool& isRev)
1093 : : {
1094 [ - + ][ - + ]: 93 : Assert(r.getKind() == Kind::REGEXP_CONCAT);
[ - - ]
1095 : 93 : isRev = false;
1096 : 186 : Node reLen = RegExpEntail::getFixedLengthForRegexp(r[0]);
1097 [ + + ]: 93 : if (!reLen.isNull())
1098 : : {
1099 : 50 : return reLen;
1100 : : }
1101 : : // try from the opposite end
1102 : 43 : size_t indexE = r.getNumChildren() - 1;
1103 : 43 : reLen = RegExpEntail::getFixedLengthForRegexp(r[indexE]);
1104 [ + + ]: 43 : if (!reLen.isNull())
1105 : : {
1106 : 37 : isRev = true;
1107 : 37 : return reLen;
1108 : : }
1109 : 6 : return Node::null();
1110 : 93 : }
1111 : :
1112 : 12 : Node RegExpOpr::reduceRegExpNeg(NodeManager* nm, Node mem)
1113 : : {
1114 : 12 : Assert(mem.getKind() == Kind::NOT
1115 : : && mem[0].getKind() == Kind::STRING_IN_REGEXP);
1116 : 12 : Node s = mem[0][0];
1117 : 12 : Node r = mem[0][1];
1118 : 12 : Kind k = r.getKind();
1119 : 12 : Node zero = nm->mkConstInt(Rational(0));
1120 : 12 : Node conc;
1121 [ + + ]: 12 : if (k == Kind::REGEXP_CONCAT)
1122 : : {
1123 : : // do not use length entailment, call regular expression concat
1124 : 6 : Node reLen;
1125 : 6 : conc = reduceRegExpNegConcatFixed(nm, mem, reLen, false);
1126 : 6 : }
1127 [ + - ]: 6 : else if (k == Kind::REGEXP_STAR)
1128 : : {
1129 : 6 : Node emp = Word::mkEmptyWord(s.getType());
1130 : 6 : Node lens = nm->mkNode(Kind::STRING_LENGTH, s);
1131 : 6 : Node sne = s.eqNode(emp).negate();
1132 : 6 : Node b1 = SkolemCache::mkIndexVar(nm, mem);
1133 : 6 : Node b1v = nm->mkNode(Kind::BOUND_VAR_LIST, b1);
1134 : 12 : Node g11n = nm->mkNode(Kind::LEQ, b1, zero);
1135 : 12 : Node g12n = nm->mkNode(Kind::LT, lens, b1);
1136 : : // internal
1137 : 12 : Node s1 = utils::mkPrefix(s, b1);
1138 : 12 : Node s2 = utils::mkSuffix(s, b1);
1139 : 12 : Node s1r1 = nm->mkNode(Kind::STRING_IN_REGEXP, s1, r[0]).negate();
1140 : 12 : Node s2r2 = nm->mkNode(Kind::STRING_IN_REGEXP, s2, r).negate();
1141 : :
1142 [ + + ][ - - ]: 30 : conc = nm->mkNode(Kind::OR, {g11n, g12n, s1r1, s2r2});
1143 : : // must mark as an internal quantifier
1144 : 6 : conc = utils::mkForallInternal(nm, b1v, conc);
1145 : 6 : conc = nm->mkNode(Kind::AND, sne, conc);
1146 : 6 : }
1147 : : else
1148 : : {
1149 : 0 : Assert(!utils::isRegExpKind(k));
1150 : : }
1151 : 24 : return conc;
1152 : 12 : }
1153 : :
1154 : 107 : Node RegExpOpr::reduceRegExpNegConcatFixed(NodeManager* nm,
1155 : : Node mem,
1156 : : Node reLen,
1157 : : bool isRev)
1158 : : {
1159 : 107 : Assert(mem.getKind() == Kind::NOT
1160 : : && mem[0].getKind() == Kind::STRING_IN_REGEXP);
1161 : 107 : Node s = mem[0][0];
1162 : 107 : Node r = mem[0][1];
1163 [ - + ][ - + ]: 107 : Assert(r.getKind() == Kind::REGEXP_CONCAT);
[ - - ]
1164 : 107 : Node zero = nm->mkConstInt(Rational(0));
1165 : : // The following simplification states that
1166 : : // ~( s in R1 ++ R2 ++... ++ Rn )
1167 : : // is equivalent to
1168 : : // forall x.
1169 : : // 0 <= x <= len(s) =>
1170 : : // ~(substr(s,0,x) in R1) OR ~(substr(s,x,len(s)-x) in R2 ++ ... ++ Rn)
1171 : : // Index is the child index of r that we are stripping off, which is either
1172 : : // from the beginning or the end.
1173 : 107 : Node lens = nm->mkNode(Kind::STRING_LENGTH, s);
1174 : 107 : Node b1;
1175 : 107 : Node b1v;
1176 : 107 : Node guard1n, guard2n;
1177 [ + + ]: 107 : if (reLen.isNull())
1178 : : {
1179 : 6 : b1 = SkolemCache::mkIndexVar(nm, mem);
1180 : 6 : b1v = nm->mkNode(Kind::BOUND_VAR_LIST, b1);
1181 : 6 : guard1n = nm->mkNode(Kind::LT, b1, zero);
1182 : 6 : guard2n = nm->mkNode(Kind::LT, nm->mkNode(Kind::STRING_LENGTH, s), b1);
1183 : : }
1184 : : else
1185 : : {
1186 : 101 : b1 = reLen;
1187 : : }
1188 : 107 : Node s1;
1189 : 107 : Node s2;
1190 [ + + ]: 107 : if (!isRev)
1191 : : {
1192 : 64 : s1 = utils::mkPrefix(s, b1);
1193 : 64 : s2 = utils::mkSuffix(s, b1);
1194 : : }
1195 : : else
1196 : : {
1197 : 43 : s1 = utils::mkSuffixOfLen(s, b1);
1198 : 43 : s2 = utils::mkPrefix(s, nm->mkNode(Kind::SUB, lens, b1));
1199 : : }
1200 [ + + ]: 107 : size_t index = isRev ? r.getNumChildren() - 1 : 0;
1201 : 214 : Node s1r1 = nm->mkNode(Kind::STRING_IN_REGEXP, s1, r[index]).negate();
1202 : 107 : std::vector<Node> nvec;
1203 [ + + ]: 427 : for (unsigned i = 0, nchild = r.getNumChildren(); i < nchild; i++)
1204 : : {
1205 [ + + ]: 320 : if (i != index)
1206 : : {
1207 : 213 : nvec.push_back(r[i]);
1208 : : }
1209 : : }
1210 [ + + ]: 107 : Node r2 = nvec.size() == 1 ? nvec[0] : nm->mkNode(Kind::REGEXP_CONCAT, nvec);
1211 : 214 : Node s2r2 = nm->mkNode(Kind::STRING_IN_REGEXP, s2, r2).negate();
1212 : 107 : Node conc;
1213 [ + + ]: 107 : if (!b1v.isNull())
1214 : : {
1215 [ + + ][ - - ]: 30 : conc = nm->mkNode(Kind::OR, {guard1n, guard2n, s1r1, s2r2});
1216 : : // must mark as an internal quantifier
1217 : 6 : conc = utils::mkForallInternal(nm, b1v, conc);
1218 : : }
1219 : : else
1220 : : {
1221 : 101 : conc = nm->mkNode(Kind::OR, s1r1, s2r2);
1222 : : }
1223 : 214 : return conc;
1224 : 107 : }
1225 : :
1226 : 1771 : Node RegExpOpr::reduceRegExpPos(NodeManager* nm,
1227 : : Node mem,
1228 : : SkolemCache* sc,
1229 : : std::vector<Node>& newSkolems)
1230 : : {
1231 [ - + ][ - + ]: 1771 : Assert(mem.getKind() == Kind::STRING_IN_REGEXP);
[ - - ]
1232 : 1771 : Node s = mem[0];
1233 : 1771 : Node r = mem[1];
1234 : 1771 : Kind k = r.getKind();
1235 : 1771 : Node conc;
1236 [ + + ]: 1771 : if (k == Kind::REGEXP_CONCAT)
1237 : : {
1238 : 1289 : std::vector<Node> nvec;
1239 : 1289 : std::vector<Node> cc;
1240 : 1289 : SkolemManager* sm = nm->getSkolemManager();
1241 : : // Look up skolems for each of the components. If sc has optimizations
1242 : : // enabled, this will return arguments of str.to_re.
1243 [ + + ]: 4865 : for (unsigned i = 0, nchild = r.getNumChildren(); i < nchild; ++i)
1244 : : {
1245 [ + + ]: 3576 : if (r[i].getKind() == Kind::STRING_TO_REGEXP)
1246 : : {
1247 : : // optimization, just take the body
1248 : 1277 : newSkolems.push_back(r[i][0]);
1249 : : }
1250 : : else
1251 : : {
1252 : 2299 : Node ivalue = nm->mkConstInt(Rational(i));
1253 : 6897 : Node sk = sm->mkSkolemFunction(SkolemId::RE_UNFOLD_POS_COMPONENT,
1254 : 4598 : {mem[0], mem[1], ivalue});
1255 : 2299 : newSkolems.push_back(sk);
1256 : 2299 : nvec.push_back(nm->mkNode(Kind::STRING_IN_REGEXP, newSkolems[i], r[i]));
1257 : 2299 : }
1258 : : }
1259 : : // (str.in_re x (re.++ R0 .... Rn)) =>
1260 : : // (and (= x (str.++ k0 ... kn)) (str.in_re k0 R0) ... (str.in_re kn Rn) )
1261 : 1289 : Node lem = s.eqNode(nm->mkNode(Kind::STRING_CONCAT, newSkolems));
1262 : 1289 : nvec.insert(nvec.begin(), lem);
1263 [ - + ]: 1289 : conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(Kind::AND, nvec);
1264 : 1289 : }
1265 [ + - ]: 482 : else if (k == Kind::REGEXP_STAR)
1266 : : {
1267 : 482 : Node emp = Word::mkEmptyWord(s.getType());
1268 : 482 : Node se = s.eqNode(emp);
1269 : 964 : Node sinr = nm->mkNode(Kind::STRING_IN_REGEXP, s, r[0]);
1270 : 964 : Node reExpand = nm->mkNode(Kind::REGEXP_CONCAT, r[0], r, r[0]);
1271 : 964 : Node sinRExp = nm->mkNode(Kind::STRING_IN_REGEXP, s, reExpand);
1272 : : // We unfold `x in R*` by considering three cases: `x` is empty, `x`
1273 : : // is matched by `R`, or `x` is matched by two or more `R`s. For the
1274 : : // last case, `x` will break into three pieces, making the beginning
1275 : : // and the end each match `R` and the middle match `R*`. Matching the
1276 : : // beginning and the end with `R` allows us to reason about the
1277 : : // beginning and the end of `x` simultaneously.
1278 : : //
1279 : : // x in R* ---> (x = "") v (x in R) v (x in (re.++ R (re.* R) R))
1280 : :
1281 : : // We also immediately unfold the last disjunct for re.*. The advantage
1282 : : // of doing this is that we use the same scheme for skolems above.
1283 : 482 : std::vector<Node> newSkolemsC;
1284 : 482 : sinRExp = reduceRegExpPos(nm, sinRExp, sc, newSkolemsC);
1285 [ - + ][ - + ]: 482 : Assert(newSkolemsC.size() == 3);
[ - - ]
1286 : : // make the return lemma
1287 : : // can also assume the component match the first and last R are non-empty.
1288 : : // This means that the overall conclusion is:
1289 : : // (x = "") v (x in R) v (x = (str.++ k1 k2 k3) ^
1290 : : // k1 in R ^ k2 in (re.* R) ^ k3 in R ^
1291 : : // k1 != "" ^ k3 != "")
1292 : 964 : conc = nm->mkNode(Kind::OR,
1293 : : se,
1294 : : sinr,
1295 [ + + ][ - - ]: 3374 : nm->mkNode(Kind::AND,
1296 : : {sinRExp,
1297 : 964 : newSkolemsC[0].eqNode(emp).negate(),
1298 : 1446 : newSkolemsC[2].eqNode(emp).negate()}));
1299 : 482 : }
1300 : : else
1301 : : {
1302 : 0 : Assert(!utils::isRegExpKind(k));
1303 : : }
1304 : 3542 : return conc;
1305 : 1771 : }
1306 : :
1307 : 0 : bool RegExpOpr::isPairNodesInSet(std::set<PairNodes>& s, Node n1, Node n2)
1308 : : {
1309 [ - - ]: 0 : for (std::set<PairNodes>::const_iterator itr = s.begin(); itr != s.end();
1310 : 0 : ++itr)
1311 : : {
1312 [ - - ]: 0 : if ((itr->first == n1 && itr->second == n2)
1313 : 0 : || (itr->first == n2 && itr->second == n1))
1314 : : {
1315 : 0 : return true;
1316 : : }
1317 : : }
1318 : 0 : return false;
1319 : : }
1320 : :
1321 : 0 : bool RegExpOpr::containC2(unsigned cnt, Node n)
1322 : : {
1323 [ - - ]: 0 : if (n.getKind() == Kind::REGEXP_RV)
1324 : : {
1325 : 0 : Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()))
1326 : 0 : << "Exceeded UINT32_MAX in RegExpOpr::containC2";
1327 : 0 : unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
1328 : 0 : return cnt == y;
1329 : : }
1330 [ - - ]: 0 : else if (n.getKind() == Kind::REGEXP_CONCAT)
1331 : : {
1332 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
1333 : : {
1334 [ - - ]: 0 : if (containC2(cnt, n[i]))
1335 : : {
1336 : 0 : return true;
1337 : : }
1338 : : }
1339 : : }
1340 [ - - ]: 0 : else if (n.getKind() == Kind::REGEXP_STAR)
1341 : : {
1342 : 0 : return containC2(cnt, n[0]);
1343 : : }
1344 [ - - ]: 0 : else if (n.getKind() == Kind::REGEXP_LOOP)
1345 : : {
1346 : 0 : return containC2(cnt, n[0]);
1347 : : }
1348 [ - - ]: 0 : else if (n.getKind() == Kind::REGEXP_UNION)
1349 : : {
1350 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
1351 : : {
1352 [ - - ]: 0 : if (containC2(cnt, n[i]))
1353 : : {
1354 : 0 : return true;
1355 : : }
1356 : : }
1357 : : }
1358 : 0 : return false;
1359 : : }
1360 : 0 : Node RegExpOpr::convert1(unsigned cnt, Node n)
1361 : : {
1362 [ - - ]: 0 : Trace("regexp-debug") << "Converting " << n << " at " << cnt << "... "
1363 : 0 : << std::endl;
1364 : 0 : Node r1, r2;
1365 : 0 : convert2(cnt, n, r1, r2);
1366 [ - - ]: 0 : Trace("regexp-debug") << "... getting r1=" << r1 << ", and r2=" << r2
1367 : 0 : << std::endl;
1368 : : Node ret =
1369 : 0 : r1 == d_emptySingleton
1370 : : ? r2
1371 : 0 : : nodeManager()->mkNode(Kind::REGEXP_CONCAT,
1372 : 0 : nodeManager()->mkNode(Kind::REGEXP_STAR, r1),
1373 : 0 : r2);
1374 : 0 : ret = rewrite(ret);
1375 [ - - ]: 0 : Trace("regexp-debug") << "... done convert at " << cnt << ", with return "
1376 : 0 : << ret << std::endl;
1377 : 0 : return ret;
1378 : 0 : }
1379 : 0 : void RegExpOpr::convert2(unsigned cnt, Node n, Node& r1, Node& r2)
1380 : : {
1381 [ - - ]: 0 : if (n == d_emptyRegexp)
1382 : : {
1383 : 0 : r1 = d_emptyRegexp;
1384 : 0 : r2 = d_emptyRegexp;
1385 : 0 : return;
1386 : : }
1387 [ - - ]: 0 : else if (n == d_emptySingleton)
1388 : : {
1389 : 0 : r1 = d_emptySingleton;
1390 : 0 : r2 = d_emptySingleton;
1391 : : }
1392 : 0 : Kind nk = n.getKind();
1393 [ - - ]: 0 : if (nk == Kind::REGEXP_RV)
1394 : : {
1395 : 0 : Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()))
1396 : 0 : << "Exceeded UINT32_MAX in RegExpOpr::convert2";
1397 : 0 : unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
1398 : 0 : r1 = d_emptySingleton;
1399 [ - - ]: 0 : if (cnt == y)
1400 : : {
1401 : 0 : r2 = d_emptyRegexp;
1402 : : }
1403 : : else
1404 : : {
1405 : 0 : r2 = n;
1406 : : }
1407 : : }
1408 [ - - ]: 0 : else if (nk == Kind::REGEXP_CONCAT)
1409 : : {
1410 : 0 : bool flag = true;
1411 : 0 : std::vector<Node> vr1, vr2;
1412 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
1413 : : {
1414 [ - - ]: 0 : if (containC2(cnt, n[i]))
1415 : : {
1416 : 0 : Node t1, t2;
1417 : 0 : convert2(cnt, n[i], t1, t2);
1418 : 0 : vr1.push_back(t1);
1419 : 0 : r1 = vr1.size() == 0 ? d_emptyRegexp
1420 : 0 : : vr1.size() == 1
1421 : 0 : ? vr1[0]
1422 : 0 : : nodeManager()->mkNode(Kind::REGEXP_CONCAT, vr1);
1423 : 0 : vr2.push_back(t2);
1424 [ - - ]: 0 : for (unsigned j = i + 1; j < n.getNumChildren(); j++)
1425 : : {
1426 : 0 : vr2.push_back(n[j]);
1427 : : }
1428 : 0 : r2 = vr2.size() == 0 ? d_emptyRegexp
1429 : 0 : : vr2.size() == 1
1430 : 0 : ? vr2[0]
1431 : 0 : : nodeManager()->mkNode(Kind::REGEXP_CONCAT, vr2);
1432 : 0 : flag = false;
1433 : 0 : break;
1434 : 0 : }
1435 : : else
1436 : : {
1437 : 0 : vr1.push_back(n[i]);
1438 : : }
1439 : : }
1440 [ - - ]: 0 : if (flag)
1441 : : {
1442 : 0 : r1 = d_emptySingleton;
1443 : 0 : r2 = n;
1444 : : }
1445 : 0 : }
1446 [ - - ]: 0 : else if (nk == Kind::REGEXP_UNION)
1447 : : {
1448 : 0 : std::vector<Node> vr1, vr2;
1449 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
1450 : : {
1451 : 0 : Node t1, t2;
1452 : 0 : convert2(cnt, n[i], t1, t2);
1453 : 0 : vr1.push_back(t1);
1454 : 0 : vr2.push_back(t2);
1455 : 0 : }
1456 : 0 : r1 = nodeManager()->mkNode(Kind::REGEXP_UNION, vr1);
1457 : 0 : r2 = nodeManager()->mkNode(Kind::REGEXP_UNION, vr2);
1458 : 0 : }
1459 [ - - ][ - - ]: 0 : else if (nk == Kind::STRING_TO_REGEXP || nk == Kind::REGEXP_ALLCHAR
1460 [ - - ][ - - ]: 0 : || nk == Kind::REGEXP_RANGE || nk == Kind::REGEXP_COMPLEMENT
1461 [ - - ]: 0 : || nk == Kind::REGEXP_LOOP)
1462 : : {
1463 : : // this leaves n unchanged
1464 : 0 : r1 = d_emptySingleton;
1465 : 0 : r2 = n;
1466 : : }
1467 : : else
1468 : : {
1469 : : // is it possible?
1470 : 0 : Unreachable();
1471 : : }
1472 : : }
1473 : :
1474 : 0 : Node RegExpOpr::intersectInternal(Node r1,
1475 : : Node r2,
1476 : : std::map<PairNodes, Node> cache,
1477 : : unsigned cnt)
1478 : : {
1479 : : // Assert(checkConstRegExp(r1) && checkConstRegExp(r2));
1480 [ - - ]: 0 : if (r1 > r2)
1481 : : {
1482 : 0 : TNode tmpNode = r1;
1483 : 0 : r1 = r2;
1484 : 0 : r2 = tmpNode;
1485 : 0 : }
1486 : 0 : NodeManager* nm = nodeManager();
1487 [ - - ]: 0 : Trace("regexp-int") << "Starting INTERSECT(" << cnt << "):\n "
1488 : 0 : << mkString(r1) << ",\n " << mkString(r2) << std::endl;
1489 : 0 : std::pair<Node, Node> p(r1, r2);
1490 : 0 : std::map<PairNodes, Node>::const_iterator itr = d_inter_cache.find(p);
1491 : 0 : Node rNode;
1492 [ - - ]: 0 : if (itr != d_inter_cache.end())
1493 : : {
1494 : 0 : rNode = itr->second;
1495 : : }
1496 : : else
1497 : : {
1498 [ - - ]: 0 : Trace("regexp-int-debug") << " ... not in cache" << std::endl;
1499 : 0 : if (r1 == d_emptyRegexp || r2 == d_emptyRegexp)
1500 : : {
1501 [ - - ]: 0 : Trace("regexp-int-debug") << " ... one is empty set" << std::endl;
1502 : 0 : rNode = d_emptyRegexp;
1503 : : }
1504 : 0 : else if (r1 == d_emptySingleton || r2 == d_emptySingleton)
1505 : : {
1506 [ - - ]: 0 : Trace("regexp-int-debug") << " ... one is empty singleton" << std::endl;
1507 : 0 : Node exp;
1508 [ - - ]: 0 : int r = delta((r1 == d_emptySingleton ? r2 : r1), exp);
1509 [ - - ]: 0 : if (r == 0)
1510 : : {
1511 : : // TODO: variable
1512 : 0 : Unreachable();
1513 : : }
1514 [ - - ]: 0 : else if (r == 1)
1515 : : {
1516 : 0 : rNode = d_emptySingleton;
1517 : : }
1518 : : else
1519 : : {
1520 : 0 : rNode = d_emptyRegexp;
1521 : : }
1522 : 0 : }
1523 [ - - ]: 0 : else if (r1 == r2)
1524 : : {
1525 [ - - ]: 0 : Trace("regexp-int-debug") << " ... equal" << std::endl;
1526 : 0 : rNode = r1; // convert1(cnt, r1);
1527 : : }
1528 : : else
1529 : : {
1530 [ - - ]: 0 : Trace("regexp-int-debug") << " ... normal checking" << std::endl;
1531 : 0 : std::map<PairNodes, Node>::const_iterator itrcache = cache.find(p);
1532 [ - - ]: 0 : if (itrcache != cache.end())
1533 : : {
1534 : 0 : rNode = itrcache->second;
1535 : : }
1536 : : else
1537 : : {
1538 [ - - ]: 0 : Trace("regexp-int-debug") << " ... normal without cache" << std::endl;
1539 : 0 : std::vector<unsigned> cset;
1540 : 0 : std::set<unsigned> cset1, cset2;
1541 : 0 : std::set<Node> vset1, vset2;
1542 : 0 : firstChars(r1, cset1, vset1);
1543 : 0 : firstChars(r2, cset2, vset2);
1544 [ - - ]: 0 : Trace("regexp-int-debug") << " ... got fset" << std::endl;
1545 : 0 : std::set_intersection(cset1.begin(),
1546 : : cset1.end(),
1547 : : cset2.begin(),
1548 : : cset2.end(),
1549 : : std::inserter(cset, cset.begin()));
1550 : 0 : std::vector<Node> vec_nodes;
1551 : 0 : Node delta_exp;
1552 [ - - ]: 0 : Trace("regexp-int-debug") << " ... try delta" << std::endl;
1553 : 0 : int flag = delta(r1, delta_exp);
1554 : 0 : int flag2 = delta(r2, delta_exp);
1555 [ - - ]: 0 : Trace("regexp-int-debug")
1556 : 0 : << " ... delta1=" << flag << ", delta2=" << flag2 << std::endl;
1557 [ - - ][ - - ]: 0 : if (flag != 2 && flag2 != 2)
1558 : : {
1559 [ - - ][ - - ]: 0 : if (flag == 1 && flag2 == 1)
1560 : : {
1561 : 0 : vec_nodes.push_back(d_emptySingleton);
1562 : : }
1563 : : else
1564 : : {
1565 : : // TODO: variable
1566 : 0 : Unreachable();
1567 : : }
1568 : : }
1569 [ - - ]: 0 : if (TraceIsOn("regexp-int-debug"))
1570 : : {
1571 [ - - ]: 0 : Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {";
1572 : 0 : for (std::vector<unsigned>::const_iterator it = cset.begin();
1573 [ - - ]: 0 : it != cset.end();
1574 : 0 : ++it)
1575 : : {
1576 [ - - ]: 0 : if (it != cset.begin())
1577 : : {
1578 [ - - ]: 0 : Trace("regexp-int-debug") << ", ";
1579 : : }
1580 [ - - ]: 0 : Trace("regexp-int-debug") << (*it);
1581 : : }
1582 [ - - ]: 0 : Trace("regexp-int-debug") << std::endl;
1583 : : }
1584 : 0 : std::map<PairNodes, Node> cacheX;
1585 : 0 : for (std::vector<unsigned>::const_iterator it = cset.begin();
1586 [ - - ]: 0 : it != cset.end();
1587 : 0 : ++it)
1588 : : {
1589 : 0 : std::vector<unsigned> cvec;
1590 : 0 : cvec.push_back(*it);
1591 : 0 : String c(cvec);
1592 [ - - ]: 0 : Trace("regexp-int-debug")
1593 : 0 : << "Try character " << c << " ... " << std::endl;
1594 : 0 : Node r1l = derivativeSingle(r1, c);
1595 : 0 : Node r2l = derivativeSingle(r2, c);
1596 [ - - ]: 0 : Trace("regexp-int-debug")
1597 : 0 : << " ... got partial(r1,c) = " << mkString(r1l) << std::endl;
1598 [ - - ]: 0 : Trace("regexp-int-debug")
1599 : 0 : << " ... got partial(r2,c) = " << mkString(r2l) << std::endl;
1600 : 0 : Node rt;
1601 : :
1602 [ - - ]: 0 : if (r1l > r2l)
1603 : : {
1604 : 0 : Node tnode = r1l;
1605 : 0 : r1l = r2l;
1606 : 0 : r2l = tnode;
1607 : 0 : }
1608 : 0 : PairNodes pp(r1l, r2l);
1609 : 0 : std::map<PairNodes, Node>::const_iterator itr2 = cacheX.find(pp);
1610 [ - - ]: 0 : if (itr2 != cacheX.end())
1611 : : {
1612 : 0 : rt = itr2->second;
1613 : : }
1614 : : else
1615 : : {
1616 : 0 : std::map<PairNodes, Node> cache2(cache);
1617 : 0 : cache2[p] =
1618 : 0 : nm->mkNode(Kind::REGEXP_RV, nm->mkConstInt(Rational(cnt)));
1619 : 0 : rt = intersectInternal(r1l, r2l, cache2, cnt + 1);
1620 : 0 : cacheX[pp] = rt;
1621 : 0 : }
1622 : :
1623 : 0 : rt = rewrite(
1624 : 0 : nm->mkNode(Kind::REGEXP_CONCAT,
1625 : 0 : nm->mkNode(Kind::STRING_TO_REGEXP, nm->mkConst(c)),
1626 : 0 : rt));
1627 : :
1628 [ - - ]: 0 : Trace("regexp-int-debug")
1629 : 0 : << " ... got p(r1,c) && p(r2,c) = " << mkString(rt) << std::endl;
1630 : 0 : vec_nodes.push_back(rt);
1631 : 0 : }
1632 : 0 : rNode = rewrite(vec_nodes.size() == 0 ? d_emptyRegexp
1633 : 0 : : vec_nodes.size() == 1
1634 : 0 : ? vec_nodes[0]
1635 : 0 : : nm->mkNode(Kind::REGEXP_UNION, vec_nodes));
1636 : 0 : rNode = convert1(cnt, rNode);
1637 : 0 : rNode = rewrite(rNode);
1638 : 0 : }
1639 : : }
1640 [ - - ]: 0 : Trace("regexp-int-debug")
1641 : 0 : << " ... try testing no RV of " << mkString(rNode) << std::endl;
1642 [ - - ]: 0 : if (!expr::hasSubtermKind(Kind::REGEXP_RV, rNode))
1643 : : {
1644 : 0 : d_inter_cache[p] = rNode;
1645 : : }
1646 : : }
1647 : 0 : Trace("regexp-int") << "End(" << cnt << ") of INTERSECT( " << mkString(r1)
1648 : 0 : << ", " << mkString(r2) << " ) = " << mkString(rNode)
1649 : 0 : << std::endl;
1650 : 0 : return rNode;
1651 : 0 : }
1652 : :
1653 : 0 : Node RegExpOpr::removeIntersection(Node r)
1654 : : {
1655 : 0 : Assert(checkConstRegExp(r));
1656 : 0 : NodeManager* nm = nodeManager();
1657 : 0 : std::unordered_map<TNode, Node> visited;
1658 : 0 : std::unordered_map<TNode, Node>::iterator it;
1659 : 0 : std::vector<TNode> visit;
1660 : 0 : TNode cur;
1661 : 0 : visit.push_back(r);
1662 : : do
1663 : : {
1664 : 0 : cur = visit.back();
1665 : 0 : visit.pop_back();
1666 : 0 : it = visited.find(cur);
1667 : :
1668 [ - - ]: 0 : if (it == visited.end())
1669 : : {
1670 : 0 : visited[cur] = Node::null();
1671 : 0 : visit.push_back(cur);
1672 [ - - ]: 0 : for (const Node& cn : cur)
1673 : : {
1674 : 0 : visit.push_back(cn);
1675 : 0 : }
1676 : : }
1677 [ - - ]: 0 : else if (it->second.isNull())
1678 : : {
1679 : 0 : Kind ck = cur.getKind();
1680 : 0 : Node ret;
1681 : 0 : bool childChanged = false;
1682 : 0 : std::vector<Node> children;
1683 [ - - ]: 0 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
1684 : : {
1685 : 0 : children.push_back(cur.getOperator());
1686 : : }
1687 [ - - ]: 0 : for (const Node& cn : cur)
1688 : : {
1689 : 0 : it = visited.find(cn);
1690 : 0 : Assert(it != visited.end());
1691 : 0 : Assert(!it->second.isNull());
1692 [ - - ]: 0 : if (ck == Kind::REGEXP_INTER)
1693 : : {
1694 [ - - ]: 0 : if (ret.isNull())
1695 : : {
1696 : 0 : ret = it->second;
1697 : : }
1698 : : else
1699 : : {
1700 : 0 : ret = intersect(ret, it->second);
1701 : : }
1702 : : }
1703 : : else
1704 : : {
1705 : : // will construct below
1706 : 0 : childChanged = childChanged || cn != it->second;
1707 : 0 : children.push_back(it->second);
1708 : : }
1709 : 0 : }
1710 [ - - ]: 0 : if (ck != Kind::REGEXP_INTER)
1711 : : {
1712 [ - - ]: 0 : if (childChanged)
1713 : : {
1714 : 0 : ret = nm->mkNode(cur.getKind(), children);
1715 : : }
1716 : : else
1717 : : {
1718 : 0 : ret = cur;
1719 : : }
1720 : : }
1721 : 0 : visited[cur] = ret;
1722 : 0 : }
1723 [ - - ]: 0 : } while (!visit.empty());
1724 : 0 : Assert(visited.find(r) != visited.end());
1725 : 0 : Assert(!visited.find(r)->second.isNull());
1726 [ - - ]: 0 : if (TraceIsOn("regexp-intersect"))
1727 : : {
1728 : 0 : Trace("regexp-intersect") << "Remove INTERSECTION( " << mkString(r)
1729 : 0 : << " ) = " << mkString(visited[r]) << std::endl;
1730 : : }
1731 : 0 : return visited[r];
1732 : 0 : }
1733 : :
1734 : 0 : Node RegExpOpr::intersect(Node r1, Node r2)
1735 : : {
1736 : 0 : if (!checkConstRegExp(r1) || !checkConstRegExp(r2)
1737 : 0 : || expr::hasSubtermKind(Kind::REGEXP_COMPLEMENT, r1)
1738 : 0 : || expr::hasSubtermKind(Kind::REGEXP_COMPLEMENT, r2))
1739 : : {
1740 : 0 : return Node::null();
1741 : : }
1742 : 0 : Node rr1 = removeIntersection(r1);
1743 : 0 : Node rr2 = removeIntersection(r2);
1744 : 0 : std::map<PairNodes, Node> cache;
1745 [ - - ]: 0 : Trace("regexp-intersect-node") << "Intersect (1): " << rr1 << std::endl;
1746 [ - - ]: 0 : Trace("regexp-intersect-node") << "Intersect (2): " << rr2 << std::endl;
1747 : 0 : Trace("regexp-intersect") << "Start INTERSECTION(\n\t" << mkString(r1)
1748 : 0 : << ",\n\t" << mkString(r2) << ")" << std::endl;
1749 : 0 : Node retNode = intersectInternal(rr1, rr2, cache, 1);
1750 [ - - ]: 0 : Trace("regexp-intersect")
1751 : 0 : << "End INTERSECTION(\n\t" << mkString(r1) << ",\n\t" << mkString(r2)
1752 : 0 : << ") =\n\t" << mkString(retNode) << std::endl;
1753 [ - - ]: 0 : Trace("regexp-intersect-node") << "Intersect finished." << std::endl;
1754 : 0 : return retNode;
1755 : 0 : }
1756 : :
1757 : : // printing
1758 : 0 : std::string RegExpOpr::niceChar(Node r)
1759 : : {
1760 [ - - ]: 0 : if (r.isConst())
1761 : : {
1762 : 0 : std::string s = r.getConst<String>().toString();
1763 : 0 : return s == "." ? "\\." : s;
1764 : 0 : }
1765 : : else
1766 : : {
1767 : 0 : std::string ss = "$" + r.toString();
1768 : 0 : return ss;
1769 : 0 : }
1770 : : }
1771 : 0 : std::string RegExpOpr::mkString(Node r)
1772 : : {
1773 : 0 : std::string retStr;
1774 [ - - ]: 0 : if (r.isNull())
1775 : : {
1776 : 0 : retStr = "\\E";
1777 : : }
1778 : : else
1779 : : {
1780 : 0 : Kind k = r.getKind();
1781 [ - - ][ - - ]: 0 : switch (k)
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ]
1782 : : {
1783 : 0 : case Kind::REGEXP_NONE:
1784 : : {
1785 : 0 : retStr += "\\E";
1786 : 0 : break;
1787 : : }
1788 : 0 : case Kind::REGEXP_ALLCHAR:
1789 : : {
1790 : 0 : retStr += ".";
1791 : 0 : break;
1792 : : }
1793 : 0 : case Kind::STRING_TO_REGEXP:
1794 : : {
1795 : 0 : std::string tmp(niceChar(r[0]));
1796 : 0 : retStr += tmp.size() == 1 ? tmp : "(" + tmp + ")";
1797 : 0 : break;
1798 : 0 : }
1799 : 0 : case Kind::REGEXP_CONCAT:
1800 : : {
1801 : 0 : retStr += "(";
1802 [ - - ]: 0 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
1803 : : {
1804 : : // if(i != 0) retStr += ".";
1805 : 0 : retStr += mkString(r[i]);
1806 : : }
1807 : 0 : retStr += ")";
1808 : 0 : break;
1809 : : }
1810 : 0 : case Kind::REGEXP_UNION:
1811 : : {
1812 : 0 : retStr += "(";
1813 [ - - ]: 0 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
1814 : : {
1815 [ - - ]: 0 : if (i != 0) retStr += "|";
1816 : 0 : retStr += mkString(r[i]);
1817 : : }
1818 : 0 : retStr += ")";
1819 : 0 : break;
1820 : : }
1821 : 0 : case Kind::REGEXP_INTER:
1822 : : {
1823 : 0 : retStr += "(";
1824 [ - - ]: 0 : for (unsigned i = 0; i < r.getNumChildren(); ++i)
1825 : : {
1826 [ - - ]: 0 : if (i != 0) retStr += "&";
1827 : 0 : retStr += mkString(r[i]);
1828 : : }
1829 : 0 : retStr += ")";
1830 : 0 : break;
1831 : : }
1832 : 0 : case Kind::REGEXP_STAR:
1833 : : {
1834 : 0 : retStr += mkString(r[0]);
1835 : 0 : retStr += "*";
1836 : 0 : break;
1837 : : }
1838 : 0 : case Kind::REGEXP_PLUS:
1839 : : {
1840 : 0 : retStr += mkString(r[0]);
1841 : 0 : retStr += "+";
1842 : 0 : break;
1843 : : }
1844 : 0 : case Kind::REGEXP_OPT:
1845 : : {
1846 : 0 : retStr += mkString(r[0]);
1847 : 0 : retStr += "?";
1848 : 0 : break;
1849 : : }
1850 : 0 : case Kind::REGEXP_RANGE:
1851 : : {
1852 : 0 : retStr += "[";
1853 : 0 : retStr += niceChar(r[0]);
1854 : 0 : retStr += "-";
1855 : 0 : retStr += niceChar(r[1]);
1856 : 0 : retStr += "]";
1857 : 0 : break;
1858 : : }
1859 : 0 : case Kind::REGEXP_LOOP:
1860 : : {
1861 : 0 : uint32_t l = utils::getLoopMinOccurrences(r);
1862 : 0 : std::stringstream ss;
1863 : 0 : ss << "(" << mkString(r[0]) << "){" << l << ",";
1864 [ - - ]: 0 : if (r.getNumChildren() == 3)
1865 : : {
1866 : 0 : uint32_t u = utils::getLoopMaxOccurrences(r);
1867 : 0 : ss << u;
1868 : : }
1869 : 0 : ss << "}";
1870 : 0 : retStr += ss.str();
1871 : 0 : break;
1872 : 0 : }
1873 : 0 : case Kind::REGEXP_RV:
1874 : : {
1875 : 0 : retStr += "<";
1876 : 0 : retStr += r[0].getConst<Rational>().getNumerator().toString();
1877 : 0 : retStr += ">";
1878 : 0 : break;
1879 : : }
1880 : 0 : case Kind::REGEXP_COMPLEMENT:
1881 : : {
1882 : 0 : retStr += "^(";
1883 : 0 : retStr += mkString(r[0]);
1884 : 0 : retStr += ")";
1885 : 0 : break;
1886 : : }
1887 : 0 : default:
1888 : : {
1889 : 0 : std::stringstream ss;
1890 : 0 : ss << r;
1891 : 0 : retStr = ss.str();
1892 : 0 : Assert(!utils::isRegExpKind(r.getKind()));
1893 : 0 : break;
1894 : 0 : }
1895 : : }
1896 : : }
1897 : :
1898 : 0 : return retStr;
1899 : 0 : }
1900 : :
1901 : 1735 : bool RegExpOpr::regExpIncludes(Node r1, Node r2)
1902 : : {
1903 : 1735 : return RegExpEntail::regExpIncludes(r1, r2, d_inclusionCache);
1904 : : }
1905 : :
1906 : : } // namespace strings
1907 : : } // namespace theory
1908 : : } // namespace cvc5::internal
|
