2710a60fe45c2e9b04a1eee981c9779d8db939aa
[cvc5.git] / test / unit / theory / theory_strings_rewriter_white.h
1 /********************* */
2 /*! \file theory_strings_rewriter_white.h
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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 rewriter
13 **
14 ** Unit tests for the strings rewriter.
15 **/
16
17 #include "expr/node.h"
18 #include "expr/node_manager.h"
19 #include "smt/smt_engine.h"
20 #include "smt/smt_engine_scope.h"
21 #include "theory/rewriter.h"
22 #include "theory/strings/theory_strings_rewriter.h"
23
24 #include <cxxtest/TestSuite.h>
25 #include <vector>
26
27 using namespace CVC4;
28 using namespace CVC4::smt;
29 using namespace CVC4::theory;
30 using namespace CVC4::theory::strings;
31
32 class TheoryStringsRewriterWhite : public CxxTest::TestSuite
33 {
34 ExprManager *d_em;
35 NodeManager *d_nm;
36 SmtEngine *d_smt;
37 SmtScope *d_scope;
38
39 public:
40 TheoryStringsRewriterWhite() {}
41
42 void setUp() override
43 {
44 Options opts;
45 opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
46 d_em = new ExprManager(opts);
47 d_nm = NodeManager::fromExprManager(d_em);
48 d_smt = new SmtEngine(d_em);
49 d_scope = new SmtScope(d_smt);
50 }
51
52 void tearDown() override
53 {
54 delete d_scope;
55 delete d_smt;
56 delete d_em;
57 }
58
59 void testCheckEntailArithWithAssumption()
60 {
61 TypeNode intType = d_nm->integerType();
62 TypeNode strType = d_nm->stringType();
63
64 Node x = d_nm->mkVar("x", intType);
65 Node y = d_nm->mkVar("y", strType);
66 Node z = d_nm->mkVar("z", intType);
67
68 Node zero = d_nm->mkConst(Rational(0));
69
70 Node slen_y = d_nm->mkNode(kind::STRING_LENGTH, y);
71 Node x_plus_slen_y = d_nm->mkNode(kind::PLUS, x, slen_y);
72 Node x_plus_slen_y_eq_zero =
73 Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x_plus_slen_y, zero));
74
75 // x + (str.len y) = 0 |= 0 >= x --> true
76 TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
77 x_plus_slen_y_eq_zero, zero, x, false));
78
79 // x + (str.len y) = 0 |= 0 > x --> false
80 TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption(
81 x_plus_slen_y_eq_zero, zero, x, true));
82
83 Node x_plus_slen_y_plus_z_eq_zero = Rewriter::rewrite(d_nm->mkNode(
84 kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, z), zero));
85
86 // x + (str.len y) + z = 0 |= 0 > x --> false
87 TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption(
88 x_plus_slen_y_plus_z_eq_zero, zero, x, true));
89
90 Node x_plus_slen_y_plus_slen_y_eq_zero = Rewriter::rewrite(d_nm->mkNode(
91 kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, slen_y), zero));
92
93 // x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true
94 TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
95 x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false));
96
97 Node five = d_nm->mkConst(Rational(5));
98 Node six = d_nm->mkConst(Rational(6));
99 Node x_plus_five = d_nm->mkNode(kind::PLUS, x, five);
100 Node x_plus_five_lt_six =
101 Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, six));
102
103 // x + 5 < 6 |= 0 >= x --> true
104 TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
105 x_plus_five_lt_six, zero, x, false));
106
107 // x + 5 < 6 |= 0 > x --> false
108 TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption(
109 x_plus_five_lt_six, zero, x, true));
110
111 Node neg_x = d_nm->mkNode(kind::UMINUS, x);
112 Node x_plus_five_lt_five =
113 Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, five));
114
115 // x + 5 < 5 |= -x >= 0 --> true
116 TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
117 x_plus_five_lt_five, neg_x, zero, false));
118
119 // x + 5 < 5 |= 0 > x --> true
120 TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
121 x_plus_five_lt_five, zero, x, false));
122 }
123
124 void testRewriteSubstr()
125 {
126 TypeNode intType = d_nm->integerType();
127 TypeNode strType = d_nm->stringType();
128
129 Node empty = d_nm->mkConst(::CVC4::String(""));
130 Node a = d_nm->mkConst(::CVC4::String("A"));
131 Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
132 Node two = d_nm->mkConst(Rational(2));
133 Node three = d_nm->mkConst(Rational(3));
134
135 Node s = d_nm->mkVar("s", strType);
136 Node x = d_nm->mkVar("x", intType);
137 Node y = d_nm->mkVar("y", intType);
138
139 // (str.substr "A" x x) --> ""
140 Node n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, x);
141 Node res = TheoryStringsRewriter::rewriteSubstr(n);
142 TS_ASSERT_EQUALS(res, empty);
143
144 // (str.substr "A" (+ x 1) x) -> ""
145 n = d_nm->mkNode(kind::STRING_SUBSTR,
146 a,
147 d_nm->mkNode(kind::PLUS, x, d_nm->mkConst(Rational(1))),
148 x);
149 res = TheoryStringsRewriter::rewriteSubstr(n);
150 TS_ASSERT_EQUALS(res, empty);
151
152 // (str.substr "A" (+ x (str.len s2)) x) -> ""
153 n = d_nm->mkNode(
154 kind::STRING_SUBSTR,
155 a,
156 d_nm->mkNode(kind::PLUS, x, d_nm->mkNode(kind::STRING_LENGTH, s)),
157 x);
158 res = TheoryStringsRewriter::rewriteSubstr(n);
159 TS_ASSERT_EQUALS(res, empty);
160
161 // (str.substr "A" x y) -> (str.substr "A" x y)
162 n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, y);
163 res = TheoryStringsRewriter::rewriteSubstr(n);
164 TS_ASSERT_EQUALS(res, n);
165
166 // (str.substr "ABCD" (+ x 3) x) -> ""
167 n = d_nm->mkNode(
168 kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, three), x);
169 res = TheoryStringsRewriter::rewriteSubstr(n);
170 TS_ASSERT_EQUALS(res, empty);
171
172 // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
173 n = d_nm->mkNode(
174 kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, two), x);
175 res = TheoryStringsRewriter::rewriteSubstr(n);
176 TS_ASSERT_EQUALS(res, n);
177 }
178
179 void testRewriteConcat()
180 {
181 TypeNode intType = d_nm->integerType();
182 TypeNode strType = d_nm->stringType();
183
184 Node empty = d_nm->mkConst(::CVC4::String(""));
185 Node a = d_nm->mkConst(::CVC4::String("A"));
186 Node zero = d_nm->mkConst(Rational(0));
187 Node three = d_nm->mkConst(Rational(3));
188
189 Node i = d_nm->mkVar("i", intType);
190 Node s = d_nm->mkVar("s", strType);
191 Node x = d_nm->mkVar("x", strType);
192 Node y = d_nm->mkVar("y", strType);
193
194 // Same normal form for:
195 //
196 // (str.++ (str.replace "A" x "") "A")
197 //
198 // (str.++ "A" (str.replace "A" x ""))
199 Node repl_a_x_e = d_nm->mkNode(kind::STRING_STRREPL, a, x, empty);
200 Node repl_a = d_nm->mkNode(kind::STRING_CONCAT, repl_a_x_e, a);
201 Node a_repl = d_nm->mkNode(kind::STRING_CONCAT, a, repl_a_x_e);
202 Node res_repl_a = Rewriter::rewrite(repl_a);
203 Node res_a_repl = Rewriter::rewrite(a_repl);
204 TS_ASSERT_EQUALS(res_repl_a, res_a_repl);
205
206 // Same normal form for:
207 //
208 // (str.++ y (str.replace "" x (str.substr y 0 3)) (str.substr y 0 3) "A" (str.substr y 0 3))
209 //
210 // (str.++ y (str.substr y 0 3) (str.replace "" x (str.substr y 0 3)) "A" (str.substr y 0 3))
211 Node z = d_nm->mkNode(kind::STRING_SUBSTR, y, zero, three);
212 Node repl_e_x_z = d_nm->mkNode(kind::STRING_STRREPL, empty, x, z);
213 repl_a = d_nm->mkNode(kind::STRING_CONCAT, y, repl_e_x_z, z, a, z);
214 a_repl = d_nm->mkNode(kind::STRING_CONCAT, y, z, repl_e_x_z, a, z);
215 res_repl_a = Rewriter::rewrite(repl_a);
216 res_a_repl = Rewriter::rewrite(a_repl);
217 TS_ASSERT_EQUALS(res_repl_a, res_a_repl);
218
219 // Same normal form for:
220 //
221 // (str.++ "A" (str.replace "A" x "") (str.substr "A" 0 i))
222 //
223 // (str.++ (str.substr "A" 0 i) (str.replace "A" x "") "A")
224 Node substr_a = d_nm->mkNode(kind::STRING_SUBSTR, a, zero, i);
225 Node a_substr_repl =
226 d_nm->mkNode(kind::STRING_CONCAT, a, substr_a, repl_a_x_e);
227 Node substr_repl_a =
228 d_nm->mkNode(kind::STRING_CONCAT, substr_a, repl_a_x_e, a);
229 Node res_a_substr_repl = Rewriter::rewrite(a_substr_repl);
230 Node res_substr_repl_a = Rewriter::rewrite(substr_repl_a);
231 TS_ASSERT_EQUALS(res_a_substr_repl, res_substr_repl_a);
232
233 // Same normal form for:
234 //
235 // (str.++ (str.replace "" x (str.substr "A" 0 i)) (str.substr "A" 0 i) (str.at "A" i))
236 //
237 // (str.++ (str.at "A" i) (str.replace "" x (str.substr "A" 0 i)) (str.substr "A" 0 i))
238 Node charat_a = d_nm->mkNode(kind::STRING_CHARAT, a, i);
239 Node repl_e_x_s = d_nm->mkNode(kind::STRING_STRREPL, empty, x, substr_a);
240 Node repl_substr_a =
241 d_nm->mkNode(kind::STRING_CONCAT, repl_e_x_s, substr_a, charat_a);
242 Node a_repl_substr =
243 d_nm->mkNode(kind::STRING_CONCAT, charat_a, repl_e_x_s, substr_a);
244 Node res_repl_substr_a = Rewriter::rewrite(repl_substr_a);
245 Node res_a_repl_substr = Rewriter::rewrite(a_repl_substr);
246 TS_ASSERT_EQUALS(res_repl_substr_a, res_a_repl_substr);
247 }
248
249 void testLengthPreserveRewrite()
250 {
251 TypeNode intType = d_nm->integerType();
252 TypeNode strType = d_nm->stringType();
253
254 Node empty = d_nm->mkConst(::CVC4::String(""));
255 Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
256 Node f = d_nm->mkConst(::CVC4::String("F"));
257 Node gh = d_nm->mkConst(::CVC4::String("GH"));
258 Node ij = d_nm->mkConst(::CVC4::String("IJ"));
259
260 Node i = d_nm->mkVar("i", intType);
261 Node s = d_nm->mkVar("s", strType);
262 Node x = d_nm->mkVar("x", strType);
263 Node y = d_nm->mkVar("y", strType);
264
265 // Same length preserving rewrite for:
266 //
267 // (str.++ "ABCD" (str.++ x x))
268 //
269 // (str.++ "GH" (str.repl "GH" "IJ") "IJ")
270 Node concat1 = d_nm->mkNode(
271 kind::STRING_CONCAT, abcd, d_nm->mkNode(kind::STRING_CONCAT, x, x));
272 Node concat2 = d_nm->mkNode(kind::STRING_CONCAT,
273 gh,
274 x,
275 d_nm->mkNode(kind::STRING_STRREPL, x, gh, ij),
276 ij);
277 Node res_concat1 = TheoryStringsRewriter::lengthPreserveRewrite(concat1);
278 Node res_concat2 = TheoryStringsRewriter::lengthPreserveRewrite(concat2);
279 TS_ASSERT_EQUALS(res_concat1, res_concat2);
280 }
281
282 void testRewriteIndexOf()
283 {
284 TypeNode strType = d_nm->stringType();
285
286 Node a = d_nm->mkConst(::CVC4::String("A"));
287 Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
288 Node aaad = d_nm->mkConst(::CVC4::String("AAAD"));
289 Node b = d_nm->mkConst(::CVC4::String("B"));
290 Node x = d_nm->mkVar("x", strType);
291 Node y = d_nm->mkVar("y", strType);
292 Node one = d_nm->mkConst(Rational(2));
293 Node three = d_nm->mkConst(Rational(3));
294
295 // Same normal form for:
296 //
297 // (str.to.int (str.indexof "A" x 1))
298 //
299 // (str.to.int (str.indexof "B" x 1))
300 Node a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, one);
301 Node itos_a_idof_x = d_nm->mkNode(kind::STRING_ITOS, a_idof_x);
302 Node b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, one);
303 Node itos_b_idof_x = d_nm->mkNode(kind::STRING_ITOS, b_idof_x);
304 Node res_itos_a_idof_x = Rewriter::rewrite(itos_a_idof_x);
305 Node res_itos_b_idof_x = Rewriter::rewrite(itos_b_idof_x);
306 TS_ASSERT_EQUALS(res_itos_a_idof_x, res_itos_b_idof_x);
307
308 // Same normal form for:
309 //
310 // (str.indexof (str.++ "ABCD" x) y 3)
311 //
312 // (str.indexof (str.++ "AAAD" x) y 3)
313 Node idof_abcd = d_nm->mkNode(kind::STRING_STRIDOF,
314 d_nm->mkNode(kind::STRING_CONCAT, abcd, x),
315 y,
316 three);
317 Node idof_aaad = d_nm->mkNode(kind::STRING_STRIDOF,
318 d_nm->mkNode(kind::STRING_CONCAT, aaad, x),
319 y,
320 three);
321 Node res_idof_abcd = Rewriter::rewrite(idof_abcd);
322 Node res_idof_aaad = Rewriter::rewrite(idof_aaad);
323 TS_ASSERT_EQUALS(res_idof_abcd, res_idof_aaad);
324 }
325
326 void testRewriteReplace()
327 {
328 TypeNode strType = d_nm->stringType();
329
330 Node empty = d_nm->mkConst(::CVC4::String(""));
331 Node a = d_nm->mkConst(::CVC4::String("A"));
332 Node b = d_nm->mkConst(::CVC4::String("B"));
333 Node c = d_nm->mkConst(::CVC4::String("C"));
334 Node d = d_nm->mkConst(::CVC4::String("D"));
335 Node x = d_nm->mkVar("x", strType);
336 Node y = d_nm->mkVar("y", strType);
337 Node z = d_nm->mkVar("z", strType);
338
339 // (str.replace (str.replace x "B" x) x "A") -->
340 // (str.replace (str.replace x "B" "A") x "A")
341 Node repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
342 d_nm->mkNode(kind::STRING_STRREPL, x, b, x),
343 x,
344 a);
345 Node repl_repl_short =
346 d_nm->mkNode(kind::STRING_STRREPL,
347 d_nm->mkNode(kind::STRING_STRREPL, x, b, a),
348 x,
349 a);
350 Node res_repl_repl = Rewriter::rewrite(repl_repl);
351 Node res_repl_repl_short = Rewriter::rewrite(repl_repl_short);
352 TS_ASSERT_EQUALS(res_repl_repl, res_repl_repl_short);
353
354 // (str.replace "A" (str.replace "B", x, "C") "D") --> "A"
355 repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
356 a,
357 d_nm->mkNode(kind::STRING_STRREPL, b, x, c),
358 d);
359 res_repl_repl = Rewriter::rewrite(repl_repl);
360 TS_ASSERT_EQUALS(res_repl_repl, a);
361
362 // (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A"
363 repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
364 a,
365 d_nm->mkNode(kind::STRING_STRREPL, b, x, a),
366 d);
367 res_repl_repl = Rewriter::rewrite(repl_repl);
368 TS_ASSERT_DIFFERS(res_repl_repl, a);
369
370 // Same normal form for:
371 //
372 // (str.replace x (str.++ x y z) y)
373 //
374 // (str.replace x (str.++ x y z) z)
375 Node xyz = d_nm->mkNode(kind::STRING_CONCAT, x, y, z);
376 Node repl_x_xyz = d_nm->mkNode(kind::STRING_STRREPL, x, xyz, y);
377 Node repl_x_zyx = d_nm->mkNode(kind::STRING_STRREPL, x, xyz, z);
378 Node res_repl_x_xyz = Rewriter::rewrite(repl_x_xyz);
379 Node res_repl_x_zyx = Rewriter::rewrite(repl_x_zyx);
380 TS_ASSERT_EQUALS(res_repl_x_xyz, res_repl_x_zyx);
381
382 // (str.replace "" (str.++ x x) x) --> ""
383 Node repl_empty_xx = d_nm->mkNode(kind::STRING_STRREPL,
384 empty,
385 d_nm->mkNode(kind::STRING_CONCAT, x, x),
386 x);
387 Node res_repl_empty_xx = Rewriter::rewrite(repl_empty_xx);
388 TS_ASSERT_EQUALS(res_repl_empty_xx, empty);
389
390 // (str.replace "AB" (str.++ x "A") x) --> (str.replace "AB" (str.++ x "A")
391 // "")
392 Node repl_ab_xa_x = d_nm->mkNode(kind::STRING_STRREPL,
393 d_nm->mkNode(kind::STRING_CONCAT, a, b),
394 d_nm->mkNode(kind::STRING_CONCAT, x, a),
395 x);
396 Node repl_ab_xa_e = d_nm->mkNode(kind::STRING_STRREPL,
397 d_nm->mkNode(kind::STRING_CONCAT, a, b),
398 d_nm->mkNode(kind::STRING_CONCAT, x, a),
399 empty);
400 Node res_repl_ab_xa_x = Rewriter::rewrite(repl_ab_xa_x);
401 Node res_repl_ab_xa_e = Rewriter::rewrite(repl_ab_xa_e);
402 TS_ASSERT_EQUALS(res_repl_ab_xa_x, res_repl_ab_xa_e);
403
404 // (str.replace "AB" (str.++ x "A") x) -/-> (str.replace "AB" (str.++ "A" x)
405 // "")
406 Node repl_ab_ax_e = d_nm->mkNode(kind::STRING_STRREPL,
407 d_nm->mkNode(kind::STRING_CONCAT, a, b),
408 d_nm->mkNode(kind::STRING_CONCAT, a, x),
409 empty);
410 Node res_repl_ab_ax_e = Rewriter::rewrite(repl_ab_ax_e);
411 TS_ASSERT_DIFFERS(res_repl_ab_xa_x, res_repl_ab_ax_e);
412 }
413
414 void testRewriteContains()
415 {
416 TypeNode strType = d_nm->stringType();
417
418 Node empty = d_nm->mkConst(::CVC4::String(""));
419 Node a = d_nm->mkConst(::CVC4::String("A"));
420 Node b = d_nm->mkConst(::CVC4::String("B"));
421 Node c = d_nm->mkConst(::CVC4::String("C"));
422 Node x = d_nm->mkVar("x", strType);
423 Node y = d_nm->mkVar("y", strType);
424 Node z = d_nm->mkVar("z", strType);
425 Node one = d_nm->mkConst(Rational(2));
426 Node three = d_nm->mkConst(Rational(3));
427 Node four = d_nm->mkConst(Rational(4));
428 Node f = d_nm->mkConst(false);
429
430 // Same normal form for:
431 //
432 // (str.replace "A" (str.substr x 1 3) y z)
433 //
434 // (str.replace "A" (str.substr x 1 4) y z)
435 Node substr_3 =
436 d_nm->mkNode(kind::STRING_STRREPL,
437 a,
438 d_nm->mkNode(kind::STRING_SUBSTR, x, one, three),
439 z);
440 Node substr_4 =
441 d_nm->mkNode(kind::STRING_STRREPL,
442 a,
443 d_nm->mkNode(kind::STRING_SUBSTR, x, one, four),
444 z);
445 Node res_substr_3 = Rewriter::rewrite(substr_3);
446 Node res_substr_4 = Rewriter::rewrite(substr_4);
447 TS_ASSERT_EQUALS(res_substr_3, res_substr_4);
448
449 // Same normal form for:
450 //
451 // (str.replace "A" (str.++ y (str.substr x 1 3)) y z)
452 //
453 // (str.replace "A" (str.++ y (str.substr x 1 4)) y z)
454 Node concat_substr_3 = d_nm->mkNode(
455 kind::STRING_STRREPL,
456 a,
457 d_nm->mkNode(kind::STRING_CONCAT,
458 y,
459 d_nm->mkNode(kind::STRING_SUBSTR, x, one, three)),
460 z);
461 Node concat_substr_4 = d_nm->mkNode(
462 kind::STRING_STRREPL,
463 a,
464 d_nm->mkNode(kind::STRING_CONCAT,
465 y,
466 d_nm->mkNode(kind::STRING_SUBSTR, x, one, four)),
467 z);
468 Node res_concat_substr_3 = Rewriter::rewrite(concat_substr_3);
469 Node res_concat_substr_4 = Rewriter::rewrite(concat_substr_4);
470 TS_ASSERT_EQUALS(res_concat_substr_3, res_concat_substr_4);
471
472 // (str.contains "A" (str.++ a (str.replace "B", x, "C")) --> false
473 Node ctn_repl =
474 d_nm->mkNode(kind::STRING_STRCTN,
475 a,
476 d_nm->mkNode(kind::STRING_CONCAT,
477 a,
478 d_nm->mkNode(kind::STRING_STRREPL, b, x, c)));
479 Node res_ctn_repl = Rewriter::rewrite(ctn_repl);
480 TS_ASSERT_EQUALS(res_ctn_repl, f);
481
482 // (str.contains x (str.++ x x)) --> (= x "")
483 Node x_cnts_x_x = d_nm->mkNode(
484 kind::STRING_STRCTN, x, d_nm->mkNode(kind::STRING_CONCAT, x, x));
485 Node res_x_cnts_x_x = Rewriter::rewrite(x_cnts_x_x);
486 Node res_x_eq_empty =
487 Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x, empty));
488 TS_ASSERT_EQUALS(res_x_cnts_x_x, res_x_eq_empty);
489
490 // Same normal form for:
491 //
492 // (str.contains (str.++ y x) (str.++ x z y))
493 //
494 // (and (str.contains (str.++ y x) (str.++ x y)) (= z ""))
495 Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x);
496 Node yx_cnts_xzy = d_nm->mkNode(
497 kind::STRING_STRCTN, yx, d_nm->mkNode(kind::STRING_CONCAT, x, z, y));
498 Node res_yx_cnts_xzy = Rewriter::rewrite(yx_cnts_xzy);
499 Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y);
500 Node yx_cnts_xy = d_nm->mkNode(kind::AND,
501 d_nm->mkNode(kind::STRING_STRCTN, yx, xy),
502 d_nm->mkNode(kind::EQUAL, z, empty));
503 Node res_yx_cnts_xy = Rewriter::rewrite(yx_cnts_xy);
504 TS_ASSERT_EQUALS(res_yx_cnts_xzy, res_yx_cnts_xy);
505 }
506 };