1 /* Grid 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_Grid_defs_hh 25 #define PPL_Grid_defs_hh 1 26 27 #include "Grid_types.hh" 28 #include "globals_defs.hh" 29 #include "Variable_defs.hh" 30 #include "Variables_Set_types.hh" 31 #include "Linear_Expression_defs.hh" 32 #include "Constraint_types.hh" 33 #include "Constraint_System_defs.hh" 34 #include "Constraint_System_inlines.hh" 35 #include "Congruence_System_defs.hh" 36 #include "Congruence_System_inlines.hh" 37 #include "Grid_Generator_System_defs.hh" 38 #include "Grid_Generator_System_inlines.hh" 39 #include "Grid_Generator_types.hh" 40 #include "Poly_Con_Relation_defs.hh" 41 #include "Poly_Gen_Relation_defs.hh" 42 #include "Grid_Certificate_types.hh" 43 #include "Box_types.hh" 44 #include "Polyhedron_types.hh" 45 #include "BD_Shape_types.hh" 46 #include "Octagonal_Shape_types.hh" 47 #include <vector> 48 #include <iosfwd> 49 50 namespace Parma_Polyhedra_Library { 51 52 namespace IO_Operators { 53 54 //! Output operator. 55 /*! 56 \relates Parma_Polyhedra_Library::Grid 57 Writes a textual representation of \p gr on \p s: <CODE>false</CODE> 58 is written if \p gr is an empty grid; <CODE>true</CODE> is written 59 if \p gr is a universe grid; a minimized system of congruences 60 defining \p gr is written otherwise, all congruences in one row 61 separated by ", "s. 62 */ 63 std::ostream& 64 operator<<(std::ostream& s, const Grid& gr); 65 66 } // namespace IO_Operators 67 68 //! Swaps \p x with \p y. 69 /*! \relates Grid */ 70 void swap(Grid& x, Grid& y); 71 72 /*! \brief 73 Returns <CODE>true</CODE> if and only if \p x and \p y are the same 74 grid. 75 76 \relates Grid 77 Note that \p x and \p y may be dimension-incompatible grids: in 78 those cases, the value <CODE>false</CODE> is returned. 79 */ 80 bool operator==(const Grid& x, const Grid& y); 81 82 /*! \brief 83 Returns <CODE>true</CODE> if and only if \p x and \p y are different 84 grids. 85 86 \relates Grid 87 Note that \p x and \p y may be dimension-incompatible grids: in 88 those cases, the value <CODE>true</CODE> is returned. 89 */ 90 bool operator!=(const Grid& x, const Grid& y); 91 92 } // namespace Parma_Polyhedra_Library 93 94 95 //! A grid. 96 /*! \ingroup PPL_CXX_interface 97 An object of the class Grid represents a rational grid. 98 99 The domain of grids <EM>optimally supports</EM>: 100 - all (proper and non-proper) congruences; 101 - tautological and inconsistent constraints; 102 - linear equality constraints (i.e., non-proper congruences). 103 104 Depending on the method, using a constraint that is not optimally 105 supported by the domain will either raise an exception or 106 result in a (possibly non-optimal) upward approximation. 107 108 The domain of grids support a concept of double description similar 109 to the one developed for polyhedra: hence, a grid can be specified 110 as either a finite system of congruences or a finite system of 111 generators (see Section \ref sect_rational_grids) and it is always 112 possible to obtain either representation. 113 That is, if we know the system of congruences, we can obtain 114 from this a system of generators that define the same grid 115 and vice versa. 116 These systems can contain redundant members, or they can be in the 117 minimal form. 118 119 A key attribute of any grid is its space dimension (the dimension 120 \f$n \in \Nset\f$ of the enclosing vector space): 121 122 - all grids, the empty ones included, are endowed with a space 123 dimension; 124 - most operations working on a grid and another object (another 125 grid, a congruence, a generator, a set of variables, etc.) will 126 throw an exception if the grid and the object are not 127 dimension-compatible (see Section \ref Grid_Space_Dimensions); 128 - the only ways in which the space dimension of a grid can be 129 changed are with <EM>explicit</EM> calls to operators provided for 130 that purpose, and with standard copy, assignment and swap 131 operators. 132 133 Note that two different grids can be defined on the zero-dimension 134 space: the empty grid and the universe grid \f$R^0\f$. 135 136 \par 137 In all the examples it is assumed that variables 138 <CODE>x</CODE> and <CODE>y</CODE> are defined (where they are 139 used) as follows: 140 \code 141 Variable x(0); 142 Variable y(1); 143 \endcode 144 145 \par Example 1 146 The following code builds a grid corresponding to the even integer 147 pairs in \f$\Rset^2\f$, given as a system of congruences: 148 \code 149 Congruence_System cgs; 150 cgs.insert((x %= 0) / 2); 151 cgs.insert((y %= 0) / 2); 152 Grid gr(cgs); 153 \endcode 154 The following code builds the same grid as above, but starting 155 from a system of generators specifying three of the points: 156 \code 157 Grid_Generator_System gs; 158 gs.insert(grid_point(0*x + 0*y)); 159 gs.insert(grid_point(0*x + 2*y)); 160 gs.insert(grid_point(2*x + 0*y)); 161 Grid gr(gs); 162 \endcode 163 164 \par Example 2 165 The following code builds a grid corresponding to a line in 166 \f$\Rset^2\f$ by adding a single congruence to the universe grid: 167 \code 168 Congruence_System cgs; 169 cgs.insert(x - y == 0); 170 Grid gr(cgs); 171 \endcode 172 The following code builds the same grid as above, but starting 173 from a system of generators specifying a point and a line: 174 \code 175 Grid_Generator_System gs; 176 gs.insert(grid_point(0*x + 0*y)); 177 gs.insert(grid_line(x + y)); 178 Grid gr(gs); 179 \endcode 180 181 \par Example 3 182 The following code builds a grid corresponding to the integral 183 points on the line \f$x = y\f$ in \f$\Rset^2\f$ constructed 184 by adding an equality and congruence to the universe grid: 185 \code 186 Congruence_System cgs; 187 cgs.insert(x - y == 0); 188 cgs.insert(x %= 0); 189 Grid gr(cgs); 190 \endcode 191 The following code builds the same grid as above, but starting 192 from a system of generators specifying a point and a parameter: 193 \code 194 Grid_Generator_System gs; 195 gs.insert(grid_point(0*x + 0*y)); 196 gs.insert(parameter(x + y)); 197 Grid gr(gs); 198 \endcode 199 200 \par Example 4 201 The following code builds the grid corresponding to a plane by 202 creating the universe grid in \f$\Rset^2\f$: 203 \code 204 Grid gr(2); 205 \endcode 206 The following code builds the same grid as above, but starting 207 from the empty grid in \f$\Rset^2\f$ and inserting the appropriate 208 generators (a point, and two lines). 209 \code 210 Grid gr(2, EMPTY); 211 gr.add_grid_generator(grid_point(0*x + 0*y)); 212 gr.add_grid_generator(grid_line(x)); 213 gr.add_grid_generator(grid_line(y)); 214 \endcode 215 Note that a generator system must contain a point when describing 216 a grid. To ensure that this is always the case it is required 217 that the first generator inserted in an empty grid is a point 218 (otherwise, an exception is thrown). 219 220 \par Example 5 221 The following code shows the use of the function 222 <CODE>add_space_dimensions_and_embed</CODE>: 223 \code 224 Grid gr(1); 225 gr.add_congruence(x == 2); 226 gr.add_space_dimensions_and_embed(1); 227 \endcode 228 We build the universe grid in the 1-dimension space \f$\Rset\f$. 229 Then we add a single equality congruence, 230 thus obtaining the grid corresponding to the singleton set 231 \f$\{ 2 \} \sseq \Rset\f$. 232 After the last line of code, the resulting grid is 233 \f[ 234 \bigl\{\, 235 (2, y)^\transpose \in \Rset^2 236 \bigm| 237 y \in \Rset 238 \,\bigr\}. 239 \f] 240 241 \par Example 6 242 The following code shows the use of the function 243 <CODE>add_space_dimensions_and_project</CODE>: 244 \code 245 Grid gr(1); 246 gr.add_congruence(x == 2); 247 gr.add_space_dimensions_and_project(1); 248 \endcode 249 The first two lines of code are the same as in Example 4 for 250 <CODE>add_space_dimensions_and_embed</CODE>. 251 After the last line of code, the resulting grid is 252 the singleton set 253 \f$\bigl\{ (2, 0)^\transpose \bigr\} \sseq \Rset^2\f$. 254 255 \par Example 7 256 The following code shows the use of the function 257 <CODE>affine_image</CODE>: 258 \code 259 Grid gr(2, EMPTY); 260 gr.add_grid_generator(grid_point(0*x + 0*y)); 261 gr.add_grid_generator(grid_point(4*x + 0*y)); 262 gr.add_grid_generator(grid_point(0*x + 2*y)); 263 Linear_Expression expr = x + 3; 264 gr.affine_image(x, expr); 265 \endcode 266 In this example the starting grid is all the pairs of \f$x\f$ and 267 \f$y\f$ in \f$\Rset^2\f$ where \f$x\f$ is an integer multiple of 4 268 and \f$y\f$ is an integer multiple of 2. The considered variable 269 is \f$x\f$ and the affine expression is \f$x+3\f$. The resulting 270 grid is the given grid translated 3 integers to the right (all the 271 pairs \f$(x, y)\f$ where \f$x\f$ is -1 plus an integer multiple of 4 272 and \f$y\f$ is an integer multiple of 2). 273 Moreover, if the affine transformation for the same variable \p x 274 is instead \f$x+y\f$: 275 \code 276 Linear_Expression expr = x + y; 277 \endcode 278 the resulting grid is every second integral point along the \f$x=y\f$ 279 line, with this line of points repeated at every fourth integral value 280 along the \f$x\f$ axis. 281 Instead, if we do not use an invertible transformation for the 282 same variable; for example, the affine expression \f$y\f$: 283 \code 284 Linear_Expression expr = y; 285 \endcode 286 the resulting grid is every second point along the \f$x=y\f$ line. 287 288 \par Example 8 289 The following code shows the use of the function 290 <CODE>affine_preimage</CODE>: 291 \code 292 Grid gr(2, EMPTY); 293 gr.add_grid_generator(grid_point(0*x + 0*y)); 294 gr.add_grid_generator(grid_point(4*x + 0*y)); 295 gr.add_grid_generator(grid_point(0*x + 2*y)); 296 Linear_Expression expr = x + 3; 297 gr.affine_preimage(x, expr); 298 \endcode 299 In this example the starting grid, \p var and the affine 300 expression and the denominator are the same as in Example 6, while 301 the resulting grid is similar but translated 3 integers to the 302 left (all the pairs \f$(x, y)\f$ 303 where \f$x\f$ is -3 plus an integer multiple of 4 and 304 \f$y\f$ is an integer multiple of 2).. 305 Moreover, if the affine transformation for \p x is \f$x+y\f$ 306 \code 307 Linear_Expression expr = x + y; 308 \endcode 309 the resulting grid is a similar grid to the result in Example 6, 310 only the grid is slanted along \f$x=-y\f$. 311 Instead, if we do not use an invertible transformation for the same 312 variable \p x, for example, the affine expression \f$y\f$: 313 \code 314 Linear_Expression expr = y; 315 \endcode 316 the resulting grid is every fourth line parallel to the \f$x\f$ 317 axis. 318 319 \par Example 9 320 For this example we also use the variables: 321 \code 322 Variable z(2); 323 Variable w(3); 324 \endcode 325 The following code shows the use of the function 326 <CODE>remove_space_dimensions</CODE>: 327 \code 328 Grid_Generator_System gs; 329 gs.insert(grid_point(3*x + y +0*z + 2*w)); 330 Grid gr(gs); 331 Variables_Set vars; 332 vars.insert(y); 333 vars.insert(z); 334 gr.remove_space_dimensions(vars); 335 \endcode 336 The starting grid is the singleton set 337 \f$\bigl\{ (3, 1, 0, 2)^\transpose \bigr\} \sseq \Rset^4\f$, while 338 the resulting grid is 339 \f$\bigl\{ (3, 2)^\transpose \bigr\} \sseq \Rset^2\f$. 340 Be careful when removing space dimensions <EM>incrementally</EM>: 341 since dimensions are automatically renamed after each application 342 of the <CODE>remove_space_dimensions</CODE> operator, unexpected 343 results can be obtained. 344 For instance, by using the following code we would obtain 345 a different result: 346 \code 347 set<Variable> vars1; 348 vars1.insert(y); 349 gr.remove_space_dimensions(vars1); 350 set<Variable> vars2; 351 vars2.insert(z); 352 gr.remove_space_dimensions(vars2); 353 \endcode 354 In this case, the result is the grid 355 \f$\bigl\{(3, 0)^\transpose \bigr\} \sseq \Rset^2\f$: 356 when removing the set of dimensions \p vars2 357 we are actually removing variable \f$w\f$ of the original grid. 358 For the same reason, the operator \p remove_space_dimensions 359 is not idempotent: removing twice the same non-empty set of dimensions 360 is never the same as removing them just once. 361 */ 362 363 class Parma_Polyhedra_Library::Grid { 364 public: 365 //! The numeric type of coefficients. 366 typedef Coefficient coefficient_type; 367 368 //! Returns the maximum space dimension all kinds of Grid can handle. 369 static dimension_type max_space_dimension(); 370 371 /*! \brief 372 Returns true indicating that this domain has methods that 373 can recycle congruences. 374 */ 375 static bool can_recycle_congruence_systems(); 376 377 /*! \brief 378 Returns true indicating that this domain has methods that 379 can recycle constraints. 380 */ 381 static bool can_recycle_constraint_systems(); 382 383 //! Builds a grid having the specified properties. 384 /*! 385 \param num_dimensions 386 The number of dimensions of the vector space enclosing the grid; 387 388 \param kind 389 Specifies whether the universe or the empty grid has to be built. 390 391 \exception std::length_error 392 Thrown if \p num_dimensions exceeds the maximum allowed space 393 dimension. 394 */ 395 explicit Grid(dimension_type num_dimensions = 0, 396 Degenerate_Element kind = UNIVERSE); 397 398 //! Builds a grid, copying a system of congruences. 399 /*! 400 The grid inherits the space dimension of the congruence system. 401 402 \param cgs 403 The system of congruences defining the grid. 404 405 \exception std::length_error 406 Thrown if \p num_dimensions exceeds the maximum allowed space 407 dimension. 408 */ 409 explicit Grid(const Congruence_System& cgs); 410 411 //! Builds a grid, recycling a system of congruences. 412 /*! 413 The grid inherits the space dimension of the congruence system. 414 415 \param cgs 416 The system of congruences defining the grid. Its data-structures 417 may be recycled to build the grid. 418 419 \param dummy 420 A dummy tag to syntactically differentiate this one 421 from the other constructors. 422 423 \exception std::length_error 424 Thrown if \p num_dimensions exceeds the maximum allowed space 425 dimension. 426 */ 427 Grid(Congruence_System& cgs, Recycle_Input dummy); 428 429 //! Builds a grid, copying a system of constraints. 430 /*! 431 The grid inherits the space dimension of the constraint system. 432 433 \param cs 434 The system of constraints defining the grid. 435 436 \exception std::invalid_argument 437 Thrown if the constraint system \p cs contains inequality constraints. 438 439 \exception std::length_error 440 Thrown if \p num_dimensions exceeds the maximum allowed space 441 dimension. 442 */ 443 explicit Grid(const Constraint_System& cs); 444 445 //! Builds a grid, recycling a system of constraints. 446 /*! 447 The grid inherits the space dimension of the constraint system. 448 449 \param cs 450 The system of constraints defining the grid. Its data-structures 451 may be recycled to build the grid. 452 453 \param dummy 454 A dummy tag to syntactically differentiate this one 455 from the other constructors. 456 457 \exception std::invalid_argument 458 Thrown if the constraint system \p cs contains inequality constraints. 459 460 \exception std::length_error 461 Thrown if \p num_dimensions exceeds the maximum allowed space 462 dimension. 463 */ 464 Grid(Constraint_System& cs, Recycle_Input dummy); 465 466 //! Builds a grid, copying a system of grid generators. 467 /*! 468 The grid inherits the space dimension of the generator system. 469 470 \param ggs 471 The system of generators defining the grid. 472 473 \exception std::invalid_argument 474 Thrown if the system of generators is not empty but has no points. 475 476 \exception std::length_error 477 Thrown if \p num_dimensions exceeds the maximum allowed space 478 dimension. 479 */ 480 explicit Grid(const Grid_Generator_System& ggs); 481 482 //! Builds a grid, recycling a system of grid generators. 483 /*! 484 The grid inherits the space dimension of the generator system. 485 486 \param ggs 487 The system of generators defining the grid. Its data-structures 488 may be recycled to build the grid. 489 490 \param dummy 491 A dummy tag to syntactically differentiate this one 492 from the other constructors. 493 494 \exception std::invalid_argument 495 Thrown if the system of generators is not empty but has no points. 496 497 \exception std::length_error 498 Thrown if \p num_dimensions exceeds the maximum allowed space dimension. 499 */ 500 Grid(Grid_Generator_System& ggs, Recycle_Input dummy); 501 502 //! Builds a grid out of a box. 503 /*! 504 The grid inherits the space dimension of the box. 505 The built grid is the most precise grid that includes the box. 506 507 \param box 508 The box representing the grid to be built. 509 510 \param complexity 511 This argument is ignored as the algorithm used has 512 polynomial complexity. 513 514 \exception std::length_error 515 Thrown if the space dimension of \p box exceeds the maximum 516 allowed space dimension. 517 */ 518 template <typename Interval> 519 explicit Grid(const Box<Interval>& box, 520 Complexity_Class complexity = ANY_COMPLEXITY); 521 522 //! Builds a grid out of a bounded-difference shape. 523 /*! 524 The grid inherits the space dimension of the BDS. 525 The built grid is the most precise grid that includes the BDS. 526 527 \param bd 528 The BDS representing the grid to be built. 529 530 \param complexity 531 This argument is ignored as the algorithm used has 532 polynomial complexity. 533 534 \exception std::length_error 535 Thrown if the space dimension of \p bd exceeds the maximum 536 allowed space dimension. 537 */ 538 template <typename U> 539 explicit Grid(const BD_Shape<U>& bd, 540 Complexity_Class complexity = ANY_COMPLEXITY); 541 542 //! Builds a grid out of an octagonal shape. 543 /*! 544 The grid inherits the space dimension of the octagonal shape. 545 The built grid is the most precise grid that includes the octagonal shape. 546 547 \param os 548 The octagonal shape representing the grid to be built. 549 550 \param complexity 551 This argument is ignored as the algorithm used has 552 polynomial complexity. 553 554 \exception std::length_error 555 Thrown if the space dimension of \p os exceeds the maximum 556 allowed space dimension. 557 */ 558 template <typename U> 559 explicit Grid(const Octagonal_Shape<U>& os, 560 Complexity_Class complexity = ANY_COMPLEXITY); 561 562 /*! \brief 563 Builds a grid from a polyhedron using algorithms whose complexity 564 does not exceed the one specified by \p complexity. 565 If \p complexity is \p ANY_COMPLEXITY, then the grid built is the 566 smallest one containing \p ph. 567 568 The grid inherits the space dimension of polyhedron. 569 570 \param ph 571 The polyhedron. 572 573 \param complexity 574 The complexity class. 575 576 \exception std::length_error 577 Thrown if \p num_dimensions exceeds the maximum allowed space 578 dimension. 579 */ 580 explicit Grid(const Polyhedron& ph, 581 Complexity_Class complexity = ANY_COMPLEXITY); 582 583 //! Ordinary copy constructor. 584 /*! 585 The complexity argument is ignored. 586 */ 587 Grid(const Grid& y, 588 Complexity_Class complexity = ANY_COMPLEXITY); 589 590 /*! \brief 591 The assignment operator. (\p *this and \p y can be 592 dimension-incompatible.) 593 */ 594 Grid& operator=(const Grid& y); 595 596 //! \name Member Functions that Do Not Modify the Grid 597 //@{ 598 599 //! Returns the dimension of the vector space enclosing \p *this. 600 dimension_type space_dimension() const; 601 602 /*! \brief 603 Returns \f$0\f$, if \p *this is empty; otherwise, returns 604 the \ref Grid_Affine_Dimension "affine dimension" of \p *this. 605 */ 606 dimension_type affine_dimension() const; 607 608 /*! \brief 609 Returns a system of equality constraints satisfied by \p *this 610 with the same affine dimension as \p *this. 611 */ 612 Constraint_System constraints() const; 613 614 /*! \brief 615 Returns a minimal system of equality constraints satisfied by 616 \p *this with the same affine dimension as \p *this. 617 */ 618 Constraint_System minimized_constraints() const; 619 620 //! Returns the system of congruences. 621 const Congruence_System& congruences() const; 622 623 //! Returns the system of congruences in minimal form. 624 const Congruence_System& minimized_congruences() const; 625 626 //! Returns the system of generators. 627 const Grid_Generator_System& grid_generators() const; 628 629 //! Returns the minimized system of generators. 630 const Grid_Generator_System& minimized_grid_generators() const; 631 632 //! Returns the relations holding between \p *this and \p cg. 633 /* 634 \exception std::invalid_argument 635 Thrown if \p *this and congruence \p cg are dimension-incompatible. 636 */ 637 // FIXME: Poly_Con_Relation seems to encode exactly what we want 638 // here. We must find a new name for that class. Temporarily, 639 // we keep using it without changing the name. 640 Poly_Con_Relation relation_with(const Congruence& cg) const; 641 642 //! Returns the relations holding between \p *this and \p g. 643 /* 644 \exception std::invalid_argument 645 Thrown if \p *this and generator \p g are dimension-incompatible. 646 */ 647 // FIXME: see the comment for Poly_Con_Relation above. 648 Poly_Gen_Relation 649 relation_with(const Grid_Generator& g) const; 650 651 //! Returns the relations holding between \p *this and \p g. 652 /* 653 \exception std::invalid_argument 654 Thrown if \p *this and generator \p g are dimension-incompatible. 655 */ 656 // FIXME: see the comment for Poly_Con_Relation above. 657 Poly_Gen_Relation 658 relation_with(const Generator& g) const; 659 660 //! Returns the relations holding between \p *this and \p c. 661 /* 662 \exception std::invalid_argument 663 Thrown if \p *this and constraint \p c are dimension-incompatible. 664 */ 665 // FIXME: Poly_Con_Relation seems to encode exactly what we want 666 // here. We must find a new name for that class. Temporarily, 667 // we keep using it without changing the name. 668 Poly_Con_Relation relation_with(const Constraint& c) const; 669 670 //! Returns \c true if and only if \p *this is an empty grid. 671 bool is_empty() const; 672 673 //! Returns \c true if and only if \p *this is a universe grid. 674 bool is_universe() const; 675 676 /*! \brief 677 Returns <CODE>true</CODE> if and only if \p *this is a 678 topologically closed subset of the vector space. 679 680 A grid is always topologically closed. 681 */ 682 bool is_topologically_closed() const; 683 684 /*! \brief 685 Returns <CODE>true</CODE> if and only if \p *this and \p y are 686 disjoint. 687 688 \exception std::invalid_argument 689 Thrown if \p x and \p y are dimension-incompatible. 690 */ 691 bool is_disjoint_from(const Grid& y) const; 692 693 //! Returns <CODE>true</CODE> if and only if \p *this is discrete. 694 /*! 695 A grid is discrete if it can be defined by a generator system which 696 contains only points and parameters. This includes the empty grid 697 and any grid in dimension zero. 698 */ 699 bool is_discrete() const; 700 701 //! Returns <CODE>true</CODE> if and only if \p *this is bounded. 702 bool is_bounded() const; 703 704 /*! \brief 705 Returns <CODE>true</CODE> if and only if \p *this 706 contains at least one integer point. 707 */ 708 bool contains_integer_point() const; 709 710 /*! \brief 711 Returns <CODE>true</CODE> if and only if \p var is constrained in 712 \p *this. 713 714 \exception std::invalid_argument 715 Thrown if \p var is not a space dimension of \p *this. 716 */ 717 bool constrains(Variable var) const; 718 719 //! Returns <CODE>true</CODE> if and only if \p expr is bounded in \p *this. 720 /*! 721 This method is the same as bounds_from_below. 722 723 \exception std::invalid_argument 724 Thrown if \p expr and \p *this are dimension-incompatible. 725 */ 726 bool bounds_from_above(const Linear_Expression& expr) const; 727 728 //! Returns <CODE>true</CODE> if and only if \p expr is bounded in \p *this. 729 /*! 730 This method is the same as bounds_from_above. 731 732 \exception std::invalid_argument 733 Thrown if \p expr and \p *this are dimension-incompatible. 734 */ 735 bool bounds_from_below(const Linear_Expression& expr) const; 736 737 /*! \brief 738 Returns <CODE>true</CODE> if and only if \p *this is not empty and 739 \p expr is bounded from above in \p *this, in which case the 740 supremum value is computed. 741 742 \param expr 743 The linear expression to be maximized subject to \p *this; 744 745 \param sup_n 746 The numerator of the supremum value; 747 748 \param sup_d 749 The denominator of the supremum value; 750 751 \param maximum 752 <CODE>true</CODE> if the supremum value can be reached in \p this. 753 Always <CODE>true</CODE> when \p this bounds \p expr. Present for 754 interface compatibility with class Polyhedron, where closure 755 points can result in a value of false. 756 757 \exception std::invalid_argument 758 Thrown if \p expr and \p *this are dimension-incompatible. 759 760 If \p *this is empty or \p expr is not bounded by \p *this, 761 <CODE>false</CODE> is returned and \p sup_n, \p sup_d and \p 762 maximum are left untouched. 763 */ 764 bool maximize(const Linear_Expression& expr, 765 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const; 766 767 /*! \brief 768 Returns <CODE>true</CODE> if and only if \p *this is not empty and 769 \p expr is bounded from above in \p *this, in which case the 770 supremum value and a point where \p expr reaches it are computed. 771 772 \param expr 773 The linear expression to be maximized subject to \p *this; 774 775 \param sup_n 776 The numerator of the supremum value; 777 778 \param sup_d 779 The denominator of the supremum value; 780 781 \param maximum 782 <CODE>true</CODE> if the supremum value can be reached in \p this. 783 Always <CODE>true</CODE> when \p this bounds \p expr. Present for 784 interface compatibility with class Polyhedron, where closure 785 points can result in a value of false; 786 787 \param point 788 When maximization succeeds, will be assigned a point where \p expr 789 reaches its supremum value. 790 791 \exception std::invalid_argument 792 Thrown if \p expr and \p *this are dimension-incompatible. 793 794 If \p *this is empty or \p expr is not bounded by \p *this, 795 <CODE>false</CODE> is returned and \p sup_n, \p sup_d, \p maximum 796 and \p point are left untouched. 797 */ 798 bool maximize(const Linear_Expression& expr, 799 Coefficient& sup_n, Coefficient& sup_d, bool& maximum, 800 Generator& point) const; 801 802 /*! \brief 803 Returns <CODE>true</CODE> if and only if \p *this is not empty and 804 \p expr is bounded from below in \p *this, in which case the 805 infimum value is computed. 806 807 \param expr 808 The linear expression to be minimized subject to \p *this; 809 810 \param inf_n 811 The numerator of the infimum value; 812 813 \param inf_d 814 The denominator of the infimum value; 815 816 \param minimum 817 <CODE>true</CODE> if the is the infimum value can be reached in \p 818 this. Always <CODE>true</CODE> when \p this bounds \p expr. 819 Present for interface compatibility with class Polyhedron, where 820 closure points can result in a value of false. 821 822 \exception std::invalid_argument 823 Thrown if \p expr and \p *this are dimension-incompatible. 824 825 If \p *this is empty or \p expr is not bounded from below, 826 <CODE>false</CODE> is returned and \p inf_n, \p inf_d 827 and \p minimum are left untouched. 828 */ 829 bool minimize(const Linear_Expression& expr, 830 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const; 831 832 /*! \brief 833 Returns <CODE>true</CODE> if and only if \p *this is not empty and 834 \p expr is bounded from below in \p *this, in which case the 835 infimum value and a point where \p expr reaches it are computed. 836 837 \param expr 838 The linear expression to be minimized subject to \p *this; 839 840 \param inf_n 841 The numerator of the infimum value; 842 843 \param inf_d 844 The denominator of the infimum value; 845 846 \param minimum 847 <CODE>true</CODE> if the is the infimum value can be reached in \p 848 this. Always <CODE>true</CODE> when \p this bounds \p expr. 849 Present for interface compatibility with class Polyhedron, where 850 closure points can result in a value of false; 851 852 \param point 853 When minimization succeeds, will be assigned a point where \p expr 854 reaches its infimum value. 855 856 \exception std::invalid_argument 857 Thrown if \p expr and \p *this are dimension-incompatible. 858 859 If \p *this is empty or \p expr is not bounded from below, 860 <CODE>false</CODE> is returned and \p inf_n, \p inf_d, \p minimum 861 and \p point are left untouched. 862 */ 863 bool minimize(const Linear_Expression& expr, 864 Coefficient& inf_n, Coefficient& inf_d, bool& minimum, 865 Generator& point) const; 866 867 /*! \brief 868 Returns <CODE>true</CODE> if and only if \p *this is not empty and 869 \ref Grid_Frequency "frequency" for \p *this with respect to \p expr 870 is defined, in which case the frequency and the value for \p expr 871 that is closest to zero are computed. 872 873 \param expr 874 The linear expression for which the frequency is needed; 875 876 \param freq_n 877 The numerator of the maximum frequency of \p expr; 878 879 \param freq_d 880 The denominator of the maximum frequency of \p expr; 881 882 \param val_n 883 The numerator of them value of \p expr at a point in the grid 884 that is closest to zero; 885 886 \param val_d 887 The denominator of a value of \p expr at a point in the grid 888 that is closest to zero; 889 890 \exception std::invalid_argument 891 Thrown if \p expr and \p *this are dimension-incompatible. 892 893 If \p *this is empty or frequency is undefined with respect to \p expr, 894 then <CODE>false</CODE> is returned and \p freq_n, \p freq_d, 895 \p val_n and \p val_d are left untouched. 896 */ 897 bool frequency(const Linear_Expression& expr, 898 Coefficient& freq_n, Coefficient& freq_d, 899 Coefficient& val_n, Coefficient& val_d) const; 900 901 //! Returns <CODE>true</CODE> if and only if \p *this contains \p y. 902 /*! 903 \exception std::invalid_argument 904 Thrown if \p *this and \p y are dimension-incompatible. 905 */ 906 bool contains(const Grid& y) const; 907 908 /*! \brief 909 Returns <CODE>true</CODE> if and only if \p *this strictly 910 contains \p y. 911 912 \exception std::invalid_argument 913 Thrown if \p *this and \p y are dimension-incompatible. 914 */ 915 bool strictly_contains(const Grid& y) const; 916 917 //! Checks if all the invariants are satisfied. 918 /*! 919 \return 920 <CODE>true</CODE> if and only if \p *this satisfies all the 921 invariants and either \p check_not_empty is <CODE>false</CODE> or 922 \p *this is not empty. 923 924 \param check_not_empty 925 <CODE>true</CODE> if and only if, in addition to checking the 926 invariants, \p *this must be checked to be not empty. 927 928 The check is performed so as to intrude as little as possible. If 929 the library has been compiled with run-time assertions enabled, 930 error messages are written on <CODE>std::cerr</CODE> in case 931 invariants are violated. This is useful for the purpose of 932 debugging the library. 933 */ 934 bool OK(bool check_not_empty = false) const; 935 936 //@} // Member Functions that Do Not Modify the Grid 937 938 //! \name Space Dimension Preserving Member Functions that May Modify the Grid 939 //@{ 940 941 //! Adds a copy of congruence \p cg to \p *this. 942 /*! 943 \exception std::invalid_argument 944 Thrown if \p *this and congruence \p cg are 945 dimension-incompatible. 946 */ 947 void add_congruence(const Congruence& cg); 948 949 /*! \brief 950 Adds a copy of grid generator \p g to the system of generators of 951 \p *this. 952 953 \exception std::invalid_argument 954 Thrown if \p *this and generator \p g are dimension-incompatible, 955 or if \p *this is an empty grid and \p g is not a point. 956 */ 957 void add_grid_generator(const Grid_Generator& g); 958 959 //! Adds a copy of each congruence in \p cgs to \p *this. 960 /*! 961 \param cgs 962 Contains the congruences that will be added to the system of 963 congruences of \p *this. 964 965 \exception std::invalid_argument 966 Thrown if \p *this and \p cgs are dimension-incompatible. 967 */ 968 void add_congruences(const Congruence_System& cgs); 969 970 //! Adds the congruences in \p cgs to *this. 971 /*! 972 \param cgs 973 The congruence system to be added to \p *this. The congruences in 974 \p cgs may be recycled. 975 976 \exception std::invalid_argument 977 Thrown if \p *this and \p cgs are dimension-incompatible. 978 979 \warning 980 The only assumption that can be made about \p cgs upon successful 981 or exceptional return is that it can be safely destroyed. 982 */ 983 void add_recycled_congruences(Congruence_System& cgs); 984 985 /*! \brief 986 Adds to \p *this a congruence equivalent to constraint \p c. 987 988 \param c 989 The constraint to be added. 990 991 \exception std::invalid_argument 992 Thrown if \p *this and \p c are dimension-incompatible 993 or if constraint \p c is not optimally supported by the grid domain. 994 */ 995 void add_constraint(const Constraint& c); 996 997 /*! \brief 998 Adds to \p *this congruences equivalent to the constraints in \p cs. 999 1000 \param cs 1001 The constraints to be added. 1002 1003 \exception std::invalid_argument 1004 Thrown if \p *this and \p cs are dimension-incompatible 1005 or if \p cs contains a constraint which is not optimally supported 1006 by the grid domain. 1007 */ 1008 void add_constraints(const Constraint_System& cs); 1009 1010 /*! \brief 1011 Adds to \p *this congruences equivalent to the constraints in \p cs. 1012 1013 \param cs 1014 The constraints to be added. They may be recycled. 1015 1016 \exception std::invalid_argument 1017 Thrown if \p *this and \p cs are dimension-incompatible 1018 or if \p cs contains a constraint which is not optimally supported 1019 by the grid domain. 1020 1021 \warning 1022 The only assumption that can be made about \p cs upon successful 1023 or exceptional return is that it can be safely destroyed. 1024 */ 1025 void add_recycled_constraints(Constraint_System& cs); 1026 1027 //! Uses a copy of the congruence \p cg to refine \p *this. 1028 /*! 1029 \param cg 1030 The congruence used. 1031 1032 \exception std::invalid_argument 1033 Thrown if \p *this and congruence \p cg are dimension-incompatible. 1034 */ 1035 void refine_with_congruence(const Congruence& cg); 1036 1037 //! Uses a copy of the congruences in \p cgs to refine \p *this. 1038 /*! 1039 \param cgs 1040 The congruences used. 1041 1042 \exception std::invalid_argument 1043 Thrown if \p *this and \p cgs are dimension-incompatible. 1044 */ 1045 void refine_with_congruences(const Congruence_System& cgs); 1046 1047 //! Uses a copy of the constraint \p c to refine \p *this. 1048 /*! 1049 1050 \param c 1051 The constraint used. If it is not an equality, it will be ignored 1052 1053 \exception std::invalid_argument 1054 Thrown if \p *this and \p c are dimension-incompatible. 1055 */ 1056 void refine_with_constraint(const Constraint& c); 1057 1058 //! Uses a copy of the constraints in \p cs to refine \p *this. 1059 /*! 1060 \param cs 1061 The constraints used. Constraints that are not equalities are ignored. 1062 1063 \exception std::invalid_argument 1064 Thrown if \p *this and \p cs are dimension-incompatible. 1065 */ 1066 void refine_with_constraints(const Constraint_System& cs); 1067 1068 /*! \brief 1069 Adds a copy of the generators in \p gs to the system of generators 1070 of \p *this. 1071 1072 \param gs 1073 Contains the generators that will be added to the system of 1074 generators of \p *this. 1075 1076 \exception std::invalid_argument 1077 Thrown if \p *this and \p gs are dimension-incompatible, or if 1078 \p *this is empty and the system of generators \p gs is not empty, 1079 but has no points. 1080 */ 1081 void add_grid_generators(const Grid_Generator_System& gs); 1082 1083 /*! \brief 1084 Adds the generators in \p gs to the system of generators of \p 1085 *this. 1086 1087 \param gs 1088 The generator system to be added to \p *this. The generators in 1089 \p gs may be recycled. 1090 1091 \exception std::invalid_argument 1092 Thrown if \p *this and \p gs are dimension-incompatible. 1093 1094 \warning 1095 The only assumption that can be made about \p gs upon successful 1096 or exceptional return is that it can be safely destroyed. 1097 */ 1098 void add_recycled_grid_generators(Grid_Generator_System& gs); 1099 1100 /*! \brief 1101 Computes the \ref Cylindrification "cylindrification" of \p *this with 1102 respect to space dimension \p var, assigning the result to \p *this. 1103 1104 \param var 1105 The space dimension that will be unconstrained. 1106 1107 \exception std::invalid_argument 1108 Thrown if \p var is not a space dimension of \p *this. 1109 */ 1110 void unconstrain(Variable var); 1111 1112 /*! \brief 1113 Computes the \ref Cylindrification "cylindrification" of \p *this with 1114 respect to the set of space dimensions \p vars, 1115 assigning the result to \p *this. 1116 1117 \param vars 1118 The set of space dimension that will be unconstrained. 1119 1120 \exception std::invalid_argument 1121 Thrown if \p *this is dimension-incompatible with one of the 1122 Variable objects contained in \p vars. 1123 */ 1124 void unconstrain(const Variables_Set& vars); 1125 1126 /*! \brief 1127 Assigns to \p *this the intersection of \p *this and \p y. 1128 1129 \exception std::invalid_argument 1130 Thrown if \p *this and \p y are dimension-incompatible. 1131 */ 1132 void intersection_assign(const Grid& y); 1133 1134 /*! \brief 1135 Assigns to \p *this the least upper bound of \p *this and \p y. 1136 1137 \exception std::invalid_argument 1138 Thrown if \p *this and \p y are dimension-incompatible. 1139 */ 1140 void upper_bound_assign(const Grid& y); 1141 1142 /*! \brief 1143 If the upper bound of \p *this and \p y is exact it is assigned to \p 1144 *this and <CODE>true</CODE> is returned, otherwise 1145 <CODE>false</CODE> is returned. 1146 1147 \exception std::invalid_argument 1148 Thrown if \p *this and \p y are dimension-incompatible. 1149 */ 1150 bool upper_bound_assign_if_exact(const Grid& y); 1151 1152 /*! \brief 1153 Assigns to \p *this the \ref Convex_Polyhedral_Difference "grid-difference" 1154 of \p *this and \p y. 1155 1156 The grid difference between grids x and y is the smallest grid 1157 containing all the points from x and y that are only in x. 1158 1159 \exception std::invalid_argument 1160 Thrown if \p *this and \p y are dimension-incompatible. 1161 */ 1162 void difference_assign(const Grid& y); 1163 1164 /*! \brief 1165 Assigns to \p *this a \ref Meet_Preserving_Simplification 1166 "meet-preserving simplification" of \p *this with respect to \p y. 1167 If \c false is returned, then the intersection is empty. 1168 1169 \exception std::invalid_argument 1170 Thrown if \p *this and \p y are topology-incompatible or 1171 dimension-incompatible. 1172 */ 1173 bool simplify_using_context_assign(const Grid& y); 1174 1175 /*! \brief 1176 Assigns to \p *this the \ref Grid_Affine_Transformation 1177 "affine image" of \p 1178 *this under the function mapping variable \p var to the affine 1179 expression specified by \p expr and \p denominator. 1180 1181 \param var 1182 The variable to which the affine expression is assigned; 1183 1184 \param expr 1185 The numerator of the affine expression; 1186 1187 \param denominator 1188 The denominator of the affine expression (optional argument with 1189 default value 1). 1190 1191 \exception std::invalid_argument 1192 Thrown if \p denominator is zero or if \p expr and \p *this are 1193 dimension-incompatible or if \p var is not a space dimension of 1194 \p *this. 1195 1196 \if Include_Implementation_Details 1197 1198 When considering the generators of a grid, the 1199 affine transformation 1200 \f[ 1201 \frac{\sum_{i=0}^{n-1} a_i x_i + b}{\mathrm{denominator}} 1202 \f] 1203 is assigned to \p var where \p expr is 1204 \f$\sum_{i=0}^{n-1} a_i x_i + b\f$ 1205 (\f$b\f$ is the inhomogeneous term). 1206 1207 If congruences are up-to-date, it uses the specialized function 1208 affine_preimage() (for the system of congruences) 1209 and inverse transformation to reach the same result. 1210 To obtain the inverse transformation we use the following observation. 1211 1212 Observation: 1213 -# The affine transformation is invertible if the coefficient 1214 of \p var in this transformation (i.e., \f$a_\mathrm{var}\f$) 1215 is different from zero. 1216 -# If the transformation is invertible, then we can write 1217 \f[ 1218 \mathrm{denominator} * {x'}_\mathrm{var} 1219 = \sum_{i = 0}^{n - 1} a_i x_i + b 1220 = a_\mathrm{var} x_\mathrm{var} 1221 + \sum_{i \neq var} a_i x_i + b, 1222 \f] 1223 so that the inverse transformation is 1224 \f[ 1225 a_\mathrm{var} x_\mathrm{var} 1226 = \mathrm{denominator} * {x'}_\mathrm{var} 1227 - \sum_{i \neq j} a_i x_i - b. 1228 \f] 1229 1230 Then, if the transformation is invertible, all the entities that 1231 were up-to-date remain up-to-date. Otherwise only generators remain 1232 up-to-date. 1233 1234 \endif 1235 */ 1236 void affine_image(Variable var, 1237 const Linear_Expression& expr, 1238 Coefficient_traits::const_reference denominator 1239 = Coefficient_one()); 1240 1241 /*! \brief 1242 Assigns to \p *this the \ref Grid_Affine_Transformation 1243 "affine preimage" of 1244 \p *this under the function mapping variable \p var to the affine 1245 expression specified by \p expr and \p denominator. 1246 1247 \param var 1248 The variable to which the affine expression is substituted; 1249 1250 \param expr 1251 The numerator of the affine expression; 1252 1253 \param denominator 1254 The denominator of the affine expression (optional argument with 1255 default value 1). 1256 1257 \exception std::invalid_argument 1258 Thrown if \p denominator is zero or if \p expr and \p *this are 1259 dimension-incompatible or if \p var is not a space dimension of \p *this. 1260 1261 \if Include_Implementation_Details 1262 1263 When considering congruences of a grid, the affine transformation 1264 \f[ 1265 \frac{\sum_{i=0}^{n-1} a_i x_i + b}{denominator}, 1266 \f] 1267 is assigned to \p var where \p expr is 1268 \f$\sum_{i=0}^{n-1} a_i x_i + b\f$ 1269 (\f$b\f$ is the inhomogeneous term). 1270 1271 If generators are up-to-date, then the specialized function 1272 affine_image() is used (for the system of generators) 1273 and inverse transformation to reach the same result. 1274 To obtain the inverse transformation, we use the following observation. 1275 1276 Observation: 1277 -# The affine transformation is invertible if the coefficient 1278 of \p var in this transformation (i.e. \f$a_\mathrm{var}\f$) 1279 is different from zero. 1280 -# If the transformation is invertible, then we can write 1281 \f[ 1282 \mathrm{denominator} * {x'}_\mathrm{var} 1283 = \sum_{i = 0}^{n - 1} a_i x_i + b 1284 = a_\mathrm{var} x_\mathrm{var} 1285 + \sum_{i \neq \mathrm{var}} a_i x_i + b, 1286 \f], 1287 the inverse transformation is 1288 \f[ 1289 a_\mathrm{var} x_\mathrm{var} 1290 = \mathrm{denominator} * {x'}_\mathrm{var} 1291 - \sum_{i \neq j} a_i x_i - b. 1292 \f]. 1293 1294 Then, if the transformation is invertible, all the entities that 1295 were up-to-date remain up-to-date. Otherwise only congruences remain 1296 up-to-date. 1297 1298 \endif 1299 */ 1300 void affine_preimage(Variable var, 1301 const Linear_Expression& expr, 1302 Coefficient_traits::const_reference denominator 1303 = Coefficient_one()); 1304 1305 /*! \brief 1306 Assigns to \p *this the image of \p *this with respect to 1307 the \ref Grid_Generalized_Image "generalized affine relation" 1308 \f$\mathrm{var}' = \frac{\mathrm{expr}}{\mathrm{denominator}} 1309 \pmod{\mathrm{modulus}}\f$. 1310 1311 \param var 1312 The left hand side variable of the generalized affine relation; 1313 1314 \param relsym 1315 The relation symbol where EQUAL is the symbol for a congruence 1316 relation; 1317 1318 \param expr 1319 The numerator of the right hand side affine expression; 1320 1321 \param denominator 1322 The denominator of the right hand side affine expression. 1323 Optional argument with an automatic value of one; 1324 1325 \param modulus 1326 The modulus of the congruence lhs %= rhs. A modulus of zero 1327 indicates lhs == rhs. Optional argument with an automatic value 1328 of zero. 1329 1330 \exception std::invalid_argument 1331 Thrown if \p denominator is zero or if \p expr and \p *this are 1332 dimension-incompatible or if \p var is not a space dimension of \p 1333 *this. 1334 */ 1335 void 1336 generalized_affine_image(Variable var, 1337 Relation_Symbol relsym, 1338 const Linear_Expression& expr, 1339 Coefficient_traits::const_reference denominator 1340 = Coefficient_one(), 1341 Coefficient_traits::const_reference modulus 1342 = Coefficient_zero()); 1343 1344 /*! \brief 1345 Assigns to \p *this the preimage of \p *this with respect to the 1346 \ref Grid_Generalized_Image "generalized affine relation" 1347 \f$\mathrm{var}' = \frac{\mathrm{expr}}{\mathrm{denominator}} 1348 \pmod{\mathrm{modulus}}\f$. 1349 1350 \param var 1351 The left hand side variable of the generalized affine relation; 1352 1353 \param relsym 1354 The relation symbol where EQUAL is the symbol for a congruence 1355 relation; 1356 1357 \param expr 1358 The numerator of the right hand side affine expression; 1359 1360 \param denominator 1361 The denominator of the right hand side affine expression. 1362 Optional argument with an automatic value of one; 1363 1364 \param modulus 1365 The modulus of the congruence lhs %= rhs. A modulus of zero 1366 indicates lhs == rhs. Optional argument with an automatic value 1367 of zero. 1368 1369 \exception std::invalid_argument 1370 Thrown if \p denominator is zero or if \p expr and \p *this are 1371 dimension-incompatible or if \p var is not a space dimension of \p 1372 *this. 1373 */ 1374 void 1375 generalized_affine_preimage(Variable var, 1376 Relation_Symbol relsym, 1377 const Linear_Expression& expr, 1378 Coefficient_traits::const_reference denominator 1379 = Coefficient_one(), 1380 Coefficient_traits::const_reference modulus 1381 = Coefficient_zero()); 1382 1383 /*! \brief 1384 Assigns to \p *this the image of \p *this with respect to 1385 the \ref Grid_Generalized_Image "generalized affine relation" 1386 \f$\mathrm{lhs}' = \mathrm{rhs} \pmod{\mathrm{modulus}}\f$. 1387 1388 \param lhs 1389 The left hand side affine expression. 1390 1391 \param relsym 1392 The relation symbol where EQUAL is the symbol for a congruence 1393 relation; 1394 1395 \param rhs 1396 The right hand side affine expression. 1397 1398 \param modulus 1399 The modulus of the congruence lhs %= rhs. A modulus of zero 1400 indicates lhs == rhs. Optional argument with an automatic value 1401 of zero. 1402 1403 \exception std::invalid_argument 1404 Thrown if \p *this is dimension-incompatible with \p lhs or \p 1405 rhs. 1406 */ 1407 void 1408 generalized_affine_image(const Linear_Expression& lhs, 1409 Relation_Symbol relsym, 1410 const Linear_Expression& rhs, 1411 Coefficient_traits::const_reference modulus 1412 = Coefficient_zero()); 1413 1414 /*! \brief 1415 Assigns to \p *this the preimage of \p *this with respect to the 1416 \ref Grid_Generalized_Image "generalized affine relation" 1417 \f$\mathrm{lhs}' = \mathrm{rhs} \pmod{\mathrm{modulus}}\f$. 1418 1419 \param lhs 1420 The left hand side affine expression; 1421 1422 \param relsym 1423 The relation symbol where EQUAL is the symbol for a congruence 1424 relation; 1425 1426 \param rhs 1427 The right hand side affine expression; 1428 1429 \param modulus 1430 The modulus of the congruence lhs %= rhs. A modulus of zero 1431 indicates lhs == rhs. Optional argument with an automatic value 1432 of zero. 1433 1434 \exception std::invalid_argument 1435 Thrown if \p *this is dimension-incompatible with \p lhs or \p 1436 rhs. 1437 */ 1438 void 1439 generalized_affine_preimage(const Linear_Expression& lhs, 1440 Relation_Symbol relsym, 1441 const Linear_Expression& rhs, 1442 Coefficient_traits::const_reference modulus 1443 = Coefficient_zero()); 1444 1445 /*! 1446 \brief 1447 Assigns to \p *this the image of \p *this with respect to the 1448 \ref Single_Update_Bounded_Affine_Relations "bounded affine relation" 1449 \f$\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} 1450 \leq \mathrm{var}' 1451 \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}\f$. 1452 1453 \param var 1454 The variable updated by the affine relation; 1455 1456 \param lb_expr 1457 The numerator of the lower bounding affine expression; 1458 1459 \param ub_expr 1460 The numerator of the upper bounding affine expression; 1461 1462 \param denominator 1463 The (common) denominator for the lower and upper bounding 1464 affine expressions (optional argument with default value 1). 1465 1466 \exception std::invalid_argument 1467 Thrown if \p denominator is zero or if \p lb_expr (resp., \p ub_expr) 1468 and \p *this are dimension-incompatible or if \p var is not a space 1469 dimension of \p *this. 1470 */ 1471 void bounded_affine_image(Variable var, 1472 const Linear_Expression& lb_expr, 1473 const Linear_Expression& ub_expr, 1474 Coefficient_traits::const_reference denominator 1475 = Coefficient_one()); 1476 1477 /*! 1478 \brief 1479 Assigns to \p *this the preimage of \p *this with respect to the 1480 \ref Single_Update_Bounded_Affine_Relations "bounded affine relation" 1481 \f$\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} 1482 \leq \mathrm{var}' 1483 \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}\f$. 1484 1485 \param var 1486 The variable updated by the affine relation; 1487 1488 \param lb_expr 1489 The numerator of the lower bounding affine expression; 1490 1491 \param ub_expr 1492 The numerator of the upper bounding affine expression; 1493 1494 \param denominator 1495 The (common) denominator for the lower and upper bounding 1496 affine expressions (optional argument with default value 1). 1497 1498 \exception std::invalid_argument 1499 Thrown if \p denominator is zero or if \p lb_expr (resp., \p ub_expr) 1500 and \p *this are dimension-incompatible or if \p var is not a space 1501 dimension of \p *this. 1502 */ 1503 void bounded_affine_preimage(Variable var, 1504 const Linear_Expression& lb_expr, 1505 const Linear_Expression& ub_expr, 1506 Coefficient_traits::const_reference denominator 1507 = Coefficient_one()); 1508 1509 /*! \brief 1510 Assigns to \p *this the result of computing the \ref Grid_Time_Elapse 1511 "time-elapse" between \p *this and \p y. 1512 1513 \exception std::invalid_argument 1514 Thrown if \p *this and \p y are dimension-incompatible. 1515 */ 1516 void time_elapse_assign(const Grid& y); 1517 1518 /*! \brief 1519 \ref Wrapping_Operator "Wraps" the specified dimensions of the 1520 vector space. 1521 1522 \param vars 1523 The set of Variable objects corresponding to the space dimensions 1524 to be wrapped. 1525 1526 \param w 1527 The width of the bounded integer type corresponding to 1528 all the dimensions to be wrapped. 1529 1530 \param r 1531 The representation of the bounded integer type corresponding to 1532 all the dimensions to be wrapped. 1533 1534 \param o 1535 The overflow behavior of the bounded integer type corresponding to 1536 all the dimensions to be wrapped. 1537 1538 \param cs_p 1539 Possibly null pointer to a constraint system. 1540 This argument is for compatibility with wrap_assign() 1541 for the other domains and only checked for dimension-compatibility. 1542 1543 \param complexity_threshold 1544 A precision parameter of the \ref Wrapping_Operator "wrapping operator". 1545 This argument is for compatibility with wrap_assign() 1546 for the other domains and is ignored. 1547 1548 \param wrap_individually 1549 <CODE>true</CODE> if the dimensions should be wrapped individually. 1550 As wrapping dimensions collectively does not improve the precision, 1551 this argument is ignored. 1552 1553 \exception std::invalid_argument 1554 Thrown if \p *this is dimension-incompatible with one of the 1555 Variable objects contained in \p vars or with <CODE>*cs_p</CODE>. 1556 1557 \warning 1558 It is assumed that variables in \p Vars represent integers. Thus, 1559 where the extra cost is negligible, the integrality of these 1560 variables is enforced; possibly causing a non-integral grid to 1561 become empty. 1562 */ 1563 void wrap_assign(const Variables_Set& vars, 1564 Bounded_Integer_Type_Width w, 1565 Bounded_Integer_Type_Representation r, 1566 Bounded_Integer_Type_Overflow o, 1567 const Constraint_System* cs_p = 0, 1568 unsigned complexity_threshold = 16, 1569 bool wrap_individually = true); 1570 1571 /*! \brief 1572 Possibly tightens \p *this by dropping all points with non-integer 1573 coordinates. 1574 1575 \param complexity 1576 This argument is ignored as the algorithm used has polynomial 1577 complexity. 1578 */ 1579 void drop_some_non_integer_points(Complexity_Class complexity 1580 = ANY_COMPLEXITY); 1581 1582 /*! \brief 1583 Possibly tightens \p *this by dropping all points with non-integer 1584 coordinates for the space dimensions corresponding to \p vars. 1585 1586 \param vars 1587 Points with non-integer coordinates for these variables/space-dimensions 1588 can be discarded. 1589 1590 \param complexity 1591 This argument is ignored as the algorithm used has polynomial 1592 complexity. 1593 */ 1594 void drop_some_non_integer_points(const Variables_Set& vars, 1595 Complexity_Class complexity 1596 = ANY_COMPLEXITY); 1597 1598 //! Assigns to \p *this its topological closure. 1599 void topological_closure_assign(); 1600 1601 /*! \brief 1602 Assigns to \p *this the result of computing the \ref Grid_Widening 1603 "Grid widening" between \p *this and \p y using congruence systems. 1604 1605 \param y 1606 A grid that <EM>must</EM> be contained in \p *this; 1607 1608 \param tp 1609 An optional pointer to an unsigned variable storing the number of 1610 available tokens (to be used when applying the 1611 \ref Grid_Widening_with_Tokens "widening with tokens" delay technique). 1612 1613 \exception std::invalid_argument 1614 Thrown if \p *this and \p y are dimension-incompatible. 1615 */ 1616 void congruence_widening_assign(const Grid& y, unsigned* tp = NULL); 1617 1618 /*! \brief 1619 Assigns to \p *this the result of computing the \ref Grid_Widening 1620 "Grid widening" between \p *this and \p y using generator systems. 1621 1622 \param y 1623 A grid that <EM>must</EM> be contained in \p *this; 1624 1625 \param tp 1626 An optional pointer to an unsigned variable storing the number of 1627 available tokens (to be used when applying the 1628 \ref Grid_Widening_with_Tokens "widening with tokens" delay technique). 1629 1630 \exception std::invalid_argument 1631 Thrown if \p *this and \p y are dimension-incompatible. 1632 */ 1633 void generator_widening_assign(const Grid& y, unsigned* tp = NULL); 1634 1635 /*! \brief 1636 Assigns to \p *this the result of computing the \ref Grid_Widening 1637 "Grid widening" between \p *this and \p y. 1638 1639 This widening uses either the congruence or generator systems 1640 depending on which of the systems describing x and y 1641 are up to date and minimized. 1642 1643 \param y 1644 A grid that <EM>must</EM> be contained in \p *this; 1645 1646 \param tp 1647 An optional pointer to an unsigned variable storing the number of 1648 available tokens (to be used when applying the 1649 \ref Grid_Widening_with_Tokens "widening with tokens" delay technique). 1650 1651 \exception std::invalid_argument 1652 Thrown if \p *this and \p y are dimension-incompatible. 1653 */ 1654 void widening_assign(const Grid& y, unsigned* tp = NULL); 1655 1656 /*! \brief 1657 Improves the result of the congruence variant of 1658 \ref Grid_Widening "Grid widening" computation by also enforcing 1659 those congruences in \p cgs that are satisfied by all the points 1660 of \p *this. 1661 1662 \param y 1663 A grid that <EM>must</EM> be contained in \p *this; 1664 1665 \param cgs 1666 The system of congruences used to improve the widened grid; 1667 1668 \param tp 1669 An optional pointer to an unsigned variable storing the number of 1670 available tokens (to be used when applying the 1671 \ref Grid_Widening_with_Tokens "widening with tokens" delay technique). 1672 1673 \exception std::invalid_argument 1674 Thrown if \p *this, \p y and \p cgs are dimension-incompatible. 1675 */ 1676 void limited_congruence_extrapolation_assign(const Grid& y, 1677 const Congruence_System& cgs, 1678 unsigned* tp = NULL); 1679 1680 /*! \brief 1681 Improves the result of the generator variant of the 1682 \ref Grid_Widening "Grid widening" 1683 computation by also enforcing those congruences in \p cgs that are 1684 satisfied by all the points of \p *this. 1685 1686 \param y 1687 A grid that <EM>must</EM> be contained in \p *this; 1688 1689 \param cgs 1690 The system of congruences used to improve the widened grid; 1691 1692 \param tp 1693 An optional pointer to an unsigned variable storing the number of 1694 available tokens (to be used when applying the 1695 \ref Grid_Widening_with_Tokens "widening with tokens" delay technique). 1696 1697 \exception std::invalid_argument 1698 Thrown if \p *this, \p y and \p cgs are dimension-incompatible. 1699 */ 1700 void limited_generator_extrapolation_assign(const Grid& y, 1701 const Congruence_System& cgs, 1702 unsigned* tp = NULL); 1703 1704 /*! \brief 1705 Improves the result of the \ref Grid_Widening "Grid widening" 1706 computation by also enforcing those congruences in \p cgs that are 1707 satisfied by all the points of \p *this. 1708 1709 \param y 1710 A grid that <EM>must</EM> be contained in \p *this; 1711 1712 \param cgs 1713 The system of congruences used to improve the widened grid; 1714 1715 \param tp 1716 An optional pointer to an unsigned variable storing the number of 1717 available tokens (to be used when applying the 1718 \ref Grid_Widening_with_Tokens "widening with tokens" delay technique). 1719 1720 \exception std::invalid_argument 1721 Thrown if \p *this, \p y and \p cgs are dimension-incompatible. 1722 */ 1723 void limited_extrapolation_assign(const Grid& y, 1724 const Congruence_System& cgs, 1725 unsigned* tp = NULL); 1726 1727 //@} // Space Dimension Preserving Member Functions that May Modify [...] 1728 1729 //! \name Member Functions that May Modify the Dimension of the Vector Space 1730 //@{ 1731 1732 /*! \brief 1733 \ref Adding_New_Dimensions_to_the_Vector_Space "Adds" 1734 \p m new space dimensions and embeds the old grid in the new 1735 vector space. 1736 1737 \param m 1738 The number of dimensions to add. 1739 1740 \exception std::length_error 1741 Thrown if adding \p m new space dimensions would cause the vector 1742 space to exceed dimension <CODE>max_space_dimension()</CODE>. 1743 1744 The new space dimensions will be those having the highest indexes 1745 in the new grid, which is characterized by a system of congruences 1746 in which the variables which are the new dimensions can have any 1747 value. For instance, when starting from the grid \f$\cL \sseq 1748 \Rset^2\f$ and adding a third space dimension, the result will be 1749 the grid 1750 \f[ 1751 \bigl\{\, 1752 (x, y, z)^\transpose \in \Rset^3 1753 \bigm| 1754 (x, y)^\transpose \in \cL 1755 \,\bigr\}. 1756 \f] 1757 */ 1758 void add_space_dimensions_and_embed(dimension_type m); 1759 1760 /*! \brief 1761 \ref Adding_New_Dimensions_to_the_Vector_Space "Adds" 1762 \p m new space dimensions to the grid and does not embed it 1763 in the new vector space. 1764 1765 \param m 1766 The number of space dimensions to add. 1767 1768 \exception std::length_error 1769 Thrown if adding \p m new space dimensions would cause the 1770 vector space to exceed dimension <CODE>max_space_dimension()</CODE>. 1771 1772 The new space dimensions will be those having the highest indexes 1773 in the new grid, which is characterized by a system of congruences 1774 in which the variables running through the new dimensions are all 1775 constrained to be equal to 0. For instance, when starting from 1776 the grid \f$\cL \sseq \Rset^2\f$ and adding a third space 1777 dimension, the result will be the grid 1778 \f[ 1779 \bigl\{\, 1780 (x, y, 0)^\transpose \in \Rset^3 1781 \bigm| 1782 (x, y)^\transpose \in \cL 1783 \,\bigr\}. 1784 \f] 1785 */ 1786 void add_space_dimensions_and_project(dimension_type m); 1787 1788 /*! \brief 1789 Assigns to \p *this the \ref Concatenating_Polyhedra "concatenation" of 1790 \p *this and \p y, taken in this order. 1791 1792 \exception std::length_error 1793 Thrown if the concatenation would cause the vector space 1794 to exceed dimension <CODE>max_space_dimension()</CODE>. 1795 */ 1796 void concatenate_assign(const Grid& y); 1797 1798 //! Removes all the specified dimensions from the vector space. 1799 /*! 1800 \param vars 1801 The set of Variable objects corresponding to the space dimensions 1802 to be removed. 1803 1804 \exception std::invalid_argument 1805 Thrown if \p *this is dimension-incompatible with one of the 1806 Variable objects contained in \p vars. 1807 */ 1808 void remove_space_dimensions(const Variables_Set& vars); 1809 1810 /*! \brief 1811 Removes the higher dimensions of the vector space so that the 1812 resulting space will have \ref Removing_Dimensions_from_the_Vector_Space 1813 "dimension \p new_dimension." 1814 1815 \exception std::invalid_argument 1816 Thrown if \p new_dimensions is greater than the space dimension of 1817 \p *this. 1818 */ 1819 void remove_higher_space_dimensions(dimension_type new_dimension); 1820 1821 /*! \brief 1822 Remaps the dimensions of the vector space according to 1823 a \ref Mapping_the_Dimensions_of_the_Vector_Space "partial function". 1824 1825 If \p pfunc maps only some of the dimensions of \p *this then the 1826 rest will be projected away. 1827 1828 If the highest dimension mapped to by \p pfunc is higher than the 1829 highest dimension in \p *this then the number of dimensions in \p 1830 *this will be increased to the highest dimension mapped to by \p 1831 pfunc. 1832 1833 \param pfunc 1834 The partial function specifying the destiny of each space 1835 dimension. 1836 1837 The template type parameter Partial_Function must provide 1838 the following methods. 1839 \code 1840 bool has_empty_codomain() const 1841 \endcode 1842 returns <CODE>true</CODE> if and only if the represented partial 1843 function has an empty codomain (i.e., it is always undefined). 1844 The <CODE>has_empty_codomain()</CODE> method will always be called 1845 before the methods below. However, if 1846 <CODE>has_empty_codomain()</CODE> returns <CODE>true</CODE>, none 1847 of the functions below will be called. 1848 \code 1849 dimension_type max_in_codomain() const 1850 \endcode 1851 returns the maximum value that belongs to the codomain of the 1852 partial function. 1853 The <CODE>max_in_codomain()</CODE> method is called at most once. 1854 \code 1855 bool maps(dimension_type i, dimension_type& j) const 1856 \endcode 1857 Let \f$f\f$ be the represented function and \f$k\f$ be the value 1858 of \p i. If \f$f\f$ is defined in \f$k\f$, then \f$f(k)\f$ is 1859 assigned to \p j and <CODE>true</CODE> is returned. If \f$f\f$ is 1860 undefined in \f$k\f$, then <CODE>false</CODE> is returned. 1861 This method is called at most \f$n\f$ times, where \f$n\f$ is the 1862 dimension of the vector space enclosing the grid. 1863 1864 The result is undefined if \p pfunc does not encode a partial 1865 function with the properties described in the 1866 \ref Mapping_the_Dimensions_of_the_Vector_Space "specification of the mapping operator". 1867 */ 1868 template <typename Partial_Function> 1869 void map_space_dimensions(const Partial_Function& pfunc); 1870 1871 //! Creates \p m copies of the space dimension corresponding to \p var. 1872 /*! 1873 \param var 1874 The variable corresponding to the space dimension to be replicated; 1875 1876 \param m 1877 The number of replicas to be created. 1878 1879 \exception std::invalid_argument 1880 Thrown if \p var does not correspond to a dimension of the vector 1881 space. 1882 1883 \exception std::length_error 1884 Thrown if adding \p m new space dimensions would cause the vector 1885 space to exceed dimension <CODE>max_space_dimension()</CODE>. 1886 1887 If \p *this has space dimension \f$n\f$, with \f$n > 0\f$, 1888 and <CODE>var</CODE> has space dimension \f$k \leq n\f$, 1889 then the \f$k\f$-th space dimension is 1890 \ref Expanding_One_Dimension_of_the_Vector_Space_to_Multiple_Dimensions 1891 "expanded" to \p m new space dimensions 1892 \f$n\f$, \f$n+1\f$, \f$\dots\f$, \f$n+m-1\f$. 1893 */ 1894 void expand_space_dimension(Variable var, dimension_type m); 1895 1896 //! Folds the space dimensions in \p vars into \p dest. 1897 /*! 1898 \param vars 1899 The set of Variable objects corresponding to the space dimensions 1900 to be folded; 1901 1902 \param dest 1903 The variable corresponding to the space dimension that is the 1904 destination of the folding operation. 1905 1906 \exception std::invalid_argument 1907 Thrown if \p *this is dimension-incompatible with \p dest or with 1908 one of the Variable objects contained in \p vars. Also 1909 thrown if \p dest is contained in \p vars. 1910 1911 If \p *this has space dimension \f$n\f$, with \f$n > 0\f$, 1912 <CODE>dest</CODE> has space dimension \f$k \leq n\f$, 1913 \p vars is a set of variables whose maximum space dimension 1914 is also less than or equal to \f$n\f$, and \p dest is not a member 1915 of \p vars, then the space dimensions corresponding to 1916 variables in \p vars are 1917 \ref Folding_Multiple_Dimensions_of_the_Vector_Space_into_One_Dimension "folded" 1918 into the \f$k\f$-th space dimension. 1919 */ 1920 void fold_space_dimensions(const Variables_Set& vars, Variable dest); 1921 1922 //@} // Member Functions that May Modify the Dimension of the Vector Space 1923 1924 friend bool operator==(const Grid& x, const Grid& y); 1925 1926 friend class Parma_Polyhedra_Library::Grid_Certificate; 1927 1928 template <typename Interval> friend class Parma_Polyhedra_Library::Box; 1929 1930 //! \name Miscellaneous Member Functions 1931 //@{ 1932 1933 //! Destructor. 1934 ~Grid(); 1935 1936 /*! \brief 1937 Swaps \p *this with grid \p y. (\p *this and \p y can be 1938 dimension-incompatible.) 1939 */ 1940 void m_swap(Grid& y); 1941 1942 PPL_OUTPUT_DECLARATIONS 1943 1944 /*! \brief 1945 Loads from \p s an ASCII representation (as produced by 1946 ascii_dump(std::ostream&) const) and sets \p *this accordingly. 1947 Returns <CODE>true</CODE> if successful, <CODE>false</CODE> otherwise. 1948 */ 1949 bool ascii_load(std::istream& s); 1950 1951 //! Returns the total size in bytes of the memory occupied by \p *this. 1952 memory_size_type total_memory_in_bytes() const; 1953 1954 //! Returns the size in bytes of the memory managed by \p *this. 1955 memory_size_type external_memory_in_bytes() const; 1956 1957 /*! \brief 1958 Returns a 32-bit hash code for \p *this. 1959 1960 If \p x and \p y are such that <CODE>x == y</CODE>, 1961 then <CODE>x.hash_code() == y.hash_code()</CODE>. 1962 */ 1963 int32_t hash_code() const; 1964 1965 //@} // Miscellaneous Member Functions 1966 1967 private: 1968 1969 //! The system of congruences. 1970 Congruence_System con_sys; 1971 1972 //! The system of generators. 1973 Grid_Generator_System gen_sys; 1974 1975 #define PPL_IN_Grid_CLASS 1976 #include "Grid_Status_idefs.hh" 1977 #undef PPL_IN_Grid_CLASS 1978 1979 //! The status flags to keep track of the grid's internal state. 1980 Status status; 1981 1982 //! The number of dimensions of the enclosing vector space. 1983 dimension_type space_dim; 1984 1985 enum Dimension_Kind { 1986 PARAMETER = 0, 1987 LINE = 1, 1988 GEN_VIRTUAL = 2, 1989 PROPER_CONGRUENCE = PARAMETER, 1990 CON_VIRTUAL = LINE, 1991 EQUALITY = GEN_VIRTUAL 1992 }; 1993 1994 typedef std::vector<Dimension_Kind> Dimension_Kinds; 1995 1996 // The type of row associated with each dimension. If the virtual 1997 // rows existed then the reduced systems would be square and upper 1998 // or lower triangular, and the rows in each would have the types 1999 // given in this vector. As the congruence system is reduced to an 2000 // upside-down lower triangular form the ordering of the congruence 2001 // types is last to first. 2002 Dimension_Kinds dim_kinds; 2003 2004 //! Builds a grid universe or empty grid. 2005 /*! 2006 \param num_dimensions 2007 The number of dimensions of the vector space enclosing the grid; 2008 2009 \param kind 2010 specifies whether the universe or the empty grid has to be built. 2011 */ 2012 void construct(dimension_type num_dimensions, Degenerate_Element kind); 2013 2014 //! Builds a grid from a system of congruences. 2015 /*! 2016 The grid inherits the space dimension of the congruence system. 2017 2018 \param cgs 2019 The system of congruences defining the grid. Its data-structures 2020 may be recycled to build the grid. 2021 */ 2022 void construct(Congruence_System& cgs); 2023 2024 //! Builds a grid from a system of grid generators. 2025 /*! 2026 The grid inherits the space dimension of the generator system. 2027 2028 \param ggs 2029 The system of grid generators defining the grid. Its data-structures 2030 may be recycled to build the grid. 2031 */ 2032 void construct(Grid_Generator_System& ggs); 2033 2034 //! \name Private Verifiers: Verify if Individual Flags are Set 2035 //@{ 2036 2037 //! Returns <CODE>true</CODE> if the grid is known to be empty. 2038 /*! 2039 The return value <CODE>false</CODE> does not necessarily 2040 implies that \p *this is non-empty. 2041 */ 2042 bool marked_empty() const; 2043 2044 //! Returns <CODE>true</CODE> if the system of congruences is up-to-date. 2045 bool congruences_are_up_to_date() const; 2046 2047 //! Returns <CODE>true</CODE> if the system of generators is up-to-date. 2048 bool generators_are_up_to_date() const; 2049 2050 //! Returns <CODE>true</CODE> if the system of congruences is minimized. 2051 bool congruences_are_minimized() const; 2052 2053 //! Returns <CODE>true</CODE> if the system of generators is minimized. 2054 bool generators_are_minimized() const; 2055 2056 //@} // Private Verifiers: Verify if Individual Flags are Set 2057 2058 //! \name State Flag Setters: Set Only the Specified Flags 2059 //@{ 2060 2061 /*! \brief 2062 Sets \p status to express that the grid is the universe 2063 0-dimension vector space, clearing all corresponding matrices. 2064 */ 2065 void set_zero_dim_univ(); 2066 2067 /*! \brief 2068 Sets \p status to express that the grid is empty, clearing all 2069 corresponding matrices. 2070 */ 2071 void set_empty(); 2072 2073 //! Sets \p status to express that congruences are up-to-date. 2074 void set_congruences_up_to_date(); 2075 2076 //! Sets \p status to express that generators are up-to-date. 2077 void set_generators_up_to_date(); 2078 2079 //! Sets \p status to express that congruences are minimized. 2080 void set_congruences_minimized(); 2081 2082 //! Sets \p status to express that generators are minimized. 2083 void set_generators_minimized(); 2084 2085 //@} // State Flag Setters: Set Only the Specified Flags 2086 2087 //! \name State Flag Cleaners: Clear Only the Specified Flag 2088 //@{ 2089 2090 //! Clears the \p status flag indicating that the grid is empty. 2091 void clear_empty(); 2092 2093 //! Sets \p status to express that congruences are out of date. 2094 void clear_congruences_up_to_date(); 2095 2096 //! Sets \p status to express that generators are out of date. 2097 void clear_generators_up_to_date(); 2098 2099 //! Sets \p status to express that congruences are no longer minimized. 2100 void clear_congruences_minimized(); 2101 2102 //! Sets \p status to express that generators are no longer minimized. 2103 void clear_generators_minimized(); 2104 2105 //@} // State Flag Cleaners: Clear Only the Specified Flag 2106 2107 //! \name Updating Matrices 2108 //@{ 2109 2110 //! Updates and minimizes the congruences from the generators. 2111 void update_congruences() const; 2112 2113 //! Updates and minimizes the generators from the congruences. 2114 /*! 2115 \return 2116 <CODE>false</CODE> if and only if \p *this turns out to be an 2117 empty grid. 2118 2119 It is illegal to call this method when the Status field already 2120 declares the grid to be empty. 2121 */ 2122 bool update_generators() const; 2123 2124 //@} // Updating Matrices 2125 2126 //! \name Minimization of Descriptions 2127 //@{ 2128 2129 //! Minimizes both the congruences and the generators. 2130 /*! 2131 \return 2132 <CODE>false</CODE> if and only if \p *this turns out to be an 2133 empty grid. 2134 2135 Minimization is performed on each system only if the minimized 2136 Status field is clear. 2137 */ 2138 bool minimize() const; 2139 2140 //@} // Minimization of Descriptions 2141 2142 enum Three_Valued_Boolean { 2143 TVB_TRUE, 2144 TVB_FALSE, 2145 TVB_DONT_KNOW 2146 }; 2147 2148 //! Polynomial but incomplete equivalence test between grids. 2149 Three_Valued_Boolean quick_equivalence_test(const Grid& y) const; 2150 2151 //! Returns <CODE>true</CODE> if and only if \p *this is included in \p y. 2152 bool is_included_in(const Grid& y) const; 2153 2154 //! Checks if and how \p expr is bounded in \p *this. 2155 /*! 2156 Returns <CODE>true</CODE> if and only if \p from_above is 2157 <CODE>true</CODE> and \p expr is bounded from above in \p *this, 2158 or \p from_above is <CODE>false</CODE> and \p expr is bounded 2159 from below in \p *this. 2160 2161 \param expr 2162 The linear expression to test; 2163 2164 \param method_call 2165 The call description of the public parent method, for example 2166 "bounded_from_above(e)". Passed to throw_dimension_incompatible, 2167 as the first argument. 2168 2169 \exception std::invalid_argument 2170 Thrown if \p expr and \p *this are dimension-incompatible. 2171 */ 2172 bool bounds(const Linear_Expression& expr, const char* method_call) const; 2173 2174 //! Maximizes or minimizes \p expr subject to \p *this. 2175 /*! 2176 \param expr 2177 The linear expression to be maximized or minimized subject to \p 2178 *this; 2179 2180 \param method_call 2181 The call description of the public parent method, for example 2182 "maximize(e)". Passed to throw_dimension_incompatible, as the 2183 first argument; 2184 2185 \param ext_n 2186 The numerator of the extremum value; 2187 2188 \param ext_d 2189 The denominator of the extremum value; 2190 2191 \param included 2192 <CODE>true</CODE> if and only if the extremum of \p expr in \p 2193 *this can actually be reached (which is always the case); 2194 2195 \param point 2196 When maximization or minimization succeeds, will be assigned the 2197 point where \p expr reaches the extremum value. 2198 2199 \exception std::invalid_argument 2200 Thrown if \p expr and \p *this are dimension-incompatible. 2201 2202 If \p *this is empty or \p expr is not bounded in the appropriate 2203 direction, <CODE>false</CODE> is returned and \p ext_n, \p ext_d, 2204 \p included and \p point are left untouched. 2205 */ 2206 bool max_min(const Linear_Expression& expr, 2207 const char* method_call, 2208 Coefficient& ext_n, Coefficient& ext_d, bool& included, 2209 Generator* point = NULL) const; 2210 2211 /*! \brief 2212 Returns <CODE>true</CODE> if and only if \p *this is not empty and 2213 \ref Grid_Frequency "frequency" for \p *this with respect to \p expr 2214 is defined, in which case the frequency and the value for \p expr 2215 that is closest to zero are computed. 2216 2217 \param expr 2218 The linear expression for which the frequency is needed; 2219 2220 \param freq_n 2221 The numerator of the maximum frequency of \p expr; 2222 2223 \param freq_d 2224 The denominator of the maximum frequency of \p expr; 2225 2226 \param val_n 2227 The numerator of a value of \p expr at a point in the grid 2228 that is closest to zero; 2229 2230 \param val_d 2231 The denominator of a value of \p expr at a point in the grid 2232 that is closest to zero; 2233 2234 If \p *this is empty or frequency is undefined with respect to \p expr, 2235 then <CODE>false</CODE> is returned and \p freq_n, \p freq_d, 2236 \p val_n and \p val_d are left untouched. 2237 2238 \warning 2239 If \p expr and \p *this are dimension-incompatible, 2240 the grid generator system is not minimized or \p *this is 2241 empty, then the behavior is undefined. 2242 */ 2243 bool frequency_no_check(const Linear_Expression& expr, 2244 Coefficient& freq_n, Coefficient& freq_d, 2245 Coefficient& val_n, Coefficient& val_d) const; 2246 2247 //! Checks if and how \p expr is bounded in \p *this. 2248 /*! 2249 Returns <CODE>true</CODE> if and only if \p from_above is 2250 <CODE>true</CODE> and \p expr is bounded from above in \p *this, 2251 or \p from_above is <CODE>false</CODE> and \p expr is bounded 2252 from below in \p *this. 2253 2254 \param expr 2255 The linear expression to test; 2256 */ 2257 bool bounds_no_check(const Linear_Expression& expr) const; 2258 2259 /*! \brief 2260 Adds the congruence \p cg to \p *this. 2261 2262 \warning 2263 If \p cg and \p *this are dimension-incompatible, 2264 the grid generator system is not minimized or \p *this is 2265 empty, then the behavior is undefined. 2266 */ 2267 void add_congruence_no_check(const Congruence& cg); 2268 2269 /*! \brief 2270 Uses the constraint \p c to refine \p *this. 2271 2272 \param c 2273 The constraint to be added. 2274 2275 \exception std::invalid_argument 2276 Thrown if c is a non-trivial inequality constraint. 2277 2278 \warning 2279 If \p c and \p *this are dimension-incompatible, 2280 the behavior is undefined. 2281 */ 2282 void add_constraint_no_check(const Constraint& c); 2283 2284 /*! \brief 2285 Uses the constraint \p c to refine \p *this. 2286 2287 \param c 2288 The constraint to be added. 2289 Non-trivial inequalities are ignored. 2290 2291 \warning 2292 If \p c and \p *this are dimension-incompatible, 2293 the behavior is undefined. 2294 */ 2295 void refine_no_check(const Constraint& c); 2296 2297 //! \name Widening- and Extrapolation-Related Functions 2298 //@{ 2299 2300 //! Copies a widened selection of congruences from \p y to \p selected_cgs. 2301 void select_wider_congruences(const Grid& y, 2302 Congruence_System& selected_cgs) const; 2303 2304 //! Copies widened generators from \p y to \p widened_ggs. 2305 void select_wider_generators(const Grid& y, 2306 Grid_Generator_System& widened_ggs) const; 2307 2308 //@} // Widening- and Extrapolation-Related Functions 2309 2310 //! Adds new space dimensions to the given systems. 2311 /*! 2312 \param cgs 2313 A congruence system, to which columns are added; 2314 2315 \param gs 2316 A generator system, to which rows and columns are added; 2317 2318 \param dims 2319 The number of space dimensions to add. 2320 2321 This method is invoked only by 2322 <CODE>add_space_dimensions_and_embed()</CODE>. 2323 */ 2324 void add_space_dimensions(Congruence_System& cgs, 2325 Grid_Generator_System& gs, 2326 dimension_type dims); 2327 2328 //! Adds new space dimensions to the given systems. 2329 /*! 2330 \param gs 2331 A generator system, to which columns are added; 2332 2333 \param cgs 2334 A congruence system, to which rows and columns are added; 2335 2336 \param dims 2337 The number of space dimensions to add. 2338 2339 This method is invoked only by 2340 <CODE>add_space_dimensions_and_project()</CODE>. 2341 */ 2342 void add_space_dimensions(Grid_Generator_System& gs, 2343 Congruence_System& cgs, 2344 dimension_type dims); 2345 2346 //! \name Minimization-related Static Member Functions 2347 //@{ 2348 2349 //! Normalizes the divisors in \p sys. 2350 /*! 2351 Converts \p sys to an equivalent system in which the divisors are 2352 of equal value. 2353 2354 \param sys 2355 The generator system to be normalized. It must have at least one 2356 row. 2357 2358 \param divisor 2359 A reference to the initial value of the divisor. The resulting 2360 value of this object is the new system divisor. 2361 2362 \param first_point 2363 If \p first_point has a value other than NULL then it is taken as 2364 the first point in \p sys, and it is assumed that any following 2365 points have the same divisor as \p first_point. 2366 */ 2367 static void 2368 normalize_divisors(Grid_Generator_System& sys, 2369 Coefficient& divisor, 2370 const Grid_Generator* first_point = NULL); 2371 2372 //! Normalizes the divisors in \p sys. 2373 /*! 2374 Converts \p sys to an equivalent system in which the divisors are 2375 of equal value. 2376 2377 \param sys 2378 The generator system to be normalized. It must have at least one 2379 row. 2380 */ 2381 static void 2382 normalize_divisors(Grid_Generator_System& sys); 2383 2384 //! Normalize all the divisors in \p sys and \p gen_sys. 2385 /*! 2386 Modify \p sys and \p gen_sys to use the same single divisor value 2387 for all generators, leaving each system representing the grid it 2388 represented originally. 2389 2390 \param sys 2391 The first of the generator systems to be normalized. 2392 2393 \param gen_sys 2394 The second of the generator systems to be normalized. This system 2395 must have at least one row and the divisors of the generators in 2396 this system must be equal. 2397 2398 \exception std::runtime_error 2399 Thrown if all rows in \p gen_sys are lines and/or parameters. 2400 */ 2401 static void normalize_divisors(Grid_Generator_System& sys, 2402 Grid_Generator_System& gen_sys); 2403 2404 /*! \brief 2405 Converts generator system \p dest to be equivalent to congruence 2406 system \p source. 2407 */ 2408 static void conversion(Congruence_System& source, 2409 Grid_Generator_System& dest, 2410 Dimension_Kinds& dim_kinds); 2411 2412 /*! \brief 2413 Converts congruence system \p dest to be equivalent to generator 2414 system \p source. 2415 */ 2416 static void conversion(Grid_Generator_System& source, 2417 Congruence_System& dest, 2418 Dimension_Kinds& dim_kinds); 2419 2420 //! Converts \p cgs to upper triangular (i.e. minimized) form. 2421 /*! 2422 Returns <CODE>true</CODE> if \p cgs represents the empty set, 2423 otherwise returns <CODE>false</CODE>. 2424 */ 2425 static bool simplify(Congruence_System& cgs, 2426 Dimension_Kinds& dim_kinds); 2427 2428 //! Converts \p gs to lower triangular (i.e. minimized) form. 2429 /*! 2430 Expects \p gs to contain at least one point. 2431 */ 2432 static void simplify(Grid_Generator_System& ggs, 2433 Dimension_Kinds& dim_kinds); 2434 2435 //! Reduces the line \p row using the line \p pivot. 2436 /*! 2437 Uses the line \p pivot to change the representation of the line 2438 \p row so that the element at index \p column of \p row is zero. 2439 */ 2440 // A member of Grid for access to Matrix<Dense_Row>::rows. 2441 static void reduce_line_with_line(Grid_Generator& row, 2442 Grid_Generator& pivot, 2443 dimension_type column); 2444 2445 //! Reduces the equality \p row using the equality \p pivot. 2446 /*! 2447 Uses the equality \p pivot to change the representation of the 2448 equality \p row so that the element at index \p column of \p row 2449 is zero. 2450 */ 2451 // A member of Grid for access to Matrix<Dense_Row>::rows. 2452 static void reduce_equality_with_equality(Congruence& row, 2453 const Congruence& pivot, 2454 dimension_type column); 2455 2456 //! Reduces \p row using \p pivot. 2457 /*! 2458 Uses the point, parameter or proper congruence at \p pivot to 2459 change the representation of the point, parameter or proper 2460 congruence at \p row so that the element at index \p column of \p row 2461 is zero. Only elements from index \p start to index \p end are 2462 modified (i.e. it is assumed that all other elements are zero). 2463 This means that \p col must be in [start,end). 2464 2465 NOTE: This may invalidate the rows, since it messes with the divisors. 2466 Client code has to fix that (if needed) and assert OK(). 2467 */ 2468 // Part of Grid for access to Matrix<Dense_Row>::rows. 2469 template <typename R> 2470 static void reduce_pc_with_pc(R& row, 2471 R& pivot, 2472 dimension_type column, 2473 dimension_type start, 2474 dimension_type end); 2475 2476 //! Reduce \p row using \p pivot. 2477 /*! 2478 Use the line \p pivot to change the representation of the 2479 parameter \p row such that the element at index \p column of \p row 2480 is zero. 2481 */ 2482 // This takes a parameter with type Swapping_Vector<Grid_Generator> (instead 2483 // of Grid_Generator_System) to simplify the implementation of `simplify()'. 2484 // NOTE: This may invalidate `row' and the rows in `sys'. Client code must 2485 // fix/check this. 2486 static void reduce_parameter_with_line(Grid_Generator& row, 2487 const Grid_Generator& pivot, 2488 dimension_type column, 2489 Swapping_Vector<Grid_Generator>& sys, 2490 dimension_type num_columns); 2491 2492 //! Reduce \p row using \p pivot. 2493 /*! 2494 Use the equality \p pivot to change the representation of the 2495 congruence \p row such that element at index \p column of \p row 2496 is zero. 2497 */ 2498 // A member of Grid for access to Matrix<Dense_Row>::rows. 2499 // This takes a parameter with type Swapping_Vector<Congruence> (instead of 2500 // Congruence_System) to simplify the implementation of `conversion()'. 2501 static void reduce_congruence_with_equality(Congruence& row, 2502 const Congruence& pivot, 2503 dimension_type column, 2504 Swapping_Vector<Congruence>& sys); 2505 2506 //! Reduce column \p dim in rows preceding \p pivot_index in \p sys. 2507 /*! 2508 Required when converting (or simplifying) a congruence or generator 2509 system to "strong minimal form"; informally, strong minimal form means 2510 that, not only is the system in minimal form (ie a triangular matrix), 2511 but also the absolute values of the coefficients of the proper congruences 2512 and parameters are minimal. As a simple example, the set of congruences 2513 \f$\{3x \equiv_3 0, 4x + y \equiv_3 1\}\f$, 2514 (which is in minimal form) is equivalent to the set 2515 \f$\{3x \equiv_3 0, x + y \equiv_3 1\}\f$ 2516 (which is in strong minimal form). 2517 2518 \param sys 2519 The generator or congruence system to be reduced to strong minimal form. 2520 2521 \param dim 2522 Column to be reduced. 2523 2524 \param pivot_index 2525 Index of last row to be reduced. 2526 2527 \param start 2528 Index of first column to be changed. 2529 2530 \param end 2531 Index of last column to be changed. 2532 2533 \param sys_dim_kinds 2534 Dimension kinds of the elements of \p sys. 2535 2536 \param generators 2537 Flag indicating whether \p sys is a congruence or generator system 2538 */ 2539 template <typename M> 2540 // This takes a parameter with type `Swapping_Vector<M::row_type>' 2541 // instead of `M' to simplify the implementation of simplify(). 2542 // NOTE: This may invalidate the rows in `sys'. Client code must 2543 // fix/check this. 2544 static void reduce_reduced(Swapping_Vector<typename M::row_type>& sys, 2545 dimension_type dim, 2546 dimension_type pivot_index, 2547 dimension_type start, dimension_type end, 2548 const Dimension_Kinds& sys_dim_kinds, 2549 bool generators = true); 2550 2551 //! Multiply the elements of \p dest by \p multiplier. 2552 // A member of Grid for access to Matrix<Dense_Row>::rows and cgs::operator[]. 2553 // The type of `dest' is Swapping_Vector<Congruence> instead of 2554 // Congruence_System to simplify the implementation of conversion(). 2555 static void multiply_grid(const Coefficient& multiplier, 2556 Congruence& cg, 2557 Swapping_Vector<Congruence>& dest, 2558 dimension_type num_rows); 2559 2560 //! Multiply the elements of \p dest by \p multiplier. 2561 // A member of Grid for access to Grid_Generator::operator[]. 2562 // The type of `dest' is Swapping_Vector<Grid_Generator> instead of 2563 // Grid_Generator_System to simplify the implementation of conversion(). 2564 // NOTE: This does not check whether the rows are OK(). Client code 2565 // should do that. 2566 static void multiply_grid(const Coefficient& multiplier, 2567 Grid_Generator& gen, 2568 Swapping_Vector<Grid_Generator>& dest, 2569 dimension_type num_rows); 2570 2571 /*! \brief 2572 If \p sys is lower triangular return <CODE>true</CODE>, else 2573 return <CODE>false</CODE>. 2574 */ 2575 static bool lower_triangular(const Congruence_System& sys, 2576 const Dimension_Kinds& dim_kinds); 2577 2578 /*! \brief 2579 If \p sys is upper triangular return <CODE>true</CODE>, else 2580 return <CODE>false</CODE>. 2581 */ 2582 static bool upper_triangular(const Grid_Generator_System& sys, 2583 const Dimension_Kinds& dim_kinds); 2584 2585 #ifndef NDEBUG 2586 //! Checks that trailing rows contain only zero terms. 2587 /*! 2588 If all columns contain zero in the rows of \p system from row 2589 index \p first to row index \p last then return <code>true</code>, 2590 else return <code>false</code>. \p row_size gives the number of 2591 columns in each row. 2592 2593 This method is only used in assertions in the simplify methods. 2594 */ 2595 template <typename M, typename R> 2596 static bool rows_are_zero(M& system, 2597 dimension_type first, 2598 dimension_type last, 2599 dimension_type row_size); 2600 #endif 2601 2602 //@} // Minimization-Related Static Member Functions 2603 2604 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 2605 //! \name Exception Throwers 2606 //@{ 2607 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 2608 protected: 2609 void throw_dimension_incompatible(const char* method, 2610 const char* other_name, 2611 dimension_type other_dim) const; 2612 void throw_dimension_incompatible(const char* method, 2613 const char* gr_name, 2614 const Grid& gr) const; 2615 void throw_dimension_incompatible(const char* method, 2616 const char* le_name, 2617 const Linear_Expression& le) const; 2618 void throw_dimension_incompatible(const char* method, 2619 const char* cg_name, 2620 const Congruence& cg) const; 2621 void throw_dimension_incompatible(const char* method, 2622 const char* c_name, 2623 const Constraint& c) const; 2624 void throw_dimension_incompatible(const char* method, 2625 const char* g_name, 2626 const Grid_Generator& g) const; 2627 void throw_dimension_incompatible(const char* method, 2628 const char* g_name, 2629 const Generator& g) const; 2630 void throw_dimension_incompatible(const char* method, 2631 const char* cgs_name, 2632 const Congruence_System& cgs) const; 2633 void throw_dimension_incompatible(const char* method, 2634 const char* cs_name, 2635 const Constraint_System& cs) const; 2636 void throw_dimension_incompatible(const char* method, 2637 const char* gs_name, 2638 const Grid_Generator_System& gs) const; 2639 void throw_dimension_incompatible(const char* method, 2640 const char* var_name, 2641 Variable var) const; 2642 void throw_dimension_incompatible(const char* method, 2643 dimension_type required_space_dim) const; 2644 2645 static void throw_invalid_argument(const char* method, 2646 const char* reason); 2647 static void throw_invalid_constraint(const char* method, 2648 const char* c_name); 2649 static void throw_invalid_constraints(const char* method, 2650 const char* cs_name); 2651 static void throw_invalid_generator(const char* method, 2652 const char* g_name); 2653 static void throw_invalid_generators(const char* method, 2654 const char* gs_name); 2655 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 2656 //@} // Exception Throwers 2657 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 2658 2659 }; 2660 2661 #include "Grid_Status_inlines.hh" 2662 #include "Grid_inlines.hh" 2663 #include "Grid_templates.hh" 2664 2665 #endif // !defined(PPL_Grid_defs_hh) 2666