A system of constraints. More...

#include <Constraint_System.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Constraint_System:

Collaboration diagram for Parma_Polyhedra_Library::Constraint_System:

Classes
class	const_iterator
	An iterator over a system of constraints. More...
Public Member Functions
	Constraint_System ()
	Default constructor: builds an empty system of constraints.
	Constraint_System (const Constraint &c)
	Builds the singleton system containing only constraint `c`.
	Constraint_System (const Congruence_System &cgs)
	Builds a system containing copies of any equalities in `cgs`.
	Constraint_System (const Constraint_System &cs)
	Ordinary copy constructor.
	~Constraint_System ()
	Destructor.
Constraint_System &	operator= (const Constraint_System &y)
	Assignment operator.
dimension_type	space_dimension () const
	Returns the dimension of the vector space enclosing `*this`.
bool	has_equalities () const
	Returns `true` if and only if `*this` contains one or more equality constraints.
bool	has_strict_inequalities () const
	Returns `true` if and only if `*this` contains one or more strict inequality constraints.
void	clear ()
	Removes all the constraints from the constraint system and sets its space dimension to 0.
void	insert (const Constraint &c)
	Inserts in `*this` a copy of the constraint `c`, increasing the number of space dimensions if needed.
bool	empty () const
	Returns `true` if and only if `*this` has no constraints.
