1 /* Generator_System class implementation (non-inline 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 #include "ppl-config.h"
25 #include "Generator_System_defs.hh"
26 #include "Generator_System_inlines.hh"
27 #include "Constraint_defs.hh"
28 #include "Scalar_Products_defs.hh"
29 #include "Scalar_Products_inlines.hh"
30 #include "assertions.hh"
31 #include <string>
32 #include <vector>
33 #include <iostream>
34 #include <stdexcept>
35 
36 namespace PPL = Parma_Polyhedra_Library;
37 
38 bool
39 PPL::Generator_System::
adjust_topology_and_space_dimension(const Topology new_topology,const dimension_type new_space_dim)40 adjust_topology_and_space_dimension(const Topology new_topology,
41                                     const dimension_type new_space_dim) {
42   PPL_ASSERT(space_dimension() <= new_space_dim);
43 
44   if (sys.topology() != new_topology) {
45     if (new_topology == NECESSARILY_CLOSED) {
46       // A NOT_NECESSARILY_CLOSED generator system
47       // can be converted to a NECESSARILY_CLOSED one
48       // only if it does not contain closure points.
49       // This check has to be performed under the user viewpoint.
50       if (has_closure_points()) {
51         return false;
52       }
53       // For a correct implementation, we have to remove those
54       // closure points that were matching a point (i.e., those
55       // that are in the generator system, but are invisible to
56       // the user).
57       const Generator_System& gs = *this;
58       for (dimension_type i = 0; i < sys.num_rows(); ) {
59         if (gs[i].is_closure_point()) {
60           sys.remove_row(i, false);
61         }
62         else {
63           ++i;
64         }
65       }
66       sys.set_necessarily_closed();
67     }
68     else {
69       convert_into_non_necessarily_closed();
70     }
71   }
72 
73   sys.set_space_dimension(new_space_dim);
74 
75   // We successfully adjusted dimensions and topology.
76   PPL_ASSERT(OK());
77   return true;
78 }
79 
80 // TODO: would be worth to avoid adding closure points
81 // that already are in the system of generators?
82 // To do this efficiently we could sort the system and
83 // perform insertions keeping its sortedness.
84 void
add_corresponding_closure_points()85 PPL::Generator_System::add_corresponding_closure_points() {
86   PPL_ASSERT(!sys.is_necessarily_closed());
87   // NOTE: we always add (pending) rows at the end of the generator system.
88   // Updating `index_first_pending', if needed, is done by the caller.
89   Generator_System& gs = *this;
90   const dimension_type n_rows = gs.sys.num_rows();
91   for (dimension_type i = n_rows; i-- > 0; ) {
92     const Generator& g = gs[i];
93     if (g.epsilon_coefficient() > 0) {
94       // `g' is a point: adding the closure point.
95       Generator cp = g;
96       cp.set_epsilon_coefficient(0);
97       // Enforcing normalization.
98       cp.expr.normalize();
99       gs.insert_pending(cp, Recycle_Input());
100     }
101   }
102   PPL_ASSERT(OK());
103 }
104 
105 
106 // TODO: would be worth to avoid adding points
107 // that already are in the system of generators?
108 // To do this efficiently we could sort the system and
109 // perform insertions keeping its sortedness.
110 void
add_corresponding_points()111 PPL::Generator_System::add_corresponding_points() {
112   PPL_ASSERT(!sys.is_necessarily_closed());
113   // NOTE: we always add (pending) rows at the end of the generator system.
114   // Updating `index_first_pending', if needed, is done by the caller.
115   Generator_System& gs = *this;
116   const dimension_type n_rows = gs.sys.num_rows();
117   for (dimension_type i = 0; i < n_rows; ++i) {
118     const Generator& g = gs[i];
119     if (!g.is_line_or_ray() && g.epsilon_coefficient() == 0) {
120       // `g' is a closure point: adding the point.
121       // Note: normalization is preserved.
122       Generator p = g;
123       p.set_epsilon_coefficient(p.expr.inhomogeneous_term());
124       gs.insert_pending(p, Recycle_Input());
125     }
126   }
127   PPL_ASSERT(OK());
128 }
129 
130 bool
has_closure_points() const131 PPL::Generator_System::has_closure_points() const {
132   if (sys.is_necessarily_closed()) {
133     return false;
134   }
135   // Adopt the point of view of the user.
136   for (Generator_System::const_iterator i = begin(),
137          this_end = end(); i != this_end; ++i) {
138     if (i->is_closure_point()) {
139       return true;
140     }
141   }
142   return false;
143 }
144 
145 void
convert_into_non_necessarily_closed()146 PPL::Generator_System::convert_into_non_necessarily_closed() {
147   // Padding the matrix with the column
148   // corresponding to the epsilon coefficients:
149   // all points must have epsilon coordinate equal to 1
150   // (i.e., the epsilon coefficient is equal to the divisor);
151   // rays and lines must have epsilon coefficient equal to 0.
152   // Note: normalization is preserved.
153   sys.set_not_necessarily_closed();
154 
155   for (dimension_type i = sys.rows.size(); i-- > 0; ) {
156     Generator& gen = sys.rows[i];
157     if (!gen.is_line_or_ray()) {
158       gen.set_epsilon_coefficient(gen.expr.inhomogeneous_term());
159     }
160   }
161 
162   PPL_ASSERT(sys.OK());
163 }
164 
165 bool
has_points() const166 PPL::Generator_System::has_points() const {
167   const Generator_System& gs = *this;
168   // Avoiding the repeated tests on topology.
169   if (sys.is_necessarily_closed()) {
170     for (dimension_type i = sys.num_rows(); i-- > 0; ) {
171       if (!gs[i].is_line_or_ray()) {
172         return true;
173       }
174     }
175   }
176   else {
177     // !is_necessarily_closed()
178     for (dimension_type i = sys.num_rows(); i-- > 0; ) {
179       if (gs[i].epsilon_coefficient() != 0) {
180         return true;
181       }
182     }
183   }
184   return false;
185 }
186 
187 void
skip_forward()188 PPL::Generator_System_const_iterator::skip_forward() {
189   const Linear_System<Generator>::const_iterator gsp_end = gsp->end();
190   if (i != gsp_end) {
191     Linear_System<Generator>::const_iterator i_next = i;
192     ++i_next;
193     if (i_next != gsp_end) {
194       const Generator& cp = *i;
195       const Generator& p = *i_next;
196       if (cp.is_closure_point()
197           && p.is_point()
198           && cp.is_matching_closure_point(p)) {
199         i = i_next;
200       }
201     }
202   }
203 }
204 
205 void
insert(const Generator & g)206 PPL::Generator_System::insert(const Generator& g) {
207   Generator tmp = g;
208   insert(tmp, Recycle_Input());
209 }
210 
211 void
insert_pending(const Generator & g)212 PPL::Generator_System::insert_pending(const Generator& g) {
213   Generator tmp = g;
214   insert_pending(tmp, Recycle_Input());
215 }
216 
217 void
insert(Generator & g,Recycle_Input)218 PPL::Generator_System::insert(Generator& g, Recycle_Input) {
219   // We are sure that the matrix has no pending rows
220   // and that the new row is not a pending generator.
221   PPL_ASSERT(sys.num_pending_rows() == 0);
222   if (sys.topology() == g.topology()) {
223     sys.insert(g, Recycle_Input());
224   }
225   else {
226     // `*this' and `g' have different topologies.
227     if (sys.is_necessarily_closed()) {
228       convert_into_non_necessarily_closed();
229       // Inserting the new generator.
230       sys.insert(g, Recycle_Input());
231     }
232     else {
233       // The generator system is NOT necessarily closed:
234       // copy the generator, adding the missing dimensions
235       // and the epsilon coefficient.
236       const dimension_type new_space_dim = std::max(g.space_dimension(),
237                                                     space_dimension());
238       g.set_not_necessarily_closed();
239       g.set_space_dimension(new_space_dim);
240       // If it was a point, set the epsilon coordinate to 1
241       // (i.e., set the coefficient equal to the divisor).
242       // Note: normalization is preserved.
243       if (!g.is_line_or_ray()) {
244         g.set_epsilon_coefficient(g.expr.inhomogeneous_term());
245       }
246       // Inserting the new generator.
247       sys.insert(g, Recycle_Input());
248     }
249   }
250   PPL_ASSERT(OK());
251 }
252 
253 void
insert_pending(Generator & g,Recycle_Input)254 PPL::Generator_System::insert_pending(Generator& g, Recycle_Input) {
255   if (sys.topology() == g.topology()) {
256     sys.insert_pending(g, Recycle_Input());
257   }
258   else {
259     // `*this' and `g' have different topologies.
260     if (sys.is_necessarily_closed()) {
261       convert_into_non_necessarily_closed();
262 
263       // Inserting the new generator.
264       sys.insert_pending(g, Recycle_Input());
265     }
266     else {
267       // The generator system is NOT necessarily closed:
268       // copy the generator, adding the missing dimensions
269       // and the epsilon coefficient.
270       const dimension_type new_space_dim = std::max(g.space_dimension(),
271                                                     space_dimension());
272       g.set_topology(NOT_NECESSARILY_CLOSED);
273       g.set_space_dimension(new_space_dim);
274       // If it was a point, set the epsilon coordinate to 1
275       // (i.e., set the coefficient equal to the divisor).
276       // Note: normalization is preserved.
277       if (!g.is_line_or_ray()) {
278         g.set_epsilon_coefficient(g.expr.inhomogeneous_term());
279       }
280       // Inserting the new generator.
281       sys.insert_pending(g, Recycle_Input());
282     }
283   }
284   PPL_ASSERT(OK());
285 }
286 
287 PPL::dimension_type
num_lines() const288 PPL::Generator_System::num_lines() const {
289   // We are sure that this method is applied only to a matrix
290   // that does not contain pending rows.
291   PPL_ASSERT(sys.num_pending_rows() == 0);
292   const Generator_System& gs = *this;
293   dimension_type n = 0;
294   // If sys happens to be sorted, take advantage of the fact
295   // that lines are at the top of the system.
296   if (sys.is_sorted()) {
297     const dimension_type nrows = sys.num_rows();
298     for (dimension_type i = 0; i < nrows && gs[i].is_line(); ++i) {
299       ++n;
300     }
301   }
302   else {
303     for (dimension_type i = sys.num_rows(); i-- > 0 ; ) {
304       if (gs[i].is_line()) {
305         ++n;
306       }
307     }
308   }
309   return n;
310 }
311 
312 PPL::dimension_type
num_rays() const313 PPL::Generator_System::num_rays() const {
314   // We are sure that this method is applied only to a matrix
315   // that does not contain pending rows.
316   PPL_ASSERT(sys.num_pending_rows() == 0);
317   const Generator_System& gs = *this;
318   dimension_type n = 0;
319   // If sys happens to be sorted, take advantage of the fact
320   // that rays and points are at the bottom of the system and
321   // rays have the inhomogeneous term equal to zero.
322   if (sys.is_sorted()) {
323     for (dimension_type i = sys.num_rows();
324          i != 0 && gs[--i].is_ray_or_point(); ) {
325       if (gs[i].is_line_or_ray()) {
326         ++n;
327       }
328     }
329   }
330   else {
331     for (dimension_type i = sys.num_rows(); i-- > 0 ; ) {
332       if (gs[i].is_ray()) {
333         ++n;
334       }
335     }
336   }
337   return n;
338 }
339 
340 PPL::Poly_Con_Relation
relation_with(const Constraint & c) const341 PPL::Generator_System::relation_with(const Constraint& c) const {
342   // Note: this method is not public and it is the responsibility
343   // of the caller to actually test for dimension compatibility.
344   // We simply assert it.
345   PPL_ASSERT(space_dimension() >= c.space_dimension());
346   // Number of generators: the case of an empty polyhedron
347   // has already been filtered out by the caller.
348   const dimension_type n_rows = sys.num_rows();
349   PPL_ASSERT(n_rows > 0);
350   const Generator_System& gs = *this;
351 
352   // `result' will keep the relation holding between the generators
353   // we have seen so far and the constraint `c'.
354   Poly_Con_Relation result = Poly_Con_Relation::saturates();
355 
356   switch (c.type()) {
357 
358   case Constraint::EQUALITY:
359     {
360       // The hyperplane defined by the equality `c' is included
361       // in the set of points satisfying `c' (it is the same set!).
362       result = result && Poly_Con_Relation::is_included();
363       // The following integer variable will hold the scalar product sign
364       // of either the first point or the first non-saturating ray we find.
365       // If it is equal to 2, then it means that we haven't found such
366       // a generator yet.
367       int first_point_or_nonsaturating_ray_sign = 2;
368 
369       for (dimension_type i = n_rows; i-- > 0; ) {
370         const Generator& g = gs[i];
371         const int sp_sign = Scalar_Products::sign(c, g);
372         // Checking whether the generator saturates the equality.
373         // If that is the case, then we have to do something only if
374         // the generator is a point.
375         if (sp_sign == 0) {
376           if (g.is_point()) {
377             if (first_point_or_nonsaturating_ray_sign == 2) {
378               // It is the first time that we find a point and
379               // we have not found a non-saturating ray yet.
380               first_point_or_nonsaturating_ray_sign = 0;
381             }
382             else {
383               // We already found a point or a non-saturating ray.
384               if (first_point_or_nonsaturating_ray_sign != 0) {
385                 return Poly_Con_Relation::strictly_intersects();
386               }
387             }
388           }
389         }
390         else {
391           // Here we know that sp_sign != 0.
392           switch (g.type()) {
393 
394           case Generator::LINE:
395             // If a line does not saturate `c', then there is a strict
396             // intersection between the points satisfying `c'
397             // and the points generated by `gs'.
398             return Poly_Con_Relation::strictly_intersects();
399 
400           case Generator::RAY:
401             if (first_point_or_nonsaturating_ray_sign == 2) {
402               // It is the first time that we have a non-saturating ray
403               // and we have not found any point yet.
404               first_point_or_nonsaturating_ray_sign = sp_sign;
405               result = Poly_Con_Relation::is_disjoint();
406             }
407             else
408               // We already found a point or a non-saturating ray.
409               if (sp_sign != first_point_or_nonsaturating_ray_sign) {
410                 return Poly_Con_Relation::strictly_intersects();
411               }
412             break;
413 
414           case Generator::POINT:
415           case Generator::CLOSURE_POINT:
416             // NOTE: a non-saturating closure point is treated as
417             // a normal point.
418             if (first_point_or_nonsaturating_ray_sign == 2) {
419               // It is the first time that we find a point and
420               // we have not found a non-saturating ray yet.
421               first_point_or_nonsaturating_ray_sign = sp_sign;
422               result = Poly_Con_Relation::is_disjoint();
423             }
424             else
425               // We already found a point or a non-saturating ray.
426               if (sp_sign != first_point_or_nonsaturating_ray_sign) {
427                 return Poly_Con_Relation::strictly_intersects();
428               }
429             break;
430           }
431         }
432       }
433     }
434     break;
435 
436   case Constraint::NONSTRICT_INEQUALITY:
437     {
438       // The hyperplane implicitly defined by the non-strict inequality `c'
439       // is included in the set of points satisfying `c'.
440       result = result && Poly_Con_Relation::is_included();
441       // The following Boolean variable will be set to `false'
442       // as soon as either we find (any) point or we find a
443       // non-saturating ray.
444       bool first_point_or_nonsaturating_ray = true;
445 
446       for (dimension_type i = n_rows; i-- > 0; ) {
447         const Generator& g = gs[i];
448         const int sp_sign = Scalar_Products::sign(c, g);
449         // Checking whether the generator saturates the non-strict
450         // inequality. If that is the case, then we have to do something
451         // only if the generator is a point.
452         if (sp_sign == 0) {
453           if (g.is_point()) {
454             if (first_point_or_nonsaturating_ray) {
455               // It is the first time that we have a point and
456               // we have not found a non-saturating ray yet.
457               first_point_or_nonsaturating_ray = false;
458             }
459             else {
460               // We already found a point or a non-saturating ray before.
461               if (result == Poly_Con_Relation::is_disjoint()) {
462                 // Since g saturates c, we have a strict intersection if
463                 // none of the generators seen so far are included in `c'.
464                 return Poly_Con_Relation::strictly_intersects();
465               }
466             }
467           }
468         }
469         else {
470           // Here we know that sp_sign != 0.
471           switch (g.type()) {
472 
473           case Generator::LINE:
474             // If a line does not saturate `c', then there is a strict
475             // intersection between the points satisfying `c' and
476             // the points generated by `gs'.
477             return Poly_Con_Relation::strictly_intersects();
478 
479           case Generator::RAY:
480             if (first_point_or_nonsaturating_ray) {
481               // It is the first time that we have a non-saturating ray
482               // and we have not found any point yet.
483               first_point_or_nonsaturating_ray = false;
484               result = (sp_sign > 0)
485                 ? Poly_Con_Relation::is_included()
486                 : Poly_Con_Relation::is_disjoint();
487             }
488             else {
489               // We already found a point or a non-saturating ray.
490               if ((sp_sign > 0
491                    && result == Poly_Con_Relation::is_disjoint())
492                   || (sp_sign < 0
493                       && result.implies(Poly_Con_Relation::is_included()))) {
494                 // We have a strict intersection if either:
495                 // - `g' satisfies `c' but none of the generators seen
496                 //    so far are included in `c'; or
497                 // - `g' does not satisfy `c' and all the generators
498                 //    seen so far are included in `c'.
499                 return Poly_Con_Relation::strictly_intersects();
500               }
501               if (sp_sign > 0) {
502                 // Here all the generators seen so far either saturate
503                 // or are included in `c'.
504                 // Since `g' does not saturate `c' ...
505                 result = Poly_Con_Relation::is_included();
506               }
507             }
508             break;
509 
510           case Generator::POINT:
511           case Generator::CLOSURE_POINT:
512             // NOTE: a non-saturating closure point is treated as
513             // a normal point.
514             if (first_point_or_nonsaturating_ray) {
515               // It is the first time that we have a point and
516               // we have not found a non-saturating ray yet.
517               // - If point `g' saturates `c', then all the generators
518               //   seen so far saturate `c'.
519               // - If point `g' is included (but does not saturate) `c',
520               //   then all the generators seen so far are included in `c'.
521               // - If point `g' does not satisfy `c', then all the
522               //   generators seen so far are disjoint from `c'.
523               first_point_or_nonsaturating_ray = false;
524               if (sp_sign > 0) {
525                 result = Poly_Con_Relation::is_included();
526               }
527               else if (sp_sign < 0) {
528                 result = Poly_Con_Relation::is_disjoint();
529               }
530             }
531             else {
532               // We already found a point or a non-saturating ray before.
533               if ((sp_sign > 0
534                    && result == Poly_Con_Relation::is_disjoint())
535                   || (sp_sign < 0
536                       && result.implies(Poly_Con_Relation::is_included()))) {
537                 // We have a strict intersection if either:
538                 // - `g' satisfies or saturates `c' but none of the
539                 //    generators seen so far are included in `c'; or
540                 // - `g' does not satisfy `c' and all the generators
541                 //    seen so far are included in `c'.
542                 return Poly_Con_Relation::strictly_intersects();
543               }
544               if (sp_sign > 0) {
545                 // Here all the generators seen so far either saturate
546                 // or are included in `c'.
547                 // Since `g' does not saturate `c' ...
548                 result = Poly_Con_Relation::is_included();
549               }
550             }
551             break;
552           }
553         }
554       }
555     }
556     break;
557 
558   case Constraint::STRICT_INEQUALITY:
559     {
560       // The hyperplane implicitly defined by the strict inequality `c'
561       // is disjoint from the set of points satisfying `c'.
562       result = result && Poly_Con_Relation::is_disjoint();
563       // The following Boolean variable will be set to `false'
564       // as soon as either we find (any) point or we find a
565       // non-saturating ray.
566       bool first_point_or_nonsaturating_ray = true;
567       for (dimension_type i = n_rows; i-- > 0; ) {
568         const Generator& g = gs[i];
569         // Using the reduced scalar product operator to avoid
570         // both topology and space dimension mismatches.
571         const int sp_sign = Scalar_Products::reduced_sign(c, g);
572         // Checking whether the generator saturates the strict inequality.
573         // If that is the case, then we have to do something
574         // only if the generator is a point.
575         if (sp_sign == 0) {
576           if (g.is_point()) {
577             if (first_point_or_nonsaturating_ray) {
578               // It is the first time that we have a point and
579               // we have not found a non-saturating ray yet.
580               first_point_or_nonsaturating_ray = false;
581             }
582             else {
583               // We already found a point or a non-saturating ray before.
584               if (result == Poly_Con_Relation::is_included()) {
585                 return Poly_Con_Relation::strictly_intersects();
586               }
587             }
588           }
589         }
590         else {
591           // Here we know that sp_sign != 0.
592           switch (g.type()) {
593 
594           case Generator::LINE:
595             // If a line does not saturate `c', then there is a strict
596             // intersection between the points satisfying `c' and the points
597             // generated by `gs'.
598             return Poly_Con_Relation::strictly_intersects();
599 
600           case Generator::RAY:
601             if (first_point_or_nonsaturating_ray) {
602               // It is the first time that we have a non-saturating ray
603               // and we have not found any point yet.
604               first_point_or_nonsaturating_ray = false;
605               result = (sp_sign > 0)
606                 ? Poly_Con_Relation::is_included()
607                 : Poly_Con_Relation::is_disjoint();
608             }
609             else {
610               // We already found a point or a non-saturating ray before.
611               if ((sp_sign > 0
612                    && result.implies(Poly_Con_Relation::is_disjoint()))
613                   ||
614                   (sp_sign <= 0
615                    && result == Poly_Con_Relation::is_included())) {
616                 return Poly_Con_Relation::strictly_intersects();
617               }
618               if (sp_sign < 0) {
619                 // Here all the generators seen so far either saturate
620                 // or are disjoint from `c'.
621                 // Since `g' does not saturate `c' ...
622                 result = Poly_Con_Relation::is_disjoint();
623               }
624             }
625             break;
626 
627           case Generator::POINT:
628           case Generator::CLOSURE_POINT:
629             if (first_point_or_nonsaturating_ray) {
630               // It is the first time that we have a point and
631               // we have not found a non-saturating ray yet.
632               // - If point `g' saturates `c', then all the generators
633               //   seen so far saturate `c'.
634               // - If point `g' is included in (but does not saturate) `c',
635               //   then all the generators seen so far are included in `c'.
636               // - If point `g' strictly violates `c', then all the
637               //   generators seen so far are disjoint from `c'.
638               first_point_or_nonsaturating_ray = false;
639               if (sp_sign > 0) {
640                 result = Poly_Con_Relation::is_included();
641               }
642               else if (sp_sign < 0) {
643                 result = Poly_Con_Relation::is_disjoint();
644               }
645             }
646             else {
647               // We already found a point or a non-saturating ray before.
648               if ((sp_sign > 0
649                    && result.implies(Poly_Con_Relation::is_disjoint()))
650                   ||
651                   (sp_sign <= 0
652                    && result == Poly_Con_Relation::is_included())) {
653                 return Poly_Con_Relation::strictly_intersects();
654               }
655               if (sp_sign < 0) {
656                 // Here all the generators seen so far either saturate
657                 // or are disjoint from `c'.
658                 // Since `g' does not saturate `c' ...
659                 result = Poly_Con_Relation::is_disjoint();
660               }
661             }
662             break;
663           }
664         }
665       }
666     }
667     break;
668   }
669   // We have seen all generators.
670   return result;
671 }
672 
673 
674 bool
satisfied_by_all_generators(const Constraint & c) const675 PPL::Generator_System::satisfied_by_all_generators(const Constraint& c) const {
676   PPL_ASSERT(c.space_dimension() <= space_dimension());
677 
678   // Setting `sps' to the appropriate scalar product sign operator.
679   // This also avoids problems when having _legal_ topology mismatches
680   // (which could also cause a mismatch in the number of space dimensions).
681   const Topology_Adjusted_Scalar_Product_Sign sps(c);
682 
683   const Generator_System& gs = *this;
684   switch (c.type()) {
685   case Constraint::EQUALITY:
686     // Equalities must be saturated by all generators.
687     for (dimension_type i = gs.sys.num_rows(); i-- > 0; ) {
688       if (sps(c, gs[i]) != 0) {
689         return false;
690       }
691     }
692     break;
693   case Constraint::NONSTRICT_INEQUALITY:
694     // Non-strict inequalities must be saturated by lines and
695     // satisfied by all the other generators.
696     for (dimension_type i = gs.sys.num_rows(); i-- > 0; ) {
697       const Generator& g = gs[i];
698       const int sp_sign = sps(c, g);
699       if (g.is_line()) {
700         if (sp_sign != 0) {
701           return false;
702         }
703       }
704       else
705         // `g' is a ray, point or closure point.
706         if (sp_sign < 0) {
707           return false;
708         }
709     }
710     break;
711   case Constraint::STRICT_INEQUALITY:
712     // Strict inequalities must be saturated by lines,
713     // satisfied by all generators, and must not be saturated by points.
714     for (dimension_type i = gs.sys.num_rows(); i-- > 0; ) {
715       const Generator& g = gs[i];
716       const int sp_sign = sps(c, g);
717       switch (g.type()) {
718       case Generator::POINT:
719         if (sp_sign <= 0) {
720           return false;
721         }
722         break;
723       case Generator::LINE:
724         if (sp_sign != 0) {
725           return false;
726         }
727         break;
728       default:
729         // `g' is a ray or closure point.
730         if (sp_sign < 0) {
731           return false;
732         }
733         break;
734       }
735     }
736     break;
737   }
738   // If we reach this point, `c' is satisfied by all generators.
739   return true;
740 }
741 
742 
743 void
744 PPL::Generator_System
affine_image(Variable v,const Linear_Expression & expr,Coefficient_traits::const_reference denominator)745 ::affine_image(Variable v,
746                const Linear_Expression& expr,
747                Coefficient_traits::const_reference denominator) {
748   Generator_System& x = *this;
749   PPL_ASSERT(v.space_dimension() <= x.space_dimension());
750   PPL_ASSERT(expr.space_dimension() <= x.space_dimension());
751   PPL_ASSERT(denominator > 0);
752 
753   const dimension_type n_rows = x.sys.num_rows();
754 
755   // Compute the numerator of the affine transformation and assign it
756   // to the column of `*this' indexed by `v'.
757   PPL_DIRTY_TEMP_COEFFICIENT(numerator);
758   for (dimension_type i = n_rows; i-- > 0; ) {
759     Generator& row = sys.rows[i];
760     Scalar_Products::assign(numerator, expr, row.expr);
761     if (denominator != 1) {
762       // Since we want integer elements in the matrix,
763       // we multiply by `denominator' all the columns of `*this'
764       // having an index different from `v'.
765       // Note that this operation also modifies the coefficient of v, but
766       // it will be overwritten by the set_coefficient() below.
767       row.expr *= denominator;
768     }
769     row.expr.set_coefficient(v, numerator);
770   }
771 
772   set_sorted(false);
773 
774   // If the mapping is not invertible we may have transformed
775   // valid lines and rays into the origin of the space.
776   const bool not_invertible = (v.space_dimension() > expr.space_dimension()
777                                || expr.coefficient(v) == 0);
778   if (not_invertible) {
779     x.remove_invalid_lines_and_rays();
780   }
781 
782   // TODO: Consider normalizing individual rows in the loop above.
783   // Strong normalization also resets the sortedness flag.
784   x.sys.strong_normalize();
785 
786 #ifndef NDEBUG
787   // Make sure that the (remaining) generators are still OK after fiddling
788   // with their internal data.
789   for (dimension_type i = x.num_rows(); i-- > 0; ) {
790     PPL_ASSERT(x.sys[i].OK());
791   }
792 #endif
793 
794   PPL_ASSERT(sys.OK());
795 }
796 
797 void
ascii_dump(std::ostream & s) const798 PPL::Generator_System::ascii_dump(std::ostream& s) const {
799   sys.ascii_dump(s);
800 }
801 
PPL_OUTPUT_DEFINITIONS(Generator_System)802 PPL_OUTPUT_DEFINITIONS(Generator_System)
803 
804 bool
805 PPL::Generator_System::ascii_load(std::istream& s) {
806   if (!sys.ascii_load(s)) {
807     return false;
808   }
809 
810   PPL_ASSERT(OK());
811   return true;
812 }
813 
814 void
remove_invalid_lines_and_rays()815 PPL::Generator_System::remove_invalid_lines_and_rays() {
816   // The origin of the vector space cannot be a valid line/ray.
817   // NOTE: the following swaps will mix generators without even trying
818   // to preserve sortedness: as a matter of fact, it will almost always
819   // be the case that the input generator system is NOT sorted.
820 
821   // Note that num_rows() is *not* constant, because it is decreased by
822   // remove_row().
823   for (dimension_type i = 0; i < num_rows(); ) {
824     const Generator& g = (*this)[i];
825     if (g.is_line_or_ray() && g.expr.all_homogeneous_terms_are_zero()) {
826       sys.remove_row(i, false);
827       set_sorted(false);
828     }
829     else {
830       ++i;
831     }
832   }
833 }
834 
835 const PPL::Generator_System* PPL::Generator_System::zero_dim_univ_p = 0;
836 
837 void
initialize()838 PPL::Generator_System::initialize() {
839   PPL_ASSERT(zero_dim_univ_p == 0);
840   zero_dim_univ_p
841     = new Generator_System(Generator::zero_dim_point());
842 }
843 
844 void
finalize()845 PPL::Generator_System::finalize() {
846   PPL_ASSERT(zero_dim_univ_p != 0);
847   delete zero_dim_univ_p;
848   zero_dim_univ_p = 0;
849 }
850 
851 bool
OK() const852 PPL::Generator_System::OK() const {
853   return sys.OK();
854 }
855 
856 /*! \relates Parma_Polyhedra_Library::Generator_System */
857 std::ostream&
operator <<(std::ostream & s,const Generator_System & gs)858 PPL::IO_Operators::operator<<(std::ostream& s, const Generator_System& gs) {
859   Generator_System::const_iterator i = gs.begin();
860   const Generator_System::const_iterator gs_end = gs.end();
861   if (i == gs_end) {
862     return s << "false";
863   }
864   while (true) {
865     s << *i;
866     ++i;
867     if (i == gs_end) {
868       return s;
869     }
870     s << ", ";
871   }
872 }
873