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