00001 /* Polyhedron class implementation: conversion(). 00002 Copyright (C) 2001-2006 Roberto Bagnara <bagnara@cs.unipr.it> 00003 00004 This file is part of the Parma Polyhedra Library (PPL). 00005 00006 The PPL is free software; you can redistribute it and/or modify it 00007 under the terms of the GNU General Public License as published by the 00008 Free Software Foundation; either version 2 of the License, or (at your 00009 option) any later version. 00010 00011 The PPL is distributed in the hope that it will be useful, but WITHOUT 00012 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 00013 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 00014 for more details. 00015 00016 You should have received a copy of the GNU General Public License 00017 along with this program; if not, write to the Free Software Foundation, 00018 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. 00019 00020 For the most up-to-date information see the Parma Polyhedra Library 00021 site: http://www.cs.unipr.it/ppl/ . */ 00022 00023 #include <config.h> 00024 00025 #include "Linear_Row.defs.hh" 00026 #include "Linear_System.defs.hh" 00027 #include "Saturation_Row.defs.hh" 00028 #include "Saturation_Matrix.defs.hh" 00029 #include "Polyhedron.defs.hh" 00030 #include "Scalar_Products.defs.hh" 00031 #include <cstddef> 00032 00033 namespace PPL = Parma_Polyhedra_Library; 00034 00035 // True if abandon_expensive_computations should be checked often, 00036 // where the meaning of "often" is as stated in the documentation 00037 // of that variable. 00038 #define REACTIVE_ABANDONING 1 00039 00349 PPL::dimension_type 00350 PPL::Polyhedron::conversion(Linear_System& source, 00351 const dimension_type start, 00352 Linear_System& dest, 00353 Saturation_Matrix& sat, 00354 dimension_type num_lines_or_equalities) { 00355 dimension_type source_num_rows = source.num_rows(); 00356 dimension_type dest_num_rows = dest.num_rows(); 00357 const dimension_type source_num_columns = source.num_columns(); 00358 const dimension_type dest_num_columns = dest.num_columns(); 00359 00360 // By construction, the number of columns of `sat' is the same as 00361 // the number of rows of `source'; also, the number of rows of `sat' 00362 // is the same as the number of rows of `dest'. 00363 assert(source_num_rows == sat.num_columns()); 00364 assert(dest_num_rows == sat.num_rows()); 00365 00366 // If `start > 0', then we are converting the pending constraints. 00367 assert(start == 0 || start == source.first_pending_row()); 00368 00369 // During the iteration on the constraints in `source' we may identify 00370 // constraints that are redundant: these have to be removed by swapping 00371 // the rows of `source', taking care not to compromise the sortedness 00372 // of the constraints that still have to be considered. 00373 // To this end, the following counter keeps the number of redundant 00374 // constraints seen so far, to be used as a displacement when swapping rows. 00375 dimension_type source_num_redundant = 0; 00376 00377 TEMP_INTEGER(normalized_sp_i); 00378 TEMP_INTEGER(normalized_sp_o); 00379 00380 // Converting the sub-system of `source' having rows with indexes 00381 // from `start' to the last one (i.e., `source_num_rows' - 1). 00382 for (dimension_type k = start; k < source_num_rows; ) { 00383 00384 // All the `source_num_redundant' redundant constraints identified so far 00385 // have consecutive indices starting from `k'. 00386 if (source_num_redundant > 0) 00387 // Let the next constraint have index `k'. 00388 // There is no need to swap the columns of `sat' (all zeroes). 00389 std::swap(source[k], source[k+source_num_redundant]); 00390 00391 Linear_Row& source_k = source[k]; 00392 00393 // Constraints and generators must have the same dimension, 00394 // otherwise the scalar product below will bomb. 00395 assert(source_num_columns == dest_num_columns); 00396 00397 // `scalar_prod[i]' will contain the scalar product 00398 // of the constraint `source_k' and the generator `dest[i]'. 00399 // This product is 0 iff the generator saturates the constraint. 00400 static std::vector<Coefficient> scalar_prod; 00401 const int needed_space = dest_num_rows - scalar_prod.size(); 00402 if (needed_space > 0) 00403 scalar_prod.insert(scalar_prod.end(), needed_space, Coefficient_zero()); 00404 // `index_non_zero' will indicate the first generator in `dest' 00405 // that does not saturate the constraint `source_k'. 00406 dimension_type index_non_zero = 0; 00407 for ( ; index_non_zero < dest_num_rows; ++index_non_zero) { 00408 Scalar_Products::assign(scalar_prod[index_non_zero], 00409 source_k, 00410 dest[index_non_zero]); 00411 if (scalar_prod[index_non_zero] != 0) 00412 // The generator does not saturate the constraint. 00413 break; 00414 #if REACTIVE_ABANDONING 00415 // Check if the client has requested abandoning all exponential 00416 // computations. If so, the exception specified by the client 00417 // is thrown now. 00418 maybe_abandon(); 00419 #endif 00420 } 00421 for (dimension_type i = index_non_zero + 1; i < dest_num_rows; ++i) { 00422 Scalar_Products::assign(scalar_prod[i], source_k, dest[i]); 00423 #if REACTIVE_ABANDONING 00424 maybe_abandon(); 00425 #endif 00426 } 00427 00428 // We first treat the case when `index_non_zero' is less than 00429 // `num_lines_or_equalities', i.e., when the generator that 00430 // does not saturate the constraint `source_k' is a line. 00431 // The other case (described later) is when all the lines 00432 // in `dest' (i.e., all the rows having indexes less than 00433 // `num_lines_or_equalities') do saturate the constraint. 00434 00435 if (index_non_zero < num_lines_or_equalities) { 00436 // Since the generator `dest[index_non_zero]' does not saturate 00437 // the constraint `source_k', it can no longer be a line 00438 // (see saturation rule in Section \ref prelims). 00439 // Therefore, we first transform it to a ray. 00440 dest[index_non_zero].set_is_ray_or_point_or_inequality(); 00441 // Of the two possible choices, we select the ray satisfying 00442 // the constraint (namely, the ray whose scalar product 00443 // with the constraint gives a positive result). 00444 if (scalar_prod[index_non_zero] < 0) { 00445 // The ray `dest[index_non_zero]' lies on the wrong half-space: 00446 // we change it to have the opposite direction. 00447 neg_assign(scalar_prod[index_non_zero]); 00448 for (dimension_type j = dest_num_columns; j-- > 0; ) 00449 neg_assign(dest[index_non_zero][j]); 00450 } 00451 // Having changed a line to a ray, we set `dest' to be a 00452 // non-sorted system, we decrement the number of lines of `dest' and, 00453 // if necessary, we move the new ray below all the remaining lines. 00454 dest.set_sorted(false); 00455 --num_lines_or_equalities; 00456 if (index_non_zero != num_lines_or_equalities) { 00457 std::swap(dest[index_non_zero], 00458 dest[num_lines_or_equalities]); 00459 std::swap(scalar_prod[index_non_zero], 00460 scalar_prod[num_lines_or_equalities]); 00461 } 00462 Linear_Row& dest_nle = dest[num_lines_or_equalities]; 00463 00464 // Computing the new lineality space. 00465 // Since each line must lie on the hyper-plane corresponding to 00466 // the constraint `source_k', the scalar product between 00467 // the line and the constraint must be 0. 00468 // This property already holds for the lines having indexes 00469 // between 0 and `index_non_zero' - 1. 00470 // We have to consider the remaining lines, having indexes 00471 // between `index_non_zero' and `num_lines_or_equalities' - 1. 00472 // Each line that does not saturate the constraint has to be 00473 // linearly combined with generator `dest_nle' so that the 00474 // resulting new line saturates the constraint. 00475 // Note that, by Observation 1 above, the resulting new line 00476 // will still saturate all the constraints that were saturated by 00477 // the old line. 00478 00479 Coefficient& scalar_prod_nle = scalar_prod[num_lines_or_equalities]; 00480 for (dimension_type 00481 i = index_non_zero; i < num_lines_or_equalities; ++i) { 00482 if (scalar_prod[i] != 0) { 00483 // The following fragment optimizes the computation of 00484 // 00485 // Coefficient scale = scalar_prod[i]; 00486 // scale.gcd_assign(scalar_prod_nle); 00487 // Coefficient normalized_sp_i = scalar_prod[i] / scale; 00488 // Coefficient normalized_sp_n = scalar_prod_nle / scale; 00489 // for (dimension_type c = dest_num_columns; c-- > 0; ) { 00490 // dest[i][c] *= normalized_sp_n; 00491 // dest[i][c] -= normalized_sp_i * dest_nle[c]; 00492 // } 00493 normalize2(scalar_prod[i], 00494 scalar_prod_nle, 00495 normalized_sp_i, 00496 normalized_sp_o); 00497 Linear_Row& dest_i = dest[i]; 00498 for (dimension_type c = dest_num_columns; c-- > 0; ) { 00499 Coefficient& dest_i_c = dest_i[c]; 00500 dest_i_c *= normalized_sp_o; 00501 sub_mul_assign(dest_i_c, normalized_sp_i, dest_nle[c]); 00502 } 00503 dest_i.strong_normalize(); 00504 scalar_prod[i] = 0; 00505 // `dest' has already been set as non-sorted. 00506 } 00507 } 00508 00509 // Computing the new pointed cone. 00510 // Similarly to what we have done during the computation of 00511 // the lineality space, we consider all the remaining rays 00512 // (having indexes strictly greater than `num_lines_or_equalities') 00513 // that do not saturate the constraint `source_k'. These rays 00514 // are positively combined with the ray `dest_nle' so that the 00515 // resulting new rays saturate the constraint. 00516 for (dimension_type 00517 i = num_lines_or_equalities + 1; i < dest_num_rows; ++i) { 00518 if (scalar_prod[i] != 0) { 00519 // The following fragment optimizes the computation of 00520 // 00521 // Coefficient scale = scalar_prod[i]; 00522 // scale.gcd_assign(scalar_prod_nle); 00523 // Coefficient normalized_sp_i = scalar_prod[i] / scale; 00524 // Coefficient normalized_sp_n = scalar_prod_nle / scale; 00525 // for (dimension_type c = dest_num_columns; c-- > 0; ) { 00526 // dest[i][c] *= normalized_sp_n; 00527 // dest[i][c] -= normalized_sp_i * dest_nle[c]; 00528 // } 00529 normalize2(scalar_prod[i], 00530 scalar_prod_nle, 00531 normalized_sp_i, 00532 normalized_sp_o); 00533 Linear_Row& dest_i = dest[i]; 00534 for (dimension_type c = dest_num_columns; c-- > 0; ) { 00535 Coefficient& dest_i_c = dest_i[c]; 00536 dest_i_c *= normalized_sp_o; 00537 sub_mul_assign(dest_i_c, normalized_sp_i, dest_nle[c]); 00538 } 00539 dest_i.strong_normalize(); 00540 scalar_prod[i] = 0; 00541 // `dest' has already been set as non-sorted. 00542 } 00543 #if REACTIVE_ABANDONING 00544 maybe_abandon(); 00545 #endif 00546 } 00547 // Since the `scalar_prod_nle' is positive (by construction), it 00548 // does not saturate the constraint `source_k'. Therefore, if 00549 // the constraint is an inequality, we set to 1 the 00550 // corresponding element of `sat' ... 00551 Saturation_Row& sat_nle = sat[num_lines_or_equalities]; 00552 if (source_k.is_ray_or_point_or_inequality()) 00553 sat_nle.set(k); 00554 // ... otherwise, the constraint is an equality which is 00555 // violated by the generator `dest_nle': the generator has to be 00556 // removed from `dest'. 00557 else { 00558 --dest_num_rows; 00559 std::swap(dest_nle, dest[dest_num_rows]); 00560 std::swap(scalar_prod_nle, scalar_prod[dest_num_rows]); 00561 std::swap(sat_nle, sat[dest_num_rows]); 00562 // `dest' has already been set as non-sorted. 00563 } 00564 // We continue with the next constraint. 00565 ++k; 00566 } 00567 // Here we have `index_non_zero' >= `num_lines_or_equalities', 00568 // so that all the lines in `dest' saturate the constraint `source_k'. 00569 else { 00570 // First, we reorder the generators in `dest' as follows: 00571 // -# all the lines should have indexes between 0 and 00572 // `num_lines_or_equalities' - 1 (this already holds); 00573 // -# all the rays that saturate the constraint should have 00574 // indexes between `num_lines_or_equalities' and 00575 // `lines_or_equal_bound' - 1; these rays form the set Q=. 00576 // -# all the rays that have a positive scalar product with the 00577 // constraint should have indexes between `lines_or_equal_bound' 00578 // and `sup_bound' - 1; these rays form the set Q+. 00579 // -# all the rays that have a negative scalar product with the 00580 // constraint should have indexes between `sup_bound' and 00581 // `dest_num_rows' - 1; these rays form the set Q-. 00582 dimension_type lines_or_equal_bound = num_lines_or_equalities; 00583 dimension_type inf_bound = dest_num_rows; 00584 // While we find saturating generators, we simply increment 00585 // `lines_or_equal_bound'. 00586 while (inf_bound > lines_or_equal_bound 00587 && scalar_prod[lines_or_equal_bound] == 0) 00588 ++lines_or_equal_bound; 00589 dimension_type sup_bound = lines_or_equal_bound; 00590 while (inf_bound > sup_bound) { 00591 const int sp_sign = sgn(scalar_prod[sup_bound]); 00592 if (sp_sign == 0) { 00593 // This generator has to be moved in Q=. 00594 std::swap(dest[sup_bound], dest[lines_or_equal_bound]); 00595 std::swap(scalar_prod[sup_bound], scalar_prod[lines_or_equal_bound]); 00596 std::swap(sat[sup_bound], sat[lines_or_equal_bound]); 00597 ++lines_or_equal_bound; 00598 ++sup_bound; 00599 dest.set_sorted(false); 00600 } 00601 else if (sp_sign < 0) { 00602 // This generator has to be moved in Q-. 00603 --inf_bound; 00604 std::swap(dest[sup_bound], dest[inf_bound]); 00605 std::swap(scalar_prod[sup_bound], scalar_prod[inf_bound]); 00606 std::swap(sat[sup_bound], sat[inf_bound]); 00607 dest.set_sorted(false); 00608 } 00609 else 00610 // sp_sign > 0: this generator has to be moved in Q+. 00611 ++sup_bound; 00612 } 00613 00614 if (sup_bound == dest_num_rows) { 00615 // Here the set Q- is empty. 00616 // If the constraint is an inequality, then all the generators 00617 // in Q= and Q+ satisfy the constraint. The constraint is redundant 00618 // and it can be safely removed from the constraint system. 00619 // This is why the `source' parameter is not declared `const'. 00620 if (source_k.is_ray_or_point_or_inequality()) { 00621 ++source_num_redundant; 00622 --source_num_rows; 00623 // NOTE: we continue with the next cycle of the loop 00624 // without incrementing the index `k', because: 00625 // -# either `k == source_num_rows', and we will exit the loop; 00626 // -# or, having increased `source_num_redundant', we will swap 00627 // in position `k' a constraint that still has to be examined. 00628 } 00629 else { 00630 // The constraint is an equality, so that all the generators 00631 // in Q+ violate it. Since the set Q- is empty, we can simply 00632 // remove from `dest' all the generators of Q+. 00633 dest_num_rows = lines_or_equal_bound; 00634 // We continue with the next constraint. 00635 ++k; 00636 } 00637 } 00638 else { 00639 // The set Q- is not empty, i.e., at least one generator 00640 // violates the constraint `source_k'. 00641 // We have to further distinguish two cases: 00642 if (sup_bound == num_lines_or_equalities) 00643 // The set Q+ is empty, so that all generators that satisfy 00644 // the constraint also saturate it. 00645 // We can simply remove from `dest' all the generators in Q-. 00646 dest_num_rows = sup_bound; 00647 else { 00648 // The sets Q+ and Q- are both non-empty. 00649 // The generators of the new pointed cone are all those satisfying 00650 // the constraint `source_k' plus a set of new rays enjoying 00651 // the following properties: 00652 // -# they lie on the hyper-plane represented by the constraint 00653 // -# they are obtained as a positive combination of two 00654 // adjacent rays, the first taken from Q+ and the second 00655 // taken from Q-. 00656 00657 // The adjacency property is necessary to have an irredundant 00658 // set of new rays (see proposition 2). 00659 const dimension_type bound = dest_num_rows; 00660 00661 // In the following loop, 00662 // `i' runs through the generators in the set Q+ and 00663 // `j' runs through the generators in the set Q-. 00664 for (dimension_type i = lines_or_equal_bound; i < sup_bound; ++i) { 00665 for(dimension_type j = sup_bound; j < bound; ++j) { 00666 // Checking if generators `dest[i]' and `dest[j]' are adjacent. 00667 // If there exist another generator that saturates 00668 // all the constraints saturated by both `dest[i]' and 00669 // `dest[j]', then they are NOT adjacent. 00670 Saturation_Row new_satrow; 00671 assert(sat[i].last() == ULONG_MAX || sat[i].last() < k); 00672 assert(sat[j].last() == ULONG_MAX || sat[j].last() < k); 00673 // Being the union of `sat[i]' and `sat[j]', 00674 // `new_satrow' corresponds to a ray that saturates all the 00675 // constraints saturated by both `dest[i]' and `dest[j]'. 00676 set_union(sat[i], sat[j], new_satrow); 00677 00678 // Computing the number of common saturators. 00679 // NOTE: this number has to be less than `k' because 00680 // we are treating the `k'-th constraint. 00681 const dimension_type 00682 num_common_satur = k - new_satrow.count_ones(); 00683 00684 // Even before actually creating the new ray as a 00685 // positive combination of `dest[i]' and `dest[j]', 00686 // we exploit saturation information to check if 00687 // it can be an extremal ray. To this end, we refer 00688 // to the definition of a minimal proper face 00689 // (see comments in Polyhedron.defs.hh): 00690 // an extremal ray saturates at least `n' - `t' - 1 00691 // constraints, where `n' is the dimension of the space 00692 // and `t' is the dimension of the lineality space. 00693 // Since `n == source_num_columns - 1' and 00694 // `t == num_lines_or_equalities', we obtain that 00695 // an extremal ray saturates at least 00696 // `source_num_columns - num_lines_or_equalities - 2' 00697 // constraints. 00698 if (num_common_satur 00699 >= source_num_columns - num_lines_or_equalities - 2) { 00700 // The minimal proper face rule is satisfied. 00701 // Now we actually check for redundancy by computing 00702 // adjacency information. 00703 bool redundant = false; 00704 for (dimension_type 00705 l = num_lines_or_equalities; l < bound; ++l) 00706 if (l != i && l != j 00707 && subset_or_equal(sat[l], new_satrow)) { 00708 // Found another generator saturating all the 00709 // constraints saturated by both `dest[i]' and `dest[j]'. 00710 redundant = true; 00711 break; 00712 } 00713 if (!redundant) { 00714 // Adding the new ray to `dest' and the corresponding 00715 // saturation row to `sat'. 00716 if (dest_num_rows == dest.num_rows()) { 00717 // Make room for one more row. 00718 dest.add_pending_row(Linear_Row::Flags(dest.topology(), 00719 Linear_Row::RAY_OR_POINT_OR_INEQUALITY)); 00720 sat.add_row(new_satrow); 00721 } 00722 else 00723 sat[dest_num_rows] = new_satrow; 00724 Linear_Row& new_row = dest[dest_num_rows]; 00725 // The following fragment optimizes the computation of 00726 // 00727 // Coefficient scale = scalar_prod[i]; 00728 // scale.gcd_assign(scalar_prod[j]); 00729 // Coefficient normalized_sp_i = scalar_prod[i] / scale; 00730 // Coefficient normalized_sp_j = scalar_prod[j] / scale; 00731 // for (dimension_type c = dest_num_columns; c-- > 0; ) { 00732 // new_row[c] = normalized_sp_i * dest[j][c]; 00733 // new_row[c] -= normalized_sp_j * dest[i][c]; 00734 // } 00735 normalize2(scalar_prod[i], 00736 scalar_prod[j], 00737 normalized_sp_i, 00738 normalized_sp_o); 00739 for (dimension_type c = dest_num_columns; c-- > 0; ) { 00740 Coefficient& new_row_c = new_row[c]; 00741 new_row_c = normalized_sp_i * dest[j][c]; 00742 sub_mul_assign(new_row_c, normalized_sp_o, dest[i][c]); 00743 } 00744 new_row.strong_normalize(); 00745 // Since we added a new generator to `dest', 00746 // we also add a new element to `scalar_prod'; 00747 // by construction, the new ray lies on the hyper-plane 00748 // represented by the constraint `source_k'. 00749 // Thus, the added scalar product is 0. 00750 assert(scalar_prod.size() >= dest_num_rows); 00751 if (scalar_prod.size() <= dest_num_rows) 00752 scalar_prod.push_back(Coefficient_zero()); 00753 else 00754 scalar_prod[dest_num_rows] = Coefficient_zero(); 00755 // Increment the number of generators. 00756 ++dest_num_rows; 00757 } 00758 } 00759 } 00760 #if REACTIVE_ABANDONING 00761 maybe_abandon(); 00762 #endif 00763 } 00764 // Now we substitute the rays in Q- (i.e., the rays violating 00765 // the constraint) with the newly added rays. 00766 dimension_type j; 00767 if (source_k.is_ray_or_point_or_inequality()) { 00768 // The constraint is an inequality: 00769 // the violating generators are those in Q-. 00770 j = sup_bound; 00771 // For all the generators in Q+, set to 1 the corresponding 00772 // entry for the constraint `source_k' in the saturation matrix. 00773 for (dimension_type l = lines_or_equal_bound; l < sup_bound; ++l) 00774 sat[l].set(k); 00775 } 00776 else 00777 // The constraint is an equality: 00778 // the violating generators are those in the union of Q+ and Q-. 00779 j = lines_or_equal_bound; 00780 00781 // Swapping the newly added rays 00782 // (index `i' running through `dest_num_rows - 1' down-to `bound') 00783 // with the generators violating the constraint 00784 // (index `j' running through `j' up-to `bound - 1'). 00785 dimension_type i = dest_num_rows; 00786 while (j < bound && i > bound) { 00787 --i; 00788 std::swap(dest[i], dest[j]); 00789 std::swap(scalar_prod[i], scalar_prod[j]); 00790 std::swap(sat[i], sat[j]); 00791 ++j; 00792 dest.set_sorted(false); 00793 } 00794 // Setting the number of generators in `dest': 00795 // - if the number of generators violating the constraint 00796 // is less than or equal to the number of the newly added 00797 // generators, we assign `i' to `dest_num_rows' because 00798 // all generators above this index are significant; 00799 // - otherwise, we assign `j' to `dest_num_rows' because 00800 // all generators below index `j-1' violates the constraint. 00801 dest_num_rows = (j == bound) ? i : j; 00802 } 00803 // We continue with the next constraint. 00804 ++k; 00805 } 00806 } 00807 #if !REACTIVE_ABANDONING 00808 // Check if the client has requested abandoning all exponential 00809 // computations. If so, the exception specified by the client 00810 // is thrown now. 00811 maybe_abandon(); 00812 #endif 00813 } 00814 00815 // We may have identified some redundant constraints in `source', 00816 // which have been swapped at the end of the system. 00817 if (source_num_redundant > 0) { 00818 assert(source_num_redundant == source.num_rows() - source_num_rows); 00819 source.erase_to_end(source_num_rows); 00820 sat.columns_erase_to_end(source_num_rows); 00821 } 00822 // If `start == 0', then `source' was sorted and remained so. 00823 // If otherwise `start > 0', then the two sub-system made by the 00824 // non-pending rows and the pending rows, respectively, were both sorted. 00825 // Thus, the overall system is sorted if and only if either 00826 // `start == source_num_rows' (i.e., the second sub-system is empty) 00827 // or the row ordering holds for the two rows at the boundary between 00828 // the two sub-systems. 00829 if (start > 0 && start < source_num_rows) 00830 source.set_sorted(compare(source[start - 1], source[start]) <= 0); 00831 // There are no longer pending constraints in `source'. 00832 source.unset_pending_rows(); 00833 00834 // We may have identified some redundant rays in `dest', 00835 // which have been swapped at the end of the system. 00836 if (dest_num_rows < dest.num_rows()) { 00837 dest.erase_to_end(dest_num_rows); 00838 // Be careful: we might have erased some of the non-pending rows. 00839 if (dest.first_pending_row() > dest_num_rows) 00840 dest.unset_pending_rows(); 00841 sat.rows_erase_to_end(dest_num_rows); 00842 } 00843 if (dest.is_sorted()) 00844 // If the non-pending generators in `dest' are still declared to be 00845 // sorted, then we have to also check for the sortedness of the 00846 // pending generators. 00847 for (dimension_type i = dest.first_pending_row(); i < dest_num_rows; ++i) 00848 if (compare(dest[i - 1], dest[i]) > 0) { 00849 dest.set_sorted(false); 00850 break; 00851 } 00852 // There are no pending generators in `dest'. 00853 dest.unset_pending_rows(); 00854 00855 return num_lines_or_equalities; 00856 }