1 /* Test Box::propagate_constraints().
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 struct Edge {
29 unsigned int from;
30 unsigned int to;
31 unsigned long distance;
32 };
33
34 Edge hawaii[] = {
35 { 0, 1, 6191 },
36 { 1, 0, 6191 },
37 { 2, 3, 4147 },
38 { 3, 2, 4147 },
39 { 4, 5, 3884 },
40 { 5, 4, 3884 },
41 { 5, 6, 1609 },
42 { 6, 5, 1609 },
43 { 7, 0, 12521 },
44 { 0, 7, 12521 },
45 { 8, 1, 2872 },
46 { 1, 8, 2872 },
47 { 9, 10, 4036 },
48 { 10, 9, 4036 },
49 { 4, 11, 2959 },
50 { 11, 4, 2959 },
51 { 12, 13, 27415 },
52 { 13, 12, 27415 },
53 { 14, 15, 6068 },
54 { 15, 14, 6068 },
55 { 15, 16, 7337 },
56 { 16, 15, 7337 },
57 { 17, 18, 2894 },
58 { 18, 17, 2894 },
59 { 18, 19, 5425 },
60 { 19, 18, 5425 },
61 { 20, 21, 2265 },
62 { 21, 20, 2265 },
63 { 19, 20, 3008 },
64 { 20, 19, 3008 },
65 { 21, 12, 6654 },
66 { 12, 21, 6654 },
67 { 22, 23, 1563 },
68 { 23, 22, 1563 },
69 { 23, 24, 3470 },
70 { 24, 23, 3470 },
71 { 25, 26, 6536 },
72 { 26, 25, 6536 },
73 { 27, 28, 10373 },
74 { 28, 27, 10373 },
75 { 28, 29, 7866 },
76 { 29, 28, 7866 },
77 { 29, 30, 8961 },
78 { 30, 29, 8961 },
79 { 31, 32, 6954 },
80 { 32, 31, 6954 },
81 { 33, 34, 24135 },
82 { 34, 33, 24135 },
83 { 34, 35, 5943 },
84 { 35, 34, 5943 },
85 { 33, 36, 2389 },
86 { 36, 33, 2389 },
87 { 35, 37, 3374 },
88 { 37, 35, 3374 },
89 { 34, 38, 4494 },
90 { 38, 34, 4494 },
91 { 37, 38, 8295 },
92 { 38, 37, 8295 },
93 { 38, 39, 12091 },
94 { 39, 38, 12091 },
95 { 39, 40, 4356 },
96 { 40, 39, 4356 },
97 { 39, 30, 3986 },
98 { 30, 39, 3986 },
99 { 29, 41, 3937 },
100 { 41, 29, 3937 },
101 { 41, 28, 7159 },
102 { 28, 41, 7159 },
103 { 42, 43, 3887 },
104 { 43, 42, 3887 },
105 { 43, 44, 3685 },
106 { 44, 43, 3685 },
107 { 43, 45, 20903 },
108 { 45, 43, 20903 },
109 { 45, 46, 2226 },
110 { 46, 45, 2226 },
111 { 47, 44, 7487 },
112 { 44, 47, 7487 },
113 { 44, 48, 22511 },
114 { 48, 44, 22511 },
115 { 46, 48, 7280 },
116 { 48, 46, 7280 },
117 { 48, 49, 3112 },
118 { 49, 48, 3112 },
119 { 49, 50, 2530 },
120 { 50, 49, 2530 },
121 { 50, 51, 17408 },
122 { 51, 50, 17408 },
123 { 45, 52, 15249 },
124 { 52, 45, 15249 },
125 { 53, 54, 36470 },
126 { 54, 53, 36470 },
127 { 54, 49, 7694 },
128 { 49, 54, 7694 },
129 { 51, 55, 11400 },
130 { 55, 51, 11400 },
131 { 52, 46, 15473 },
132 { 46, 52, 15473 },
133 { 55, 56, 37433 },
134 { 56, 55, 37433 },
135 { 53, 57, 3855 },
136 { 57, 53, 3855 },
137 { 57, 58, 1508 },
138 { 58, 57, 1508 },
139 { 59, 60, 3574 },
140 { 60, 59, 3574 },
141 { 59, 53, 7377 },
142 { 53, 59, 7377 },
143 { 58, 60, 6801 },
144 { 60, 58, 6801 },
145 { 60, 61, 9191 },
146 { 61, 60, 9191 },
147 { 61, 62, 3940 },
148 { 62, 61, 3940 },
149 { 62, 63, 1941 },
150 { 63, 62, 1941 },
151 { 63, 64, 17861 },
152 { 64, 63, 17861 },
153 { 65, 66, 12138 },
154 { 66, 65, 12138 },
155 { 66, 67, 5764 },
156 { 67, 66, 5764 },
157 { 68, 62, 2365 },
158 { 62, 68, 2365 },
159 { 69, 70, 14756 },
160 { 70, 69, 14756 },
161 { 70, 71, 3931 },
162 { 71, 70, 3931 },
163 { 71, 72, 6955 },
164 { 72, 71, 6955 },
165 { 69, 73, 4265 },
166 { 73, 69, 4265 },
167 { 73, 56, 5278 },
168 { 56, 73, 5278 },
169 { 74, 75, 1088 },
170 { 75, 74, 1088 },
171 { 76, 77, 2549 },
172 { 77, 76, 2549 },
173 { 78, 79, 2029 },
174 { 79, 78, 2029 },
175 { 80, 81, 4607 },
176 { 81, 80, 4607 },
177 { 81, 82, 995 },
178 { 82, 81, 995 },
179 { 82, 83, 5708 },
180 { 83, 82, 5708 },
181 { 83, 84, 1015 },
182 { 84, 83, 1015 },
183 { 85, 86, 2592 },
184 { 86, 85, 2592 },
185 { 86, 75, 9272 },
186 { 75, 86, 9272 },
187 { 86, 87, 1549 },
188 { 87, 86, 1549 },
189 { 87, 88, 1155 },
190 { 88, 87, 1155 },
191 { 85, 84, 8375 },
192 { 84, 85, 8375 },
193 { 84, 89, 3022 },
194 { 89, 84, 3022 },
195 { 89, 90, 6455 },
196 { 90, 89, 6455 },
197 { 80, 91, 2912 },
198 { 91, 80, 2912 },
199 { 78, 92, 2087 },
200 { 92, 78, 2087 },
201 { 91, 76, 7736 },
202 { 76, 91, 7736 },
203 { 88, 85, 2143 },
204 { 85, 88, 2143 },
205 { 93, 8, 9507 },
206 { 8, 93, 9507 },
207 { 89, 88, 9385 },
208 { 88, 89, 9385 },
209 { 64, 65, 24795 },
210 { 65, 64, 24795 },
211 { 54, 94, 32035 },
212 { 94, 54, 32035 },
213 { 94, 56, 35025 },
214 { 56, 94, 35025 },
215 { 69, 95, 25243 },
216 { 95, 69, 25243 },
217 { 67, 96, 30757 },
218 { 96, 67, 30757 },
219 { 96, 97, 859 },
220 { 97, 96, 859 },
221 { 97, 95, 3230 },
222 { 95, 97, 3230 },
223 { 1, 9, 16155 },
224 { 9, 1, 16155 },
225 { 98, 51, 11706 },
226 { 51, 98, 11706 },
227 { 75, 99, 51590 },
228 { 99, 75, 51590 },
229 { 11, 100, 23417 },
230 { 100, 11, 23417 },
231 { 100, 101, 12368 },
232 { 101, 100, 12368 },
233 { 102, 103, 4846 },
234 { 103, 102, 4846 },
235 { 103, 104, 2901 },
236 { 104, 103, 2901 },
237 { 10, 104, 7849 },
238 { 104, 10, 7849 },
239 { 104, 2, 2147 },
240 { 2, 104, 2147 },
241 { 2, 102, 1761 },
242 { 102, 2, 1761 },
243 { 102, 4, 4444 },
244 { 4, 102, 4444 },
245 { 74, 105, 8183 },
246 { 105, 74, 8183 },
247 { 106, 107, 7075 },
248 { 107, 106, 7075 },
249 { 89, 107, 1178 },
250 { 107, 89, 1178 },
251 { 108, 81, 1312 },
252 { 81, 108, 1312 },
253 { 81, 109, 1793 },
254 { 109, 81, 1793 },
255 { 82, 108, 1001 },
256 { 108, 82, 1001 },
257 { 108, 80, 7421 },
258 { 80, 108, 7421 },
259 { 110, 92, 434 },
260 { 92, 110, 434 },
261 { 92, 79, 3285 },
262 { 79, 92, 3285 },
263 { 79, 99, 2706 },
264 { 99, 79, 2706 },
265 { 111, 78, 3052 },
266 { 78, 111, 3052 },
267 { 77, 111, 2036 },
268 { 111, 77, 2036 },
269 { 24, 25, 2634 },
270 { 25, 24, 2634 },
271 { 25, 21, 1832 },
272 { 21, 25, 1832 },
273 { 33, 112, 14461 },
274 { 112, 33, 14461 },
275 { 113, 114, 7998 },
276 { 114, 113, 7998 },
277 { 41, 115, 6937 },
278 { 115, 41, 6937 },
279 { 32, 116, 47595 },
280 { 116, 32, 47595 },
281 { 99, 117, 3887 },
282 { 117, 99, 3887 },
283 { 117, 118, 736 },
284 { 118, 117, 736 },
285 { 85, 83, 9281 },
286 { 83, 85, 9281 },
287 { 118, 80, 4823 },
288 { 80, 118, 4823 },
289 { 77, 119, 22341 },
290 { 119, 77, 22341 },
291 { 56, 120, 1612 },
292 { 120, 56, 1612 },
293 { 79, 121, 3258 },
294 { 121, 79, 3258 },
295 { 52, 57, 25357 },
296 { 57, 52, 25357 },
297 { 99, 121, 1646 },
298 { 121, 99, 1646 },
299 { 121, 76, 1359 },
300 { 76, 121, 1359 },
301 { 37, 27, 3890 },
302 { 27, 37, 3890 },
303 { 27, 31, 5066 },
304 { 31, 27, 5066 },
305 { 122, 123, 2556 },
306 { 123, 122, 2556 },
307 { 90, 122, 947 },
308 { 122, 90, 947 },
309 { 122, 124, 911 },
310 { 124, 122, 911 },
311 { 124, 125, 23829 },
312 { 125, 124, 23829 },
313 { 91, 119, 7911 },
314 { 119, 91, 7911 },
315 };
316
317 Edge hawaii1[] = {
318 { 1, 0, 600 },
319 { 2, 1, 2872 },
320 };
321
322 Edge hawaii2[] = {
323 { 0, 1, 600 },
324 { 1, 2, 2872 },
325 };
326
327 const mpq_class&
perturbate(unsigned long a)328 perturbate(unsigned long a) {
329 static mpq_class q;
330 q = a;
331 q = (q*q)/(q-1);
332 return q;
333 }
334
335 template <typename T>
336 void
propagate_edges(Box<T> & box,const Edge * edges,unsigned n)337 propagate_edges(Box<T>& box, const Edge* edges, unsigned n) {
338 Constraint_System cs;
339 for (unsigned i = 0; i < n; ++i) {
340 const mpq_class& q = perturbate(edges[i].distance);
341 Coefficient a;
342 a = q.get_den();
343 Coefficient b;
344 b = q.get_num();
345
346 vnout << "a = " << a << "; b = " << b << endl;
347
348 cs.insert(a*Variable(edges[i].from) - a*Variable(edges[i].to) <= b);
349 }
350 box.propagate_constraints(cs);
351 }
352
353 } // namespace
354
test01()355 bool test01() {
356 Rational_Box qbox1(126);
357
358 qbox1.add_constraint(Variable(0) >= 100000);
359 qbox1.add_constraint(Variable(0) <= 100001);
360 qbox1.add_constraint(Variable(12) >= 110000);
361 qbox1.add_constraint(Variable(12) <= 110001);
362 qbox1.add_constraint(Variable(14) >= 120000);
363 qbox1.add_constraint(Variable(14) <= 120001);
364 qbox1.add_constraint(Variable(27) >= 130000);
365 qbox1.add_constraint(Variable(27) <= 130001);
366 qbox1.add_constraint(Variable(42) >= 140000);
367 qbox1.add_constraint(Variable(42) <= 140001);
368 qbox1.add_constraint(Variable(113) >= 150000);
369 qbox1.add_constraint(Variable(113) <= 150001);
370 qbox1.add_constraint(Variable(125) >= 200000);
371 qbox1.add_constraint(Variable(125) <= 200001);
372
373 Rational_Box qbox2(qbox1);
374
375 print_constraints(qbox1, "*** qbox1, qbox2 ***");
376
377 propagate_edges(qbox2, hawaii, sizeof(hawaii)/sizeof(Edge));
378
379 print_constraints(qbox2, "*** qbox2.propagate_edges() ***");
380
381 TBox tbox(qbox1);
382
383 print_constraints(tbox, "*** tbox ***");
384
385 propagate_edges(tbox, hawaii, sizeof(hawaii)/sizeof(Edge));
386
387 print_constraints(tbox, "*** tbox.propagate_edges() ***");
388
389 #if PPL_SUPPORTED_DOUBLE
390 bool ok = check_result(tbox, qbox2, "18.36", "2.83", "2.79");
391 #else
392 bool ok = check_result(tbox, qbox2, "30.96", "2.83", "2.79");
393 #endif
394
395 return ok;
396 }
397
test02()398 bool test02() {
399 Rational_Box qbox1(3);
400
401 qbox1.add_constraint(Variable(0) <= 0);
402
403 Rational_Box qbox2(qbox1);
404
405 print_constraints(qbox1, "*** qbox1, qbox2 ***");
406
407 propagate_edges(qbox2, hawaii1, sizeof(hawaii1)/sizeof(Edge));
408
409 print_constraints(qbox2, "*** qbox2.propagate_edges() ***");
410
411 TBox tbox(qbox1);
412
413 print_constraints(tbox, "*** tbox ***");
414
415 propagate_edges(tbox, hawaii1, sizeof(hawaii1)/sizeof(Edge));
416
417 print_constraints(tbox, "*** tbox.propagate_edges() ***");
418
419 bool ok = check_result(tbox, qbox2, "3.28", "2.83", "2.79");
420
421 return ok;
422 }
423
test03()424 bool test03() {
425 Rational_Box qbox1(3);
426
427 qbox1.add_constraint(Variable(0) >= 0);
428
429 Rational_Box qbox2(qbox1);
430
431 print_constraints(qbox1, "*** qbox1, qbox2 ***");
432
433 propagate_edges(qbox2, hawaii2, sizeof(hawaii2)/sizeof(Edge));
434
435 print_constraints(qbox2, "*** qbox2.propagate_edges() ***");
436
437 TBox tbox(qbox1);
438
439 print_constraints(tbox, "*** tbox ***");
440
441 propagate_edges(tbox, hawaii2, sizeof(hawaii2)/sizeof(Edge));
442
443 print_constraints(tbox, "*** tbox.propagate_edges() ***");
444
445 bool ok = check_result(tbox, qbox2, "3.28", "2.83", "2.78");
446
447 return ok;
448 }
449
450 BEGIN_MAIN
451 DO_TEST_F32(test01);
452 DO_TEST_F16(test02);
453 DO_TEST_F16(test03);
454 END_MAIN
455