GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/sequences_rewriter.cpp Lines: 1524 1591 95.8 %
Date: 2021-03-23 Branches: 4734 9230 51.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sequences_rewriter.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 theory of strings.
13
 **
14
 ** Implementation of the theory of strings.
15
 **/
16
17
#include "theory/strings/sequences_rewriter.h"
18
19
#include "expr/attribute.h"
20
#include "expr/node_builder.h"
21
#include "expr/sequence.h"
22
#include "theory/rewriter.h"
23
#include "theory/strings/arith_entail.h"
24
#include "theory/strings/regexp_entail.h"
25
#include "theory/strings/strings_rewriter.h"
26
#include "theory/strings/theory_strings_utils.h"
27
#include "theory/strings/word.h"
28
29
using namespace std;
30
using namespace CVC4::kind;
31
32
namespace CVC4 {
33
namespace theory {
34
namespace strings {
35
36
9279
SequencesRewriter::SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics)
37
9279
    : d_statistics(statistics), d_stringsEntail(*this)
38
{
39
9279
}
40
41
93229
Node SequencesRewriter::rewriteEquality(Node node)
42
{
43
93229
  Assert(node.getKind() == kind::EQUAL);
44
93229
  if (node[0] == node[1])
45
  {
46
6544
    Node ret = NodeManager::currentNM()->mkConst(true);
47
3272
    return returnRewrite(node, ret, Rewrite::EQ_REFL);
48
  }
49
89957
  else if (node[0].isConst() && node[1].isConst())
50
  {
51
4942
    Node ret = NodeManager::currentNM()->mkConst(false);
52
2471
    return returnRewrite(node, ret, Rewrite::EQ_CONST_FALSE);
53
  }
54
55
  // ( ~contains( s, t ) V ~contains( t, s ) ) => ( s == t ---> false )
56
261956
  for (unsigned r = 0; r < 2; r++)
57
  {
58
    // must call rewrite contains directly to avoid infinite loop
59
    // we do a fix point since we may rewrite contains terms to simpler
60
    // contains terms.
61
349310
    Node ctn = d_stringsEntail.checkContains(node[r], node[1 - r], false);
62
174840
    if (!ctn.isNull())
63
    {
64
26504
      if (!ctn.getConst<bool>())
65
      {
66
370
        return returnRewrite(node, ctn, Rewrite::EQ_NCTN);
67
      }
68
      else
69
      {
70
        // definitely contains but not syntactically equal
71
        // We may be able to simplify, e.g.
72
        //  str.++( x, "a" ) == "a"  ----> x = ""
73
      }
74
    }
75
  }
76
77
  // ( len( s ) != len( t ) ) => ( s == t ---> false )
78
  // This covers cases like str.++( x, x ) == "a" ---> false
79
174232
  Node len0 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
80
174232
  Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
81
174232
  Node len_eq = len0.eqNode(len1);
82
87116
  len_eq = Rewriter::rewrite(len_eq);
83
87116
  if (len_eq.isConst() && !len_eq.getConst<bool>())
84
  {
85
6
    return returnRewrite(node, len_eq, Rewrite::EQ_LEN_DEQ);
86
  }
87
88
174220
  std::vector<Node> c[2];
89
261330
  for (unsigned i = 0; i < 2; i++)
90
  {
91
174220
    utils::getConcat(node[i], c[i]);
92
  }
93
94
  // check if the prefix, suffix mismatches
95
  //   For example, str.++( x, "a", y ) == str.++( x, "bc", z ) ---> false
96
87110
  unsigned minsize = std::min(c[0].size(), c[1].size());
97
261290
  for (unsigned r = 0; r < 2; r++)
98
  {
99
182970
    for (unsigned i = 0; i < minsize; i++)
100
    {
101
181359
      unsigned index1 = r == 0 ? i : (c[0].size() - 1) - i;
102
181359
      unsigned index2 = r == 0 ? i : (c[1].size() - 1) - i;
103
190126
      Node s = c[0][index1];
104
190126
      Node t = c[1][index2];
105
181359
      if (s.isConst() && t.isConst())
106
      {
107
4762
        size_t lenS = Word::getLength(s);
108
4762
        size_t lenT = Word::getLength(t);
109
4762
        size_t lenShort = lenS <= lenT ? lenS : lenT;
110
12398
        bool isSameFix = r == 1 ? Word::rstrncmp(s, t, lenShort)
111
7636
                                : Word::strncmp(s, t, lenShort);
112
4762
        if (!isSameFix)
113
        {
114
46
          Node ret = NodeManager::currentNM()->mkConst(false);
115
23
          return returnRewrite(node, ret, Rewrite::EQ_NFIX);
116
        }
117
      }
118
181336
      if (s != t)
119
      {
120
172569
        break;
121
      }
122
    }
123
  }
124
125
  // standard ordering
126
87087
  if (node[0] > node[1])
127
  {
128
37806
    Node ret = NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]);
129
18903
    return returnRewrite(node, ret, Rewrite::EQ_SYM);
130
  }
131
68184
  return node;
132
}
133
134
86339
Node SequencesRewriter::rewriteEqualityExt(Node node)
135
{
136
86339
  Assert(node.getKind() == EQUAL);
137
86339
  if (node[0].getType().isInteger())
138
  {
139
11428
    return rewriteArithEqualityExt(node);
140
  }
141
74911
  if (node[0].getType().isStringLike())
142
  {
143
74911
    return rewriteStrEqualityExt(node);
144
  }
145
  return node;
146
}
147
148
74911
Node SequencesRewriter::rewriteStrEqualityExt(Node node)
149
{
150
74911
  Assert(node.getKind() == EQUAL && node[0].getType().isStringLike());
151
149822
  TypeNode stype = node[0].getType();
152
153
74911
  NodeManager* nm = NodeManager::currentNM();
154
149822
  std::vector<Node> c[2];
155
149822
  Node new_ret;
156
224733
  for (unsigned i = 0; i < 2; i++)
157
  {
158
149822
    utils::getConcat(node[i], c[i]);
159
  }
160
  // ------- equality unification
161
74911
  bool changed = false;
162
224733
  for (unsigned i = 0; i < 2; i++)
163
  {
164
154426
    while (!c[0].empty() && !c[1].empty() && c[0].back() == c[1].back())
165
    {
166
2302
      c[0].pop_back();
167
2302
      c[1].pop_back();
168
2302
      changed = true;
169
    }
170
    // splice constants
171
446191
    if (!c[0].empty() && !c[1].empty() && c[0].back().isConst()
172
275748
        && c[1].back().isConst())
173
    {
174
868
      Node cs[2];
175
      size_t csl[2];
176
1302
      for (unsigned j = 0; j < 2; j++)
177
      {
178
868
        cs[j] = c[j].back();
179
868
        csl[j] = Word::getLength(cs[j]);
180
      }
181
434
      size_t larger = csl[0] > csl[1] ? 0 : 1;
182
434
      size_t smallerSize = csl[1 - larger];
183
868
      if (cs[1 - larger]
184
868
          == (i == 0 ? Word::suffix(cs[larger], smallerSize)
185
                     : Word::prefix(cs[larger], smallerSize)))
186
      {
187
414
        size_t sizeDiff = csl[larger] - smallerSize;
188
414
        c[larger][c[larger].size() - 1] =
189
828
            i == 0 ? Word::prefix(cs[larger], sizeDiff)
190
                   : Word::suffix(cs[larger], sizeDiff);
191
414
        c[1 - larger].pop_back();
192
414
        changed = true;
193
      }
194
    }
195
449466
    for (unsigned j = 0; j < 2; j++)
196
    {
197
299644
      std::reverse(c[j].begin(), c[j].end());
198
    }
199
  }
200
74911
  if (changed)
201
  {
202
    // e.g. x++y = x++z ---> y = z, "AB" ++ x = "A" ++ y --> "B" ++ x = y
203
5200
    Node s1 = utils::mkConcat(c[0], stype);
204
5200
    Node s2 = utils::mkConcat(c[1], stype);
205
2600
    new_ret = s1.eqNode(s2);
206
2600
    node = returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY);
207
  }
208
209
  // ------- homogeneous constants
210
224719
  for (unsigned i = 0; i < 2; i++)
211
  {
212
299630
    Node cn = StringsEntail::checkHomogeneousString(node[i]);
213
149822
    if (!cn.isNull() && !Word::isEmpty(cn))
214
    {
215
24176
      Assert(cn.isConst());
216
24176
      Assert(Word::getLength(cn) == 1);
217
218
      // The operands of the concat on each side of the equality without
219
      // constant strings
220
72528
      std::vector<Node> trimmed[2];
221
      // Counts the number of `cn`s on each side
222
24176
      size_t numCns[2] = {0, 0};
223
72500
      for (size_t j = 0; j < 2; j++)
224
      {
225
        // Sort the operands of the concats on both sides of the equality
226
        // (since both sides may only contain one char, the order does not
227
        // matter)
228
48338
        std::sort(c[j].begin(), c[j].end());
229
96525
        for (const Node& cc : c[j])
230
        {
231
48201
          if (cc.isConst())
232
          {
233
            // Count the number of `cn`s in the string constant and make
234
            // sure that all chars are `cn`s
235
48144
            std::vector<Node> veccc = Word::getChars(cc);
236
48440
            for (const Node& cv : veccc)
237
            {
238
24375
              if (cv != cn)
239
              {
240
                // This conflict case should mostly should be taken care of by
241
                // multiset reasoning in the strings rewriter, but we recognize
242
                // this conflict just in case.
243
14
                new_ret = nm->mkConst(false);
244
                return returnRewrite(
245
14
                    node, new_ret, Rewrite::STR_EQ_CONST_NHOMOG);
246
              }
247
24361
              numCns[j]++;
248
            }
249
          }
250
          else
251
          {
252
24122
            trimmed[j].push_back(cc);
253
          }
254
        }
255
      }
256
257
      // We have to remove the same number of `cn`s from both sides, so the
258
      // side with less `cn`s determines how many we can remove
259
24162
      size_t trimmedConst = std::min(numCns[0], numCns[1]);
260
72486
      for (size_t j = 0; j < 2; j++)
261
      {
262
48324
        size_t diff = numCns[j] - trimmedConst;
263
48324
        if (diff != 0)
264
        {
265
          // Add a constant string to the side with more `cn`s to restore
266
          // the difference in number of `cn`s
267
45228
          std::vector<Node> vec(diff, cn);
268
22614
          trimmed[j].push_back(Word::mkWordFlatten(vec));
269
        }
270
      }
271
272
48324
      Node lhs = utils::mkConcat(trimmed[i], stype);
273
48324
      Node ss = utils::mkConcat(trimmed[1 - i], stype);
274
24162
      if (lhs != node[i] || ss != node[1 - i])
275
      {
276
        // e.g.
277
        //  "AA" = y ++ x ---> "AA" = x ++ y if x < y
278
        //  "AAA" = y ++ "A" ++ z ---> "AA" = y ++ z
279
16
        new_ret = lhs.eqNode(ss);
280
16
        node = returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST);
281
      }
282
    }
283
  }
284
285
  // ------- rewrites for (= "" _)
286
149794
  Node empty = Word::mkEmptyWord(stype);
287
213308
  for (size_t i = 0; i < 2; i++)
288
  {
289
144164
    if (node[i] == empty)
290
    {
291
84839
      Node ne = node[1 - i];
292
45296
      if (ne.getKind() == STRING_STRREPL)
293
      {
294
        // (= "" (str.replace x y x)) ---> (= x "")
295
1221
        if (ne[0] == ne[2])
296
        {
297
350
          Node ret = nm->mkNode(EQUAL, ne[0], empty);
298
175
          return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_X_Y_X);
299
        }
300
301
        // (= "" (str.replace x y "A")) ---> (and (= x "") (not (= y "")))
302
1046
        if (StringsEntail::checkNonEmpty(ne[2]))
303
        {
304
          Node ret =
305
              nm->mkNode(AND,
306
594
                         nm->mkNode(EQUAL, ne[0], empty),
307
1188
                         nm->mkNode(NOT, nm->mkNode(EQUAL, ne[1], empty)));
308
297
          return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);
309
        }
310
311
        // (= "" (str.replace x "A" "")) ---> (str.prefix x "A")
312
749
        if (StringsEntail::checkLengthOne(ne[1], true) && ne[2] == empty)
313
        {
314
212
          Node ret = nm->mkNode(STRING_PREFIX, ne[0], ne[1]);
315
106
          return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);
316
        }
317
      }
318
44075
      else if (ne.getKind() == STRING_SUBSTR)
319
      {
320
36491
        Node zero = nm->mkConst(Rational(0));
321
322
20833
        if (ArithEntail::check(ne[1], false) && ArithEntail::check(ne[2], true))
323
        {
324
          // (= "" (str.substr x 0 m)) ---> (= "" x) if m > 0
325
4062
          if (ne[1] == zero)
326
          {
327
2626
            Node ret = nm->mkNode(EQUAL, ne[0], empty);
328
1313
            return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_LEN);
329
          }
330
331
          // (= "" (str.substr x n m)) ---> (<= (str.len x) n)
332
          // if n >= 0 and m > 0
333
5498
          Node ret = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, ne[0]), ne[1]);
334
2749
          return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_LEN);
335
        }
336
337
        // (= "" (str.substr "A" 0 z)) ---> (<= z 0)
338
16771
        if (StringsEntail::checkNonEmpty(ne[0]) && ne[1] == zero)
339
        {
340
2226
          Node ret = nm->mkNode(LEQ, ne[2], zero);
341
1113
          return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_Z);
342
        }
343
      }
344
    }
345
  }
346
347
  // ------- rewrites for (= (str.replace _ _ _) _)
348
207327
  for (size_t i = 0; i < 2; i++)
349
  {
350
138261
    if (node[i].getKind() == STRING_STRREPL)
351
    {
352
2648
      Node repl = node[i];
353
2648
      Node x = node[1 - i];
354
355
      // (= "A" (str.replace "" x y)) ---> (= "" (str.replace "A" y x))
356
1363
      if (StringsEntail::checkNonEmpty(x) && repl[0] == empty)
357
      {
358
        Node ret = nm->mkNode(
359
36
            EQUAL, empty, nm->mkNode(STRING_STRREPL, x, repl[2], repl[1]));
360
18
        return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_EMP);
361
      }
362
363
      // (= x (str.replace y x y)) ---> (= x y)
364
1345
      if (repl[0] == repl[2] && x == repl[1])
365
      {
366
4
        Node ret = nm->mkNode(EQUAL, x, repl[0]);
367
2
        return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_TO_EQ);
368
      }
369
370
      // (= x (str.replace x "A" "B")) ---> (not (str.contains x "A"))
371
1343
      if (x == repl[0])
372
      {
373
970
        Node eq = Rewriter::rewrite(nm->mkNode(EQUAL, repl[1], repl[2]));
374
512
        if (eq.isConst() && !eq.getConst<bool>())
375
        {
376
108
          Node ret = nm->mkNode(NOT, nm->mkNode(STRING_STRCTN, x, repl[1]));
377
54
          return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_NOT_CTN);
378
        }
379
      }
380
381
      // (= (str.replace x y z) z) --> (or (= x y) (= x z))
382
      // if (str.len y) = (str.len z)
383
1289
      if (repl[2] == x)
384
      {
385
1338
        Node lenY = nm->mkNode(STRING_LENGTH, repl[1]);
386
1338
        Node lenZ = nm->mkNode(STRING_LENGTH, repl[2]);
387
671
        if (ArithEntail::checkEq(lenY, lenZ))
388
        {
389
          Node ret = nm->mkNode(OR,
390
8
                                nm->mkNode(EQUAL, repl[0], repl[1]),
391
16
                                nm->mkNode(EQUAL, repl[0], repl[2]));
392
4
          return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_TO_DIS);
393
        }
394
      }
395
    }
396
  }
397
398
  // Try to rewrite (= x y) into a conjunction of equalities based on length
399
  // entailment.
400
  //
401
  // (<= (str.len x) (str.++ y1 ... yn)) AND (= x (str.++ y1 ... yn)) --->
402
  //  (and (= x (str.++ y1' ... ym')) (= y1'' "") ... (= yk'' ""))
403
  //
404
  // where yi' and yi'' correspond to some yj and
405
  //   (<= (str.len x) (str.++ y1' ... ym'))
406
204901
  for (unsigned i = 0; i < 2; i++)
407
  {
408
136994
    if (node[1 - i].getKind() == STRING_CONCAT)
409
    {
410
1510
      new_ret = StringsEntail::inferEqsFromContains(node[i], node[1 - i]);
411
1510
      if (!new_ret.isNull())
412
      {
413
1159
        return returnRewrite(node, new_ret, Rewrite::STR_EQ_CONJ_LEN_ENTAIL);
414
      }
415
    }
416
  }
417
418
67907
  if (node[0].getKind() == STRING_CONCAT && node[1].getKind() == STRING_CONCAT)
