GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/sequences_rewriter_white.cpp Lines: 775 775 100.0 %
Date: 2021-03-22 Branches: 2500 5352 46.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sequences_rewriter_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andres Noetzli, Andrew Reynolds
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 Unit tests for the strings/sequences rewriter
13
 **
14
 ** Unit tests for the strings/sequences rewriter.
15
 **/
16
17
#include <iostream>
18
#include <memory>
19
#include <vector>
20
21
#include "expr/node.h"
22
#include "expr/node_manager.h"
23
#include "test_smt.h"
24
#include "theory/quantifiers/extended_rewrite.h"
25
#include "theory/rewriter.h"
26
#include "theory/strings/arith_entail.h"
27
#include "theory/strings/sequences_rewriter.h"
28
#include "theory/strings/strings_entail.h"
29
#include "theory/strings/strings_rewriter.h"
30
31
namespace CVC4 {
32
33
using namespace theory;
34
using namespace theory::quantifiers;
35
using namespace theory::strings;
36
37
namespace test {
38
39
68
class TestTheoryWhiteSequencesRewriter : public TestSmt
40
{
41
 protected:
42
34
  void SetUp() override
43
  {
44
34
    TestSmt::SetUp();
45
68
    Options opts;
46
34
    d_rewriter.reset(new ExtendedRewriter(true));
47
34
  }
48
49
  std::unique_ptr<ExtendedRewriter> d_rewriter;
50
51
4
  void inNormalForm(Node t)
52
  {
53
8
    Node res_t = d_rewriter->extendedRewrite(t);
54
55
4
    std::cout << std::endl;
56
4
    std::cout << t << " ---> " << res_t << std::endl;
57
4
    ASSERT_EQ(t, res_t);
58
  }
59
60
182
  void sameNormalForm(Node t1, Node t2)
61
  {
62
364
    Node res_t1 = d_rewriter->extendedRewrite(t1);
63
364
    Node res_t2 = d_rewriter->extendedRewrite(t2);
64
65
182
    std::cout << std::endl;
66
182
    std::cout << t1 << " ---> " << res_t1 << std::endl;
67
182
    std::cout << t2 << " ---> " << res_t2 << std::endl;
68
182
    ASSERT_EQ(res_t1, res_t2);
69
  }
70
71
16
  void differentNormalForms(Node t1, Node t2)
72
  {
73
32
    Node res_t1 = d_rewriter->extendedRewrite(t1);
74
32
    Node res_t2 = d_rewriter->extendedRewrite(t2);
75
76
16
    std::cout << std::endl;
77
16
    std::cout << t1 << " ---> " << res_t1 << std::endl;
78
16
    std::cout << t2 << " ---> " << res_t2 << std::endl;
79
16
    ASSERT_NE(res_t1, res_t2);
80
  }
81
};
82
83
26
TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_length_one)
84
{
85
4
  TypeNode intType = d_nodeManager->integerType();
86
4
  TypeNode strType = d_nodeManager->stringType();
87
88
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
89
4
  Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD"));
90
4
  Node aaad = d_nodeManager->mkConst(::CVC4::String("AAAD"));
91
4
  Node b = d_nodeManager->mkConst(::CVC4::String("B"));
92
4
  Node x = d_nodeManager->mkVar("x", strType);
93
4
  Node y = d_nodeManager->mkVar("y", strType);
94
4
  Node negOne = d_nodeManager->mkConst(Rational(-1));
95
4
  Node zero = d_nodeManager->mkConst(Rational(0));
96
4
  Node one = d_nodeManager->mkConst(Rational(1));
97
4
  Node two = d_nodeManager->mkConst(Rational(2));
98
4
  Node three = d_nodeManager->mkConst(Rational(3));
99
4
  Node i = d_nodeManager->mkVar("i", intType);
100
101
2
  ASSERT_TRUE(StringsEntail::checkLengthOne(a));
102
2
  ASSERT_TRUE(StringsEntail::checkLengthOne(a, true));
103
104
4
  Node substr = d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, one);
105
2
  ASSERT_TRUE(StringsEntail::checkLengthOne(substr));
106
2
  ASSERT_FALSE(StringsEntail::checkLengthOne(substr, true));
107
108
2
  substr =
109
8
      d_nodeManager->mkNode(kind::STRING_SUBSTR,
110
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, a, x),
111
                            zero,
112
                            one);
113
2
  ASSERT_TRUE(StringsEntail::checkLengthOne(substr));
114
2
  ASSERT_TRUE(StringsEntail::checkLengthOne(substr, true));
115
116
2
  substr = d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, two);
117
2
  ASSERT_FALSE(StringsEntail::checkLengthOne(substr));
118
2
  ASSERT_FALSE(StringsEntail::checkLengthOne(substr, true));
119
}
120
121
26
TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_arith)
122
{
123
4
  TypeNode intType = d_nodeManager->integerType();
124
4
  TypeNode strType = d_nodeManager->stringType();
125
126
4
  Node z = d_nodeManager->mkVar("z", strType);
127
4
  Node n = d_nodeManager->mkVar("n", intType);
128
4
  Node one = d_nodeManager->mkConst(Rational(1));
129
130
  // 1 >= (str.len (str.substr z n 1)) ---> true
131
  Node substr_z = d_nodeManager->mkNode(
132
      kind::STRING_LENGTH,
133
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, z, n, one));
134
2
  ASSERT_TRUE(ArithEntail::check(one, substr_z));
135
136
  // (str.len (str.substr z n 1)) >= 1 ---> false
137
2
  ASSERT_FALSE(ArithEntail::check(substr_z, one));
138
}
139
140
26
TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption)
141
{
142
4
  TypeNode intType = d_nodeManager->integerType();
143
4
  TypeNode strType = d_nodeManager->stringType();
144
145
4
  Node x = d_nodeManager->mkVar("x", intType);
146
4
  Node y = d_nodeManager->mkVar("y", strType);
147
4
  Node z = d_nodeManager->mkVar("z", intType);
148
149
4
  Node zero = d_nodeManager->mkConst(Rational(0));
150
4
  Node one = d_nodeManager->mkConst(Rational(1));
151
152
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
153
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
154
155
4
  Node slen_y = d_nodeManager->mkNode(kind::STRING_LENGTH, y);
156
4
  Node x_plus_slen_y = d_nodeManager->mkNode(kind::PLUS, x, slen_y);
157
  Node x_plus_slen_y_eq_zero = Rewriter::rewrite(
158
4
      d_nodeManager->mkNode(kind::EQUAL, x_plus_slen_y, zero));
159
160
  // x + (str.len y) = 0 |= 0 >= x --> true
161
2
  ASSERT_TRUE(
162
2
      ArithEntail::checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, false));
163
164
  // x + (str.len y) = 0 |= 0 > x --> false
165
2
  ASSERT_FALSE(
166
2
      ArithEntail::checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, true));
167
168
8
  Node x_plus_slen_y_plus_z_eq_zero = Rewriter::rewrite(d_nodeManager->mkNode(
169
8
      kind::EQUAL, d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, z), zero));
170
171
  // x + (str.len y) + z = 0 |= 0 > x --> false
172
2
  ASSERT_FALSE(ArithEntail::checkWithAssumption(
173
2
      x_plus_slen_y_plus_z_eq_zero, zero, x, true));
174
175
  Node x_plus_slen_y_plus_slen_y_eq_zero =
176
8
      Rewriter::rewrite(d_nodeManager->mkNode(
177
          kind::EQUAL,
178
4
          d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, slen_y),
179
4
          zero));
180
181
  // x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true
182
2
  ASSERT_TRUE(ArithEntail::checkWithAssumption(
183
2
      x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false));
184
185
4
  Node five = d_nodeManager->mkConst(Rational(5));
186
4
  Node six = d_nodeManager->mkConst(Rational(6));
187
4
  Node x_plus_five = d_nodeManager->mkNode(kind::PLUS, x, five);
188
  Node x_plus_five_lt_six =
189
4
      Rewriter::rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six));
190
191
  // x + 5 < 6 |= 0 >= x --> true
192
2
  ASSERT_TRUE(
193
2
      ArithEntail::checkWithAssumption(x_plus_five_lt_six, zero, x, false));
194
195
  // x + 5 < 6 |= 0 > x --> false
196
2
  ASSERT_TRUE(
197
2
      !ArithEntail::checkWithAssumption(x_plus_five_lt_six, zero, x, true));
198
199
4
  Node neg_x = d_nodeManager->mkNode(kind::UMINUS, x);
200
  Node x_plus_five_lt_five =
201
4
      Rewriter::rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, five));
202
203
  // x + 5 < 5 |= -x >= 0 --> true
204
2
  ASSERT_TRUE(ArithEntail::checkWithAssumption(
205
2
      x_plus_five_lt_five, neg_x, zero, false));
206
207
  // x + 5 < 5 |= 0 > x --> true
208
2
  ASSERT_TRUE(
209
2
      ArithEntail::checkWithAssumption(x_plus_five_lt_five, zero, x, false));
210
211
  // 0 < x |= x >= (str.len (int.to.str x))
212
4
  Node assm = Rewriter::rewrite(d_nodeManager->mkNode(kind::LT, zero, x));
213
2
  ASSERT_TRUE(ArithEntail::checkWithAssumption(
214
      assm,
215
      x,
216
      d_nodeManager->mkNode(kind::STRING_LENGTH,
217
                            d_nodeManager->mkNode(kind::STRING_ITOS, x)),
218
2
      false));
219
}
220
221
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
222
{
223
4
  TypeNode intType = d_nodeManager->integerType();
224
4
  TypeNode strType = d_nodeManager->stringType();
225
226
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
227
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
228
4
  Node b = d_nodeManager->mkConst(::CVC4::String("B"));
229
4
  Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD"));
230
4
  Node negone = d_nodeManager->mkConst(Rational(-1));
231
4
  Node zero = d_nodeManager->mkConst(Rational(0));
232
4
  Node one = d_nodeManager->mkConst(Rational(1));
233
4
  Node two = d_nodeManager->mkConst(Rational(2));
234
4
  Node three = d_nodeManager->mkConst(Rational(3));
235
236
4
  Node s = d_nodeManager->mkVar("s", strType);
237
4
  Node s2 = d_nodeManager->mkVar("s2", strType);
238
4
  Node x = d_nodeManager->mkVar("x", intType);
239
4
  Node y = d_nodeManager->mkVar("y", intType);
240
241
  // (str.substr "A" x x) --> ""
242
4
  Node n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, x);
