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