1 /* Utilities for termination analysis: template functions.
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 #ifndef PPL_termination_templates_hh
25 #define PPL_termination_templates_hh 1
26
27 #include "globals_defs.hh"
28 #include "Variable_defs.hh"
29 #include "Generator_defs.hh"
30 #include "Constraint_System_defs.hh"
31 #include "C_Polyhedron_defs.hh"
32 #include "NNC_Polyhedron_defs.hh"
33
34 #include <stdexcept>
35
36 #define PRINT_DEBUG_INFO 0
37
38 #if PRINT_DEBUG_INFO
39 #include <iostream>
40 #endif
41
42 namespace Parma_Polyhedra_Library {
43
44 namespace Implementation {
45
46 namespace Termination {
47
48 #if PRINT_DEBUG_INFO
49 static dimension_type output_function_MS_n;
50 static dimension_type output_function_MS_m;
51
52 /* Encodes which object are we printing:
53
54 0 means input constraint system;
55 1 means first output constraint system;
56 2 means second output constraint system;
57 3 means only output constraint system
58 (i.e., when first and second are the same);
59 4 means mu space.
60 */
61 static int output_function_MS_which = -1;
62
63 /*
64 Debugging output function. See the documentation of
65 fill_constraint_systems_MS() for the allocation of variable indices.
66 */
67 inline void
output_function_MS(std::ostream & s,const Variable v)68 output_function_MS(std::ostream& s, const Variable v) {
69 dimension_type id = v.id();
70 switch (output_function_MS_which) {
71 case 0:
72 if (id < output_function_MS_n) {
73 s << "x'" << id + 1;
74 }
75 else if (id < 2*output_function_MS_n) {
76 s << "x" << id - output_function_MS_n + 1;
77 }
78 else {
79 s << "WHAT?";
80 }
81 break;
82 case 1:
83 if (id < output_function_MS_n) {
84 s << "mu" << id + 1;
85 }
86 else if (id == output_function_MS_n) {
87 s << "WHAT?";
88 }
89 else if (id <= output_function_MS_n + output_function_MS_m) {
90 s << "y" << id - output_function_MS_n;
91 }
92 else {
93 s << "WHAT?";
94 }
95 break;
96 case 2:
97 case 4:
98 if (id < output_function_MS_n) {
99 s << "mu" << id + 1;
100 }
101 else if (id == output_function_MS_n) {
102 s << "mu0";
103 }
104 else if (output_function_MS_which == 2
105 && id <= output_function_MS_n + output_function_MS_m + 2) {
106 s << "z" << id - output_function_MS_n;
107 }
108 else {
109 s << "WHAT?";
110 }
111 break;
112 case 3:
113 if (id < output_function_MS_n) {
114 s << "mu" << id + 1;
115 }
116 else if (id == output_function_MS_n) {
117 s << "mu0";
118 }
119 else if (id <= output_function_MS_n + output_function_MS_m) {
120 s << "y" << id - output_function_MS_n;
121 }
122 else if (id <= output_function_MS_n + 2*output_function_MS_m + 2) {
123 s << "z" << id - (output_function_MS_n + output_function_MS_m);
124 }
125 else {
126 s << "WHAT?";
127 }
128 break;
129 default:
130 abort();
131 break;
132 }
133 }
134
135 static dimension_type output_function_PR_s;
136 static dimension_type output_function_PR_r;
137
138 /*
139 Debugging output function. See the documentation of
140 fill_constraint_system_PR() for the allocation of variable indices.
141 */
142 inline void
output_function_PR(std::ostream & s,const Variable v)143 output_function_PR(std::ostream& s, const Variable v) {
144 dimension_type id = v.id();
145 if (id < output_function_PR_s) {
146 s << "u3_" << id + 1;
147 }
148 else if (id < output_function_PR_s + output_function_PR_r) {
149 s << "u2_" << id - output_function_PR_s + 1;
150 }
151 else if (id < output_function_PR_s + 2*output_function_PR_r) {
152 s << "u1_" << id - (output_function_PR_s + output_function_PR_r) + 1;
153 }
154 else {
155 s << "WHAT?";
156 }
157 }
158 #endif
159
160 void
161 assign_all_inequalities_approximation(const Constraint_System& cs_in,
162 Constraint_System& cs_out);
163
164 template <typename PSET>
165 inline void
assign_all_inequalities_approximation(const PSET & pset,Constraint_System & cs)166 assign_all_inequalities_approximation(const PSET& pset,
167 Constraint_System& cs) {
168 assign_all_inequalities_approximation(pset.minimized_constraints(), cs);
169 }
170
171 template <>
172 void
173 assign_all_inequalities_approximation(const C_Polyhedron& ph,
174 Constraint_System& cs);
175
176 bool
177 termination_test_MS(const Constraint_System& cs);
178
179 bool
180 one_affine_ranking_function_MS(const Constraint_System& cs,
181 Generator& mu);
182
183 void
184 all_affine_ranking_functions_MS(const Constraint_System& cs,
185 C_Polyhedron& mu_space);
186
187 void
188 all_affine_quasi_ranking_functions_MS(const Constraint_System& cs,
189 C_Polyhedron& decreasing_mu_space,
190 C_Polyhedron& bounded_mu_space);
191
192 bool
193 termination_test_PR(const Constraint_System& cs_before,
194 const Constraint_System& cs_after);
195
196 bool
197 one_affine_ranking_function_PR(const Constraint_System& cs_before,
198 const Constraint_System& cs_after,
199 Generator& mu);
200
201 void
202 all_affine_ranking_functions_PR(const Constraint_System& cs_before,
203 const Constraint_System& cs_after,
204 NNC_Polyhedron& mu_space);
205
206 bool
207 termination_test_PR_original(const Constraint_System& cs);
208
209 bool
210 one_affine_ranking_function_PR_original(const Constraint_System& cs,
211 Generator& mu);
212
213 void
214 all_affine_ranking_functions_PR_original(const Constraint_System& cs,
215 NNC_Polyhedron& mu_space);
216
217 } // namespace Termination
218
219 } // namespace Implementation
220
221 template <typename PSET>
222 void
223 Termination_Helpers
assign_all_inequalities_approximation(const PSET & pset_before,const PSET & pset_after,Constraint_System & cs)224 ::assign_all_inequalities_approximation(const PSET& pset_before,
225 const PSET& pset_after,
226 Constraint_System& cs) {
227 Implementation::Termination
228 ::assign_all_inequalities_approximation(pset_before, cs);
229 cs.shift_space_dimensions(Variable(0), cs.space_dimension());
230 Constraint_System cs_after;
231 Implementation::Termination
232 ::assign_all_inequalities_approximation(pset_after, cs_after);
233 // FIXME: provide an "append" for constraint systems.
234 for (Constraint_System::const_iterator i = cs_after.begin(),
235 cs_after_end = cs_after.end(); i != cs_after_end; ++i) {
236 cs.insert(*i);
237 }
238 }
239
240 template <typename PSET>
241 bool
termination_test_MS(const PSET & pset)242 termination_test_MS(const PSET& pset) {
243 const dimension_type space_dim = pset.space_dimension();
244 if (space_dim % 2 != 0) {
245 std::ostringstream s;
246 s << "PPL::termination_test_MS(pset):\n"
247 "pset.space_dimension() == " << space_dim
248 << " is odd.";
249 throw std::invalid_argument(s.str());
250 }
251
252 using namespace Implementation::Termination;
253 Constraint_System cs;
254 assign_all_inequalities_approximation(pset, cs);
255 return termination_test_MS(cs);
256 }
257
258 template <typename PSET>
259 bool
termination_test_MS_2(const PSET & pset_before,const PSET & pset_after)260 termination_test_MS_2(const PSET& pset_before, const PSET& pset_after) {
261 const dimension_type before_space_dim = pset_before.space_dimension();
262 const dimension_type after_space_dim = pset_after.space_dimension();
263 if (after_space_dim != 2*before_space_dim) {
264 std::ostringstream s;
265 s << "PPL::termination_test_MS_2(pset_before, pset_after):\n"
266 "pset_before.space_dimension() == " << before_space_dim
267 << ", pset_after.space_dimension() == " << after_space_dim
268 << ";\nthe latter should be twice the former.";
269 throw std::invalid_argument(s.str());
270 }
271
272 using namespace Implementation::Termination;
273 Constraint_System cs;
274 Termination_Helpers
275 ::assign_all_inequalities_approximation(pset_before, pset_after, cs);
276 return termination_test_MS(cs);
277 }
278
279 template <typename PSET>
280 bool
one_affine_ranking_function_MS(const PSET & pset,Generator & mu)281 one_affine_ranking_function_MS(const PSET& pset, Generator& mu) {
282 const dimension_type space_dim = pset.space_dimension();
283 if (space_dim % 2 != 0) {
284 std::ostringstream s;
285 s << "PPL::one_affine_ranking_function_MS(pset, mu):\n"
286 "pset.space_dimension() == " << space_dim
287 << " is odd.";
288 throw std::invalid_argument(s.str());
289 }
290
291 using namespace Implementation::Termination;
292 Constraint_System cs;
293 assign_all_inequalities_approximation(pset, cs);
294 return one_affine_ranking_function_MS(cs, mu);
295 }
296
297 template <typename PSET>
298 bool
one_affine_ranking_function_MS_2(const PSET & pset_before,const PSET & pset_after,Generator & mu)299 one_affine_ranking_function_MS_2(const PSET& pset_before,
300 const PSET& pset_after,
301 Generator& mu) {
302 const dimension_type before_space_dim = pset_before.space_dimension();
303 const dimension_type after_space_dim = pset_after.space_dimension();
304 if (after_space_dim != 2*before_space_dim) {
305 std::ostringstream s;
306 s << "PPL::one_affine_ranking_function_MS_2(pset_before, pset_after, mu):\n"
307 "pset_before.space_dimension() == " << before_space_dim
308 << ", pset_after.space_dimension() == " << after_space_dim
309 << ";\nthe latter should be twice the former.";
310 throw std::invalid_argument(s.str());
311 }
312
313 using namespace Implementation::Termination;
314 Constraint_System cs;
315 Termination_Helpers
316 ::assign_all_inequalities_approximation(pset_before, pset_after, cs);
317 return one_affine_ranking_function_MS(cs, mu);
318 }
319
320 template <typename PSET>
321 void
all_affine_ranking_functions_MS(const PSET & pset,C_Polyhedron & mu_space)322 all_affine_ranking_functions_MS(const PSET& pset, C_Polyhedron& mu_space) {
323 const dimension_type space_dim = pset.space_dimension();
324 if (space_dim % 2 != 0) {
325 std::ostringstream s;
326 s << "PPL::all_affine_ranking_functions_MS(pset, mu_space):\n"
327 "pset.space_dimension() == " << space_dim
328 << " is odd.";
329 throw std::invalid_argument(s.str());
330 }
331
332 if (pset.is_empty()) {
333 mu_space = C_Polyhedron(1 + space_dim/2, UNIVERSE);
334 return;
335 }
336
337 using namespace Implementation::Termination;
338 Constraint_System cs;
339 assign_all_inequalities_approximation(pset, cs);
340 all_affine_ranking_functions_MS(cs, mu_space);
341 }
342
343 template <typename PSET>
344 void
all_affine_ranking_functions_MS_2(const PSET & pset_before,const PSET & pset_after,C_Polyhedron & mu_space)345 all_affine_ranking_functions_MS_2(const PSET& pset_before,
346 const PSET& pset_after,
347 C_Polyhedron& mu_space) {
348 const dimension_type before_space_dim = pset_before.space_dimension();
349 const dimension_type after_space_dim = pset_after.space_dimension();
350 if (after_space_dim != 2*before_space_dim) {
351 std::ostringstream s;
352 s << "PPL::all_affine_ranking_functions_MS_2"
353 << "(pset_before, pset_after, mu_space):\n"
354 << "pset_before.space_dimension() == " << before_space_dim
355 << ", pset_after.space_dimension() == " << after_space_dim
356 << ";\nthe latter should be twice the former.";
357 throw std::invalid_argument(s.str());
358 }
359
360 if (pset_before.is_empty()) {
361 mu_space = C_Polyhedron(1 + before_space_dim, UNIVERSE);
362 return;
363 }
364
365 using namespace Implementation::Termination;
366 Constraint_System cs;
367 Termination_Helpers
368 ::assign_all_inequalities_approximation(pset_before, pset_after, cs);
369 all_affine_ranking_functions_MS(cs, mu_space);
370 }
371
372 template <typename PSET>
373 void
all_affine_quasi_ranking_functions_MS(const PSET & pset,C_Polyhedron & decreasing_mu_space,C_Polyhedron & bounded_mu_space)374 all_affine_quasi_ranking_functions_MS(const PSET& pset,
375 C_Polyhedron& decreasing_mu_space,
376 C_Polyhedron& bounded_mu_space) {
377 const dimension_type space_dim = pset.space_dimension();
378 if (space_dim % 2 != 0) {
379 std::ostringstream s;
380 s << "PPL::all_affine_quasi_ranking_functions_MS"
381 << "(pset, decr_space, bounded_space):\n"
382 << "pset.space_dimension() == " << space_dim
383 << " is odd.";
384 throw std::invalid_argument(s.str());
385 }
386
387 if (pset.is_empty()) {
388 decreasing_mu_space = C_Polyhedron(1 + space_dim/2, UNIVERSE);
389 bounded_mu_space = decreasing_mu_space;
390 return;
391 }
392
393 using namespace Implementation::Termination;
394 Constraint_System cs;
395 assign_all_inequalities_approximation(pset, cs);
396 all_affine_quasi_ranking_functions_MS(cs,
397 decreasing_mu_space,
398 bounded_mu_space);
399 }
400
401 template <typename PSET>
402 void
all_affine_quasi_ranking_functions_MS_2(const PSET & pset_before,const PSET & pset_after,C_Polyhedron & decreasing_mu_space,C_Polyhedron & bounded_mu_space)403 all_affine_quasi_ranking_functions_MS_2(const PSET& pset_before,
404 const PSET& pset_after,
405 C_Polyhedron& decreasing_mu_space,
406 C_Polyhedron& bounded_mu_space) {
407 const dimension_type before_space_dim = pset_before.space_dimension();
408 const dimension_type after_space_dim = pset_after.space_dimension();
409 if (after_space_dim != 2*before_space_dim) {
410 std::ostringstream s;
411 s << "PPL::all_affine_quasi_ranking_functions_MS_2"
412 << "(pset_before, pset_after, decr_space, bounded_space):\n"
413 << "pset_before.space_dimension() == " << before_space_dim
414 << ", pset_after.space_dimension() == " << after_space_dim
415 << ";\nthe latter should be twice the former.";
416 throw std::invalid_argument(s.str());
417 }
418
419 if (pset_before.is_empty()) {
420 decreasing_mu_space = C_Polyhedron(1 + before_space_dim, UNIVERSE);
421 bounded_mu_space = decreasing_mu_space;
422 return;
423 }
424
425 using namespace Implementation::Termination;
426 Constraint_System cs;
427 Termination_Helpers
428 ::assign_all_inequalities_approximation(pset_before, pset_after, cs);
429 all_affine_quasi_ranking_functions_MS(cs,
430 decreasing_mu_space,
431 bounded_mu_space);
432 }
433
434 template <typename PSET>
435 bool
termination_test_PR_2(const PSET & pset_before,const PSET & pset_after)436 termination_test_PR_2(const PSET& pset_before, const PSET& pset_after) {
437 const dimension_type before_space_dim = pset_before.space_dimension();
438 const dimension_type after_space_dim = pset_after.space_dimension();
439 if (after_space_dim != 2*before_space_dim) {
440 std::ostringstream s;
441 s << "PPL::termination_test_PR_2(pset_before, pset_after):\n"
442 << "pset_before.space_dimension() == " << before_space_dim
443 << ", pset_after.space_dimension() == " << after_space_dim
444 << ";\nthe latter should be twice the former.";
445 throw std::invalid_argument(s.str());
446 }
447
448 using namespace Implementation::Termination;
449 Constraint_System cs_before;
450 Constraint_System cs_after;
451 assign_all_inequalities_approximation(pset_before, cs_before);
452 assign_all_inequalities_approximation(pset_after, cs_after);
453 return termination_test_PR(cs_before, cs_after);
454 }
455
456 template <typename PSET>
457 bool
termination_test_PR(const PSET & pset)458 termination_test_PR(const PSET& pset) {
459 const dimension_type space_dim = pset.space_dimension();
460 if (space_dim % 2 != 0) {
461 std::ostringstream s;
462 s << "PPL::termination_test_PR(pset):\n"
463 << "pset.space_dimension() == " << space_dim
464 << " is odd.";
465 throw std::invalid_argument(s.str());
466 }
467
468 using namespace Implementation::Termination;
469 Constraint_System cs;
470 assign_all_inequalities_approximation(pset, cs);
471 return termination_test_PR_original(cs);
472 }
473
474 template <typename PSET>
475 bool
one_affine_ranking_function_PR_2(const PSET & pset_before,const PSET & pset_after,Generator & mu)476 one_affine_ranking_function_PR_2(const PSET& pset_before,
477 const PSET& pset_after,
478 Generator& mu) {
479 const dimension_type before_space_dim = pset_before.space_dimension();
480 const dimension_type after_space_dim = pset_after.space_dimension();
481 if (after_space_dim != 2*before_space_dim) {
482 std::ostringstream s;
483 s << "PPL::one_affine_ranking_function_PR_2"
484 << "(pset_before, pset_after, mu):\n"
485 << "pset_before.space_dimension() == " << before_space_dim
486 << ", pset_after.space_dimension() == " << after_space_dim
487 << ";\nthe latter should be twice the former.";
488 throw std::invalid_argument(s.str());
489 }
490
491 using namespace Implementation::Termination;
492 Constraint_System cs_before;
493 Constraint_System cs_after;
494 assign_all_inequalities_approximation(pset_before, cs_before);
495 assign_all_inequalities_approximation(pset_after, cs_after);
496 return one_affine_ranking_function_PR(cs_before, cs_after, mu);
497 }
498
499 template <typename PSET>
500 bool
one_affine_ranking_function_PR(const PSET & pset,Generator & mu)501 one_affine_ranking_function_PR(const PSET& pset, Generator& mu) {
502 const dimension_type space_dim = pset.space_dimension();
503 if (space_dim % 2 != 0) {
504 std::ostringstream s;
505 s << "PPL::one_affine_ranking_function_PR(pset, mu):\n"
506 << "pset.space_dimension() == " << space_dim
507 << " is odd.";
508 throw std::invalid_argument(s.str());
509 }
510
511 using namespace Implementation::Termination;
512 Constraint_System cs;
513 assign_all_inequalities_approximation(pset, cs);
514 return one_affine_ranking_function_PR_original(cs, mu);
515 }
516
517 template <typename PSET>
518 void
all_affine_ranking_functions_PR_2(const PSET & pset_before,const PSET & pset_after,NNC_Polyhedron & mu_space)519 all_affine_ranking_functions_PR_2(const PSET& pset_before,
520 const PSET& pset_after,
521 NNC_Polyhedron& mu_space) {
522 const dimension_type before_space_dim = pset_before.space_dimension();
523 const dimension_type after_space_dim = pset_after.space_dimension();
524 if (after_space_dim != 2*before_space_dim) {
525 std::ostringstream s;
526 s << "PPL::all_affine_ranking_functions_MS_2"
527 << "(pset_before, pset_after, mu_space):\n"
528 << "pset_before.space_dimension() == " << before_space_dim
529 << ", pset_after.space_dimension() == " << after_space_dim
530 << ";\nthe latter should be twice the former.";
531 throw std::invalid_argument(s.str());
532 }
533
534 if (pset_before.is_empty()) {
535 mu_space = NNC_Polyhedron(1 + before_space_dim);
536 return;
537 }
538
539 using namespace Implementation::Termination;
540 Constraint_System cs_before;
541 Constraint_System cs_after;
542 assign_all_inequalities_approximation(pset_before, cs_before);
543 assign_all_inequalities_approximation(pset_after, cs_after);
544 all_affine_ranking_functions_PR(cs_before, cs_after, mu_space);
545 }
546
547 template <typename PSET>
548 void
all_affine_ranking_functions_PR(const PSET & pset,NNC_Polyhedron & mu_space)549 all_affine_ranking_functions_PR(const PSET& pset,
550 NNC_Polyhedron& mu_space) {
551 const dimension_type space_dim = pset.space_dimension();
552 if (space_dim % 2 != 0) {
553 std::ostringstream s;
554 s << "PPL::all_affine_ranking_functions_PR(pset, mu_space):\n"
555 << "pset.space_dimension() == " << space_dim
556 << " is odd.";
557 throw std::invalid_argument(s.str());
558 }
559
560 if (pset.is_empty()) {
561 mu_space = NNC_Polyhedron(1 + space_dim/2);
562 return;
563 }
564
565 using namespace Implementation::Termination;
566 Constraint_System cs;
567 assign_all_inequalities_approximation(pset, cs);
568 all_affine_ranking_functions_PR_original(cs, mu_space);
569 }
570
571 } // namespace Parma_Polyhedra_Library
572
573 #endif // !defined(PPL_termination_templates_hh)
574