419
  {
420
    // (= (str.++ x_1 ... x_i x_{i + 1} ... x_n)
421
    //    (str.++ y_1 ... y_j y_{j + 1} ... y_m)) --->
422
    //  (and (= (str.++ x_1 ... x_i) (str.++ y_1 ... y_j))
423
    //       (= (str.++ x_{i + 1} ... x_n) (str.++ y_{j + 1} ... y_m)))
424
    //
425
    // if (str.len (str.++ x_1 ... x_i)) = (str.len (str.++ y_1 ... y_j))
426
    //
427
    // This rewrite performs length-based equality splitting: If we can show
428
    // that two prefixes have the same length, we can split an equality into
429
    // two equalities, one over the prefixes and another over the suffixes.
430
28
    std::vector<Node> v0, v1;
431
18
    utils::getConcat(node[0], v0);
432
18
    utils::getConcat(node[1], v1);
433
18
    size_t startRhs = 0;
434
70
    for (size_t i = 0, size0 = v0.size(); i <= size0; i++)
435
    {
436
112
      std::vector<Node> pfxv0(v0.begin(), v0.begin() + i);
437
112
      Node pfx0 = utils::mkConcat(pfxv0, stype);
438
218
      for (size_t j = startRhs, size1 = v1.size(); j <= size1; j++)
439
      {
440
186
        if (!(i == 0 && j == 0) && !(i == v0.size() && j == v1.size()))
441
        {
442
288
          std::vector<Node> pfxv1(v1.begin(), v1.begin() + j);
443
288
          Node pfx1 = utils::mkConcat(pfxv1, stype);
444
288
          Node lenPfx0 = nm->mkNode(STRING_LENGTH, pfx0);
445
288
          Node lenPfx1 = nm->mkNode(STRING_LENGTH, pfx1);
446
447
158
          if (ArithEntail::checkEq(lenPfx0, lenPfx1))
448
          {
449
8
            std::vector<Node> sfxv0(v0.begin() + i, v0.end());
450
8
            std::vector<Node> sfxv1(v1.begin() + j, v1.end());
451
            Node ret = nm->mkNode(kind::AND,
452
8
                                  pfx0.eqNode(pfx1),
453
8
                                  utils::mkConcat(sfxv0, stype)
454
16
                                      .eqNode(utils::mkConcat(sfxv1, stype)));
455
4
            return returnRewrite(node, ret, Rewrite::SPLIT_EQ);
456
          }
457
154
          else if (ArithEntail::check(lenPfx1, lenPfx0, true))
458
          {
459
            // The prefix on the right-hand side is strictly longer than the
460
            // prefix on the left-hand side, so we try to strip the right-hand
461
            // prefix by the length of the left-hand prefix
462
            //
463
            // Example:
464
            // (= (str.++ "A" x y) (str.++ x "AB" z)) --->
465
            //   (and (= (str.++ "A" x) (str.++ x "A")) (= y (str.++ "B" z)))
466
20
            std::vector<Node> rpfxv1;
467
20
            if (StringsEntail::stripSymbolicLength(
468
                    pfxv1, rpfxv1, 1, lenPfx0, true))
469
            {
470
              std::vector<Node> sfxv0(v0.begin() + i, v0.end());
471
              pfxv1.insert(pfxv1.end(), v1.begin() + j, v1.end());
472
              Node ret = nm->mkNode(kind::AND,
473
                                    pfx0.eqNode(utils::mkConcat(rpfxv1, stype)),
474
                                    utils::mkConcat(sfxv0, stype)
475
                                        .eqNode(utils::mkConcat(pfxv1, stype)));
476
              return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_R);
477
            }
478
479
            // If the prefix of the right-hand side is (strictly) longer than
480
            // the prefix of the left-hand side, we can advance the left-hand
481
            // side (since the length of the right-hand side is only increasing
482
            // in the inner loop)
483
20
            break;
484
          }
485
134
          else if (ArithEntail::check(lenPfx0, lenPfx1, true))
486
          {
487
            // The prefix on the left-hand side is strictly longer than the
488
            // prefix on the right-hand side, so we try to strip the left-hand
489
            // prefix by the length of the right-hand prefix
490
            //
491
            // Example:
492
            // (= (str.++ x "AB" z) (str.++ "A" x y)) --->
493
            //   (and (= (str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y))
494
48
            std::vector<Node> rpfxv0;
495
26
            if (StringsEntail::stripSymbolicLength(
496
                    pfxv0, rpfxv0, 1, lenPfx1, true))
497
            {
498
4
              pfxv0.insert(pfxv0.end(), v0.begin() + i, v0.end());
499
8
              std::vector<Node> sfxv1(v1.begin() + j, v1.end());
500
              Node ret = nm->mkNode(kind::AND,
501
8
                                    utils::mkConcat(rpfxv0, stype).eqNode(pfx1),
502
8
                                    utils::mkConcat(pfxv0, stype)
503
16
                                        .eqNode(utils::mkConcat(sfxv1, stype)));
504
4
              return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_L);
505
            }
506
507
            // If the prefix of the left-hand side is (strictly) longer than
508
            // the prefix of the right-hand side, then we don't need to check
509
            // that right-hand prefix for future left-hand prefixes anymore
510
            // (since they are increasing in length)
511
22
            startRhs = j + 1;
512
          }
513
        }
514
      }
515
    }
516
  }
517
518
67899
  return node;
519
}
520
521
11428
Node SequencesRewriter::rewriteArithEqualityExt(Node node)
522
{
523
11428
  Assert(node.getKind() == EQUAL && node[0].getType().isInteger());
524
525
  // cases where we can solve the equality
526
527
  // notice we cannot rewrite str.to.int(x)=n to x="n" due to leading zeroes.
528
529
11428
  return node;
530
}
531
532
165317
Node SequencesRewriter::rewriteLength(Node node)
533
{
534
165317
  Assert(node.getKind() == STRING_LENGTH);
535
165317
  NodeManager* nm = NodeManager::currentNM();
536
165317
  Kind nk0 = node[0].getKind();
537
165317
  if (node[0].isConst())
538
  {
539
12906
    Node retNode = nm->mkConst(Rational(Word::getLength(node[0])));
540
6453
    return returnRewrite(node, retNode, Rewrite::LEN_EVAL);
541
  }
542
158864
  else if (nk0 == kind::STRING_CONCAT)
543
  {
544
8078
    Node tmpNode = node[0];
545
8078
    if (tmpNode.getKind() == kind::STRING_CONCAT)
546
    {
547
16156
      std::vector<Node> node_vec;
548
31935
      for (unsigned int i = 0; i < tmpNode.getNumChildren(); ++i)
549
      {
550
23857
        if (tmpNode[i].isConst())
551
        {
552
5918
          node_vec.push_back(
553
11836
              nm->mkConst(Rational(Word::getLength(tmpNode[i]))));
554
        }
555
        else
556
        {
557
17939
          node_vec.push_back(NodeManager::currentNM()->mkNode(
558
              kind::STRING_LENGTH, tmpNode[i]));
559
        }
560
      }
561
16156
      Node retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
562
8078
      return returnRewrite(node, retNode, Rewrite::LEN_CONCAT);
563
    }
564
  }
565
150786
  else if (nk0 == STRING_STRREPL || nk0 == STRING_STRREPLALL)
566
  {
567
1443
    Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1]));
568
1443
    Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2]));
569
741
    if (len1 == len2)
570
    {
571
      // len( y ) == len( z ) => len( str.replace( x, y, z ) ) ---> len( x )
572
78
      Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
573
39
      return returnRewrite(node, retNode, Rewrite::LEN_REPL_INV);
574
702
    }
575
  }
576
150045
  else if (nk0 == STRING_TOLOWER || nk0 == STRING_TOUPPER || nk0 == STRING_REV
577
149939
           || nk0 == STRING_UPDATE)
578
  {
579
    // len( f( x ) ) == len( x ) where f is tolower, toupper, or rev.
580
    // len( update( x, n, y ) ) = len( x )
581
240
    Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
582
120
    return returnRewrite(node, retNode, Rewrite::LEN_CONV_INV);
583
  }
584
149925
  else if (nk0 == SEQ_UNIT)
585
  {
586
182
    Node retNode = nm->mkConst(Rational(1));
587
91
    return returnRewrite(node, retNode, Rewrite::LEN_SEQ_UNIT);
588
  }
589
150536
  return node;
590
}
591
592
// TODO (#1180) add rewrite
593
//  str.++( str.substr( x, n1, n2 ), str.substr( x, n1+n2, n3 ) ) --->
594
//  str.substr( x, n1, n2+n3 )
595
44432
Node SequencesRewriter::rewriteConcat(Node node)
596
{
597
44432
  Assert(node.getKind() == kind::STRING_CONCAT);
598
88864
  Trace("strings-rewrite-debug")
599
44432
      << "Strings::rewriteConcat start " << node << std::endl;
600
88864
  std::vector<Node> node_vec;
601
88864
  Node preNode = Node::null();
602
180120
  for (Node tmpNode : node)
603
  {
604
135688
    if (tmpNode.getKind() == STRING_CONCAT)
605
    {
606
610
      unsigned j = 0;
607
      // combine the first term with the previous constant if applicable
608
610
      if (!preNode.isNull())
609
      {
610
198
        if (tmpNode[0].isConst())
611
        {
612
224
          std::vector<Node> wvec;
613
112
          wvec.push_back(preNode);
614
112
          wvec.push_back(tmpNode[0]);
615
112
          preNode = Word::mkWordFlatten(wvec);
616
112
          node_vec.push_back(preNode);
617
        }
618
        else
619
        {
620
86
          node_vec.push_back(preNode);
621
86
          node_vec.push_back(tmpNode[0]);
622
        }
623
198
        preNode = Node::null();
624
198
        ++j;
625
      }
626
      // insert the middle terms to node_vec
627
610
      if (j <= tmpNode.getNumChildren() - 1)
628
      {
629
610
        node_vec.insert(node_vec.end(), tmpNode.begin() + j, tmpNode.end() - 1);
630
      }
631
      // take the last term as the current
632
610
      tmpNode = tmpNode[tmpNode.getNumChildren() - 1];
633
    }
634
135688
    if (!tmpNode.isConst())
635
    {
636
72272
      if (!preNode.isNull())
637
      {
638
14981
        if (preNode.isConst() && !Word::isEmpty(preNode))
639
        {
640
14507
          node_vec.push_back(preNode);
641
        }
642
14981
        preNode = Node::null();
643
      }
644
72272
      node_vec.push_back(tmpNode);
645
    }
646
    else
647
    {
648
63416
      if (preNode.isNull())
649
      {
650
39002
        preNode = tmpNode;
651
      }
652
      else
653
      {
654
48828
        std::vector<Node> vec;
655
24414
        vec.push_back(preNode);
656
24414
        vec.push_back(tmpNode);
657
24414
        preNode = Word::mkWordFlatten(vec);
658
      }
659
    }
660
  }
661
44432
  if (!preNode.isNull() && (!preNode.isConst() || !Word::isEmpty(preNode)))
662
  {
663
23047
    node_vec.push_back(preNode);
664
  }
665
666
  // Sort adjacent operands in str.++ that all result in the same string or the
667
  // empty string.
668
  //
669
  // E.g.: (str.++ ... (str.replace "A" x "") "A" (str.substr "A" 0 z) ...) -->
670
  // (str.++ ... [sort those 3 arguments] ... )
671
44432
  size_t lastIdx = 0;
672
88864
  Node lastX;
673
155762
  for (size_t i = 0, nsize = node_vec.size(); i < nsize; i++)
674
  {
675
222660
    Node s = StringsEntail::getStringOrEmpty(node_vec[i]);
676
111330
    bool nextX = false;
677
111330
    if (s != lastX)
678
    {
679
107969
      nextX = true;
680
    }
681
682
111330
    if (nextX)
683
    {
684
107969
      std::sort(node_vec.begin() + lastIdx, node_vec.begin() + i);
685
107969
      lastX = s;
686
107969
      lastIdx = i;
687
    }
688
  }
689
44432
  std::sort(node_vec.begin() + lastIdx, node_vec.end());
690
691
88864
  TypeNode tn = node.getType();
692
88864
  Node retNode = utils::mkConcat(node_vec, tn);
693
88864
  Trace("strings-rewrite-debug")
694
44432
      << "Strings::rewriteConcat end " << retNode << std::endl;
695
44432
  if (retNode != node)
696
  {
697
15408
    return returnRewrite(node, retNode, Rewrite::CONCAT_NORM);
698
  }
699
29024
  return node;
700
}
701
702
2275
Node SequencesRewriter::rewriteConcatRegExp(TNode node)
703
{
704
2275
  Assert(node.getKind() == kind::REGEXP_CONCAT);
705
2275
  NodeManager* nm = NodeManager::currentNM();
706
4550
  Trace("strings-rewrite-debug")
707
2275
      << "Strings::rewriteConcatRegExp flatten " << node << std::endl;
708
4550
  Node retNode = node;
709
4550
  std::vector<Node> vec;
710
2275
  bool changed = false;
711
4550
  Node emptyRe;
712
713
  // get the string type that are members of this regular expression
714
4550
  TypeNode rtype = node.getType();
715
4550
  TypeNode stype;
716
2275
  if (rtype.isRegExp())
717
  {
718
    // standard regular expressions are for strings
719
2275
    stype = nm->stringType();
720
  }
721
  else
722
  {
723
    Unimplemented();
724
  }
725
726
8916
  for (const Node& c : node)
727
  {
728
6665
    if (c.getKind() == REGEXP_CONCAT)
729
    {
730
177
      changed = true;
731
567
      for (const Node& cc : c)
732
      {
733
390
        vec.push_back(cc);
734
      }
735
    }
736
15809
    else if (c.getKind() == STRING_TO_REGEXP && c[0].isConst()
737
15780
             && Word::isEmpty(c[0]))
738
    {
739
104
      changed = true;
740
104
      emptyRe = c;
741
    }
742
6384
    else if (c.getKind() == REGEXP_EMPTY)
743
    {
744
      // re.++( ..., empty, ... ) ---> empty
745
48
      std::vector<Node> nvec;
746
48
      Node ret = nm->mkNode(REGEXP_EMPTY, nvec);
747
24
      return returnRewrite(node, ret, Rewrite::RE_CONCAT_EMPTY);
748
    }
749
    else
750
    {
751
6360
      vec.push_back(c);
752
    }
753
  }
754
2251
  if (changed)
755
  {
756
    // flatten
757
    // this handles nested re.++ and elimination or str.to.re(""), e.g.:
758
    // re.++( re.++( R1, R2 ), str.to.re(""), R3 ) ---> re.++( R1, R2, R3 )
759
263
    if (vec.empty())
760
    {
761
2
      Assert(!emptyRe.isNull());
762
2
      retNode = emptyRe;
763
    }
764
    else
765
    {
766
261
      retNode = vec.size() == 1 ? vec[0] : nm->mkNode(REGEXP_CONCAT, vec);
767
    }
768
263
    return returnRewrite(node, retNode, Rewrite::RE_CONCAT_FLATTEN);
769
  }
770
3976
  Trace("strings-rewrite-debug")
771
1988
      << "Strings::rewriteConcatRegExp start " << node << std::endl;
772
3976
  std::vector<Node> cvec;
773
  // the current accumulation of constant strings
774
3976
  std::vector<Node> preReStr;
775
  // whether the last component was (_)*
776
1988
  bool lastAllStar = false;
777
3976
  String emptyStr = String("");
778
  // this loop checks to see if components can be combined or dropped
779
10002
  for (unsigned i = 0, size = vec.size(); i <= size; i++)
780
  {
781
16028
    Node curr;
782
8014
    if (i < size)
783
    {
784
6026
      curr = vec[i];
785
6026
      Assert(curr.getKind() != REGEXP_CONCAT);
786
    }
787
    // update preReStr
788
8014
    if (!curr.isNull() && curr.getKind() == STRING_TO_REGEXP)
789
    {
790
2535
      lastAllStar = false;
791
2535
      preReStr.push_back(curr[0]);
792
2535
      curr = Node::null();
793
    }
794
5479
    else if (!preReStr.empty())
795
    {
796
2082
      Assert(!lastAllStar);
797
      // this groups consecutive strings a++b ---> ab
798
4164
      Node acc = nm->mkNode(STRING_TO_REGEXP, utils::mkConcat(preReStr, stype));
799
2082
      cvec.push_back(acc);
800
2082
      preReStr.clear();
801
    }
802
3397
    else if (!curr.isNull() && lastAllStar)
803
    {
804
      // if empty, drop it
805
      // e.g. this ensures we rewrite (_)* ++ (a)* ---> (_)*
806
387
      if (RegExpEntail::isConstRegExp(curr)
807
387
          && RegExpEntail::testConstStringInRegExp(emptyStr, 0, curr))
808
      {
809
49
        curr = Node::null();
810
      }
811
    }
812
8014
    if (!curr.isNull())
813
    {
814
3442
      lastAllStar = false;
815
3442
      if (curr.getKind() == REGEXP_STAR)
816
      {
817
        // we can group stars (a)* ++ (a)* ---> (a)*
818
1806
        if (!cvec.empty() && cvec.back() == curr)
819
        {
820
8
          curr = Node::null();
821
        }
822
1798
        else if (curr[0].getKind() == REGEXP_SIGMA)
823
        {
824
854
          Assert(!lastAllStar);
825
854
          lastAllStar = true;
826
          // go back and remove empty ones from back of cvec
827
          // e.g. this ensures we rewrite (a)* ++ (_)* ---> (_)*
828
2433
          while (!cvec.empty() && RegExpEntail::isConstRegExp(cvec.back())
829
3279
                 && RegExpEntail::testConstStringInRegExp(
830
693
                     emptyStr, 0, cvec.back()))
831
          {
832
8
            cvec.pop_back();
833
          }
834
        }
835
      }
836
    }
837
8014
    if (!curr.isNull())
838
    {
839
3434
      cvec.push_back(curr);
840
    }
841
  }
842
1988
  Assert(!cvec.empty());
843
1988
  retNode = utils::mkConcat(cvec, rtype);
844
1988
  if (retNode != node)
845
  {
846
    // handles all cases where consecutive re constants are combined or
847
    // dropped as described in the loop above.
848
200
    return returnRewrite(node, retNode, Rewrite::RE_CONCAT);
849
  }
850
851
  // flipping adjacent star arguments
852
1788
  changed = false;
853
5044
  for (size_t i = 0, size = cvec.size() - 1; i < size; i++)
854
  {
855
3256
    if (cvec[i].getKind() == REGEXP_STAR && cvec[i][0] == cvec[i + 1])
856
    {
857
      // by convention, flip the order (a*)++a ---> a++(a*)
858
64
      std::swap(cvec[i], cvec[i + 1]);
859
64
      changed = true;
860
    }
861
  }
862
1788
  if (changed)
863
  {
864
48
    retNode = utils::mkConcat(cvec, rtype);
865
48
    return returnRewrite(node, retNode, Rewrite::RE_CONCAT_OPT);
866
  }
867
1740
  return node;
868
}
869
870
832
Node SequencesRewriter::rewriteStarRegExp(TNode node)
871
{
872
832
  Assert(node.getKind() == REGEXP_STAR);
873
832
  NodeManager* nm = NodeManager::currentNM();
874
1664
  Node retNode = node;
875
832
  if (node[0].getKind() == REGEXP_STAR)
876
  {
877
    // ((R)*)* ---> R*
878
4
    return returnRewrite(node, node[0], Rewrite::RE_STAR_NESTED_STAR);
879
  }
880
2804
  else if (node[0].getKind() == STRING_TO_REGEXP && node[0][0].isConst()
881
2804
           && Word::isEmpty(node[0][0]))
882
  {
883
    // ("")* ---> ""
884
12
    return returnRewrite(node, node[0], Rewrite::RE_STAR_EMPTY_STRING);
885
  }
886
816
  else if (node[0].getKind() == REGEXP_EMPTY)
887
  {
888
    // (empty)* ---> ""
889
6
    retNode = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")));
890
6
    return returnRewrite(node, retNode, Rewrite::RE_STAR_EMPTY);
891
  }
892
810
  else if (node[0].getKind() == REGEXP_UNION)
893
  {
894
    // simplification of unions under star
895
146
    if (RegExpEntail::hasEpsilonNode(node[0]))
896
    {
897
20
      bool changed = false;
898
20
      std::vector<Node> node_vec;
899
60
      for (const Node& nc : node[0])
900
      {
901
120
        if (nc.getKind() == STRING_TO_REGEXP && nc[0].isConst()
902
120
            && Word::isEmpty(nc[0]))
903
        {
904
          // can be removed
905
20
          changed = true;
906
        }
907
        else
908
        {
909
20
          node_vec.push_back(nc);
910
        }
911
      }
912
20
      if (changed)
913
      {
914
20
        retNode = node_vec.size() == 1 ? node_vec[0]
915
                                       : nm->mkNode(REGEXP_UNION, node_vec);
916
20
        retNode = nm->mkNode(REGEXP_STAR, retNode);
917
        // simplification of union beneath star based on loop above
918
        // for example, ( "" | "a" )* ---> ("a")*
919
20
        return returnRewrite(node, retNode, Rewrite::RE_STAR_UNION);
920
      }
921
    }
922
  }
923
790
  return node;
924
}
925
926
694
Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
927
{
928
694
  Kind nk = node.getKind();
929
694
  Assert(nk == REGEXP_UNION || nk == REGEXP_INTER);
930
1388
  Trace("strings-rewrite-debug")
931
694
      << "Strings::rewriteAndOrRegExp start " << node << std::endl;
932
1388
  std::vector<Node> node_vec;
933
1388
  std::vector<Node> polRegExp[2];
934
2220
  for (const Node& ni : node)
935
  {
936
1528
    if (ni.getKind() == nk)
937
    {
938
33
      for (const Node& nic : ni)
939
      {
940
22
        if (std::find(node_vec.begin(), node_vec.end(), nic) == node_vec.end())
941
        {
942
22
          node_vec.push_back(nic);
943
        }
944
      }
945
    }
946
1517
    else if (ni.getKind() == REGEXP_EMPTY)
947
    {
948
39
      if (nk == REGEXP_INTER)
949
      {
950
2
        return returnRewrite(node, ni, Rewrite::RE_AND_EMPTY);
951
      }
952
      // otherwise, can ignore
953
    }
954
1478
    else if (ni.getKind() == REGEXP_STAR && ni[0].getKind() == REGEXP_SIGMA)
955
    {
956
8
      if (nk == REGEXP_UNION)
957
      {
958
        return returnRewrite(node, ni, Rewrite::RE_OR_ALL);
959
      }
960
      // otherwise, can ignore
961
    }
962
1470
    else if (std::find(node_vec.begin(), node_vec.end(), ni) == node_vec.end())
963
    {
964
1452
      node_vec.push_back(ni);
965
1452
      uint32_t pindex = ni.getKind() == REGEXP_COMPLEMENT ? 1 : 0;
966
2904
      Node nia = pindex == 1 ? ni[0] : ni;
967
1452
      polRegExp[pindex].push_back(nia);
968
    }
969
  }
970
692
  NodeManager* nm = NodeManager::currentNM();
971
1384
  std::vector<Node> emptyVec;
972
  // use inclusion tests
973
770
  for (const Node& negMem : polRegExp[1])
974
  {
975
134
    for (const Node& posMem : polRegExp[0])
976
    {
977
104
      Node m1 = nk == REGEXP_INTER ? negMem : posMem;
978
104
      Node m2 = nk == REGEXP_INTER ? posMem : negMem;
979
      // inclusion test for conflicting case m1 contains m2
980
      // (re.inter (re.comp R1) R2) --> re.none where R1 includes R2
981
      // (re.union R1 (re.comp R2)) --> (re.* re.allchar) where R1 includes R2
982
56
      if (RegExpEntail::regExpIncludes(m1, m2))
983
      {
984
16
        Node retNode;
985
8
        if (nk == REGEXP_INTER)
986
        {
987
8
          retNode = nm->mkNode(kind::REGEXP_EMPTY, emptyVec);
988
        }
989
        else
990
        {
991
          retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
992
        }
993
8
        return returnRewrite(node, retNode, Rewrite::RE_ANDOR_INC_CONFLICT);
994
      }
995
    }
996
  }
997
1368
  Node retNode;
998
684
  if (node_vec.empty())
999
  {
1000
    if (nk == REGEXP_INTER)
1001
    {
1002
      retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
1003
    }
1004
    else
1005
    {
1006
      retNode = nm->mkNode(kind::REGEXP_EMPTY, emptyVec);
1007
    }
1008
  }
1009
  else
1010
  {
1011
684
    retNode = node_vec.size() == 1 ? node_vec[0] : nm->mkNode(nk, node_vec);
1012
  }
1013
684
  if (retNode != node)
1014
  {
1015
    // flattening and removing children, based on loop above
1016
64
    return returnRewrite(node, retNode, Rewrite::RE_ANDOR_FLATTEN);
1017
  }
1018
620
  return node;
1019
}
1020
1021
24
Node SequencesRewriter::rewriteLoopRegExp(TNode node)
1022
{
1023
24
  Assert(node.getKind() == REGEXP_LOOP);
1024
48
  Node retNode = node;
1025
48
  Node r = node[0];
1026
24
  if (r.getKind() == REGEXP_STAR)
1027
  {
1028
    return returnRewrite(node, r, Rewrite::RE_LOOP_STAR);
1029
  }
1030
24
  NodeManager* nm = NodeManager::currentNM();
1031
48
  CVC4::Rational rMaxInt(String::maxSize());
1032
24
  uint32_t l = utils::getLoopMinOccurrences(node);
1033
48
  std::vector<Node> vec_nodes;
1034
110
  for (unsigned i = 0; i < l; i++)
1035
  {
1036
86
    vec_nodes.push_back(r);
1037
  }
1038
  Node n =
1039
24
      vec_nodes.size() == 0
1040
24
          ? nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")))
1041
48
          : vec_nodes.size() == 1 ? r : nm->mkNode(REGEXP_CONCAT, vec_nodes);
1042
24
  uint32_t u = utils::getLoopMaxOccurrences(node);
1043
24
  if (u < l)
1044
  {
1045
8
    std::vector<Node> nvec;
1046
4
    retNode = nm->mkNode(REGEXP_EMPTY, nvec);
1047
  }
1048
20
  else if (u == l)
1049
  {
1050
10
    retNode = n;
1051
  }
1052
  else
1053
  {
1054
20
    std::vector<Node> vec2;
1055
10
    vec2.push_back(n);
1056
20
    TypeNode rtype = nm->regExpType();
1057
52
    for (uint32_t j = l; j < u; j++)
1058
    {
1059
42
      vec_nodes.push_back(r);
1060
42
      n = utils::mkConcat(vec_nodes, rtype);
1061
42
      vec2.push_back(n);
1062
    }
1063
10
    retNode = nm->mkNode(REGEXP_UNION, vec2);
1064
  }
1065
48
  Trace("strings-lp") << "Strings::lp " << node << " => " << retNode
1066
24
                      << std::endl;
1067
24
  if (retNode != node)
1068
  {
1069
24
    return returnRewrite(node, retNode, Rewrite::RE_LOOP);
1070
  }
1071
  return node;
1072
}
1073
1074
4
Node SequencesRewriter::rewriteRepeatRegExp(TNode node)
1075
{
1076
4
  Assert(node.getKind() == REGEXP_REPEAT);
1077
4
  NodeManager* nm = NodeManager::currentNM();
1078
  // ((_ re.^ n) R) --> ((_ re.loop n n) R)
1079
4
  unsigned r = utils::getRepeatAmount(node);
1080
8
  Node lop = nm->mkConst(RegExpLoop(r, r));
1081
8
  Node retNode = nm->mkNode(REGEXP_LOOP, lop, node[0]);
1082
8
  return returnRewrite(node, retNode, Rewrite::RE_REPEAT_ELIM);
1083
}
1084
1085
22
Node SequencesRewriter::rewriteOptionRegExp(TNode node)
1086
{
1087
22
  Assert(node.getKind() == REGEXP_OPT);
1088
22
  NodeManager* nm = NodeManager::currentNM();
1089
  Node retNode =
1090
      nm->mkNode(REGEXP_UNION,
1091
44
                 nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))),
