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

A convergence certificate for the H79 widening operator. More...

#include <H79_Certificate.defs.hh>

List of all members.

Public Member Functions

 H79_Certificate ()
 Default constructor.
template<typename PH>
 H79_Certificate (const PH &ph)
 Constructor: computes the certificate for ph.
 H79_Certificate (const Polyhedron &ph)
 Constructor: computes the certificate for ph.
 H79_Certificate (const H79_Certificate &y)
 Copy constructor.
 ~H79_Certificate ()
 Destructor.
int compare (const H79_Certificate &y) const
 The comparison function for certificates.
template<typename PH>
int compare (const PH &ph) const
 Compares *this with the certificate for polyhedron ph.
int compare (const Polyhedron &ph) const
 Compares *this with the certificate for polyhedron ph.

Private Attributes

dimension_type affine_dim
 Affine dimension of the polyhedron.
dimension_type num_constraints
 Cardinality of a non-redundant constraint system for the polyhedron.

Classes

struct  Compare
 A total ordering on H79 certificates. More...


Detailed Description

A convergence certificate for the H79 widening operator.

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

Note:
The convergence of the H79 widening can also be certified by BHRZ03_Certificate.

Definition at line 40 of file H79_Certificate.defs.hh.


Constructor & Destructor Documentation

Parma_Polyhedra_Library::H79_Certificate::H79_Certificate (  )  [inline]

Default constructor.

Definition at line 31 of file H79_Certificate.inlines.hh.

00032   : affine_dim(0), num_constraints(0) {
00033   // This is the certificate for a zero-dim universe polyhedron.
00034 }

template<typename PH>
Parma_Polyhedra_Library::H79_Certificate::H79_Certificate ( const PH &  ph  )  [inline]

Constructor: computes the certificate for ph.

Definition at line 55 of file H79_Certificate.inlines.hh.

References affine_dim, Parma_Polyhedra_Library::NECESSARILY_CLOSED, and num_constraints.

00056   : affine_dim(0), num_constraints(0) {
00057   H79_Certificate cert(Polyhedron(NECESSARILY_CLOSED, ph.constraints()));
00058   affine_dim = cert.affine_dim;
00059   num_constraints = cert.num_constraints;
00060 }

Parma_Polyhedra_Library::H79_Certificate::H79_Certificate ( const Polyhedron ph  ) 

Constructor: computes the certificate for ph.

Definition at line 34 of file H79_Certificate.cc.

