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