#include <Saturation_Matrix.defs.hh>
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_Matrix & | operator= (const Saturation_Matrix &y) |
Assignment operator. | |
void | swap (Saturation_Matrix &y) |
Swaps *this with y . | |
Saturation_Row & | operator[] (dimension_type k) |
Subscript operator. | |
const Saturation_Row & | operator[] (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_Row > | rows |
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... |
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 , otherwise (i.e., if the generator satisfies but does not saturate the constraint) the corresponding element is
.
Definition at line 47 of file Saturation_Matrix.defs.hh.
Parma_Polyhedra_Library::Saturation_Matrix::Saturation_Matrix | ( | ) | [inline] |
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.
Parma_Polyhedra_Library::Saturation_Matrix::Saturation_Matrix | ( | const Saturation_Matrix & | y | ) | [inline] |
Parma_Polyhedra_Library::Saturation_Matrix::~Saturation_Matrix | ( | ) | [inline] |
PPL::Saturation_Matrix & Parma_Polyhedra_Library::Saturation_Matrix::operator= | ( | const Saturation_Matrix & | y | ) |
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().
Saturation_Row & Parma_Polyhedra_Library::Saturation_Matrix::operator[] | ( | dimension_type | k | ) | [inline] |
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.
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 | ) |
Makes *this
a transposed copy of y
.
Definition at line 93 of file Saturation_Matrix.cc.
References num_columns(), num_rows(), OK(), and swap().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), Parma_Polyhedra_Library::Polyhedron::concatenate_assign(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_constraints(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_constraints_with_sat_c(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_generators(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_generators_with_sat_g(), Parma_Polyhedra_Library::Polyhedron::process_pending_constraints(), Parma_Polyhedra_Library::Polyhedron::process_pending_generators(), Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints(), and Parma_Polyhedra_Library::Polyhedron::strongly_minimize_generators().
00093 { 00094 const dimension_type y_nrows = y.num_rows(); 00095 const dimension_type y_ncols = y.num_columns(); 00096 Saturation_Matrix tmp(y_ncols, y_nrows); 00097 for (dimension_type i = y_nrows; i-- > 0; ) 00098 for (unsigned long j = y[i].last(); j != ULONG_MAX; j = y[i].prev(j)) 00099 tmp[j].set(i); 00100 swap(tmp); 00101 assert(OK()); 00102 }
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().
dimension_type Parma_Polyhedra_Library::Saturation_Matrix::num_columns | ( | ) | const [inline] |
Returns the number of columns of *this
.
Definition at line 97 of file Saturation_Matrix.inlines.hh.
References row_size.
Referenced by Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), ascii_dump(), ascii_load(), Parma_Polyhedra_Library::Polyhedron::concatenate_assign(), Parma_Polyhedra_Library::Polyhedron::conversion(), Parma_Polyhedra_Library::Polyhedron::OK(), Parma_Polyhedra_Library::Polyhedron::simplify(), transpose(), and transpose_assign().
00097 { 00098 return row_size; 00099 }
dimension_type Parma_Polyhedra_Library::Saturation_Matrix::num_rows | ( | ) | const [inline] |
Returns the number of rows of *this
.
Definition at line 102 of file Saturation_Matrix.inlines.hh.
References rows.
Referenced by Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), ascii_dump(), ascii_load(), check_sorted(), Parma_Polyhedra_Library::Polyhedron::concatenate_assign(), Parma_Polyhedra_Library::Polyhedron::conversion(), external_memory_in_bytes(), OK(), Parma_Polyhedra_Library::Polyhedron::OK(), resize(), Parma_Polyhedra_Library::Linear_System::sort_and_remove_with_sat(), transpose(), and transpose_assign().
00102 { 00103 return rows.size(); 00104 }
void Parma_Polyhedra_Library::Saturation_Matrix::sort_rows | ( | ) |
Sorts the rows and removes duplicates.
Definition at line 43 of file Saturation_Matrix.cc.
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.
true
if row
belongs to *this
, false otherwise.row | The row that will be searched for in the matrix. |
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.
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 }
void Parma_Polyhedra_Library::Linear_System::sort_and_remove_with_sat | ( | Saturation_Matrix & | sat | ) | [friend] |
void swap | ( | Parma_Polyhedra_Library::Saturation_Matrix & | x, | |
Parma_Polyhedra_Library::Saturation_Matrix & | y | |||
) | [related] |
Specializes std::swap
.
Definition at line 138 of file Saturation_Matrix.inlines.hh.
References swap().
00139 { 00140 x.swap(y); 00141 }
std::vector<Saturation_Row> Parma_Polyhedra_Library::Saturation_Matrix::rows [private] |
Contains the rows of the matrix.
Definition at line 147 of file Saturation_Matrix.defs.hh.
Referenced by add_row(), clear(), external_memory_in_bytes(), num_rows(), operator=(), operator[](), resize(), rows_erase_to_end(), Parma_Polyhedra_Library::Linear_System::sort_and_remove_with_sat(), sort_rows(), sorted_contains(), and swap().
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().