243
4
  Node res = StringsRewriter(nullptr).rewriteSubstr(n);
244
2
  ASSERT_EQ(res, empty);
245
246
  // (str.substr "A" (+ x 1) x) -> ""
247
6
  n = d_nodeManager->mkNode(
248
      kind::STRING_SUBSTR,
249
      a,
250
4
      d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))),
251
      x);
252
2
  res = StringsRewriter(nullptr).rewriteSubstr(n);
253
2
  ASSERT_EQ(res, empty);
254
255
  // (str.substr "A" (+ x (str.len s2)) x) -> ""
256
6
  n = d_nodeManager->mkNode(
257
      kind::STRING_SUBSTR,
258
      a,
259
6
      d_nodeManager->mkNode(
260
4
          kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)),
261
      x);
262
2
  res = StringsRewriter(nullptr).rewriteSubstr(n);
263
2
  ASSERT_EQ(res, empty);
264
265
  // (str.substr "A" x y) -> (str.substr "A" x y)
266
2
  n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, y);
267
2
  res = StringsRewriter(nullptr).rewriteSubstr(n);
268
2
  ASSERT_EQ(res, n);
269
270
  // (str.substr "ABCD" (+ x 3) x) -> ""
271
6
  n = d_nodeManager->mkNode(kind::STRING_SUBSTR,
272
                            abcd,
273
4
                            d_nodeManager->mkNode(kind::PLUS, x, three),
274
                            x);
275
2
  res = StringsRewriter(nullptr).rewriteSubstr(n);
276
2
  ASSERT_EQ(res, empty);
277
278
  // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
279
6
  n = d_nodeManager->mkNode(
280
4
      kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x);
281
2
  res = StringsRewriter(nullptr).rewriteSubstr(n);
282
2
  ASSERT_EQ(res, n);
283
284
  // (str.substr (str.substr s x x) x x) -> ""
285
6
  n = d_nodeManager->mkNode(kind::STRING_SUBSTR,
286
4
                            d_nodeManager->mkNode(kind::STRING_SUBSTR, s, x, x),
287
                            x,
288
                            x);
289
2
  sameNormalForm(n, empty);
290
291
  // Same normal form for:
292
  //
293
  // (str.substr (str.replace "" s "B") x x)
294
  //
295
  // (str.replace "" s (str.substr "B" x x)))
296
  Node lhs = d_nodeManager->mkNode(
297
      kind::STRING_SUBSTR,
298
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, empty, s, b),
299
      x,
300
8
      x);
301
  Node rhs = d_nodeManager->mkNode(
302
      kind::STRING_STRREPL,
303
      empty,
304
      s,
305
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, b, x, x));
306
2
  sameNormalForm(lhs, rhs);
307
308
  // Same normal form:
309
  //
310
  // (str.substr (str.replace s "A" "B") 0 x)
311
  //
312
  // (str.replace (str.substr s 0 x) "A" "B")
313
  Node substr_repl = d_nodeManager->mkNode(
314
      kind::STRING_SUBSTR,
315
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, s, a, b),
316
      zero,
317
8
      x);
318
  Node repl_substr = d_nodeManager->mkNode(
319
      kind::STRING_STRREPL,
320
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, s, zero, x),
321
      a,
322
8
      b);
323
2
  sameNormalForm(substr_repl, repl_substr);
324
325
  // Same normal form:
326
  //
327
  // (str.substr (str.replace s (str.substr (str.++ s2 "A") 0 1) "B") 0 x)
328
  //
329
  // (str.replace (str.substr s 0 x) (str.substr (str.++ s2 "A") 0 1) "B")
330
  Node substr_y =
331
      d_nodeManager->mkNode(kind::STRING_SUBSTR,
332
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, s2, a),
333
                            zero,
334
8
                            one);
335
6
  substr_repl = d_nodeManager->mkNode(
336
      kind::STRING_SUBSTR,
337
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, s, substr_y, b),
338
      zero,
339
      x);
340
6
  repl_substr = d_nodeManager->mkNode(
341
      kind::STRING_STRREPL,
342
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, s, zero, x),
343
      substr_y,
344
      b);
345
2
  sameNormalForm(substr_repl, repl_substr);
346
347
  // (str.substr (str.int.to.str x) x x) ---> empty
348
  Node substr_itos = d_nodeManager->mkNode(
349
4
      kind::STRING_SUBSTR, d_nodeManager->mkNode(kind::STRING_ITOS, x), x, x);
350
2
  sameNormalForm(substr_itos, empty);
351
352
  // (str.substr s (* (- 1) (str.len s)) 1) ---> empty
353
  Node substr = d_nodeManager->mkNode(
354
      kind::STRING_SUBSTR,
355
      s,
356
6
      d_nodeManager->mkNode(
357
4
          kind::MULT, negone, d_nodeManager->mkNode(kind::STRING_LENGTH, s)),
358
8
      one);
359
2
  sameNormalForm(substr, empty);
360
}
361
362
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat)
363
{
364
4
  TypeNode intType = d_nodeManager->integerType();
365
4
  TypeNode strType = d_nodeManager->stringType();
366
367
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
368
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
369
4
  Node zero = d_nodeManager->mkConst(Rational(0));
370
4
  Node three = d_nodeManager->mkConst(Rational(3));
371
372
4
  Node i = d_nodeManager->mkVar("i", intType);
373
4
  Node s = d_nodeManager->mkVar("s", strType);
374
4
  Node x = d_nodeManager->mkVar("x", strType);
375
4
  Node y = d_nodeManager->mkVar("y", strType);
376
377
  // Same normal form for:
378
  //
379
  // (str.++ (str.replace "A" x "") "A")
380
  //
381
  // (str.++ "A" (str.replace "A" x ""))
382
4
  Node repl_a_x_e = d_nodeManager->mkNode(kind::STRING_STRREPL, a, x, empty);
383
4
  Node repl_a = d_nodeManager->mkNode(kind::STRING_CONCAT, repl_a_x_e, a);
384
4
  Node a_repl = d_nodeManager->mkNode(kind::STRING_CONCAT, a, repl_a_x_e);
385
2
  sameNormalForm(repl_a, a_repl);
386
387
  // Same normal form for:
388
  //
389
  // (str.++ y (str.replace "" x (str.substr y 0 3)) (str.substr y 0 3) "A"
390
  // (str.substr y 0 3))
391
  //
392
  // (str.++ y (str.substr y 0 3) (str.replace "" x (str.substr y 0 3)) "A"
393
  // (str.substr y 0 3))
394
4
  Node z = d_nodeManager->mkNode(kind::STRING_SUBSTR, y, zero, three);
395
4
  Node repl_e_x_z = d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, z);
396
2
  repl_a = d_nodeManager->mkNode(kind::STRING_CONCAT, y, repl_e_x_z, z, a, z);
397
2
  a_repl = d_nodeManager->mkNode(kind::STRING_CONCAT, y, z, repl_e_x_z, a, z);
398
2
  sameNormalForm(repl_a, a_repl);
399
400
  // Same normal form for:
401
  //
402
  // (str.++ "A" (str.replace "A" x "") (str.substr "A" 0 i))
403
  //
404
  // (str.++ (str.substr "A" 0 i) (str.replace "A" x "") "A")
405
4
  Node substr_a = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, zero, i);
406
  Node a_substr_repl =
407
4
      d_nodeManager->mkNode(kind::STRING_CONCAT, a, substr_a, repl_a_x_e);
408
  Node substr_repl_a =
409
4
      d_nodeManager->mkNode(kind::STRING_CONCAT, substr_a, repl_a_x_e, a);
410
2
  sameNormalForm(a_substr_repl, substr_repl_a);
411
412
  // Same normal form for:
413
  //
414
  // (str.++ (str.replace "" x (str.substr "A" 0 i)) (str.substr "A" 0 i)
415
  // (str.at "A" i))
416
  //
417
  // (str.++ (str.at "A" i) (str.replace "" x (str.substr "A" 0 i)) (str.substr
418
  // "A" 0 i))
419
4
  Node charat_a = d_nodeManager->mkNode(kind::STRING_CHARAT, a, i);
420
  Node repl_e_x_s =
421
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, substr_a);
422
  Node repl_substr_a = d_nodeManager->mkNode(
423
4
      kind::STRING_CONCAT, repl_e_x_s, substr_a, charat_a);
424
  Node a_repl_substr = d_nodeManager->mkNode(
425
4
      kind::STRING_CONCAT, charat_a, repl_e_x_s, substr_a);
426
2
  sameNormalForm(repl_substr_a, a_repl_substr);
427
2
}
428
429
26
TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite)
430
{
431
4
  TypeNode intType = d_nodeManager->integerType();
432
4
  TypeNode strType = d_nodeManager->stringType();
433
434
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
435
4
  Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD"));
436
4
  Node f = d_nodeManager->mkConst(::CVC4::String("F"));
437
4
  Node gh = d_nodeManager->mkConst(::CVC4::String("GH"));
438
4
  Node ij = d_nodeManager->mkConst(::CVC4::String("IJ"));
439
440
4
  Node i = d_nodeManager->mkVar("i", intType);
441
4
  Node s = d_nodeManager->mkVar("s", strType);
442
4
  Node x = d_nodeManager->mkVar("x", strType);
443
4
  Node y = d_nodeManager->mkVar("y", strType);
444
445
  // Same length preserving rewrite for:
446
  //
447
  // (str.++ "ABCD" (str.++ x x))
448
  //
449
  // (str.++ "GH" (str.repl "GH" "IJ") "IJ")
450
  Node concat1 =
451
      d_nodeManager->mkNode(kind::STRING_CONCAT,
452
                            abcd,
453
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, x, x));
454
  Node concat2 = d_nodeManager->mkNode(
455
      kind::STRING_CONCAT,
456
      gh,
457
      x,
458
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, gh, ij),
459
8
      ij);
460
4
  Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1);
461
4
  Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2);
462
2
  ASSERT_EQ(res_concat1, res_concat2);
