1 /* Test Polyhedron::simplify_using_context_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 bool
test01()29 test01() {
30   Variable x(0);
31   Variable y(1);
32   Variable z(2);
33 
34   C_Polyhedron icosahedron(3);
35   icosahedron.add_constraint(4*x - 2*y - z + 14 >= 0);
36   icosahedron.add_constraint(4*x + 2*y - z + 2 >= 0);
37   icosahedron.add_constraint(x + y - 1 >= 0);
38   icosahedron.add_constraint(x + y + 2*z - 5 >= 0);
39   icosahedron.add_constraint(x + 1 >= 0);
40   icosahedron.add_constraint(x + z - 1 >= 0);
41   icosahedron.add_constraint(2*x + y -2*z + 7 >= 0);
42   icosahedron.add_constraint(x - y + 2*z + 1 >= 0);
43   icosahedron.add_constraint(x - y + 5 >= 0);
44   icosahedron.add_constraint(2*x - y - 2*z + 13 >= 0);
45   icosahedron.add_constraint(-2*x - y + 2*z + 1 >= 0);
46   icosahedron.add_constraint(-x + y - 1 >= 0);
47   icosahedron.add_constraint(-x + y -2*z + 7 >= 0);
48   icosahedron.add_constraint(-4*x + 2*y + z - 4 >= 0);
49   icosahedron.add_constraint(-2*x + y + 2*z - 5 >= 0);
50   icosahedron.add_constraint(-x + 1 >= 0);
51   icosahedron.add_constraint(-x - z + 5 >= 0);
52   icosahedron.add_constraint(-4*x - 2*y + z + 8 >= 0);
53   icosahedron.add_constraint(-x - y + 5 >= 0);
54   icosahedron.add_constraint(-x - y -2*z +13 >= 0);
55 
56   C_Polyhedron column(3);
57   column.add_constraint(y >= 2);
58   column.add_constraint(y <= 4);
59   column.add_constraint(x >= 0);
60   column.add_constraint(x <= 1);
61 
62   C_Polyhedron computed_result = icosahedron;
63   computed_result.simplify_using_context_assign(column);
64 
65   C_Polyhedron known_result(3);
66   known_result.add_constraint(-4*x - 2*y + z >= -8);
67   known_result.add_constraint(-4*x + 2*y + z >= 4);
68   known_result.add_constraint(-2*x - y + 2*z >= -1);
69   known_result.add_constraint(-2*x + y + 2*z >= 5);
70   known_result.add_constraint(-x - y - 2*z >= -13);
71   known_result.add_constraint(-x - z >= -5);
72   known_result.add_constraint(-x + y - 2*z >= -7);
73 
74   bool ok = (computed_result == known_result);
75 
76   print_constraints(icosahedron, "*** icosahedron ***");
77   print_constraints(column, "*** column ***");
78   print_constraints(computed_result, "*** computed_result ***");
79   print_constraints(known_result, "*** known_result ***");
80 
81   return ok;
82 }
83 
84 bool
test02()85 test02() {
86   Variable x(0);
87   Variable y(1);
88   Variable z(2);
89 
90   C_Polyhedron icosahedron1(3);
91   icosahedron1.add_constraint(4*x - 2*y - z + 14 >= 0);
92   icosahedron1.add_constraint(4*x + 2*y - z + 2 >= 0);
93   icosahedron1.add_constraint(x + y - 1 >= 0);
94   icosahedron1.add_constraint(x + y + 2*z - 5 >= 0);
95   icosahedron1.add_constraint(x + 1 >= 0);
96   icosahedron1.add_constraint(x + z - 1 >= 0);
97   icosahedron1.add_constraint(2*x + y -2*z + 7 >= 0);
98   icosahedron1.add_constraint(x - y + 2*z + 1 >= 0);
99   icosahedron1.add_constraint(x - y + 5 >= 0);
100   icosahedron1.add_constraint(2*x - y - 2*z + 13 >= 0);
101   icosahedron1.add_constraint(-2*x - y + 2*z + 1 >= 0);
102   icosahedron1.add_constraint(-x + y - 1 >= 0);
103   icosahedron1.add_constraint(-x + y -2*z + 7 >= 0);
104   icosahedron1.add_constraint(-4*x + 2*y + z - 4 >= 0);
105   icosahedron1.add_constraint(-2*x + y + 2*z - 5 >= 0);
106   icosahedron1.add_constraint(-x + 1 >= 0);
107   icosahedron1.add_constraint(-x - z + 5 >= 0);
108   icosahedron1.add_constraint(-4*x - 2*y + z + 8 >= 0);
109   icosahedron1.add_constraint(-x - y + 5 >= 0);
110   icosahedron1.add_constraint(-x - y -2*z +13 >= 0);
111 
112   C_Polyhedron icosahedron2 = icosahedron1;
113   icosahedron2.affine_image(x, x+5);
114 
115 
116   C_Polyhedron computed_result = icosahedron1;
117   computed_result.simplify_using_context_assign(icosahedron2);
118 
119   C_Polyhedron known_result(3);
120   known_result.add_constraint(-4*x - 2*y + z >= -8);
121 
122   bool ok = (computed_result == known_result);
123 
124   print_constraints(icosahedron1, "*** icosahedron1 ***");
125   print_constraints(icosahedron2, "*** icosahedron2 ***");
126   print_constraints(computed_result, "*** computed_result ***");
127   print_constraints(known_result, "*** known_result ***");
128 
129   return ok;
130 }
131 
132 bool
test03()133 test03() {
134   Variable x(0);
135 
136   C_Polyhedron ph1(1);
137   ph1.add_constraint(x >= 0);
138   ph1.add_constraint(x <= 6);
139 
140   print_constraints(ph1, "*** ph1 ***");
141 
142   C_Polyhedron ph2(1);
143   ph2.add_constraint(x >= 0);
144   ph2.add_constraint(x <= 5);
145 
146   print_constraints(ph2, "*** ph2 ***");
147 
148   C_Polyhedron computed_result = ph1;
149 
150   computed_result.simplify_using_context_assign(ph2);
151 
152   C_Polyhedron known_result(1);
153 
154   bool ok = (computed_result == known_result);
155 
156   print_constraints(computed_result,
157                     "*** ph1.simplify_using_context_assign ***");
158 
159   return ok;
160 }
161 
162 bool
test04()163 test04() {
164   Variable i(0);
165   Variable j(1);
166   Variable k(2);
167 
168   C_Polyhedron ph1 = C_Polyhedron(3, UNIVERSE);
169   ph1.add_constraint(i >= 1);
170   ph1.add_constraint(i <= 10);
171   ph1.add_constraint(j >= 1);
172   ph1.add_constraint(j <= 10);
173   ph1.add_constraint(k == 0);
174 
175   C_Polyhedron ph2 = C_Polyhedron(3, UNIVERSE);
176   ph2.add_constraint(i >= 0);
177   ph2.add_constraint(i <= 2);
178   ph2.add_constraint(j >= 2);
179   ph2.add_constraint(j <= 9);
180   ph2.add_constraint(k == 0);
181 
182   print_constraints(ph1, "=== ph1 ===");
183   print_constraints(ph2, "=== ph2 ===");
184 
185   C_Polyhedron known_result = C_Polyhedron(3, UNIVERSE);
186   known_result.add_constraint(i >= 1);
187 
188   ph1.simplify_using_context_assign(ph2);
189 
190   bool ok = (ph1 == known_result);
191 
192   print_constraints(ph1, "=== ph1.simplify_using_context_assign(ph2) ===");
193 
194   return ok;
195 }
196 
197 bool
test05()198 test05() {
199   Variable i(0);
200   Variable j(1);
201   Variable k(2);
202 
203   C_Polyhedron ph1(3, UNIVERSE);
204   ph1.add_constraint(i == 1);
205   ph1.add_constraint(j + 1 == 0);
206   ph1.add_constraint(k == 3);
207 
208   C_Polyhedron ph2(3, UNIVERSE);
209   ph2.add_constraint(i == 1);
210   ph2.add_constraint(j + k == 2);
211   ph2.add_constraint(k >= 0);
212   ph2.add_constraint(k <= 3);
213 
214   C_Polyhedron known_result(3, UNIVERSE);
215   known_result.add_constraint(k == 3);
216   // PolyLib 5.22.3 does not simplify away the following equality.
217   // known_result.add_constraint(j + 1 == 0);
218 
219   ph1.simplify_using_context_assign(ph2);
220 
221   bool ok = (ph1 == known_result);
222 
223   print_constraints(ph1, "=== ph1.simplify_using_context_assign(ph2) ===");
224 
225   return ok;
226 }
227 
228 bool
test06()229 test06() {
230   Variable A(0);
231   Variable B(1);
232   Variable C(2);
233 
234   C_Polyhedron ph1(3, UNIVERSE);
235   ph1.add_constraint(A == 0);
236   ph1.add_constraint(B == C);
237   ph1.add_constraint(B >= 2);
238   print_constraints(ph1, "\n=== ph1 ===");
239 
240   C_Polyhedron ph2(3, UNIVERSE);
241   ph2.add_constraint(A == 0);
242   ph2.add_constraint(C >= 2);
243   print_constraints(ph2, "\n=== ph2 ===");
244 
245   ph1.simplify_using_context_assign(ph2);
246 
247   C_Polyhedron known_result(3, UNIVERSE);
248   known_result.add_constraint(B == C);
249 
250   bool ok = (ph1 == known_result);
251 
252   print_constraints(ph1, "\n=== ph1.simplify_using_context_assign(ph2) ===");
253 
254   return ok;
255 }
256 
257 bool
test07()258 test07() {
259   Variable x(0);
260   Variable y(1);
261 
262   C_Polyhedron p(2);
263   p.add_constraint(x == 0);
264   p.add_constraint(y == 0);
265 
266   C_Polyhedron q(2);
267   q.add_constraint(x >= 0);
268   q.add_constraint(y >= 0);
269 
270   C_Polyhedron known_result(p);
271 
272   print_constraints(p, "*** p ***");
273   print_constraints(q, "*** q ***");
274 
275   (void) p.simplify_using_context_assign(q);
276 
277   bool ok = (p == known_result);
278 
279   print_constraints(p, "*** p.simplify_using_context_assign(q) ***");
280 
281   return ok;
282 }
283 
284 bool
test08()285 test08() {
286   Variable x(0);
287   Variable y(1);
288 
289   C_Polyhedron p(2);
290   p.add_constraint(x <= 0);
291   p.add_constraint(y <= 0);
292 
293   C_Polyhedron q(2);
294   q.add_constraint(x >= 0);
295   q.add_constraint(y >= 0);
296 
297   C_Polyhedron known_result(p);
298 
299   print_constraints(p, "*** p ***");
300   print_constraints(q, "*** q ***");
301 
302   (void) p.simplify_using_context_assign(q);
303 
304   bool ok = (p == known_result);
305 
306   print_constraints(p, "*** p.simplify_using_context_assign(q) ***");
307 
308   return ok;
309 }
310 
311 bool
test09()312 test09() {
313   Variable A(0);
314 
315   C_Polyhedron ph1(1);
316   C_Polyhedron ph2(1);
317 
318   ph2.add_constraint(A == 0);
319 
320   print_constraints(ph1, "*** ph1 ***");
321   print_constraints(ph2, "*** ph2 ***");
322 
323   C_Polyhedron known_result = ph1;
324 
325   ph1.simplify_using_context_assign(ph2);
326 
327   bool ok = (ph1 == known_result);
328 
329   print_constraints(ph1,
330                     "*** after ph1.simplify_using_context_assign(ph2) ***");
331 
332   return ok;
333 }
334 
335 bool
test10()336 test10() {
337   Variable i(0);
338   Variable j(1);
339   Variable k(2);
340 
341   C_Polyhedron ph1(3, UNIVERSE);
342   ph1.add_constraint(i >= 1);
343   ph1.add_constraint(i <= 10);
344   ph1.add_constraint(j >= 1);
345   ph1.add_constraint(j <= 10);
346   ph1.add_constraint(k == 0);
347 
348   C_Polyhedron ph2(3, UNIVERSE);
349   ph2.add_constraint(i <= 25);
350   ph2.add_constraint(j <= 25);
351   ph2.add_constraint(i + j >= 25);
352   ph2.add_constraint(k == 0);
353 
354   C_Polyhedron known_result(3, UNIVERSE);
355   known_result.add_constraint(i <= 10);
356   known_result.add_constraint(j <= 10);
357 
358   ph1.simplify_using_context_assign(ph2);
359 
360   bool ok = (ph1 == known_result);
361 
362   print_constraints(ph1);
363 
364   return ok;
365 }
366 
367 bool
test11()368 test11() {
369   C_Polyhedron ph1(0, EMPTY);
370   C_Polyhedron ph2;
371 
372   print_constraints(ph1, "*** ph1 ***");
373   print_constraints(ph2, "*** ph2 ***");
374 
375   C_Polyhedron known_result = ph1;
376 
377   ph1.simplify_using_context_assign(ph2);
378 
379   bool ok = (ph1 == known_result);
380 
381   print_constraints(ph1,
382             "*** after ph1.simplify_using_context_assign(ph2) ***");
383 
384   return ok;
385 }
386 
387 bool
test12()388 test12() {
389 
390   C_Polyhedron ph1(0, EMPTY);
391 
392   print_constraints(ph1, "*** ph1 ***");
393 
394   C_Polyhedron ph2(0, EMPTY);
395 
396   print_constraints(ph2, "*** ph2 ***");
397 
398   C_Polyhedron known_result(0, UNIVERSE);
399 
400   bool ok = !ph1.simplify_using_context_assign(ph2);
401   ok &= (ph1 == known_result);
402 
403   print_constraints(ph1,
404                    "*** ph1.simplify_using_context_assign(ph2) ***");
405   return ok;
406 }
407 
408 bool
test13()409 test13() {
410 
411   C_Polyhedron ph1(0, EMPTY);
412 
413   print_constraints(ph1, "*** ph1 ***");
414 
415   C_Polyhedron ph2(0, UNIVERSE);
416 
417   print_constraints(ph2, "*** ph2 ***");
418 
419   C_Polyhedron known_result(0, EMPTY);
420 
421   bool ok = !ph1.simplify_using_context_assign(ph2);
422   ok &= (ph1 == known_result);
423 
424   print_constraints(ph1,
425                    "*** ph1.simplify_using_context_assign(ph2) ***");
426   return ok;
427 }
428 
429 bool
test14()430 test14() {
431 
432   C_Polyhedron ph1(0, UNIVERSE);
433 
434   print_constraints(ph1, "*** ph1 ***");
435 
436   C_Polyhedron ph2(0, EMPTY);
437 
438   print_constraints(ph2, "*** ph2 ***");
439 
440   C_Polyhedron known_result(0, UNIVERSE);
441 
442   bool ok = !ph1.simplify_using_context_assign(ph2);
443   ok &= (ph1 == known_result);
444 
445   print_constraints(ph1,
446                    "*** ph1.simplify_using_context_assign(ph2) ***");
447   return ok;
448 }
449 
450 bool
test15()451 test15() {
452 
453   C_Polyhedron ph1(0, UNIVERSE);
454 
455   print_constraints(ph1, "*** ph1 ***");
456 
457   C_Polyhedron ph2(0, UNIVERSE);
458 
459   print_constraints(ph2, "*** ph2 ***");
460 
461   C_Polyhedron known_result(0, UNIVERSE);
462 
463   bool ok = ph1.simplify_using_context_assign(ph2);
464   ok &= (ph1 == known_result);
465 
466   print_constraints(ph1,
467                    "*** ph1.simplify_using_context_assign(ph2) ***");
468   return ok;
469 }
470 
471 } // namespace
472 
473 BEGIN_MAIN
474   DO_TEST_F8A(test01);
475   DO_TEST_F8(test02);
476   DO_TEST(test03);
477   DO_TEST(test04);
478   DO_TEST(test05);
479   DO_TEST(test06);
480   DO_TEST(test07);
481   DO_TEST(test08);
482   DO_TEST(test09);
483   DO_TEST(test10);
484   DO_TEST(test11);
485   DO_TEST(test12);
486   DO_TEST(test13);
487   DO_TEST(test14);
488   DO_TEST(test15);
489 END_MAIN
490