GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/regexp_solver.cpp Lines: 305 341 89.4 %
Date: 2021-03-23 Branches: 610 1261 48.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file regexp_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Tianyi Liang
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 the regular expression solver for the theory of
13
 ** strings.
14
 **
15
 **/
16
17
#include "theory/strings/regexp_solver.h"
18
19
#include <cmath>
20
21
#include "options/strings_options.h"
22
#include "smt/logic_exception.h"
23
#include "theory/ext_theory.h"
24
#include "theory/strings/theory_strings_utils.h"
25
#include "theory/theory_model.h"
26
27
using namespace std;
28
using namespace CVC4::context;
29
using namespace CVC4::kind;
30
31
namespace CVC4 {
32
namespace theory {
33
namespace strings {
34
35
8997
RegExpSolver::RegExpSolver(SolverState& s,
36
                           InferenceManager& im,
37
                           SkolemCache* skc,
38
                           CoreSolver& cs,
39
                           ExtfSolver& es,
40
8997
                           SequencesStatistics& stats)
41
    : d_state(s),
42
      d_im(im),
43
      d_csolver(cs),
44
      d_esolver(es),
45
      d_statistics(stats),
46
8997
      d_regexp_ucached(s.getUserContext()),
47
      d_regexp_ccached(s.getSatContext()),
48
      d_processed_memberships(s.getSatContext()),
49
17994
      d_regexp_opr(skc)
50
{
51
8997
  d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String(""));
52
17994
  std::vector<Node> nvec;
53
8997
  d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY, nvec);
54
8997
  d_true = NodeManager::currentNM()->mkConst(true);
55
8997
  d_false = NodeManager::currentNM()->mkConst(false);
56
8997
}
57
58
Node RegExpSolver::mkAnd(Node c1, Node c2)
59
{
60
  return NodeManager::currentNM()->mkNode(AND, c1, c2);
61
}
62
63
7346
void RegExpSolver::checkMemberships()
64
{
65
  // add the memberships
66
14692
  std::vector<Node> mems = d_esolver.getActive(STRING_IN_REGEXP);
67
  // maps representatives to regular expression memberships in that class
68
14692
  std::map<Node, std::vector<Node> > assertedMems;
69
7346
  const std::map<Node, ExtfInfoTmp>& einfo = d_esolver.getInfo();
70
7346
  std::map<Node, ExtfInfoTmp>::const_iterator it;
71
8197
  for (unsigned i = 0; i < mems.size(); i++)
72
  {
73
1702
    Node n = mems[i];
74
851
    Assert(n.getKind() == STRING_IN_REGEXP);
75
851
    it = einfo.find(n);
76
851
    Assert(it != einfo.end());
77
851
    if (!it->second.d_const.isNull())
78
    {
79
829
      bool pol = it->second.d_const.getConst<bool>();
80
1658
      Trace("strings-process-debug")
81
829
          << "  add membership : " << n << ", pol = " << pol << std::endl;
82
1658
      Node r = d_state.getRepresentative(n[0]);
83
829
      assertedMems[r].push_back(pol ? n : n.negate());
84
    }
85
    else
86
    {
87
44
      Trace("strings-process-debug")
88
22
          << "  irrelevant (non-asserted) membership : " << n << std::endl;
89
    }
90
  }
91
7346
  check(assertedMems);
92
7346
}
93
94
7346
void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
95
{
96
7346
  bool addedLemma = false;
97
7346
  bool changed = false;
98
14670
  std::vector<Node> processed;
99
14670
  std::vector<Node> cprocessed;
100
101
7346
  Trace("regexp-process") << "Checking Memberships ... " << std::endl;
102
7931
  for (const std::pair<const Node, std::vector<Node> >& mr : mems)
103
  {
104
1192
    std::vector<Node> mems2 = mr.second;
105
1214
    Trace("regexp-process")
106
607
        << "Memberships(" << mr.first << ") = " << mr.second << std::endl;
107
607
    if (!checkEqcInclusion(mems2))
108
    {
109
      // conflict discovered, return
110
10
      return;
111
    }
112
597
    if (!checkEqcIntersect(mems2))
113
    {
114
      // conflict discovered, return
115
12
      return;
116
    }
117
  }
118
119
14648
  Trace("regexp-debug")
120
7324
      << "... No Intersect Conflict in Memberships, addedLemma: " << addedLemma
121
7324
      << std::endl;
122
7324
  if (!addedLemma)
123
  {
124
    // get all memberships
125
14648
    std::map<Node, Node> allMems;
126
7909
    for (const std::pair<const Node, std::vector<Node> >& mr : mems)
127
    {
128
1355
      for (const Node& m : mr.second)
129
      {
130
770
        bool polarity = m.getKind() != NOT;
131
1084
        if (polarity || !options::stringIgnNegMembership())
132
        {
133
764
          allMems[m] = mr.first;
134
        }
135
      }
136
    }
137
138
7324
    NodeManager* nm = NodeManager::currentNM();
139
    // representatives of strings that are the LHS of positive memberships that
140
    // we unfolded
141
14648
    std::unordered_set<Node, NodeHashFunction> repUnfold;
142
    // check positive (e=0), then negative (e=1) memberships
143
21972
    for (unsigned e = 0; e < 2; e++)
144
    {
145
16170
      for (const std::pair<const Node, Node>& mp : allMems)
146
      {
147
1860
        Node assertion = mp.first;
148
1860
        Node rep = mp.second;
149
        // check regular expression membership
150
3056
        Trace("regexp-debug")
151
1528
            << "Check : " << assertion << " "
152
3056
            << (d_regexp_ucached.find(assertion) == d_regexp_ucached.end())
153
1528
            << " "
154
3056
            << (d_regexp_ccached.find(assertion) == d_regexp_ccached.end())
155
1528
            << std::endl;
156
3056
        if (d_regexp_ucached.find(assertion) != d_regexp_ucached.end()
157
1528
            || d_regexp_ccached.find(assertion) != d_regexp_ccached.end())
158
        {
159
814
          continue;
160
        }
161
1428
        Trace("strings-regexp")
162
714
            << "We have regular expression assertion : " << assertion
163
714
            << std::endl;
164
1046
        Node atom = assertion.getKind() == NOT ? assertion[0] : assertion;
165
714
        Assert(atom == Rewriter::rewrite(atom));
166
714
        bool polarity = assertion.getKind() != NOT;
167
714
        if (polarity != (e == 0))
168
        {
169
350
          continue;
170
        }
171
364
        bool flag = true;
172
696
        Node x = atom[0];
173
696
        Node r = atom[1];
174
364
        Assert(rep == d_state.getRepresentative(x));
175
        // The following code takes normal forms into account for the purposes
176
        // of simplifying a regular expression membership x in R. For example,
177
        // if x = "A" in the current context, then we may be interested in
178
        // reasoning about ( x in R ) * { x -> "A" }. Say we update the
179
        // membership to nx in R', then:
180
        // - nfexp => ( x in R ) <=> nx in R'
181
        // - rnfexp => R = R'
182
        // We use these explanations below as assumptions on inferences when
183
        // appropriate. Notice that for inferring conflicts and tautologies,
184
        // we use the normal form of x always. This is because we always want to
185
        // discover conflicts/tautologies whenever possible.
186
        // For inferences based on regular expression unfolding, we do not use
187
        // the normal form of x. The reason is that it is better to unfold
188
        // regular expression memberships in a context-indepedent manner,
189
        // that is, not taking into account the current normal form of x, since
190
        // this ensures these lemmas are still relevant after backtracking.
191
696
        std::vector<Node> nfexp;
192
696
        std::vector<Node> rnfexp;
193
        // The normal form of x is stored in nx, while x is left unchanged.
194
696
        Node nx = x;
195
364
        if (!x.isConst())
196
        {
197
348
          nx = d_csolver.getNormalString(x, nfexp);
198
        }
199
        // If r is not a constant regular expression, we update it based on
200
        // normal forms, which may concretize its variables.
201
364
        if (!d_regexp_opr.checkConstRegExp(r))
202
        {
203
24
          r = getNormalSymRegExp(r, rnfexp);
204
24
          nfexp.insert(nfexp.end(), rnfexp.begin(), rnfexp.end());
205
24
          changed = true;
206
        }
207
728
        Trace("strings-regexp-nf") << "Term " << atom << " is normalized to "
208
364
                                   << nx << " IN " << r << std::endl;
209
364
        if (nx != x || changed)
210
        {
211
          // We rewrite the membership nx IN r.
212
308
          Node tmp = Rewriter::rewrite(nm->mkNode(STRING_IN_REGEXP, nx, r));
213
161
          Trace("strings-regexp-nf") << "Simplifies to " << tmp << std::endl;
214
161
          if (tmp.isConst())
215
          {
216
22
            if (tmp.getConst<bool>() == polarity)
217
            {
218
              // it is satisfied in this SAT context
219
8
              d_regexp_ccached.insert(assertion);
220
8
              continue;
221
            }
222
            else
223
            {
224
              // we have a conflict
225
12
              std::vector<Node> iexp = nfexp;
226
12
              std::vector<Node> noExplain;
227
6
              iexp.push_back(assertion);
228
6
              noExplain.push_back(assertion);
229
12
              Node conc = Node::null();
230
6
              d_im.sendInference(
231
                  iexp, noExplain, conc, InferenceId::STRINGS_RE_NF_CONFLICT);
232
6
              addedLemma = true;
233
6
              break;
234
            }
235
          }
236
        }
237
350
        if (e == 1 && repUnfold.find(rep) != repUnfold.end())
238
        {
239
          // do not unfold negative memberships of strings that have new
240
          // positive unfoldings. For example:
241
          //   x in ("A")* ^ NOT x in ("B")*
242
          // We unfold x = "A" ++ x' only. The intution here is that positive
243
          // unfoldings lead to stronger constraints (equalities are stronger
244
          // than disequalities), and are easier to check.
245
18
          continue;
246
        }
247
332
        if (polarity)
248
        {
249
258
          flag = checkPDerivative(x, r, atom, addedLemma, rnfexp);
250
        }
251
        else
252
        {
253
74
          if (!options::stringExp())
254
          {
255
            throw LogicException(
256
                "Strings Incomplete (due to Negative Membership) by default, "
257
                "try --strings-exp option.");
258
          }
259
        }
260
332
        if (flag)
261
        {
262
          // check if the term is atomic
263
648
          Trace("strings-regexp")
264
324
              << "Unroll/simplify membership of atomic term " << rep
265
324
              << std::endl;
266
          // if so, do simple unrolling
267
324
          Trace("strings-regexp") << "Simplify on " << atom << std::endl;
268
648
          Node conc = d_regexp_opr.simplify(atom, polarity);
269
324
          Trace("strings-regexp") << "...finished" << std::endl;
270
          // if simplifying successfully generated a lemma
271
324
          if (!conc.isNull())
272
          {
273
636
            std::vector<Node> iexp = rnfexp;
274
636
            std::vector<Node> noExplain;
275
318
            iexp.push_back(assertion);
276
318
            noExplain.push_back(assertion);
277
318
            Assert(atom.getKind() == STRING_IN_REGEXP);
278
318
            if (polarity)
279
            {
280
246
              d_statistics.d_regexpUnfoldingsPos << atom[1].getKind();
281
            }
282
            else
283
            {
284
72
              d_statistics.d_regexpUnfoldingsNeg << atom[1].getKind();
285
            }
286
318
            InferenceId inf =
287
318
                polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG;
288
318
            d_im.sendInference(iexp, noExplain, conc, inf);
289
318
            addedLemma = true;
290
318
            if (changed)
291
            {
292
2
              cprocessed.push_back(assertion);
293
            }
294
            else
295
            {
296
316
              processed.push_back(assertion);
297
            }
298
318
            if (e == 0)
299
            {
300
              // Remember that we have unfolded a membership for x
301
              // notice that we only do this here, after we have definitely
302
              // added a lemma.
303
246
              repUnfold.insert(rep);
304
            }
305
          }
306
          else
307
          {
308
            // otherwise we are incomplete
309
6
            d_im.setIncomplete();
310
          }
311
        }
312
332
        if (d_state.isInConflict())
313
        {
314
          break;
315
        }
316
      }
317
    }
318
  }
319
7324
  if (addedLemma)
320
  {
321
215
    if (!d_state.isInConflict())
322
    {
323
531
      for (unsigned i = 0; i < processed.size(); i++)
324
      {
325
632
        Trace("strings-regexp")
326
316
            << "...add " << processed[i] << " to u-cache." << std::endl;
327
316
        d_regexp_ucached.insert(processed[i]);
328
      }
329
217
      for (unsigned i = 0; i < cprocessed.size(); i++)
330
      {
331
4
        Trace("strings-regexp")
332
2
            << "...add " << cprocessed[i] << " to c-cache." << std::endl;
333
2
        d_regexp_ccached.insert(cprocessed[i]);
334
      }
335
    }
336
  }
337
}
338
339
607
bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
340
{
341
1214
  std::unordered_set<Node, NodeHashFunction> remove;
342
343
1408
  for (const Node& m1 : mems)
344
  {
345
811
    bool m1Neg = m1.getKind() == NOT;
346
1610
    Node m1Lit = m1Neg ? m1[0] : m1;
347
348
811
    if (remove.find(m1) != remove.end())
349
    {
350
      // Skip memberships marked for removal
351
2
      continue;
352
    }
353
354
2170
    for (const Node& m2 : mems)
355
    {
356
1375
      if (m1 == m2)
357
      {
358
805
        continue;
359
      }
360
361
570
      bool m2Neg = m2.getKind() == NOT;
362
1126
      Node m2Lit = m2Neg ? m2[0] : m2;
363
364
      // Both regular expression memberships have the same polarity
365
570
      if (m1Neg == m2Neg)
366
      {
367
402
        if (d_regexp_opr.regExpIncludes(m1Lit[1], m2Lit[1]))
368
        {
369
8
          if (m1Neg)
370
          {
371
            // ~str.in.re(x, R1) includes ~str.in.re(x, R2) --->
372
            //   mark ~str.in.re(x, R2) as reduced
373
4
            d_im.markReduced(m2Lit);
374
4
            remove.insert(m2);
375
          }
376
          else
377
          {
378
            // str.in.re(x, R1) includes str.in.re(x, R2) --->
379
            //   mark str.in.re(x, R1) as reduced
380
4
            d_im.markReduced(m1Lit);
381
4
            remove.insert(m1);
382
383
            // We don't need to process m1 anymore
384
4
            break;
385
          }
386
        }
387
      }
388
      else
389
      {
390
326
        Node pos = m1Neg ? m2Lit : m1Lit;
391
326
        Node neg = m1Neg ? m1Lit : m2Lit;
392
168
        if (d_regexp_opr.regExpIncludes(neg[1], pos[1]))
393
        {
394
          // We have a conflict because we have a case where str.in.re(x, R1)
395
          // and ~str.in.re(x, R2) but R2 includes R1, so there is no
396
          // possible value for x that satisfies both memberships.
397
20
          std::vector<Node> vec_nodes;
398
10
          vec_nodes.push_back(pos);
399
10
          vec_nodes.push_back(neg.negate());
400
401
10
          if (pos[0] != neg[0])
402
          {
403
            vec_nodes.push_back(pos[0].eqNode(neg[0]));
404
          }
405
406
20
          Node conc;
407
10
          d_im.sendInference(
408
              vec_nodes, conc, InferenceId::STRINGS_RE_INTER_INCLUDE, false, true);
409
10
          return false;
410
        }
411
      }
412
    }
413
  }
414
415
1791
  mems.erase(std::remove_if(
416
                 mems.begin(),
417
                 mems.end(),
418
1394
                 [&remove](Node& n) { return remove.find(n) != remove.end(); }),
419
2388
             mems.end());
420
421
597
  return true;
422
}
423
424
597
bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
425
{
426
  // do not compute intersections if the re intersection mode is none
427
1826
  if (options::stringRegExpInterMode() == options::RegExpInterMode::NONE)
428
  {
429
    return true;
430
  }
431
597
  if (mems.empty())
432
  {
433
    // nothing to do
434
    return true;
435
  }
436
  // the initial regular expression membership and its constant type
437
1194
  Node mi;
438
597
  RegExpConstType rcti = RE_C_UNKNOWN;
439
597
  NodeManager* nm = NodeManager::currentNM();
440
1320
  for (const Node& m : mems)
441
  {
442
1077
    if (m.getKind() != STRING_IN_REGEXP)
443
    {
444
      // do not do negative
445
306
      Assert(m.getKind() == NOT && m[0].getKind() == STRING_IN_REGEXP);
446
1022
      continue;
447
    }
448
465
    RegExpConstType rct = d_regexp_opr.getRegExpConstType(m[1]);
449
465
    if (rct == RE_C_VARIABLE
450
741
        || (options::stringRegExpInterMode()
451
                == options::RegExpInterMode::CONSTANT
452
443
            && rct != RE_C_CONRETE_CONSTANT))
453
    {
454
      // cannot do intersection on RE with variables, or with re.allchar based
455
      // on option.
456
276
      continue;
457
    }
458
378
    if (options::stringRegExpInterMode()
459
189
        == options::RegExpInterMode::ONE_CONSTANT)
460
    {
461
      if (!mi.isNull() && rcti >= RE_C_CONSTANT && rct >= RE_C_CONSTANT)
462
      {
463
        // if both have re.allchar, do not do intersection if the
464
        // options::RegExpInterMode::ONE_CONSTANT option is set.
465
        continue;
466
      }
467
    }
468
323
    if (mi.isNull())
469
    {
470
      // first regular expression seen
471
134
      mi = m;
472
134
      rcti = rct;
473
134
      continue;
474
    }
475
62
    Node resR = d_regexp_opr.intersect(mi[1], m[1]);
476
    // intersection should be computable
477
55
    Assert(!resR.isNull());
478
55
    if (resR == d_emptyRegexp)
479
    {
480
      // conflict, explain
481
24
      std::vector<Node> vec_nodes;
482
12
      vec_nodes.push_back(mi);
483
12
      vec_nodes.push_back(m);
484
12
      if (mi[0] != m[0])
485
      {
486
8
        vec_nodes.push_back(mi[0].eqNode(m[0]));
487
      }
488
24
      Node conc;
489
12
      d_im.sendInference(
490
          vec_nodes, conc, InferenceId::STRINGS_RE_INTER_CONF, false, true);
491
      // conflict, return
492
12
      return false;
493
    }
494
    // rewrite to ensure the equality checks below are precise
495
50
    Node mres = nm->mkNode(STRING_IN_REGEXP, mi[0], resR);
496
50
    Node mresr = Rewriter::rewrite(mres);
497
43
    if (mresr == mi)
498
    {
499
      // if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent
500
      // to x in R1, hence x in R2 can be marked redundant.
501
1
      d_im.markReduced(m);
502
    }
503
42
    else if (mresr == m)
504
    {
505
      // same as above, opposite direction
506
6
      d_im.markReduced(mi);
507
    }
508
    else
509
    {
510
      // new conclusion
511
      // (x in R1 ^ y in R2 ^ x = y) => (x in intersect(R1,R2))
512
72
      std::vector<Node> vec_nodes;
513
36
      vec_nodes.push_back(mi);
514
36
      vec_nodes.push_back(m);
515
36
      if (mi[0] != m[0])
516
      {
517
        vec_nodes.push_back(mi[0].eqNode(m[0]));
518
      }
519
36
      d_im.sendInference(
520
          vec_nodes, mres, InferenceId::STRINGS_RE_INTER_INFER, false, true);
521
      // both are reduced
522
36
      d_im.markReduced(m);
523
36
      d_im.markReduced(mi);
524
      // do not send more than one lemma for this class
525
36
      return true;
526
    }
527
  }
528
549
  return true;
529
}
530
531
258
bool RegExpSolver::checkPDerivative(
532
    Node x, Node r, Node atom, bool& addedLemma, std::vector<Node>& nf_exp)
533
{
534
258
  if (d_state.areEqual(x, d_emptyString))
535
  {
536
4
    Node exp;
537
4
    switch (d_regexp_opr.delta(r, exp))
538
    {
539
      case 0:
540
      {
541
        std::vector<Node> noExplain;
542
        noExplain.push_back(atom);
543
        noExplain.push_back(x.eqNode(d_emptyString));
544
        std::vector<Node> iexp = nf_exp;
545
        iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
546
        d_im.sendInference(iexp, noExplain, exp, InferenceId::STRINGS_RE_DELTA);
547
        addedLemma = true;
548
        d_regexp_ccached.insert(atom);
549
        return false;
550
      }
551
      case 1:
552
      {
553
        d_regexp_ccached.insert(atom);
554
        break;
555
      }
556
4
      case 2:
557
      {
558
8
        std::vector<Node> noExplain;
559
4
        noExplain.push_back(atom);
560
4
        noExplain.push_back(x.eqNode(d_emptyString));
561
8
        std::vector<Node> iexp = nf_exp;
562
4
        iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
563
4
        d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF);
564
4
        addedLemma = true;
565
4
        d_regexp_ccached.insert(atom);
566
4
        return false;
567
      }
568
      default:
569
        // Impossible
570
        break;
571
    }
572
  }
573
  else
574
  {
575
254
    if (deriveRegExp(x, r, atom, nf_exp))
576
    {
577
4
      addedLemma = true;
578
4
      d_regexp_ccached.insert(atom);
579
4
      return false;
580
    }
581
  }
582
250
  return true;
583
}
584
585
254
CVC4::String RegExpSolver::getHeadConst(Node x)
586
{
587
254
  if (x.isConst())
588
  {
589
4
    return x.getConst<String>();
590
  }
591
250
  else if (x.getKind() == STRING_CONCAT)
592
  {
593
32
    if (x[0].isConst())
594
    {
595
8
      return x[0].getConst<String>();
596
    }
597
  }
598
242
  return d_emptyString.getConst<String>();
599
}
600
601
254
bool RegExpSolver::deriveRegExp(Node x,
602
                                Node r,
603
                                Node atom,
604
                                std::vector<Node>& ant)