463
}
464
465
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf)
466
{
467
4
  TypeNode intType = d_nodeManager->integerType();
468
4
  TypeNode strType = d_nodeManager->stringType();
469
470
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
471
4
  Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD"));
472
4
  Node aaad = d_nodeManager->mkConst(::CVC4::String("AAAD"));
473
4
  Node b = d_nodeManager->mkConst(::CVC4::String("B"));
474
4
  Node c = d_nodeManager->mkConst(::CVC4::String("C"));
475
4
  Node ccc = d_nodeManager->mkConst(::CVC4::String("CCC"));
476
4
  Node x = d_nodeManager->mkVar("x", strType);
477
4
  Node y = d_nodeManager->mkVar("y", strType);
478
4
  Node negOne = d_nodeManager->mkConst(Rational(-1));
479
4
  Node zero = d_nodeManager->mkConst(Rational(0));
480
4
  Node one = d_nodeManager->mkConst(Rational(1));
481
4
  Node two = d_nodeManager->mkConst(Rational(2));
482
4
  Node three = d_nodeManager->mkConst(Rational(3));
483
4
  Node i = d_nodeManager->mkVar("i", intType);
484
4
  Node j = d_nodeManager->mkVar("j", intType);
485
486
  // Same normal form for:
487
  //
488
  // (str.to.int (str.indexof "A" x 1))
489
  //
490
  // (str.to.int (str.indexof "B" x 1))
491
4
  Node a_idof_x = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, x, two);
492
4
  Node itos_a_idof_x = d_nodeManager->mkNode(kind::STRING_ITOS, a_idof_x);
493
4
  Node b_idof_x = d_nodeManager->mkNode(kind::STRING_STRIDOF, b, x, two);
494
4
  Node itos_b_idof_x = d_nodeManager->mkNode(kind::STRING_ITOS, b_idof_x);
495
2
  sameNormalForm(itos_a_idof_x, itos_b_idof_x);
496
497
  // Same normal form for:
498
  //
499
  // (str.indexof (str.++ "ABCD" x) y 3)
500
  //
501
  // (str.indexof (str.++ "AAAD" x) y 3)
502
  Node idof_abcd =
503
      d_nodeManager->mkNode(kind::STRING_STRIDOF,
504
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, abcd, x),
505
                            y,
506
8
                            three);
507
  Node idof_aaad =
508
      d_nodeManager->mkNode(kind::STRING_STRIDOF,
509
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, aaad, x),
510
                            y,
511
8
                            three);
512
2
  sameNormalForm(idof_abcd, idof_aaad);
513
514
  // (str.indexof (str.substr x 1 i) "A" i) ---> -1
515
  Node idof_substr = d_nodeManager->mkNode(
516
      kind::STRING_STRIDOF,
517
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, i),
518
      a,
519
8
      i);
520
2
  sameNormalForm(idof_substr, negOne);
521
522
  {
523
    // Same normal form for:
524
    //
525
    // (str.indexof (str.++ "B" (str.substr "CCC" i j) x "A") "A" 0)
526
    //
527
    // (+ 1 (str.len (str.substr "CCC" i j))
528
    //    (str.indexof (str.++ "A" x y) "A" 0))
529
    Node lhs = d_nodeManager->mkNode(
530
        kind::STRING_STRIDOF,
531
8
        d_nodeManager->mkNode(
532
            kind::STRING_CONCAT,
533
            b,
534
4
            d_nodeManager->mkNode(kind::STRING_SUBSTR, ccc, i, j),
535
            x,
536
            a),
537
        a,
538
8
        zero);
539
    Node rhs = d_nodeManager->mkNode(
540
        kind::PLUS,
541
        one,
542
6
        d_nodeManager->mkNode(
543
            kind::STRING_LENGTH,
544
4
            d_nodeManager->mkNode(kind::STRING_SUBSTR, ccc, i, j)),
545
8
        d_nodeManager->mkNode(kind::STRING_STRIDOF,
546
4
                              d_nodeManager->mkNode(kind::STRING_CONCAT, x, a),
547
                              a,
548
10
                              zero));
549
2
    sameNormalForm(lhs, rhs);
550
  }
551
552
  {
553
    // Same normal form for:
554
    //
555
    // (str.indexof (str.++ "B" "C" "A" x y) "A" 0)
556
    //
557
    // (+ 2 (str.indexof (str.++ "A" x y) "A" 0))
558
    Node lhs = d_nodeManager->mkNode(
559
        kind::STRING_STRIDOF,
560
4
        d_nodeManager->mkNode(kind::STRING_CONCAT, b, c, a, x, y),
561
        a,
562
8
        zero);
563
    Node rhs = d_nodeManager->mkNode(
564
        kind::PLUS,
565
        two,
566
8
        d_nodeManager->mkNode(
567
            kind::STRING_STRIDOF,
568
4
            d_nodeManager->mkNode(kind::STRING_CONCAT, a, x, y),
569
            a,
570
6
            zero));
571
2
    sameNormalForm(lhs, rhs);
572
  }
573
2
}
574
575
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
576
{
577
4
  TypeNode intType = d_nodeManager->integerType();
578
4
  TypeNode strType = d_nodeManager->stringType();
579
580
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
581
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
582
4
  Node ab = d_nodeManager->mkConst(::CVC4::String("AB"));
583
4
  Node b = d_nodeManager->mkConst(::CVC4::String("B"));
584
4
  Node c = d_nodeManager->mkConst(::CVC4::String("C"));
585
4
  Node d = d_nodeManager->mkConst(::CVC4::String("D"));
586
4
  Node x = d_nodeManager->mkVar("x", strType);
587
4
  Node y = d_nodeManager->mkVar("y", strType);
588
4
  Node z = d_nodeManager->mkVar("z", strType);
589
4
  Node zero = d_nodeManager->mkConst(Rational(0));
590
4
  Node one = d_nodeManager->mkConst(Rational(1));
591
4
  Node n = d_nodeManager->mkVar("n", intType);
592
593
  // (str.replace (str.replace x "B" x) x "A") -->
594
  //   (str.replace (str.replace x "B" "A") x "A")
595
  Node repl_repl = d_nodeManager->mkNode(
596
      kind::STRING_STRREPL,
597
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, x),
598
      x,
599
8
      a);
600
  Node repl_repl_short = d_nodeManager->mkNode(
601
      kind::STRING_STRREPL,
602
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, a),
603
      x,
604
8
      a);
605
2
  sameNormalForm(repl_repl, repl_repl_short);
606
607
  // (str.replace "A" (str.replace "B", x, "C") "D") --> "A"
608
6
  repl_repl = d_nodeManager->mkNode(
609
      kind::STRING_STRREPL,
610
      a,
611
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, c),
612
      d);
613
2
  sameNormalForm(repl_repl, a);
614
615
  // (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A"
616
6
  repl_repl = d_nodeManager->mkNode(
617
      kind::STRING_STRREPL,
618
      a,
619
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, a),
620
      d);
621
2
  differentNormalForms(repl_repl, a);
622
623
  // Same normal form for:
624
  //
625
  // (str.replace x (str.++ x y z) y)
626
  //
627
  // (str.replace x (str.++ x y z) z)
628
4
  Node xyz = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y, z);
629
4
  Node repl_x_xyz = d_nodeManager->mkNode(kind::STRING_STRREPL, x, xyz, y);
630
4
  Node repl_x_zyx = d_nodeManager->mkNode(kind::STRING_STRREPL, x, xyz, z);
631
2
  sameNormalForm(repl_x_xyz, repl_x_zyx);
632
633
  // (str.replace "" (str.++ x x) x) --> ""
634
  Node repl_empty_xx =
635
      d_nodeManager->mkNode(kind::STRING_STRREPL,
636
                            empty,
637
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, x, x),
638
8
                            x);
639
2
  sameNormalForm(repl_empty_xx, empty);
640
641
  // (str.replace "AB" (str.++ x "A") x) --> (str.replace "AB" (str.++ x "A")
642
  // "")
643
  Node repl_ab_xa_x =
644
      d_nodeManager->mkNode(kind::STRING_STRREPL,
645
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, a, b),
646
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, x, a),
647
12
                            x);
648
  Node repl_ab_xa_e =
649
      d_nodeManager->mkNode(kind::STRING_STRREPL,
650
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, a, b),
651
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, x, a),
652
12
                            empty);
653
2
  sameNormalForm(repl_ab_xa_x, repl_ab_xa_e);
654
655
  // (str.replace "AB" (str.++ x "A") x) -/-> (str.replace "AB" (str.++ "A" x)
656
  // "")
657
  Node repl_ab_ax_e =
658
      d_nodeManager->mkNode(kind::STRING_STRREPL,
659
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, a, b),
660
4
                            d_nodeManager->mkNode(kind::STRING_CONCAT, a, x),
661
12
                            empty);
662
2
  differentNormalForms(repl_ab_ax_e, repl_ab_xa_e);
663
664
  // (str.replace "" (str.replace y x "A") y) ---> ""
665
6
  repl_repl = d_nodeManager->mkNode(
666
      kind::STRING_STRREPL,
667
      empty,
668
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, y, x, a),
669
      y);
670
2
  sameNormalForm(repl_repl, empty);
671
672
  // (str.replace "" (str.replace x y x) x) ---> ""
673
6
  repl_repl = d_nodeManager->mkNode(
674
      kind::STRING_STRREPL,
675
      empty,
676
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
677
      x);
678
2
  sameNormalForm(repl_repl, empty);
679
680
  // (str.replace "" (str.substr x 0 1) x) ---> ""
681
6
  repl_repl = d_nodeManager->mkNode(
682
      kind::STRING_STRREPL,
683
      empty,
684
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, one),
685
      x);
686
2
  sameNormalForm(repl_repl, empty);
687
688
  // Same normal form for:
689
  //
690
  // (str.replace "" (str.replace x y x) y)
691
  //
692
  // (str.replace "" x y)
693
6
  repl_repl = d_nodeManager->mkNode(
694
      kind::STRING_STRREPL,
695
      empty,
696
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
697
      y);
698
4
  Node repl = d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, y);
699
2
  sameNormalForm(repl_repl, repl);
700
701
  // Same normal form:
702
  //
703
  // (str.replace "B" (str.replace x "A" "B") "B")
704
  //
705
  // (str.replace "B" x "B"))
