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