Parma_Polyhedra_Library::H79_Certificate Class Reference

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

Private Attributes
dimension_type	affine_dim
	Affine dimension of the polyhedron. More...
dimension_type	num_constraints
	Cardinality of a non-redundant constraint system for the polyhedron. 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 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, 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 66 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 78 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(), 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 90 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 92 of file H79_Certificate_defs.hh.

Referenced by compare(), and H79_Certificate().

---

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

• H79_Certificate_defs.hh
• H79_Certificate.cc
• H79_Certificate_inlines.hh