const_iterator	begin () const
	Returns the const_iterator pointing to the first constraint, 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`.
void	m_swap (Constraint_System &y)
	Swaps `*this` with `y`.
Static Public Member Functions
static dimension_type	max_space_dimension ()
	Returns the maximum space dimension a Constraint_System can handle.
static void	initialize ()
	Initializes the class.
static void	finalize ()
	Finalizes the class.
static const Constraint_System &	zero_dim_empty ()
	Returns the singleton system containing only Constraint::zero_dim_false().
Private Member Functions
	Constraint_System (Topology topol)
	Builds an empty system of constraints having the specified topology.
	Constraint_System (Topology topol, dimension_type n_rows, dimension_type n_columns)
	Builds a system of `n_rows` constraints on a `n_columns` - 1 dimensional space (including the $\epsilon$ dimension, if `topol` is `NOT_NECESSARILY_CLOSED`).
bool	adjust_topology_and_space_dimension (Topology new_topology, dimension_type new_space_dim)
	Adjusts `this` so that it matches `new_topology` and `new_space_dim` (adding or removing columns if needed). Returns `false` if and only if `topol` is equal to `NECESSARILY_CLOSED` and `this` contains strict inequalities.
Constraint &	operator[] (dimension_type k)
	Returns the `k-` th constraint of the system.
const Constraint &	operator[] (dimension_type k) const
	Returns a constant reference to the `k-` th constraint of the system.
bool	satisfies_all_constraints (const Generator &g) const
	Returns `true` if `g` satisfies all the constraints.
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.
dimension_type	num_equalities () const
	Returns the number of equality constraints.
dimension_type	num_inequalities () const
	Returns the number of inequality constraints.
void	simplify ()
	Applies Gaussian elimination and back-substitution so as to provide a partial simplification of the system of constraints.
void	insert_pending (const Constraint &c)
	Inserts in `*this` a copy of the constraint `c`, increasing the number of space dimensions if needed. It is a pending constraint.
void	add_low_level_constraints ()
	Adds low-level constraints to the constraint system.
Static Private Attributes
static const Constraint_System *	zero_dim_empty_p = 0
	Holds (between class initialization and finalization) a pointer to the singleton system containing only Constraint::zero_dim_false().
Friends
class	const_iterator
class	Parma_Polyhedra_Library::Polyhedron
bool	operator== (const Polyhedron &x, const Polyhedron &y)
Related Functions
(Note that these are not member functions.)
std::ostream &	operator<< (std::ostream &s, const Constraint_System &cs)
std::ostream &	operator<< (std::ostream &s, const Constraint_System &cs)
	Output operator.
void	swap (Constraint_System &x, Constraint_System &y)
	Swaps `x` with `y`.
void	swap (Constraint_System &x, Constraint_System &y)
dimension_type	num_constraints (const Constraint_System &cs)

Detailed Description

A system of constraints.

An object of the class Constraint_System is a system of constraints, i.e., a multiset of objects of the class Constraint. When inserting constraints in a system, space dimensions are automatically adjusted so that all the constraints 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 constraints corresponding to a square in $\Rset^2$ :

  Constraint_System cs;
  cs.insert(x >= 0);
  cs.insert(x <= 3);
  cs.insert(y >= 0);
  cs.insert(y <= 3);

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

and

, respectively.

Example 2

By adding four strict inequalities to the constraint system of the previous example, we can remove just the four vertices from the square defined above.

  cs.insert(x + y > 0);
  cs.insert(x + y < 6);
  cs.insert(x - y < 3);
  cs.insert(y - x < 3);

Example 3

The following code builds a system of constraints corresponding to a half-strip in $\Rset^2$ :

  Constraint_System cs;
  cs.insert(x >= 0);
  cs.insert(x - y <= 0);
  cs.insert(x - y + 1 >= 0);

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

Definition at line 122 of file Constraint_System.defs.hh.

Constructor & Destructor Documentation

Parma_Polyhedra_Library::Constraint_System::Constraint_System ( )

inline

Default constructor: builds an empty system of constraints.

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

  : Linear_System(NECESSARILY_CLOSED) {
}

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

inlineexplicit

Builds the singleton system containing only constraint c.

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

References insert().

  : Linear_System(c.topology()) {
  Linear_System::insert(c);
}

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

explicit

Builds a system containing copies of any equalities in cgs.

Definition at line 39 of file Constraint_System.cc.

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

  : Linear_System(NECESSARILY_CLOSED, 0, cgs.space_dimension() + 1) {
  for (Congruence_System::const_iterator i = cgs.begin(),
         cgs_end = cgs.end(); i != cgs_end; ++i)
    if (i->is_equality())
      // TODO: Consider adding a recycling_insert to save the extra copy here.
      insert(Constraint(*i));
}

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

inline

Ordinary copy constructor.

Definition at line 43 of file Constraint_System.inlines.hh.

  : Linear_System(cs) {
}

Parma_Polyhedra_Library::Constraint_System::~Constraint_System ( )

inline

Destructor.

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

{
}

Parma_Polyhedra_Library::Constraint_System::Constraint_System ( Topology topol )

inlineexplicitprivate

Builds an empty system of constraints having the specified topology.

Definition at line 48 of file Constraint_System.inlines.hh.

  : Linear_System(topol) {
}

Parma_Polyhedra_Library::Constraint_System::Constraint_System	(	Topology	topol,
		dimension_type	n_rows,
		dimension_type	n_columns
	)

inlineprivate

Builds a system of n_rows constraints on a n_columns - 1 dimensional space (including the $\epsilon$ dimension, if topol is NOT_NECESSARILY_CLOSED).

Definition at line 53 of file Constraint_System.inlines.hh.

  : Linear_System(topol, n_rows, n_columns) {
}

Member Function Documentation

void Parma_Polyhedra_Library::Constraint_System::add_low_level_constraints ( )

inlineprivate

Adds low-level constraints to the constraint system.

Definition at line 181 of file Constraint_System.inlines.hh.

References Parma_Polyhedra_Library::Constraint::epsilon_geq_zero(), Parma_Polyhedra_Library::Constraint::epsilon_leq_one(), insert(), Parma_Polyhedra_Library::Linear_System::is_necessarily_closed(), and Parma_Polyhedra_Library::Constraint::zero_dim_positivity().

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

                                             {
  if (is_necessarily_closed())
    // The positivity constraint.
    insert(Constraint::zero_dim_positivity());
  else {
    // Add the epsilon constraints.
    insert(Constraint::epsilon_leq_one());
    insert(Constraint::epsilon_geq_zero());
  }
}

bool Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension	(	Topology	new_topology,
		dimension_type	new_space_dim
	)

private

Adjusts *this so that it matches new_topology and new_space_dim (adding or removing columns if needed). Returns false if and only if topol is equal to NECESSARILY_CLOSED and *this contains strict inequalities.

Definition at line 50 of file Constraint_System.cc.

Referenced by Parma_Polyhedra_Library::Polyhedron::add_recycled_constraints(), Parma_Polyhedra_Library::Polyhedron::constraints(), and Parma_Polyhedra_Library::Polyhedron::Polyhedron().

                                                                        {
  PPL_ASSERT(space_dimension() <= new_space_dim);

  const dimension_type old_space_dim = space_dimension();
  const Topology old_topology = topology();
  dimension_type cols_to_be_added = new_space_dim - old_space_dim;

  // Dealing with empty constraint systems first.
  if (num_rows() == 0) {
    if (num_columns() == 0)
      if (new_topology == NECESSARILY_CLOSED) {
        add_zero_columns(++cols_to_be_added);
        set_necessarily_closed();
      }
      else {
        cols_to_be_added += 2;
        add_zero_columns(cols_to_be_added);
        set_not_necessarily_closed();
      }
    else
      // Here `num_columns() > 0'.
      if (old_topology != new_topology)
        if (new_topology == NECESSARILY_CLOSED) {
          switch (cols_to_be_added) {
          case 0:
            remove_trailing_columns(1);
            break;
          case 1:
            // Nothing to do.
            break;
          default:
            add_zero_columns(--cols_to_be_added);
          }
          set_necessarily_closed();
        }
        else {
          // Here old_topology == NECESSARILY_CLOSED
          //  and new_topology == NOT_NECESSARILY_CLOSED.
          add_zero_columns(++cols_to_be_added);
          set_not_necessarily_closed();
        }
      else {
        // Here topologies agree.
        if (cols_to_be_added > 0)
          add_zero_columns(cols_to_be_added);
      }
    PPL_ASSERT(OK());
    return true;
  }

  // Here the constraint system is not empty.
  using std::swap;
  if (cols_to_be_added > 0)
    if (old_topology != new_topology)
      if (new_topology == NECESSARILY_CLOSED) {
        // A NOT_NECESSARILY_CLOSED constraint system
        // can be converted to a NECESSARILY_CLOSED one
        // only if it does not contain strict inequalities.
        if (has_strict_inequalities())
          return false;
        // Since there were no strict inequalities,
        // the only constraints that may have a non-zero epsilon coefficient
        // are the eps-leq-one and the eps-geq-zero constraints.
        // If they are present, we erase these rows, so that the
        // epsilon column will only contain zeroes: as a consequence,
        // we just decrement the number of columns to be added.
        Constraint_System& cs = *this;
        const dimension_type eps_index = old_space_dim + 1;
        const dimension_type old_cs_num_rows = cs.num_rows();
        dimension_type cs_num_rows = old_cs_num_rows;
        bool was_sorted = cs.is_sorted();
        if (was_sorted)
          cs.set_sorted(false);

        // If we have no pending rows, we only check if
        // we must erase some rows.
        if (cs.num_pending_rows() == 0) {
          for (dimension_type i = cs_num_rows; i-- > 0; )
            if (cs[i][eps_index] != 0) {
              --cs_num_rows;
              swap(cs[i], cs[cs_num_rows]);
            }
          cs.remove_trailing_rows(old_cs_num_rows - cs_num_rows);
          cs.unset_pending_rows();
        }
        else {
          // There are pending rows, and we cannot swap them
          // into the non-pending part of the matrix.
          // Thus, we first work on the non-pending part as if it was
          // an independent matrix; then we work on the pending part.
          const dimension_type old_first_pending = cs.first_pending_row();
          dimension_type new_first_pending = old_first_pending;
          for (dimension_type i = new_first_pending; i-- > 0; )
            if (cs[i][eps_index] != 0) {
              --new_first_pending;
              swap(cs[i], cs[new_first_pending]);
            }
          const dimension_type num_swaps
            = old_first_pending - new_first_pending;
          cs.set_index_first_pending_row(new_first_pending);
          // Move the swapped rows to the real end of the matrix.
          for (dimension_type i = num_swaps; i-- > 0; )
            swap(cs[old_first_pending - i], cs[cs_num_rows - i]);
          cs_num_rows -= num_swaps;
          // Now iterate through the pending rows.
          for (dimension_type i = cs_num_rows; i-- > new_first_pending; )
            if (cs[i][eps_index] != 0) {
              --cs_num_rows;
              swap(cs[i], cs[cs_num_rows]);
            }
          cs.remove_trailing_rows(old_cs_num_rows - cs_num_rows);
        }

        // If `cs' was sorted we sort it again.
        if (was_sorted)
          cs.sort_rows();
        if (--cols_to_be_added > 0)
          add_zero_columns(cols_to_be_added);
        set_necessarily_closed();
      }
      else {
        // A NECESSARILY_CLOSED constraint system is converted to
        // a NOT_NECESSARILY_CLOSED one by adding a further column
        // of zeroes for the epsilon coefficients.
        add_zero_columns(++cols_to_be_added);
        set_not_necessarily_closed();
      }
    else {
      // Topologies agree: first add the required zero columns ...
      add_zero_columns(cols_to_be_added);
      // ... and, if needed, move the epsilon coefficients
      // to the new last column.
      if (old_topology == NOT_NECESSARILY_CLOSED)
        swap_columns(old_space_dim + 1, new_space_dim + 1);
    }
  else
    // Here `cols_to_be_added == 0'.
    if (old_topology != new_topology) {
      if (new_topology == NECESSARILY_CLOSED) {
        // A NOT_NECESSARILY_CLOSED constraint system
        // can be converted to a NECESSARILY_CLOSED one
        // only if it does not contain strict inequalities.
        if (has_strict_inequalities())
          return false;
        // We just remove the column of the epsilon coefficients.
        remove_trailing_columns(1);
        set_necessarily_closed();
      }
      else {
        // We just add the column of the epsilon coefficients.
        add_zero_columns(1);
        set_not_necessarily_closed();
      }
    }
  // We successfully adjusted space dimensions and topology.
  PPL_ASSERT(OK());
  return true;
}

