1 /* Polyhedron class implementation: minimize() and add_and_minimize().
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_Polyhedron_minimize_templates_hh
25 #define PPL_Polyhedron_minimize_templates_hh 1
26
27 #include "Bit_Matrix_defs.hh"
28 #include "Polyhedron_defs.hh"
29 #include <stdexcept>
30
31 namespace Parma_Polyhedra_Library {
32
33 /*!
34 \return
35 <CODE>true</CODE> if the polyhedron is empty, <CODE>false</CODE>
36 otherwise.
37
38 \param con_to_gen
39 <CODE>true</CODE> if \p source represents the constraints,
40 <CODE>false</CODE> otherwise;
41
42 \param source
43 The given system, which is not empty;
44
45 \param dest
46 The system to build and minimize;
47
48 \param sat
49 The saturation matrix.
50
51 \p dest is not <CODE>const</CODE> because it will be built (and then
52 modified) during minimize(). Also, \p sat and \p source are
53 not <CODE>const</CODE> because the former will be built during
54 \p dest creation and the latter will maybe be sorted and modified by
55 <CODE>conversion()</CODE> and <CODE>simplify()</CODE>.
56
57 \p sat has the generators on its columns and the constraints on its rows
58 if \p con_to_gen is <CODE>true</CODE>, otherwise it has the generators on
59 its rows and the constraints on its columns.
60
61 Given \p source, this function builds (by means of
62 <CODE>conversion()</CODE>) \p dest and then simplifies (invoking
63 <CODE>simplify()</CODE>) \p source, erasing redundant rows.
64 For the sequel we assume that \p source is the system of constraints
65 and \p dest is the system of generators.
66 This will simplify the description of the function; the dual case is
67 similar.
68 */
69 template <typename Source_Linear_System, typename Dest_Linear_System>
70 bool
minimize(const bool con_to_gen,Source_Linear_System & source,Dest_Linear_System & dest,Bit_Matrix & sat)71 Polyhedron::minimize(const bool con_to_gen,
72 Source_Linear_System& source,
73 Dest_Linear_System& dest,
74 Bit_Matrix& sat) {
75
76 typedef typename Dest_Linear_System::row_type dest_row_type;
77
78 // Topologies have to agree.
79 PPL_ASSERT(source.topology() == dest.topology());
80 // `source' cannot be empty: even if it is an empty constraint system,
81 // representing the universe polyhedron, homogenization has added
82 // the positive constraint. It also cannot be an empty generator system,
83 // since this function is always called starting from a non-empty
84 // polyhedron.
85 PPL_ASSERT(!source.has_no_rows());
86
87 // Sort the source system, if necessary.
88 if (!source.is_sorted()) {
89 source.sort_rows();
90 }
91 // Initialization of the system of generators `dest'.
92 // The algorithm works incrementally and we haven't seen any
93 // constraint yet: as a consequence, `dest' should describe
94 // the universe polyhedron of the appropriate dimension.
95 // To this end, we initialize it to the identity matrix of dimension
96 // `source.num_columns()': the rows represent the lines corresponding
97 // to the canonical basis of the vector space.
98 dimension_type dest_num_rows
99 = source.topology() == NECESSARILY_CLOSED ? source.space_dimension() + 1
100 : source.space_dimension() + 2;
101
102 dest.clear();
103 dest.set_space_dimension(source.space_dimension());
104
105 // Initialize `dest' to the identity matrix.
106 for (dimension_type i = 0; i < dest_num_rows; ++i) {
107 Linear_Expression expr;
108 expr.set_space_dimension(dest_num_rows - 1);
109 if (i == 0) {
110 expr += 1;
111 }
112 else {
113 expr += Variable(i - 1);
114 }
115 dest_row_type dest_i(expr, dest_row_type::LINE_OR_EQUALITY, NECESSARILY_CLOSED);
116 if (dest.topology() == NOT_NECESSARILY_CLOSED) {
117 dest_i.mark_as_not_necessarily_closed();
118 }
119 dest.sys.insert_no_ok(dest_i, Recycle_Input());
120 }
121 // The identity matrix `dest' is not sorted (see the sorting rules
122 // in Constrant.cc and Generator.cc).
123 dest.set_sorted(false);
124
125 // NOTE: the system `dest', as it is now, is not a _legal_ system of
126 // generators, because in the first row we have a line with a
127 // non-zero divisor (which should only happen for
128 // points). However, this is NOT a problem, because `source'
129 // necessarily contains the positivity constraint (or a
130 // combination of it with another constraint) which will
131 // restore things as they should be.
132
133
134 // Building a saturation matrix and initializing it by setting
135 // all of its elements to zero. This matrix will be modified together
136 // with `dest' during the conversion.
137 // NOTE: since we haven't seen any constraint yet, the relevant
138 // portion of `tmp_sat' is the sub-matrix consisting of
139 // the first 0 columns: thus the relevant portion correctly
140 // characterizes the initial saturation information.
141 Bit_Matrix tmp_sat(dest_num_rows, source.num_rows());
142
143 // By invoking the function conversion(), we populate `dest' with
144 // the generators characterizing the polyhedron described by all
145 // the constraints in `source'.
146 // The `start' parameter is zero (we haven't seen any constraint yet)
147 // and the 5th parameter (representing the number of lines in `dest'),
148 // by construction, is equal to `dest_num_rows'.
149 const dimension_type num_lines_or_equalities
150 = conversion(source, 0U, dest, tmp_sat, dest_num_rows);
151 // conversion() may have modified the number of rows in `dest'.
152 dest_num_rows = dest.num_rows();
153
154 #ifndef NDEBUG
155 for (dimension_type i = dest.num_rows(); i-- > 0; ) {
156 PPL_ASSERT(dest[i].OK());
157 }
158 #endif
159
160 // Checking if the generators in `dest' represent an empty polyhedron:
161 // the polyhedron is empty if there are no points
162 // (because rays, lines and closure points need a supporting point).
163 // Points can be detected by looking at:
164 // - the divisor, for necessarily closed polyhedra;
165 // - the epsilon coordinate, for NNC polyhedra.
166 dimension_type first_point;
167 if (dest.is_necessarily_closed()) {
168 for (first_point = num_lines_or_equalities;
169 first_point < dest_num_rows;
170 ++first_point) {
171 if (dest[first_point].expr.inhomogeneous_term() > 0) {
172 break;
173 }
174 }
175 }
176 else {
177 for (first_point = num_lines_or_equalities;
178 first_point < dest_num_rows;
179 ++first_point) {
180 if (dest[first_point].expr.get(Variable(dest.space_dimension())) > 0) {
181 break;
182 }
183 }
184 }
185
186 if (first_point == dest_num_rows) {
187 if (con_to_gen) {
188 // No point has been found: the polyhedron is empty.
189 return true;
190 }
191 else {
192 // Here `con_to_gen' is false: `dest' is a system of constraints.
193 // In this case the condition `first_point == dest_num_rows'
194 // actually means that all the constraints in `dest' have their
195 // inhomogeneous term equal to 0.
196 // This is an ILLEGAL situation, because it implies that
197 // the constraint system `dest' lacks the positivity constraint
198 // and no linear combination of the constraints in `dest'
199 // can reintroduce the positivity constraint.
200 PPL_UNREACHABLE;
201 return false;
202 }
203 }
204 else {
205 // A point has been found: the polyhedron is not empty.
206 // Now invoking simplify() to remove all the redundant constraints
207 // from the system `source'.
208 // Since the saturation matrix `tmp_sat' returned by conversion()
209 // has rows indexed by generators (the rows of `dest') and columns
210 // indexed by constraints (the rows of `source'), we have to
211 // transpose it to obtain the saturation matrix needed by simplify().
212 sat.transpose_assign(tmp_sat);
213 simplify(source, sat);
214 return false;
215 }
216 }
217
218
219 /*!
220 \return
221 <CODE>true</CODE> if the obtained polyhedron is empty,
222 <CODE>false</CODE> otherwise.
223
224 \param con_to_gen
225 <CODE>true</CODE> if \p source1 and \p source2 are system of
226 constraints, <CODE>false</CODE> otherwise;
227
228 \param source1
229 The first element of the given DD pair;
230
231 \param dest
232 The second element of the given DD pair;
233
234 \param sat
235 The saturation matrix that bind \p source1 to \p dest;
236
237 \param source2
238 The new system of generators or constraints.
239
240 It is assumed that \p source1 and \p source2 are sorted and have
241 no pending rows. It is also assumed that \p dest has no pending rows.
242 On entry, the rows of \p sat are indexed by the rows of \p dest
243 and its columns are indexed by the rows of \p source1.
244 On exit, the rows of \p sat are indexed by the rows of \p dest
245 and its columns are indexed by the rows of the system obtained
246 by merging \p source1 and \p source2.
247
248 Let us suppose we want to add some constraints to a given system of
249 constraints \p source1. This method, given a minimized double description
250 pair (\p source1, \p dest) and a system of new constraints \p source2,
251 modifies \p source1 by adding to it the constraints of \p source2 that
252 are not in \p source1. Then, by invoking
253 <CODE>add_and_minimize(bool, Linear_System_Class&, Linear_System_Class&, Bit_Matrix&)</CODE>,
254 processes the added constraints obtaining a new DD pair.
255
256 This method treats also the dual case, i.e., adding new generators to
257 a previous system of generators. In this case \p source1 contains the
258 old generators, \p source2 the new ones and \p dest is the system
259 of constraints in the given minimized DD pair.
260
261 Since \p source2 contains the constraints (or the generators) that
262 will be added to \p source1, it is constant: it will not be modified.
263 */
264 template <typename Source_Linear_System1, typename Source_Linear_System2,
265 typename Dest_Linear_System>
266 bool
add_and_minimize(const bool con_to_gen,Source_Linear_System1 & source1,Dest_Linear_System & dest,Bit_Matrix & sat,const Source_Linear_System2 & source2)267 Polyhedron::add_and_minimize(const bool con_to_gen,
268 Source_Linear_System1& source1,
269 Dest_Linear_System& dest,
270 Bit_Matrix& sat,
271 const Source_Linear_System2& source2) {
272 // `source1' and `source2' cannot be empty.
273 PPL_ASSERT(!source1.has_no_rows() && !source2.has_no_rows());
274 // `source1' and `source2' must have the same number of columns
275 // to be merged.
276 PPL_ASSERT(source1.num_columns() == source2.num_columns());
277 // `source1' and `source2' are fully sorted.
278 PPL_ASSERT(source1.is_sorted() && source1.num_pending_rows() == 0);
279 PPL_ASSERT(source2.is_sorted() && source2.num_pending_rows() == 0);
280 PPL_ASSERT(dest.num_pending_rows() == 0);
281
282 const dimension_type old_source1_num_rows = source1.num_rows();
283 // `k1' and `k2' run through the rows of `source1' and `source2', resp.
284 dimension_type k1 = 0;
285 dimension_type k2 = 0;
286 dimension_type source2_num_rows = source2.num_rows();
287 while (k1 < old_source1_num_rows && k2 < source2_num_rows) {
288 // Add to `source1' the constraints from `source2', as pending rows.
289 // We exploit the property that initially both `source1' and `source2'
290 // are sorted and index `k1' only scans the non-pending rows of `source1',
291 // so that it is not influenced by the pending rows appended to it.
292 // This way no duplicate (i.e., trivially redundant) constraint
293 // is introduced in `source1'.
294 const int cmp = compare(source1[k1], source2[k2]);
295 if (cmp == 0) {
296 // We found the same row: there is no need to add `source2[k2]'.
297 ++k2;
298 // By sortedness, since `k1 < old_source1_num_rows',
299 // we can increment index `k1' too.
300 ++k1;
301 }
302 else if (cmp < 0) {
303 // By sortedness, we can increment `k1'.
304 ++k1;
305 }
306 else {
307 // Here `cmp > 0'.
308 // By sortedness, `source2[k2]' cannot be in `source1'.
309 // We add it as a pending row of `source1' (sortedness unaffected).
310 source1.add_pending_row(source2[k2]);
311 // We can increment `k2'.
312 ++k2;
313 }
314 }
315 // Have we scanned all the rows in `source2'?
316 if (k2 < source2_num_rows) {
317 // By sortedness, all the rows in `source2' having indexes
318 // greater than or equal to `k2' were not in `source1'.
319 // We add them as pending rows of 'source1' (sortedness not affected).
320 for ( ; k2 < source2_num_rows; ++k2) {
321 source1.add_pending_row(source2[k2]);
322 }
323 }
324
325 if (source1.num_pending_rows() == 0) {
326 // No row was appended to `source1', because all the constraints
327 // in `source2' were already in `source1'.
328 // There is nothing left to do ...
329 return false;
330 }
331 return add_and_minimize(con_to_gen, source1, dest, sat);
332 }
333
334 /*!
335 \return
336 <CODE>true</CODE> if the obtained polyhedron is empty,
337 <CODE>false</CODE> otherwise.
338
339 \param con_to_gen
340 <CODE>true</CODE> if \p source is a system of constraints,
341 <CODE>false</CODE> otherwise;
342
343 \param source
344 The first element of the given DD pair. It also contains the pending
345 rows to be processed;
346
347 \param dest
348 The second element of the given DD pair. It cannot have pending rows;
349
350 \param sat
351 The saturation matrix that bind the upper part of \p source to \p dest.
352
353 On entry, the rows of \p sat are indexed by the rows of \p dest
354 and its columns are indexed by the non-pending rows of \p source.
355 On exit, the rows of \p sat are indexed by the rows of \p dest
356 and its columns are indexed by the rows of \p source.
357
358 Let us suppose that \p source is a system of constraints.
359 This method assumes that the non-pending part of \p source and
360 system \p dest form a double description pair in minimal form and
361 will build a new DD pair in minimal form by processing the pending
362 constraints in \p source. To this end, it will call
363 <CODE>conversion()</CODE>) and <CODE>simplify</CODE>.
364
365 This method treats also the dual case, i.e., processing pending
366 generators. In this case \p source contains generators and \p dest
367 is the system of constraints corresponding to the non-pending part
368 of \p source.
369 */
370 template <typename Source_Linear_System, typename Dest_Linear_System>
371 bool
add_and_minimize(const bool con_to_gen,Source_Linear_System & source,Dest_Linear_System & dest,Bit_Matrix & sat)372 Polyhedron::add_and_minimize(const bool con_to_gen,
373 Source_Linear_System& source,
374 Dest_Linear_System& dest,
375 Bit_Matrix& sat) {
376 PPL_ASSERT(source.num_pending_rows() > 0);
377 PPL_ASSERT(source.space_dimension() == dest.space_dimension());
378 PPL_ASSERT(source.is_sorted());
379
380 // First, pad the saturation matrix with new columns (of zeroes)
381 // to accommodate for the pending rows of `source'.
382 sat.resize(dest.num_rows(), source.num_rows());
383
384 // Incrementally compute the new system of generators.
385 // Parameter `start' is set to the index of the first pending constraint.
386 const dimension_type num_lines_or_equalities
387 = conversion(source, source.first_pending_row(),
388 dest, sat,
389 dest.num_lines_or_equalities());
390
391 // conversion() may have modified the number of rows in `dest'.
392 const dimension_type dest_num_rows = dest.num_rows();
393
394 // Checking if the generators in `dest' represent an empty polyhedron:
395 // the polyhedron is empty if there are no points
396 // (because rays, lines and closure points need a supporting point).
397 // Points can be detected by looking at:
398 // - the divisor, for necessarily closed polyhedra;
399 // - the epsilon coordinate, for NNC polyhedra.
400 dimension_type first_point;
401 if (dest.is_necessarily_closed()) {
402 for (first_point = num_lines_or_equalities;
403 first_point < dest_num_rows;
404 ++first_point) {
405 if (dest[first_point].expr.inhomogeneous_term() > 0) {
406 break;
407 }
408 }
409 }
410 else {
411 for (first_point = num_lines_or_equalities;
412 first_point < dest_num_rows;
413 ++first_point) {
414 if (dest[first_point].expr.get(Variable(dest.space_dimension())) > 0) {
415 break;
416 }
417 }
418 }
419
420 if (first_point == dest_num_rows) {
421 if (con_to_gen) {
422 // No point has been found: the polyhedron is empty.
423 return true;
424 }
425 else {
426 // Here `con_to_gen' is false: `dest' is a system of constraints.
427 // In this case the condition `first_point == dest_num_rows'
428 // actually means that all the constraints in `dest' have their
429 // inhomogeneous term equal to 0.
430 // This is an ILLEGAL situation, because it implies that
431 // the constraint system `dest' lacks the positivity constraint
432 // and no linear combination of the constraints in `dest'
433 // can reintroduce the positivity constraint.
434 PPL_UNREACHABLE;
435 return false;
436 }
437 }
438 else {
439 // A point has been found: the polyhedron is not empty.
440 // Now invoking `simplify()' to remove all the redundant constraints
441 // from the system `source'.
442 // Since the saturation matrix `sat' returned by `conversion()'
443 // has rows indexed by generators (the rows of `dest') and columns
444 // indexed by constraints (the rows of `source'), we have to
445 // transpose it to obtain the saturation matrix needed by `simplify()'.
446 sat.transpose();
447 simplify(source, sat);
448 // Transposing back.
449 sat.transpose();
450 return false;
451 }
452 }
453
454 } // namespace Parma_Polyhedra_Library
455
456 #endif // !defined(PPL_Polyhedron_minimize_templates_hh)
457