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

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

#include <Grid_Certificate.defs.hh>

List of all members.

Public Member Functions

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

Private Attributes

dimension_type num_equalities
dimension_type num_proper_congruences

Classes

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


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 29 of file Grid_Certificate.inlines.hh.

References OK().

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

Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate ( const Grid gr  ) 

Constructor: computes the certificate for gr.

Definition at line 34 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::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(), Parma_Polyhedra_Library::Congruence_System::num_equalities(), num_equalities, Parma_Polyhedra_Library::Grid_Generator_System::num_generators(), Parma_Polyhedra_Library::Grid_Generator_System::num_parameters(), Parma_Polyhedra_Library::Congruence_System::num_proper_congruences(), num_proper_congruences, 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().

00035   : num_equalities(0), num_proper_congruences(0) {
00036   Grid& gr = const_cast<Grid&>(cgr);
00037   // As in Polyhedron assume that gr contains at least one point.
00038   assert(!gr.marked_empty());
00039   if (gr.space_dimension() == 0)
00040     return;
00041   // One of the systems must be in minimal form.
00042   if (gr.congruences_are_up_to_date())
00043     if (gr.congruences_are_minimized()) {
00044       num_proper_congruences = gr.con_sys.num_proper_congruences();
00045       num_equalities = gr.con_sys.num_equalities();
00046     }
00047     else
00048       if (gr.generators_are_up_to_date() && gr.generators_are_minimized()) {
00049         // Calculate number of congruences from generators.
00050         num_proper_congruences
00051           = gr.gen_sys.num_parameters() + 1 /* Integrality cg. */;
00052         num_equalities
00053           = gr.space_dimension() + 1 - gr.gen_sys.num_generators();
00054       }
00055       else {
00056         // Minimize gr congruence system.  As in Polyhedron assume
00057         // that gr contains at least one point.
00058 #ifndef NDEBUG
00059         Grid::simplify(gr.con_sys, gr.dim_kinds);
00060 #else
00061         bool contains_points = Grid::simplify(gr.con_sys, gr.dim_kinds);
00062         used(contains_points);  // Quiet compiler warning.
00063         assert(contains_points);
00064 #endif
00065         gr.set_congruences_minimized();
00066 
00067         num_proper_congruences = gr.con_sys.num_proper_congruences();
00068         num_equalities = gr.con_sys.num_equalities();
00069       }
00070   else {
00071     if (!gr.generators_are_minimized()) {
00072       // Minimize gr generator system.  As in Polyhedron assume that
00073       // gr contains at least one point.
00074       Grid::simplify(gr.gen_sys, gr.dim_kinds);
00075       // If gen_sys contained rows before being reduced, it should
00076       // contain at least a single point afterwards.
00077       assert(gr.gen_sys.num_generators() > 0);
00078       gr.set_generators_minimized();
00079     }
00080     // Calculate number of congruences from generators.
00081     num_proper_congruences
00082       = gr.gen_sys.num_parameters() + 1 /* Integrality cg. */;
00083     num_equalities
00084       = gr.space_dimension() + 1 - gr.gen_sys.num_generators();
00085   }
00086 }

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

Copy constructor.

Definition at line 36 of file Grid_Certificate.inlines.hh.

00037   : num_equalities(y.num_equalities),
00038     num_proper_congruences(y.num_proper_congruences) {
00039 }

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

Destructor.

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

00042                                     {
00043 }


Member Function Documentation

int Parma_Polyhedra_Library::Grid_Certificate::compare ( const Grid_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.

Definition at line 89 of file Grid_Certificate.cc.

References num_equalities, num_proper_congruences, and OK().

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

00089                                                             {
00090   assert(OK() && y.OK());
00091   if (num_equalities == y.num_equalities)
00092     if (num_proper_congruences == y.num_proper_congruences)
00093       return 0;
00094     else
00095       return num_proper_congruences > y.num_proper_congruences ? 1 : -1;
00096   return num_equalities > y.num_equalities ? 1 : -1;
00097 }

int Parma_Polyhedra_Library::Grid_Certificate::compare ( const Grid gr  )  const

Compares *this with the certificate for grid gr.

Definition at line 100 of file Grid_Certificate.cc.

References compare().

00100                                                  {
00101   Grid_Certificate gc(gr);
00102   return compare(gc);
00103 }

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 46 of file Grid_Certificate.inlines.hh.

References compare().

00046                                                      {
00047   return compare(gr) == 1;
00048 }

bool Parma_Polyhedra_Library::Grid_Certificate::OK (  )  const

Check if gathered information is meaningful.

Definition at line 106 of file Grid_Certificate.cc.

Referenced by compare(), and Grid_Certificate().

00106                               {
00107 #ifndef NDEBUG
00108   using std::endl;
00109   using std::cerr;
00110 #endif
00111 
00112   // All tests passed.
00113   return true;
00114 }


Member Data Documentation

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().

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:

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