void Parma_Polyhedra_Library::Constraint_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 want to allow affine transformations (see Section Images and Preimages of Affine Transfer Relations) having any rational coefficients. Since the coefficients of the constraints are integers we must also provide an integer denominator that will be used as denominator of the affine transformation. The denominator is required to be a positive integer.

The affine transformation substitutes the matrix of constraints 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 425 of file Constraint_System.cc.

References Parma_Polyhedra_Library::add_mul_assign(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, Parma_Polyhedra_Library::Dense_Row::size(), space_dimension(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), and Parma_Polyhedra_Library::Linear_System::strong_normalize().

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

  const dimension_type n_columns = x.num_columns();
  const dimension_type n_rows = x.num_rows();
  const dimension_type expr_size = expr.size();
  const bool not_invertible = (v >= expr_size || expr[v] == 0);

  if (denominator != 1)
    for (dimension_type i = n_rows; i-- > 0; ) {
      Constraint& row = x[i];
      Coefficient& row_v = row[v];
      if (row_v != 0) {
        for (dimension_type j = n_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];
      }
    }
  else
    // Here `denominator' == 1: optimized computation
    // only considering columns having indexes < expr_size.
    for (dimension_type i = n_rows; i-- > 0; ) {
      Constraint& row = x[i];
      Coefficient& row_v = row[v];
      if (row_v != 0) {
        for (dimension_type j = expr_size; j-- > 0; )
          if (j != v)
            add_mul_assign(row[j], row_v, expr[j]);
        if (not_invertible)
          row_v = 0;
        else
          row_v *= expr[v];
      }
    }
  // Strong normalization also resets the sortedness flag.
  x.strong_normalize();
}

