A system of congruences. More...

#include <Congruence_System.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Congruence_System:

Collaboration diagram for Parma_Polyhedra_Library::Congruence_System:

Classes
class	const_iterator
	An iterator over a system of congruences. More...
Public Member Functions
	Congruence_System ()
	Default constructor: builds an empty system of congruences.
	Congruence_System (const Congruence &cg)
	Builds the singleton system containing only congruence `cg`.
	Congruence_System (const Constraint &c)
	If `c` represents the constraint , builds the singleton system containing only constraint $e_1 = e_2 \pmod{0}$ .
	Congruence_System (const Constraint_System &cs)
	Builds a system containing copies of any equalities in `cs`.
	Congruence_System (const Congruence_System &cgs)
	Ordinary copy constructor.
	~Congruence_System ()
	Destructor.
Congruence_System &	operator= (const Congruence_System &y)
	Assignment operator.
dimension_type	space_dimension () const
	Returns the dimension of the vector space enclosing `*this`.
bool	is_equal_to (const Congruence_System &y) const
	Returns `true` if and only if `*this` is exactly equal to `y`.
bool	has_linear_equalities () const
	Returns `true` if and only if `*this` contains one or more linear equalities.
void	clear ()
	Removes all the congruences and sets the space dimension to 0.
void	insert (const Congruence &cg)
	Inserts in `*this` a copy of the congruence `cg`, increasing the number of space dimensions if needed.
void	insert (const Constraint &c)
	Inserts in `*this` a copy of the equality constraint `c`, seen as a modulo 0 congruence, increasing the number of space dimensions if needed.
void	insert (const Congruence_System &y)
	Inserts in `*this` a copy of the congruences in `y`, increasing the number of space dimensions if needed.
void	recycling_insert (Congruence_System &cgs)
	Inserts into `*this` the congruences in `cgs`, increasing the number of space dimensions if needed.
bool	empty () const
	Returns `true` if and only if `*this` has no congruences.
const_iterator	begin () const
	Returns the const_iterator pointing to the first congruence, if `*this` is not empty; otherwise, returns the past-the-end const_iterator.
const_iterator	end () const
	Returns the past-the-end const_iterator.
bool	OK () const
	Checks if all the invariants are satisfied.
void	ascii_dump () const
	Writes to `std::cerr` an ASCII representation of `*this`.
void	ascii_dump (std::ostream &s) const
	Writes to `s` an ASCII representation of `*this`.
void	print () const
	Prints `*this` to `std::cerr` using `operator<<`.
