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

A system of constraints. More...

#include <Constraint_System.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Constraint_System:

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

Collaboration graph
[legend]

List of all members.

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_Systemoperator= (const Constraint_System &y)
 Assignment operator.
dimension_type space_dimension () const
 Returns the dimension of the vector space enclosing *this.
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 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_Systemzero_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 topol, dimension_type num_dimensions)
 Adjusts *this so that it matches the topology and the number of space dimensions given as parameters (adding or removing columns if needed). Returns false if and only if topol is equal to NECESSARILY_CLOSED and *this contains strict inequalities.
Constraintoperator[] (dimension_type k)
 Returns the k- th constraint of the system.
const Constraintoperator[] (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_Systemzero_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)
 Returns true if and only if x and y are the same polyhedron.

Related Functions

(Note that these are not member functions.)

std::ostream & operator<< (std::ostream &s, const Constraint_System &cs)
 Output operator.
void swap (Parma_Polyhedra_Library::Constraint_System &x, Parma_Polyhedra_Library::Constraint_System &y)
 Specializes std::swap.

Classes

class  const_iterator
 An iterator over a system of constraints. More...


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 $2$, 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 127 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 31 of file Constraint_System.inlines.hh.

Referenced by initialize().

00032   : Linear_System(NECESSARILY_CLOSED) {
00033 }

Parma_Polyhedra_Library::Constraint_System::Constraint_System ( const Constraint c  )  [inline, explicit]

Builds the singleton system containing only constraint c.

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

References Parma_Polyhedra_Library::Linear_System::insert().

00037   : Linear_System(c.topology()) {
00038   Linear_System::insert(c);
00039 }

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

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

Parma_Polyhedra_Library::Constraint_System::Constraint_System ( const Constraint_System cs  )  [inline]

Ordinary copy-constructor.

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

00043   : Linear_System(cs) {
00044 }

Parma_Polyhedra_Library::Constraint_System::~Constraint_System (  )  [inline]

Destructor.

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

00059                                       {
00060 }

Parma_Polyhedra_Library::Constraint_System::Constraint_System ( Topology  topol  )  [inline, explicit, private]

Builds an empty system of constraints having the specified topology.

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

00048   : Linear_System(topol) {
00049 }

Parma_Polyhedra_Library::Constraint_System::Constraint_System ( Topology  topol,
dimension_type  n_rows,
dimension_type  n_columns 
) [inline, private]

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

00055   : Linear_System(topol, n_rows, n_columns) {
00056 }


Member Function Documentation

Constraint_System & Parma_Polyhedra_Library::Constraint_System::operator= ( const Constraint_System y  )  [inline]

Assignment operator.

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

References Parma_Polyhedra_Library::Linear_System::operator=().

00063                                                        {
00064   Linear_System::operator=(y);
00065   return *this;
00066 }

dimension_type Parma_Polyhedra_Library::Constraint_System::max_space_dimension (  )  [inline, static]

Returns the maximum space dimension a Constraint_System can handle.

Reimplemented from Parma_Polyhedra_Library::Linear_System.

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

References Parma_Polyhedra_Library::Linear_System::max_space_dimension().

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

00079                                        {
00080   return Linear_System::max_space_dimension();
00081 }

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 84 of file Constraint_System.inlines.hh.

References Parma_Polyhedra_Library::Linear_System::space_dimension().