void Parma_Polyhedra_Library::Constraint_System::ascii_dump ( ) const

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

Reimplemented from Parma_Polyhedra_Library::Linear_System.

Referenced by Parma_Polyhedra_Library::PIP_Tree_Node::ascii_dump(), and Parma_Polyhedra_Library::Polyhedron::OK().

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

Writes to s an ASCII representation of *this.

Reimplemented from Parma_Polyhedra_Library::Linear_System.

Definition at line 480 of file Constraint_System.cc.

References c, Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::Linear_System::first_pending_row(), Parma_Polyhedra_Library::Linear_System::is_sorted(), Parma_Polyhedra_Library::Constraint::NONSTRICT_INEQUALITY, Parma_Polyhedra_Library::Dense_Matrix::num_columns(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), Parma_Polyhedra_Library::Constraint::STRICT_INEQUALITY, and Parma_Polyhedra_Library::Constraint::type().

                                                    {
  const Constraint_System& x = *this;
  const dimension_type x_num_rows = x.num_rows();
  const 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.is_sorted() ? "(sorted)" : "(not_sorted)")
    << "\n"
    << "index_first_pending " << x.first_pending_row()
    << "\n";
  for (dimension_type i = 0; i < x_num_rows; ++i) {
    const Constraint& c = x[i];
    for (dimension_type j = 0; j < x_num_columns; ++j)
      s << c[j] << ' ';
    switch (c.type()) {
    case Constraint::EQUALITY:
      s << "=";
      break;
    case Constraint::NONSTRICT_INEQUALITY:
      s << ">=";
      break;
    case Constraint::STRICT_INEQUALITY:
      s << ">";
      break;
    }
    s << "\n";
  }
}

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

