1 /* BHRZ03_Certificate class implementation (non-inline member 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 #include "ppl-config.h"
25 #include "BHRZ03_Certificate_defs.hh"
26 #include "Polyhedron_defs.hh"
27 #include "assertions.hh"
28 #include <iostream>
29
30 namespace PPL = Parma_Polyhedra_Library;
31
BHRZ03_Certificate(const Polyhedron & ph)32 PPL::BHRZ03_Certificate::BHRZ03_Certificate(const Polyhedron& ph)
33 : affine_dim(0), lin_space_dim(0), num_constraints(0), num_points(0),
34 num_rays_null_coord(ph.space_dimension(), 0) {
35 // TODO: provide a correct and reasonably efficient
36 // implementation for NNC polyhedra.
37
38 // The computation of the certificate requires both the
39 // constraint and the generator systems in minimal form.
40 ph.minimize();
41 // It is assumed that `ph' is not an empty polyhedron.
42 PPL_ASSERT(!ph.marked_empty());
43
44 // The dimension of the polyhedron is obtained by subtracting
45 // the number of equalities from the space dimension.
46 // When counting constraints, for a correct reasoning, we have
47 // to disregard the low-level constraints (i.e., the positivity
48 // constraint and epsilon bounds).
49 const dimension_type space_dim = ph.space_dimension();
50 affine_dim = space_dim;
51 PPL_ASSERT(num_constraints == 0);
52 const Constraint_System& cs = ph.minimized_constraints();
53 for (Constraint_System::const_iterator i = cs.begin(),
54 cs_end = cs.end(); i != cs_end; ++i) {
55 ++num_constraints;
56 if (i->is_equality()) {
57 --affine_dim;
58 }
59 }
60
61 PPL_ASSERT(lin_space_dim == 0);
62 PPL_ASSERT(num_points == 0);
63 const Generator_System& gs = ph.minimized_generators();
64 for (Generator_System::const_iterator i = gs.begin(),
65 gs_end = gs.end(); i != gs_end; ++i) {
66 switch (i->type()) {
67 case Generator::POINT:
68 // Intentionally fall through.
69 case Generator::CLOSURE_POINT:
70 ++num_points;
71 break;
72 case Generator::RAY:
73 // For each i such that 0 <= j < space_dim,
74 // `num_rays_null_coord[j]' will be the number of rays
75 // having exactly `j' coordinates equal to 0.
76 ++num_rays_null_coord[i->expression().num_zeroes(1, space_dim + 1)];
77 break;
78 case Generator::LINE:
79 // Since the generator systems is minimized, the dimension of
80 // the lineality space is equal to the number of lines.
81 ++lin_space_dim;
82 break;
83 }
84 }
85 PPL_ASSERT(OK());
86
87 // TODO: this is an inefficient workaround.
88 // For NNC polyhedra, constraints might be no longer up-to-date
89 // (and hence, neither minimized) due to the strong minimization
90 // process applied to generators when constructing the certificate.
91 // We have to reinforce the (normal) minimization of the constraint
92 // system. The future, lazy implementation of the strong minimization
93 // process will solve this problem.
94 if (!ph.is_necessarily_closed()) {
95 ph.minimize();
96 }
97 }
98
99 int
compare(const BHRZ03_Certificate & y) const100 PPL::BHRZ03_Certificate::compare(const BHRZ03_Certificate& y) const {
101 PPL_ASSERT(OK() && y.OK());
102 if (affine_dim != y.affine_dim) {
103 return (affine_dim > y.affine_dim) ? 1 : -1;
104 }
105 if (lin_space_dim != y.lin_space_dim) {
106 return (lin_space_dim > y.lin_space_dim) ? 1 : -1;
107 }
108 if (num_constraints != y.num_constraints) {
109 return (num_constraints > y.num_constraints) ? 1 : -1;
110 }
111 if (num_points != y.num_points) {
112 return (num_points > y.num_points) ? 1 : -1;
113 }
114 const dimension_type space_dim = num_rays_null_coord.size();
115 PPL_ASSERT(num_rays_null_coord.size() == y.num_rays_null_coord.size());
116 // Note: iterating upwards, because we have to check first
117 // the number of rays having more NON-zero coordinates.
118 for (dimension_type i = 0; i < space_dim; ++i) {
119 if (num_rays_null_coord[i] != y.num_rays_null_coord[i]) {
120 return (num_rays_null_coord[i] > y.num_rays_null_coord[i]) ? 1 : -1;
121 }
122 }
123 // All components are equal.
124 return 0;
125 }
126
127 int
compare(const Polyhedron & ph) const128 PPL::BHRZ03_Certificate::compare(const Polyhedron& ph) const {
129 PPL_ASSERT(ph.space_dimension() == num_rays_null_coord.size());
130
131 // TODO: provide a correct and reasonably efficient
132 // implementation for NNC polyhedra.
133
134 // The computation of the certificate requires both the
135 // constraint and the generator systems in minimal form.
136 ph.minimize();
137 // It is assumed that `ph' is a polyhedron containing the
138 // polyhedron described by `*this': hence, it cannot be empty.
139 PPL_ASSERT(!ph.marked_empty());
140
141 // The dimension of the polyhedron is obtained by subtracting
142 // the number of equalities from the space dimension.
143 // When counting constraints, for a correct reasoning, we have
144 // to disregard the low-level constraints (i.e., the positivity
145 // constraint and epsilon bounds).
146 const dimension_type space_dim = ph.space_dimension();
147 dimension_type ph_affine_dim = space_dim;
148 dimension_type ph_num_constraints = 0;
149 const Constraint_System& cs = ph.minimized_constraints();
150 for (Constraint_System::const_iterator i = cs.begin(),
151 cs_end = cs.end(); i != cs_end; ++i) {
152 ++ph_num_constraints;
153 if (i->is_equality()) {
154 --ph_affine_dim;
155 }
156 }
157 // TODO: this is an inefficient workaround.
158 // For NNC polyhedra, constraints might be no longer up-to-date
159 // (and hence, neither minimized) due to the strong minimization
160 // process applied to generators when constructing the certificate.
161 // We have to reinforce the (normal) minimization of the constraint
162 // system. The future, lazy implementation of the strong minimization
163 // process will solve this problem.
164 if (!ph.is_necessarily_closed()) {
165 ph.minimize();
166 }
167 // If the dimension of `ph' is increasing, the chain is stabilizing.
168 if (ph_affine_dim > affine_dim) {
169 return 1;
170 }
171 // At this point the two polyhedra must have the same dimension.
172 PPL_ASSERT(ph_affine_dim == affine_dim);
173
174 // Speculative optimization: in order to better exploit the incrementality
175 // of the comparison, we do not compute information about rays here,
176 // hoping that the other components will be enough.
177 dimension_type ph_lin_space_dim = 0;
178 dimension_type ph_num_points = 0;
179 const Generator_System& gs = ph.minimized_generators();
180 for (Generator_System::const_iterator i = gs.begin(),
181 gs_end = gs.end(); i != gs_end; ++i) {
182 switch (i->type()) {
183 case Generator::POINT:
184 // Intentionally fall through.
185 case Generator::CLOSURE_POINT:
186 ++ph_num_points;
187 break;
188 case Generator::RAY:
189 break;
190 case Generator::LINE:
191 // Since the generator systems is minimized, the dimension of
192 // the lineality space is equal to the number of lines.
193 ++ph_lin_space_dim;
194 break;
195 }
196 }
197 // TODO: this is an inefficient workaround.
198 // For NNC polyhedra, constraints might be no longer up-to-date
199 // (and hence, neither minimized) due to the strong minimization
200 // process applied to generators when constructing the certificate.
201 // We have to reinforce the (normal) minimization of the constraint
202 // system. The future, lazy implementation of the strong minimization
203 // process will solve this problem.
204 if (!ph.is_necessarily_closed()) {
205 ph.minimize();
206 }
207 // If the dimension of the lineality space is increasing,
208 // then the chain is stabilizing.
209 if (ph_lin_space_dim > lin_space_dim) {
210 return 1;
211 }
212 // At this point the lineality space of the two polyhedra must have
213 // the same dimension.
214 PPL_ASSERT(ph_lin_space_dim == lin_space_dim);
215
216 // If the number of constraints of `ph' is decreasing, then the chain
217 // is stabilizing. If it is increasing, the chain is not stabilizing.
218 // If they are equal, further investigation is needed.
219 if (ph_num_constraints != num_constraints) {
220 return (ph_num_constraints < num_constraints) ? 1 : -1;
221 }
222 // If the number of points of `ph' is decreasing, then the chain
223 // is stabilizing. If it is increasing, the chain is not stabilizing.
224 // If they are equal, further investigation is needed.
225 if (ph_num_points != num_points) {
226 return (ph_num_points < num_points) ? 1 : -1;
227 }
228 // The speculative optimization was not worth:
229 // compute information about rays.
230 std::vector<dimension_type> ph_num_rays_null_coord(ph.space_dim, 0);
231 for (Generator_System::const_iterator i = gs.begin(),
232 gs_end = gs.end(); i != gs_end; ++i) {
233 if (i->is_ray()) {
234 ++ph_num_rays_null_coord[i->expression().num_zeroes(1, space_dim + 1)];
235 }
236 }
237 // Compare (lexicographically) the two vectors:
238 // if ph_num_rays_null_coord < num_rays_null_coord the chain is stabilizing.
239 for (dimension_type i = 0; i < space_dim; ++i) {
240 if (ph_num_rays_null_coord[i] != num_rays_null_coord[i]) {
241 return (ph_num_rays_null_coord[i] < num_rays_null_coord[i]) ? 1 : -1;
242 }
243 }
244 // All components are equal.
245 return 0;
246 }
247
248 bool
OK() const249 PPL::BHRZ03_Certificate::OK() const {
250 #ifndef NDEBUG
251 using std::endl;
252 using std::cerr;
253 #endif
254
255 // The dimension of the vector space.
256 const dimension_type space_dim = num_rays_null_coord.size();
257
258 if (affine_dim > space_dim) {
259 #ifndef NDEBUG
260 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
261 << endl
262 << "the affine dimension is greater than the space dimension!"
263 << endl;
264 #endif
265 return false;
266 }
267
268 if (lin_space_dim > affine_dim) {
269 #ifndef NDEBUG
270 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
271 << endl
272 << "the lineality space dimension is greater than "
273 << "the affine dimension!"
274 << endl;
275 #endif
276 return false;
277 }
278
279 if (num_constraints < space_dim - affine_dim) {
280 #ifndef NDEBUG
281 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
282 << endl
283 << "in a vector space of dimension `n',"
284 << "any polyhedron of affine dimension `k'" << endl
285 << "should have `n-k' non-redundant constraints at least."
286 << endl
287 << "Here space_dim = " << space_dim << ", "
288 << "affine_dim = " << affine_dim << ", "
289 << "but num_constraints = " << num_constraints << "!"
290 << endl;
291 #endif
292 return false;
293 }
294
295 if (num_points == 0) {
296 #ifndef NDEBUG
297 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
298 << endl
299 << "the generator system has no points!"
300 << endl;
301 #endif
302 return false;
303 }
304
305 if (lin_space_dim == space_dim) {
306 // This was a universe polyhedron.
307 if (num_constraints > 0) {
308 #ifndef NDEBUG
309 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
310 << endl
311 << "a universe polyhedron has non-redundant constraints!"
312 << endl;
313 #endif
314 return false;
315 }
316
317 if (num_points != 1) {
318 #ifndef NDEBUG
319 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
320 << endl
321 << "a universe polyhedron has more than one non-redundant point!"
322 << endl;
323 #endif
324 return false;
325 }
326 }
327
328 // All tests passed.
329 return true;
330 }
331