Parma_Polyhedra_Library::BHRZ03_Certificate Class Reference
[C++ Language Interface]

The convergence certificate for the BHRZ03 widening operator. More...

#include <BHRZ03_Certificate.defs.hh>

List of all members.

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_typenum_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...


Detailed Description

The convergence certificate for the BHRZ03 widening operator.

Convergence certificates are used to instantiate the BHZ03 framework so as to define widening operators for the finite powerset domain.

Note:
Each convergence certificate has to be used together with a compatible widening operator. In particular, BHRZ03_Certificate can certify the convergence of both the BHRZ03 and the H79 widenings.

Definition at line 42 of file BHRZ03_Certificate.defs.hh.


Constructor & Destructor Documentation

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]

Destructor.

Definition at line 44 of file BHRZ03_Certificate.inlines.hh.

00044                                         {
00045 }


Member Function Documentation

int Parma_Polyhedra_Library::BHRZ03_Certificate::compare ( const BHRZ03_Certificate y  )  const

The comparison function for certificates.

Returns:
$-1$, $0$ or $1$ depending on whether *this is smaller than, equal to, or greater than y, respectively.
Compares *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 }


Member Data Documentation

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().

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().


The documentation for this class was generated from the following files:

Generated on Sat Oct 11 10:41:13 2008 for PPL by  doxygen 1.5.6