1092
88
                 node[0]);
1093
44
  return returnRewrite(node, retNode, Rewrite::RE_OPT_ELIM);
1094
}
1095
1096
32
Node SequencesRewriter::rewritePlusRegExp(TNode node)
1097
{
1098
32
  Assert(node.getKind() == REGEXP_PLUS);
1099
32
  NodeManager* nm = NodeManager::currentNM();
1100
  Node retNode =
1101
64
      nm->mkNode(REGEXP_CONCAT, node[0], nm->mkNode(REGEXP_STAR, node[0]));
1102
64
  return returnRewrite(node, retNode, Rewrite::RE_PLUS_ELIM);
1103
}
1104
1105
28
Node SequencesRewriter::rewriteDifferenceRegExp(TNode node)
1106
{
1107
28
  Assert(node.getKind() == REGEXP_DIFF);
1108
28
  NodeManager* nm = NodeManager::currentNM();
1109
  Node retNode =
1110
56
      nm->mkNode(REGEXP_INTER, node[0], nm->mkNode(REGEXP_COMPLEMENT, node[1]));
1111
56
  return returnRewrite(node, retNode, Rewrite::RE_DIFF_ELIM);
1112
}
1113
1114
322
Node SequencesRewriter::rewriteRangeRegExp(TNode node)
1115
{
1116
322
  Assert(node.getKind() == REGEXP_RANGE);
1117
322
  if (node[0] == node[1])
1118
  {
1119
    NodeManager* nm = NodeManager::currentNM();
1120
    Node retNode = nm->mkNode(STRING_TO_REGEXP, node[0]);
1121
    // re.range( "A", "A" ) ---> str.to_re( "A" )
1122
    return returnRewrite(node, retNode, Rewrite::RE_RANGE_SINGLE);
1123
  }
1124
322
  return node;
1125
}
1126
1127
6832
Node SequencesRewriter::rewriteMembership(TNode node)
1128
{
1129
6832
  NodeManager* nm = NodeManager::currentNM();
1130
13664
  Node x = node[0];
1131
13664
  Node r = node[1];
1132
1133
13664
  TypeNode stype = x.getType();
1134
13664
  TypeNode rtype = r.getType();
1135
1136
6832
  if(r.getKind() == kind::REGEXP_EMPTY)
1137
  {
1138
50
    Node retNode = NodeManager::currentNM()->mkConst(false);
1139
25
    return returnRewrite(node, retNode, Rewrite::RE_IN_EMPTY);
1140
  }
1141
6807
  else if (x.isConst() && RegExpEntail::isConstRegExp(r))
1142
  {
1143
    // test whether x in node[1]
1144
2722
    CVC4::String s = x.getConst<String>();
1145
1361
    bool test = RegExpEntail::testConstStringInRegExp(s, 0, r);
1146
2722
    Node retNode = NodeManager::currentNM()->mkConst(test);
1147
1361
    return returnRewrite(node, retNode, Rewrite::RE_IN_EVAL);
1148
  }
1149
5446
  else if (r.getKind() == kind::REGEXP_SIGMA)
1150
  {
1151
68
    Node one = nm->mkConst(Rational(1));
1152
68
    Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x));
1153
34
    return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA);
1154
  }
1155
5412
  else if (r.getKind() == kind::REGEXP_STAR)
1156
  {
1157
1744
    if (x.isConst())
1158
    {
1159
      size_t xlen = Word::getLength(x);
1160
      if (xlen == 0)
1161
      {
1162
        Node retNode = nm->mkConst(true);
1163
        // e.g. (str.in.re "" (re.* (str.to.re x))) ----> true
1164
        return returnRewrite(node, retNode, Rewrite::RE_EMPTY_IN_STR_STAR);
1165
      }
1166
      else if (xlen == 1)
1167
      {
1168
        if (r[0].getKind() == STRING_TO_REGEXP)
1169
        {
1170
          Node retNode = r[0][0].eqNode(x);
1171
          // e.g. (str.in.re "A" (re.* (str.to.re x))) ----> "A" = x
1172
          return returnRewrite(node, retNode, Rewrite::RE_CHAR_IN_STR_STAR);
1173
        }
1174
      }
1175
    }
1176
1744
    else if (x.getKind() == STRING_CONCAT)
1177
    {
1178
      // (str.in.re (str.++ x1 ... xn) (re.* R)) -->
1179
      //   (str.in.re x1 (re.* R)) AND ... AND (str.in.re xn (re.* R))
1180
      //     if the length of all strings in R is one.
1181
366
      Node flr = RegExpEntail::getFixedLengthForRegexp(r[0]);
1182
240
      if (!flr.isNull())
1183
      {
1184
114
        Node one = nm->mkConst(Rational(1));
1185
114
        if (flr == one)
1186
        {
1187
228
          NodeBuilder<> nb(AND);
1188
418
          for (const Node& xc : x)
1189
          {
1190
304
            nb << nm->mkNode(STRING_IN_REGEXP, xc, r);
1191
          }
1192
          return returnRewrite(
1193
114
              node, nb.constructNode(), Rewrite::RE_IN_DIST_CHAR_STAR);
1194
        }
1195
      }
1196
    }
1197
1630
    if (r[0].getKind() == kind::REGEXP_SIGMA)
1198
    {
1199
216
      Node retNode = NodeManager::currentNM()->mkConst(true);
1200
108
      return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA_STAR);
1201
    }
1202
  }
1203
3668
  else if (r.getKind() == kind::REGEXP_CONCAT)
1204
  {
1205
2735
    bool allSigma = true;
1206
2735
    bool allSigmaStrict = true;
1207
2735
    unsigned allSigmaMinSize = 0;
1208
5443
    Node constStr;
1209
2735
    size_t constIdx = 0;
1210
2735
    size_t nchildren = r.getNumChildren();
1211
6119
    for (size_t i = 0; i < nchildren; i++)
1212
    {
1213
9097
      Node rc = r[i];
1214
5713
      Assert(rc.getKind() != kind::REGEXP_EMPTY);
1215
5713
      if (rc.getKind() == kind::REGEXP_SIGMA)
1216
      {
1217
689
        allSigmaMinSize++;
1218
      }
1219
5024
      else if (rc.getKind() == REGEXP_STAR && rc[0].getKind() == REGEXP_SIGMA)
1220
      {
1221
1297
        allSigmaStrict = false;
1222
      }
1223
3727
      else if (rc.getKind() == STRING_TO_REGEXP)
1224
      {
1225
1947
        if (constStr.isNull())
1226
        {
1227
1398
          constStr = rc[0];
1228
1398
          constIdx = i;
1229
        }
1230
        else
1231
        {
1232
549
          allSigma = false;
1233
549
          break;
1234
        }
1235
      }
1236
      else
1237
      {
1238
1780
        allSigma = false;
1239
1780
        break;
1240
      }
1241
    }
1242
2735
    if (allSigma)
1243
    {
1244
406
      if (constStr.isNull())
1245
      {
1246
        // x in re.++(_*, _, _) ---> str.len(x) >= 2
1247
20
        Node num = nm->mkConst(Rational(allSigmaMinSize));
1248
20
        Node lenx = nm->mkNode(STRING_LENGTH, x);
1249
20
        Node retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
1250
10
        return returnRewrite(node, retNode, Rewrite::RE_CONCAT_PURE_ALLCHAR);
1251
      }
1252
396
      else if (allSigmaMinSize == 0 && nchildren >= 3 && constIdx != 0
1253
17
               && constIdx != nchildren - 1)
1254
      {
1255
        // x in re.++(_*, "abc", _*) ---> str.contains(x, "abc")
1256
34
        Node retNode = nm->mkNode(STRING_STRCTN, x, constStr);
1257
17
        return returnRewrite(node, retNode, Rewrite::RE_CONCAT_TO_CONTAINS);
1258
      }
1259
    }
1260
  }
1261
1866
  else if (r.getKind() == kind::REGEXP_INTER
1262
933
           || r.getKind() == kind::REGEXP_UNION)
1263
  {
1264
390
    std::vector<Node> mvec;
1265
635
    for (unsigned i = 0; i < r.getNumChildren(); i++)
1266
    {
1267
440
      mvec.push_back(
1268
880
          NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r[i]));
1269
    }
1270
    Node retNode = NodeManager::currentNM()->mkNode(
1271
390
        r.getKind() == kind::REGEXP_INTER ? kind::AND : kind::OR, mvec);
1272
195
    return returnRewrite(node, retNode, Rewrite::RE_IN_ANDOR);
1273
  }
1274
738
  else if (r.getKind() == kind::STRING_TO_REGEXP)
1275
  {
1276
716
    Node retNode = x.eqNode(r[0]);
1277
358
    return returnRewrite(node, retNode, Rewrite::RE_IN_CSTRING);
1278
  }
1279
380
  else if (r.getKind() == REGEXP_RANGE)
1280
  {
1281
    // x in re.range( char_i, char_j ) ---> i <= str.code(x) <= j
1282
552
    Node xcode = nm->mkNode(STRING_TO_CODE, x);
1283
    Node retNode =
1284
        nm->mkNode(AND,
1285
552
                   nm->mkNode(LEQ, nm->mkNode(STRING_TO_CODE, r[0]), xcode),
1286
1104
                   nm->mkNode(LEQ, xcode, nm->mkNode(STRING_TO_CODE, r[1])));
1287
276
    return returnRewrite(node, retNode, Rewrite::RE_IN_RANGE);
1288
  }
1289
104
  else if (r.getKind() == REGEXP_COMPLEMENT)
1290
  {
1291
88
    Node retNode = nm->mkNode(STRING_IN_REGEXP, x, r[0]).negate();
1292
44
    return returnRewrite(node, retNode, Rewrite::RE_IN_COMPLEMENT);
1293
  }
1294
1295
  // do simple consumes
1296
8580
  Node retNode = node;
1297
4290
  if (r.getKind() == kind::REGEXP_STAR)