706
6
  repl_repl = d_nodeManager->mkNode(
707
      kind::STRING_STRREPL,
708
      b,
709
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b),
710
      b);
711
2
  repl = d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, b);
712
2
  sameNormalForm(repl_repl, repl);
713
714
  // Different normal forms for:
715
  //
716
  // (str.replace "B" (str.replace "" x "A") "B")
717
  //
718
  // (str.replace "B" x "B")
719
6
  repl_repl = d_nodeManager->mkNode(
720
      kind::STRING_STRREPL,
721
      b,
722
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, a),
723
      b);
724
2
  repl = d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, b);
725
2
  differentNormalForms(repl_repl, repl);
726
727
  {
728
    // Same normal form:
729
    //
730
    // (str.replace (str.++ "AB" x) "C" y)
731
    //
732
    // (str.++ "AB" (str.replace x "C" y))
733
    Node lhs =
734
        d_nodeManager->mkNode(kind::STRING_STRREPL,
735
4
                              d_nodeManager->mkNode(kind::STRING_CONCAT, ab, x),
736
                              c,
737
8
                              y);
738
    Node rhs = d_nodeManager->mkNode(
739
        kind::STRING_CONCAT,
740
        ab,
741
4
        d_nodeManager->mkNode(kind::STRING_STRREPL, x, c, y));
742
2
    sameNormalForm(lhs, rhs);
743
  }
744
2
}
745
746
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re)
747
{
748
4
  TypeNode intType = d_nodeManager->integerType();
749
4
  TypeNode strType = d_nodeManager->stringType();
750
751
4
  std::vector<Node> emptyVec;
752
  Node sigStar = d_nodeManager->mkNode(
753
4
      kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec));
754
4
  Node foo = d_nodeManager->mkConst(String("FOO"));
755
4
  Node a = d_nodeManager->mkConst(String("A"));
756
4
  Node b = d_nodeManager->mkConst(String("B"));
757
  Node re =
758
      d_nodeManager->mkNode(kind::REGEXP_CONCAT,
759
4
                            d_nodeManager->mkNode(kind::STRING_TO_REGEXP, a),
760
                            sigStar,
761
8
                            d_nodeManager->mkNode(kind::STRING_TO_REGEXP, b));
762
763
  // Same normal form:
764
  //
765
  // (str.replace_re
766
  //   "AZZZB"
767
  //   (re.++ (str.to_re "A") re.all (str.to_re "B"))
768
  //   "FOO")
769
  //
770
  // "FOO"
771
  {
772
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE,
773
4
                                   d_nodeManager->mkConst(String("AZZZB")),
774
                                   re,
775
8
                                   foo);
776
4
    Node res = d_nodeManager->mkConst(::CVC4::String("FOO"));
777
2
    sameNormalForm(t, res);
778
  }
779
780
  // Same normal form:
781
  //
782
  // (str.replace_re
783
  //   "ZAZZZBZZB"
784
  //   (re.++ (str.to_re "A") re.all (str.to_re "B"))
785
  //   "FOO")
786
  //
787
  // "ZFOOZZB"
788
  {
789
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE,
790
4
                                   d_nodeManager->mkConst(String("ZAZZZBZZB")),
791
                                   re,
792
8
                                   foo);
793
4
    Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZZB"));
794
2
    sameNormalForm(t, res);
795
  }
796
797
  // Same normal form:
798
  //
799
  // (str.replace_re
800
  //   "ZAZZZBZAZB"
801
  //   (re.++ (str.to_re "A") re.all (str.to_re "B"))
802
  //   "FOO")
803
  //
804
  // "ZFOOZAZB"
805
  {
806
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE,
807
4
                                   d_nodeManager->mkConst(String("ZAZZZBZAZB")),
808
                                   re,
809
8
                                   foo);
810
4
    Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZAZB"));
811
2
    sameNormalForm(t, res);
812
  }
813
814
  // Same normal form:
815
  //
816
  // (str.replace_re
817
  //   "ZZZ"
818
  //   (re.++ (str.to_re "A") re.all (str.to_re "B"))
819
  //   "FOO")
820
  //
821
  // "ZZZ"
822
  {
823
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE,
824
4
                                   d_nodeManager->mkConst(String("ZZZ")),
825
                                   re,
826
8
                                   foo);
827
4
    Node res = d_nodeManager->mkConst(::CVC4::String("ZZZ"));
828
2
    sameNormalForm(t, res);
829
  }
830
831
  // Same normal form:
832
  //
833
  // (str.replace_re
834
  //   "ZZZ"
835
  //   re.all
836
  //   "FOO")
837
  //
838
  // "FOOZZZ"
839
  {
840
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE,
841
4
                                   d_nodeManager->mkConst(String("ZZZ")),
842
                                   sigStar,
843
8
                                   foo);
844
4
    Node res = d_nodeManager->mkConst(::CVC4::String("FOOZZZ"));
845
2
    sameNormalForm(t, res);
846
  }
847
848
  // Same normal form:
849
  //
850
  // (str.replace_re
851
  //   ""
852
  //   re.all
853
  //   "FOO")
854
  //
855
  // "FOO"
856
  {
857
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE,
858
4
                                   d_nodeManager->mkConst(String("")),
859
                                   sigStar,
860
8
                                   foo);
861
4
    Node res = d_nodeManager->mkConst(::CVC4::String("FOO"));
862
2
    sameNormalForm(t, res);
863
  }
864
2
}
865
866
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all)
867
{
868
4
  TypeNode intType = d_nodeManager->integerType();
869
4
  TypeNode strType = d_nodeManager->stringType();
870
871
4
  std::vector<Node> emptyVec;
872
  Node sigStar = d_nodeManager->mkNode(
873
4
      kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec));
874
4
  Node foo = d_nodeManager->mkConst(String("FOO"));
875
4
  Node a = d_nodeManager->mkConst(String("A"));
876
4
  Node b = d_nodeManager->mkConst(String("B"));
877
  Node re =
878
      d_nodeManager->mkNode(kind::REGEXP_CONCAT,
879
4
                            d_nodeManager->mkNode(kind::STRING_TO_REGEXP, a),
880
                            sigStar,
881
8
                            d_nodeManager->mkNode(kind::STRING_TO_REGEXP, b));
882
883
  // Same normal form:
884
  //
885
  // (str.replace_re
886
  //   "AZZZB"
887
  //   (re.++ (str.to_re "A") re.all (str.to_re "B"))
888
  //   "FOO")
889
  //
890
  // "FOO"
891
  {
892
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL,
893
4
                                   d_nodeManager->mkConst(String("AZZZB")),
894
                                   re,
895
8
                                   foo);
896
4
    Node res = d_nodeManager->mkConst(::CVC4::String("FOO"));
897
2
    sameNormalForm(t, res);
898
  }
899
900
  // Same normal form:
901
  //
902
  // (str.replace_re
903
  //   "ZAZZZBZZB"
904
  //   (re.++ (str.to_re "A") re.all (str.to_re "B"))
905
  //   "FOO")
906
  //
907
  // "ZFOOZZB"
908
  {
909
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL,
910
4
                                   d_nodeManager->mkConst(String("ZAZZZBZZB")),
911
                                   re,
912
8
                                   foo);
913
4
    Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZZB"));
914
2
    sameNormalForm(t, res);
915
  }
916
917
  // Same normal form:
918
  //
919
  // (str.replace_re
920
  //   "ZAZZZBZAZB"
921
  //   (re.++ (str.to_re "A") re.all (str.to_re "B"))
922
  //   "FOO")
923
  //
924
  // "ZFOOZFOO"
925
  {
926
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL,
927
4
                                   d_nodeManager->mkConst(String("ZAZZZBZAZB")),
928
                                   re,
929
8
                                   foo);
930
4
    Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZFOO"));
931
2
    sameNormalForm(t, res);
932
  }
933
934
  // Same normal form:
935
  //
936
  // (str.replace_re
937
  //   "ZZZ"
938
  //   (re.++ (str.to_re "A") re.all (str.to_re "B"))
939
  //   "FOO")
940
  //
941
  // "ZZZ"
942
  {
943
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL,
944
4
                                   d_nodeManager->mkConst(String("ZZZ")),
945
                                   re,
946
8
                                   foo);
947
4
    Node res = d_nodeManager->mkConst(::CVC4::String("ZZZ"));
948
2
    sameNormalForm(t, res);
949
  }
950
951
  // Same normal form:
952
  //
953
  // (str.replace_re
954
  //   "ZZZ"
955
  //   re.all
956
  //   "FOO")
957
  //
958
  // "FOOFOOFOO"
959
  {
960
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL,
961
4
                                   d_nodeManager->mkConst(String("ZZZ")),
962
                                   sigStar,
963
8
                                   foo);
964
4
    Node res = d_nodeManager->mkConst(::CVC4::String("FOOFOOFOO"));
965
2
    sameNormalForm(t, res);
966
  }
967
968
  // Same normal form:
969
  //
970
  // (str.replace_re
971
  //   ""
972
  //   re.all
973
  //   "FOO")
974
  //
975
  // ""
976
  {
977
    Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL,
978
4
                                   d_nodeManager->mkConst(String("")),
979
                                   sigStar,
980
8
                                   foo);
981
4
    Node res = d_nodeManager->mkConst(::CVC4::String(""));
982
2
    sameNormalForm(t, res);
983
  }
984
2
}
985
986
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
987
{
988
4
  TypeNode intType = d_nodeManager->integerType();
989
4
  TypeNode strType = d_nodeManager->stringType();
990
991
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
992
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
993
4
  Node ab = d_nodeManager->mkConst(::CVC4::String("AB"));
994
4
  Node b = d_nodeManager->mkConst(::CVC4::String("B"));
995
4
  Node c = d_nodeManager->mkConst(::CVC4::String("C"));
996
4
  Node e = d_nodeManager->mkConst(::CVC4::String("E"));
997
4
  Node h = d_nodeManager->mkConst(::CVC4::String("H"));
998
4
  Node j = d_nodeManager->mkConst(::CVC4::String("J"));
999
4
  Node p = d_nodeManager->mkConst(::CVC4::String("P"));
1000
4
  Node abc = d_nodeManager->mkConst(::CVC4::String("ABC"));
1001
4
  Node def = d_nodeManager->mkConst(::CVC4::String("DEF"));
1002
4
  Node ghi = d_nodeManager->mkConst(::CVC4::String("GHI"));
1003
4
  Node x = d_nodeManager->mkVar("x", strType);
1004
4
  Node y = d_nodeManager->mkVar("y", strType);
1005
4
  Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y);
