1 /* Partially_Reduced_Product 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_Partially_Reduced_Product_defs_hh 25 #define PPL_Partially_Reduced_Product_defs_hh 1 26 27 #include "Partially_Reduced_Product_types.hh" 28 #include "globals_types.hh" 29 #include "Coefficient_defs.hh" 30 #include "Variable_types.hh" 31 #include "Variables_Set_types.hh" 32 #include "Linear_Expression_types.hh" 33 #include "Constraint_types.hh" 34 #include "Generator_types.hh" 35 #include "Congruence_types.hh" 36 #include "Grid_Generator_types.hh" 37 #include "Constraint_System_types.hh" 38 #include "Generator_System_types.hh" 39 #include "Congruence_System_types.hh" 40 #include "Grid_Generator_System_types.hh" 41 #include "Poly_Con_Relation_defs.hh" 42 #include "Poly_Gen_Relation_defs.hh" 43 #include "C_Polyhedron_types.hh" 44 #include "NNC_Polyhedron_types.hh" 45 #include "Grid_types.hh" 46 #include "Box_types.hh" 47 #include "BD_Shape_types.hh" 48 #include "Octagonal_Shape_types.hh" 49 50 namespace Parma_Polyhedra_Library { 51 52 namespace IO_Operators { 53 54 //! Output operator. 55 /*! 56 \relates Parma_Polyhedra_Library::Partially_Reduced_Product 57 Writes a textual representation of \p dp on \p s. 58 */ 59 template <typename D1, typename D2, typename R> 60 std::ostream& 61 operator<<(std::ostream& s, const Partially_Reduced_Product<D1, D2, R>& dp); 62 63 } // namespace IO_Operators 64 65 //! Swaps \p x with \p y. 66 /*! \relates Partially_Reduced_Product */ 67 template <typename D1, typename D2, typename R> 68 void swap(Partially_Reduced_Product<D1, D2, R>& x, 69 Partially_Reduced_Product<D1, D2, R>& y); 70 71 /*! \brief 72 Returns <CODE>true</CODE> if and only if the components of \p x and \p y 73 are pairwise equal. 74 75 \relates Partially_Reduced_Product 76 Note that \p x and \p y may be dimension-incompatible: in 77 those cases, the value <CODE>false</CODE> is returned. 78 */ 79 template <typename D1, typename D2, typename R> 80 bool operator==(const Partially_Reduced_Product<D1, D2, R>& x, 81 const Partially_Reduced_Product<D1, D2, R>& y); 82 83 /*! \brief 84 Returns <CODE>true</CODE> if and only if the components of \p x and \p y 85 are not pairwise equal. 86 87 \relates Partially_Reduced_Product 88 Note that \p x and \p y may be dimension-incompatible: in 89 those cases, the value <CODE>true</CODE> is returned. 90 */ 91 template <typename D1, typename D2, typename R> 92 bool operator!=(const Partially_Reduced_Product<D1, D2, R>& x, 93 const Partially_Reduced_Product<D1, D2, R>& y); 94 95 } // namespace Parma_Polyhedra_Library 96 97 98 /*! \brief 99 This class provides the reduction method for the Smash_Product 100 domain. 101 102 \ingroup PPL_CXX_interface 103 The reduction classes are used to instantiate the Partially_Reduced_Product 104 domain. This class propagates emptiness between its components. 105 */ 106 template <typename D1, typename D2> 107 class Parma_Polyhedra_Library::Smash_Reduction { 108 public: 109 //! Default constructor. 110 Smash_Reduction(); 111 112 /*! \brief 113 The smash reduction operator for propagating emptiness between the 114 domain elements \p d1 and \p d2. 115 116 If either of the the domain elements \p d1 or \p d2 is empty 117 then the other is also set empty. 118 119 \param d1 120 A pointset domain element; 121 122 \param d2 123 A pointset domain element; 124 */ 125 void product_reduce(D1& d1, D2& d2); 126 127 //! Destructor. 128 ~Smash_Reduction(); 129 }; 130 131 /*! \brief 132 This class provides the reduction method for the Constraints_Product 133 domain. 134 135 \ingroup PPL_CXX_interface 136 The reduction classes are used to instantiate the Partially_Reduced_Product 137 domain. This class adds the constraints defining each of the component 138 domains to the other component. 139 */ 140 template <typename D1, typename D2> 141 class Parma_Polyhedra_Library::Constraints_Reduction { 142 public: 143 //! Default constructor. 144 Constraints_Reduction(); 145 146 /*! \brief 147 The constraints reduction operator for sharing constraints between the 148 domains. 149 150 The minimized constraint system defining the domain element \p d1 151 is added to \p d2 and the minimized constraint system defining \p d2 152 is added to \p d1. 153 In each case, the donor domain must provide a constraint system 154 in minimal form; this must define a polyhedron in which the 155 donor element is contained. 156 The recipient domain selects a subset of these constraints 157 that it can add to the recipient element. 158 For example: if the domain \p D1 is the Grid domain and \p D2 159 the NNC Polyhedron domain, then only the equality constraints are copied 160 from \p d1 to \p d2 and from \p d2 to \p d1. 161 162 \param d1 163 A pointset domain element; 164 165 \param d2 166 A pointset domain element; 167 */ 168 void product_reduce(D1& d1, D2& d2); 169 170 //! Destructor. 171 ~Constraints_Reduction(); 172 }; 173 174 /*! \brief 175 This class provides the reduction method for the Congruences_Product 176 domain. 177 178 \ingroup PPL_CXX_interface 179 The reduction classes are used to instantiate the Partially_Reduced_Product 180 domain. 181 182 This class uses the minimized congruences defining each of the components. 183 For each of the congruences, it checks if the other component 184 intersects none, one or more than one hyperplane defined by the congruence 185 and adds equalities or emptiness as appropriate; in more detail: 186 Letting the components be d1 and d2, then, for each congruence cg 187 representing d1: 188 - if more than one hyperplane defined by cg intersects 189 d2, then d1 and d2 are unchanged; 190 - if exactly one hyperplane intersects d2, then d1 and d2 are 191 refined with the corresponding equality ; 192 - otherwise, d1 and d2 are set to empty. 193 Unless d1 and d2 are already empty, the process is repeated where the 194 roles of d1 and d2 are reversed. 195 If d1 or d2 is empty, then the emptiness is propagated. 196 197 */ 198 template <typename D1, typename D2> 199 class Parma_Polyhedra_Library::Congruences_Reduction { 200 public: 201 //! Default constructor. 202 Congruences_Reduction(); 203 204 /*! \brief 205 The congruences reduction operator for detect emptiness or any equalities 206 implied by each of the congruences defining one of the components 207 and the bounds of the other component. It is assumed that the 208 components are already constraints reduced. 209 210 The minimized congruence system defining the domain element \p d1 211 is used to check if \p d2 intersects none, one or more than one 212 of the hyperplanes defined by the congruences: if it intersects none, 213 then product is set empty; if it intersects one, then the equality 214 defining this hyperplane is added to both components; otherwise, 215 the product is unchanged. 216 In each case, the donor domain must provide a congruence system 217 in minimal form. 218 219 \param d1 220 A pointset domain element; 221 222 \param d2 223 A pointset domain element; 224 */ 225 void product_reduce(D1& d1, D2& d2); 226 227 //! Destructor. 228 ~Congruences_Reduction(); 229 }; 230 231 /*! \brief 232 This class provides the reduction method for the Shape_Preserving_Product 233 domain. 234 235 \ingroup PPL_CXX_interface 236 The reduction classes are used to instantiate the Partially_Reduced_Product 237 domain. 238 239 This reduction method includes the congruences reduction. 240 This class uses the minimized constraints defining each of the components. 241 For each of the constraints, it checks the frequency and value for the same 242 linear expression in the other component. If the constraint does not satisfy 243 the implied congruence, the inhomogeneous term is adjusted so that it does. 244 Note that, unless the congruences reduction adds equalities, the 245 shapes of the domains are unaltered. 246 247 */ 248 template <typename D1, typename D2> 249 class Parma_Polyhedra_Library::Shape_Preserving_Reduction { 250 public: 251 //! Default constructor. 252 Shape_Preserving_Reduction(); 253 254 /*! \brief 255 The congruences reduction operator for detect emptiness or any equalities 256 implied by each of the congruences defining one of the components 257 and the bounds of the other component. It is assumed that the 258 components are already constraints reduced. 259 260 The minimized congruence system defining the domain element \p d1 261 is used to check if \p d2 intersects none, one or more than one 262 of the hyperplanes defined by the congruences: if it intersects none, 263 then product is set empty; if it intersects one, then the equality 264 defining this hyperplane is added to both components; otherwise, 265 the product is unchanged. 266 In each case, the donor domain must provide a congruence system 267 in minimal form. 268 269 \param d1 270 A pointset domain element; 271 272 \param d2 273 A pointset domain element; 274 */ 275 void product_reduce(D1& d1, D2& d2); 276 277 //! Destructor. 278 ~Shape_Preserving_Reduction(); 279 }; 280 281 /*! \brief 282 This class provides the reduction method for the Direct_Product domain. 283 284 \ingroup PPL_CXX_interface 285 The reduction classes are used to instantiate the Partially_Reduced_Product 286 domain template parameter \p R. This class does no reduction at all. 287 */ 288 template <typename D1, typename D2> 289 class Parma_Polyhedra_Library::No_Reduction { 290 public: 291 //! Default constructor. 292 No_Reduction(); 293 294 /*! \brief 295 The null reduction operator. 296 297 The parameters \p d1 and \p d2 are ignored. 298 */ 299 void product_reduce(D1& d1, D2& d2); 300 301 //! Destructor. 302 ~No_Reduction(); 303 }; 304 305 //! The partially reduced product of two abstractions. 306 /*! \ingroup PPL_CXX_interface 307 308 \warning 309 At present, the supported instantiations for the 310 two domain templates \p D1 and \p D2 are the simple pointset domains: 311 <CODE>C_Polyhedron</CODE>, 312 <CODE>NNC_Polyhedron</CODE>, 313 <CODE>Grid</CODE>, 314 <CODE>Octagonal_Shape\<T\></CODE>, 315 <CODE>BD_Shape\<T\></CODE>, 316 <CODE>Box\<T\></CODE>. 317 318 An object of the class <CODE>Partially_Reduced_Product\<D1, D2, R\></CODE> 319 represents the (partially reduced) product of two pointset domains \p D1 320 and \p D2 where the form of any reduction is defined by the 321 reduction class \p R. 322 323 Suppose \f$D_1\f$ and \f$D_2\f$ are two abstract domains 324 with concretization functions: 325 \f$\fund{\gamma_1}{D_1}{\Rset^n}\f$ and 326 \f$\fund{\gamma_2}{D_2}{\Rset^n}\f$, respectively. 327 328 The partially reduced product \f$D = D_1 \times D_2\f$, 329 for any reduction class \p R, has a concretization 330 \f$\fund{\gamma}{D}{\Rset^n}\f$ 331 where, if \f$d = (d_1, d_2) \in D\f$ 332 \f[ 333 \gamma(d) = \gamma_1(d_1) \inters \gamma_2(d_2). 334 \f] 335 336 The operations are defined to be the result of applying the corresponding 337 operations on each of the components provided the product is already reduced 338 by the reduction method defined by \p R. 339 In particular, if \p R is the <CODE>No_Reduction\<D1, D2\></CODE> class, 340 then the class <CODE>Partially_Reduced_Product\<D1, D2, R\></CODE> domain 341 is the direct product as defined in \ref CC79 "[CC79]". 342 343 How the results on the components are interpreted and 344 combined depend on the specific test. 345 For example, the test for emptiness will first make sure 346 the product is reduced (using the reduction method provided by \p R 347 if it is not already known to be reduced) and then test if either component 348 is empty; thus, if \p R defines no reduction between its components and 349 \f$d = (G, P) \in (\Gset \times \Pset)\f$ 350 is a direct product in one dimension where \f$G\f$ denotes the set of 351 numbers that are integral multiples of 3 while \f$P\f$ denotes the 352 set of numbers between 1 and 2, then an operation that tests for 353 emptiness should return false. 354 However, the test for the universe returns true if and only if the 355 test <CODE>is_universe()</CODE> on both components returns true. 356 357 \par 358 In all the examples it is assumed that the template \c R is the 359 <CODE>No_Reduction\<D1, D2\></CODE> class and that variables 360 \c x and \c y are defined (where they are used) as follows: 361 \code 362 Variable x(0); 363 Variable y(1); 364 \endcode 365 366 \par Example 1 367 The following code builds a direct product of a Grid and NNC Polyhedron, 368 corresponding to the positive even integer 369 pairs in \f$\Rset^2\f$, given as a system of congruences: 370 \code 371 Congruence_System cgs; 372 cgs.insert((x %= 0) / 2); 373 cgs.insert((y %= 0) / 2); 374 Partially_Reduced_Product<Grid, NNC_Polyhedron, No_Reduction<D1, D2> > 375 dp(cgs); 376 dp.add_constraint(x >= 0); 377 dp.add_constraint(y >= 0); 378 \endcode 379 380 \par Example 2 381 The following code builds the same product 382 in \f$\Rset^2\f$: 383 \code 384 Partially_Reduced_Product<Grid, NNC_Polyhedron, No_Reduction<D1, D2> > dp(2); 385 dp.add_constraint(x >= 0); 386 dp.add_constraint(y >= 0); 387 dp.add_congruence((x %= 0) / 2); 388 dp.add_congruence((y %= 0) / 2); 389 \endcode 390 391 \par Example 3 392 The following code will write "dp is empty": 393 \code 394 Partially_Reduced_Product<Grid, NNC_Polyhedron, No_Reduction<D1, D2> > dp(1); 395 dp.add_congruence((x %= 0) / 2); 396 dp.add_congruence((x %= 1) / 2); 397 if (dp.is_empty()) 398 cout << "dp is empty." << endl; 399 else 400 cout << "dp is not empty." << endl; 401 \endcode 402 403 \par Example 4 404 The following code will write "dp is not empty": 405 \code 406 Partially_Reduced_Product<Grid, NNC_Polyhedron, No_Reduction<D1, D2> > dp(1); 407 dp.add_congruence((x %= 0) / 2); 408 dp.add_constraint(x >= 1); 409 dp.add_constraint(x <= 1); 410 if (dp.is_empty()) 411 cout << "dp is empty." << endl; 412 else 413 cout << "dp is not empty." << endl; 414 \endcode 415 */ 416 417 template <typename D1, typename D2, typename R> 418 class Parma_Polyhedra_Library::Partially_Reduced_Product { 419 public: 420 /*! \brief 421 Returns the maximum space dimension this product 422 can handle. 423 */ 424 static dimension_type max_space_dimension(); 425 426 //! Builds an object having the specified properties. 427 /*! 428 \param num_dimensions 429 The number of dimensions of the vector space enclosing the pair; 430 431 \param kind 432 Specifies whether a universe or an empty pair has to be built. 433 434 \exception std::length_error 435 Thrown if \p num_dimensions exceeds the maximum allowed space 436 dimension. 437 */ 438 explicit Partially_Reduced_Product(dimension_type num_dimensions = 0, 439 Degenerate_Element kind = UNIVERSE); 440 441 //! Builds a pair, copying a system of congruences. 442 /*! 443 The pair inherits the space dimension of the congruence system. 444 445 \param cgs 446 The system of congruences to be approximated by the pair. 447 448 \exception std::length_error 449 Thrown if \p num_dimensions exceeds the maximum allowed space 450 dimension. 451 */ 452 explicit Partially_Reduced_Product(const Congruence_System& cgs); 453 454 //! Builds a pair, recycling a system of congruences. 455 /*! 456 The pair inherits the space dimension of the congruence system. 457 458 \param cgs 459 The system of congruences to be approximates by the pair. 460 Its data-structures may be recycled to build the pair. 461 462 \exception std::length_error 463 Thrown if \p num_dimensions exceeds the maximum allowed space 464 dimension. 465 */ 466 explicit Partially_Reduced_Product(Congruence_System& cgs); 467 468 //! Builds a pair, copying a system of constraints. 469 /*! 470 The pair inherits the space dimension of the constraint system. 471 472 \param cs 473 The system of constraints to be approximated by the pair. 474 475 \exception std::length_error 476 Thrown if \p num_dimensions exceeds the maximum allowed space 477 dimension. 478 */ 479 explicit Partially_Reduced_Product(const Constraint_System& cs); 480 481 //! Builds a pair, recycling a system of constraints. 482 /*! 483 The pair inherits the space dimension of the constraint system. 484 485 \param cs 486 The system of constraints to be approximated by the pair. 487 488 \exception std::length_error 489 Thrown if the space dimension of \p cs exceeds the maximum allowed 490 space dimension. 491 */ 492 explicit Partially_Reduced_Product(Constraint_System& cs); 493 494 //! Builds a product, from a C polyhedron. 495 /*! 496 Builds a product containing \p ph using algorithms whose 497 complexity does not exceed the one specified by \p complexity. 498 If \p complexity is \p ANY_COMPLEXITY, then the built product is the 499 smallest one containing \p ph. 500 The product inherits the space dimension of the polyhedron. 501 502 \param ph 503 The polyhedron to be approximated by the product. 504 505 \param complexity 506 The complexity that will not be exceeded. 507 508 \exception std::length_error 509 Thrown if the space dimension of \p ph exceeds the maximum allowed 510 space dimension. 511 */ 512 explicit 513 Partially_Reduced_Product(const C_Polyhedron& ph, 514 Complexity_Class complexity = ANY_COMPLEXITY); 515 516 //! Builds a product, from an NNC polyhedron. 517 /*! 518 Builds a product containing \p ph using algorithms whose 519 complexity does not exceed the one specified by \p complexity. 520 If \p complexity is \p ANY_COMPLEXITY, then the built product is the 521 smallest one containing \p ph. 522 The product inherits the space dimension of the polyhedron. 523 524 \param ph 525 The polyhedron to be approximated by the product. 526 527 \param complexity 528 The complexity that will not be exceeded. 529 530 \exception std::length_error 531 Thrown if the space dimension of \p ph exceeds the maximum allowed 532 space dimension. 533 */ 534 explicit 535 Partially_Reduced_Product(const NNC_Polyhedron& ph, 536 Complexity_Class complexity = ANY_COMPLEXITY); 537 538 //! Builds a product, from a grid. 539 /*! 540 Builds a product containing \p gr. 541 The product inherits the space dimension of the grid. 542 543 \param gr 544 The grid to be approximated by the product. 545 546 \param complexity 547 The complexity is ignored. 548 549 \exception std::length_error 550 Thrown if the space dimension of \p gr exceeds the maximum allowed 551 space dimension. 552 */ 553 explicit 554 Partially_Reduced_Product(const Grid& gr, 555 Complexity_Class complexity = ANY_COMPLEXITY); 556 557 //! Builds a product out of a box. 558 /*! 559 Builds a product containing \p box. 560 The product inherits the space dimension of the box. 561 562 \param box 563 The box representing the pair to be built. 564 565 \param complexity 566 The complexity is ignored. 567 568 \exception std::length_error 569 Thrown if the space dimension of \p box exceeds the maximum 570 allowed space dimension. 571 */ 572 template <typename Interval> 573 Partially_Reduced_Product(const Box<Interval>& box, 574 Complexity_Class complexity = ANY_COMPLEXITY); 575 576 //! Builds a product out of a BD shape. 577 /*! 578 Builds a product containing \p bd. 579 The product inherits the space dimension of the BD shape. 580 581 \param bd 582 The BD shape representing the product to be built. 583 584 \param complexity 585 The complexity is ignored. 586 587 \exception std::length_error 588 Thrown if the space dimension of \p bd exceeds the maximum 589 allowed space dimension. 590 */ 591 template <typename U> 592 Partially_Reduced_Product(const BD_Shape<U>& bd, 593 Complexity_Class complexity = ANY_COMPLEXITY); 594 595 //! Builds a product out of an octagonal shape. 596 /*! 597 Builds a product containing \p os. 598 The product inherits the space dimension of the octagonal shape. 599 600 \param os 601 The octagonal shape representing the product to be built. 602 603 \param complexity 604 The complexity is ignored. 605 606 \exception std::length_error 607 Thrown if the space dimension of \p os exceeds the maximum 608 allowed space dimension. 609 */ 610 template <typename U> 611 Partially_Reduced_Product(const Octagonal_Shape<U>& os, 612 Complexity_Class complexity = ANY_COMPLEXITY); 613 614 //! Ordinary copy constructor. 615 Partially_Reduced_Product(const Partially_Reduced_Product& y, 616 Complexity_Class complexity = ANY_COMPLEXITY); 617 618 //! Builds a conservative, upward approximation of \p y. 619 /*! 620 The complexity argument is ignored. 621 */ 622 template <typename E1, typename E2, typename S> 623 explicit 624 Partially_Reduced_Product(const Partially_Reduced_Product<E1, E2, S>& y, 625 Complexity_Class complexity = ANY_COMPLEXITY); 626 627 /*! \brief 628 The assignment operator. (\p *this and \p y can be 629 dimension-incompatible.) 630 */ 631 Partially_Reduced_Product& operator=(const Partially_Reduced_Product& y); 632 633 //! \name Member Functions that Do Not Modify the Partially_Reduced_Product 634 //@{ 635 636 //! Returns the dimension of the vector space enclosing \p *this. 637 dimension_type space_dimension() const; 638 639 /*! \brief 640 Returns the minimum \ref Affine_Independence_and_Affine_Dimension 641 "affine dimension" 642 (see also \ref Grid_Affine_Dimension "grid affine dimension") 643 of the components of \p *this. 644 */ 645 dimension_type affine_dimension() const; 646 647 //! Returns a constant reference to the first of the pair. 648 const D1& domain1() const; 649 650 //! Returns a constant reference to the second of the pair. 651 const D2& domain2() const; 652 653 //! Returns a system of constraints which approximates \p *this. 654 Constraint_System constraints() const; 655 656 /*! \brief 657 Returns a system of constraints which approximates \p *this, in 658 reduced form. 659 */ 660 Constraint_System minimized_constraints() const; 661 662 //! Returns a system of congruences which approximates \p *this. 663 Congruence_System congruences() const; 664 665 /*! \brief 666 Returns a system of congruences which approximates \p *this, in 667 reduced form. 668 */ 669 Congruence_System minimized_congruences() const; 670 671 //! Returns the relations holding between \p *this and \p c. 672 /* 673 \exception std::invalid_argument 674 Thrown if \p *this and congruence \p cg are dimension-incompatible. 675 676 Returns the Poly_Con_Relation \p r for \p *this: 677 suppose the first component returns \p r1 and the second \p r2, 678 then \p r implies <CODE>is_included()</CODE> 679 if and only if one or both of \p r1 and \p r2 imply 680 <CODE>is_included()</CODE>; 681 \p r implies <CODE>saturates()</CODE> 682 if and only if one or both of \p r1 and \p r2 imply 683 <CODE>saturates()</CODE>; 684 \p r implies <CODE>is_disjoint()</CODE> 685 if and only if one or both of \p r1 and \p r2 imply 686 <CODE>is_disjoint()</CODE>; 687 and \p r implies <CODE>nothing()</CODE> 688 if and only if both \p r1 and \p r2 imply 689 <CODE>strictly_intersects()</CODE>. 690 */ 691 Poly_Con_Relation relation_with(const Constraint& c) const; 692 693 //! Returns the relations holding between \p *this and \p cg. 694 /* 695 \exception std::invalid_argument 696 Thrown if \p *this and congruence \p cg are dimension-incompatible. 697 */ 698 Poly_Con_Relation relation_with(const Congruence& cg) const; 699 700 //! Returns the relations holding between \p *this and \p g. 701 /* 702 \exception std::invalid_argument 703 Thrown if \p *this and generator \p g are dimension-incompatible. 704 705 Returns the Poly_Gen_Relation \p r for \p *this: 706 suppose the first component returns \p r1 and the second \p r2, 707 then \p r = <CODE>subsumes()</CODE> 708 if and only if \p r1 = \p r2 = <CODE>subsumes()</CODE>; 709 and \p r = <CODE>nothing()</CODE> 710 if and only if one or both of \p r1 and \p r2 = <CODE>nothing()</CODE>; 711 */ 712 Poly_Gen_Relation relation_with(const Generator& g) const; 713 714 /*! \brief 715 Returns <CODE>true</CODE> if and only if either of the components 716 of \p *this are empty. 717 */ 718 bool is_empty() const; 719 720 /*! \brief 721 Returns <CODE>true</CODE> if and only if both of the components 722 of \p *this are the universe. 723 */ 724 bool is_universe() const; 725 726 /*! \brief 727 Returns <CODE>true</CODE> if and only if both of the components 728 of \p *this are topologically closed subsets of the vector space. 729 */ 730 bool is_topologically_closed() const; 731 732 /*! \brief 733 Returns <CODE>true</CODE> if and only if \p *this and \p y are 734 componentwise disjoint. 735 736 \exception std::invalid_argument 737 Thrown if \p x and \p y are dimension-incompatible. 738 */ 739 bool is_disjoint_from(const Partially_Reduced_Product& y) const; 740 741 /*! \brief 742 Returns <CODE>true</CODE> if and only if a component of \p *this 743 is discrete. 744 */ 745 bool is_discrete() const; 746 747 /*! \brief 748 Returns <CODE>true</CODE> if and only if a component of \p *this 749 is bounded. 750 */ 751 bool is_bounded() const; 752 753 /*! \brief 754 Returns <CODE>true</CODE> if and only if \p var is constrained in 755 \p *this. 756 757 \exception std::invalid_argument 758 Thrown if \p var is not a space dimension of \p *this. 759 */ 760 bool constrains(Variable var) const; 761 762 //! Returns <CODE>true</CODE> if and only if \p expr is bounded in \p *this. 763 /*! 764 This method is the same as bounds_from_below. 765 766 \exception std::invalid_argument 767 Thrown if \p expr and \p *this are dimension-incompatible. 768 */ 769 bool bounds_from_above(const Linear_Expression& expr) const; 770 771 //! Returns <CODE>true</CODE> if and only if \p expr is bounded in \p *this. 772 /*! 773 This method is the same as bounds_from_above. 774 775 \exception std::invalid_argument 776 Thrown if \p expr and \p *this are dimension-incompatible. 777 */ 778 bool bounds_from_below(const Linear_Expression& expr) const; 779 780 /*! \brief 781 Returns <CODE>true</CODE> if and only if \p *this is not empty and 782 \p expr is bounded from above in \p *this, in which case the 783 supremum value is computed. 784 785 \param expr 786 The linear expression to be maximized subject to \p *this; 787 788 \param sup_n 789 The numerator of the supremum value; 790 791 \param sup_d 792 The denominator of the supremum value; 793 794 \param maximum 795 <CODE>true</CODE> if the supremum value can be reached in \p this. 796 797 \exception std::invalid_argument 798 Thrown if \p expr and \p *this are dimension-incompatible. 799 800 If \p *this is empty or \p expr is not bounded by \p *this, 801 <CODE>false</CODE> is returned and \p sup_n, \p sup_d and \p 802 maximum are left untouched. 803 */ 804 bool maximize(const Linear_Expression& expr, 805 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const; 806 807 /*! \brief 808 Returns <CODE>true</CODE> if and only if \p *this is not empty and 809 \p expr is bounded from above in \p *this, in which case the 810 supremum value and a point where \p expr reaches it are computed. 811 812 \param expr 813 The linear expression to be maximized subject to \p *this; 814 815 \param sup_n 816 The numerator of the supremum value; 817 818 \param sup_d 819 The denominator of the supremum value; 820 821 \param maximum 822 <CODE>true</CODE> if the supremum value can be reached in \p this. 823 824 \param g 825 When maximization succeeds, will be assigned the point or 826 closure point where \p expr reaches its supremum value. 827 828 \exception std::invalid_argument 829 Thrown if \p expr and \p *this are dimension-incompatible. 830 831 If \p *this is empty or \p expr is not bounded by \p *this, 832 <CODE>false</CODE> is returned and \p sup_n, \p sup_d, \p maximum 833 and \p g are left untouched. 834 */ 835 bool maximize(const Linear_Expression& expr, 836 Coefficient& sup_n, Coefficient& sup_d, bool& maximum, 837 Generator& g) const; 838 839 /*! \brief 840 Returns <CODE>true</CODE> if and only if \p *this is not empty and 841 \p expr is bounded from below i \p *this, in which case the 842 infimum value is computed. 843 844 \param expr 845 The linear expression to be minimized subject to \p *this; 846 847 \param inf_n 848 The numerator of the infimum value; 849 850 \param inf_d 851 The denominator of the infimum value; 852 853 \param minimum 854 <CODE>true</CODE> if the infimum value can be reached in \p this. 855 856 \exception std::invalid_argument 857 Thrown if \p expr and \p *this are dimension-incompatible. 858 859 If \p *this is empty or \p expr is not bounded from below, 860 <CODE>false</CODE> is returned and \p inf_n, \p inf_d 861 and \p minimum are left untouched. 862 */ 863 bool minimize(const Linear_Expression& expr, 864 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const; 865 866 /*! \brief 867 Returns <CODE>true</CODE> if and only if \p *this is not empty and 868 \p expr is bounded from below in \p *this, in which case the 869 infimum value and a point where \p expr reaches it are computed. 870 871 \param expr 872 The linear expression to be minimized subject to \p *this; 873 874 \param inf_n 875 The numerator of the infimum value; 876 877 \param inf_d 878 The denominator of the infimum value; 879 880 \param minimum 881 <CODE>true</CODE> if the infimum value can be reached in \p this. 882 883 \param g 884 When minimization succeeds, will be assigned the point or closure 885 point where \p expr reaches its infimum value. 886 887 \exception std::invalid_argument 888 Thrown if \p expr and \p *this are dimension-incompatible. 889 890 If \p *this is empty or \p expr is not bounded from below, 891 <CODE>false</CODE> is returned and \p inf_n, \p inf_d, \p minimum 892 and \p point are left untouched. 893 */ 894 bool minimize(const Linear_Expression& expr, 895 Coefficient& inf_n, Coefficient& inf_d, bool& minimum, 896 Generator& g) const; 897 898 /*! \brief 899 Returns <CODE>true</CODE> if and only if each component of \p *this 900 contains the corresponding component of \p y. 901 902 \exception std::invalid_argument 903 Thrown if \p *this and \p y are dimension-incompatible. 904 */ 905 bool contains(const Partially_Reduced_Product& y) const; 906 907 /*! \brief 908 Returns <CODE>true</CODE> if and only if each component of \p *this 909 strictly contains the corresponding component of \p y. 910 911 \exception std::invalid_argument 912 Thrown if \p *this and \p y are dimension-incompatible. 913 */ 914 bool strictly_contains(const Partially_Reduced_Product& y) const; 915 916 //! Checks if all the invariants are satisfied. 917 bool OK() const; 918 919 //@} // Member Functions that Do Not Modify the Partially_Reduced_Product 920 921 //! \name Space Dimension Preserving Member Functions that May Modify the Partially_Reduced_Product 922 //@{ 923 924 //! Adds constraint \p c to \p *this. 925 /*! 926 \exception std::invalid_argument 927 Thrown if \p *this and \p c are dimension-incompatible. 928 */ 929 void add_constraint(const Constraint& c); 930 931 /*! \brief 932 Use the constraint \p c to refine \p *this. 933 934 \param c 935 The constraint to be used for refinement. 936 937 \exception std::invalid_argument 938 Thrown if \p *this and \p c are dimension-incompatible. 939 */ 940 void refine_with_constraint(const Constraint& c); 941 942 //! Adds a copy of congruence \p cg to \p *this. 943 /*! 944 \exception std::invalid_argument 945 Thrown if \p *this and congruence \p cg are 946 dimension-incompatible. 947 */ 948 void add_congruence(const Congruence& cg); 949 950 /*! \brief 951 Use the congruence \p cg to refine \p *this. 952 953 \param cg 954 The congruence to be used for refinement. 955 956 \exception std::invalid_argument 957 Thrown if \p *this and \p cg are dimension-incompatible. 958 */ 959 void refine_with_congruence(const Congruence& cg); 960 961 //! Adds a copy of the congruences in \p cgs to \p *this. 962 /*! 963 \param cgs 964 The congruence system to be added. 965 966 \exception std::invalid_argument 967 Thrown if \p *this and \p cgs are dimension-incompatible. 968 */ 969 void add_congruences(const Congruence_System& cgs); 970 971 /*! \brief 972 Use the congruences in \p cgs to refine \p *this. 973 974 \param cgs 975 The congruences to be used for refinement. 976 977 \exception std::invalid_argument 978 Thrown if \p *this and \p cgs are dimension-incompatible. 979 */ 980 void refine_with_congruences(const Congruence_System& cgs); 981 982 //! Adds the congruences in \p cgs to *this. 983 /*! 984 \param cgs 985 The congruence system to be added that may be recycled. 986 987 \exception std::invalid_argument 988 Thrown if \p *this and \p cs are dimension-incompatible. 989 990 \warning 991 The only assumption that can be made about \p cgs upon successful 992 or exceptional return is that it can be safely destroyed. 993 */ 994 void add_recycled_congruences(Congruence_System& cgs); 995 996 //! Adds a copy of the constraint system in \p cs to \p *this. 997 /*! 998 \param cs 999 The constraint system to be added. 1000 1001 \exception std::invalid_argument 1002 Thrown if \p *this and \p cs are dimension-incompatible. 1003 */ 1004 void add_constraints(const Constraint_System& cs); 1005 1006 /*! \brief 1007 Use the constraints in \p cs to refine \p *this. 1008 1009 \param cs 1010 The constraints to be used for refinement. 1011 1012 \exception std::invalid_argument 1013 Thrown if \p *this and \p cs are dimension-incompatible. 1014 */ 1015 void refine_with_constraints(const Constraint_System& cs); 1016 1017 //! Adds the constraint system in \p cs to \p *this. 1018 /*! 1019 \param cs 1020 The constraint system to be added that may be recycled. 1021 1022 \exception std::invalid_argument 1023 Thrown if \p *this and \p cs are dimension-incompatible. 1024 1025 \warning 1026 The only assumption that can be made about \p cs upon successful 1027 or exceptional return is that it can be safely destroyed. 1028 */ 1029 void add_recycled_constraints(Constraint_System& cs); 1030 1031 /*! \brief 1032 Computes the \ref Cylindrification "cylindrification" of \p *this with 1033 respect to space dimension \p var, assigning the result to \p *this. 1034 1035 \param var 1036 The space dimension that will be unconstrained. 1037 1038 \exception std::invalid_argument 1039 Thrown if \p var is not a space dimension of \p *this. 1040 */ 1041 void unconstrain(Variable var); 1042 1043 /*! \brief 1044 Computes the \ref Cylindrification "cylindrification" of \p *this with 1045 respect to the set of space dimensions \p vars, 1046 assigning the result to \p *this. 1047 1048 \param vars 1049 The set of space dimension that will be unconstrained. 1050 1051 \exception std::invalid_argument 1052 Thrown if \p *this is dimension-incompatible with one of the 1053 Variable objects contained in \p vars. 1054 */ 1055 void unconstrain(const Variables_Set& vars); 1056 1057 /*! \brief 1058 Assigns to \p *this the componentwise intersection of \p *this and \p y. 1059 1060 \exception std::invalid_argument 1061 Thrown if \p *this and \p y are dimension-incompatible. 1062 */ 1063 void intersection_assign(const Partially_Reduced_Product& y); 1064 1065 /*! \brief 1066 Assigns to \p *this an upper bound of \p *this and \p y 1067 computed on the corresponding components. 1068 1069 \exception std::invalid_argument 1070 Thrown if \p *this and \p y are dimension-incompatible. 1071 */ 1072 void upper_bound_assign(const Partially_Reduced_Product& y); 1073 1074 /*! \brief 1075 Assigns to \p *this an upper bound of \p *this and \p y 1076 computed on the corresponding components. 1077 If it is exact on each of the components of \p *this, <CODE>true</CODE> 1078 is returned, otherwise <CODE>false</CODE> is returned. 1079 1080 \exception std::invalid_argument 1081 Thrown if \p *this and \p y are dimension-incompatible. 1082 */ 1083 bool upper_bound_assign_if_exact(const Partially_Reduced_Product& y); 1084 1085 /*! \brief 1086 Assigns to \p *this an approximation of the set-theoretic difference 1087 of \p *this and \p y. 1088 1089 \exception std::invalid_argument 1090 Thrown if \p *this and \p y are dimension-incompatible. 1091 */ 1092 void difference_assign(const Partially_Reduced_Product& y); 1093 1094 /*! \brief 1095 Assigns to \p *this the \ref Single_Update_Affine_Functions 1096 "affine image" of \p 1097 *this under the function mapping variable \p var to the affine 1098 expression specified by \p expr and \p denominator. 1099 1100 \param var 1101 The variable to which the affine expression is assigned; 1102 1103 \param expr 1104 The numerator of the affine expression; 1105 1106 \param denominator 1107 The denominator of the affine expression (optional argument with 1108 default value 1). 1109 1110 \exception std::invalid_argument 1111 Thrown if \p denominator is zero or if \p expr and \p *this are 1112 dimension-incompatible or if \p var is not a space dimension of 1113 \p *this. 1114 1115 */ 1116 void affine_image(Variable var, 1117 const Linear_Expression& expr, 1118 Coefficient_traits::const_reference denominator 1119 = Coefficient_one()); 1120 1121 /*! \brief 1122 Assigns to \p *this the \ref Single_Update_Affine_Functions 1123 "affine preimage" of 1124 \p *this under the function mapping variable \p var to the affine 1125 expression specified by \p expr and \p denominator. 1126 1127 \param var 1128 The variable to which the affine expression is substituted; 1129 1130 \param expr 1131 The numerator of the affine expression; 1132 1133 \param denominator 1134 The denominator of the affine expression (optional argument with 1135 default value 1). 1136 1137 \exception std::invalid_argument 1138 Thrown if \p denominator is zero or if \p expr and \p *this are 1139 dimension-incompatible or if \p var is not a space dimension of \p *this. 1140 */ 1141 void affine_preimage(Variable var, 1142 const Linear_Expression& expr, 1143 Coefficient_traits::const_reference denominator 1144 = Coefficient_one()); 1145 1146 /*! \brief 1147 Assigns to \p *this the image of \p *this with respect to the 1148 \ref Generalized_Affine_Relations "generalized affine relation" 1149 \f$\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}\f$, 1150 where \f$\mathord{\relsym}\f$ is the relation symbol encoded 1151 by \p relsym 1152 (see also \ref Grid_Generalized_Image "generalized affine relation".) 1153 1154 \param var 1155 The left hand side variable of the generalized affine relation; 1156 1157 \param relsym 1158 The relation symbol; 1159 1160 \param expr 1161 The numerator of the right hand side affine expression; 1162 1163 \param denominator 1164 The denominator of the right hand side affine expression (optional 1165 argument with default value 1). 1166 1167 \exception std::invalid_argument 1168 Thrown if \p denominator is zero or if \p expr and \p *this are 1169 dimension-incompatible or if \p var is not a space dimension of \p *this 1170 or if \p *this is a C_Polyhedron and \p relsym is a strict 1171 relation symbol. 1172 */ 1173 void generalized_affine_image(Variable var, 1174 Relation_Symbol relsym, 1175 const Linear_Expression& expr, 1176 Coefficient_traits::const_reference denominator 1177 = Coefficient_one()); 1178 1179 /*! \brief 1180 Assigns to \p *this the preimage of \p *this with respect to the 1181 \ref Generalized_Affine_Relations "generalized affine relation" 1182 \f$\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}\f$, 1183 where \f$\mathord{\relsym}\f$ is the relation symbol encoded 1184 by \p relsym. 1185 (see also \ref Grid_Generalized_Image "generalized affine relation".) 1186 1187 \param var 1188 The left hand side variable of the generalized affine relation; 1189 1190 \param relsym 1191 The relation symbol; 1192 1193 \param expr 1194 The numerator of the right hand side affine expression; 1195 1196 \param denominator 1197 The denominator of the right hand side affine expression (optional 1198 argument with default value 1). 1199 1200 \exception std::invalid_argument 1201 Thrown if \p denominator is zero or if \p expr and \p *this are 1202 dimension-incompatible or if \p var is not a space dimension of \p *this 1203 or if \p *this is a C_Polyhedron and \p relsym is a strict 1204 relation symbol. 1205 */ 1206 void 1207 generalized_affine_preimage(Variable var, 1208 Relation_Symbol relsym, 1209 const Linear_Expression& expr, 1210 Coefficient_traits::const_reference denominator 1211 = Coefficient_one()); 1212 1213 /*! \brief 1214 Assigns to \p *this the image of \p *this with respect to the 1215 \ref Generalized_Affine_Relations "generalized affine relation" 1216 \f$\mathrm{lhs}' \relsym \mathrm{rhs}\f$, where 1217 \f$\mathord{\relsym}\f$ is the relation symbol encoded by \p relsym. 1218 (see also \ref Grid_Generalized_Image "generalized affine relation".) 1219 1220 \param lhs 1221 The left hand side affine expression; 1222 1223 \param relsym 1224 The relation symbol; 1225 1226 \param rhs 1227 The right hand side affine expression. 1228 1229 \exception std::invalid_argument 1230 Thrown if \p *this is dimension-incompatible with \p lhs or \p rhs 1231 or if \p *this is a C_Polyhedron and \p relsym is a strict 1232 relation symbol. 1233 */ 1234 void generalized_affine_image(const Linear_Expression& lhs, 1235 Relation_Symbol relsym, 1236 const Linear_Expression& rhs); 1237 1238 /*! \brief 1239 Assigns to \p *this the preimage of \p *this with respect to the 1240 \ref Generalized_Affine_Relations "generalized affine relation" 1241 \f$\mathrm{lhs}' \relsym \mathrm{rhs}\f$, where 1242 \f$\mathord{\relsym}\f$ is the relation symbol encoded by \p relsym. 1243 (see also \ref Grid_Generalized_Image "generalized affine relation".) 1244 1245 \param lhs 1246 The left hand side affine expression; 1247 1248 \param relsym 1249 The relation symbol; 1250 1251 \param rhs 1252 The right hand side affine expression. 1253 1254 \exception std::invalid_argument 1255 Thrown if \p *this is dimension-incompatible with \p lhs or \p rhs 1256 or if \p *this is a C_Polyhedron and \p relsym is a strict 1257 relation symbol. 1258 */ 1259 void generalized_affine_preimage(const Linear_Expression& lhs, 1260 Relation_Symbol relsym, 1261 const Linear_Expression& rhs); 1262 1263 /*! 1264 \brief 1265 Assigns to \p *this the image of \p *this with respect to the 1266 \ref Single_Update_Bounded_Affine_Relations "bounded affine relation" 1267 \f$\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} 1268 \leq \mathrm{var}' 1269 \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}\f$. 1270 1271 \param var 1272 The variable updated by the affine relation; 1273 1274 \param lb_expr 1275 The numerator of the lower bounding affine expression; 1276 1277 \param ub_expr 1278 The numerator of the upper bounding affine expression; 1279 1280 \param denominator 1281 The (common) denominator for the lower and upper bounding 1282 affine expressions (optional argument with default value 1). 1283 1284 \exception std::invalid_argument 1285 Thrown if \p denominator is zero or if \p lb_expr (resp., \p ub_expr) 1286 and \p *this are dimension-incompatible or if \p var is not a space 1287 dimension of \p *this. 1288 */ 1289 void bounded_affine_image(Variable var, 1290 const Linear_Expression& lb_expr, 1291 const Linear_Expression& ub_expr, 1292 Coefficient_traits::const_reference denominator 1293 = Coefficient_one()); 1294 1295 /*! 1296 \brief 1297 Assigns to \p *this the preimage of \p *this with respect to the 1298 \ref Single_Update_Bounded_Affine_Relations "bounded affine relation" 1299 \f$\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} 1300 \leq \mathrm{var}' 1301 \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}\f$. 1302 1303 \param var 1304 The variable updated by the affine relation; 1305 1306 \param lb_expr 1307 The numerator of the lower bounding affine expression; 1308 1309 \param ub_expr 1310 The numerator of the upper bounding affine expression; 1311 1312 \param denominator 1313 The (common) denominator for the lower and upper bounding 1314 affine expressions (optional argument with default value 1). 1315 1316 \exception std::invalid_argument 1317 Thrown if \p denominator is zero or if \p lb_expr (resp., \p ub_expr) 1318 and \p *this are dimension-incompatible or if \p var is not a space 1319 dimension of \p *this. 1320 */ 1321 void bounded_affine_preimage(Variable var, 1322 const Linear_Expression& lb_expr, 1323 const Linear_Expression& ub_expr, 1324 Coefficient_traits::const_reference denominator 1325 = Coefficient_one()); 1326 1327 /*! \brief 1328 Assigns to \p *this the result of computing the \ref Time_Elapse_Operator 1329 "time-elapse" between \p *this and \p y. 1330 (See also \ref Grid_Time_Elapse "time-elapse".) 1331 1332 \exception std::invalid_argument 1333 Thrown if \p *this and \p y are dimension-incompatible. 1334 */ 1335 void time_elapse_assign(const Partially_Reduced_Product& y); 1336 1337 //! Assigns to \p *this its topological closure. 1338 void topological_closure_assign(); 1339 1340 // TODO: Add a way to call other widenings. 1341 1342 // CHECKME: This may not be a real widening; it depends on the reduction 1343 // class R and the widening used. 1344 1345 /*! \brief 1346 Assigns to \p *this the result of computing the 1347 "widening" between \p *this and \p y. 1348 1349 This widening uses either the congruence or generator systems 1350 depending on which of the systems describing x and y 1351 are up to date and minimized. 1352 1353 \param y 1354 A product that <EM>must</EM> be contained in \p *this; 1355 1356 \param tp 1357 An optional pointer to an unsigned variable storing the number of 1358 available tokens (to be used when applying the 1359 \ref Widening_with_Tokens "widening with tokens" delay technique). 1360 1361 \exception std::invalid_argument 1362 Thrown if \p *this and \p y are dimension-incompatible. 1363 */ 1364 void widening_assign(const Partially_Reduced_Product& y, 1365 unsigned* tp = NULL); 1366 1367 /*! \brief 1368 Possibly tightens \p *this by dropping some points with non-integer 1369 coordinates. 1370 1371 \param complexity 1372 The maximal complexity of any algorithms used. 1373 1374 \note 1375 Currently there is no optimality guarantee, not even if 1376 \p complexity is <CODE>ANY_COMPLEXITY</CODE>. 1377 */ 1378 void drop_some_non_integer_points(Complexity_Class complexity 1379 = ANY_COMPLEXITY); 1380 1381 /*! \brief 1382 Possibly tightens \p *this by dropping some points with non-integer 1383 coordinates for the space dimensions corresponding to \p vars. 1384 1385 \param vars 1386 Points with non-integer coordinates for these variables/space-dimensions 1387 can be discarded. 1388 1389 \param complexity 1390 The maximal complexity of any algorithms used. 1391 1392 \note 1393 Currently there is no optimality guarantee, not even if 1394 \p complexity is <CODE>ANY_COMPLEXITY</CODE>. 1395 */ 1396 void drop_some_non_integer_points(const Variables_Set& vars, 1397 Complexity_Class complexity 1398 = ANY_COMPLEXITY); 1399 1400 //@} // Space Dimension Preserving Member Functions that May Modify [...] 1401 1402 //! \name Member Functions that May Modify the Dimension of the Vector Space 1403 //@{ 1404 1405 /*! \brief 1406 Adds \p m new space dimensions and embeds the components 1407 of \p *this in the new vector space. 1408 1409 \param m 1410 The number of dimensions to add. 1411 1412 \exception std::length_error 1413 Thrown if adding \p m new space dimensions would cause the vector 1414 space to exceed dimension <CODE>max_space_dimension()</CODE>. 1415 */ 1416 void add_space_dimensions_and_embed(dimension_type m); 1417 1418 /*! \brief 1419 Adds \p m new space dimensions and does not embed the components 1420 in the new vector space. 1421 1422 \param m 1423 The number of space dimensions to add. 1424 1425 \exception std::length_error 1426 Thrown if adding \p m new space dimensions would cause the 1427 vector space to exceed dimension <CODE>max_space_dimension()</CODE>. 1428 */ 1429 void add_space_dimensions_and_project(dimension_type m); 1430 1431 /*! \brief 1432 Assigns to the first (resp., second) component of \p *this 1433 the "concatenation" of the first (resp., second) components 1434 of \p *this and \p y, taken in this order. 1435 See also \ref Concatenating_Polyhedra. 1436 1437 \exception std::length_error 1438 Thrown if the concatenation would cause the vector space 1439 to exceed dimension <CODE>max_space_dimension()</CODE>. 1440 */ 1441 void concatenate_assign(const Partially_Reduced_Product& y); 1442 1443 //! Removes all the specified dimensions from the vector space. 1444 /*! 1445 \param vars 1446 The set of Variable objects corresponding to the space dimensions 1447 to be removed. 1448 1449 \exception std::invalid_argument 1450 Thrown if \p *this is dimension-incompatible with one of the 1451 Variable objects contained in \p vars. 1452 */ 1453 void remove_space_dimensions(const Variables_Set& vars); 1454 1455 /*! \brief 1456 Removes the higher dimensions of the vector space so that the 1457 resulting space will have dimension \p new_dimension. 1458 1459 \exception std::invalid_argument 1460 Thrown if \p new_dimensions is greater than the space dimension of 1461 \p *this. 1462 */ 1463 void remove_higher_space_dimensions(dimension_type new_dimension); 1464 1465 /*! \brief 1466 Remaps the dimensions of the vector space according to 1467 a \ref Mapping_the_Dimensions_of_the_Vector_Space "partial function". 1468 1469 If \p pfunc maps only some of the dimensions of \p *this then the 1470 rest will be projected away. 1471 1472 If the highest dimension mapped to by \p pfunc is higher than the 1473 highest dimension in \p *this then the number of dimensions in \p 1474 *this will be increased to the highest dimension mapped to by \p 1475 pfunc. 1476 1477 \param pfunc 1478 The partial function specifying the destiny of each space 1479 dimension. 1480 1481 The template class <CODE>Partial_Function</CODE> must provide the following 1482 methods. 1483 \code 1484 bool has_empty_codomain() const 1485 \endcode 1486 returns <CODE>true</CODE> if and only if the represented partial 1487 function has an empty codomain (i.e., it is always undefined). 1488 The <CODE>has_empty_codomain()</CODE> method will always be called 1489 before the methods below. However, if 1490 <CODE>has_empty_codomain()</CODE> returns <CODE>true</CODE>, none 1491 of the functions below will be called. 1492 \code 1493 dimension_type max_in_codomain() const 1494 \endcode 1495 returns the maximum value that belongs to the codomain of the 1496 partial function. 1497 The <CODE>max_in_codomain()</CODE> method is called at most once. 1498 \code 1499 bool maps(dimension_type i, dimension_type& j) const 1500 \endcode 1501 Let \f$f\f$ be the represented function and \f$k\f$ be the value 1502 of \p i. If \f$f\f$ is defined in \f$k\f$, then \f$f(k)\f$ is 1503 assigned to \p j and <CODE>true</CODE> is returned. If \f$f\f$ is 1504 undefined in \f$k\f$, then <CODE>false</CODE> is returned. 1505 This method is called at most \f$n\f$ times, where \f$n\f$ is the 1506 dimension of the vector space enclosing \p *this. 1507 1508 The result is undefined if \p pfunc does not encode a partial 1509 function with the properties described in 1510 \ref Mapping_the_Dimensions_of_the_Vector_Space 1511 "specification of the mapping operator". 1512 */ 1513 template <typename Partial_Function> 1514 void map_space_dimensions(const Partial_Function& pfunc); 1515 1516 //! Creates \p m copies of the space dimension corresponding to \p var. 1517 /*! 1518 \param var 1519 The variable corresponding to the space dimension to be replicated; 1520 1521 \param m 1522 The number of replicas to be created. 1523 1524 \exception std::invalid_argument 1525 Thrown if \p var does not correspond to a dimension of the vector 1526 space. 1527 1528 \exception std::length_error 1529 Thrown if adding \p m new space dimensions would cause the vector 1530 space to exceed dimension <CODE>max_space_dimension()</CODE>. 1531 1532 If \p *this has space dimension \f$n\f$, with \f$n > 0\f$, 1533 and <CODE>var</CODE> has space dimension \f$k \leq n\f$, 1534 then the \f$k\f$-th space dimension is 1535 \ref Expanding_One_Dimension_of_the_Vector_Space_to_Multiple_Dimensions 1536 "expanded" to \p m new space dimensions 1537 \f$n\f$, \f$n+1\f$, \f$\dots\f$, \f$n+m-1\f$. 1538 */ 1539 void expand_space_dimension(Variable var, dimension_type m); 1540 1541 //! Folds the space dimensions in \p vars into \p dest. 1542 /*! 1543 \param vars 1544 The set of Variable objects corresponding to the space dimensions 1545 to be folded; 1546 1547 \param dest 1548 The variable corresponding to the space dimension that is the 1549 destination of the folding operation. 1550 1551 \exception std::invalid_argument 1552 Thrown if \p *this is dimension-incompatible with \p dest or with 1553 one of the Variable objects contained in \p vars. Also 1554 thrown if \p dest is contained in \p vars. 1555 1556 If \p *this has space dimension \f$n\f$, with \f$n > 0\f$, 1557 <CODE>dest</CODE> has space dimension \f$k \leq n\f$, 1558 \p vars is a set of variables whose maximum space dimension 1559 is also less than or equal to \f$n\f$, and \p dest is not a member 1560 of \p vars, then the space dimensions corresponding to 1561 variables in \p vars are 1562 \ref Folding_Multiple_Dimensions_of_the_Vector_Space_into_One_Dimension 1563 "folded" into the \f$k\f$-th space dimension. 1564 */ 1565 void fold_space_dimensions(const Variables_Set& vars, Variable dest); 1566 1567 //@} // Member Functions that May Modify the Dimension of the Vector Space 1568 1569 friend bool operator==<>(const Partially_Reduced_Product<D1, D2, R>& x, 1570 const Partially_Reduced_Product<D1, D2, R>& y); 1571 1572 friend std::ostream& 1573 Parma_Polyhedra_Library::IO_Operators:: 1574 operator<<<>(std::ostream& s, const Partially_Reduced_Product<D1, D2, R>& dp); 1575 1576 //! \name Miscellaneous Member Functions 1577 //@{ 1578 1579 //! Destructor. 1580 ~Partially_Reduced_Product(); 1581 1582 /*! \brief 1583 Swaps \p *this with product \p y. (\p *this and \p y can be 1584 dimension-incompatible.) 1585 */ 1586 void m_swap(Partially_Reduced_Product& y); 1587 1588 PPL_OUTPUT_DECLARATIONS 1589 1590 /*! \brief 1591 Loads from \p s an ASCII representation (as produced by 1592 ascii_dump(std::ostream&) const) and sets \p *this accordingly. 1593 Returns <CODE>true</CODE> if successful, <CODE>false</CODE> otherwise. 1594 */ 1595 bool ascii_load(std::istream& s); 1596 1597 //! Returns the total size in bytes of the memory occupied by \p *this. 1598 memory_size_type total_memory_in_bytes() const; 1599 1600 //! Returns the size in bytes of the memory managed by \p *this. 1601 memory_size_type external_memory_in_bytes() const; 1602 1603 /*! \brief 1604 Returns a 32-bit hash code for \p *this. 1605 1606 If \p x and \p y are such that <CODE>x == y</CODE>, 1607 then <CODE>x.hash_code() == y.hash_code()</CODE>. 1608 */ 1609 int32_t hash_code() const; 1610 1611 //@} // Miscellaneous Member Functions 1612 1613 //! Reduce. 1614 /* 1615 \return 1616 <CODE>true</CODE> if and only if either of the resulting component 1617 is strictly contained in the respective original. 1618 */ 1619 bool reduce() const; 1620 1621 protected: 1622 //! The type of the first component. 1623 typedef D1 Domain1; 1624 1625 //! The type of the second component. 1626 typedef D2 Domain2; 1627 1628 //! The first component. 1629 D1 d1; 1630 1631 //! The second component. 1632 D2 d2; 1633 1634 protected: 1635 //! Clears the reduced flag. 1636 void clear_reduced_flag() const; 1637 1638 //! Sets the reduced flag. 1639 void set_reduced_flag() const; 1640 1641 //! Return <CODE>true</CODE> if and only if the reduced flag is set. 1642 bool is_reduced() const; 1643 1644 /*! \brief 1645 Flag to record whether the components are reduced with respect 1646 to each other and the reduction class. 1647 */ 1648 bool reduced; 1649 1650 private: 1651 void throw_space_dimension_overflow(const char* method, 1652 const char* reason); 1653 }; 1654 1655 namespace Parma_Polyhedra_Library { 1656 1657 /*! \brief 1658 This class is temporary and will be removed when template typedefs will 1659 be supported in C++. 1660 1661 When template typedefs will be supported in C++, what now is verbosely 1662 denoted by <CODE>Domain_Product\<Domain1, Domain2\>::%Direct_Product</CODE> 1663 will simply be denoted by <CODE>Direct_Product\<Domain1, Domain2\></CODE>. 1664 */ 1665 template <typename D1, typename D2> 1666 class Domain_Product { 1667 public: 1668 typedef Partially_Reduced_Product<D1, D2, No_Reduction<D1, D2> > 1669 Direct_Product; 1670 1671 typedef Partially_Reduced_Product<D1, D2, Smash_Reduction<D1, D2> > 1672 Smash_Product; 1673 1674 typedef Partially_Reduced_Product<D1, D2, Constraints_Reduction<D1, D2> > 1675 Constraints_Product; 1676 1677 typedef Partially_Reduced_Product<D1, D2, Congruences_Reduction<D1, D2> > 1678 Congruences_Product; 1679 1680 typedef Partially_Reduced_Product<D1, D2, Shape_Preserving_Reduction<D1, D2> > 1681 Shape_Preserving_Product; 1682 }; 1683 1684 } // namespace Parma_Polyhedra_Library 1685 1686 #include "Partially_Reduced_Product_inlines.hh" 1687 #include "Partially_Reduced_Product_templates.hh" 1688 1689 #endif // !defined(PPL_Partially_Reduced_Product_defs_hh) 1690