#include <Linear_System.defs.hh>
Public Member Functions | |
Linear_System (Topology topol) | |
Builds an empty linear system with specified topology. | |
Linear_System (Topology topol, dimension_type n_rows, dimension_type n_columns) | |
Builds a system with specified topology and dimensions. | |
Linear_System (const Linear_System &y) | |
Copy-constructor: pending rows are transformed into non-pending ones. | |
Linear_System (const Linear_System &y, With_Pending) | |
Full copy-constructor: pending rows are copied as pending. | |
Linear_System & | operator= (const Linear_System &y) |
Assignment operator: pending rows are transformed into non-pending ones. | |
void | assign_with_pending (const Linear_System &y) |
Full assignment operator: pending rows are copied as pending. | |
void | swap (Linear_System &y) |
Swaps *this with y . | |
dimension_type | space_dimension () const |
Returns the space dimension of the rows in the system. | |
void | remove_trailing_columns (dimension_type n) |
Makes the system shrink by removing its n trailing columns. | |
void | permute_columns (const std::vector< dimension_type > &cycles) |
Permutes the columns of the system. | |
void | strong_normalize () |
Strongly normalizes the system. | |
void | sign_normalize () |
Sign-normalizes the system. | |
bool | check_sorted () const |
Returns true if and only if *this is sorted, without checking for duplicates. | |
void | set_necessarily_closed () |
Sets the system topology to NECESSARILY_CLOSED . | |
void | set_not_necessarily_closed () |
Sets the system topology to NOT_NECESSARILY_CLOSED . | |
void | set_rows_topology () |
Sets the topology of all rows equal to the system topology. | |
void | unset_pending_rows () |
Sets the index to indicate that the system has no pending rows. | |
void | set_index_first_pending_row (dimension_type i) |
Sets the index of the first pending row to i . | |
void | set_sorted (bool b) |
Sets the sortedness flag of the system to b . | |
void | resize_no_copy (dimension_type new_n_rows, dimension_type new_n_columns) |
Resizes the system without worrying about the old contents. | |
void | add_rows_and_columns (dimension_type n) |
Adds n rows and columns to the system. | |
void | insert (const Linear_Row &r) |
Adds a copy of r to the system, automatically resizing the system or the row's copy, if needed. | |
void | insert_pending (const Linear_Row &r) |
Adds a copy of the given row to the pending part of the system, automatically resizing the system or the row, if needed. | |
void | add_row (const Linear_Row &r) |
Adds a copy of the given row to the system. | |
void | add_pending_row (Linear_Row::Flags flags) |
Adds a new empty row to the system, setting only its flags. | |
void | add_pending_row (const Linear_Row &r) |
Adds a copy of the given row to the pending part of the system. | |
void | add_rows (const Linear_System &y) |
Adds to *this a copy of the rows of `y'. | |
void | add_pending_rows (const Linear_System &y) |
Adds a copy of the rows of `y' to the pending part of `*this'. | |
void | sort_rows () |
Sorts the non-pending rows (in growing order) and eliminates duplicated ones. | |
void | sort_rows (dimension_type first_row, dimension_type last_row) |
Sorts the rows (in growing order) form first_row to last_row and eliminates duplicated ones. | |
void | merge_rows_assign (const Linear_System &y) |
Assigns to *this the result of merging its rows with those of y , obtaining a sorted system. | |
void | sort_pending_and_remove_duplicates () |
Sorts the pending rows and eliminates those that also occur in the non-pending part of the system. | |
void | sort_and_remove_with_sat (Bit_Matrix &sat) |
Sorts the system, removing duplicates, keeping the saturation matrix consistent. | |
dimension_type | gauss (dimension_type n_lines_or_equalities) |
Minimizes the subsystem of equations contained in *this . | |
void | back_substitute (dimension_type n_lines_or_equalities) |
Back-substitutes the coefficients to reduce the complexity of the system. | |
void | simplify () |
Applies Gaussian elimination and back-substitution so as to simplify the linear system. | |
void | normalize () |
Normalizes the system by dividing each row for the GCD of the row's elements. | |
void | clear () |
Clears the system deallocating all its rows. | |
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(std::ostream&) const) 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 | OK (bool check_strong_normalized=true) const |
Checks if all the invariants are satisfied. | |
Subscript operators | |
Linear_Row & | operator[] (dimension_type k) |
Returns a reference to the k-th row of the system. | |
const Linear_Row & | operator[] (dimension_type k) const |
Returns a constant reference to the k-th row of the system. | |
Accessors | |
Topology | topology () const |
Returns the system topology. | |
bool | is_sorted () const |
Returns the value of the sortedness flag. | |
bool | is_necessarily_closed () const |
Returns true if and only if the system topology is NECESSARILY_CLOSED . | |
dimension_type | num_lines_or_equalities () const |
Returns the number of rows in the system that represent either lines or equalities. | |
dimension_type | first_pending_row () const |
Returns the index of the first pending row. | |
dimension_type | num_pending_rows () const |
Returns the number of rows that are in the pending part of the system. | |
Static Public Member Functions | |
static dimension_type | max_space_dimension () |
Returns the maximum space dimension a Linear_System can handle. | |
Private Attributes | |
Topology | row_topology |
The topological kind of the rows in the system. | |
dimension_type | index_first_pending |
The index of the first pending row. | |
bool | sorted |
true if rows are sorted in the ascending order as defined by bool compare(const Linear_Row&, const Linear_Row&) . If false may not be sorted. | |
Related Functions | |
(Note that these are not member functions.) | |
void | swap (Parma_Polyhedra_Library::Linear_System &x, Parma_Polyhedra_Library::Linear_System &y) |
Specializes std::swap . | |
bool | operator== (const Linear_System &x, const Linear_System &y) |
Returns true if and only if x and y are identical. | |
bool | operator!= (const Linear_System &x, const Linear_System &y) |
Returns true if and only if x and y are different. | |
Classes | |
struct | Row_Less_Than |
Ordering predicate (used when implementing the sort algorithm). More... | |
class | With_Bit_Matrix_iterator |
An iterator keeping a Linear_System consistent with a Bit_Matrix. More... | |
struct | With_Pending |
A tag class. More... |
An object of this class represents either a constraint system or a generator system. Each Linear_System object can be viewed as a finite sequence of strong-normalized Linear_Row objects, where each Linear_Row implements a constraint or a generator. Linear systems are characterized by the matrix of coefficients, also encoding the number, size and capacity of Linear_row objects, as well as a few additional information, including:
true
, ensures that the non-pending prefix of the sequence of rows is sorted. Definition at line 54 of file Linear_System.defs.hh.
Parma_Polyhedra_Library::Linear_System::Linear_System | ( | Topology | topol | ) | [inline] |
Builds an empty linear system with specified topology.
Rows size and capacity are initialized to .
Definition at line 56 of file Linear_System.inlines.hh.
00057 : Matrix(), 00058 row_topology(topol), 00059 index_first_pending(0), 00060 sorted(true) { 00061 }
Parma_Polyhedra_Library::Linear_System::Linear_System | ( | Topology | topol, | |
dimension_type | n_rows, | |||
dimension_type | n_columns | |||
) | [inline] |
Builds a system with specified topology and dimensions.
topol | The topology of the system that will be created; | |
n_rows | The number of rows of the system that will be created; | |
n_columns | The number of columns of the system that will be created. |
n_rows
n_columns
system whose coefficients are all zero and whose rows are all initialized to be of the given topology.
Definition at line 64 of file Linear_System.inlines.hh.
00066 : Matrix(n_rows, n_columns, Linear_Row::Flags(topol)), 00067 row_topology(topol), 00068 index_first_pending(n_rows), 00069 sorted(true) { 00070 }
Parma_Polyhedra_Library::Linear_System::Linear_System | ( | const Linear_System & | y | ) | [inline] |
Copy-constructor: pending rows are transformed into non-pending ones.
Definition at line 94 of file Linear_System.inlines.hh.
References num_pending_rows(), sorted, and unset_pending_rows().
00095 : Matrix(y), 00096 row_topology(y.row_topology) { 00097 unset_pending_rows(); 00098 // Previously pending rows may violate sortedness. 00099 sorted = (y.num_pending_rows() > 0) ? false : y.sorted; 00100 assert(num_pending_rows() == 0); 00101 }
Parma_Polyhedra_Library::Linear_System::Linear_System | ( | const Linear_System & | y, | |
With_Pending | ||||
) | [inline] |
Full copy-constructor: pending rows are copied as pending.
Definition at line 104 of file Linear_System.inlines.hh.
00105 : Matrix(y), 00106 row_topology(y.row_topology), 00107 index_first_pending(y.index_first_pending), 00108 sorted(y.sorted) { 00109 }
Linear_System & Parma_Polyhedra_Library::Linear_System::operator= | ( | const Linear_System & | y | ) | [inline] |
Assignment operator: pending rows are transformed into non-pending ones.
Definition at line 112 of file Linear_System.inlines.hh.
References num_pending_rows(), Parma_Polyhedra_Library::Matrix::operator=(), row_topology, sorted, and unset_pending_rows().
Referenced by Parma_Polyhedra_Library::Generator_System::operator=(), and Parma_Polyhedra_Library::Constraint_System::operator=().
00112 { 00113 Matrix::operator=(y); 00114 row_topology = y.row_topology; 00115 unset_pending_rows(); 00116 // Previously pending rows may violate sortedness. 00117 sorted = (y.num_pending_rows() > 0) ? false : y.sorted; 00118 assert(num_pending_rows() == 0); 00119 return *this; 00120 }
void Parma_Polyhedra_Library::Linear_System::assign_with_pending | ( | const Linear_System & | y | ) | [inline] |
Full assignment operator: pending rows are copied as pending.
Definition at line 123 of file Linear_System.inlines.hh.
References index_first_pending, Parma_Polyhedra_Library::Matrix::operator=(), row_topology, and sorted.
Referenced by Parma_Polyhedra_Library::Polyhedron::operator=(), and Parma_Polyhedra_Library::Polyhedron::Polyhedron().
00123 { 00124 Matrix::operator=(y); 00125 row_topology = y.row_topology; 00126 index_first_pending = y.index_first_pending; 00127 sorted = y.sorted; 00128 }
void Parma_Polyhedra_Library::Linear_System::swap | ( | Linear_System & | y | ) | [inline] |
Swaps *this
with y
.
Definition at line 131 of file Linear_System.inlines.hh.
References index_first_pending, row_topology, sorted, and Parma_Polyhedra_Library::swap().
Referenced by swap().
00131 { 00132 Matrix::swap(y); 00133 std::swap(row_topology, y.row_topology); 00134 std::swap(index_first_pending, y.index_first_pending); 00135 std::swap(sorted, y.sorted); 00136 }
dimension_type Parma_Polyhedra_Library::Linear_System::max_space_dimension | ( | ) | [inline, static] |
Returns the maximum space dimension a Linear_System can handle.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 193 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::max_num_columns().
Referenced by Parma_Polyhedra_Library::Generator_System::max_space_dimension(), and Parma_Polyhedra_Library::Constraint_System::max_space_dimension().
00193 { 00194 // Column zero holds the inhomogeneous term or the divisor. 00195 // In NNC linear systems, the last column holds the coefficient 00196 // of the epsilon dimension. 00197 return max_num_columns() - 2; 00198 }
dimension_type Parma_Polyhedra_Library::Linear_System::space_dimension | ( | ) | const [inline] |
Returns the space dimension of the rows in the system.
The computation of the space dimension correctly ignores the column encoding the inhomogeneous terms of constraint (resp., the divisors of generators); if the system topology is NOT_NECESSARILY_CLOSED
, also the column of the -dimension coefficients will be ignored.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 201 of file Linear_System.inlines.hh.
References is_necessarily_closed(), and Parma_Polyhedra_Library::Matrix::num_columns().
Referenced by Parma_Polyhedra_Library::Generator_System::space_dimension(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().
00201 { 00202 const dimension_type n_columns = num_columns(); 00203 return (n_columns == 0) 00204 ? 0 00205 : n_columns - (is_necessarily_closed() ? 1 : 2); 00206 }
void Parma_Polyhedra_Library::Linear_System::remove_trailing_columns | ( | dimension_type | n | ) | [inline] |
Makes the system shrink by removing its n
trailing columns.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Definition at line 209 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::remove_trailing_columns(), and strong_normalize().
Referenced by Parma_Polyhedra_Library::Generator_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Polyhedron::remove_higher_space_dimensions(), and Parma_Polyhedra_Library::Polyhedron::remove_space_dimensions().
00209 { 00210 Matrix::remove_trailing_columns(n); 00211 // Have to re-normalize the rows of the system, 00212 // since we removed some coefficients. 00213 strong_normalize(); 00214 }
void Parma_Polyhedra_Library::Linear_System::permute_columns | ( | const std::vector< dimension_type > & | cycles | ) | [inline] |
Permutes the columns of the system.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 217 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::permute_columns(), and sign_normalize().
Referenced by Parma_Polyhedra_Library::Polyhedron::bounded_affine_preimage(), Parma_Polyhedra_Library::Polyhedron::map_space_dimensions(), and Parma_Polyhedra_Library::Grid_Generator_System::permute_columns().
00217 { 00218 Matrix::permute_columns(cycles); 00219 // The rows with permuted columns are still normalized but may 00220 // be not strongly normalized: sign normalization is necessary. 00221 sign_normalize(); 00222 }
Linear_Row & Parma_Polyhedra_Library::Linear_System::operator[] | ( | dimension_type | k | ) | [inline] |
Returns a reference to the k-th
row of the system.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 178 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::operator[]().
Referenced by Parma_Polyhedra_Library::Generator_System::operator[](), and Parma_Polyhedra_Library::Constraint_System::operator[]().
00178 { 00179 return static_cast<Linear_Row&>(Matrix::operator[](k)); 00180 }
const Linear_Row & Parma_Polyhedra_Library::Linear_System::operator[] | ( | dimension_type | k | ) | const [inline] |
Returns a constant reference to the k-th
row of the system.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 183 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::operator[]().
00183 { 00184 return static_cast<const Linear_Row&>(Matrix::operator[](k)); 00185 }
void Parma_Polyhedra_Library::Linear_System::strong_normalize | ( | ) |
Strongly normalizes the system.
Definition at line 463 of file Linear_System.cc.
References Parma_Polyhedra_Library::Matrix::num_rows(), and set_sorted().
Referenced by Parma_Polyhedra_Library::Generator_System::affine_image(), Parma_Polyhedra_Library::Constraint_System::affine_preimage(), Parma_Polyhedra_Library::Polyhedron::OK(), OK(), and remove_trailing_columns().
00463 { 00464 Linear_System& x = *this; 00465 const dimension_type nrows = x.num_rows(); 00466 // We strongly normalize also the pending rows. 00467 for (dimension_type i = nrows; i-- > 0; ) 00468 x[i].strong_normalize(); 00469 set_sorted(nrows <= 1); 00470 }
void Parma_Polyhedra_Library::Linear_System::sign_normalize | ( | ) |
Sign-normalizes the system.
Definition at line 473 of file Linear_System.cc.
References Parma_Polyhedra_Library::Matrix::num_rows(), and set_sorted().
Referenced by permute_columns(), and Parma_Polyhedra_Library::Polyhedron::simplify().
00473 { 00474 Linear_System& x = *this; 00475 const dimension_type nrows = x.num_rows(); 00476 // We sign-normalize also the pending rows. 00477 for (dimension_type i = num_rows(); i-- > 0; ) 00478 x[i].sign_normalize(); 00479 set_sorted(nrows <= 1); 00480 }
Topology Parma_Polyhedra_Library::Linear_System::topology | ( | ) | const [inline] |
Returns the system topology.
Definition at line 188 of file Linear_System.inlines.hh.
References row_topology.
Referenced by Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), Parma_Polyhedra_Library::Generator_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Polyhedron::BHRZ03_combining_constraints(), Parma_Polyhedra_Library::Polyhedron::conversion(), insert(), Parma_Polyhedra_Library::Grid_Generator_System::insert(), Parma_Polyhedra_Library::Generator_System::insert(), Parma_Polyhedra_Library::Constraint_System::insert(), insert_pending(), Parma_Polyhedra_Library::Generator_System::insert_pending(), Parma_Polyhedra_Library::Constraint_System::insert_pending(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Polyhedron::OK(), OK(), Parma_Polyhedra_Library::Grid_Generator_System::OK(), Parma_Polyhedra_Library::Polyhedron::select_CH78_constraints(), Parma_Polyhedra_Library::Polyhedron::select_H79_constraints(), and Parma_Polyhedra_Library::Polyhedron::topology().
00188 { 00189 return row_topology; 00190 }
bool Parma_Polyhedra_Library::Linear_System::is_sorted | ( | ) | const [inline] |
Returns the value of the sortedness flag.
Definition at line 41 of file Linear_System.inlines.hh.
References check_sorted(), and sorted.
Referenced by Parma_Polyhedra_Library::Polyhedron::add_and_minimize(), Parma_Polyhedra_Library::Polyhedron::add_recycled_generators_and_minimize(), add_row(), add_rows(), add_rows_and_columns(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions_and_project(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Generator_System::ascii_dump(), Parma_Polyhedra_Library::Constraint_System::ascii_dump(), back_substitute(), Parma_Polyhedra_Library::Polyhedron::conversion(), Parma_Polyhedra_Library::Polyhedron::intersection_assign(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Constraint_System::num_inequalities(), Parma_Polyhedra_Library::Generator_System::num_lines(), Parma_Polyhedra_Library::Generator_System::num_rays(), 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::Grid_Generator_System::OK(), Parma_Polyhedra_Library::Polyhedron::poly_hull_assign(), Parma_Polyhedra_Library::Polyhedron::process_pending_constraints(), Parma_Polyhedra_Library::Polyhedron::process_pending_generators(), sort_pending_and_remove_duplicates(), and Parma_Polyhedra_Library::Polyhedron::time_elapse_assign().
00041 { 00042 // The flag `sorted' does not really reflect the sortedness status 00043 // of a system (if `sorted' evaluates to `false' nothing is known). 00044 // This assertion is used to ensure that the system 00045 // is actually sorted when `sorted' value is 'true'. 00046 assert(!sorted || check_sorted()); 00047 return sorted; 00048 }
bool Parma_Polyhedra_Library::Linear_System::is_necessarily_closed | ( | ) | const [inline] |
Returns true
if and only if the system topology is NECESSARILY_CLOSED
.
Definition at line 173 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::NECESSARILY_CLOSED, and row_topology.
Referenced by Parma_Polyhedra_Library::Polyhedron::add_and_minimize(), Parma_Polyhedra_Library::Generator_System::add_corresponding_closure_points(), Parma_Polyhedra_Library::Generator_System::add_corresponding_points(), Parma_Polyhedra_Library::Constraint_System::add_low_level_constraints(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), ascii_dump(), Parma_Polyhedra_Library::Generator_System::ascii_dump(), Parma_Polyhedra_Library::Constraint_System::ascii_dump(), Parma_Polyhedra_Library::Generator_System::begin(), Parma_Polyhedra_Library::Generator_System::has_closure_points(), Parma_Polyhedra_Library::Generator_System::has_points(), Parma_Polyhedra_Library::Constraint_System::has_strict_inequalities(), insert(), Parma_Polyhedra_Library::Grid_Generator_System::insert(), Parma_Polyhedra_Library::Generator_System::insert(), Parma_Polyhedra_Library::Constraint_System::insert(), insert_pending(), Parma_Polyhedra_Library::Generator_System::insert_pending(), Parma_Polyhedra_Library::Constraint_System::insert_pending(), Parma_Polyhedra_Library::Polyhedron::is_necessarily_closed(), Parma_Polyhedra_Library::Polyhedron::minimize(), OK(), Parma_Polyhedra_Library::Generator_System::const_iterator::operator++(), Parma_Polyhedra_Library::Constraint_System::satisfies_all_constraints(), set_rows_topology(), and space_dimension().
00173 { 00174 return row_topology == NECESSARILY_CLOSED; 00175 }
PPL::dimension_type Parma_Polyhedra_Library::Linear_System::num_lines_or_equalities | ( | ) | const |
Returns the number of rows in the system that represent either lines or equalities.
Definition at line 40 of file Linear_System.cc.
References num_pending_rows(), and Parma_Polyhedra_Library::Matrix::num_rows().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_and_minimize(), back_substitute(), and gauss().
00040 { 00041 assert(num_pending_rows() == 0); 00042 const Linear_System& x = *this; 00043 dimension_type n = 0; 00044 for (dimension_type i = num_rows(); i-- > 0; ) 00045 if (x[i].is_line_or_equality()) 00046 ++n; 00047 return n; 00048 }
dimension_type Parma_Polyhedra_Library::Linear_System::first_pending_row | ( | ) | const [inline] |
Returns the index of the first pending row.
Definition at line 73 of file Linear_System.inlines.hh.
References index_first_pending.
Referenced by Parma_Polyhedra_Library::Polyhedron::add_and_minimize(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), ascii_dump(), Parma_Polyhedra_Library::Generator_System::ascii_dump(), Parma_Polyhedra_Library::Constraint_System::ascii_dump(), check_sorted(), Parma_Polyhedra_Library::Polyhedron::constrains(), Parma_Polyhedra_Library::Polyhedron::conversion(), Parma_Polyhedra_Library::Polyhedron::is_universe(), num_pending_rows(), Parma_Polyhedra_Library::Polyhedron::OK(), OK(), operator==(), Parma_Polyhedra_Library::Generator_System::remove_invalid_lines_and_rays(), sort_and_remove_with_sat(), sort_pending_and_remove_duplicates(), sort_rows(), Parma_Polyhedra_Library::Polyhedron::update_sat_c(), and Parma_Polyhedra_Library::Polyhedron::update_sat_g().
00073 { 00074 return index_first_pending; 00075 }
dimension_type Parma_Polyhedra_Library::Linear_System::num_pending_rows | ( | ) | const [inline] |
Returns the number of rows that are in the pending part of the system.
Definition at line 78 of file Linear_System.inlines.hh.
References first_pending_row(), and Parma_Polyhedra_Library::Matrix::num_rows().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_and_minimize(), add_pending_row(), Parma_Polyhedra_Library::Polyhedron::add_recycled_generators(), Parma_Polyhedra_Library::Polyhedron::add_recycled_generators_and_minimize(), add_row(), add_rows(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), back_substitute(), gauss(), insert(), Parma_Polyhedra_Library::Grid_Generator_System::insert(), Parma_Polyhedra_Library::Generator_System::insert(), Parma_Polyhedra_Library::Constraint_System::insert(), insert_pending(), Parma_Polyhedra_Library::Polyhedron::intersection_assign_and_minimize(), Linear_System(), merge_rows_assign(), Parma_Polyhedra_Library::Constraint_System::num_equalities(), Parma_Polyhedra_Library::Constraint_System::num_inequalities(), Parma_Polyhedra_Library::Generator_System::num_lines(), num_lines_or_equalities(), Parma_Polyhedra_Library::Generator_System::num_rays(), Parma_Polyhedra_Library::Polyhedron::OK(), operator=(), Parma_Polyhedra_Library::Polyhedron::poly_hull_assign_and_minimize(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Polyhedron::process_pending_constraints(), Parma_Polyhedra_Library::Polyhedron::process_pending_generators(), Parma_Polyhedra_Library::Generator_System::remove_invalid_lines_and_rays(), Parma_Polyhedra_Library::Polyhedron::simplified_constraints(), simplify(), sort_and_remove_with_sat(), sort_pending_and_remove_duplicates(), and sort_rows().
00078 { 00079 assert(num_rows() >= first_pending_row()); 00080 return num_rows() - first_pending_row(); 00081 }
bool Parma_Polyhedra_Library::Linear_System::check_sorted | ( | ) | const |
Returns true
if and only if *this
is sorted, without checking for duplicates.
Definition at line 824 of file Linear_System.cc.
References first_pending_row().
Referenced by is_sorted(), merge_rows_assign(), 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(), OK(), and sort_and_remove_with_sat().
00824 { 00825 const Linear_System& x = *this; 00826 for (dimension_type i = first_pending_row(); i-- > 1; ) 00827 if (compare(x[i], x[i-1]) < 0) 00828 return false; 00829 return true; 00830 }
void Parma_Polyhedra_Library::Linear_System::set_necessarily_closed | ( | ) | [inline] |
Sets the system topology to NECESSARILY_CLOSED
.
Definition at line 159 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::has_no_rows(), Parma_Polyhedra_Library::NECESSARILY_CLOSED, row_topology, and set_rows_topology().
Referenced by Parma_Polyhedra_Library::Generator_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), ascii_load(), Parma_Polyhedra_Library::Generator_System::ascii_load(), Parma_Polyhedra_Library::Constraint_System::ascii_load(), set_rows_topology(), and Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints().
00159 { 00160 row_topology = NECESSARILY_CLOSED; 00161 if (!has_no_rows()) 00162 set_rows_topology(); 00163 }
void Parma_Polyhedra_Library::Linear_System::set_not_necessarily_closed | ( | ) | [inline] |
Sets the system topology to NOT_NECESSARILY_CLOSED
.
Definition at line 166 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::has_no_rows(), Parma_Polyhedra_Library::NOT_NECESSARILY_CLOSED, row_topology, and set_rows_topology().
Referenced by Parma_Polyhedra_Library::Generator_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), ascii_load(), Parma_Polyhedra_Library::Generator_System::ascii_load(), Parma_Polyhedra_Library::Constraint_System::ascii_load(), Parma_Polyhedra_Library::Generator_System::insert(), Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::Generator_System::insert_pending(), Parma_Polyhedra_Library::Constraint_System::insert_pending(), set_rows_topology(), and Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints().
00166 { 00167 row_topology = NOT_NECESSARILY_CLOSED; 00168 if (!has_no_rows()) 00169 set_rows_topology(); 00170 }
void Parma_Polyhedra_Library::Linear_System::set_rows_topology | ( | ) |
Sets the topology of all rows equal to the system topology.
Definition at line 102 of file Linear_System.cc.
References is_necessarily_closed(), Parma_Polyhedra_Library::Matrix::num_rows(), set_necessarily_closed(), and set_not_necessarily_closed().
Referenced by set_necessarily_closed(), and set_not_necessarily_closed().
00102 { 00103 Linear_System& x = *this; 00104 if (is_necessarily_closed()) 00105 for (dimension_type i = num_rows(); i-- > 0; ) 00106 x[i].set_necessarily_closed(); 00107 else 00108 for (dimension_type i = num_rows(); i-- > 0; ) 00109 x[i].set_not_necessarily_closed(); 00110 }
void Parma_Polyhedra_Library::Linear_System::unset_pending_rows | ( | ) | [inline] |
Sets the index to indicate that the system has no pending rows.
Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 84 of file Linear_System.inlines.hh.
References index_first_pending, and Parma_Polyhedra_Library::Matrix::num_rows().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_recycled_constraints(), Parma_Polyhedra_Library::Polyhedron::add_recycled_generators(), Parma_Polyhedra_Library::Polyhedron::add_recycled_generators_and_minimize(), add_rows(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions_and_project(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Polyhedron::concatenate_assign(), Parma_Polyhedra_Library::Polyhedron::conversion(), Linear_System(), merge_rows_assign(), Parma_Polyhedra_Library::Polyhedron::OK(), operator=(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Polyhedron::remove_pending_to_obtain_constraints(), Parma_Polyhedra_Library::Polyhedron::remove_pending_to_obtain_generators(), Parma_Polyhedra_Library::Polyhedron::simplified_constraints(), Parma_Polyhedra_Library::Polyhedron::simplify(), simplify(), Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints(), Parma_Polyhedra_Library::Polyhedron::strongly_minimize_generators(), Parma_Polyhedra_Library::Polyhedron::time_elapse_assign(), Parma_Polyhedra_Library::Polyhedron::topological_closure_assign(), and Parma_Polyhedra_Library::Grid_Generator_System::unset_pending_rows().
00084 { 00085 index_first_pending = num_rows(); 00086 }
void Parma_Polyhedra_Library::Linear_System::set_index_first_pending_row | ( | dimension_type | i | ) | [inline] |
Sets the index of the first pending row to i
.
Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 89 of file Linear_System.inlines.hh.
References index_first_pending.
Referenced by add_row(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), ascii_load(), Parma_Polyhedra_Library::Generator_System::ascii_load(), Parma_Polyhedra_Library::Constraint_System::ascii_load(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Generator_System::remove_invalid_lines_and_rays(), Parma_Polyhedra_Library::Grid_Generator_System::set_index_first_pending_row(), sort_and_remove_with_sat(), and sort_rows().
00089 { 00090 index_first_pending = i; 00091 }
void Parma_Polyhedra_Library::Linear_System::set_sorted | ( | bool | b | ) | [inline] |
Sets the sortedness flag of the system to b
.
Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 51 of file Linear_System.inlines.hh.
References sorted.
Referenced by Parma_Polyhedra_Library::Polyhedron::add_recycled_constraints(), Parma_Polyhedra_Library::Polyhedron::add_recycled_generators(), add_row(), add_rows(), add_rows_and_columns(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), ascii_load(), Parma_Polyhedra_Library::Generator_System::ascii_load(), Parma_Polyhedra_Library::Constraint_System::ascii_load(), back_substitute(), Parma_Polyhedra_Library::Polyhedron::concatenate_assign(), Parma_Polyhedra_Library::Polyhedron::conversion(), gauss(), Parma_Polyhedra_Library::Polyhedron::generalized_affine_image(), Parma_Polyhedra_Library::Polyhedron::minimize(), normalize(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_constraints_with_sat_c(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_generators_with_sat_g(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Generator_System::remove_invalid_lines_and_rays(), Parma_Polyhedra_Library::Polyhedron::remove_pending_to_obtain_constraints(), Parma_Polyhedra_Library::Polyhedron::remove_pending_to_obtain_generators(), resize_no_copy(), Parma_Polyhedra_Library::Grid_Generator_System::set_sorted(), sign_normalize(), Parma_Polyhedra_Library::Polyhedron::simplify(), simplify(), sort_and_remove_with_sat(), strong_normalize(), Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints(), Parma_Polyhedra_Library::Polyhedron::strongly_minimize_generators(), and Parma_Polyhedra_Library::Polyhedron::topological_closure_assign().
00051 { 00052 sorted = b; 00053 }
void Parma_Polyhedra_Library::Linear_System::resize_no_copy | ( | dimension_type | new_n_rows, | |
dimension_type | new_n_columns | |||
) | [inline] |
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. |
Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 147 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::resize_no_copy(), row_topology, and set_sorted().
Referenced by ascii_load(), Parma_Polyhedra_Library::Generator_System::ascii_load(), Parma_Polyhedra_Library::Constraint_System::ascii_load(), Parma_Polyhedra_Library::Polyhedron::minimize(), and Parma_Polyhedra_Library::Grid_Generator_System::resize_no_copy().
00148 { 00149 Matrix::resize_no_copy(new_n_rows, new_n_columns, 00150 Linear_Row::Flags(row_topology)); 00151 // Even though `*this' may happen to keep its sortedness, we believe 00152 // that checking such a property is not worth the effort. In fact, 00153 // it is very likely that the system will be overwritten as soon as 00154 // we return. 00155 set_sorted(false); 00156 }
void Parma_Polyhedra_Library::Linear_System::add_rows_and_columns | ( | dimension_type | n | ) |
Adds n
rows and columns to the system.
n | The number of rows and columns to be added: must be strictly positive. |
Definition at line 733 of file Linear_System.cc.
References Parma_Polyhedra_Library::Matrix::add_zero_rows_and_columns(), is_sorted(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::OK(), row_topology, Parma_Polyhedra_Library::Linear_Row::set_is_line_or_equality(), set_sorted(), and Parma_Polyhedra_Library::swap().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions_and_project(), and Parma_Polyhedra_Library::Polyhedron::concatenate_assign().
00733 { 00734 assert(n > 0); 00735 const bool was_sorted = is_sorted(); 00736 const dimension_type old_n_rows = num_rows(); 00737 const dimension_type old_n_columns = num_columns(); 00738 add_zero_rows_and_columns(n, n, Linear_Row::Flags(row_topology)); 00739 Linear_System& x = *this; 00740 // The old system is moved to the bottom. 00741 for (dimension_type i = old_n_rows; i-- > 0; ) 00742 std::swap(x[i], x[i + n]); 00743 for (dimension_type i = n, c = old_n_columns; i-- > 0; ) { 00744 // The top right-hand sub-system (i.e., the system made of new 00745 // rows and columns) is set to the specular image of the identity 00746 // matrix. 00747 Linear_Row& r = x[i]; 00748 r[c++] = 1; 00749 r.set_is_line_or_equality(); 00750 // Note: `r' is strongly normalized. 00751 } 00752 // If the old system was empty, the last row added is either 00753 // a positivity constraint or a point. 00754 if (old_n_columns == 0) { 00755 x[n-1].set_is_ray_or_point_or_inequality(); 00756 // Since ray, points and inequalities come after lines 00757 // and equalities, this case implies the system is sorted. 00758 set_sorted(true); 00759 } 00760 else if (was_sorted) 00761 set_sorted(compare(x[n-1], x[n]) <= 0); 00762 00763 // A well-formed system has to be returned. 00764 assert(OK(true)); 00765 }
void Parma_Polyhedra_Library::Linear_System::insert | ( | const Linear_Row & | r | ) |
Adds a copy of r
to the system, automatically resizing the system or the row's copy, if needed.
Definition at line 182 of file Linear_System.cc.
References add_row(), Parma_Polyhedra_Library::Matrix::add_zero_columns(), Parma_Polyhedra_Library::Linear_Row::check_strong_normalized(), is_necessarily_closed(), Parma_Polyhedra_Library::Matrix::num_columns(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::OK(), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Row::size(), Parma_Polyhedra_Library::swap(), Parma_Polyhedra_Library::Matrix::swap_columns(), Parma_Polyhedra_Library::Linear_Row::topology(), and topology().
Referenced by add_to_system_and_check_independence(), Parma_Polyhedra_Library::Constraint_System::Constraint_System(), Parma_Polyhedra_Library::Generator_System::Generator_System(), Parma_Polyhedra_Library::Generator_System::insert(), and Parma_Polyhedra_Library::Constraint_System::insert().
00182 { 00183 // The added row must be strongly normalized and have the same 00184 // topology of the system. 00185 assert(r.check_strong_normalized()); 00186 assert(topology() == r.topology()); 00187 // This method is only used when the system has no pending rows. 00188 assert(num_pending_rows() == 0); 00189 00190 const dimension_type old_num_rows = num_rows(); 00191 const dimension_type old_num_columns = num_columns(); 00192 const dimension_type r_size = r.size(); 00193 00194 // Resize the system, if necessary. 00195 if (r_size > old_num_columns) { 00196 add_zero_columns(r_size - old_num_columns); 00197 if (!is_necessarily_closed() && old_num_rows != 0) 00198 // Move the epsilon coefficients to the last column 00199 // (note: sorting is preserved). 00200 swap_columns(old_num_columns - 1, r_size - 1); 00201 add_row(r); 00202 } 00203 else if (r_size < old_num_columns) { 00204 // Create a resized copy of the row. 00205 Linear_Row tmp_row(r, old_num_columns, row_capacity); 00206 // If needed, move the epsilon coefficient to the last position. 00207 if (!is_necessarily_closed()) 00208 std::swap(tmp_row[r_size - 1], tmp_row[old_num_columns - 1]); 00209 add_row(tmp_row); 00210 } 00211 else 00212 // Here r_size == old_num_columns. 00213 add_row(r); 00214 00215 // The added row was not a pending row. 00216 assert(num_pending_rows() == 0); 00217 // Do not check for strong normalization, 00218 // because no modification of rows has occurred. 00219 assert(OK(false)); 00220 }
void Parma_Polyhedra_Library::Linear_System::insert_pending | ( | const Linear_Row & | r | ) |
Adds a copy of the given row to the pending part of the system, automatically resizing the system or the row, if needed.
Definition at line 223 of file Linear_System.cc.
References add_pending_row(), Parma_Polyhedra_Library::Matrix::add_zero_columns(), Parma_Polyhedra_Library::Linear_Row::check_strong_normalized(), is_necessarily_closed(), Parma_Polyhedra_Library::Matrix::num_columns(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::OK(), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Row::size(), Parma_Polyhedra_Library::swap(), Parma_Polyhedra_Library::Matrix::swap_columns(), Parma_Polyhedra_Library::Linear_Row::topology(), and topology().
Referenced by Parma_Polyhedra_Library::Generator_System::insert_pending(), and Parma_Polyhedra_Library::Constraint_System::insert_pending().
00223 { 00224 // The added row must be strongly normalized and have the same 00225 // topology of the system. 00226 assert(r.check_strong_normalized()); 00227 assert(topology() == r.topology()); 00228 00229 const dimension_type old_num_rows = num_rows(); 00230 const dimension_type old_num_columns = num_columns(); 00231 const dimension_type r_size = r.size(); 00232 00233 // Resize the system, if necessary. 00234 if (r_size > old_num_columns) { 00235 add_zero_columns(r_size - old_num_columns); 00236 if (!is_necessarily_closed() && old_num_rows != 0) 00237 // Move the epsilon coefficients to the last column 00238 // (note: sorting is preserved). 00239 swap_columns(old_num_columns - 1, r_size - 1); 00240 add_pending_row(r); 00241 } 00242 else if (r_size < old_num_columns) 00243 if (is_necessarily_closed() || old_num_rows == 0) 00244 add_pending_row(Linear_Row(r, old_num_columns, row_capacity)); 00245 else { 00246 // Create a resized copy of the row (and move the epsilon 00247 // coefficient to its last position). 00248 Linear_Row tmp_row(r, old_num_columns, row_capacity); 00249 std::swap(tmp_row[r_size - 1], tmp_row[old_num_columns - 1]); 00250 add_pending_row(tmp_row); 00251 } 00252 else 00253 // Here r_size == old_num_columns. 00254 add_pending_row(r); 00255 00256 // The added row was a pending row. 00257 assert(num_pending_rows() > 0); 00258 // Do not check for strong normalization, 00259 // because no modification of rows has occurred. 00260 assert(OK(false)); 00261 }
void Parma_Polyhedra_Library::Linear_System::add_row | ( | const Linear_Row & | r | ) |
Adds a copy of the given row to the system.
Definition at line 347 of file Linear_System.cc.
References Parma_Polyhedra_Library::Matrix::add_row(), Parma_Polyhedra_Library::Linear_Row::check_strong_normalized(), is_sorted(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::OK(), Parma_Polyhedra_Library::Matrix::row_size, set_index_first_pending_row(), set_sorted(), and Parma_Polyhedra_Library::Row::size().
Referenced by Parma_Polyhedra_Library::Polyhedron::generalized_affine_image(), and insert().
00347 { 00348 // The added row must be strongly normalized and have the same 00349 // number of elements as the existing rows of the system. 00350 assert(r.check_strong_normalized()); 00351 assert(r.size() == row_size); 00352 // This method is only used when the system has no pending rows. 00353 assert(num_pending_rows() == 0); 00354 00355 const bool was_sorted = is_sorted(); 00356 00357 Matrix::add_row(r); 00358 00359 // We update `index_first_pending', because it must be equal to 00360 // `num_rows()'. 00361 set_index_first_pending_row(num_rows()); 00362 00363 if (was_sorted) { 00364 const dimension_type nrows = num_rows(); 00365 // The added row may have caused the system to be not sorted anymore. 00366 if (nrows > 1) { 00367 // If the system is not empty and the inserted row is the 00368 // greatest one, the system is set to be sorted. 00369 // If it is not the greatest one then the system is no longer sorted. 00370 Linear_System& x = *this; 00371 set_sorted(compare(x[nrows-2], x[nrows-1]) <= 0); 00372 } 00373 else 00374 // A system having only one row is sorted. 00375 set_sorted(true); 00376 } 00377 // The added row was not a pending row. 00378 assert(num_pending_rows() == 0); 00379 // Do not check for strong normalization, because no modification of 00380 // rows has occurred. 00381 assert(OK(false)); 00382 }
void Parma_Polyhedra_Library::Linear_System::add_pending_row | ( | Linear_Row::Flags | flags | ) |
Adds a new empty row to the system, setting only its flags.
Definition at line 423 of file Linear_System.cc.
References Parma_Polyhedra_Library::compute_capacity(), Parma_Polyhedra_Library::construct(), Parma_Polyhedra_Library::Matrix::max_num_rows(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Matrix::row_size, Parma_Polyhedra_Library::Matrix::rows, and Parma_Polyhedra_Library::swap().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_and_minimize(), Parma_Polyhedra_Library::Generator_System::add_corresponding_closure_points(), Parma_Polyhedra_Library::Generator_System::add_corresponding_points(), Parma_Polyhedra_Library::Polyhedron::conversion(), and insert_pending().
00423 { 00424 const dimension_type new_rows_size = rows.size() + 1; 00425 if (rows.capacity() < new_rows_size) { 00426 // Reallocation will take place. 00427 std::vector<Row> new_rows; 00428 new_rows.reserve(compute_capacity(new_rows_size, max_num_rows())); 00429 new_rows.insert(new_rows.end(), new_rows_size, Row()); 00430 // Put the new row in place. 00431 Linear_Row new_row(row_size, row_capacity, flags); 00432 dimension_type i = new_rows_size-1; 00433 std::swap(new_rows[i], new_row); 00434 // Steal the old rows. 00435 while (i-- > 0) 00436 new_rows[i].swap(rows[i]); 00437 // Put the new vector into place. 00438 std::swap(rows, new_rows); 00439 } 00440 else { 00441 // Reallocation will NOT take place. 00442 // Insert a new empty row at the end, then construct it assigning 00443 // it the given type. 00444 Row& new_row = *rows.insert(rows.end(), Row()); 00445 static_cast<Linear_Row&>(new_row).construct(row_size, row_capacity, flags); 00446 } 00447 00448 // The added row was a pending row. 00449 assert(num_pending_rows() > 0); 00450 }
void Parma_Polyhedra_Library::Linear_System::add_pending_row | ( | const Linear_Row & | r | ) |
Adds a copy of the given row to the pending part of the system.
Definition at line 385 of file Linear_System.cc.
References Parma_Polyhedra_Library::Linear_Row::check_strong_normalized(), Parma_Polyhedra_Library::compute_capacity(), Parma_Polyhedra_Library::Matrix::max_num_rows(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::OK(), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Matrix::row_size, Parma_Polyhedra_Library::Matrix::rows, Parma_Polyhedra_Library::Row::size(), and Parma_Polyhedra_Library::swap().
00385 { 00386 // The added row must be strongly normalized and have the same 00387 // number of elements of the existing rows of the system. 00388 assert(r.check_strong_normalized()); 00389 assert(r.size() == row_size); 00390 00391 const dimension_type new_rows_size = rows.size() + 1; 00392 if (rows.capacity() < new_rows_size) { 00393 // Reallocation will take place. 00394 std::vector<Row> new_rows; 00395 new_rows.reserve(compute_capacity(new_rows_size, max_num_rows())); 00396 new_rows.insert(new_rows.end(), new_rows_size, Row()); 00397 // Put the new row in place. 00398 Row new_row(r, row_capacity); 00399 dimension_type i = new_rows_size-1; 00400 std::swap(new_rows[i], new_row); 00401 // Steal the old rows. 00402 while (i-- > 0) 00403 new_rows[i].swap(rows[i]); 00404 // Put the new rows into place. 00405 std::swap(rows, new_rows); 00406 } 00407 else { 00408 // Reallocation will NOT take place. 00409 // Inserts a new empty row at the end, then substitutes it with a 00410 // copy of the given row. 00411 Row tmp(r, row_capacity); 00412 std::swap(*rows.insert(rows.end(), Row()), tmp); 00413 } 00414 00415 // The added row was a pending row. 00416 assert(num_pending_rows() > 0); 00417 // Do not check for strong normalization, because no modification of 00418 // rows has occurred. 00419 assert(OK(false)); 00420 }
void Parma_Polyhedra_Library::Linear_System::add_rows | ( | const Linear_System & | y | ) |
Adds to *this
a copy of the rows of `y'.
It is assumed that *this
has no pending rows.
Definition at line 286 of file Linear_System.cc.
References add_pending_rows(), Parma_Polyhedra_Library::Matrix::has_no_rows(), is_sorted(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::OK(), set_sorted(), and unset_pending_rows().
Referenced by Parma_Polyhedra_Library::Polyhedron::intersection_assign(), and Parma_Polyhedra_Library::Polyhedron::poly_hull_assign().
00286 { 00287 assert(num_pending_rows() == 0); 00288 00289 // Adding no rows is a no-op. 00290 if (y.has_no_rows()) 00291 return; 00292 00293 // Check if sortedness is preserved. 00294 if (is_sorted()) { 00295 if (!y.is_sorted() || y.num_pending_rows() > 0) 00296 set_sorted(false); 00297 else { 00298 // `y' is sorted and has no pending rows. 00299 const dimension_type n_rows = num_rows(); 00300 if (n_rows > 0) 00301 set_sorted(compare((*this)[n_rows-1], y[0]) <= 0); 00302 } 00303 } 00304 00305 // Add the rows of `y' as if they were pending. 00306 add_pending_rows(y); 00307 // There are no pending_rows. 00308 unset_pending_rows(); 00309 00310 // Do not check for strong normalization, 00311 // because no modification of rows has occurred. 00312 assert(OK(false)); 00313 }
void Parma_Polyhedra_Library::Linear_System::add_pending_rows | ( | const Linear_System & | y | ) |
Adds a copy of the rows of `y' to the pending part of `*this'.
Definition at line 264 of file Linear_System.cc.
References Parma_Polyhedra_Library::Matrix::add_zero_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::OK(), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Matrix::row_size, row_topology, sorted, and Parma_Polyhedra_Library::swap().
Referenced by add_rows(), Parma_Polyhedra_Library::Polyhedron::intersection_assign(), Parma_Polyhedra_Library::Polyhedron::intersection_assign_and_minimize(), Parma_Polyhedra_Library::Polyhedron::poly_hull_assign(), Parma_Polyhedra_Library::Polyhedron::poly_hull_assign_and_minimize(), and Parma_Polyhedra_Library::Polyhedron::time_elapse_assign().
00264 { 00265 Linear_System& x = *this; 00266 assert(x.row_size == y.row_size); 00267 00268 const dimension_type x_n_rows = x.num_rows(); 00269 const dimension_type y_n_rows = y.num_rows(); 00270 // Grow to the required size without changing sortedness. 00271 const bool was_sorted = sorted; 00272 add_zero_rows(y_n_rows, Linear_Row::Flags(row_topology)); 00273 sorted = was_sorted; 00274 00275 // Copy the rows of `y', forcing size and capacity. 00276 for (dimension_type i = y_n_rows; i-- > 0; ) { 00277 Row copy(y[i], x.row_size, x.row_capacity); 00278 std::swap(copy, x[x_n_rows+i]); 00279 } 00280 // Do not check for strong normalization, 00281 // because no modification of rows has occurred. 00282 assert(OK(false)); 00283 }
void Parma_Polyhedra_Library::Linear_System::sort_rows | ( | ) |
Sorts the non-pending rows (in growing order) and eliminates duplicated ones.
Definition at line 316 of file Linear_System.cc.
References first_pending_row(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::OK(), set_index_first_pending_row(), and sorted.
Referenced by Parma_Polyhedra_Library::Polyhedron::add_recycled_generators_and_minimize(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Polyhedron::concatenate_assign(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_constraints(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_generators(), Parma_Polyhedra_Library::Polyhedron::OK(), sort_pending_and_remove_duplicates(), and Parma_Polyhedra_Library::Polyhedron::time_elapse_assign().
00316 { 00317 const dimension_type num_pending = num_pending_rows(); 00318 // We sort the non-pending rows only. 00319 sort_rows(0, first_pending_row()); 00320 set_index_first_pending_row(num_rows() - num_pending); 00321 sorted = true; 00322 // Do not check for strong normalization, 00323 // because no modification of rows has occurred. 00324 assert(OK(false)); 00325 }
void Parma_Polyhedra_Library::Linear_System::sort_rows | ( | dimension_type | first_row, | |
dimension_type | last_row | |||
) |
Sorts the rows (in growing order) form first_row
to last_row
and eliminates duplicated ones.
Definition at line 328 of file Linear_System.cc.
References first_pending_row(), Parma_Polyhedra_Library::Matrix::num_rows(), and Parma_Polyhedra_Library::Matrix::rows.
00329 { 00330 assert(first_row <= last_row && last_row <= num_rows()); 00331 // We cannot mix pending and non-pending rows. 00332 assert(first_row >= first_pending_row() || last_row <= first_pending_row()); 00333 00334 // First sort without removing duplicates. 00335 std::vector<Row>::iterator first = rows.begin() + first_row; 00336 std::vector<Row>::iterator last = rows.begin() + last_row; 00337 swapping_sort(first, last, Row_Less_Than()); 00338 // Second, move duplicates to the end. 00339 std::vector<Row>::iterator new_last = swapping_unique(first, last); 00340 // Finally, remove duplicates. 00341 rows.erase(new_last, last); 00342 // NOTE: we cannot check all invariants of the system here, 00343 // because the caller still has to update `index_first_pending'. 00344 }
void Parma_Polyhedra_Library::Linear_System::merge_rows_assign | ( | const Linear_System & | y | ) |
Assigns to *this
the result of merging its rows with those of y
, obtaining a sorted system.
Duplicated rows will occur only once in the result. On entry, both systems are assumed to be sorted and have no pending rows.
Definition at line 51 of file Linear_System.cc.
References check_sorted(), Parma_Polyhedra_Library::compute_capacity(), Parma_Polyhedra_Library::Matrix::max_num_rows(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Matrix::row_size, Parma_Polyhedra_Library::Matrix::rows, Parma_Polyhedra_Library::swap(), and unset_pending_rows().
Referenced by Parma_Polyhedra_Library::Polyhedron::intersection_assign(), Parma_Polyhedra_Library::Polyhedron::poly_hull_assign(), and Parma_Polyhedra_Library::Polyhedron::time_elapse_assign().
00051 { 00052 assert(row_size >= y.row_size); 00053 // Both systems have to be sorted and have no pending rows. 00054 assert(check_sorted() && y.check_sorted()); 00055 assert(num_pending_rows() == 0 && y.num_pending_rows() == 0); 00056 00057 Linear_System& x = *this; 00058 00059 // A temporary vector of rows... 00060 std::vector<Row> tmp; 00061 // ... with enough capacity not to require any reallocations. 00062 tmp.reserve(compute_capacity(x.num_rows() + y.num_rows(), max_num_rows())); 00063 00064 dimension_type xi = 0; 00065 dimension_type x_num_rows = x.num_rows(); 00066 dimension_type yi = 0; 00067 dimension_type y_num_rows = y.num_rows(); 00068 00069 while (xi < x_num_rows && yi < y_num_rows) { 00070 const int comp = compare(x[xi], y[yi]); 00071 if (comp <= 0) { 00072 // Elements that can be taken from `x' are actually _stolen_ from `x' 00073 std::swap(x[xi++], *tmp.insert(tmp.end(), Linear_Row())); 00074 if (comp == 0) 00075 // A duplicate element. 00076 ++yi; 00077 } 00078 else { 00079 // (comp > 0) 00080 Linear_Row copy(y[yi++], row_size, row_capacity); 00081 std::swap(copy, *tmp.insert(tmp.end(), Linear_Row())); 00082 } 00083 } 00084 // Insert what is left. 00085 if (xi < x_num_rows) 00086 while (xi < x_num_rows) 00087 std::swap(x[xi++], *tmp.insert(tmp.end(), Linear_Row())); 00088 else 00089 while (yi < y_num_rows) { 00090 Linear_Row copy(y[yi++], row_size, row_capacity); 00091 std::swap(copy, *tmp.insert(tmp.end(), Linear_Row())); 00092 } 00093 00094 // We get the result vector and let the old one be destroyed. 00095 std::swap(tmp, rows); 00096 // There are no pending rows. 00097 unset_pending_rows(); 00098 assert(check_sorted()); 00099 }
void Parma_Polyhedra_Library::Linear_System::sort_pending_and_remove_duplicates | ( | ) |
Sorts the pending rows and eliminates those that also occur in the non-pending part of the system.
Definition at line 768 of file Linear_System.cc.
References Parma_Polyhedra_Library::cmp(), Parma_Polyhedra_Library::Matrix::erase_to_end(), first_pending_row(), is_sorted(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::OK(), sort_rows(), and Parma_Polyhedra_Library::swap().
Referenced by Parma_Polyhedra_Library::Polyhedron::intersection_assign_and_minimize(), Parma_Polyhedra_Library::Polyhedron::poly_hull_assign_and_minimize(), Parma_Polyhedra_Library::Polyhedron::process_pending_constraints(), and Parma_Polyhedra_Library::Polyhedron::process_pending_generators().
00768 { 00769 assert(num_pending_rows() > 0); 00770 assert(is_sorted()); 00771 Linear_System& x = *this; 00772 00773 // The non-pending part of the system is already sorted. 00774 // Now sorting the pending part.. 00775 const dimension_type first_pending = x.first_pending_row(); 00776 x.sort_rows(first_pending, x.num_rows()); 00777 // Recompute the number of rows, because we may have removed 00778 // some rows occurring more than once in the pending part. 00779 dimension_type num_rows = x.num_rows(); 00780 00781 dimension_type k1 = 0; 00782 dimension_type k2 = first_pending; 00783 dimension_type num_duplicates = 0; 00784 // In order to erase them, put at the end of the system 00785 // those pending rows that also occur in the non-pending part. 00786 while (k1 < first_pending && k2 < num_rows) { 00787 const int cmp = compare(x[k1], x[k2]); 00788 if (cmp == 0) { 00789 // We found the same row. 00790 ++num_duplicates; 00791 --num_rows; 00792 // By initial sortedness, we can increment index `k1'. 00793 ++k1; 00794 // Do not increment `k2'; instead, swap there the next pending row. 00795 if (k2 < num_rows) 00796 std::swap(x[k2], x[k2 + num_duplicates]); 00797 } 00798 else if (cmp < 0) 00799 // By initial sortedness, we can increment `k1'. 00800 ++k1; 00801 else { 00802 // Here `cmp > 0'. 00803 // Increment `k2' and, if we already found any duplicate, 00804 // swap the next pending row in position `k2'. 00805 ++k2; 00806 if (num_duplicates > 0 && k2 < num_rows) 00807 std::swap(x[k2], x[k2 + num_duplicates]); 00808 } 00809 } 00810 // If needed, swap any duplicates found past the pending rows 00811 // that has not been considered yet; then erase the duplicates. 00812 if (num_duplicates > 0) { 00813 if (k2 < num_rows) 00814 for (++k2; k2 < num_rows; ++k2) 00815 std::swap(x[k2], x[k2 + num_duplicates]); 00816 x.erase_to_end(num_rows); 00817 } 00818 // Do not check for strong normalization, 00819 // because no modification of rows has occurred. 00820 assert(OK(false)); 00821 }
void Parma_Polyhedra_Library::Linear_System::sort_and_remove_with_sat | ( | Bit_Matrix & | sat | ) |
Sorts the system, removing duplicates, keeping the saturation matrix consistent.
sat | Bit matrix with rows corresponding to the rows of *this . |
Definition at line 503 of file Linear_System.cc.
References check_sorted(), Parma_Polyhedra_Library::Matrix::erase_to_end(), first_pending_row(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Bit_Matrix::num_rows(), Parma_Polyhedra_Library::Bit_Matrix::rows, Parma_Polyhedra_Library::Matrix::rows, Parma_Polyhedra_Library::Bit_Matrix::rows_erase_to_end(), set_index_first_pending_row(), set_sorted(), and Parma_Polyhedra_Library::swap().
Referenced by Parma_Polyhedra_Library::Polyhedron::obtain_sorted_constraints(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_constraints_with_sat_c(), Parma_Polyhedra_Library::Polyhedron::obtain_sorted_generators(), and Parma_Polyhedra_Library::Polyhedron::obtain_sorted_generators_with_sat_g().
00503 { 00504 Linear_System& sys = *this; 00505 // We can only sort the non-pending part of the system. 00506 assert(sys.first_pending_row() == sat.num_rows()); 00507 if (sys.first_pending_row() <= 1) { 00508 sys.set_sorted(true); 00509 return; 00510 } 00511 00512 // First, sort `sys' (keeping `sat' consistent) without removing duplicates. 00513 With_Bit_Matrix_iterator first(sys.rows.begin(), sat.rows.begin()); 00514 With_Bit_Matrix_iterator last = first + sat.num_rows(); 00515 swapping_sort(first, last, Row_Less_Than()); 00516 // Second, move duplicates in `sys' to the end (keeping `sat' consistent). 00517 With_Bit_Matrix_iterator new_last = swapping_unique(first, last); 00518 00519 const dimension_type num_duplicates = last - new_last; 00520 const dimension_type new_first_pending_row 00521 = sys.first_pending_row() - num_duplicates; 00522 00523 if (sys.num_pending_rows() > 0) { 00524 // In this case, we must put the duplicates after the pending rows. 00525 const dimension_type n_rows = sys.num_rows() - 1; 00526 for (dimension_type i = 0; i < num_duplicates; ++i) 00527 std::swap(sys[new_first_pending_row + i], sys[n_rows - i]); 00528 } 00529 // Erasing the duplicated rows... 00530 sys.erase_to_end(sys.num_rows() - num_duplicates); 00531 sys.set_index_first_pending_row(new_first_pending_row); 00532 // ... and the corresponding rows of the saturation matrix. 00533 sat.rows_erase_to_end(sat.num_rows() - num_duplicates); 00534 assert(sys.check_sorted()); 00535 // Now the system is sorted. 00536 sys.set_sorted(true); 00537 }
PPL::dimension_type Parma_Polyhedra_Library::Linear_System::gauss | ( | dimension_type | n_lines_or_equalities | ) |
Minimizes the subsystem of equations contained in *this
.
This method works only on the equalities of the system: the system is required to be partially sorted, so that all the equalities are grouped at its top; it is assumed that the number of equalities is exactly n_lines_or_equalities
. The method finds a minimal system for the equalities and returns its rank, i.e., the number of linearly independent equalities. The result is an upper triangular subsystem of equalities: for each equality, the pivot is chosen starting from the right-most columns.
Definition at line 540 of file Linear_System.cc.
References Parma_Polyhedra_Library::Matrix::num_columns(), num_lines_or_equalities(), num_pending_rows(), OK(), set_sorted(), and Parma_Polyhedra_Library::swap().
Referenced by add_to_system_and_check_independence(), Parma_Polyhedra_Library::Polyhedron::simplify(), and simplify().
00540 { 00541 Linear_System& x = *this; 00542 // This method is only applied to a well-formed linear system 00543 // having no pending rows and exactly `n_lines_or_equalities' 00544 // lines or equalities, all of which occur before the rays or points 00545 // or inequalities. 00546 assert(x.OK(true)); 00547 assert(x.num_pending_rows() == 0); 00548 assert(n_lines_or_equalities == x.num_lines_or_equalities()); 00549 #ifndef NDEBUG 00550 for (dimension_type i = n_lines_or_equalities; i-- > 0; ) 00551 assert(x[i].is_line_or_equality()); 00552 #endif 00553 00554 dimension_type rank = 0; 00555 // Will keep track of the variations on the system of equalities. 00556 bool changed = false; 00557 for (dimension_type j = x.num_columns(); j-- > 0; ) 00558 for (dimension_type i = rank; i < n_lines_or_equalities; ++i) { 00559 // Search for the first row having a non-zero coefficient 00560 // (the pivot) in the j-th column. 00561 if (x[i][j] == 0) 00562 continue; 00563 // Pivot found: if needed, swap rows so that this one becomes 00564 // the rank-th row in the linear system. 00565 if (i > rank) { 00566 std::swap(x[i], x[rank]); 00567 // After swapping the system is no longer sorted. 00568 changed = true; 00569 } 00570 // Combine the row containing the pivot with all the lines or 00571 // equalities following it, so that all the elements on the j-th 00572 // column in these rows become 0. 00573 for (dimension_type k = i + 1; k < n_lines_or_equalities; ++k) 00574 if (x[k][j] != 0) { 00575 x[k].linear_combine(x[rank], j); 00576 changed = true; 00577 } 00578 // Already dealt with the rank-th row. 00579 ++rank; 00580 // Consider another column index `j'. 00581 break; 00582 } 00583 if (changed) 00584 x.set_sorted(false); 00585 // A well-formed system is returned. 00586 assert(x.OK(true)); 00587 return rank; 00588 }
void Parma_Polyhedra_Library::Linear_System::back_substitute | ( | dimension_type | n_lines_or_equalities | ) |
Back-substitutes the coefficients to reduce the complexity of the system.
Takes an upper triangular system having n_lines_or_equalities
rows. For each row, starting from the one having the minimum number of coefficients different from zero, computes the expression of an element as a function of the remaining ones and then substitutes this expression in all the other rows.
Definition at line 592 of file Linear_System.cc.
References is_sorted(), Parma_Polyhedra_Library::Linear_Row::linear_combine(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::Matrix::num_columns(), num_lines_or_equalities(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), and set_sorted().
Referenced by Parma_Polyhedra_Library::Polyhedron::simplify(), and simplify().
00592 { 00593 Linear_System& x = *this; 00594 // This method is only applied to a well-formed system 00595 // having no pending rows and exactly `n_lines_or_equalities' 00596 // lines or equalities, all of which occur before the first ray 00597 // or point or inequality. 00598 assert(x.OK(true)); 00599 assert(x.num_columns() >= 1); 00600 assert(x.num_pending_rows() == 0); 00601 assert(n_lines_or_equalities <= x.num_lines_or_equalities()); 00602 #ifndef NDEBUG 00603 for (dimension_type i = n_lines_or_equalities; i-- > 0; ) 00604 assert(x[i].is_line_or_equality()); 00605 #endif 00606 00607 const dimension_type nrows = x.num_rows(); 00608 const dimension_type ncols = x.num_columns(); 00609 // Trying to keep sortedness. 00610 bool still_sorted = x.is_sorted(); 00611 // This deque of Booleans will be used to flag those rows that, 00612 // before exiting, need to be re-checked for sortedness. 00613 std::deque<bool> check_for_sortedness; 00614 if (still_sorted) 00615 check_for_sortedness.insert(check_for_sortedness.end(), nrows, false); 00616 00617 for (dimension_type k = n_lines_or_equalities; k-- > 0; ) { 00618 // For each line or equality, starting from the last one, 00619 // looks for the last non-zero element. 00620 // `j' will be the index of such a element. 00621 Linear_Row& x_k = x[k]; 00622 dimension_type j = ncols - 1; 00623 while (j != 0 && x_k[j] == 0) 00624 --j; 00625 00626 // Go through the equalities above `x_k'. 00627 for (dimension_type i = k; i-- > 0; ) { 00628 Linear_Row& x_i = x[i]; 00629 if (x_i[j] != 0) { 00630 // Combine linearly `x_i' with `x_k' 00631 // so that `x_i[j]' becomes zero. 00632 x_i.linear_combine(x_k, j); 00633 if (still_sorted) { 00634 // Trying to keep sortedness: remember which rows 00635 // have to be re-checked for sortedness at the end. 00636 if (i > 0) 00637 check_for_sortedness[i-1] = true; 00638 check_for_sortedness[i] = true; 00639 } 00640 } 00641 } 00642 00643 // Due to strong normalization during previous iterations, 00644 // the pivot coefficient `x_k[j]' may now be negative. 00645 // Since an inequality (or ray or point) cannot be multiplied 00646 // by a negative factor, the coefficient of the pivot must be 00647 // forced to be positive. 00648 const bool have_to_negate = (x_k[j] < 0); 00649 if (have_to_negate) 00650 for (dimension_type h = ncols; h-- > 0; ) 00651 PPL::neg_assign(x_k[h]); 00652 // Note: we do not mark index `k' in `check_for_sortedness', 00653 // because we will later negate back the row. 00654 00655 // Go through all the other rows of the system. 00656 for (dimension_type i = n_lines_or_equalities; i < nrows; ++i) { 00657 Linear_Row& x_i = x[i]; 00658 if (x_i[j] != 0) { 00659 // Combine linearly the `x_i' with `x_k' 00660 // so that `x_i[j]' becomes zero. 00661 x_i.linear_combine(x_k, j); 00662 if (still_sorted) { 00663 // Trying to keep sortedness: remember which rows 00664 // have to be re-checked for sortedness at the end. 00665 if (i > n_lines_or_equalities) 00666 check_for_sortedness[i-1] = true; 00667 check_for_sortedness[i] = true; 00668 } 00669 } 00670 } 00671 if (have_to_negate) 00672 // Negate `x_k' to restore strong-normalization. 00673 for (dimension_type h = ncols; h-- > 0; ) 00674 PPL::neg_assign(x_k[h]); 00675 } 00676 00677 // Trying to keep sortedness. 00678 for (dimension_type i = 0; still_sorted && i+1 < nrows; ++i) 00679 if (check_for_sortedness[i]) 00680 // Have to check sortedness of `x[i]' with respect to `x[i+1]'. 00681 still_sorted = (compare(x[i], x[i+1]) <= 0); 00682 // Set the sortedness flag. 00683 x.set_sorted(still_sorted); 00684 00685 // A well-formed system is returned. 00686 assert(x.OK(true)); 00687 }
void Parma_Polyhedra_Library::Linear_System::simplify | ( | ) |
Applies Gaussian elimination and back-substitution so as to simplify the linear system.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, and Parma_Polyhedra_Library::Generator_System.
Definition at line 690 of file Linear_System.cc.
References back_substitute(), Parma_Polyhedra_Library::Matrix::erase_to_end(), gauss(), num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), set_sorted(), sorted, Parma_Polyhedra_Library::swap(), and unset_pending_rows().
Referenced by Parma_Polyhedra_Library::Generator_System::simplify(), and Parma_Polyhedra_Library::Constraint_System::simplify().
00690 { 00691 Linear_System& x = *this; 00692 // This method is only applied to a well-formed system 00693 // having no pending rows. 00694 assert(x.OK(true)); 00695 assert(x.num_pending_rows() == 0); 00696 00697 // Partially sort the linear system so that all lines/equalities come first. 00698 dimension_type nrows = x.num_rows(); 00699 dimension_type n_lines_or_equalities = 0; 00700 for (dimension_type i = 0; i < nrows; ++i) 00701 if (x[i].is_line_or_equality()) { 00702 if (n_lines_or_equalities < i) { 00703 std::swap(x[i], x[n_lines_or_equalities]); 00704 // The system was not sorted. 00705 assert(!x.sorted); 00706 } 00707 ++n_lines_or_equalities; 00708 } 00709 // Apply Gaussian elimination to the subsystem of lines/equalities. 00710 const dimension_type rank = x.gauss(n_lines_or_equalities); 00711 // Eliminate any redundant line/equality that has been detected. 00712 if (rank < n_lines_or_equalities) { 00713 const dimension_type 00714 n_rays_or_points_or_inequalities = nrows - n_lines_or_equalities; 00715 const dimension_type 00716 num_swaps = std::min(n_lines_or_equalities - rank, 00717 n_rays_or_points_or_inequalities); 00718 for (dimension_type i = num_swaps; i-- > 0; ) 00719 std::swap(x[--nrows], x[rank + i]); 00720 x.erase_to_end(nrows); 00721 x.unset_pending_rows(); 00722 if (n_rays_or_points_or_inequalities > num_swaps) 00723 x.set_sorted(false); 00724 n_lines_or_equalities = rank; 00725 } 00726 // Apply back-substitution to the system of rays/points/inequalities. 00727 x.back_substitute(n_lines_or_equalities); 00728 // A well-formed system is returned. 00729 assert(x.OK(true)); 00730 }
void Parma_Polyhedra_Library::Linear_System::normalize | ( | ) |
Normalizes the system by dividing each row for the GCD of the row's elements.
Definition at line 453 of file Linear_System.cc.
References Parma_Polyhedra_Library::Matrix::num_rows(), and set_sorted().
Referenced by Parma_Polyhedra_Library::Generator_System::adjust_topology_and_space_dimension().
00453 { 00454 Linear_System& x = *this; 00455 const dimension_type nrows = x.num_rows(); 00456 // We normalize also the pending rows. 00457 for (dimension_type i = nrows; i-- > 0; ) 00458 x[i].normalize(); 00459 set_sorted(nrows <= 1); 00460 }
void Parma_Polyhedra_Library::Linear_System::clear | ( | ) | [inline] |
Clears the system deallocating all its rows.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 139 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::Matrix::clear(), index_first_pending, and sorted.
Referenced by Parma_Polyhedra_Library::Generator_System::clear(), and Parma_Polyhedra_Library::Constraint_System::clear().
00139 { 00140 // Note: do NOT modify the value of `row_topology'. 00141 Matrix::clear(); 00142 index_first_pending = 0; 00143 sorted = true; 00144 }
void Parma_Polyhedra_Library::Linear_System::ascii_dump | ( | ) | const |
Writes to std::cerr
an ASCII representation of *this
.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Referenced by ascii_dump().
void Parma_Polyhedra_Library::Linear_System::ascii_dump | ( | std::ostream & | s | ) | const |
Writes to s
an ASCII representation of *this
.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 113 of file Linear_System.cc.
References ascii_dump(), first_pending_row(), is_necessarily_closed(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), and sorted.
00113 { 00114 // Prints the topology, the number of rows, the number of columns 00115 // and the sorted flag. The specialized methods provided by 00116 // Constraint_System and Generator_System take care of properly 00117 // printing the contents of the system. 00118 const Linear_System& x = *this; 00119 dimension_type x_num_rows = x.num_rows(); 00120 dimension_type x_num_columns = x.num_columns(); 00121 s << "topology " << (is_necessarily_closed() 00122 ? "NECESSARILY_CLOSED" 00123 : "NOT_NECESSARILY_CLOSED") 00124 << "\n" 00125 << x_num_rows << " x " << x_num_columns 00126 << (x.sorted ? "(sorted)" : "(not_sorted)") 00127 << "\n" 00128 << "index_first_pending " << x.first_pending_row() 00129 << "\n"; 00130 for (dimension_type i = 0; i < x_num_rows; ++i) 00131 x[i].ascii_dump(s); 00132 }
void Parma_Polyhedra_Library::Linear_System::print | ( | ) | const |
Prints *this
to std::cerr
using operator<<
.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
bool Parma_Polyhedra_Library::Linear_System::ascii_load | ( | std::istream & | s | ) |
Loads from s
an ASCII representation (as produced by ascii_dump(std::ostream&) const) and sets *this
accordingly. Returns true
if successful, false
otherwise.
Reads into a Linear_System object the information produced by the output of ascii_dump(std::ostream&) const. The specialized methods provided by Constraint_System and Generator_System take care of properly reading the contents of the system.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 137 of file Linear_System.cc.
References Parma_Polyhedra_Library::Matrix::OK(), resize_no_copy(), set_index_first_pending_row(), set_necessarily_closed(), set_not_necessarily_closed(), and set_sorted().
00137 { 00138 std::string str; 00139 if (!(s >> str) || str != "topology") 00140 return false; 00141 if (!(s >> str)) 00142 return false; 00143 if (str == "NECESSARILY_CLOSED") 00144 set_necessarily_closed(); 00145 else { 00146 if (str != "NOT_NECESSARILY_CLOSED") 00147 return false; 00148 set_not_necessarily_closed(); 00149 } 00150 00151 dimension_type nrows; 00152 dimension_type ncols; 00153 if (!(s >> nrows)) 00154 return false; 00155 if (!(s >> str)) 00156 return false; 00157 if (!(s >> ncols)) 00158 return false; 00159 resize_no_copy(nrows, ncols); 00160 00161 if (!(s >> str) || (str != "(sorted)" && str != "(not_sorted)")) 00162 return false; 00163 set_sorted(str == "(sorted)"); 00164 dimension_type index; 00165 if (!(s >> str) || str != "index_first_pending") 00166 return false; 00167 if (!(s >> index)) 00168 return false; 00169 set_index_first_pending_row(index); 00170 00171 Linear_System& x = *this; 00172 for (dimension_type row = 0; row < nrows; ++row) 00173 if (!x[row].ascii_load(s)) 00174 return false; 00175 00176 // Check invariants. 00177 assert(OK(true)); 00178 return true; 00179 }
memory_size_type Parma_Polyhedra_Library::Linear_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.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 36 of file Linear_System.inlines.hh.
References external_memory_in_bytes().
00036 { 00037 return sizeof(*this) + external_memory_in_bytes(); 00038 }
memory_size_type Parma_Polyhedra_Library::Linear_System::external_memory_in_bytes | ( | ) | const [inline] |
Returns the size in bytes of the memory managed by *this
.
Reimplemented from Parma_Polyhedra_Library::Matrix.
Reimplemented in Parma_Polyhedra_Library::Constraint_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Grid_Generator_System.
Definition at line 31 of file Linear_System.inlines.hh.
References Parma_Polyhedra_Library::external_memory_in_bytes().
Referenced by total_memory_in_bytes().
00031 { 00032 return Matrix::external_memory_in_bytes(); 00033 }
bool Parma_Polyhedra_Library::Linear_System::OK | ( | bool | check_strong_normalized = true |
) | const |
Checks if all the invariants are satisfied.
check_strong_normalized | true if and only if the strong normalization of all the rows in the system has to be checked. |
Definition at line 833 of file Linear_System.cc.
References check_sorted(), first_pending_row(), Parma_Polyhedra_Library::Matrix::has_no_rows(), is_necessarily_closed(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Matrix::OK(), Parma_Polyhedra_Library::Matrix::row_capacity, Parma_Polyhedra_Library::Matrix::row_size, sorted, strong_normalize(), and topology().
Referenced by back_substitute(), gauss(), Parma_Polyhedra_Library::Polyhedron::simplify(), and simplify().
00833 { 00834 #ifndef NDEBUG 00835 using std::endl; 00836 using std::cerr; 00837 #endif 00838 00839 // `index_first_pending' must be less than or equal to `num_rows()'. 00840 if (first_pending_row() > num_rows()) { 00841 #ifndef NDEBUG 00842 cerr << "Linear_System has a negative number of pending rows!" 00843 << endl; 00844 #endif 00845 return false; 00846 } 00847 00848 // An empty system is OK, 00849 // unless it is an NNC system with exactly one column. 00850 if (has_no_rows()) { 00851 if (is_necessarily_closed() || num_columns() != 1) 00852 return true; 00853 else { 00854 #ifndef NDEBUG 00855 cerr << "NNC Linear_System has one column" << endl; 00856 #endif 00857 return false; 00858 } 00859 } 00860 00861 // A non-empty system will contain constraints or generators; in 00862 // both cases it must have at least one column for the inhomogeneous 00863 // term and, if it is NNC, another one for the epsilon coefficient. 00864 const dimension_type min_cols = is_necessarily_closed() ? 1 : 2; 00865 if (num_columns() < min_cols) { 00866 #ifndef NDEBUG 00867 cerr << "Linear_System has fewer columns than the minimum " 00868 << "allowed by its topology:" 00869 << endl 00870 << "num_columns is " << num_columns() 00871 << ", minimum is " << min_cols 00872 << endl; 00873 #endif 00874 return false; 00875 } 00876 00877 const Linear_System& x = *this; 00878 const dimension_type n_rows = num_rows(); 00879 for (dimension_type i = 0; i < n_rows; ++i) { 00880 if (!x[i].OK(row_size, row_capacity)) 00881 return false; 00882 // Checking for topology mismatches. 00883 if (x.topology() != x[i].topology()) { 00884 #ifndef NDEBUG 00885 cerr << "Topology mismatch between the system " 00886 << "and one of its rows!" 00887 << endl; 00888 #endif 00889 return false; 00890 } 00891 } 00892 00893 if (check_strong_normalized) { 00894 // Check for strong normalization of rows. 00895 // Note: normalization cannot be checked inside the 00896 // Linear_Row::OK() method, because a Linear_Row object may also 00897 // implement a Linear_Expression object, which in general cannot 00898 // be (strongly) normalized. 00899 Linear_System tmp(x, With_Pending()); 00900 tmp.strong_normalize(); 00901 if (x != tmp) { 00902 #ifndef NDEBUG 00903 cerr << "Linear_System rows are not strongly normalized!" 00904 << endl; 00905 #endif 00906 return false; 00907 } 00908 } 00909 00910 if (sorted && !check_sorted()) { 00911 #ifndef NDEBUG 00912 cerr << "The system declares itself to be sorted but it is not!" 00913 << endl; 00914 #endif 00915 return false; 00916 } 00917 00918 // All checks passed. 00919 return true; 00920 }
void swap | ( | Parma_Polyhedra_Library::Linear_System & | x, | |
Parma_Polyhedra_Library::Linear_System & | y | |||
) | [related] |
Specializes std::swap
.
Definition at line 242 of file Linear_System.inlines.hh.
References swap().
00243 { 00244 x.swap(y); 00245 }
bool operator== | ( | const Linear_System & | x, | |
const Linear_System & | y | |||
) | [related] |
Returns true
if and only if x
and y
are identical.
Definition at line 484 of file Linear_System.cc.
References first_pending_row(), Parma_Polyhedra_Library::Matrix::num_columns(), and Parma_Polyhedra_Library::Matrix::num_rows().
00484 { 00485 if (x.num_columns() != y.num_columns()) 00486 return false; 00487 const dimension_type x_num_rows = x.num_rows(); 00488 const dimension_type y_num_rows = y.num_rows(); 00489 if (x_num_rows != y_num_rows) 00490 return false; 00491 if (x.first_pending_row() != y.first_pending_row()) 00492 return false; 00493 // Notice that calling operator==(const Matrix&, const Matrix&) 00494 // would be wrong here, as equality of the type fields would 00495 // not be checked. 00496 for (dimension_type i = x_num_rows; i-- > 0; ) 00497 if (x[i] != y[i]) 00498 return false; 00499 return true; 00500 }
bool operator!= | ( | const Linear_System & | x, | |
const Linear_System & | y | |||
) | [related] |
Returns true
if and only if x
and y
are different.
Definition at line 226 of file Linear_System.inlines.hh.
The topological kind of the rows in the system.
Definition at line 380 of file Linear_System.defs.hh.
Referenced by add_pending_rows(), add_rows_and_columns(), assign_with_pending(), is_necessarily_closed(), operator=(), resize_no_copy(), set_necessarily_closed(), set_not_necessarily_closed(), swap(), and topology().
The index of the first pending row.
Definition at line 383 of file Linear_System.defs.hh.
Referenced by assign_with_pending(), clear(), first_pending_row(), set_index_first_pending_row(), swap(), and unset_pending_rows().
bool Parma_Polyhedra_Library::Linear_System::sorted [private] |
true
if rows are sorted in the ascending order as defined by bool compare(const Linear_Row&, const Linear_Row&)
. If false
may not be sorted.
Definition at line 390 of file Linear_System.defs.hh.
Referenced by add_pending_rows(), ascii_dump(), assign_with_pending(), clear(), is_sorted(), Linear_System(), OK(), operator=(), set_sorted(), simplify(), sort_rows(), and swap().