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