1006
4
  Node yx = d_nodeManager->mkNode(kind::STRING_CONCAT, y, x);
1007
4
  Node z = d_nodeManager->mkVar("z", strType);
1008
4
  Node n = d_nodeManager->mkVar("n", intType);
1009
4
  Node m = d_nodeManager->mkVar("m", intType);
1010
4
  Node one = d_nodeManager->mkConst(Rational(1));
1011
4
  Node two = d_nodeManager->mkConst(Rational(2));
1012
4
  Node three = d_nodeManager->mkConst(Rational(3));
1013
4
  Node four = d_nodeManager->mkConst(Rational(4));
1014
4
  Node t = d_nodeManager->mkConst(true);
1015
4
  Node f = d_nodeManager->mkConst(false);
1016
1017
  // Same normal form for:
1018
  //
1019
  // (str.replace "A" (str.substr x 1 3) y z)
1020
  //
1021
  // (str.replace "A" (str.substr x 1 4) y z)
1022
  Node substr_3 = d_nodeManager->mkNode(
1023
      kind::STRING_STRREPL,
1024
      a,
1025
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three),
1026
8
      z);
1027
  Node substr_4 = d_nodeManager->mkNode(
1028
      kind::STRING_STRREPL,
1029
      a,
1030
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, four),
1031
8
      z);
1032
2
  sameNormalForm(substr_3, substr_4);
1033
1034
  // Same normal form for:
1035
  //
1036
  // (str.replace "A" (str.++ y (str.substr x 1 3)) y z)
1037
  //
1038
  // (str.replace "A" (str.++ y (str.substr x 1 4)) y z)
1039
  Node concat_substr_3 = d_nodeManager->mkNode(
1040
      kind::STRING_STRREPL,
1041
      a,
1042
6
      d_nodeManager->mkNode(
1043
          kind::STRING_CONCAT,
1044
          y,
1045
4
          d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three)),
1046
8
      z);
1047
  Node concat_substr_4 = d_nodeManager->mkNode(
1048
      kind::STRING_STRREPL,
1049
      a,
1050
6
      d_nodeManager->mkNode(
1051
          kind::STRING_CONCAT,
1052
          y,
1053
4
          d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, four)),
1054
8
      z);
1055
2
  sameNormalForm(concat_substr_3, concat_substr_4);
1056
1057
  // (str.contains "A" (str.++ a (str.replace "B", x, "C")) --> false
1058
  Node ctn_repl = d_nodeManager->mkNode(
1059
      kind::STRING_STRCTN,
1060
      a,
1061
6
      d_nodeManager->mkNode(
1062
          kind::STRING_CONCAT,
1063
          a,
1064
10
          d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, c)));
1065
2
  sameNormalForm(ctn_repl, f);
1066
1067
  // (str.contains x (str.++ x x)) --> (= x "")
1068
  Node x_cnts_x_x = d_nodeManager->mkNode(
1069
4
      kind::STRING_STRCTN, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, x));
1070
2
  sameNormalForm(x_cnts_x_x, d_nodeManager->mkNode(kind::EQUAL, x, empty));
1071
1072
  // Same normal form for:
1073
  //
1074
  // (str.contains (str.++ y x) (str.++ x z y))
1075
  //
1076
  // (and (str.contains (str.++ y x) (str.++ x y)) (= z ""))
1077
  Node yx_cnts_xzy = d_nodeManager->mkNode(
1078
      kind::STRING_STRCTN,
1079
      yx,
1080
4
      d_nodeManager->mkNode(kind::STRING_CONCAT, x, z, y));
1081
  Node yx_cnts_xy =
1082
      d_nodeManager->mkNode(kind::AND,
1083
4
                            d_nodeManager->mkNode(kind::EQUAL, z, empty),
1084
8
                            d_nodeManager->mkNode(kind::STRING_STRCTN, yx, xy));
1085
2
  sameNormalForm(yx_cnts_xzy, yx_cnts_xy);
1086
1087
  // Same normal form for:
1088
  //
1089
  // (str.contains (str.substr x n (str.len y)) y)
1090
  //
1091
  // (= (str.substr x n (str.len y)) y)
1092
  Node ctn_substr = d_nodeManager->mkNode(
1093
      kind::STRING_STRCTN,
1094
6
      d_nodeManager->mkNode(kind::STRING_SUBSTR,
1095
                            x,
1096
                            n,
1097
4
                            d_nodeManager->mkNode(kind::STRING_LENGTH, y)),
1098
8
      y);
1099
  Node substr_eq = d_nodeManager->mkNode(
1100
      kind::EQUAL,
1101
6
      d_nodeManager->mkNode(kind::STRING_SUBSTR,
1102
                            x,
1103
                            n,
1104
4
                            d_nodeManager->mkNode(kind::STRING_LENGTH, y)),
1105
8
      y);
1106
2
  sameNormalForm(ctn_substr, substr_eq);
1107
1108
  // Same normal form for:
1109
  //
1110
  // (str.contains x (str.replace y x y))
1111
  //
1112
  // (str.contains x y)
1113
  Node ctn_repl_y_x_y = d_nodeManager->mkNode(
1114
      kind::STRING_STRCTN,
1115
      x,
1116
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, y, x, y));
1117
4
  Node ctn_x_y = d_nodeManager->mkNode(kind::STRING_STRCTN, x, y);
1118
2
  sameNormalForm(ctn_repl_y_x_y, ctn_repl_y_x_y);
1119
1120
  // Same normal form for:
1121
  //
1122
  // (str.contains x (str.replace x y x))
1123
  //
1124
  // (= x (str.replace x y x))
1125
  Node ctn_repl_self = d_nodeManager->mkNode(
1126
      kind::STRING_STRCTN,
1127
      x,
1128
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x));
1129
  Node eq_repl = d_nodeManager->mkNode(
1130
4
      kind::EQUAL, x, d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x));
1131
2
  sameNormalForm(ctn_repl_self, eq_repl);
1132
1133
  // (str.contains x (str.++ "A" (str.replace x y x))) ---> false
1134
  Node ctn_repl_self_f = d_nodeManager->mkNode(
1135
      kind::STRING_STRCTN,
1136
      x,
1137
6
      d_nodeManager->mkNode(
1138
          kind::STRING_CONCAT,
1139
          a,
1140
10
          d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x)));
1141
2
  sameNormalForm(ctn_repl_self_f, f);
1142
1143
  // Same normal form for:
1144
  //
1145
  // (str.contains x (str.replace "" x y))
1146
  //
1147
  // (= "" (str.replace "" x y))
1148
  Node ctn_repl_empty = d_nodeManager->mkNode(
1149
      kind::STRING_STRCTN,
1150
      x,
1151
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, y));
1152
  Node eq_repl_empty = d_nodeManager->mkNode(
1153
      kind::EQUAL,
1154
      empty,
1155
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, y));
1156
2
  sameNormalForm(ctn_repl_empty, eq_repl_empty);
1157
1158
  // Same normal form for:
1159
  //
1160
  // (str.contains x (str.++ x y))
1161
  //
1162
  // (= "" y)
1163
  Node ctn_x_x_y = d_nodeManager->mkNode(
1164
4
      kind::STRING_STRCTN, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, y));
1165
4
  Node eq_emp_y = d_nodeManager->mkNode(kind::EQUAL, empty, y);
1166
2
  sameNormalForm(ctn_x_x_y, eq_emp_y);
1167
1168
  // Same normal form for:
1169
  //
1170
  // (str.contains (str.++ y x) (str.++ x y))
1171
  //
1172
  // (= (str.++ y x) (str.++ x y))
1173
4
  Node ctn_yxxy = d_nodeManager->mkNode(kind::STRING_STRCTN, yx, xy);
1174
4
  Node eq_yxxy = d_nodeManager->mkNode(kind::EQUAL, yx, xy);
1175
2
  sameNormalForm(ctn_yxxy, eq_yxxy);
1176
1177
  // (str.contains (str.replace x y x) x) ---> true
1178
6
  ctn_repl = d_nodeManager->mkNode(
1179
      kind::STRING_STRCTN,
1180
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
1181
      x);
1182
2
  sameNormalForm(ctn_repl, t);
1183
1184
  // (str.contains (str.replace (str.++ x y) z (str.++ y x)) x) ---> true
1185
6
  ctn_repl = d_nodeManager->mkNode(
1186
      kind::STRING_STRCTN,
1187
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, xy, z, yx),
1188
      x);
1189
2
  sameNormalForm(ctn_repl, t);
1190
1191
  // (str.contains (str.++ z (str.replace (str.++ x y) z (str.++ y x))) x)
1192
  //   ---> true
1193
6
  ctn_repl = d_nodeManager->mkNode(
1194
      kind::STRING_STRCTN,
1195
6
      d_nodeManager->mkNode(
1196
          kind::STRING_CONCAT,
1197
          z,
1198
4
          d_nodeManager->mkNode(kind::STRING_STRREPL, xy, z, yx)),
1199
      x);
1200
2
  sameNormalForm(ctn_repl, t);
1201
1202
  // Same normal form for:
1203
  //
1204
  // (str.contains (str.replace x y x) y)
1205
  //
1206
  // (str.contains x y)
1207
  Node lhs = d_nodeManager->mkNode(
1208
      kind::STRING_STRCTN,
1209
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
1210
8
      y);
1211
4
  Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, y);
1212
2
  sameNormalForm(lhs, rhs);
1213
1214
  // Same normal form for:
1215
  //
1216
  // (str.contains (str.replace x y x) "B")
1217
  //
1218
  // (str.contains x "B")
1219
6
  lhs = d_nodeManager->mkNode(
1220
      kind::STRING_STRCTN,
1221
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
1222
      b);
1223
2
  rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, b);
1224
2
  sameNormalForm(lhs, rhs);
1225
1226
  // Same normal form for:
1227
  //
1228
  // (str.contains (str.replace x y x) (str.substr z n 1))
1229
  //
1230
  // (str.contains x (str.substr z n 1))
