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

A saturation matrix. More...

#include <Saturation_Matrix.defs.hh>

List of all members.

Public Member Functions

 Saturation_Matrix ()
 Default constructor.
 Saturation_Matrix (dimension_type n_rows, dimension_type n_columns)
 Construct a saturation matrix with n_rows rows and n_columns columns.
 Saturation_Matrix (const Saturation_Matrix &y)
 Copy-constructor.
 ~Saturation_Matrix ()
 Destructor.
Saturation_Matrixoperator= (const Saturation_Matrix &y)
 Assignment operator.
void swap (Saturation_Matrix &y)
 Swaps *this with y.
Saturation_Rowoperator[] (dimension_type k)
 Subscript operator.
const Saturation_Rowoperator[] (dimension_type k) const
 Constant subscript operator.
void clear ()
 Clears the matrix deallocating all its rows.
void transpose ()
 Transposes the matrix.
void transpose_assign (const Saturation_Matrix &y)
 Makes *this a transposed copy of y.
dimension_type num_columns () const
 Returns the number of columns of *this.
dimension_type num_rows () const
 Returns the number of rows of *this.
void sort_rows ()
 Sorts the rows and removes duplicates.
bool sorted_contains (const Saturation_Row &row) const
 Looks for row in *this, which is assumed to be sorted.
void add_row (const Saturation_Row &row)
 Adds row to *this.
void rows_erase_to_end (dimension_type first_to_erase)
 Erases the rows from the first_to_erase -th to the last one.
void columns_erase_to_end (dimension_type first_to_erase)
 Erases the columns from the first_to_erase -th to the last one.
void resize (dimension_type new_n_rows, dimension_type new_n_columns)
 Resizes the matrix copying the old contents.
bool OK () const
 Checks if all the invariants are satisfied.
void ascii_dump () const
 Writes to std::cerr an ASCII representation of *this.
void ascii_dump (std::ostream &s) const
 Writes to s an ASCII representation of *this.
void print () const
 Prints *this to std::cerr using operator<<.
bool ascii_load (std::istream &s)
 Loads from s an ASCII representation (as produced by ascii_dump) and sets *this accordingly. Returns true if successful, false otherwise.
memory_size_type total_memory_in_bytes () const
 Returns the total size in bytes of the memory occupied by *this.
memory_size_type external_memory_in_bytes () const
 Returns the size in bytes of the memory managed by *this.
bool check_sorted () const
 Checks whether *this is sorted. It does NOT check for duplicates.

Static Public Member Functions

static dimension_type max_num_rows ()
 Returns the maximum number of rows of a Saturation_Matrix.

Private Attributes

std::vector< Saturation_Rowrows
 Contains the rows of the matrix.
dimension_type row_size
 Size of the initialized part of each row.

Friends

void Parma_Polyhedra_Library::Linear_System::sort_and_remove_with_sat (Saturation_Matrix &sat)

Related Functions

(Note that these are not member functions.)

void swap (Parma_Polyhedra_Library::Saturation_Matrix &x, Parma_Polyhedra_Library::Saturation_Matrix &y)
 Specializes std::swap.

Classes

struct  Saturation_Row_Less_Than
 Ordering predicate (used when implementing the sort algorithm). More...


Detailed Description

A saturation matrix.

A saturation matrix is used to encode the relation between the generators and the constraints of a polyhedron: if a generator saturates a constraint the corresponding element of the saturation matrix is $0$, otherwise (i.e., if the generator satisfies but does not saturate the constraint) the corresponding element is $1$.

Note:
since the constraints and generators are taken from the same polyhedron description, it cannot be the case that a generator violates a constraint.

Definition at line 47 of file Saturation_Matrix.defs.hh.


Constructor & Destructor Documentation

Parma_Polyhedra_Library::Saturation_Matrix::Saturation_Matrix (  )  [inline]

Default constructor.

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

00033   : rows(),
00034     row_size(0) {
00035 }

Parma_Polyhedra_Library::Saturation_Matrix::Saturation_Matrix ( dimension_type  n_rows,
dimension_type  n_columns 
) [inline]

