00001 /* Polyhedron class implementation: minimize() and add_and_minimize(). 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 #include "Linear_Row.defs.hh" 00025 #include "Linear_System.defs.hh" 00026 #include "Saturation_Matrix.defs.hh" 00027 #include "Polyhedron.defs.hh" 00028 #include <stdexcept> 00029 00030 namespace PPL = Parma_Polyhedra_Library; 00031 00068 bool 00069 PPL::Polyhedron::minimize(const bool con_to_gen, 00070 Linear_System& source, 00071 Linear_System& dest, 00072 Saturation_Matrix& sat) { 00073 // Topologies have to agree. 00074 assert(source.topology() == dest.topology()); 00075 // `source' cannot be empty: even if it is an empty constraint system, 00076 // representing the universe polyhedron, homogenization has added 00077 // the positive constraint. It also cannot be an empty generator system, 00078 // since this function is always called starting from a non-empty 00079 // polyhedron. 00080 assert(source.num_rows() > 0); 00081 00082 // Sort the source system, if necessary. 00083 if (!source.is_sorted()) 00084 source.sort_rows(); 00085 00086 // Initialization of the system of generators `dest'. 00087 // The algorithm works incrementally and we haven't seen any 00088 // constraint yet: as a consequence, `dest' should describe 00089 // the universe polyhedron of the appropriate dimension. 00090 // To this end, we initialize it to the identity matrix of dimension 00091 // `source.num_columns()': the rows represent the lines corresponding 00092 // to the canonical basis of the vector space. 00093 00094 // Resizing `dest' to be the appropriate square matrix. 00095 dimension_type dest_num_rows = source.num_columns(); 00096 // Note that before calling `resize_no_copy()' we must update 00097 // `index_first_pending'. 00098 dest.set_index_first_pending_row(dest_num_rows); 00099 dest.resize_no_copy(dest_num_rows, dest_num_rows); 00100 00101 // Initialize `dest' to the identity matrix. 00102 for (dimension_type i = dest_num_rows; i-- > 0; ) { 00103 Linear_Row& dest_i = dest[i]; 00104 for (dimension_type j = dest_num_rows; j-- > 0; ) 00105 dest_i[j] = (i == j) ? 1 : 0; 00106 dest_i.set_is_line_or_equality(); 00107 } 00108 // The identity matrix `dest' is not sorted (see the sorting rules 00109 // in Linear_Row.cc). 00110 dest.set_sorted(false); 00111 00112 // NOTE: the system `dest', as it is now, is not a _legal_ system of 00113 // generators, because in the first row we have a line with a 00114 // non-zero divisor (which should only happen for 00115 // points). However, this is NOT a problem, because `source' 00116 // necessarily contains the positivity constraint (or a 00117 // combination of it with another constraint) which will 00118 // restore things as they should be. 00119 00120 00121 // Building a saturation matrix and initializing it by setting 00122 // all of its elements to zero. This matrix will be modified together 00123 // with `dest' during the conversion. 00124 // NOTE: since we haven't seen any constraint yet, the relevant 00125 // portion of `tmp_sat' is the sub-matrix consisting of 00126 // the first 0 columns: thus the relevant portion correctly 00127 // characterizes the initial saturation information. 00128 Saturation_Matrix tmp_sat(dest_num_rows, source.num_rows()); 00129 00130 // By invoking the function conversion(), we populate `dest' with 00131 // the generators characterizing the polyhedron described by all 00132 // the constraints in `source'. 00133 // The `start' parameter is zero (we haven't seen any constraint yet) 00134 // and the 5th parameter (representing the number of lines in `dest'), 00135 // by construction, is equal to `dest_num_rows'. 00136 const dimension_type num_lines_or_equalities 00137 = conversion(source, 0, dest, tmp_sat, dest_num_rows); 00138 // conversion() may have modified the number of rows in `dest'. 00139 dest_num_rows = dest.num_rows(); 00140 00141 // Checking if the generators in `dest' represent an empty polyhedron: 00142 // the polyhedron is empty if there are no points 00143 // (because rays, lines and closure points need a supporting point). 00144 // Points can be detected by looking at: 00145 // - the divisor, for necessarily closed polyhedra; 00146 // - the epsilon coordinate, for NNC polyhedra. 00147 const dimension_type checking_index 00148 = dest.is_necessarily_closed() 00149 ? 0 00150 : dest.num_columns() - 1; 00151 dimension_type first_point; 00152 for (first_point = num_lines_or_equalities; 00153 first_point < dest_num_rows; 00154 ++first_point) 00155 if (dest[first_point][checking_index] > 0) 00156 break; 00157 00158 if (first_point == dest_num_rows) 00159 if (con_to_gen) 00160 // No point has been found: the polyhedron is empty. 00161 return true; 00162 else 00163 // Here `con_to_gen' is false: `dest' is a system of constraints. 00164 // In this case the condition `first_point == dest_num_rows' 00165 // actually means that all the constraints in `dest' have their 00166 // inhomogeneous term equal to 0. 00167 // This is an ILLEGAL situation, because it implies that 00168 // the constraint system `dest' lacks the positivity constraint 00169 // and no linear combination of the constraints in `dest' 00170 // can reintroduce the positivity constraint. 00171 throw std::runtime_error("PPL internal error"); 00172 else { 00173 // A point has been found: the polyhedron is not empty. 00174 // Now invoking simplify() to remove all the redundant constraints 00175 // from the system `source'. 00176 // Since the saturation matrix `tmp_sat' returned by conversion() 00177 // has rows indexed by generators (the rows of `dest') and columns 00178 // indexed by constraints (the rows of `source'), we have to 00179 // transpose it to obtain the saturation matrix needed by simplify(). 00180 sat.transpose_assign(tmp_sat); 00181 simplify(source, sat); 00182 return false; 00183 } 00184 } 00185 00186 00232 bool 00233 PPL::Polyhedron::add_and_minimize(const bool con_to_gen, 00234 Linear_System& source1, 00235 Linear_System& dest, 00236 Saturation_Matrix& sat, 00237 const Linear_System& source2) { 00238 // `source1' and `source2' cannot be empty. 00239 assert(source1.num_rows() > 0 && source2.num_rows() > 0); 00240 // `source1' and `source2' must have the same number of columns 00241 // to be merged. 00242 assert(source1.num_columns() == source2.num_columns()); 00243 // `source1' and `source2' are fully sorted. 00244 assert(source1.is_sorted() && source1.num_pending_rows() == 0); 00245 assert(source2.is_sorted() && source2.num_pending_rows() == 0); 00246 assert(dest.num_pending_rows() == 0); 00247 00248 const dimension_type old_source1_num_rows = source1.num_rows(); 00249 // `k1' and `k2' run through the rows of `source1' and `source2', resp. 00250 dimension_type k1 = 0; 00251 dimension_type k2 = 0; 00252 dimension_type source2_num_rows = source2.num_rows(); 00253 while (k1 < old_source1_num_rows && k2 < source2_num_rows) { 00254 // Add to `source1' the constraints from `source2', as pending rows. 00255 // We exploit the property that initially both `source1' and `source2' 00256 // are sorted and index `k1' only scans the non-pending rows of `source1', 00257 // so that it is not influenced by the pending rows appended to it. 00258 // This way no duplicate (i.e., trivially redundant) constraint 00259 // is introduced in `source1'. 00260 const int cmp = compare(source1[k1], source2[k2]); 00261 if (cmp == 0) { 00262 // We found the same row: there is no need to add `source2[k2]'. 00263 ++k2; 00264 // By sortedness, since `k1 < old_source1_num_rows', 00265 // we can increment index `k1' too. 00266 ++k1; 00267 } 00268 else if (cmp < 0) 00269 // By sortedness, we can increment `k1'. 00270 ++k1; 00271 else { 00272 // Here `cmp > 0'. 00273 // By sortedness, `source2[k2]' cannot be in `source1'. 00274 // We add it as a pending row of `source1' (sortedness unaffected). 00275 source1.add_pending_row(source2[k2]); 00276 // We can increment `k2'. 00277 ++k2; 00278 } 00279 } 00280 // Have we scanned all the rows in `source2'? 00281 if (k2 < source2_num_rows) 00282 // By sortedness, all the rows in `source2' having indexes 00283 // greater than or equal to `k2' were not in `source1'. 00284 // We add them as pending rows of 'source1' (sortedness not affected). 00285 for ( ; k2 < source2_num_rows; ++k2) 00286 source1.add_pending_row(source2[k2]); 00287 00288 if (source1.num_pending_rows() == 0) 00289 // No row was appended to `source1', because all the constraints 00290 // in `source2' were already in `source1'. 00291 // There is nothing left to do ... 00292 return false; 00293 00294 return add_and_minimize(con_to_gen, source1, dest, sat); 00295 } 00296 00333 bool 00334 PPL::Polyhedron::add_and_minimize(const bool con_to_gen, 00335 Linear_System& source, 00336 Linear_System& dest, 00337 Saturation_Matrix& sat) { 00338 assert(source.num_pending_rows() > 0); 00339 assert(source.num_columns() == dest.num_columns()); 00340 assert(source.is_sorted()); 00341 00342 // First, pad the saturation matrix with new columns (of zeroes) 00343 // to accommodate for the pending rows of `source'. 00344 sat.resize(dest.num_rows(), source.num_rows()); 00345 00346 // Incrementally compute the new system of generators. 00347 // Parameter `start' is set to the index of the first pending constraint. 00348 const dimension_type num_lines_or_equalities 00349 = conversion(source, source.first_pending_row(), 00350 dest, sat, 00351 dest.num_lines_or_equalities()); 00352 00353 // conversion() may have modified the number of rows in `dest'. 00354 const dimension_type dest_num_rows = dest.num_rows(); 00355 00356 // Checking if the generators in `dest' represent an empty polyhedron: 00357 // the polyhedron is empty if there are no points 00358 // (because rays, lines and closure points need a supporting point). 00359 // Points can be detected by looking at: 00360 // - the divisor, for necessarily closed polyhedra; 00361 // - the epsilon coordinate, for NNC polyhedra. 00362 const dimension_type checking_index 00363 = dest.is_necessarily_closed() 00364 ? 0 00365 : dest.num_columns() - 1; 00366 dimension_type first_point; 00367 for (first_point = num_lines_or_equalities; 00368 first_point < dest_num_rows; 00369 ++first_point) 00370 if (dest[first_point][checking_index] > 0) 00371 break; 00372 00373 if (first_point == dest_num_rows) 00374 if (con_to_gen) 00375 // No point has been found: the polyhedron is empty. 00376 return true; 00377 else 00378 // Here `con_to_gen' is false: `dest' is a system of constraints. 00379 // In this case the condition `first_point == dest_num_rows' 00380 // actually means that all the constraints in `dest' have their 00381 // inhomogeneous term equal to 0. 00382 // This is an ILLEGAL situation, because it implies that 00383 // the constraint system `dest' lacks the positivity constraint 00384 // and no linear combination of the constraints in `dest' 00385 // can reintroduce the positivity constraint. 00386 throw std::runtime_error("PPL internal error"); 00387 else { 00388 // A point has been found: the polyhedron is not empty. 00389 // Now invoking `simplify()' to remove all the redundant constraints 00390 // from the system `source'. 00391 // Since the saturation matrix `sat' returned by `conversion()' 00392 // has rows indexed by generators (the rows of `dest') and columns 00393 // indexed by constraints (the rows of `source'), we have to 00394 // transpose it to obtain the saturation matrix needed by `simplify()'. 00395 sat.transpose(); 00396 simplify(source, sat); 00397 // Transposing back. 00398 sat.transpose(); 00399 return false; 00400 } 00401 }