1231
4
  Node substr_z = d_nodeManager->mkNode(kind::STRING_SUBSTR, z, n, one);
1232
6
  lhs = d_nodeManager->mkNode(
1233
      kind::STRING_STRCTN,
1234
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
1235
      substr_z);
1236
2
  rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, substr_z);
1237
2
  sameNormalForm(lhs, rhs);
1238
1239
  // Same normal form for:
1240
  //
1241
  // (str.contains (str.replace x y z) z)
1242
  //
1243
  // (str.contains (str.replace x z y) y)
1244
6
  lhs = d_nodeManager->mkNode(
1245
      kind::STRING_STRCTN,
1246
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, z),
1247
      z);
1248
6
  rhs = d_nodeManager->mkNode(
1249
      kind::STRING_STRCTN,
1250
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, z, y),
1251
      y);
1252
2
  sameNormalForm(lhs, rhs);
1253
1254
  // Same normal form for:
1255
  //
1256
  // (str.contains (str.replace x "A" "B") "A")
1257
  //
1258
  // (str.contains (str.replace x "A" "") "A")
1259
6
  lhs = d_nodeManager->mkNode(
1260
      kind::STRING_STRCTN,
1261
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b),
1262
      a);
1263
6
  rhs = d_nodeManager->mkNode(
1264
      kind::STRING_STRCTN,
1265
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, empty),
1266
      a);
1267
2
  sameNormalForm(lhs, rhs);
1268
1269
  {
1270
    // (str.contains (str.++ x "A") (str.++ "B" x)) ---> false
1271
    Node ctn =
1272
        d_nodeManager->mkNode(kind::STRING_STRCTN,
1273
4
                              d_nodeManager->mkNode(kind::STRING_CONCAT, x, a),
1274
8
                              d_nodeManager->mkNode(kind::STRING_CONCAT, b, x));
1275
2
    sameNormalForm(ctn, f);
1276
  }
1277
1278
  {
1279
    // Same normal form for:
1280
    //
1281
    // (str.contains (str.replace x "ABC" "DEF") "GHI")
1282
    //
1283
    // (str.contains x "GHI")
1284
6
    lhs = d_nodeManager->mkNode(
1285
        kind::STRING_STRCTN,
1286
4
        d_nodeManager->mkNode(kind::STRING_STRREPL, x, abc, def),
1287
        ghi);
1288
2
    rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, ghi);
1289
2
    sameNormalForm(lhs, rhs);
1290
  }
1291
1292
  {
1293
    // Different normal forms for:
1294
    //
1295
    // (str.contains (str.replace x "ABC" "DEF") "B")
1296
    //
1297
    // (str.contains x "B")
1298
6
    lhs = d_nodeManager->mkNode(
1299
        kind::STRING_STRCTN,
1300
4
        d_nodeManager->mkNode(kind::STRING_STRREPL, x, abc, def),
1301
        b);
1302
2
    rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, b);
1303
2
    differentNormalForms(lhs, rhs);
1304
  }
1305
1306
  {
1307
    // Different normal forms for:
1308
    //
1309
    // (str.contains (str.replace x "B" "DEF") "ABC")
1310
    //
1311
    // (str.contains x "ABC")
1312
6
    lhs = d_nodeManager->mkNode(
1313
        kind::STRING_STRCTN,
1314
4
        d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, def),
1315
        abc);
1316
2
    rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc);
1317
2
    differentNormalForms(lhs, rhs);
1318
  }
1319
1320
  {
1321
    // Same normal form for:
1322
    //
1323
    // (str.contains (str.++ (str.substr "DEF" n m) x) "AB")
1324
    //
1325
    // (str.contains x "AB")
1326
6
    lhs = d_nodeManager->mkNode(
1327
        kind::STRING_STRCTN,
1328
8
        d_nodeManager->mkNode(
1329
            kind::STRING_CONCAT,
1330
4
            d_nodeManager->mkNode(kind::STRING_SUBSTR, def, n, m),
1331
            x),
1332
        ab);
1333
2
    rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, ab);
1334
2
    sameNormalForm(lhs, rhs);
1335
  }
1336
1337
  {
1338
    // Same normal form for:
1339
    //
1340
    // (str.contains "ABC" (str.at x n))
1341
    //
1342
    // (or (= x "")
1343
    //     (= x "A") (= x "B") (= x "C"))
1344
4
    Node cat = d_nodeManager->mkNode(kind::STRING_CHARAT, x, n);
1345
2
    lhs = d_nodeManager->mkNode(kind::STRING_STRCTN, abc, cat);
1346
16
    rhs = d_nodeManager->mkNode(kind::OR,
1347
4
                                d_nodeManager->mkNode(kind::EQUAL, cat, empty),
1348
4
                                d_nodeManager->mkNode(kind::EQUAL, cat, a),
1349
4
                                d_nodeManager->mkNode(kind::EQUAL, cat, b),
1350
4
                                d_nodeManager->mkNode(kind::EQUAL, cat, c));
1351
2
    sameNormalForm(lhs, rhs);
1352
  }
1353
2
}
1354
1355
26
TEST_F(TestTheoryWhiteSequencesRewriter, infer_eqs_from_contains)
1356
{
1357
4
  TypeNode strType = d_nodeManager->stringType();
1358
1359
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
1360
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
1361
4
  Node b = d_nodeManager->mkConst(::CVC4::String("B"));
1362
4
  Node x = d_nodeManager->mkVar("x", strType);
1363
4
  Node y = d_nodeManager->mkVar("y", strType);
1364
4
  Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y);
1365
4
  Node f = d_nodeManager->mkConst(false);
1366
1367
  // inferEqsFromContains("", (str.++ x y)) returns something equivalent to
1368
  // (= "" y)
1369
  Node empty_x_y =
1370
      d_nodeManager->mkNode(kind::AND,
1371
4
                            d_nodeManager->mkNode(kind::EQUAL, empty, x),
1372
8
                            d_nodeManager->mkNode(kind::EQUAL, empty, y));
1373
2
  sameNormalForm(StringsEntail::inferEqsFromContains(empty, xy), empty_x_y);
1374
1375
  // inferEqsFromContains(x, (str.++ x y)) returns false
1376
4
  Node bxya = d_nodeManager->mkNode(kind::STRING_CONCAT, b, y, x, a);
1377
2
  sameNormalForm(StringsEntail::inferEqsFromContains(x, bxya), f);
1378
1379
  // inferEqsFromContains(x, y) returns null
1380
4
  Node n = StringsEntail::inferEqsFromContains(x, y);
1381
2
  ASSERT_TRUE(n.isNull());
1382
1383
  // inferEqsFromContains(x, x) returns something equivalent to (= x x)
1384
4
  Node eq_x_x = d_nodeManager->mkNode(kind::EQUAL, x, x);
1385
2
  sameNormalForm(StringsEntail::inferEqsFromContains(x, x), eq_x_x);
1386
1387
  // inferEqsFromContains((str.replace x "B" "A"), x) returns something
1388
  // equivalent to (= (str.replace x "B" "A") x)
1389
4
  Node repl = d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, a);
1390
4
  Node eq_repl_x = d_nodeManager->mkNode(kind::EQUAL, repl, x);
1391
2
  sameNormalForm(StringsEntail::inferEqsFromContains(repl, x), eq_repl_x);
1392
1393
  // inferEqsFromContains(x, (str.replace x "B" "A")) returns something
1394
  // equivalent to (= (str.replace x "B" "A") x)
1395
4
  Node eq_x_repl = d_nodeManager->mkNode(kind::EQUAL, x, repl);
1396
2
  sameNormalForm(StringsEntail::inferEqsFromContains(x, repl), eq_x_repl);
1397
}
1398
1399
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_prefix_suffix)
1400
{
1401
4
  TypeNode strType = d_nodeManager->stringType();
1402
1403
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
1404
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
1405
4
  Node x = d_nodeManager->mkVar("x", strType);
1406
4
  Node y = d_nodeManager->mkVar("y", strType);
1407
4
  Node xx = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x);
1408
4
  Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a);
1409
4
  Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y);
1410
4
  Node f = d_nodeManager->mkConst(false);
1411
1412
  // Same normal form for:
1413
  //
1414
  // (str.prefix (str.++ x y) x)
1415
  //
1416
  // (= y "")
1417
4
  Node p_xy = d_nodeManager->mkNode(kind::STRING_PREFIX, xy, x);
1418
4
  Node empty_y = d_nodeManager->mkNode(kind::EQUAL, y, empty);
1419
2
  sameNormalForm(p_xy, empty_y);
1420
1421
  // Same normal form for:
1422
  //
1423
  // (str.suffix (str.++ x x) x)
1424
  //
1425
  // (= x "")
1426
4
  Node p_xx = d_nodeManager->mkNode(kind::STRING_SUFFIX, xx, x);
1427
4
  Node empty_x = d_nodeManager->mkNode(kind::EQUAL, x, empty);
1428
2
  sameNormalForm(p_xx, empty_x);
1429
1430
  // (str.suffix x (str.++ x x "A")) ---> false
1431
4
  Node p_xxa = d_nodeManager->mkNode(kind::STRING_SUFFIX, xxa, x);
1432
2
  sameNormalForm(p_xxa, f);
1433
2
}
1434
1435
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
1436
{
1437
4
  TypeNode strType = d_nodeManager->stringType();
1438
4
  TypeNode intType = d_nodeManager->integerType();
1439
1440
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
1441
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
1442
4
  Node aaa = d_nodeManager->mkConst(::CVC4::String("AAA"));
1443
4
  Node b = d_nodeManager->mkConst(::CVC4::String("B"));
1444
4
  Node ba = d_nodeManager->mkConst(::CVC4::String("BA"));
1445
4
  Node w = d_nodeManager->mkVar("w", strType);
1446
4
  Node x = d_nodeManager->mkVar("x", strType);
1447
4
  Node y = d_nodeManager->mkVar("y", strType);
1448
4
  Node z = d_nodeManager->mkVar("z", strType);
1449
4
  Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a);
1450
4
  Node f = d_nodeManager->mkConst(false);
1451
4
  Node n = d_nodeManager->mkVar("n", intType);
1452
4
  Node zero = d_nodeManager->mkConst(Rational(0));
1453
4
  Node one = d_nodeManager->mkConst(Rational(1));
