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

#include <Linear_System.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Linear_System:

Collaboration diagram for Parma_Polyhedra_Library::Linear_System:

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...
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	m_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.)
bool	operator== (const Linear_System &x, const Linear_System &y)
void	swap (Linear_System &x, Linear_System &y)
	Swaps `x` with `y`.
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.
bool	operator!= (const Linear_System &x, const Linear_System &y)
void	swap (Linear_System &x, Linear_System &y)

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:

the topological kind of (all) the rows;
an indication of whether or not some of the rows in the Linear_System are pending, meaning that they still have to undergo an (unspecified) elaboration; if there are pending rows, then these form a proper suffix of the overall sequence of rows;
a Boolean flag that, when true, ensures that the non-pending prefix of the sequence of rows is sorted.

Definition at line 55 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 57 of file Linear_System.inlines.hh.

  : Dense_Matrix(),
    row_topology(topol),
    index_first_pending(0),
    sorted(true) {
}

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 65 of file Linear_System.inlines.hh.

  : Dense_Matrix(n_rows, n_columns, Linear_Row::Flags(topol)),
    row_topology(topol),
    index_first_pending(n_rows),
    sorted(true) {
}

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 95 of file Linear_System.inlines.hh.

References num_pending_rows(), PPL_ASSERT, sorted, and unset_pending_rows().

  : Dense_Matrix(y),
    row_topology(y.row_topology) {
  unset_pending_rows();
  // Previously pending rows may violate sortedness.
  sorted = (y.num_pending_rows() > 0) ? false : y.sorted;
  PPL_ASSERT(num_pending_rows() == 0);
}

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 105 of file Linear_System.inlines.hh.

  : Dense_Matrix(y),
    row_topology(y.row_topology),
    index_first_pending(y.index_first_pending),
    sorted(y.sorted) {
}

Member Function Documentation

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 431 of file Linear_System.cc.

References Parma_Polyhedra_Library::compute_capacity(), Parma_Polyhedra_Library::Dense_Row::insert(), PPL_ASSERT, 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(), and Parma_Polyhedra_Library::Polyhedron::conversion().

                                                             {
  using std::swap;
  const dimension_type new_rows_size = rows.size() + 1;
  if (rows.capacity() < new_rows_size) {
    // Reallocation will take place.
    std::vector<Dense_Row> new_rows;
    new_rows.reserve(compute_capacity(new_rows_size, max_num_rows()));
    new_rows.insert(new_rows.end(), new_rows_size, Dense_Row());
    // Put the new row in place.
    Linear_Row new_row(row_size, row_capacity, flags);
    dimension_type i = new_rows_size-1;
    swap(new_rows[i], new_row);
    // Steal the old rows.
    while (i-- > 0)
      new_rows[i].m_swap(rows[i]);
    // Put the new vector into place.
    swap(rows, new_rows);
  }
  else {
    // Reallocation will NOT take place.
    // Insert a new empty row at the end, then construct it assigning
    // it the given type.
    Dense_Row& new_row = *rows.insert(rows.end(), Dense_Row(flags));
    static_cast<Linear_Row&>(new_row).resize(row_size, row_capacity);
  }

  // The added row was a pending row.
  PPL_ASSERT(num_pending_rows() > 0);
}

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 391 of file Linear_System.cc.

References Parma_Polyhedra_Library::Linear_Row::check_strong_normalized(), Parma_Polyhedra_Library::compute_capacity(), PPL_ASSERT, Parma_Polyhedra_Library::Dense_Row::size(), and Parma_Polyhedra_Library::swap().

                                                     {
  // The added row must be strongly normalized and have the same
  // number of elements of the existing rows of the system.
  PPL_ASSERT(r.check_strong_normalized());
  PPL_ASSERT(r.size() == row_size);

  using std::swap;

  const dimension_type new_rows_size = rows.size() + 1;
  if (rows.capacity() < new_rows_size) {
    // Reallocation will take place.
    std::vector<Dense_Row> new_rows;
    new_rows.reserve(compute_capacity(new_rows_size, max_num_rows()));
    new_rows.insert(new_rows.end(), new_rows_size, Dense_Row());
    // Put the new row in place.
    Dense_Row new_row(r, row_capacity);
    dimension_type i = new_rows_size-1;
    swap(new_rows[i], new_row);
    // Steal the old rows.
    while (i-- > 0)
      new_rows[i].m_swap(rows[i]);
    // Put the new rows into place.
    swap(rows, new_rows);
  }
  else {
    // Reallocation will NOT take place.
    // Inserts a new empty row at the end, then substitutes it with a
    // copy of the given row.
    Dense_Row tmp(r, row_capacity);
    swap(*rows.insert(rows.end(), Dense_Row()), tmp);
  }

  // The added row was a pending row.
  PPL_ASSERT(num_pending_rows() > 0);
  // Do not check for strong normalization, because no modification of
  // rows has occurred.
  PPL_ASSERT(OK(false));
}

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 268 of file Linear_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, Parma_Polyhedra_Library::Dense_Matrix::row_capacity, Parma_Polyhedra_Library::Dense_Matrix::row_size, and Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Polyhedron::intersection_assign(), Parma_Polyhedra_Library::Polyhedron::poly_hull_assign(), and Parma_Polyhedra_Library::Polyhedron::time_elapse_assign().

                                                         {
  Linear_System& x = *this;
  PPL_ASSERT(x.row_size == y.row_size);

  const dimension_type x_n_rows = x.num_rows();
  const dimension_type y_n_rows = y.num_rows();
  // Grow to the required size without changing sortedness.
  const bool was_sorted = sorted;
  add_zero_rows(y_n_rows, Linear_Row::Flags(row_topology));
  sorted = was_sorted;

  // Copy the rows of `y', forcing size and capacity.
  for (dimension_type i = y_n_rows; i-- > 0; ) {
    Dense_Row copy(y[i], x.row_size, x.row_capacity);
    using std::swap;
    swap(copy, x[x_n_rows+i]);
  }
  // Do not check for strong normalization,
  // because no modification of rows has occurred.
  PPL_ASSERT(OK(false));
}

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 353 of file Linear_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::add_row(), Parma_Polyhedra_Library::Linear_Row::check_strong_normalized(), PPL_ASSERT, and Parma_Polyhedra_Library::Dense_Row::size().

                                             {
  // The added row must be strongly normalized and have the same
  // number of elements as the existing rows of the system.
  PPL_ASSERT(r.check_strong_normalized());
  PPL_ASSERT(r.size() == row_size);
  // This method is only used when the system has no pending rows.
  PPL_ASSERT(num_pending_rows() == 0);

  const bool was_sorted = is_sorted();

  Dense_Matrix::add_row(r);

  //  We update `index_first_pending', because it must be equal to
  // `num_rows()'.
  set_index_first_pending_row(num_rows());

  if (was_sorted) {
    const dimension_type nrows = num_rows();
    // The added row may have caused the system to be not sorted anymore.
    if (nrows > 1) {
      // If the system is not empty and the inserted row is the
      // greatest one, the system is set to be sorted.
      // If it is not the greatest one then the system is no longer sorted.
      Linear_System& x = *this;
      set_sorted(compare(x[nrows-2], x[nrows-1]) <= 0);
    }
    else
      // A system having only one row is sorted.
      set_sorted(true);
  }
  // The added row was not a pending row.
  PPL_ASSERT(num_pending_rows() == 0);
  // Do not check for strong normalization, because no modification of
  // rows has occurred.
  PPL_ASSERT(OK(false));
}

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 291 of file Linear_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::has_no_rows(), is_sorted(), num_pending_rows(), and PPL_ASSERT.