Referenced by Parma_Polyhedra_Library::MIP_Problem::add_constraints(), Parma_Polyhedra_Library::Grid::add_constraints(), Parma_Polyhedra_Library::Box< ITV >::add_constraints(), Parma_Polyhedra_Library::Box< ITV >::add_constraints_no_check(), Parma_Polyhedra_Library::Polyhedron::add_recycled_constraints(), adjust_topology_and_space_dimension(), affine_preimage(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::Polyhedron::BHRZ03_combining_constraints(), Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::Polyhedron::constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::get_limiting_octagon(), Parma_Polyhedra_Library::BD_Shape< T >::get_limiting_shape(), Parma_Polyhedra_Library::Grid::Grid(), insert(), insert_pending(), Parma_Polyhedra_Library::Octagonal_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::Polyhedron::limited_BHRZ03_extrapolation_assign(), Parma_Polyhedra_Library::Octagonal_Shape< T >::limited_CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign(), Parma_Polyhedra_Library::Polyhedron::limited_H79_extrapolation_assign(), Parma_Polyhedra_Library::MIP_Problem::MIP_Problem(), Parma_Polyhedra_Library::Octagonal_Shape< T >::Octagonal_Shape(), Parma_Polyhedra_Library::Polyhedron::OK(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints_no_check(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Polyhedron::refine_with_constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::refine_with_constraints(), Parma_Polyhedra_Library::Grid::refine_with_constraints(), Parma_Polyhedra_Library::Box< ITV >::refine_with_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::refine_with_constraints(), satisfies_all_constraints(), Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints(), Parma_Polyhedra_Library::Polyhedron::throw_dimension_incompatible(), Parma_Polyhedra_Library::Grid::throw_dimension_incompatible(), and Parma_Polyhedra_Library::Box< ITV >::throw_dimension_incompatible().

00084                                          {
00085   return Linear_System::space_dimension();
00086 }

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 209 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Linear_System::is_necessarily_closed(), Parma_Polyhedra_Library::Constraint::is_tautological(), Parma_Polyhedra_Library::Matrix::num_columns(), and Parma_Polyhedra_Library::Matrix::num_rows().

Referenced by Parma_Polyhedra_Library::MIP_Problem::add_constraints(), Parma_Polyhedra_Library::Polyhedron::add_recycled_constraints(), adjust_topology_and_space_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::Polyhedron::is_topologically_closed(), Parma_Polyhedra_Library::Octagonal_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_BHMZ05_extrapolation_assign(), Parma_Polyhedra_Library::Polyhedron::limited_BHRZ03_extrapolation_assign(), Parma_Polyhedra_Library::Octagonal_Shape< T >::limited_CC76_extrapolation_assign(), Parma_Polyhedra_Library::BD_Shape< T >::limited_CC76_extrapolation_assign(), Parma_Polyhedra_Library::Polyhedron::limited_H79_extrapolation_assign(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::minimized_constraints(), Parma_Polyhedra_Library::MIP_Problem::MIP_Problem(), and Parma_Polyhedra_Library::Octagonal_Shape< T >::Octagonal_Shape().

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

void Parma_Polyhedra_Library::Constraint_System::clear (  )  [inline]

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 229 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Matrix::add_zero_columns(), Parma_Polyhedra_Library::Linear_System::insert(), Parma_Polyhedra_Library::Linear_System::is_necessarily_closed(), Parma_Polyhedra_Library::Linear_System::num_pending_rows(), OK(), Parma_Polyhedra_Library::Linear_System::set_not_necessarily_closed(), space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), Parma_Polyhedra_Library::Linear_Row::topology(), and Parma_Polyhedra_Library::Linear_System::topology().

Referenced by Parma_Polyhedra_Library::Polyhedron::add_congruences(), add_low_level_constraints(), Parma_Polyhedra_Library::Polyhedron::BHRZ03_combining_constraints(), Constraint_System(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::constraints(), Parma_Polyhedra_Library::Box< ITV >::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::Polyhedron::expand_space_dimension(), Parma_Polyhedra_Library::Polyhedron::limited_BHRZ03_extrapolation_assign(), Parma_Polyhedra_Library::Polyhedron::limited_H79_extrapolation_assign(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::minimized_constraints(), Parma_Polyhedra_Library::Box< ITV >::minimized_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints(), Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Polyhedron::refine_no_check(), Parma_Polyhedra_Library::Polyhedron::refine_with_congruences(), Parma_Polyhedra_Library::Polyhedron::refine_with_constraints(), Parma_Polyhedra_Library::Polyhedron::select_CH78_constraints(), Parma_Polyhedra_Library::Polyhedron::select_H79_constraints(), Parma_Polyhedra_Library::Polyhedron::simplify_using_context_assign(), Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints(), and Parma_Polyhedra_Library::Polyhedron::topological_closure_assign().

00229                                                 {
00230   // We are sure that the matrix has no pending rows
00231   // and that the new row is not a pending constraint.
00232   assert(num_pending_rows() == 0);
00233   if (topology() == c.topology())
00234     Linear_System::insert(c);
00235   else
00236     // `*this' and `c' have different topologies.
00237     if (is_necessarily_closed()) {
00238       // Padding the matrix with a columns of zeroes
00239       // corresponding to the epsilon coefficients.
00240       add_zero_columns(1);
00241       set_not_necessarily_closed();
00242       Linear_System::insert(c);
00243     }
00244     else {
00245       // Here `*this' is NNC and `c' is necessarily closed.
00246       // Copying the constraint adding the epsilon coefficient
00247       // and the missing space dimensions, if any.
00248       // FIXME: provide a resizing copy-constructor taking
00249       // topology and the space dimension.
00250       const dimension_type new_size = 2 + std::max(c.space_dimension(),
00251                                                    space_dimension());
00252       Constraint tmp_c(c, new_size);
00253       tmp_c.set_not_necessarily_closed();
00254       Linear_System::insert(tmp_c);
00255     }
00256   assert(OK());
00257 }

void Parma_Polyhedra_Library::Constraint_System::initialize (  )  [static]

Initializes the class.

Definition at line 576 of file Constraint_System.cc.

References Constraint_System(), zero_dim_empty_p, and Parma_Polyhedra_Library::Constraint::zero_dim_false().

00576                                  {
00577   assert(zero_dim_empty_p == 0);
00578   zero_dim_empty_p
00579     = new Constraint_System(Constraint::zero_dim_false());
00580 }

void Parma_Polyhedra_Library::Constraint_System::finalize (  )  [static]

Finalizes the class.

Definition at line 583 of file Constraint_System.cc.

References zero_dim_empty_p.

00583                                {
00584   assert(zero_dim_empty_p != 0);
00585   delete zero_dim_empty_p;
00586   zero_dim_empty_p = 0;
00587 }

const Constraint_System & Parma_Polyhedra_Library::Constraint_System::zero_dim_empty (  )  [inline, static]

bool Parma_Polyhedra_Library::Constraint_System::empty (  )  const [inline]

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

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

References begin(), and end().

00175                                {
00176   return begin() == end();
00177 }

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

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

References Parma_Polyhedra_Library::Matrix::begin().

Referenced by Parma_Polyhedra_Library::Octagonal_Shape< T >::add_constraints(), Parma_Polyhedra_Library::MIP_Problem::add_constraints(), Parma_Polyhedra_Library::Grid::add_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::add_constraints(), Parma_Polyhedra_Library::Box< ITV >::add_constraints_no_check(), Parma_Polyhedra_Library::Polyhedron::add_recycled_constraints(), Parma_Polyhedra_Library::Polyhedron::affine_dimension(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BHRZ03_Certificate::BHRZ03_Certificate(), Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::C_Polyhedron::C_Polyhedron(), Parma_Polyhedra_Library::H79_Certificate::compare(), Parma_Polyhedra_Library::BHRZ03_Certificate::compare(), Parma_Polyhedra_Library::Congruence_System::Congruence_System(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::constraints(), Parma_Polyhedra_Library::Polyhedron::contains_integer_point(), Parma_Polyhedra_Library::Octagonal_Shape< T >::difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::difference_assign(), empty(), Parma_Polyhedra_Library::Polyhedron::expand_space_dimension(), Parma_Polyhedra_Library::Octagonal_Shape< T >::get_limiting_octagon(), Parma_Polyhedra_Library::BD_Shape< T >::get_limiting_shape(), Parma_Polyhedra_Library::Grid::Grid(), Parma_Polyhedra_Library::H79_Certificate::H79_Certificate(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::linear_partition(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::minimized_constraints(), Parma_Polyhedra_Library::MIP_Problem::MIP_Problem(), Parma_Polyhedra_Library::Octagonal_Shape< T >::Octagonal_Shape(), operator<<(), Parma_Polyhedra_Library::Polyhedron::poly_difference_assign(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints_no_check(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Polyhedron::refine_with_constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::refine_with_constraints(), Parma_Polyhedra_Library::Grid::refine_with_constraints(), and Parma_Polyhedra_Library::BD_Shape< T >::refine_with_constraints().

00162                                {
00163   const_iterator i(Linear_System::begin(), *this);
00164   i.skip_forward();
00165   return i;
00166 }

Constraint_System::const_iterator Parma_Polyhedra_Library::Constraint_System::end (  )  const [inline]

Returns the past-the-end const_iterator.

Reimplemented from Parma_Polyhedra_Library::Matrix.

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

References Parma_Polyhedra_Library::Matrix::end().

Referenced by Parma_Polyhedra_Library::Octagonal_Shape< T >::add_constraints(), Parma_Polyhedra_Library::MIP_Problem::add_constraints(), Parma_Polyhedra_Library::Grid::add_constraints(), Parma_Polyhedra_Library::BD_Shape< T >::add_constraints(), Parma_Polyhedra_Library::Box< ITV >::add_constraints_no_check(), Parma_Polyhedra_Library::Polyhedron::add_recycled_constraints(), Parma_Polyhedra_Library::Polyhedron::affine_dimension(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::affine_dimension(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::BHRZ03_Certificate::BHRZ03_Certificate(), Parma_Polyhedra_Library::Box< ITV >::Box(), Parma_Polyhedra_Library::C_Polyhedron::C_Polyhedron(), Parma_Polyhedra_Library::H79_Certificate::compare(), Parma_Polyhedra_Library::BHRZ03_Certificate::compare(), Parma_Polyhedra_Library::Congruence_System::Congruence_System(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::constraints(), Parma_Polyhedra_Library::Polyhedron::contains_integer_point(), Parma_Polyhedra_Library::Octagonal_Shape< T >::difference_assign(), Parma_Polyhedra_Library::BD_Shape< T >::difference_assign(), empty(), Parma_Polyhedra_Library::Polyhedron::expand_space_dimension(), Parma_Polyhedra_Library::Octagonal_Shape< T >::get_limiting_octagon(), Parma_Polyhedra_Library::BD_Shape< T >::get_limiting_shape(), Parma_Polyhedra_Library::Grid::Grid(), Parma_Polyhedra_Library::H79_Certificate::H79_Certificate(), Parma_Polyhedra_Library::Pointset_Powerset< PS >::linear_partition(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::minimized_constraints(), Parma_Polyhedra_Library::MIP_Problem::MIP_Problem(), Parma_Polyhedra_Library::Octagonal_Shape< T >::Octagonal_Shape(), operator<<(), Parma_Polyhedra_Library::Polyhedron::poly_difference_assign(), Parma_Polyhedra_Library::Box< ITV >::propagate_constraints_no_check(), Parma_Polyhedra_Library::Box< ITV >::refine_no_check(), Parma_Polyhedra_Library::Polyhedron::refine_with_constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::refine_with_constraints(), Parma_Polyhedra_Library::Grid::refine_with_constraints(), and Parma_Polyhedra_Library::BD_Shape< T >::refine_with_constraints().

00169                              {
00170   const const_iterator i(Linear_System::end(), *this);
00171   return i;
00172 }

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

Definition at line 590 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Matrix::num_rows(), and Parma_Polyhedra_Library::Matrix::OK().

Referenced by adjust_topology_and_space_dimension(), ascii_load(), insert(), insert_pending(), and Parma_Polyhedra_Library::Polyhedron::OK().

00590                                {
00591   // A Constraint_System must be a valid Linear_System; do not check for
00592   // strong normalization, since this will be done when
00593   // checking each individual constraint.
00594   if (!Linear_System::OK(false))
00595     return false;
00596 
00597   // Checking each constraint in the system.
00598   const Constraint_System& x = *this;
00599   for (dimension_type i = num_rows(); i-- > 0; )
00600     if (!x[i].OK())
00601       return false;
00602 
00603   // All checks passed.
00604   return true;
00605 }

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::Polyhedron::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 468 of file Constraint_System.cc.

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

00468                                                     {
00469   const Constraint_System& x = *this;
00470   const dimension_type x_num_rows = x.num_rows();
00471   const dimension_type x_num_columns = x.num_columns();
00472   s << "topology " << (is_necessarily_closed()
00473                        ? "NECESSARILY_CLOSED"
00474                        : "NOT_NECESSARILY_CLOSED")
00475     << "\n"
00476     << x_num_rows << " x " << x_num_columns << ' '
00477     << (x.is_sorted() ? "(sorted)" : "(not_sorted)")
00478     << "\n"
00479     << "index_first_pending " << x.first_pending_row()
00480     << "\n";
00481   for (dimension_type i = 0; i < x_num_rows; ++i) {
00482     const Constraint& c = x[i];
00483     for (dimension_type j = 0; j < x_num_columns; ++j)
00484       s << c[j] << ' ';
00485     switch (c.type()) {
00486     case Constraint::EQUALITY:
00487       s << "=";
00488       break;
00489     case Constraint::NONSTRICT_INEQUALITY:
00490       s << ">=";
00491       break;
00492     case Constraint::STRICT_INEQUALITY:
00493       s << ">";
00494       break;
00495     }
00496     s << "\n";
00497   }
00498 }

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::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 503 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::Constraint::NONSTRICT_INEQUALITY, Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), Parma_Polyhedra_Library::Linear_System::resize_no_copy(), Parma_Polyhedra_Library::Linear_System::set_index_first_pending_row(), Parma_Polyhedra_Library::Linear_System::set_necessarily_closed(), Parma_Polyhedra_Library::Linear_System::set_not_necessarily_closed(), Parma_Polyhedra_Library::Linear_System::set_sorted(), and Parma_Polyhedra_Library::Constraint::STRICT_INEQUALITY.

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

00503                                               {
00504   std::string str;
00505   if (!(s >> str) || str != "topology")
00506     return false;
00507   if (!(s >> str))
00508     return false;
00509   if (str == "NECESSARILY_CLOSED")
00510     set_necessarily_closed();
00511   else {
00512     if (str != "NOT_NECESSARILY_CLOSED")
00513       return false;
00514     set_not_necessarily_closed();
00515   }
00516 
00517   dimension_type nrows;
00518   dimension_type ncols;
00519   if (!(s >> nrows))
00520     return false;
00521   if (!(s >> str))
00522     return false;
00523   if (!(s >> ncols))
00524       return false;
00525   resize_no_copy(nrows, ncols);
00526 
00527   if (!(s >> str) || (str != "(sorted)" && str != "(not_sorted)"))
00528     return false;
00529   set_sorted(str == "(sorted)");
00530   dimension_type index;
00531   if (!(s >> str) || str != "index_first_pending")
00532     return false;
00533   if (!(s >> index))
00534     return false;
00535   set_index_first_pending_row(index);
00536 
00537   Constraint_System& x = *this;
00538   for (dimension_type i = 0; i < x.num_rows(); ++i) {
00539     for (dimension_type j = 0; j < x.num_columns(); ++j)
00540       if (!(s >> x[i][j]))
00541         return false;
00542 
00543     if (!(s >> str))
00544       return false;
00545     if (str == "=")
00546       x[i].set_is_equality();
00547     else
00548       x[i].set_is_inequality();
00549 
00550     // Checking for equality of actual and declared types.
00551     switch (x[i].type()) {
00552     case Constraint::EQUALITY:
00553       if (str == "=")
00554         continue;
00555       break;
00556     case Constraint::NONSTRICT_INEQUALITY:
00557       if (str == ">=")
00558         continue;
00559       break;
00560     case Constraint::STRICT_INEQUALITY:
00561       if (str == ">")
00562         continue;
00563       break;
00564     }
00565     // Reaching this point means that the input was illegal.
00566     return false;
00567   }
00568   // Check invariants.
00569   assert(OK());
00570   return true;
00571 }

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 202 of file Constraint_System.inlines.hh.

References Parma_Polyhedra_Library::total_memory_in_bytes().

00202                                                {
00203   return Linear_System::total_memory_in_bytes();
00204 }

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 197 of file Constraint_System.inlines.hh.

References Parma_Polyhedra_Library::external_memory_in_bytes().

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

00197                                                   {
00198   return Linear_System::external_memory_in_bytes();
00199 }

void Parma_Polyhedra_Library::Constraint_System::swap ( Constraint_System y  )  [inline]

bool Parma_Polyhedra_Library::Constraint_System::adjust_topology_and_space_dimension ( Topology  topol,
dimension_type  num_dimensions 
) [private]

Adjusts *this so that it matches the topology and the number of space dimensions given as parameters (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.

References Parma_Polyhedra_Library::Matrix::add_zero_columns(), Parma_Polyhedra_Library::Matrix::erase_to_end(), Parma_Polyhedra_Library::Linear_System::first_pending_row(), has_strict_inequalities(), Parma_Polyhedra_Library::Linear_System::is_sorted(), Parma_Polyhedra_Library::NECESSARILY_CLOSED, Parma_Polyhedra_Library::NOT_NECESSARILY_CLOSED, Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Linear_System::num_pending_rows(), Parma_Polyhedra_Library::Matrix::num_rows(), OK(), Parma_Polyhedra_Library::Linear_System::remove_trailing_columns(), Parma_Polyhedra_Library::Linear_System::set_index_first_pending_row(), Parma_Polyhedra_Library::Linear_System::set_necessarily_closed(), Parma_Polyhedra_Library::Linear_System::set_not_necessarily_closed(), Parma_Polyhedra_Library::Linear_System::set_sorted(), Parma_Polyhedra_Library::Linear_System::sort_rows(), space_dimension(), Parma_Polyhedra_Library::swap(), Parma_Polyhedra_Library::Matrix::swap_columns(), Parma_Polyhedra_Library::Linear_System::topology(), and Parma_Polyhedra_Library::Linear_System::unset_pending_rows().

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

00051                                                                         {
00052   assert(space_dimension() <= new_space_dim);
00053 
00054   const dimension_type old_space_dim = space_dimension();
00055   const Topology old_topology = topology();
00056   dimension_type cols_to_be_added = new_space_dim - old_space_dim;
00057 
00058   // Dealing with empty constraint systems first.
00059   if (num_rows() == 0) {
00060     if (num_columns() == 0)
00061       if (new_topology == NECESSARILY_CLOSED) {
00062         add_zero_columns(++cols_to_be_added);
00063         set_necessarily_closed();
00064       }
00065       else {
00066         cols_to_be_added += 2;
00067         add_zero_columns(cols_to_be_added);
00068         set_not_necessarily_closed();
00069       }
00070     else
00071       // Here `num_columns() > 0'.
00072       if (old_topology != new_topology)
00073         if (new_topology == NECESSARILY_CLOSED) {
00074           switch (cols_to_be_added) {
00075           case 0:
00076             remove_trailing_columns(1);
00077             break;
00078           case 1:
00079             // Nothing to do.
00080             break;
00081           default:
00082             add_zero_columns(--cols_to_be_added);
00083           }
00084           set_necessarily_closed();
00085         }
00086         else {
00087           // Here old_topology == NECESSARILY_CLOSED
00088           //  and new_topology == NOT_NECESSARILY_CLOSED.
00089           add_zero_columns(++cols_to_be_added);
00090           set_not_necessarily_closed();
00091         }
00092       else {
00093         // Here topologies agree.
00094         if (cols_to_be_added > 0)
00095           add_zero_columns(cols_to_be_added);
00096       }
00097     assert(OK());
00098     return true;
00099   }
00100 
00101   // Here the constraint system is not empty.
00102   if (cols_to_be_added > 0)
00103     if (old_topology != new_topology)
00104       if (new_topology == NECESSARILY_CLOSED) {
00105         // A NOT_NECESSARILY_CLOSED constraint system
00106         // can be converted to a NECESSARILY_CLOSED one
00107         // only if it does not contain strict inequalities.
00108         if (has_strict_inequalities())
00109           return false;
00110         // Since there were no strict inequalities,
00111         // the only constraints that may have a non-zero epsilon coefficient
00112         // are the eps-leq-one and the eps-geq-zero constraints.
00113         // If they are present, we erase these rows, so that the
00114         // epsilon column will only contain zeroes: as a consequence,
00115         // we just decrement the number of columns to be added.
00116         Constraint_System& cs = *this;
00117         const dimension_type eps_index = old_space_dim + 1;
00118         dimension_type cs_num_rows = cs.num_rows();
00119         bool was_sorted = cs.is_sorted();
00120         if (was_sorted)
00121           cs.set_sorted(false);
00122 
00123         // If we have no pending rows, we only check if
00124         // we must erase some rows.
00125         if (cs.num_pending_rows() == 0) {
00126           for (dimension_type i = cs_num_rows; i-- > 0; )
00127             if (cs[i][eps_index] != 0) {
00128               --cs_num_rows;
00129               std::swap(cs[i], cs[cs_num_rows]);
00130             }
00131           cs.erase_to_end(cs_num_rows);
00132           cs.unset_pending_rows();
00133         }
00134         else {
00135           // There are pending rows, and we cannot swap them
00136           // into the non-pending part of the matrix.
00137           // Thus, we first work on the non-pending part as if it was
00138           // an independent matrix; then we work on the pending part.
00139           const dimension_type old_first_pending = cs.first_pending_row();
00140           dimension_type new_first_pending = old_first_pending;
00141           for (dimension_type i = new_first_pending; i-- > 0; )
00142             if (cs[i][eps_index] != 0) {
00143               --new_first_pending;
00144               std::swap(cs[i], cs[new_first_pending]);
00145             }
00146           const dimension_type num_swaps
00147             = old_first_pending - new_first_pending;
00148           cs.set_index_first_pending_row(new_first_pending);
00149           // Move the swapped rows to the real end of the matrix.
00150           for (dimension_type i = num_swaps; i-- > 0; )
00151             std::swap(cs[old_first_pending - i], cs[cs_num_rows - i]);
00152           cs_num_rows -= num_swaps;
00153           // Now iterate through the pending rows.
00154           for (dimension_type i = cs_num_rows; i-- > new_first_pending; )
00155             if (cs[i][eps_index] != 0) {
00156               --cs_num_rows;
00157               std::swap(cs[i], cs[cs_num_rows]);
00158             }
00159           cs.erase_to_end(cs_num_rows);
00160         }
00161 
00162         // If `cs' was sorted we sort it again.
00163         if (was_sorted)
00164           cs.sort_rows();
00165         if (--cols_to_be_added > 0)
00166           add_zero_columns(cols_to_be_added);
00167         set_necessarily_closed();
00168       }
00169       else {
00170         // A NECESSARILY_CLOSED constraint system is converted to
00171         // a NOT_NECESSARILY_CLOSED one by adding a further column
00172         // of zeroes for the epsilon coefficients.
00173         add_zero_columns(++cols_to_be_added);
00174         set_not_necessarily_closed();
00175       }
00176     else {
00177       // Topologies agree: first add the required zero columns ...
00178       add_zero_columns(cols_to_be_added);
00179       // ... and, if needed, move the epsilon coefficients
00180       // to the new last column.
00181       if (old_topology == NOT_NECESSARILY_CLOSED)
00182         swap_columns(old_space_dim + 1, new_space_dim + 1);
00183     }
00184   else
00185     // Here `cols_to_be_added == 0'.
00186     if (old_topology != new_topology) {
00187       if (new_topology == NECESSARILY_CLOSED) {
00188         // A NOT_NECESSARILY_CLOSED constraint system
00189         // can be converted to a NECESSARILY_CLOSED one
00190         // only if it does not contain strict inequalities.
00191         if (has_strict_inequalities())
00192           return false;
00193         // We just remove the column of the epsilon coefficients.
00194         remove_trailing_columns(1);
00195         set_necessarily_closed();
00196       }
00197       else {
00198         // We just add the column of the epsilon coefficients.
00199         add_zero_columns(1);
00200         set_not_necessarily_closed();
00201       }
00202     }
00203   // We successfully adjusted space dimensions and topology.
00204   assert(OK());
00205   return true;
00206 }

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

Returns the k- th constraint of the system.

Reimplemented from Parma_Polyhedra_Library::Linear_System.

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

References Parma_Polyhedra_Library::Linear_System::operator[]().

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

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

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

Reimplemented from Parma_Polyhedra_Library::Linear_System.

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

References Parma_Polyhedra_Library::Linear_System::operator[]().

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

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 320 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Generator::CLOSURE_POINT, Parma_Polyhedra_Library::Constraint::EQUALITY, Parma_Polyhedra_Library::Constraint::is_inequality(), Parma_Polyhedra_Library::Generator::is_line(), Parma_Polyhedra_Library::Linear_System::is_necessarily_closed(), Parma_Polyhedra_Library::Generator::LINE, Parma_Polyhedra_Library::Constraint::NONSTRICT_INEQUALITY, Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Generator::POINT, Parma_Polyhedra_Library::Generator::RAY, space_dimension(), Parma_Polyhedra_Library::Generator::space_dimension(), Parma_Polyhedra_Library::Constraint::STRICT_INEQUALITY, Parma_Polyhedra_Library::Constraint::type(), and Parma_Polyhedra_Library::Generator::type().

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

00320                                                                         {
00321   assert(g.space_dimension() <= space_dimension());
00322 
00323   // Setting `sps' to the appropriate scalar product sign operator.
00324   // This also avoids problems when having _legal_ topology mismatches
00325   // (which could also cause a mismatch in the number of columns).
00326   Topology_Adjusted_Scalar_Product_Sign sps(g);
00327 
00328   const Constraint_System& cs = *this;
00329   if (cs.is_necessarily_closed()) {
00330     if (g.is_line()) {
00331       // Lines must saturate all constraints.
00332       for (dimension_type i = cs.num_rows(); i-- > 0; )
00333         if (sps(g, cs[i]) != 0)
00334           return false;
00335     }
00336     else
00337       // `g' is either a ray, a point or a closure point.
00338       for (dimension_type i = cs.num_rows(); i-- > 0; ) {
00339         const Constraint& c = cs[i];
00340         const int sp_sign = sps(g, c);
00341         if (c.is_inequality()) {
00342           // As `cs' is necessarily closed,
00343           // `c' is a non-strict inequality.
00344           if (sp_sign < 0)
00345             return false;
00346         }
00347         else
00348           // `c' is an equality.
00349           if (sp_sign != 0)
00350             return false;
00351       }
00352   }
00353   else
00354     // `cs' is not necessarily closed.
00355     switch (g.type()) {
00356 
00357     case Generator::LINE:
00358       // Lines must saturate all constraints.
00359       for (dimension_type i = cs.num_rows(); i-- > 0; )
00360         if (sps(g, cs[i]) != 0)
00361           return false;
00362       break;
00363 
00364     case Generator::POINT:
00365       // Have to perform the special test
00366       // when dealing with a strict inequality.
00367       for (dimension_type i = cs.num_rows(); i-- > 0; ) {
00368         const Constraint& c = cs[i];
00369         const int sp_sign = sps(g, c);
00370         switch (c.type()) {
00371         case Constraint::EQUALITY:
00372           if (sp_sign != 0)
00373             return false;
00374           break;
00375         case Constraint::NONSTRICT_INEQUALITY:
00376           if (sp_sign < 0)
00377             return false;
00378           break;
00379         case Constraint::STRICT_INEQUALITY:
00380           if (sp_sign <= 0)
00381             return false;
00382           break;
00383         }
00384       }
00385       break;
00386 
00387     case Generator::RAY:
00388       // Intentionally fall through.
00389     case Generator::CLOSURE_POINT:
00390       for (dimension_type i = cs.num_rows(); i-- > 0; ) {
00391         const Constraint& c = cs[i];
00392         const int sp_sign = sps(g, c);
00393         if (c.is_inequality()) {
00394           // Constraint `c' is either a strict or a non-strict inequality.
00395           if (sp_sign < 0)
00396             return false;
00397         }
00398         else
00399           // Constraint `c' is an equality.
00400           if (sp_sign != 0)
00401             return false;
00402       }
00403       break;
00404     }
00405 
00406   // If we reach this point, `g' satisfies all constraints.
00407   return true;
00408 }

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 413 of file Constraint_System.cc.

References Parma_Polyhedra_Library::add_mul_assign(), Parma_Polyhedra_Library::Matrix::num_columns(), Parma_Polyhedra_Library::Matrix::num_rows(), Parma_Polyhedra_Library::Row::size(), Parma_Polyhedra_Library::Linear_Expression::space_dimension(), space_dimension(), and Parma_Polyhedra_Library::Linear_System::strong_normalize().

Referenced by Parma_Polyhedra_Library::Polyhedron::affine_image(), and Parma_Polyhedra_Library::Polyhedron::affine_preimage().

00415                                                                  {
00416   Constraint_System& x = *this;
00417   // `v' is the index of a column corresponding to
00418   // a "user" variable (i.e., it cannot be the inhomogeneous term,
00419   // nor the epsilon dimension of NNC polyhedra).
00420   assert(v > 0 && v <= x.space_dimension());
00421   assert(expr.space_dimension() <= x.space_dimension());
00422   assert(denominator > 0);
00423 
00424   const dimension_type n_columns = x.num_columns();
00425   const dimension_type n_rows = x.num_rows();
00426   const dimension_type expr_size = expr.size();
00427   const bool not_invertible = (v >= expr_size || expr[v] == 0);
00428 
00429   if (denominator != 1)
00430     for (dimension_type i = n_rows; i-- > 0; ) {
00431       Constraint& row = x[i];
00432       Coefficient& row_v = row[v];
00433       if (row_v != 0) {
00434         for (dimension_type j = n_columns; j-- > 0; )
00435           if (j != v) {
00436             Coefficient& row_j = row[j];
00437             row_j *= denominator;
00438             if (j < expr_size)
00439               add_mul_assign(row_j, row_v, expr[j]);
00440           }
00441         if (not_invertible)
00442           row_v = 0;
00443         else
00444           row_v *= expr[v];
00445       }
00446     }
00447   else
00448     // Here `denominator' == 1: optimized computation
00449     // only considering columns having indexes < expr_size.
00450     for (dimension_type i = n_rows; i-- > 0; ) {
00451       Constraint& row = x[i];
00452       Coefficient& row_v = row[v];
00453       if (row_v != 0) {
00454         for (dimension_type j = expr_size; j-- > 0; )
00455           if (j != v)
00456             add_mul_assign(row[j], row_v, expr[j]);
00457         if (not_invertible)
00458           row_v = 0;
00459         else
00460           row_v *= expr[v];
00461       }
00462     }
00463   // Strong normalization also resets the sortedness flag.
00464   x.strong_normalize();
00465 }

PPL::dimension_type Parma_Polyhedra_Library::Constraint_System::num_equalities (  )  const [private]

Returns the number of equality constraints.

Definition at line 305 of file Constraint_System.cc.

References num_inequalities(), Parma_Polyhedra_Library::Linear_System::num_pending_rows(), and Parma_Polyhedra_Library::Matrix::num_rows().

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

00305                                            {
00306   // We are sure that we call this method only when
00307   // the matrix has no pending rows.
00308   assert(num_pending_rows() == 0);
00309   return num_rows() - num_inequalities();
00310 }

PPL::dimension_type Parma_Polyhedra_Library::Constraint_System::num_inequalities (  )  const [private]

Returns the number of inequality constraints.

Definition at line 286 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Linear_System::is_sorted(), Parma_Polyhedra_Library::Linear_System::num_pending_rows(), and Parma_Polyhedra_Library::Matrix::num_rows().

Referenced by num_equalities().

00286                                              {
00287   // We are sure that we call this method only when
00288   // the matrix has no pending rows.
00289   assert(num_pending_rows() == 0);
00290   const Constraint_System& cs = *this;
00291   dimension_type n = 0;
00292   // If the Linear_System happens to be sorted, take advantage of the fact
00293   // that inequalities are at the bottom of the system.
00294   if (is_sorted())
00295     for (dimension_type i = num_rows(); i > 0 && cs[--i].is_inequality(); )
00296       ++n;
00297   else
00298     for (dimension_type i = num_rows(); i-- > 0 ; )
00299       if (cs[i].is_inequality())
00300         ++n;
00301   return n;
00302 }

void Parma_Polyhedra_Library::Constraint_System::simplify (  )  [inline, private]

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 207 of file Constraint_System.inlines.hh.

References Parma_Polyhedra_Library::Linear_System::simplify().

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

00207                             {
00208   Linear_System::simplify();
00209 }

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 260 of file Constraint_System.cc.

References Parma_Polyhedra_Library::Matrix::add_zero_columns(), Parma_Polyhedra_Library::Linear_System::insert_pending(), Parma_Polyhedra_Library::Linear_System::is_necessarily_closed(), OK(), Parma_Polyhedra_Library::Linear_System::set_not_necessarily_closed(), space_dimension(), Parma_Polyhedra_Library::Constraint::space_dimension(), Parma_Polyhedra_Library::Linear_Row::topology(), and Parma_Polyhedra_Library::Linear_System::topology().

Referenced by Parma_Polyhedra_Library::Polyhedron::refine_no_check(), and Parma_Polyhedra_Library::Polyhedron::refine_with_constraints().

00260                                                         {
00261   if (topology() == c.topology())
00262     Linear_System::insert_pending(c);
00263   else
00264     // `*this' and `c' have different topologies.
00265     if (is_necessarily_closed()) {
00266       // Padding the matrix with a columns of zeroes
00267       // corresponding to the epsilon coefficients.
00268       add_zero_columns(1);
00269       set_not_necessarily_closed();
00270       Linear_System::insert_pending(c);
00271     }
00272     else {
00273       // Here `*this' is NNC and `c' is necessarily closed.
00274       // Copying the constraint adding the epsilon coefficient
00275       // and the missing space dimensions, if any.
00276       const dimension_type new_size = 2 + std::max(c.space_dimension(),
00277                                                    space_dimension());
00278       Constraint tmp_c(c, new_size);
00279       tmp_c.set_not_necessarily_closed();
00280       Linear_System::insert_pending(tmp_c);
00281     }
00282   assert(OK());
00283 }

void Parma_Polyhedra_Library::Constraint_System::add_low_level_constraints (  )  [inline, private]


Friends And Related Function Documentation

friend class const_iterator [friend]

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

friend class Parma_Polyhedra_Library::Polyhedron [friend]

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

bool operator== ( const Polyhedron x,
const Polyhedron y 
) [friend]

Returns true if and only if x and y are the same polyhedron.

Note that x and y may be topology- and/or dimension-incompatible polyhedra: in those cases, the value false is returned.

Definition at line 3754 of file Polyhedron_public.cc.

03754                                                         {
03755   // If the two polyhedra are topology-incompatible or dimension-incompatible,
03756   // then they cannot be the same polyhedron.
03757   if (x.topology() != y.topology() || x.space_dim != y.space_dim)
03758     return false;
03759 
03760   if (x.marked_empty())
03761     return y.is_empty();
03762   else if (y.marked_empty())
03763     return x.is_empty();
03764   else if (x.space_dim == 0)
03765     return true;
03766 
03767   switch (x.quick_equivalence_test(y)) {
03768   case Polyhedron::TVB_TRUE:
03769     return true;
03770 
03771   case Polyhedron::TVB_FALSE:
03772     return false;
03773 
03774   default:
03775     if (x.is_included_in(y))
03776       if (x.marked_empty())
03777         return y.is_empty();
03778       else
03779         return y.is_included_in(x);
03780     else
03781       return false;
03782   }
03783 }

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

Output operator.

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

Definition at line 609 of file Constraint_System.cc.

References begin(), and end().

00609                                                                       {
00610   Constraint_System::const_iterator i = cs.begin();
00611   const Constraint_System::const_iterator cs_end = cs.end();
00612   if (i == cs_end)
00613     s << "true";
00614   else {
00615     while (i != cs_end) {
00616       s << *i++;
00617       if (i != cs_end)
00618         s << ", ";
00619     }
00620   }
00621   return s;
00622 }

Specializes std::swap.

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

References swap().

00219                                                   {
00220   x.swap(y);
00221 }


Member Data Documentation

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

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

Referenced by finalize(), initialize(), and zero_dim_empty().


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

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