1454
4
  Node three = d_nodeManager->mkConst(Rational(3));
1455
1456
  // Same normal form for:
1457
  //
1458
  // (= "" (str.replace "" x "B"))
1459
  //
1460
  // (not (= x ""))
1461
  Node empty_repl = d_nodeManager->mkNode(
1462
      kind::EQUAL,
1463
      empty,
1464
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, b));
1465
  Node empty_x = d_nodeManager->mkNode(
1466
4
      kind::NOT, d_nodeManager->mkNode(kind::EQUAL, x, empty));
1467
2
  sameNormalForm(empty_repl, empty_x);
1468
1469
  // Same normal form for:
1470
  //
1471
  // (= "" (str.replace x y (str.++ x x "A")))
1472
  //
1473
  // (and (= x "") (not (= y "")))
1474
  Node empty_repl_xaa = d_nodeManager->mkNode(
1475
      kind::EQUAL,
1476
      empty,
1477
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, xxa));
1478
  Node empty_xy = d_nodeManager->mkNode(
1479
      kind::AND,
1480
4
      d_nodeManager->mkNode(kind::EQUAL, x, empty),
1481
6
      d_nodeManager->mkNode(kind::NOT,
1482
14
                            d_nodeManager->mkNode(kind::EQUAL, y, empty)));
1483
2
  sameNormalForm(empty_repl_xaa, empty_xy);
1484
1485
  // (= "" (str.replace (str.++ x x "A") x y)) ---> false
1486
  Node empty_repl_xxaxy = d_nodeManager->mkNode(
1487
      kind::EQUAL,
1488
      empty,
1489
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, xxa, x, y));
1490
  Node eq_xxa_repl = d_nodeManager->mkNode(
1491
      kind::EQUAL,
1492
      xxa,
1493
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, empty, y, x));
1494
2
  sameNormalForm(empty_repl_xxaxy, f);
1495
1496
  // Same normal form for:
1497
  //
1498
  // (= "" (str.replace "A" x y))
1499
  //
1500
  // (= "A" (str.replace "" y x))
1501
  Node empty_repl_axy = d_nodeManager->mkNode(
1502
4
      kind::EQUAL, empty, d_nodeManager->mkNode(kind::STRING_STRREPL, a, x, y));
1503
  Node eq_a_repl = d_nodeManager->mkNode(
1504
4
      kind::EQUAL, a, d_nodeManager->mkNode(kind::STRING_STRREPL, empty, y, x));
1505
2
  sameNormalForm(empty_repl_axy, eq_a_repl);
1506
1507
  // Same normal form for:
1508
  //
1509
  // (= "" (str.replace x "A" ""))
1510
  //
1511
  // (str.prefix x "A")
1512
  Node empty_repl_a = d_nodeManager->mkNode(
1513
      kind::EQUAL,
1514
      empty,
1515
4
      d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, empty));
1516
4
  Node prefix_a = d_nodeManager->mkNode(kind::STRING_PREFIX, x, a);
1517
2
  sameNormalForm(empty_repl_a, prefix_a);
1518
1519
  // Same normal form for:
1520
  //
1521
  // (= "" (str.substr x 1 2))
1522
  //
1523
  // (<= (str.len x) 1)
1524
  Node empty_substr = d_nodeManager->mkNode(
1525
      kind::EQUAL,
1526
      empty,
1527
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three));
1528
  Node leq_len_x = d_nodeManager->mkNode(
1529
4
      kind::LEQ, d_nodeManager->mkNode(kind::STRING_LENGTH, x), one);
1530
2
  sameNormalForm(empty_substr, leq_len_x);
1531
1532
  // Different normal form for:
1533
  //
1534
  // (= "" (str.substr x 0 n))
1535
  //
1536
  // (<= n 0)
1537
  Node empty_substr_x = d_nodeManager->mkNode(
1538
      kind::EQUAL,
1539
      empty,
1540
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, n));
1541
4
  Node leq_n = d_nodeManager->mkNode(kind::LEQ, n, zero);
1542
2
  differentNormalForms(empty_substr_x, leq_n);
1543
1544
  // Same normal form for:
1545
  //
1546
  // (= "" (str.substr "A" 0 n))
1547
  //
1548
  // (<= n 0)
1549
  Node empty_substr_a = d_nodeManager->mkNode(
1550
      kind::EQUAL,
1551
      empty,
1552
4
      d_nodeManager->mkNode(kind::STRING_SUBSTR, a, zero, n));
1553
2
  sameNormalForm(empty_substr_a, leq_n);
1554
1555
  // Same normal form for:
1556
  //
1557
  // (= (str.++ x x a) (str.replace y (str.++ x x a) y))
1558
  //
1559
  // (= (str.++ x x a) y)
1560
  Node eq_xxa_repl_y = d_nodeManager->mkNode(
1561
4
      kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_STRREPL, y, xxa, y));
1562
4
  Node eq_xxa_y = d_nodeManager->mkNode(kind::EQUAL, xxa, y);
1563
2
  sameNormalForm(eq_xxa_repl_y, eq_xxa_y);
1564
1565
  // (= (str.++ x x a) (str.replace (str.++ x x a) "A" "B")) ---> false
1566
  Node eq_xxa_repl_xxa = d_nodeManager->mkNode(
1567
4
      kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_STRREPL, xxa, a, b));
1568
2
  sameNormalForm(eq_xxa_repl_xxa, f);
1569
1570
  // Same normal form for:
1571
  //
1572
  // (= (str.replace x "A" "B") "")
1573
  //
1574
  // (= x "")
1575
  Node eq_repl = d_nodeManager->mkNode(
1576
4
      kind::EQUAL, d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b), empty);
1577
4
  Node eq_x = d_nodeManager->mkNode(kind::EQUAL, x, empty);
1578
2
  sameNormalForm(eq_repl, eq_x);
1579
1580
  {
1581
    // Same normal form for:
1582
    //
1583
    // (= (str.replace y "A" "B") "B")
1584
    //
1585
    // (= (str.replace y "B" "A") "A")
1586
    Node lhs = d_nodeManager->mkNode(
1587
4
        kind::EQUAL, d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b), b);
1588
    Node rhs = d_nodeManager->mkNode(
1589
4
        kind::EQUAL, d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, a), a);
1590
2
    sameNormalForm(lhs, rhs);
1591
  }
1592
1593
  {
1594
    // Same normal form for:
1595
    //
1596
    // (= (str.++ x "A" y) (str.++ "A" "A" (str.substr "AAA" 0 n)))
1597
    //
1598
    // (= (str.++ y x) (str.++ (str.substr "AAA" 0 n) "A"))
1599
    Node lhs = d_nodeManager->mkNode(
1600
        kind::EQUAL,
1601
4
        d_nodeManager->mkNode(kind::STRING_CONCAT, x, a, y),
1602
6
        d_nodeManager->mkNode(
1603
            kind::STRING_CONCAT,
1604
            a,
1605
            a,
1606
14
            d_nodeManager->mkNode(kind::STRING_SUBSTR, aaa, zero, n)));
1607
    Node rhs = d_nodeManager->mkNode(
1608
        kind::EQUAL,
1609
4
        d_nodeManager->mkNode(kind::STRING_CONCAT, x, y),
1610
8
        d_nodeManager->mkNode(
1611
            kind::STRING_CONCAT,
1612
4
            d_nodeManager->mkNode(kind::STRING_SUBSTR, aaa, zero, n),
1613
10
            a));
1614
2
    sameNormalForm(lhs, rhs);
1615
  }
1616
1617
  {
1618
    // Same normal form for:
1619
    //
1620
    // (= (str.++ "A" x) "A")
1621
    //
1622
    // (= x "")
1623
    Node lhs = d_nodeManager->mkNode(
1624
4
        kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, a, x), a);
1625
4
    Node rhs = d_nodeManager->mkNode(kind::EQUAL, x, empty);
1626
2
    sameNormalForm(lhs, rhs);
1627
  }
1628
1629
  {
1630
    // (= (str.++ x "A") "") ---> false
1631
    Node eq = d_nodeManager->mkNode(
1632
4
        kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), empty);
1633
2
    sameNormalForm(eq, f);
1634
  }
1635
1636
  {
1637
    // (= (str.++ x "B") "AAA") ---> false
1638
    Node eq = d_nodeManager->mkNode(
1639
4
        kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, x, b), aaa);
1640
2
    sameNormalForm(eq, f);
1641
  }
1642
1643
  {
1644
    // (= (str.++ x "AAA") "A") ---> false
1645
    Node eq = d_nodeManager->mkNode(
1646
4
        kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, x, aaa), a);
1647
2
    sameNormalForm(eq, f);
1648
  }
1649
1650
  {
1651
    // (= (str.++ "AAA" (str.substr "A" 0 n)) (str.++ x "B")) ---> false
1652
    Node eq = d_nodeManager->mkNode(
1653
        kind::EQUAL,
1654
6
        d_nodeManager->mkNode(
1655
            kind::STRING_CONCAT,
1656
            aaa,
1657
6
            d_nodeManager->mkNode(
1658
                kind::STRING_CONCAT,
1659
                a,
1660
                a,
1661
4
                d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, n))),
1662
8
        d_nodeManager->mkNode(kind::STRING_CONCAT, x, b));
1663
2
    sameNormalForm(eq, f);
1664
  }
1665
1666
  {
1667
    // (= (str.++ "A" (int.to.str n)) "A") -/-> false
1668
    Node eq = d_nodeManager->mkNode(
1669
        kind::EQUAL,
1670
6
        d_nodeManager->mkNode(kind::STRING_CONCAT,
1671
                              a,
1672
4
                              d_nodeManager->mkNode(kind::STRING_ITOS, n)),
1673
8
        a);
1674
2
    differentNormalForms(eq, f);
1675
  }
1676
1677
  {
1678
    // (= (str.++ "A" x y) (str.++ x "B" z)) --> false
1679
    Node eq = d_nodeManager->mkNode(
1680
        kind::EQUAL,
1681
4
        d_nodeManager->mkNode(kind::STRING_CONCAT, a, x, y),
1682
8
        d_nodeManager->mkNode(kind::STRING_CONCAT, x, b, z));
1683
2
    sameNormalForm(eq, f);
1684
  }
