1 /* Box 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_Box_defs_hh 25 #define PPL_Box_defs_hh 1 26 27 #include "Box_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 "Constraint_defs.hh" 35 #include "Constraint_System_types.hh" 36 #include "Generator_types.hh" 37 #include "Generator_System_types.hh" 38 #include "Congruence_types.hh" 39 #include "Congruence_System_types.hh" 40 #include "BD_Shape_types.hh" 41 #include "Octagonal_Shape_types.hh" 42 #include "Poly_Con_Relation_types.hh" 43 #include "Poly_Gen_Relation_types.hh" 44 #include "Polyhedron_types.hh" 45 #include "Grid_types.hh" 46 #include "Partially_Reduced_Product_types.hh" 47 #include "intervals_defs.hh" 48 #include "Interval_types.hh" 49 #include "Linear_Form_types.hh" 50 #include <vector> 51 #include <iosfwd> 52 53 namespace Parma_Polyhedra_Library { 54 55 struct Interval_Base; 56 57 //! Swaps \p x with \p y. 58 /*! \relates Box */ 59 template <typename ITV> 60 void swap(Box<ITV>& x, Box<ITV>& y); 61 62 //! Returns <CODE>true</CODE> if and only if \p x and \p y are the same box. 63 /*! \relates Box 64 Note that \p x and \p y may be dimension-incompatible boxes: 65 in this case, the value <CODE>false</CODE> is returned. 66 */ 67 template <typename ITV> 68 bool operator==(const Box<ITV>& x, const Box<ITV>& y); 69 70 //! Returns <CODE>true</CODE> if and only if \p x and \p y are not the same box. 71 /*! \relates Box 72 Note that \p x and \p y may be dimension-incompatible boxes: 73 in this case, the value <CODE>true</CODE> is returned. 74 */ 75 template <typename ITV> 76 bool operator!=(const Box<ITV>& x, const Box<ITV>& y); 77 78 namespace IO_Operators { 79 80 //! Output operator. 81 /*! \relates Parma_Polyhedra_Library::Box */ 82 template <typename ITV> 83 std::ostream& operator<<(std::ostream& s, const Box<ITV>& box); 84 85 } // namespace IO_Operators 86 87 //! Computes the rectilinear (or Manhattan) distance between \p x and \p y. 88 /*! \relates Box 89 If the rectilinear distance between \p x and \p y is defined, 90 stores an approximation of it into \p r and returns <CODE>true</CODE>; 91 returns <CODE>false</CODE> otherwise. 92 93 The direction of the approximation is specified by \p dir. 94 95 All computations are performed using variables of type 96 <CODE>Checked_Number\<To, Extended_Number_Policy\></CODE>. 97 */ 98 template <typename To, typename ITV> 99 bool 100 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 101 const Box<ITV>& x, 102 const Box<ITV>& y, 103 Rounding_Dir dir); 104 105 //! Computes the rectilinear (or Manhattan) distance between \p x and \p y. 106 /*! \relates Box 107 If the rectilinear distance between \p x and \p y is defined, 108 stores an approximation of it into \p r and returns <CODE>true</CODE>; 109 returns <CODE>false</CODE> otherwise. 110 111 The direction of the approximation is specified by \p dir. 112 113 All computations are performed using variables of type 114 <CODE>Checked_Number\<Temp, Extended_Number_Policy\></CODE>. 115 */ 116 template <typename Temp, typename To, typename ITV> 117 bool 118 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 119 const Box<ITV>& x, 120 const Box<ITV>& y, 121 Rounding_Dir dir); 122 123 //! Computes the rectilinear (or Manhattan) distance between \p x and \p y. 124 /*! \relates Box 125 If the rectilinear distance between \p x and \p y is defined, 126 stores an approximation of it into \p r and returns <CODE>true</CODE>; 127 returns <CODE>false</CODE> otherwise. 128 129 The direction of the approximation is specified by \p dir. 130 131 All computations are performed using the temporary variables 132 \p tmp0, \p tmp1 and \p tmp2. 133 */ 134 template <typename Temp, typename To, typename ITV> 135 bool 136 rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 137 const Box<ITV>& x, 138 const Box<ITV>& y, 139 Rounding_Dir dir, 140 Temp& tmp0, 141 Temp& tmp1, 142 Temp& tmp2); 143 144 //! Computes the euclidean distance between \p x and \p y. 145 /*! \relates Box 146 If the euclidean distance between \p x and \p y is defined, 147 stores an approximation of it into \p r and returns <CODE>true</CODE>; 148 returns <CODE>false</CODE> otherwise. 149 150 The direction of the approximation is specified by \p dir. 151 152 All computations are performed using variables of type 153 <CODE>Checked_Number\<To, Extended_Number_Policy\></CODE>. 154 */ 155 template <typename To, typename ITV> 156 bool 157 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 158 const Box<ITV>& x, 159 const Box<ITV>& y, 160 Rounding_Dir dir); 161 162 //! Computes the euclidean distance between \p x and \p y. 163 /*! \relates Box 164 If the euclidean distance between \p x and \p y is defined, 165 stores an approximation of it into \p r and returns <CODE>true</CODE>; 166 returns <CODE>false</CODE> otherwise. 167 168 The direction of the approximation is specified by \p dir. 169 170 All computations are performed using variables of type 171 <CODE>Checked_Number\<Temp, Extended_Number_Policy\></CODE>. 172 */ 173 template <typename Temp, typename To, typename ITV> 174 bool 175 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 176 const Box<ITV>& x, 177 const Box<ITV>& y, 178 Rounding_Dir dir); 179 180 //! Computes the euclidean distance between \p x and \p y. 181 /*! \relates Box 182 If the euclidean distance between \p x and \p y is defined, 183 stores an approximation of it into \p r and returns <CODE>true</CODE>; 184 returns <CODE>false</CODE> otherwise. 185 186 The direction of the approximation is specified by \p dir. 187 188 All computations are performed using the temporary variables 189 \p tmp0, \p tmp1 and \p tmp2. 190 */ 191 template <typename Temp, typename To, typename ITV> 192 bool 193 euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 194 const Box<ITV>& x, 195 const Box<ITV>& y, 196 Rounding_Dir dir, 197 Temp& tmp0, 198 Temp& tmp1, 199 Temp& tmp2); 200 201 //! Computes the \f$L_\infty\f$ distance between \p x and \p y. 202 /*! \relates Box 203 If the \f$L_\infty\f$ distance between \p x and \p y is defined, 204 stores an approximation of it into \p r and returns <CODE>true</CODE>; 205 returns <CODE>false</CODE> otherwise. 206 207 The direction of the approximation is specified by \p dir. 208 209 All computations are performed using variables of type 210 <CODE>Checked_Number\<To, Extended_Number_Policy\></CODE>. 211 */ 212 template <typename To, typename ITV> 213 bool 214 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 215 const Box<ITV>& x, 216 const Box<ITV>& y, 217 Rounding_Dir dir); 218 219 //! Computes the \f$L_\infty\f$ distance between \p x and \p y. 220 /*! \relates Box 221 If the \f$L_\infty\f$ distance between \p x and \p y is defined, 222 stores an approximation of it into \p r and returns <CODE>true</CODE>; 223 returns <CODE>false</CODE> otherwise. 224 225 The direction of the approximation is specified by \p dir. 226 227 All computations are performed using variables of type 228 <CODE>Checked_Number\<Temp, Extended_Number_Policy\></CODE>. 229 */ 230 template <typename Temp, typename To, typename ITV> 231 bool 232 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 233 const Box<ITV>& x, 234 const Box<ITV>& y, 235 Rounding_Dir dir); 236 237 //! Computes the \f$L_\infty\f$ distance between \p x and \p y. 238 /*! \relates Box 239 If the \f$L_\infty\f$ distance between \p x and \p y is defined, 240 stores an approximation of it into \p r and returns <CODE>true</CODE>; 241 returns <CODE>false</CODE> otherwise. 242 243 The direction of the approximation is specified by \p dir. 244 245 All computations are performed using the temporary variables 246 \p tmp0, \p tmp1 and \p tmp2. 247 */ 248 template <typename Temp, typename To, typename ITV> 249 bool 250 l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 251 const Box<ITV>& x, 252 const Box<ITV>& y, 253 Rounding_Dir dir, 254 Temp& tmp0, 255 Temp& tmp1, 256 Temp& tmp2); 257 258 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 259 /*! \relates Box 260 Helper function for computing distances. 261 */ 262 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 263 template <typename Specialization, 264 typename Temp, typename To, typename ITV> 265 bool 266 l_m_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 267 const Box<ITV>& x, const Box<ITV>& y, 268 Rounding_Dir dir, 269 Temp& tmp0, Temp& tmp1, Temp& tmp2); 270 271 } // namespace Parma_Polyhedra_Library 272 273 //! A not necessarily closed, iso-oriented hyperrectangle. 274 /*! \ingroup PPL_CXX_interface 275 A Box object represents the smash product of \f$n\f$ 276 not necessarily closed and possibly unbounded intervals 277 represented by objects of class \p ITV, 278 where \f$n\f$ is the space dimension of the box. 279 280 An <EM>interval constraint</EM> (resp., <EM>interval congruence</EM>) 281 is a syntactic constraint (resp., congruence) that only mentions 282 a single space dimension. 283 284 The Box domain <EM>optimally supports</EM>: 285 - tautological and inconsistent constraints and congruences; 286 - the interval constraints that are optimally supported by 287 the template argument class \c ITV; 288 - the interval congruences that are optimally supported by 289 the template argument class \c ITV. 290 291 Depending on the method, using a constraint or congruence that is not 292 optimally supported by the domain will either raise an exception or 293 result in a (possibly non-optimal) upward approximation. 294 295 The user interface for the Box domain is meant to be as similar 296 as possible to the one developed for the polyhedron class C_Polyhedron. 297 */ 298 template <typename ITV> 299 class Parma_Polyhedra_Library::Box { 300 public: 301 //! The type of intervals used to implement the box. 302 typedef ITV interval_type; 303 304 //! Returns the maximum space dimension that a Box can handle. 305 static dimension_type max_space_dimension(); 306 307 /*! \brief 308 Returns false indicating that this domain does not recycle constraints 309 */ 310 static bool can_recycle_constraint_systems(); 311 312 /*! \brief 313 Returns false indicating that this domain does not recycle congruences 314 */ 315 static bool can_recycle_congruence_systems(); 316 317 //! \name Constructors, Assignment, Swap and Destructor 318 //@{ 319 320 //! Builds a universe or empty box of the specified space dimension. 321 /*! 322 \param num_dimensions 323 The number of dimensions of the vector space enclosing the box; 324 325 \param kind 326 Specifies whether the universe or the empty box has to be built. 327 */ 328 explicit Box(dimension_type num_dimensions = 0, 329 Degenerate_Element kind = UNIVERSE); 330 331 //! Ordinary copy constructor. 332 /*! 333 The complexity argument is ignored. 334 */ 335 Box(const Box& y, 336 Complexity_Class complexity = ANY_COMPLEXITY); 337 338 //! Builds a conservative, upward approximation of \p y. 339 /*! 340 The complexity argument is ignored. 341 */ 342 template <typename Other_ITV> 343 explicit Box(const Box<Other_ITV>& y, 344 Complexity_Class complexity = ANY_COMPLEXITY); 345 346 //! Builds a box from the system of constraints \p cs. 347 /*! 348 The box inherits the space dimension of \p cs. 349 350 \param cs 351 A system of constraints: constraints that are not 352 \ref intervals "interval constraints" 353 are ignored (even though they may have contributed 354 to the space dimension). 355 */ 356 explicit Box(const Constraint_System& cs); 357 358 //! Builds a box recycling a system of constraints \p cs. 359 /*! 360 The box inherits the space dimension of \p cs. 361 362 \param cs 363 A system of constraints: constraints that are not 364 \ref intervals "interval constraints" 365 are ignored (even though they may have contributed 366 to the space dimension). 367 368 \param dummy 369 A dummy tag to syntactically differentiate this one 370 from the other constructors. 371 */ 372 Box(const Constraint_System& cs, Recycle_Input dummy); 373 374 //! Builds a box from the system of generators \p gs. 375 /*! 376 Builds the smallest box containing the polyhedron defined by \p gs. 377 The box inherits the space dimension of \p gs. 378 379 \exception std::invalid_argument 380 Thrown if the system of generators is not empty but has no points. 381 */ 382 explicit Box(const Generator_System& gs); 383 384 //! Builds a box recycling the system of generators \p gs. 385 /*! 386 Builds the smallest box containing the polyhedron defined by \p gs. 387 The box inherits the space dimension of \p gs. 388 389 \param gs 390 The generator system describing the polyhedron to be approximated. 391 392 \param dummy 393 A dummy tag to syntactically differentiate this one 394 from the other constructors. 395 396 \exception std::invalid_argument 397 Thrown if the system of generators is not empty but has no points. 398 */ 399 Box(const Generator_System& gs, Recycle_Input dummy); 400 401 /*! 402 Builds the smallest box containing the grid defined by a 403 system of congruences \p cgs. 404 The box inherits the space dimension of \p cgs. 405 406 \param cgs 407 A system of congruences: congruences that are not 408 non-relational equality constraints are ignored 409 (though they may have contributed to the space dimension). 410 */ 411 explicit Box(const Congruence_System& cgs); 412 413 /*! 414 Builds the smallest box containing the grid defined by a 415 system of congruences \p cgs, recycling \p cgs. 416 The box inherits the space dimension of \p cgs. 417 418 \param cgs 419 A system of congruences: congruences that are not 420 non-relational equality constraints are ignored 421 (though they will contribute to the space dimension). 422 423 \param dummy 424 A dummy tag to syntactically differentiate this one 425 from the other constructors. 426 */ 427 Box(const Congruence_System& cgs, Recycle_Input dummy); 428 429 //! Builds a box containing the BDS \p bds. 430 /*! 431 Builds the smallest box containing \p bds using a polynomial algorithm. 432 The \p complexity argument is ignored. 433 */ 434 template <typename T> 435 explicit Box(const BD_Shape<T>& bds, 436 Complexity_Class complexity = POLYNOMIAL_COMPLEXITY); 437 438 //! Builds a box containing the octagonal shape \p oct. 439 /*! 440 Builds the smallest box containing \p oct using a polynomial algorithm. 441 The \p complexity argument is ignored. 442 */ 443 template <typename T> 444 explicit Box(const Octagonal_Shape<T>& oct, 445 Complexity_Class complexity = POLYNOMIAL_COMPLEXITY); 446 447 //! Builds a box containing the polyhedron \p ph. 448 /*! 449 Builds a box containing \p ph using algorithms whose complexity 450 does not exceed the one specified by \p complexity. If 451 \p complexity is \p ANY_COMPLEXITY, then the built box is the 452 smallest one containing \p ph. 453 */ 454 explicit Box(const Polyhedron& ph, 455 Complexity_Class complexity = ANY_COMPLEXITY); 456 457 //! Builds a box containing the grid \p gr. 458 /*! 459 Builds the smallest box containing \p gr using a polynomial algorithm. 460 The \p complexity argument is ignored. 461 */ 462 explicit Box(const Grid& gr, 463 Complexity_Class complexity = POLYNOMIAL_COMPLEXITY); 464 465 //! Builds a box containing the partially reduced product \p dp. 466 /*! 467 Builds a box containing \p ph using algorithms whose complexity 468 does not exceed the one specified by \p complexity. 469 */ 470 template <typename D1, typename D2, typename R> 471 explicit Box(const Partially_Reduced_Product<D1, D2, R>& dp, 472 Complexity_Class complexity = ANY_COMPLEXITY); 473 474 /*! \brief 475 The assignment operator 476 (\p *this and \p y can be dimension-incompatible). 477 */ 478 Box& operator=(const Box& y); 479 480 /*! \brief 481 Swaps \p *this with \p y 482 (\p *this and \p y can be dimension-incompatible). 483 */ 484 void m_swap(Box& y); 485 486 //@} Constructors, Assignment, Swap and Destructor 487 488 //! \name Member Functions that Do Not Modify the Box 489 //@{ 490 491 //! Returns the dimension of the vector space enclosing \p *this. 492 dimension_type space_dimension() const; 493 494 /*! \brief 495 Returns \f$0\f$, if \p *this is empty; otherwise, returns the 496 \ref Affine_Independence_and_Affine_Dimension "affine dimension" 497 of \p *this. 498 */ 499 dimension_type affine_dimension() const; 500 501 //! Returns <CODE>true</CODE> if and only if \p *this is an empty box. 502 bool is_empty() const; 503 504 //! Returns <CODE>true</CODE> if and only if \p *this is a universe box. 505 bool is_universe() const; 506 507 /*! \brief 508 Returns <CODE>true</CODE> if and only if \p *this 509 is a topologically closed subset of the vector space. 510 */ 511 bool is_topologically_closed() const; 512 513 //! Returns <CODE>true</CODE> if and only if \p *this is discrete. 514 bool is_discrete() const; 515 516 //! Returns <CODE>true</CODE> if and only if \p *this is a bounded box. 517 bool is_bounded() const; 518 519 /*! \brief 520 Returns <CODE>true</CODE> if and only if \p *this 521 contains at least one integer point. 522 */ 523 bool contains_integer_point() const; 524 525 /*! \brief 526 Returns <CODE>true</CODE> if and only if \p var is constrained in 527 \p *this. 528 529 \exception std::invalid_argument 530 Thrown if \p var is not a space dimension of \p *this. 531 */ 532 bool constrains(Variable var) const; 533 534 //! Returns the relations holding between \p *this and the constraint \p c. 535 /*! 536 \exception std::invalid_argument 537 Thrown if \p *this and constraint \p c are dimension-incompatible. 538 */ 539 Poly_Con_Relation relation_with(const Constraint& c) const; 540 541 //! Returns the relations holding between \p *this and the congruence \p cg. 542 /*! 543 \exception std::invalid_argument 544 Thrown if \p *this and constraint \p cg are dimension-incompatible. 545 */ 546 Poly_Con_Relation relation_with(const Congruence& cg) const; 547 548 //! Returns the relations holding between \p *this and the generator \p g. 549 /*! 550 \exception std::invalid_argument 551 Thrown if \p *this and generator \p g are dimension-incompatible. 552 */ 553 Poly_Gen_Relation relation_with(const Generator& g) const; 554 555 /*! \brief 556 Returns <CODE>true</CODE> if and only if \p expr is 557 bounded from above in \p *this. 558 559 \exception std::invalid_argument 560 Thrown if \p expr and \p *this are dimension-incompatible. 561 */ 562 bool bounds_from_above(const Linear_Expression& expr) const; 563 564 /*! \brief 565 Returns <CODE>true</CODE> if and only if \p expr is 566 bounded from below in \p *this. 567 568 \exception std::invalid_argument 569 Thrown if \p expr and \p *this are dimension-incompatible. 570 */ 571 bool bounds_from_below(const Linear_Expression& expr) const; 572 573 /*! \brief 574 Returns <CODE>true</CODE> if and only if \p *this is not empty 575 and \p expr is bounded from above in \p *this, in which case 576 the supremum value is computed. 577 578 \param expr 579 The linear expression to be maximized subject to \p *this; 580 581 \param sup_n 582 The numerator of the supremum value; 583 584 \param sup_d 585 The denominator of the supremum value; 586 587 \param maximum 588 <CODE>true</CODE> if and only if the supremum is also the maximum value. 589 590 \exception std::invalid_argument 591 Thrown if \p expr and \p *this are dimension-incompatible. 592 593 If \p *this is empty or \p expr is not bounded from above, 594 <CODE>false</CODE> is returned and \p sup_n, \p sup_d 595 and \p maximum are left untouched. 596 */ 597 bool maximize(const Linear_Expression& expr, 598 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const; 599 600 /*! \brief 601 Returns <CODE>true</CODE> if and only if \p *this is not empty 602 and \p expr is bounded from above in \p *this, in which case 603 the supremum value and a point where \p expr reaches it are computed. 604 605 \param expr 606 The linear expression to be maximized subject to \p *this; 607 608 \param sup_n 609 The numerator of the supremum value; 610 611 \param sup_d 612 The denominator of the supremum value; 613 614 \param maximum 615 <CODE>true</CODE> if and only if the supremum is also the maximum value; 616 617 \param g 618 When maximization succeeds, will be assigned the point or 619 closure point where \p expr reaches its supremum value. 620 621 \exception std::invalid_argument 622 Thrown if \p expr and \p *this are dimension-incompatible. 623 624 If \p *this is empty or \p expr is not bounded from above, 625 <CODE>false</CODE> is returned and \p sup_n, \p sup_d, \p maximum 626 and \p g are left untouched. 627 */ 628 bool maximize(const Linear_Expression& expr, 629 Coefficient& sup_n, Coefficient& sup_d, bool& maximum, 630 Generator& g) const; 631 632 /*! \brief 633 Returns <CODE>true</CODE> if and only if \p *this is not empty 634 and \p expr is bounded from below in \p *this, in which case 635 the infimum value is computed. 636 637 \param expr 638 The linear expression to be minimized subject to \p *this; 639 640 \param inf_n 641 The numerator of the infimum value; 642 643 \param inf_d 644 The denominator of the infimum value; 645 646 \param minimum 647 <CODE>true</CODE> if and only if the infimum is also the minimum value. 648 649 \exception std::invalid_argument 650 Thrown if \p expr and \p *this are dimension-incompatible. 651 652 If \p *this is empty or \p expr is not bounded from below, 653 <CODE>false</CODE> is returned and \p inf_n, \p inf_d 654 and \p minimum are left untouched. 655 */ 656 bool minimize(const Linear_Expression& expr, 657 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const; 658 659 /*! \brief 660 Returns <CODE>true</CODE> if and only if \p *this is not empty 661 and \p expr is bounded from below in \p *this, in which case 662 the infimum value and a point where \p expr reaches it are computed. 663 664 \param expr 665 The linear expression to be minimized subject to \p *this; 666 667 \param inf_n 668 The numerator of the infimum value; 669 670 \param inf_d 671 The denominator of the infimum value; 672 673 \param minimum 674 <CODE>true</CODE> if and only if the infimum is also the minimum value; 675 676 \param g 677 When minimization succeeds, will be assigned a point or 678 closure point where \p expr reaches its infimum value. 679 680 \exception std::invalid_argument 681 Thrown if \p expr and \p *this are dimension-incompatible. 682 683 If \p *this is empty or \p expr is not bounded from below, 684 <CODE>false</CODE> is returned and \p inf_n, \p inf_d, \p minimum 685 and \p g are left untouched. 686 */ 687 bool minimize(const Linear_Expression& expr, 688 Coefficient& inf_n, Coefficient& inf_d, bool& minimum, 689 Generator& g) const; 690 691 /*! \brief 692 Returns <CODE>true</CODE> if and only if there exist a 693 unique value \p val such that \p *this 694 saturates the equality <CODE>expr = val</CODE>. 695 696 \param expr 697 The linear expression for which the frequency is needed; 698 699 \param freq_n 700 If <CODE>true</CODE> is returned, the value is set to \f$0\f$; 701 Present for interface compatibility with class Grid, where 702 the \ref Grid_Frequency "frequency" can have a non-zero value; 703 704 \param freq_d 705 If <CODE>true</CODE> is returned, the value is set to \f$1\f$; 706 707 \param val_n 708 The numerator of \p val; 709 710 \param val_d 711 The denominator of \p val; 712 713 \exception std::invalid_argument 714 Thrown if \p expr and \p *this are dimension-incompatible. 715 716 If <CODE>false</CODE> is returned, then \p freq_n, \p freq_d, 717 \p val_n and \p val_d are left untouched. 718 */ 719 bool frequency(const Linear_Expression& expr, 720 Coefficient& freq_n, Coefficient& freq_d, 721 Coefficient& val_n, Coefficient& val_d) const; 722 723 /*! \brief 724 Returns <CODE>true</CODE> if and only if \p *this contains \p y. 725 726 \exception std::invalid_argument 727 Thrown if \p x and \p y are dimension-incompatible. 728 */ 729 bool contains(const Box& y) const; 730 731 /*! \brief 732 Returns <CODE>true</CODE> if and only if \p *this strictly contains \p y. 733 734 \exception std::invalid_argument 735 Thrown if \p x and \p y are dimension-incompatible. 736 */ 737 bool strictly_contains(const Box& y) const; 738 739 /*! \brief 740 Returns <CODE>true</CODE> if and only if \p *this and \p y are disjoint. 741 742 \exception std::invalid_argument 743 Thrown if \p x and \p y are dimension-incompatible. 744 */ 745 bool is_disjoint_from(const Box& y) const; 746 747 /*! \brief 748 Returns <CODE>true</CODE> if and only if \p *this satisfies 749 all its invariants. 750 */ 751 bool OK() const; 752 753 //@} Member Functions that Do Not Modify the Box 754 755 //! \name Space-Dimension Preserving Member Functions that May Modify the Box 756 //@{ 757 758 /*! \brief 759 Adds a copy of constraint \p c to the system of constraints 760 defining \p *this. 761 762 \param c 763 The constraint to be added. 764 765 \exception std::invalid_argument 766 Thrown if \p *this and constraint \p c are dimension-incompatible, 767 or \p c is not optimally supported by the Box domain. 768 */ 769 void add_constraint(const Constraint& c); 770 771 /*! \brief 772 Adds the constraints in \p cs to the system of constraints 773 defining \p *this. 774 775 \param cs 776 The constraints to be added. 777 778 \exception std::invalid_argument 779 Thrown if \p *this and \p cs are dimension-incompatible, 780 or \p cs contains a constraint which is not optimally supported 781 by the box domain. 782 */ 783 void add_constraints(const Constraint_System& cs); 784 785 /*! \brief 786 Adds the constraints in \p cs to the system of constraints 787 defining \p *this. 788 789 \param cs 790 The constraints to be added. They may be recycled. 791 792 \exception std::invalid_argument 793 Thrown if \p *this and \p cs are dimension-incompatible, 794 or \p cs contains a constraint which is not optimally supported 795 by the box domain. 796 797 \warning 798 The only assumption that can be made on \p cs upon successful or 799 exceptional return is that it can be safely destroyed. 800 */ 801 void add_recycled_constraints(Constraint_System& cs); 802 803 /*! \brief 804 Adds to \p *this a constraint equivalent to the congruence \p cg. 805 806 \param cg 807 The congruence to be added. 808 809 \exception std::invalid_argument 810 Thrown if \p *this and congruence \p cg are dimension-incompatible, 811 or \p cg is not optimally supported by the box domain. 812 */ 813 void add_congruence(const Congruence& cg); 814 815 /*! \brief 816 Adds to \p *this constraints equivalent to the congruences in \p cgs. 817 818 \param cgs 819 The congruences to be added. 820 821 \exception std::invalid_argument 822 Thrown if \p *this and \p cgs are dimension-incompatible, 823 or \p cgs contains a congruence which is not optimally supported 824 by the box domain. 825 */ 826 void add_congruences(const Congruence_System& cgs); 827 828 /*! \brief 829 Adds to \p *this constraints equivalent to the congruences in \p cgs. 830 831 \param cgs 832 The congruence system to be added to \p *this. The congruences in 833 \p cgs may be recycled. 834 835 \exception std::invalid_argument 836 Thrown if \p *this and \p cgs are dimension-incompatible, 837 or \p cgs contains a congruence which is not optimally supported 838 by the box domain. 839 840 \warning 841 The only assumption that can be made on \p cgs upon successful or 842 exceptional return is that it can be safely destroyed. 843 */ 844 void add_recycled_congruences(Congruence_System& cgs); 845 846 /*! \brief 847 Use the constraint \p c to refine \p *this. 848 849 \param c 850 The constraint to be used for refinement. 851 852 \exception std::invalid_argument 853 Thrown if \p *this and \p c are dimension-incompatible. 854 */ 855 void refine_with_constraint(const Constraint& c); 856 857 /*! \brief 858 Use the constraints in \p cs to refine \p *this. 859 860 \param cs 861 The constraints to be used for refinement. 862 To avoid termination problems, each constraint in \p cs 863 will be used for a single refinement step. 864 865 \exception std::invalid_argument 866 Thrown if \p *this and \p cs are dimension-incompatible. 867 868 \note 869 The user is warned that the accuracy of this refinement operator 870 depends on the order of evaluation of the constraints in \p cs, 871 which is in general unpredictable. If a fine control on such an 872 order is needed, the user should consider calling the method 873 <code>refine_with_constraint(const Constraint& c)</code> inside 874 an appropriate looping construct. 875 */ 876 void refine_with_constraints(const Constraint_System& cs); 877 878 /*! \brief 879 Use the congruence \p cg to refine \p *this. 880 881 \param cg 882 The congruence to be used for refinement. 883 884 \exception std::invalid_argument 885 Thrown if \p *this and \p cg are dimension-incompatible. 886 */ 887 void refine_with_congruence(const Congruence& cg); 888 889 /*! \brief 890 Use the congruences in \p cgs to refine \p *this. 891 892 \param cgs 893 The congruences to be used for refinement. 894 895 \exception std::invalid_argument 896 Thrown if \p *this and \p cgs are dimension-incompatible. 897 */ 898 void refine_with_congruences(const Congruence_System& cgs); 899 900 /*! \brief 901 Use the constraint \p c for constraint propagation on \p *this. 902 903 \param c 904 The constraint to be used for constraint propagation. 905 906 \exception std::invalid_argument 907 Thrown if \p *this and \p c are dimension-incompatible. 908 */ 909 void propagate_constraint(const Constraint& c); 910 911 /*! \brief 912 Use the constraints in \p cs for constraint propagation on \p *this. 913 914 \param cs 915 The constraints to be used for constraint propagation. 916 917 \param max_iterations 918 The maximum number of propagation steps for each constraint in 919 \p cs. If zero (the default), the number of propagation steps 920 will be unbounded, possibly resulting in an infinite loop. 921 922 \exception std::invalid_argument 923 Thrown if \p *this and \p cs are dimension-incompatible. 924 925 \warning 926 This method may lead to non-termination if \p max_iterations is 0. 927 */ 928 void propagate_constraints(const Constraint_System& cs, 929 dimension_type max_iterations = 0); 930 931 /*! \brief 932 Computes the \ref Cylindrification "cylindrification" of \p *this with 933 respect to space dimension \p var, assigning the result to \p *this. 934 935 \param var 936 The space dimension that will be unconstrained. 937 938 \exception std::invalid_argument 939 Thrown if \p var is not a space dimension of \p *this. 940 */ 941 void unconstrain(Variable var); 942 943 /*! \brief 944 Computes the \ref Cylindrification "cylindrification" of \p *this with 945 respect to the set of space dimensions \p vars, 946 assigning the result to \p *this. 947 948 \param vars 949 The set of space dimension that will be unconstrained. 950 951 \exception std::invalid_argument 952 Thrown if \p *this is dimension-incompatible with one of the 953 Variable objects contained in \p vars. 954 */ 955 void unconstrain(const Variables_Set& vars); 956 957 //! Assigns to \p *this the intersection of \p *this and \p y. 958 /*! 959 \exception std::invalid_argument 960 Thrown if \p *this and \p y are dimension-incompatible. 961 */ 962 void intersection_assign(const Box& y); 963 964 /*! \brief 965 Assigns to \p *this the smallest box containing the union 966 of \p *this and \p y. 967 968 \exception std::invalid_argument 969 Thrown if \p *this and \p y are dimension-incompatible. 970 */ 971 void upper_bound_assign(const Box& y); 972 973 /*! \brief 974 If the upper bound of \p *this and \p y is exact, it is assigned 975 to \p *this and <CODE>true</CODE> is returned, 976 otherwise <CODE>false</CODE> is returned. 977 978 \exception std::invalid_argument 979 Thrown if \p *this and \p y are dimension-incompatible. 980 */ 981 bool upper_bound_assign_if_exact(const Box& y); 982 983 /*! \brief 984 Assigns to \p *this the difference of \p *this and \p y. 985 986 \exception std::invalid_argument 987 Thrown if \p *this and \p y are dimension-incompatible. 988 */ 989 void difference_assign(const Box& y); 990 991 /*! \brief 992 Assigns to \p *this a \ref Meet_Preserving_Simplification 993 "meet-preserving simplification" of \p *this with respect to \p y. 994 If \c false is returned, then the intersection is empty. 995 996 \exception std::invalid_argument 997 Thrown if \p *this and \p y are dimension-incompatible. 998 */ 999 bool simplify_using_context_assign(const Box& y); 1000 1001 /*! \brief 1002 Assigns to \p *this the 1003 \ref Single_Update_Affine_Functions "affine image" 1004 of \p *this under the function mapping variable \p var to the 1005 affine expression specified by \p expr and \p denominator. 1006 1007 \param var 1008 The variable to which the affine expression is assigned; 1009 1010 \param expr 1011 The numerator of the affine expression; 1012 1013 \param denominator 1014 The denominator of the affine expression (optional argument with 1015 default value 1). 1016 1017 \exception std::invalid_argument 1018 Thrown if \p denominator is zero or if \p expr and \p *this are 1019 dimension-incompatible or if \p var is not a space dimension of 1020 \p *this. 1021 */ 1022 void affine_image(Variable var, 1023 const Linear_Expression& expr, 1024 Coefficient_traits::const_reference denominator 1025 = Coefficient_one()); 1026 1027 // FIXME: To be completed. 1028 /*! \brief 1029 Assigns to \p *this the \ref affine_form_relation "affine form image" 1030 of \p *this under the function mapping variable \p var into the 1031 affine expression(s) specified by \p lf. 1032 1033 \param var 1034 The variable to which the affine expression is assigned. 1035 1036 \param lf 1037 The linear form on intervals with floating point boundaries that 1038 defines the affine expression(s). ALL of its coefficients MUST be bounded. 1039 1040 \exception std::invalid_argument 1041 Thrown if \p lf and \p *this are dimension-incompatible or if \p var 1042 is not a dimension of \p *this. 1043 1044 This function is used in abstract interpretation to model an assignment 1045 of a value that is correctly overapproximated by \p lf to the 1046 floating point variable represented by \p var. 1047 */ 1048 void affine_form_image(Variable var, 1049 const Linear_Form<ITV>& lf); 1050 1051 /*! \brief 1052 Assigns to \p *this the 1053 \ref Single_Update_Affine_Functions "affine preimage" 1054 of \p *this under the function mapping variable \p var to the 1055 affine expression specified by \p expr and \p denominator. 1056 1057 \param var 1058 The variable to which the affine expression is substituted; 1059 1060 \param expr 1061 The numerator of the affine expression; 1062 1063 \param denominator 1064 The denominator of the affine expression (optional argument with 1065 default value 1). 1066 1067 \exception std::invalid_argument 1068 Thrown if \p denominator is zero or if \p expr and \p *this are 1069 dimension-incompatible or if \p var is not a space dimension of \p *this. 1070 */ 1071 void affine_preimage(Variable var, 1072 const Linear_Expression& expr, 1073 Coefficient_traits::const_reference denominator 1074 = Coefficient_one()); 1075 1076 /*! \brief 1077 Assigns to \p *this the image of \p *this with respect to the 1078 \ref Generalized_Affine_Relations "generalized affine relation" 1079 \f$\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}\f$, 1080 where \f$\mathord{\relsym}\f$ is the relation symbol encoded 1081 by \p relsym. 1082 1083 \param var 1084 The left hand side variable of the generalized affine relation; 1085 1086 \param relsym 1087 The relation symbol; 1088 1089 \param expr 1090 The numerator of the right hand side affine expression; 1091 1092 \param denominator 1093 The denominator of the right hand side affine expression (optional 1094 argument with default value 1). 1095 1096 \exception std::invalid_argument 1097 Thrown if \p denominator is zero or if \p expr and \p *this are 1098 dimension-incompatible or if \p var is not a space dimension of \p *this. 1099 */ 1100 void generalized_affine_image(Variable var, 1101 Relation_Symbol relsym, 1102 const Linear_Expression& expr, 1103 Coefficient_traits::const_reference denominator 1104 = Coefficient_one()); 1105 1106 /*! \brief 1107 Assigns to \p *this the preimage of \p *this with respect to the 1108 \ref Generalized_Affine_Relations "generalized affine relation" 1109 \f$\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}\f$, 1110 where \f$\mathord{\relsym}\f$ is the relation symbol encoded 1111 by \p relsym. 1112 1113 \param var 1114 The left hand side variable of the generalized affine relation; 1115 1116 \param relsym 1117 The relation symbol; 1118 1119 \param expr 1120 The numerator of the right hand side affine expression; 1121 1122 \param denominator 1123 The denominator of the right hand side affine expression (optional 1124 argument with default value 1). 1125 1126 \exception std::invalid_argument 1127 Thrown if \p denominator is zero or if \p expr and \p *this are 1128 dimension-incompatible or if \p var is not a space dimension of \p *this. 1129 */ 1130 void 1131 generalized_affine_preimage(Variable var, 1132 Relation_Symbol relsym, 1133 const Linear_Expression& expr, 1134 Coefficient_traits::const_reference denominator 1135 = Coefficient_one()); 1136 1137 /*! \brief 1138 Assigns to \p *this the image of \p *this with respect to the 1139 \ref Generalized_Affine_Relations "generalized affine relation" 1140 \f$\mathrm{lhs}' \relsym \mathrm{rhs}\f$, where 1141 \f$\mathord{\relsym}\f$ is the relation symbol encoded by \p relsym. 1142 1143 \param lhs 1144 The left hand side affine expression; 1145 1146 \param relsym 1147 The relation symbol; 1148 1149 \param rhs 1150 The right hand side affine expression. 1151 1152 \exception std::invalid_argument 1153 Thrown if \p *this is dimension-incompatible with \p lhs or \p rhs. 1154 */ 1155 void generalized_affine_image(const Linear_Expression& lhs, 1156 Relation_Symbol relsym, 1157 const Linear_Expression& rhs); 1158 1159 /*! \brief 1160 Assigns to \p *this the preimage of \p *this with respect to the 1161 \ref Generalized_Affine_Relations "generalized affine relation" 1162 \f$\mathrm{lhs}' \relsym \mathrm{rhs}\f$, where 1163 \f$\mathord{\relsym}\f$ is the relation symbol encoded by \p relsym. 1164 1165 \param lhs 1166 The left hand side affine expression; 1167 1168 \param relsym 1169 The relation symbol; 1170 1171 \param rhs 1172 The right hand side affine expression. 1173 1174 \exception std::invalid_argument 1175 Thrown if \p *this is dimension-incompatible with \p lhs or \p rhs. 1176 */ 1177 void generalized_affine_preimage(const Linear_Expression& lhs, 1178 Relation_Symbol relsym, 1179 const Linear_Expression& rhs); 1180 1181 /*! \brief 1182 Assigns to \p *this the image of \p *this with respect to the 1183 \ref Single_Update_Bounded_Affine_Relations "bounded affine relation" 1184 \f$\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} 1185 \leq \mathrm{var}' 1186 \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}\f$. 1187 1188 \param var 1189 The variable updated by the affine relation; 1190 1191 \param lb_expr 1192 The numerator of the lower bounding affine expression; 1193 1194 \param ub_expr 1195 The numerator of the upper bounding affine expression; 1196 1197 \param denominator 1198 The (common) denominator for the lower and upper bounding 1199 affine expressions (optional argument with default value 1). 1200 1201 \exception std::invalid_argument 1202 Thrown if \p denominator is zero or if \p lb_expr (resp., \p ub_expr) 1203 and \p *this are dimension-incompatible or if \p var is not a space 1204 dimension of \p *this. 1205 */ 1206 void bounded_affine_image(Variable var, 1207 const Linear_Expression& lb_expr, 1208 const Linear_Expression& ub_expr, 1209 Coefficient_traits::const_reference denominator 1210 = Coefficient_one()); 1211 1212 /*! \brief 1213 Assigns to \p *this the preimage of \p *this with respect to the 1214 \ref Single_Update_Bounded_Affine_Relations "bounded affine relation" 1215 \f$\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} 1216 \leq \mathrm{var}' 1217 \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}\f$. 1218 1219 \param var 1220 The variable updated by the affine relation; 1221 1222 \param lb_expr 1223 The numerator of the lower bounding affine expression; 1224 1225 \param ub_expr 1226 The numerator of the upper bounding affine expression; 1227 1228 \param denominator 1229 The (common) denominator for the lower and upper bounding 1230 affine expressions (optional argument with default value 1). 1231 1232 \exception std::invalid_argument 1233 Thrown if \p denominator is zero or if \p lb_expr (resp., \p ub_expr) 1234 and \p *this are dimension-incompatible or if \p var is not a space 1235 dimension of \p *this. 1236 */ 1237 void bounded_affine_preimage(Variable var, 1238 const Linear_Expression& lb_expr, 1239 const Linear_Expression& ub_expr, 1240 Coefficient_traits::const_reference denominator 1241 = Coefficient_one()); 1242 1243 /*! \brief 1244 Assigns to \p *this the result of computing the 1245 \ref Time_Elapse_Operator "time-elapse" between \p *this and \p y. 1246 1247 \exception std::invalid_argument 1248 Thrown if \p *this and \p y are dimension-incompatible. 1249 */ 1250 void time_elapse_assign(const Box& y); 1251 1252 //! Assigns to \p *this its topological closure. 1253 void topological_closure_assign(); 1254 1255 /*! \brief 1256 \ref Wrapping_Operator "Wraps" the specified dimensions of the 1257 vector space. 1258 1259 \param vars 1260 The set of Variable objects corresponding to the space dimensions 1261 to be wrapped. 1262 1263 \param w 1264 The width of the bounded integer type corresponding to 1265 all the dimensions to be wrapped. 1266 1267 \param r 1268 The representation of the bounded integer type corresponding to 1269 all the dimensions to be wrapped. 1270 1271 \param o 1272 The overflow behavior of the bounded integer type corresponding to 1273 all the dimensions to be wrapped. 1274 1275 \param cs_p 1276 Possibly null pointer to a constraint system. When non-null, 1277 the pointed-to constraint system is assumed to represent the 1278 conditional or looping construct guard with respect to which 1279 wrapping is performed. Since wrapping requires the computation 1280 of upper bounds and due to non-distributivity of constraint 1281 refinement over upper bounds, passing a constraint system in this 1282 way can be more precise than refining the result of the wrapping 1283 operation with the constraints in <CODE>*cs_p</CODE>. 1284 1285 \param complexity_threshold 1286 A precision parameter which is ignored for the Box domain. 1287 1288 \param wrap_individually 1289 A precision parameter which is ignored for the Box domain. 1290 1291 \exception std::invalid_argument 1292 Thrown if \p *this is dimension-incompatible with one of the 1293 Variable objects contained in \p vars or with <CODE>*cs_p</CODE>. 1294 */ 1295 void wrap_assign(const Variables_Set& vars, 1296 Bounded_Integer_Type_Width w, 1297 Bounded_Integer_Type_Representation r, 1298 Bounded_Integer_Type_Overflow o, 1299 const Constraint_System* cs_p = 0, 1300 unsigned complexity_threshold = 16, 1301 bool wrap_individually = true); 1302 1303 /*! \brief 1304 Possibly tightens \p *this by dropping some points with non-integer 1305 coordinates. 1306 1307 \param complexity 1308 The maximal complexity of any algorithms used. 1309 1310 \note 1311 Currently there is no optimality guarantee, not even if 1312 \p complexity is <CODE>ANY_COMPLEXITY</CODE>. 1313 */ 1314 void drop_some_non_integer_points(Complexity_Class complexity 1315 = ANY_COMPLEXITY); 1316 1317 /*! \brief 1318 Possibly tightens \p *this by dropping some points with non-integer 1319 coordinates for the space dimensions corresponding to \p vars. 1320 1321 \param vars 1322 Points with non-integer coordinates for these variables/space-dimensions 1323 can be discarded. 1324 1325 \param complexity 1326 The maximal complexity of any algorithms used. 1327 1328 \note 1329 Currently there is no optimality guarantee, not even if 1330 \p complexity is <CODE>ANY_COMPLEXITY</CODE>. 1331 */ 1332 void drop_some_non_integer_points(const Variables_Set& vars, 1333 Complexity_Class complexity 1334 = ANY_COMPLEXITY); 1335 1336 /*! \brief 1337 Assigns to \p *this the result of computing the 1338 \ref CC76_extrapolation "CC76-widening" between \p *this and \p y. 1339 1340 \param y 1341 A box that <EM>must</EM> be contained in \p *this. 1342 1343 \param tp 1344 An optional pointer to an unsigned variable storing the number of 1345 available tokens (to be used when applying the 1346 \ref Widening_with_Tokens "widening with tokens" delay technique). 1347 1348 \exception std::invalid_argument 1349 Thrown if \p *this and \p y are dimension-incompatible. 1350 */ 1351 template <typename T> 1352 typename Enable_If<Is_Same<T, Box>::value 1353 && Is_Same_Or_Derived<Interval_Base, ITV>::value, 1354 void>::type 1355 CC76_widening_assign(const T& y, unsigned* tp = 0); 1356 1357 /*! \brief 1358 Assigns to \p *this the result of computing the 1359 \ref CC76_extrapolation "CC76-widening" between \p *this and \p y. 1360 1361 \param y 1362 A box that <EM>must</EM> be contained in \p *this. 1363 1364 \param first 1365 An iterator that points to the first stop-point. 1366 1367 \param last 1368 An iterator that points one past the last stop-point. 1369 1370 \exception std::invalid_argument 1371 Thrown if \p *this and \p y are dimension-incompatible. 1372 */ 1373 template <typename T, typename Iterator> 1374 typename Enable_If<Is_Same<T, Box>::value 1375 && Is_Same_Or_Derived<Interval_Base, ITV>::value, 1376 void>::type 1377 CC76_widening_assign(const T& y, 1378 Iterator first, Iterator last); 1379 1380 //! Same as CC76_widening_assign(y, tp). 1381 void widening_assign(const Box& y, unsigned* tp = 0); 1382 1383 /*! \brief 1384 Improves the result of the \ref CC76_extrapolation "CC76-extrapolation" 1385 computation by also enforcing those constraints in \p cs that are 1386 satisfied by all the points of \p *this. 1387 1388 \param y 1389 A box that <EM>must</EM> be contained in \p *this. 1390 1391 \param cs 1392 The system of constraints used to improve the widened box. 1393 1394 \param tp 1395 An optional pointer to an unsigned variable storing the number of 1396 available tokens (to be used when applying the 1397 \ref Widening_with_Tokens "widening with tokens" delay technique). 1398 1399 \exception std::invalid_argument 1400 Thrown if \p *this, \p y and \p cs are dimension-incompatible or 1401 if \p cs contains a strict inequality. 1402 */ 1403 void limited_CC76_extrapolation_assign(const Box& y, 1404 const Constraint_System& cs, 1405 unsigned* tp = 0); 1406 1407 /*! \brief 1408 Assigns to \p *this the result of restoring in \p y the constraints 1409 of \p *this that were lost by 1410 \ref CC76_extrapolation "CC76-extrapolation" applications. 1411 1412 \param y 1413 A Box that <EM>must</EM> contain \p *this. 1414 1415 \exception std::invalid_argument 1416 Thrown if \p *this and \p y are dimension-incompatible. 1417 1418 \note 1419 As was the case for widening operators, the argument \p y is meant to 1420 denote the value computed in the previous iteration step, whereas 1421 \p *this denotes the value computed in the current iteration step 1422 (in the <EM>decreasing</EM> iteration sequence). Hence, the call 1423 <CODE>x.CC76_narrowing_assign(y)</CODE> will assign to \p x 1424 the result of the computation \f$\mathtt{y} \Delta \mathtt{x}\f$. 1425 */ 1426 template <typename T> 1427 typename Enable_If<Is_Same<T, Box>::value 1428 && Is_Same_Or_Derived<Interval_Base, ITV>::value, 1429 void>::type 1430 CC76_narrowing_assign(const T& y); 1431 1432 //@} Space-Dimension Preserving Member Functions that May Modify [...] 1433 1434 //! \name Member Functions that May Modify the Dimension of the Vector Space 1435 //@{ 1436 1437 //! Adds \p m new dimensions and embeds the old box into the new space. 1438 /*! 1439 \param m 1440 The number of dimensions to add. 1441 1442 The new dimensions will be those having the highest indexes in the new 1443 box, which is defined by a system of interval constraints in which the 1444 variables running through the new dimensions are unconstrained. 1445 For instance, when starting from the box \f$\cB \sseq \Rset^2\f$ 1446 and adding a third dimension, the result will be the box 1447 \f[ 1448 \bigl\{\, 1449 (x, y, z)^\transpose \in \Rset^3 1450 \bigm| 1451 (x, y)^\transpose \in \cB 1452 \,\bigr\}. 1453 \f] 1454 */ 1455 void add_space_dimensions_and_embed(dimension_type m); 1456 1457 /*! \brief 1458 Adds \p m new dimensions to the box and does not embed it in 1459 the new vector space. 1460 1461 \param m 1462 The number of dimensions to add. 1463 1464 The new dimensions will be those having the highest indexes in the 1465 new box, which is defined by a system of bounded differences in 1466 which the variables running through the new dimensions are all 1467 constrained to be equal to 0. 1468 For instance, when starting from the box \f$\cB \sseq \Rset^2\f$ 1469 and adding a third dimension, the result will be the box 1470 \f[ 1471 \bigl\{\, 1472 (x, y, 0)^\transpose \in \Rset^3 1473 \bigm| 1474 (x, y)^\transpose \in \cB 1475 \,\bigr\}. 1476 \f] 1477 */ 1478 void add_space_dimensions_and_project(dimension_type m); 1479 1480 /*! \brief 1481 Seeing a box as a set of tuples (its points), 1482 assigns to \p *this all the tuples that can be obtained by concatenating, 1483 in the order given, a tuple of \p *this with a tuple of \p y. 1484 1485 Let \f$B \sseq \Rset^n\f$ and \f$D \sseq \Rset^m\f$ be the boxes 1486 corresponding, on entry, to \p *this and \p y, respectively. 1487 Upon successful completion, \p *this will represent the box 1488 \f$R \sseq \Rset^{n+m}\f$ such that 1489 \f[ 1490 R \defeq 1491 \Bigl\{\, 1492 (x_1, \ldots, x_n, y_1, \ldots, y_m)^\transpose 1493 \Bigm| 1494 (x_1, \ldots, x_n)^\transpose \in B, 1495 (y_1, \ldots, y_m)^\transpose \in D 1496 \,\Bigl\}. 1497 \f] 1498 Another way of seeing it is as follows: first increases the space 1499 dimension of \p *this by adding \p y.space_dimension() new 1500 dimensions; then adds to the system of constraints of \p *this a 1501 renamed-apart version of the constraints of \p y. 1502 */ 1503 void concatenate_assign(const Box& y); 1504 1505 //! Removes all the specified dimensions. 1506 /*! 1507 \param vars 1508 The set of Variable objects corresponding to the dimensions to be removed. 1509 1510 \exception std::invalid_argument 1511 Thrown if \p *this is dimension-incompatible with one of the Variable 1512 objects contained in \p vars. 1513 */ 1514 void remove_space_dimensions(const Variables_Set& vars); 1515 1516 /*! \brief 1517 Removes the higher dimensions so that the resulting space 1518 will have dimension \p new_dimension. 1519 1520 \exception std::invalid_argument 1521 Thrown if \p new_dimension is greater than the space dimension 1522 of \p *this. 1523 */ 1524 void remove_higher_space_dimensions(dimension_type new_dimension); 1525 1526 /*! \brief 1527 Remaps the dimensions of the vector space according to 1528 a \ref Mapping_the_Dimensions_of_the_Vector_Space "partial function". 1529 1530 \param pfunc 1531 The partial function specifying the destiny of each dimension. 1532 1533 The template type parameter Partial_Function must provide 1534 the following methods. 1535 \code 1536 bool has_empty_codomain() const 1537 \endcode 1538 returns <CODE>true</CODE> if and only if the represented partial 1539 function has an empty co-domain (i.e., it is always undefined). 1540 The <CODE>has_empty_codomain()</CODE> method will always be called 1541 before the methods below. However, if 1542 <CODE>has_empty_codomain()</CODE> returns <CODE>true</CODE>, none 1543 of the functions below will be called. 1544 \code 1545 dimension_type max_in_codomain() const 1546 \endcode 1547 returns the maximum value that belongs to the co-domain 1548 of the partial function. 1549 \code 1550 bool maps(dimension_type i, dimension_type& j) const 1551 \endcode 1552 Let \f$f\f$ be the represented function and \f$k\f$ be the value 1553 of \p i. If \f$f\f$ is defined in \f$k\f$, then \f$f(k)\f$ is 1554 assigned to \p j and <CODE>true</CODE> is returned. 1555 If \f$f\f$ is undefined in \f$k\f$, then <CODE>false</CODE> is 1556 returned. 1557 1558 The result is undefined if \p pfunc does not encode a partial 1559 function with the properties described in the 1560 \ref Mapping_the_Dimensions_of_the_Vector_Space 1561 "specification of the mapping operator". 1562 */ 1563 template <typename Partial_Function> 1564 void map_space_dimensions(const Partial_Function& pfunc); 1565 1566 //! Creates \p m copies of the space dimension corresponding to \p var. 1567 /*! 1568 \param var 1569 The variable corresponding to the space dimension to be replicated; 1570 1571 \param m 1572 The number of replicas to be created. 1573 1574 \exception std::invalid_argument 1575 Thrown if \p var does not correspond to a dimension of the vector space. 1576 1577 \exception std::length_error 1578 Thrown if adding \p m new space dimensions would cause the 1579 vector space to exceed dimension <CODE>max_space_dimension()</CODE>. 1580 1581 If \p *this has space dimension \f$n\f$, with \f$n > 0\f$, 1582 and <CODE>var</CODE> has space dimension \f$k \leq n\f$, 1583 then the \f$k\f$-th space dimension is 1584 \ref expand_space_dimension "expanded" to \p m new space dimensions 1585 \f$n\f$, \f$n+1\f$, \f$\dots\f$, \f$n+m-1\f$. 1586 */ 1587 void expand_space_dimension(Variable var, dimension_type m); 1588 1589 //! Folds the space dimensions in \p vars into \p dest. 1590 /*! 1591 \param vars 1592 The set of Variable objects corresponding to the space dimensions 1593 to be folded; 1594 1595 \param dest 1596 The variable corresponding to the space dimension that is the 1597 destination of the folding operation. 1598 1599 \exception std::invalid_argument 1600 Thrown if \p *this is dimension-incompatible with \p dest or with 1601 one of the Variable objects contained in \p vars. 1602 Also thrown if \p dest is contained in \p vars. 1603 1604 If \p *this has space dimension \f$n\f$, with \f$n > 0\f$, 1605 <CODE>dest</CODE> has space dimension \f$k \leq n\f$, 1606 \p vars is a set of variables whose maximum space dimension 1607 is also less than or equal to \f$n\f$, and \p dest is not a member 1608 of \p vars, then the space dimensions corresponding to 1609 variables in \p vars are \ref fold_space_dimensions "folded" 1610 into the \f$k\f$-th space dimension. 1611 */ 1612 void fold_space_dimensions(const Variables_Set& vars, Variable dest); 1613 1614 //@} // Member Functions that May Modify the Dimension of the Vector Space 1615 1616 /*! \brief 1617 Returns a reference the interval that bounds \p var. 1618 1619 \exception std::invalid_argument 1620 Thrown if \p var is not a space dimension of \p *this. 1621 */ 1622 const ITV& get_interval(Variable var) const; 1623 1624 /*! \brief 1625 Sets to \p i the interval that bounds \p var. 1626 1627 \exception std::invalid_argument 1628 Thrown if \p var is not a space dimension of \p *this. 1629 */ 1630 void set_interval(Variable var, const ITV& i); 1631 1632 /*! \brief 1633 If the space dimension of \p var is unbounded below, return 1634 <CODE>false</CODE>. Otherwise return <CODE>true</CODE> and set 1635 \p n, \p d and \p closed accordingly. 1636 1637 \note 1638 It is assumed that <CODE>*this</CODE> is a non-empty box 1639 having space dimension greater than or equal to that of \p var. 1640 An undefined behavior is obtained if this assumption is not met. 1641 \if Include_Implementation_Details 1642 To be more precise, if <CODE>*this</CODE> is an <EM>empty</EM> box 1643 (having space dimension greater than or equal to that of \p var) 1644 such that <CODE>!marked_empty()</CODE> holds, then the method can be 1645 called without incurring in undefined behavior: it will return 1646 <EM>unspecified</EM> boundary values that, if queried systematically 1647 on all space dimensions, will encode the box emptiness. 1648 \endif 1649 1650 Let \f$I\f$ be the interval corresponding to variable \p var 1651 in the non-empty box <CODE>*this</CODE>. 1652 If \f$I\f$ is not bounded from below, simply return <CODE>false</CODE> 1653 (leaving all other parameters unchanged). 1654 Otherwise, set \p n, \p d and \p closed as follows: 1655 - \p n and \p d are assigned the integers \f$n\f$ and \f$d\f$ such 1656 that the fraction \f$n/d\f$ corresponds to the greatest lower bound 1657 of \f$I\f$. The fraction \f$n/d\f$ is in canonical form, meaning 1658 that \f$n\f$ and \f$d\f$ have no common factors, \f$d\f$ is positive, 1659 and if \f$n\f$ is zero then \f$d\f$ is one; 1660 - \p closed is set to <CODE>true</CODE> if and only if the lower 1661 boundary of \f$I\f$ is closed (i.e., it is included in the interval). 1662 */ 1663 bool has_lower_bound(Variable var, 1664 Coefficient& n, Coefficient& d, bool& closed) const; 1665 1666 /*! \brief 1667 If the space dimension of \p var is unbounded above, return 1668 <CODE>false</CODE>. Otherwise return <CODE>true</CODE> and set 1669 \p n, \p d and \p closed accordingly. 1670 1671 \note 1672 It is assumed that <CODE>*this</CODE> is a non-empty box 1673 having space dimension greater than or equal to that of \p var. 1674 An undefined behavior is obtained if this assumption is not met. 1675 \if Include_Implementation_Details 1676 To be more precise, if <CODE>*this</CODE> is an <EM>empty</EM> box 1677 (having space dimension greater than or equal to that of \p var) 1678 such that <CODE>!marked_empty()</CODE> holds, then the method can be 1679 called without incurring in undefined behavior: it will return 1680 <EM>unspecified</EM> boundary values that, if queried systematically 1681 on all space dimensions, will encode the box emptiness. 1682 \endif 1683 1684 Let \f$I\f$ be the interval corresponding to variable \p var 1685 in the non-empty box <CODE>*this</CODE>. 1686 If \f$I\f$ is not bounded from above, simply return <CODE>false</CODE> 1687 (leaving all other parameters unchanged). 1688 Otherwise, set \p n, \p d and \p closed as follows: 1689 - \p n and \p d are assigned the integers \f$n\f$ and \f$d\f$ such 1690 that the fraction \f$n/d\f$ corresponds to the least upper bound 1691 of \f$I\f$. The fraction \f$n/d\f$ is in canonical form, meaning 1692 that \f$n\f$ and \f$d\f$ have no common factors, \f$d\f$ is positive, 1693 and if \f$n\f$ is zero then \f$d\f$ is one; 1694 - \p closed is set to <CODE>true</CODE> if and only if the upper 1695 boundary of \f$I\f$ is closed (i.e., it is included in the interval). 1696 */ 1697 bool has_upper_bound(Variable var, 1698 Coefficient& n, Coefficient& d, bool& closed) const; 1699 1700 //! Returns a system of constraints defining \p *this. 1701 Constraint_System constraints() const; 1702 1703 //! Returns a minimized system of constraints defining \p *this. 1704 Constraint_System minimized_constraints() const; 1705 1706 //! Returns a system of congruences approximating \p *this. 1707 Congruence_System congruences() const; 1708 1709 //! Returns a minimized system of congruences approximating \p *this. 1710 Congruence_System minimized_congruences() const; 1711 1712 //! Returns the total size in bytes of the memory occupied by \p *this. 1713 memory_size_type total_memory_in_bytes() const; 1714 1715 //! Returns the size in bytes of the memory managed by \p *this. 1716 memory_size_type external_memory_in_bytes() const; 1717 1718 /*! \brief 1719 Returns a 32-bit hash code for \p *this. 1720 1721 If <CODE>x</CODE> and <CODE>y</CODE> are such that <CODE>x == y</CODE>, 1722 then <CODE>x.hash_code() == y.hash_code()</CODE>. 1723 */ 1724 int32_t hash_code() const; 1725 1726 PPL_OUTPUT_DECLARATIONS 1727 1728 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 1729 /*! \brief 1730 Loads from \p s an ASCII representation (as produced by 1731 ascii_dump(std::ostream&) const) and sets \p *this accordingly. 1732 Returns <CODE>true</CODE> if successful, <CODE>false</CODE> otherwise. 1733 */ 1734 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 1735 bool ascii_load(std::istream& s); 1736 1737 private: 1738 template <typename Other_ITV> 1739 friend class Parma_Polyhedra_Library::Box; 1740 1741 friend bool 1742 operator==<ITV>(const Box<ITV>& x, const Box<ITV>& y); 1743 1744 friend std::ostream& 1745 Parma_Polyhedra_Library 1746 ::IO_Operators::operator<<<>(std::ostream& s, const Box<ITV>& box); 1747 1748 template <typename Specialization, typename Temp, typename To, typename I> 1749 friend bool Parma_Polyhedra_Library 1750 ::l_m_distance_assign(Checked_Number<To, Extended_Number_Policy>& r, 1751 const Box<I>& x, const Box<I>& y, 1752 const Rounding_Dir dir, 1753 Temp& tmp0, Temp& tmp1, Temp& tmp2); 1754 1755 //! The type of sequence used to implement the box. 1756 typedef std::vector<ITV> Sequence; 1757 1758 /*! \brief 1759 The type of intervals used by inner computations when trying to limit 1760 the cumulative effect of approximation errors. 1761 */ 1762 typedef ITV Tmp_Interval_Type; 1763 1764 //! A sequence of intervals, one for each dimension of the vector space. 1765 Sequence seq; 1766 1767 #define PPL_IN_Box_CLASS 1768 #include "Box_Status_idefs.hh" 1769 #undef PPL_IN_Box_CLASS 1770 1771 //! The status flags to keep track of the internal state. 1772 Status status; 1773 1774 /*! \brief 1775 Returns <CODE>true</CODE> if and only if the box is known to be empty. 1776 1777 The return value <CODE>false</CODE> does not necessarily 1778 implies that \p *this is non-empty. 1779 */ 1780 bool marked_empty() const; 1781 1782 public: 1783 //! Causes the box to become empty, i.e., to represent the empty set. 1784 void set_empty(); 1785 1786 private: 1787 //! Marks \p *this as definitely not empty. 1788 void set_nonempty(); 1789 1790 //! Asserts the validity of the empty flag of \p *this. 1791 void set_empty_up_to_date(); 1792 1793 //! Invalidates empty flag of \p *this. 1794 void reset_empty_up_to_date(); 1795 1796 /*! \brief 1797 Checks the hard way whether \p *this is an empty box: 1798 returns <CODE>true</CODE> if and only if it is so. 1799 */ 1800 bool check_empty() const; 1801 1802 /*! \brief 1803 Returns a reference the interval that bounds 1804 the box on the <CODE>k</CODE>-th space dimension. 1805 */ 1806 const ITV& operator[](dimension_type k) const; 1807 1808 /*! \brief 1809 WRITE ME. 1810 */ 1811 static I_Result 1812 refine_interval_no_check(ITV& itv, 1813 Constraint::Type type, 1814 Coefficient_traits::const_reference numer, 1815 Coefficient_traits::const_reference denom); 1816 1817 /*! \brief 1818 WRITE ME. 1819 */ 1820 void 1821 add_interval_constraint_no_check(dimension_type var_id, 1822 Constraint::Type type, 1823 Coefficient_traits::const_reference numer, 1824 Coefficient_traits::const_reference denom); 1825 1826 /*! \brief 1827 WRITE ME. 1828 */ 1829 void add_constraint_no_check(const Constraint& c); 1830 1831 /*! \brief 1832 WRITE ME. 1833 */ 1834 void add_constraints_no_check(const Constraint_System& cs); 1835 1836 /*! \brief 1837 WRITE ME. 1838 */ 1839 void add_congruence_no_check(const Congruence& cg); 1840 1841 /*! \brief 1842 WRITE ME. 1843 */ 1844 void add_congruences_no_check(const Congruence_System& cgs); 1845 1846 /*! \brief 1847 Uses the constraint \p c to refine \p *this. 1848 1849 \param c 1850 The constraint to be used for the refinement. 1851 1852 \warning 1853 If \p c and \p *this are dimension-incompatible, 1854 the behavior is undefined. 1855 */ 1856 void refine_no_check(const Constraint& c); 1857 1858 /*! \brief 1859 Uses the constraints in \p cs to refine \p *this. 1860 1861 \param cs 1862 The constraints to be used for the refinement. 1863 To avoid termination problems, each constraint in \p cs 1864 will be used for a single refinement step. 1865 1866 \warning 1867 If \p cs and \p *this are dimension-incompatible, 1868 the behavior is undefined. 1869 */ 1870 void refine_no_check(const Constraint_System& cs); 1871 1872 /*! \brief 1873 Uses the congruence \p cg to refine \p *this. 1874 1875 \param cg 1876 The congruence to be added. 1877 Nontrivial proper congruences are ignored. 1878 1879 \warning 1880 If \p cg and \p *this are dimension-incompatible, 1881 the behavior is undefined. 1882 */ 1883 void refine_no_check(const Congruence& cg); 1884 1885 /*! \brief 1886 Uses the congruences in \p cgs to refine \p *this. 1887 1888 \param cgs 1889 The congruences to be added. 1890 Nontrivial proper congruences are ignored. 1891 1892 \warning 1893 If \p cgs and \p *this are dimension-incompatible, 1894 the behavior is undefined. 1895 */ 1896 void refine_no_check(const Congruence_System& cgs); 1897 1898 /*! \brief 1899 Propagates the constraint \p c to refine \p *this. 1900 1901 \param c 1902 The constraint to be propagated. 1903 1904 \warning 1905 If \p c and \p *this are dimension-incompatible, 1906 the behavior is undefined. 1907 1908 \warning 1909 This method may lead to non-termination. 1910 1911 \if Include_Implementation_Details 1912 1913 For any expression \f$e\f$, we denote by 1914 \f$\left\uparrow e \right\uparrow\f$ (resp., \f$\left\downarrow e 1915 \right\downarrow\f$) the result of any computation that is 1916 guaranteed to yield an upper (resp., lower) approximation of 1917 \f$e\f$. So there exists \f$\epsilon \in \Rset\f$ with 1918 \f$\epsilon \geq 0\f$ such that 1919 \f$\left\uparrow e \right\uparrow = e + \epsilon\f$. 1920 If \f$\epsilon = 0\f$ we say that the computation of 1921 \f$\left\uparrow e \right\uparrow\f$ is <EM>exact</EM>; 1922 we say it is <EM>inexact</EM> otherwise. 1923 Similarly for \f$\left\downarrow e \right\downarrow\f$. 1924 1925 Consider a constraint of the general form 1926 \f[ 1927 z + \sum_{i \in I}{a_ix_i} \relsym 0, 1928 \f] 1929 where \f$z \in \Zset\f$, \f$I\f$ is a set of indices, 1930 \f$a_i \in \Zset\f$ with \f$a_i \neq 0\f$ for each \f$i \in I\f$, and 1931 \f$\mathord{\relsym} \in \{ \mathord{\geq}, \mathord{>}, \mathord{=} \}\f$. 1932 The set \f$I\f$ is subdivided into the disjoint sets \f$P\f$ and \f$N\f$ 1933 such that, for each \f$i \in I\f$, \f$a_i > 0\f$ if \f$i \in P\f$ and 1934 \f$a_i < 0\f$ if \f$i \in N\f$. 1935 Suppose that, for each \f$i \in P \union N\f$ a variation interval 1936 \f$\chi_i \sseq \Rset\f$ is known for \f$x_i\f$ and that the infimum 1937 and the supremum of \f$\chi_i\f$ are denoted, respectively, 1938 by \f$\chi_i^\mathrm{l}\f$ and \f$\chi_i^\mathrm{u}\f$, where 1939 \f$\chi_i^\mathrm{l}, \chi_i^\mathrm{u} \in \Rset \union \{ -\infty, +\infty \}\f$. 1940 1941 For each \f$k \in P\f$, we have 1942 \f[ 1943 x_k 1944 \relsym 1945 \frac{1}{a_k} 1946 \Biggl( 1947 - z 1948 - \sum_{i \in N}{a_ix_i} 1949 - \sum_{\genfrac{}{}{0pt}{} 1950 {\scriptstyle i \in P} 1951 {\scriptstyle i \neq k}}{a_ix_i} 1952 \Biggr). 1953 \f] 1954 Thus, if \f$\chi_i^\mathrm{l} \in \Rset\f$ for each \f$i \in N\f$ and 1955 \f$\chi_i^\mathrm{u} \in \Rset\f$ for each \f$i \in P \setdiff \{ k \}\f$, 1956 we have 1957 \f[ 1958 x_k 1959 \geq 1960 \Biggl\downarrow 1961 \frac{1}{a_k} 1962 \Biggl( 1963 - z 1964 - \sum_{i \in N}{a_i\chi_i^\mathrm{l}} 1965 - \sum_{\genfrac{}{}{0pt}{} 1966 {\scriptstyle i \in P} 1967 {\scriptstyle i \neq k}}{a_i\chi_i^\mathrm{u}} 1968 \Biggr) 1969 \Biggr\downarrow 1970 \f] 1971 and, if \f$\mathord{\relsym} \in \{ \mathord{=} \}\f$, 1972 \f$\chi_i^\mathrm{u} \in \Rset\f$ for each \f$i \in N\f$ and 1973 \f$\chi_i^\mathrm{l} \in \Rset\f$ for each \f$P \setdiff \{ k \}\f$, 1974 \f[ 1975 x_k 1976 \leq 1977 \Biggl\uparrow 1978 \frac{1}{a_k} 1979 \Biggl( 1980 - z 1981 - \sum_{i \in N}{a_i\chi_i^\mathrm{u}} 1982 - \sum_{\genfrac{}{}{0pt}{} 1983 {\scriptstyle i \in P} 1984 {\scriptstyle i \neq k}}{a_i\chi_i^\mathrm{l}} 1985 \Biggr) 1986 \Biggl\uparrow. 1987 \f] 1988 In the first inequality, the relation is strict if 1989 \f$\mathord{\relsym} \in \{ \mathord{>} \}\f$, or if 1990 \f$\chi_i^\mathrm{l} \notin \chi_i\f$ for some \f$i \in N\f$, or if 1991 \f$\chi_i^\mathrm{u} \notin \chi_i\f$ for some 1992 \f$i \in P \setdiff \{ k \}\f$, or if the computation is inexact. 1993 In the second inequality, the relation is strict if 1994 \f$\chi_i^\mathrm{u} \notin \chi_i\f$ for some \f$i \in N\f$, or if 1995 \f$\chi_i^\mathrm{l} \notin \chi_i\f$ for some 1996 \f$i \in P \setdiff \{ k \}\f$, or if the computation is inexact. 1997 1998 For each \f$k \in N\f$, we have 1999 \f[ 2000 \frac{1}{a_k} 2001 \Biggl( 2002 - z 2003 - \sum_{\genfrac{}{}{0pt}{} 2004 {\scriptstyle i \in N} 2005 {\scriptstyle i \neq k}}{a_ix_i} 2006 - \sum_{i \in P}{a_ix_i} 2007 \Biggr) 2008 \relsym 2009 x_k. 2010 \f] 2011 Thus, if 2012 \f$\chi_i^\mathrm{l} \in \Rset\f$ 2013 for each \f$i \in N \setdiff \{ k \}\f$ and 2014 \f$\chi_i^\mathrm{u} \in \Rset\f$ for each \f$i \in P\f$, 2015 we have 2016 \f[ 2017 \Biggl\uparrow 2018 \frac{1}{a_k} 2019 \Biggl( 2020 - z 2021 - \sum_{\genfrac{}{}{0pt}{} 2022 {\scriptstyle i \in N} 2023 {\scriptstyle i \neq k}}{a_i\chi_i^\mathrm{l}} 2024 - \sum_{i \in P}{a_i\chi_i^\mathrm{u}} 2025 \Biggr) 2026 \Biggl\uparrow 2027 \geq 2028 x_k 2029 \f] 2030 and, if \f$\mathord{\relsym} \in \{ \mathord{=} \}\f$, 2031 \f$\chi_i^\mathrm{u} \in \Rset\f$ for each \f$i \in N \setdiff \{ k \}\f$ 2032 and \f$\chi_i^\mathrm{l} \in \Rset\f$ for each \f$i \in P\f$, 2033 \f[ 2034 \Biggl\downarrow 2035 \frac{1}{a_k} 2036 \Biggl( 2037 - z 2038 - \sum_{\genfrac{}{}{0pt}{} 2039 {\scriptstyle i \in N} 2040 {\scriptstyle i \neq k}}{a_i\chi_i^\mathrm{u}} 2041 - \sum_{i \in P}{a_i\chi_i^\mathrm{l}} 2042 \Biggr) 2043 \Biggl\downarrow 2044 \leq 2045 x_k. 2046 \f] 2047 In the first inequality, the relation is strict if 2048 \f$\mathord{\relsym} \in \{ \mathord{>} \}\f$, or if 2049 \f$\chi_i^\mathrm{u} \notin \chi_i\f$ for some \f$i \in P\f$, or if 2050 \f$\chi_i^\mathrm{l} \notin \chi_i\f$ for some 2051 \f$i \in N \setdiff \{ k \}\f$, or if the computation is inexact. 2052 In the second inequality, the relation is strict if 2053 \f$\chi_i^\mathrm{l} \notin \chi_i\f$ for some \f$i \in P\f$, or if 2054 \f$\chi_i^\mathrm{u} \notin \chi_i\f$ for some 2055 \f$i \in N \setdiff \{ k \}\f$, or if the computation is inexact. 2056 \endif 2057 */ 2058 void propagate_constraint_no_check(const Constraint& c); 2059 2060 /*! \brief 2061 Propagates the constraints in \p cs to refine \p *this. 2062 2063 \param cs 2064 The constraints to be propagated. 2065 2066 \param max_iterations 2067 The maximum number of propagation steps for each constraint in \p cs. 2068 If zero, the number of propagation steps will be unbounded, possibly 2069 resulting in an infinite loop. 2070 2071 \warning 2072 If \p cs and \p *this are dimension-incompatible, 2073 the behavior is undefined. 2074 2075 \warning 2076 This method may lead to non-termination if \p max_iterations is 0. 2077 */ 2078 void propagate_constraints_no_check(const Constraint_System& cs, 2079 dimension_type max_iterations); 2080 2081 //! Checks if and how \p expr is bounded in \p *this. 2082 /*! 2083 Returns <CODE>true</CODE> if and only if \p from_above is 2084 <CODE>true</CODE> and \p expr is bounded from above in \p *this, 2085 or \p from_above is <CODE>false</CODE> and \p expr is bounded 2086 from below in \p *this. 2087 2088 \param expr 2089 The linear expression to test; 2090 2091 \param from_above 2092 <CODE>true</CODE> if and only if the boundedness of interest is 2093 "from above". 2094 2095 \exception std::invalid_argument 2096 Thrown if \p expr and \p *this are dimension-incompatible. 2097 */ 2098 bool bounds(const Linear_Expression& expr, bool from_above) const; 2099 2100 //! Maximizes or minimizes \p expr subject to \p *this. 2101 /*! 2102 \param expr 2103 The linear expression to be maximized or minimized subject to \p *this; 2104 2105 \param maximize 2106 <CODE>true</CODE> if maximization is what is wanted; 2107 2108 \param ext_n 2109 The numerator of the extremum value; 2110 2111 \param ext_d 2112 The denominator of the extremum value; 2113 2114 \param included 2115 <CODE>true</CODE> if and only if the extremum of \p expr can 2116 actually be reached in \p *this; 2117 2118 \param g 2119 When maximization or minimization succeeds, will be assigned 2120 a point or closure point where \p expr reaches the 2121 corresponding extremum value. 2122 2123 \exception std::invalid_argument 2124 Thrown if \p expr and \p *this are dimension-incompatible. 2125 2126 If \p *this is empty or \p expr is not bounded in the appropriate 2127 direction, <CODE>false</CODE> is returned and \p ext_n, \p ext_d, 2128 \p included and \p g are left untouched. 2129 */ 2130 bool max_min(const Linear_Expression& expr, 2131 bool maximize, 2132 Coefficient& ext_n, Coefficient& ext_d, bool& included, 2133 Generator& g) const; 2134 2135 //! Maximizes or minimizes \p expr subject to \p *this. 2136 /*! 2137 \param expr 2138 The linear expression to be maximized or minimized subject to \p *this; 2139 2140 \param maximize 2141 <CODE>true</CODE> if maximization is what is wanted; 2142 2143 \param ext_n 2144 The numerator of the extremum value; 2145 2146 \param ext_d 2147 The denominator of the extremum value; 2148 2149 \param included 2150 <CODE>true</CODE> if and only if the extremum of \p expr can 2151 actually be reached in \p * this; 2152 2153 \exception std::invalid_argument 2154 Thrown if \p expr and \p *this are dimension-incompatible. 2155 2156 If \p *this is empty or \p expr is not bounded in the appropriate 2157 direction, <CODE>false</CODE> is returned and \p ext_n, \p ext_d, 2158 \p included and \p point are left untouched. 2159 */ 2160 bool max_min(const Linear_Expression& expr, 2161 bool maximize, 2162 Coefficient& ext_n, Coefficient& ext_d, bool& included) const; 2163 2164 /*! \brief 2165 Adds to \p limiting_box the interval constraints in \p cs 2166 that are satisfied by \p *this. 2167 */ 2168 void get_limiting_box(const Constraint_System& cs, 2169 Box& limiting_box) const; 2170 2171 //! \name Exception Throwers 2172 //@{ 2173 void throw_dimension_incompatible(const char* method, 2174 const Box& y) const; 2175 2176 void throw_dimension_incompatible(const char* method, 2177 dimension_type required_dim) const; 2178 2179 void throw_dimension_incompatible(const char* method, 2180 const Constraint& c) const; 2181 2182 void throw_dimension_incompatible(const char* method, 2183 const Congruence& cg) const; 2184 2185 void throw_dimension_incompatible(const char* method, 2186 const Constraint_System& cs) const; 2187 2188 void throw_dimension_incompatible(const char* method, 2189 const Congruence_System& cgs) const; 2190 2191 void throw_dimension_incompatible(const char* method, 2192 const Generator& g) const; 2193 2194 void throw_dimension_incompatible(const char* method, 2195 const char* le_name, 2196 const Linear_Expression& le) const; 2197 2198 template <typename C> 2199 void throw_dimension_incompatible(const char* method, 2200 const char* lf_name, 2201 const Linear_Form<C>& lf) const; 2202 2203 static void throw_constraint_incompatible(const char* method); 2204 2205 static void throw_expression_too_complex(const char* method, 2206 const Linear_Expression& le); 2207 2208 static void throw_invalid_argument(const char* method, const char* reason); 2209 //@} // Exception Throwers 2210 }; 2211 2212 namespace Parma_Polyhedra_Library { 2213 2214 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 2215 /*! \brief 2216 Returns the relations holding between an interval and 2217 an interval constraint. 2218 2219 \param i 2220 The interval; 2221 2222 \param constraint_type 2223 The constraint type; 2224 2225 \param numer 2226 The numerator of the constraint bound; 2227 2228 \param denom 2229 The denominator of the constraint bound 2230 2231 The interval constraint has the form 2232 <CODE>denom * Variable(0) relsym numer</CODE> 2233 where relsym is <CODE>==</CODE>, <CODE>></CODE> or <CODE>>=</CODE> 2234 depending on the <CODE>constraint_type</CODE>. 2235 */ 2236 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 2237 template <typename ITV> 2238 Poly_Con_Relation 2239 interval_relation(const ITV& i, 2240 const Constraint::Type constraint_type, 2241 Coefficient_traits::const_reference numer, 2242 Coefficient_traits::const_reference denom 2243 = Coefficient_one()); 2244 2245 class Box_Helpers { 2246 public: 2247 // This is declared here so that Linear_Expression needs to be friend of 2248 // Box_Helpers only, and doesn't need to be friend of this, too. 2249 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 2250 //! Decodes the constraint \p c as an interval constraint. 2251 /*! \relates Box 2252 \return 2253 <CODE>true</CODE> if the constraint \p c is an 2254 \ref intervals "interval constraint"; 2255 <CODE>false</CODE> otherwise. 2256 2257 \param c 2258 The constraint to be decoded. 2259 2260 \param c_num_vars 2261 If <CODE>true</CODE> is returned, then it will be set to the number 2262 of variables having a non-zero coefficient. The only legal values 2263 will therefore be 0 and 1. 2264 2265 \param c_only_var 2266 If <CODE>true</CODE> is returned and if \p c_num_vars is not set to 0, 2267 then it will be set to the index of the only variable having 2268 a non-zero coefficient in \p c. 2269 */ 2270 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) 2271 static bool extract_interval_constraint(const Constraint& c, 2272 dimension_type& c_num_vars, 2273 dimension_type& c_only_var); 2274 2275 // This is declared here so that Linear_Expression needs to be friend of 2276 // Box_Helpers only, and doesn't need to be friend of this, too. 2277 static bool extract_interval_congruence(const Congruence& cg, 2278 dimension_type& cg_num_vars, 2279 dimension_type& cg_only_var); 2280 }; 2281 2282 } // namespace Parma_Polyhedra_Library 2283 2284 #include "Box_Status_inlines.hh" 2285 #include "Box_inlines.hh" 2286 #include "Box_templates.hh" 2287 2288 #endif // !defined(PPL_Box_defs_hh) 2289