1 /* Congruence_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 "Congruence_System_defs.hh"
26 #include "Congruence_System_inlines.hh"
27 #include "Constraint_System_defs.hh"
28 #include "Constraint_System_inlines.hh"
29 #include "Congruence_defs.hh"
30 #include "Grid_Generator_defs.hh"
31 #include "Scalar_Products_defs.hh"
32 #include "Scalar_Products_inlines.hh"
33 #include "assertions.hh"
34 #include <string>
35 #include <vector>
36 #include <iostream>
37 #include <stdexcept>
38
39 namespace PPL = Parma_Polyhedra_Library;
40
Congruence_System(const Constraint_System & cs,Representation r)41 PPL::Congruence_System::Congruence_System(const Constraint_System& cs,
42 Representation r)
43 : rows(),
44 space_dimension_(cs.space_dimension()),
45 representation_(r) {
46 for (Constraint_System::const_iterator i = cs.begin(),
47 cs_end = cs.end(); i != cs_end; ++i) {
48 if (i->is_equality()) {
49 insert(*i);
50 }
51 }
52 }
53
54 void
55 PPL::Congruence_System
permute_space_dimensions(const std::vector<Variable> & cycle)56 ::permute_space_dimensions(const std::vector<Variable>& cycle) {
57 for (dimension_type k = rows.size(); k-- > 0; ) {
58 Congruence& rows_k = rows[k];
59 rows_k.permute_space_dimensions(cycle);
60 }
61 PPL_ASSERT(OK());
62 }
63
64 void
remove_rows(const dimension_type first,const dimension_type last,bool keep_sorted)65 PPL::Congruence_System::remove_rows(const dimension_type first,
66 const dimension_type last,
67 bool keep_sorted) {
68 PPL_ASSERT(first <= last);
69 PPL_ASSERT(last <= num_rows());
70 const dimension_type n = last - first;
71
72 // Swap the rows in [first, last) with the rows in [size() - n, size())
73 // (note that these intervals may not be disjunct).
74 if (keep_sorted) {
75 for (dimension_type i = last; i < rows.size(); ++i) {
76 swap(rows[i], rows[i - n]);
77 }
78 }
79 else {
80 const dimension_type offset = rows.size() - n - first;
81 for (dimension_type i = first; i < last; ++i) {
82 swap(rows[i], rows[i + offset]);
83 }
84 }
85
86 rows.resize(rows.size() - n);
87 PPL_ASSERT(OK());
88 }
89
90 bool
91 PPL::Congruence_System
set_space_dimension(const dimension_type new_space_dim)92 ::set_space_dimension(const dimension_type new_space_dim) {
93 if (space_dimension() != new_space_dim) {
94 space_dimension_ = new_space_dim;
95 for (dimension_type i = num_rows(); i-- > 0; ) {
96 rows[i].set_space_dimension(new_space_dim);
97 }
98 }
99 PPL_ASSERT(OK());
100 return true;
101 }
102
103 void
swap_space_dimensions(Variable v1,Variable v2)104 PPL::Congruence_System::swap_space_dimensions(Variable v1, Variable v2) {
105 for (dimension_type k = num_rows(); k-- > 0; ) {
106 rows[k].swap_space_dimensions(v1, v2);
107 }
108 }
109
110 void
insert_verbatim(Congruence & cg,Recycle_Input)111 PPL::Congruence_System::insert_verbatim(Congruence& cg, Recycle_Input) {
112 // TODO: Remove this.
113 PPL_ASSERT(cg.OK());
114
115 cg.set_representation(representation());
116
117 if (cg.space_dimension() >= space_dimension()) {
118 set_space_dimension(cg.space_dimension());
119 }
120 else {
121 cg.set_space_dimension(space_dimension());
122 }
123
124 rows.resize(num_rows() + 1);
125
126 swap(cg, rows.back());
127
128 PPL_ASSERT(OK());
129 }
130
131 void
insert(const Constraint & c)132 PPL::Congruence_System::insert(const Constraint& c) {
133 if (c.space_dimension() > space_dimension()) {
134 set_space_dimension(c.space_dimension());
135 }
136 Congruence cg(c, space_dimension(), representation());
137 cg.strong_normalize();
138 rows.resize(num_rows() + 1);
139
140 swap(cg, rows.back());
141
142 PPL_ASSERT(OK());
143 }
144
145 void
insert(Congruence_System & cgs,Recycle_Input)146 PPL::Congruence_System::insert(Congruence_System& cgs, Recycle_Input) {
147 const dimension_type old_num_rows = num_rows();
148 const dimension_type cgs_num_rows = cgs.num_rows();
149 if (space_dimension() < cgs.space_dimension()) {
150 set_space_dimension(cgs.space_dimension());
151 }
152 rows.resize(old_num_rows + cgs_num_rows);
153 for (dimension_type i = cgs_num_rows; i-- > 0; ) {
154 cgs.rows[i].set_space_dimension(space_dimension());
155 cgs.rows[i].set_representation(representation());
156 swap(cgs.rows[i], rows[old_num_rows + i]);
157 }
158 cgs.clear();
159
160 PPL_ASSERT(OK());
161 }
162
163 void
insert(const Congruence_System & y)164 PPL::Congruence_System::insert(const Congruence_System& y) {
165 Congruence_System& x = *this;
166
167 const dimension_type x_num_rows = x.num_rows();
168 const dimension_type y_num_rows = y.num_rows();
169
170 // Grow to the required size.
171 if (space_dimension() < y.space_dimension()) {
172 set_space_dimension(y.space_dimension());
173 }
174
175 rows.resize(rows.size() + y_num_rows);
176
177 // Copy the rows of `y', with the new space dimension.
178 for (dimension_type i = y_num_rows; i-- > 0; ) {
179 Congruence copy(y[i], space_dimension(), representation());
180 swap(copy, x.rows[x_num_rows+i]);
181 }
182 PPL_ASSERT(OK());
183 }
184
185 void
normalize_moduli()186 PPL::Congruence_System::normalize_moduli() {
187 const Congruence_System& cgs = *this;
188 dimension_type row = cgs.num_rows();
189 if (row > 0) {
190 // Calculate the LCM of all the moduli.
191 PPL_DIRTY_TEMP_COEFFICIENT(lcm);
192 // Find last proper congruence.
193 while (true) {
194 --row;
195 lcm = cgs[row].modulus();
196 if (lcm > 0) {
197 break;
198 }
199 if (row == 0) {
200 // All rows are equalities.
201 return;
202 }
203 }
204 while (row > 0) {
205 --row;
206 const Coefficient& modulus = cgs[row].modulus();
207 if (modulus > 0) {
208 lcm_assign(lcm, lcm, modulus);
209 }
210 }
211
212 // Represent every row using the LCM as the modulus.
213 PPL_DIRTY_TEMP_COEFFICIENT(factor);
214 for (row = num_rows(); row-- > 0; ) {
215 const Coefficient& modulus = cgs[row].modulus();
216 if (modulus <= 0 || modulus == lcm) {
217 continue;
218 }
219 exact_div_assign(factor, lcm, modulus);
220 rows[row].scale(factor);
221 }
222 }
223 PPL_ASSERT(OK());
224 }
225
226 bool
is_equal_to(const Congruence_System & cgs) const227 PPL::Congruence_System::is_equal_to(const Congruence_System& cgs) const {
228 return (*this) == cgs;
229 }
230
231 bool
has_linear_equalities() const232 PPL::Congruence_System::has_linear_equalities() const {
233 const Congruence_System& cgs = *this;
234 for (dimension_type i = cgs.num_rows(); i-- > 0; ) {
235 if (cgs[i].modulus() == 0) {
236 return true;
237 }
238 }
239 return false;
240 }
241
242 void
skip_forward()243 PPL::Congruence_System::const_iterator::skip_forward() {
244 const Swapping_Vector<Congruence>::const_iterator csp_end = csp->end();
245 while (i != csp_end && (*this)->is_tautological()) {
246 ++i;
247 }
248 }
249
250 PPL::dimension_type
num_equalities() const251 PPL::Congruence_System::num_equalities() const {
252 const Congruence_System& cgs = *this;
253 dimension_type n = 0;
254 for (dimension_type i = num_rows(); i-- > 0 ; ) {
255 if (cgs[i].is_equality()) {
256 ++n;
257 }
258 }
259 return n;
260 }
261
262 PPL::dimension_type
num_proper_congruences() const263 PPL::Congruence_System::num_proper_congruences() const {
264 const Congruence_System& cgs = *this;
265 dimension_type n = 0;
266 for (dimension_type i = num_rows(); i-- > 0 ; ) {
267 const Congruence& cg = cgs[i];
268 if (cg.is_proper_congruence()) {
269 ++n;
270 }
271 }
272 return n;
273 }
274
275 bool
276 PPL::Congruence_System::
satisfies_all_congruences(const Grid_Generator & g) const277 satisfies_all_congruences(const Grid_Generator& g) const {
278 PPL_ASSERT(g.space_dimension() <= space_dimension());
279
280 const Congruence_System& cgs = *this;
281 PPL_DIRTY_TEMP_COEFFICIENT(sp);
282 if (g.is_line()) {
283 for (dimension_type i = cgs.num_rows(); i-- > 0; ) {
284 const Congruence& cg = cgs[i];
285 Scalar_Products::assign(sp, g, cg);
286 if (sp != 0) {
287 return false;
288 }
289 }
290 }
291 else {
292 const Coefficient& divisor = g.divisor();
293 for (dimension_type i = cgs.num_rows(); i-- > 0; ) {
294 const Congruence& cg = cgs[i];
295 Scalar_Products::assign(sp, g, cg);
296 if (cg.is_equality()) {
297 if (sp != 0) {
298 return false;
299 }
300 }
301 else if (sp % (cg.modulus() * divisor) != 0) {
302 return false;
303 }
304 }
305 }
306 return true;
307 }
308
309 bool
has_a_free_dimension() const310 PPL::Congruence_System::has_a_free_dimension() const {
311 // Search for a dimension that is free of any congruence or equality
312 // constraint. Assumes a minimized system.
313 std::set<dimension_type> candidates;
314 for (dimension_type i = space_dimension(); i-- > 0; ) {
315 candidates.insert(i + 1);
316 }
317
318 for (dimension_type i = num_rows(); i-- > 0; ) {
319 rows[i].expression().has_a_free_dimension_helper(candidates);
320 if (candidates.empty()) {
321 return false;
322 }
323 }
324 return !candidates.empty();
325 }
326
327 void
328 PPL::Congruence_System::
affine_preimage(Variable v,const Linear_Expression & expr,Coefficient_traits::const_reference denominator)329 affine_preimage(Variable v,
330 const Linear_Expression& expr,
331 Coefficient_traits::const_reference denominator) {
332 PPL_ASSERT(v.space_dimension() <= space_dimension());
333 PPL_ASSERT(expr.space_dimension() <= space_dimension());
334 PPL_ASSERT(denominator > 0);
335
336 for (dimension_type i = num_rows(); i-- > 0; ) {
337 rows[i].affine_preimage(v, expr, denominator);
338 }
339 }
340
341 void
ascii_dump(std::ostream & s) const342 PPL::Congruence_System::ascii_dump(std::ostream& s) const {
343 const Congruence_System& x = *this;
344 const dimension_type x_num_rows = x.num_rows();
345 const dimension_type x_space_dim = x.space_dimension();
346 s << x_num_rows << " x " << x_space_dim << " ";
347 Parma_Polyhedra_Library::ascii_dump(s, representation());
348 s << std::endl;
349 for (dimension_type i = 0; i < x_num_rows; ++i) {
350 x[i].ascii_dump(s);
351 }
352 }
353
PPL_OUTPUT_DEFINITIONS(Congruence_System)354 PPL_OUTPUT_DEFINITIONS(Congruence_System)
355
356 bool
357 PPL::Congruence_System::ascii_load(std::istream& s) {
358 std::string str;
359 dimension_type num_rows;
360 dimension_type space_dim;
361 if (!(s >> num_rows)) {
362 return false;
363 }
364 if (!(s >> str) || str != "x") {
365 return false;
366 }
367 if (!(s >> space_dim)) {
368 return false;
369 }
370 clear();
371 space_dimension_ = space_dim;
372
373 if (!Parma_Polyhedra_Library::ascii_load(s, representation_)) {
374 return false;
375 }
376
377 Congruence c;
378 for (dimension_type i = 0; i < num_rows; ++i) {
379 if (!c.ascii_load(s)) {
380 return false;
381 }
382 insert_verbatim(c, Recycle_Input());
383 }
384
385 // Check invariants.
386 PPL_ASSERT(OK());
387 return true;
388 }
389
390 const PPL::Congruence_System* PPL::Congruence_System::zero_dim_empty_p = 0;
391
392 void
initialize()393 PPL::Congruence_System::initialize() {
394 PPL_ASSERT(zero_dim_empty_p == 0);
395 zero_dim_empty_p
396 = new Congruence_System(Congruence::zero_dim_false());
397 }
398
399 void
finalize()400 PPL::Congruence_System::finalize() {
401 PPL_ASSERT(zero_dim_empty_p != 0);
402 delete zero_dim_empty_p;
403 zero_dim_empty_p = 0;
404 }
405
406 bool
OK() const407 PPL::Congruence_System::OK() const {
408 // All rows must have space dimension `space_dimension()'
409 // and representation `representation()'.
410 for (dimension_type i = num_rows(); i-- > 0; ) {
411 const Congruence& cg = rows[i];
412 if (cg.space_dimension() != space_dimension()) {
413 return false;
414 }
415 if (cg.representation() != representation()) {
416 return false;
417 }
418 if (!cg.OK()) {
419 return false;
420 }
421 }
422 // All checks passed.
423 return true;
424 }
425
426 /*! \relates Parma_Polyhedra_Library::Congruence_System */
427 std::ostream&
operator <<(std::ostream & s,const Congruence_System & cgs)428 PPL::IO_Operators::operator<<(std::ostream& s, const Congruence_System& cgs) {
429 Congruence_System::const_iterator i = cgs.begin();
430 const Congruence_System::const_iterator cgs_end = cgs.end();
431 if (i == cgs_end) {
432 return s << "true";
433 }
434 while (true) {
435 Congruence cg = *i;
436 cg.strong_normalize();
437 s << cg;
438 ++i;
439 if (i == cgs_end) {
440 return s;
441 }
442 s << ", ";
443 }
444 }
445
446 /*! \relates Parma_Polyhedra_Library::Congruence_System */
447 bool
operator ==(const Congruence_System & x,const Congruence_System & y)448 PPL::operator==(const Congruence_System& x, const Congruence_System& y) {
449 if (x.num_rows() != y.num_rows()) {
450 return false;
451 }
452 for (dimension_type i = x.num_rows(); i-- > 0; ) {
453 // NOTE: this also checks for space dimension.
454 if (x[i] != y[i]) {
455 return false;
456 }
457 }
458 return true;
459 }
460
461 void
462 PPL::Congruence_System
add_unit_rows_and_space_dimensions(dimension_type dims)463 ::add_unit_rows_and_space_dimensions(dimension_type dims) {
464 const dimension_type old_num_rows = num_rows();
465 set_space_dimension(space_dimension() + dims);
466
467 rows.resize(rows.size() + dims);
468
469 // Swap the added rows to the front of the vector.
470 for (dimension_type row = old_num_rows; row-- > 0; ) {
471 swap(rows[row], rows[row + dims]);
472 }
473
474 const dimension_type dim = space_dimension();
475 // Set the space dimension and the diagonal element of each added row.
476 for (dimension_type row = dims; row-- > 0; ) {
477 Linear_Expression expr(representation());
478 expr.set_space_dimension(space_dimension());
479 PPL_ASSERT(dim >= row + 1);
480 expr += Variable(dim - row - 1);
481 // This constructor steals the contents of `expr'.
482 Congruence cg(expr, Coefficient_zero(), Recycle_Input());
483 swap(rows[row], cg);
484 }
485
486 PPL_ASSERT(OK());
487 }
488
489 void
concatenate(const Congruence_System & y)490 PPL::Congruence_System::concatenate(const Congruence_System& y) {
491 // TODO: this implementation is just an executable specification.
492 Congruence_System cgs = y;
493
494 const dimension_type added_rows = cgs.num_rows();
495 const dimension_type added_columns = cgs.space_dimension();
496
497 const dimension_type old_num_rows = num_rows();
498 const dimension_type old_space_dim = space_dimension();
499
500 set_space_dimension(space_dimension() + added_columns);
501
502 rows.resize(rows.size() + added_rows);
503
504 // Move the congruences into *this from `cgs', shifting the
505 // coefficients along into the appropriate columns.
506 for (dimension_type i = added_rows; i-- > 0; ) {
507 Congruence& cg_old = cgs.rows[i];
508 Congruence& cg_new = rows[old_num_rows + i];
509 cg_old.set_representation(representation());
510 cg_old.shift_space_dimensions(Variable(0), old_space_dim);
511 swap(cg_old, cg_new);
512 }
513 }
514