GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/regexp_entail.cpp Lines: 333 378 88.1 %
Date: 2021-03-22 Branches: 693 1431 48.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file regexp_entail.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Implementation of entailment tests involving regular expressions
13
 **/
14
15
#include "theory/strings/regexp_entail.h"
16
17
#include "theory/rewriter.h"
18
#include "theory/strings/theory_strings_utils.h"
19
#include "theory/strings/word.h"
20
21
using namespace std;
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace strings {
27
28
8389
Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
29
                                       std::vector<Node>& children,
30
                                       int dir)
31
{
32
16778
  Trace("regexp-ext-rewrite-debug")
33
8389
      << "Simple reg exp consume, dir=" << dir << ":" << std::endl;
34
16778
  Trace("regexp-ext-rewrite-debug")
35
8389
      << "  mchildren : " << mchildren << std::endl;
36
8389
  Trace("regexp-ext-rewrite-debug") << "  children : " << children << std::endl;
37
8389
  NodeManager* nm = NodeManager::currentNM();
38
8389
  unsigned tmin = dir < 0 ? 0 : dir;
39
8389
  unsigned tmax = dir < 0 ? 1 : dir;
40
  // try to remove off front and back
41
23664
  for (unsigned t = 0; t < 2; t++)
42
  {
43
16354
    if (tmin <= t && t <= tmax)
44
    {
45
11149
      bool do_next = true;
46
33239
      while (!children.empty() && !mchildren.empty() && do_next)
47
      {
48
12124
        do_next = false;
49
23169
        Node xc = mchildren[mchildren.size() - 1];
50
23169
        Node rc = children[children.size() - 1];
51
24248
        Trace("regexp-ext-rewrite-debug")
52
12124
            << "* " << xc << " in " << rc << std::endl;
53
12124
        Assert(rc.getKind() != REGEXP_CONCAT);
54
12124
        Assert(xc.getKind() != STRING_CONCAT);
55
12124
        if (rc.getKind() == STRING_TO_REGEXP)
56
        {
57
4273
          if (xc == rc[0])
58
          {
59
376
            children.pop_back();
60
376
            mchildren.pop_back();
61
376
            do_next = true;
62
376
            Trace("regexp-ext-rewrite-debug") << "- strip equal" << std::endl;
63
          }
64
3897
          else if (rc[0].isConst() && Word::isEmpty(rc[0]))
65
          {
66
80
            Trace("regexp-ext-rewrite-debug")
67
40
                << "- ignore empty RE" << std::endl;
68
            // ignore and continue
69
40
            children.pop_back();
70
40
            do_next = true;
71
          }
72
3857
          else if (xc.isConst() && rc[0].isConst())
73
          {
74
            // split the constant
75
            size_t index;
76
1153
            Node s = Word::splitConstant(xc, rc[0], index, t == 0);
77
1846
            Trace("regexp-ext-rewrite-debug")
78
1846
                << "- CRE: Regexp const split : " << xc << " " << rc[0]
79
923
                << " -> " << s << " " << index << " " << t << std::endl;
80
923
            if (s.isNull())
81
            {
82
1386
              Trace("regexp-ext-rewrite-debug")
83
693
                  << "...return false" << std::endl;
84
693
              return nm->mkConst(false);
85
            }
86
            else
87
            {
88
460
              Trace("regexp-ext-rewrite-debug")
89
230
                  << "- strip equal const" << std::endl;
90
230
              children.pop_back();
91
230
              mchildren.pop_back();
92
230
              if (index == 0)
93
              {
94
220
                mchildren.push_back(s);
95
              }
96
              else
97
              {
98
10
                children.push_back(nm->mkNode(STRING_TO_REGEXP, s));
99
              }
100
            }
101
230
            Trace("regexp-ext-rewrite-debug") << "- split const" << std::endl;
102
230
            do_next = true;
103
          }
104
        }
105
7851
        else if (xc.isConst())
106
        {
107
          // check for constants
108
4896
          CVC4::String s = xc.getConst<String>();
109
2641
          if (Word::isEmpty(xc))
110
          {
111
20
            Trace("regexp-ext-rewrite-debug") << "- ignore empty" << std::endl;
112
            // ignore and continue
113
20
            mchildren.pop_back();
114
20
            do_next = true;
115
          }
116
2621
          else if (rc.getKind() == REGEXP_RANGE || rc.getKind() == REGEXP_SIGMA)
117
          {
118
1867
            std::vector<unsigned> ssVec;
119
1038
            ssVec.push_back(t == 0 ? s.back() : s.front());
120
1867
            CVC4::String ss(ssVec);
121
1038
            if (testConstStringInRegExp(ss, 0, rc))
122
            {
123
              // strip off one character
124
829
              mchildren.pop_back();
125
829
              if (s.size() > 1)
126
              {
127
604
                if (t == 0)
128
                {
129
308
                  mchildren.push_back(nm->mkConst(s.substr(0, s.size() - 1)));
130
                }
131
                else
132
                {
133
296
                  mchildren.push_back(nm->mkConst(s.substr(1)));
134
                }
135
              }
136
829
              children.pop_back();
137
829
              do_next = true;
138
            }
139
            else
140
            {
141
418
              Trace("regexp-ext-rewrite-debug")
142
209
                  << "...return false" << std::endl;
143
209
              return nm->mkConst(false);
144
            }
145
          }
146
1583
          else if (rc.getKind() == REGEXP_INTER || rc.getKind() == REGEXP_UNION)
147
          {
148
            // see if any/each child does not work
149
567
            bool result_valid = true;
150
957
            Node result;
151
957
            Node emp_s = nm->mkConst(String(""));
152
1411
            for (unsigned i = 0; i < rc.getNumChildren(); i++)
153
            {
154
1849
              std::vector<Node> mchildren_s;
155
1849
              std::vector<Node> children_s;
156
1005
              mchildren_s.push_back(xc);
157
1005
              utils::getConcat(rc[i], children_s);
158
1005
              Trace("regexp-ext-rewrite-debug") << push;
159
1849
              Node ret = simpleRegexpConsume(mchildren_s, children_s, t);
160
1005
              Trace("regexp-ext-rewrite-debug") << pop;
161
1005
              if (!ret.isNull())
162
              {
163
                // one conjunct cannot be satisfied, return false
164
513
                if (rc.getKind() == REGEXP_INTER)
165
                {
166
322
                  Trace("regexp-ext-rewrite-debug")
167
161
                      << "...return " << ret << std::endl;
168
161
                  return ret;
169
                }
170
              }
171
              else
172
              {
173
492
                if (children_s.empty())
174
                {
175
                  // if we were able to fully consume, store the result
176
262
                  Assert(mchildren_s.size() <= 1);
177
262
                  if (mchildren_s.empty())
178
                  {
179
62
                    mchildren_s.push_back(emp_s);
180
                  }
181
262
                  if (result.isNull())
182
                  {
183
250
                    result = mchildren_s[0];
184
                  }
185
12
                  else if (result != mchildren_s[0])
186
                  {
187
12
                    result_valid = false;
188
                  }
189
                }
190
                else
191
                {
192
230
                  result_valid = false;
193
                }
194
              }
195
            }
196
406
            if (result_valid)
197
            {
198
246
              if (result.isNull())
199
              {
200
                // all disjuncts cannot be satisfied, return false
201
16
                Assert(rc.getKind() == REGEXP_UNION);
202
32
                Trace("regexp-ext-rewrite-debug")
203
16
                    << "...return false" << std::endl;
204
16
                return nm->mkConst(false);
205
              }
206
              else
207
              {
208
460
                Trace("regexp-ext-rewrite-debug")
209
230
                    << "- same result, try again, children now " << children
210
230
                    << std::endl;
211
                // all branches led to the same result
212
230
                children.pop_back();
213
230
                mchildren.pop_back();
214
230
                if (result != emp_s)
215
                {
216
180
                  mchildren.push_back(result);
217
                }
218
230
                do_next = true;
219
              }
220
            }
221
          }
222
1016
          else if (rc.getKind() == REGEXP_STAR)
223
          {
224
            // check if there is no way that this star can be unrolled even once
225
1668
            std::vector<Node> mchildren_s;
226
834
            mchildren_s.insert(
227
1668
                mchildren_s.end(), mchildren.begin(), mchildren.end());
228
834
            if (t == 1)
229
            {
230
424
              std::reverse(mchildren_s.begin(), mchildren_s.end());
231
            }
232
1668
            std::vector<Node> children_s;
233
834
            utils::getConcat(rc[0], children_s);
234
1668
            Trace("regexp-ext-rewrite-debug")
235
834
                << "- recursive call on body of star" << std::endl;
236
834
            Trace("regexp-ext-rewrite-debug") << push;
237
1668
            Node ret = simpleRegexpConsume(mchildren_s, children_s, t);
238
834
            Trace("regexp-ext-rewrite-debug") << pop;
239
834
            if (!ret.isNull())
240
            {
241
76
              Trace("regexp-ext-rewrite-debug")
242
38
                  << "- CRE : regexp star infeasable " << xc << " " << rc
243
38
                  << std::endl;
244
38
              children.pop_back();
245
38
              if (!children.empty())
246
              {
247
24
                Trace("regexp-ext-rewrite-debug") << "- continue" << std::endl;
248
24
                do_next = true;
249
              }
250
            }
251
            else
252
            {
253
796
              if (children_s.empty())
254
              {
255
                // Check if beyond this, we hit a conflict. In this case, we
256
                // must repeat.  Notice that we do not treat the case where
257
                // there are no more strings to consume as a failure, since
258
                // we may be within a recursive call, see issue #5510.
259
770
                bool can_skip = true;
260
770
                if (children.size() > 1)
261
                {
262
1456
                  std::vector<Node> mchildren_ss;
263
728
                  mchildren_ss.insert(
264
1456
                      mchildren_ss.end(), mchildren.begin(), mchildren.end());
265
1456
                  std::vector<Node> children_ss;
266
728
                  children_ss.insert(
267
1456
                      children_ss.end(), children.begin(), children.end() - 1);
268
728
                  if (t == 1)
269
                  {
270
382
                    std::reverse(mchildren_ss.begin(), mchildren_ss.end());
271
382
                    std::reverse(children_ss.begin(), children_ss.end());
272
                  }
273
1456
                  Trace("regexp-ext-rewrite-debug")
274
728
                      << "- recursive call required repeat star" << std::endl;
275
728
                  Trace("regexp-ext-rewrite-debug") << push;
276
1456
                  Node rets = simpleRegexpConsume(mchildren_ss, children_ss, t);
277
728
                  Trace("regexp-ext-rewrite-debug") << pop;
278
728
                  if (!rets.isNull())
279
                  {
280
476
                    can_skip = false;
281
                  }
282
                }
283
770
                if (!can_skip)
284
                {
285
952
                  TypeNode stype = nm->stringType();
286
952
                  Node prev = utils::mkConcat(mchildren, stype);
287
952
                  Trace("regexp-ext-rewrite-debug")
288
476
                      << "- can't skip" << std::endl;
289
                  // take the result of fully consuming once
290
476
                  if (t == 1)
291
                  {
292
246
                    std::reverse(mchildren_s.begin(), mchildren_s.end());
293
                  }
294
476
                  mchildren.clear();
295
476
                  mchildren.insert(
296
952
                      mchildren.end(), mchildren_s.begin(), mchildren_s.end());
297
952
                  Node curr = utils::mkConcat(mchildren, stype);
298
476
                  do_next = (prev != curr);
299
952
                  Trace("regexp-ext-rewrite-debug")
300
476
                      << "- do_next = " << do_next << std::endl;
301
                }
302
                else
303
                {
304
588
                  Trace("regexp-ext-rewrite-debug")
305
294
                      << "- can skip " << rc << " from " << xc << std::endl;
306
                }
307
              }
308
            }
309
          }
310
        }
311
11045
        if (!do_next)
312
        {
313
17640
          Trace("regexp-ext-rewrite")
314
8820
              << "- cannot consume : " << xc << " " << rc << std::endl;
315
        }
316
      }
317
    }
318
15275
    if (dir != 0)
319
    {
320
10891
      std::reverse(children.begin(), children.end());
321
10891
      std::reverse(mchildren.begin(), mchildren.end());
322
    }
323
  }
324
7310
  Trace("regexp-ext-rewrite-debug") << "...finished, return null" << std::endl;
325
7310
  return Node::null();
326
}
327
328
12024
bool RegExpEntail::isConstRegExp(TNode t)
329
{
330
12024
  if (t.getKind() == STRING_TO_REGEXP)
331
  {
332
3007
    return t[0].isConst();
333
  }
334
9017
  else if (t.isVar())
335
  {
336
50
    return false;
337
  }
338
18457
  for (unsigned i = 0; i < t.getNumChildren(); ++i)
339
  {
340
9530
    if (!isConstRegExp(t[i]))
341
    {
342
40
      return false;
343
    }
344
  }
345
8927
  return true;
346
}
347
348
1063992
bool RegExpEntail::testConstStringInRegExp(CVC4::String& s,
349
                                           unsigned index_start,
350
                                           TNode r)