Referenced by Parma_Polyhedra_Library::Polyhedron::intersection_assign(), and Parma_Polyhedra_Library::Polyhedron::poly_hull_assign().

                                                 {
  PPL_ASSERT(num_pending_rows() == 0);

  // Adding no rows is a no-op.
  if (y.has_no_rows())
    return;

  // Check if sortedness is preserved.
  if (is_sorted()) {
    if (!y.is_sorted() || y.num_pending_rows() > 0)
      set_sorted(false);
    else {
      // `y' is sorted and has no pending rows.
      const dimension_type n_rows = num_rows();
      if (n_rows > 0)
        set_sorted(compare((*this)[n_rows-1], y[0]) <= 0);
    }
  }

  // Add the rows of `y' as if they were pending.
  add_pending_rows(y);
  // There are no pending_rows.
  unset_pending_rows();

  // Do not check for strong normalization,
  // because no modification of rows has occurred.
  PPL_ASSERT(OK(false));
}

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 752 of file Linear_System.cc.

References c, PPL_ASSERT, Parma_Polyhedra_Library::Linear_Row::set_is_line_or_equality(), and Parma_Polyhedra_Library::swap().

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

                                                             {
  PPL_ASSERT(n > 0);
  const bool was_sorted = is_sorted();
  const dimension_type old_n_rows = num_rows();
  const dimension_type old_n_columns = num_columns();
  add_zero_rows_and_columns(n, n, Linear_Row::Flags(row_topology));
  Linear_System& x = *this;
  // The old system is moved to the bottom.
  using std::swap;
  for (dimension_type i = old_n_rows; i-- > 0; )
    swap(x[i], x[i + n]);
  for (dimension_type i = n, c = old_n_columns; i-- > 0; ) {
    // The top right-hand sub-system (i.e., the system made of new
    // rows and columns) is set to the specular image of the identity
    // matrix.
    Linear_Row& r = x[i];
    r[c++] = 1;
    r.set_is_line_or_equality();
    // Note: `r' is strongly normalized.
  }
  // If the old system was empty, the last row added is either
  // a positivity constraint or a point.
  if (old_n_columns == 0) {
    x[n-1].set_is_ray_or_point_or_inequality();
    // Since ray, points and inequalities come after lines
    // and equalities, this case implies the system is sorted.
    set_sorted(true);
  }
  else if (was_sorted)
    set_sorted(compare(x[n-1], x[n]) <= 0);

  // A well-formed system has to be returned.
  PPL_ASSERT(OK(true));
}

void Parma_Polyhedra_Library::Linear_System::ascii_dump ( ) const

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

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Constraint_System.

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::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Constraint_System.

Definition at line 115 of file Linear_System.cc.

References Parma_Polyhedra_Library::ascii_dump(), first_pending_row(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), and sorted.

                                                {
  // Prints the topology, the number of rows, the number of columns
  // and the sorted flag.  The specialized methods provided by
  // Constraint_System and Generator_System take care of properly
  // printing the contents of the system.
  const Linear_System& x = *this;
  dimension_type x_num_rows = x.num_rows();
  dimension_type x_num_columns = x.num_columns();
  s << "topology " << (is_necessarily_closed()
                       ? "NECESSARILY_CLOSED"
                       : "NOT_NECESSARILY_CLOSED")
    << "\n"
    << x_num_rows << " x " << x_num_columns
    << (x.sorted ? "(sorted)" : "(not_sorted)")
    << "\n"
    << "index_first_pending " << x.first_pending_row()
    << "\n";
  for (dimension_type i = 0; i < x_num_rows; ++i)
    x[i].ascii_dump(s);
}

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::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Constraint_System.

Definition at line 139 of file Linear_System.cc.

References Parma_Polyhedra_Library::ascii_load(), and PPL_ASSERT.

                                          {
  std::string str;
  if (!(s >> str) || str != "topology")
    return false;
  if (!(s >> str))
    return false;
  if (str == "NECESSARILY_CLOSED")
    set_necessarily_closed();
  else {
    if (str != "NOT_NECESSARILY_CLOSED")
      return false;
    set_not_necessarily_closed();
  }

  dimension_type nrows;
  dimension_type ncols;
  if (!(s >> nrows))
    return false;
  if (!(s >> str) || str != "x")
    return false;
  if (!(s >> ncols))
    return false;
  resize_no_copy(nrows, ncols);

  if (!(s >> str) || (str != "(sorted)" && str != "(not_sorted)"))
    return false;
  set_sorted(str == "(sorted)");
  dimension_type index;
  if (!(s >> str) || str != "index_first_pending")
    return false;
  if (!(s >> index))
    return false;
  set_index_first_pending_row(index);

  Linear_System& x = *this;
  for (dimension_type row = 0; row < nrows; ++row)
    if (!x[row].ascii_load(s))
      return false;

  // Check invariants.
  PPL_ASSERT(OK(true));
  return true;
}

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 124 of file Linear_System.inlines.hh.

