#include <Congruence_System.defs.hh>
Public Member Functions | |
Congruence_System () | |
Default constructor: builds an empty system of congruences. | |
Congruence_System (const Congruence &cg) | |
Builds the singleton system containing only congruence cg . | |
Congruence_System (const Constraint &c) | |
If c represents the constraint ![]() ![]() | |
Congruence_System (const Constraint_System &cs) | |
Builds a system containing copies of any equalities in cs . | |
Congruence_System (const Congruence_System &cgs) | |
Ordinary copy-constructor. | |
~Congruence_System () | |
Destructor. | |
Congruence_System & | operator= (const Congruence_System &cgs) |
Assignment operator. | |
dimension_type | space_dimension () const |
Returns the dimension of the vector space enclosing *this . | |
bool | is_equal_to (const Congruence_System &cgs) const |
Returns true if and only if *this is exactly equal to cgs . | |
bool | has_linear_equalities () const |
Returns true if and only if *this contains one or more linear equalities. | |
void | clear () |
Removes all the congruences and sets the space dimension to 0. | |
void | insert (const Congruence &cg) |
Inserts in *this a copy of the congruence cg , increasing the number of space dimensions if needed. | |
void | insert (const Constraint &c) |
Inserts in *this a copy of the equality constraint c , seen as a modulo 0 congruence, increasing the number of space dimensions if needed. | |
void | insert (const Congruence_System &cgs) |
Inserts in *this a copy of the congruences in cgs , increasing the number of space dimensions if needed. | |
void | recycling_insert (Congruence_System &cgs) |
Inserts into *this the congruences in cgs , increasing the number of space dimensions if needed. | |
const_iterator | begin () const |
Returns the const_iterator pointing to the first congruence, if this is not empty; otherwise, returns the past-the-end const_iterator. | |
const_iterator | end () const |
Returns the past-the-end const_iterator. | |
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 . | |
dimension_type | num_equalities () const |
Returns the number of equalities. | |
dimension_type | num_proper_congruences () const |
Returns the number of proper congruences. | |
void | swap (Congruence_System &cgs) |
Swaps *this with y . | |
void | add_unit_rows_and_columns (dimension_type dims) |
Adds dims rows and dims columns of zeroes to the matrix, initializing the added rows as in the unit congruence system. | |
void | concatenate (const Congruence_System &cgs) |
Concatenates copies of the congruences from cgs onto *this . | |
Static Public Member Functions | |
static dimension_type | max_space_dimension () |
Returns the maximum space dimension a Congruence_System can handle. | |
static const Congruence_System & | zero_dim_empty () |
Returns the system containing only Congruence::zero_dim_false(). | |
Protected Member Functions | |
bool | satisfies_all_congruences (const Grid_Generator &g) const |
Returns true if g satisfies all the congruences. | |
Private Member Functions | |
void | normalize_moduli () |
Adjusts all expressions to have the same moduli. | |
bool | increase_space_dimension (const dimension_type new_space_dim) |
Increase the number of space dimensions to new_space_dim . | |
void | insert_verbatim (const Congruence &cg) |
Inserts in *this an exact copy of the congruence cg , increasing the number of space dimensions if needed. | |
Congruence & | operator[] (dimension_type k) |
Returns the k- th congruence of the system. | |
const Congruence & | operator[] (dimension_type k) const |
Returns a constant reference to the k- th congruence of the system. | |
bool | has_a_free_dimension () const |
Returns true if and only if any of the dimensions in *this is free of constraint. | |
void | affine_preimage (dimension_type v, const Linear_Expression &expr, Coefficient_traits::const_reference denominator) |
Substitutes a given column of coefficients by a given affine expression. | |
void | resize_no_copy (dimension_type new_n_rows, dimension_type new_n_columns) |
Resizes the system without worrying about the old contents. | |
Friends | |
class | const_iterator |
class | Grid |
class | Grid_Certificate |
void | swap (Parma_Polyhedra_Library::Congruence_System &x, Parma_Polyhedra_Library::Congruence_System &y) |
Specializes std::swap . | |
bool | operator== (const Congruence_System &x, const Congruence_System &y) |
Returns true if and only if x and y are equivalent. | |
Related Functions | |
(Note that these are not member functions.) | |
std::ostream & | operator<< (std::ostream &s, const Congruence_System &cgs) |
Output operator. | |
Classes | |
class | const_iterator |
An iterator over a system of congruences. More... |
An object of the class Congruence_System is a system of congruences, i.e., a multiset of objects of the class Congruence. When inserting congruences in a system, space dimensions are automatically adjusted so that all the congruences in the system are defined on the same vector space.
x
and y
are defined as follows: Variable x(0); Variable y(1);
Congruence_System cgs; cgs.insert(x %= 0); cgs.insert(y %= 0);
cgs.insert((x + y %= 1) / 2);
x
and y
values is odd.x
axis: Congruence_System cgs; cgs.insert(x %= 0); cgs.insert((y %= 0) / 0);
Definition at line 127 of file Congruence_System.defs.hh.
Parma_Polyhedra_Library::Congruence_System::Congruence_System | ( | ) | [inline] |
Default constructor: builds an empty system of congruences.
Definition at line 31 of file Congruence_System.inlines.hh.
00032 : Matrix(0, 2) { 00033 }
Parma_Polyhedra_Library::Congruence_System::Congruence_System | ( | const Congruence & | cg | ) | [inline, explicit] |
Builds the singleton system containing only congruence cg
.
Definition at line 36 of file Congruence_System.inlines.hh.
References insert().
Parma_Polyhedra_Library::Congruence_System::Congruence_System | ( | const Constraint & | c | ) | [inline, explicit] |
If c
represents the constraint , builds the singleton system containing only constraint
.
std::invalid_argument | Thrown if c is not an equality constraint. |
Definition at line 42 of file Congruence_System.inlines.hh.
References insert().
Parma_Polyhedra_Library::Congruence_System::Congruence_System | ( | const Constraint_System & | cs | ) | [explicit] |
Builds a system containing copies of any equalities in cs
.
Definition at line 40 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), and insert().
00041 : Matrix(0, 2) { 00042 for (Constraint_System::const_iterator i = cs.begin(), 00043 cs_end = cs.end(); i != cs_end; ++i) 00044 if (i->is_equality()) 00045 insert(*i); 00046 }
Parma_Polyhedra_Library::Congruence_System::Congruence_System | ( | const Congruence_System & | cgs | ) | [inline] |
Ordinary copy-constructor.
Definition at line 48 of file Congruence_System.inlines.hh.
00049 : Matrix(cs) { 00050 }
Parma_Polyhedra_Library::Congruence_System::~Congruence_System | ( | ) | [inline] |
Congruence_System & Parma_Polyhedra_Library::Congruence_System::operator= | ( | const Congruence_System & | cgs | ) | [inline] |
Assignment operator.
Definition at line 57 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::operator=().
00057 { 00058 Matrix::operator=(y); 00059 return *this; 00060 }
dimension_type Parma_Polyhedra_Library::Congruence_System::max_space_dimension | ( | ) | [inline, static] |
Returns the maximum space dimension a Congruence_System can handle.
Definition at line 73 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::max_num_columns().
Referenced by Parma_Polyhedra_Library::Grid::max_space_dimension().
00073 { 00074 return Matrix::max_num_columns() - 2; 00075 }
dimension_type Parma_Polyhedra_Library::Congruence_System::space_dimension | ( | ) | const [inline] |
Returns the dimension of the vector space enclosing *this
.
Definition at line 78 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::num_columns().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_congruences(), Parma_Polyhedra_Library::Grid::add_congruences(), Parma_Polyhedra_Library::Grid::add_recycled_congruences(), Parma_Polyhedra_Library::Grid::add_recycled_congruences_and_minimize(), affine_preimage(), concatenate(), Parma_Polyhedra_Library::Grid::construct(), Parma_Polyhedra_Library::Grid::Grid(), has_a_free_dimension(), increase_space_dimension(), Parma_Polyhedra_Library::Grid::limited_extrapolation_assign(), Parma_Polyhedra_Library::Grid::OK(), satisfies_all_congruences(), Parma_Polyhedra_Library::Grid::select_wider_congruences(), Parma_Polyhedra_Library::Polyhedron::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Grid::throw_dimension_incompatible().
00078 { 00079 return Matrix::num_columns() - 2; 00080 }
bool Parma_Polyhedra_Library::Congruence_System::is_equal_to | ( | const Congruence_System & | cgs | ) | const |
Returns true
if and only if *this
is exactly equal to cgs
.
Definition at line 224 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::num_columns(), and Parma_Polyhedra_Library::Matrix::num_rows().
Referenced by Parma_Polyhedra_Library::Grid::OK().
00224 { 00225 if (num_rows() != cgs.num_rows()) 00226 return false; 00227 00228 for (dimension_type row = 0; row < cgs.num_rows(); ++row) 00229 for (dimension_type col = 0; col < cgs.num_columns(); ++col) { 00230 if (operator[](row)[col] == cgs[row][col]) 00231 continue; 00232 return false; 00233 } 00234 return true; 00235 }
bool Parma_Polyhedra_Library::Congruence_System::has_linear_equalities | ( | ) | const |
Returns true
if and only if *this
contains one or more linear equalities.
Definition at line 238 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::num_columns(), and Parma_Polyhedra_Library::Matrix::num_rows().
00238 { 00239 const Congruence_System& cgs = *this; 00240 dimension_type modulus_index = cgs.num_columns() - 1; 00241 for (dimension_type i = cgs.num_rows(); i-- > 0; ) 00242 if (cgs[i][modulus_index] == 0) 00243 return true; 00244 return false; 00245 }
void Parma_Polyhedra_Library::Congruence_System::clear | ( | ) | [inline] |
Removes all the congruences and sets the space dimension to 0.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 83 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::add_zero_columns(), and Parma_Polyhedra_Library::Matrix::clear().
Referenced by Parma_Polyhedra_Library::Grid::set_zero_dim_univ().
00083 { 00084 Matrix::clear(); 00085 add_zero_columns(2); // Modulus and constant term. 00086 }
void Parma_Polyhedra_Library::Congruence_System::insert | ( | const Congruence & | cg | ) | [inline] |
Inserts in *this
a copy of the congruence cg
, increasing the number of space dimensions if needed.
The copy of cg
will be strongly normalized after being inserted.
Definition at line 89 of file Congruence_System.inlines.hh.
References insert_verbatim(), OK(), operator[](), and Parma_Polyhedra_Library::Matrix::rows.
Referenced by Parma_Polyhedra_Library::Grid::add_congruence(), Congruence_System(), Parma_Polyhedra_Library::Grid::Grid(), Parma_Polyhedra_Library::Grid::intersection_assign(), Parma_Polyhedra_Library::Grid::limited_extrapolation_assign(), and Parma_Polyhedra_Library::Grid::select_wider_congruences().
00089 { 00090 insert_verbatim(cg); 00091 static_cast<Congruence&>(operator[](rows.size()-1)).strong_normalize(); 00092 assert(OK()); 00093 }
void Parma_Polyhedra_Library::Congruence_System::insert | ( | const Constraint & | c | ) |
Inserts in *this
a copy of the equality constraint c
, seen as a modulo 0 congruence, increasing the number of space dimensions if needed.
The modulo 0 congruence will be strongly normalized after being inserted.
std::invalid_argument | Thrown if c is a relation. |
Definition at line 98 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::add_recycled_row(), Parma_Polyhedra_Library::Matrix::add_zero_columns(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), operator[](), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Matrix::rows, Parma_Polyhedra_Library::Constraint::space_dimension(), and Parma_Polyhedra_Library::Matrix::swap_columns().
00098 { 00099 dimension_type cg_size = c.space_dimension() + 2; 00100 const dimension_type old_num_columns = num_columns(); 00101 if (cg_size < old_num_columns) { 00102 // Create a congruence of the required size from `c'. 00103 Congruence cg(c, old_num_columns, row_capacity); 00104 add_recycled_row(cg); 00105 } 00106 else { 00107 if (cg_size > old_num_columns) { 00108 // Resize the system, if necessary. 00109 add_zero_columns(cg_size - old_num_columns); 00110 if (num_rows() != 0) 00111 // Move the moduli to the last column. 00112 swap_columns(old_num_columns - 1, cg_size - 1); 00113 } 00114 Congruence cg(c, cg_size, row_capacity); 00115 add_recycled_row(cg); 00116 } 00117 operator[](rows.size()-1).strong_normalize(); 00118 00119 assert(OK()); 00120 }
void Parma_Polyhedra_Library::Congruence_System::insert | ( | const Congruence_System & | cgs | ) |
Inserts in *this
a copy of the congruences in cgs
, increasing the number of space dimensions if needed.
The inserted copies will be strongly normalized.
Definition at line 154 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::add_zero_rows(), Parma_Polyhedra_Library::Matrix::add_zero_rows_and_columns(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Matrix::row_size, and Parma_Polyhedra_Library::Matrix::swap_columns().
00154 { 00155 Congruence_System& x = *this; 00156 00157 const dimension_type x_n_rows = x.num_rows(); 00158 const dimension_type y_n_rows = y.num_rows(); 00159 const dimension_type old_n_cols = x.num_columns(); 00160 const dimension_type y_n_cols = y.num_columns(); 00161 // Grow to the required size. 00162 if (old_n_cols >= y_n_cols) 00163 add_zero_rows(y_n_rows, Row::Flags()); 00164 else { 00165 add_zero_rows_and_columns(y_n_rows, 00166 y_n_cols - old_n_cols, 00167 Row::Flags()); 00168 // Swap the modulus column into the new last column. 00169 swap_columns(old_n_cols - 1, num_columns() - 1); 00170 } 00171 00172 // Copy the rows of `y', forcing size and capacity. 00173 const dimension_type x_mod_index = x.num_columns() - 1; 00174 const dimension_type y_mod_index = y_n_cols - 1; 00175 for (dimension_type i = y_n_rows; i-- > 0; ) { 00176 Row copy(y[i], x.row_size, x.row_capacity); 00177 // Swap the modulus to the correct column. 00178 std::swap(copy[x_mod_index], copy[y_mod_index]); 00179 std::swap(copy, x[x_n_rows+i]); 00180 } 00181 assert(OK()); 00182 }
void Parma_Polyhedra_Library::Congruence_System::recycling_insert | ( | Congruence_System & | cgs | ) |
Inserts into *this
the congruences in cgs
, increasing the number of space dimensions if needed.
Definition at line 123 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::add_zero_rows(), Parma_Polyhedra_Library::Matrix::add_zero_rows_and_columns(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), operator[](), and Parma_Polyhedra_Library::Matrix::swap_columns().
Referenced by Parma_Polyhedra_Library::Grid::add_recycled_congruences(), and Parma_Polyhedra_Library::Grid::add_recycled_congruences_and_minimize().
00123 { 00124 const dimension_type old_num_rows = num_rows(); 00125 const dimension_type cgs_num_rows = cgs.num_rows(); 00126 const dimension_type old_num_cols = num_columns(); 00127 dimension_type cgs_num_cols = cgs.num_columns(); 00128 if (old_num_cols >= cgs_num_cols) 00129 add_zero_rows(cgs_num_rows, Row::Flags()); 00130 else { 00131 add_zero_rows_and_columns(cgs_num_rows, 00132 cgs_num_cols - old_num_cols, 00133 Row::Flags()); 00134 // Swap the modulus column into the new last column. 00135 swap_columns(old_num_cols - 1, num_columns() - 1); 00136 } 00137 --cgs_num_cols; // Convert to modulus index. 00138 const dimension_type mod_index = num_columns() - 1; 00139 for (dimension_type i = cgs_num_rows; i-- > 0; ) { 00140 // Swap one coefficient at a time into the newly added rows, instead 00141 // of swapping each entire row. This ensures that the added rows 00142 // have the same capacities as the existing rows. 00143 Congruence& new_cg = operator[](old_num_rows + i); 00144 Congruence& old_cg = cgs[i]; 00145 for (dimension_type j = cgs_num_cols; j-- > 0; ) 00146 std::swap(new_cg[j], old_cg[j]); 00147 std::swap(new_cg[mod_index], old_cg[cgs_num_cols]); // Modulus. 00148 } 00149 00150 assert(OK()); 00151 }
const Congruence_System & Parma_Polyhedra_Library::Congruence_System::zero_dim_empty | ( | ) | [inline, static] |
Returns the system containing only Congruence::zero_dim_false().
Definition at line 102 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Congruence::zero_dim_false().
00102 { 00103 static const Congruence_System zdf(Congruence::zero_dim_false()); 00104 return zdf; 00105 }
Congruence_System::const_iterator Parma_Polyhedra_Library::Congruence_System::begin | ( | ) | const [inline] |
Returns the const_iterator pointing to the first congruence, if this
is not empty; otherwise, returns the past-the-end const_iterator.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 170 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::begin().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_congruences(), Parma_Polyhedra_Library::Grid::add_recycled_congruences(), Parma_Polyhedra_Library::Grid::add_recycled_congruences_and_minimize(), Parma_Polyhedra_Library::Grid::expand_space_dimension(), Parma_Polyhedra_Library::Grid::grid_difference_assign(), and operator<<().
00170 { 00171 const_iterator i(Matrix::begin(), *this); 00172 i.skip_forward(); 00173 return i; 00174 }
Congruence_System::const_iterator Parma_Polyhedra_Library::Congruence_System::end | ( | ) | const [inline] |
Returns the past-the-end const_iterator.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 177 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::end().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_congruences(), Parma_Polyhedra_Library::Grid::add_recycled_congruences(), Parma_Polyhedra_Library::Grid::add_recycled_congruences_and_minimize(), Parma_Polyhedra_Library::Grid::expand_space_dimension(), Parma_Polyhedra_Library::Grid::grid_difference_assign(), and operator<<().
00177 { 00178 const const_iterator i(Matrix::end(), *this); 00179 return i; 00180 }
bool Parma_Polyhedra_Library::Congruence_System::OK | ( | ) | const |
Checks if all the invariants are satisfied.
Returns true
if and only if *this
is a valid Matrix, each row in the system is a valid Congruence and the number of columns is consistent with the number of congruences.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 428 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Congruence::OK(), and Parma_Polyhedra_Library::Matrix::OK().
Referenced by ascii_load(), increase_space_dimension(), insert(), insert_verbatim(), normalize_moduli(), Parma_Polyhedra_Library::Grid::OK(), recycling_insert(), and Parma_Polyhedra_Library::Grid::simplify().
00428 { 00429 // A Congruence_System must be a valid Matrix. 00430 if (!Matrix::OK()) 00431 return false; 00432 00433 if (num_rows()) { 00434 if (num_columns() < 2) { 00435 #ifndef NDEBUG 00436 std::cerr << "Congruence_System has rows and fewer than two columns." 00437 << std::endl; 00438 #endif 00439 return false; 00440 } 00441 } 00442 00443 // Checking each congruence in the system. 00444 const Congruence_System& x = *this; 00445 for (dimension_type i = num_rows(); i-- > 0; ) { 00446 const Congruence& cg = x[i]; 00447 if (!cg.OK()) 00448 return false; 00449 } 00450 00451 // All checks passed. 00452 return true; 00453 }
void Parma_Polyhedra_Library::Congruence_System::ascii_dump | ( | ) | const |
Writes to std::cerr
an ASCII representation of *this
.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Referenced by Parma_Polyhedra_Library::Grid::ascii_dump(), ascii_dump(), Parma_Polyhedra_Library::Grid::conversion(), Parma_Polyhedra_Library::Grid::OK(), and Parma_Polyhedra_Library::Grid::simplify().
void Parma_Polyhedra_Library::Congruence_System::ascii_dump | ( | std::ostream & | s | ) | const |
Writes to s
an ASCII representation of *this
.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 392 of file Congruence_System.cc.
References ascii_dump(), Parma_Polyhedra_Library::Matrix::num_columns(), and Parma_Polyhedra_Library::Matrix::num_rows().
00392 { 00393 const Congruence_System& x = *this; 00394 dimension_type x_num_rows = x.num_rows(); 00395 dimension_type x_num_columns = x.num_columns(); 00396 s << x_num_rows << " x " << x_num_columns 00397 << std::endl; 00398 if (x_num_rows && x_num_columns) 00399 for (dimension_type i = 0; i < x_num_rows; ++i) 00400 x[i].ascii_dump(s); 00401 }
void Parma_Polyhedra_Library::Congruence_System::print | ( | ) | const |
bool Parma_Polyhedra_Library::Congruence_System::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.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 406 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::num_rows(), OK(), and resize_no_copy().
Referenced by Parma_Polyhedra_Library::Grid::ascii_load().
00406 { 00407 std::string str; 00408 dimension_type nrows; 00409 dimension_type ncols; 00410 if (!(s >> nrows)) 00411 return false; 00412 if (!(s >> str)) 00413 return false; 00414 if (!(s >> ncols)) 00415 return false; 00416 resize_no_copy(nrows, ncols); 00417 00418 Congruence_System& x = *this; 00419 for (dimension_type i = 0; i < x.num_rows(); ++i) 00420 x[i].ascii_load(s); 00421 00422 // Check for well-formedness. 00423 assert(OK()); 00424 return true; 00425 }
memory_size_type Parma_Polyhedra_Library::Congruence_System::total_memory_in_bytes | ( | ) | const [inline] |
Returns the total size in bytes of the memory occupied by *this
.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 193 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Checked::total_memory_in_bytes().
00193 { 00194 return Matrix::total_memory_in_bytes(); 00195 }
memory_size_type Parma_Polyhedra_Library::Congruence_System::external_memory_in_bytes | ( | ) | const [inline] |
Returns the size in bytes of the memory managed by *this
.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 188 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Checked::external_memory_in_bytes().
Referenced by Parma_Polyhedra_Library::Grid::external_memory_in_bytes().
00188 { 00189 return Matrix::external_memory_in_bytes(); 00190 }
PPL::dimension_type Parma_Polyhedra_Library::Congruence_System::num_equalities | ( | ) | const |
Returns the number of equalities.
Definition at line 255 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::num_rows().
Referenced by Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate(), Parma_Polyhedra_Library::Grid::quick_equivalence_test(), and Parma_Polyhedra_Library::Grid::widening_assign().
00255 { 00256 const Congruence_System& cgs = *this; 00257 dimension_type n = 0; 00258 for (dimension_type i = num_rows(); i-- > 0 ; ) 00259 if (cgs[i].is_equality()) 00260 ++n; 00261 return n; 00262 }
PPL::dimension_type Parma_Polyhedra_Library::Congruence_System::num_proper_congruences | ( | ) | const |
Returns the number of proper congruences.
Definition at line 265 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Congruence::is_proper_congruence(), and Parma_Polyhedra_Library::Matrix::num_rows().
Referenced by Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate().
00265 { 00266 const Congruence_System& cgs = *this; 00267 dimension_type n = 0; 00268 for (dimension_type i = num_rows(); i-- > 0 ; ) { 00269 const Congruence& cg = cgs[i]; 00270 if (cg.is_proper_congruence()) 00271 ++n; 00272 } 00273 return n; 00274 }
void Parma_Polyhedra_Library::Congruence_System::swap | ( | Congruence_System & | cgs | ) | [inline] |
Swaps *this
with y
.
Definition at line 183 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::swap().
Referenced by Parma_Polyhedra_Library::Grid::Grid().
00183 { 00184 Matrix::swap(y); 00185 }
void Parma_Polyhedra_Library::Congruence_System::add_unit_rows_and_columns | ( | dimension_type | dims | ) |
Adds dims
rows and dims
columns of zeroes to the matrix, initializing the added rows as in the unit congruence system.
dims | The number of rows and columns to be added: must be strictly positive. |
Definition at line 490 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::add_zero_rows_and_columns(), Parma_Polyhedra_Library::Linear_Row::LINE_OR_EQUALITY, Parma_Polyhedra_Library::NECESSARILY_CLOSED, Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), and Parma_Polyhedra_Library::Matrix::swap_columns().
Referenced by Parma_Polyhedra_Library::Grid::add_space_dimensions(), and Parma_Polyhedra_Library::Grid::add_space_dimensions_and_project().
00490 { 00491 assert(num_columns() > 0); 00492 dimension_type col = num_columns() - 1; 00493 dimension_type old_num_rows = num_rows(); 00494 add_zero_rows_and_columns(dims, dims, 00495 Linear_Row::Flags(NECESSARILY_CLOSED, 00496 Linear_Row::LINE_OR_EQUALITY)); 00497 // Swap the modulus column into the new last column. 00498 swap_columns(col, col + dims); 00499 00500 // Swap the added columns to the front of the matrix. 00501 for (dimension_type row = old_num_rows; row-- > 0; ) 00502 std::swap(operator[](row), operator[](row + dims)); 00503 00504 col += dims - 1; 00505 // Set the diagonal element of each added row. 00506 for (dimension_type row = 0; row < dims; ++row) 00507 const_cast<Coefficient&>(operator[](row)[col - row]) = 1; 00508 }
void Parma_Polyhedra_Library::Congruence_System::concatenate | ( | const Congruence_System & | cgs | ) |
Concatenates copies of the congruences from cgs
onto *this
.
The matrix for the new system of congruences is obtained by leaving the old system in the upper left-hand side and placing the congruences of cgs
in the lower right-hand side, and padding with zeroes.
Definition at line 511 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::add_zero_rows_and_columns(), increase_space_dimension(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), operator[](), and space_dimension().
Referenced by Parma_Polyhedra_Library::Grid::concatenate_assign().
00511 { 00512 // TODO: this implementation is just an executable specification. 00513 Congruence_System cgs = const_cgs; 00514 00515 dimension_type added_rows = cgs.num_rows(); 00516 dimension_type added_columns = cgs.space_dimension(); 00517 00518 if (added_rows == 0) { 00519 increase_space_dimension(space_dimension() + added_columns); 00520 return; 00521 } 00522 00523 dimension_type old_num_rows = num_rows(); 00524 dimension_type old_modi = num_columns() - 1; 00525 dimension_type old_space_dim = space_dimension(); 00526 00527 add_zero_rows_and_columns(added_rows, added_columns, 00528 Row::Flags()); 00529 00530 dimension_type cgs_num_columns = cgs.num_columns(); 00531 dimension_type modi = num_columns() - 1; 00532 00533 // Swap the modulus and the new last column, in the old rows. 00534 for (dimension_type i = 0; i < old_num_rows; ++i) { 00535 Congruence& cg = operator[](i); 00536 std::swap(cg[old_modi], cg[modi]); 00537 } 00538 00539 // Move the congruences into *this from `cgs', shifting the 00540 // coefficients along into the appropriate columns. 00541 for (dimension_type i = added_rows; i-- > 0; ) { 00542 Congruence& cg_old = cgs[i]; 00543 Congruence& cg_new = operator[](old_num_rows + i); 00544 // The inhomogeneous term is moved to the same column. 00545 std::swap(cg_new[0], cg_old[0]); 00546 // All homogeneous terms are shifted by `space_dim' columns. 00547 for (dimension_type j = 1; j < cgs_num_columns; ++j) 00548 std::swap(cg_old[j], cg_new[old_space_dim + j]); 00549 } 00550 }
bool Parma_Polyhedra_Library::Congruence_System::satisfies_all_congruences | ( | const Grid_Generator & | g | ) | const [protected] |
Returns true
if g
satisfies all the congruences.
Definition at line 278 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Scalar_Products::assign(), Parma_Polyhedra_Library::Grid_Generator::divisor(), Parma_Polyhedra_Library::Congruence::is_equality(), Parma_Polyhedra_Library::Grid_Generator::is_line(), Parma_Polyhedra_Library::Congruence::modulus(), space_dimension(), Parma_Polyhedra_Library::Grid_Generator::space_dimension(), and TEMP_INTEGER.
Referenced by Parma_Polyhedra_Library::Grid::is_included_in(), Parma_Polyhedra_Library::Grid::is_universe(), and Parma_Polyhedra_Library::Grid::relation_with().
00278 { 00279 assert(g.space_dimension() <= space_dimension()); 00280 00281 const Congruence_System& cgs = *this; 00282 TEMP_INTEGER(sp); 00283 if (g.is_line()) 00284 for (dimension_type i = cgs.num_rows(); i-- > 0; ) { 00285 const Congruence& cg = cgs[i]; 00286 Scalar_Products::assign(sp, g, cg); 00287 if (sp != 0) 00288 return false; 00289 } 00290 else { 00291 const Coefficient& divisor = g.divisor(); 00292 for (dimension_type i = cgs.num_rows(); i-- > 0; ) { 00293 const Congruence& cg = cgs[i]; 00294 Scalar_Products::assign(sp, g, cg); 00295 if (cg.is_equality()) { 00296 if (sp != 0) 00297 return false; 00298 } 00299 else if (sp % (cg.modulus() * divisor) != 0) 00300 return false; 00301 } 00302 } 00303 return true; 00304 }
void Parma_Polyhedra_Library::Congruence_System::normalize_moduli | ( | ) | [private] |
Adjusts all expressions to have the same moduli.
Definition at line 185 of file Congruence_System.cc.
References Parma_Polyhedra_Library::lcm_assign(), Parma_Polyhedra_Library::Congruence::modulus(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), operator[](), Parma_Polyhedra_Library::Matrix::row_size, Parma_Polyhedra_Library::Row::size(), and TEMP_INTEGER.
Referenced by Parma_Polyhedra_Library::Grid::construct(), and Parma_Polyhedra_Library::Grid::simplify().
00185 { 00186 dimension_type row = num_rows(); 00187 if (row > 0) { 00188 // Calculate the LCM of all the moduli. 00189 TEMP_INTEGER(lcm); 00190 // Find last proper congruence. 00191 while (true) { 00192 lcm = operator[](--row).modulus(); 00193 if (lcm > 0) 00194 break; 00195 if (row == 0) 00196 // All rows are equalities. 00197 return; 00198 } 00199 while (row > 0) { 00200 TEMP_INTEGER(modulus); 00201 modulus = operator[](--row).modulus(); 00202 if (modulus > 0) 00203 lcm_assign(lcm, lcm, modulus); 00204 } 00205 00206 // Represent every row using the LCM as the modulus. 00207 dimension_type row_size = operator[](0).size(); 00208 for (dimension_type row = num_rows(); row-- > 0; ) { 00209 TEMP_INTEGER(modulus); 00210 modulus = operator[](row).modulus(); 00211 if (modulus <= 0 || modulus == lcm) 00212 continue; 00213 TEMP_INTEGER(factor); 00214 factor = lcm / modulus; 00215 for (dimension_type col = row_size; col-- > 0; ) 00216 operator[](row)[col] *= factor; 00217 operator[](row)[row_size-1] = lcm; 00218 } 00219 } 00220 assert(OK()); 00221 }
bool Parma_Polyhedra_Library::Congruence_System::increase_space_dimension | ( | const dimension_type | new_space_dim | ) | [private] |
Increase the number of space dimensions to new_space_dim
.
new_space_dim
must at least equal to the current space dimension.
Definition at line 50 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::add_zero_columns(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), space_dimension(), and Parma_Polyhedra_Library::Matrix::swap_columns().
Referenced by concatenate(), Parma_Polyhedra_Library::Grid::Grid(), Parma_Polyhedra_Library::Grid::minimized_congruences(), and Parma_Polyhedra_Library::Grid::set_empty().
00050 { 00051 assert(space_dimension() <= new_space_dim); 00052 00053 dimension_type cols_to_add = new_space_dim - space_dimension(); 00054 00055 if (cols_to_add) 00056 if (num_rows()) { 00057 dimension_type old_num_cols = num_columns(); 00058 add_zero_columns(cols_to_add); 00059 // Move the moduli. 00060 swap_columns(num_columns() - 1, old_num_cols - 1); 00061 } 00062 else 00063 // Empty system. 00064 add_zero_columns(cols_to_add); 00065 00066 assert(OK()); 00067 return true; 00068 }
void Parma_Polyhedra_Library::Congruence_System::insert_verbatim | ( | const Congruence & | cg | ) | [private] |
Inserts in *this
an exact copy of the congruence cg
, increasing the number of space dimensions if needed.
This method inserts a copy of cg
in the given form, instead of first strong normalizing cg
as insert would do.
Definition at line 71 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::add_recycled_row(), Parma_Polyhedra_Library::Matrix::add_row(), Parma_Polyhedra_Library::Matrix::add_zero_columns(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Row::size(), and Parma_Polyhedra_Library::Matrix::swap_columns().
Referenced by Parma_Polyhedra_Library::Grid::expand_space_dimension(), and insert().
00071 { 00072 const dimension_type old_num_columns = num_columns(); 00073 const dimension_type cg_size = cg.size(); 00074 00075 if (cg_size > old_num_columns) { 00076 // Resize the system, if necessary. 00077 add_zero_columns(cg_size - old_num_columns); 00078 if (num_rows() != 0) 00079 // Move the moduli to the last column. 00080 swap_columns(old_num_columns - 1, cg_size - 1); 00081 add_row(cg); 00082 } 00083 else if (cg_size < old_num_columns) { 00084 // Create a resized copy of `cg'. 00085 Congruence rc(cg, old_num_columns, row_capacity); 00086 // Move the modulus to its place. 00087 std::swap(rc[cg_size - 1], rc[old_num_columns - 1]); 00088 add_recycled_row(rc); 00089 } 00090 else 00091 // Here cg_size == old_num_columns. 00092 add_row(cg); 00093 00094 assert(OK()); 00095 }
Congruence & Parma_Polyhedra_Library::Congruence_System::operator[] | ( | dimension_type | k | ) | [inline, private] |
Returns the k-
th congruence of the system.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 63 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::operator[]().
Referenced by concatenate(), has_a_free_dimension(), insert(), normalize_moduli(), and recycling_insert().
00063 { 00064 return static_cast<Congruence&>(Matrix::operator[](k)); 00065 }
const Congruence & Parma_Polyhedra_Library::Congruence_System::operator[] | ( | dimension_type | k | ) | const [inline, private] |
Returns a constant reference to the k-
th congruence of the system.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 68 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::operator[]().
00068 { 00069 return static_cast<const Congruence&>(Matrix::operator[](k)); 00070 }
bool Parma_Polyhedra_Library::Congruence_System::has_a_free_dimension | ( | ) | const [private] |
Returns true
if and only if any of the dimensions in *this
is free of constraint.
Any equality or proper congruence affecting a dimension constrains that dimension.
This method assumes the system is in minimal form.
Definition at line 307 of file Congruence_System.cc.
References Parma_Polyhedra_Library::Matrix::num_rows(), operator[](), and space_dimension().
Referenced by Parma_Polyhedra_Library::Grid::is_discrete().
00307 { 00308 // Search for a dimension that is free of any congruence or equality 00309 // constraint. Assumes a minimized system. 00310 dimension_type space_dim = space_dimension(); 00311 std::vector<bool> free_dim(space_dim, true); 00312 dimension_type free_dims = space_dim; 00313 for (dimension_type row = num_rows(); row-- > 0; ) { 00314 const Congruence& cg = operator[](row); 00315 for (dimension_type dim = 0; dim < space_dim; ++dim) 00316 if (free_dim[dim] && cg[dim+1] != 0) { 00317 if (--free_dims == 0) { 00318 // All dimensions are constrained. 00319 #ifndef NDEBUG 00320 free_dim[dim] = false; 00321 // Check that there are free_dims dimensions marked free 00322 // in free_dim. 00323 dimension_type count = 0; 00324 for (dimension_type dim = 0; dim < space_dim; ++dim) 00325 count += free_dim[dim]; 00326 assert(count == free_dims); 00327 #endif 00328 return true; 00329 } 00330 free_dim[dim] = false; 00331 } 00332 } 00333 // At least one dimension is free of constraint. 00334 return false; 00335 }
void Parma_Polyhedra_Library::Congruence_System::affine_preimage | ( | dimension_type | v, | |
const Linear_Expression & | expr, | |||
Coefficient_traits::const_reference | denominator | |||
) | [private] |
Substitutes a given column of coefficients by a given affine expression.
v | Index of the column to which the affine transformation is substituted; | |
expr | The numerator of the affine transformation: ![]() | |
denominator | The denominator of the affine transformation. |
denominator
that will be used as denominator of the affine transformation. The denominator is required to be a positive integer and its default value is 1.
The affine transformation substitutes the matrix of congruences by a new matrix whose elements are built from the old one
as follows:
expr
is a constant parameter and unaltered by this computation.
Definition at line 339 of file Congruence_System.cc.
References Parma_Polyhedra_Library::add_mul_assign(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Row::size(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), and space_dimension().
Referenced by Parma_Polyhedra_Library::Grid::affine_image(), and Parma_Polyhedra_Library::Grid::affine_preimage().
00341 { 00342 // `v' is the index of a column corresponding to a "user" variable 00343 // (i.e., it cannot be the inhomogeneous term). 00344 assert(v > 0 && v <= space_dimension()); 00345 assert(expr.space_dimension() <= space_dimension()); 00346 assert(denominator > 0); 00347 00348 const dimension_type n_columns = num_columns(); 00349 const dimension_type n_rows = num_rows(); 00350 const dimension_type expr_size = expr.size(); 00351 const bool not_invertible = (v >= expr_size || expr[v] == 0); 00352 Congruence_System& x = *this; 00353 00354 if (denominator == 1) 00355 // Optimized computation only considering columns having indexes < 00356 // expr_size. 00357 for (dimension_type i = n_rows; i-- > 0; ) { 00358 Congruence& row = x[i]; 00359 Coefficient& row_v = row[v]; 00360 if (row_v != 0) { 00361 for (dimension_type j = expr_size; j-- > 0; ) 00362 if (j != v) 00363 // row[j] = row[j] + row_v * expr[j] 00364 add_mul_assign(row[j], row_v, expr[j]); 00365 if (not_invertible) 00366 row_v = 0; 00367 else 00368 row_v *= expr[v]; 00369 } 00370 } 00371 else 00372 for (dimension_type i = n_rows; i-- > 0; ) { 00373 Congruence& row = x[i]; 00374 Coefficient& row_v = row[v]; 00375 if (row_v != 0) { 00376 for (dimension_type j = n_columns; j-- > 0; ) 00377 if (j != v) { 00378 Coefficient& row_j = row[j]; 00379 row_j *= denominator; 00380 if (j < expr_size) 00381 add_mul_assign(row_j, row_v, expr[j]); 00382 } 00383 if (not_invertible) 00384 row_v = 0; 00385 else 00386 row_v *= expr[v]; 00387 } 00388 } 00389 }
void Parma_Polyhedra_Library::Congruence_System::resize_no_copy | ( | dimension_type | new_n_rows, | |
dimension_type | new_n_columns | |||
) | [inline, private] |
Resizes the system without worrying about the old contents.
new_n_rows | The number of rows of the resized system; | |
new_n_columns | The number of columns of the resized system. |
Definition at line 96 of file Congruence_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::resize_no_copy().
Referenced by ascii_load(), and Parma_Polyhedra_Library::Grid::conversion().
00097 { 00098 Matrix::resize_no_copy(new_n_rows, new_n_columns, Row::Flags()); 00099 }
friend class const_iterator [friend] |
Definition at line 392 of file Congruence_System.defs.hh.
friend class Grid [friend] |
Definition at line 394 of file Congruence_System.defs.hh.
friend class Grid_Certificate [friend] |
Definition at line 395 of file Congruence_System.defs.hh.
void swap | ( | Parma_Polyhedra_Library::Congruence_System & | x, | |
Parma_Polyhedra_Library::Congruence_System & | y | |||
) | [friend] |
Specializes std::swap
.
Definition at line 204 of file Congruence_System.inlines.hh.
00205 { 00206 x.swap(y); 00207 }
bool operator== | ( | const Congruence_System & | x, | |
const Congruence_System & | y | |||
) | [friend] |
Returns true
if and only if x
and y
are equivalent.
Definition at line 474 of file Congruence_System.cc.
00474 { 00475 if (x.num_columns() == y.num_columns()) { 00476 dimension_type num_rows = x.num_rows(); 00477 if (num_rows == y.num_rows()) { 00478 while (num_rows--) { 00479 if (x[num_rows] == y[num_rows]) 00480 continue; 00481 return false; 00482 } 00483 return true; 00484 } 00485 } 00486 return false; 00487 }
std::ostream & operator<< | ( | std::ostream & | s, | |
const Congruence_System & | cgs | |||
) | [related] |
Output operator.
Writes true
if cgs
is empty. Otherwise, writes on s
the congruences of cgs
, all in one row and separated by ", ".
Definition at line 457 of file Congruence_System.cc.
References begin(), end(), and Parma_Polyhedra_Library::Congruence::strong_normalize().
00457 { 00458 Congruence_System::const_iterator i = cgs.begin(); 00459 const Congruence_System::const_iterator cgs_end = cgs.end(); 00460 if (i == cgs_end) 00461 return s << "true"; 00462 while (true) { 00463 Congruence cg = *i++; 00464 cg.strong_normalize(); 00465 s << cg; 00466 if (i == cgs_end) 00467 return s; 00468 s << ", "; 00469 } 00470 }