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