1685
1686
  {
1687
    // (= (str.++ "B" x y) (str.++ x "AAA" z)) --> false
1688
    Node eq = d_nodeManager->mkNode(
1689
        kind::EQUAL,
1690
4
        d_nodeManager->mkNode(kind::STRING_CONCAT, b, x, y),
1691
8
        d_nodeManager->mkNode(kind::STRING_CONCAT, x, aaa, z));
1692
2
    sameNormalForm(eq, f);
1693
  }
1694
1695
  {
1696
4
    Node xrepl = d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b);
1697
1698
    // Same normal form for:
1699
    //
1700
    // (= (str.++ "B" (str.replace x "A" "B") z y w)
1701
    //    (str.++ z x "BA" z))
1702
    //
1703
    // (and (= (str.++ "B" (str.replace x "A" "B") z)
1704
    //         (str.++ z x "B"))
1705
    //      (= (str.++ y w) (str.++ "A" z)))
1706
    Node lhs = d_nodeManager->mkNode(
1707
        kind::EQUAL,
1708
4
        d_nodeManager->mkNode(kind::STRING_CONCAT, b, xrepl, z, y, w),
1709
8
        d_nodeManager->mkNode(kind::STRING_CONCAT, z, x, ba, z));
1710
    Node rhs = d_nodeManager->mkNode(
1711
        kind::AND,
1712
10
        d_nodeManager->mkNode(
1713
            kind::EQUAL,
1714
4
            d_nodeManager->mkNode(kind::STRING_CONCAT, b, xrepl, z),
1715
4
            d_nodeManager->mkNode(kind::STRING_CONCAT, z, x, b)),
1716
10
        d_nodeManager->mkNode(
1717
            kind::EQUAL,
1718
4
            d_nodeManager->mkNode(kind::STRING_CONCAT, y, w),
1719
14
            d_nodeManager->mkNode(kind::STRING_CONCAT, a, z)));
1720
2
    sameNormalForm(lhs, rhs);
1721
  }
1722
2
}
1723
1724
26
TEST_F(TestTheoryWhiteSequencesRewriter, strip_constant_endpoints)
1725
{
1726
4
  TypeNode intType = d_nodeManager->integerType();
1727
4
  TypeNode strType = d_nodeManager->stringType();
1728
1729
4
  Node empty = d_nodeManager->mkConst(::CVC4::String(""));
1730
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
1731
4
  Node ab = d_nodeManager->mkConst(::CVC4::String("AB"));
1732
4
  Node abc = d_nodeManager->mkConst(::CVC4::String("ABC"));
1733
4
  Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD"));
1734
4
  Node bc = d_nodeManager->mkConst(::CVC4::String("BC"));
1735
4
  Node c = d_nodeManager->mkConst(::CVC4::String("C"));
1736
4
  Node cd = d_nodeManager->mkConst(::CVC4::String("CD"));
1737
4
  Node x = d_nodeManager->mkVar("x", strType);
1738
4
  Node y = d_nodeManager->mkVar("y", strType);
1739
4
  Node n = d_nodeManager->mkVar("n", intType);
1740
1741
  {
1742
    // stripConstantEndpoints({ "" }, { "A" }, {}, {}, 0) ---> false
1743
4
    std::vector<Node> n1 = {empty};
1744
4
    std::vector<Node> n2 = {a};
1745
4
    std::vector<Node> nb;
1746
4
    std::vector<Node> ne;
1747
2
    bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0);
1748
2
    ASSERT_FALSE(res);
1749
  }
1750
1751
  {
1752
    // stripConstantEndpoints({ "A" }, { "A". (int.to.str n) }, {}, {}, 0)
1753
    // ---> false
1754
4
    std::vector<Node> n1 = {a};
1755
4
    std::vector<Node> n2 = {a, d_nodeManager->mkNode(kind::STRING_ITOS, n)};
1756
4
    std::vector<Node> nb;
1757
4
    std::vector<Node> ne;
1758
2
    bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0);
1759
2
    ASSERT_FALSE(res);
1760
  }
1761
1762
  {
1763
    // stripConstantEndpoints({ "ABCD" }, { "C" }, {}, {}, 1)
1764
    // ---> true
1765
    // n1 is updated to { "CD" }
1766
    // nb is updated to { "AB" }
1767
4
    std::vector<Node> n1 = {abcd};
1768
4
    std::vector<Node> n2 = {c};
1769
4
    std::vector<Node> nb;
1770
4
    std::vector<Node> ne;
1771
4
    std::vector<Node> n1r = {cd};
1772
4
    std::vector<Node> nbr = {ab};
1773
2
    bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1);
1774
2
    ASSERT_TRUE(res);
1775
2
    ASSERT_EQ(n1, n1r);
1776
2
    ASSERT_EQ(nb, nbr);
1777
  }
1778
1779
  {
1780
    // stripConstantEndpoints({ "ABC", x }, { "CD" }, {}, {}, 1)
1781
    // ---> true
1782
    // n1 is updated to { "C", x }
1783
    // nb is updated to { "AB" }
1784
4
    std::vector<Node> n1 = {abc, x};
1785
4
    std::vector<Node> n2 = {cd};
1786
4
    std::vector<Node> nb;
1787
4
    std::vector<Node> ne;
1788
4
    std::vector<Node> n1r = {c, x};
1789
4
    std::vector<Node> nbr = {ab};
1790
2
    bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1);
1791
2
    ASSERT_TRUE(res);
1792
2
    ASSERT_EQ(n1, n1r);
1793
2
    ASSERT_EQ(nb, nbr);
1794
  }
1795
1796
  {
1797
    // stripConstantEndpoints({ "ABC" }, { "A" }, {}, {}, -1)
1798
    // ---> true
1799
    // n1 is updated to { "A" }
1800
    // nb is updated to { "BC" }
1801
4
    std::vector<Node> n1 = {abc};
1802
4
    std::vector<Node> n2 = {a};
1803
4
    std::vector<Node> nb;
1804
4
    std::vector<Node> ne;
1805
4
    std::vector<Node> n1r = {a};
1806
4
    std::vector<Node> ner = {bc};
1807
2
    bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1);
1808
2
    ASSERT_TRUE(res);
1809
2
    ASSERT_EQ(n1, n1r);
1810
2
    ASSERT_EQ(ne, ner);
1811
  }
1812
1813
  {
1814
    // stripConstantEndpoints({ x, "ABC" }, { y, "A" }, {}, {}, -1)
1815
    // ---> true
1816
    // n1 is updated to { x, "A" }
1817
    // nb is updated to { "BC" }
1818
4
    std::vector<Node> n1 = {x, abc};
1819
4
    std::vector<Node> n2 = {y, a};
1820
4
    std::vector<Node> nb;
1821
4
    std::vector<Node> ne;
1822
4
    std::vector<Node> n1r = {x, a};
1823
4
    std::vector<Node> ner = {bc};
1824
2
    bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1);
1825
2
    ASSERT_TRUE(res);
1826
2
    ASSERT_EQ(n1, n1r);
1827
2
    ASSERT_EQ(ne, ner);
1828
  }
1829
}
1830
1831
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership)
1832
{
1833
4
  TypeNode strType = d_nodeManager->stringType();
1834
1835
4
  std::vector<Node> vec_empty;
1836
4
  Node abc = d_nodeManager->mkConst(::CVC4::String("ABC"));
1837
4
  Node re_abc = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, abc);
1838
4
  Node x = d_nodeManager->mkVar("x", strType);
1839
1840
  {
1841
    // Same normal form for:
1842
    //
1843
    // (str.in.re x (re.++ (re.* re.allchar)
1844
    //                     (re.* re.allchar)
1845
    //                     (str.to.re "ABC")
1846
    //                     (re.* re.allchar)))
1847
    //
1848
    // (str.contains x "ABC")
1849
    Node sig_star = d_nodeManager->mkNode(
1850
        kind::REGEXP_STAR,
1851
4
        d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty));
1852
    Node lhs = d_nodeManager->mkNode(
1853
        kind::STRING_IN_REGEXP,
1854
        x,
1855
4
        d_nodeManager->mkNode(
1856
6
            kind::REGEXP_CONCAT, sig_star, sig_star, re_abc, sig_star));
1857
4
    Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc);
1858
2
    sameNormalForm(lhs, rhs);
1859
  }
1860
1861
  {
1862
    // Different normal forms for:
1863
    //
1864
    // (str.in.re x (re.++ (re.* re.allchar) (str.to.re "ABC")))
1865
    //
1866
    // (str.contains x "ABC")
1867
    Node sig_star = d_nodeManager->mkNode(
1868
        kind::REGEXP_STAR,
1869
4
        d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty));
1870
    Node lhs = d_nodeManager->mkNode(
1871
        kind::STRING_IN_REGEXP,
1872
        x,
1873
4
        d_nodeManager->mkNode(kind::REGEXP_CONCAT, sig_star, re_abc));
1874
4
    Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc);
1875
2
    differentNormalForms(lhs, rhs);
1876
  }
1877
2
}
1878
1879
26
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_regexp_concat)
1880
{
1881
4
  TypeNode strType = d_nodeManager->stringType();
1882
1883
4
  std::vector<Node> emptyArgs;
1884
4
  Node x = d_nodeManager->mkVar("x", strType);
1885
4
  Node y = d_nodeManager->mkVar("y", strType);
1886
  Node allStar = d_nodeManager->mkNode(
1887
4
      kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyArgs));
1888
4
  Node xReg = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, x);
1889
4
  Node yReg = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, y);
1890
1891
  {
1892
    // In normal form:
1893
    //
1894
    // (re.++ (re.* re.allchar) (re.union (str.to.re x) (str.to.re y)))
1895
    Node n = d_nodeManager->mkNode(
1896
        kind::REGEXP_CONCAT,
1897
        allStar,
1898
4
        d_nodeManager->mkNode(kind::REGEXP_UNION, xReg, yReg));
1899
2
    inNormalForm(n);
1900
  }
1901
1902
  {
1903
    // In normal form:
1904
    //
1905
    // (re.++ (str.to.re x) (re.* re.allchar))
1906
4
    Node n = d_nodeManager->mkNode(kind::REGEXP_CONCAT, xReg, allStar);
1907
2
    inNormalForm(n);
1908
  }
1909
2
}
1910
}  // namespace test
1911
13469150
}  // namespace CVC4