References index_first_pending, operator=(), row_topology, and sorted.

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

                                                         {
  Dense_Matrix::operator=(y);
  row_topology = y.row_topology;
  index_first_pending = y.index_first_pending;
  sorted = y.sorted;
}

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 608 of file Linear_System.cc.

References is_sorted(), Parma_Polyhedra_Library::Linear_Row::linear_combine(), Parma_Polyhedra_Library::Boundary_NS::neg_assign(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), num_lines_or_equalities(), num_pending_rows(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), OK(), PPL_ASSERT, and set_sorted().

Referenced by simplify(), and Parma_Polyhedra_Library::Polyhedron::simplify().

                                                            {
  Linear_System& x = *this;
  // This method is only applied to a well-formed system
  // having no pending rows and exactly `n_lines_or_equalities'
  // lines or equalities, all of which occur before the first ray
  // or point or inequality.
  PPL_ASSERT(x.OK(true));
  PPL_ASSERT(x.num_columns() >= 1);
  PPL_ASSERT(x.num_pending_rows() == 0);
  PPL_ASSERT(n_lines_or_equalities <= x.num_lines_or_equalities());
#ifndef NDEBUG
  for (dimension_type i = n_lines_or_equalities; i-- > 0; )
    PPL_ASSERT(x[i].is_line_or_equality());
#endif

  const dimension_type nrows = x.num_rows();
  const dimension_type ncols = x.num_columns();
  // Trying to keep sortedness.
  bool still_sorted = x.is_sorted();
  // This deque of Booleans will be used to flag those rows that,
  // before exiting, need to be re-checked for sortedness.
  std::deque<bool> check_for_sortedness;
  if (still_sorted)
    check_for_sortedness.insert(check_for_sortedness.end(), nrows, false);

  for (dimension_type k = n_lines_or_equalities; k-- > 0; ) {
    // For each line or equality, starting from the last one,
    // looks for the last non-zero element.
    // `j' will be the index of such a element.
    Linear_Row& x_k = x[k];
    dimension_type j = ncols - 1;
    while (j != 0 && x_k[j] == 0)
      --j;

    // Go through the equalities above `x_k'.
    for (dimension_type i = k; i-- > 0; ) {
      Linear_Row& x_i = x[i];
      if (x_i[j] != 0) {
        // Combine linearly `x_i' with `x_k'
        // so that `x_i[j]' becomes zero.
        x_i.linear_combine(x_k, j);
        if (still_sorted) {
          // Trying to keep sortedness: remember which rows
          // have to be re-checked for sortedness at the end.
          if (i > 0)
            check_for_sortedness[i-1] = true;
          check_for_sortedness[i] = true;
        }
      }
    }

    // Due to strong normalization during previous iterations,
    // the pivot coefficient `x_k[j]' may now be negative.
    // Since an inequality (or ray or point) cannot be multiplied
    // by a negative factor, the coefficient of the pivot must be
    // forced to be positive.
    const bool have_to_negate = (x_k[j] < 0);
    if (have_to_negate)
      for (dimension_type h = ncols; h-- > 0; )
        PPL::neg_assign(x_k[h]);
    // Note: we do not mark index `k' in `check_for_sortedness',
    // because we will later negate back the row.

    // Go through all the other rows of the system.
    for (dimension_type i = n_lines_or_equalities; i < nrows; ++i) {
      Linear_Row& x_i = x[i];
      if (x_i[j] != 0) {
        // Combine linearly the `x_i' with `x_k'
        // so that `x_i[j]' becomes zero.
        x_i.linear_combine(x_k, j);
        if (still_sorted) {
          // Trying to keep sortedness: remember which rows
          // have to be re-checked for sortedness at the end.
          if (i > n_lines_or_equalities)
            check_for_sortedness[i-1] = true;
          check_for_sortedness[i] = true;
        }
      }
    }
    if (have_to_negate)
      // Negate `x_k' to restore strong-normalization.
      for (dimension_type h = ncols; h-- > 0; )
        PPL::neg_assign(x_k[h]);
  }

  // Trying to keep sortedness.
  for (dimension_type i = 0; still_sorted && i+1 < nrows; ++i)
    if (check_for_sortedness[i])
      // Have to check sortedness of `x[i]' with respect to `x[i+1]'.
      still_sorted = (compare(x[i], x[i+1]) <= 0);
  // Set the sortedness flag.
  x.set_sorted(still_sorted);

  // A well-formed system is returned.
  PPL_ASSERT(x.OK(true));
}

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 846 of file Linear_System.cc.

Referenced by is_sorted(), merge_rows_assign(), and sort_and_remove_with_sat().

                                     {
  const Linear_System& x = *this;
  for (dimension_type i = first_pending_row(); i-- > 1; )
    if (compare(x[i], x[i-1]) < 0)
      return false;
  return true;
}

void Parma_Polyhedra_Library::Linear_System::clear ( )

inline

Clears the system deallocating all its rows.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Generator_System, Parma_Polyhedra_Library::Grid_Generator_System, and Parma_Polyhedra_Library::Constraint_System.

Definition at line 141 of file Linear_System.inlines.hh.

References index_first_pending, and sorted.

                     {
  // Note: do NOT modify the value of `row_topology'.
  Dense_Matrix::clear();
  index_first_pending = 0;
  sorted = true;
}

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::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Constraint_System.

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

Referenced by total_memory_in_bytes().

                                              {
  return Dense_Matrix::external_memory_in_bytes();
}

dimension_type Parma_Polyhedra_Library::Linear_System::first_pending_row ( ) const

inline

Returns the index of the first pending row.

Definition at line 74 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(), Parma_Polyhedra_Library::Constraint_System::ascii_dump(), Parma_Polyhedra_Library::Generator_System::ascii_dump(), ascii_dump(), Parma_Polyhedra_Library::Polyhedron::conversion(), num_pending_rows(), operator==(), sort_and_remove_with_sat(), and sort_pending_and_remove_duplicates().

                                       {
  return index_first_pending;
}

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 555 of file Linear_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::num_columns(), num_lines_or_equalities(), num_pending_rows(), OK(), PPL_ASSERT, set_sorted(), and Parma_Polyhedra_Library::swap().

