1 /********************* */
2 /*! \file theory_strings_rewriter_white.h
4 ** Top contributors (to current version):
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
12 ** \brief Unit tests for the strings rewriter
14 ** Unit tests for the strings rewriter.
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"
24 #include <cxxtest/TestSuite.h>
28 using namespace CVC4::smt
;
29 using namespace CVC4::theory
;
30 using namespace CVC4::theory::strings
;
32 class TheoryStringsRewriterWhite
: public CxxTest::TestSuite
40 TheoryStringsRewriterWhite() {}
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
);
52 void tearDown() override
59 void testCheckEntailArithWithAssumption()
61 TypeNode intType
= d_nm
->integerType();
62 TypeNode strType
= d_nm
->stringType();
64 Node x
= d_nm
->mkVar("x", intType
);
65 Node y
= d_nm
->mkVar("y", strType
);
66 Node z
= d_nm
->mkVar("z", intType
);
68 Node zero
= d_nm
->mkConst(Rational(0));
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
));
75 // x + (str.len y) = 0 |= 0 >= x --> true
76 TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
77 x_plus_slen_y_eq_zero
, zero
, x
, false));
79 // x + (str.len y) = 0 |= 0 > x --> false
80 TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption(
81 x_plus_slen_y_eq_zero
, zero
, x
, true));
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
));
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));
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
));
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));
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
));
103 // x + 5 < 6 |= 0 >= x --> true
104 TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
105 x_plus_five_lt_six
, zero
, x
, false));
107 // x + 5 < 6 |= 0 > x --> false
108 TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption(
109 x_plus_five_lt_six
, zero
, x
, true));
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
));
115 // x + 5 < 5 |= -x >= 0 --> true
116 TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
117 x_plus_five_lt_five
, neg_x
, zero
, false));
119 // x + 5 < 5 |= 0 > x --> true
120 TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
121 x_plus_five_lt_five
, zero
, x
, false));
124 void testRewriteSubstr()
126 TypeNode intType
= d_nm
->integerType();
127 TypeNode strType
= d_nm
->stringType();
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));
135 Node s
= d_nm
->mkVar("s", strType
);
136 Node x
= d_nm
->mkVar("x", intType
);
137 Node y
= d_nm
->mkVar("y", intType
);
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
);
144 // (str.substr "A" (+ x 1) x) -> ""
145 n
= d_nm
->mkNode(kind::STRING_SUBSTR
,
147 d_nm
->mkNode(kind::PLUS
, x
, d_nm
->mkConst(Rational(1))),
149 res
= TheoryStringsRewriter::rewriteSubstr(n
);
150 TS_ASSERT_EQUALS(res
, empty
);
152 // (str.substr "A" (+ x (str.len s2)) x) -> ""
156 d_nm
->mkNode(kind::PLUS
, x
, d_nm
->mkNode(kind::STRING_LENGTH
, s
)),
158 res
= TheoryStringsRewriter::rewriteSubstr(n
);
159 TS_ASSERT_EQUALS(res
, empty
);
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
);
166 // (str.substr "ABCD" (+ x 3) x) -> ""
168 kind::STRING_SUBSTR
, abcd
, d_nm
->mkNode(kind::PLUS
, x
, three
), x
);
169 res
= TheoryStringsRewriter::rewriteSubstr(n
);
170 TS_ASSERT_EQUALS(res
, empty
);
172 // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
174 kind::STRING_SUBSTR
, abcd
, d_nm
->mkNode(kind::PLUS
, x
, two
), x
);
175 res
= TheoryStringsRewriter::rewriteSubstr(n
);
176 TS_ASSERT_EQUALS(res
, n
);
179 void testRewriteConcat()
181 TypeNode intType
= d_nm
->integerType();
182 TypeNode strType
= d_nm
->stringType();
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));
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
);
194 // Same normal form for:
196 // (str.++ (str.replace "A" x "") "A")
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
);
206 // Same normal form for:
208 // (str.++ y (str.replace "" x (str.substr y 0 3)) (str.substr y 0 3) "A" (str.substr y 0 3))
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
);
219 // Same normal form for:
221 // (str.++ "A" (str.replace "A" x "") (str.substr "A" 0 i))
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
);
226 d_nm
->mkNode(kind::STRING_CONCAT
, a
, substr_a
, repl_a_x_e
);
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
);
233 // Same normal form for:
235 // (str.++ (str.replace "" x (str.substr "A" 0 i)) (str.substr "A" 0 i) (str.at "A" i))
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
);
241 d_nm
->mkNode(kind::STRING_CONCAT
, repl_e_x_s
, substr_a
, charat_a
);
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
);
249 void testLengthPreserveRewrite()
251 TypeNode intType
= d_nm
->integerType();
252 TypeNode strType
= d_nm
->stringType();
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"));
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
);
265 // Same length preserving rewrite for:
267 // (str.++ "ABCD" (str.++ x x))
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
,
275 d_nm
->mkNode(kind::STRING_STRREPL
, x
, gh
, ij
),
277 Node res_concat1
= TheoryStringsRewriter::lengthPreserveRewrite(concat1
);
278 Node res_concat2
= TheoryStringsRewriter::lengthPreserveRewrite(concat2
);
279 TS_ASSERT_EQUALS(res_concat1
, res_concat2
);
282 void testRewriteIndexOf()
284 TypeNode strType
= d_nm
->stringType();
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));
295 // Same normal form for:
297 // (str.to.int (str.indexof "A" x 1))
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
);
308 // Same normal form for:
310 // (str.indexof (str.++ "ABCD" x) y 3)
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
),
317 Node idof_aaad
= d_nm
->mkNode(kind::STRING_STRIDOF
,
318 d_nm
->mkNode(kind::STRING_CONCAT
, aaad
, x
),
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
);
326 void testRewriteReplace()
328 TypeNode strType
= d_nm
->stringType();
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
);
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
),
345 Node repl_repl_short
=
346 d_nm
->mkNode(kind::STRING_STRREPL
,
347 d_nm
->mkNode(kind::STRING_STRREPL
, x
, b
, 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
);
354 // (str.replace "A" (str.replace "B", x, "C") "D") --> "A"
355 repl_repl
= d_nm
->mkNode(kind::STRING_STRREPL
,
357 d_nm
->mkNode(kind::STRING_STRREPL
, b
, x
, c
),
359 res_repl_repl
= Rewriter::rewrite(repl_repl
);
360 TS_ASSERT_EQUALS(res_repl_repl
, a
);
362 // (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A"
363 repl_repl
= d_nm
->mkNode(kind::STRING_STRREPL
,
365 d_nm
->mkNode(kind::STRING_STRREPL
, b
, x
, a
),
367 res_repl_repl
= Rewriter::rewrite(repl_repl
);
368 TS_ASSERT_DIFFERS(res_repl_repl
, a
);
370 // Same normal form for:
372 // (str.replace x (str.++ x y z) y)
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
);
382 // (str.replace "" (str.++ x x) x) --> ""
383 Node repl_empty_xx
= d_nm
->mkNode(kind::STRING_STRREPL
,
385 d_nm
->mkNode(kind::STRING_CONCAT
, x
, x
),
387 Node res_repl_empty_xx
= Rewriter::rewrite(repl_empty_xx
);
388 TS_ASSERT_EQUALS(res_repl_empty_xx
, empty
);
390 // (str.replace "AB" (str.++ x "A") x) --> (str.replace "AB" (str.++ x "A")
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
),
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
),
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
);
404 // (str.replace "AB" (str.++ x "A") x) -/-> (str.replace "AB" (str.++ "A" x)
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
),
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
);
414 void testRewriteContains()
416 TypeNode strType
= d_nm
->stringType();
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);
430 // Same normal form for:
432 // (str.replace "A" (str.substr x 1 3) y z)
434 // (str.replace "A" (str.substr x 1 4) y z)
436 d_nm
->mkNode(kind::STRING_STRREPL
,
438 d_nm
->mkNode(kind::STRING_SUBSTR
, x
, one
, three
),
441 d_nm
->mkNode(kind::STRING_STRREPL
,
443 d_nm
->mkNode(kind::STRING_SUBSTR
, x
, one
, four
),
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
);
449 // Same normal form for:
451 // (str.replace "A" (str.++ y (str.substr x 1 3)) y z)
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
,
457 d_nm
->mkNode(kind::STRING_CONCAT
,
459 d_nm
->mkNode(kind::STRING_SUBSTR
, x
, one
, three
)),
461 Node concat_substr_4
= d_nm
->mkNode(
462 kind::STRING_STRREPL
,
464 d_nm
->mkNode(kind::STRING_CONCAT
,
466 d_nm
->mkNode(kind::STRING_SUBSTR
, x
, one
, four
)),
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
);
472 // (str.contains "A" (str.++ a (str.replace "B", x, "C")) --> false
474 d_nm
->mkNode(kind::STRING_STRCTN
,
476 d_nm
->mkNode(kind::STRING_CONCAT
,
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
);
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
);
490 // Same normal form for:
492 // (str.contains (str.++ y x) (str.++ x z y))
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
);