1 /* Linear_System class implementation: 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 #ifndef PPL_Linear_System_inlines_hh
25 #define PPL_Linear_System_inlines_hh 1
26
27 #include "Bit_Row_defs.hh"
28 #include "Coefficient_defs.hh"
29
30 #include <algorithm>
31
32 namespace Parma_Polyhedra_Library {
33
34 template <typename Row>
35 inline memory_size_type
external_memory_in_bytes() const36 Linear_System<Row>::external_memory_in_bytes() const {
37 return rows.external_memory_in_bytes();
38 }
39
40 template <typename Row>
41 inline memory_size_type
total_memory_in_bytes() const42 Linear_System<Row>::total_memory_in_bytes() const {
43 return sizeof(*this) + external_memory_in_bytes();
44 }
45
46 template <typename Row>
47 inline bool
is_sorted() const48 Linear_System<Row>::is_sorted() const {
49 // The flag `sorted' does not really reflect the sortedness status
50 // of a system (if `sorted' evaluates to `false' nothing is known).
51 // This assertion is used to ensure that the system
52 // is actually sorted when `sorted' value is 'true'.
53 PPL_ASSERT(!sorted || check_sorted());
54 return sorted;
55 }
56
57 template <typename Row>
58 inline void
set_sorted(const bool b)59 Linear_System<Row>::set_sorted(const bool b) {
60 sorted = b;
61 PPL_ASSERT(OK());
62 }
63
64 template <typename Row>
65 inline
Linear_System(Topology topol,Representation r)66 Linear_System<Row>::Linear_System(Topology topol, Representation r)
67 : rows(),
68 space_dimension_(0),
69 row_topology(topol),
70 index_first_pending(0),
71 sorted(true),
72 representation_(r) {
73
74 PPL_ASSERT(OK());
75 }
76
77 template <typename Row>
78 inline
Linear_System(Topology topol,dimension_type space_dim,Representation r)79 Linear_System<Row>::Linear_System(Topology topol,
80 dimension_type space_dim,
81 Representation r)
82 : rows(),
83 space_dimension_(0),
84 row_topology(topol),
85 index_first_pending(0),
86 sorted(true),
87 representation_(r) {
88 set_space_dimension(space_dim);
89 PPL_ASSERT(OK());
90 }
91
92 template <typename Row>
93 inline dimension_type
first_pending_row() const94 Linear_System<Row>::first_pending_row() const {
95 return index_first_pending;
96 }
97
98 template <typename Row>
99 inline dimension_type
num_pending_rows() const100 Linear_System<Row>::num_pending_rows() const {
101 PPL_ASSERT(num_rows() >= first_pending_row());
102 return num_rows() - first_pending_row();
103 }
104
105 template <typename Row>
106 inline void
unset_pending_rows()107 Linear_System<Row>::unset_pending_rows() {
108 index_first_pending = num_rows();
109 PPL_ASSERT(OK());
110 }
111
112 template <typename Row>
113 inline void
set_index_first_pending_row(const dimension_type i)114 Linear_System<Row>::set_index_first_pending_row(const dimension_type i) {
115 index_first_pending = i;
116 PPL_ASSERT(OK());
117 }
118
119 template <typename Row>
120 inline
Linear_System(const Linear_System & y)121 Linear_System<Row>::Linear_System(const Linear_System& y)
122 : rows(y.rows),
123 space_dimension_(y.space_dimension_),
124 row_topology(y.row_topology),
125 representation_(y.representation_) {
126 // Previously pending rows may violate sortedness.
127 sorted = (y.num_pending_rows() > 0) ? false : y.sorted;
128 unset_pending_rows();
129 PPL_ASSERT(OK());
130 }
131
132 template <typename Row>
133 inline
Linear_System(const Linear_System & y,Representation r)134 Linear_System<Row>::Linear_System(const Linear_System& y, Representation r)
135 : rows(),
136 space_dimension_(y.space_dimension_),
137 row_topology(y.row_topology),
138 representation_(r) {
139 rows.resize(y.num_rows());
140 for (dimension_type i = 0; i < y.num_rows(); ++i) {
141 // Create the copies with the right representation.
142 Row row(y.rows[i], r);
143 swap(rows[i], row);
144 }
145 // Previously pending rows may violate sortedness.
146 sorted = (y.num_pending_rows() > 0) ? false : y.sorted;
147 unset_pending_rows();
148 PPL_ASSERT(OK());
149 }
150
151 template <typename Row>
152 inline
Linear_System(const Linear_System & y,With_Pending)153 Linear_System<Row>::Linear_System(const Linear_System& y, With_Pending)
154 : rows(y.rows),
155 space_dimension_(y.space_dimension_),
156 row_topology(y.row_topology),
157 index_first_pending(y.index_first_pending),
158 sorted(y.sorted),
159 representation_(y.representation_) {
160 PPL_ASSERT(OK());
161 }
162
163 template <typename Row>
164 inline
Linear_System(const Linear_System & y,Representation r,With_Pending)165 Linear_System<Row>::Linear_System(const Linear_System& y, Representation r,
166 With_Pending)
167 : rows(),
168 space_dimension_(y.space_dimension_),
169 row_topology(y.row_topology),
170 index_first_pending(y.index_first_pending),
171 sorted(y.sorted),
172 representation_(r) {
173 rows.resize(y.num_rows());
174 for (dimension_type i = 0; i < y.num_rows(); ++i) {
175 // Create the copies with the right representation.
176 Row row(y.rows[i], r);
177 swap(rows[i], row);
178 }
179 PPL_ASSERT(OK());
180 }
181
182 template <typename Row>
183 inline Linear_System<Row>&
operator =(const Linear_System & y)184 Linear_System<Row>::operator=(const Linear_System& y) {
185 // NOTE: Pending rows are transformed into non-pending ones.
186 Linear_System<Row> tmp = y;
187 swap(*this, tmp);
188 return *this;
189 }
190
191 template <typename Row>
192 inline void
assign_with_pending(const Linear_System & y)193 Linear_System<Row>::assign_with_pending(const Linear_System& y) {
194 Linear_System<Row> tmp(y, With_Pending());
195 swap(*this, tmp);
196 }
197
198 template <typename Row>
199 inline void
m_swap(Linear_System & y)200 Linear_System<Row>::m_swap(Linear_System& y) {
201 using std::swap;
202 swap(rows, y.rows);
203 swap(space_dimension_, y.space_dimension_);
204 swap(row_topology, y.row_topology);
205 swap(index_first_pending, y.index_first_pending);
206 swap(sorted, y.sorted);
207 swap(representation_, y.representation_);
208 PPL_ASSERT(OK());
209 PPL_ASSERT(y.OK());
210 }
211
212 template <typename Row>
213 inline void
clear()214 Linear_System<Row>::clear() {
215 // Note: do NOT modify the value of `row_topology' and `representation'.
216 rows.clear();
217 index_first_pending = 0;
218 sorted = true;
219 space_dimension_ = 0;
220
221 PPL_ASSERT(OK());
222 }
223
224 template <typename Row>
225 inline void
mark_as_necessarily_closed()226 Linear_System<Row>::mark_as_necessarily_closed() {
227 PPL_ASSERT(topology() == NOT_NECESSARILY_CLOSED);
228 row_topology = NECESSARILY_CLOSED;
229 ++space_dimension_;
230 for (dimension_type i = num_rows(); i-- > 0; ) {
231 rows[i].mark_as_necessarily_closed();
232 }
233 }
234
235 template <typename Row>
236 inline void
mark_as_not_necessarily_closed()237 Linear_System<Row>::mark_as_not_necessarily_closed() {
238 PPL_ASSERT(topology() == NECESSARILY_CLOSED);
239 PPL_ASSERT(space_dimension() > 0);
240 row_topology = NOT_NECESSARILY_CLOSED;
241 --space_dimension_;
242 for (dimension_type i = num_rows(); i-- > 0; ) {
243 rows[i].mark_as_not_necessarily_closed();
244 }
245 }
246
247 template <typename Row>
248 inline void
set_topology(Topology t)249 Linear_System<Row>::set_topology(Topology t) {
250 if (topology() == t) {
251 return;
252 }
253 for (dimension_type i = num_rows(); i-- > 0; ) {
254 rows[i].set_topology(t);
255 }
256 row_topology = t;
257 PPL_ASSERT(OK());
258 }
259
260 template <typename Row>
261 inline void
set_necessarily_closed()262 Linear_System<Row>::set_necessarily_closed() {
263 set_topology(NECESSARILY_CLOSED);
264 }
265
266 template <typename Row>
267 inline void
set_not_necessarily_closed()268 Linear_System<Row>::set_not_necessarily_closed() {
269 set_topology(NOT_NECESSARILY_CLOSED);
270 }
271
272 template <typename Row>
273 inline bool
is_necessarily_closed() const274 Linear_System<Row>::is_necessarily_closed() const {
275 return row_topology == NECESSARILY_CLOSED;
276 }
277
278 template <typename Row>
279 inline const Row&
operator [](const dimension_type k) const280 Linear_System<Row>::operator[](const dimension_type k) const {
281 return rows[k];
282 }
283
284 template <typename Row>
285 inline typename Linear_System<Row>::iterator
begin()286 Linear_System<Row>::begin() {
287 return rows.begin();
288 }
289
290 template <typename Row>
291 inline typename Linear_System<Row>::iterator
end()292 Linear_System<Row>::end() {
293 return rows.end();
294 }
295
296 template <typename Row>
297 inline typename Linear_System<Row>::const_iterator
begin() const298 Linear_System<Row>::begin() const {
299 return rows.begin();
300 }
301
302 template <typename Row>
303 inline typename Linear_System<Row>::const_iterator
end() const304 Linear_System<Row>::end() const {
305 return rows.end();
306 }
307
308 template <typename Row>
309 inline bool
has_no_rows() const310 Linear_System<Row>::has_no_rows() const {
311 return rows.empty();
312 }
313
314 template <typename Row>
315 inline dimension_type
num_rows() const316 Linear_System<Row>::num_rows() const {
317 return rows.size();
318 }
319
320 template <typename Row>
321 inline Topology
topology() const322 Linear_System<Row>::topology() const {
323 return row_topology;
324 }
325
326 template <typename Row>
327 inline Representation
representation() const328 Linear_System<Row>::representation() const {
329 return representation_;
330 }
331
332 template <typename Row>
333 inline void
set_representation(Representation r)334 Linear_System<Row>::set_representation(Representation r) {
335 representation_ = r;
336 for (dimension_type i = 0; i < rows.size(); ++i) {
337 rows[i].set_representation(r);
338 }
339 PPL_ASSERT(OK());
340 }
341
342 template <typename Row>
343 inline dimension_type
max_space_dimension()344 Linear_System<Row>::max_space_dimension() {
345 return Row::max_space_dimension();
346 }
347
348 template <typename Row>
349 inline dimension_type
space_dimension() const350 Linear_System<Row>::space_dimension() const {
351 return space_dimension_;
352 }
353
354 template <typename Row>
355 inline void
set_space_dimension_no_ok(dimension_type space_dim)356 Linear_System<Row>::set_space_dimension_no_ok(dimension_type space_dim) {
357 for (dimension_type i = rows.size(); i-- > 0; ) {
358 rows[i].set_space_dimension_no_ok(space_dim);
359 }
360 space_dimension_ = space_dim;
361 }
362
363 template <typename Row>
364 inline void
set_space_dimension(dimension_type space_dim)365 Linear_System<Row>::set_space_dimension(dimension_type space_dim) {
366 set_space_dimension_no_ok(space_dim);
367 PPL_ASSERT(OK());
368 }
369
370 template <typename Row>
371 inline void
remove_row_no_ok(const dimension_type i,const bool keep_sorted)372 Linear_System<Row>::remove_row_no_ok(const dimension_type i,
373 const bool keep_sorted) {
374 PPL_ASSERT(i < num_rows());
375 const bool was_pending = (i >= index_first_pending);
376
377 if (sorted && keep_sorted && !was_pending) {
378 for (dimension_type j = i + 1; j < rows.size(); ++j) {
379 swap(rows[j], rows[j-1]);
380 }
381 rows.pop_back();
382 }
383 else {
384 if (!was_pending) {
385 sorted = false;
386 }
387 const bool last_row_is_pending = (num_rows() - 1 >= index_first_pending);
388 if (was_pending == last_row_is_pending) {
389 // Either both rows are pending or both rows are not pending.
390 swap(rows[i], rows.back());
391 }
392 else {
393 // Pending rows are stored after the non-pending ones.
394 PPL_ASSERT(!was_pending);
395 PPL_ASSERT(last_row_is_pending);
396
397 // Swap the row with the last non-pending row.
398 swap(rows[i], rows[index_first_pending - 1]);
399
400 // Now the (non-pending) row that has to be deleted is between the
401 // non-pending and the pending rows.
402 swap(rows[i], rows.back());
403 }
404 rows.pop_back();
405 }
406 if (!was_pending) {
407 // A non-pending row has been removed.
408 --index_first_pending;
409 }
410 }
411
412 template <typename Row>
413 inline void
remove_row(const dimension_type i,bool keep_sorted)414 Linear_System<Row>::remove_row(const dimension_type i, bool keep_sorted) {
415 remove_row_no_ok(i, keep_sorted);
416 PPL_ASSERT(OK());
417 }
418
419
420 template <typename Row>
421 inline void
remove_rows(dimension_type first,dimension_type last,bool keep_sorted)422 Linear_System<Row>::remove_rows(dimension_type first,
423 dimension_type last,
424 bool keep_sorted) {
425 PPL_ASSERT(first <= last);
426 PPL_ASSERT(last <= num_rows());
427 const dimension_type n = last - first;
428
429 if (n == 0) {
430 return;
431 }
432
433 // All the rows that have to be removed must have the same (pending or
434 // non-pending) status.
435 PPL_ASSERT(first >= index_first_pending || last <= index_first_pending);
436
437 const bool were_pending = (first >= index_first_pending);
438
439 // Move the rows in [first,last) at the end of the system.
440 if (sorted && keep_sorted && !were_pending) {
441 // Preserve the row ordering.
442 for (dimension_type i = last; i < rows.size(); ++i) {
443 swap(rows[i], rows[i - n]);
444 }
445
446 rows.resize(rows.size() - n);
447
448 // `n' non-pending rows have been removed.
449 index_first_pending -= n;
450
451 PPL_ASSERT(OK());
452 return;
453 }
454
455 // We can ignore the row ordering, but we must not mix pending and
456 // non-pending rows.
457
458 const dimension_type offset = rows.size() - n - first;
459 // We want to swap the rows in [first, last) and
460 // [first + offset, last + offset) (note that these intervals may not be
461 // disjunct).
462
463 if (index_first_pending == num_rows()) {
464 // There are no pending rows.
465 PPL_ASSERT(!were_pending);
466
467 swap_row_intervals(first, last, offset);
468
469 rows.resize(rows.size() - n);
470
471 // `n' non-pending rows have been removed.
472 index_first_pending -= n;
473 }
474 else {
475 // There are some pending rows in [first + offset, last + offset).
476 if (were_pending) {
477 // Both intervals contain only pending rows, because the second
478 // interval is after the first.
479
480 swap_row_intervals(first, last, offset);
481
482 rows.resize(rows.size() - n);
483
484 // `n' non-pending rows have been removed.
485 index_first_pending -= n;
486 }
487 else {
488 PPL_ASSERT(rows.size() - n < index_first_pending);
489 PPL_ASSERT(rows.size() > index_first_pending);
490 PPL_ASSERT(!were_pending);
491 // In the [size() - n, size()) interval there are some non-pending
492 // rows and some pending ones. Be careful not to mix them.
493
494 PPL_ASSERT(index_first_pending >= last);
495 swap_row_intervals(first, last, index_first_pending - last);
496
497 // Mark the rows that must be deleted as pending.
498 index_first_pending -= n;
499 first = index_first_pending;
500 last = first + n;
501
502 // Move them at the end of the system.
503 swap_row_intervals(first, last, num_rows() - last);
504
505 // Actually remove the rows.
506 rows.resize(rows.size() - n);
507 }
508 }
509
510 PPL_ASSERT(OK());
511 }
512
513 template <typename Row>
514 inline void
swap_row_intervals(dimension_type first,dimension_type last,dimension_type offset)515 Linear_System<Row>::swap_row_intervals(dimension_type first,
516 dimension_type last,
517 dimension_type offset) {
518 PPL_ASSERT(first <= last);
519 PPL_ASSERT(last + offset <= num_rows());
520 #ifndef NDEBUG
521 if (first < last) {
522 bool first_interval_has_pending_rows = (last > index_first_pending);
523 bool second_interval_has_pending_rows = (last + offset > index_first_pending);
524 bool first_interval_has_not_pending_rows = (first < index_first_pending);
525 bool second_interval_has_not_pending_rows = (first + offset < index_first_pending);
526 PPL_ASSERT(first_interval_has_not_pending_rows
527 == !first_interval_has_pending_rows);
528 PPL_ASSERT(second_interval_has_not_pending_rows
529 == !second_interval_has_pending_rows);
530 PPL_ASSERT(first_interval_has_pending_rows
531 == second_interval_has_pending_rows);
532 }
533 #endif
534 if (first + offset < last) {
535 // The intervals are not disjunct, make them so.
536 const dimension_type k = last - first - offset;
537 last -= k;
538 offset += k;
539 }
540
541 if (first == last) {
542 // Nothing to do.
543 return;
544 }
545
546 for (dimension_type i = first; i < last; ++i) {
547 swap(rows[i], rows[i + offset]);
548 }
549
550 if (first < index_first_pending) {
551 // The swaps involved not pending rows, so they may not be sorted anymore.
552 set_sorted(false);
553 }
554
555 PPL_ASSERT(OK());
556 }
557
558 template <typename Row>
559 inline void
remove_rows(const std::vector<dimension_type> & indexes)560 Linear_System<Row>::remove_rows(const std::vector<dimension_type>& indexes) {
561 #ifndef NDEBUG
562 {
563 // Check that `indexes' is sorted.
564 std::vector<dimension_type> sorted_indexes = indexes;
565 std::sort(sorted_indexes.begin(), sorted_indexes.end());
566 PPL_ASSERT(indexes == sorted_indexes);
567
568 // Check that the last index (if any) is lower than num_rows().
569 // This guarantees that all indexes are in [0, num_rows()).
570 if (!indexes.empty()) {
571 PPL_ASSERT(indexes.back() < num_rows());
572 }
573 }
574 #endif
575
576 if (indexes.empty()) {
577 return;
578 }
579
580 const dimension_type rows_size = rows.size();
581 typedef std::vector<dimension_type>::const_iterator itr_t;
582
583 // `i' and last_unused_row' start with the value `indexes[0]' instead
584 // of `0', because the loop would just increment `last_unused_row' in the
585 // preceding iterations.
586 dimension_type last_unused_row = indexes[0];
587 dimension_type i = indexes[0];
588 itr_t itr = indexes.begin();
589 itr_t itr_end = indexes.end();
590 while (itr != itr_end) {
591 // i <= *itr < rows_size
592 PPL_ASSERT(i < rows_size);
593 if (*itr == i) {
594 // The current row has to be removed, don't increment last_unused_row.
595 ++itr;
596 }
597 else {
598 // The current row must not be removed, swap it after the last used row.
599 swap(rows[last_unused_row], rows[i]);
600 ++last_unused_row;
601 }
602 ++i;
603 }
604
605 // Move up the remaining rows, if any.
606 for ( ; i < rows_size; ++i) {
607 swap(rows[last_unused_row], rows[i]);
608 ++last_unused_row;
609 }
610
611 PPL_ASSERT(last_unused_row == num_rows() - indexes.size());
612
613 // The rows that have to be removed are now at the end of the system, just
614 // remove them.
615 rows.resize(last_unused_row);
616
617 // Adjust index_first_pending.
618 if (indexes[0] >= index_first_pending) {
619 // Removing pending rows only.
620 }
621 else {
622 if (indexes.back() < index_first_pending) {
623 // Removing non-pending rows only.
624 index_first_pending -= indexes.size();
625 }
626 else {
627 // Removing some pending and some non-pending rows, count the
628 // non-pending rows that must be removed.
629 // This exploits the fact that `indexes' is sorted by using binary
630 // search.
631 itr_t j = std::lower_bound(indexes.begin(), indexes.end(),
632 index_first_pending);
633 std::iterator_traits<itr_t>::difference_type
634 non_pending = j - indexes.begin();
635 index_first_pending -= static_cast<dimension_type>(non_pending);
636 }
637 }
638
639 // NOTE: This method does *not* call set_sorted(false), because it preserves
640 // the relative row ordering.
641
642 PPL_ASSERT(OK());
643 }
644
645 template <typename Row>
646 inline void
remove_trailing_rows(const dimension_type n)647 Linear_System<Row>::remove_trailing_rows(const dimension_type n) {
648 PPL_ASSERT(rows.size() >= n);
649 rows.resize(rows.size() - n);
650 if (first_pending_row() > rows.size()) {
651 index_first_pending = rows.size();
652 }
653 PPL_ASSERT(OK());
654 }
655
656 template <typename Row>
657 inline void
658 Linear_System<Row>
permute_space_dimensions(const std::vector<Variable> & cycle)659 ::permute_space_dimensions(const std::vector<Variable>& cycle) {
660 for (dimension_type i = num_rows(); i-- > 0; ) {
661 rows[i].permute_space_dimensions(cycle);
662 }
663 sorted = false;
664 PPL_ASSERT(OK());
665 }
666
667 template <typename Row>
668 inline void
669 Linear_System<Row>
swap_space_dimensions(Variable v1,Variable v2)670 ::swap_space_dimensions(Variable v1, Variable v2) {
671 PPL_ASSERT(v1.space_dimension() <= space_dimension());
672 PPL_ASSERT(v2.space_dimension() <= space_dimension());
673 for (dimension_type k = num_rows(); k-- > 0; ) {
674 rows[k].swap_space_dimensions(v1, v2);
675 }
676 sorted = false;
677 PPL_ASSERT(OK());
678 }
679
680 /*! \relates Linear_System */
681 template <typename Row>
682 inline bool
operator !=(const Linear_System<Row> & x,const Linear_System<Row> & y)683 operator!=(const Linear_System<Row>& x, const Linear_System<Row>& y) {
684 return !(x == y);
685 }
686
687 template <typename Row>
688 inline bool
operator ()(const Row & x,const Row & y) const689 Linear_System<Row>::Row_Less_Than::operator()(const Row& x,
690 const Row& y) const {
691 return compare(x, y) < 0;
692 }
693
694 template <typename Row>
695 inline
696 Linear_System<Row>::Unique_Compare
Unique_Compare(const Swapping_Vector<Row> & cont,dimension_type base)697 ::Unique_Compare(const Swapping_Vector<Row>& cont,
698 dimension_type base)
699 : container(cont), base_index(base) {
700 }
701
702 template <typename Row>
703 inline bool
704 Linear_System<Row>::Unique_Compare
operator ()(dimension_type i,dimension_type j) const705 ::operator()(dimension_type i, dimension_type j) const {
706 return container[base_index + i].is_equal_to(container[base_index + j]);
707 }
708
709 /*! \relates Linear_System */
710 template <typename Row>
711 inline void
swap(Linear_System<Row> & x,Linear_System<Row> & y)712 swap(Linear_System<Row>& x, Linear_System<Row>& y) {
713 x.m_swap(y);
714 }
715
716 } // namespace Parma_Polyhedra_Library
717
718 #endif // !defined(PPL_Linear_System_inlines_hh)
719