1298
  {
1299
4556
    for (unsigned dir = 0; dir <= 1; dir++)
1300
    {
1301
6078
      std::vector<Node> mchildren;
1302
3044
      utils::getConcat(x, mchildren);
1303
3044
      bool success = true;
1304
9152
      while (success)
1305
      {
1306
3054
        success = false;
1307
6108
        std::vector<Node> children;
1308
3054
        utils::getConcat(r[0], children);
1309
6108
        Node scn = RegExpEntail::simpleRegexpConsume(mchildren, children, dir);
1310
3054
        if (!scn.isNull())
1311
        {
1312
          Trace("regexp-ext-rewrite")
1313
              << "Regexp star : const conflict : " << node << std::endl;
1314
          return returnRewrite(node, scn, Rewrite::RE_CONSUME_S_CCONF);
1315
        }
1316
3054
        else if (children.empty())
1317
        {
1318
          // fully consumed one copy of the STAR
1319
18
          if (mchildren.empty())
1320
          {
1321
            Trace("regexp-ext-rewrite")
1322
                << "Regexp star : full consume : " << node << std::endl;
1323
            Node ret = NodeManager::currentNM()->mkConst(true);
1324
            return returnRewrite(node, ret, Rewrite::RE_CONSUME_S_FULL);
1325
          }
1326
          else
1327
          {
1328
36
            Node prev = retNode;
1329
54
            retNode = nm->mkNode(
1330
36
                STRING_IN_REGEXP, utils::mkConcat(mchildren, stype), r);
1331
            // Iterate again if the node changed. It may not have changed if
1332
            // nothing was consumed from mchildren (e.g. if the body of the
1333
            // re.* accepts the empty string.
1334
18
            success = (retNode != prev);
1335
          }
1336
        }
1337
      }
1338
3044
      if (retNode != node)
1339
      {
1340
20
        Trace("regexp-ext-rewrite") << "Regexp star : rewrite " << node
1341
10
                                    << " -> " << retNode << std::endl;
1342
10
        return returnRewrite(node, retNode, Rewrite::RE_CONSUME_S);
1343
      }
1344
    }
1345
  }
1346
  else
1347
  {
1348
5208
    std::vector<Node> children;
1349
2768
    utils::getConcat(r, children);
1350
5208
    std::vector<Node> mchildren;
1351
2768
    utils::getConcat(x, mchildren);
1352
2768
    unsigned prevSize = children.size() + mchildren.size();
1353
5208
    Node scn = RegExpEntail::simpleRegexpConsume(mchildren, children);
1354
2768
    if (!scn.isNull())
1355
    {
1356
104
      Trace("regexp-ext-rewrite")
1357
52
          << "Regexp : const conflict : " << node << std::endl;
1358
52
      return returnRewrite(node, scn, Rewrite::RE_CONSUME_CCONF);
1359
    }
1360
2716
    else if ((children.size() + mchildren.size()) != prevSize)
1361
    {
1362
      // Given a membership (str.++ x1 ... xn) in (re.++ r1 ... rm),
1363
      // above, we strip components to construct an equivalent membership:
1364
      // (str.++ xi .. xj) in (re.++ rk ... rl).
1365
552
      Node xn = utils::mkConcat(mchildren, stype);
1366
552
      Node emptyStr = Word::mkEmptyWord(stype);
1367
276
      if (children.empty())
1368
      {
1369
        // If we stripped all components on the right, then the left is
1370
        // equal to the empty string.
1371
        // e.g. (str.++ "a" x) in (re.++ (str.to.re "a")) ---> (= x "")
1372
4
        retNode = xn.eqNode(emptyStr);
1373
      }
1374
      else
1375
      {
1376
        // otherwise, construct the updated regular expression
1377
272
        retNode =
1378
544
            nm->mkNode(STRING_IN_REGEXP, xn, utils::mkConcat(children, rtype));
1379
      }
1380
552
      Trace("regexp-ext-rewrite")
1381
276
          << "Regexp : rewrite : " << node << " -> " << retNode << std::endl;
1382
276
      return returnRewrite(node, retNode, Rewrite::RE_SIMPLE_CONSUME);
1383
    }
1384
  }
1385
3952
  return node;
1386
}
1387
1388
425863
RewriteResponse SequencesRewriter::postRewrite(TNode node)
1389
{
1390
851726
  Trace("sequences-postrewrite")
1391
425863
      << "Strings::SequencesRewriter::postRewrite start " << node << std::endl;
1392
851726
  Node retNode = node;
1393
425863
  Kind nk = node.getKind();
1394
425863
  if (nk == kind::STRING_CONCAT)
1395
  {
1396
44432
    retNode = rewriteConcat(node);
1397
  }
1398
381431
  else if (nk == kind::EQUAL)
1399
  {
1400
93229
    retNode = rewriteEquality(node);
1401
  }
1402
288202
  else if (nk == kind::STRING_LENGTH)
1403
  {
1404
165317
    retNode = rewriteLength(node);
1405
  }
1406
122885
  else if (nk == kind::STRING_CHARAT)
1407
  {
1408
110
    retNode = rewriteCharAt(node);
1409
  }
1410
122775
  else if (nk == kind::STRING_SUBSTR)
1411
  {
1412
39182
    retNode = rewriteSubstr(node);
1413
  }
1414
83593
  else if (nk == kind::STRING_UPDATE)
1415
  {
1416
175
    retNode = rewriteUpdate(node);
1417
  }
1418
83418
  else if (nk == kind::STRING_STRCTN)
1419
  {
1420
37385
    retNode = rewriteContains(node);
1421
  }
1422
46033
  else if (nk == kind::STRING_STRIDOF)
1423
  {
1424
4353
    retNode = rewriteIndexof(node);
1425
  }
1426
41680
  else if (nk == kind::STRING_STRREPL)
1427
  {
1428
2840
    retNode = rewriteReplace(node);
1429
  }
1430
38840
  else if (nk == kind::STRING_STRREPLALL)
1431
  {
1432
138
    retNode = rewriteReplaceAll(node);
1433
  }
1434
38702
  else if (nk == kind::STRING_REPLACE_RE)
1435
  {
1436
119
    retNode = rewriteReplaceRe(node);
1437
  }
1438
38583
  else if (nk == kind::STRING_REPLACE_RE_ALL)
1439
  {
1440
110
    retNode = rewriteReplaceReAll(node);
1441
  }
1442
38473
  else if (nk == STRING_REV)
1443
  {
1444
235
    retNode = rewriteStrReverse(node);
1445
  }
1446
38238
  else if (nk == kind::STRING_PREFIX || nk == kind::STRING_SUFFIX)
1447
  {
1448
130
    retNode = rewritePrefixSuffix(node);
1449
  }
1450
38108
  else if (nk == kind::STRING_IN_REGEXP)
1451
  {
1452
6832
    retNode = rewriteMembership(node);
1453
  }
1454
31276
  else if (nk == REGEXP_CONCAT)
1455
  {
1456
2275
    retNode = rewriteConcatRegExp(node);
1457
  }
1458
29001
  else if (nk == REGEXP_UNION || nk == REGEXP_INTER)
1459
  {
1460
694
    retNode = rewriteAndOrRegExp(node);
1461
  }
1462
28307
  else if (nk == REGEXP_DIFF)
1463
  {
1464
28
    retNode = rewriteDifferenceRegExp(node);
1465
  }
1466
28279
  else if (nk == REGEXP_STAR)
1467
  {
1468
832
    retNode = rewriteStarRegExp(node);
1469
  }
1470
27447
  else if (nk == REGEXP_PLUS)
1471
  {
1472
32
    retNode = rewritePlusRegExp(node);
1473
  }
1474
27415
  else if (nk == REGEXP_OPT)
1475
  {
1476
22
    retNode = rewriteOptionRegExp(node);
1477
  }
1478
27393
  else if (nk == REGEXP_RANGE)
1479
  {
1480
322
    retNode = rewriteRangeRegExp(node);
1481
  }
1482
27071
  else if (nk == REGEXP_LOOP)
1483
  {
1484
24
    retNode = rewriteLoopRegExp(node);
1485
  }
1486
27047
  else if (nk == REGEXP_REPEAT)
1487
  {
1488
4
    retNode = rewriteRepeatRegExp(node);
1489
  }
1490
27043
  else if (nk == SEQ_UNIT)
1491
  {
1492
292
    retNode = rewriteSeqUnit(node);
1493
  }
1494
26751
  else if (nk == SEQ_NTH || nk == SEQ_NTH_TOTAL)
1495
  {
1496
317
    retNode = rewriteSeqNth(node);
1497
  }
1498
1499
851726
  Trace("sequences-postrewrite")
1500
425863
      << "Strings::SequencesRewriter::postRewrite returning " << retNode
1501
425863
      << std::endl;
1502
425863
  if (node != retNode)
1503
  {
1504
171798
    Trace("strings-rewrite-debug") << "Strings::SequencesRewriter::postRewrite "
1505
85899
                                   << node << " to " << retNode << std::endl;
1506
85899
    return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
1507
  }
1508
339964
  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
1509
339964
  return RewriteResponse(REWRITE_DONE, retNode);
1510
}
1511
1512
265186
RewriteResponse SequencesRewriter::preRewrite(TNode node)
1513
{
1514
265186
  return RewriteResponse(REWRITE_DONE, node);
1515
}
1516
1517
317
Node SequencesRewriter::rewriteSeqNth(Node node)
1518
{
1519
317
  Assert(node.getKind() == SEQ_NTH || node.getKind() == SEQ_NTH_TOTAL);
1520
634
  Node s = node[0];
1521
634
  Node i = node[1];
1522
317
  if (s.isConst() && i.isConst())
1523
  {
1524
23
    size_t len = Word::getLength(s);
1525
23
    size_t pos = i.getConst<Rational>().getNumerator().toUnsignedInt();
1526
23
    if (pos < len)
1527
    {
1528
18
      std::vector<Node> elements = s.getConst<Sequence>().getVec();
1529
9
      const Node& ret = elements[pos];
1530
9
      return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL);
1531
    }
1532
14
    else if (node.getKind() == SEQ_NTH_TOTAL)
1533
    {
1534
      // return arbitrary term
1535
4
      Node ret = s.getType().getSequenceElementType().mkGroundValue();
1536
2
      return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB);
1537
    }
1538
    else
1539
    {
1540
12
      return node;
1541
    }
1542
  }
1543
  else
1544
  {
1545
294
    return node;
1546
  }
1547
}
1548
1549
110
Node SequencesRewriter::rewriteCharAt(Node node)
1550
{
1551
110
  Assert(node.getKind() == STRING_CHARAT);
1552
110
  NodeManager* nm = NodeManager::currentNM();
1553
220
  Node one = nm->mkConst(Rational(1));
1554
220
  Node retNode = nm->mkNode(STRING_SUBSTR, node[0], node[1], one);
1555
220
  return returnRewrite(node, retNode, Rewrite::CHARAT_ELIM);
1556
}
1557
1558
39194
Node SequencesRewriter::rewriteSubstr(Node node)
1559
{
1560
39194
  Assert(node.getKind() == kind::STRING_SUBSTR);
1561
1562
39194
  NodeManager* nm = NodeManager::currentNM();
1563
39194
  if (node[0].isConst())
1564
  {
1565
15377
    if (Word::isEmpty(node[0]))
1566
    {
1567
1690
      Node ret = node[0];
1568
845
      return returnRewrite(node, ret, Rewrite::SS_EMPTYSTR);
1569
    }
1570
    // rewriting for constant arguments
1571
14532
    if (node[1].isConst() && node[2].isConst())
1572
    {
1573
15350
      Node s = node[0];
1574
15350
      CVC4::Rational rMaxInt(String::maxSize());
1575
      uint32_t start;
1576
7675
      if (node[1].getConst<Rational>() > rMaxInt)
1577
      {
1578
        // start beyond the maximum size of strings
1579
        // thus, it must be beyond the end point of this string
1580
8
        Node ret = Word::mkEmptyWord(node.getType());
1581
4
        return returnRewrite(node, ret, Rewrite::SS_CONST_START_MAX_OOB);
1582
      }
1583
7671
      else if (node[1].getConst<Rational>().sgn() < 0)
1584
      {
1585
        // start before the beginning of the string
1586
1374
        Node ret = Word::mkEmptyWord(node.getType());
1587
687
        return returnRewrite(node, ret, Rewrite::SS_CONST_START_NEG);
1588
      }
1589
      else
1590
      {
1591
6984
        start = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
1592
6984
        if (start >= Word::getLength(node[0]))
1593
        {
1594
          // start beyond the end of the string
1595
760
          Node ret = Word::mkEmptyWord(node.getType());
1596
380
          return returnRewrite(node, ret, Rewrite::SS_CONST_START_OOB);
1597
        }
1598
      }
1599
6604
      if (node[2].getConst<Rational>() > rMaxInt)
1600
      {
1601
        // take up to the end of the string
1602
1
        size_t lenS = Word::getLength(s);
1603
2
        Node ret = Word::suffix(s, lenS - start);
1604
1
        return returnRewrite(node, ret, Rewrite::SS_CONST_LEN_MAX_OOB);
1605
      }
1606
6603
      else if (node[2].getConst<Rational>().sgn() <= 0)
1607
      {
1608
552
        Node ret = Word::mkEmptyWord(node.getType());
1609
276
        return returnRewrite(node, ret, Rewrite::SS_CONST_LEN_NON_POS);
1610
      }
1611
      else
1612
      {
1613
        uint32_t len =
1614
6327
            node[2].getConst<Rational>().getNumerator().toUnsignedInt();
1615
6327
        if (start + len > Word::getLength(node[0]))
1616
        {
1617
          // take up to the end of the string
1618
530
          size_t lenS = Word::getLength(s);
1619
1060
          Node ret = Word::suffix(s, lenS - start);
1620
530
          return returnRewrite(node, ret, Rewrite::SS_CONST_END_OOB);
1621
        }
1622
        else
1623
        {
1624
          // compute the substr using the constant string
1625
11594
          Node ret = Word::substr(s, start, len);
1626
5797
          return returnRewrite(node, ret, Rewrite::SS_CONST_SS);
1627
        }
1628
      }
1629
    }
1630
  }
1631
61348
  Node zero = nm->mkConst(CVC4::Rational(0));
1632
1633
  // if entailed non-positive length or negative start point
1634
30674
  if (ArithEntail::check(zero, node[1], true))
1635
  {
1636
20
    Node ret = Word::mkEmptyWord(node.getType());
1637
10
    return returnRewrite(node, ret, Rewrite::SS_START_NEG);
1638
  }
1639
30664
  else if (ArithEntail::check(zero, node[2]))
1640
  {
1641
1052
    Node ret = Word::mkEmptyWord(node.getType());
1642
526
    return returnRewrite(node, ret, Rewrite::SS_LEN_NON_POS);
1643
  }
1644
1645
30138
  if (node[0].getKind() == STRING_SUBSTR)
1646
  {
1647
    // (str.substr (str.substr x a b) c d) ---> "" if c >= b
1648
    //
1649
    // Note that this rewrite can be generalized to:
1650
    //
1651
    // (str.substr x a b) ---> "" if a >= (str.len x)
1652
    //
1653
    // This can be done when we generalize our entailment methods to
1654
    // accept an optional context. Then we could conjecture that
1655
    // (str.substr x a b) rewrites to "" and do a case analysis:
1656
    //
1657
    // - a < 0 or b < 0 (the result is trivially empty in these cases)
1658
    // - a >= (str.len x) assuming that { a >= 0, b >= 0 }
1659
    //
1660
    // For example, for (str.substr (str.substr x a a) a a), we could
1661
    // then deduce that under those assumptions, "a" is an
1662
    // over-approximation of the length of (str.substr x a a), which
1663
    // then allows us to reason that the result of the whole term must
1664
    // be empty.
1665
2626
    if (ArithEntail::check(node[1], node[0][2]))
1666
    {
1667
84
      Node ret = Word::mkEmptyWord(node.getType());
1668
42
      return returnRewrite(node, ret, Rewrite::SS_START_GEQ_LEN);
1669
    }
1670
  }
1671
27512
  else if (node[0].getKind() == STRING_STRREPL)
1672
  {
1673
    // (str.substr (str.replace x y z) 0 n)
1674
    // 	 ---> (str.replace (str.substr x 0 n) y z)
1675
    // if (str.len y) = 1 and (str.len z) = 1
1676
228
    if (node[1] == zero)
1677
    {
1678
246
      if (StringsEntail::checkLengthOne(node[0][1], true)
1679
246
          && StringsEntail::checkLengthOne(node[0][2], true))
1680
      {
1681
        Node ret = nm->mkNode(
1682
            kind::STRING_STRREPL,
1683
8
            nm->mkNode(kind::STRING_SUBSTR, node[0][0], node[1], node[2]),
1684
            node[0][1],
1685
16
            node[0][2]);
1686
4
        return returnRewrite(node, ret, Rewrite::SUBSTR_REPL_SWAP);
1687
      }
1688
    }
1689
  }
1690
1691
60184
  std::vector<Node> n1;
1692
30092
  utils::getConcat(node[0], n1);
1693
60184
  TypeNode stype = node.getType();
1694
1695
  // definite inclusion
1696
30092
  if (node[1] == zero)
1697
  {
1698
20223
    Node curr = node[2];
1699
20223
    std::vector<Node> childrenr;
1700
10360
    if (StringsEntail::stripSymbolicLength(n1, childrenr, 1, curr))
1701
    {
1702
497
      if (curr != zero && !n1.empty())
1703
      {
1704
303
        childrenr.push_back(nm->mkNode(
1705
202
            kind::STRING_SUBSTR, utils::mkConcat(n1, stype), node[1], curr));
1706
      }
1707
994
      Node ret = utils::mkConcat(childrenr, stype);
1708
497
      return returnRewrite(node, ret, Rewrite::SS_LEN_INCLUDE);
1709
    }
1710
  }
1711
1712
  // symbolic length analysis
1713
83978
  for (unsigned r = 0; r < 2; r++)
1714
  {
1715
    // the amount of characters we can strip
1716
111238
    Node curr;
1717
56855
    if (r == 0)
1718
    {
1719
29595
      if (node[1] != zero)
1720
      {
1721
        // strip up to start point off the start of the string
1722
19732
        curr = node[1];
1723
      }
1724
    }
1725
27260
    else if (r == 1)
1726
    {
1727
      Node tot_len =
1728
54450
          Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, node[0]));
1729
54450
      Node end_pt = Rewriter::rewrite(nm->mkNode(kind::PLUS, node[1], node[2]));
1730
27260
      if (node[2] != tot_len)
1731
      {
1732
26524
        if (ArithEntail::check(node[2], tot_len))
1733
        {
1734
          // end point beyond end point of string, map to tot_len
1735
88
          Node ret = nm->mkNode(kind::STRING_SUBSTR, node[0], node[1], tot_len);
1736
44
          return returnRewrite(node, ret, Rewrite::SS_END_PT_NORM);
1737
        }
1738
        else
1739
        {
1740
          // strip up to ( str.len(node[0]) - end_pt ) off the end of the string
1741
26480
          curr = Rewriter::rewrite(nm->mkNode(kind::MINUS, tot_len, end_pt));
1742
        }
1743
      }
1744
1745
      // (str.substr s x y) --> "" if x < len(s) |= 0 >= y
1746
      Node n1_lt_tot_len =
1747
54406
          Rewriter::rewrite(nm->mkNode(kind::LT, node[1], tot_len));
1748
27216
      if (ArithEntail::checkWithAssumption(n1_lt_tot_len, zero, node[2], false))
1749
      {
1750
32
        Node ret = Word::mkEmptyWord(node.getType());
1751
16
        return returnRewrite(node, ret, Rewrite::SS_START_ENTAILS_ZERO_LEN);
1752
      }
1753
1754
      // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
1755
      Node non_zero_len =
1756
54390
          Rewriter::rewrite(nm->mkNode(kind::LT, zero, node[2]));
1757
27200
      if (ArithEntail::checkWithAssumption(
1758
              non_zero_len, node[1], tot_len, false))
1759
      {
1760
4
        Node ret = Word::mkEmptyWord(node.getType());
1761
2
        return returnRewrite(node, ret, Rewrite::SS_NON_ZERO_LEN_ENTAILS_OOB);
1762
      }
1763
1764
      // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
1765
      Node geq_zero_start =
1766
54388
          Rewriter::rewrite(nm->mkNode(kind::GEQ, node[1], zero));
1767
27198
      if (ArithEntail::checkWithAssumption(
1768
              geq_zero_start, zero, tot_len, false))
1769
      {
1770
4
        Node ret = Word::mkEmptyWord(node.getType());
1771
        return returnRewrite(
1772
2
            node, ret, Rewrite::SS_GEQ_ZERO_START_ENTAILS_EMP_S);
1773
      }
1774
1775
      // (str.substr s x x) ---> "" if (str.len s) <= 1
1776
27196
      if (node[1] == node[2] && StringsEntail::checkLengthOne(node[0]))
1777
      {
1778
12
        Node ret = Word::mkEmptyWord(node.getType());
1779
6
        return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z);
1780
      }
