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