PPL  1.2
Generator_System.cc
Go to the documentation of this file.
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"
27 #include "Constraint_defs.hh"
28 #include "Scalar_Products_defs.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
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 {
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
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;
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
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;
124  gs.insert_pending(p, Recycle_Input());
125  }
126  }
127  PPL_ASSERT(OK());
128 }
129 
130 bool
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
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()) {
159  }
160  }
161 
162  PPL_ASSERT(sys.OK());
163 }
164 
165 bool
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
189  const Linear_System<Generator>::const_iterator gsp_end = gsp->end();
190  if (i != gsp_end) {
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
207  Generator tmp = g;
208  insert(tmp, Recycle_Input());
209 }
210 
211 void
213  Generator tmp = g;
214  insert_pending(tmp, Recycle_Input());
215 }
216 
217 void
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());
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()) {
245  }
246  // Inserting the new generator.
247  sys.insert(g, Recycle_Input());
248  }
249  }
250  PPL_ASSERT(OK());
251 }
252 
253 void
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());
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()) {
279  }
280  // Inserting the new generator.
281  sys.insert_pending(g, Recycle_Input());
282  }
283  }
284  PPL_ASSERT(OK());
285 }
286 
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 
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 
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'.
355 
356  switch (c.type()) {
357 
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) {
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'.
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;
406  }
407  else
408  // We already found a point or a non-saturating ray.
409  if (sp_sign != first_point_or_nonsaturating_ray_sign) {
411  }
412  break;
413 
414  case Generator::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;
423  }
424  else
425  // We already found a point or a non-saturating ray.
426  if (sp_sign != first_point_or_nonsaturating_ray_sign) {
428  }
429  break;
430  }
431  }
432  }
433  }
434  break;
435 
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'.
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'.
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()
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'.
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' ...
506  }
507  }
508  break;
509 
510  case Generator::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) {
526  }
527  else if (sp_sign < 0) {
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'.
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' ...
549  }
550  }
551  break;
552  }
553  }
554  }
555  }
556  break;
557 
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()) {
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'.
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)
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())) {
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' ...
623  }
624  }
625  break;
626 
627  case Generator::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) {
641  }
642  else if (sp_sign < 0) {
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())) {
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' ...
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
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).
682 
683  const Generator_System& gs = *this;
684  switch (c.type()) {
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;
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;
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
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) {
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
798 PPL::Generator_System::ascii_dump(std::ostream& s) const {
799  sys.ascii_dump(s);
800 }
801 
803 
804 bool
806  if (!sys.ascii_load(s)) {
807  return false;
808  }
809 
810  PPL_ASSERT(OK());
811  return true;
812 }
813 
814 void
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];
826  sys.remove_row(i, false);
827  set_sorted(false);
828  }
829  else {
830  ++i;
831  }
832  }
833 }
834 
836 
837 void
839  PPL_ASSERT(zero_dim_univ_p == 0);
840  zero_dim_univ_p
842 }
843 
844 void
846  PPL_ASSERT(zero_dim_univ_p != 0);
847  delete zero_dim_univ_p;
848  zero_dim_univ_p = 0;
849 }
850 
851 bool
853  return sys.OK();
854 }
855 
857 std::ostream&
858 PPL::IO_Operators::operator<<(std::ostream& s, const Generator_System& gs) {
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 }
Scalar product sign function object depending on topology.
static Poly_Con_Relation is_disjoint()
The polyhedron and the set of points satisfying the constraint are disjoint.
A linear equality or inequality.
bool adjust_topology_and_space_dimension(Topology new_topology, dimension_type new_space_dim)
Adjusts *this so that it matches the new_topology and new_space_dim (adding or removing columns if ne...
static bool implies(flags_t x, flags_t y)
True if and only if the conjunction x implies the conjunction y.
size_t dimension_type
An unsigned integral type for representing space dimensions.
Type type() const
Returns the constraint type of *this.
A line, ray, point or closure point.
Linear_Expression expr
The linear expression encoding *this.
bool is_line_or_ray() const
Returns true if and only if *this is a line or a ray.
Coefficient_traits::const_reference inhomogeneous_term() const
Returns the inhomogeneous term of *this.
#define PPL_DIRTY_TEMP_COEFFICIENT(id)
Declare a local variable named id, of type Coefficient, and containing an unknown initial value...
void skip_forward()
*this skips to the next generator, skipping those closure points that are immediately followed by a m...
static const Generator & zero_dim_point()
Returns the origin of the zero-dimensional space .
std::ostream & operator<<(std::ostream &s, const Ask_Tell< D > &x)
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
static Poly_Con_Relation is_included()
The polyhedron is included in the set of points satisfying the constraint.
The standard C++ namespace.
bool has_points() const
Returns true if and only if *this contains one or more points.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
void set_coefficient(Variable v, Coefficient_traits::const_reference n)
Sets the coefficient of v in *this to n.
static Poly_Con_Relation saturates()
The polyhedron is included in the set of points saturating the constraint.
bool is_matching_closure_point(const Generator &p) const
Returns true if and only if the closure point *this has the same coordinates of the point p...
Definition: Generator.cc:399
static void initialize()
Initializes the class.
void set_topology(Topology x)
Sets to x the topological kind of *this row.
Coefficient_traits::const_reference coefficient(Variable v) const
Returns the coefficient of v in *this.
A dimension of the vector space.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
bool satisfied_by_all_generators(const Constraint &c) const
Returns true if all the generators satisfy c.
void remove_invalid_lines_and_rays()
Removes all the invalid lines and rays.
void ascii_dump() const
Writes to std::cerr an ASCII representation of *this.
static int reduced_sign(const Linear_Expression &x, const Linear_Expression &y)
Returns the sign of the reduced scalar product of x and y, where the coefficient of x is ignored...
Type type() const
Returns the generator type of *this.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
void insert_pending(const Generator_System &r)
Adds a copy of the rows of `y' to the pending part of `*this'.
void set_not_necessarily_closed()
Sets to NOT_NECESSARILY_CLOSED the topological kind of *this row.
Enable_If< Is_Native_Or_Checked< T >::value, bool >::type ascii_load(std::istream &s, T &t)
Parma_Polyhedra_Library::Poly_Con_Relation relation_with(const Constraint &c) const
Returns the relations holding between the generator system and the constraint c.
bool all_homogeneous_terms_are_zero() const
Returns true if and only if all the homogeneous terms of *this are .
Swapping_Vector< Row >::const_iterator const_iterator
bool is_point() const
Returns true if and only if *this is a point.
dimension_type num_rays() const
Returns the number of rays of the system.
void set_space_dimension(dimension_type space_dim)
void add_corresponding_closure_points()
For each unmatched point in *this, adds the corresponding closure point.
static const Generator_System * zero_dim_univ_p
Holds (between class initialization and finalization) a pointer to the singleton system containing on...
#define PPL_OUTPUT_DEFINITIONS(class_name)
The entire library is confined to this namespace.
Definition: version.hh:61
static void finalize()
Finalizes the class.
void set_epsilon_coefficient(Coefficient_traits::const_reference n)
Sets the epsilon coefficient to n. The generator must be NNC.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
Topology topology() const
Returns the topological kind of *this.
const_iterator end() const
Returns the past-the-end const_iterator.
const_iterator begin() const
Returns the const_iterator pointing to the first generator, if *this is not empty; otherwise...
Coefficient_traits::const_reference epsilon_coefficient() const
Returns the epsilon coefficient. The generator must be NNC.
dimension_type num_lines() const
Returns the number of lines of the system.
static int sign(const Linear_Expression &x, const Linear_Expression &y)
Returns the sign of the scalar product between x and y.
bool OK() const
Checks if all the invariants are satisfied.
static void assign(Coefficient &z, const Linear_Expression &x, const Linear_Expression &y)
Computes the scalar product of x and y and assigns it to z.
Coefficient c
Definition: PIP_Tree.cc:64
void insert(const Generator &g)
Inserts in *this a copy of the generator g, increasing the number of space dimensions if needed...
void add_corresponding_points()
For each unmatched closure point in *this, adds the corresponding point.
bool has_closure_points() const
Returns true if and only if *this contains one or more closure points.
bool is_line() const
Returns true if and only if *this is a line.
static Poly_Con_Relation strictly_intersects()
The polyhedron intersects the set of points satisfying the constraint, but it is not included in it...
Topology
Kinds of polyhedra domains.
The relation between a polyhedron and a constraint.
void affine_image(Variable v, const Linear_Expression &expr, Coefficient_traits::const_reference denominator)
Assigns to a given variable an affine expression.
bool is_closure_point() const
Returns true if and only if *this is a closure point.