Definition at line 515 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::Constraint::NONSTRICT_INEQUALITY, Parma_Polyhedra_Library::Dense_Matrix::num_columns(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, and Parma_Polyhedra_Library::Constraint::STRICT_INEQUALITY.

Referenced by Parma_Polyhedra_Library::PIP_Tree_Node::ascii_load().

                                              {
  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);

  Constraint_System& x = *this;
  for (dimension_type i = 0; i < x.num_rows(); ++i) {
    for (dimension_type j = 0; j < x.num_columns(); ++j)
      if (!(s >> x[i][j]))
        return false;

    if (!(s >> str))
      return false;
    if (str == "=")
      x[i].set_is_equality();
    else if (str == ">=" || str == ">")
      x[i].set_is_inequality();
    else
      return false;

    // Checking for equality of actual and declared types.
    switch (x[i].type()) {
    case Constraint::EQUALITY:
      if (str == "=")
        continue;
      break;
    case Constraint::NONSTRICT_INEQUALITY:
      if (str == ">=")
        continue;
      break;
    case Constraint::STRICT_INEQUALITY:
      if (str == ">")
        continue;
      break;
    }
    // Reaching this point means that the input was illegal.
    return false;
  }
  // Check invariants.
  PPL_ASSERT(OK());
  return true;
}

Constraint_System::const_iterator Parma_Polyhedra_Library::Constraint_System::begin ( ) const

inline

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

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 163 of file Constraint_System.inlines.hh.

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

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

void Parma_Polyhedra_Library::Constraint_System::clear ( )

inline

Removes all the constraints from the constraint system and sets its space dimension to 0.

Reimplemented from Parma_Polyhedra_Library::Linear_System.

Definition at line 90 of file Constraint_System.inlines.hh.

Referenced by Parma_Polyhedra_Library::Polyhedron::BHRZ03_combining_constraints(), Parma_Polyhedra_Library::Polyhedron::map_space_dimensions(), and Parma_Polyhedra_Library::Shape_Preserving_Reduction< D1, D2 >::product_reduce().

                         {
  Linear_System::clear();
}

bool Parma_Polyhedra_Library::Constraint_System::empty ( ) const

inline

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

Definition at line 176 of file Constraint_System.inlines.hh.

References begin(), and end().

Referenced by Parma_Polyhedra_Library::BD_Shape< T >::BFT00_upper_bound_assign_if_exact(), Parma_Polyhedra_Library::PIP_Tree_Node::print_tree(), Parma_Polyhedra_Library::PIP_Solution_Node::print_tree(), Parma_Polyhedra_Library::PIP_Solution_Node::solve(), and Parma_Polyhedra_Library::PIP_Decision_Node::solve().

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

Constraint_System::const_iterator Parma_Polyhedra_Library::Constraint_System::end ( ) const

inline

Returns the past-the-end const_iterator.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 170 of file Constraint_System.inlines.hh.

References Parma_Polyhedra_Library::Dense_Matrix::end().

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

memory_size_type Parma_Polyhedra_Library::Constraint_System::external_memory_in_bytes ( ) const

inline

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

Reimplemented from Parma_Polyhedra_Library::Linear_System.

Definition at line 198 of file Constraint_System.inlines.hh.

Referenced by Parma_Polyhedra_Library::PIP_Tree_Node::external_memory_in_bytes().

                                                  {
  return Linear_System::external_memory_in_bytes();
}

void Parma_Polyhedra_Library::Constraint_System::finalize ( )

static

Finalizes the class.

Definition at line 597 of file Constraint_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::Constraint_System::has_equalities ( ) const

Returns true if and only if *this contains one or more equality constraints.

Definition at line 211 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::num_rows().

Referenced by Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation().

                                           {
  const Constraint_System& cs = *this;
  // We verify if the system has equalities also in the pending part.
  for (dimension_type i = cs.num_rows(); i-- > 0; )
    if (cs[i].is_equality())
      return true;
  return false;
}

bool Parma_Polyhedra_Library::Constraint_System::has_strict_inequalities ( ) const

Returns true if and only if *this contains one or more strict inequality constraints.

