1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Andres Noetzli, Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Unit tests for the strings/sequences rewriter. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <iostream> |
17 |
|
#include <memory> |
18 |
|
#include <vector> |
19 |
|
|
20 |
|
#include "expr/node.h" |
21 |
|
#include "expr/node_manager.h" |
22 |
|
#include "test_smt.h" |
23 |
|
#include "theory/rewriter.h" |
24 |
|
#include "theory/strings/arith_entail.h" |
25 |
|
#include "theory/strings/sequences_rewriter.h" |
26 |
|
#include "theory/strings/strings_entail.h" |
27 |
|
#include "theory/strings/strings_rewriter.h" |
28 |
|
#include "util/rational.h" |
29 |
|
#include "util/string.h" |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
|
33 |
|
using namespace theory; |
34 |
|
using namespace theory::strings; |
35 |
|
|
36 |
|
namespace test { |
37 |
|
|
38 |
68 |
class TestTheoryWhiteSequencesRewriter : public TestSmt |
39 |
|
{ |
40 |
|
protected: |
41 |
34 |
void SetUp() override |
42 |
|
{ |
43 |
34 |
TestSmt::SetUp(); |
44 |
68 |
Options opts; |
45 |
34 |
d_rewriter = d_smtEngine->getRewriter(); |
46 |
34 |
d_seqRewriter.reset(new SequencesRewriter(d_rewriter, nullptr)); |
47 |
34 |
} |
48 |
|
|
49 |
|
Rewriter* d_rewriter; |
50 |
|
std::unique_ptr<SequencesRewriter> d_seqRewriter; |
51 |
|
|
52 |
4 |
void inNormalForm(Node t) |
53 |
|
{ |
54 |
8 |
Node res_t = d_rewriter->extendedRewrite(t); |
55 |
|
|
56 |
4 |
std::cout << std::endl; |
57 |
4 |
std::cout << t << " ---> " << res_t << std::endl; |
58 |
4 |
ASSERT_EQ(t, res_t); |
59 |
|
} |
60 |
|
|
61 |
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 |
2 |
StringsEntail& se = d_seqRewriter->getStringsEntail(); |
87 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
88 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
89 |
|
|
90 |
4 |
Node a = d_nodeManager->mkConst(::cvc5::String("A")); |
91 |
4 |
Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD")); |
92 |
4 |
Node aaad = d_nodeManager->mkConst(::cvc5::String("AAAD")); |
93 |
4 |
Node b = d_nodeManager->mkConst(::cvc5::String("B")); |
94 |
4 |
Node x = d_nodeManager->mkVar("x", strType); |
95 |
4 |
Node y = d_nodeManager->mkVar("y", strType); |
96 |
4 |
Node negOne = d_nodeManager->mkConst(Rational(-1)); |
97 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
98 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
99 |
4 |
Node two = d_nodeManager->mkConst(Rational(2)); |
100 |
4 |
Node three = d_nodeManager->mkConst(Rational(3)); |
101 |
4 |
Node i = d_nodeManager->mkVar("i", intType); |
102 |
|
|
103 |
2 |
ASSERT_TRUE(se.checkLengthOne(a)); |
104 |
2 |
ASSERT_TRUE(se.checkLengthOne(a, true)); |
105 |
|
|
106 |
4 |
Node substr = d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, one); |
107 |
2 |
ASSERT_TRUE(se.checkLengthOne(substr)); |
108 |
2 |
ASSERT_FALSE(se.checkLengthOne(substr, true)); |
109 |
|
|
110 |
2 |
substr = |
111 |
8 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, |
112 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, a, x), |
113 |
|
zero, |
114 |
|
one); |
115 |
2 |
ASSERT_TRUE(se.checkLengthOne(substr)); |
116 |
2 |
ASSERT_TRUE(se.checkLengthOne(substr, true)); |
117 |
|
|
118 |
2 |
substr = d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, two); |
119 |
2 |
ASSERT_FALSE(se.checkLengthOne(substr)); |
120 |
2 |
ASSERT_FALSE(se.checkLengthOne(substr, true)); |
121 |
|
} |
122 |
|
|
123 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_arith) |
124 |
|
{ |
125 |
2 |
ArithEntail& ae = d_seqRewriter->getArithEntail(); |
126 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
127 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
128 |
|
|
129 |
4 |
Node z = d_nodeManager->mkVar("z", strType); |
130 |
4 |
Node n = d_nodeManager->mkVar("n", intType); |
131 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
132 |
|
|
133 |
|
// 1 >= (str.len (str.substr z n 1)) ---> true |
134 |
2 |
Node substr_z = d_nodeManager->mkNode( |
135 |
|
kind::STRING_LENGTH, |
136 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, z, n, one)); |
137 |
2 |
ASSERT_TRUE(ae.check(one, substr_z)); |
138 |
|
|
139 |
|
// (str.len (str.substr z n 1)) >= 1 ---> false |
140 |
2 |
ASSERT_FALSE(ae.check(substr_z, one)); |
141 |
|
} |
142 |
|
|
143 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) |
144 |
|
{ |
145 |
2 |
ArithEntail& ae = d_seqRewriter->getArithEntail(); |
146 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
147 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
148 |
|
|
149 |
4 |
Node x = d_nodeManager->mkVar("x", intType); |
150 |
4 |
Node y = d_nodeManager->mkVar("y", strType); |
151 |
4 |
Node z = d_nodeManager->mkVar("z", intType); |
152 |
|
|
153 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
154 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
155 |
|
|
156 |
4 |
Node empty = d_nodeManager->mkConst(::cvc5::String("")); |
157 |
4 |
Node a = d_nodeManager->mkConst(::cvc5::String("A")); |
158 |
|
|
159 |
4 |
Node slen_y = d_nodeManager->mkNode(kind::STRING_LENGTH, y); |
160 |
4 |
Node x_plus_slen_y = d_nodeManager->mkNode(kind::PLUS, x, slen_y); |
161 |
|
Node x_plus_slen_y_eq_zero = d_rewriter->rewrite( |
162 |
4 |
d_nodeManager->mkNode(kind::EQUAL, x_plus_slen_y, zero)); |
163 |
|
|
164 |
|
// x + (str.len y) = 0 |= 0 >= x --> true |
165 |
2 |
ASSERT_TRUE(ae.checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, false)); |
166 |
|
|
167 |
|
// x + (str.len y) = 0 |= 0 > x --> false |
168 |
2 |
ASSERT_FALSE(ae.checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, true)); |
169 |
|
|
170 |
8 |
Node x_plus_slen_y_plus_z_eq_zero = d_rewriter->rewrite(d_nodeManager->mkNode( |
171 |
8 |
kind::EQUAL, d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, z), zero)); |
172 |
|
|
173 |
|
// x + (str.len y) + z = 0 |= 0 > x --> false |
174 |
2 |
ASSERT_FALSE( |
175 |
2 |
ae.checkWithAssumption(x_plus_slen_y_plus_z_eq_zero, zero, x, true)); |
176 |
|
|
177 |
|
Node x_plus_slen_y_plus_slen_y_eq_zero = |
178 |
8 |
d_rewriter->rewrite(d_nodeManager->mkNode( |
179 |
|
kind::EQUAL, |
180 |
4 |
d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, slen_y), |
181 |
4 |
zero)); |
182 |
|
|
183 |
|
// x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true |
184 |
2 |
ASSERT_TRUE(ae.checkWithAssumption( |
185 |
2 |
x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false)); |
186 |
|
|
187 |
4 |
Node five = d_nodeManager->mkConst(Rational(5)); |
188 |
4 |
Node six = d_nodeManager->mkConst(Rational(6)); |
189 |
4 |
Node x_plus_five = d_nodeManager->mkNode(kind::PLUS, x, five); |
190 |
|
Node x_plus_five_lt_six = |
191 |
4 |
d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six)); |
192 |
|
|
193 |
|
// x + 5 < 6 |= 0 >= x --> true |
194 |
2 |
ASSERT_TRUE(ae.checkWithAssumption(x_plus_five_lt_six, zero, x, false)); |
195 |
|
|
196 |
|
// x + 5 < 6 |= 0 > x --> false |
197 |
2 |
ASSERT_TRUE(!ae.checkWithAssumption(x_plus_five_lt_six, zero, x, true)); |
198 |
|
|
199 |
4 |
Node neg_x = d_nodeManager->mkNode(kind::UMINUS, x); |
200 |
|
Node x_plus_five_lt_five = |
201 |
4 |
d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, five)); |
202 |
|
|
203 |
|
// x + 5 < 5 |= -x >= 0 --> true |
204 |
2 |
ASSERT_TRUE(ae.checkWithAssumption(x_plus_five_lt_five, neg_x, zero, false)); |
205 |
|
|
206 |
|
// x + 5 < 5 |= 0 > x --> true |
207 |
2 |
ASSERT_TRUE(ae.checkWithAssumption(x_plus_five_lt_five, zero, x, false)); |
208 |
|
|
209 |
|
// 0 < x |= x >= (str.len (int.to.str x)) |
210 |
4 |
Node assm = d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, zero, x)); |
211 |
2 |
ASSERT_TRUE(ae.checkWithAssumption( |
212 |
|
assm, |
213 |
|
x, |
214 |
|
d_nodeManager->mkNode(kind::STRING_LENGTH, |
215 |
|
d_nodeManager->mkNode(kind::STRING_ITOS, x)), |
216 |
2 |
false)); |
217 |
|
} |
218 |
|
|
219 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) |
220 |
|
{ |
221 |
4 |
StringsRewriter sr(d_rewriter, nullptr); |
222 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
223 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
224 |
|
|
225 |
4 |
Node empty = d_nodeManager->mkConst(::cvc5::String("")); |
226 |
4 |
Node a = d_nodeManager->mkConst(::cvc5::String("A")); |
227 |
4 |
Node b = d_nodeManager->mkConst(::cvc5::String("B")); |
228 |
4 |
Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD")); |
229 |
4 |
Node negone = d_nodeManager->mkConst(Rational(-1)); |
230 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
231 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
232 |
4 |
Node two = d_nodeManager->mkConst(Rational(2)); |
233 |
4 |
Node three = d_nodeManager->mkConst(Rational(3)); |
234 |
|
|
235 |
4 |
Node s = d_nodeManager->mkVar("s", strType); |
236 |
4 |
Node s2 = d_nodeManager->mkVar("s2", strType); |
237 |
4 |
Node x = d_nodeManager->mkVar("x", intType); |
238 |
4 |
Node y = d_nodeManager->mkVar("y", intType); |
239 |
|
|
240 |
|
// (str.substr "A" x x) --> "" |
241 |
4 |
Node n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, x); |
242 |
4 |
Node res = sr.rewriteSubstr(n); |
243 |
2 |
ASSERT_EQ(res, empty); |
244 |
|
|
245 |
|
// (str.substr "A" (+ x 1) x) -> "" |
246 |
6 |
n = d_nodeManager->mkNode( |
247 |
|
kind::STRING_SUBSTR, |
248 |
|
a, |
249 |
4 |
d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))), |
250 |
|
x); |
251 |
2 |
res = sr.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 = sr.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 = sr.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 = sr.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 = sr.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 |
2 |
Node lhs = d_nodeManager->mkNode( |
296 |
|
kind::STRING_SUBSTR, |
297 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, empty, s, b), |
298 |
|
x, |
299 |
8 |
x); |
300 |
2 |
Node rhs = d_nodeManager->mkNode( |
301 |
|
kind::STRING_REPLACE, |
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 |
2 |
Node substr_repl = d_nodeManager->mkNode( |
313 |
|
kind::STRING_SUBSTR, |
314 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, s, a, b), |
315 |
|
zero, |
316 |
8 |
x); |
317 |
2 |
Node repl_substr = d_nodeManager->mkNode( |
318 |
|
kind::STRING_REPLACE, |
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 |
2 |
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_REPLACE, s, substr_y, b), |
337 |
|
zero, |
338 |
|
x); |
339 |
6 |
repl_substr = d_nodeManager->mkNode( |
340 |
|
kind::STRING_REPLACE, |
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 |
2 |
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 |
2 |
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_REPLACE, 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_REPLACE, 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_REPLACE, empty, x, substr_a); |
421 |
2 |
Node repl_substr_a = d_nodeManager->mkNode( |
422 |
4 |
kind::STRING_CONCAT, repl_e_x_s, substr_a, charat_a); |
423 |
2 |
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 |
2 |
d_nodeManager->mkNode(kind::STRING_CONCAT, |
451 |
|
abcd, |
452 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, x)); |
453 |
2 |
Node concat2 = d_nodeManager->mkNode( |
454 |
|
kind::STRING_CONCAT, |
455 |
4 |
{gh, x, d_nodeManager->mkNode(kind::STRING_REPLACE, x, gh, ij), ij}); |
456 |
4 |
Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1); |
457 |
4 |
Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2); |
458 |
2 |
ASSERT_EQ(res_concat1, res_concat2); |
459 |
|
} |
460 |
|
|
461 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf) |
462 |
|
{ |
463 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
464 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
465 |
|
|
466 |
4 |
Node a = d_nodeManager->mkConst(::cvc5::String("A")); |
467 |
4 |
Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD")); |
468 |
4 |
Node aaad = d_nodeManager->mkConst(::cvc5::String("AAAD")); |
469 |
4 |
Node b = d_nodeManager->mkConst(::cvc5::String("B")); |
470 |
4 |
Node c = d_nodeManager->mkConst(::cvc5::String("C")); |
471 |
4 |
Node ccc = d_nodeManager->mkConst(::cvc5::String("CCC")); |
472 |
4 |
Node x = d_nodeManager->mkVar("x", strType); |
473 |
4 |
Node y = d_nodeManager->mkVar("y", strType); |
474 |
4 |
Node negOne = d_nodeManager->mkConst(Rational(-1)); |
475 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
476 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
477 |
4 |
Node two = d_nodeManager->mkConst(Rational(2)); |
478 |
4 |
Node three = d_nodeManager->mkConst(Rational(3)); |
479 |
4 |
Node i = d_nodeManager->mkVar("i", intType); |
480 |
4 |
Node j = d_nodeManager->mkVar("j", intType); |
481 |
|
|
482 |
|
// Same normal form for: |
483 |
|
// |
484 |
|
// (str.to.int (str.indexof "A" x 1)) |
485 |
|
// |
486 |
|
// (str.to.int (str.indexof "B" x 1)) |
487 |
4 |
Node a_idof_x = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, x, two); |
488 |
4 |
Node itos_a_idof_x = d_nodeManager->mkNode(kind::STRING_ITOS, a_idof_x); |
489 |
4 |
Node b_idof_x = d_nodeManager->mkNode(kind::STRING_INDEXOF, b, x, two); |
490 |
4 |
Node itos_b_idof_x = d_nodeManager->mkNode(kind::STRING_ITOS, b_idof_x); |
491 |
2 |
sameNormalForm(itos_a_idof_x, itos_b_idof_x); |
492 |
|
|
493 |
|
// Same normal form for: |
494 |
|
// |
495 |
|
// (str.indexof (str.++ "ABCD" x) y 3) |
496 |
|
// |
497 |
|
// (str.indexof (str.++ "AAAD" x) y 3) |
498 |
|
Node idof_abcd = |
499 |
2 |
d_nodeManager->mkNode(kind::STRING_INDEXOF, |
500 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, abcd, x), |
501 |
|
y, |
502 |
8 |
three); |
503 |
|
Node idof_aaad = |
504 |
2 |
d_nodeManager->mkNode(kind::STRING_INDEXOF, |
505 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, aaad, x), |
506 |
|
y, |
507 |
8 |
three); |
508 |
2 |
sameNormalForm(idof_abcd, idof_aaad); |
509 |
|
|
510 |
|
// (str.indexof (str.substr x 1 i) "A" i) ---> -1 |
511 |
2 |
Node idof_substr = d_nodeManager->mkNode( |
512 |
|
kind::STRING_INDEXOF, |
513 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, i), |
514 |
|
a, |
515 |
8 |
i); |
516 |
2 |
sameNormalForm(idof_substr, negOne); |
517 |
|
|
518 |
|
{ |
519 |
|
// Same normal form for: |
520 |
|
// |
521 |
|
// (str.indexof (str.++ "B" "C" "A" x y) "A" 0) |
522 |
|
// |
523 |
|
// (+ 2 (str.indexof (str.++ "A" x y) "A" 0)) |
524 |
2 |
Node lhs = d_nodeManager->mkNode( |
525 |
|
kind::STRING_INDEXOF, |
526 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, {b, c, a, x, y}), |
527 |
|
a, |
528 |
8 |
zero); |
529 |
2 |
Node rhs = d_nodeManager->mkNode( |
530 |
|
kind::PLUS, |
531 |
|
two, |
532 |
8 |
d_nodeManager->mkNode( |
533 |
|
kind::STRING_INDEXOF, |
534 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, a, x, y), |
535 |
|
a, |
536 |
4 |
zero)); |
537 |
2 |
sameNormalForm(lhs, rhs); |
538 |
|
} |
539 |
2 |
} |
540 |
|
|
541 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace) |
542 |
|
{ |
543 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
544 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
545 |
|
|
546 |
4 |
Node empty = d_nodeManager->mkConst(::cvc5::String("")); |
547 |
4 |
Node a = d_nodeManager->mkConst(::cvc5::String("A")); |
548 |
4 |
Node ab = d_nodeManager->mkConst(::cvc5::String("AB")); |
549 |
4 |
Node b = d_nodeManager->mkConst(::cvc5::String("B")); |
550 |
4 |
Node c = d_nodeManager->mkConst(::cvc5::String("C")); |
551 |
4 |
Node d = d_nodeManager->mkConst(::cvc5::String("D")); |
552 |
4 |
Node x = d_nodeManager->mkVar("x", strType); |
553 |
4 |
Node y = d_nodeManager->mkVar("y", strType); |
554 |
4 |
Node z = d_nodeManager->mkVar("z", strType); |
555 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
556 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
557 |
4 |
Node n = d_nodeManager->mkVar("n", intType); |
558 |
|
|
559 |
|
// (str.replace (str.replace x "B" x) x "A") --> |
560 |
|
// (str.replace (str.replace x "B" "A") x "A") |
561 |
2 |
Node repl_repl = d_nodeManager->mkNode( |
562 |
|
kind::STRING_REPLACE, |
563 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, x), |
564 |
|
x, |
565 |
8 |
a); |
566 |
2 |
Node repl_repl_short = d_nodeManager->mkNode( |
567 |
|
kind::STRING_REPLACE, |
568 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, a), |
569 |
|
x, |
570 |
8 |
a); |
571 |
2 |
sameNormalForm(repl_repl, repl_repl_short); |
572 |
|
|
573 |
|
// (str.replace "A" (str.replace "B", x, "C") "D") --> "A" |
574 |
6 |
repl_repl = d_nodeManager->mkNode( |
575 |
|
kind::STRING_REPLACE, |
576 |
|
a, |
577 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, c), |
578 |
|
d); |
579 |
2 |
sameNormalForm(repl_repl, a); |
580 |
|
|
581 |
|
// (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A" |
582 |
6 |
repl_repl = d_nodeManager->mkNode( |
583 |
|
kind::STRING_REPLACE, |
584 |
|
a, |
585 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, a), |
586 |
|
d); |
587 |
2 |
differentNormalForms(repl_repl, a); |
588 |
|
|
589 |
|
// Same normal form for: |
590 |
|
// |
591 |
|
// (str.replace x (str.++ x y z) y) |
592 |
|
// |
593 |
|
// (str.replace x (str.++ x y z) z) |
594 |
4 |
Node xyz = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y, z); |
595 |
4 |
Node repl_x_xyz = d_nodeManager->mkNode(kind::STRING_REPLACE, x, xyz, y); |
596 |
4 |
Node repl_x_zyx = d_nodeManager->mkNode(kind::STRING_REPLACE, x, xyz, z); |
597 |
2 |
sameNormalForm(repl_x_xyz, repl_x_zyx); |
598 |
|
|
599 |
|
// (str.replace "" (str.++ x x) x) --> "" |
600 |
|
Node repl_empty_xx = |
601 |
2 |
d_nodeManager->mkNode(kind::STRING_REPLACE, |
602 |
|
empty, |
603 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, x), |
604 |
8 |
x); |
605 |
2 |
sameNormalForm(repl_empty_xx, empty); |
606 |
|
|
607 |
|
// (str.replace "AB" (str.++ x "A") x) --> (str.replace "AB" (str.++ x "A") |
608 |
|
// "") |
609 |
|
Node repl_ab_xa_x = |
610 |
2 |
d_nodeManager->mkNode(kind::STRING_REPLACE, |
611 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, a, b), |
612 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), |
613 |
12 |
x); |
614 |
|
Node repl_ab_xa_e = |
615 |
2 |
d_nodeManager->mkNode(kind::STRING_REPLACE, |
616 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, a, b), |
617 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), |
618 |
12 |
empty); |
619 |
2 |
sameNormalForm(repl_ab_xa_x, repl_ab_xa_e); |
620 |
|
|
621 |
|
// (str.replace "AB" (str.++ x "A") x) -/-> (str.replace "AB" (str.++ "A" x) |
622 |
|
// "") |
623 |
|
Node repl_ab_ax_e = |
624 |
2 |
d_nodeManager->mkNode(kind::STRING_REPLACE, |
625 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, a, b), |
626 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, a, x), |
627 |
12 |
empty); |
628 |
2 |
differentNormalForms(repl_ab_ax_e, repl_ab_xa_e); |
629 |
|
|
630 |
|
// (str.replace "" (str.replace y x "A") y) ---> "" |
631 |
6 |
repl_repl = d_nodeManager->mkNode( |
632 |
|
kind::STRING_REPLACE, |
633 |
|
empty, |
634 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, y, x, a), |
635 |
|
y); |
636 |
2 |
sameNormalForm(repl_repl, empty); |
637 |
|
|
638 |
|
// (str.replace "" (str.replace x y x) x) ---> "" |
639 |
6 |
repl_repl = d_nodeManager->mkNode( |
640 |
|
kind::STRING_REPLACE, |
641 |
|
empty, |
642 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x), |
643 |
|
x); |
644 |
2 |
sameNormalForm(repl_repl, empty); |
645 |
|
|
646 |
|
// (str.replace "" (str.substr x 0 1) x) ---> "" |
647 |
6 |
repl_repl = d_nodeManager->mkNode( |
648 |
|
kind::STRING_REPLACE, |
649 |
|
empty, |
650 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, one), |
651 |
|
x); |
652 |
2 |
sameNormalForm(repl_repl, empty); |
653 |
|
|
654 |
|
// Same normal form for: |
655 |
|
// |
656 |
|
// (str.replace "" (str.replace x y x) y) |
657 |
|
// |
658 |
|
// (str.replace "" x y) |
659 |
6 |
repl_repl = d_nodeManager->mkNode( |
660 |
|
kind::STRING_REPLACE, |
661 |
|
empty, |
662 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x), |
663 |
|
y); |
664 |
4 |
Node repl = d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, y); |
665 |
2 |
sameNormalForm(repl_repl, repl); |
666 |
|
|
667 |
|
// Same normal form: |
668 |
|
// |
669 |
|
// (str.replace "B" (str.replace x "A" "B") "B") |
670 |
|
// |
671 |
|
// (str.replace "B" x "B")) |
672 |
6 |
repl_repl = d_nodeManager->mkNode( |
673 |
|
kind::STRING_REPLACE, |
674 |
|
b, |
675 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b), |
676 |
|
b); |
677 |
2 |
repl = d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, b); |
678 |
2 |
sameNormalForm(repl_repl, repl); |
679 |
|
|
680 |
|
// Different normal forms for: |
681 |
|
// |
682 |
|
// (str.replace "B" (str.replace "" x "A") "B") |
683 |
|
// |
684 |
|
// (str.replace "B" x "B") |
685 |
6 |
repl_repl = d_nodeManager->mkNode( |
686 |
|
kind::STRING_REPLACE, |
687 |
|
b, |
688 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, a), |
689 |
|
b); |
690 |
2 |
repl = d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, b); |
691 |
2 |
differentNormalForms(repl_repl, repl); |
692 |
|
|
693 |
|
{ |
694 |
|
// Same normal form: |
695 |
|
// |
696 |
|
// (str.replace (str.++ "AB" x) "C" y) |
697 |
|
// |
698 |
|
// (str.++ "AB" (str.replace x "C" y)) |
699 |
|
Node lhs = |
700 |
2 |
d_nodeManager->mkNode(kind::STRING_REPLACE, |
701 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, ab, x), |
702 |
|
c, |
703 |
8 |
y); |
704 |
2 |
Node rhs = d_nodeManager->mkNode( |
705 |
|
kind::STRING_CONCAT, |
706 |
|
ab, |
707 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, c, y)); |
708 |
2 |
sameNormalForm(lhs, rhs); |
709 |
|
} |
710 |
2 |
} |
711 |
|
|
712 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) |
713 |
|
{ |
714 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
715 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
716 |
|
|
717 |
4 |
std::vector<Node> emptyVec; |
718 |
2 |
Node sigStar = d_nodeManager->mkNode( |
719 |
4 |
kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec)); |
720 |
4 |
Node foo = d_nodeManager->mkConst(String("FOO")); |
721 |
4 |
Node a = d_nodeManager->mkConst(String("A")); |
722 |
4 |
Node b = d_nodeManager->mkConst(String("B")); |
723 |
|
Node re = |
724 |
2 |
d_nodeManager->mkNode(kind::REGEXP_CONCAT, |
725 |
4 |
d_nodeManager->mkNode(kind::STRING_TO_REGEXP, a), |
726 |
|
sigStar, |
727 |
8 |
d_nodeManager->mkNode(kind::STRING_TO_REGEXP, b)); |
728 |
|
|
729 |
|
// Same normal form: |
730 |
|
// |
731 |
|
// (str.replace_re |
732 |
|
// "AZZZB" |
733 |
|
// (re.++ (str.to_re "A") re.all (str.to_re "B")) |
734 |
|
// "FOO") |
735 |
|
// |
736 |
|
// "FOO" |
737 |
|
{ |
738 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, |
739 |
4 |
d_nodeManager->mkConst(String("AZZZB")), |
740 |
|
re, |
741 |
8 |
foo); |
742 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("FOO")); |
743 |
2 |
sameNormalForm(t, res); |
744 |
|
} |
745 |
|
|
746 |
|
// Same normal form: |
747 |
|
// |
748 |
|
// (str.replace_re |
749 |
|
// "ZAZZZBZZB" |
750 |
|
// (re.++ (str.to_re "A") re.all (str.to_re "B")) |
751 |
|
// "FOO") |
752 |
|
// |
753 |
|
// "ZFOOZZB" |
754 |
|
{ |
755 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, |
756 |
4 |
d_nodeManager->mkConst(String("ZAZZZBZZB")), |
757 |
|
re, |
758 |
8 |
foo); |
759 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("ZFOOZZB")); |
760 |
2 |
sameNormalForm(t, res); |
761 |
|
} |
762 |
|
|
763 |
|
// Same normal form: |
764 |
|
// |
765 |
|
// (str.replace_re |
766 |
|
// "ZAZZZBZAZB" |
767 |
|
// (re.++ (str.to_re "A") re.all (str.to_re "B")) |
768 |
|
// "FOO") |
769 |
|
// |
770 |
|
// "ZFOOZAZB" |
771 |
|
{ |
772 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, |
773 |
4 |
d_nodeManager->mkConst(String("ZAZZZBZAZB")), |
774 |
|
re, |
775 |
8 |
foo); |
776 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("ZFOOZAZB")); |
777 |
2 |
sameNormalForm(t, res); |
778 |
|
} |
779 |
|
|
780 |
|
// Same normal form: |
781 |
|
// |
782 |
|
// (str.replace_re |
783 |
|
// "ZZZ" |
784 |
|
// (re.++ (str.to_re "A") re.all (str.to_re "B")) |
785 |
|
// "FOO") |
786 |
|
// |
787 |
|
// "ZZZ" |
788 |
|
{ |
789 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, |
790 |
4 |
d_nodeManager->mkConst(String("ZZZ")), |
791 |
|
re, |
792 |
8 |
foo); |
793 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("ZZZ")); |
794 |
2 |
sameNormalForm(t, res); |
795 |
|
} |
796 |
|
|
797 |
|
// Same normal form: |
798 |
|
// |
799 |
|
// (str.replace_re |
800 |
|
// "ZZZ" |
801 |
|
// re.all |
802 |
|
// "FOO") |
803 |
|
// |
804 |
|
// "FOOZZZ" |
805 |
|
{ |
806 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, |
807 |
4 |
d_nodeManager->mkConst(String("ZZZ")), |
808 |
|
sigStar, |
809 |
8 |
foo); |
810 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("FOOZZZ")); |
811 |
2 |
sameNormalForm(t, res); |
812 |
|
} |
813 |
|
|
814 |
|
// Same normal form: |
815 |
|
// |
816 |
|
// (str.replace_re |
817 |
|
// "" |
818 |
|
// re.all |
819 |
|
// "FOO") |
820 |
|
// |
821 |
|
// "FOO" |
822 |
|
{ |
823 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, |
824 |
4 |
d_nodeManager->mkConst(String("")), |
825 |
|
sigStar, |
826 |
8 |
foo); |
827 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("FOO")); |
828 |
2 |
sameNormalForm(t, res); |
829 |
|
} |
830 |
2 |
} |
831 |
|
|
832 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) |
833 |
|
{ |
834 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
835 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
836 |
|
|
837 |
4 |
std::vector<Node> emptyVec; |
838 |
2 |
Node sigStar = d_nodeManager->mkNode( |
839 |
4 |
kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec)); |
840 |
4 |
Node foo = d_nodeManager->mkConst(String("FOO")); |
841 |
4 |
Node a = d_nodeManager->mkConst(String("A")); |
842 |
4 |
Node b = d_nodeManager->mkConst(String("B")); |
843 |
|
Node re = |
844 |
2 |
d_nodeManager->mkNode(kind::REGEXP_CONCAT, |
845 |
4 |
d_nodeManager->mkNode(kind::STRING_TO_REGEXP, a), |
846 |
|
sigStar, |
847 |
8 |
d_nodeManager->mkNode(kind::STRING_TO_REGEXP, b)); |
848 |
|
|
849 |
|
// Same normal form: |
850 |
|
// |
851 |
|
// (str.replace_re |
852 |
|
// "AZZZB" |
853 |
|
// (re.++ (str.to_re "A") re.all (str.to_re "B")) |
854 |
|
// "FOO") |
855 |
|
// |
856 |
|
// "FOO" |
857 |
|
{ |
858 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, |
859 |
4 |
d_nodeManager->mkConst(String("AZZZB")), |
860 |
|
re, |
861 |
8 |
foo); |
862 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("FOO")); |
863 |
2 |
sameNormalForm(t, res); |
864 |
|
} |
865 |
|
|
866 |
|
// Same normal form: |
867 |
|
// |
868 |
|
// (str.replace_re |
869 |
|
// "ZAZZZBZZB" |
870 |
|
// (re.++ (str.to_re "A") re.all (str.to_re "B")) |
871 |
|
// "FOO") |
872 |
|
// |
873 |
|
// "ZFOOZZB" |
874 |
|
{ |
875 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, |
876 |
4 |
d_nodeManager->mkConst(String("ZAZZZBZZB")), |
877 |
|
re, |
878 |
8 |
foo); |
879 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("ZFOOZZB")); |
880 |
2 |
sameNormalForm(t, res); |
881 |
|
} |
882 |
|
|
883 |
|
// Same normal form: |
884 |
|
// |
885 |
|
// (str.replace_re |
886 |
|
// "ZAZZZBZAZB" |
887 |
|
// (re.++ (str.to_re "A") re.all (str.to_re "B")) |
888 |
|
// "FOO") |
889 |
|
// |
890 |
|
// "ZFOOZFOO" |
891 |
|
{ |
892 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, |
893 |
4 |
d_nodeManager->mkConst(String("ZAZZZBZAZB")), |
894 |
|
re, |
895 |
8 |
foo); |
896 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("ZFOOZFOO")); |
897 |
2 |
sameNormalForm(t, res); |
898 |
|
} |
899 |
|
|
900 |
|
// Same normal form: |
901 |
|
// |
902 |
|
// (str.replace_re |
903 |
|
// "ZZZ" |
904 |
|
// (re.++ (str.to_re "A") re.all (str.to_re "B")) |
905 |
|
// "FOO") |
906 |
|
// |
907 |
|
// "ZZZ" |
908 |
|
{ |
909 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, |
910 |
4 |
d_nodeManager->mkConst(String("ZZZ")), |
911 |
|
re, |
912 |
8 |
foo); |
913 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("ZZZ")); |
914 |
2 |
sameNormalForm(t, res); |
915 |
|
} |
916 |
|
|
917 |
|
// Same normal form: |
918 |
|
// |
919 |
|
// (str.replace_re |
920 |
|
// "ZZZ" |
921 |
|
// re.all |
922 |
|
// "FOO") |
923 |
|
// |
924 |
|
// "FOOFOOFOO" |
925 |
|
{ |
926 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, |
927 |
4 |
d_nodeManager->mkConst(String("ZZZ")), |
928 |
|
sigStar, |
929 |
8 |
foo); |
930 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("FOOFOOFOO")); |
931 |
2 |
sameNormalForm(t, res); |
932 |
|
} |
933 |
|
|
934 |
|
// Same normal form: |
935 |
|
// |
936 |
|
// (str.replace_re |
937 |
|
// "" |
938 |
|
// re.all |
939 |
|
// "FOO") |
940 |
|
// |
941 |
|
// "" |
942 |
|
{ |
943 |
2 |
Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, |
944 |
4 |
d_nodeManager->mkConst(String("")), |
945 |
|
sigStar, |
946 |
8 |
foo); |
947 |
4 |
Node res = d_nodeManager->mkConst(::cvc5::String("")); |
948 |
2 |
sameNormalForm(t, res); |
949 |
|
} |
950 |
2 |
} |
951 |
|
|
952 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains) |
953 |
|
{ |
954 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
955 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
956 |
|
|
957 |
4 |
Node empty = d_nodeManager->mkConst(::cvc5::String("")); |
958 |
4 |
Node a = d_nodeManager->mkConst(::cvc5::String("A")); |
959 |
4 |
Node ab = d_nodeManager->mkConst(::cvc5::String("AB")); |
960 |
4 |
Node b = d_nodeManager->mkConst(::cvc5::String("B")); |
961 |
4 |
Node c = d_nodeManager->mkConst(::cvc5::String("C")); |
962 |
4 |
Node e = d_nodeManager->mkConst(::cvc5::String("E")); |
963 |
4 |
Node h = d_nodeManager->mkConst(::cvc5::String("H")); |
964 |
4 |
Node j = d_nodeManager->mkConst(::cvc5::String("J")); |
965 |
4 |
Node p = d_nodeManager->mkConst(::cvc5::String("P")); |
966 |
4 |
Node abc = d_nodeManager->mkConst(::cvc5::String("ABC")); |
967 |
4 |
Node def = d_nodeManager->mkConst(::cvc5::String("DEF")); |
968 |
4 |
Node ghi = d_nodeManager->mkConst(::cvc5::String("GHI")); |
969 |
4 |
Node x = d_nodeManager->mkVar("x", strType); |
970 |
4 |
Node y = d_nodeManager->mkVar("y", strType); |
971 |
4 |
Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); |
972 |
4 |
Node yx = d_nodeManager->mkNode(kind::STRING_CONCAT, y, x); |
973 |
4 |
Node z = d_nodeManager->mkVar("z", strType); |
974 |
4 |
Node n = d_nodeManager->mkVar("n", intType); |
975 |
4 |
Node m = d_nodeManager->mkVar("m", intType); |
976 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
977 |
4 |
Node two = d_nodeManager->mkConst(Rational(2)); |
978 |
4 |
Node three = d_nodeManager->mkConst(Rational(3)); |
979 |
4 |
Node four = d_nodeManager->mkConst(Rational(4)); |
980 |
4 |
Node t = d_nodeManager->mkConst(true); |
981 |
4 |
Node f = d_nodeManager->mkConst(false); |
982 |
|
|
983 |
|
// Same normal form for: |
984 |
|
// |
985 |
|
// (str.replace "A" (str.substr x 1 3) y z) |
986 |
|
// |
987 |
|
// (str.replace "A" (str.substr x 1 4) y z) |
988 |
2 |
Node substr_3 = d_nodeManager->mkNode( |
989 |
|
kind::STRING_REPLACE, |
990 |
|
a, |
991 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three), |
992 |
8 |
z); |
993 |
2 |
Node substr_4 = d_nodeManager->mkNode( |
994 |
|
kind::STRING_REPLACE, |
995 |
|
a, |
996 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, four), |
997 |
8 |
z); |
998 |
2 |
sameNormalForm(substr_3, substr_4); |
999 |
|
|
1000 |
|
// Same normal form for: |
1001 |
|
// |
1002 |
|
// (str.replace "A" (str.++ y (str.substr x 1 3)) y z) |
1003 |
|
// |
1004 |
|
// (str.replace "A" (str.++ y (str.substr x 1 4)) y z) |
1005 |
2 |
Node concat_substr_3 = d_nodeManager->mkNode( |
1006 |
|
kind::STRING_REPLACE, |
1007 |
|
a, |
1008 |
6 |
d_nodeManager->mkNode( |
1009 |
|
kind::STRING_CONCAT, |
1010 |
|
y, |
1011 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three)), |
1012 |
8 |
z); |
1013 |
2 |
Node concat_substr_4 = d_nodeManager->mkNode( |
1014 |
|
kind::STRING_REPLACE, |
1015 |
|
a, |
1016 |
6 |
d_nodeManager->mkNode( |
1017 |
|
kind::STRING_CONCAT, |
1018 |
|
y, |
1019 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, four)), |
1020 |
8 |
z); |
1021 |
2 |
sameNormalForm(concat_substr_3, concat_substr_4); |
1022 |
|
|
1023 |
|
// (str.contains "A" (str.++ a (str.replace "B", x, "C")) --> false |
1024 |
2 |
Node ctn_repl = d_nodeManager->mkNode( |
1025 |
|
kind::STRING_CONTAINS, |
1026 |
|
a, |
1027 |
6 |
d_nodeManager->mkNode( |
1028 |
|
kind::STRING_CONCAT, |
1029 |
|
a, |
1030 |
8 |
d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, c))); |
1031 |
2 |
sameNormalForm(ctn_repl, f); |
1032 |
|
|
1033 |
|
// (str.contains x (str.++ x x)) --> (= x "") |
1034 |
2 |
Node x_cnts_x_x = d_nodeManager->mkNode( |
1035 |
4 |
kind::STRING_CONTAINS, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, x)); |
1036 |
2 |
sameNormalForm(x_cnts_x_x, d_nodeManager->mkNode(kind::EQUAL, x, empty)); |
1037 |
|
|
1038 |
|
// Same normal form for: |
1039 |
|
// |
1040 |
|
// (str.contains (str.++ y x) (str.++ x z y)) |
1041 |
|
// |
1042 |
|
// (and (str.contains (str.++ y x) (str.++ x y)) (= z "")) |
1043 |
2 |
Node yx_cnts_xzy = d_nodeManager->mkNode( |
1044 |
|
kind::STRING_CONTAINS, |
1045 |
|
yx, |
1046 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, z, y)); |
1047 |
|
Node yx_cnts_xy = |
1048 |
2 |
d_nodeManager->mkNode(kind::AND, |
1049 |
4 |
d_nodeManager->mkNode(kind::EQUAL, z, empty), |
1050 |
8 |
d_nodeManager->mkNode(kind::STRING_CONTAINS, yx, xy)); |
1051 |
2 |
sameNormalForm(yx_cnts_xzy, yx_cnts_xy); |
1052 |
|
|
1053 |
|
// Same normal form for: |
1054 |
|
// |
1055 |
|
// (str.contains (str.substr x n (str.len y)) y) |
1056 |
|
// |
1057 |
|
// (= (str.substr x n (str.len y)) y) |
1058 |
2 |
Node ctn_substr = d_nodeManager->mkNode( |
1059 |
|
kind::STRING_CONTAINS, |
1060 |
6 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, |
1061 |
|
x, |
1062 |
|
n, |
1063 |
4 |
d_nodeManager->mkNode(kind::STRING_LENGTH, y)), |
1064 |
8 |
y); |
1065 |
2 |
Node substr_eq = d_nodeManager->mkNode( |
1066 |
|
kind::EQUAL, |
1067 |
6 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, |
1068 |
|
x, |
1069 |
|
n, |
1070 |
4 |
d_nodeManager->mkNode(kind::STRING_LENGTH, y)), |
1071 |
8 |
y); |
1072 |
2 |
sameNormalForm(ctn_substr, substr_eq); |
1073 |
|
|
1074 |
|
// Same normal form for: |
1075 |
|
// |
1076 |
|
// (str.contains x (str.replace y x y)) |
1077 |
|
// |
1078 |
|
// (str.contains x y) |
1079 |
2 |
Node ctn_repl_y_x_y = d_nodeManager->mkNode( |
1080 |
|
kind::STRING_CONTAINS, |
1081 |
|
x, |
1082 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, y, x, y)); |
1083 |
4 |
Node ctn_x_y = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, y); |
1084 |
2 |
sameNormalForm(ctn_repl_y_x_y, ctn_repl_y_x_y); |
1085 |
|
|
1086 |
|
// Same normal form for: |
1087 |
|
// |
1088 |
|
// (str.contains x (str.replace x y x)) |
1089 |
|
// |
1090 |
|
// (= x (str.replace x y x)) |
1091 |
2 |
Node ctn_repl_self = d_nodeManager->mkNode( |
1092 |
|
kind::STRING_CONTAINS, |
1093 |
|
x, |
1094 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x)); |
1095 |
2 |
Node eq_repl = d_nodeManager->mkNode( |
1096 |
4 |
kind::EQUAL, x, d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x)); |
1097 |
2 |
sameNormalForm(ctn_repl_self, eq_repl); |
1098 |
|
|
1099 |
|
// (str.contains x (str.++ "A" (str.replace x y x))) ---> false |
1100 |
2 |
Node ctn_repl_self_f = d_nodeManager->mkNode( |
1101 |
|
kind::STRING_CONTAINS, |
1102 |
|
x, |
1103 |
6 |
d_nodeManager->mkNode( |
1104 |
|
kind::STRING_CONCAT, |
1105 |
|
a, |
1106 |
8 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x))); |
1107 |
2 |
sameNormalForm(ctn_repl_self_f, f); |
1108 |
|
|
1109 |
|
// Same normal form for: |
1110 |
|
// |
1111 |
|
// (str.contains x (str.replace "" x y)) |
1112 |
|
// |
1113 |
|
// (= "" (str.replace "" x y)) |
1114 |
2 |
Node ctn_repl_empty = d_nodeManager->mkNode( |
1115 |
|
kind::STRING_CONTAINS, |
1116 |
|
x, |
1117 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, y)); |
1118 |
2 |
Node eq_repl_empty = d_nodeManager->mkNode( |
1119 |
|
kind::EQUAL, |
1120 |
|
empty, |
1121 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, y)); |
1122 |
2 |
sameNormalForm(ctn_repl_empty, eq_repl_empty); |
1123 |
|
|
1124 |
|
// Same normal form for: |
1125 |
|
// |
1126 |
|
// (str.contains x (str.++ x y)) |
1127 |
|
// |
1128 |
|
// (= "" y) |
1129 |
2 |
Node ctn_x_x_y = d_nodeManager->mkNode( |
1130 |
4 |
kind::STRING_CONTAINS, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, y)); |
1131 |
4 |
Node eq_emp_y = d_nodeManager->mkNode(kind::EQUAL, empty, y); |
1132 |
2 |
sameNormalForm(ctn_x_x_y, eq_emp_y); |
1133 |
|
|
1134 |
|
// Same normal form for: |
1135 |
|
// |
1136 |
|
// (str.contains (str.++ y x) (str.++ x y)) |
1137 |
|
// |
1138 |
|
// (= (str.++ y x) (str.++ x y)) |
1139 |
4 |
Node ctn_yxxy = d_nodeManager->mkNode(kind::STRING_CONTAINS, yx, xy); |
1140 |
4 |
Node eq_yxxy = d_nodeManager->mkNode(kind::EQUAL, yx, xy); |
1141 |
2 |
sameNormalForm(ctn_yxxy, eq_yxxy); |
1142 |
|
|
1143 |
|
// (str.contains (str.replace x y x) x) ---> true |
1144 |
6 |
ctn_repl = d_nodeManager->mkNode( |
1145 |
|
kind::STRING_CONTAINS, |
1146 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x), |
1147 |
|
x); |
1148 |
2 |
sameNormalForm(ctn_repl, t); |
1149 |
|
|
1150 |
|
// (str.contains (str.replace (str.++ x y) z (str.++ y x)) x) ---> true |
1151 |
6 |
ctn_repl = d_nodeManager->mkNode( |
1152 |
|
kind::STRING_CONTAINS, |
1153 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, xy, z, yx), |
1154 |
|
x); |
1155 |
2 |
sameNormalForm(ctn_repl, t); |
1156 |
|
|
1157 |
|
// (str.contains (str.++ z (str.replace (str.++ x y) z (str.++ y x))) x) |
1158 |
|
// ---> true |
1159 |
6 |
ctn_repl = d_nodeManager->mkNode( |
1160 |
|
kind::STRING_CONTAINS, |
1161 |
6 |
d_nodeManager->mkNode( |
1162 |
|
kind::STRING_CONCAT, |
1163 |
|
z, |
1164 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, xy, z, yx)), |
1165 |
|
x); |
1166 |
2 |
sameNormalForm(ctn_repl, t); |
1167 |
|
|
1168 |
|
// Same normal form for: |
1169 |
|
// |
1170 |
|
// (str.contains (str.replace x y x) y) |
1171 |
|
// |
1172 |
|
// (str.contains x y) |
1173 |
2 |
Node lhs = d_nodeManager->mkNode( |
1174 |
|
kind::STRING_CONTAINS, |
1175 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x), |
1176 |
8 |
y); |
1177 |
4 |
Node rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, y); |
1178 |
2 |
sameNormalForm(lhs, rhs); |
1179 |
|
|
1180 |
|
// Same normal form for: |
1181 |
|
// |
1182 |
|
// (str.contains (str.replace x y x) "B") |
1183 |
|
// |
1184 |
|
// (str.contains x "B") |
1185 |
6 |
lhs = d_nodeManager->mkNode( |
1186 |
|
kind::STRING_CONTAINS, |
1187 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x), |
1188 |
|
b); |
1189 |
2 |
rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, b); |
1190 |
2 |
sameNormalForm(lhs, rhs); |
1191 |
|
|
1192 |
|
// Same normal form for: |
1193 |
|
// |
1194 |
|
// (str.contains (str.replace x y x) (str.substr z n 1)) |
1195 |
|
// |
1196 |
|
// (str.contains x (str.substr z n 1)) |
1197 |
4 |
Node substr_z = d_nodeManager->mkNode(kind::STRING_SUBSTR, z, n, one); |
1198 |
6 |
lhs = d_nodeManager->mkNode( |
1199 |
|
kind::STRING_CONTAINS, |
1200 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x), |
1201 |
|
substr_z); |
1202 |
2 |
rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, substr_z); |
1203 |
2 |
sameNormalForm(lhs, rhs); |
1204 |
|
|
1205 |
|
// Same normal form for: |
1206 |
|
// |
1207 |
|
// (str.contains (str.replace x y z) z) |
1208 |
|
// |
1209 |
|
// (str.contains (str.replace x z y) y) |
1210 |
6 |
lhs = d_nodeManager->mkNode( |
1211 |
|
kind::STRING_CONTAINS, |
1212 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, z), |
1213 |
|
z); |
1214 |
6 |
rhs = d_nodeManager->mkNode( |
1215 |
|
kind::STRING_CONTAINS, |
1216 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, z, y), |
1217 |
|
y); |
1218 |
2 |
sameNormalForm(lhs, rhs); |
1219 |
|
|
1220 |
|
// Same normal form for: |
1221 |
|
// |
1222 |
|
// (str.contains (str.replace x "A" "B") "A") |
1223 |
|
// |
1224 |
|
// (str.contains (str.replace x "A" "") "A") |
1225 |
6 |
lhs = d_nodeManager->mkNode( |
1226 |
|
kind::STRING_CONTAINS, |
1227 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b), |
1228 |
|
a); |
1229 |
6 |
rhs = d_nodeManager->mkNode( |
1230 |
|
kind::STRING_CONTAINS, |
1231 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, empty), |
1232 |
|
a); |
1233 |
2 |
sameNormalForm(lhs, rhs); |
1234 |
|
|
1235 |
|
{ |
1236 |
|
// (str.contains (str.++ x "A") (str.++ "B" x)) ---> false |
1237 |
|
Node ctn = |
1238 |
2 |
d_nodeManager->mkNode(kind::STRING_CONTAINS, |
1239 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), |
1240 |
8 |
d_nodeManager->mkNode(kind::STRING_CONCAT, b, x)); |
1241 |
2 |
sameNormalForm(ctn, f); |
1242 |
|
} |
1243 |
|
|
1244 |
|
{ |
1245 |
|
// Same normal form for: |
1246 |
|
// |
1247 |
|
// (str.contains (str.replace x "ABC" "DEF") "GHI") |
1248 |
|
// |
1249 |
|
// (str.contains x "GHI") |
1250 |
6 |
lhs = d_nodeManager->mkNode( |
1251 |
|
kind::STRING_CONTAINS, |
1252 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, abc, def), |
1253 |
|
ghi); |
1254 |
2 |
rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, ghi); |
1255 |
2 |
sameNormalForm(lhs, rhs); |
1256 |
|
} |
1257 |
|
|
1258 |
|
{ |
1259 |
|
// Different normal forms for: |
1260 |
|
// |
1261 |
|
// (str.contains (str.replace x "ABC" "DEF") "B") |
1262 |
|
// |
1263 |
|
// (str.contains x "B") |
1264 |
6 |
lhs = d_nodeManager->mkNode( |
1265 |
|
kind::STRING_CONTAINS, |
1266 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, abc, def), |
1267 |
|
b); |
1268 |
2 |
rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, b); |
1269 |
2 |
differentNormalForms(lhs, rhs); |
1270 |
|
} |
1271 |
|
|
1272 |
|
{ |
1273 |
|
// Different normal forms for: |
1274 |
|
// |
1275 |
|
// (str.contains (str.replace x "B" "DEF") "ABC") |
1276 |
|
// |
1277 |
|
// (str.contains x "ABC") |
1278 |
6 |
lhs = d_nodeManager->mkNode( |
1279 |
|
kind::STRING_CONTAINS, |
1280 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, def), |
1281 |
|
abc); |
1282 |
2 |
rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, abc); |
1283 |
2 |
differentNormalForms(lhs, rhs); |
1284 |
|
} |
1285 |
|
|
1286 |
|
{ |
1287 |
|
// Same normal form for: |
1288 |
|
// |
1289 |
|
// (str.contains "ABC" (str.at x n)) |
1290 |
|
// |
1291 |
|
// (or (= x "") |
1292 |
|
// (= x "A") (= x "B") (= x "C")) |
1293 |
4 |
Node cat = d_nodeManager->mkNode(kind::STRING_CHARAT, x, n); |
1294 |
2 |
lhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, abc, cat); |
1295 |
18 |
rhs = d_nodeManager->mkNode(kind::OR, |
1296 |
4 |
{d_nodeManager->mkNode(kind::EQUAL, cat, empty), |
1297 |
4 |
d_nodeManager->mkNode(kind::EQUAL, cat, a), |
1298 |
4 |
d_nodeManager->mkNode(kind::EQUAL, cat, b), |
1299 |
12 |
d_nodeManager->mkNode(kind::EQUAL, cat, c)}); |
1300 |
2 |
sameNormalForm(lhs, rhs); |
1301 |
|
} |
1302 |
2 |
} |
1303 |
|
|
1304 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, infer_eqs_from_contains) |
1305 |
|
{ |
1306 |
2 |
StringsEntail& se = d_seqRewriter->getStringsEntail(); |
1307 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
1308 |
|
|
1309 |
4 |
Node empty = d_nodeManager->mkConst(::cvc5::String("")); |
1310 |
4 |
Node a = d_nodeManager->mkConst(::cvc5::String("A")); |
1311 |
4 |
Node b = d_nodeManager->mkConst(::cvc5::String("B")); |
1312 |
4 |
Node x = d_nodeManager->mkVar("x", strType); |
1313 |
4 |
Node y = d_nodeManager->mkVar("y", strType); |
1314 |
4 |
Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); |
1315 |
4 |
Node f = d_nodeManager->mkConst(false); |
1316 |
|
|
1317 |
|
// inferEqsFromContains("", (str.++ x y)) returns something equivalent to |
1318 |
|
// (= "" y) |
1319 |
|
Node empty_x_y = |
1320 |
2 |
d_nodeManager->mkNode(kind::AND, |
1321 |
4 |
d_nodeManager->mkNode(kind::EQUAL, empty, x), |
1322 |
8 |
d_nodeManager->mkNode(kind::EQUAL, empty, y)); |
1323 |
2 |
sameNormalForm(se.inferEqsFromContains(empty, xy), empty_x_y); |
1324 |
|
|
1325 |
|
// inferEqsFromContains(x, (str.++ x y)) returns false |
1326 |
4 |
Node bxya = d_nodeManager->mkNode(kind::STRING_CONCAT, {b, y, x, a}); |
1327 |
2 |
sameNormalForm(se.inferEqsFromContains(x, bxya), f); |
1328 |
|
|
1329 |
|
// inferEqsFromContains(x, y) returns null |
1330 |
4 |
Node n = se.inferEqsFromContains(x, y); |
1331 |
2 |
ASSERT_TRUE(n.isNull()); |
1332 |
|
|
1333 |
|
// inferEqsFromContains(x, x) returns something equivalent to (= x x) |
1334 |
4 |
Node eq_x_x = d_nodeManager->mkNode(kind::EQUAL, x, x); |
1335 |
2 |
sameNormalForm(se.inferEqsFromContains(x, x), eq_x_x); |
1336 |
|
|
1337 |
|
// inferEqsFromContains((str.replace x "B" "A"), x) returns something |
1338 |
|
// equivalent to (= (str.replace x "B" "A") x) |
1339 |
4 |
Node repl = d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, a); |
1340 |
4 |
Node eq_repl_x = d_nodeManager->mkNode(kind::EQUAL, repl, x); |
1341 |
2 |
sameNormalForm(se.inferEqsFromContains(repl, x), eq_repl_x); |
1342 |
|
|
1343 |
|
// inferEqsFromContains(x, (str.replace x "B" "A")) returns something |
1344 |
|
// equivalent to (= (str.replace x "B" "A") x) |
1345 |
4 |
Node eq_x_repl = d_nodeManager->mkNode(kind::EQUAL, x, repl); |
1346 |
2 |
sameNormalForm(se.inferEqsFromContains(x, repl), eq_x_repl); |
1347 |
|
} |
1348 |
|
|
1349 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_prefix_suffix) |
1350 |
|
{ |
1351 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
1352 |
|
|
1353 |
4 |
Node empty = d_nodeManager->mkConst(::cvc5::String("")); |
1354 |
4 |
Node a = d_nodeManager->mkConst(::cvc5::String("A")); |
1355 |
4 |
Node x = d_nodeManager->mkVar("x", strType); |
1356 |
4 |
Node y = d_nodeManager->mkVar("y", strType); |
1357 |
4 |
Node xx = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x); |
1358 |
4 |
Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a); |
1359 |
4 |
Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); |
1360 |
4 |
Node f = d_nodeManager->mkConst(false); |
1361 |
|
|
1362 |
|
// Same normal form for: |
1363 |
|
// |
1364 |
|
// (str.prefix (str.++ x y) x) |
1365 |
|
// |
1366 |
|
// (= y "") |
1367 |
4 |
Node p_xy = d_nodeManager->mkNode(kind::STRING_PREFIX, xy, x); |
1368 |
4 |
Node empty_y = d_nodeManager->mkNode(kind::EQUAL, y, empty); |
1369 |
2 |
sameNormalForm(p_xy, empty_y); |
1370 |
|
|
1371 |
|
// Same normal form for: |
1372 |
|
// |
1373 |
|
// (str.suffix (str.++ x x) x) |
1374 |
|
// |
1375 |
|
// (= x "") |
1376 |
4 |
Node p_xx = d_nodeManager->mkNode(kind::STRING_SUFFIX, xx, x); |
1377 |
4 |
Node empty_x = d_nodeManager->mkNode(kind::EQUAL, x, empty); |
1378 |
2 |
sameNormalForm(p_xx, empty_x); |
1379 |
|
|
1380 |
|
// (str.suffix x (str.++ x x "A")) ---> false |
1381 |
4 |
Node p_xxa = d_nodeManager->mkNode(kind::STRING_SUFFIX, xxa, x); |
1382 |
2 |
sameNormalForm(p_xxa, f); |
1383 |
2 |
} |
1384 |
|
|
1385 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext) |
1386 |
|
{ |
1387 |
4 |
TypeNode strType = d_nodeManager->stringType(); |
1388 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
1389 |
|
|
1390 |
4 |
Node empty = d_nodeManager->mkConst(::cvc5::String("")); |
1391 |
4 |
Node a = d_nodeManager->mkConst(::cvc5::String("A")); |
1392 |
4 |
Node aaa = d_nodeManager->mkConst(::cvc5::String("AAA")); |
1393 |
4 |
Node b = d_nodeManager->mkConst(::cvc5::String("B")); |
1394 |
4 |
Node ba = d_nodeManager->mkConst(::cvc5::String("BA")); |
1395 |
4 |
Node w = d_nodeManager->mkVar("w", strType); |
1396 |
4 |
Node x = d_nodeManager->mkVar("x", strType); |
1397 |
4 |
Node y = d_nodeManager->mkVar("y", strType); |
1398 |
4 |
Node z = d_nodeManager->mkVar("z", strType); |
1399 |
4 |
Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a); |
1400 |
4 |
Node f = d_nodeManager->mkConst(false); |
1401 |
4 |
Node n = d_nodeManager->mkVar("n", intType); |
1402 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
1403 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
1404 |
4 |
Node three = d_nodeManager->mkConst(Rational(3)); |
1405 |
|
|
1406 |
|
// Same normal form for: |
1407 |
|
// |
1408 |
|
// (= "" (str.replace "" x "B")) |
1409 |
|
// |
1410 |
|
// (not (= x "")) |
1411 |
2 |
Node empty_repl = d_nodeManager->mkNode( |
1412 |
|
kind::EQUAL, |
1413 |
|
empty, |
1414 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, b)); |
1415 |
2 |
Node empty_x = d_nodeManager->mkNode( |
1416 |
4 |
kind::NOT, d_nodeManager->mkNode(kind::EQUAL, x, empty)); |
1417 |
2 |
sameNormalForm(empty_repl, empty_x); |
1418 |
|
|
1419 |
|
// Same normal form for: |
1420 |
|
// |
1421 |
|
// (= "" (str.replace x y (str.++ x x "A"))) |
1422 |
|
// |
1423 |
|
// (and (= x "") (not (= y ""))) |
1424 |
2 |
Node empty_repl_xaa = d_nodeManager->mkNode( |
1425 |
|
kind::EQUAL, |
1426 |
|
empty, |
1427 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, xxa)); |
1428 |
2 |
Node empty_xy = d_nodeManager->mkNode( |
1429 |
|
kind::AND, |
1430 |
4 |
d_nodeManager->mkNode(kind::EQUAL, x, empty), |
1431 |
6 |
d_nodeManager->mkNode(kind::NOT, |
1432 |
12 |
d_nodeManager->mkNode(kind::EQUAL, y, empty))); |
1433 |
2 |
sameNormalForm(empty_repl_xaa, empty_xy); |
1434 |
|
|
1435 |
|
// (= "" (str.replace (str.++ x x "A") x y)) ---> false |
1436 |
2 |
Node empty_repl_xxaxy = d_nodeManager->mkNode( |
1437 |
|
kind::EQUAL, |
1438 |
|
empty, |
1439 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, xxa, x, y)); |
1440 |
2 |
Node eq_xxa_repl = d_nodeManager->mkNode( |
1441 |
|
kind::EQUAL, |
1442 |
|
xxa, |
1443 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, empty, y, x)); |
1444 |
2 |
sameNormalForm(empty_repl_xxaxy, f); |
1445 |
|
|
1446 |
|
// Same normal form for: |
1447 |
|
// |
1448 |
|
// (= "" (str.replace "A" x y)) |
1449 |
|
// |
1450 |
|
// (= "A" (str.replace "" y x)) |
1451 |
2 |
Node empty_repl_axy = d_nodeManager->mkNode( |
1452 |
4 |
kind::EQUAL, empty, d_nodeManager->mkNode(kind::STRING_REPLACE, a, x, y)); |
1453 |
2 |
Node eq_a_repl = d_nodeManager->mkNode( |
1454 |
4 |
kind::EQUAL, a, d_nodeManager->mkNode(kind::STRING_REPLACE, empty, y, x)); |
1455 |
2 |
sameNormalForm(empty_repl_axy, eq_a_repl); |
1456 |
|
|
1457 |
|
// Same normal form for: |
1458 |
|
// |
1459 |
|
// (= "" (str.replace x "A" "")) |
1460 |
|
// |
1461 |
|
// (str.prefix x "A") |
1462 |
2 |
Node empty_repl_a = d_nodeManager->mkNode( |
1463 |
|
kind::EQUAL, |
1464 |
|
empty, |
1465 |
4 |
d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, empty)); |
1466 |
4 |
Node prefix_a = d_nodeManager->mkNode(kind::STRING_PREFIX, x, a); |
1467 |
2 |
sameNormalForm(empty_repl_a, prefix_a); |
1468 |
|
|
1469 |
|
// Same normal form for: |
1470 |
|
// |
1471 |
|
// (= "" (str.substr x 1 2)) |
1472 |
|
// |
1473 |
|
// (<= (str.len x) 1) |
1474 |
2 |
Node empty_substr = d_nodeManager->mkNode( |
1475 |
|
kind::EQUAL, |
1476 |
|
empty, |
1477 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three)); |
1478 |
2 |
Node leq_len_x = d_nodeManager->mkNode( |
1479 |
4 |
kind::LEQ, d_nodeManager->mkNode(kind::STRING_LENGTH, x), one); |
1480 |
2 |
sameNormalForm(empty_substr, leq_len_x); |
1481 |
|
|
1482 |
|
// Different normal form for: |
1483 |
|
// |
1484 |
|
// (= "" (str.substr x 0 n)) |
1485 |
|
// |
1486 |
|
// (<= n 0) |
1487 |
2 |
Node empty_substr_x = d_nodeManager->mkNode( |
1488 |
|
kind::EQUAL, |
1489 |
|
empty, |
1490 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, n)); |
1491 |
4 |
Node leq_n = d_nodeManager->mkNode(kind::LEQ, n, zero); |
1492 |
2 |
differentNormalForms(empty_substr_x, leq_n); |
1493 |
|
|
1494 |
|
// Same normal form for: |
1495 |
|
// |
1496 |
|
// (= "" (str.substr "A" 0 n)) |
1497 |
|
// |
1498 |
|
// (<= n 0) |
1499 |
2 |
Node empty_substr_a = d_nodeManager->mkNode( |
1500 |
|
kind::EQUAL, |
1501 |
|
empty, |
1502 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, a, zero, n)); |
1503 |
2 |
sameNormalForm(empty_substr_a, leq_n); |
1504 |
|
|
1505 |
|
// Same normal form for: |
1506 |
|
// |
1507 |
|
// (= (str.++ x x a) (str.replace y (str.++ x x a) y)) |
1508 |
|
// |
1509 |
|
// (= (str.++ x x a) y) |
1510 |
2 |
Node eq_xxa_repl_y = d_nodeManager->mkNode( |
1511 |
4 |
kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_REPLACE, y, xxa, y)); |
1512 |
4 |
Node eq_xxa_y = d_nodeManager->mkNode(kind::EQUAL, xxa, y); |
1513 |
2 |
sameNormalForm(eq_xxa_repl_y, eq_xxa_y); |
1514 |
|
|
1515 |
|
// (= (str.++ x x a) (str.replace (str.++ x x a) "A" "B")) ---> false |
1516 |
2 |
Node eq_xxa_repl_xxa = d_nodeManager->mkNode( |
1517 |
4 |
kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_REPLACE, xxa, a, b)); |
1518 |
2 |
sameNormalForm(eq_xxa_repl_xxa, f); |
1519 |
|
|
1520 |
|
// Same normal form for: |
1521 |
|
// |
1522 |
|
// (= (str.replace x "A" "B") "") |
1523 |
|
// |
1524 |
|
// (= x "") |
1525 |
2 |
Node eq_repl = d_nodeManager->mkNode( |
1526 |
4 |
kind::EQUAL, d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b), empty); |
1527 |
4 |
Node eq_x = d_nodeManager->mkNode(kind::EQUAL, x, empty); |
1528 |
2 |
sameNormalForm(eq_repl, eq_x); |
1529 |
|
|
1530 |
|
{ |
1531 |
|
// Same normal form for: |
1532 |
|
// |
1533 |
|
// (= (str.replace y "A" "B") "B") |
1534 |
|
// |
1535 |
|
// (= (str.replace y "B" "A") "A") |
1536 |
2 |
Node lhs = d_nodeManager->mkNode( |
1537 |
4 |
kind::EQUAL, d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b), b); |
1538 |
2 |
Node rhs = d_nodeManager->mkNode( |
1539 |
4 |
kind::EQUAL, d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, a), a); |
1540 |
2 |
sameNormalForm(lhs, rhs); |
1541 |
|
} |
1542 |
|
|
1543 |
|
{ |
1544 |
|
// Same normal form for: |
1545 |
|
// |
1546 |
|
// (= (str.++ x "A" y) (str.++ "A" "A" (str.substr "AAA" 0 n))) |
1547 |
|
// |
1548 |
|
// (= (str.++ y x) (str.++ (str.substr "AAA" 0 n) "A")) |
1549 |
2 |
Node lhs = d_nodeManager->mkNode( |
1550 |
|
kind::EQUAL, |
1551 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, a, y), |
1552 |
6 |
d_nodeManager->mkNode( |
1553 |
|
kind::STRING_CONCAT, |
1554 |
|
a, |
1555 |
|
a, |
1556 |
12 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, aaa, zero, n))); |
1557 |
2 |
Node rhs = d_nodeManager->mkNode( |
1558 |
|
kind::EQUAL, |
1559 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, y), |
1560 |
8 |
d_nodeManager->mkNode( |
1561 |
|
kind::STRING_CONCAT, |
1562 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, aaa, zero, n), |
1563 |
8 |
a)); |
1564 |
2 |
sameNormalForm(lhs, rhs); |
1565 |
|
} |
1566 |
|
|
1567 |
|
{ |
1568 |
|
// Same normal form for: |
1569 |
|
// |
1570 |
|
// (= (str.++ "A" x) "A") |
1571 |
|
// |
1572 |
|
// (= x "") |
1573 |
2 |
Node lhs = d_nodeManager->mkNode( |
1574 |
4 |
kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, a, x), a); |
1575 |
4 |
Node rhs = d_nodeManager->mkNode(kind::EQUAL, x, empty); |
1576 |
2 |
sameNormalForm(lhs, rhs); |
1577 |
|
} |
1578 |
|
|
1579 |
|
{ |
1580 |
|
// (= (str.++ x "A") "") ---> false |
1581 |
2 |
Node eq = d_nodeManager->mkNode( |
1582 |
4 |
kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), empty); |
1583 |
2 |
sameNormalForm(eq, f); |
1584 |
|
} |
1585 |
|
|
1586 |
|
{ |
1587 |
|
// (= (str.++ x "B") "AAA") ---> false |
1588 |
2 |
Node eq = d_nodeManager->mkNode( |
1589 |
4 |
kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, x, b), aaa); |
1590 |
2 |
sameNormalForm(eq, f); |
1591 |
|
} |
1592 |
|
|
1593 |
|
{ |
1594 |
|
// (= (str.++ x "AAA") "A") ---> false |
1595 |
2 |
Node eq = d_nodeManager->mkNode( |
1596 |
4 |
kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, x, aaa), a); |
1597 |
2 |
sameNormalForm(eq, f); |
1598 |
|
} |
1599 |
|
|
1600 |
|
{ |
1601 |
|
// (= (str.++ "AAA" (str.substr "A" 0 n)) (str.++ x "B")) ---> false |
1602 |
2 |
Node eq = d_nodeManager->mkNode( |
1603 |
|
kind::EQUAL, |
1604 |
6 |
d_nodeManager->mkNode( |
1605 |
|
kind::STRING_CONCAT, |
1606 |
|
aaa, |
1607 |
6 |
d_nodeManager->mkNode( |
1608 |
|
kind::STRING_CONCAT, |
1609 |
|
a, |
1610 |
|
a, |
1611 |
4 |
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, n))), |
1612 |
8 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, b)); |
1613 |
2 |
sameNormalForm(eq, f); |
1614 |
|
} |
1615 |
|
|
1616 |
|
{ |
1617 |
|
// (= (str.++ "A" (int.to.str n)) "A") -/-> false |
1618 |
2 |
Node eq = d_nodeManager->mkNode( |
1619 |
|
kind::EQUAL, |
1620 |
6 |
d_nodeManager->mkNode(kind::STRING_CONCAT, |
1621 |
|
a, |
1622 |
4 |
d_nodeManager->mkNode(kind::STRING_ITOS, n)), |
1623 |
8 |
a); |
1624 |
2 |
differentNormalForms(eq, f); |
1625 |
|
} |
1626 |
|
|
1627 |
|
{ |
1628 |
|
// (= (str.++ "A" x y) (str.++ x "B" z)) --> false |
1629 |
2 |
Node eq = d_nodeManager->mkNode( |
1630 |
|
kind::EQUAL, |
1631 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, a, x, y), |
1632 |
8 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, b, z)); |
1633 |
2 |
sameNormalForm(eq, f); |
1634 |
|
} |
1635 |
|
|
1636 |
|
{ |
1637 |
|
// (= (str.++ "B" x y) (str.++ x "AAA" z)) --> false |
1638 |
2 |
Node eq = d_nodeManager->mkNode( |
1639 |
|
kind::EQUAL, |
1640 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, b, x, y), |
1641 |
8 |
d_nodeManager->mkNode(kind::STRING_CONCAT, x, aaa, z)); |
1642 |
2 |
sameNormalForm(eq, f); |
1643 |
|
} |
1644 |
|
|
1645 |
|
{ |
1646 |
4 |
Node xrepl = d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b); |
1647 |
|
|
1648 |
|
// Same normal form for: |
1649 |
|
// |
1650 |
|
// (= (str.++ "B" (str.replace x "A" "B") z y w) |
1651 |
|
// (str.++ z x "BA" z)) |
1652 |
|
// |
1653 |
|
// (and (= (str.++ "B" (str.replace x "A" "B") z) |
1654 |
|
// (str.++ z x "B")) |
1655 |
|
// (= (str.++ y w) (str.++ "A" z))) |
1656 |
2 |
Node lhs = d_nodeManager->mkNode( |
1657 |
|
kind::EQUAL, |
1658 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, {b, xrepl, z, y, w}), |
1659 |
8 |
d_nodeManager->mkNode(kind::STRING_CONCAT, {z, x, ba, z})); |
1660 |
2 |
Node rhs = d_nodeManager->mkNode( |
1661 |
|
kind::AND, |
1662 |
10 |
d_nodeManager->mkNode( |
1663 |
|
kind::EQUAL, |
1664 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, b, xrepl, z), |
1665 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, z, x, b)), |
1666 |
10 |
d_nodeManager->mkNode( |
1667 |
|
kind::EQUAL, |
1668 |
4 |
d_nodeManager->mkNode(kind::STRING_CONCAT, y, w), |
1669 |
12 |
d_nodeManager->mkNode(kind::STRING_CONCAT, a, z))); |
1670 |
2 |
sameNormalForm(lhs, rhs); |
1671 |
|
} |
1672 |
2 |
} |
1673 |
|
|
1674 |
26 |
TEST_F(TestTheoryWhiteSequencesRewriter, strip_constant_endpoints) |
1675 |
|
{ |
1676 |
2 |
StringsEntail& se = d_seqRewriter->getStringsEntail(); |
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 = se.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 = se.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 = se.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 = se.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 = se.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 = se.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 |
2 |
Node sig_star = d_nodeManager->mkNode( |
1801 |
|
kind::REGEXP_STAR, |
1802 |
4 |
d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty)); |
1803 |
2 |
Node lhs = d_nodeManager->mkNode( |
1804 |
|
kind::STRING_IN_REGEXP, |
1805 |
|
x, |
1806 |
6 |
d_nodeManager->mkNode(kind::REGEXP_CONCAT, |
1807 |
12 |
{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 |
2 |
Node sig_star = d_nodeManager->mkNode( |
1819 |
|
kind::REGEXP_STAR, |
1820 |
4 |
d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty)); |
1821 |
2 |
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 |
2 |
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 |
2 |
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 |
54 |
} // namespace cvc5 |