Parma_Polyhedra_Library::Grid_Certificate Class Reference

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

#include <Grid_Certificate_defs.hh>

Classes
struct	Compare
	A total ordering on Grid certificates. More...

Public Member Functions
	Grid_Certificate ()
	Default constructor. More...
	Grid_Certificate (const Grid &gr)
	Constructor: computes the certificate for gr. More...
	Grid_Certificate (const Grid_Certificate &y)
	Copy constructor. More...
	~Grid_Certificate ()
	Destructor. More...
int	compare (const Grid_Certificate &y) const
	The comparison function for certificates. More...
int	compare (const Grid &gr) const
	Compares *this with the certificate for grid gr. More...
bool	is_stabilizing (const Grid &gr) const
	Returns true if and only if the certificate for grid gr is strictly smaller than *this. More...
bool	OK () const
	Check if gathered information is meaningful. More...

Private Attributes
dimension_type	num_equalities
dimension_type	num_proper_congruences

Detailed Description

The convergence certificate for the Grid 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, Grid_Certificate can certify the Grid widening.

Definition at line 43 of file Grid_Certificate_defs.hh.

Constructor & Destructor Documentation

Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate ( )

inline

Default constructor.

Definition at line 32 of file Grid_Certificate_inlines.hh.

References OK().

  : num_equalities(0), num_proper_congruences(0) {
  // This is the certificate for a zero-dim universe grid.
  PPL_ASSERT(OK());
}

Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate

(

const Grid &

gr

)

Constructor: computes the certificate for gr.

Definition at line 33 of file Grid_Certificate.cc.

References Parma_Polyhedra_Library::Grid::con_sys, Parma_Polyhedra_Library::Grid::congruences_are_minimized(), Parma_Polyhedra_Library::Grid::congruences_are_up_to_date(), Parma_Polyhedra_Library::Grid::dim_kinds, Parma_Polyhedra_Library::Implementation::BD_Shapes::empty, Parma_Polyhedra_Library::Grid_Generator_System::empty(), Parma_Polyhedra_Library::Grid::gen_sys, Parma_Polyhedra_Library::Grid::generators_are_minimized(), Parma_Polyhedra_Library::Grid::generators_are_up_to_date(), Parma_Polyhedra_Library::Grid::marked_empty(), num_equalities, Parma_Polyhedra_Library::Congruence_System::num_equalities(), Parma_Polyhedra_Library::Grid_Generator_System::num_parameters(), num_proper_congruences, Parma_Polyhedra_Library::Congruence_System::num_proper_congruences(), Parma_Polyhedra_Library::Grid_Generator_System::num_rows(), PPL_USED, Parma_Polyhedra_Library::Grid::set_congruences_minimized(), Parma_Polyhedra_Library::Grid::set_generators_minimized(), Parma_Polyhedra_Library::Grid::simplify(), and Parma_Polyhedra_Library::Grid::space_dimension().

  : num_equalities(0), num_proper_congruences(0) {

  // As in Polyhedron assume that `gr' contains at least one point.
  PPL_ASSERT(!gr.marked_empty());
  if (gr.space_dimension() == 0) {
    return;
  }
  // One of the systems must be in minimal form.
  if (gr.congruences_are_up_to_date()) {
    if (gr.congruences_are_minimized()) {
      num_proper_congruences = gr.con_sys.num_proper_congruences();
      num_equalities = gr.con_sys.num_equalities();
    }
    else {
      if (gr.generators_are_up_to_date() && gr.generators_are_minimized()) {
        // Calculate number of congruences from generators.
        num_proper_congruences
          = gr.gen_sys.num_parameters() + 1 /* Integrality cg. */;
        num_equalities = gr.space_dimension() + 1 - gr.gen_sys.num_rows();
      }
      else {
        // Minimize `gr' congruence system.  As in Polyhedron assume
        // that `gr' contains at least one point.
        Grid& mgr = const_cast<Grid&>(gr);
        const bool empty = Grid::simplify(mgr.con_sys, mgr.dim_kinds);
        // Avoid possible compiler warning.
        PPL_USED(empty);
        PPL_ASSERT(!empty);
        mgr.set_congruences_minimized();

        num_proper_congruences = mgr.con_sys.num_proper_congruences();
        num_equalities = mgr.con_sys.num_equalities();
      }
    }
  }
  else {
    if (!gr.generators_are_minimized()) {
      // Minimize `gr' generator system.  As in Polyhedron assume that
      // `gr' contains at least one point.
      Grid& mgr = const_cast<Grid&>(gr);
      Grid::simplify(mgr.gen_sys, mgr.dim_kinds);
      // If gen_sys contained rows before being reduced, it should
      // contain at least a single point afterward.
      PPL_ASSERT(!mgr.gen_sys.empty());
      mgr.set_generators_minimized();
    }
    // Calculate number of congruences from generators.
    num_proper_congruences
      = gr.gen_sys.num_parameters() + 1 /* Integrality cg. */;
    num_equalities
      = gr.space_dimension() + 1 - gr.gen_sys.num_rows();
  }
}

Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate ( const Grid_Certificate &  y )