Definition at line 221 of file Constraint_System.cc.

References c, Parma_Polyhedra_Library::Constraint::is_tautological(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), and Parma_Polyhedra_Library::Dense_Matrix::num_rows().

                                                    {
  if (is_necessarily_closed())
    return false;
  const Constraint_System& cs = *this;
  const dimension_type eps_index = cs.num_columns() - 1;
  // We verify if the system has strict inequalities
  // also in the pending part.
  for (dimension_type i = cs.num_rows(); i-- > 0; ) {
    const Constraint& c = cs[i];
    // Optimized type checking: we already know the topology;
    // also, equalities have the epsilon coefficient equal to zero.
    // NOTE: the constraint eps_leq_one should not be considered
    //       a strict inequality.
    if (c[eps_index] < 0 && !c.is_tautological())
      return true;
  }
  return false;
}

void Parma_Polyhedra_Library::Constraint_System::initialize ( )

static

Initializes the class.

Definition at line 590 of file Constraint_System.cc.

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

                                 {
  PPL_ASSERT(zero_dim_empty_p == 0);
  zero_dim_empty_p
    = new Constraint_System(Constraint::zero_dim_false());
}

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

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

Definition at line 241 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Linear_System::insert(), PPL_ASSERT, Parma_Polyhedra_Library::Constraint::space_dimension(), and Parma_Polyhedra_Library::Linear_Row::topology().

                                                {
  // We are sure that the matrix has no pending rows
  // and that the new row is not a pending constraint.
  PPL_ASSERT(num_pending_rows() == 0);
  if (topology() == c.topology())
    Linear_System::insert(c);
  else
    // `*this' and `c' have different topologies.
    if (is_necessarily_closed()) {
      // Padding the matrix with a columns of zeroes
      // corresponding to the epsilon coefficients.
      add_zero_columns(1);
      set_not_necessarily_closed();
      Linear_System::insert(c);
    }
    else {
      // Here `*this' is NNC and `c' is necessarily closed.
      // Copying the constraint adding the epsilon coefficient
      // and the missing space dimensions, if any.
      // FIXME: provide a resizing copy constructor taking
      // topology and the space dimension.
      const dimension_type new_size = 2 + std::max(c.space_dimension(),
                                                   space_dimension());
      Constraint tmp_c(c, new_size);
      tmp_c.set_not_necessarily_closed();
      Linear_System::insert(tmp_c);
    }
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Constraint_System::insert_pending ( const Constraint & c )

private

Inserts in *this a copy of the constraint c, increasing the number of space dimensions if needed. It is a pending constraint.

Definition at line 272 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Linear_System::insert_pending(), PPL_ASSERT, Parma_Polyhedra_Library::Constraint::space_dimension(), and Parma_Polyhedra_Library::Linear_Row::topology().

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

                                                        {
  if (topology() == c.topology())
    Linear_System::insert_pending(c);
  else
    // `*this' and `c' have different topologies.
    if (is_necessarily_closed()) {
      // Padding the matrix with a columns of zeroes
      // corresponding to the epsilon coefficients.
      add_zero_columns(1);
      set_not_necessarily_closed();
      Linear_System::insert_pending(c);
    }
    else {
      // Here `*this' is NNC and `c' is necessarily closed.
      // Copying the constraint adding the epsilon coefficient
      // and the missing space dimensions, if any.
      const dimension_type new_size = 2 + std::max(c.space_dimension(),
                                                   space_dimension());
      Constraint tmp_c(c, new_size);
      tmp_c.set_not_necessarily_closed();
      Linear_System::insert_pending(tmp_c);
    }
  PPL_ASSERT(OK());
}

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

inline

Swaps *this with y.

Definition at line 193 of file Constraint_System.inlines.hh.

Referenced by Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Implementation::Termination::shift_unprimed_variables(), Parma_Polyhedra_Library::Polyhedron::simplify_using_context_assign(), and swap().

                                              {
  Linear_System::m_swap(y);
}

dimension_type Parma_Polyhedra_Library::Constraint_System::max_space_dimension ( )

inlinestatic

Returns the maximum space dimension a Constraint_System can handle.

Reimplemented from Parma_Polyhedra_Library::Linear_System.

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

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

                                       {
  return Linear_System::max_space_dimension();
}

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

private

Returns the number of equality constraints.

Definition at line 317 of file Constraint_System.cc.

References PPL_ASSERT.

Referenced by Parma_Polyhedra_Library::Polyhedron::H79_widening_assign(), Parma_Polyhedra_Library::Polyhedron::OK(), and Parma_Polyhedra_Library::Polyhedron::quick_equivalence_test().

                                           {
  // We are sure that we call this method only when
  // the matrix has no pending rows.
  PPL_ASSERT(num_pending_rows() == 0);
  return num_rows() - num_inequalities();
}

PPL::dimension_type Parma_Polyhedra_Library::Constraint_System::num_inequalities ( ) const

private

Returns the number of inequality constraints.

Definition at line 298 of file Constraint_System.cc.

References PPL_ASSERT.

                                             {
  // We are sure that we call this method only when
  // the matrix has no pending rows.
  PPL_ASSERT(num_pending_rows() == 0);
  const Constraint_System& cs = *this;
  dimension_type n = 0;
  // If the Linear_System happens to be sorted, take advantage of the fact
  // that inequalities are at the bottom of the system.
  if (is_sorted())
    for (dimension_type i = num_rows(); i > 0 && cs[--i].is_inequality(); )
      ++n;
  else
    for (dimension_type i = num_rows(); i-- > 0 ; )
      if (cs[i].is_inequality())
        ++n;
  return n;
}

bool Parma_Polyhedra_Library::Constraint_System::OK ( ) const

Checks if all the invariants are satisfied.

Returns true if and only if *this is a valid Linear_System and each row in the system is a valid Constraint.

Reimplemented from Parma_Polyhedra_Library::Dense_Matrix.

Definition at line 604 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Dense_Matrix::OK().

                               {
  // A Constraint_System must be a valid Linear_System; do not check for
  // strong normalization, since this will be done when
  // checking each individual constraint.
  if (!Linear_System::OK(false))
    return false;

  // Checking each constraint in the system.
  const Constraint_System& x = *this;
  for (dimension_type i = num_rows(); i-- > 0; )
    if (!x[i].OK())
      return false;

  // All checks passed.
  return true;
}

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

inline

Assignment operator.

Definition at line 64 of file Constraint_System.inlines.hh.

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

Constraint & Parma_Polyhedra_Library::Constraint_System::operator[] ( dimension_type k )

inlineprivate

Returns the k- th constraint of the system.

Reimplemented from Parma_Polyhedra_Library::Linear_System.

Definition at line 70 of file Constraint_System.inlines.hh.

Referenced by operator[]().

                                                    {
  return static_cast<Constraint&>(Linear_System::operator[](k));
}

const Constraint & Parma_Polyhedra_Library::Constraint_System::operator[] ( dimension_type k ) const

inlineprivate

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

Reimplemented from Parma_Polyhedra_Library::Linear_System.

Definition at line 75 of file Constraint_System.inlines.hh.

References operator[]().

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

void Parma_Polyhedra_Library::Constraint_System::print ( ) const

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

Reimplemented from Parma_Polyhedra_Library::Linear_System.

bool Parma_Polyhedra_Library::Constraint_System::satisfies_all_constraints ( const Generator & g ) const

private

Returns true if g satisfies all the constraints.

Definition at line 332 of file Constraint_System.cc.

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

  // Setting `sps' to the appropriate scalar product sign operator.
  // This also avoids problems when having _legal_ topology mismatches
  // (which could also cause a mismatch in the number of columns).
  Topology_Adjusted_Scalar_Product_Sign sps(g);

  const Constraint_System& cs = *this;
  if (cs.is_necessarily_closed()) {
    if (g.is_line()) {
      // Lines must saturate all constraints.
      for (dimension_type i = cs.num_rows(); i-- > 0; )
        if (sps(g, cs[i]) != 0)
          return false;
    }
    else
      // `g' is either a ray, a point or a closure point.
      for (dimension_type i = cs.num_rows(); i-- > 0; ) {
        const Constraint& c = cs[i];
        const int sp_sign = sps(g, c);
        if (c.is_inequality()) {
          // As `cs' is necessarily closed,
          // `c' is a non-strict inequality.
          if (sp_sign < 0)
            return false;
        }
        else
          // `c' is an equality.
          if (sp_sign != 0)
            return false;
      }
  }
  else
    // `cs' is not necessarily closed.
    switch (g.type()) {

    case Generator::LINE:
      // Lines must saturate all constraints.
      for (dimension_type i = cs.num_rows(); i-- > 0; )
        if (sps(g, cs[i]) != 0)
          return false;
      break;

    case Generator::POINT:
      // Have to perform the special test
      // when dealing with a strict inequality.
      for (dimension_type i = cs.num_rows(); i-- > 0; ) {
        const Constraint& c = cs[i];
        const int sp_sign = sps(g, c);
        switch (c.type()) {
        case Constraint::EQUALITY:
          if (sp_sign != 0)
            return false;
          break;
        case Constraint::NONSTRICT_INEQUALITY:
          if (sp_sign < 0)
            return false;
          break;
        case Constraint::STRICT_INEQUALITY:
          if (sp_sign <= 0)
            return false;
          break;
        }
      }
      break;

    case Generator::RAY:
      // Intentionally fall through.
    case Generator::CLOSURE_POINT:
      for (dimension_type i = cs.num_rows(); i-- > 0; ) {
        const Constraint& c = cs[i];
        const int sp_sign = sps(g, c);
        if (c.is_inequality()) {
          // Constraint `c' is either a strict or a non-strict inequality.
          if (sp_sign < 0)
            return false;
        }
        else
          // Constraint `c' is an equality.
          if (sp_sign != 0)
            return false;
      }
      break;
    }

  // If we reach this point, `g' satisfies all constraints.
  return true;
}

