1 /* Test BD_Shape::relation_with().
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 A(0);
31 Variable B(1);
32 Variable C(2);
33
34 TBD_Shape bds(2);
35 bds.add_constraint(A >= 1);
36
37 try {
38 // This is an incorrect use of method
39 // BD_Shape::relation_with(c):
40 // it is illegal to use a constraint that is
41 // dimensional incompatible with the BDS.
42 Poly_Con_Relation rel = bds.relation_with(C - B <= 2);
43 (void) rel;
44 }
45 catch (std::invalid_argument& e) {
46 nout << "std::invalid_argument: " << endl;
47 return true;
48 }
49 catch (...) {
50 }
51 return false;
52 }
53
54 bool
test02()55 test02() {
56 Variable A(0);
57 Variable B(1);
58 Variable C(2);
59
60 TBD_Shape bds(3);
61 bds.add_constraint(A >= 1);
62
63 Poly_Con_Relation rel = bds.relation_with(A - 2*B <= 2);
64 Poly_Con_Relation known_result = Poly_Con_Relation::strictly_intersects();
65 print_constraints(bds, "*** bds ***");
66
67 return rel == known_result;
68 }
69
70 bool
test03()71 test03() {
72 Variable A(0);
73 Variable B(1);
74 Variable C(2);
75
76 TBD_Shape bds(2);
77 bds.add_constraint(A >= 1);
78
79 try {
80 // This is an incorrect use of method
81 // BD_Shape::relation_with(c):
82 // it is illegal to use a generator that is
83 // dimensional incompatible with the BDS.
84 Poly_Gen_Relation rel = bds.relation_with(ray(C));
85 (void) rel;
86 }
87 catch (std::invalid_argument& e) {
88 nout << "std::invalid_argument: " << endl;
89 return true;
90 }
91 catch (...) {
92 }
93 return false;
94 }
95
96 bool
test04()97 test04() {
98 Variable A(0);
99
100 TBD_Shape bds(1);
101 bds.add_constraint(A == -1);
102
103 Poly_Con_Relation rel = bds.relation_with(A == 0);
104
105 print_constraints(bds, "*** bds ***");
106 using namespace IO_Operators;
107 nout << "bds.relation_with(A == 0) == " << rel << endl;
108
109 Poly_Con_Relation known_result = Poly_Con_Relation::is_disjoint();
110
111 return rel == known_result;
112 }
113
114 bool
test05()115 test05() {
116 Variable A(0);
117
118 TBD_Shape bds(1);
119 bds.add_constraint(A == -1);
120
121 Poly_Con_Relation rel = bds.relation_with(A >= 0);
122
123 print_constraints(bds, "*** bds ***");
124 using namespace IO_Operators;
125 nout << "bds.relation_with(A >= 0) == " << rel << endl;
126
127 Poly_Con_Relation known_result = Poly_Con_Relation::is_disjoint();
128
129 return rel == known_result;
130 }
131
132 bool
test06()133 test06() {
134 Variable A(0);
135
136 TBD_Shape bds(1);
137 bds.add_constraint(A == -1);
138
139 Poly_Con_Relation rel = bds.relation_with(A <= -2);
140
141 print_constraints(bds, "*** bds ***");
142 using namespace IO_Operators;
143 nout << "bds.relation_with(A <= -2) == " << rel << endl;
144
145 Poly_Con_Relation known_result = Poly_Con_Relation::is_disjoint();
146
147 return rel == known_result;
148 }
149
150 bool
test07()151 test07() {
152 Variable A(0);
153
154 TBD_Shape bds(1);
155 bds.add_constraint(A == -1);
156
157 Poly_Con_Relation rel = bds.relation_with(A == -1);
158
159 print_constraints(bds, "*** bds ***");
160 using namespace IO_Operators;
161 nout << "bds.relation_with(A == -1) == " << rel << endl;
162
163 Poly_Con_Relation known_result = Poly_Con_Relation::is_included() &&
164 Poly_Con_Relation::saturates();
165
166 return rel == known_result;
167 }
168
169 bool
test08()170 test08() {
171 Variable A(0);
172 Variable B(1);
173
174 TBD_Shape bds(2);
175 bds.add_constraint(A - B == -1);
176
177 Poly_Con_Relation rel = bds.relation_with(A - B == 0);
178
179 print_constraints(bds, "*** bds ***");
180 using namespace IO_Operators;
181 nout << "bds.relation_with(A == 0) == " << rel << endl;
182
183 Poly_Con_Relation known_result = Poly_Con_Relation::is_disjoint();
184
185 return rel == known_result;
186 }
187
188 bool
test09()189 test09() {
190 Variable A(0);
191 Variable B(1);
192
193 TBD_Shape bds(2);
194 bds.add_constraint(A - B == -1);
195
196 Poly_Con_Relation rel = bds.relation_with(A - B >= 0);
197
198 print_constraints(bds, "*** bds ***");
199 using namespace IO_Operators;
200 nout << "bds.relation_with(A >= 0) == " << rel << endl;
201
202 Poly_Con_Relation known_result = Poly_Con_Relation::is_disjoint();
203
204 return rel == known_result;
205 }
206
207 bool
test10()208 test10() {
209 Variable A(0);
210 Variable B(1);
211
212 TBD_Shape bds(2);
213 bds.add_constraint(A - B == -1);
214
215 Poly_Con_Relation rel = bds.relation_with(A - B <= -2);
216
217 print_constraints(bds, "*** bds ***");
218 using namespace IO_Operators;
219 nout << "bds.relation_with(A <= -2) == " << rel << endl;
220
221 Poly_Con_Relation known_result = Poly_Con_Relation::is_disjoint();
222
223 return rel == known_result;
224 }
225
226 bool
test11()227 test11() {
228 Variable A(0);
229 Variable B(1);
230
231 TBD_Shape bds(2);
232 bds.add_constraint(A - B == -1);
233
234 Poly_Con_Relation rel = bds.relation_with(A - B == -1);
235
236 print_constraints(bds, "*** bds ***");
237 using namespace IO_Operators;
238 nout << "bds.relation_with(A == -1) == " << rel << endl;
239
240 Poly_Con_Relation known_result = Poly_Con_Relation::is_included() &&
241 Poly_Con_Relation::saturates();
242
243 return rel == known_result;
244 }
245
246 bool
test12()247 test12() {
248 Variable A(0);
249 Variable B(1);
250
251 TBD_Shape bds(2);
252 bds.add_constraint(A - B == -1);
253
254 Poly_Con_Relation rel = bds.relation_with(A - B == -2);
255
256 print_constraints(bds, "*** bds ***");
257 using namespace IO_Operators;
258 nout << "bds.relation_with(A == -1) == " << rel << endl;
259
260 Poly_Con_Relation known_result = Poly_Con_Relation::is_disjoint();
261
262 return rel == known_result;
263 }
264
265 bool
test13()266 test13() {
267 // A 1D empty BDS that is not in minimal form and the point is the origin.
268 Variable A(0);
269
270 TBD_Shape bds(1);
271 bds.add_constraint(A <= 0);
272 bds.add_constraint(A >= 1);
273
274 Generator g = point();
275 Poly_Gen_Relation rel = bds.relation_with(g);
276
277 print_constraints(bds, "*** bds ***");
278 print_generator(g, "*** g ***");
279 using namespace IO_Operators;
280 nout << "bds.relation_with(v()) == " << rel << endl;
281
282 Poly_Gen_Relation known_result = Poly_Gen_Relation::nothing();
283
284 return rel == known_result;
285 }
286
287 bool
test14()288 test14() {
289 // A single point does not subsume another (different) point.
290 Variable A(0);
291
292 TBD_Shape bds(1);
293 bds.add_constraint(A == 1);
294
295 Generator g = point();
296 Poly_Gen_Relation rel = bds.relation_with(g);
297
298 print_constraints(bds, "*** bds ***");
299 print_generator(g, "*** g ***");
300 using namespace IO_Operators;
301 nout << "bds.relation_with(v()) == " << rel << endl;
302
303 Poly_Gen_Relation known_result = Poly_Gen_Relation::nothing();
304
305 return rel == known_result;
306 }
307
308 bool
test15()309 test15() {
310 // A single point does not subsume another (different) point.
311 Variable A(0);
312
313 TBD_Shape bds(1);
314 bds.add_constraint(A == 1);
315
316 Generator g = point(3*A, 2);
317 Poly_Gen_Relation rel = bds.relation_with(g);
318
319 print_constraints(bds, "*** bds ***");
320 print_generator(g, "*** g ***");
321 using namespace IO_Operators;
322 nout << "bds.relation_with(v()) == " << rel << endl;
323
324 Poly_Gen_Relation known_result = Poly_Gen_Relation::nothing();
325
326 return rel == known_result;
327 }
328
329 bool
test16()330 test16() {
331 // A single point does not subsume another (different) point.
332 Variable A(0);
333
334 BD_Shape<mpz_class> bds(1);
335 bds.add_constraint(A >= 0);
336 bds.add_constraint(A <= 1);
337
338 Constraint c(2*A == 1);
339 Poly_Con_Relation rel = bds.relation_with(c);
340
341 print_constraints(bds, "*** bds ***");
342 print_constraint(c, "*** c ***");
343 using namespace IO_Operators;
344 nout << "bds.relation_with(c) == " << rel << endl;
345
346 Poly_Con_Relation known_result = Poly_Con_Relation::strictly_intersects();
347
348 return rel == known_result;
349 }
350
351 bool
test17()352 test17() {
353 Variable A(0);
354
355 TBD_Shape bds(1);
356 bds.add_constraint(A >= 0);
357 bds.add_constraint(A <= 1);
358
359 Constraint c(Linear_Expression(1) == 0);
360 Poly_Con_Relation rel = bds.relation_with(c);
361
362 print_constraints(bds, "*** bds ***");
363 print_constraint(c, "*** c ***");
364 using namespace IO_Operators;
365 nout << "bds.relation_with(c) == " << rel << endl;
366
367 Poly_Con_Relation known_result = Poly_Con_Relation::is_disjoint();
368
369 return rel == known_result;
370 }
371
372 bool
test18()373 test18() {
374 Variable A(0);
375
376 TBD_Shape bds(1);
377 bds.add_constraint(A >= 0);
378 bds.add_constraint(A <= 1);
379
380 Congruence cg((A %= 0) / 0);
381 Poly_Con_Relation rel = bds.relation_with(cg);
382
383 print_constraints(bds, "--- bds ---");
384 print_congruence(cg, "--- cg ---");
385 using namespace IO_Operators;
386 nout << "bds.relation_with(A == 0) == " << rel << endl;
387
388 Poly_Con_Relation known_result = Poly_Con_Relation::strictly_intersects();
389
390 return rel == known_result;
391 }
392
393 bool
test19()394 test19() {
395 Variable A(0);
396 Variable B(1);
397
398 TBD_Shape bds(2);
399 bds.add_constraint(A >= 0);
400 bds.add_constraint(B >= 0);
401 bds.add_constraint(B <= 2);
402 bds.add_constraint(A - B <= 1);
403
404 Congruence cg((A + 3*B %= 1) / 10);
405 Poly_Con_Relation rel = bds.relation_with(cg);
406
407 print_constraints(bds, "--- bds ---");
408 print_congruence(cg, "--- cg ---");
409 using namespace IO_Operators;
410 nout << "bds.relation_with((A + 3*B %= 1)/10) == " << rel << endl;
411
412 Poly_Con_Relation known_result = Poly_Con_Relation::strictly_intersects();
413
414 return rel == known_result;
415 }
416
417 bool
test20()418 test20() {
419 Variable A(0);
420 Variable B(1);
421
422 TBD_Shape bds(2);
423 bds.add_constraint(A >= 0);
424 bds.add_constraint(B >= 0);
425 bds.add_constraint(B <= 2);
426 bds.add_constraint(A - B <= 1);
427
428 Congruence cg((A + 3*B %= 10) / 11);
429 Poly_Con_Relation rel = bds.relation_with(cg);
430
431 print_constraints(bds, "--- bds ---");
432 print_congruence(cg, "--- cg ---");
433 using namespace IO_Operators;
434 nout << "bds.relation_with((A + 3*B %= 1)/10) == " << rel << endl;
435
436 Poly_Con_Relation known_result = Poly_Con_Relation::is_disjoint();
437
438 return rel == known_result;
439 }
440
441 } // namespace
442
443 BEGIN_MAIN
444 DO_TEST(test01);
445 DO_TEST(test02);
446 DO_TEST(test03);
447 DO_TEST(test04);
448 DO_TEST(test05);
449 DO_TEST(test06);
450 DO_TEST(test07);
451 DO_TEST(test08);
452 DO_TEST(test09);
453 DO_TEST(test10);
454 DO_TEST(test11);
455 DO_TEST(test12);
456 DO_TEST(test13);
457 DO_TEST(test14);
458 DO_TEST(test15);
459 DO_TEST(test16);
460 DO_TEST(test17);
461 DO_TEST(test18);
462 DO_TEST(test19);
463 DO_TEST(test20);
464 END_MAIN
465