351
{
352
1063992
  Assert(index_start <= s.size());
353
2127984
  Trace("regexp-debug") << "Checking " << s << " in " << r << ", starting at "
354
1063992
                        << index_start << std::endl;
355
1063992
  Assert(!r.isVar());
356
1063992
  Kind k = r.getKind();
357
1063992
  switch (k)
358
  {
359
18343
    case STRING_TO_REGEXP:
360
    {
361
36686
      CVC4::String s2 = s.substr(index_start, s.size() - index_start);
362
18343
      if (r[0].isConst())
363
      {
364
18343
        return (s2 == r[0].getConst<String>());
365
      }
366
      Assert(false) << "RegExp contains variables";
367
      return false;
368
    }
369
3708
    case REGEXP_CONCAT:
370
    {
371
3708
      if (s.size() != index_start)
372
      {
373
5552
        std::vector<int> vec_k(r.getNumChildren(), -1);
374
2776
        int start = 0;
375
2776
        int left = (int)s.size() - index_start;
376
2776
        int i = 0;
377
21898
        while (i < (int)r.getNumChildren())
378
        {
379
12337
          bool flag = true;
380
12337
          if (i == (int)r.getNumChildren() - 1)
381
          {
382
2734
            if (testConstStringInRegExp(s, index_start + start, r[i]))
383
            {
384
644
              return true;
385
            }
386
          }
387
9603
          else if (i == -1)
388
          {
389
2132
            return false;
390
          }
391
          else
392
          {
393
25254
            for (vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i])
394
            {
395
39800
              CVC4::String t = s.substr(index_start + start, vec_k[i]);
396
22017
              if (testConstStringInRegExp(t, 0, r[i]))
397
              {
398
4234
                start += vec_k[i];
399
4234
                left -= vec_k[i];
400
4234
                flag = false;
401
4234
                ++i;
402
4234
                vec_k[i] = -1;
403
4234
                break;
404
              }
405
            }
406
          }
407
408
9561
          if (flag)
409
          {
410
5327
            --i;
411
5327
            if (i >= 0)
412
            {
413
3195
              start -= vec_k[i];
414
3195
              left += vec_k[i];
415
            }
416
          }
417
        }
418
        return false;
419
      }
420
      else
421
      {
422
986
        for (unsigned i = 0; i < r.getNumChildren(); ++i)
423
        {
424
986
          if (!testConstStringInRegExp(s, index_start, r[i]))
425
          {
426
932
            return false;
427
          }
428
        }
429
        return true;
430
      }
431
    }
432
336540
    case REGEXP_UNION:
433
    {
434
977050
      for (unsigned i = 0; i < r.getNumChildren(); ++i)
435
      {
436
663856
        if (testConstStringInRegExp(s, index_start, r[i]))
437
        {
438
23346
          return true;
439
        }
440
      }
441
313194
      return false;
442
    }
443
2337
    case REGEXP_INTER:
444
    {
445
2567
      for (unsigned i = 0; i < r.getNumChildren(); ++i)
446
      {
447
2454
        if (!testConstStringInRegExp(s, index_start, r[i]))
448
        {
449
2224
          return false;
450
        }
451
      }
452
113
      return true;
453
    }
454
30097
    case REGEXP_STAR:
455
    {
456
30097
      if (s.size() != index_start)
457
      {
458
364426
        for (unsigned i = s.size() - index_start; i > 0; --i)
459
        {
460
679689
          CVC4::String t = s.substr(index_start, i);
461
344081
          if (testConstStringInRegExp(t, 0, r[0]))
462
          {
463
53144
            if (index_start + i == s.size()
464
53144
                || testConstStringInRegExp(s, index_start + i, r))
465
            {
466
8473
              return true;
467
            }
468
          }
469
        }
470
20345
        return false;
471
      }
472
      else
473
      {
474
1279
        return true;
475
      }
476
    }
477
10
    case REGEXP_EMPTY:
478
    {
479
10
      return false;
480
    }
481
6153
    case REGEXP_SIGMA:
482
    {
483
6153
      if (s.size() == index_start + 1)
484
      {
485
2743
        return true;
486
      }
487
      else
488
      {
489
3410
        return false;
490
      }
491
    }
492
666634
    case REGEXP_RANGE:
493
    {
494
666634
      if (s.size() == index_start + 1)
495
      {
496
43184
        unsigned a = r[0].getConst<String>().front();
497
43184
        unsigned b = r[1].getConst<String>().front();
498
43184
        unsigned c = s.back();
499
43184
        return (a <= c && c <= b);
500
      }
501
      else
502
      {
503
623450
        return false;
504
      }
505
    }
506
    case REGEXP_LOOP:
507
    {
508
      NodeManager* nm = NodeManager::currentNM();
509
      uint32_t l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
510
      if (s.size() == index_start)
511
      {
512
        return l == 0 ? true : testConstStringInRegExp(s, index_start, r[0]);
513
      }
514
      else if (l == 0 && r[1] == r[2])
515
      {
516
        return false;
517
      }
518
      else
519
      {
520
        Assert(r.getNumChildren() == 3)
521
            << "String rewriter error: LOOP has 2 children";
522
        if (l == 0)
523
        {
524
          // R{0,u}
525
          uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
526
          for (unsigned len = s.size() - index_start; len >= 1; len--)
527
          {
528
            CVC4::String t = s.substr(index_start, len);
529
            if (testConstStringInRegExp(t, 0, r[0]))
530
            {
531
              if (len + index_start == s.size())
532
              {
533
                return true;
534
              }
535
              else
536
              {
537
                Node num2 = nm->mkConst(CVC4::Rational(u - 1));
538
                Node r2 = nm->mkNode(REGEXP_LOOP, r[0], r[1], num2);
539
                if (testConstStringInRegExp(s, index_start + len, r2))
540
                {
541
                  return true;
542
                }
543
              }
544
            }
545
          }
546
          return false;
547
        }
548
        else
549
        {
550
          // R{l,l}
551
          Assert(r[1] == r[2])
552
              << "String rewriter error: LOOP nums are not equal";
553
          if (l > s.size() - index_start)
554
          {
555
            if (testConstStringInRegExp(s, s.size(), r[0]))
556
            {
557
              l = s.size() - index_start;
558
            }
559
            else
560
            {
561
              return false;
562
            }
563
          }
564
          for (unsigned len = 1; len <= s.size() - index_start; len++)
565
          {
566
            CVC4::String t = s.substr(index_start, len);
567
            if (testConstStringInRegExp(t, 0, r[0]))
568
            {
569
              Node num2 = nm->mkConst(CVC4::Rational(l - 1));
570
              Node r2 = nm->mkNode(REGEXP_LOOP, r[0], num2, num2);
571
              if (testConstStringInRegExp(s, index_start + len, r2))
572
              {
573
                return true;
574
              }
575
            }
576
          }
577
          return false;
578
        }
579
      }
580
    }
581
170
    case REGEXP_COMPLEMENT:
582
    {
583
170
      return !testConstStringInRegExp(s, index_start, r[0]);
584
      break;
585
    }
586
    default:
587
    {
588
      Assert(!utils::isRegExpKind(k));
589
      return false;
590
    }
591
  }