Referenced by simplify(), and Parma_Polyhedra_Library::Polyhedron::simplify().

                                                                  {
  Linear_System& x = *this;
  // This method is only applied to a well-formed linear system
  // having no pending rows and exactly `n_lines_or_equalities'
  // lines or equalities, all of which occur before the rays or points
  // or inequalities.
  PPL_ASSERT(x.OK(true));
  PPL_ASSERT(x.num_pending_rows() == 0);
  PPL_ASSERT(n_lines_or_equalities == x.num_lines_or_equalities());
#ifndef NDEBUG
  for (dimension_type i = n_lines_or_equalities; i-- > 0; )
    PPL_ASSERT(x[i].is_line_or_equality());
#endif

  dimension_type rank = 0;
  // Will keep track of the variations on the system of equalities.
  bool changed = false;
  for (dimension_type j = x.num_columns(); j-- > 0; )
    for (dimension_type i = rank; i < n_lines_or_equalities; ++i) {
      // Search for the first row having a non-zero coefficient
      // (the pivot) in the j-th column.
      if (x[i][j] == 0)
        continue;
      // Pivot found: if needed, swap rows so that this one becomes
      // the rank-th row in the linear system.
      if (i > rank) {
        using std::swap;
        swap(x[i], x[rank]);
        // After swapping the system is no longer sorted.
        changed = true;
      }
      // Combine the row containing the pivot with all the lines or
      // equalities following it, so that all the elements on the j-th
      // column in these rows become 0.
      for (dimension_type k = i + 1; k < n_lines_or_equalities; ++k)
        if (x[k][j] != 0) {
          x[k].linear_combine(x[rank], j);
          changed = true;
        }
      // Already dealt with the rank-th row.
      ++rank;
      // Consider another column index `j'.
      break;
    }
  if (changed)
    x.set_sorted(false);
  // A well-formed system is returned.
  PPL_ASSERT(x.OK(true));
  return rank;
}

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 184 of file Linear_System.cc.

References Parma_Polyhedra_Library::Linear_Row::check_strong_normalized(), PPL_ASSERT, Parma_Polyhedra_Library::Dense_Row::size(), Parma_Polyhedra_Library::swap(), and Parma_Polyhedra_Library::Linear_Row::topology().

Referenced by Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::Generator_System::insert(), merge_rows_assign(), and Parma_Polyhedra_Library::Polyhedron::simplify_using_context_assign().

                                            {
  // The added row must be strongly normalized and have the same
  // topology of the system.
  PPL_ASSERT(r.check_strong_normalized());
  PPL_ASSERT(topology() == r.topology());
  // This method is only used when the system has no pending rows.
  PPL_ASSERT(num_pending_rows() == 0);

  using std::swap;
  const dimension_type old_num_rows = num_rows();
  const dimension_type old_num_columns = num_columns();
  const dimension_type r_size = r.size();

  // Resize the system, if necessary.
  if (r_size > old_num_columns) {
    add_zero_columns(r_size - old_num_columns);
    if (!is_necessarily_closed() && old_num_rows != 0)
      // Move the epsilon coefficients to the last column
      // (note: sorting is preserved).
      swap_columns(old_num_columns - 1, r_size - 1);
    add_row(r);
  }
  else if (r_size < old_num_columns) {
    // Create a resized copy of the row.
    Linear_Row tmp_row(r, old_num_columns, row_capacity);
    // If needed, move the epsilon coefficient to the last position.
    if (!is_necessarily_closed())
      swap(tmp_row[r_size - 1], tmp_row[old_num_columns - 1]);
    add_row(tmp_row);
  }
  else
    // Here r_size == old_num_columns.
    add_row(r);

  // The added row was not a pending row.
  PPL_ASSERT(num_pending_rows() == 0);
  // Do not check for strong normalization,
  // because no modification of rows has occurred.
  PPL_ASSERT(OK(false));
}

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 226 of file Linear_System.cc.

References Parma_Polyhedra_Library::Linear_Row::check_strong_normalized(), PPL_ASSERT, Parma_Polyhedra_Library::Dense_Row::size(), Parma_Polyhedra_Library::swap(), and Parma_Polyhedra_Library::Linear_Row::topology().