Construct a saturation matrix with n_rows rows and n_columns columns.

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

00045   : rows(n_rows),
00046     row_size(n_columns) {
00047 }

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

Copy-constructor.

Definition at line 50 of file Saturation_Matrix.inlines.hh.

00051   : rows(y.rows),
00052     row_size(y.row_size) {
00053 }

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

Destructor.

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

00056                                       {
00057 }


Member Function Documentation

PPL::Saturation_Matrix & Parma_Polyhedra_Library::Saturation_Matrix::operator= ( const Saturation_Matrix y  ) 

Assignment operator.

Definition at line 35 of file Saturation_Matrix.cc.

References OK(), row_size, and rows.

00035                                                          {
00036   rows = y.rows;
00037   row_size = y.row_size;
00038   assert(OK());
00039   return *this;
00040 }

void Parma_Polyhedra_Library::Saturation_Matrix::swap ( Saturation_Matrix y  )  [inline]

Swaps *this with y.

Definition at line 79 of file Saturation_Matrix.inlines.hh.

References row_size, and rows.

Referenced by clear(), resize(), swap(), transpose(), and transpose_assign().

00079                                             {
00080   std::swap(row_size, y.row_size);
00081   std::swap(rows, y.rows);
00082 }

Saturation_Row & Parma_Polyhedra_Library::Saturation_Matrix::operator[] ( dimension_type  k  )  [inline]

Subscript operator.

Definition at line 85 of file Saturation_Matrix.inlines.hh.

References rows.

00085                                                     {
00086   assert(k < rows.size());
00087   return rows[k];
00088 }

const Saturation_Row & Parma_Polyhedra_Library::Saturation_Matrix::operator[] ( dimension_type  k  )  const [inline]

Constant subscript operator.

Definition at line 91 of file Saturation_Matrix.inlines.hh.

References rows.

00091                                                           {
00092   assert(k < rows.size());
00093   return rows[k];
00094 }

void Parma_Polyhedra_Library::Saturation_Matrix::clear (  )  [inline]

Clears the matrix deallocating all its rows.

Definition at line 107 of file Saturation_Matrix.inlines.hh.

References row_size, rows, and swap().

Referenced by ascii_load(), Parma_Polyhedra_Library::Polyhedron::set_empty(), Parma_Polyhedra_Library::Polyhedron::update_sat_c(), and Parma_Polyhedra_Library::Polyhedron::update_sat_g().

00107                          {
00108   // Clear `rows' and minimize its capacity.
00109   std::vector<Saturation_Row>().swap(rows);
00110   row_size = 0;
00111 }

void Parma_Polyhedra_Library::Saturation_Matrix::transpose (  ) 

Transposes the matrix.

Definition at line 80 of file Saturation_Matrix.cc.

References num_columns(), num_rows(), OK(), and swap().

00080                                 {
00081   const Saturation_Matrix& x = *this;
00082   const dimension_type nrows = num_rows();
00083   const dimension_type ncols = num_columns();
00084   Saturation_Matrix tmp(ncols, nrows);
00085   for (dimension_type i = nrows; i-- > 0; )
00086     for (unsigned long j = x[i].last(); j != ULONG_MAX; j = x[i].prev(j))
00087       tmp[j].set(i);
00088   swap(tmp);
00089   assert(OK());
00090 }

void Parma_Polyhedra_Library::Saturation_Matrix::transpose_assign ( const Saturation_Matrix y  ) 

dimension_type Parma_Polyhedra_Library::Saturation_Matrix::max_num_rows (  )  [inline, static]

Returns the maximum number of rows of a Saturation_Matrix.

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

Referenced by add_row(), and resize().

00038                                 {
00039   return std::vector<Saturation_Row>().max_size();
00040 }

dimension_type Parma_Polyhedra_Library::Saturation_Matrix::num_columns (  )  const [inline]

dimension_type Parma_Polyhedra_Library::Saturation_Matrix::num_rows (  )  const [inline]

void Parma_Polyhedra_Library::Saturation_Matrix::sort_rows (  ) 

Sorts the rows and removes duplicates.

