1 /* Test Partially_Reduced_Product<>:: Shrink_Using_Congruences_Reduction()
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 using namespace Parma_Polyhedra_Library::IO_Operators;
27
28 typedef NNC_Polyhedron Poly;
29
30 typedef Domain_Product<Poly, Grid>::Constraints_Product PolyGrid;
31 typedef Domain_Product<Poly, TBox>::Constraints_Product PolyBox;
32 #if 0
33 typedef Domain_Product<Affine_Space, TBox>::Constraints_Product AffBox;
34 #endif
35 typedef Domain_Product<Grid, TBox>::Constraints_Product GridBox;
36
37 namespace {
38
39 // Constraints_Reduction with non-strict constraints and
40 // equality found. Positive coefficients.
41 bool
test01()42 test01() {
43 Variable A(0);
44 Variable B(1);
45
46 PolyGrid cp(2);
47 Constraint_System cs;
48 cs.insert(3*A >= 7);
49 cs.insert(3*A <= 7);
50 cp.refine_with_constraints(cs);
51
52 PolyGrid known_cp(2);
53
54 known_cp.refine_with_constraint(3*A == 7);
55
56 bool ok = cp.OK();
57
58 print_congruences(cp, "*** after ok check: cp congruences ***");
59 print_constraints(cp, "*** after ok check: cp constraints ***");
60
61 if (ok) {
62 ok = ok && cp == known_cp;
63 print_congruences(cp, "*** after known_cp check: cp congruences ***");
64 print_constraints(cp, "*** after known_cp check: cp constraints ***");
65 }
66
67 return ok;
68 }
69
70 // Constraints_Reduction with non-strict constraints and
71 // equality found. Negative coefficients.
72 bool
test02()73 test02() {
74 Variable A(0);
75 Variable B(1);
76
77 PolyGrid cp(2);
78 Constraint_System cs;
79 cs.insert(2*A >= -9);
80 cs.insert(2*A <= -9);
81 cp.refine_with_constraints(cs);
82
83 PolyGrid known_cp(2);
84
85 known_cp.refine_with_constraint(2*A == -9);
86
87 bool ok = cp.OK();
88
89 print_congruences(cp, "*** after ok check: cp congruences ***");
90 print_constraints(cp, "*** after ok check: cp constraints ***");
91
92 if (ok) {
93 ok = ok && cp == known_cp;
94
95 print_congruences(cp, "*** after known_cp check: cp congruences ***");
96 print_constraints(cp, "*** after known_cp check: cp constraints ***");
97 }
98
99 return ok;
100 }
101
102 // Constraints_Reduction with strict lower bound and an equality
103 // is found.
104 bool
test03()105 test03() {
106 Variable A(0);
107 Variable B(1);
108
109 PolyGrid cp(2);
110 Constraint_System cs;
111 cs.insert(A > 0);
112 cs.insert(A <= 0);
113 cp.refine_with_constraints(cs);
114
115 PolyGrid known_cp(2, EMPTY);
116
117 bool ok = cp.OK();
118
119 print_congruences(cp, "*** after ok check: cp congruences ***");
120 print_constraints(cp, "*** after ok check: cp constraints ***");
121
122 if (ok) {
123 ok = ok && cp == known_cp;
124
125 print_congruences(cp, "*** after known_cp check: cp congruences ***");
126 print_constraints(cp, "*** after known_cp check: cp constraints ***");
127 }
128
129 return ok;
130 }
131
132 // Constraints_Reduction with strict upper bound and an equality
133 // is found.
134 bool
test04()135 test04() {
136 Variable A(0);
137 Variable B(1);
138
139 PolyGrid cp(2);
140 Constraint_System cs;
141 cs.insert(A >= 1);
142 cs.insert(A < 3);
143 cp.refine_with_constraints(cs);
144 cp.refine_with_congruence((A %= 1)/ 0);
145
146 PolyGrid known_cp(2);
147
148 known_cp.refine_with_constraint(A == 1);
149
150 bool ok = cp.OK();
151
152 print_congruences(cp, "*** after ok check: cp congruences ***");
153 print_constraints(cp, "*** after ok check: cp constraints ***");
154
155 if (ok) {
156 ok = ok && cp == known_cp;
157
158 print_congruences(cp, "*** after known_cp check: cp congruences ***");
159 print_constraints(cp, "*** after known_cp check: cp constraints ***");
160 }
161
162 return ok;
163 }
164
165 // Constraints_Reduction where emptiness is found.
166 bool
test05()167 test05() {
168 Variable A(0);
169 Variable B(1);
170
171 PolyGrid cp(2);
172 Constraint_System cs;
173 cs.insert(A >= 1);
174 cs.insert(A <= 2);
175 cp.refine_with_constraints(cs);
176 cp.refine_with_congruence((A %= 0)/ 0);
177
178 PolyGrid known_cp(2, EMPTY);
179
180 bool ok = cp.OK();
181
182 print_congruences(cp, "*** after ok check: cp congruences ***");
183 print_constraints(cp, "*** after ok check: cp constraints ***");
184
185 if (ok) {
186 ok = cp == known_cp;
187
188 print_congruences(cp, "*** after known_cp check: cp congruences ***");
189 print_constraints(cp, "*** after known_cp check: cp constraints ***");
190 }
191
192 return ok;
193 }
194
195 // Constraints_Reduction where emptiness is found.
196 bool
test06()197 test06() {
198 Variable A(0);
199 Variable B(1);
200
201 PolyGrid cp(2);
202 Constraint_System cs;
203 cs.insert(A >= 1);
204 cs.insert(A <= 1);
205 cp.refine_with_constraints(cs);
206 cp.refine_with_congruence((A %= 0)/ 2);
207
208 PolyGrid known_cp(2, EMPTY);
209
210 bool ok = cp.OK();
211
212 print_congruences(cp, "*** after ok check: cp congruences ***");
213 print_constraints(cp, "*** after ok check: cp constraints ***");
214
215 if (ok) {
216 ok = cp == known_cp;
217
218 print_congruences(cp, "*** after known_cp check: cp congruences ***");
219 print_constraints(cp, "*** after known_cp check: cp constraints ***");
220 }
221
222 return ok;
223 }
224
225 // Constraints_Reduction that calls constraints()
226 // and hence reduce().
227 bool
test07()228 test07() {
229 Variable A(0);
230
231 PolyGrid cp(1);
232 Constraint_System cs;
233 cs.insert(A >= 1);
234 cs.insert(A <= 2);
235 cp.refine_with_constraints(cs);
236 cp.refine_with_congruence((A %= 0)/ 2);
237
238 bool ok = cp.OK();
239
240 Constraint_System cs1 = cp.constraints();
241
242 PolyGrid known_cp(1);
243 known_cp.refine_with_constraints(cs1);
244 known_cp.refine_with_congruence((A %= 0)/ 2);
245
246 print_congruences(cp, "*** after ok check: cp congruences ***");
247 print_constraints(cp, "*** after ok check: cp constraints ***");
248
249 if (ok) {
250 ok = (cp == known_cp);
251 print_constraints(cp,
252 "*** after known_cp check: cp constraints ***");
253 print_congruences(cp,
254 "*** after known_cp check: cp congruences ***");
255 if (!ok) {
256 print_constraints(known_cp,
257 "*** known_cp constraints ***");
258 print_congruences(known_cp,
259 "*** known_cp congruences ***");
260 }
261 }
262
263 return ok;
264 }
265
266 bool
test08()267 test08() {
268 Variable A(0);
269 Variable B(1);
270
271 PolyBox cp(2);
272
273 Constraint_System cs;
274 cs.insert(A + B >= 0);
275 cs.insert(A + B <= 1);
276 cs.insert(A - 2*B <= 10);
277 cs.insert(A - 2*B >= 0);
278 cp.refine_with_constraints(cs);
279 cp.refine_with_constraint(A >= 4);
280
281 PolyBox known_cp(2);
282 known_cp.refine_with_constraint(A == 4);
283 known_cp.refine_with_constraint(B == -3);
284
285 bool ok = cp.OK();
286
287 print_congruences(cp, "*** after ok check: cp congruences ***");
288 print_constraints(cp, "*** after ok check: cp constraints ***");
289
290 if (ok) {
291 ok = ok && cp == known_cp;
292
293 print_congruences(cp, "*** after known_cp check: cp congruences ***");
294 print_constraints(cp, "*** after known_cp check: cp constraints ***");
295 }
296
297 return ok;
298 }
299
300 #if 0
301 bool
302 test09() {
303 Variable A(0);
304 Variable B(1);
305
306 AffBox cp(2);
307
308 Constraint_System cs;
309 cs.insert(A >= 0);
310 cs.insert(A <= 4);
311 cs.insert(B <= 10);
312 cs.insert(B >= 3);
313 cp.refine_with_constraints(cs);
314 cp.refine_with_constraint(A >= 4);
315 cp.refine_with_constraint(B <= 3);
316
317 AffBox known_cp(2);
318 known_cp.refine_with_constraint(A == 4);
319 known_cp.refine_with_constraint(B == 3);
320
321 bool ok = cp.OK();
322
323 print_constraints(cp, "*** after ok check: cp constraints ***");
324
325 if (ok) {
326 ok = ok && cp == known_cp;
327
328 print_constraints(cp, "*** after known_cp check: cp constraints ***");
329 }
330
331 return ok;
332 }
333 #endif
334
335 // space_dimension()
336 bool
test10()337 test10() {
338 Variable A(0);
339 Variable E(4);
340
341 Constraint_System cs;
342 cs.insert(A + E <= 9);
343 cs.insert(A + E >= 9);
344
345 PolyGrid cp(5);
346 cp.refine_with_constraints(cs);
347
348 bool cons_ok = (cp.space_dimension() == 5);
349
350 print_congruences(cp, "*** cp congruences ***");
351 print_constraints(cp, "*** cp constraints ***");
352
353 return cons_ok;
354 }
355
356 #if 0
357 // Example taken from SenS07 (figure 5(a)
358 bool
359 test11() {
360 Variable A(0);
361 Variable B(1);
362 Variable C(2);
363 Variable D(3);
364
365 Constraint_System cs;
366 cs.insert(B >= -10);
367 cs.insert(B <= 5);
368 cs.insert(C >= 2);
369 cs.insert(C <= 3);
370 cs.insert(D >= 4);
371 cs.insert(D <= 9);
372 Congruence_System cgs;
373 cgs.insert(A %= 0);
374 cgs.insert((B %= 5) / 15);
375 cgs.insert(C %= 0);
376 cgs.insert(D %= 0);
377
378 AffBox ab1(4);
379 ab1.refine_with_constraints(cs);
380 ab1.refine_with_congruences(cgs);
381 ab1.affine_image(A, 2*B + D);
382 TBox box1(4);
383 box1.refine_with_constraints(cs);
384 box1.refine_with_congruences(cgs);
385 box1.affine_image(A, 2*B + D);
386 Affine_Space affs1(4);
387 affs1.refine_with_constraints(cs);
388 affs1.refine_with_congruences(cgs);
389 affs1.affine_image(A, 2*B + D);
390 GridBox gb1(4);
391 gb1.refine_with_constraints(cs);
392 gb1.refine_with_congruences(cgs);
393 gb1.affine_image(A, 2*B + D);
394 print_constraints(ab1,
395 "*** (Affine_Space x TBox) ab1 constraints ***");
396
397 AffBox ab2(ab1);
398 TBox box2(box1);
399 Affine_Space affs2(affs1);
400 GridBox gb2(gb1);
401
402 ab1.affine_image(A, A - 4*B);
403 box1.affine_image(A, A - 4*B);
404 affs1.affine_image(A, A - 4*B);
405 gb1.affine_image(A, A - 4*B);
406
407 ab2.affine_image(A, A + 2*B);
408 box2.affine_image(A, A + 2*B);
409 affs2.affine_image(A, A + 2*B);
410 gb2.affine_image(A, A + 2*B);
411
412 ab1.upper_bound_assign(ab2);
413 box1.upper_bound_assign(box2);
414 affs1.upper_bound_assign(affs2);
415 gb1.upper_bound_assign(gb2);
416
417 Constraint_System known_cs;
418 known_cs.insert(A >= -36);
419 known_cs.insert(A <= 29);
420 known_cs.insert(B >= -10);
421 known_cs.insert(B <= 5);
422 known_cs.insert(C >= 2);
423 known_cs.insert(C <= 3);
424 known_cs.insert(D >= 4);
425 known_cs.insert(D <= 9);
426 AffBox known_ab(4);
427 known_ab.refine_with_constraints(known_cs);
428 TBox known_box(4);
429 known_box.refine_with_constraints(known_cs);
430 known_box.unconstrain(A);
431 known_box.refine_with_constraint(A >= -36);
432 known_box.refine_with_constraint(A <= 59);
433 Affine_Space known_affs(4);
434 known_affs.refine_with_constraints(known_cs);
435 GridBox known_gb(4);
436 known_gb.refine_with_constraints(known_cs);
437 known_gb.refine_with_congruences(cgs);
438 known_gb.refine_with_congruence((A - D %= 20) / 30);
439 known_gb.refine_with_congruence((B %= 5) / 15);
440
441 bool ok = (ab1 == known_ab
442 && box1 == known_box
443 && affs1 == known_affs && gb1 == known_gb);
444
445 print_constraints(ab1,
446 "*** (Affine_Space x TBox) ab1 constraints ***");
447 print_constraints(box1,
448 "*** (TBox) box1 constraints ***");
449 print_constraints(affs1, "*** (Affine_Space) affs1 constraints ***");
450 print_constraints(gb1,
451 "*** (Grid x TBox) gb1 constraints ***");
452 print_congruences(gb1,
453 "*** (Grid x TBox) gb1 congruences ***");
454
455 return ok;
456 }
457
458 // Example taken from SenS07 (figure 5(b)
459 bool
460 test12() {
461 Variable A(0);
462 Variable B(1);
463 Variable C(2);
464 Variable D(3);
465 Variable E(4);
466
467 Constraint_System cs;
468 cs.insert(B >= 6);
469 cs.insert(B <= 8);
470 cs.insert(C >= 1);
471 cs.insert(C <= 9);
472 Congruence_System cgs;
473 cgs.insert(A %= 0);
474 cgs.insert((B %= 0) / 2);
475 cgs.insert(C %= 0);
476 cgs.insert(D %= 0);
477 cgs.insert(E %= 0);
478
479 AffBox ab1(5);
480 TBox box1(5);
481 Affine_Space affs1(5);
482 GridBox gb1(5);
483 ab1.refine_with_constraints(cs);
484 ab1.refine_with_congruences(cgs);
485 box1.refine_with_constraints(cs);
486 box1.refine_with_congruences(cgs);
487 affs1.refine_with_constraints(cs);
488 affs1.refine_with_congruences(cgs);
489 gb1.refine_with_constraints(cs);
490 gb1.refine_with_congruences(cgs);
491
492 AffBox ab2(ab1);
493 TBox box2(box1);
494 Affine_Space affs2(affs1);
495 GridBox gb2(gb1);
496
497 ab1.affine_image(E, 2*B);
498 box1.affine_image(E, 2*B);
499 affs1.affine_image(E, 2*B);
500 gb1.affine_image(E, 2*B);
501
502 ab2.affine_image(E, B + C);
503 box2.affine_image(E, B + C);
504 affs2.affine_image(E, B + C);
505 gb2.affine_image(E, B + C);
506
507 ab1.upper_bound_assign(ab2);
508 box1.upper_bound_assign(box2);
509 affs1.upper_bound_assign(affs2);
510 gb1.upper_bound_assign(gb2);
511
512 Constraint_System known_cs(cs);
513 known_cs.insert(E >= 7);
514 known_cs.insert(E <= 17);
515 AffBox known_ab(5);
516 known_ab.refine_with_constraints(known_cs);
517 TBox known_box(5);
518 known_box.refine_with_constraints(known_cs);
519 Affine_Space known_affs(5);
520 known_affs.refine_with_constraints(known_cs);
521 GridBox known_gb(5);
522 known_gb.refine_with_constraints(known_cs);
523 known_gb.refine_with_congruences(cgs);
524
525 bool ok = (ab1 == known_ab && box1 == known_box
526 && affs1 == known_affs && gb1 == known_gb);
527
528 print_constraints(ab1, "*** (Affine_Space x TBox) ab1 constraints ***");
529 print_constraints(box1, "*** (TBox) box1 constraints ***");
530 print_constraints(affs1, "*** (Affine_Space) affs1 constraints ***");
531 print_constraints(gb1, "*** (Grid x TBox) gb1 constraints ***");
532 print_congruences(gb1, "*** (Grid x TBox) gb1 congruences ***");
533
534 return ok;
535 }
536 #endif
537
538 } // namespace
539
540 BEGIN_MAIN
541 DO_TEST(test01);
542 DO_TEST(test02);
543 DO_TEST(test03);
544 DO_TEST(test04);
545 DO_TEST(test05);
546 DO_TEST(test06);
547 DO_TEST(test07);
548 DO_TEST(test08);
549 //DO_TEST(test09);
550 DO_TEST(test10);
551 //DO_TEST_F8(test11);
552 //DO_TEST(test12);
553 END_MAIN
554