1 /* Grid class implementation
2    (non-inline private or protected functions).
3    Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
4    Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
5 
6 This file is part of the Parma Polyhedra Library (PPL).
7 
8 The PPL is free software; you can redistribute it and/or modify it
9 under the terms of the GNU General Public License as published by the
10 Free Software Foundation; either version 3 of the License, or (at your
11 option) any later version.
12 
13 The PPL is distributed in the hope that it will be useful, but WITHOUT
14 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
15 FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
16 for more details.
17 
18 You should have received a copy of the GNU General Public License
19 along with this program; if not, write to the Free Software Foundation,
20 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
21 
22 For the most up-to-date information see the Parma Polyhedra Library
23 site: http://bugseng.com/products/ppl/ . */
24 
25 #include "ppl-config.h"
26 #include "Grid_defs.hh"
27 #include "Grid_Generator_defs.hh"
28 #include "Scalar_Products_defs.hh"
29 #include "Scalar_Products_inlines.hh"
30 #include "assertions.hh"
31 #include <string>
32 #include <iostream>
33 #include <sstream>
34 #include <stdexcept>
35 
36 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
37 /*! \ingroup PPL_defines
38   \brief
39   Controls the laziness level of the implementation.
40 
41   Temporarily used in a few of the function implementations to
42   switch to an even more lazy algorithm. To be removed as soon as
43   we collect enough information to decide which is the better
44   implementation alternative.
45 */
46 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
47 #define BE_LAZY 1
48 
49 namespace PPL = Parma_Polyhedra_Library;
50 
51 void
construct(dimension_type num_dimensions,const Degenerate_Element kind)52 PPL::Grid::construct(dimension_type num_dimensions,
53                      const Degenerate_Element kind) {
54   space_dim = num_dimensions;
55 
56   if (kind == EMPTY) {
57     // Set emptiness directly instead of with set_empty, as gen_sys is
58     // already correctly initialized.
59     status.set_empty();
60 
61     // Extend the zero dim false congruence system to the appropriate
62     // dimension and then store it in `con_sys'.
63     Congruence_System cgs(Congruence::zero_dim_false());
64     cgs.set_space_dimension(space_dim);
65     swap(con_sys, cgs);
66 
67     PPL_ASSERT(OK());
68     return;
69   }
70 
71   if (space_dim == 0) {
72     set_zero_dim_univ();
73     return;
74   }
75 
76   // Initialize both systems to universe representations.
77   set_congruences_minimized();
78   set_generators_minimized();
79   dim_kinds.resize(space_dim + 1);
80 
81   // Building a universe congruence system.
82   // Extend the zero dim integrality congruence system to the
83   // appropriate dimension and then store it in `con_sys'.
84   Congruence_System cgs(Congruence::zero_dim_integrality());
85   cgs.set_space_dimension(num_dimensions);
86   // Recover minimal form after cgs(zdi) normalization.
87   cgs.rows[0].expr.set_inhomogeneous_term(Coefficient_one());
88   PPL_ASSERT(cgs.OK());
89   swap(con_sys, cgs);
90 
91   // Building a universe grid generator system (and dim_kinds).
92   gen_sys.set_space_dimension(space_dim);
93   gen_sys.insert(grid_point());
94   dim_kinds[0] = PROPER_CONGRUENCE /* a.k.a. PARAMETER */;
95   for (dimension_type dim = 0; dim < space_dim; ++dim) {
96     gen_sys.insert(grid_line(Variable(dim)));
97     dim_kinds[1+dim] = CON_VIRTUAL /* a.k.a. LINE */;
98   }
99   PPL_ASSERT(OK());
100 }
101 
102 void
construct(Congruence_System & cgs)103 PPL::Grid::construct(Congruence_System& cgs) {
104   // Protecting against space dimension overflow is up to the caller.
105   PPL_ASSERT(cgs.space_dimension() <= max_space_dimension());
106   // Preparing con_sys and gen_sys is up to the caller.
107   PPL_ASSERT(cgs.space_dimension() == con_sys.space_dimension());
108   PPL_ASSERT(cgs.space_dimension() == gen_sys.space_dimension());
109   PPL_ASSERT(con_sys.has_no_rows());
110   PPL_ASSERT(gen_sys.has_no_rows());
111 
112   // Set the space dimension.
113   space_dim = cgs.space_dimension();
114 
115   if (space_dim > 0) {
116     // Stealing the rows from `cgs'.
117     con_sys.m_swap(cgs);
118     con_sys.normalize_moduli();
119     set_congruences_up_to_date();
120   }
121   else {
122     // Here `space_dim == 0'.
123     // See if an inconsistent congruence has been passed.
124     for (dimension_type i = cgs.num_rows(); i-- > 0; ) {
125       if (cgs[i].is_inconsistent()) {
126         // Inconsistent congruence found: the grid is empty.
127         status.set_empty();
128         // Insert the zero dim false congruence system into `con_sys'.
129         // `gen_sys' is already in empty form.
130         con_sys.insert(Congruence::zero_dim_false());
131         PPL_ASSERT(OK());
132         return;
133       }
134     }
135     set_zero_dim_univ();
136   }
137   PPL_ASSERT(OK());
138 }
139 
140 void
construct(Grid_Generator_System & ggs)141 PPL::Grid::construct(Grid_Generator_System& ggs) {
142   // Protecting against space dimension overflow is up to the caller.
143   PPL_ASSERT(ggs.space_dimension() <= max_space_dimension());
144   // Preparing con_sys and gen_sys is up to the caller.
145   PPL_ASSERT(ggs.space_dimension() == con_sys.space_dimension());
146   PPL_ASSERT(ggs.space_dimension() == gen_sys.space_dimension());
147   PPL_ASSERT(con_sys.has_no_rows());
148   PPL_ASSERT(gen_sys.has_no_rows());
149 
150   // Set the space dimension.
151   space_dim = ggs.space_dimension();
152 
153   // An empty set of generators defines the empty grid.
154   if (ggs.has_no_rows()) {
155     status.set_empty();
156     // Insert the zero dim false congruence system into `con_sys'.
157     // `gen_sys' is already in empty form.
158     con_sys.insert(Congruence::zero_dim_false());
159     return;
160   }
161 
162   // Non-empty valid generator systems have a supporting point, at least.
163   if (!ggs.has_points()) {
164     throw_invalid_generators("Grid(ggs)", "ggs");
165   }
166 
167   if (space_dim == 0) {
168     set_zero_dim_univ();
169   }
170   else {
171     // Steal the rows from `ggs'.
172     gen_sys.m_swap(ggs);
173     normalize_divisors(gen_sys);
174     // Generators are now up-to-date.
175     set_generators_up_to_date();
176   }
177 
178   PPL_ASSERT(OK());
179 }
180 
181 PPL::Grid::Three_Valued_Boolean
quick_equivalence_test(const Grid & y) const182 PPL::Grid::quick_equivalence_test(const Grid& y) const {
183   // Private method: the caller must ensure the following.
184   PPL_ASSERT(space_dim == y.space_dim);
185   PPL_ASSERT(!marked_empty() && !y.marked_empty() && space_dim > 0);
186 
187   const Grid& x = *this;
188 
189   bool css_normalized = false;
190 
191   if (x.congruences_are_minimized() && y.congruences_are_minimized()) {
192     // Equivalent minimized congruence systems have:
193     //  - the same number of congruences; ...
194     if (x.con_sys.num_rows() != y.con_sys.num_rows()) {
195       return Grid::TVB_FALSE;
196     }
197     //  - the same number of equalities; ...
198     const dimension_type x_num_equalities = x.con_sys.num_equalities();
199     if (x_num_equalities != y.con_sys.num_equalities()) {
200       return Grid::TVB_FALSE;
201     }
202     //  - and if there are no equalities, the same congruences.
203     //    Delay this test: try cheaper tests on generators first.
204     css_normalized = (x_num_equalities == 0);
205   }
206 
207   if (x.generators_are_minimized() && y.generators_are_minimized()) {
208     // Equivalent minimized generator systems have:
209     //  - the same number of generators; ...
210     if (x.gen_sys.num_rows() != y.gen_sys.num_rows()) {
211       return Grid::TVB_FALSE;
212     }
213     //  - the same number of lines; ...
214     const dimension_type x_num_lines = x.gen_sys.num_lines();
215     if (x_num_lines != y.gen_sys.num_lines()) {
216       return Grid::TVB_FALSE;
217     }
218       //  - and if there are no lines, the same generators.
219     if (x_num_lines == 0) {
220       // Check for syntactic identity.
221 
222       if (x.gen_sys == y.gen_sys) {
223         return Grid::TVB_TRUE;
224       }
225       else {
226         return Grid::TVB_FALSE;
227       }
228     }
229   }
230 
231   // TODO: Consider minimizing the systems and re-performing these
232   //       checks.
233 
234   if (css_normalized) {
235     if (x.con_sys == y.con_sys) {
236       return Grid::TVB_TRUE;
237     }
238     else {
239       return Grid::TVB_FALSE;
240     }
241   }
242 
243   return Grid::TVB_DONT_KNOW;
244 }
245 
246 bool
is_included_in(const Grid & y) const247 PPL::Grid::is_included_in(const Grid& y) const {
248   // Private method: the caller must ensure the following.
249   PPL_ASSERT(space_dim == y.space_dim);
250   PPL_ASSERT(!marked_empty() && !y.marked_empty() && space_dim > 0);
251 
252   const Grid& x = *this;
253 
254 #if BE_LAZY
255   if (!x.generators_are_up_to_date() && !x.update_generators()) {
256     // Updating found `x' empty.
257     return true;
258   }
259   if (!y.congruences_are_up_to_date()) {
260     y.update_congruences();
261   }
262 #else
263   if (!x.generators_are_minimized() && !x.minimize()) {
264     // Minimizing found `x' empty.
265     return true;
266   }
267   if (!y.congruences_are_minimized())
268     y.minimize();
269 #endif
270 
271   PPL_ASSERT(x.OK());
272   PPL_ASSERT(y.OK());
273 
274   const Grid_Generator_System& gs = x.gen_sys;
275   const Congruence_System& cgs = y.con_sys;
276 
277   const dimension_type num_rows = gs.num_rows();
278   for (dimension_type i = num_rows; i-- > 0; ) {
279     if (!cgs.satisfies_all_congruences(gs[i])) {
280       return false;
281     }
282   }
283 
284   // Inclusion holds.
285   return true;
286 }
287 
288 bool
bounds(const Linear_Expression & expr,const char * method_call) const289 PPL::Grid::bounds(const Linear_Expression& expr,
290                   const char* method_call) const {
291   // The dimension of `expr' must be at most the dimension of *this.
292   if (space_dim < expr.space_dimension()) {
293     throw_dimension_incompatible(method_call, "e", expr);
294   }
295   // A zero-dimensional or empty grid bounds everything.
296   if (space_dim == 0
297       || marked_empty()
298       || (!generators_are_up_to_date() && !update_generators())) {
299     return true;
300   }
301   if (!generators_are_minimized() && !minimize()) {
302     // Minimizing found `this' empty.
303     return true;
304   }
305 
306   return bounds_no_check(expr);
307 }
308 
309 bool
bounds_no_check(const Linear_Expression & expr) const310 PPL::Grid::bounds_no_check(const Linear_Expression& expr) const {
311   // The dimension of `expr' must be at most the dimension of *this.
312   PPL_ASSERT(space_dim > 0 && space_dim >= expr.space_dimension());
313   PPL_ASSERT(generators_are_minimized() && !marked_empty());
314 
315   // The generators are up to date and minimized.
316   for (dimension_type i = gen_sys.num_rows(); i-- > 0; ) {
317     const Grid_Generator& g = gen_sys[i];
318     // Only lines and parameters in `*this' can cause `expr' to be
319     // unbounded.
320     if (g.is_line_or_parameter()) {
321       const int sp_sign = Scalar_Products::homogeneous_sign(expr, g);
322       if (sp_sign != 0) {
323         // `*this' does not bound `expr'.
324         return false;
325       }
326     }
327   }
328   return true;
329 }
330 
331 bool
frequency_no_check(const Linear_Expression & expr,Coefficient & freq_n,Coefficient & freq_d,Coefficient & val_n,Coefficient & val_d) const332 PPL::Grid::frequency_no_check(const Linear_Expression& expr,
333                      Coefficient& freq_n, Coefficient& freq_d,
334                      Coefficient& val_n, Coefficient& val_d) const {
335 
336   // The dimension of `expr' must be at most the dimension of *this.
337   PPL_ASSERT(space_dim >= expr.space_dimension());
338   PPL_ASSERT(generators_are_minimized() && !marked_empty());
339 
340   // The generators are up to date and minimized and the grid is non-empty.
341 
342   // If the grid is bounded for the expression `expr',
343   // then `expr' has a constant value and the frequency is 0.
344   if (bounds_no_check(expr)) {
345     freq_n = 0;
346     freq_d = 1;
347     // Find the value of the constant expression.
348     const Grid_Generator& point = gen_sys[0];
349     val_d = point.divisor();
350     Scalar_Products::homogeneous_assign(val_n, expr, point);
351     val_n += expr.inhomogeneous_term() * val_d;
352     // Reduce `val_n' and `val_d'.
353     PPL_DIRTY_TEMP_COEFFICIENT(gcd);
354     gcd_assign(gcd, val_n, val_d);
355     exact_div_assign(val_n, val_n, gcd);
356     exact_div_assign(val_d, val_d, gcd);
357     return true;
358   }
359 
360   // The frequency is the gcd of the scalar products of the parameters
361   // in `gen_sys'.
362   const dimension_type num_rows = gen_sys.num_rows();
363   PPL_DIRTY_TEMP_COEFFICIENT(sp);
364   freq_n = 0;
365 
366   // As the generators are minimized, `gen_sys[0]' is a point
367   // and considered later.
368   for (dimension_type row = 1; row < num_rows; ++row) {
369     const Grid_Generator& gen = gen_sys[row];
370     Scalar_Products::homogeneous_assign(sp, expr, gen);
371     if (gen.is_line()) {
372       if (sgn(sp) != 0) {
373           return false;
374       }
375       continue;
376     }
377     // `gen' must be a parameter.
378     PPL_ASSERT(gen.is_parameter());
379     if (sgn(sp) != 0) {
380       gcd_assign(freq_n, freq_n, sp);
381     }
382   }
383   const Grid_Generator& point = gen_sys[0];
384   PPL_ASSERT(point.is_point());
385 
386   // The denominator of the frequency and of the value is
387   // the divisor for the generators.
388   freq_d = point.divisor();
389   val_d = freq_d;
390 
391   // As point is a grid generator, homogeneous_assign() must be used.
392   Scalar_Products::homogeneous_assign(val_n, expr, point);
393   val_n += expr.inhomogeneous_term() * val_d;
394 
395   // Reduce `val_n' by the frequency `freq_n'.
396   val_n %= freq_n;
397 
398   PPL_DIRTY_TEMP_COEFFICIENT(gcd);
399   // Reduce `freq_n' and `freq_d'.
400   gcd_assign(gcd, freq_n, freq_d);
401   exact_div_assign(freq_n, freq_n, gcd);
402   exact_div_assign(freq_d, freq_d, gcd);
403 
404   // Reduce `val_n' and `val_d'.
405   gcd_assign(gcd, val_n, val_d);
406   exact_div_assign(val_n, val_n, gcd);
407   exact_div_assign(val_d, val_d, gcd);
408 
409   return true;
410 }
411 
412 bool
max_min(const Linear_Expression & expr,const char * method_call,Coefficient & ext_n,Coefficient & ext_d,bool & included,Generator * point) const413 PPL::Grid::max_min(const Linear_Expression& expr,
414                    const char* method_call,
415                    Coefficient& ext_n, Coefficient& ext_d, bool& included,
416                    Generator* point) const {
417   if (bounds(expr, method_call)) {
418     if (marked_empty()) {
419       return false;
420     }
421     if (space_dim == 0) {
422       ext_n = 0;
423       ext_d = 1;
424       included = true;
425       if (point != 0) {
426         *point = Generator::point();
427       }
428       return true;
429     }
430     // Grid::bounds above ensures the generators are up to date.
431     if (!generators_are_minimized()) {
432       // Minimize the generator system.
433       Grid& gr = const_cast<Grid&>(*this);
434       gr.simplify(gr.gen_sys, gr.dim_kinds);
435       gr.set_generators_minimized();
436     }
437 
438     const Grid_Generator& gen = gen_sys[0];
439     Scalar_Products::homogeneous_assign(ext_n, expr, gen);
440     ext_n += expr.inhomogeneous_term();
441     ext_d = gen.divisor();
442     // Reduce ext_n and ext_d.
443     PPL_DIRTY_TEMP_COEFFICIENT(gcd);
444     gcd_assign(gcd, ext_n, ext_d);
445     exact_div_assign(ext_n, ext_n, gcd);
446     exact_div_assign(ext_d, ext_d, gcd);
447 
448     included = true;
449     if (point != 0) {
450       const Linear_Expression g_expr(gen.expression());
451       *point = Generator::point(g_expr, gen.divisor());
452     }
453     return true;
454   }
455   return false;
456 }
457 
458 void
set_zero_dim_univ()459 PPL::Grid::set_zero_dim_univ() {
460   status.set_zero_dim_univ();
461   space_dim = 0;
462   con_sys.clear();
463   gen_sys.clear();
464   gen_sys.insert(grid_point());
465 }
466 
467 void
set_empty()468 PPL::Grid::set_empty() {
469   status.set_empty();
470 
471   // Replace gen_sys with an empty system of the right dimension.
472   Grid_Generator_System gs(space_dim);
473   gen_sys.m_swap(gs);
474 
475   // Extend the zero dim false congruence system to the appropriate
476   // dimension and then swap it with `con_sys'.
477   Congruence_System cgs(Congruence::zero_dim_false());
478   cgs.set_space_dimension(space_dim);
479   swap(con_sys, cgs);
480 }
481 
482 void
update_congruences() const483 PPL::Grid::update_congruences() const {
484   // The caller must ensure that the generators are up to date.
485   PPL_ASSERT(space_dim > 0);
486   PPL_ASSERT(!marked_empty());
487   PPL_ASSERT(!gen_sys.has_no_rows());
488   PPL_ASSERT(gen_sys.space_dimension() > 0);
489 
490   Grid& gr = const_cast<Grid&>(*this);
491 
492   if (!generators_are_minimized()) {
493     gr.simplify(gr.gen_sys, gr.dim_kinds);
494   }
495 
496   // `gen_sys' contained rows before being reduced, so it should
497   // contain at least a single point afterward.
498   PPL_ASSERT(!gen_sys.has_no_rows());
499 
500   // Populate `con_sys' with congruences characterizing the grid
501   // described by `gen_sys'.
502   gr.conversion(gr.gen_sys, gr.con_sys, gr.dim_kinds);
503 
504   // Both systems are minimized.
505   gr.set_congruences_minimized();
506   gr.set_generators_minimized();
507 }
508 
509 bool
update_generators() const510 PPL::Grid::update_generators() const {
511   PPL_ASSERT(space_dim > 0);
512   PPL_ASSERT(!marked_empty());
513   PPL_ASSERT(congruences_are_up_to_date());
514 
515   Grid& x = const_cast<Grid&>(*this);
516 
517   if (!congruences_are_minimized()) {
518     // Either the system of congruences is consistent, or the grid is
519     // empty.
520     if (simplify(x.con_sys, x.dim_kinds)) {
521       x.set_empty();
522       return false;
523     }
524   }
525   // Populate gen_sys with generators characterizing the grid
526   // described by con_sys.
527   conversion(x.con_sys, x.gen_sys, x.dim_kinds);
528 
529   // Both systems are minimized.
530   x.set_congruences_minimized();
531   x.set_generators_minimized();
532   return true;
533 }
534 
535 bool
minimize() const536 PPL::Grid::minimize() const {
537   // 0-dimension and empty grids are already minimized.
538   if (marked_empty()) {
539     return false;
540   }
541   if (space_dim == 0) {
542     return true;
543   }
544   // Are both systems already minimized?
545   if (congruences_are_minimized() && generators_are_minimized()) {
546     return true;
547   }
548   // Invoke update_generators, update_congruences or simplify,
549   // depending on the state of the systems.
550   if (congruences_are_up_to_date()) {
551     if (generators_are_up_to_date()) {
552       Grid& gr = const_cast<Grid&>(*this);
553       // Only one of the systems can be minimized here.
554       if (congruences_are_minimized()) {
555         // Minimize the generator system.
556         gr.simplify(gr.gen_sys, gr.dim_kinds);
557         gr.set_generators_minimized();
558       }
559       else {
560 #ifndef NDEBUG
561         // Both systems are up to date, and the empty case is handled
562         // above, so the grid should contain points.
563         bool empty = simplify(gr.con_sys, gr.dim_kinds);
564         PPL_ASSERT(!empty);
565 #else
566         simplify(gr.con_sys, gr.dim_kinds);
567 #endif
568         gr.set_congruences_minimized();
569         if (!generators_are_minimized()) {
570           // Minimize the generator system.
571           gr.simplify(gr.gen_sys, gr.dim_kinds);
572           gr.set_generators_minimized();
573         }
574       }
575     }
576     else {
577       // Updating the generators may reveal that `*this' is empty.
578       const bool ret = update_generators();
579       PPL_ASSERT(OK());
580       return ret;
581     }
582   }
583   else {
584     PPL_ASSERT(generators_are_up_to_date());
585     update_congruences();
586   }
587   PPL_ASSERT(OK());
588   return true;
589 }
590 
591 void
normalize_divisors(Grid_Generator_System & sys,Grid_Generator_System & gen_sys)592 PPL::Grid::normalize_divisors(Grid_Generator_System& sys,
593                               Grid_Generator_System& gen_sys) {
594 #ifndef NDEBUG
595   const dimension_type num_rows = gen_sys.num_rows();
596 #endif
597   PPL_ASSERT(num_rows > 0);
598 
599   // Find the first point in gen_sys.
600   dimension_type row = 0;
601   while (gen_sys[row].is_line_or_parameter()) {
602     ++row;
603     // gen_sys should have at least one point.
604     PPL_ASSERT(row < num_rows);
605   }
606   const Grid_Generator& first_point = gen_sys[row];
607   const Coefficient& gen_sys_divisor = first_point.divisor();
608 
609 #ifndef NDEBUG
610   // Check that the divisors in gen_sys are equal.
611   for (dimension_type i = row + 1; i < num_rows; ++i) {
612     const Grid_Generator& g = gen_sys[i];
613     if (g.is_parameter_or_point()) {
614       PPL_ASSERT(gen_sys_divisor == g.divisor());
615     }
616   }
617 #endif // !defined(NDEBUG)
618 
619   PPL_DIRTY_TEMP_COEFFICIENT(divisor);
620   divisor = gen_sys_divisor;
621   // Adjust sys to include the gen_sys divisor.
622   normalize_divisors(sys, divisor);
623   if (divisor != gen_sys_divisor) {
624     // Adjust gen_sys to use the new divisor.
625     //
626     // The points and parameters in gen_sys share a common divisor
627     // value, so the new divisor will be the LCM of this common
628     // divisor and `divisor', hence the third argument.
629     normalize_divisors(gen_sys, divisor, &first_point);
630   }
631 }
632 
633 void
normalize_divisors(Grid_Generator_System & sys,Coefficient & divisor,const Grid_Generator * first_point)634 PPL::Grid::normalize_divisors(Grid_Generator_System& sys,
635                               Coefficient& divisor,
636                               const Grid_Generator* first_point) {
637   PPL_ASSERT(divisor >= 0);
638   if (sys.space_dimension() > 0 && divisor > 0) {
639     const dimension_type num_rows = sys.num_rows();
640 
641     if (first_point != 0) {
642       lcm_assign(divisor, divisor, (*first_point).divisor());
643     }
644     else {
645       PPL_ASSERT(num_rows > 0);
646       // Move to the first point or parameter.
647       dimension_type row = 0;
648       while (sys[row].is_line()) {
649         if (++row == num_rows) {
650           // All rows are lines.
651           return;
652         }
653       }
654 
655       // Calculate the LCM of the given divisor and the divisor of
656       // every point or parameter.
657       while (row < num_rows) {
658         const Grid_Generator& g = sys[row];
659         if (g.is_parameter_or_point()) {
660           lcm_assign(divisor, divisor, g.divisor());
661         }
662         ++row;
663       }
664     }
665 
666     // Represent every point and every parameter using the newly
667     // calculated divisor.
668     for (dimension_type i = num_rows; i-- > 0; ) {
669       sys.sys.rows[i].scale_to_divisor(divisor);
670     }
671 
672     // Put the rows back into the linear system.
673     PPL_ASSERT(sys.sys.OK());
674   }
675 }
676 
677 void
add_congruence_no_check(const Congruence & cg)678 PPL::Grid::add_congruence_no_check(const Congruence& cg) {
679   PPL_ASSERT(!marked_empty());
680   PPL_ASSERT(space_dim >= cg.space_dimension());
681 
682   // Dealing with a zero-dimensional space grid first.
683   if (space_dim == 0) {
684     if (cg.is_inconsistent()) {
685       set_empty();
686     }
687     return;
688   }
689 
690   if (!congruences_are_up_to_date()) {
691     update_congruences();
692   }
693 
694   con_sys.insert(cg);
695 
696   clear_congruences_minimized();
697   set_congruences_up_to_date();
698   clear_generators_up_to_date();
699 
700   // Note: the congruence system may have become unsatisfiable, thus
701   // we do not check for satisfiability.
702   PPL_ASSERT(OK());
703 }
704 
705 void
add_constraint_no_check(const Constraint & c)706 PPL::Grid::add_constraint_no_check(const Constraint& c) {
707   PPL_ASSERT(!marked_empty());
708   PPL_ASSERT(space_dim >= c.space_dimension());
709 
710   if (c.is_inequality()) {
711     // Only trivial inequalities can be handled.
712     if (c.is_inconsistent()) {
713       set_empty();
714       return;
715     }
716     if (c.is_tautological()) {
717       return;
718     }
719     // Non-trivial inequality constraints are not allowed.
720     throw_invalid_constraint("add_constraint(c)", "c");
721   }
722 
723   PPL_ASSERT(c.is_equality());
724   const Congruence cg(c);
725   add_congruence_no_check(cg);
726 }
727 
728 void
refine_no_check(const Constraint & c)729 PPL::Grid::refine_no_check(const Constraint& c) {
730   PPL_ASSERT(!marked_empty());
731   PPL_ASSERT(space_dim >= c.space_dimension());
732 
733   if (c.is_equality()) {
734     const Congruence cg(c);
735     add_congruence_no_check(cg);
736   }
737   else if (c.is_inconsistent()) {
738     set_empty();
739   }
740 }
741 
742 void
throw_invalid_argument(const char * method,const char * reason)743 PPL::Grid::throw_invalid_argument(const char* method, const char* reason) {
744   std::ostringstream s;
745   s << "PPL::Grid::" << method << ":" << std::endl
746     << reason << ".";
747   throw std::invalid_argument(s.str());
748 }
749 
750 void
throw_dimension_incompatible(const char * method,const char * other_name,dimension_type other_dim) const751 PPL::Grid::throw_dimension_incompatible(const char* method,
752                                         const char* other_name,
753                                         dimension_type other_dim) const {
754   std::ostringstream s;
755   s << "PPL::Grid::" << method << ":\n"
756     << "this->space_dimension() == " << space_dimension() << ", "
757     << other_name << ".space_dimension() == " << other_dim << ".";
758   throw std::invalid_argument(s.str());
759 }
760 
761 void
throw_dimension_incompatible(const char * method,const char * gr_name,const Grid & gr) const762 PPL::Grid::throw_dimension_incompatible(const char* method,
763                                         const char* gr_name,
764                                         const Grid& gr) const {
765   throw_dimension_incompatible(method, gr_name, gr.space_dimension());
766 }
767 
768 void
throw_dimension_incompatible(const char * method,const char * le_name,const Linear_Expression & le) const769 PPL::Grid::throw_dimension_incompatible(const char* method,
770                                         const char* le_name,
771                                         const Linear_Expression& le) const {
772   throw_dimension_incompatible(method, le_name, le.space_dimension());
773 }
774 
775 void
throw_dimension_incompatible(const char * method,const char * cg_name,const Congruence & cg) const776 PPL::Grid::throw_dimension_incompatible(const char* method,
777                                         const char* cg_name,
778                                         const Congruence& cg) const {
779   throw_dimension_incompatible(method, cg_name, cg.space_dimension());
780 }
781 
782 void
throw_dimension_incompatible(const char * method,const char * c_name,const Constraint & c) const783 PPL::Grid::throw_dimension_incompatible(const char* method,
784                                         const char* c_name,
785                                         const Constraint& c) const {
786   throw_dimension_incompatible(method, c_name, c.space_dimension());
787 }
788 
789 void
throw_dimension_incompatible(const char * method,const char * g_name,const Grid_Generator & g) const790 PPL::Grid::throw_dimension_incompatible(const char* method,
791                                         const char* g_name,
792                                         const Grid_Generator& g) const {
793   throw_dimension_incompatible(method, g_name, g.space_dimension());
794 }
795 
796 void
throw_dimension_incompatible(const char * method,const char * g_name,const Generator & g) const797 PPL::Grid::throw_dimension_incompatible(const char* method,
798                                         const char* g_name,
799                                         const Generator& g) const {
800   throw_dimension_incompatible(method, g_name, g.space_dimension());
801 }
802 
803 void
throw_dimension_incompatible(const char * method,const char * cgs_name,const Congruence_System & cgs) const804 PPL::Grid::throw_dimension_incompatible(const char* method,
805                                         const char* cgs_name,
806                                         const Congruence_System& cgs) const {
807   throw_dimension_incompatible(method, cgs_name, cgs.space_dimension());
808 }
809 
810 void
throw_dimension_incompatible(const char * method,const char * cs_name,const Constraint_System & cs) const811 PPL::Grid::throw_dimension_incompatible(const char* method,
812                                         const char* cs_name,
813                                         const Constraint_System& cs) const {
814   throw_dimension_incompatible(method, cs_name, cs.space_dimension());
815 }
816 
817 void
throw_dimension_incompatible(const char * method,const char * gs_name,const Grid_Generator_System & gs) const818 PPL::Grid::throw_dimension_incompatible(const char* method,
819                                         const char* gs_name,
820                                         const Grid_Generator_System& gs) const {
821   throw_dimension_incompatible(method, gs_name, gs.space_dimension());
822 }
823 
824 void
throw_dimension_incompatible(const char * method,const char * var_name,const Variable var) const825 PPL::Grid::throw_dimension_incompatible(const char* method,
826                                         const char* var_name,
827                                         const Variable var) const {
828   std::ostringstream s;
829   s << "PPL::Grid::" << method << ":" << std::endl
830     << "this->space_dimension() == " << space_dimension() << ", "
831     << var_name << ".space_dimension() == " << var.space_dimension() << ".";
832   throw std::invalid_argument(s.str());
833 }
834 
835 void
836 PPL::Grid::
throw_dimension_incompatible(const char * method,dimension_type required_space_dim) const837 throw_dimension_incompatible(const char* method,
838                              dimension_type required_space_dim) const {
839   std::ostringstream s;
840   s << "PPL::Grid::" << method << ":" << std::endl
841     << "this->space_dimension() == " << space_dimension()
842     << ", required space dimension == " << required_space_dim << ".";
843   throw std::invalid_argument(s.str());
844 }
845 
846 void
throw_invalid_constraint(const char * method,const char * c_name)847 PPL::Grid::throw_invalid_constraint(const char* method,
848                                     const char* c_name) {
849   std::ostringstream s;
850   s << "PPL::Grid::" << method << ":" << std::endl
851     << c_name << " is not an equality constraint.";
852   throw std::invalid_argument(s.str());
853 }
854 
855 void
throw_invalid_constraints(const char * method,const char * cs_name)856 PPL::Grid::throw_invalid_constraints(const char* method,
857                                     const char* cs_name) {
858   std::ostringstream s;
859   s << "PPL::Grid::" << method << ":" << std::endl
860     << "the constraint system " << cs_name
861     << " contains inequalities.";
862   throw std::invalid_argument(s.str());
863 }
864 
865 void
throw_invalid_generator(const char * method,const char * g_name)866 PPL::Grid::throw_invalid_generator(const char* method,
867                                    const char* g_name) {
868   std::ostringstream s;
869   s << "PPL::Grid::" << method << ":" << std::endl
870     << "*this is an empty grid and "
871     << g_name << " is not a point.";
872   throw std::invalid_argument(s.str());
873 }
874 
875 void
throw_invalid_generators(const char * method,const char * gs_name)876 PPL::Grid::throw_invalid_generators(const char* method,
877                                     const char* gs_name) {
878   std::ostringstream s;
879   s << "PPL::Grid::" << method << ":" << std::endl
880     << "*this is an empty grid and" << std::endl
881     << "the non-empty generator system " << gs_name << " contains no points.";
882   throw std::invalid_argument(s.str());
883 }
884