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

The base class for systems of constraints and generators. More...

#include <Linear_System.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Linear_System:

Inheritance graph
[legend]
Collaboration diagram for Parma_Polyhedra_Library::Linear_System:

Collaboration graph
[legend]

List of all members.

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_Systemoperator= (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_Rowoperator[] (dimension_type k)
 Returns a reference to the k-th row of the system.
const Linear_Rowoperator[] (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...


Detailed Description

The base class for systems of constraints and generators.

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:

Definition at line 54 of file Linear_System.defs.hh.


Constructor & Destructor Documentation

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 $0$.

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.

Parameters:
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.
Creates a n_rows $\times$ 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 }


Member Function Documentation

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 $\epsilon$-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]

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]

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]

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]

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]

void Parma_Polyhedra_Library::Linear_System::set_not_necessarily_closed (  )  [inline]

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]

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.

Parameters:
new_n_rows The number of rows of the resized system;
new_n_columns The number of columns of the resized system.
The system is expanded to the specified dimensions avoiding reallocation whenever possible. The contents of the original system is lost.

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.

Parameters:
n The number of rows and columns to be added: must be strictly positive.
Turns the system $M \in \Rset^r \times \Rset^c$ into the system $N \in \Rset^{r+n} \times \Rset^{c+n}$ such that $N = \bigl(\genfrac{}{}{0pt}{}{0}{M}\genfrac{}{}{0pt}{}{J}{o}\bigr)$, where $J$ is the specular image of the $n \times n$ identity matrix.

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

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.

Parameters:
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

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.

Parameters:
check_strong_normalized true if and only if the strong normalization of all the rows in the system has to be checked.
By default, the strong normalization check is performed. This check may be turned off to avoid useless repeated checking; e.g., when re-checking a well-formed Linear_System after the permutation or deletion of some of its rows.

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 }


Friends And Related Function Documentation

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.

00226                                                            {
00227   return !(x == y);
00228 }


Member Data Documentation

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

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


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

Generated on Sat Oct 11 10:41:06 2008 for PPL by  doxygen 1.5.6