PPL  1.2
Generator_System_defs.hh
Go to the documentation of this file.
1 /* Generator_System class declaration.
2  Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3  Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4 
5 This file is part of the Parma Polyhedra Library (PPL).
6 
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11 
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16 
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20 
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23 
24 #ifndef PPL_Generator_System_defs_hh
25 #define PPL_Generator_System_defs_hh 1
26 
28 
30 #include "Linear_System_defs.hh"
31 #include "Generator_defs.hh"
32 #include "Constraint_types.hh"
34 #include "Polyhedron_types.hh"
35 #include <iosfwd>
36 #include <cstddef>
37 
38 namespace Parma_Polyhedra_Library {
39 
40 namespace IO_Operators {
41 
43 
48 std::ostream& operator<<(std::ostream& s, const Generator_System& gs);
49 
50 } // namespace IO_Operators
51 
52 // TODO: Consider removing this.
53 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
54 
56 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
57 bool operator==(const Generator_System& x, const Generator_System& y);
58 
59 // TODO: Consider removing this.
60 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
61 
63 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
64 bool operator!=(const Generator_System& x, const Generator_System& y);
65 
67 void
68 swap(Generator_System& x, Generator_System& y);
69 
70 } // namespace Parma_Polyhedra_Library
71 
73 
189 public:
191 
193 
195  Generator_System(Representation r = default_representation);
196 
198  explicit Generator_System(const Generator& g,
199  Representation r = default_representation);
200 
204 
207 
210 
213 
216 
219 
222 
225 
227  void set_space_dimension(dimension_type space_dim);
228 
233  void clear();
234 
239  void insert(const Generator& g);
240 
245  void insert(Generator& g, Recycle_Input);
246 
248  static void initialize();
249 
251  static void finalize();
252 
256  static const Generator_System& zero_dim_univ();
257 
259 
261  bool empty() const;
262 
268  const_iterator begin() const;
269 
271  const_iterator end() const;
272 
274  bool OK() const;
275 
277 
287  bool ascii_load(std::istream& s);
288 
291 
294 
296  void m_swap(Generator_System& y);
297 
298 private:
299 
300  bool has_no_rows() const;
301 
303 
308  void remove_space_dimensions(const Variables_Set& vars);
309 
313 
315  /*
316  \param cycle
317  A vector representing a cycle of the permutation according to which the
318  columns must be rearranged.
319 
320  The \p cycle vector represents a cycle of a permutation of space
321  dimensions.
322  For example, the permutation
323  \f$ \{ x_1 \mapsto x_2, x_2 \mapsto x_3, x_3 \mapsto x_1 \}\f$ can be
324  represented by the vector containing \f$ x_1, x_2, x_3 \f$.
325  */
326  void permute_space_dimensions(const std::vector<Variable>& cycle);
327 
330 
331  dimension_type num_rows() const;
332 
334 
347 
348  Topology topology() const;
349 
352 
354  void unset_pending_rows();
355 
357  void set_sorted(bool b);
358 
360  bool is_sorted() const;
361 
364 
369  bool is_necessarily_closed() const;
370 
372  void assign_with_pending(const Generator_System& y);
373 
376 
382 
391 
396  void sort_rows();
397 
402  bool check_sorted() const;
403 
409 
411 
418  void remove_row(dimension_type i, bool keep_sorted = false);
419 
421 
428  void remove_rows(dimension_type first, dimension_type last,
429  bool keep_sorted = false);
430 
433 
437  void remove_rows(const std::vector<dimension_type>& indexes);
438 
441 
443 
454  dimension_type gauss(dimension_type n_lines_or_equalities);
455 
466  void back_substitute(dimension_type n_lines_or_equalities);
467 
469  void strong_normalize();
470 
479  void merge_rows_assign(const Generator_System& y);
480 
482 
485  void insert(const Generator_System& y);
486 
488  void insert_pending(const Generator_System& r);
489 
495 
497 
499  explicit Generator_System(Topology topol,
500  Representation r = default_representation);
501 
507  Generator_System(Topology topol, dimension_type space_dim,
508  Representation r = default_representation);
509 
518  dimension_type new_space_dim);
519 
528 
533  bool has_points() const;
534 
543 
554  bool has_closure_points() const;
555 
559 
561  const Generator& operator[](dimension_type k) const;
562 
568  relation_with(const Constraint& c) const;
569 
571  bool satisfied_by_all_generators(const Constraint& c) const;
572 
574 
577  bool satisfied_by_all_generators_C(const Constraint& c) const;
578 
580 
583  bool satisfied_by_all_generators_NNC(const Constraint& c) const;
584 
586 
612  void affine_image(Variable v,
613  const Linear_Expression& expr,
614  Coefficient_traits::const_reference denominator);
615 
617  dimension_type num_lines() const;
618 
620  dimension_type num_rays() const;
621 
623 
628 
635  void simplify();
636 
642  void insert_pending(const Generator& g);
643 
650 
652 
653  friend bool
654  operator==(const Generator_System& x, const Generator_System& y);
655 
656  friend class Polyhedron;
657 };
658 
660 
681  : public std::iterator<std::forward_iterator_tag,
682  Generator,
683  std::ptrdiff_t,
684  const Generator*,
685  const Generator&> {
686 public:
689 
692 
695 
698 
700  const Generator& operator*() const;
701 
703  const Generator* operator->() const;
704 
707 
710 
715  bool operator==(const Generator_System_const_iterator& y) const;
716 
721  bool operator!=(const Generator_System_const_iterator& y) const;
722 
723 private:
724  friend class Generator_System;
725 
728 
731 
734  const Generator_System& gsys);
735 
740  void skip_forward();
741 };
742 
743 // Generator_System_inlines.hh is not included here on purpose.
744 
745 #endif // !defined(PPL_Generator_System_defs_hh)
void remove_row(dimension_type i, bool keep_sorted=false)
Makes the system shrink by removing its i-th row.
void simplify()
Applies Gaussian elimination and back-substitution so as to provide a partial simplification of the s...
bool operator!=(const Box< ITV > &x, const Box< ITV > &y)
Definition: Box_inlines.hh:264
void merge_rows_assign(const Generator_System &y)
Assigns to *this the result of merging its rows with those of y, obtaining a sorted system...
void sort_and_remove_with_sat(Bit_Matrix &sat)
Sorts the system, removing duplicates, keeping the saturation matrix consistent.
dimension_type first_pending_row() const
Returns the index of the first pending row.
A linear equality or inequality.
void swap(CO_Tree &x, CO_Tree &y)
friend bool operator==(const Generator_System &x, const Generator_System &y)
static const Generator_System & zero_dim_univ()
Returns the singleton system containing only Generator::zero_dim_point().
The base class for systems of constraints and generators.
bool adjust_topology_and_space_dimension(Topology new_topology, dimension_type new_space_dim)
Adjusts *this so that it matches the new_topology and new_space_dim (adding or removing columns if ne...
static const Representation default_representation
size_t dimension_type
An unsigned integral type for representing space dimensions.
bool satisfied_by_all_generators_C(const Constraint &c) const
Returns true if all the generators satisfy c.
An std::set of variables' indexes.
A line, ray, point or closure point.
void add_universe_rows_and_space_dimensions(dimension_type n)
Adds n rows and space dimensions to the system.
void remove_trailing_rows(dimension_type n)
Makes the system shrink by removing its n trailing rows.
void skip_forward()
*this skips to the next generator, skipping those closure points that are immediately followed by a m...
void remove_space_dimensions(const Variables_Set &vars)
Removes all the specified dimensions from the generator system.
void shift_space_dimensions(Variable v, dimension_type n)
std::ostream & operator<<(std::ostream &s, const Ask_Tell< D > &x)
const Generator * operator->() const
Indirect member selector.
const Generator & operator*() const
Dereference operator.
void permute_space_dimensions(const std::vector< Variable > &cycle)
Permutes the space dimensions of the matrix.
bool has_points() const
Returns true if and only if *this contains one or more points.
dimension_type gauss(dimension_type n_lines_or_equalities)
Minimizes the subsystem of equations contained in *this.
void assign_with_pending(const Generator_System &y)
Full assignment operator: pending rows are copied as pending.
memory_size_type external_memory_in_bytes() const
Returns the size in bytes of the memory managed by *this.
const Linear_System< Generator > * gsp
A const pointer to the Linear_System.
bool is_sorted() const
Returns the value of the sortedness flag.
static void initialize()
Initializes the class.
Generator_System_const_iterator & operator=(const Generator_System_const_iterator &y)
Assignment operator.
void set_index_first_pending_row(dimension_type i)
Sets the index of the first pending row to i.
A dimension of the vector space.
void sort_pending_and_remove_duplicates()
Sorts the pending rows and eliminates those that also occur in the non-pending part of the system...
The base class for convex polyhedra.
const Generator & operator[](dimension_type k) const
Returns a constant reference to the k- th generator of the system.
bool is_necessarily_closed() const
Returns true if and only if the system topology is NECESSARILY_CLOSED.
bool satisfied_by_all_generators(const Constraint &c) const
Returns true if all the generators satisfy c.
#define PPL_OUTPUT_DECLARATIONS
void clear()
Removes all the generators from the generator system and sets its space dimension to 0...
void remove_invalid_lines_and_rays()
Removes all the invalid lines and rays.
Representation representation() const
Returns the current representation of *this.
void remove_rows(dimension_type first, dimension_type last, bool keep_sorted=false)
Makes the system shrink by removing the rows in [first,last).
void swap_space_dimensions(Variable v1, Variable v2)
Swaps the coefficients of the variables v1 and v2 .
void insert_pending(const Generator_System &r)
Adds a copy of the rows of `y' to the pending part of `*this'.
Parma_Polyhedra_Library::Poly_Con_Relation relation_with(const Constraint &c) const
Returns the relations holding between the generator system and the constraint c.
Swapping_Vector< Row >::const_iterator const_iterator
Generator_System & operator=(const Generator_System &y)
Assignment operator.
void sort_rows()
Sorts the non-pending rows (in growing order) and eliminates duplicated ones.
dimension_type num_rays() const
Returns the number of rays of the system.
void set_representation(Representation r)
Converts *this to the specified representation.
void m_swap(Generator_System &y)
Swaps *this with y.
void add_corresponding_closure_points()
For each unmatched point in *this, adds the corresponding closure point.
static const Generator_System * zero_dim_univ_p
Holds (between class initialization and finalization) a pointer to the singleton system containing on...
Generator_System_const_iterator const_iterator
The entire library is confined to this namespace.
Definition: version.hh:61
static void finalize()
Finalizes the class.
Generator_System(Representation r=default_representation)
Default constructor: builds an empty system of generators.
void set_sorted(bool b)
Sets the sortedness flag of the system to b.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
const_iterator end() const
Returns the past-the-end const_iterator.
const_iterator begin() const
Returns the const_iterator pointing to the first generator, if *this is not empty; otherwise...
bool check_sorted() const
Returns true if and only if *this is sorted, without checking for duplicates.
Linear_System< Generator >::const_iterator i
The const iterator over the Linear_System.
dimension_type num_lines() const
Returns the number of lines of the system.
void back_substitute(dimension_type n_lines_or_equalities)
Back-substitutes the coefficients to reduce the complexity of the system.
bool operator!=(const Generator_System_const_iterator &y) const
Returns true if and only if *this and y are different.
void set_space_dimension(dimension_type space_dim)
Sets the space dimension of the rows in the system to space_dim .
Sparse representation: only the nonzero coefficient are stored. If there are many nonzero coefficient...
bool operator==(const Box< ITV > &x, const Box< ITV > &y)
memory_size_type total_memory_in_bytes() const
Returns the total size in bytes of the memory occupied by *this.
bool OK() const
Checks if all the invariants are satisfied.
static dimension_type max_space_dimension()
Returns the maximum space dimension a Generator_System can handle.
bool ascii_load(std::istream &s)
Loads from s an ASCII representation (as produced by ascii_dump(std::ostream&) const) and sets *this ...
dimension_type num_pending_rows() const
Returns the number of rows that are in the pending part of the system.
size_t memory_size_type
An unsigned integral type for representing memory size in bytes.
Coefficient c
Definition: PIP_Tree.cc:64
dimension_type num_lines_or_equalities() const
Returns the number of rows in the system that represent either lines or equalities.
void insert(const Generator &g)
Inserts in *this a copy of the generator g, increasing the number of space dimensions if needed...
bool empty() const
Returns true if and only if *this has no generators.
Generator_System_const_iterator & operator++()
Prefix increment operator.
void add_corresponding_points()
For each unmatched closure point in *this, adds the corresponding point.
void strong_normalize()
Strongly normalizes the system.
bool satisfied_by_all_generators_NNC(const Constraint &c) const
Returns true if all the generators satisfy c.
bool has_closure_points() const
Returns true if and only if *this contains one or more closure points.
bool operator==(const Generator_System_const_iterator &y) const
Returns true if and only if *this and y are identical.
void unset_pending_rows()
Sets the index to indicate that the system has no pending rows.
Topology
Kinds of polyhedra domains.
The relation between a polyhedron and a constraint.
void affine_image(Variable v, const Linear_Expression &expr, Coefficient_traits::const_reference denominator)
Assigns to a given variable an affine expression.