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