void Parma_Polyhedra_Library::Constraint_System::simplify ( )

inlineprivate

Applies Gaussian elimination and back-substitution so as to provide a partial simplification of the system of constraints.

It is assumed that the system has no pending constraints.

Reimplemented from Parma_Polyhedra_Library::Linear_System.

Definition at line 208 of file Constraint_System.inlines.hh.

Referenced by Parma_Polyhedra_Library::Polyhedron::OK(), and Parma_Polyhedra_Library::Polyhedron::simplified_constraints().

                            {
  Linear_System::simplify();
}

dimension_type Parma_Polyhedra_Library::Constraint_System::space_dimension ( ) const

inline

Returns the dimension of the vector space enclosing *this.

Reimplemented from Parma_Polyhedra_Library::Linear_System.

Definition at line 85 of file Constraint_System.inlines.hh.

                                         {
  return Linear_System::space_dimension();
}

memory_size_type Parma_Polyhedra_Library::Constraint_System::total_memory_in_bytes ( ) const

inline

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

Reimplemented from Parma_Polyhedra_Library::Linear_System.

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

                                               {
  return Linear_System::total_memory_in_bytes();
}

const Constraint_System & Parma_Polyhedra_Library::Constraint_System::zero_dim_empty ( )

inlinestatic

Returns the singleton system containing only Constraint::zero_dim_false().