Definition at line 43 of file Saturation_Matrix.cc.

References OK(), and rows.

Referenced by Parma_Polyhedra_Library::Polyhedron::select_H79_constraints().

00043                                 {
00044   typedef std::vector<Saturation_Row>::iterator Iter;
00045   // Sorting without removing duplicates.
00046   Iter first = rows.begin();
00047   Iter last = rows.end();
00048   swapping_sort(first, last, Saturation_Row_Less_Than());
00049   // Moving all the duplicate elements at the end of the vector.
00050   Iter new_last = swapping_unique(first, last);
00051   // Removing duplicates.
00052   rows.erase(new_last, last);
00053   assert(OK());
00054 }

bool Parma_Polyhedra_Library::Saturation_Matrix::sorted_contains ( const Saturation_Row row  )  const [inline]

Looks for row in *this, which is assumed to be sorted.

Returns:
true if row belongs to *this, false otherwise.
Parameters:
row The row that will be searched for in the matrix.
Given a sorted saturation matrix (this ensures better efficiency), tells whether it contains the given row.

Definition at line 125 of file Saturation_Matrix.inlines.hh.

References check_sorted(), and rows.

Referenced by Parma_Polyhedra_Library::Polyhedron::select_H79_constraints().

00125                                                                   {
00126   assert(check_sorted());
00127   return std::binary_search(rows.begin(), rows.end(), row,
00128                             Saturation_Row_Less_Than());
00129 }

void Parma_Polyhedra_Library::Saturation_Matrix::add_row ( const Saturation_Row row  ) 

Adds row to *this.

Definition at line 57 of file Saturation_Matrix.cc.

References Parma_Polyhedra_Library::compute_capacity(), max_num_rows(), OK(), rows, and Parma_Polyhedra_Library::Saturation_Row::swap().

Referenced by Parma_Polyhedra_Library::Polyhedron::conversion().

00057                                                        {
00058   const dimension_type new_rows_size = rows.size() + 1;
00059   if (rows.capacity() < new_rows_size) {
00060     // Reallocation will take place.
00061     std::vector<Saturation_Row> new_rows;
00062     new_rows.reserve(compute_capacity(new_rows_size, max_num_rows()));
00063     new_rows.insert(new_rows.end(), new_rows_size, Saturation_Row());
00064     // Put the new row in place.
00065     dimension_type i = new_rows_size-1;
00066     new_rows[i] = row;
00067     // Steal the old rows.
00068     while (i-- > 0)
00069       new_rows[i].swap(rows[i]);
00070     // Put the new rows into place.
00071     std::swap(rows, new_rows);
00072   }
00073   else
00074     // Reallocation will NOT take place: append a new empty row.
00075     rows.push_back(row);
00076   assert(OK());
00077 }

void Parma_Polyhedra_Library::Saturation_Matrix::rows_erase_to_end ( dimension_type  first_to_erase  )  [inline]

Erases the rows from the first_to_erase -th to the last one.

Definition at line 60 of file Saturation_Matrix.inlines.hh.

References OK(), and rows.

Referenced by Parma_Polyhedra_Library::Polyhedron::conversion(), Parma_Polyhedra_Library::Polyhedron::select_H79_constraints(), Parma_Polyhedra_Library::Polyhedron::simplify(), and Parma_Polyhedra_Library::Linear_System::sort_and_remove_with_sat().

00060                                                                         {
00061   // The first row to be erased cannot be greater
00062   // than the actual number of the rows of the matrix.
00063   assert(first_to_erase <= rows.size());
00064   if (first_to_erase < rows.size())
00065     rows.erase(rows.begin() + first_to_erase, rows.end());
00066   assert(OK());
00067 }

void Parma_Polyhedra_Library::Saturation_Matrix::columns_erase_to_end ( dimension_type  first_to_erase  )  [inline]

Erases the columns from the first_to_erase -th to the last one.

Definition at line 70 of file Saturation_Matrix.inlines.hh.

References OK(), and row_size.

Referenced by Parma_Polyhedra_Library::Polyhedron::conversion().