bool	ascii_load (std::istream &s)
	Loads from `s` an ASCII representation (as produced by ascii_dump(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`.
dimension_type	num_equalities () const
	Returns the number of equalities.
dimension_type	num_proper_congruences () const
	Returns the number of proper congruences.
void	m_swap (Congruence_System &y)
	Swaps `*this` with `y`.
void	add_unit_rows_and_columns (dimension_type dims)
	Adds `dims` rows and `dims` columns of zeroes to the matrix, initializing the added rows as in the unit congruence system.
Static Public Member Functions
static dimension_type	max_space_dimension ()
	Returns the maximum space dimension a Congruence_System can handle.
static void	initialize ()
	Initializes the class.
static void	finalize ()
	Finalizes the class.
static const Congruence_System &	zero_dim_empty ()
	Returns the system containing only Congruence::zero_dim_false().
Protected Member Functions
bool	satisfies_all_congruences (const Grid_Generator &g) const
	Returns `true` if `g` satisfies all the congruences.
Private Member Functions
	Congruence_System (dimension_type d)
	Builds an empty (i.e. zero rows) system of dimension `d`.
void	concatenate (const Congruence_System &y)
	Concatenates copies of the congruences from `y` onto `*this`.
void	normalize_moduli ()
	Adjusts all expressions to have the same moduli.
bool	increase_space_dimension (dimension_type new_space_dim)
	Increase the number of space dimensions to `new_space_dim`.
void	insert_verbatim (const Congruence &cg)
	Inserts in `*this` an exact copy of the congruence `cg`, increasing the number of space dimensions if needed.
Congruence &	operator[] (dimension_type k)
	Returns the `k-` th congruence of the system.
const Congruence &	operator[] (dimension_type k) const
	Returns a constant reference to the `k-` th congruence of the system.
bool	has_a_free_dimension () const
	Returns `true` if and only if any of the dimensions in `*this` is free of constraint.
void	affine_preimage (dimension_type v, const Linear_Expression &expr, Coefficient_traits::const_reference denominator)
	Substitutes a given column of coefficients by a given affine expression.
void	remove_higher_space_dimensions (dimension_type new_dimension)
	Removes the higher dimensions of the system so that the resulting system will have dimension `new_dimension`.
void	resize_no_copy (dimension_type new_num_rows, dimension_type new_num_columns)
	Resizes the system without worrying about the old contents.
Static Private Attributes
static const Congruence_System *	zero_dim_empty_p = 0
	Holds (between class initialization and finalization) a pointer to the singleton system containing only Congruence::zero_dim_false().
Friends
class	const_iterator
class	Grid
class	Grid_Certificate
bool	operator== (const Congruence_System &x, const Congruence_System &y)
Related Functions
(Note that these are not member functions.)
std::ostream &	operator<< (std::ostream &s, const Congruence_System &cgs)
std::ostream &	operator<< (std::ostream &s, const Congruence_System &cgs)
bool	operator== (const Congruence_System &x, const Congruence_System &y)
std::ostream &	operator<< (std::ostream &s, const Congruence_System &cgs)
	Output operator.
void	swap (Congruence_System &x, Congruence_System &y)
	Swaps `x` with `y`.
void	swap (Congruence_System &x, Congruence_System &y)

Detailed Description

A system of congruences.

An object of the class Congruence_System is a system of congruences, i.e., a multiset of objects of the class Congruence. When inserting congruences in a system, space dimensions are automatically adjusted so that all the congruences in the system are defined on the same vector space.

In all the examples it is assumed that variables x and y are defined as follows:

  Variable x(0);
  Variable y(1);

Example 1

The following code builds a system of congruences corresponding to an integer grid in $\Rset^2$ :

  Congruence_System cgs;
  cgs.insert(x %= 0);
  cgs.insert(y %= 0);

Note that: the congruence system is created with space dimension zero; the first and second congruence insertions increase the space dimension to $1$

and

, respectively.

Example 2

By adding to the congruence system of the previous example, the congruence $x + y = 1 \pmod{2}$ :

  cgs.insert((x + y %= 1) / 2);

we obtain the grid containing just those integral points where the sum of the x and y values is odd.

Example 3

The following code builds a system of congruences corresponding to the grid in $\Zset^2$ containing just the integral points on the x axis:

  Congruence_System cgs;
  cgs.insert(x %= 0);
  cgs.insert((y %= 0) / 0);

Note:: After inserting a multiset of congruences in a congruence system, there are no guarantees that an exact copy of them can be retrieved: in general, only an equivalent congruence system will be available, where original congruences may have been reordered, removed (if they are trivial, duplicate or implied by other congruences), linearly combined, etc.

Definition at line 115 of file Congruence_System.defs.hh.

Constructor & Destructor Documentation

Parma_Polyhedra_Library::Congruence_System::Congruence_System ( )

inline

Default constructor: builds an empty system of congruences.

Definition at line 49 of file Congruence_System.inlines.hh.

  : Dense_Matrix(0, 2) {
}

Parma_Polyhedra_Library::Congruence_System::Congruence_System ( const Congruence & cg )

inlineexplicit

Builds the singleton system containing only congruence cg.

Definition at line 54 of file Congruence_System.inlines.hh.

References insert().

  : Dense_Matrix(0, 2) {
  insert(cg);
}

Parma_Polyhedra_Library::Congruence_System::Congruence_System ( const Constraint & c )

inlineexplicit

If c represents the constraint $ e_1 = e_2 $ , builds the singleton system containing only constraint $e_1 = e_2 \pmod{0}$ .

Exceptions:

std::invalid_argument Thrown if c is not an equality constraint.

Definition at line 60 of file Congruence_System.inlines.hh.

References insert().

  : Dense_Matrix(0, 2) {
  insert(c);
}

Parma_Polyhedra_Library::Congruence_System::Congruence_System ( const Constraint_System & cs )

explicit

Builds a system containing copies of any equalities in cs.

Definition at line 40 of file Congruence_System.cc.

References Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), and insert().

  : Dense_Matrix(0, cs.space_dimension() + 2) {
  for (Constraint_System::const_iterator i = cs.begin(),
         cs_end = cs.end(); i != cs_end; ++i)
    if (i->is_equality())
      insert(*i);
}

Parma_Polyhedra_Library::Congruence_System::Congruence_System ( const Congruence_System & cgs )

inline

Ordinary copy constructor.

Definition at line 66 of file Congruence_System.inlines.hh.

  : Dense_Matrix(cgs) {
}

Parma_Polyhedra_Library::Congruence_System::~Congruence_System ( )

inline

Destructor.

Definition at line 76 of file Congruence_System.inlines.hh.

{
}

Parma_Polyhedra_Library::Congruence_System::Congruence_System ( dimension_type d )

inlineexplicitprivate

Builds an empty (i.e. zero rows) system of dimension d.

Definition at line 71 of file Congruence_System.inlines.hh.

  : Dense_Matrix(0, d + 2) {
}

Member Function Documentation

void Parma_Polyhedra_Library::Congruence_System::add_unit_rows_and_columns ( dimension_type dims )

Adds dims rows and dims columns of zeroes to the matrix, initializing the added rows as in the unit congruence system.

Parameters:

dims	The number of rows and columns to be added: must be strictly positive.

Turns the $r \times c$ matrix $A$ into the $(r+dims) \times (c+dims)$ matrix $\bigl(\genfrac{}{}{0pt}{}{0}{A} \genfrac{}{}{0pt}{}{B}{A}\bigr)$ where $B$ is the $dims \times dims$ unit matrix of the form $\bigl(\genfrac{}{}{0pt}{}{0}{1} \genfrac{}{}{0pt}{}{1}{0}\bigr)$ . The matrix is expanded avoiding reallocation whenever possible.

Definition at line 519 of file Congruence_System.cc.

References Parma_Polyhedra_Library::Linear_Row::LINE_OR_EQUALITY, Parma_Polyhedra_Library::NECESSARILY_CLOSED, PPL_ASSERT, and Parma_Polyhedra_Library::swap().

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

                                                                   {
  PPL_ASSERT(num_columns() > 0);
  dimension_type col = num_columns() - 1;
  dimension_type old_num_rows = num_rows();
  add_zero_rows_and_columns(dims, dims,
                            Linear_Row::Flags(NECESSARILY_CLOSED,
                                              Linear_Row::LINE_OR_EQUALITY));
  // Swap the modulus column into the new last column.
  swap_columns(col, col + dims);

  Congruence_System& cgs = *this;
  // Swap the added columns to the front of the matrix.
  using std::swap;
  for (dimension_type row = old_num_rows; row-- > 0; )
    swap(cgs[row], cgs[row + dims]);

  col += dims - 1;
  // Set the diagonal element of each added row.
  for (dimension_type row = dims; row-- > 0; )
    cgs[row][col - row] = 1;
}

void Parma_Polyhedra_Library::Congruence_System::affine_preimage	(	dimension_type	v,
		const Linear_Expression &	expr,
		Coefficient_traits::const_reference	denominator
	)

private

Substitutes a given column of coefficients by a given affine expression.

Parameters:

v	Index of the column to which the affine transformation is substituted;
expr	The numerator of the affine transformation: $\sum_{i = 0}^{n - 1} a_i x_i + b$ ;
denominator	The denominator of the affine transformation.

We allow affine transformations (see the Section Operations on Rational Grids) to have rational coefficients. Since the coefficients of linear expressions are integers we also provide an integer denominator that will be used as denominator of the affine transformation. The denominator is required to be a positive integer and its default value is 1.

The affine transformation substitutes the matrix of congruences by a new matrix whose elements ${a'}_{ij}$ are built from the old one $a_{ij}$ as follows:

${a'}_{ij} = \begin{cases} a_{ij} * \mathrm{denominator} + a_{iv} * \mathrm{expr}[j] \quad \text{for } j \neq v; \\ \mathrm{expr}[v] * a_{iv} \quad \text{for } j = v. \end{cases}$

expr is a constant parameter and unaltered by this computation.

Definition at line 352 of file Congruence_System.cc.

References Parma_Polyhedra_Library::add_mul_assign(), PPL_ASSERT, Parma_Polyhedra_Library::Dense_Row::size(), and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

                                                               {
  // `v' is the index of a column corresponding to a "user" variable
  // (i.e., it cannot be the inhomogeneous term).
  PPL_ASSERT(v > 0 && v <= space_dimension());
  PPL_ASSERT(expr.space_dimension() <= space_dimension());
  PPL_ASSERT(denominator > 0);

  const dimension_type num_columns = this->num_columns();
  const dimension_type num_rows = this->num_rows();
  const dimension_type expr_size = expr.size();
  const bool not_invertible = (v >= expr_size || expr[v] == 0);
  Congruence_System& x = *this;

  if (denominator == 1)
    // Optimized computation only considering columns having indexes <
    // expr_size.
    for (dimension_type i = num_rows; i-- > 0; ) {
      Congruence& row = x[i];
      Coefficient& row_v = row[v];
      if (row_v != 0) {
        for (dimension_type j = expr_size; j-- > 0; )
          if (j != v)
            // row[j] = row[j] + row_v * expr[j]
            add_mul_assign(row[j], row_v, expr[j]);
        if (not_invertible)
          row_v = 0;
        else
          row_v *= expr[v];
      }
    }
  else
    for (dimension_type i = num_rows; i-- > 0; ) {
      Congruence& row = x[i];
      Coefficient& row_v = row[v];
      if (row_v != 0) {
        for (dimension_type j = num_columns; j-- > 0; )
          if (j != v) {
            Coefficient& row_j = row[j];
            row_j *= denominator;
            if (j < expr_size)
              add_mul_assign(row_j, row_v, expr[j]);
          }
        if (not_invertible)
          row_v = 0;
        else
          row_v *= expr[v];
      }
    }
}

void Parma_Polyhedra_Library::Congruence_System::ascii_dump ( std::ostream & s ) const

Writes to s an ASCII representation of *this.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 405 of file Congruence_System.cc.

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

                                                    {
  const Congruence_System& x = *this;
  dimension_type x_num_rows = x.num_rows();
  dimension_type x_num_columns = x.num_columns();
  s << x_num_rows << " x " << x_num_columns
    << std::endl;
  if (x_num_rows > 0 && x_num_columns > 0)
    for (dimension_type i = 0; i < x_num_rows; ++i)
      x[i].ascii_dump(s);
}

void Parma_Polyhedra_Library::Congruence_System::ascii_dump ( ) const

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

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Referenced by Parma_Polyhedra_Library::Grid::OK().

bool Parma_Polyhedra_Library::Congruence_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.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 419 of file Congruence_System.cc.

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

                                              {
  std::string str;
  dimension_type num_rows;
  dimension_type num_columns;
  if (!(s >> num_rows))
    return false;
  if (!(s >> str) || str != "x")
    return false;
  if (!(s >> num_columns))
    return false;
  resize_no_copy(num_rows, num_columns);

  Congruence_System& x = *this;
  for (dimension_type i = 0; i < x.num_rows(); ++i)
    if (!x[i].ascii_load(s))
      return false;

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

Congruence_System::const_iterator Parma_Polyhedra_Library::Congruence_System::begin ( ) const

inline

Returns the const_iterator pointing to the first congruence, if *this is not empty; otherwise, returns the past-the-end const_iterator.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 177 of file Congruence_System.inlines.hh.

References Parma_Polyhedra_Library::Dense_Matrix::begin(), and Parma_Polyhedra_Library::Congruence_System::const_iterator::skip_forward().

                               {
  const_iterator i(Dense_Matrix::begin(), *this);
  i.skip_forward();
  return i;
}

void Parma_Polyhedra_Library::Congruence_System::clear ( )

inline

Removes all the congruences and sets the space dimension to 0.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 96 of file Congruence_System.inlines.hh.

References Parma_Polyhedra_Library::Dense_Matrix::add_zero_columns().

                         {
  Dense_Matrix::clear();
  add_zero_columns(2);          // Modulus and constant term.
}

void Parma_Polyhedra_Library::Congruence_System::concatenate ( const Congruence_System & y )

private

Concatenates copies of the congruences from y onto *this.

Parameters:

y	The congruence system to append to `this`. The number of rows in `y` must be strictly positive.

The matrix for the new system of congruences is obtained by leaving the old system in the upper left-hand side and placing the congruences of y in the lower right-hand side, and padding with zeroes.

Definition at line 542 of file Congruence_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::num_columns(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), space_dimension(), and Parma_Polyhedra_Library::swap().

                                                            {
  // TODO: this implementation is just an executable specification.
  Congruence_System cgs = y;

  dimension_type added_rows = cgs.num_rows();
  dimension_type added_columns = cgs.space_dimension();

  dimension_type old_num_rows = num_rows();
  dimension_type old_modi = num_columns() - 1;
  dimension_type old_space_dim = space_dimension();

  add_zero_rows_and_columns(added_rows, added_columns, Dense_Row::Flags());

  dimension_type cgs_num_columns = cgs.num_columns();
  dimension_type modi = num_columns() - 1;

  // Swap the modulus and the new last column, in the old rows.
  for (dimension_type i = old_num_rows; i-- > 0; ) {
    Congruence& cg = (*this)[i];
    using std::swap;
    swap(cg[old_modi], cg[modi]);
  }

  // Move the congruences into *this from `cgs', shifting the
  // coefficients along into the appropriate columns.
  for (dimension_type i = added_rows; i-- > 0; ) {
    Congruence& cg_old = cgs[i];
    Congruence& cg_new = (*this)[old_num_rows + i];
    using std::swap;
    // The inhomogeneous term is moved to the same column.
    swap(cg_new[0], cg_old[0]);
    // All homogeneous terms are shifted by `space_dim' columns.
    for (dimension_type j = cgs_num_columns; j-- > 1; )
      swap(cg_old[j], cg_new[old_space_dim + j]);
  }
}

bool Parma_Polyhedra_Library::Congruence_System::empty ( ) const

inline

Returns true if and only if *this has no congruences.

Definition at line 190 of file Congruence_System.inlines.hh.

References begin(), and end().

                               {
  return begin() == end();
}

Congruence_System::const_iterator Parma_Polyhedra_Library::Congruence_System::end ( ) const

inline

Returns the past-the-end const_iterator.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 184 of file Congruence_System.inlines.hh.

References Parma_Polyhedra_Library::Dense_Matrix::end().

                             {
  const const_iterator i(Dense_Matrix::end(), *this);
  return i;
}

memory_size_type Parma_Polyhedra_Library::Congruence_System::external_memory_in_bytes ( ) const

inline

Returns the size in bytes of the memory managed by *this.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 200 of file Congruence_System.inlines.hh.

                                                  {
  return Dense_Matrix::external_memory_in_bytes();
}

void Parma_Polyhedra_Library::Congruence_System::finalize ( )

static

Finalizes the class.

Definition at line 451 of file Congruence_System.cc.

References PPL_ASSERT.

Referenced by Parma_Polyhedra_Library::Init::~Init().

                               {
  PPL_ASSERT(zero_dim_empty_p != 0);
  delete zero_dim_empty_p;
  zero_dim_empty_p = 0;
}

bool Parma_Polyhedra_Library::Congruence_System::has_a_free_dimension ( ) const

private

Returns true if and only if any of the dimensions in *this is free of constraint.

Any equality or proper congruence affecting a dimension constrains that dimension.

This method assumes the system is in minimal form.

Definition at line 318 of file Congruence_System.cc.

References PPL_ASSERT.

                                                 {
  // Search for a dimension that is free of any congruence or equality
  // constraint.  Assumes a minimized system.
  dimension_type space_dim = space_dimension();
  std::vector<bool> free_dim(space_dim, true);
  dimension_type free_dims = space_dim;
  for (dimension_type row = num_rows(); row-- > 0; ) {
    const Congruence& cg = (*this)[row];
    for (dimension_type dim = space_dim; dim-- > 0; )
      if (free_dim[dim] && cg[dim+1] != 0) {
        if (--free_dims == 0) {
          // All dimensions are constrained.
#ifndef NDEBUG
          free_dim[dim] = false;
          // Check that there are free_dims dimensions marked free
          // in free_dim.
          dimension_type count = 0;
          for (dimension_type i = space_dim; i-- > 0; ) {
            if (free_dim[i])
              ++count;
          }
          PPL_ASSERT(count == free_dims);
#endif
          return true;
        }
        free_dim[dim] = false;
      }
  }
  // At least one dimension is free of constraint.
  return false;
}

bool Parma_Polyhedra_Library::Congruence_System::has_linear_equalities ( ) const

Returns true if and only if *this contains one or more linear equalities.

Definition at line 249 of file Congruence_System.cc.

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

                                                  {
  const Congruence_System& cgs = *this;
  const dimension_type modulus_index = cgs.num_columns() - 1;
  for (dimension_type i = cgs.num_rows(); i-- > 0; )
    if (cgs[i][modulus_index] == 0)
      return true;
  return false;
}

bool Parma_Polyhedra_Library::Congruence_System::increase_space_dimension ( dimension_type new_space_dim )

private

Increase the number of space dimensions to new_space_dim.

new_space_dim must at least equal to the current space dimension.

Definition at line 50 of file Congruence_System.cc.

References PPL_ASSERT.

Referenced by Parma_Polyhedra_Library::Grid::construct(), Parma_Polyhedra_Library::Grid::Grid(), Parma_Polyhedra_Library::Grid::remove_higher_space_dimensions(), and Parma_Polyhedra_Library::Grid::set_empty().

                                                             {
  PPL_ASSERT(space_dimension() <= new_space_dim);

  const dimension_type cols_to_add = new_space_dim - space_dimension();

  if (cols_to_add > 0) {
    if (num_rows() > 0) {
      const dimension_type old_num_columns = num_columns();
      add_zero_columns(cols_to_add);
      // Move the moduli.
      swap_columns(num_columns() - 1, old_num_columns - 1);
    }
    else
      // Empty system.
      add_zero_columns(cols_to_add);
  }

  PPL_ASSERT(OK());
  return true;
}

void Parma_Polyhedra_Library::Congruence_System::initialize ( )

static

Initializes the class.

Definition at line 444 of file Congruence_System.cc.

References PPL_ASSERT, and Parma_Polyhedra_Library::Congruence::zero_dim_false().

                                 {
  PPL_ASSERT(zero_dim_empty_p == 0);
  zero_dim_empty_p
    = new Congruence_System(Congruence::zero_dim_false());
}

void Parma_Polyhedra_Library::Congruence_System::insert ( const Congruence & cg )

inline

Inserts in *this a copy of the congruence cg, increasing the number of space dimensions if needed.

The copy of cg will be strongly normalized after being inserted.

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

References insert_verbatim(), OK(), PPL_ASSERT, and Parma_Polyhedra_Library::Dense_Matrix::rows.

                                              {
  insert_verbatim(cg);
  (*this)[rows.size()-1].strong_normalize();
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Congruence_System::insert ( const Constraint & c )

Inserts in *this a copy of the equality constraint c, seen as a modulo 0 congruence, increasing the number of space dimensions if needed.

The modulo 0 congruence will be strongly normalized after being inserted.

Exceptions:

std::invalid_argument Thrown if c is a relational constraint.

Definition at line 100 of file Congruence_System.cc.

References PPL_ASSERT, and Parma_Polyhedra_Library::Constraint::space_dimension().

                                                {
  const dimension_type cg_size = c.space_dimension() + 2;
  const dimension_type old_num_columns = num_columns();
  if (cg_size < old_num_columns) {
    // Create a congruence of the required size from `c'.
    Congruence cg(c, old_num_columns, row_capacity);
    add_recycled_row(cg);
  }
  else {
    if (cg_size > old_num_columns) {
      // Resize the system, if necessary.
      add_zero_columns(cg_size - old_num_columns);
      if (!has_no_rows())
        // Move the moduli to the last column.
        swap_columns(old_num_columns - 1, cg_size - 1);
    }
    Congruence cg(c, cg_size, row_capacity);
    add_recycled_row(cg);
  }
  (*this)[rows.size()-1].strong_normalize();

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Congruence_System::insert ( const Congruence_System & y )

Inserts in *this a copy of the congruences in y, increasing the number of space dimensions if needed.

The inserted copies will be strongly normalized.

Definition at line 157 of file Congruence_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::num_columns(), 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().

                                                       {
  Congruence_System& x = *this;

  const dimension_type x_num_rows = x.num_rows();
  const dimension_type y_num_rows = y.num_rows();
  const dimension_type old_num_columns = x.num_columns();
  const dimension_type y_num_columns = y.num_columns();
  // Grow to the required size.
  if (old_num_columns >= y_num_columns)
    add_zero_rows(y_num_rows, Dense_Row::Flags());
  else {
    add_zero_rows_and_columns(y_num_rows,
                              y_num_columns - old_num_columns,
                              Dense_Row::Flags());
    // Swap the modulus column into the new last column.
    swap_columns(old_num_columns - 1, num_columns() - 1);
  }

  // Copy the rows of `y', forcing size and capacity.
  const dimension_type x_mod_index = x.num_columns() - 1;
  const dimension_type y_mod_index = y_num_columns - 1;
  for (dimension_type i = y_num_rows; i-- > 0; ) {
    Dense_Row copy(y[i], x.row_size, x.row_capacity);
    // Swap the modulus to the correct column.
    using std::swap;
    swap(copy[x_mod_index], copy[y_mod_index]);
    swap(copy, x[x_num_rows+i]);
  }
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Congruence_System::insert_verbatim ( const Congruence & cg )

private

Inserts in *this an exact copy of the congruence cg, increasing the number of space dimensions if needed.

This method inserts a copy of cg in the given form, instead of first strong normalizing cg as insert would do.

Definition at line 72 of file Congruence_System.cc.

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

Referenced by Parma_Polyhedra_Library::Grid::expand_space_dimension(), and insert().

                                                          {
  const dimension_type old_num_columns = num_columns();
  const dimension_type cg_size = cg.size();

  if (cg_size > old_num_columns) {
    // Resize the system, if necessary.
    add_zero_columns(cg_size - old_num_columns);
    if (!has_no_rows())
      // Move the moduli to the last column.
      swap_columns(old_num_columns - 1, cg_size - 1);
    add_row(cg);
  }
  else if (cg_size < old_num_columns) {
    // Create a resized copy of `cg'.
    Congruence rc(cg, old_num_columns, row_capacity);
    // Move the modulus to its place.
    using std::swap;
    swap(rc[cg_size - 1], rc[old_num_columns - 1]);
    add_recycled_row(rc);
  }
  else
    // Here cg_size == old_num_columns.
    add_row(cg);

  PPL_ASSERT(OK());
}

bool Parma_Polyhedra_Library::Congruence_System::is_equal_to ( const Congruence_System & y ) const

Returns true if and only if *this is exactly equal to y.

Definition at line 231 of file Congruence_System.cc.

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

                                                                  {
  const Congruence_System& x = *this;
  if (x.num_rows() != y.num_rows())
    return false;

  for (dimension_type row = y.num_rows(); row-- > 0; ) {
    const Congruence& x_row = x[row];
    const Congruence& y_row = y[row];
    for (dimension_type col = y.num_columns(); col-- > 0; ) {
      if (x_row[col] == y_row[col])
        continue;
      return false;
    }
  }
  return true;
}

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

inline

Swaps *this with y.

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

Referenced by Parma_Polyhedra_Library::Grid::construct(), and swap().

                                              {
  Dense_Matrix::m_swap(y);
}

dimension_type Parma_Polyhedra_Library::Congruence_System::max_space_dimension ( )

inlinestatic

Returns the maximum space dimension a Congruence_System can handle.

Definition at line 86 of file Congruence_System.inlines.hh.

References Parma_Polyhedra_Library::Dense_Matrix::max_num_columns().

Referenced by Parma_Polyhedra_Library::Grid::max_space_dimension().

                                       {
  return Dense_Matrix::max_num_columns() - 2;
}

void Parma_Polyhedra_Library::Congruence_System::normalize_moduli ( )

private

Adjusts all expressions to have the same moduli.

Definition at line 189 of file Congruence_System.cc.

References Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::lcm_assign(), Parma_Polyhedra_Library::Congruence::modulus(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, and PPL_DIRTY_TEMP_COEFFICIENT.

Referenced by Parma_Polyhedra_Library::Grid::simplify().

                                       {
  Congruence_System& cgs = *this;
  dimension_type row = cgs.num_rows();
  if (row > 0) {
    // Calculate the LCM of all the moduli.
    PPL_DIRTY_TEMP_COEFFICIENT(lcm);
    // Find last proper congruence.
    while (true) {
      --row;
      lcm = cgs[row].modulus();
      if (lcm > 0)
        break;
      if (row == 0)
        // All rows are equalities.
        return;
    }
    while (row > 0) {
      --row;
      const Coefficient& modulus = cgs[row].modulus();
      if (modulus > 0)
        lcm_assign(lcm, lcm, modulus);
    }

    // Represent every row using the LCM as the modulus.
    PPL_DIRTY_TEMP_COEFFICIENT(factor);
    dimension_type row_size = cgs[0].size();
    for (row = cgs.num_rows(); row-- > 0; ) {
      Congruence& cgs_row = cgs[row];
      const Coefficient& modulus = cgs_row.modulus();
      if (modulus <= 0 || modulus == lcm)
        continue;
      exact_div_assign(factor, lcm, modulus);
      for (dimension_type col = row_size; col-- > 0; ) {
        cgs_row[col] *= factor;
      }
      cgs_row[row_size-1] = lcm;
    }
  }
  PPL_ASSERT(OK());
}

PPL::dimension_type Parma_Polyhedra_Library::Congruence_System::num_equalities ( ) const

Returns the number of equalities.

Definition at line 266 of file Congruence_System.cc.

Referenced by Parma_Polyhedra_Library::Grid::congruence_widening_assign(), Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate(), and Parma_Polyhedra_Library::Grid::quick_equivalence_test().

                                           {
  const Congruence_System& cgs = *this;
  dimension_type n = 0;
  for (dimension_type i = num_rows(); i-- > 0 ; )
    if (cgs[i].is_equality())
      ++n;
  return n;
}

PPL::dimension_type Parma_Polyhedra_Library::Congruence_System::num_proper_congruences ( ) const

Returns the number of proper congruences.

Definition at line 276 of file Congruence_System.cc.

References Parma_Polyhedra_Library::Congruence::is_proper_congruence().

Referenced by Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate().

                                                   {
  const Congruence_System& cgs = *this;
  dimension_type n = 0;
  for (dimension_type i = num_rows(); i-- > 0 ; ) {
    const Congruence& cg = cgs[i];
    if (cg.is_proper_congruence())
      ++n;
  }
  return n;
}

bool Parma_Polyhedra_Library::Congruence_System::OK ( ) const

Checks if all the invariants are satisfied.

Returns true if and only if *this is a valid Dense_Matrix, each row in the system is a valid Congruence and the number of columns is consistent with the number of congruences.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 458 of file Congruence_System.cc.

References Parma_Polyhedra_Library::Congruence::OK(), and Parma_Polyhedra_Library::Dense_Matrix::OK().

Referenced by insert(), and Parma_Polyhedra_Library::Grid::simplify().

                               {
  // A Congruence_System must be a valid Dense_Matrix.
  if (!Dense_Matrix::OK())
    return false;

  if (num_rows() > 0) {
    if (num_columns() < 2) {
#ifndef NDEBUG
      std::cerr << "Congruence_System has rows and fewer than two columns."
                << std::endl;
#endif
      return false;
    }
  }

  // Checking each congruence in the system.
  const Congruence_System& x = *this;
  for (dimension_type i = num_rows(); i-- > 0; ) {
    const Congruence& cg = x[i];
    if (!cg.OK())
      return false;
  }

  // All checks passed.
  return true;
}

Congruence_System & Parma_Polyhedra_Library::Congruence_System::operator= ( const Congruence_System & y )

inline

Assignment operator.

Definition at line 80 of file Congruence_System.inlines.hh.

                                                       {
  Dense_Matrix::operator=(y);
  return *this;
}

Congruence & Parma_Polyhedra_Library::Congruence_System::operator[] ( dimension_type k )

inlineprivate

Returns the k- th congruence of the system.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

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

Referenced by operator[]().

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

const Congruence & Parma_Polyhedra_Library::Congruence_System::operator[] ( dimension_type k ) const

inlineprivate

Returns a constant reference to the k- th congruence of the system.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

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

References operator[]().

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

void Parma_Polyhedra_Library::Congruence_System::print ( ) const

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

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

void Parma_Polyhedra_Library::Congruence_System::recycling_insert ( Congruence_System & cgs )

Inserts into *this the congruences in cgs, increasing the number of space dimensions if needed.

Definition at line 125 of file Congruence_System.cc.

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

                                                             {
  const dimension_type old_num_rows = num_rows();
  const dimension_type cgs_num_rows = cgs.num_rows();
  const dimension_type old_num_columns = num_columns();
  dimension_type cgs_num_columns = cgs.num_columns();
  if (old_num_columns >= cgs_num_columns)
    add_zero_rows(cgs_num_rows, Dense_Row::Flags());
  else {
    add_zero_rows_and_columns(cgs_num_rows,
                              cgs_num_columns - old_num_columns,
                              Dense_Row::Flags());
    // Swap the modulus column into the new last column.
    swap_columns(old_num_columns - 1, num_columns() - 1);
  }
  --cgs_num_columns; // Convert to modulus index.
  const dimension_type mod_index = num_columns() - 1;
  for (dimension_type i = cgs_num_rows; i-- > 0; ) {
    // Swap one coefficient at a time into the newly added rows, instead
    // of swapping each entire row.  This ensures that the added rows
    // have the same capacities as the existing rows.
    using std::swap;
    Congruence& new_cg = (*this)[old_num_rows + i];
    Congruence& old_cg = cgs[i];
    for (dimension_type j = cgs_num_columns; j-- > 0; )
      swap(new_cg[j], old_cg[j]);
    swap(new_cg[mod_index], old_cg[cgs_num_columns]); // Modulus.
  }

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Congruence_System::remove_higher_space_dimensions ( dimension_type new_dimension )

private

Removes the higher dimensions of the system so that the resulting system will have dimension new_dimension.

The value of new_dimension must be at most the space dimension of *this.

Definition at line 581 of file Congruence_System.cc.

References PPL_ASSERT.

                                                                   {
  dimension_type space_dim = space_dimension();

  PPL_ASSERT(new_dimension <= space_dim);

  // The removal of no dimensions from any system is a no-op.  Note
  // that this case also captures the only legal removal of dimensions
  // from a system in a 0-dim space.
  if (new_dimension == space_dim)
    return;

  // Swap the modulus column into the column that will become the last
  // column.
  swap_columns(new_dimension + 1, space_dim + 1);

  remove_trailing_columns(space_dim - new_dimension);
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Congruence_System::resize_no_copy	(	dimension_type	new_num_rows,
		dimension_type	new_num_columns
	)

inlineprivate

Resizes the system without worrying about the old contents.

Parameters:

new_num_rows	The number of rows of the resized system;
new_num_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.

Definition at line 102 of file Congruence_System.inlines.hh.

Referenced by Parma_Polyhedra_Library::Grid::conversion().

                                                                        {
  Dense_Matrix::resize_no_copy(new_num_rows, new_num_columns,
                               Dense_Row::Flags());
}

bool Parma_Polyhedra_Library::Congruence_System::satisfies_all_congruences ( const Grid_Generator & g ) const

protected

Returns true if g satisfies all the congruences.

Definition at line 289 of file Congruence_System.cc.

References Parma_Polyhedra_Library::Scalar_Products::assign(), Parma_Polyhedra_Library::Grid_Generator::divisor(), Parma_Polyhedra_Library::Congruence::is_equality(), Parma_Polyhedra_Library::Grid_Generator::is_line(), Parma_Polyhedra_Library::Congruence::modulus(), PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, and Parma_Polyhedra_Library::Grid_Generator::space_dimension().

Referenced by Parma_Polyhedra_Library::Grid::is_included_in().

                                                         {
  PPL_ASSERT(g.space_dimension() <= space_dimension());

  const Congruence_System& cgs = *this;
  PPL_DIRTY_TEMP_COEFFICIENT(sp);
  if (g.is_line())
    for (dimension_type i = cgs.num_rows(); i-- > 0; ) {
      const Congruence& cg = cgs[i];
      Scalar_Products::assign(sp, g, cg);
      if (sp != 0)
        return false;
    }
  else {
    const Coefficient& divisor = g.divisor();
    for (dimension_type i = cgs.num_rows(); i-- > 0; ) {
      const Congruence& cg = cgs[i];
      Scalar_Products::assign(sp, g, cg);
      if (cg.is_equality()) {
        if (sp != 0)
          return false;
      }
      else if (sp % (cg.modulus() * divisor) != 0)
        return false;
    }
  }
  return true;
}

dimension_type Parma_Polyhedra_Library::Congruence_System::space_dimension ( ) const

inline

Returns the dimension of the vector space enclosing *this.

Definition at line 91 of file Congruence_System.inlines.hh.

References Parma_Polyhedra_Library::Dense_Matrix::num_columns().

                                         {
  return Dense_Matrix::num_columns() - 2;
}

memory_size_type Parma_Polyhedra_Library::Congruence_System::total_memory_in_bytes ( ) const

inline

Returns the total size in bytes of the memory occupied by *this.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 205 of file Congruence_System.inlines.hh.

                                               {
  return Dense_Matrix::total_memory_in_bytes();
}

const Congruence_System & Parma_Polyhedra_Library::Congruence_System::zero_dim_empty ( )

inlinestatic

Returns the system containing only Congruence::zero_dim_false().

Definition at line 109 of file Congruence_System.inlines.hh.

References PPL_ASSERT, and zero_dim_empty_p.

Referenced by Parma_Polyhedra_Library::Box< ITV >::congruences(), Parma_Polyhedra_Library::BD_Shape< T >::minimized_congruences(), and Parma_Polyhedra_Library::Octagonal_Shape< T >::minimized_congruences().

                                  {
  PPL_ASSERT(zero_dim_empty_p != 0);
  return *zero_dim_empty_p;
}

Friends And Related Function Documentation

friend class const_iterator

friend

Definition at line 400 of file Congruence_System.defs.hh.

friend class Grid

friend

Definition at line 401 of file Congruence_System.defs.hh.

friend class Grid_Certificate

friend

Definition at line 402 of file Congruence_System.defs.hh.

std::ostream & operator<<	(	std::ostream &	s,
		const Congruence_System &	cgs
	)

Writes true if cgs is empty. Otherwise, writes on s the congruences of cgs, all in one row and separated by ", ".

std::ostream & operator<<	(	std::ostream &	s,
		const Congruence_System &	cgs
	)

std::ostream & operator<<	(	std::ostream &	s,
		const Congruence_System &	cgs
	)

References begin(), end(), and Parma_Polyhedra_Library::Congruence::strong_normalize().

                                                                       {
  Congruence_System::const_iterator i = cgs.begin();
  const Congruence_System::const_iterator cgs_end = cgs.end();
  if (i == cgs_end)
    return s << "true";
  while (true) {
    Congruence cg = *i++;
    cg.strong_normalize();
    s << cg;
    if (i == cgs_end)
      return s;
    s << ", ";
  }
}

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

friend

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

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

                                                                      {
  if (x.num_columns() == y.num_columns()) {
    dimension_type num_rows = x.num_rows();
    if (num_rows == y.num_rows()) {
      while (num_rows-- > 0) {
        if (x[num_rows] != y[num_rows])
          return false;
      }
      return true;
    }
  }
  return false;
}

void swap	(	Congruence_System &	x,
		Congruence_System &	y
	)

void swap	(	Congruence_System &	x,
		Congruence_System &	y
	)

References m_swap().

                                                 {
  x.m_swap(y);
}

Member Data Documentation

const PPL::Congruence_System * Parma_Polyhedra_Library::Congruence_System::zero_dim_empty_p = 0

staticprivate

Holds (between class initialization and finalization) a pointer to the singleton system containing only Congruence::zero_dim_false().

Definition at line 362 of file Congruence_System.defs.hh.

Referenced by zero_dim_empty().

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

Classes

Public Member Functions

Static Public Member Functions

Protected Member Functions

Private Member Functions

Static Private Attributes

Friends

Related Functions

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation