1 /* Constraint_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_Constraint_System_defs_hh 25 #define PPL_Constraint_System_defs_hh 1 26 27 #include "Constraint_System_types.hh" 28 29 #include "Linear_System_defs.hh" 30 #include "Constraint_defs.hh" 31 32 #include "Linear_Expression_types.hh" 33 #include "Generator_types.hh" 34 #include "Constraint_types.hh" 35 #include "Congruence_System_types.hh" 36 #include "Polyhedron_types.hh" 37 #include "termination_types.hh" 38 #include <iterator> 39 #include <iosfwd> 40 #include <cstddef> 41 42 namespace Parma_Polyhedra_Library { 43 44 namespace IO_Operators { 45 46 //! Output operator. 47 /*! 48 \relates Parma_Polyhedra_Library::Constraint_System 49 Writes <CODE>true</CODE> if \p cs is empty. Otherwise, writes on 50 \p s the constraints of \p cs, all in one row and separated by ", ". 51 */ 52 std::ostream& operator<<(std::ostream& s, const Constraint_System& cs); 53 54 } // namespace IO_Operators 55 56 // TODO: Consider removing this. 57 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 58 //! Returns <CODE>true</CODE> if and only if \p x and \p y are identical. 59 /*! \relates Constraint_System */ 60 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 61 bool operator==(const Constraint_System& x, const Constraint_System& y); 62 63 // TODO: Consider removing this. 64 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 65 //! Returns <CODE>true</CODE> if and only if \p x and \p y are different. 66 /*! \relates Constraint_System */ 67 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 68 bool operator!=(const Constraint_System& x, const Constraint_System& y); 69 70 /*! \relates Constraint_System */ 71 void 72 swap(Constraint_System& x, Constraint_System& y); 73 74 } // namespace Parma_Polyhedra_Library 75 76 //! A system of constraints. 77 /*! \ingroup PPL_CXX_interface 78 An object of the class Constraint_System is a system of constraints, 79 i.e., a multiset of objects of the class Constraint. 80 When inserting constraints in a system, space dimensions are 81 automatically adjusted so that all the constraints in the system 82 are defined on the same vector space. 83 84 \par 85 In all the examples it is assumed that variables 86 <CODE>x</CODE> and <CODE>y</CODE> are defined as follows: 87 \code 88 Variable x(0); 89 Variable y(1); 90 \endcode 91 92 \par Example 1 93 The following code builds a system of constraints corresponding to 94 a square in \f$\Rset^2\f$: 95 \code 96 Constraint_System cs; 97 cs.insert(x >= 0); 98 cs.insert(x <= 3); 99 cs.insert(y >= 0); 100 cs.insert(y <= 3); 101 \endcode 102 Note that: 103 the constraint system is created with space dimension zero; 104 the first and third constraint insertions increase the space 105 dimension to \f$1\f$ and \f$2\f$, respectively. 106 107 \par Example 2 108 By adding four strict inequalities to the constraint system 109 of the previous example, we can remove just the four 110 vertices from the square defined above. 111 \code 112 cs.insert(x + y > 0); 113 cs.insert(x + y < 6); 114 cs.insert(x - y < 3); 115 cs.insert(y - x < 3); 116 \endcode 117 118 \par Example 3 119 The following code builds a system of constraints corresponding to 120 a half-strip in \f$\Rset^2\f$: 121 \code 122 Constraint_System cs; 123 cs.insert(x >= 0); 124 cs.insert(x - y <= 0); 125 cs.insert(x - y + 1 >= 0); 126 \endcode 127 128 \note 129 After inserting a multiset of constraints in a constraint system, 130 there are no guarantees that an <EM>exact</EM> copy of them 131 can be retrieved: 132 in general, only an <EM>equivalent</EM> constraint system 133 will be available, where original constraints may have been 134 reordered, removed (if they are trivial, duplicate or 135 implied by other constraints), linearly combined, etc. 136 */ 137 class Parma_Polyhedra_Library::Constraint_System { 138 public: 139 typedef Constraint row_type; 140 141 static const Representation default_representation = SPARSE; 142 143 //! Default constructor: builds an empty system of constraints. 144 explicit Constraint_System(Representation r = default_representation); 145 146 //! Builds the singleton system containing only constraint \p c. 147 explicit Constraint_System(const Constraint& c, 148 Representation r = default_representation); 149 150 //! Builds a system containing copies of any equalities in \p cgs. 151 explicit Constraint_System(const Congruence_System& cgs, 152 Representation r = default_representation); 153 154 //! Ordinary copy constructor. 155 /*! 156 \note The copy will have the same representation as `cs', to make it 157 indistinguishable from `cs'. 158 */ 159 Constraint_System(const Constraint_System& cs); 160 161 //! Copy constructor with specified representation. 162 Constraint_System(const Constraint_System& cs, Representation r); 163 164 //! Destructor. 165 ~Constraint_System(); 166 167 //! Assignment operator. 168 Constraint_System& operator=(const Constraint_System& y); 169 170 //! Returns the current representation of *this. 171 Representation representation() const; 172 173 //! Converts *this to the specified representation. 174 void set_representation(Representation r); 175 176 //! Returns the maximum space dimension a Constraint_System can handle. 177 static dimension_type max_space_dimension(); 178 179 //! Returns the dimension of the vector space enclosing \p *this. 180 dimension_type space_dimension() const; 181 182 //! Sets the space dimension of the rows in the system to \p space_dim . 183 void set_space_dimension(dimension_type space_dim); 184 185 /*! \brief 186 Returns <CODE>true</CODE> if and only if \p *this 187 contains one or more equality constraints. 188 */ 189 bool has_equalities() const; 190 191 /*! \brief 192 Returns <CODE>true</CODE> if and only if \p *this 193 contains one or more strict inequality constraints. 194 */ 195 bool has_strict_inequalities() const; 196 197 /*! \brief 198 Inserts in \p *this a copy of the constraint \p c, 199 increasing the number of space dimensions if needed. 200 */ 201 void insert(const Constraint& c); 202 203 //! Initializes the class. 204 static void initialize(); 205 206 //! Finalizes the class. 207 static void finalize(); 208 209 /*! \brief 210 Returns the singleton system containing only Constraint::zero_dim_false(). 211 */ 212 static const Constraint_System& zero_dim_empty(); 213 214 typedef Constraint_System_const_iterator const_iterator; 215 216 //! Returns <CODE>true</CODE> if and only if \p *this has no constraints. 217 bool empty() const; 218 219 /*! \brief 220 Removes all the constraints from the constraint system 221 and sets its space dimension to 0. 222 */ 223 void clear(); 224 225 /*! \brief 226 Returns the const_iterator pointing to the first constraint, 227 if \p *this is not empty; 228 otherwise, returns the past-the-end const_iterator. 229 */ 230 const_iterator begin() const; 231 232 //! Returns the past-the-end const_iterator. 233 const_iterator end() const; 234 235 //! Checks if all the invariants are satisfied. 236 bool OK() const; 237 238 PPL_OUTPUT_DECLARATIONS 239 240 /*! \brief 241 Loads from \p s an ASCII representation (as produced by 242 ascii_dump(std::ostream&) const) and sets \p *this accordingly. 243 Returns <CODE>true</CODE> if successful, <CODE>false</CODE> otherwise. 244 */ 245 bool ascii_load(std::istream& s); 246 247 //! Returns the total size in bytes of the memory occupied by \p *this. 248 memory_size_type total_memory_in_bytes() const; 249 250 //! Returns the size in bytes of the memory managed by \p *this. 251 memory_size_type external_memory_in_bytes() const; 252 253 //! Swaps \p *this with \p y. 254 void m_swap(Constraint_System& y); 255 256 private: 257 Linear_System<Constraint> sys; 258 259 /*! \brief 260 Holds (between class initialization and finalization) a pointer to 261 the singleton system containing only Constraint::zero_dim_false(). 262 */ 263 static const Constraint_System* zero_dim_empty_p; 264 265 friend class Constraint_System_const_iterator; 266 267 friend bool operator==(const Constraint_System& x, 268 const Constraint_System& y); 269 270 //! Builds an empty system of constraints having the specified topology. 271 explicit Constraint_System(Topology topol, 272 Representation r = default_representation); 273 274 /*! \brief 275 Builds a system of constraints on a \p space_dim dimensional space. If 276 \p topol is <CODE>NOT_NECESSARILY_CLOSED</CODE> the \f$\epsilon\f$ 277 dimension is added. 278 */ 279 Constraint_System(Topology topol, dimension_type space_dim, 280 Representation r = default_representation); 281 282 //! Returns the number of equality constraints. 283 dimension_type num_equalities() const; 284 285 //! Returns the number of inequality constraints. 286 dimension_type num_inequalities() const; 287 288 /*! \brief 289 Applies Gaussian elimination and back-substitution so as 290 to provide a partial simplification of the system of constraints. 291 292 It is assumed that the system has no pending constraints. 293 */ 294 void simplify(); 295 296 /*! \brief 297 Adjusts \p *this so that it matches \p new_topology and 298 \p new_space_dim (adding or removing columns if needed). 299 Returns <CODE>false</CODE> if and only if \p topol is 300 equal to <CODE>NECESSARILY_CLOSED</CODE> and \p *this 301 contains strict inequalities. 302 */ 303 bool adjust_topology_and_space_dimension(Topology new_topology, 304 dimension_type new_space_dim); 305 306 //! Returns a constant reference to the \p k- th constraint of the system. 307 const Constraint& operator[](dimension_type k) const; 308 309 //! Returns <CODE>true</CODE> if \p g satisfies all the constraints. 310 bool satisfies_all_constraints(const Generator& g) const; 311 312 //! Substitutes a given column of coefficients by a given affine expression. 313 /*! 314 \param v 315 The variable to which the affine transformation is substituted. 316 317 \param expr 318 The numerator of the affine transformation: 319 \f$\sum_{i = 0}^{n - 1} a_i x_i + b\f$; 320 321 \param denominator 322 The denominator of the affine transformation. 323 324 We want to allow affine transformations 325 (see Section \ref Images_and_Preimages_of_Affine_Transfer_Relations) 326 having any rational coefficients. Since the coefficients of the 327 constraints are integers we must also provide an integer \p 328 denominator that will be used as denominator of the affine 329 transformation. 330 The denominator is required to be a positive integer. 331 332 The affine transformation substitutes the matrix of constraints 333 by a new matrix whose elements \f${a'}_{ij}\f$ are built from 334 the old one \f$a_{ij}\f$ as follows: 335 \f[ 336 {a'}_{ij} = 337 \begin{cases} 338 a_{ij} * \mathrm{denominator} + a_{iv} * \mathrm{expr}[j] 339 \quad \text{for } j \neq v; \\ 340 \mathrm{expr}[v] * a_{iv} 341 \quad \text{for } j = v. 342 \end{cases} 343 \f] 344 345 \p expr is a constant parameter and unaltered by this computation. 346 */ 347 void affine_preimage(Variable v, 348 const Linear_Expression& expr, 349 Coefficient_traits::const_reference denominator); 350 351 /*! \brief 352 Inserts in \p *this a copy of the constraint \p c, 353 increasing the number of space dimensions if needed. 354 It is a pending constraint. 355 */ 356 void insert_pending(const Constraint& c); 357 358 //! Adds low-level constraints to the constraint system. 359 void add_low_level_constraints(); 360 361 //! Returns the system topology. 362 Topology topology() const; 363 364 dimension_type num_rows() const; 365 366 /*! \brief 367 Returns <CODE>true</CODE> if and only if 368 the system topology is <CODE>NECESSARILY_CLOSED</CODE>. 369 */ 370 bool is_necessarily_closed() const; 371 372 //! Returns the number of rows that are in the pending part of the system. 373 dimension_type num_pending_rows() const; 374 375 //! Returns the index of the first pending row. 376 dimension_type first_pending_row() const; 377 378 //! Returns the value of the sortedness flag. 379 bool is_sorted() const; 380 381 //! Sets the index to indicate that the system has no pending rows. 382 void unset_pending_rows(); 383 384 //! Sets the index of the first pending row to \p i. 385 void set_index_first_pending_row(dimension_type i); 386 387 //! Sets the sortedness flag of the system to \p b. 388 void set_sorted(bool b); 389 390 //! Makes the system shrink by removing its i-th row. 391 /*! 392 When \p keep_sorted is \p true and the system is sorted, sortedness will 393 be preserved, but this method costs O(n). 394 395 Otherwise, this method just swaps the i-th row with the last and then 396 removes it, so it costs O(1). 397 */ 398 void remove_row(dimension_type i, bool keep_sorted = false); 399 400 //! Removes the specified rows. The row ordering of remaining rows is 401 //! preserved. 402 /*! 403 \param indexes specifies a list of row indexes. 404 It must be sorted. 405 */ 406 void remove_rows(const std::vector<dimension_type>& indexes); 407 408 //! Makes the system shrink by removing the rows in [first,last). 409 /*! 410 When \p keep_sorted is \p true and the system is sorted, sortedness will 411 be preserved, but this method costs O(num_rows()). 412 413 Otherwise, this method just swaps the rows with the last ones and then 414 removes them, so it costs O(last - first). 415 */ 416 void remove_rows(dimension_type first, dimension_type last, 417 bool keep_sorted = false); 418 419 //! Makes the system shrink by removing its \p n trailing rows. 420 void remove_trailing_rows(dimension_type n); 421 422 //! Removes all the specified dimensions from the constraint system. 423 /*! 424 The space dimension of the variable with the highest space 425 dimension in \p vars must be at most the space dimension 426 of \p this. 427 */ 428 void remove_space_dimensions(const Variables_Set& vars); 429 430 //! Shift by \p n positions the coefficients of variables, starting from 431 //! the coefficient of \p v. This increases the space dimension by \p n. 432 void shift_space_dimensions(Variable v, dimension_type n); 433 434 //! Permutes the space dimensions of the matrix. 435 /* 436 \param cycle 437 A vector representing a cycle of the permutation according to which the 438 columns must be rearranged. 439 440 The \p cycle vector represents a cycle of a permutation of space 441 dimensions. 442 For example, the permutation 443 \f$ \{ x_1 \mapsto x_2, x_2 \mapsto x_3, x_3 \mapsto x_1 \}\f$ can be 444 represented by the vector containing \f$ x_1, x_2, x_3 \f$. 445 */ 446 void permute_space_dimensions(const std::vector<Variable>& cycle); 447 448 //! Swaps the coefficients of the variables \p v1 and \p v2 . 449 void swap_space_dimensions(Variable v1, Variable v2); 450 451 bool has_no_rows() const; 452 453 //! Strongly normalizes the system. 454 void strong_normalize(); 455 456 /*! \brief 457 Sorts the non-pending rows (in growing order) and eliminates 458 duplicated ones. 459 */ 460 void sort_rows(); 461 462 /*! \brief 463 Adds the given row to the pending part of the system, stealing its 464 contents and automatically resizing the system or the row, if needed. 465 */ 466 void insert_pending(Constraint& r, Recycle_Input); 467 468 //! Adds the rows of `y' to the pending part of `*this', stealing them from 469 //! `y'. 470 void insert_pending(Constraint_System& r, Recycle_Input); 471 472 /*! \brief 473 Adds \p r to the system, stealing its contents and 474 automatically resizing the system or the row, if needed. 475 */ 476 void insert(Constraint& r, Recycle_Input); 477 478 //! Adds to \p *this a the rows of `y', stealing them from `y'. 479 /*! 480 It is assumed that \p *this has no pending rows. 481 */ 482 void insert(Constraint_System& r, Recycle_Input); 483 484 //! Adds a copy of the rows of `y' to the pending part of `*this'. 485 void insert_pending(const Constraint_System& r); 486 487 /*! \brief 488 Assigns to \p *this the result of merging its rows with 489 those of \p y, obtaining a sorted system. 490 491 Duplicated rows will occur only once in the result. 492 On entry, both systems are assumed to be sorted and have 493 no pending rows. 494 */ 495 void merge_rows_assign(const Constraint_System& y); 496 497 //! Adds to \p *this a copy of the rows of \p y. 498 /*! 499 It is assumed that \p *this has no pending rows. 500 */ 501 void insert(const Constraint_System& y); 502 503 //! Marks the epsilon dimension as a standard dimension. 504 /*! 505 The system topology is changed to <CODE>NOT_NECESSARILY_CLOSED</CODE>, and 506 the number of space dimensions is increased by 1. 507 */ 508 void mark_as_necessarily_closed(); 509 510 //! Marks the last dimension as the epsilon dimension. 511 /*! 512 The system topology is changed to <CODE>NECESSARILY_CLOSED</CODE>, and 513 the number of space dimensions is decreased by 1. 514 */ 515 void mark_as_not_necessarily_closed(); 516 517 //! Minimizes the subsystem of equations contained in \p *this. 518 /*! 519 This method works only on the equalities of the system: 520 the system is required to be partially sorted, so that 521 all the equalities are grouped at its top; it is assumed that 522 the number of equalities is exactly \p n_lines_or_equalities. 523 The method finds a minimal system for the equalities and 524 returns its rank, i.e., the number of linearly independent equalities. 525 The result is an upper triangular subsystem of equalities: 526 for each equality, the pivot is chosen starting from 527 the right-most columns. 528 */ 529 dimension_type gauss(dimension_type n_lines_or_equalities); 530 531 /*! \brief 532 Back-substitutes the coefficients to reduce 533 the complexity of the system. 534 535 Takes an upper triangular system having \p n_lines_or_equalities rows. 536 For each row, starting from the one having the minimum number of 537 coefficients different from zero, computes the expression of an element 538 as a function of the remaining ones and then substitutes this expression 539 in all the other rows. 540 */ 541 void back_substitute(dimension_type n_lines_or_equalities); 542 543 //! Full assignment operator: pending rows are copied as pending. 544 void assign_with_pending(const Constraint_System& y); 545 546 /*! \brief 547 Sorts the pending rows and eliminates those that also occur 548 in the non-pending part of the system. 549 */ 550 void sort_pending_and_remove_duplicates(); 551 552 /*! \brief 553 Sorts the system, removing duplicates, keeping the saturation 554 matrix consistent. 555 556 \param sat 557 Bit matrix with rows corresponding to the rows of \p *this. 558 */ 559 void sort_and_remove_with_sat(Bit_Matrix& sat); 560 561 /*! \brief 562 Returns <CODE>true</CODE> if and only if \p *this is sorted, 563 without checking for duplicates. 564 */ 565 bool check_sorted() const; 566 567 /*! \brief 568 Returns the number of rows in the system 569 that represent either lines or equalities. 570 */ 571 dimension_type num_lines_or_equalities() const; 572 573 //! Adds \p n rows and space dimensions to the system. 574 /*! 575 \param n 576 The number of rows and space dimensions to be added: must be strictly 577 positive. 578 579 Turns the system \f$M \in \Rset^r \times \Rset^c\f$ into 580 the system \f$N \in \Rset^{r+n} \times \Rset^{c+n}\f$ 581 such that 582 \f$N = \bigl(\genfrac{}{}{0pt}{}{0}{M}\genfrac{}{}{0pt}{}{J}{o}\bigr)\f$, 583 where \f$J\f$ is the specular image 584 of the \f$n \times n\f$ identity matrix. 585 */ 586 void add_universe_rows_and_space_dimensions(dimension_type n); 587 588 friend class Polyhedron; 589 friend class Termination_Helpers; 590 }; 591 592 //! An iterator over a system of constraints. 593 /*! \ingroup PPL_CXX_interface 594 A const_iterator is used to provide read-only access 595 to each constraint contained in a Constraint_System object. 596 597 \par Example 598 The following code prints the system of constraints 599 defining the polyhedron <CODE>ph</CODE>: 600 \code 601 const Constraint_System& cs = ph.constraints(); 602 for (Constraint_System::const_iterator i = cs.begin(), 603 cs_end = cs.end(); i != cs_end; ++i) 604 cout << *i << endl; 605 \endcode 606 */ 607 // NOTE: This is not an inner class of Constraint_System, so Constraint can 608 // declare that this class is his friend without including this file 609 // (the .types.hh file suffices). 610 class Parma_Polyhedra_Library::Constraint_System_const_iterator 611 : public std::iterator<std::forward_iterator_tag, 612 Constraint, 613 std::ptrdiff_t, 614 const Constraint*, 615 const Constraint&> { 616 public: 617 //! Default constructor. 618 Constraint_System_const_iterator(); 619 620 //! Ordinary copy constructor. 621 Constraint_System_const_iterator(const Constraint_System_const_iterator& y); 622 623 //! Destructor. 624 ~Constraint_System_const_iterator(); 625 626 //! Assignment operator. 627 Constraint_System_const_iterator& 628 operator=(const Constraint_System_const_iterator& y); 629 630 //! Dereference operator. 631 const Constraint& operator*() const; 632 633 //! Indirect member selector. 634 const Constraint* operator->() const; 635 636 //! Prefix increment operator. 637 Constraint_System_const_iterator& operator++(); 638 639 //! Postfix increment operator. 640 Constraint_System_const_iterator operator++(int); 641 642 /*! \brief 643 Returns <CODE>true</CODE> if and only if 644 \p *this and \p y are identical. 645 */ 646 bool operator==(const Constraint_System_const_iterator& y) const; 647 648 /*! \brief 649 Returns <CODE>true</CODE> if and only if 650 \p *this and \p y are different. 651 */ 652 bool operator!=(const Constraint_System_const_iterator& y) const; 653 654 private: 655 friend class Constraint_System; 656 657 //! The const iterator over the matrix of constraints. 658 Linear_System<Constraint>::const_iterator i; 659 660 //! A const pointer to the matrix of constraints. 661 const Linear_System<Constraint>* csp; 662 663 //! Constructor. 664 Constraint_System_const_iterator(const Linear_System<Constraint> 665 ::const_iterator& iter, 666 const Constraint_System& cs); 667 668 //! \p *this skips to the next non-trivial constraint. 669 void skip_forward(); 670 }; 671 672 namespace Parma_Polyhedra_Library { 673 674 namespace Implementation { 675 676 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 677 //! Helper returning number of constraints in system. 678 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 679 dimension_type 680 num_constraints(const Constraint_System& cs); 681 682 } // namespace Implementation 683 684 } // namespace Parma_Polyhedra_Library 685 686 // Constraint_System_inlines.hh is not included here on purpose. 687 688 #endif // !defined(PPL_Constraint_System_defs_hh) 689