1 /* Test Grid::limited_congruence_extrapolation_assign().
2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4
5 This file is part of the Parma Polyhedra Library (PPL).
6
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23
24 #include "ppl_test.hh"
25
26 namespace {
27
28 // Initially empty.
29 bool
test01()30 test01() {
31 Variable A(0);
32
33 Grid gr1(2, EMPTY);
34 print_congruences(gr1, "*** gr1 ***");
35
36 Grid gr2(2);
37 gr2.add_congruence(A %= 0);
38 print_congruences(gr2, "*** gr2 ***");
39
40 Congruence_System cgs((A %= 0) / 2);
41
42 Grid known_gr = gr2;
43
44 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
45
46 bool ok = (gr2 == known_gr);
47
48 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
49
50 return ok;
51 }
52
53 // Empty after minimization.
54 bool
test02()55 test02() {
56 Variable A(0);
57
58 Grid gr1(1);
59 gr1.add_constraint(A == 0);
60 gr1.add_constraint(A == 1);
61 print_congruences(gr1, "*** gr1 ***");
62
63 Grid gr2(1);
64 gr2.add_congruence(A %= 0);
65 print_congruences(gr2, "*** gr2 ***");
66
67 Congruence_System cgs((A %= 0) / 3);
68
69 Grid known_gr = gr2;
70
71 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
72
73 bool ok = (gr2 == known_gr);
74
75 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
76
77 return ok;
78 }
79
80 // Equivalent of just widening.
81 bool
test03()82 test03() {
83 Variable A(0);
84 Variable B(1);
85
86 Grid gr1(2);
87 gr1.add_constraint(A == 0);
88 gr1.add_constraint(B == 1);
89 print_congruences(gr1, "*** gr1 ***");
90
91 Grid gr2(2);
92 gr2.add_constraint(A == 0);
93 gr2.add_congruence(B %= 1);
94 print_congruences(gr2, "*** gr2 ***");
95
96 Grid known_gr = gr2;
97
98 Congruence_System cgs(B %= 0);
99
100 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
101
102 bool ok = (gr2 == known_gr);
103
104 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
105
106 return ok;
107 }
108
109 // Keep all congruences, including a limiting congruence.
110 bool
test04()111 test04() {
112 Variable A(0);
113 Variable B(1);
114 Variable C(2);
115
116 Grid gr1(3);
117 gr1.add_congruence((A %= 0) / 2);
118 gr1.add_congruence((B %= 0) / 2);
119 gr1.add_congruence(C %= 0);
120 print_congruences(gr1, "*** gr1 ***");
121
122 Grid gr2(3);
123 gr2.add_congruence((A %= 0) / 2);
124 gr2.add_congruence(C %= 0);
125 print_congruences(gr2, "*** gr2 ***");
126
127 Grid known_gr = gr2;
128
129 Congruence_System cgs(C %= 0);
130
131 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
132
133 bool ok = (gr2 == known_gr);
134
135 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
136
137 return ok;
138 }
139
140 // Keep some congruences.
141 bool
test05()142 test05() {
143 Variable A(0);
144 Variable B(1);
145 Variable C(2);
146
147 Grid gr1(3);
148 gr1.add_congruence((A %= 0) / 2);
149 gr1.add_congruence((B %= 0) / 2);
150 gr1.add_congruence(C %= 0);
151 print_congruences(gr1, "*** gr1 ***");
152
153 Grid gr2(3);
154 gr2.add_congruence(A %= 0);
155 gr2.add_congruence((B %= 0) / 2);
156 gr2.add_congruence(C %= 0);
157 print_congruences(gr2, "*** gr2 ***");
158
159 Congruence_System cgs(A + 0*C %= 0);
160
161 Grid known_gr = gr2;
162
163 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
164
165 bool ok = (gr2 == known_gr);
166
167 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
168
169 return ok;
170 }
171
172 // Both universe.
173 bool
test06()174 test06() {
175 Variable E(4);
176
177 Grid gr1(5);
178 print_congruences(gr1, "*** gr1 ***");
179 Grid gr2(5);
180
181 Congruence_System cgs(0*E %= 0);
182
183 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
184
185 Grid known_gr(5);
186
187 bool ok = (gr2 == known_gr);
188
189 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
190
191 return ok;
192 }
193
194 // Keeping many limiting congruences.
195 bool
test07()196 test07() {
197 Variable A(0);
198 Variable B(1);
199
200 Grid gr1(2);
201 gr1.add_congruence((A %= 0) / 4);
202 gr1.add_congruence((B %= 0) / 4);
203 print_congruences(gr1, "*** gr1 ***");
204
205 Grid gr2(2);
206 gr2.add_congruence((A %= 0) / 2);
207 gr2.add_congruence(B %= 0);
208 print_congruences(gr2, "*** gr2 ***");
209
210 Congruence_System cgs;
211 cgs.insert(A %= 0);
212 cgs.insert(B %= 0);
213
214 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
215
216 Grid known_gr(cgs);
217
218 bool ok = (gr2 == known_gr);
219
220 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
221
222 return ok;
223 }
224
225 // Tokens.
226 bool
test08()227 test08() {
228 Variable A(0);
229 Variable B(1);
230
231 Grid gr1(2);
232 gr1.add_congruence((A %= 0) / 4);
233 print_congruences(gr1, "*** gr1 ***");
234
235 Grid gr2(2);
236 gr2.add_congruence(A %= 0);
237 print_congruences(gr2, "*** gr2 ***");
238
239 unsigned int tokens = 6;
240
241 Congruence_System cgs;
242 cgs.insert((A + 0*B %= 0) / 2);
243
244 Grid known_gr = gr2;
245
246 gr2.limited_congruence_extrapolation_assign(gr1, cgs, &tokens);
247
248 #undef TOKENS
249 #define TOKENS 5
250
251 bool ok = (gr2 == known_gr) && (tokens == TOKENS);
252
253 nout << "tokens: before " << TOKENS << ", after " << tokens << endl;
254
255 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs, &tokens) ***");
256
257 return ok;
258 }
259
260 // 0 tokens.
261 bool
test09()262 test09() {
263 Variable A(0);
264 Variable B(1);
265
266 Grid gr1(2);
267 gr1.add_congruence((A %= 0) / 4);
268 print_congruences(gr1, "*** gr1 ***");
269
270 Grid gr2(2);
271 gr2.add_congruence(A %= 0);
272 print_congruences(gr2, "*** gr2 ***");
273
274 #undef TOKENS
275 #define TOKENS 0
276
277 unsigned int tokens = TOKENS;
278
279 Congruence_System cgs;
280 cgs.insert((A + 0*B %= 0) / 2);
281
282 Grid known_gr(2);
283
284 gr2.limited_congruence_extrapolation_assign(gr1, cgs, &tokens);
285
286 bool ok = (gr2 == known_gr) && (tokens == TOKENS);
287
288 nout << "tokens: before " << TOKENS << ", after " << tokens << endl;
289
290 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs, &tokens) ***");
291
292 return ok;
293 }
294
295 // Zero dimension.
296 bool
test10()297 test10() {
298 Grid gr1(0);
299 print_congruences(gr1, "*** gr1 ***");
300
301 Grid gr2(0);
302 print_congruences(gr2, "*** gr2 ***");
303
304 Congruence_System cgs(
305 (Linear_Expression::zero() %= Linear_Expression::zero()) / 4);
306
307 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
308
309 Grid known_gr(0);
310
311 bool ok = (gr2 == known_gr);
312
313 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
314
315 return ok;
316 }
317
318 // Congruences and equalities.
319 bool
test11()320 test11() {
321 Variable A(0);
322 Variable B(1);
323
324 Grid gr1(2);
325 gr1.add_congruence(A %= 0);
326 gr1.add_congruence((A - B == 0) / 27);
327 print_congruences(gr1, "*** gr1 ***");
328
329 Grid gr2(2);
330 gr2.add_congruence(A %= 0);
331 gr2.add_congruence((A - B == 0) / 9);
332 print_congruences(gr2, "*** gr2 ***");
333
334 Congruence_System cgs;
335 cgs.insert((A - B == 0) / 3);
336
337 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
338
339 Grid known_gr(2);
340 known_gr.add_congruence(A %= 0);
341 known_gr.add_congruence((A - B == 0) / 3);
342
343 bool ok = (gr2 == known_gr);
344
345 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
346
347 return ok;
348 }
349
350 // From generators, with a limiting equality.
351 bool
test12()352 test12() {
353 Variable A(0);
354 Variable B(1);
355 Variable C(2);
356
357 Grid gr1(3, EMPTY);
358 gr1.add_grid_generator(grid_point(C, 3));
359 gr1.add_grid_generator(grid_line(A - 2*B));
360 gr1.add_grid_generator(grid_point(C + 3*A + 3*C, 3));
361 print_generators(gr1, "*** gr1 ***");
362
363 Grid gr2(3, EMPTY);
364 gr2.add_grid_generator(grid_point(C, 3));
365 gr2.add_grid_generator(grid_line(A - 2*B));
366 gr2.add_grid_generator(grid_line(A + C));
367 print_generators(gr2, "*** gr2 ***");
368
369 Grid known_gr = gr2;
370
371 Congruence_System cgs;
372 cgs.insert(A - 0*C == 3);
373
374 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
375
376 bool ok = (gr2 == known_gr);
377
378 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
379
380 return ok;
381 }
382
383 // Exception due to space dimensions of grids.
384 bool
test13()385 test13() {
386 Variable A(0);
387 Variable B(1);
388 Variable C(2);
389
390 Grid gr1(3, EMPTY);
391 gr1.add_grid_generator(grid_point(C, 3));
392 gr1.add_grid_generator(grid_point(C + A - 2*B, 3));
393 print_generators(gr1, "*** gr1 ***");
394
395 Grid gr2(5, EMPTY);
396 gr2.add_grid_generator(grid_point(C, 3));
397 gr2.add_grid_generator(grid_point(2*C + A - 2*B, 6));
398 print_generators(gr2, "*** gr2 ***");
399
400 Congruence_System cgs;
401 cgs.insert(A - 0*C == 3);
402
403 try {
404 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
405 }
406 catch (const std::invalid_argument& e) {
407 nout << "invalid_argument: " << e.what() << endl;
408 return true;
409 }
410 catch (...) {
411 }
412 return false;
413 }
414
415 // Exception due to space dimension of congruence system.
416 bool
test14()417 test14() {
418 Variable A(0);
419 Variable B(1);
420 Variable C(2);
421
422 Grid gr1(2, EMPTY);
423 gr1.add_grid_generator(grid_point(A));
424 gr1.add_grid_generator(parameter(B, 3));
425 print_generators(gr1, "*** gr1 ***");
426
427 Grid gr2(2, EMPTY);
428 gr2.add_grid_generator(grid_point(A));
429 gr2.add_grid_generator(parameter(B, 6));
430 print_generators(gr2, "*** gr2 ***");
431
432 Congruence_System cgs;
433 cgs.insert(A - 0*C == 3);
434
435 try {
436 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
437 }
438 catch (const std::invalid_argument& e) {
439 nout << "invalid_argument: " << e.what() << endl;
440 return true;
441 }
442 catch (...) {
443 }
444 return false;
445 }
446
447 // Limit with an empty congruence system.
448 bool
test15()449 test15() {
450 Variable A(0);
451
452 Grid gr1(3, EMPTY);
453 gr1.add_grid_generator(grid_point());
454 gr1.add_grid_generator(parameter(A, 3));
455 print_generators(gr1, "*** gr1 ***");
456
457 Grid gr2(3, EMPTY);
458 gr2.add_grid_generator(grid_point());
459 gr2.add_grid_generator(parameter(A, 6));
460 print_generators(gr2, "*** gr2 ***");
461
462 Congruence_System cgs;
463
464 gr2.limited_congruence_extrapolation_assign(gr1, cgs);
465
466 Grid known_gr = gr2;
467 known_gr.add_grid_generator(grid_point());
468 known_gr.add_grid_generator(grid_line(A));
469
470 bool ok = (gr2 == known_gr);
471
472 print_congruences(gr2, "*** gr2.limited_congruence_extrapolation_assign(gr1, cgs) ***");
473
474 return ok;
475 }
476
477 } // namespace
478
479 BEGIN_MAIN
480 DO_TEST(test01);
481 DO_TEST(test02);
482 DO_TEST(test03);
483 DO_TEST(test04);
484 DO_TEST(test05);
485 DO_TEST(test06);
486 DO_TEST(test07);
487 DO_TEST(test08);
488 DO_TEST(test09);
489 DO_TEST(test10);
490 DO_TEST(test11);
491 DO_TEST(test12);
492 DO_TEST(test13);
493 DO_TEST(test14);
494 DO_TEST(test15);
495 END_MAIN
496