592
}
593
594
146
bool RegExpEntail::hasEpsilonNode(TNode node)
595
{
596
458
  for (const Node& nc : node)
597
  {
598
332
    if (nc.getKind() == STRING_TO_REGEXP && Word::isEmpty(nc[0]))
599
    {
600
20
      return true;
601
    }
602
  }
603
126
  return false;
604
}
605
606
1039
Node RegExpEntail::getFixedLengthForRegexp(Node n)
607
{
608
1039
  NodeManager* nm = NodeManager::currentNM();
609
1039
  if (n.getKind() == STRING_TO_REGEXP)
610
  {
611
286
    Node ret = nm->mkNode(STRING_LENGTH, n[0]);
612
286
    ret = Rewriter::rewrite(ret);
613
286
    if (ret.isConst())
614
    {
615
286
      return ret;
616
    }
617
  }
618
753
  else if (n.getKind() == REGEXP_SIGMA || n.getKind() == REGEXP_RANGE)
619
  {
620
273
    return nm->mkConst(Rational(1));
621
  }
622
480
  else if (n.getKind() == REGEXP_UNION || n.getKind() == REGEXP_INTER)
623
  {
624
320
    Node ret;
625
356
    for (const Node& nc : n)
626
    {
627
472
      Node flc = getFixedLengthForRegexp(nc);
628
276
      if (flc.isNull() || (!ret.isNull() && ret != flc))
629
      {
630
80
        return Node::null();
631
      }
632
196
      else if (ret.isNull())
633
      {
634
        // first time
635
116
        ret = flc;
636
      }
637
    }
638
80
    return ret;
639
  }
640
320
  else if (n.getKind() == REGEXP_CONCAT)
641
  {
642
248
    NodeBuilder<> nb(PLUS);
643
210
    for (const Node& nc : n)
644
    {
645
296
      Node flc = getFixedLengthForRegexp(nc);
646
210
      if (flc.isNull())
647
      {
648
124
        return flc;
649
      }
650
86
      nb << flc;
651
    }
652
    Node ret = nb.constructNode();
653
    ret = Rewriter::rewrite(ret);
654
    return ret;
655
  }
656
196
  return Node::null();
657
}
658
659
378
bool RegExpEntail::regExpIncludes(Node r1, Node r2)
660
{
661
378
  Assert(Rewriter::rewrite(r1) == r1);
662
378
  Assert(Rewriter::rewrite(r2) == r2);
663
378
  if (r1 == r2)
664
  {
665
2
    return true;
666
  }
667
668
  // This method only works on a fragment of regular expressions
669
376
  if (!utils::isSimpleRegExp(r1) || !utils::isSimpleRegExp(r2))
670
  {
671
240
    return false;
672
  }
673
136
  NodeManager* nm = NodeManager::currentNM();
674
272
  Node sigma = nm->mkNode(REGEXP_SIGMA, std::vector<Node>{});
675
272
  Node sigmaStar = nm->mkNode(REGEXP_STAR, sigma);
676
677
272
  std::vector<Node> v1, v2;
678
136
  utils::getRegexpComponents(r1, v1);
679
136
  utils::getRegexpComponents(r2, v2);
680
681
  // In the following, we iterate over `r2` (the "includee") and try to
682
  // match it with `r1`. `idxs`/`newIdxs` keep track of all the possible
683
  // positions in `r1` that we could currently be at.
684
272
  std::unordered_set<size_t> newIdxs = {0};
685
272
  std::unordered_set<size_t> idxs;
686
898
  for (const Node& n2 : v2)
687
  {
688
    // Transfer elements from `newIdxs` to `idxs`. Out-of-bound indices are
689
    // removed and for (re.* re.allchar), we additionally include the option of
690
    // skipping it. Indices must be smaller than the size of `v1`.
691
798
    idxs.clear();
692
2626
    for (size_t idx : newIdxs)
693
    {
694
1828
      if (idx < v1.size())
695
      {
696
1806
        idxs.insert(idx);
697
1806
        if (idx + 1 < v1.size() && v1[idx] == sigmaStar)
698
        {
699
1032
          Assert(idx + 1 == v1.size() || v1[idx + 1] != sigmaStar);
700
1032
          idxs.insert(idx + 1);
701
        }
702
      }
703
    }
704
798
    newIdxs.clear();
705
706
798
    if (n2.getKind() == STRING_TO_REGEXP || n2 == sigma)
707
    {
708
594
      Assert(n2 == sigma
709
             || (n2[0].isConst() && n2[0].getConst<String>().size() == 1));
710
2724
      for (size_t idx : idxs)
711
      {
712
2130
        if (v1[idx] == sigma || v1[idx] == n2)
713
        {
714
          // Given a character or an re.allchar in `r2`, we can either
715
          // match it with a corresponding character in `r1` or an
716
          // re.allchar
717
642
          newIdxs.insert(idx + 1);
718
        }
719
      }
720
    }
721
722
3636
    for (size_t idx : idxs)
723
    {
724
2838
      if (v1[idx] == sigmaStar)
725
      {
726
        // (re.* re.allchar) can match an arbitrary amount of `r2`
727
1136
        newIdxs.insert(idx);
728
      }
729
1702
      else if (utils::isUnboundedWildcard(v1, idx))
730
      {
731
        // If a series of re.allchar is followed by (re.* re.allchar), we
732
        // can decide not to "waste" the re.allchar because the order of
733
        // the two wildcards is not observable (i.e. it does not change
734
        // the sequences matched by the regular expression)
735
440
        newIdxs.insert(idx);
736
      }
737
    }
738
739
798
    if (newIdxs.empty())
740
    {
741
      // If there are no candidates, we can't match the remainder of r2
742
36
      return false;
743
    }
744
  }
745
746
  // We have processed all of `r2`. We are now looking if there was also a
747
  // path to the end in `r1`. This makes sure that we don't have leftover
748
  // bits in `r1` that don't match anything in `r2`.
749
100
  bool result = false;
750
282
  for (size_t idx : newIdxs)
751
  {
752
234
    if (idx == v1.size() || (idx == v1.size() - 1 && v1[idx] == sigmaStar))
753
    {
754
52
      result = true;
755
52
      break;
756
    }
757
  }
758
759
100
  return result;
760
}
761
762
}  // namespace strings
763
}  // namespace theory
764
26676
}  // namespace CVC4