Definition at line 95 of file Constraint_System.inlines.hh.

References PPL_ASSERT, and zero_dim_empty_p.

Referenced by Parma_Polyhedra_Library::Polyhedron::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::constraints(), Parma_Polyhedra_Library::Box< ITV >::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints(), and Parma_Polyhedra_Library::Box< ITV >::minimized_constraints().

                                  {
  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 305 of file Constraint_System.defs.hh.

dimension_type num_constraints ( const Constraint_System & cs )

References begin(), and end().

                                             {
  return static_cast<dimension_type>(std::distance(cs.begin(), cs.end()));
}

std::ostream & operator<<	(	std::ostream &	s,
		const Constraint_System &	cs
	)

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

std::ostream & operator<<	(	std::ostream &	s,
		const Constraint_System &	cs
	)

References begin(), and end().

                                                                      {
  Constraint_System::const_iterator i = cs.begin();
  const Constraint_System::const_iterator cs_end = cs.end();
  if (i == cs_end)
    s << "true";
  else {
    while (i != cs_end) {
      s << *i++;
      if (i != cs_end)
        s << ", ";
    }
  }
  return s;
}

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

friend

friend class Parma_Polyhedra_Library::Polyhedron

friend

Definition at line 306 of file Constraint_System.defs.hh.

void swap	(	Constraint_System &	x,
		Constraint_System &	y
	)

void swap	(	Constraint_System &	x,
		Constraint_System &	y
	)

References m_swap().

                                                 {
  x.m_swap(y);
}

Member Data Documentation

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

staticprivate

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

Definition at line 303 of file Constraint_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

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