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