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

#include <H79_Certificate.defs.hh>

Classes
struct	Compare
	A total ordering on H79 certificates. More...
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.

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 41 of file H79_Certificate.defs.hh.

Constructor & Destructor Documentation

Parma_Polyhedra_Library::H79_Certificate::H79_Certificate ( )

inline

Default constructor.

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

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

template<typename PH >

Parma_Polyhedra_Library::H79_Certificate::H79_Certificate ( const PH & ph )

inline

Constructor: computes the certificate for ph.

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

References affine_dim, Parma_Polyhedra_Library::NECESSARILY_CLOSED, and num_constraints.

  : affine_dim(0), num_constraints(0) {
  H79_Certificate cert(Polyhedron(NECESSARILY_CLOSED, ph.constraints()));
  affine_dim = cert.affine_dim;
  num_constraints = cert.num_constraints;
}

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

Constructor: computes the certificate for ph.

Definition at line 33 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, PPL_ASSERT, and Parma_Polyhedra_Library::Polyhedron::space_dimension().

  : affine_dim(0), num_constraints(0) {
  // The affine dimension of the polyhedron is obtained by subtracting
  // the number of equalities from the space dimension.
  // When counting constraints, for a correct reasoning, we have
  // to disregard the low-level constraints (i.e., the positivity
  // constraint and epsilon bounds).
  const dimension_type space_dim = ph.space_dimension();
  affine_dim = space_dim;
  const Constraint_System& cs = ph.minimized_constraints();
  // It is assumed that `ph' is not an empty polyhedron.
  PPL_ASSERT(!ph.marked_empty());
  for (Constraint_System::const_iterator i = cs.begin(),
         cs_end = cs.end(); i != cs_end; ++i) {
    ++num_constraints;
    if (i->is_equality())
      --affine_dim;
  }

  // TODO: this is an inefficient workaround.
  // For NNC polyhedra, generators might be no longer up-to-date
  // (and hence, neither minimized) due to the strong minimization
  // process applied to constraints when constructing the certificate.
  // We have to reinforce the (normal) minimization of the generator
  // system. The future, lazy implementation of the strong minimization
  // process will solve this problem.
  if (!ph.is_necessarily_closed())
    ph.minimize();
}

Parma_Polyhedra_Library::H79_Certificate::H79_Certificate ( const H79_Certificate & y )

inline

Copy constructor.

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

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

Parma_Polyhedra_Library::H79_Certificate::~H79_Certificate ( )

inline

Destructor.

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

{
}

Member Function Documentation

int Parma_Polyhedra_Library::H79_Certificate::compare ( const H79_Certificate & y ) const

The comparison function for certificates.

Returns:: , or 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 64 of file H79_Certificate.cc.

References affine_dim, num_constraints, and Parma_Polyhedra_Library::Implementation::num_constraints().

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

                                                          {
  if (affine_dim != y.affine_dim)
    return (affine_dim > y.affine_dim) ? 1 : -1;
  if (num_constraints != y.num_constraints)
    return (num_constraints > y.num_constraints) ? 1 : -1;
  // All components are equal.
  return 0;
}

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 65 of file H79_Certificate.inlines.hh.

References compare(), and Parma_Polyhedra_Library::NECESSARILY_CLOSED.

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

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

Compares *this with the certificate for polyhedron ph.

Definition at line 74 of file H79_Certificate.cc.

References 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(), Parma_Polyhedra_Library::Implementation::num_constraints(), PPL_ASSERT, and Parma_Polyhedra_Library::Polyhedron::space_dimension().

                                                      {
  // The affine dimension of the polyhedron is obtained by subtracting
  // the number of equalities from the space dimension.
  // When counting constraints, for a correct reasoning, we have
  // to disregard the low-level constraints (i.e., the positivity
  // constraint and epsilon bounds).
  const dimension_type space_dim = ph.space_dimension();
  dimension_type ph_affine_dim = space_dim;
  dimension_type ph_num_constraints = 0;
  const Constraint_System& cs = ph.minimized_constraints();
  // It is assumed that `ph' is a polyhedron containing the
  // polyhedron described by `*this': hence, it cannot be empty.
  PPL_ASSERT(!ph.marked_empty());
  for (Constraint_System::const_iterator i = cs.begin(),
         cs_end = cs.end(); i != cs_end; ++i) {
    ++ph_num_constraints;
    if (i->is_equality())
      --ph_affine_dim;
  }
  // TODO: this is an inefficient workaround.
  // For NNC polyhedra, generators might be no longer up-to-date
  // (and hence, neither minimized) due to the strong minimization
  // process applied to constraints when constructing the certificate.
  // We have to reinforce the (normal) minimization of the generator
  // system. The future, lazy implementation of the strong minimization
  // process will solve this problem.
  if (!ph.is_necessarily_closed())
    ph.minimize();

  // If the affine dimension of `ph' is increasing, the chain is stabilizing.
  if (ph_affine_dim > affine_dim)
    return 1;

  // At this point the two polyhedra must have the same affine dimension.
  PPL_ASSERT(ph_affine_dim == affine_dim);

  // If the number of constraints of `ph' is decreasing, then the chain
  // is stabilizing. If it is increasing, the chain is not stabilizing.
  if (ph_num_constraints != num_constraints)
    return (ph_num_constraints < num_constraints) ? 1 : -1;

  // All components are equal.
  return 0;
}

Member Data Documentation

dimension_type Parma_Polyhedra_Library::H79_Certificate::affine_dim

private

Affine dimension of the polyhedron.

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

Referenced by compare(), and H79_Certificate().

dimension_type Parma_Polyhedra_Library::H79_Certificate::num_constraints

private

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

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

Referenced by compare(), and H79_Certificate().

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

Classes

Public Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation