#include <Constraint_System.defs.hh>
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_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_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 ![]() 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. | |
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) |
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... |
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.
x
and y
are defined as follows: Variable x(0); Variable y(1);
Constraint_System cs; cs.insert(x >= 0); cs.insert(x <= 3); cs.insert(y >= 0); cs.insert(y <= 3);
cs.insert(x + y > 0); cs.insert(x + y < 6); cs.insert(x - y < 3); cs.insert(y - x < 3);
Constraint_System cs; cs.insert(x >= 0); cs.insert(x - y <= 0); cs.insert(x - y + 1 >= 0);
Definition at line 127 of file Constraint_System.defs.hh.
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] |
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 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 }
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] |
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 89 of file Constraint_System.inlines.hh.
References Parma_Polyhedra_Library::Linear_System::clear().
Referenced by Parma_Polyhedra_Library::Polyhedron::add_space_dimensions_and_embed(), Parma_Polyhedra_Library::Polyhedron::add_space_dimensions_and_project(), Parma_Polyhedra_Library::Polyhedron::BHRZ03_combining_constraints(), Parma_Polyhedra_Library::Polyhedron::map_space_dimensions(), Parma_Polyhedra_Library::Polyhedron::remove_higher_space_dimensions(), Parma_Polyhedra_Library::Polyhedron::remove_space_dimensions(), Parma_Polyhedra_Library::Polyhedron::set_empty(), and Parma_Polyhedra_Library::Polyhedron::set_zero_dim_univ().
00089 { 00090 Linear_System::clear(); 00091 }
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] |
Returns the singleton system containing only Constraint::zero_dim_false().
Definition at line 94 of file Constraint_System.inlines.hh.
References zero_dim_empty_p.
Referenced by Parma_Polyhedra_Library::Polyhedron::constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::constraints(), Parma_Polyhedra_Library::Box< ITV >::constraints(), Parma_Polyhedra_Library::BD_Shape< T >::constraints(), Parma_Polyhedra_Library::Box< ITV >::minimized_constraints(), and Parma_Polyhedra_Library::BD_Shape< T >::minimized_constraints().
00094 { 00095 assert(zero_dim_empty_p != 0); 00096 return *zero_dim_empty_p; 00097 }
bool Parma_Polyhedra_Library::Constraint_System::empty | ( | ) | const [inline] |
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] |
Swaps *this
with y
.
Definition at line 192 of file Constraint_System.inlines.hh.
References Parma_Polyhedra_Library::swap().
Referenced by Parma_Polyhedra_Library::Polyhedron::Polyhedron(), Parma_Polyhedra_Library::Polyhedron::simplify_using_context_assign(), and swap().
00192 { 00193 Linear_System::swap(y); 00194 }
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.
v | Index of the column to which the affine transformation is substituted. | |
expr | The numerator of the affine transformation: ![]() | |
denominator | The denominator of the affine transformation. |
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 are built from the old one
as follows:
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] |
Adds low-level constraints to the constraint system.
Definition at line 180 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().
00180 { 00181 if (is_necessarily_closed()) 00182 // The positivity constraint. 00183 insert(Constraint::zero_dim_positivity()); 00184 else { 00185 // Add the epsilon constraints. 00186 insert(Constraint::epsilon_leq_one()); 00187 insert(Constraint::epsilon_geq_zero()); 00188 } 00189 }
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 }
void swap | ( | Parma_Polyhedra_Library::Constraint_System & | x, | |
Parma_Polyhedra_Library::Constraint_System & | y | |||
) | [related] |
Specializes std::swap
.
Definition at line 218 of file Constraint_System.inlines.hh.
References swap().
00219 { 00220 x.swap(y); 00221 }
const PPL::Constraint_System * Parma_Polyhedra_Library::Constraint_System::zero_dim_empty_p = 0 [static, private] |
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().