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