24 #ifndef PPL_Constraint_System_inlines_hh
25 #define PPL_Constraint_System_inlines_hh 1
38 : sys(c.topology(), r) {
62 : sys(topol, space_dim, r) {
83 return sys.representation();
88 sys.set_representation(r);
98 return sys.space_dimension();
103 return sys.set_space_dimension(space_dim);
124 : i(y.i), csp(y.csp) {
145 return i.operator->();
176 : i(iter), csp(&cs.sys) {
199 if (
sys.is_necessarily_closed()) {
217 return sys.external_memory_in_bytes();
232 return sys.topology();
237 return sys.num_rows();
242 return sys.is_necessarily_closed();
247 return sys.num_pending_rows();
252 return sys.first_pending_row();
257 return sys.is_sorted();
262 sys.unset_pending_rows();
267 sys.set_index_first_pending_row(i);
277 sys.remove_row(i, keep_sorted);
283 sys.remove_rows(first, last, keep_sorted);
288 sys.remove_rows(indexes);
293 sys.remove_trailing_rows(n);
299 sys.remove_space_dimensions(vars);
305 sys.shift_space_dimensions(v, n);
311 sys.permute_space_dimensions(cycle);
317 sys.swap_space_dimensions(v1, v2);
322 return sys.has_no_rows();
327 sys.strong_normalize();
347 sys.insert_pending(r.
sys);
352 sys.merge_rows_assign(y.
sys);
362 sys.mark_as_necessarily_closed();
367 sys.mark_as_not_necessarily_closed();
372 return sys.gauss(n_lines_or_equalities);
377 sys.back_substitute(n_lines_or_equalities);
382 sys.assign_with_pending(y.
sys);
387 sys.sort_pending_and_remove_duplicates();
392 sys.sort_and_remove_with_sat(sat);
397 return sys.check_sorted();
402 return sys.num_lines_or_equalities();
407 sys.add_universe_rows_and_space_dimensions(n);
426 namespace Implementation {
428 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
430 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
440 #endif // !defined(PPL_Constraint_System_inlines_hh)
void m_swap(Constraint_System &y)
Swaps *this with y.
An iterator over a system of constraints.
bool operator!=(const Box< ITV > &x, const Box< ITV > &y)
void shift_space_dimensions(Variable v, dimension_type n)
A linear equality or inequality.
memory_size_type total_memory_in_bytes() const
Returns the total size in bytes of the memory occupied by *this.
void insert_pending(const Constraint &c)
Inserts in *this a copy of the constraint c, increasing the number of space dimensions if needed...
void set_representation(Representation r)
Converts *this to the specified representation.
bool check_sorted() const
Returns true if and only if *this is sorted, without checking for duplicates.
size_t dimension_type
An unsigned integral type for representing space dimensions.
void set_space_dimension(dimension_type space_dim)
Sets the space dimension of the rows in the system to space_dim .
An std::set of variables' indexes.
bool operator!=(const Constraint_System_const_iterator &y) const
Returns true if and only if *this and y are different.
void simplify()
Applies Gaussian elimination and back-substitution so as to provide a partial simplification of the s...
bool is_necessarily_closed() const
Returns true if and only if the system topology is NECESSARILY_CLOSED.
void merge_rows_assign(const Constraint_System &y)
Assigns to *this the result of merging its rows with those of y, obtaining a sorted system...
void assign_with_pending(const Constraint_System &y)
Full assignment operator: pending rows are copied as pending.
const Constraint * operator->() const
Indirect member selector.
dimension_type first_pending_row() const
Returns the index of the first pending row.
static const Constraint_System & zero_dim_empty()
Returns the singleton system containing only Constraint::zero_dim_false().
void insert(const Constraint &c)
Inserts in *this a copy of the constraint c, increasing the number of space dimensions if needed...
Linear_System< Constraint >::const_iterator i
The const iterator over the matrix of constraints.
void add_universe_rows_and_space_dimensions(dimension_type n)
Adds n rows and space dimensions to the system.
dimension_type num_pending_rows() const
Returns the number of rows that are in the pending part of the system.
bool is_sorted() const
Returns the value of the sortedness flag.
Representation representation() const
Returns the current representation of *this.
Topology topology() const
Returns the system topology.
void clear()
Removes all the constraints from the constraint system and sets its space dimension to 0...
const_iterator begin() const
Returns the const_iterator pointing to the first constraint, if *this is not empty; otherwise...
const Linear_System< Constraint > * csp
A const pointer to the matrix of constraints.
void mark_as_not_necessarily_closed()
Marks the last dimension as the epsilon dimension.
Constraint_System_const_iterator()
Default constructor.
bool operator==(const Constraint_System_const_iterator &y) const
Returns true if and only if *this and y are identical.
A dimension of the vector space.
Constraint_System_const_iterator & operator=(const Constraint_System_const_iterator &y)
Assignment operator.
~Constraint_System_const_iterator()
Destructor.
void remove_row(dimension_type i, bool keep_sorted=false)
Makes the system shrink by removing its i-th row.
void skip_forward()
*this skips to the next non-trivial constraint.
void permute_space_dimensions(const std::vector< Variable > &cycle)
Permutes the space dimensions of the matrix.
static const Constraint & epsilon_geq_zero()
Returns the zero-dimension space constraint .
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
bool empty() const
Returns true if and only if *this has no constraints.
const_iterator end() const
Returns the past-the-end const_iterator.
memory_size_type external_memory_in_bytes() const
Returns the size in bytes of the memory managed by *this.
dimension_type num_lines_or_equalities() const
Returns the number of rows in the system that represent either lines or equalities.
void sort_and_remove_with_sat(Bit_Matrix &sat)
Sorts the system, removing duplicates, keeping the saturation matrix consistent.
static const Constraint_System * zero_dim_empty_p
Holds (between class initialization and finalization) a pointer to the singleton system containing on...
const Constraint & operator[](dimension_type k) const
Returns a constant reference to the k- th constraint of the system.
Swapping_Vector< Row >::const_iterator const_iterator
void sort_rows()
Sorts the non-pending rows (in growing order) and eliminates duplicated ones.
dimension_type num_constraints(const Constraint_System &cs)
Constraint_System_const_iterator & operator++()
Prefix increment operator.
static dimension_type max_space_dimension()
Returns the maximum space dimension a Constraint_System can handle.
void remove_rows(const std::vector< dimension_type > &indexes)
The entire library is confined to this namespace.
Linear_System< Constraint > sys
void remove_trailing_rows(dimension_type n)
Makes the system shrink by removing its n trailing rows.
void remove_space_dimensions(const Variables_Set &vars)
Removes all the specified dimensions from the constraint system.
void strong_normalize()
Strongly normalizes the system.
static const Constraint & epsilon_leq_one()
The zero-dimension space constraint (used to implement NNC polyhedra).
static const Constraint & zero_dim_positivity()
The true (zero-dimension space) constraint , also known as positivity constraint. ...
Constraint_System(Representation r=default_representation)
Default constructor: builds an empty system of constraints.
void unset_pending_rows()
Sets the index to indicate that the system has no pending rows.
void add_low_level_constraints()
Adds low-level constraints to the constraint system.
static dimension_type max_space_dimension()
Returns the maximum space dimension a Linear_System can handle.
bool operator==(const Box< ITV > &x, const Box< ITV > &y)
const Constraint & operator*() const
Dereference operator.
void set_sorted(bool b)
Sets the sortedness flag of the system to b.
size_t memory_size_type
An unsigned integral type for representing memory size in bytes.
Constraint_System & operator=(const Constraint_System &y)
Assignment operator.
void sort_pending_and_remove_duplicates()
Sorts the pending rows and eliminates those that also occur in the non-pending part of the system...
void back_substitute(dimension_type n_lines_or_equalities)
Back-substitutes the coefficients to reduce the complexity of the system.
void set_index_first_pending_row(dimension_type i)
Sets the index of the first pending row to i.
void swap_space_dimensions(Variable v1, Variable v2)
Swaps the coefficients of the variables v1 and v2 .
dimension_type num_rows() const
void mark_as_necessarily_closed()
Marks the epsilon dimension as a standard dimension.
dimension_type gauss(dimension_type n_lines_or_equalities)
Minimizes the subsystem of equations contained in *this.
Topology
Kinds of polyhedra domains.
void swap(Constraint_System &x, Constraint_System &y)
~Constraint_System()
Destructor.