00070                                                                            {
00071   // The first column to be erased cannot be greater
00072   // than the actual number of the columns of the matrix.
00073   assert(first_to_erase <= row_size);
00074   row_size = first_to_erase;
00075   assert(OK());
00076 }

void Parma_Polyhedra_Library::Saturation_Matrix::resize ( dimension_type  new_n_rows,
dimension_type  new_n_columns 
)

Resizes the matrix copying the old contents.

Definition at line 105 of file Saturation_Matrix.cc.

References Parma_Polyhedra_Library::compute_capacity(), max_num_rows(), num_rows(), OK(), row_size, rows, and swap().

Referenced by Parma_Polyhedra_Library::Polyhedron::add_and_minimize(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), ascii_load(), Parma_Polyhedra_Library::Polyhedron::concatenate_assign(), Parma_Polyhedra_Library::Polyhedron::update_sat_c(), and Parma_Polyhedra_Library::Polyhedron::update_sat_g().

00106                                                      {
00107   assert(OK());
00108   const dimension_type old_num_rows = num_rows();
00109   if (new_n_columns < row_size) {
00110     const dimension_type num_preserved_rows
00111       = std::min(old_num_rows, new_n_rows);
00112     Saturation_Matrix& x = *this;
00113     for (dimension_type i = num_preserved_rows; i-- > 0; )
00114       x[i].clear_from(new_n_columns);
00115   }
00116   row_size = new_n_columns;
00117   if (new_n_rows > old_num_rows) {
00118     if (rows.capacity() < new_n_rows) {
00119       // Reallocation will take place.
00120       std::vector<Saturation_Row> new_rows;
00121       new_rows.reserve(compute_capacity(new_n_rows, max_num_rows()));
00122       new_rows.insert(new_rows.end(), new_n_rows, Saturation_Row());
00123       // Steal the old rows.
00124       for (dimension_type i = old_num_rows; i-- > 0; )
00125         new_rows[i].swap(rows[i]);
00126       // Put the new vector into place.
00127       std::swap(rows, new_rows);
00128     }
00129     else
00130       // Reallocation will NOT take place.
00131       rows.insert(rows.end(), new_n_rows - old_num_rows, Saturation_Row());
00132   }
00133   else if (new_n_rows < old_num_rows)
00134     // Drop some rows.
00135     rows.erase(rows.begin() + new_n_rows, rows.end());
00136 
00137   assert(OK());
00138 }

bool Parma_Polyhedra_Library::Saturation_Matrix::OK (  )  const

Checks if all the invariants are satisfied.

Definition at line 193 of file Saturation_Matrix.cc.

References Parma_Polyhedra_Library::Saturation_Row::last(), num_rows(), Parma_Polyhedra_Library::Saturation_Row::OK(), and row_size.

Referenced by add_row(), ascii_load(), columns_erase_to_end(), Parma_Polyhedra_Library::Polyhedron::OK(), operator=(), resize(), rows_erase_to_end(), sort_rows(), transpose(), and transpose_assign().

00193                                {
00194 #ifndef NDEBUG
00195   using std::endl;
00196   using std::cerr;
00197 #endif
00198 
00199   const Saturation_Matrix& x = *this;
00200   for (dimension_type i = num_rows(); i-- > 1; ) {
00201     const Saturation_Row& row = x[i];
00202     if (!row.OK())
00203       return false;
00204     else if (row.last() != ULONG_MAX && row.last() >= row_size) {
00205 #ifndef NDEBUG
00206       cerr << "Saturation_Matrix[" << i << "] is a row with too many bits!"
00207            << endl
00208            << "(row_size == " << row_size
00209            << ", row.last() == " << row.last() << ")"
00210            << endl;
00211 #endif
00212       return false;
00213     }
00214   }
00215   return true;
00216 }

void Parma_Polyhedra_Library::Saturation_Matrix::ascii_dump (  )  const

Writes to std::cerr an ASCII representation of *this.

Referenced by Parma_Polyhedra_Library::Polyhedron::ascii_dump().

void Parma_Polyhedra_Library::Saturation_Matrix::ascii_dump ( std::ostream &  s  )  const

