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