1781
    }
1782
56785
    if (!curr.isNull())
1783
    {
1784
      // strip off components while quantity is entailed positive
1785
46186
      int dir = r == 0 ? 1 : -1;
1786
89970
      std::vector<Node> childrenr;
1787
46186
      if (StringsEntail::stripSymbolicLength(n1, childrenr, dir, curr))
1788
      {
1789
2402
        if (r == 0)
1790
        {
1791
          Node ret = nm->mkNode(
1792
4670
              kind::STRING_SUBSTR, utils::mkConcat(n1, stype), curr, node[2]);
1793
2335
          return returnRewrite(node, ret, Rewrite::SS_STRIP_START_PT);
1794
        }
1795
        else
1796
        {
1797
          Node ret = nm->mkNode(kind::STRING_SUBSTR,
1798
134
                                utils::mkConcat(n1, stype),
1799
                                node[1],
1800
268
                                node[2]);
1801
67
          return returnRewrite(node, ret, Rewrite::SS_STRIP_END_PT);
1802
        }
1803
      }
1804
    }
1805
  }
1806
  // combine substr
1807
27123
  if (node[0].getKind() == kind::STRING_SUBSTR)
1808
  {
1809
4659
    Node start_inner = node[0][1];
1810
4659
    Node start_outer = node[1];
1811
2505
    if (ArithEntail::check(start_outer) && ArithEntail::check(start_inner))
1812
    {
1813
      // both are positive
1814
      // thus, start point is definitely start_inner+start_outer.
1815
      // We can rewrite if it for certain what the length is
1816
1817
      // the length of a string from the inner substr subtracts the start point
1818
      // of the outer substr
1819
      Node len_from_inner =
1820
2655
          Rewriter::rewrite(nm->mkNode(kind::MINUS, node[0][2], start_outer));
1821
2655
      Node len_from_outer = node[2];
1822
2655
      Node new_len;
1823
      // take quantity that is for sure smaller than the other
1824
1503
      if (len_from_inner == len_from_outer)
1825
      {
1826
9
        new_len = len_from_inner;
1827
      }
1828
1494
      else if (ArithEntail::check(len_from_inner, len_from_outer))
1829
      {
1830
270
        new_len = len_from_outer;
1831
      }
1832
1224
      else if (ArithEntail::check(len_from_outer, len_from_inner))
1833
      {
1834
72
        new_len = len_from_inner;
1835
      }
1836
1503
      if (!new_len.isNull())
1837
      {
1838
702
        Node new_start = nm->mkNode(kind::PLUS, start_inner, start_outer);
1839
        Node ret =
1840
702
            nm->mkNode(kind::STRING_SUBSTR, node[0][0], new_start, new_len);
1841
351
        return returnRewrite(node, ret, Rewrite::SS_COMBINE);
1842
      }
1843
    }
1844
  }
1845
26772
  return node;
1846
}
1847
1848
175
Node SequencesRewriter::rewriteUpdate(Node node)
1849
{
1850
175
  Assert(node.getKind() == kind::STRING_UPDATE);
1851
350
  Node s = node[0];
1852
175
  if (s.isConst())
1853
  {
1854
163
    if (Word::isEmpty(s))
1855
    {
1856
      return returnRewrite(node, s, Rewrite::UPD_EMPTYSTR);
1857
    }
1858
    // rewriting for constant arguments
1859
163
    if (node[1].isConst())
1860
    {
1861
135
      CVC4::Rational rMaxInt(String::maxSize());
1862
119
      if (node[1].getConst<Rational>() > rMaxInt)
1863
      {
1864
        // start beyond the maximum size of strings
1865
        // thus, it must be beyond the end point of this string
1866
        return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_MAX_OOB);
1867
      }
1868
119
      else if (node[1].getConst<Rational>().sgn() < 0)
1869
      {
1870
        // start before the beginning of the string
1871
        return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_NEG);
1872
      }
1873
      uint32_t start =
1874
119
          node[1].getConst<Rational>().getNumerator().toUnsignedInt();
1875
119
      size_t len = Word::getLength(s);
1876
119
      if (start >= len)
1877
      {
1878
        // start beyond the end of the string
1879
        return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_OOB);
1880
      }
1881
119
      if (node[2].isConst())
1882
      {
1883
206
        Node ret = Word::update(s, start, node[2]);
1884
103
        return returnRewrite(node, ret, Rewrite::UPD_EVAL);
1885
      }
1886
    }
1887
  }
1888
1889
72
  return node;
1890
}
1891
1892
212369
Node SequencesRewriter::rewriteContains(Node node)
1893
{
1894
212369
  Assert(node.getKind() == kind::STRING_STRCTN);
1895
212369
  NodeManager* nm = NodeManager::currentNM();
1896
1897
212369
  if (node[0] == node[1])
1898
  {
1899
1178
    Node ret = NodeManager::currentNM()->mkConst(true);
1900
589
    return returnRewrite(node, ret, Rewrite::CTN_EQ);
1901
  }
1902
211780
  if (node[0].isConst())
1903
  {
1904
74471
    if (node[1].isConst())
1905
    {
1906
16396
      Node ret = nm->mkConst(Word::find(node[0], node[1]) != std::string::npos);
1907
8198
      return returnRewrite(node, ret, Rewrite::CTN_CONST);
1908
    }
1909
    else
1910
    {
1911
127549
      Node t = node[1];
1912
66273
      if (Word::isEmpty(node[0]))
1913
      {
1914
        Node len1 =
1915
48252
            NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
1916
24200
        if (ArithEntail::check(len1, true))
1917
        {
1918
          // we handle the false case here since the rewrite for equality
1919
          // uses this function, hence we want to conclude false if possible.
1920
          // len(x)>0 => contains( "", x ) ---> false
1921
296
          Node ret = NodeManager::currentNM()->mkConst(false);
1922
148
          return returnRewrite(node, ret, Rewrite::CTN_LHS_EMPTYSTR);
1923
        }
1924
      }
1925
42073
      else if (StringsEntail::checkLengthOne(t))
1926
      {
1927
9462
        std::vector<Node> vec = Word::getChars(node[0]);
1928
9462
        Node emp = Word::mkEmptyWord(t.getType());
1929
9462
        NodeBuilder<> nb(OR);
1930
4731
        nb << emp.eqNode(t);
1931
11878
        for (const Node& c : vec)
1932
        {
1933
7147
          Assert(c.getType() == t.getType());
1934
7147
          nb << c.eqNode(t);
1935
        }
1936
1937
        // str.contains("ABCabc", t) --->
1938
        // t = "" v t = "A" v t = "B" v t = "C" v t = "a" v t = "b" v t = "c"
1939
        // if len(t) <= 1
1940
9462
        Node ret = nb;
1941
4731
        return returnRewrite(node, ret, Rewrite::CTN_SPLIT);
1942
      }
1943
37342
      else if (node[1].getKind() == kind::STRING_CONCAT)
1944
      {
1945
        int firstc, lastc;
1946
2308
        if (!StringsEntail::canConstantContainConcat(
1947
                node[0], node[1], firstc, lastc))
1948
        {
1949
236
          Node ret = NodeManager::currentNM()->mkConst(false);
1950
118
          return returnRewrite(node, ret, Rewrite::CTN_NCONST_CTN_CONCAT);
1951
        }
1952
      }
1953
    }
1954
  }
1955
198585
  if (node[1].isConst())
1956
  {
1957
52300
    size_t len = Word::getLength(node[1]);
1958
52300
    if (len == 0)
1959
    {
1960
      // contains( x, "" ) ---> true
1961
47994
      Node ret = NodeManager::currentNM()->mkConst(true);
1962
23997
      return returnRewrite(node, ret, Rewrite::CTN_RHS_EMPTYSTR);
1963
    }
1964
28303
    else if (len == 1)
1965
    {
1966
      // The following rewrites are specific to a single character second
1967
      // argument of contains, where we can reason that this character is
1968
      // not split over multiple components in the first argument.
1969
14634
      if (node[0].getKind() == STRING_CONCAT)
1970
      {
1971
2026
        std::vector<Node> nc1;
1972
1013
        utils::getConcat(node[0], nc1);
1973
2026
        NodeBuilder<> nb(OR);
1974
3652
        for (const Node& ncc : nc1)
1975
        {
1976
2639
          nb << nm->mkNode(STRING_STRCTN, ncc, node[1]);
1977
        }
1978
2026
        Node ret = nb.constructNode();
1979
        // str.contains( x ++ y, "A" ) --->
1980
        //   str.contains( x, "A" ) OR str.contains( y, "A" )
1981
1013
        return returnRewrite(node, ret, Rewrite::CTN_CONCAT_CHAR);
1982
      }
1983
13621
      else if (node[0].getKind() == STRING_STRREPL)
1984
      {
1985
572
        Node rplDomain = d_stringsEntail.checkContains(node[0][1], node[1]);
1986
352
        if (!rplDomain.isNull() && !rplDomain.getConst<bool>())
1987
        {
1988
264
          Node d1 = nm->mkNode(STRING_STRCTN, node[0][0], node[1]);
1989
          Node d2 =
1990
              nm->mkNode(AND,
1991
264
                         nm->mkNode(STRING_STRCTN, node[0][0], node[0][1]),
1992
528
                         nm->mkNode(STRING_STRCTN, node[0][2], node[1]));
1993
264
          Node ret = nm->mkNode(OR, d1, d2);
1994
          // If str.contains( y, "A" ) ---> false, then:
1995
          // str.contains( str.replace( x, y, z ), "A" ) --->
1996
          //   str.contains( x, "A" ) OR
1997
          //   ( str.contains( x, y ) AND str.contains( z, "A" ) )
1998
132
          return returnRewrite(node, ret, Rewrite::CTN_REPL_CHAR);
1999
        }
2000
      }
2001
    }
2002
  }
2003
346886
  std::vector<Node> nc1;
2004
173443
  utils::getConcat(node[0], nc1);
2005
346886
  std::vector<Node> nc2;
2006
173443
  utils::getConcat(node[1], nc2);
2007
2008
  // component-wise containment
2009
346886
  std::vector<Node> nc1rb;
2010
346886
  std::vector<Node> nc1re;
2011
173443
  if (d_stringsEntail.componentContains(nc1, nc2, nc1rb, nc1re) != -1)
2012
  {
2013
4694
    Node ret = NodeManager::currentNM()->mkConst(true);
2014
2347
    return returnRewrite(node, ret, Rewrite::CTN_COMPONENT);
2015
  }
2016
342192
  TypeNode stype = node[0].getType();
2017
2018
  // strip endpoints
2019
342192
  std::vector<Node> nb;
2020
342192
  std::vector<Node> ne;
2021
171096
  if (StringsEntail::stripConstantEndpoints(nc1, nc2, nb, ne))
2022
  {
2023
    Node ret = NodeManager::currentNM()->mkNode(
2024
364
        kind::STRING_STRCTN, utils::mkConcat(nc1, stype), node[1]);
2025
182
    return returnRewrite(node, ret, Rewrite::CTN_STRIP_ENDPT);
2026
  }
2027
2028
421493
  for (const Node& n : nc2)
2029
  {
2030
250670
    if (n.getKind() == kind::STRING_STRREPL)
2031
    {
2032
      // (str.contains x (str.replace y z w)) --> false
2033
      // if (str.contains x y) = false and (str.contains x w) = false
2034
      //
2035
      // Reasoning: (str.contains x y) checks that x does not contain y if the
2036
      // replacement does not change y. (str.contains x w) checks that if the
2037
      // replacement changes anything in y, the w makes it impossible for it to
2038
      // occur in x.
2039
5145
      Node ctnConst = d_stringsEntail.checkContains(node[0], n[0]);
2040
2618
      if (!ctnConst.isNull() && !ctnConst.getConst<bool>())
2041
      {
2042
260
        Node ctnConst2 = d_stringsEntail.checkContains(node[0], n[2]);
2043
134
        if (!ctnConst2.isNull() && !ctnConst2.getConst<bool>())
2044
        {
2045
16
          Node res = nm->mkConst(false);
2046
8
          return returnRewrite(node, res, Rewrite::CTN_RPL_NON_CTN);
2047
        }
2048
      }
2049
2050
      // (str.contains x (str.++ w (str.replace x y x) z)) --->
2051
      //   (and (= w "") (= x (str.replace x y x)) (= z ""))
2052
      //
2053
      // TODO: Remove with under-/over-approximation
2054
2610
      if (node[0] == n[0] && node[0] == n[2])
2055
      {
2056
166
        Node ret;
2057
83
        if (nc2.size() > 1)
2058
        {
2059
4
          Node emp = Word::mkEmptyWord(stype);
2060
4
          NodeBuilder<> nb2(kind::AND);
2061
6
          for (const Node& n2 : nc2)
2062
          {
2063
4
            if (n2 == n)
2064
            {
2065
2
              nb2 << nm->mkNode(kind::EQUAL, node[0], node[1]);
2066
            }
2067
            else
2068
            {
2069
2
              nb2 << nm->mkNode(kind::EQUAL, emp, n2);
2070
            }
2071
          }
2072
2
          ret = nb2.constructNode();
2073
        }
2074
        else
2075
        {
2076
81
          ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
2077
        }
2078
83
        return returnRewrite(node, ret, Rewrite::CTN_REPL_SELF);
2079
      }
2080
    }
2081
  }
2082
2083
  // length entailment
2084
341646
  Node len_n1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
2085
341646
  Node len_n2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
2086
170823
  if (ArithEntail::check(len_n2, len_n1, true))
2087
  {
2088
    // len( n2 ) > len( n1 ) => contains( n1, n2 ) ---> false
2089
184
    Node ret = NodeManager::currentNM()->mkConst(false);
2090
92
    return returnRewrite(node, ret, Rewrite::CTN_LEN_INEQ);
2091
  }
2092
2093
  // multi-set reasoning
2094
  //   For example, contains( str.++( x, "b" ), str.++( "a", x ) ) ---> false
2095
  //   since the number of a's in the second argument is greater than the number
2096
  //   of a's in the first argument
2097
170731
  if (StringsEntail::checkMultisetSubset(node[0], node[1]))
2098
  {
2099
88
    Node ret = nm->mkConst(false);
2100
44
    return returnRewrite(node, ret, Rewrite::CTN_MSET_NSS);
2101
  }
2102
2103
170687
  if (ArithEntail::check(len_n2, len_n1, false))
2104
  {
2105
    // len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
2106
63080
    Node ret = node[0].eqNode(node[1]);
2107
31540
    return returnRewrite(node, ret, Rewrite::CTN_LEN_INEQ_NSTRICT);
2108
  }
2109
2110
  // splitting
2111
139147
  if (node[0].getKind() == kind::STRING_CONCAT)
2112
  {
2113
39504
    if (node[1].isConst())
2114
    {
2115
3944
      Node t = node[1];
2116
      // Below, we are looking for a constant component of node[0]
2117
      // has no overlap with node[1], which means we can split.
2118
      // Notice that if the first or last components had no
2119
      // overlap, these would have been removed by strip
2120
      // constant endpoints above.
2121
      // Hence, we consider only the inner children.
2122
4063
      for (unsigned i = 1; i < (node[0].getNumChildren() - 1); i++)
2123
      {
2124
        // constant contains
2125
2130
        if (node[0][i].isConst())
2126
        {
2127
          // if no overlap, we can split into disjunction
2128
254
          if (Word::noOverlapWith(node[0][i], node[1]))
2129
          {
2130
156
            std::vector<Node> nc0;
2131
78
            utils::getConcat(node[0], nc0);
2132
156
            std::vector<Node> spl[2];
2133
78
            spl[0].insert(spl[0].end(), nc0.begin(), nc0.begin() + i);
2134
78
            Assert(i < nc0.size() - 1);
2135
78
            spl[1].insert(spl[1].end(), nc0.begin() + i + 1, nc0.end());
2136
            Node ret = NodeManager::currentNM()->mkNode(
2137
                kind::OR,
2138
312
                NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
2139
156
                                                 utils::mkConcat(spl[0], stype),
2140
                                                 node[1]),
2141
312
                NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
2142
156
                                                 utils::mkConcat(spl[1], stype),
2143
390
                                                 node[1]));
2144
78
            return returnRewrite(node, ret, Rewrite::CTN_SPLIT);
2145
          }
2146
        }
2147
      }
2148
    }