Writes to s an ASCII representation of *this.

Definition at line 141 of file Saturation_Matrix.cc.

References num_columns(), and num_rows().

00141                                                     {
00142   const Saturation_Matrix& x = *this;
00143   const char separator = ' ';
00144   s << num_rows() << separator << 'x' << separator
00145     << num_columns() << "\n";
00146   for (dimension_type i = 0; i < num_rows(); ++i) {
00147     for (dimension_type j = 0; j < num_columns(); ++j)
00148       s << x[i][j] << separator;
00149     s << "\n";
00150   }
00151 }

void Parma_Polyhedra_Library::Saturation_Matrix::print (  )  const

Prints *this to std::cerr using operator<<.

bool Parma_Polyhedra_Library::Saturation_Matrix::ascii_load ( std::istream &  s  ) 

Loads from s an ASCII representation (as produced by ascii_dump) and sets *this accordingly. Returns true if successful, false otherwise.

Definition at line 156 of file Saturation_Matrix.cc.

References clear(), num_columns(), num_rows(), OK(), and resize().

Referenced by Parma_Polyhedra_Library::Polyhedron::ascii_load().

00156                                               {
00157   Saturation_Matrix& x = *this;
00158   dimension_type nrows;
00159   dimension_type ncols;
00160   std::string str;
00161   if (!(s >> nrows))
00162     return false;
00163   if (!(s >> str))
00164     return false;
00165   if (!(s >> ncols))
00166     return false;
00167   resize(nrows, ncols);
00168 
00169   for (dimension_type i = 0; i < num_rows(); ++i)
00170     for (dimension_type j = 0; j < num_columns(); ++j) {
00171       int bit;
00172       if (!(s >> bit))
00173         return false;
00174       if (bit)
00175         x[i].set(j);
00176       else
00177         x[i].clear(j);
00178     }
00179   // Check for well-formedness.
00180   assert(OK());
00181   return true;
00182 }

memory_size_type Parma_Polyhedra_Library::Saturation_Matrix::total_memory_in_bytes (  )  const [inline]

Returns the total size in bytes of the memory occupied by *this.

Definition at line 114 of file Saturation_Matrix.inlines.hh.

References external_memory_in_bytes().

00114                                                {
00115   return sizeof(*this) + external_memory_in_bytes();
00116 }

PPL::memory_size_type Parma_Polyhedra_Library::Saturation_Matrix::external_memory_in_bytes (  )  const

Returns the size in bytes of the memory managed by *this.

Definition at line 185 of file Saturation_Matrix.cc.

References num_rows(), and rows.

Referenced by Parma_Polyhedra_Library::Polyhedron::external_memory_in_bytes(), and total_memory_in_bytes().

00185                                                      {
00186   memory_size_type n = rows.capacity() * sizeof(Row);
00187   for (dimension_type i = num_rows(); i-- > 0; )
00188     n += rows[i].external_memory_in_bytes();
00189   return n;
00190 }

bool Parma_Polyhedra_Library::Saturation_Matrix::check_sorted (  )  const

Checks whether *this is sorted. It does NOT check for duplicates.

Definition at line 220 of file Saturation_Matrix.cc.

References num_rows().

Referenced by sorted_contains().

00220                                          {
00221   const Saturation_Matrix& x = *this;
00222   for (dimension_type i = num_rows(); i-- > 1; )
00223     if (compare(x[i-1], x[i]) > 0)
00224       return false;
00225   return true;
00226 }


Friends And Related Function Documentation

void Parma_Polyhedra_Library::Linear_System::sort_and_remove_with_sat ( Saturation_Matrix sat  )  [friend]

Specializes std::swap.

Definition at line 138 of file Saturation_Matrix.inlines.hh.

References swap().

00139                                                   {
00140   x.swap(y);
00141 }


Member Data Documentation

Size of the initialized part of each row.

Definition at line 150 of file Saturation_Matrix.defs.hh.

Referenced by clear(), columns_erase_to_end(), num_columns(), OK(), operator=(), resize(), and swap().


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

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