References affine_dim, Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Polyhedron::is_necessarily_closed(), Parma_Polyhedra_Library::Polyhedron::marked_empty(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Polyhedron::minimized_constraints(), num_constraints, and Parma_Polyhedra_Library::Polyhedron::space_dimension().

00035   : affine_dim(0), num_constraints(0) {
00036   // The affine dimension of the polyhedron is obtained by subtracting
00037   // the number of equalities from the space dimension.
00038   // When counting constraints, for a correct reasoning, we have
00039   // to disregard the low-level constraints (i.e., the positivity
00040   // constraint and epsilon bounds).
00041   const dimension_type space_dim = ph.space_dimension();
00042   affine_dim = space_dim;
00043   const Constraint_System& cs = ph.minimized_constraints();
00044   // It is assumed that `ph' is not an empty polyhedron.
00045   assert(!ph.marked_empty());
00046   for (Constraint_System::const_iterator i = cs.begin(),
00047          cs_end = cs.end(); i != cs_end; ++i) {
00048     ++num_constraints;
00049     if (i->is_equality())
00050       --affine_dim;
00051   }
00052 
00053   // TODO: this is an inefficient workaround.
00054   // For NNC polyhedra, generators might be no longer up-to-date
00055   // (and hence, neither minimized) due to the strong minimization
00056   // process applied to constraints when constructing the certificate.
00057   // We have to reinforce the (normal) minimization of the generator
00058   // system. The future, lazy implementation of the strong minimization
00059   // process will solve this problem.
00060   if (!ph.is_necessarily_closed())
00061     ph.minimize();
00062 }

Parma_Polyhedra_Library::H79_Certificate::H79_Certificate ( const H79_Certificate y  )  [inline]

Copy constructor.

Definition at line 37 of file H79_Certificate.inlines.hh.

00038   : affine_dim(y.affine_dim), num_constraints(y.num_constraints) {
00039 }

Parma_Polyhedra_Library::H79_Certificate::~H79_Certificate (  )  [inline]

Destructor.

Definition at line 42 of file H79_Certificate.inlines.hh.

00042                                   {
00043 }


Member Function Documentation

int Parma_Polyhedra_Library::H79_Certificate::compare ( const H79_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 H79 widening.

Definition at line 65 of file H79_Certificate.cc.

References affine_dim, and num_constraints.

Referenced by compare(), and Parma_Polyhedra_Library::H79_Certificate::Compare::operator()().

00065                                                           {
00066   if (affine_dim != y.affine_dim)
00067     return affine_dim > y.affine_dim ? 1 : -1;
00068   if (num_constraints != y.num_constraints)
00069     return num_constraints > y.num_constraints ? 1 : -1;
00070   // All components are equal.
00071   return 0;
00072 }

template<typename PH>
int Parma_Polyhedra_Library::H79_Certificate::compare ( const PH &  ph  )  const [inline]

Compares *this with the certificate for polyhedron ph.

Definition at line 64 of file H79_Certificate.inlines.hh.

References compare(), and Parma_Polyhedra_Library::NECESSARILY_CLOSED.

00064                                            {
00065   return this->compare(Polyhedron(NECESSARILY_CLOSED, ph.constraints()));
00066 }

int Parma_Polyhedra_Library::H79_Certificate::compare ( const Polyhedron ph  )  const

Compares *this with the certificate for polyhedron ph.

Definition at line 75 of file H79_Certificate.cc.

References affine_dim, Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Polyhedron::is_necessarily_closed(), Parma_Polyhedra_Library::Polyhedron::marked_empty(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Polyhedron::minimized_constraints(), num_constraints, and Parma_Polyhedra_Library::Polyhedron::space_dimension().

00075                                                       {
00076   // The affine dimension of the polyhedron is obtained by subtracting
00077   // the number of equalities from the space dimension.
00078   // When counting constraints, for a correct reasoning, we have
00079   // to disregard the low-level constraints (i.e., the positivity
00080   // constraint and epsilon bounds).
00081   const dimension_type space_dim = ph.space_dimension();
00082   dimension_type ph_affine_dim = space_dim;
00083   dimension_type ph_num_constraints = 0;
00084   const Constraint_System& cs = ph.minimized_constraints();
00085   // It is assumed that `ph' is a polyhedron containing the
00086   // polyhedron described by `*this': hence, it cannot be empty.
00087   assert(!ph.marked_empty());
00088   for (Constraint_System::const_iterator i = cs.begin(),
00089          cs_end = cs.end(); i != cs_end; ++i) {
00090     ++ph_num_constraints;
00091     if (i->is_equality())
00092       --ph_affine_dim;
00093   }
00094   // TODO: this is an inefficient workaround.
00095   // For NNC polyhedra, generators might be no longer up-to-date
00096   // (and hence, neither minimized) due to the strong minimization
00097   // process applied to constraints when constructing the certificate.
00098   // We have to reinforce the (normal) minimization of the generator
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 
00104   // If the affine dimension of `ph' is increasing, the chain is stabilizing.
00105   if (ph_affine_dim > affine_dim)
00106     return 1;
00107 
00108   // At this point the two polyhedra must have the same affine dimension.
00109   assert(ph_affine_dim == affine_dim);
00110 
00111   // If the number of constraints of `ph' is decreasing, then the chain
00112   // is stabilizing. If it is increasing, the chain is not stabilizing.
00113   if (ph_num_constraints != num_constraints)
00114     return ph_num_constraints < num_constraints ? 1 : -1;
00115 
00116   // All components are equal.
00117   return 0;
00118 }


Member Data Documentation

Affine dimension of the polyhedron.

Definition at line 90 of file H79_Certificate.defs.hh.

Referenced by compare(), and H79_Certificate().

Cardinality of a non-redundant constraint system for the polyhedron.

Definition at line 92 of file H79_Certificate.defs.hh.

Referenced by compare(), and H79_Certificate().


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

Generated on Wed Jul 16 22:55:51 2008 for PPL by  doxygen 1.5.6