#include <BHRZ03_Certificate.defs.hh>
Public Member Functions | |
BHRZ03_Certificate () | |
Default constructor. | |
BHRZ03_Certificate (const Polyhedron &ph) | |
Constructor: computes the certificate for ph . | |
BHRZ03_Certificate (const BHRZ03_Certificate &y) | |
Copy constructor. | |
~BHRZ03_Certificate () | |
Destructor. | |
int | compare (const BHRZ03_Certificate &y) const |
The comparison function for certificates. | |
int | compare (const Polyhedron &ph) const |
Compares *this with the certificate for polyhedron ph . | |
bool | is_stabilizing (const Polyhedron &ph) const |
Returns true if and only if the certificate for polyhedron ph is strictly smaller than *this . | |
bool | OK () const |
Check if gathered information is meaningful. | |
Private Attributes | |
dimension_type | affine_dim |
Affine dimension of the polyhedron. | |
dimension_type | lin_space_dim |
Dimension of the lineality space of the polyhedron. | |
dimension_type | num_constraints |
Cardinality of a non-redundant constraint system for the polyhedron. | |
dimension_type | num_points |
Number of non-redundant points in a generator system for the polyhedron. | |
std::vector< dimension_type > | num_rays_null_coord |
A vector containing, for each index `0 <= i < space_dim', the number of non-redundant rays in a generator system of the polyhedron having exactly `i' null coordinates. | |
Classes | |
struct | Compare |
A total ordering on BHRZ03 certificates. More... |
Convergence certificates are used to instantiate the BHZ03 framework so as to define widening operators for the finite powerset domain.
Definition at line 42 of file BHRZ03_Certificate.defs.hh.
Parma_Polyhedra_Library::BHRZ03_Certificate::BHRZ03_Certificate | ( | ) | [inline] |
Default constructor.
Definition at line 29 of file BHRZ03_Certificate.inlines.hh.
References OK().
00030 : affine_dim(0), lin_space_dim(0), num_constraints(0), num_points(1), 00031 num_rays_null_coord() { 00032 // This is the certificate for a zero-dim universe polyhedron. 00033 assert(OK()); 00034 }
Parma_Polyhedra_Library::BHRZ03_Certificate::BHRZ03_Certificate | ( | const Polyhedron & | ph | ) |
Constructor: computes the certificate for ph
.
Definition at line 34 of file BHRZ03_Certificate.cc.
References affine_dim, Parma_Polyhedra_Library::Generator_System::begin(), Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Generator::CLOSURE_POINT, Parma_Polyhedra_Library::Generator::coefficient(), Parma_Polyhedra_Library::Generator_System::end(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Polyhedron::is_necessarily_closed(), lin_space_dim, Parma_Polyhedra_Library::Generator::LINE, Parma_Polyhedra_Library::Polyhedron::marked_empty(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Polyhedron::minimized_constraints(), Parma_Polyhedra_Library::Polyhedron::minimized_generators(), num_constraints, num_points, num_rays_null_coord, OK(), Parma_Polyhedra_Library::Generator::POINT, Parma_Polyhedra_Library::Generator::RAY, and Parma_Polyhedra_Library::Polyhedron::space_dimension().
00035 : affine_dim(0), lin_space_dim(0), num_constraints(0), num_points(0), 00036 num_rays_null_coord(ph.space_dimension(), 0) { 00037 // TODO: provide a correct and reasonably efficient 00038 // implementation for NNC polyhedra. 00039 00040 // The computation of the certificate requires both the 00041 // constraint and the generator systems in minimal form. 00042 ph.minimize(); 00043 // It is assumed that `ph' is not an empty polyhedron. 00044 assert(!ph.marked_empty()); 00045 00046 // The dimension of the polyhedron is obtained by subtracting 00047 // the number of equalities from the space dimension. 00048 // When counting constraints, for a correct reasoning, we have 00049 // to disregard the low-level constraints (i.e., the positivity 00050 // constraint and epsilon bounds). 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 // Intentionally fall through. 00070 case Generator::CLOSURE_POINT: 00071 ++num_points; 00072 break; 00073 case Generator::RAY: 00074 // For each i such that 0 <= j < space_dim, 00075 // `num_rays_null_coord[j]' will be the number of rays 00076 // having exactly `j' coordinates equal to 0. 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 // Since the generator systems is minimized, the dimension of 00088 // the lineality space is equal to the number of lines. 00089 ++lin_space_dim; 00090 break; 00091 } 00092 assert(OK()); 00093 00094 // TODO: this is an inefficient workaround. 00095 // For NNC polyhedra, constraints might be no longer up-to-date 00096 // (and hence, neither minimized) due to the strong minimization 00097 // process applied to generators when constructing the certificate. 00098 // We have to reinforce the (normal) minimization of the constraint 00099 // system. The future, lazy implementation of the strong minimization 00100 // process will solve this problem. 00101 if (!ph.is_necessarily_closed()) 00102 ph.minimize(); 00103 }
Parma_Polyhedra_Library::BHRZ03_Certificate::BHRZ03_Certificate | ( | const BHRZ03_Certificate & | y | ) | [inline] |
Copy constructor.
Definition at line 37 of file BHRZ03_Certificate.inlines.hh.
00038 : affine_dim(y.affine_dim), lin_space_dim(y.lin_space_dim), 00039 num_constraints(y.num_constraints), num_points(y.num_points), 00040 num_rays_null_coord(y.num_rays_null_coord) { 00041 }
Parma_Polyhedra_Library::BHRZ03_Certificate::~BHRZ03_Certificate | ( | ) | [inline] |
int Parma_Polyhedra_Library::BHRZ03_Certificate::compare | ( | const BHRZ03_Certificate & | y | ) | const |
The comparison function for certificates.
*this
is smaller than, equal to, or greater than y
, respectively.*this
with y
, using a total ordering which is a refinement of the limited growth ordering relation for the BHRZ03 widening.
Definition at line 106 of file BHRZ03_Certificate.cc.
References affine_dim, lin_space_dim, num_constraints, num_points, num_rays_null_coord, and OK().
Referenced by is_stabilizing(), and Parma_Polyhedra_Library::BHRZ03_Certificate::Compare::operator()().
00106 { 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 // Note: iterating upwards, because we have to check first 00120 // the number of rays having more NON-zero coordinates. 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 // All components are equal. 00125 return 0; 00126 }
int Parma_Polyhedra_Library::BHRZ03_Certificate::compare | ( | const Polyhedron & | ph | ) | const |
Compares *this
with the certificate for polyhedron ph
.
Definition at line 129 of file BHRZ03_Certificate.cc.
References affine_dim, Parma_Polyhedra_Library::Generator_System::begin(), Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Generator::CLOSURE_POINT, Parma_Polyhedra_Library::Generator::coefficient(), Parma_Polyhedra_Library::Generator_System::end(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Polyhedron::is_necessarily_closed(), lin_space_dim, Parma_Polyhedra_Library::Generator::LINE, Parma_Polyhedra_Library::Polyhedron::marked_empty(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Polyhedron::minimized_constraints(), Parma_Polyhedra_Library::Polyhedron::minimized_generators(), num_constraints, num_points, num_rays_null_coord, Parma_Polyhedra_Library::Generator::POINT, Parma_Polyhedra_Library::Generator::RAY, Parma_Polyhedra_Library::Polyhedron::space_dim, and Parma_Polyhedra_Library::Polyhedron::space_dimension().
00129 { 00130 assert(ph.space_dimension() == num_rays_null_coord.size()); 00131 00132 // TODO: provide a correct and reasonably efficient 00133 // implementation for NNC polyhedra. 00134 00135 // The computation of the certificate requires both the 00136 // constraint and the generator systems in minimal form. 00137 ph.minimize(); 00138 // It is assumed that `ph' is a polyhedron containing the 00139 // polyhedron described by `*this': hence, it cannot be empty. 00140 assert(!ph.marked_empty()); 00141 00142 // The dimension of the polyhedron is obtained by subtracting 00143 // the number of equalities from the space dimension. 00144 // When counting constraints, for a correct reasoning, we have 00145 // to disregard the low-level constraints (i.e., the positivity 00146 // constraint and epsilon bounds). 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 // TODO: this is an inefficient workaround. 00158 // For NNC polyhedra, constraints might be no longer up-to-date 00159 // (and hence, neither minimized) due to the strong minimization 00160 // process applied to generators when constructing the certificate. 00161 // We have to reinforce the (normal) minimization of the constraint 00162 // system. The future, lazy implementation of the strong minimization 00163 // process will solve this problem. 00164 if (!ph.is_necessarily_closed()) 00165 ph.minimize(); 00166 00167 // If the dimension of `ph' is increasing, the chain is stabilizing. 00168 if (ph_affine_dim > affine_dim) 00169 return 1; 00170 00171 // At this point the two polyhedra must have the same dimension. 00172 assert(ph_affine_dim == affine_dim); 00173 00174 // Speculative optimization: in order to better exploit the incrementality 00175 // of the comparison, we do not compute information about rays here, 00176 // hoping that the other components will be enough. 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 // Intentionally fall through. 00185 case Generator::CLOSURE_POINT: 00186 ++ph_num_points; 00187 break; 00188 case Generator::RAY: 00189 break; 00190 case Generator::LINE: 00191 // Since the generator systems is minimized, the dimension of 00192 // the lineality space is equal to the number of lines. 00193 ++ph_lin_space_dim; 00194 break; 00195 } 00196 // TODO: this is an inefficient workaround. 00197 // For NNC polyhedra, constraints might be no longer up-to-date 00198 // (and hence, neither minimized) due to the strong minimization 00199 // process applied to generators when constructing the certificate. 00200 // We have to reinforce the (normal) minimization of the constraint 00201 // system. The future, lazy implementation of the strong minimization 00202 // process will solve this problem. 00203 if (!ph.is_necessarily_closed()) 00204 ph.minimize(); 00205 00206 // If the dimension of the lineality space is increasing, 00207 // then the chain is stabilizing. 00208 if (ph_lin_space_dim > lin_space_dim) 00209 return 1; 00210 00211 // At this point the lineality space of the two polyhedra must have 00212 // the same dimension. 00213 assert(ph_lin_space_dim == lin_space_dim); 00214 00215 // If the number of constraints of `ph' is decreasing, then the chain 00216 // is stabilizing. If it is increasing, the chain is not stabilizing. 00217 // If they are equal, further investigation is needed. 00218 if (ph_num_constraints != num_constraints) 00219 return ph_num_constraints < num_constraints ? 1 : -1; 00220 00221 // If the number of points of `ph' is decreasing, then the chain 00222 // is stabilizing. If it is increasing, the chain is not stabilizing. 00223 // If they are equal, further investigation is needed. 00224 if (ph_num_points != num_points) 00225 return ph_num_points < num_points ? 1 : -1; 00226 00227 // The speculative optimization was not worth: 00228 // compute information about rays. 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 // Compare (lexicographically) the two vectors: 00241 // if ph_num_rays_null_coord < num_rays_null_coord the chain is stabilizing. 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 // All components are equal. 00247 return 0; 00248 }
bool Parma_Polyhedra_Library::BHRZ03_Certificate::is_stabilizing | ( | const Polyhedron & | ph | ) | const [inline] |
Returns true
if and only if the certificate for polyhedron ph
is strictly smaller than *this
.
Definition at line 48 of file BHRZ03_Certificate.inlines.hh.
References compare().
Referenced by Parma_Polyhedra_Library::Polyhedron::BHRZ03_combining_constraints(), Parma_Polyhedra_Library::Polyhedron::BHRZ03_evolving_points(), Parma_Polyhedra_Library::Polyhedron::BHRZ03_evolving_rays(), and Parma_Polyhedra_Library::Polyhedron::BHRZ03_widening_assign().
00048 { 00049 return compare(ph) == 1; 00050 }
bool Parma_Polyhedra_Library::BHRZ03_Certificate::OK | ( | ) | const |
Check if gathered information is meaningful.
Definition at line 251 of file BHRZ03_Certificate.cc.
References affine_dim, lin_space_dim, num_constraints, num_points, and num_rays_null_coord.
Referenced by BHRZ03_Certificate(), and compare().
00251 { 00252 #ifndef NDEBUG 00253 using std::endl; 00254 using std::cerr; 00255 #endif 00256 00257 // The dimension of the vector space. 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 // This was a universe polyhedron. 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 // All tests passed. 00331 return true; 00332 }
Affine dimension of the polyhedron.
Definition at line 97 of file BHRZ03_Certificate.defs.hh.
Referenced by BHRZ03_Certificate(), compare(), and OK().
Dimension of the lineality space of the polyhedron.
Definition at line 99 of file BHRZ03_Certificate.defs.hh.
Referenced by BHRZ03_Certificate(), compare(), and OK().
Cardinality of a non-redundant constraint system for the polyhedron.
Definition at line 101 of file BHRZ03_Certificate.defs.hh.
Referenced by BHRZ03_Certificate(), compare(), and OK().
Number of non-redundant points in a generator system for the polyhedron.
Definition at line 106 of file BHRZ03_Certificate.defs.hh.
Referenced by BHRZ03_Certificate(), compare(), and OK().
std::vector<dimension_type> Parma_Polyhedra_Library::BHRZ03_Certificate::num_rays_null_coord [private] |
A vector containing, for each index `0 <= i < space_dim', the number of non-redundant rays in a generator system of the polyhedron having exactly `i' null coordinates.
Definition at line 112 of file BHRZ03_Certificate.defs.hh.
Referenced by BHRZ03_Certificate(), compare(), and OK().