Referenced by Parma_Polyhedra_Library::Constraint_System::insert_pending(), and Parma_Polyhedra_Library::Generator_System::insert_pending().

                                                    {
  // The added row must be strongly normalized and have the same
  // topology of the system.
  PPL_ASSERT(r.check_strong_normalized());
  PPL_ASSERT(topology() == r.topology());

  const dimension_type old_num_rows = num_rows();
  const dimension_type old_num_columns = num_columns();
  const dimension_type r_size = r.size();

  // Resize the system, if necessary.
  if (r_size > old_num_columns) {
    add_zero_columns(r_size - old_num_columns);
    if (!is_necessarily_closed() && old_num_rows != 0)
      // Move the epsilon coefficients to the last column
      // (note: sorting is preserved).
      swap_columns(old_num_columns - 1, r_size - 1);
    add_pending_row(r);
  }
  else if (r_size < old_num_columns)
    if (is_necessarily_closed() || old_num_rows == 0)
      add_pending_row(Linear_Row(r, old_num_columns, row_capacity));
    else {
      // Create a resized copy of the row (and move the epsilon
      // coefficient to its last position).
      using std::swap;
      Linear_Row tmp_row(r, old_num_columns, row_capacity);
      swap(tmp_row[r_size - 1], tmp_row[old_num_columns - 1]);
      add_pending_row(tmp_row);
    }
  else
    // Here r_size == old_num_columns.
    add_pending_row(r);

  // The added row was a pending row.
  PPL_ASSERT(num_pending_rows() > 0);
  // Do not check for strong normalization,
  // because no modification of rows has occurred.
  PPL_ASSERT(OK(false));
}

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 175 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::Constraint_System::add_low_level_constraints(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), Parma_Polyhedra_Library::Generator_System::begin(), Parma_Polyhedra_Library::Polyhedron::is_necessarily_closed(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Constraint_System::satisfies_all_constraints(), and space_dimension().

                                           {
  return row_topology == NECESSARILY_CLOSED;
}

bool Parma_Polyhedra_Library::Linear_System::is_sorted ( ) const

inline

Returns the value of the sortedness flag.

Definition at line 42 of file Linear_System.inlines.hh.

References check_sorted(), PPL_ASSERT, and sorted.

                               {
  // The flag `sorted' does not really reflect the sortedness status
  // of a system (if `sorted' evaluates to `false' nothing is known).
  // This assertion is used to ensure that the system
  // is actually sorted when `sorted' value is 'true'.
  PPL_ASSERT(!sorted || check_sorted());
  return sorted;
}

void Parma_Polyhedra_Library::Linear_System::m_swap ( Linear_System & y )

inline

Swaps *this with y.

Definition at line 132 of file Linear_System.inlines.hh.

References index_first_pending, row_topology, sorted, and swap().

Referenced by swap().

                                      {
  Dense_Matrix::m_swap(y);
  using std::swap;
  swap(row_topology, y.row_topology);
  swap(index_first_pending, y.index_first_pending);
  swap(sorted, y.sorted);
}

dimension_type Parma_Polyhedra_Library::Linear_System::max_space_dimension ( )

inlinestatic

Returns the maximum space dimension a Linear_System can handle.

Reimplemented in Parma_Polyhedra_Library::Generator_System, Parma_Polyhedra_Library::Grid_Generator_System, and Parma_Polyhedra_Library::Constraint_System.

Definition at line 195 of file Linear_System.inlines.hh.

References Parma_Polyhedra_Library::Dense_Matrix::max_num_columns().

                                   {
  // Column zero holds the inhomogeneous term or the divisor.
  // In NNC linear systems, the last column holds the coefficient
  // of the epsilon dimension.
  return max_num_columns() - 2;
}

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 50 of file Linear_System.cc.

References check_sorted(), Parma_Polyhedra_Library::compute_capacity(), Parma_Polyhedra_Library::Dense_Row::insert(), insert(), num_pending_rows(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, Parma_Polyhedra_Library::Dense_Matrix::row_size, and Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Polyhedron::intersection_assign(), Parma_Polyhedra_Library::Polyhedron::poly_hull_assign(), and Parma_Polyhedra_Library::Polyhedron::time_elapse_assign().

                                                          {
  PPL_ASSERT(row_size >= y.row_size);
  // Both systems have to be sorted and have no pending rows.
  PPL_ASSERT(check_sorted() && y.check_sorted());
  PPL_ASSERT(num_pending_rows() == 0 && y.num_pending_rows() == 0);

  using std::swap;
  Linear_System& x = *this;

  // A temporary vector of rows...
  std::vector<Dense_Row> tmp;
  // ... with enough capacity not to require any reallocations.
  tmp.reserve(compute_capacity(x.num_rows() + y.num_rows(), max_num_rows()));

  dimension_type xi = 0;
  dimension_type x_num_rows = x.num_rows();
  dimension_type yi = 0;
  dimension_type y_num_rows = y.num_rows();

  while (xi < x_num_rows && yi < y_num_rows) {
    const int comp = compare(x[xi], y[yi]);
    if (comp <= 0) {
      // Elements that can be taken from `x' are actually _stolen_ from `x'
      swap(x[xi++], *tmp.insert(tmp.end(), Linear_Row()));
      if (comp == 0)
        // A duplicate element.
        ++yi;
    }
    else {
      // (comp > 0)
      Linear_Row copy(y[yi++], row_size, row_capacity);
      swap(copy, *tmp.insert(tmp.end(), Linear_Row()));
    }
  }
  // Insert what is left.
  if (xi < x_num_rows) {
    while (xi < x_num_rows)
      swap(x[xi++], *tmp.insert(tmp.end(), Linear_Row()));
  }
  else {
    while (yi < y_num_rows) {
      Linear_Row copy(y[yi++], row_size, row_capacity);
      swap(copy, *tmp.insert(tmp.end(), Linear_Row()));
    }
  }

  // We get the result vector and let the old one be destroyed.
  swap(tmp, rows);
  // There are no pending rows.
  unset_pending_rows();
  PPL_ASSERT(check_sorted());
}

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 462 of file Linear_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::num_rows().

Referenced by Parma_Polyhedra_Library::Generator_System::adjust_topology_and_space_dimension().

                            {
  Linear_System& x = *this;
  const dimension_type nrows = x.num_rows();
  // We normalize also the pending rows.
  for (dimension_type i = nrows; i-- > 0; )
    x[i].normalize();
  set_sorted(nrows <= 1);
}

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 39 of file Linear_System.cc.

References num_pending_rows(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), and PPL_ASSERT.

Referenced by Parma_Polyhedra_Library::Polyhedron::add_and_minimize(), back_substitute(), and gauss().

                                                {
  PPL_ASSERT(num_pending_rows() == 0);
  const Linear_System& x = *this;
  dimension_type n = 0;
  for (dimension_type i = num_rows(); i-- > 0; )
    if (x[i].is_line_or_equality())
      ++n;
  return n;
}

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 79 of file Linear_System.inlines.hh.

References first_pending_row(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), and PPL_ASSERT.

Referenced by Parma_Polyhedra_Library::Polyhedron::add_and_minimize(), add_rows(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), back_substitute(), gauss(), Linear_System(), merge_rows_assign(), num_lines_or_equalities(), operator=(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Polyhedron::process_pending_constraints(), Parma_Polyhedra_Library::Polyhedron::process_pending_generators(), Parma_Polyhedra_Library::Polyhedron::simplified_constraints(), simplify(), and sort_and_remove_with_sat().

                                      {
  PPL_ASSERT(num_rows() >= first_pending_row());
  return num_rows() - first_pending_row();
}

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 855 of file Linear_System.cc.

References strong_normalize(), and topology().

Referenced by back_substitute(), gauss(), simplify(), and Parma_Polyhedra_Library::Polyhedron::simplify().

                                                             {
#ifndef NDEBUG
  using std::endl;
  using std::cerr;
#endif

  // `index_first_pending' must be less than or equal to `num_rows()'.
  if (first_pending_row() > num_rows()) {
#ifndef NDEBUG
    cerr << "Linear_System has a negative number of pending rows!"
         << endl;
#endif
    return false;
  }

  // An empty system is OK,
  // unless it is an NNC system with exactly one column.
  if (has_no_rows()) {
    if (is_necessarily_closed() || num_columns() != 1)
      return true;
    else {
#ifndef NDEBUG
      cerr << "NNC Linear_System has one column" << endl;
#endif
      return false;
    }
  }

  // A non-empty system will contain constraints or generators; in
  // both cases it must have at least one column for the inhomogeneous
  // term and, if it is NNC, another one for the epsilon coefficient.
  const dimension_type min_cols = is_necessarily_closed() ? 1U : 2U;
  if (num_columns() < min_cols) {
#ifndef NDEBUG
    cerr << "Linear_System has fewer columns than the minimum "
         << "allowed by its topology:"
         << endl
         << "num_columns is " << num_columns()
         << ", minimum is " << min_cols
         << endl;
#endif
    return false;
  }

  const Linear_System& x = *this;
  const dimension_type n_rows = num_rows();
  for (dimension_type i = 0; i < n_rows; ++i) {
    if (!x[i].OK(row_size, row_capacity))
      return false;
    // Checking for topology mismatches.
    if (x.topology() != x[i].topology()) {
#ifndef NDEBUG
      cerr << "Topology mismatch between the system "
           << "and one of its rows!"
           << endl;
#endif
      return false;
    }
  }

  if (check_strong_normalized) {
    // Check for strong normalization of rows.
    // Note: normalization cannot be checked inside the
    // Linear_Row::OK() method, because a Linear_Row object may also
    // implement a Linear_Expression object, which in general cannot
    // be (strongly) normalized.
    Linear_System tmp(x, With_Pending());
    tmp.strong_normalize();
    if (x != tmp) {
#ifndef NDEBUG
      cerr << "Linear_System rows are not strongly normalized!"
           << endl;
#endif
      return false;
    }
  }

  if (sorted && !check_sorted()) {
#ifndef NDEBUG
    cerr << "The system declares itself to be sorted but it is not!"
         << endl;
#endif
    return false;
  }

  // All checks passed.
  return true;
}

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 113 of file Linear_System.inlines.hh.

References num_pending_rows(), PPL_ASSERT, row_topology, sorted, and unset_pending_rows().

Referenced by assign_with_pending().

                                               {
  Dense_Matrix::operator=(y);
  row_topology = y.row_topology;
  unset_pending_rows();
  // Previously pending rows may violate sortedness.
  sorted = (y.num_pending_rows() > 0) ? false : y.sorted;
  PPL_ASSERT(num_pending_rows() == 0);
  return *this;
}

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::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Generator_System, Parma_Polyhedra_Library::Grid_Generator_System, and Parma_Polyhedra_Library::Constraint_System.

Definition at line 180 of file Linear_System.inlines.hh.

Referenced by operator[]().

                                                {
  return static_cast<Linear_Row&>(Dense_Matrix::operator[](k));
}

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::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Generator_System, Parma_Polyhedra_Library::Grid_Generator_System, and Parma_Polyhedra_Library::Constraint_System.

Definition at line 185 of file Linear_System.inlines.hh.

References operator[]().

                                                      {
  return static_cast<const Linear_Row&>(Dense_Matrix::operator[](k));
}

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::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System.

Definition at line 219 of file Linear_System.inlines.hh.

References sign_normalize().

Referenced by Parma_Polyhedra_Library::Polyhedron::map_space_dimensions(), and Parma_Polyhedra_Library::Grid_Generator_System::permute_columns().

                                                                      {
  Dense_Matrix::permute_columns(cycles);
  // The rows with permuted columns are still normalized but may
  // be not strongly normalized: sign normalization is necessary.
  sign_normalize();
}

void Parma_Polyhedra_Library::Linear_System::print ( ) const

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

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Constraint_System.

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::Dense_Matrix.

Definition at line 211 of file Linear_System.inlines.hh.

References strong_normalize().

Referenced by Parma_Polyhedra_Library::Generator_System::adjust_topology_and_space_dimension().

                                                             {
  Dense_Matrix::remove_trailing_columns(n);
  // Have to re-normalize the rows of the system,
  // since we removed some coefficients.
  strong_normalize();
}

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 149 of file Linear_System.inlines.hh.

References row_topology, and set_sorted().

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

                                                                  {
  Dense_Matrix::resize_no_copy(new_n_rows, new_n_columns,
                         Linear_Row::Flags(row_topology));
  // Even though `*this' may happen to keep its sortedness, we believe
  // that checking such a property is not worth the effort.  In fact,
  // it is very likely that the system will be overwritten as soon as
  // we return.
  set_sorted(false);
}

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 90 of file Linear_System.inlines.hh.

References index_first_pending.

Referenced by Parma_Polyhedra_Library::Polyhedron::add_space_dimensions(), Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::Polyhedron::minimize(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), and sort_and_remove_with_sat().

                                                                 {
  index_first_pending = i;
}

void Parma_Polyhedra_Library::Linear_System::set_necessarily_closed ( )

inline

Sets the system topology to NECESSARILY_CLOSED.

Definition at line 161 of file Linear_System.inlines.hh.

References Parma_Polyhedra_Library::Dense_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(), and Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints().

                                      {
  row_topology = NECESSARILY_CLOSED;
  if (!has_no_rows())
    set_rows_topology();
}

void Parma_Polyhedra_Library::Linear_System::set_not_necessarily_closed ( )

inline

Sets the system topology to NOT_NECESSARILY_CLOSED.

Definition at line 168 of file Linear_System.inlines.hh.

References Parma_Polyhedra_Library::Dense_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(), and Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints().

                                          {
  row_topology = NOT_NECESSARILY_CLOSED;
  if (!has_no_rows())
    set_rows_topology();
}

void Parma_Polyhedra_Library::Linear_System::set_rows_topology ( )

Sets the topology of all rows equal to the system topology.

Definition at line 104 of file Linear_System.cc.

Referenced by set_necessarily_closed(), and set_not_necessarily_closed().

                                    {
  Linear_System& x = *this;
  if (is_necessarily_closed())
    for (dimension_type i = num_rows(); i-- > 0; )
      x[i].set_necessarily_closed();
  else
    for (dimension_type i = num_rows(); i-- > 0; )
      x[i].set_not_necessarily_closed();
}

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 52 of file Linear_System.inlines.hh.

References sorted.

                                      {
  sorted = b;
}

void Parma_Polyhedra_Library::Linear_System::sign_normalize ( )

Sign-normalizes the system.

Definition at line 482 of file Linear_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::num_rows().

Referenced by permute_columns(), and Parma_Polyhedra_Library::Polyhedron::simplify().

                                 {
  Linear_System& x = *this;
  const dimension_type nrows = x.num_rows();
  // We sign-normalize also the pending rows.
  for (dimension_type i = num_rows(); i-- > 0; )
    x[i].sign_normalize();
  set_sorted(nrows <= 1);
}

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::Generator_System, and Parma_Polyhedra_Library::Constraint_System.

Definition at line 706 of file Linear_System.cc.

References back_substitute(), gauss(), num_pending_rows(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), OK(), PPL_ASSERT, Parma_Polyhedra_Library::Dense_Matrix::remove_trailing_rows(), set_sorted(), sorted, Parma_Polyhedra_Library::swap(), and unset_pending_rows().

                           {
  Linear_System& x = *this;
  // This method is only applied to a well-formed system
  // having no pending rows.
  PPL_ASSERT(x.OK(true));
  PPL_ASSERT(x.num_pending_rows() == 0);

  // Partially sort the linear system so that all lines/equalities come first.
  const dimension_type old_nrows = x.num_rows();
  dimension_type nrows = old_nrows;
  dimension_type n_lines_or_equalities = 0;
  for (dimension_type i = 0; i < nrows; ++i)
    if (x[i].is_line_or_equality()) {
      if (n_lines_or_equalities < i) {
        using std::swap;
        swap(x[i], x[n_lines_or_equalities]);
        // The system was not sorted.
        PPL_ASSERT(!x.sorted);
      }
      ++n_lines_or_equalities;
    }
  // Apply Gaussian elimination to the subsystem of lines/equalities.
  const dimension_type rank = x.gauss(n_lines_or_equalities);
  // Eliminate any redundant line/equality that has been detected.
  if (rank < n_lines_or_equalities) {
    const dimension_type
      n_rays_or_points_or_inequalities = nrows - n_lines_or_equalities;
    const dimension_type
      num_swaps = std::min(n_lines_or_equalities - rank,
                           n_rays_or_points_or_inequalities);
    using std::swap;
    for (dimension_type i = num_swaps; i-- > 0; )
      swap(x[--nrows], x[rank + i]);
    x.remove_trailing_rows(old_nrows - nrows);
    x.unset_pending_rows();
    if (n_rays_or_points_or_inequalities > num_swaps)
      x.set_sorted(false);
    n_lines_or_equalities = rank;
  }
  // Apply back-substitution to the system of rays/points/inequalities.
  x.back_substitute(n_lines_or_equalities);
  // A well-formed system is returned.
  PPL_ASSERT(x.OK(true));
}

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 512 of file Linear_System.cc.

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

                                                          {
  Linear_System& sys = *this;
  // We can only sort the non-pending part of the system.
  PPL_ASSERT(sys.first_pending_row() == sat.num_rows());
  if (sys.first_pending_row() <= 1) {
    sys.set_sorted(true);
    return;
  }

  // First, sort `sys' (keeping `sat' consistent) without removing duplicates.
  With_Bit_Matrix_iterator first(sys.rows.begin(), sat.rows.begin());
  typedef With_Bit_Matrix_iterator::difference_type diff_type;
  With_Bit_Matrix_iterator last
    = first + static_cast<diff_type>(sat.num_rows());
  Implementation::swapping_sort(first, last, Row_Less_Than());
  // Second, move duplicates in `sys' to the end (keeping `sat' consistent).
  With_Bit_Matrix_iterator new_last
    = Implementation::swapping_unique(first, last);

  const diff_type dist = last - new_last;
  PPL_ASSERT(dist >= 0);
  const dimension_type num_duplicates = static_cast<dimension_type>(dist);
  const dimension_type new_first_pending_row
    = sys.first_pending_row() - num_duplicates;

  if (sys.num_pending_rows() > 0) {
    // In this case, we must put the duplicates after the pending rows.
    using std::swap;
    const dimension_type n_rows = sys.num_rows() - 1;
    for (dimension_type i = 0; i < num_duplicates; ++i)
      swap(sys[new_first_pending_row + i], sys[n_rows - i]);
  }
  // Erasing the duplicated rows...
  sys.remove_trailing_rows(num_duplicates);
  sys.set_index_first_pending_row(new_first_pending_row);
  // ... and the corresponding rows of the saturation matrix.
  sat.remove_trailing_rows(num_duplicates);
  PPL_ASSERT(sys.check_sorted());
  // Now the system is sorted.
  sys.set_sorted(true);
}

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 788 of file Linear_System.cc.

References Parma_Polyhedra_Library::cmp(), first_pending_row(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, Parma_Polyhedra_Library::Dense_Matrix::remove_trailing_rows(), sort_rows(), and Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Polyhedron::process_pending_constraints(), and Parma_Polyhedra_Library::Polyhedron::process_pending_generators().

                                                     {
  PPL_ASSERT(num_pending_rows() > 0);
  PPL_ASSERT(is_sorted());
  Linear_System& x = *this;

  // The non-pending part of the system is already sorted.
  // Now sorting the pending part..
  const dimension_type first_pending = x.first_pending_row();
  x.sort_rows(first_pending, x.num_rows());
  // Recompute the number of rows, because we may have removed
  // some rows occurring more than once in the pending part.
  const dimension_type old_num_rows = x.num_rows();
  dimension_type num_rows = old_num_rows;

  dimension_type k1 = 0;
  dimension_type k2 = first_pending;
  dimension_type num_duplicates = 0;
  // In order to erase them, put at the end of the system
  // those pending rows that also occur in the non-pending part.
  using std::swap;
  while (k1 < first_pending && k2 < num_rows) {
    const int cmp = compare(x[k1], x[k2]);
    if (cmp == 0) {
      // We found the same row.
      ++num_duplicates;
      --num_rows;
      // By initial sortedness, we can increment index `k1'.
      ++k1;
      // Do not increment `k2'; instead, swap there the next pending row.
      if (k2 < num_rows)
        swap(x[k2], x[k2 + num_duplicates]);
    }
    else if (cmp < 0)
      // By initial sortedness, we can increment `k1'.
      ++k1;
    else {
      // Here `cmp > 0'.
      // Increment `k2' and, if we already found any duplicate,
      // swap the next pending row in position `k2'.
      ++k2;
      if (num_duplicates > 0 && k2 < num_rows)
        swap(x[k2], x[k2 + num_duplicates]);
    }
  }
  // If needed, swap any duplicates found past the pending rows
  // that has not been considered yet; then erase the duplicates.
  if (num_duplicates > 0) {
    if (k2 < num_rows)
      for (++k2; k2 < num_rows; ++k2)
        swap(x[k2], x[k2 + num_duplicates]);
    x.remove_trailing_rows(old_num_rows - num_rows);
  }
  // Do not check for strong normalization,
  // because no modification of rows has occurred.
  PPL_ASSERT(OK(false));
}

void Parma_Polyhedra_Library::Linear_System::sort_rows ( )

Sorts the non-pending rows (in growing order) and eliminates duplicated ones.

Definition at line 321 of file Linear_System.cc.

References PPL_ASSERT.

Referenced by Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension(), 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().

                            {
  const dimension_type num_pending = num_pending_rows();
  // We sort the non-pending rows only.
  sort_rows(0, first_pending_row());
  set_index_first_pending_row(num_rows() - num_pending);
  sorted = true;
  // Do not check for strong normalization,
  // because no modification of rows has occurred.
  PPL_ASSERT(OK(false));
}

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 333 of file Linear_System.cc.

References Parma_Polyhedra_Library::nth_iter(), PPL_ASSERT, Parma_Polyhedra_Library::Implementation::swapping_sort(), and Parma_Polyhedra_Library::Implementation::swapping_unique().

                                                             {
  PPL_ASSERT(first_row <= last_row && last_row <= num_rows());
  // We cannot mix pending and non-pending rows.
  PPL_ASSERT(first_row >= first_pending_row() || last_row <= first_pending_row());

  // First sort without removing duplicates.
  std::vector<Dense_Row>::iterator first = nth_iter(rows, first_row);
  std::vector<Dense_Row>::iterator last = nth_iter(rows, last_row);
  Implementation::swapping_sort(first, last, Row_Less_Than());
  // Second, move duplicates to the end.
  std::vector<Dense_Row>::iterator new_last
    = Implementation::swapping_unique(first, last);
  // Finally, remove duplicates.
  rows.erase(new_last, last);
  // NOTE: we cannot check all invariants of the system here,
  // because the caller still has to update `index_first_pending'.
}

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::Generator_System, Parma_Polyhedra_Library::Grid_Generator_System, and Parma_Polyhedra_Library::Constraint_System.

Definition at line 203 of file Linear_System.inlines.hh.

References is_necessarily_closed(), and Parma_Polyhedra_Library::Dense_Matrix::num_columns().

                                     {
  const dimension_type n_columns = num_columns();
  return (n_columns == 0)
    ? 0
    : (n_columns - (is_necessarily_closed() ? 1U : 2U));
}

void Parma_Polyhedra_Library::Linear_System::strong_normalize ( )

Strongly normalizes the system.

Definition at line 472 of file Linear_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::num_rows().

Referenced by Parma_Polyhedra_Library::Generator_System::affine_image(), Parma_Polyhedra_Library::Constraint_System::affine_preimage(), OK(), Parma_Polyhedra_Library::Polyhedron::OK(), and remove_trailing_columns().

                                   {
  Linear_System& x = *this;
  const dimension_type nrows = x.num_rows();
  // We strongly normalize also the pending rows.
  for (dimension_type i = nrows; i-- > 0; )
    x[i].strong_normalize();
  set_sorted(nrows <= 1);
}

Topology Parma_Polyhedra_Library::Linear_System::topology ( ) const

inline

Returns the system topology.

Definition at line 190 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::Polyhedron::BHRZ03_combining_constraints(), Parma_Polyhedra_Library::Polyhedron::conversion(), Parma_Polyhedra_Library::Polyhedron::minimize(), OK(), Parma_Polyhedra_Library::Polyhedron::select_CH78_constraints(), Parma_Polyhedra_Library::Polyhedron::select_H79_constraints(), and Parma_Polyhedra_Library::Polyhedron::topology().

                              {
  return row_topology;
}

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::Dense_Matrix.

Reimplemented in Parma_Polyhedra_Library::Grid_Generator_System, Parma_Polyhedra_Library::Generator_System, and Parma_Polyhedra_Library::Constraint_System.

Definition at line 37 of file Linear_System.inlines.hh.

References external_memory_in_bytes().

                                           {
  return sizeof(*this) + external_memory_in_bytes();
}

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 85 of file Linear_System.inlines.hh.

References index_first_pending, and Parma_Polyhedra_Library::Dense_Matrix::num_rows().

                                  {
  index_first_pending = num_rows();
}

Friends And Related Function Documentation

bool operator!=	(	const Linear_System &	x,
		const Linear_System &	y
	)

                                                           {
  return !(x == y);
}

bool operator!=	(	const Linear_System &	x,
		const Linear_System &	y
	)

Referenced by Parma_Polyhedra_Library::Grid_Generator_System::const_iterator::operator!=().

bool operator==	(	const Linear_System &	x,
		const Linear_System &	y
	)

bool operator==	(	const Linear_System &	x,
		const Linear_System &	y
	)

References first_pending_row(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), and Parma_Polyhedra_Library::Dense_Matrix::num_rows().

                                                              {
  if (x.num_columns() != y.num_columns())
    return false;
  const dimension_type x_num_rows = x.num_rows();
  const dimension_type y_num_rows = y.num_rows();
  if (x_num_rows != y_num_rows)
    return false;
  if (x.first_pending_row() != y.first_pending_row())
    return false;
  // Notice that calling operator==(const Dense_Matrix&, const Dense_Matrix&)
  // would be wrong here, as equality of the type fields would
  // not be checked.
  for (dimension_type i = x_num_rows; i-- > 0; )
    if (x[i] != y[i])
      return false;
  return true;
}

void swap	(	Linear_System &	x,
		Linear_System &	y
	)

References m_swap().

                                         {
  x.m_swap(y);
}

void swap	(	Linear_System &	x,
		Linear_System &	y
	)

Referenced by m_swap().

Member Data Documentation

dimension_type Parma_Polyhedra_Library::Linear_System::index_first_pending

private

The index of the first pending row.

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

Referenced by assign_with_pending(), clear(), first_pending_row(), m_swap(), set_index_first_pending_row(), and unset_pending_rows().

Topology Parma_Polyhedra_Library::Linear_System::row_topology

private

The topological kind of the rows in the system.

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

Referenced by assign_with_pending(), is_necessarily_closed(), m_swap(), operator=(), resize_no_copy(), set_necessarily_closed(), set_not_necessarily_closed(), and topology().

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 391 of file Linear_System.defs.hh.

Referenced by ascii_dump(), assign_with_pending(), clear(), is_sorted(), Linear_System(), m_swap(), operator=(), set_sorted(), and simplify().

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

Classes

Public Member Functions

Static Public Member Functions

Private Attributes

Related Functions

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation