PPL  1.2
Linear_Expression_Impl.cc
Go to the documentation of this file.
1 /* Linear_Expression_Impl class implementation.
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"
26 #include "Dense_Row_defs.hh"
27 #include "Sparse_Row_defs.hh"
28 #include "assertions.hh"
29 #include <iostream>
30 
31 namespace Parma_Polyhedra_Library {
32 
33 template <>
34 bool
36  return (row.size() != 0);
37 }
38 
39 template <>
40 bool
42  if (row.size() == 0) {
43  return false;
44  }
45  for (Sparse_Row::const_iterator i = row.begin(),
46  i_end = row.end(); i != i_end; ++i) {
47  if (*i == 0) {
48  std::cerr << "Linear_Expression_Impl<Sparse_Row>::OK() failed."
49  << " row was:\n";
50  row.ascii_dump(std::cerr);
51  // Found a stored zero.
52  return false;
53  }
54  }
55  return true;
56 }
57 
58 template <>
59 void
62  PPL_ASSERT(vars.space_dimension() <= space_dimension());
63  if (vars.empty()) {
64  return;
65  }
66 
67  // For each variable to be removed, replace the corresponding coefficient
68  // by shifting left the coefficient to the right that will be kept.
69  Variables_Set::const_iterator vsi = vars.begin();
70  Variables_Set::const_iterator vsi_end = vars.end();
71  dimension_type dst_col = *vsi+1;
72  dimension_type src_col = dst_col + 1;
73  for (++vsi; vsi != vsi_end; ++vsi) {
74  const dimension_type vsi_col = *vsi+1;
75  // Move all columns in between to the left.
76  while (src_col < vsi_col) {
77  row.swap_coefficients(dst_col++, src_col++);
78  }
79  ++src_col;
80  }
81  // Move any remaining columns.
82  const dimension_type sz = row.size();
83  while (src_col < sz) {
84  row.swap_coefficients(dst_col++, src_col++);
85  }
86 
87  // The number of remaining coefficients is `dst_col'.
88  row.resize(dst_col);
89  PPL_ASSERT(OK());
90 }
91 
92 template <>
93 void
96  PPL_ASSERT(vars.space_dimension() <= space_dimension());
97  if (vars.empty()) {
98  return;
99  }
100 
101  // For each variable to be removed, replace the corresponding coefficient
102  // by shifting left the coefficient to the right that will be kept.
103  Variables_Set::const_iterator vsi = vars.begin();
104  Variables_Set::const_iterator vsi_end = vars.end();
105  Sparse_Row::iterator src = row.lower_bound(*vsi + 1);
106  const Sparse_Row::iterator& row_end = row.end();
107  dimension_type num_removed = 0;
108  while (vsi != vsi_end) {
109  // Delete the element.
110  if (src != row_end && src.index() == *vsi + 1) {
111  src = row.reset(src);
112  }
113  ++num_removed;
114  ++vsi;
115  if (vsi != vsi_end) {
116  // Shift left the coefficients in [src.index(), *vsi + 1) by num_removed
117  // positions.
118  while (src != row_end && src.index() < *vsi + 1) {
119  row.fast_swap(src.index() - num_removed, src);
120  ++src;
121  }
122  }
123  else {
124  // Shift left the coefficients in [src.index(), row.size()) by
125  // num_removed positions.
126  while (src != row_end) {
127  row.fast_swap(src.index() - num_removed, src);
128  ++src;
129  }
130  }
131  }
132 
133  PPL_ASSERT(num_removed == vars.size());
134 
135  row.resize(row.size() - num_removed);
136  PPL_ASSERT(OK());
137 }
138 
139 template <>
140 bool
142  for (dimension_type i = row.size(); i-- > 0; ) {
143  if (row[i] != 0) {
144  return false;
145  }
146  }
147  return true;
148 }
149 
150 template <>
151 bool
153  for (dimension_type i = 1; i < row.size(); ++i) {
154  if (row[i] != 0) {
155  return false;
156  }
157  }
158  return true;
159 }
160 
161 template <>
162 bool
164  dimension_type end) const {
165  for (dimension_type i = start; i < end; ++i) {
166  if (row[i] != 0) {
167  return false;
168  }
169  }
170  return true;
171 }
172 
173 template <>
176  dimension_type end) const {
177  PPL_ASSERT(start <= end);
178  dimension_type result = 0;
179  for (dimension_type i = start; i < end; ++i) {
180  if (row[i] == 0) {
181  ++result;
182  }
183  }
184  return result;
185 }
186 
187 template <>
190  dimension_type end) const {
191  dimension_type i;
192 
193  for (i = start; i < end; ++i) {
194  if (row[i] != 0) {
195  break;
196  }
197  }
198 
199  if (i == end) {
200  return 0;
201  }
202 
203  PPL_ASSERT(row[i] != 0);
204 
205  Coefficient result = row[i];
206  ++i;
207 
208  if (result < 0) {
209  neg_assign(result);
210  }
211 
212  for ( ; i < end; ++i) {
213  if (row[i] == 0) {
214  continue;
215  }
216  gcd_assign(result, row[i], result);
217  if (result == 1) {
218  return result;
219  }
220  }
221 
222  return result;
223 }
224 
225 template <>
228  dimension_type end) const {
229  Sparse_Row::const_iterator i = row.lower_bound(start);
230  Sparse_Row::const_iterator i_end = row.lower_bound(end);
231 
232  if (i == i_end) {
233  return 0;
234  }
235 
236  PPL_ASSERT(*i != 0);
237 
238  Coefficient result = *i;
239  ++i;
240 
241  if (result < 0) {
242  neg_assign(result);
243  }
244 
245  for ( ; i != i_end; ++i) {
246  gcd_assign(result, *i, result);
247  if (result == 1) {
248  return result;
249  }
250  }
251 
252  return result;
253 }
254 
255 template <>
256 bool
258 ::all_zeroes(const Variables_Set& vars) const {
259  Variables_Set::const_iterator j = vars.begin();
260  Variables_Set::const_iterator j_end = vars.end();
261 
262  for ( ; j != j_end; ++j) {
263  if (row[*j + 1] != 0) {
264  return false;
265  }
266  }
267 
268  return true;
269 }
270 
271 template <>
272 bool
274 ::all_zeroes(const Variables_Set& vars) const {
275  Sparse_Row::const_iterator i = row.begin();
276  Sparse_Row::const_iterator i_end = row.end();
277  Variables_Set::const_iterator j = vars.begin();
278  Variables_Set::const_iterator j_end = vars.end();
279 
280  for ( ; j != j_end; ++j) {
281  i = row.lower_bound(i, *j + 1);
282  if (i == i_end) {
283  break;
284  }
285  if (i.index() == *j + 1) {
286  return false;
287  }
288  }
289 
290  return true;
291 }
292 
293 template <>
294 bool
297  dimension_type start, dimension_type end) const {
298  if (start == 0) {
299  if (row[0] != 0) {
300  return false;
301  }
302  ++start;
303  }
304  for (dimension_type i = start; i < end; ++i) {
305  if (row[i] != 0 && vars.count(i - 1) == 0) {
306  return false;
307  }
308  }
309  return true;
310 }
311 
312 template <>
313 bool
316  dimension_type start, dimension_type end) const {
317  PPL_ASSERT(start <= end);
318  if (start == end) {
319  return true;
320  }
321  if (start == 0) {
322  if (row.find(0) != row.end()) {
323  return false;
324  }
325 
326  start = 1;
327  }
328 
329  PPL_ASSERT(start != 0);
330  PPL_ASSERT(start <= end);
331  for (Sparse_Row::const_iterator i = row.lower_bound(start),
332  i_end = row.lower_bound(end); i != i_end; ++i) {
333  if (vars.count(i.index() - 1) == 0) {
334  return false;
335  }
336  }
337 
338  return true;
339 }
340 
341 template <>
344  for (dimension_type i = row.size(); i-- > 0; ) {
345  if (row[i] != 0) {
346  return i;
347  }
348  }
349  return 0;
350 }
351 
352 template <>
356  PPL_ASSERT(first <= last);
357  PPL_ASSERT(last <= row.size());
358  for (dimension_type i = first; i < last; ++i) {
359  if (row[i] != 0) {
360  return i;
361  }
362  }
363 
364  return last;
365 }
366 
367 template <>
371  PPL_ASSERT(first <= last);
372  PPL_ASSERT(last <= row.size());
373  for (dimension_type i = last; i-- > first; ) {
374  if (row[i] != 0) {
375  return i;
376  }
377  }
378 
379  return last;
380 }
381 
382 template <>
383 void
385 ::has_a_free_dimension_helper(std::set<dimension_type>& x) const {
386  typedef std::set<dimension_type> set_t;
387  set_t result;
388  for (set_t::const_iterator i = x.begin(), i_end = x.end(); i != i_end; ++i) {
389  if (row[*i] == 0) {
390  result.insert(*i);
391  }
392  }
393  using std::swap;
394  swap(x, result);
395 }
396 
397 template <>
398 void
400 ::has_a_free_dimension_helper(std::set<dimension_type>& x) const {
401  typedef std::set<dimension_type> set_t;
402  set_t result;
403  Sparse_Row::const_iterator itr = row.end();
404  Sparse_Row::const_iterator itr_end = row.end();
405  set_t::const_iterator i = x.begin();
406  set_t::const_iterator i_end = x.end();
407  for ( ; i != i_end; ++i) {
408  itr = row.lower_bound(itr, *i);
409  if (itr == itr_end) {
410  break;
411  }
412  if (itr.index() != *i) {
413  result.insert(*i);
414  }
415  }
416  for ( ; i != i_end; ++i) {
417  result.insert(*i);
418  }
419  using std::swap;
420  swap(x, result);
421 }
422 
423 template <>
424 template <>
425 bool
428  Variable first, Variable last) const {
429  const dimension_type start = first.space_dimension();
430  const dimension_type end = last.space_dimension();
431  PPL_ASSERT(start <= end);
432  PPL_ASSERT(end <= row.size());
433  PPL_ASSERT(end <= y.row.size());
434  for (dimension_type i = start; i < end; ++i) {
435  if (row[i] != 0 && y.row[i] != 0) {
436  return true;
437  }
438  }
439  return false;
440 }
441 
442 template <>
443 template <>
444 bool
447  Variable first, Variable last) const {
448  const dimension_type start = first.space_dimension();
449  const dimension_type end = last.space_dimension();
450  PPL_ASSERT(start <= end);
451  PPL_ASSERT(end <= row.size());
452  PPL_ASSERT(end <= y.row.size());
453  for (Sparse_Row::const_iterator i = row.lower_bound(start),
454  i_end = row.lower_bound(end); i != i_end; ++i) {
455  if (y.row[i.index()] != 0) {
456  return true;
457  }
458  }
459  return false;
460 }
461 
462 template <>
463 template <>
464 bool
467  Variable first, Variable last) const {
468  return y.have_a_common_variable(*this, first, last);
469 }
470 
471 template <>
472 template <>
473 bool
476  Variable first, Variable last) const {
477  const dimension_type start = first.space_dimension();
478  const dimension_type end = last.space_dimension();
479  PPL_ASSERT(start <= end);
480  PPL_ASSERT(end <= row.size());
481  PPL_ASSERT(end <= y.row.size());
482  Sparse_Row::const_iterator i = row.lower_bound(start);
483  Sparse_Row::const_iterator i_end = row.lower_bound(end);
486  while (i != i_end && j != j_end) {
487  if (i.index() == j.index()) {
488  return true;
489  }
490  if (i.index() < j.index()) {
491  ++i;
492  }
493  else {
494  ++j;
495  }
496  }
497  return false;
498 }
499 
500 template <>
501 void
504  while (itr != row->end() && *itr == 0) {
505  ++itr;
506  }
507 }
508 
509 template <>
510 void
513  PPL_ASSERT(itr.index() > 0);
514  while (*itr == 0) {
515  PPL_ASSERT(itr.index() > 1);
516  --itr;
517  }
518 }
519 
520 } // namespace Parma_Polyhedra_Library
dimension_type index() const
Returns the index of the element pointed to by *this.
dimension_type space_dimension() const
Returns the dimension of the smallest vector space enclosing all the variables whose indexes are in t...
virtual void has_a_free_dimension_helper(std::set< dimension_type > &x) const
Removes from the set x all the indexes of nonzero elements of *this.
void swap(CO_Tree &x, CO_Tree &y)
virtual dimension_type first_nonzero(dimension_type first, dimension_type last) const
size_t dimension_type
An unsigned integral type for representing space dimensions.
An std::set of variables' indexes.
dimension_type size() const
Returns the size of the row.
virtual bool have_a_common_variable(const Linear_Expression_Interface &x, Variable first, Variable last) const
virtual bool OK() const
Checks if all the invariants are satisfied.
An iterator on the tree elements, ordered by key.
virtual void remove_space_dimensions(const Variables_Set &vars)
Removes all the specified dimensions from the expression.
virtual dimension_type num_zeroes(dimension_type start, dimension_type end) const
Returns the number of zero coefficient in [start, end).
A dimension of the vector space.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
dimension_type size() const
Gives the number of coefficients currently in use.
virtual bool all_zeroes_except(const Variables_Set &vars, dimension_type start, dimension_type end) const
Returns true if each coefficient in [start,end) is *not* in , disregarding coefficients of variables ...
virtual bool is_zero() const
Returns true if and only if *this is .
PPL_COEFFICIENT_TYPE Coefficient
An alias for easily naming the type of PPL coefficients.
void neg_assign(GMP_Integer &x)
The entire library is confined to this namespace.
Definition: version.hh:61
A const iterator on the tree elements, ordered by key.
iterator lower_bound(dimension_type i)
Lower bound of index i.
void gcd_assign(GMP_Integer &x, const GMP_Integer &y, const GMP_Integer &z)
virtual Coefficient gcd(dimension_type start, dimension_type end) const
Returns the gcd of the nonzero coefficients in [start,end). If all the coefficients in this range are...
virtual bool all_zeroes(const Variables_Set &vars) const
Returns true if the coefficient of each variable in vars[i] is .
dimension_type index() const
Returns the index of the element pointed to by *this.
virtual bool all_homogeneous_terms_are_zero() const
Returns true if and only if all the homogeneous terms of *this are .
virtual dimension_type last_nonzero() const