2149
  }
2150
99643
  else if (node[0].getKind() == kind::STRING_SUBSTR)
2151
  {
2152
    // (str.contains (str.substr x n (str.len y)) y) --->
2153
    //   (= (str.substr x n (str.len y)) y)
2154
    //
2155
    // TODO: Remove with under-/over-approximation
2156
8632
    if (node[0][2] == nm->mkNode(kind::STRING_LENGTH, node[1]))
2157
    {
2158
16
      Node ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
2159
8
      return returnRewrite(node, ret, Rewrite::CTN_SUBSTR);
2160
    }
2161
  }
2162
91011
  else if (node[0].getKind() == kind::STRING_STRREPL)
2163
  {
2164
1360
    if (node[1].isConst() && node[0][1].isConst() && node[0][2].isConst())
2165
    {
2166
296
      if (Word::noOverlapWith(node[1], node[0][1])
2167
296
          && Word::noOverlapWith(node[1], node[0][2]))
2168
      {
2169
        // (str.contains (str.replace x c1 c2) c3) ---> (str.contains x c3)
2170
        // if there is no overlap between c1 and c3 and none between c2 and c3
2171
4
        Node ret = nm->mkNode(STRING_STRCTN, node[0][0], node[1]);
2172
2
        return returnRewrite(node, ret, Rewrite::CTN_REPL_CNSTS_TO_CTN);
2173
      }
2174
    }
2175
2176
1358
    if (node[0][0] == node[0][2])
2177
    {
2178
      // (str.contains (str.replace x y x) y) ---> (str.contains x y)
2179
194
      if (node[0][1] == node[1])
2180
      {
2181
12
        Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
2182
6
        return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN);
2183
      }
2184
2185
      // (str.contains (str.replace x y x) z) ---> (str.contains x z)
2186
      // if (str.len z) <= 1
2187
188
      if (StringsEntail::checkLengthOne(node[1]))
2188
      {
2189
24
        Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
2190
12
        return returnRewrite(node, ret, Rewrite::CTN_REPL_LEN_ONE_TO_CTN);
2191
      }
2192
    }
2193
2194
    // (str.contains (str.replace x y z) z) --->
2195
    //   (or (str.contains x y) (str.contains x z))
2196
1340
    if (node[0][2] == node[1])
2197
    {
2198
      Node ret = nm->mkNode(OR,
2199
136
                            nm->mkNode(STRING_STRCTN, node[0][0], node[0][1]),
2200
272
                            nm->mkNode(STRING_STRCTN, node[0][0], node[0][2]));
2201
68
      return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN_DISJ);
2202
    }
2203
2204
    // (str.contains (str.replace x y z) w) --->
2205
    //   (str.contains (str.replace x y "") w)
2206
    // if (str.contains z w) ---> false and (str.len w) = 1
2207
1272
    if (StringsEntail::checkLengthOne(node[1]))
2208
    {
2209
264
      Node ctn = d_stringsEntail.checkContains(node[0][2], node[1]);
2210
150
      if (!ctn.isNull() && !ctn.getConst<bool>())
2211
      {
2212
72
        Node empty = Word::mkEmptyWord(stype);
2213
        Node ret = nm->mkNode(
2214
            kind::STRING_STRCTN,
2215
72
            nm->mkNode(kind::STRING_STRREPL, node[0][0], node[0][1], empty),
2216
144
            node[1]);
2217
36
        return returnRewrite(node, ret, Rewrite::CTN_REPL_SIMP_REPL);
2218
      }
2219
    }
2220
  }
2221
2222
138937
  if (node[1].getKind() == kind::STRING_STRREPL)
2223
  {
2224
    // (str.contains x (str.replace y x y)) --->
2225
    //   (str.contains x y)
2226
1403
    if (node[0] == node[1][1] && node[1][0] == node[1][2])
2227
    {
2228
12
      Node ret = nm->mkNode(kind::STRING_STRCTN, node[0], node[1][0]);
2229
6
      return returnRewrite(node, ret, Rewrite::CTN_REPL);
2230
    }
2231
2232
    // (str.contains x (str.replace "" x y)) --->
2233
    //   (= "" (str.replace "" x y))
2234
    //
2235
    // Note: Length-based reasoning is not sufficient to get this rewrite. We
2236
    // can neither show that str.len(str.replace("", x, y)) - str.len(x) >= 0
2237
    // nor str.len(x) - str.len(str.replace("", x, y)) >= 0
2238
2792
    Node emp = Word::mkEmptyWord(stype);
2239
1397
    if (node[0] == node[1][1] && node[1][0] == emp)
2240
    {
2241
4
      Node ret = nm->mkNode(kind::EQUAL, emp, node[1]);
2242
2
      return returnRewrite(node, ret, Rewrite::CTN_REPL_EMPTY);
2243
    }
2244
  }
2245
2246
138929
  return node;
2247
}
2248
2249
4353
Node SequencesRewriter::rewriteIndexof(Node node)
2250
{
2251
4353
  Assert(node.getKind() == kind::STRING_STRIDOF);
2252
4353
  NodeManager* nm = NodeManager::currentNM();
2253
2254
4353
  if (node[2].isConst() && node[2].getConst<Rational>().sgn() < 0)
2255
  {
2256
    // z<0  implies  str.indexof( x, y, z ) --> -1
2257
322
    Node negone = nm->mkConst(Rational(-1));
2258
161
    return returnRewrite(node, negone, Rewrite::IDOF_NEG);
2259
  }
2260
2261
  // the string type
2262
8384
  TypeNode stype = node[0].getType();
2263
2264
  // evaluation and simple cases
2265
8384
  std::vector<Node> children0;
2266
4192
  utils::getConcat(node[0], children0);
2267
4192
  if (children0[0].isConst() && node[1].isConst() && node[2].isConst())
2268
  {
2269
1031
    CVC4::Rational rMaxInt(CVC4::String::maxSize());
2270
872
    if (node[2].getConst<Rational>() > rMaxInt)
2271
    {
2272
      // We know that, due to limitations on the size of string constants
2273
      // in our implementation, that accessing a position greater than
2274
      // rMaxInt is guaranteed to be out of bounds.
2275
      Node negone = nm->mkConst(Rational(-1));
2276
      return returnRewrite(node, negone, Rewrite::IDOF_MAX);
2277
    }
2278
872
    Assert(node[2].getConst<Rational>().sgn() >= 0);
2279
1031
    Node s = children0[0];
2280
1031
    Node t = node[1];
2281
    uint32_t start =
2282
872
        node[2].getConst<Rational>().getNumerator().toUnsignedInt();
2283
872
    std::size_t ret = Word::find(s, t, start);
2284
872
    if (ret != std::string::npos)
2285
    {
2286
670
      Node retv = nm->mkConst(Rational(static_cast<unsigned>(ret)));
2287
335
      return returnRewrite(node, retv, Rewrite::IDOF_FIND);
2288
    }
2289
537
    else if (children0.size() == 1)
2290
    {
2291
756
      Node negone = nm->mkConst(Rational(-1));
2292
378
      return returnRewrite(node, negone, Rewrite::IDOF_NFIND);
2293
    }
2294
  }
2295
2296
3479
  if (node[0] == node[1])
2297
  {
2298
46
    if (node[2].isConst())
2299
    {
2300
16
      if (node[2].getConst<Rational>().sgn() == 0)
2301
      {
2302
        // indexof( x, x, 0 ) --> 0
2303
28
        Node zero = nm->mkConst(Rational(0));
2304
14
        return returnRewrite(node, zero, Rewrite::IDOF_EQ_CST_START);
2305
      }
2306
    }
2307
32
    if (ArithEntail::check(node[2], true))
2308
    {
2309
      // y>0  implies  indexof( x, x, y ) --> -1
2310
4
      Node negone = nm->mkConst(Rational(-1));
2311
2
      return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART);
2312
    }
2313
50
    Node emp = Word::mkEmptyWord(stype);
2314
30
    if (node[0] != emp)
2315
    {
2316
      // indexof( x, x, z ) ---> indexof( "", "", z )
2317
20
      Node ret = nm->mkNode(STRING_STRIDOF, emp, emp, node[2]);
2318
10
      return returnRewrite(node, ret, Rewrite::IDOF_EQ_NORM);
2319
    }
2320
  }
2321
2322
6906
  Node len0 = nm->mkNode(STRING_LENGTH, node[0]);
2323
6906
  Node len1 = nm->mkNode(STRING_LENGTH, node[1]);
2324
6906
  Node len0m2 = nm->mkNode(MINUS, len0, node[2]);
2325
2326
3453
  if (node[1].isConst())
2327
  {
2328
3001
    if (Word::isEmpty(node[1]))
2329
    {
2330
34
      if (ArithEntail::check(len0, node[2]) && ArithEntail::check(node[2]))
2331
      {
2332
        // len(x)>=z ^ z >=0 implies indexof( x, "", z ) ---> z
2333
6
        return returnRewrite(node, node[2], Rewrite::IDOF_EMP_IDOF);
2334
      }
2335
    }
2336
  }
2337
2338
3447
  if (ArithEntail::check(len1, len0m2, true))
2339
  {
2340
    // len(x)-z < len(y)  implies  indexof( x, y, z ) ----> -1
2341
12
    Node negone = nm->mkConst(Rational(-1));
2342
6
    return returnRewrite(node, negone, Rewrite::IDOF_LEN);
2343
  }
2344
2345
6882
  Node fstr = node[0];
2346
3441
  if (!node[2].isConst() || node[2].getConst<Rational>().sgn() != 0)
2347
  {
2348
512
    fstr = nm->mkNode(kind::STRING_SUBSTR, node[0], node[2], len0);
2349
512
    fstr = Rewriter::rewrite(fstr);
2350
  }
2351
2352
6882
  Node cmp_conr = d_stringsEntail.checkContains(fstr, node[1]);
2353
6882
  Trace("strings-rewrite-debug") << "For " << node << ", check contains("
2354
3441
                                 << fstr << ", " << node[1] << ")" << std::endl;
2355
3441
  Trace("strings-rewrite-debug") << "...got " << cmp_conr << std::endl;
2356
6882
  std::vector<Node> children1;
2357
3441
  utils::getConcat(node[1], children1);
2358
3441
  if (!cmp_conr.isNull())
2359
  {
2360
236
    if (cmp_conr.getConst<bool>())
2361
    {
2362
231
      if (node[2].isConst() && node[2].getConst<Rational>().sgn() == 0)
2363
      {
2364
        // past the first position in node[0] that contains node[1], we can drop
2365
329
        std::vector<Node> nb;
2366
329
        std::vector<Node> ne;
2367
197
        int cc = d_stringsEntail.componentContains(
2368
197
            children0, children1, nb, ne, true, 1);
2369
197
        if (cc != -1 && !ne.empty())
2370
        {
2371
          // For example:
2372
          // str.indexof(str.++(x,y,z),y,0) ---> str.indexof(str.++(x,y),y,0)
2373
98
          Node nn = utils::mkConcat(children0, stype);
2374
98
          Node ret = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
2375
49
          return returnRewrite(node, ret, Rewrite::IDOF_DEF_CTN);
2376
        }
2377
2378
        // Strip components from the beginning that are guaranteed not to match
2379
148
        if (StringsEntail::stripConstantEndpoints(
2380
                children0, children1, nb, ne, 1))
2381
        {
2382
          // str.indexof(str.++("AB", x, "C"), "C", 0) --->
2383
          // 2 + str.indexof(str.++(x, "C"), "C", 0)
2384
          Node ret = nm->mkNode(
2385
              kind::PLUS,
2386
32
              nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(nb, stype)),
2387
64
              nm->mkNode(kind::STRING_STRIDOF,
2388
32
                         utils::mkConcat(children0, stype),
2389
                         node[1],
2390
64
                         node[2]));
2391
16
          return returnRewrite(node, ret, Rewrite::IDOF_STRIP_CNST_ENDPTS);
2392
        }
2393
      }
2394
2395
      // strip symbolic length
2396
326
      Node new_len = node[2];
2397
326
      std::vector<Node> nr;
2398
166
      if (StringsEntail::stripSymbolicLength(children0, nr, 1, new_len))
2399
      {
2400
        // For example:
2401
        // z>str.len( x1 ) and str.contains( x2, y )-->true
2402
        // implies
2403
        // str.indexof( str.++( x1, x2 ), y, z ) --->
2404
        // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) )
2405
12
        Node nn = utils::mkConcat(children0, stype);
2406
        Node ret =
2407
            nm->mkNode(kind::PLUS,
2408
12
                       nm->mkNode(kind::MINUS, node[2], new_len),
2409
24
                       nm->mkNode(kind::STRING_STRIDOF, nn, node[1], new_len));
2410
6
        return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN);
2411
      }
2412
    }
2413
    else
2414
    {
2415
      // str.contains( x, y ) --> false  implies  str.indexof(x,y,z) --> -1
2416
10
      Node negone = nm->mkConst(Rational(-1));
2417
5
      return returnRewrite(node, negone, Rewrite::IDOF_NCTN);
2418
    }
2419
  }
2420
  else
2421
  {
2422
6379
    Node new_len = node[2];
2423
6379
    std::vector<Node> nr;
2424
3205
    if (StringsEntail::stripSymbolicLength(children0, nr, 1, new_len))
2425
    {
2426
      // Normalize the string before the start index.
2427
      //
2428
      // For example:
2429
      // str.indexof(str.++("ABCD", x), y, 3) --->
2430
      // str.indexof(str.++("AAAD", x), y, 3)
2431
111
      Node nodeNr = utils::mkConcat(nr, stype);
2432
111
      Node normNr = lengthPreserveRewrite(nodeNr);
2433
71
      if (normNr != nodeNr)
2434
      {
2435
62
        std::vector<Node> normNrChildren;
2436
31
        utils::getConcat(normNr, normNrChildren);
2437
62
        std::vector<Node> children(normNrChildren);
2438
31
        children.insert(children.end(), children0.begin(), children0.end());
2439
62
        Node nn = utils::mkConcat(children, stype);
2440
62
        Node res = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
2441
31
        return returnRewrite(node, res, Rewrite::IDOF_NORM_PREFIX);
2442
      }
2443
    }
2444
  }
2445
2446
3334
  if (node[2].isConst() && node[2].getConst<Rational>().sgn() == 0)
2447
  {
2448
5714
    std::vector<Node> cb;
2449
5714
    std::vector<Node> ce;
2450
2864
    if (StringsEntail::stripConstantEndpoints(children0, children1, cb, ce, -1))
2451
    {
2452
28
      Node ret = utils::mkConcat(children0, stype);
2453
14
      ret = nm->mkNode(STRING_STRIDOF, ret, node[1], node[2]);
2454
      // For example:
2455
      // str.indexof( str.++( x, "A" ), "B", 0 ) ---> str.indexof( x, "B", 0 )
2456
14
      return returnRewrite(node, ret, Rewrite::RPL_PULL_ENDPT);
2457
    }
2458
  }
2459
2460
3320
  return node;
2461
}
2462
2463
2840
Node SequencesRewriter::rewriteReplace(Node node)
2464
{
2465
2840
  Assert(node.getKind() == kind::STRING_STRREPL);
2466
2840
  NodeManager* nm = NodeManager::currentNM();
2467
2468
2840
  if (node[1].isConst() && Word::isEmpty(node[1]))
2469
  {
2470
764
    Node ret = nm->mkNode(STRING_CONCAT, node[2], node[0]);
2471
382
    return returnRewrite(node, ret, Rewrite::RPL_RPL_EMPTY);
2472
  }
2473
  // the string type
2474
4916
  TypeNode stype = node.getType();
2475
2476
4916
  std::vector<Node> children0;
2477
2458
  utils::getConcat(node[0], children0);
2478
2479
2458
  if (node[1].isConst() && children0[0].isConst())
2480
  {
2481
765
    Node s = children0[0];
2482
765
    Node t = node[1];
2483
756
    std::size_t p = Word::find(s, t);
2484
756
    if (p == std::string::npos)
2485
    {
2486
534
      if (children0.size() == 1)
2487
      {
2488
525
        return returnRewrite(node, node[0], Rewrite::RPL_CONST_NFIND);
2489
      }
2490
    }
2491
    else
2492
    {
2493
444
      Node s1 = Word::substr(s, 0, p);
2494
444
      Node s3 = Word::substr(s, p + Word::getLength(t));
2495
444
      std::vector<Node> children;
2496
222
      if (!Word::isEmpty(s1))
2497
      {
2498
49
        children.push_back(s1);
2499
      }
2500
222
      children.push_back(node[2]);
2501
222
      if (!Word::isEmpty(s3))
2502
      {
2503
81
        children.push_back(s3);
2504
      }
2505
222
      children.insert(children.end(), children0.begin() + 1, children0.end());
2506
444
      Node ret = utils::mkConcat(children, stype);
2507
222
      return returnRewrite(node, ret, Rewrite::RPL_CONST_FIND);
2508
    }
2509
  }
2510
2511
  // rewrites that apply to both replace and replaceall
2512
3422
  Node rri = rewriteReplaceInternal(node);
2513
1711
  if (!rri.isNull())
2514
  {
2515
    // printing of the rewrite managed by the call above
2516
123
    return rri;
2517
  }
2518
2519
1588
  if (node[0] == node[2])
2520
  {
2521
    // ( len( y )>=len(x) ) => str.replace( x, y, x ) ---> x
2522
394
    Node l0 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
2523
394
    Node l1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
2524
213
    if (ArithEntail::check(l1, l0))
2525
    {
2526
30
      return returnRewrite(node, node[0], Rewrite::RPL_RPL_LEN_ID);
2527
    }
2528
2529
    // (str.replace x y x) ---> (str.replace x (str.++ y1 ... yn) x)
2530
    // if 1 >= (str.len x) and (= y "") ---> (= y1 "") ... (= yn "")
2531
183
    if (StringsEntail::checkLengthOne(node[0]))
2532
    {
2533
50
      Node empty = Word::mkEmptyWord(stype);
2534
      Node rn1 = Rewriter::rewrite(
2535
50
          rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty)));
2536
26
      if (rn1 != node[1])
2537
      {
2538
50
        std::vector<Node> emptyNodes;
2539
        bool allEmptyEqs;
2540
26
        std::tie(allEmptyEqs, emptyNodes) = utils::collectEmptyEqs(rn1);
2541
2542
26
        if (allEmptyEqs)
2543
        {
2544
34
          Node nn1 = utils::mkConcat(emptyNodes, stype);
2545
18
          if (node[1] != nn1)
2546
          {
2547
4
            Node ret = nm->mkNode(STRING_STRREPL, node[0], nn1, node[2]);
2548
2
            return returnRewrite(node, ret, Rewrite::RPL_X_Y_X_SIMP);
2549
          }
2550
        }
2551
      }
2552
    }
