00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024 #include <ppl-config.h>
00025
00026 #include "BHRZ03_Certificate.defs.hh"
00027
00028 #include "Polyhedron.defs.hh"
00029 #include <cassert>
00030 #include <iostream>
00031
00032 namespace PPL = Parma_Polyhedra_Library;
00033
00034 PPL::BHRZ03_Certificate::BHRZ03_Certificate(const Polyhedron& ph)
00035 : affine_dim(0), lin_space_dim(0), num_constraints(0), num_points(0),
00036 num_rays_null_coord(ph.space_dimension(), 0) {
00037
00038
00039
00040
00041
00042 ph.minimize();
00043
00044 assert(!ph.marked_empty());
00045
00046
00047
00048
00049
00050
00051 const dimension_type space_dim = ph.space_dimension();
00052 affine_dim = space_dim;
00053 assert(num_constraints == 0);
00054 const Constraint_System& cs = ph.minimized_constraints();
00055 for (Constraint_System::const_iterator i = cs.begin(),
00056 cs_end = cs.end(); i != cs_end; ++i) {
00057 ++num_constraints;
00058 if (i->is_equality())
00059 --affine_dim;
00060 }
00061
00062 assert(lin_space_dim == 0);
00063 assert(num_points == 0);
00064 const Generator_System& gs = ph.minimized_generators();
00065 for (Generator_System::const_iterator i = gs.begin(),
00066 gs_end = gs.end(); i != gs_end; ++i)
00067 switch (i->type()) {
00068 case Generator::POINT:
00069
00070 case Generator::CLOSURE_POINT:
00071 ++num_points;
00072 break;
00073 case Generator::RAY:
00074
00075
00076
00077 {
00078 const Generator& r = *i;
00079 dimension_type num_zeroes = 0;
00080 for (dimension_type j = space_dim; j-- > 0; )
00081 if (r.coefficient(Variable(j)) == 0)
00082 ++num_zeroes;
00083 ++num_rays_null_coord[num_zeroes];
00084 }
00085 break;
00086 case Generator::LINE:
00087
00088
00089 ++lin_space_dim;
00090 break;
00091 }
00092 assert(OK());
00093
00094
00095
00096
00097
00098
00099
00100
00101 if (!ph.is_necessarily_closed())
00102 ph.minimize();
00103 }
00104
00105 int
00106 PPL::BHRZ03_Certificate::compare(const BHRZ03_Certificate& y) const {
00107 assert(OK() && y.OK());
00108 if (affine_dim != y.affine_dim)
00109 return affine_dim > y.affine_dim ? 1 : -1;
00110 if (lin_space_dim != y.lin_space_dim)
00111 return lin_space_dim > y.lin_space_dim ? 1 : -1;
00112 if (num_constraints != y.num_constraints)
00113 return num_constraints > y.num_constraints ? 1 : -1;
00114 if (num_points != y.num_points)
00115 return num_points > y.num_points ? 1 : -1;
00116
00117 const dimension_type space_dim = num_rays_null_coord.size();
00118 assert(num_rays_null_coord.size() == y.num_rays_null_coord.size());
00119
00120
00121 for (dimension_type i = 0; i < space_dim; i++)
00122 if (num_rays_null_coord[i] != y.num_rays_null_coord[i])
00123 return num_rays_null_coord[i] > y.num_rays_null_coord[i] ? 1 : -1;
00124
00125 return 0;
00126 }
00127
00128 int
00129 PPL::BHRZ03_Certificate::compare(const Polyhedron& ph) const {
00130 assert(ph.space_dimension() == num_rays_null_coord.size());
00131
00132
00133
00134
00135
00136
00137 ph.minimize();
00138
00139
00140 assert(!ph.marked_empty());
00141
00142
00143
00144
00145
00146
00147 const dimension_type space_dim = ph.space_dimension();
00148 dimension_type ph_affine_dim = space_dim;
00149 dimension_type ph_num_constraints = 0;
00150 const Constraint_System& cs = ph.minimized_constraints();
00151 for (Constraint_System::const_iterator i = cs.begin(),
00152 cs_end = cs.end(); i != cs_end; ++i) {
00153 ++ph_num_constraints;
00154 if (i->is_equality())
00155 --ph_affine_dim;
00156 }
00157
00158
00159
00160
00161
00162
00163
00164 if (!ph.is_necessarily_closed())
00165 ph.minimize();
00166
00167
00168 if (ph_affine_dim > affine_dim)
00169 return 1;
00170
00171
00172 assert(ph_affine_dim == affine_dim);
00173
00174
00175
00176
00177 dimension_type ph_lin_space_dim = 0;
00178 dimension_type ph_num_points = 0;
00179 const Generator_System& gs = ph.minimized_generators();
00180 for (Generator_System::const_iterator i = gs.begin(),
00181 gs_end = gs.end(); i != gs_end; ++i)
00182 switch (i->type()) {
00183 case Generator::POINT:
00184
00185 case Generator::CLOSURE_POINT:
00186 ++ph_num_points;
00187 break;
00188 case Generator::RAY:
00189 break;
00190 case Generator::LINE:
00191
00192
00193 ++ph_lin_space_dim;
00194 break;
00195 }
00196
00197
00198
00199
00200
00201
00202
00203 if (!ph.is_necessarily_closed())
00204 ph.minimize();
00205
00206
00207
00208 if (ph_lin_space_dim > lin_space_dim)
00209 return 1;
00210
00211
00212
00213 assert(ph_lin_space_dim == lin_space_dim);
00214
00215
00216
00217
00218 if (ph_num_constraints != num_constraints)
00219 return ph_num_constraints < num_constraints ? 1 : -1;
00220
00221
00222
00223
00224 if (ph_num_points != num_points)
00225 return ph_num_points < num_points ? 1 : -1;
00226
00227
00228
00229 std::vector<dimension_type> ph_num_rays_null_coord(ph.space_dim, 0);
00230 for (Generator_System::const_iterator i = gs.begin(),
00231 gs_end = gs.end(); i != gs_end; ++i)
00232 if (i->is_ray()) {
00233 const Generator& r = *i;
00234 dimension_type num_zeroes = 0;
00235 for (dimension_type j = space_dim; j-- > 0; )
00236 if (r.coefficient(Variable(j)) == 0)
00237 ++num_zeroes;
00238 ++ph_num_rays_null_coord[num_zeroes];
00239 }
00240
00241
00242 for (dimension_type i = 0; i < space_dim; i++)
00243 if (ph_num_rays_null_coord[i] != num_rays_null_coord[i])
00244 return ph_num_rays_null_coord[i] < num_rays_null_coord[i] ? 1 : -1;
00245
00246
00247 return 0;
00248 }
00249
00250 bool
00251 PPL::BHRZ03_Certificate::OK() const {
00252 #ifndef NDEBUG
00253 using std::endl;
00254 using std::cerr;
00255 #endif
00256
00257
00258 const dimension_type space_dim = num_rays_null_coord.size();
00259
00260 if (affine_dim > space_dim) {
00261 #ifndef NDEBUG
00262 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
00263 << endl
00264 << "the affine dimension is greater than the space dimension!"
00265 << endl;
00266 #endif
00267 return false;
00268 }
00269
00270 if (lin_space_dim > affine_dim) {
00271 #ifndef NDEBUG
00272 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
00273 << endl
00274 << "the lineality space dimension is greater than "
00275 << "the affine dimension!"
00276 << endl;
00277 #endif
00278 return false;
00279 }
00280
00281 if (num_constraints < space_dim - affine_dim) {
00282 #ifndef NDEBUG
00283 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
00284 << endl
00285 << "in a vector space of dimension `n',"
00286 << "any polyhedron of affine dimension `k'" << endl
00287 << "should have `n-k' non-redundant constraints at least."
00288 << endl
00289 << "Here space_dim = " << space_dim << ", "
00290 << "affine_dim = " << affine_dim << ", "
00291 << "but num_constraints = " << num_constraints << "!"
00292 << endl;
00293 #endif
00294 return false;
00295 }
00296
00297 if (num_points == 0) {
00298 #ifndef NDEBUG
00299 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
00300 << endl
00301 << "the generator system has no points!"
00302 << endl;
00303 #endif
00304 return false;
00305 }
00306
00307 if (lin_space_dim == space_dim) {
00308
00309 if (num_constraints > 0) {
00310 #ifndef NDEBUG
00311 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
00312 << endl
00313 << "a universe polyhedron has non-redundant constraints!"
00314 << endl;
00315 #endif
00316 return false;
00317 }
00318
00319 if (num_points != 1) {
00320 #ifndef NDEBUG
00321 cerr << "In the BHRZ03 certificate about a non-empty polyhedron:"
00322 << endl
00323 << "a universe polyhedron has more than one non-redundant point!"
00324 << endl;
00325 #endif
00326 return false;
00327 }
00328 }
00329
00330
00331 return true;
00332 }