inline

Copy constructor.

Definition at line 39 of file Grid_Certificate_inlines.hh.

  : num_equalities(y.num_equalities),
    num_proper_congruences(y.num_proper_congruences) {
}

Parma_Polyhedra_Library::Grid_Certificate::~Grid_Certificate ( )

inline

Destructor.

Definition at line 45 of file Grid_Certificate_inlines.hh.

                                    {
}

Member Function Documentation

int Parma_Polyhedra_Library::Grid_Certificate::compare

(

const Grid_Certificate &

y

)

const

The comparison function for certificates.

Returns

, or depending on whether *this is smaller than, equal to, or greater than y, respectively.

Definition at line 89 of file Grid_Certificate.cc.

References num_equalities, num_proper_congruences, and OK().

Referenced by is_stabilizing(), and Parma_Polyhedra_Library::Grid_Certificate::Compare::operator()().

                                                            {
  PPL_ASSERT(OK() && y.OK());
  if (num_equalities == y.num_equalities) {
    if (num_proper_congruences == y.num_proper_congruences) {
      return 0;
    }
    else {
      return (num_proper_congruences > y.num_proper_congruences) ? 1 : -1;
    }
  }
  return (num_equalities > y.num_equalities) ? 1 : -1;
}

int Parma_Polyhedra_Library::Grid_Certificate::compare

(

const Grid &

gr

)

const

Compares *this with the certificate for grid gr.

Definition at line 103 of file Grid_Certificate.cc.

References Parma_Polyhedra_Library::compare().

                                                 {
  const Grid_Certificate gc(gr);
  return compare(gc);
}

bool Parma_Polyhedra_Library::Grid_Certificate::is_stabilizing ( const Grid &  gr ) const

inline

Returns true if and only if the certificate for grid gr is strictly smaller than *this.

Definition at line 49 of file Grid_Certificate_inlines.hh.

References compare().

                                                     {
  return compare(gr) == 1;
}

bool Parma_Polyhedra_Library::Grid_Certificate::OK

(

)

const

Check if gathered information is meaningful.

Definition at line 109 of file Grid_Certificate.cc.

Referenced by compare(), and Grid_Certificate().

                              {
  // There is nothing to test.
  return true;
}

Member Data Documentation

dimension_type Parma_Polyhedra_Library::Grid_Certificate::num_equalities

private

Number of a equalities in a minimized congruence system for the grid.

Definition at line 95 of file Grid_Certificate_defs.hh.

Referenced by compare(), and Grid_Certificate().

dimension_type Parma_Polyhedra_Library::Grid_Certificate::num_proper_congruences

private

Number of a proper congruences in a minimized congruence system for the grid.

Definition at line 98 of file Grid_Certificate_defs.hh.

Referenced by compare(), and Grid_Certificate().

---

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

• Grid_Certificate_defs.hh
• Grid_Certificate.cc
• Grid_Certificate_inlines.hh