2553
  }
2554
2555
3112
  std::vector<Node> children1;
2556
1556
  utils::getConcat(node[1], children1);
2557
2558
  // check if contains definitely does (or does not) hold
2559
3112
  Node cmp_con = nm->mkNode(kind::STRING_STRCTN, node[0], node[1]);
2560
3112
  Node cmp_conr = Rewriter::rewrite(cmp_con);
2561
1556
  if (cmp_conr.isConst())
2562
  {
2563
167
    if (cmp_conr.getConst<bool>())
2564
    {
2565
      // component-wise containment
2566
273
      std::vector<Node> cb;
2567
273
      std::vector<Node> ce;
2568
157
      int cc = d_stringsEntail.componentContains(
2569
157
          children0, children1, cb, ce, true, 1);
2570
157
      if (cc != -1)
2571
      {
2572
101
        if (cc == 0 && children0[0] == children1[0])
2573
        {
2574
          // definitely a prefix, can do the replace
2575
          // for example,
2576
          //   str.replace( str.++( x, "ab" ), str.++( x, "a" ), y )  --->
2577
          //   str.++( y, "b" )
2578
52
          std::vector<Node> cres;
2579
26
          cres.push_back(node[2]);
2580
26
          cres.insert(cres.end(), ce.begin(), ce.end());
2581
52
          Node ret = utils::mkConcat(cres, stype);
2582
26
          return returnRewrite(node, ret, Rewrite::RPL_CCTN_RPL);
2583
        }
2584
75
        else if (!ce.empty())
2585
        {
2586
          // we can pull remainder past first definite containment
2587
          // for example,
2588
          //   str.replace( str.++( x, "ab" ), "a", y ) --->
2589
          //   str.++( str.replace( str.++( x, "a" ), "a", y ), "b" )
2590
          // this is independent of whether the second argument may be empty
2591
30
          std::vector<Node> scc;
2592
45
          scc.push_back(NodeManager::currentNM()->mkNode(
2593
              kind::STRING_STRREPL,
2594
30
              utils::mkConcat(children0, stype),
2595
              node[1],
2596
              node[2]));
2597
15
          scc.insert(scc.end(), ce.begin(), ce.end());
2598
30
          Node ret = utils::mkConcat(scc, stype);
2599
15
          return returnRewrite(node, ret, Rewrite::RPL_CCTN);
2600
        }
2601
      }
2602
    }
2603
    else
2604
    {
2605
      // ~contains( t, s ) => ( replace( t, s, r ) ----> t )
2606
10
      return returnRewrite(node, node[0], Rewrite::RPL_NCTN);
2607
    }
2608
  }
2609
1389
  else if (cmp_conr.getKind() == kind::EQUAL || cmp_conr.getKind() == kind::AND)
2610
  {
2611
    // Rewriting the str.contains may return equalities of the form (= x "").
2612
    // In that case, we can substitute the variables appearing in those
2613
    // equalities with the empty string in the third argument of the
2614
    // str.replace. For example:
2615
    //
2616
    // (str.replace x (str.++ x y) y) --> (str.replace x (str.++ x y) "")
2617
    //
2618
    // This can be done because str.replace changes x iff (str.++ x y) is in x
2619
    // but that means that y must be empty in that case. Thus, we can
2620
    // substitute y with "" in the third argument. Note that the third argument
2621
    // does not matter when the str.replace does not apply.
2622
    //
2623
502
    Node empty = Word::mkEmptyWord(stype);
2624
2625
502
    std::vector<Node> emptyNodes;
2626
    bool allEmptyEqs;
2627
260
    std::tie(allEmptyEqs, emptyNodes) = utils::collectEmptyEqs(cmp_conr);
2628
2629
260
    if (emptyNodes.size() > 0)
2630
    {
2631
      // Perform the substitutions
2632
278
      std::vector<TNode> substs(emptyNodes.size(), TNode(empty));
2633
      Node nn2 = node[2].substitute(
2634
278
          emptyNodes.begin(), emptyNodes.end(), substs.begin(), substs.end());
2635
2636
      // If the contains rewrites to a conjunction of empty-string equalities
2637
      // and we are doing the replacement in an empty string, we can rewrite
2638
      // the string-to-replace with a concatenation of all the terms that must
2639
      // be empty:
2640
      //
2641
      // (str.replace "" y z) ---> (str.replace "" (str.++ y1 ... yn)  z)
2642
      // if (str.contains "" y) ---> (and (= y1 "") ... (= yn ""))
2643
148
      if (node[0] == empty && allEmptyEqs)
2644
      {
2645
188
        std::vector<Node> emptyNodesList(emptyNodes.begin(), emptyNodes.end());
2646
188
        Node nn1 = utils::mkConcat(emptyNodesList, stype);
2647
98
        if (nn1 != node[1] || nn2 != node[2])
2648
        {
2649
16
          Node res = nm->mkNode(kind::STRING_STRREPL, node[0], nn1, nn2);
2650
8
          return returnRewrite(node, res, Rewrite::RPL_EMP_CNTS_SUBSTS);
2651
        }
2652
      }
2653
2654
140
      if (nn2 != node[2])
2655
      {
2656
20
        Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1], nn2);
2657
10
        return returnRewrite(node, res, Rewrite::RPL_CNTS_SUBSTS);
2658
      }
2659
    }
2660
  }
2661
2662
1487
  if (cmp_conr != cmp_con)
2663
  {
2664
467
    if (StringsEntail::checkNonEmpty(node[1]))
2665
    {
2666
      // pull endpoints that can be stripped
2667
      // for example,
2668
      //   str.replace( str.++( "b", x, "b" ), "a", y ) --->
2669
      //   str.++( "b", str.replace( x, "a", y ), "b" )
2670
501
      std::vector<Node> cb;
2671
501
      std::vector<Node> ce;
2672
259
      if (StringsEntail::stripConstantEndpoints(children0, children1, cb, ce))
2673
      {
2674
34
        std::vector<Node> cc;
2675
17
        cc.insert(cc.end(), cb.begin(), cb.end());
2676
17
        cc.push_back(
2677
68
            NodeManager::currentNM()->mkNode(kind::STRING_STRREPL,
2678
34
                                             utils::mkConcat(children0, stype),
2679
                                             node[1],
2680
                                             node[2]));
2681
17
        cc.insert(cc.end(), ce.begin(), ce.end());
2682
34
        Node ret = utils::mkConcat(cc, stype);
2683
17
        return returnRewrite(node, ret, Rewrite::RPL_PULL_ENDPT);
2684
      }
2685
    }
2686
  }
2687
2688
1470
  children1.clear();
2689
1470
  utils::getConcat(node[1], children1);
2690
2940
  Node lastChild1 = children1[children1.size() - 1];
2691
1470
  if (lastChild1.getKind() == kind::STRING_SUBSTR)
2692
  {
2693
    // (str.replace x (str.++ t (str.substr y i j)) z) --->
2694
    // (str.replace x (str.++ t
2695
    //                  (str.substr y i (+ (str.len x) 1 (- (str.len t))))) z)
2696
    // if j > len(x)
2697
    //
2698
    // Reasoning: If the string to be replaced is longer than x, then it does
2699
    // not matter how much longer it is, the result is always x. Thus, it is
2700
    // fine to only look at the prefix of length len(x) + 1 - len(t).
2701
2702
100
    children1.pop_back();
2703
    // Length of the non-substr components in the second argument
2704
    Node partLen1 =
2705
192
        nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(children1, stype));
2706
192
    Node maxLen1 = nm->mkNode(kind::PLUS, partLen1, lastChild1[2]);
2707
2708
192
    Node zero = nm->mkConst(Rational(0));
2709
192
    Node one = nm->mkConst(Rational(1));
2710
192
    Node len0 = nm->mkNode(kind::STRING_LENGTH, node[0]);
2711
192
    Node len0_1 = nm->mkNode(kind::PLUS, len0, one);
2712
    // Check len(t) + j > len(x) + 1
2713
100
    if (ArithEntail::check(maxLen1, len0_1, true))
2714
    {
2715
8
      children1.push_back(nm->mkNode(
2716
          kind::STRING_SUBSTR,
2717
          lastChild1[0],
2718
          lastChild1[1],
2719
16
          nm->mkNode(
2720
16
              kind::PLUS, len0, one, nm->mkNode(kind::UMINUS, partLen1))));
2721
      Node res = nm->mkNode(kind::STRING_STRREPL,
2722
                            node[0],
2723
16
                            utils::mkConcat(children1, stype),
2724
32
                            node[2]);
2725
8
      return returnRewrite(node, res, Rewrite::REPL_SUBST_IDX);
2726
    }
2727
  }
2728
2729
1462
  if (node[0].getKind() == STRING_STRREPL)
2730
  {
2731
270
    Node x = node[0];
2732
270
    Node y = node[1];
2733
270
    Node z = node[2];
2734
140
    if (x[0] == x[2] && x[0] == y)
2735
    {
2736
      // (str.replace (str.replace y w y) y z) -->
2737
      //   (str.replace (str.replace y w z) y z)
2738
      // if (str.len w) >= (str.len z) and w != z
2739
      //
2740
      // Reasoning: There are two cases: (1) w does not appear in y and (2) w
2741
      // does appear in y.
2742
      //
2743
      // Case (1): In this case, the reasoning is trivial. The
2744
      // inner replace does not do anything, so we can just replace its third
2745
      // argument with any string.
2746
      //
2747
      // Case (2): After the inner replace, we are guaranteed to have a string
2748
      // that contains y at the index of w in the original string y. The outer
2749
      // replace then replaces that y with z, so we can short-circuit that
2750
      // replace by directly replacing w with z in the inner replace. We can
2751
      // only do that if the result of the new inner replace does not contain
2752
      // y, otherwise we end up doing two replaces that are different from the
2753
      // original expression. We enforce that by requiring that the length of w
2754
      // has to be greater or equal to the length of z and that w and z have to
2755
      // be different. This makes sure that an inner replace changes a string
2756
      // to a string that is shorter than y, making it impossible for the outer
2757
      // replace to match.
2758
86
      Node w = x[1];
2759
2760
      // (str.len w) >= (str.len z)
2761
86
      Node wlen = nm->mkNode(kind::STRING_LENGTH, w);
2762
86
      Node zlen = nm->mkNode(kind::STRING_LENGTH, z);
2763
48
      if (ArithEntail::check(wlen, zlen))
2764
      {
2765
        // w != z
2766
38
        Node wEqZ = Rewriter::rewrite(nm->mkNode(kind::EQUAL, w, z));
2767
24
        if (wEqZ.isConst() && !wEqZ.getConst<bool>())
2768
        {
2769
          Node ret = nm->mkNode(kind::STRING_STRREPL,
2770
20
                                nm->mkNode(kind::STRING_STRREPL, y, w, z),
2771
                                y,
2772
40
                                z);
2773
10
          return returnRewrite(node, ret, Rewrite::REPL_REPL_SHORT_CIRCUIT);
2774
        }
2775
      }
2776
    }
2777
  }
2778
2779
1452
  if (node[1].getKind() == STRING_STRREPL)
2780
  {
2781
38
    if (node[1][0] == node[0])
2782
    {
2783
14
      if (node[1][0] == node[1][2] && node[1][0] == node[2])
2784
      {
2785
        // str.replace( x, str.replace( x, y, x ), x ) ---> x
2786
        return returnRewrite(node, node[0], Rewrite::REPL_REPL2_INV_ID);
2787
      }
2788
14
      bool dualReplIteSuccess = false;
2789
28
      Node cmp_con2 = d_stringsEntail.checkContains(node[1][0], node[1][2]);
2790
14
      if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
2791
      {
2792
        // str.contains( x, z ) ---> false
2793
        //   implies
2794
        // str.replace( x, str.replace( x, y, z ), w ) --->
2795
        // ite( str.contains( x, y ), x, w )
2796
        dualReplIteSuccess = true;
2797
      }
2798
      else
2799
      {
2800
        // str.contains( y, z ) ---> false and str.contains( z, y ) ---> false
2801
        //   implies
2802
        // str.replace( x, str.replace( x, y, z ), w ) --->
2803
        // ite( str.contains( x, y ), x, w )
2804
14
        cmp_con2 = d_stringsEntail.checkContains(node[1][1], node[1][2]);
2805
14
        if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
2806
        {
2807
          cmp_con2 = d_stringsEntail.checkContains(node[1][2], node[1][1]);
2808
          if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
2809
          {
2810
            dualReplIteSuccess = true;
2811
          }
2812
        }
2813
      }
2814
14
      if (dualReplIteSuccess)
2815
      {
2816
        Node res = nm->mkNode(ITE,
2817
                              nm->mkNode(STRING_STRCTN, node[0], node[1][1]),
2818
                              node[0],
2819
                              node[2]);
2820
        return returnRewrite(node, res, Rewrite::REPL_DUAL_REPL_ITE);
2821
      }
2822
    }
2823
2824
38
    bool invSuccess = false;
2825
38
    if (node[1][1] == node[0])
2826
    {
2827
12
      if (node[1][0] == node[1][2])
2828
      {
2829
        // str.replace(x, str.replace(y, x, y), w) ---> str.replace(x, y, w)
2830
        invSuccess = true;
2831
      }
2832
12
      else if (node[1][1] == node[2] || node[1][0] == node[2])
2833
      {
2834
        // str.contains(y, z) ----> false and ( y == w or x == w ) implies
2835
        //   implies
2836
        // str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w)
2837
8
        Node cmp_con2 = d_stringsEntail.checkContains(node[1][0], node[1][2]);
2838
4
        invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>();
2839
      }
2840
    }
2841
    else
2842
    {
2843
      // str.contains(x, z) ----> false and str.contains(x, w) ----> false
2844
      //   implies
2845
      // str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u)
2846
52
      Node cmp_con2 = d_stringsEntail.checkContains(node[0], node[1][1]);
2847
26
      if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
2848
      {
2849
        cmp_con2 = d_stringsEntail.checkContains(node[0], node[1][2]);
2850
        invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>();
2851
      }
2852
    }
2853
38
    if (invSuccess)
2854
    {
2855
      Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1][0], node[2]);
2856
      return returnRewrite(node, res, Rewrite::REPL_REPL2_INV);
2857
    }
2858
  }
2859
1452
  if (node[2].getKind() == STRING_STRREPL)
2860
  {
2861
16
    if (node[2][1] == node[0])
2862
    {
2863
      // str.contains( z, w ) ----> false implies
2864
      // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z )
2865
24
      Node cmp_con2 = d_stringsEntail.checkContains(node[2][0], node[1]);
2866
12
      if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
2867
      {
2868
        Node res =
2869
            nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]);
2870
        return returnRewrite(node, res, Rewrite::REPL_REPL3_INV);
2871
      }
2872
    }
2873
16
    if (node[2][0] == node[1])
2874
    {
2875
4
      bool success = false;
2876
4
      if (node[2][0] == node[2][2] && node[2][1] == node[0])
2877
      {
2878
        // str.replace( x, y, str.replace( y, x, y ) ) ---> x
2879
        success = true;
2880
      }
2881
      else
2882
      {
2883
        // str.contains( x, z ) ----> false implies
2884
        // str.replace( x, y, str.replace( y, z, w ) ) ---> x
2885
4
        cmp_con = d_stringsEntail.checkContains(node[0], node[2][1]);
2886
4
        success = !cmp_con.isNull() && !cmp_con.getConst<bool>();
2887
      }
2888
4
      if (success)
2889
      {
2890
        return returnRewrite(node, node[0], Rewrite::REPL_REPL3_INV_ID);
2891
      }
2892
    }
2893
  }
2894
  // miniscope based on components that do not contribute to contains
2895
  // for example,
2896
  //   str.replace( x ++ y ++ x ++ y, "A", z ) -->
2897
  //   str.replace( x ++ y, "A", z ) ++ x ++ y
2898
  // since if "A" occurs in x ++ y ++ x ++ y, then it must occur in x ++ y.
2899
1452
  if (StringsEntail::checkLengthOne(node[1]))
2900
  {
2901
1240
    Node lastLhs;
2902
624
    unsigned lastCheckIndex = 0;
2903
636
    for (unsigned i = 1, iend = children0.size(); i < iend; i++)
2904
    {
2905
106
      unsigned checkIndex = children0.size() - i;
2906
118
      std::vector<Node> checkLhs;
2907
106
      checkLhs.insert(
2908
212
          checkLhs.end(), children0.begin(), children0.begin() + checkIndex);
2909
118
      Node lhs = utils::mkConcat(checkLhs, stype);
2910
118
      Node rhs = children0[checkIndex];
2911
118
      Node ctn = d_stringsEntail.checkContains(lhs, rhs);
2912
106
      if (!ctn.isNull() && ctn.getConst<bool>())
2913
      {
2914
12
        lastLhs = lhs;
2915
12
        lastCheckIndex = checkIndex;
2916
      }
2917
      else
2918
      {
2919
94
        break;
2920
      }
2921
    }
2922
624
    if (!lastLhs.isNull())
2923
    {
2924
16
      std::vector<Node> remc(children0.begin() + lastCheckIndex,
2925
32
                             children0.end());
2926
16
      Node rem = utils::mkConcat(remc, stype);
2927
      Node ret =
2928
          nm->mkNode(STRING_CONCAT,
2929
16
                     nm->mkNode(STRING_STRREPL, lastLhs, node[1], node[2]),
2930
32
                     rem);
2931
      // for example:
2932
      //   str.replace( x ++ x, "A", y ) ---> str.replace( x, "A", y ) ++ x
2933
      // Since we know that the first occurrence of "A" cannot be in the
2934
      // second occurrence of x. Notice this is specific to single characters
2935
      // due to complications with finds that span multiple components for
2936
      // non-characters.
2937
8
      return returnRewrite(node, ret, Rewrite::REPL_CHAR_NCONTRIB_FIND);
2938
    }
2939
  }
2940
2941
  // TODO (#1180) incorporate these?
