00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include <ppl-config.h>
00024
00025 #include "Linear_System.defs.hh"
00026 #include "Coefficient.defs.hh"
00027 #include "Row.defs.hh"
00028 #include "Bit_Matrix.defs.hh"
00029 #include "Scalar_Products.defs.hh"
00030 #include <algorithm>
00031 #include <iostream>
00032 #include <string>
00033 #include <deque>
00034
00035 #include "swapping_sort.icc"
00036
00037 namespace PPL = Parma_Polyhedra_Library;
00038
00039 PPL::dimension_type
00040 PPL::Linear_System::num_lines_or_equalities() const {
00041 assert(num_pending_rows() == 0);
00042 const Linear_System& x = *this;
00043 dimension_type n = 0;
00044 for (dimension_type i = num_rows(); i-- > 0; )
00045 if (x[i].is_line_or_equality())
00046 ++n;
00047 return n;
00048 }
00049
00050 void
00051 PPL::Linear_System::merge_rows_assign(const Linear_System& y) {
00052 assert(row_size >= y.row_size);
00053
00054 assert(check_sorted() && y.check_sorted());
00055 assert(num_pending_rows() == 0 && y.num_pending_rows() == 0);
00056
00057 Linear_System& x = *this;
00058
00059
00060 std::vector<Row> tmp;
00061
00062 tmp.reserve(compute_capacity(x.num_rows() + y.num_rows(), max_num_rows()));
00063
00064 dimension_type xi = 0;
00065 dimension_type x_num_rows = x.num_rows();
00066 dimension_type yi = 0;
00067 dimension_type y_num_rows = y.num_rows();
00068
00069 while (xi < x_num_rows && yi < y_num_rows) {
00070 const int comp = compare(x[xi], y[yi]);
00071 if (comp <= 0) {
00072
00073 std::swap(x[xi++], *tmp.insert(tmp.end(), Linear_Row()));
00074 if (comp == 0)
00075
00076 ++yi;
00077 }
00078 else {
00079
00080 Linear_Row copy(y[yi++], row_size, row_capacity);
00081 std::swap(copy, *tmp.insert(tmp.end(), Linear_Row()));
00082 }
00083 }
00084
00085 if (xi < x_num_rows)
00086 while (xi < x_num_rows)
00087 std::swap(x[xi++], *tmp.insert(tmp.end(), Linear_Row()));
00088 else
00089 while (yi < y_num_rows) {
00090 Linear_Row copy(y[yi++], row_size, row_capacity);
00091 std::swap(copy, *tmp.insert(tmp.end(), Linear_Row()));
00092 }
00093
00094
00095 std::swap(tmp, rows);
00096
00097 unset_pending_rows();
00098 assert(check_sorted());
00099 }
00100
00101 void
00102 PPL::Linear_System::set_rows_topology() {
00103 Linear_System& x = *this;
00104 if (is_necessarily_closed())
00105 for (dimension_type i = num_rows(); i-- > 0; )
00106 x[i].set_necessarily_closed();
00107 else
00108 for (dimension_type i = num_rows(); i-- > 0; )
00109 x[i].set_not_necessarily_closed();
00110 }
00111
00112 void
00113 PPL::Linear_System::ascii_dump(std::ostream& s) const {
00114
00115
00116
00117
00118 const Linear_System& x = *this;
00119 dimension_type x_num_rows = x.num_rows();
00120 dimension_type x_num_columns = x.num_columns();
00121 s << "topology " << (is_necessarily_closed()
00122 ? "NECESSARILY_CLOSED"
00123 : "NOT_NECESSARILY_CLOSED")
00124 << "\n"
00125 << x_num_rows << " x " << x_num_columns
00126 << (x.sorted ? "(sorted)" : "(not_sorted)")
00127 << "\n"
00128 << "index_first_pending " << x.first_pending_row()
00129 << "\n";
00130 for (dimension_type i = 0; i < x_num_rows; ++i)
00131 x[i].ascii_dump(s);
00132 }
00133
00134 PPL_OUTPUT_DEFINITIONS_ASCII_ONLY(Linear_System)
00135
00136 bool
00137 PPL::Linear_System::ascii_load(std::istream& s) {
00138 std::string str;
00139 if (!(s >> str) || str != "topology")
00140 return false;
00141 if (!(s >> str))
00142 return false;
00143 if (str == "NECESSARILY_CLOSED")
00144 set_necessarily_closed();
00145 else {
00146 if (str != "NOT_NECESSARILY_CLOSED")
00147 return false;
00148 set_not_necessarily_closed();
00149 }
00150
00151 dimension_type nrows;
00152 dimension_type ncols;
00153 if (!(s >> nrows))
00154 return false;
00155 if (!(s >> str))
00156 return false;
00157 if (!(s >> ncols))
00158 return false;
00159 resize_no_copy(nrows, ncols);
00160
00161 if (!(s >> str) || (str != "(sorted)" && str != "(not_sorted)"))
00162 return false;
00163 set_sorted(str == "(sorted)");
00164 dimension_type index;
00165 if (!(s >> str) || str != "index_first_pending")
00166 return false;
00167 if (!(s >> index))
00168 return false;
00169 set_index_first_pending_row(index);
00170
00171 Linear_System& x = *this;
00172 for (dimension_type row = 0; row < nrows; ++row)
00173 if (!x[row].ascii_load(s))
00174 return false;
00175
00176
00177 assert(OK(true));
00178 return true;
00179 }
00180
00181 void
00182 PPL::Linear_System::insert(const Linear_Row& r) {
00183
00184
00185 assert(r.check_strong_normalized());
00186 assert(topology() == r.topology());
00187
00188 assert(num_pending_rows() == 0);
00189
00190 const dimension_type old_num_rows = num_rows();
00191 const dimension_type old_num_columns = num_columns();
00192 const dimension_type r_size = r.size();
00193
00194
00195 if (r_size > old_num_columns) {
00196 add_zero_columns(r_size - old_num_columns);
00197 if (!is_necessarily_closed() && old_num_rows != 0)
00198
00199
00200 swap_columns(old_num_columns - 1, r_size - 1);
00201 add_row(r);
00202 }
00203 else if (r_size < old_num_columns) {
00204
00205 Linear_Row tmp_row(r, old_num_columns, row_capacity);
00206
00207 if (!is_necessarily_closed())
00208 std::swap(tmp_row[r_size - 1], tmp_row[old_num_columns - 1]);
00209 add_row(tmp_row);
00210 }
00211 else
00212
00213 add_row(r);
00214
00215
00216 assert(num_pending_rows() == 0);
00217
00218
00219 assert(OK(false));
00220 }
00221
00222 void
00223 PPL::Linear_System::insert_pending(const Linear_Row& r) {
00224
00225
00226 assert(r.check_strong_normalized());
00227 assert(topology() == r.topology());
00228
00229 const dimension_type old_num_rows = num_rows();
00230 const dimension_type old_num_columns = num_columns();
00231 const dimension_type r_size = r.size();
00232
00233
00234 if (r_size > old_num_columns) {
00235 add_zero_columns(r_size - old_num_columns);
00236 if (!is_necessarily_closed() && old_num_rows != 0)
00237
00238
00239 swap_columns(old_num_columns - 1, r_size - 1);
00240 add_pending_row(r);
00241 }
00242 else if (r_size < old_num_columns)
00243 if (is_necessarily_closed() || old_num_rows == 0)
00244 add_pending_row(Linear_Row(r, old_num_columns, row_capacity));
00245 else {
00246
00247
00248 Linear_Row tmp_row(r, old_num_columns, row_capacity);
00249 std::swap(tmp_row[r_size - 1], tmp_row[old_num_columns - 1]);
00250 add_pending_row(tmp_row);
00251 }
00252 else
00253
00254 add_pending_row(r);
00255
00256
00257 assert(num_pending_rows() > 0);
00258
00259
00260 assert(OK(false));
00261 }
00262
00263 void
00264 PPL::Linear_System::add_pending_rows(const Linear_System& y) {
00265 Linear_System& x = *this;
00266 assert(x.row_size == y.row_size);
00267
00268 const dimension_type x_n_rows = x.num_rows();
00269 const dimension_type y_n_rows = y.num_rows();
00270
00271 const bool was_sorted = sorted;
00272 add_zero_rows(y_n_rows, Linear_Row::Flags(row_topology));
00273 sorted = was_sorted;
00274
00275
00276 for (dimension_type i = y_n_rows; i-- > 0; ) {
00277 Row copy(y[i], x.row_size, x.row_capacity);
00278 std::swap(copy, x[x_n_rows+i]);
00279 }
00280
00281
00282 assert(OK(false));
00283 }
00284
00285 void
00286 PPL::Linear_System::add_rows(const Linear_System& y) {
00287 assert(num_pending_rows() == 0);
00288
00289
00290 if (y.has_no_rows())
00291 return;
00292
00293
00294 if (is_sorted()) {
00295 if (!y.is_sorted() || y.num_pending_rows() > 0)
00296 set_sorted(false);
00297 else {
00298
00299 const dimension_type n_rows = num_rows();
00300 if (n_rows > 0)
00301 set_sorted(compare((*this)[n_rows-1], y[0]) <= 0);
00302 }
00303 }
00304
00305
00306 add_pending_rows(y);
00307
00308 unset_pending_rows();
00309
00310
00311
00312 assert(OK(false));
00313 }
00314
00315 void
00316 PPL::Linear_System::sort_rows() {
00317 const dimension_type num_pending = num_pending_rows();
00318
00319 sort_rows(0, first_pending_row());
00320 set_index_first_pending_row(num_rows() - num_pending);
00321 sorted = true;
00322
00323
00324 assert(OK(false));
00325 }
00326
00327 void
00328 PPL::Linear_System::sort_rows(const dimension_type first_row,
00329 const dimension_type last_row) {
00330 assert(first_row <= last_row && last_row <= num_rows());
00331
00332 assert(first_row >= first_pending_row() || last_row <= first_pending_row());
00333
00334
00335 std::vector<Row>::iterator first = rows.begin() + first_row;
00336 std::vector<Row>::iterator last = rows.begin() + last_row;
00337 swapping_sort(first, last, Row_Less_Than());
00338
00339 std::vector<Row>::iterator new_last = swapping_unique(first, last);
00340
00341 rows.erase(new_last, last);
00342
00343
00344 }
00345
00346 void
00347 PPL::Linear_System::add_row(const Linear_Row& r) {
00348
00349
00350 assert(r.check_strong_normalized());
00351 assert(r.size() == row_size);
00352
00353 assert(num_pending_rows() == 0);
00354
00355 const bool was_sorted = is_sorted();
00356
00357 Matrix::add_row(r);
00358
00359
00360
00361 set_index_first_pending_row(num_rows());
00362
00363 if (was_sorted) {
00364 const dimension_type nrows = num_rows();
00365
00366 if (nrows > 1) {
00367
00368
00369
00370 Linear_System& x = *this;
00371 set_sorted(compare(x[nrows-2], x[nrows-1]) <= 0);
00372 }
00373 else
00374
00375 set_sorted(true);
00376 }
00377
00378 assert(num_pending_rows() == 0);
00379
00380
00381 assert(OK(false));
00382 }
00383
00384 void
00385 PPL::Linear_System::add_pending_row(const Linear_Row& r) {
00386
00387
00388 assert(r.check_strong_normalized());
00389 assert(r.size() == row_size);
00390
00391 const dimension_type new_rows_size = rows.size() + 1;
00392 if (rows.capacity() < new_rows_size) {
00393
00394 std::vector<Row> new_rows;
00395 new_rows.reserve(compute_capacity(new_rows_size, max_num_rows()));
00396 new_rows.insert(new_rows.end(), new_rows_size, Row());
00397
00398 Row new_row(r, row_capacity);
00399 dimension_type i = new_rows_size-1;
00400 std::swap(new_rows[i], new_row);
00401
00402 while (i-- > 0)
00403 new_rows[i].swap(rows[i]);
00404
00405 std::swap(rows, new_rows);
00406 }
00407 else {
00408
00409
00410
00411 Row tmp(r, row_capacity);
00412 std::swap(*rows.insert(rows.end(), Row()), tmp);
00413 }
00414
00415
00416 assert(num_pending_rows() > 0);
00417
00418
00419 assert(OK(false));
00420 }
00421
00422 void
00423 PPL::Linear_System::add_pending_row(const Linear_Row::Flags flags) {
00424 const dimension_type new_rows_size = rows.size() + 1;
00425 if (rows.capacity() < new_rows_size) {
00426
00427 std::vector<Row> new_rows;
00428 new_rows.reserve(compute_capacity(new_rows_size, max_num_rows()));
00429 new_rows.insert(new_rows.end(), new_rows_size, Row());
00430
00431 Linear_Row new_row(row_size, row_capacity, flags);
00432 dimension_type i = new_rows_size-1;
00433 std::swap(new_rows[i], new_row);
00434
00435 while (i-- > 0)
00436 new_rows[i].swap(rows[i]);
00437
00438 std::swap(rows, new_rows);
00439 }
00440 else {
00441
00442
00443
00444 Row& new_row = *rows.insert(rows.end(), Row());
00445 static_cast<Linear_Row&>(new_row).construct(row_size, row_capacity, flags);
00446 }
00447
00448
00449 assert(num_pending_rows() > 0);
00450 }
00451
00452 void
00453 PPL::Linear_System::normalize() {
00454 Linear_System& x = *this;
00455 const dimension_type nrows = x.num_rows();
00456
00457 for (dimension_type i = nrows; i-- > 0; )
00458 x[i].normalize();
00459 set_sorted(nrows <= 1);
00460 }
00461
00462 void
00463 PPL::Linear_System::strong_normalize() {
00464 Linear_System& x = *this;
00465 const dimension_type nrows = x.num_rows();
00466
00467 for (dimension_type i = nrows; i-- > 0; )
00468 x[i].strong_normalize();
00469 set_sorted(nrows <= 1);
00470 }
00471
00472 void
00473 PPL::Linear_System::sign_normalize() {
00474 Linear_System& x = *this;
00475 const dimension_type nrows = x.num_rows();
00476
00477 for (dimension_type i = num_rows(); i-- > 0; )
00478 x[i].sign_normalize();
00479 set_sorted(nrows <= 1);
00480 }
00481
00483 bool
00484 PPL::operator==(const Linear_System& x, const Linear_System& y) {
00485 if (x.num_columns() != y.num_columns())
00486 return false;
00487 const dimension_type x_num_rows = x.num_rows();
00488 const dimension_type y_num_rows = y.num_rows();
00489 if (x_num_rows != y_num_rows)
00490 return false;
00491 if (x.first_pending_row() != y.first_pending_row())
00492 return false;
00493
00494
00495
00496 for (dimension_type i = x_num_rows; i-- > 0; )
00497 if (x[i] != y[i])
00498 return false;
00499 return true;
00500 }
00501
00502 void
00503 PPL::Linear_System::sort_and_remove_with_sat(Bit_Matrix& sat) {
00504 Linear_System& sys = *this;
00505
00506 assert(sys.first_pending_row() == sat.num_rows());
00507 if (sys.first_pending_row() <= 1) {
00508 sys.set_sorted(true);
00509 return;
00510 }
00511
00512
00513 With_Bit_Matrix_iterator first(sys.rows.begin(), sat.rows.begin());
00514 With_Bit_Matrix_iterator last = first + sat.num_rows();
00515 swapping_sort(first, last, Row_Less_Than());
00516
00517 With_Bit_Matrix_iterator new_last = swapping_unique(first, last);
00518
00519 const dimension_type num_duplicates = last - new_last;
00520 const dimension_type new_first_pending_row
00521 = sys.first_pending_row() - num_duplicates;
00522
00523 if (sys.num_pending_rows() > 0) {
00524
00525 const dimension_type n_rows = sys.num_rows() - 1;
00526 for (dimension_type i = 0; i < num_duplicates; ++i)
00527 std::swap(sys[new_first_pending_row + i], sys[n_rows - i]);
00528 }
00529
00530 sys.erase_to_end(sys.num_rows() - num_duplicates);
00531 sys.set_index_first_pending_row(new_first_pending_row);
00532
00533 sat.rows_erase_to_end(sat.num_rows() - num_duplicates);
00534 assert(sys.check_sorted());
00535
00536 sys.set_sorted(true);
00537 }
00538
00539 PPL::dimension_type
00540 PPL::Linear_System::gauss(const dimension_type n_lines_or_equalities) {
00541 Linear_System& x = *this;
00542
00543
00544
00545
00546 assert(x.OK(true));
00547 assert(x.num_pending_rows() == 0);
00548 assert(n_lines_or_equalities == x.num_lines_or_equalities());
00549 #ifndef NDEBUG
00550 for (dimension_type i = n_lines_or_equalities; i-- > 0; )
00551 assert(x[i].is_line_or_equality());
00552 #endif
00553
00554 dimension_type rank = 0;
00555
00556 bool changed = false;
00557 for (dimension_type j = x.num_columns(); j-- > 0; )
00558 for (dimension_type i = rank; i < n_lines_or_equalities; ++i) {
00559
00560
00561 if (x[i][j] == 0)
00562 continue;
00563
00564
00565 if (i > rank) {
00566 std::swap(x[i], x[rank]);
00567
00568 changed = true;
00569 }
00570
00571
00572
00573 for (dimension_type k = i + 1; k < n_lines_or_equalities; ++k)
00574 if (x[k][j] != 0) {
00575 x[k].linear_combine(x[rank], j);
00576 changed = true;
00577 }
00578
00579 ++rank;
00580
00581 break;
00582 }
00583 if (changed)
00584 x.set_sorted(false);
00585
00586 assert(x.OK(true));
00587 return rank;
00588 }
00589
00590 void
00591 PPL::Linear_System
00592 ::back_substitute(const dimension_type n_lines_or_equalities) {
00593 Linear_System& x = *this;
00594
00595
00596
00597
00598 assert(x.OK(true));
00599 assert(x.num_columns() >= 1);
00600 assert(x.num_pending_rows() == 0);
00601 assert(n_lines_or_equalities <= x.num_lines_or_equalities());
00602 #ifndef NDEBUG
00603 for (dimension_type i = n_lines_or_equalities; i-- > 0; )
00604 assert(x[i].is_line_or_equality());
00605 #endif
00606
00607 const dimension_type nrows = x.num_rows();
00608 const dimension_type ncols = x.num_columns();
00609
00610 bool still_sorted = x.is_sorted();
00611
00612
00613 std::deque<bool> check_for_sortedness;
00614 if (still_sorted)
00615 check_for_sortedness.insert(check_for_sortedness.end(), nrows, false);
00616
00617 for (dimension_type k = n_lines_or_equalities; k-- > 0; ) {
00618
00619
00620
00621 Linear_Row& x_k = x[k];
00622 dimension_type j = ncols - 1;
00623 while (j != 0 && x_k[j] == 0)
00624 --j;
00625
00626
00627 for (dimension_type i = k; i-- > 0; ) {
00628 Linear_Row& x_i = x[i];
00629 if (x_i[j] != 0) {
00630
00631
00632 x_i.linear_combine(x_k, j);
00633 if (still_sorted) {
00634
00635
00636 if (i > 0)
00637 check_for_sortedness[i-1] = true;
00638 check_for_sortedness[i] = true;
00639 }
00640 }
00641 }
00642
00643
00644
00645
00646
00647
00648 const bool have_to_negate = (x_k[j] < 0);
00649 if (have_to_negate)
00650 for (dimension_type h = ncols; h-- > 0; )
00651 PPL::neg_assign(x_k[h]);
00652
00653
00654
00655
00656 for (dimension_type i = n_lines_or_equalities; i < nrows; ++i) {
00657 Linear_Row& x_i = x[i];
00658 if (x_i[j] != 0) {
00659
00660
00661 x_i.linear_combine(x_k, j);
00662 if (still_sorted) {
00663
00664
00665 if (i > n_lines_or_equalities)
00666 check_for_sortedness[i-1] = true;
00667 check_for_sortedness[i] = true;
00668 }
00669 }
00670 }
00671 if (have_to_negate)
00672
00673 for (dimension_type h = ncols; h-- > 0; )
00674 PPL::neg_assign(x_k[h]);
00675 }
00676
00677
00678 for (dimension_type i = 0; still_sorted && i+1 < nrows; ++i)
00679 if (check_for_sortedness[i])
00680
00681 still_sorted = (compare(x[i], x[i+1]) <= 0);
00682
00683 x.set_sorted(still_sorted);
00684
00685
00686 assert(x.OK(true));
00687 }
00688
00689 void
00690 PPL::Linear_System::simplify() {
00691 Linear_System& x = *this;
00692
00693
00694 assert(x.OK(true));
00695 assert(x.num_pending_rows() == 0);
00696
00697
00698 dimension_type nrows = x.num_rows();
00699 dimension_type n_lines_or_equalities = 0;
00700 for (dimension_type i = 0; i < nrows; ++i)
00701 if (x[i].is_line_or_equality()) {
00702 if (n_lines_or_equalities < i) {
00703 std::swap(x[i], x[n_lines_or_equalities]);
00704
00705 assert(!x.sorted);
00706 }
00707 ++n_lines_or_equalities;
00708 }
00709
00710 const dimension_type rank = x.gauss(n_lines_or_equalities);
00711
00712 if (rank < n_lines_or_equalities) {
00713 const dimension_type
00714 n_rays_or_points_or_inequalities = nrows - n_lines_or_equalities;
00715 const dimension_type
00716 num_swaps = std::min(n_lines_or_equalities - rank,
00717 n_rays_or_points_or_inequalities);
00718 for (dimension_type i = num_swaps; i-- > 0; )
00719 std::swap(x[--nrows], x[rank + i]);
00720 x.erase_to_end(nrows);
00721 x.unset_pending_rows();
00722 if (n_rays_or_points_or_inequalities > num_swaps)
00723 x.set_sorted(false);
00724 n_lines_or_equalities = rank;
00725 }
00726
00727 x.back_substitute(n_lines_or_equalities);
00728
00729 assert(x.OK(true));
00730 }
00731
00732 void
00733 PPL::Linear_System::add_rows_and_columns(const dimension_type n) {
00734 assert(n > 0);
00735 const bool was_sorted = is_sorted();
00736 const dimension_type old_n_rows = num_rows();
00737 const dimension_type old_n_columns = num_columns();
00738 add_zero_rows_and_columns(n, n, Linear_Row::Flags(row_topology));
00739 Linear_System& x = *this;
00740
00741 for (dimension_type i = old_n_rows; i-- > 0; )
00742 std::swap(x[i], x[i + n]);
00743 for (dimension_type i = n, c = old_n_columns; i-- > 0; ) {
00744
00745
00746
00747 Linear_Row& r = x[i];
00748 r[c++] = 1;
00749 r.set_is_line_or_equality();
00750
00751 }
00752
00753
00754 if (old_n_columns == 0) {
00755 x[n-1].set_is_ray_or_point_or_inequality();
00756
00757
00758 set_sorted(true);
00759 }
00760 else if (was_sorted)
00761 set_sorted(compare(x[n-1], x[n]) <= 0);
00762
00763
00764 assert(OK(true));
00765 }
00766
00767 void
00768 PPL::Linear_System::sort_pending_and_remove_duplicates() {
00769 assert(num_pending_rows() > 0);
00770 assert(is_sorted());
00771 Linear_System& x = *this;
00772
00773
00774
00775 const dimension_type first_pending = x.first_pending_row();
00776 x.sort_rows(first_pending, x.num_rows());
00777
00778
00779 dimension_type num_rows = x.num_rows();
00780
00781 dimension_type k1 = 0;
00782 dimension_type k2 = first_pending;
00783 dimension_type num_duplicates = 0;
00784
00785
00786 while (k1 < first_pending && k2 < num_rows) {
00787 const int cmp = compare(x[k1], x[k2]);
00788 if (cmp == 0) {
00789
00790 ++num_duplicates;
00791 --num_rows;
00792
00793 ++k1;
00794
00795 if (k2 < num_rows)
00796 std::swap(x[k2], x[k2 + num_duplicates]);
00797 }
00798 else if (cmp < 0)
00799
00800 ++k1;
00801 else {
00802
00803
00804
00805 ++k2;
00806 if (num_duplicates > 0 && k2 < num_rows)
00807 std::swap(x[k2], x[k2 + num_duplicates]);
00808 }
00809 }
00810
00811
00812 if (num_duplicates > 0) {
00813 if (k2 < num_rows)
00814 for (++k2; k2 < num_rows; ++k2)
00815 std::swap(x[k2], x[k2 + num_duplicates]);
00816 x.erase_to_end(num_rows);
00817 }
00818
00819
00820 assert(OK(false));
00821 }
00822
00823 bool
00824 PPL::Linear_System::check_sorted() const {
00825 const Linear_System& x = *this;
00826 for (dimension_type i = first_pending_row(); i-- > 1; )
00827 if (compare(x[i], x[i-1]) < 0)
00828 return false;
00829 return true;
00830 }
00831
00832 bool
00833 PPL::Linear_System::OK(const bool check_strong_normalized) const {
00834 #ifndef NDEBUG
00835 using std::endl;
00836 using std::cerr;
00837 #endif
00838
00839
00840 if (first_pending_row() > num_rows()) {
00841 #ifndef NDEBUG
00842 cerr << "Linear_System has a negative number of pending rows!"
00843 << endl;
00844 #endif
00845 return false;
00846 }
00847
00848
00849
00850 if (has_no_rows()) {
00851 if (is_necessarily_closed() || num_columns() != 1)
00852 return true;
00853 else {
00854 #ifndef NDEBUG
00855 cerr << "NNC Linear_System has one column" << endl;
00856 #endif
00857 return false;
00858 }
00859 }
00860
00861
00862
00863
00864 const dimension_type min_cols = is_necessarily_closed() ? 1 : 2;
00865 if (num_columns() < min_cols) {
00866 #ifndef NDEBUG
00867 cerr << "Linear_System has fewer columns than the minimum "
00868 << "allowed by its topology:"
00869 << endl
00870 << "num_columns is " << num_columns()
00871 << ", minimum is " << min_cols
00872 << endl;
00873 #endif
00874 return false;
00875 }
00876
00877 const Linear_System& x = *this;
00878 const dimension_type n_rows = num_rows();
00879 for (dimension_type i = 0; i < n_rows; ++i) {
00880 if (!x[i].OK(row_size, row_capacity))
00881 return false;
00882
00883 if (x.topology() != x[i].topology()) {
00884 #ifndef NDEBUG
00885 cerr << "Topology mismatch between the system "
00886 << "and one of its rows!"
00887 << endl;
00888 #endif
00889 return false;
00890 }
00891 }
00892
00893 if (check_strong_normalized) {
00894
00895
00896
00897
00898
00899 Linear_System tmp(x, With_Pending());
00900 tmp.strong_normalize();
00901 if (x != tmp) {
00902 #ifndef NDEBUG
00903 cerr << "Linear_System rows are not strongly normalized!"
00904 << endl;
00905 #endif
00906 return false;
00907 }
00908 }
00909
00910 if (sorted && !check_sorted()) {
00911 #ifndef NDEBUG
00912 cerr << "The system declares itself to be sorted but it is not!"
00913 << endl;
00914 #endif
00915 return false;
00916 }
00917
00918
00919 return true;
00920 }