1 /* Congruence_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_Congruence_System_defs_hh 25 #define PPL_Congruence_System_defs_hh 1 26 27 #include "Congruence_System_types.hh" 28 #include "Linear_Expression_types.hh" 29 #include "Constraint_types.hh" 30 #include "Congruence_types.hh" 31 #include "Grid_Generator_types.hh" 32 #include "Swapping_Vector_defs.hh" 33 #include "Congruence_defs.hh" 34 #include "Constraint_System_types.hh" 35 #include <iosfwd> 36 #include <cstddef> 37 38 namespace Parma_Polyhedra_Library { 39 40 /*! \relates Congruence_System */ 41 bool 42 operator==(const Congruence_System& x, const Congruence_System& y); 43 44 } 45 46 //! A system of congruences. 47 /*! \ingroup PPL_CXX_interface 48 An object of the class Congruence_System is a system of congruences, 49 i.e., a multiset of objects of the class Congruence. 50 When inserting congruences in a system, space dimensions are 51 automatically adjusted so that all the congruences in the system 52 are defined on the same vector space. 53 54 \par 55 In all the examples it is assumed that variables 56 <CODE>x</CODE> and <CODE>y</CODE> are defined as follows: 57 \code 58 Variable x(0); 59 Variable y(1); 60 \endcode 61 62 \par Example 1 63 The following code builds a system of congruences corresponding to 64 an integer grid in \f$\Rset^2\f$: 65 \code 66 Congruence_System cgs; 67 cgs.insert(x %= 0); 68 cgs.insert(y %= 0); 69 \endcode 70 Note that: 71 the congruence system is created with space dimension zero; 72 the first and second congruence insertions increase the space 73 dimension to \f$1\f$ and \f$2\f$, respectively. 74 75 \par Example 2 76 By adding to the congruence system of the previous example, 77 the congruence \f$x + y = 1 \pmod{2}\f$: 78 \code 79 cgs.insert((x + y %= 1) / 2); 80 \endcode 81 we obtain the grid containing just those integral 82 points where the sum of the \p x and \p y values is odd. 83 84 \par Example 3 85 The following code builds a system of congruences corresponding to 86 the grid in \f$\Zset^2\f$ containing just the integral points on 87 the \p x axis: 88 \code 89 Congruence_System cgs; 90 cgs.insert(x %= 0); 91 cgs.insert((y %= 0) / 0); 92 \endcode 93 94 \note 95 After inserting a multiset of congruences in a congruence system, 96 there are no guarantees that an <EM>exact</EM> copy of them 97 can be retrieved: 98 in general, only an <EM>equivalent</EM> congruence system 99 will be available, where original congruences may have been 100 reordered, removed (if they are trivial, duplicate or 101 implied by other congruences), linearly combined, etc. 102 */ 103 class Parma_Polyhedra_Library::Congruence_System { 104 public: 105 106 typedef Congruence row_type; 107 108 static const Representation default_representation = SPARSE; 109 110 //! Default constructor: builds an empty system of congruences. 111 explicit Congruence_System(Representation r = default_representation); 112 113 //! Builds an empty (i.e. zero rows) system of dimension \p d. 114 explicit Congruence_System(dimension_type d, 115 Representation r = default_representation); 116 117 //! Builds the singleton system containing only congruence \p cg. 118 explicit Congruence_System(const Congruence& cg, 119 Representation r = default_representation); 120 121 /*! \brief 122 If \p c represents the constraint \f$ e_1 = e_2 \f$, builds the 123 singleton system containing only constraint \f$ e_1 = e_2 124 \pmod{0}\f$. 125 126 \exception std::invalid_argument 127 Thrown if \p c is not an equality constraint. 128 */ 129 explicit Congruence_System(const Constraint& c, 130 Representation r = default_representation); 131 132 //! Builds a system containing copies of any equalities in \p cs. 133 explicit Congruence_System(const Constraint_System& cs, 134 Representation r = default_representation); 135 136 //! Ordinary copy constructor. 137 /*! 138 \note 139 The new Congruence_System will have the same Representation as `cgs' 140 so that it's indistinguishable from `cgs'. 141 */ 142 Congruence_System(const Congruence_System& cgs); 143 144 //! Copy constructor with specified representation. 145 Congruence_System(const Congruence_System& cgs, Representation r); 146 147 //! Destructor. 148 ~Congruence_System(); 149 150 //! Assignment operator. 151 Congruence_System& operator=(const Congruence_System& y); 152 153 //! Returns the current representation of *this. 154 Representation representation() const; 155 156 //! Converts *this to the specified representation. 157 void set_representation(Representation r); 158 159 //! Returns the maximum space dimension a Congruence_System can handle. 160 static dimension_type max_space_dimension(); 161 162 //! Returns the dimension of the vector space enclosing \p *this. 163 dimension_type space_dimension() const; 164 165 /*! \brief 166 Returns <CODE>true</CODE> if and only if \p *this is exactly equal 167 to \p y. 168 */ 169 bool is_equal_to(const Congruence_System& y) const; 170 171 /*! \brief 172 Returns <CODE>true</CODE> if and only if \p *this contains one or 173 more linear equalities. 174 */ 175 bool has_linear_equalities() const; 176 177 //! Removes all the congruences and sets the space dimension to 0. 178 void clear(); 179 180 /*! \brief 181 Inserts in \p *this a copy of the congruence \p cg, increasing the 182 number of space dimensions if needed. 183 184 The copy of \p cg will be strongly normalized after being 185 inserted. 186 */ 187 void insert(const Congruence& cg); 188 189 /*! \brief 190 Inserts in \p *this the congruence \p cg, stealing its contents and 191 increasing the number of space dimensions if needed. 192 193 \p cg will be strongly normalized. 194 */ 195 void insert(Congruence& cg, Recycle_Input); 196 197 /*! \brief 198 Inserts in \p *this a copy of the equality constraint \p c, seen 199 as a modulo 0 congruence, increasing the number of space 200 dimensions if needed. 201 202 The modulo 0 congruence will be strongly normalized after being 203 inserted. 204 205 \exception std::invalid_argument 206 Thrown if \p c is a relational constraint. 207 */ 208 void insert(const Constraint& c); 209 210 // TODO: Consider adding a insert(cg, Recycle_Input). 211 212 /*! \brief 213 Inserts in \p *this a copy of the congruences in \p y, 214 increasing the number of space dimensions if needed. 215 216 The inserted copies will be strongly normalized. 217 */ 218 void insert(const Congruence_System& y); 219 220 /*! \brief 221 Inserts into \p *this the congruences in \p cgs, increasing the 222 number of space dimensions if needed. 223 */ 224 void insert(Congruence_System& cgs, Recycle_Input); 225 226 //! Initializes the class. 227 static void initialize(); 228 229 //! Finalizes the class. 230 static void finalize(); 231 232 //! Returns the system containing only Congruence::zero_dim_false(). 233 static const Congruence_System& zero_dim_empty(); 234 235 //! An iterator over a system of congruences. 236 /*! \ingroup PPL_CXX_interface 237 A const_iterator is used to provide read-only access 238 to each congruence contained in an object of Congruence_System. 239 240 \par Example 241 The following code prints the system of congruences 242 defining the grid <CODE>gr</CODE>: 243 \code 244 const Congruence_System& cgs = gr.congruences(); 245 for (Congruence_System::const_iterator i = cgs.begin(), 246 cgs_end = cgs.end(); i != cgs_end; ++i) 247 cout << *i << endl; 248 \endcode 249 */ 250 class const_iterator 251 : public std::iterator<std::forward_iterator_tag, 252 Congruence, 253 std::ptrdiff_t, 254 const Congruence*, 255 const Congruence&> { 256 public: 257 //! Default constructor. 258 const_iterator(); 259 260 //! Ordinary copy constructor. 261 const_iterator(const const_iterator& y); 262 263 //! Destructor. 264 ~const_iterator(); 265 266 //! Assignment operator. 267 const_iterator& operator=(const const_iterator& y); 268 269 //! Dereference operator. 270 const Congruence& operator*() const; 271 272 //! Indirect member selector. 273 const Congruence* operator->() const; 274 275 //! Prefix increment operator. 276 const_iterator& operator++(); 277 278 //! Postfix increment operator. 279 const_iterator operator++(int); 280 281 /*! \brief 282 Returns <CODE>true</CODE> if and only if \p *this and \p y are 283 identical. 284 */ 285 bool operator==(const const_iterator& y) const; 286 287 /*! \brief 288 Returns <CODE>true</CODE> if and only if \p *this and \p y are 289 different. 290 */ 291 bool operator!=(const const_iterator& y) const; 292 293 private: 294 friend class Congruence_System; 295 296 //! The const iterator over the vector of congruences. 297 Swapping_Vector<Congruence>::const_iterator i; 298 299 //! A const pointer to the vector of congruences. 300 const Swapping_Vector<Congruence>* csp; 301 302 //! Constructor. 303 const_iterator(const Swapping_Vector<Congruence>::const_iterator& iter, 304 const Congruence_System& cgs); 305 306 //! \p *this skips to the next non-trivial congruence. 307 void skip_forward(); 308 }; 309 310 //! Returns <CODE>true</CODE> if and only if \p *this has no congruences. 311 bool empty() const; 312 313 /*! \brief 314 Returns the const_iterator pointing to the first congruence, if \p 315 *this is not empty; otherwise, returns the past-the-end 316 const_iterator. 317 */ 318 const_iterator begin() const; 319 320 //! Returns the past-the-end const_iterator. 321 const_iterator end() const; 322 323 //! Checks if all the invariants are satisfied. 324 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 325 /*! 326 Returns <CODE>true</CODE> if and only if all rows have space dimension 327 space_dimension_, each row in the system is a valid Congruence and the 328 space dimension is consistent with the number of congruences. 329 */ 330 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 331 bool OK() const; 332 333 PPL_OUTPUT_DECLARATIONS 334 335 /*! \brief 336 Loads from \p s an ASCII representation (as produced by 337 ascii_dump(std::ostream&) const) and sets \p *this accordingly. 338 Returns <CODE>true</CODE> if successful, <CODE>false</CODE> otherwise. 339 */ 340 bool ascii_load(std::istream& s); 341 342 //! Returns the total size in bytes of the memory occupied by \p *this. 343 memory_size_type total_memory_in_bytes() const; 344 345 //! Returns the size in bytes of the memory managed by \p *this. 346 memory_size_type external_memory_in_bytes() const; 347 348 //! Returns the number of equalities. 349 dimension_type num_equalities() const; 350 351 //! Returns the number of proper congruences. 352 dimension_type num_proper_congruences() const; 353 354 //! Swaps \p *this with \p y. 355 void m_swap(Congruence_System& y); 356 357 /*! \brief 358 Adds \p dims rows and \p dims space dimensions to the matrix, 359 initializing the added rows as in the unit congruence system. 360 361 \param dims 362 The number of rows and space dimensions to be added: must be strictly 363 positive. 364 365 Turns the \f$r \times c\f$ matrix \f$A\f$ into the \f$(r+dims) \times 366 (c+dims)\f$ matrix 367 \f$\bigl(\genfrac{}{}{0pt}{}{0}{A} \genfrac{}{}{0pt}{}{B}{A}\bigr)\f$ 368 where \f$B\f$ is the \f$dims \times dims\f$ unit matrix of the form 369 \f$\bigl(\genfrac{}{}{0pt}{}{0}{1} \genfrac{}{}{0pt}{}{1}{0}\bigr)\f$. 370 The matrix is expanded avoiding reallocation whenever possible. 371 */ 372 void add_unit_rows_and_space_dimensions(dimension_type dims); 373 374 //! Permutes the space dimensions of the system. 375 /*! 376 \param cycle 377 A vector representing a cycle of the permutation according to which the 378 columns must be rearranged. 379 380 The \p cycle vector represents a cycle of a permutation of space 381 dimensions. 382 For example, the permutation 383 \f$ \{ x_1 \mapsto x_2, x_2 \mapsto x_3, x_3 \mapsto x_1 \}\f$ can be 384 represented by the vector containing \f$ x_1, x_2, x_3 \f$. 385 */ 386 void permute_space_dimensions(const std::vector<Variable>& cycle); 387 388 //! Swaps the columns having indexes \p i and \p j. 389 void swap_space_dimensions(Variable v1, Variable v2); 390 391 //! Sets the number of space dimensions to \p new_space_dim. 392 /*! 393 If \p new_space_dim is lower than the current space dimension, the 394 coefficients referring to the removed space dimensions are lost. 395 */ 396 bool set_space_dimension(dimension_type new_space_dim); 397 398 // Note: the following method is protected to allow tests/Grid/congruences2 399 // to call it using a derived class. 400 protected: 401 //! Returns <CODE>true</CODE> if \p g satisfies all the congruences. 402 bool satisfies_all_congruences(const Grid_Generator& g) const; 403 404 private: 405 //! Returns the number of rows in the system. 406 dimension_type num_rows() const; 407 408 //! Returns \c true if num_rows()==0. 409 bool has_no_rows() const; 410 411 //! Returns a constant reference to the \p k- th congruence of the system. 412 const Congruence& operator[](dimension_type k) const; 413 414 //! Adjusts all expressions to have the same moduli. 415 void normalize_moduli(); 416 417 /*! \brief 418 Substitutes a given column of coefficients by a given affine 419 expression. 420 421 \param v 422 Index of the column to which the affine transformation is 423 substituted; 424 425 \param expr 426 The numerator of the affine transformation: 427 \f$\sum_{i = 0}^{n - 1} a_i x_i + b\f$; 428 429 \param denominator 430 The denominator of the affine transformation. 431 432 We allow affine transformations (see the Section \ref 433 rational_grid_operations) to have rational 434 coefficients. Since the coefficients of linear expressions are 435 integers we also provide an integer \p denominator that will 436 be used as denominator of the affine transformation. The 437 denominator is required to be a positive integer and its default value 438 is 1. 439 440 The affine transformation substitutes the matrix of congruences 441 by a new matrix whose elements \f${a'}_{ij}\f$ are built from 442 the old one \f$a_{ij}\f$ as follows: 443 \f[ 444 {a'}_{ij} = 445 \begin{cases} 446 a_{ij} * \mathrm{denominator} + a_{iv} * \mathrm{expr}[j] 447 \quad \text{for } j \neq v; \\ 448 \mathrm{expr}[v] * a_{iv} 449 \quad \text{for } j = v. 450 \end{cases} 451 \f] 452 453 \p expr is a constant parameter and unaltered by this computation. 454 */ 455 void affine_preimage(Variable v, 456 const Linear_Expression& expr, 457 Coefficient_traits::const_reference denominator); 458 459 // TODO: Consider making this private. 460 /*! \brief 461 Concatenates copies of the congruences from \p y onto \p *this. 462 463 \param y 464 The congruence system to append to \p this. The number of rows in 465 \p y must be strictly positive. 466 467 The matrix for the new system of congruences is obtained by 468 leaving the old system in the upper left-hand side and placing the 469 congruences of \p y in the lower right-hand side, and padding 470 with zeroes. 471 */ 472 void concatenate(const Congruence_System& y); 473 474 /*! \brief 475 Inserts in \p *this the congruence \p cg, stealing its contents and 476 increasing the number of space dimensions if needed. 477 478 This method inserts \p cg in the given form, instead of first strong 479 normalizing \p cg as \ref insert would do. 480 */ 481 void insert_verbatim(Congruence& cg, Recycle_Input); 482 483 //! Makes the system shrink by removing the rows in [first,last). 484 /*! 485 If \p keep_sorted is <CODE>true</CODE>, the ordering of the remaining rows 486 will be preserved. 487 */ 488 void remove_rows(dimension_type first, dimension_type last, 489 bool keep_sorted); 490 491 void remove_trailing_rows(dimension_type n); 492 493 /*! \brief 494 Holds (between class initialization and finalization) a pointer to 495 the singleton system containing only Congruence::zero_dim_false(). 496 */ 497 static const Congruence_System* zero_dim_empty_p; 498 499 Swapping_Vector<Congruence> rows; 500 501 dimension_type space_dimension_; 502 503 Representation representation_; 504 505 /*! \brief 506 Returns <CODE>true</CODE> if and only if any of the dimensions in 507 \p *this is free of constraint. 508 509 Any equality or proper congruence affecting a dimension constrains 510 that dimension. 511 512 This method assumes the system is in minimal form. 513 */ 514 bool has_a_free_dimension() const; 515 516 friend class Grid; 517 518 friend bool 519 operator==(const Congruence_System& x, const Congruence_System& y); 520 }; 521 522 namespace Parma_Polyhedra_Library { 523 524 namespace IO_Operators { 525 526 //! Output operator. 527 /*! 528 \relates Parma_Polyhedra_Library::Congruence_System 529 Writes <CODE>true</CODE> if \p cgs is empty. Otherwise, writes on 530 \p s the congruences of \p cgs, all in one row and separated by ", ". 531 */ 532 std::ostream& 533 operator<<(std::ostream& s, const Congruence_System& cgs); 534 535 } // namespace IO_Operators 536 537 /*! \relates Congruence_System */ 538 void 539 swap(Congruence_System& x, Congruence_System& y); 540 541 } // namespace Parma_Polyhedra_Library 542 543 // Congruence_System_inlines.hh is not included here on purpose. 544 545 #endif // !defined(PPL_Congruence_System_defs_hh) 546