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