605
{
606
254
  Assert(x != d_emptyString);
607
508
  Trace("regexp-derive") << "RegExpSolver::deriveRegExp: x=" << x
608
254
                         << ", r= " << r << std::endl;
609
508
  CVC4::String s = getHeadConst(x);
610
  // only allow RE_DERIVE for concrete constant regular expressions
611
254
  if (!s.empty() && d_regexp_opr.getRegExpConstType(r) == RE_C_CONRETE_CONSTANT)
612
  {
613
8
    Node conc = Node::null();
614
8
    Node dc = r;
615
4
    bool flag = true;
616
4
    for (unsigned i = 0; i < s.size(); ++i)
617
    {
618
4
      CVC4::String c = s.substr(i, 1);
619
4
      Node dc2;
620
4
      int rt = d_regexp_opr.derivativeS(dc, c, dc2);
621
4
      dc = dc2;
622
4
      if (rt == 2)
623
      {
624
        // CONFLICT
625
4
        flag = false;
626
4
        break;
627
      }
628
    }
629
    // send lemma
630
4
    if (flag)
631
    {
632
      if (x.isConst())
633
      {
634
        Assert(false)
635
            << "Impossible: RegExpSolver::deriveRegExp: const string in const "
636
               "regular expression.";
637
        return false;
638
      }
639
      else
640
      {
641
        Assert(x.getKind() == STRING_CONCAT);
642
        std::vector<Node> vec_nodes;
643
        for (unsigned int i = 1; i < x.getNumChildren(); ++i)
644
        {
645
          vec_nodes.push_back(x[i]);
646
        }
647
        Node left = utils::mkConcat(vec_nodes, x.getType());
648
        left = Rewriter::rewrite(left);
649
        conc = NodeManager::currentNM()->mkNode(STRING_IN_REGEXP, left, dc);
650
      }
651
    }
652
8
    std::vector<Node> iexp = ant;
653
8
    std::vector<Node> noExplain;
654
4
    noExplain.push_back(atom);
655
4
    iexp.push_back(atom);
656
4
    d_im.sendInference(iexp, noExplain, conc, InferenceId::STRINGS_RE_DERIVE);
657
4
    return true;
658
  }
659
250
  return false;
660
}
661
662
80
Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp)
663
{
664
80
  Node ret = r;
665
80
  switch (r.getKind())
666
  {
667
18
    case REGEXP_EMPTY:
668
    case REGEXP_SIGMA:
669
18
    case REGEXP_RANGE: break;
670
18
    case STRING_TO_REGEXP:
671
    {
672
18
      if (!r[0].isConst())
673
      {
674
36
        Node tmp = d_csolver.getNormalString(r[0], nf_exp);
675
18
        if (tmp != r[0])
676
        {
677
14
          ret = NodeManager::currentNM()->mkNode(STRING_TO_REGEXP, tmp);
678
        }
679
      }
680
18
      break;
681
    }
682
38
    case REGEXP_CONCAT:
683
    case REGEXP_UNION:
684
    case REGEXP_INTER:
685
    case REGEXP_STAR:
686
    case REGEXP_COMPLEMENT:
687
    {
688
76
      std::vector<Node> vec_nodes;
689
94
      for (const Node& cr : r)
690
      {
691
56
        vec_nodes.push_back(getNormalSymRegExp(cr, nf_exp));
692
      }
693
38
      ret = Rewriter::rewrite(
694
76
          NodeManager::currentNM()->mkNode(r.getKind(), vec_nodes));
695
38
      break;
696
    }
697
6
    default:
698
    {
699
12
      Trace("strings-error") << "Unsupported term: " << r
700
6
                             << " in normalization SymRegExp." << std::endl;
701
6
      Assert(!utils::isRegExpKind(r.getKind()));
702
    }
703
  }
704
80
  return ret;
705
}
706
707
}  // namespace strings
708
}  // namespace theory
709
28228
}  // namespace CVC4