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