1 /* Test Octagonal_Shape::generalized_affine_image().
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 bool
test01()29 test01() {
30   Variable x(0);
31   Variable y(1);
32 
33   TOctagonal_Shape oct(2);
34   oct.add_constraint(x <= 4);
35   oct.add_constraint(x >= -6);
36   oct.add_constraint(y == 0);
37 
38   print_constraints(oct, "*** oct ***");
39 
40   Octagonal_Shape<mpq_class> known_result(2);
41   known_result.add_constraint(x <= 4);
42   known_result.add_constraint(x >= -6);
43   known_result.add_constraint(y <= 1);
44 
45   oct.generalized_affine_image(y, LESS_OR_EQUAL, -y + 1);
46 
47   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
48 
49   print_constraints(oct, "*** oct.generalized_affine_image(y, "
50                          "LESS_OR_EQUAL, -y + 1) ***");
51 
52   return ok;
53 }
54 
55 bool
test02()56 test02() {
57   Variable x(0);
58   Variable y(1);
59 
60   TOctagonal_Shape oct(2);
61   oct.add_constraint(x <= 4);
62   oct.add_constraint(x >= -6);
63   oct.add_constraint(y == 0);
64 
65   print_constraints(oct, "*** oct ***");
66 
67   Octagonal_Shape<mpq_class> known_result(2);
68   known_result.add_constraint(x >= -7);
69   known_result.add_constraint(y == 0);
70 
71   oct.generalized_affine_image(x, GREATER_OR_EQUAL, -x - 3);
72 
73   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
74 
75   print_constraints(oct,
76                     "*** oct.generalized_affine_image(x, "
77                     "GREATER_OR_EQUAL, -x - 3) ***");
78 
79   return ok;
80 }
81 
82 bool
test03()83 test03() {
84   Variable A(0);
85   Variable B(1);
86 
87   TOctagonal_Shape oct(2);
88   oct.add_constraint(A >= 0);
89   oct.add_constraint(B <= 1);
90 
91   print_constraints(oct, "*** oct ***");
92 
93   Octagonal_Shape<mpq_class> known_result(2);
94   known_result.add_constraint(A >= 0);
95   known_result.add_constraint(B <= 2);
96 
97   oct.generalized_affine_image(B, LESS_OR_EQUAL, 3*B + 1, 2);
98 
99   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
100 
101   print_constraints(oct, "*** oct.generalized_affine_image(B, "
102                          "LESS_OR_EQUAL, 3*B + 1, 2) ***");
103 
104   return ok;
105 }
106 
107 bool
test04()108 test04() {
109   Variable A(0);
110   Variable B(1);
111 
112   TOctagonal_Shape oct(2);
113   oct.add_constraint(A == 0);
114   oct.add_constraint(B >= 1);
115 
116   print_constraints(oct, "*** oct ***");
117 
118   Octagonal_Shape<mpq_class> known_result(2);
119   known_result.add_constraint(A == 0);
120   known_result.add_constraint(B >= -1);
121 
122   oct.generalized_affine_image(B, GREATER_OR_EQUAL, B - 2);
123 
124   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
125 
126   print_constraints(oct, "*** oct.generalized_affine_image(B, "
127                     "GREATER_OR_EQUAL, B - 2) ***");
128 
129   return ok;
130 }
131 
132 bool
test05()133 test05() {
134   Variable A(0);
135   Variable B(1);
136   Linear_Expression expr(2*A + 3);
137 
138   TOctagonal_Shape oct(2);
139   oct.add_constraint(B <= 1);
140   oct.add_constraint(A + B == 0);
141 
142   print_constraints(oct, "*** oct ***");
143 
144   Octagonal_Shape<mpq_class> known_result(2);
145   known_result.add_constraint(2*A >= 1);
146   known_result.add_constraint(B <= 1);
147   known_result.add_constraint(2*(-A - B) <= -3);
148 
149   oct.generalized_affine_image(A, GREATER_OR_EQUAL, 2*A + 3, 2);
150 
151   bool ok = check_result(oct, known_result);
152 
153   print_constraints(oct, "*** oct.generalized_affine_image(A, "
154                     "GREATER_OR_EQUAL, 2*A + 3, 2) ***");
155 
156   return ok;
157 }
158 
159 bool
test06()160 test06() {
161   Variable A(0);
162   Variable B(1);
163   Variable C(2);
164 
165   TOctagonal_Shape oct(3);
166   oct.add_constraint(A - B == 0);
167   oct.add_constraint(B <= 1);
168   oct.add_constraint(C + A <= 2);
169 
170   print_constraints(oct, "*** oct ***");
171 
172   Octagonal_Shape<mpq_class> known_result(3);
173   known_result.add_constraint(A - B == 0);
174   known_result.add_constraint(B <= 1);
175   known_result.add_constraint(A + B <= 2);
176   known_result.add_constraint(A <= 1);
177 
178   oct.generalized_affine_image(C, LESS_OR_EQUAL, 2*C + 1, 5);
179 
180   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
181 
182   print_constraints(oct, "*** oct.generalized_affine_image(C, "
183                          "LESS_OR_EQUAL, 2*C + 1, 5) ***");
184 
185   return ok;
186 }
187 
188 bool
test07()189 test07() {
190   Variable A(0);
191   Variable B(1);
192   Variable C(2);
193 
194   TOctagonal_Shape oct(3);
195   oct.add_constraint(A - B == 0);
196   oct.add_constraint(B <= 1);
197   oct.add_constraint(C + A <= 2);
198 
199   print_constraints(oct, "*** oct ***");
200 
201   Octagonal_Shape<mpq_class> known_result(oct);
202   known_result.affine_image(C, 5*C - 3, 4);
203 
204   oct.generalized_affine_image(C, EQUAL, 5*C - 3, 4);
205 
206   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
207 
208   print_constraints(oct, "*** oct.generalized_affine_image(C, "
209                     "EQUAL, 5*C - 3, 4) ***");
210 
211   return ok;
212 }
213 
214 bool
test08()215 test08() {
216   Variable A(0);
217   Variable B(1);
218   Variable C(2);
219 
220   TOctagonal_Shape oct(3);
221   oct.add_constraint(A - B == 0);
222   oct.add_constraint(B <= 1);
223   oct.add_constraint(C + A <= 2);
224 
225   print_constraints(oct, "*** oct ***");
226 
227   Octagonal_Shape<mpq_class> known_result(3);
228   known_result.add_constraint(B >= -1);
229   known_result.add_constraint(C + A <= 2);
230   known_result.add_constraint(A <= 1);
231 
232   oct.generalized_affine_image(B, GREATER_OR_EQUAL, -B - 2, 3);
233 
234   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
235 
236   print_constraints(oct, "*** oct.generalized_affine_image(B, "
237                          "GREATER_OR_EQUAL, -B - 2, 3) ***");
238 
239   return ok;
240 }
241 
242 bool
test09()243 test09() {
244   Variable A(0);
245   Variable B(1);
246   Variable C(2);
247 
248   TOctagonal_Shape oct(3);
249   oct.add_constraint(A - B == 0);
250   oct.add_constraint(B <= 1);
251   oct.add_constraint(C + A <= 2);
252 
253   print_constraints(oct, "*** oct ***");
254 
255   Octagonal_Shape<mpq_class> known_result(3);
256   known_result.add_constraint(A <= 1);
257   known_result.add_constraint(C + A <= 2);
258 
259   oct.generalized_affine_image(B, LESS_OR_EQUAL, 4*A - 2*C + 3, -3);
260 
261   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
262 
263   print_constraints(oct, "*** oct.generalized_affine_image(B, "
264                          "LESS_OR_EQUAL, 4*A - 2*C + 3, -3) ***");
265 
266   return ok;
267 }
268 
269 bool
test10()270 test10() {
271   Variable A(0);
272   Variable B(1);
273   Variable C(2);
274 
275   TOctagonal_Shape oct(3);
276   oct.add_constraint(A - B == 0);
277   oct.add_constraint(B <= 1);
278   oct.add_constraint(C + A <=2);
279 
280   print_constraints(oct, "*** oct ***");
281 
282   Octagonal_Shape<mpq_class> known_result(oct);
283   known_result.affine_image(B, 2*A - 4*B + C + 3, 3);
284 
285   oct.generalized_affine_image(B, EQUAL, 2*A - 4*B + C + 3, 3);
286 
287   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
288 
289   print_constraints(oct, "*** oct.generalized_affine_image(B, "
290                          "EQUAL, 2*A - 4*B + C + 3, 3) ***");
291 
292   return ok;
293 }
294 
295 bool
test11()296 test11() {
297   Variable x(0);
298   Variable y(1);
299   Variable z(2);
300 
301   TOctagonal_Shape oct(3);
302   oct.add_constraint(x + y >= 0);
303   oct.add_constraint(y >= 0);
304   oct.add_constraint(z <= 2);
305   oct.add_constraint(z - x >= 9);
306 
307   try {
308     // This is an invalid use of the method
309     // Octagonal_Shape::generalized_affine_image(v, e, d): it is illegal
310     // to apply the method to a linear expression
311     // with the denominator equal to zero.
312     Coefficient d = 0;
313     oct.generalized_affine_image(y, LESS_OR_EQUAL, y + 1, d);
314   }
315   catch (std::invalid_argument& e) {
316     nout << "invalid_argument: " << e.what() << endl;
317     return true;
318   }
319   catch (...) {
320     return false;
321   }
322   return false;
323 }
324 
325 bool
test12()326 test12() {
327   Variable x(0);
328   Variable y(1);
329 
330   TOctagonal_Shape oct(2);
331   oct.add_constraint(x >= y);
332 
333   try {
334     // This is an incorrect use of the method
335     // Octagonal_Shape::generalized_affine_image(v, r, expr, d): it is illegal
336     // to use a strict relation symbol.
337     oct.generalized_affine_image(x, LESS_THAN, x + 1);
338   }
339   catch (std::invalid_argument& e) {
340     nout << "invalid_argument: " << e.what() << endl;
341     return true;
342   }
343   catch (...) {
344     return false;
345   }
346   return false;
347 }
348 
349 bool
test13()350 test13() {
351   Variable x(0);
352   Variable y(1);
353 
354   TOctagonal_Shape oct(2);
355   oct.add_constraint(x >= y);
356 
357   try {
358     // This is an incorrect use of the method
359     // Octagonal_Shape::generalized_affine_image(v, r, expr, d): it is illegal
360     // to use a strict relation symbol.
361     oct.generalized_affine_image(x, GREATER_THAN, x + 1);
362   }
363   catch (std::invalid_argument& e) {
364     nout << "invalid_argument: " << e.what() << endl;
365     return true;
366   }
367   catch (...) {
368     return false;
369   }
370   return false;
371 }
372 
373 bool
test14()374 test14() {
375   Variable x(0);
376   Variable y(1);
377   Variable z(2);
378 
379   TOctagonal_Shape oct(2);
380   oct.add_constraint(x >= y);
381 
382   try {
383     // This is an incorrect use of the method
384     // Octagonal_Shape::generalized_affine_image(v, r, expr, d): it is illegal
385     // to apply this method to an expression having space dimension
386     // greater than the octagon's space dimension.
387     oct.generalized_affine_image(y, GREATER_OR_EQUAL, z);
388   }
389   catch (std::invalid_argument& e) {
390     nout << "invalid_argument: " << e.what() << endl;
391     return true;
392   }
393   catch (...) {
394     return false;
395   }
396   return false;
397 }
398 
399 bool
test15()400 test15() {
401   Variable x(0);
402   Variable y(1);
403   Variable z(2);
404 
405   TOctagonal_Shape oct(2);
406   oct.add_constraint(x >= y);
407 
408   try {
409     // This is an incorrect use of the method
410     // Octagonal_Shape::generalized_affine_image(v, r, expr, d): it is illegal
411     // to apply this method to a variable having space dimension
412     // greater than the octagon's space dimension.
413     oct.generalized_affine_image(z, GREATER_OR_EQUAL, y);
414   }
415   catch (std::invalid_argument& e) {
416     nout << "invalid_argument: " << e.what() << endl;
417     return true;
418   }
419   catch (...) {
420     return false;
421   }
422   return false;
423 }
424 
425 bool
test16()426 test16() {
427   Variable A(0);
428   Variable B(1);
429   Variable C(2);
430 
431   TOctagonal_Shape oct(2);
432   oct.add_constraint(A >= 0);
433 
434   try {
435     // This is an incorrect use of method
436     // Octagonal_Shape::generalized_affine_image(lhs, r, rhs):
437     // it is illegal to use a variable in the `rhs' expression that
438     // does not appear in the octagon.
439     oct.generalized_affine_image(A + B, GREATER_OR_EQUAL, B + C);
440   }
441   catch (std::invalid_argument& e) {
442     nout << "invalid_argument: " << e.what() << endl;
443     return true;
444   }
445   catch (...) {
446     return false;
447   }
448   return false;
449 }
450 
451 bool
test17()452 test17() {
453   Variable A(0);
454   Variable B(1);
455   Variable C(2);
456 
457   TOctagonal_Shape oct(2);
458   oct.add_constraint(A >= 1);
459 
460   try {
461     // This is an incorrect use of method
462     // Octagonal_Shape::generalized_affine_image(lhs, r, rhs):
463     // it is illegal to use a variable in the `lhs' expression that
464     // does not appear in the octagon.
465     oct.generalized_affine_image(B + C, LESS_OR_EQUAL, A + 1);
466   }
467   catch (std::invalid_argument& e) {
468     nout << "invalid_argument: " << e.what() << endl;
469     return true;
470   }
471   catch (...) {
472     return false;
473   }
474   return false;
475 }
476 
477 bool
test18()478 test18() {
479   Variable x(0);
480   Variable y(1);
481 
482   TOctagonal_Shape oct(2);
483   oct.add_constraint(x >= y);
484   oct.add_constraint(1 >= y);
485 
486   try {
487     // This is an incorrect use of the method
488     // Octagonal_Shape::generalized_affine_image(lhs, r, rhs): it is illegal
489     // to use a strict relation symbol.
490     oct.generalized_affine_image(y - 3, GREATER_THAN, x + 1);
491   }
492   catch (std::invalid_argument& e) {
493     nout << "invalid_argument: " << e.what() << endl;
494     return true;
495   }
496   catch (...) {
497     return false;
498   }
499   return false;
500 }
501 
502 bool
test19()503 test19() {
504   Variable A(0);
505   Variable B(1);
506   Variable C(2);
507 
508   TOctagonal_Shape oct(3);
509   oct.add_constraint(A <= 21);
510   oct.add_constraint(B <= 1);
511   oct.add_constraint(C <= 2);
512   oct.add_constraint(A >= 2);
513   oct.add_constraint(B >= -1);
514   oct.add_constraint(C >= -2);
515 
516   print_constraints(oct, "*** oct ***");
517 
518   Octagonal_Shape<mpq_class> known_result(3);
519   known_result.add_constraint(A <= 21);
520   known_result.add_constraint(A >= 2);
521   known_result.add_constraint(C <= 2);
522   known_result.add_constraint(C >= -2);
523   known_result.add_constraint(C + B >= -3);
524 
525   oct.generalized_affine_image(B, GREATER_OR_EQUAL, C + 3, -1);
526 
527   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
528 
529   print_constraints(oct,
530                     "*** oct.generalized_affine_image(B, "
531                     "GREATER_OR_EQUAL, C + 3, -1) ***");
532 
533   return ok;
534 }
535 
536 bool
test20()537 test20() {
538   Variable A(0);
539   Variable B(1);
540   Variable C(2);
541 
542   TOctagonal_Shape oct(3);
543   oct.add_constraint(A <= 21);
544   oct.add_constraint(B <= 1);
545   oct.add_constraint(C <= 2);
546   oct.add_constraint(A >= 2);
547   oct.add_constraint(B >= -1);
548   oct.add_constraint(C >= -2);
549 
550   print_constraints(oct, "*** oct ***");
551 
552   Octagonal_Shape<mpq_class> known_result(3);
553   known_result.add_constraint(A <= 21);
554   known_result.add_constraint(A >= 2);
555   known_result.add_constraint(C <= 2);
556   known_result.add_constraint(C >= -2);
557   known_result.add_constraint(B - C >= 3);
558 
559   oct.generalized_affine_image(B, GREATER_OR_EQUAL, C + 3);
560 
561   bool ok = (Octagonal_Shape<mpq_class>(oct) == known_result);
562 
563   print_constraints(oct,
564                     "*** oct.generalized_affine_image(B, "
565                     "GREATER_OR_EQUAL, C + 3) ***");
566 
567   return ok;
568 }
569 
570 } // namespace
571 
572 BEGIN_MAIN
573   DO_TEST(test01);
574   DO_TEST(test02);
575   DO_TEST(test03);
576   DO_TEST(test04);
577   DO_TEST(test05);
578   DO_TEST(test06);
579   DO_TEST(test07);
580   DO_TEST(test08);
581   DO_TEST(test09);
582   DO_TEST(test10);
583   DO_TEST(test11);
584   DO_TEST(test12);
585   DO_TEST(test13);
586   DO_TEST(test14);
587   DO_TEST(test15);
588   DO_TEST(test16);
589   DO_TEST(test17);
590   DO_TEST(test18);
591   DO_TEST(test19);
592   DO_TEST(test20);
593 END_MAIN
594