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