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