2942
  // contains( t, s ) =>
2943
  //   replace( replace( x, t, s ), s, r ) ----> replace( x, t, r )
2944
  // contains( t, s ) =>
2945
  //   contains( replace( t, s, r ), r ) ----> true
2946
2947
1444
  return node;
2948
}
2949
2950
138
Node SequencesRewriter::rewriteReplaceAll(Node node)
2951
{
2952
138
  Assert(node.getKind() == STRING_STRREPLALL);
2953
2954
276
  TypeNode stype = node.getType();
2955
2956
138
  if (node[0].isConst() && node[1].isConst())
2957
  {
2958
52
    std::vector<Node> children;
2959
52
    Node s = node[0];
2960
52
    Node t = node[1];
2961
26
    if (Word::isEmpty(s) || Word::isEmpty(t))
2962
    {
2963
6
      return returnRewrite(node, node[0], Rewrite::REPLALL_EMPTY_FIND);
2964
    }
2965
20
    std::size_t sizeS = Word::getLength(s);
2966
20
    std::size_t sizeT = Word::getLength(t);
2967
20
    std::size_t index = 0;
2968
20
    std::size_t curr = 0;
2969
56
    do
2970
    {
2971
76
      curr = Word::find(s, t, index);
2972
76
      if (curr != std::string::npos)
2973
      {
2974
56
        if (curr > index)
2975
        {
2976
34
          children.push_back(Word::substr(s, index, curr - index));
2977
        }
2978
56
        children.push_back(node[2]);
2979
56
        index = curr + sizeT;
2980
      }
2981
      else
2982
      {
2983
20
        children.push_back(Word::substr(s, index, sizeS - index));
2984
      }
2985
76
    } while (curr != std::string::npos && curr < sizeS);
2986
    // constant evaluation
2987
40
    Node res = utils::mkConcat(children, stype);
2988
20
    return returnRewrite(node, res, Rewrite::REPLALL_CONST);
2989
  }
2990
2991
  // rewrites that apply to both replace and replaceall
2992
224
  Node rri = rewriteReplaceInternal(node);
2993
112
  if (!rri.isNull())
2994
  {
2995
    // printing of the rewrite managed by the call above
2996
4
    return rri;
2997
  }
2998
2999
108
  return node;
3000
}
3001
3002
1823
Node SequencesRewriter::rewriteReplaceInternal(Node node)
3003
{
3004
1823
  Kind nk = node.getKind();
3005
1823
  Assert(nk == STRING_STRREPL || nk == STRING_STRREPLALL);
3006
3007
1823
  if (node[1] == node[2])
3008
  {
3009
56
    return returnRewrite(node, node[0], Rewrite::RPL_ID);
3010
  }
3011
3012
1767
  if (node[0] == node[1])
3013
  {
3014
    // only holds for replaceall if non-empty
3015
91
    if (nk == STRING_STRREPL || StringsEntail::checkNonEmpty(node[1]))
3016
    {
3017
71
      return returnRewrite(node, node[2], Rewrite::RPL_REPLACE);
3018
    }
3019
  }
3020
3021
1696
  return Node::null();
3022
}
3023
3024
119
Node SequencesRewriter::rewriteReplaceRe(Node node)
3025
{
3026
119
  Assert(node.getKind() == STRING_REPLACE_RE);
3027
119
  NodeManager* nm = NodeManager::currentNM();
3028
238
  Node x = node[0];
3029
238
  Node y = node[1];
3030
238
  Node z = node[2];
3031
3032
119
  if (RegExpEntail::isConstRegExp(y))
3033
  {
3034
117
    if (x.isConst())
3035
    {
3036
      // str.replace_re("ZABCZ", re.++("A", _*, "C"), y) ---> "Z" ++ y ++ "Z"
3037
37
      std::pair<size_t, size_t> match = firstMatch(x, y);
3038
37
      if (match.first != string::npos)
3039
      {
3040
38
        String s = x.getConst<String>();
3041
        Node ret = nm->mkNode(STRING_CONCAT,
3042
38
                              nm->mkConst(s.substr(0, match.first)),
3043
                              z,
3044
76
                              nm->mkConst(s.substr(match.second)));
3045
19
        return returnRewrite(node, ret, Rewrite::REPLACE_RE_EVAL);
3046
      }
3047
      else
3048
      {
3049
18
        return returnRewrite(node, x, Rewrite::REPLACE_RE_EVAL);
3050
      }
3051
    }
3052
    // str.replace_re( x, y, z ) ---> z ++ x if "" in y ---> true
3053
156
    String emptyStr("");
3054
80
    if (RegExpEntail::testConstStringInRegExp(emptyStr, 0, y))
3055
    {
3056
8
      Node ret = nm->mkNode(STRING_CONCAT, z, x);
3057
4
      return returnRewrite(node, ret, Rewrite::REPLACE_RE_EMP_RE);
3058
    }
3059
  }
3060
78
  return node;
3061
}
3062
3063
110
Node SequencesRewriter::rewriteReplaceReAll(Node node)
3064
{
3065
110
  Assert(node.getKind() == STRING_REPLACE_RE_ALL);
3066
110
  NodeManager* nm = NodeManager::currentNM();
3067
220
  Node x = node[0];
3068
220
  Node y = node[1];
3069
220
  Node z = node[2];
3070
3071
110
  if (RegExpEntail::isConstRegExp(y))
3072
  {
3073
110
    if (x.isConst())
3074
    {
3075
      // str.replace_re_all("ZABCZAB", re.++("A", _*, "C"), y) --->
3076
      //   "Z" ++ y ++ "Z" ++ y
3077
68
      TypeNode t = x.getType();
3078
68
      Node emp = Word::mkEmptyWord(t);
3079
      Node yp = Rewriter::rewrite(
3080
68
          nm->mkNode(REGEXP_DIFF, y, nm->mkNode(STRING_TO_REGEXP, emp)));
3081
68
      std::vector<Node> res;
3082
68
      String rem = x.getConst<String>();
3083
34
      std::pair<size_t, size_t> match(0, 0);
3084
98
      while (rem.size() >= 0)
3085
      {
3086
66
        match = firstMatch(nm->mkConst(rem), yp);
3087
66
        if (match.first == string::npos)
3088
        {
3089
34
          break;
3090
        }
3091
32
        res.push_back(nm->mkConst(rem.substr(0, match.first)));
3092
32
        res.push_back(z);
3093
32
        rem = rem.substr(match.second);
3094
      }
3095
34
      res.push_back(nm->mkConst(rem));
3096
68
      Node ret = utils::mkConcat(res, t);
3097
34
      return returnRewrite(node, ret, Rewrite::REPLACE_RE_ALL_EVAL);
3098
    }
3099
  }
3100
3101
76
  return node;
3102
}
3103
3104
103
std::pair<size_t, size_t> SequencesRewriter::firstMatch(Node n, Node r)
3105
{
3106
103
  Assert(n.isConst() && n.getType().isStringLike());
3107
103
  Assert(r.getType().isRegExp());
3108
103
  NodeManager* nm = NodeManager::currentNM();
3109
3110
206
  std::vector<Node> emptyVec;
3111
206
  Node sigmaStar = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
3112
206
  Node re = nm->mkNode(REGEXP_CONCAT, r, sigmaStar);
3113
206
  String s = n.getConst<String>();
3114
3115
103
  if (s.size() == 0)
3116
  {
3117
38
    if (RegExpEntail::testConstStringInRegExp(s, 0, r))
3118
    {
3119
2
      return std::make_pair(0, 0);
3120
    }
3121
    else
3122
    {
3123
36
      return std::make_pair(string::npos, string::npos);
3124
    }
3125
  }
3126
3127
156
  for (size_t i = 0, size = s.size(); i < size; i++)
3128
  {
3129
140
    if (RegExpEntail::testConstStringInRegExp(s, i, re))
3130
    {
3131
178
      for (size_t j = i; j <= size; j++)
3132
      {
3133
307
        String substr = s.substr(i, j - i);
3134
178
        if (RegExpEntail::testConstStringInRegExp(substr, 0, r))
3135
        {
3136
49
          return std::make_pair(i, j);
3137
        }
3138
      }
3139
    }
3140
  }
3141
3142
16
  return std::make_pair(string::npos, string::npos);
3143
}
3144
3145
235
Node SequencesRewriter::rewriteStrReverse(Node node)
3146
{
3147
235
  Assert(node.getKind() == STRING_REV);
3148
235
  NodeManager* nm = NodeManager::currentNM();
3149
470
  Node x = node[0];
3150
235
  if (x.isConst())
3151
  {
3152
    // reverse the characters in the constant
3153
128
    Node retNode = Word::reverse(x);
3154
64
    return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
3155
  }
3156
171
  else if (x.getKind() == STRING_CONCAT)
3157
  {
3158
72
    std::vector<Node> children;
3159
110
    for (const Node& nc : x)
3160
    {
3161
74
      children.push_back(nm->mkNode(STRING_REV, nc));
3162
    }
3163
36
    std::reverse(children.begin(), children.end());
3164
    // rev( x1 ++ x2 ) --> rev( x2 ) ++ rev( x1 )
3165
72
    Node retNode = nm->mkNode(STRING_CONCAT, children);
3166
36
    return returnRewrite(node, retNode, Rewrite::STR_REV_MINSCOPE_CONCAT);
3167
  }
3168
135
  else if (x.getKind() == STRING_REV)
3169
  {
3170
    // rev( rev( x ) ) --> x
3171
10
    Node retNode = x[0];
3172
5
    return returnRewrite(node, retNode, Rewrite::STR_REV_IDEM);
3173
  }
3174
130
  return node;
3175
}
3176
3177
130
Node SequencesRewriter::rewritePrefixSuffix(Node n)
3178
{
3179
130
  Assert(n.getKind() == kind::STRING_PREFIX
3180
         || n.getKind() == kind::STRING_SUFFIX);
3181
130
  bool isPrefix = n.getKind() == kind::STRING_PREFIX;
3182
130
  if (n[0] == n[1])
3183
  {
3184
16
    Node ret = NodeManager::currentNM()->mkConst(true);
3185
8
    return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EQ);
3186
  }
3187
122
  if (n[0].isConst())
3188
  {
3189
52
    if (Word::isEmpty(n[0]))
3190
    {
3191
8
      Node ret = NodeManager::currentNM()->mkConst(true);
3192
4
      return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY_CONST);
3193
    }
3194
  }
3195
118
  if (n[1].isConst())
3196
  {
3197
30
    Node s = n[1];
3198
30
    size_t lenS = Word::getLength(s);
3199
30
    if (n[0].isConst())
3200
    {
3201
      Node ret = NodeManager::currentNM()->mkConst(false);
3202
      Node t = n[0];
3203
      size_t lenT = Word::getLength(t);
3204
      if (lenS >= lenT)
3205
      {
3206
        if ((isPrefix && t == Word::prefix(s, lenT))
3207
            || (!isPrefix && t == Word::suffix(s, lenT)))
3208
        {
3209
          ret = NodeManager::currentNM()->mkConst(true);
3210
        }
3211
      }
3212
      return returnRewrite(n, ret, Rewrite::SUF_PREFIX_CONST);
3213
    }
3214
30
    else if (lenS == 0)
3215
    {
3216
4
      Node ret = n[0].eqNode(n[1]);
3217
2
      return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY);
3218
    }
3219
28
    else if (lenS == 1)
3220
    {
3221
      // (str.prefix x "A") and (str.suffix x "A") are equivalent to
3222
      // (str.contains "A" x )
3223
      Node ret =
3224
56
          NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, n[1], n[0]);
3225
28
      return returnRewrite(n, ret, Rewrite::SUF_PREFIX_CTN);
3226
    }
3227
  }
3228
176
  Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]);
3229
176
  Node lent = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[1]);
3230
176
  Node val;
3231
88
  if (isPrefix)
3232
  {
3233
61
    val = NodeManager::currentNM()->mkConst(::CVC4::Rational(0));
3234
  }
3235
  else
3236
  {
3237
27
    val = NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens);
3238
  }
3239
3240
  // Check if we can turn the prefix/suffix into equalities by showing that the
3241
  // prefix/suffix is at least as long as the string
3242
176
  Node eqs = StringsEntail::inferEqsFromContains(n[1], n[0]);
3243
88
  if (!eqs.isNull())
3244
  {
3245
8
    return returnRewrite(n, eqs, Rewrite::SUF_PREFIX_TO_EQS);
3246
  }
3247
3248
  // general reduction to equality + substr
3249
  Node retNode = n[0].eqNode(
3250
160
      NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, n[1], val, lens));
3251
3252
80
  return returnRewrite(n, retNode, Rewrite::SUF_PREFIX_ELIM);
3253
}
3254
3255
75
Node SequencesRewriter::lengthPreserveRewrite(Node n)
3256
{
3257
75
  NodeManager* nm = NodeManager::currentNM();
3258
150
  Node len = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n));
3259
150
  Node res = canonicalStrForSymbolicLength(len, n.getType());
3260
150
  return res.isNull() ? n : res;
3261
}
3262
3263
87
Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype)
3264
{
3265
87
  NodeManager* nm = NodeManager::currentNM();
3266
3267
174
  Node res;
3268
87
  if (len.getKind() == CONST_RATIONAL)
3269
  {
3270
    // c -> "A" repeated c times
3271
150
    Rational ratLen = len.getConst<Rational>();
3272
75
    Assert(ratLen.getDenominator() == 1);
3273
150
    Integer intLen = ratLen.getNumerator();
3274
75
    uint32_t u = intLen.getUnsignedInt();
3275
75
    if (stype.isString())  // string-only
3276
    {
3277
75
      res = nm->mkConst(String(std::string(u, 'A')));
3278
    }
3279
    // we could do this for sequences, but we need to be careful: some
3280
    // sorts do not permit values that the solver can handle (e.g. uninterpreted
3281
    // sorts and arrays).
3282
  }
3283
12
  else if (len.getKind() == PLUS)
3284
  {
3285
    // x + y -> norm(x) + norm(y)
3286
8
    NodeBuilder<> concatBuilder(STRING_CONCAT);
3287
12
    for (const auto& n : len)
3288
    {
3289
16
      Node sn = canonicalStrForSymbolicLength(n, stype);
3290
8
      if (sn.isNull())
3291
      {
3292
        return Node::null();
3293
      }
3294
16
      std::vector<Node> snChildren;
3295
8
      utils::getConcat(sn, snChildren);
3296
8
      concatBuilder.append(snChildren);
3297
    }
3298
4
    res = concatBuilder.constructNode();
3299
  }
3300
20
  else if (len.getKind() == MULT && len.getNumChildren() == 2
3301
20
           && len[0].isConst())
3302
  {
3303
    // c * x -> norm(x) repeated c times
3304
8
    Rational ratReps = len[0].getConst<Rational>();
3305
4
    Assert(ratReps.getDenominator() == 1);
3306
8
    Integer intReps = ratReps.getNumerator();
3307
3308
8
    Node nRep = canonicalStrForSymbolicLength(len[1], stype);
3309
4
    if (nRep.isNull())
3310
    {
3311
      return Node::null();
3312
    }
3313
8
    std::vector<Node> nRepChildren;
3314
4
    utils::getConcat(nRep, nRepChildren);
3315
8
    NodeBuilder<> concatBuilder(STRING_CONCAT);
3316
12
    for (size_t i = 0, reps = intReps.getUnsignedInt(); i < reps; i++)
3317
    {
3318
8
      concatBuilder.append(nRepChildren);
3319
    }
3320
4
    res = concatBuilder.constructNode();
3321
  }
3322
4
  else if (len.getKind() == STRING_LENGTH)
3323
  {
3324
    // len(x) -> x
3325
4
    res = len[0];
3326
  }
3327
87
  return res;
3328
}
3329
3330
292
Node SequencesRewriter::rewriteSeqUnit(Node node)
3331
{
3332
292
  NodeManager* nm = NodeManager::currentNM();
3333
292
  if (node[0].isConst())
3334
  {
3335
216
    std::vector<Node> seq;
3336
108
    seq.push_back(node[0]);
3337
216
    TypeNode stype = node[0].getType();
3338
216
    Node ret = nm->mkConst(Sequence(stype, seq));
3339
108
    return returnRewrite(node, ret, Rewrite::SEQ_UNIT_EVAL);
3340
  }
3341
184
  return node;
3342
}
3343
3344
159034
Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r)
3345
{
3346
318068
  Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << r
3347
159034
                           << "." << std::endl;
3348
3349
159034
  NodeManager* nm = NodeManager::currentNM();
3350
3351
159034
  if (d_statistics != nullptr)
3352
  {
3353
158952
    (*d_statistics) << r;
3354
  }
3355
3356
  // standard post-processing
3357
  // We rewrite (string) equalities immediately here. This allows us to forego
3358
  // the standard invariant on equality rewrites (that s=t must rewrite to one
3359
  // of { s=t, t=s, true, false } ).
3360
159034
  Kind retk = ret.getKind();
3361
159034
  if (retk == OR || retk == AND)
3362
  {
3363
15362
    std::vector<Node> children;
3364
7681
    bool childChanged = false;
3365
26602
    for (const Node& cret : ret)
3366
    {
3367
37842
      Node creter = cret;
3368
18921
      if (cret.getKind() == EQUAL)
3369
      {
3370
14081
        creter = rewriteEqualityExt(cret);
3371
      }
3372
4840
      else if (cret.getKind() == NOT && cret[0].getKind() == EQUAL)
3373
      {
3374
315
        creter = nm->mkNode(NOT, rewriteEqualityExt(cret[0]));
3375
      }
3376
18921
      childChanged = childChanged || cret != creter;
3377
18921
      children.push_back(creter);
3378
    }
3379
7681
    if (childChanged)
3380
    {
3381
2502
      ret = nm->mkNode(retk, children);
3382
7681
    }
3383
  }
3384
151353
  else if (retk == NOT && ret[0].getKind() == EQUAL)
3385
  {
3386
    ret = nm->mkNode(NOT, rewriteEqualityExt(ret[0]));
3387
  }
3388
151353
  else if (retk == EQUAL && node.getKind() != EQUAL)
3389
  {
3390
64248
    Trace("strings-rewrite")
3391
32124
        << "Apply extended equality rewrite on " << ret << std::endl;
3392
32124
    ret = rewriteEqualityExt(ret);
3393
  }
3394
159034
  return ret;
3395
}
3396
3397
}  // namespace strings
3398
}  // namespace theory
3399
26685
}  // namespace CVC4