#include <H79_Certificate.defs.hh>
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... |
Convergence certificates are used to instantiate the BHZ03 framework so as to define widening operators for the finite powerset domain.
Definition at line 40 of file H79_Certificate.defs.hh.
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 }
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] |
int Parma_Polyhedra_Library::H79_Certificate::compare | ( | const H79_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 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 }
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 }
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().