1 /* Doxumentation for the Java interface. 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 package parma_polyhedra_library; 25 26 // A fake class, just to cheat Doxygen. 27 public class Fake_Class_For_Doxygen {} 28 29 //! The Java base class for (C and NNC) convex polyhedra. 30 /*! \ingroup PPL_Java_interface 31 The base class Polyhedron provides declarations for most of 32 the methods common to classes C_Polyhedron and NNC_Polyhedron. 33 Note that the user should always use the derived classes. 34 Moreover, C and NNC polyhedra can not be freely interchanged: 35 as specified in the main manual, most library functions require 36 their arguments to be topologically compatible. 37 */ 38 public class Polyhedron extends PPL_Object { 39 40 //! \name Member Functions that Do Not Modify the Polyhedron 41 //@{ 42 43 //! Returns the dimension of the vector space enclosing \p this. space_dimension()44 public native long space_dimension(); 45 46 /*! \brief 47 Returns \f$0\f$, if \p this is empty; otherwise, returns the 48 \extref{Affine_Independence_and_Affine_Dimension, affine dimension} 49 of \p this. 50 */ affine_dimension()51 public native long affine_dimension(); 52 53 //! Returns the system of constraints. constraints()54 public native Constraint_System constraints(); 55 56 //! Returns a system of (equality) congruences satisfied by \p this. congruences()57 public native Congruence_System congruences(); 58 59 //! Returns the system of constraints, with no redundant constraint. minimized_constraints()60 public native Constraint_System minimized_constraints(); 61 62 /*! \brief 63 Returns a system of (equality) congruences satisfied by \p this, 64 with no redundant congruences and having the same affine dimension 65 as \p this. 66 */ minimized_congruences()67 public native Congruence_System minimized_congruences(); 68 69 //! Returns \c true if and only if \p this is an empty polyhedron. is_empty()70 public native boolean is_empty(); 71 72 //! Returns \c true if and only if \p this is a universe polyhedron. is_universe()73 public native boolean is_universe(); 74 75 /*! \brief 76 Returns \c true if and only if \p this 77 is a bounded polyhedron. 78 */ is_bounded()79 public native boolean is_bounded(); 80 81 //! Returns \c true if and only if \p this is discrete. is_discrete()82 public native boolean is_discrete(); 83 84 /*! \brief 85 Returns \c true if and only if \p this 86 is a topologically closed subset of the vector space. 87 */ is_topologically_closed()88 public native boolean is_topologically_closed(); 89 90 /*! \brief 91 Returns \c true if and only if \p this 92 contains at least one integer point. 93 */ contains_integer_point()94 public native boolean contains_integer_point(); 95 96 /*! \brief 97 Returns \c true if and only if \p var is constrained in 98 \p this. 99 100 \exception Invalid_Argument_Exception 101 Thrown if \p var is not a space dimension of \p this. 102 */ constrains(Variable var)103 public native boolean constrains(Variable var); 104 105 /*! \brief 106 Returns \c true if and only if \p expr is 107 bounded from above in \p this. 108 109 \exception Invalid_Argument_Exception 110 Thrown if \p expr and \p this are dimension-incompatible. 111 */ bounds_from_above(Linear_Expression expr)112 public native boolean bounds_from_above(Linear_Expression expr); 113 114 /*! \brief 115 Returns \c true if and only if \p expr is 116 bounded from below in \p this. 117 118 \exception Invalid_Argument_Exception 119 Thrown if \p expr and \p this are dimension-incompatible. 120 */ bounds_from_below(Linear_Expression expr)121 public native boolean bounds_from_below(Linear_Expression expr); 122 123 /*! \brief 124 Returns \c true if and only if \p this is not empty 125 and \p expr is bounded from above in \p this, in which case 126 the supremum value is computed. 127 128 \param expr 129 The linear expression to be maximized subject to \p this; 130 131 \param sup_n 132 The numerator of the supremum value; 133 134 \param sup_d 135 The denominator of the supremum value; 136 137 \param maximum 138 \c true if and only if the supremum is also the maximum value. 139 140 \exception Invalid_Argument_Exception 141 Thrown if \p expr and \p this are dimension-incompatible. 142 143 If \p this is empty or \p expr is not bounded from above, 144 \c false is returned and \p sup_n, \p sup_d 145 and \p maximum are left untouched. 146 */ maximize(Linear_Expression expr, Coefficient sup_n, Coefficient sup_d, By_Reference<Boolean> maximum)147 public native boolean maximize(Linear_Expression expr, 148 Coefficient sup_n, Coefficient sup_d, 149 By_Reference<Boolean> maximum); 150 151 /*! \brief 152 Returns \c true if and only if \p this is not empty 153 and \p expr is bounded from below in \p this, in which case 154 the infimum value is computed. 155 156 \param expr 157 The linear expression to be minimized subject to \p this; 158 159 \param inf_n 160 The numerator of the infimum value; 161 162 \param inf_d 163 The denominator of the infimum value; 164 165 \param minimum 166 \c true if and only if the infimum is also the minimum value. 167 168 \exception Invalid_Argument_Exception 169 Thrown if \p expr and \p this are dimension-incompatible. 170 171 If \p this is empty or \p expr is not bounded from below, 172 \c false is returned and \p inf_n, \p inf_d 173 and \p minimum are left untouched. 174 */ minimize(Linear_Expression expr, Coefficient inf_n, Coefficient inf_d, By_Reference<Boolean> minimum)175 public native boolean minimize(Linear_Expression expr, 176 Coefficient inf_n, Coefficient inf_d, 177 By_Reference<Boolean> minimum); 178 179 /*! \brief 180 Returns \c true if and only if \p this is not empty 181 and \p expr is bounded from above in \p this, in which case 182 the supremum value and a point where \p expr reaches it are computed. 183 184 \param expr 185 The linear expression to be maximized subject to \p this; 186 187 \param sup_n 188 The numerator of the supremum value; 189 190 \param sup_d 191 The denominator of the supremum value; 192 193 \param maximum 194 \c true if and only if the supremum is also the maximum value; 195 196 \param g 197 When maximization succeeds, will be assigned the point or 198 closure point where \p expr reaches its supremum value. 199 200 \exception Invalid_Argument_Exception 201 Thrown if \p expr and \p this are dimension-incompatible. 202 203 If \p this is empty or \p expr is not bounded from above, 204 \c false is returned and \p sup_n, \p sup_d, \p maximum 205 and \p g are left untouched. 206 */ maximize(Linear_Expression expr, Coefficient sup_n, Coefficient sup_d, By_Reference<Boolean> maximum, Generator g)207 public native boolean maximize(Linear_Expression expr, 208 Coefficient sup_n, Coefficient sup_d, 209 By_Reference<Boolean> maximum, 210 Generator g); 211 212 /*! \brief 213 Returns \c true if and only if \p this is not empty 214 and \p expr is bounded from below in \p this, in which case 215 the infimum value and a point where \p expr reaches it are computed. 216 217 \param expr 218 The linear expression to be minimized subject to \p this; 219 220 \param inf_n 221 The numerator of the infimum value; 222 223 \param inf_d 224 The denominator of the infimum value; 225 226 \param minimum 227 \c true if and only if the infimum is also the minimum value; 228 229 \param g 230 When minimization succeeds, will be assigned a point or 231 closure point where \p expr reaches its infimum value. 232 233 \exception Invalid_Argument_Exception 234 Thrown if \p expr and \p this are dimension-incompatible. 235 236 If \p this is empty or \p expr is not bounded from below, 237 \c false is returned and \p inf_n, \p inf_d, \p minimum 238 and \p g are left untouched. 239 */ minimize(Linear_Expression expr, Coefficient inf_n, Coefficient inf_d, By_Reference<Boolean> minimum, Generator g)240 public native boolean minimize(Linear_Expression expr, 241 Coefficient inf_n, Coefficient inf_d, 242 By_Reference<Boolean> minimum, 243 Generator g); 244 245 /*! \brief 246 Returns the relations holding between the polyhedron \p this 247 and the constraint \p c. 248 249 \exception Invalid_Argument_Exception 250 Thrown if \p this and constraint \p c are dimension-incompatible. 251 */ relation_with(Constraint c)252 public native Poly_Con_Relation relation_with(Constraint c); 253 254 /*! \brief 255 Returns the relations holding between the polyhedron \p this 256 and the generator \p g. 257 258 \exception Invalid_Argument_Exception 259 Thrown if \p this and generator \p g are dimension-incompatible. 260 */ relation_with(Generator c)261 public native Poly_Gen_Relation relation_with(Generator c); 262 263 /*! \brief 264 Returns the relations holding between the polyhedron \p this 265 and the congruence \p c. 266 267 \exception Invalid_Argument_Exception 268 Thrown if \p this and congruence \p c are dimension-incompatible. 269 */ relation_with(Congruence c)270 public native Poly_Con_Relation relation_with(Congruence c); 271 272 //! Returns \c true if and only if \p this contains \p y. 273 /*! 274 \exception Invalid_Argument_Exception 275 Thrown if \p this and \p y are topology-incompatible or 276 dimension-incompatible. 277 */ contains(Polyhedron y)278 public native boolean contains(Polyhedron y); 279 280 //! Returns \c true if and only if \p this strictly contains \p y. 281 /*! 282 \exception Invalid_Argument_Exception 283 Thrown if \p this and \p y are topology-incompatible or 284 dimension-incompatible. 285 */ strictly_contains(Polyhedron y)286 public native boolean strictly_contains(Polyhedron y); 287 288 //! Returns \c true if and only if \p this and \p y are disjoint. 289 /*! 290 \exception Invalid_Argument_Exception 291 Thrown if \p x and \p y are topology-incompatible or 292 dimension-incompatible. 293 */ is_disjoint_from(Polyhedron y)294 public native boolean is_disjoint_from(Polyhedron y); 295 296 //! Returns \c true if and only if \p this and \p y are equal. equals(Polyhedron y)297 public native boolean equals(Polyhedron y); 298 299 //! Returns \c true if and only if \p this and \p y are equal. equals(Object y)300 public boolean equals(Object y); 301 302 //! Returns a hash code for \p this. 303 /*! 304 If \p x and \p y are such that <CODE>x == y</CODE>, 305 then <CODE>x.hash_code() == y.hash_code()</CODE>. 306 */ hashCode()307 public native int hashCode(); 308 309 //! Returns the size in bytes of the memory managed by \p this. external_memory_in_bytes()310 public native long external_memory_in_bytes(); 311 312 //! Returns the total size in bytes of the memory occupied by \p this. total_memory_in_bytes()313 public native long total_memory_in_bytes(); 314 315 //! Returns a string representing \p this. toString()316 public native String toString(); 317 318 /*! \brief 319 Returns a string containing a low-level representation of \p this. 320 321 Useful for debugging purposes. 322 */ ascii_dump()323 public native String ascii_dump(); 324 325 //! Checks if all the invariants are satisfied. OK()326 public native boolean OK(); 327 328 //@} // Member Functions that Do Not Modify the Polyhedron 329 330 //! \name Space Dimension Preserving Member Functions that May Modify the Polyhedron 331 //@{ 332 333 /*! \brief 334 Adds a copy of constraint \p c to the system of constraints 335 of \p this (without minimizing the result). 336 337 \param c 338 The constraint that will be added to the system of 339 constraints of \p this. 340 341 \exception Invalid_Argument_Exception 342 Thrown if \p this and constraint \p c are topology-incompatible 343 or dimension-incompatible. 344 */ add_constraint(Constraint c)345 public native void add_constraint(Constraint c); 346 347 /*! \brief 348 Adds a copy of congruence \p cg to \p this, 349 if \p cg can be exactly represented by a polyhedron. 350 351 \exception Invalid_Argument_Exception 352 Thrown if \p this and congruence \p cg are dimension-incompatible, 353 of if \p cg is a proper congruence which is neither a tautology, 354 nor a contradiction. 355 */ add_congruence(Congruence cg)356 public native void add_congruence(Congruence cg); 357 358 /*! \brief 359 Adds a copy of the constraints in \p cs to the system 360 of constraints of \p this (without minimizing the result). 361 362 \param cs 363 Contains the constraints that will be added to the system of 364 constraints of \p this. 365 366 \exception Invalid_Argument_Exception 367 Thrown if \p this and \p cs are topology-incompatible or 368 dimension-incompatible. 369 */ add_constraints(Constraint_System cs)370 public native void add_constraints(Constraint_System cs); 371 372 /*! \brief 373 Adds a copy of the congruences in \p cgs to \p this, 374 if all the congruences can be exactly represented by a polyhedron. 375 376 \param cgs 377 The congruences to be added. 378 379 \exception Invalid_Argument_Exception 380 Thrown if \p this and \p cgs are dimension-incompatible, 381 of if there exists in \p cgs a proper congruence which is 382 neither a tautology, nor a contradiction. 383 */ add_congruences(Congruence_System cgs)384 public native void add_congruences(Congruence_System cgs); 385 386 /*! \brief 387 Uses a copy of constraint \p c to refine \p this. 388 389 \exception Invalid_Argument_Exception 390 Thrown if \p this and constraint \p c are dimension-incompatible. 391 */ refine_with_constraint(Constraint c)392 public native void refine_with_constraint(Constraint c); 393 394 /*! \brief 395 Uses a copy of congruence \p cg to refine \p this. 396 397 \exception Invalid_Argument_Exception 398 Thrown if \p this and congruence \p cg are dimension-incompatible. 399 */ refine_with_congruence(Congruence cg)400 public native void refine_with_congruence(Congruence cg); 401 402 /*! \brief 403 Uses a copy of the constraints in \p cs to refine \p this. 404 405 \param cs 406 Contains the constraints used to refine the system of 407 constraints of \p this. 408 409 \exception Invalid_Argument_Exception 410 Thrown if \p this and \p cs are dimension-incompatible. 411 */ refine_with_constraints(Constraint_System cs)412 public native void refine_with_constraints(Constraint_System cs); 413 414 /*! \brief 415 Uses a copy of the congruences in \p cgs to refine \p this. 416 417 \param cgs 418 Contains the congruences used to refine the system of 419 constraints of \p this. 420 421 \exception Invalid_Argument_Exception 422 Thrown if \p this and \p cgs are dimension-incompatible. 423 */ refine_with_congruences(Congruence_System cgs)424 public native void refine_with_congruences(Congruence_System cgs); 425 426 /*! \brief 427 Assigns to \p this the intersection of \p this and \p y. 428 The result is not guaranteed to be minimized. 429 430 \exception Invalid_Argument_Exception 431 Thrown if \p this and \p y are topology-incompatible or 432 dimension-incompatible. 433 */ intersection_assign(Polyhedron y)434 public native void intersection_assign(Polyhedron y); 435 436 /*! \brief 437 Assigns to \p this the upper bound of \p this and \p y. 438 439 \exception Invalid_Argument_Exception 440 Thrown if \p this and \p y are topology-incompatible or 441 dimension-incompatible. 442 */ upper_bound_assign(Polyhedron y)443 public native void upper_bound_assign(Polyhedron y); 444 445 /*! \brief 446 Assigns to \p this 447 the \extref{Convex_Polyhedral_Difference, poly-difference} 448 of \p this and \p y. The result is not guaranteed to be minimized. 449 450 \exception Invalid_Argument_Exception 451 Thrown if \p this and \p y are topology-incompatible or 452 dimension-incompatible. 453 */ difference_assign(Polyhedron y)454 public native void difference_assign(Polyhedron y); 455 456 /*! \brief 457 Assigns to \p this the result of computing the 458 \extref{Time_Elapse_Operator, time-elapse} between \p this and \p y. 459 460 \exception Invalid_Argument_Exception 461 Thrown if \p this and \p y are topology-incompatible or 462 dimension-incompatible. 463 */ time_elapse_assign(Polyhedron y)464 public native void time_elapse_assign(Polyhedron y); 465 466 //! Assigns to \p this its topological closure. topological_closure_assign()467 public native void topological_closure_assign(); 468 469 /*! \brief 470 Assigns to \p this a \extref{Meet_Preserving_Simplification, 471 meet-preserving simplification} of \p this with respect to \p y. 472 If \c false is returned, then the intersection is empty. 473 474 \exception Invalid_Argument_Exception 475 Thrown if \p this and \p y are topology-incompatible or 476 dimension-incompatible. 477 */ simplify_using_context_assign(Polyhedron y)478 public native boolean simplify_using_context_assign(Polyhedron y); 479 480 /*! \brief 481 Assigns to \p this the 482 \extref{Single_Update_Affine_Functions, affine image} 483 of \p this under the function mapping variable \p var to the 484 affine expression specified by \p expr and \p denominator. 485 486 \param var 487 The variable to which the affine expression is assigned; 488 489 \param expr 490 The numerator of the affine expression; 491 492 \param denominator 493 The denominator of the affine expression (optional argument with 494 default value 1). 495 496 \exception Invalid_Argument_Exception 497 Thrown if \p denominator is zero or if \p expr and \p this are 498 dimension-incompatible or if \p var is not a space dimension of 499 \p this. 500 */ affine_image(Variable var, Linear_Expression expr, Coefficient denominator)501 public native void affine_image(Variable var, Linear_Expression expr, 502 Coefficient denominator); 503 504 /*! \brief 505 Assigns to \p this the 506 \extref{Single_Update_Affine_Functions, affine preimage} 507 of \p this under the function mapping variable \p var to the 508 affine expression specified by \p expr and \p denominator. 509 510 \param var 511 The variable to which the affine expression is substituted; 512 513 \param expr 514 The numerator of the affine expression; 515 516 \param denominator 517 The denominator of the affine expression (optional argument with 518 default value 1). 519 520 \exception Invalid_Argument_Exception 521 Thrown if \p denominator is zero or if \p expr and \p this are 522 dimension-incompatible or if \p var is not a space dimension of \p this. 523 */ affine_preimage(Variable var, Linear_Expression expr, Coefficient denominator)524 public native void affine_preimage(Variable var, Linear_Expression expr, 525 Coefficient denominator); 526 527 /*! 528 \brief 529 Assigns to \p this the image of \p this with respect to the 530 \extref{Single_Update_Bounded_Affine_Relations, bounded affine relation} 531 \f$\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} 532 \leq \mathrm{var}' 533 \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}\f$. 534 535 \param var 536 The variable updated by the affine relation; 537 538 \param lb_expr 539 The numerator of the lower bounding affine expression; 540 541 \param ub_expr 542 The numerator of the upper bounding affine expression; 543 544 \param denominator 545 The (common) denominator for the lower and upper bounding 546 affine expressions (optional argument with default value 1). 547 548 \exception Invalid_Argument_Exception 549 Thrown if \p denominator is zero or if \p lb_expr (resp., \p ub_expr) 550 and \p this are dimension-incompatible or if \p var is not a space 551 dimension of \p this. 552 */ bounded_affine_image(Variable var, Linear_Expression lb_expr, Linear_Expression ub_expr, Coefficient denominator)553 public native void bounded_affine_image(Variable var, 554 Linear_Expression lb_expr, 555 Linear_Expression ub_expr, 556 Coefficient denominator); 557 558 /*! \brief 559 Assigns to \p this the preimage of \p this with respect to the 560 \extref{Single_Update_Bounded_Affine_Relations, bounded affine relation} 561 \f$\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} 562 \leq \mathrm{var}' 563 \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}\f$. 564 565 \param var 566 The variable updated by the affine relation; 567 568 \param lb_expr 569 The numerator of the lower bounding affine expression; 570 571 \param ub_expr 572 The numerator of the upper bounding affine expression; 573 574 \param denominator 575 The (common) denominator for the lower and upper bounding 576 affine expressions (optional argument with default value 1). 577 578 \exception Invalid_Argument_Exception 579 Thrown if \p denominator is zero or if \p lb_expr (resp., \p ub_expr) 580 and \p this are dimension-incompatible or if \p var is not a space 581 dimension of \p this. 582 */ bounded_affine_preimage(Variable var, Linear_Expression lb_expr, Linear_Expression ub_expr, Coefficient denominator)583 public native void bounded_affine_preimage(Variable var, 584 Linear_Expression lb_expr, 585 Linear_Expression ub_expr, 586 Coefficient denominator); 587 588 /*! \brief 589 Assigns to \p this the image of \p this with respect to the 590 \extref{Generalized_Affine_Relations, generalized affine relation} 591 \f$\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}\f$, 592 where \f$\mathord{\relsym}\f$ is the relation symbol encoded 593 by \p relsym. 594 595 \param var 596 The left hand side variable of the generalized affine relation; 597 598 \param relsym 599 The relation symbol; 600 601 \param expr 602 The numerator of the right hand side affine expression; 603 604 \param denominator 605 The denominator of the right hand side affine expression (optional 606 argument with default value 1). 607 608 \exception Invalid_Argument_Exception 609 Thrown if \p denominator is zero or if \p expr and \p this are 610 dimension-incompatible or if \p var is not a space dimension of \p this 611 or if \p this is a C_Polyhedron and \p relsym is a strict 612 relation symbol. 613 */ generalized_affine_image(Variable var, Relation_Symbol relsym, Linear_Expression expr, Coefficient denominator)614 public native void generalized_affine_image(Variable var, 615 Relation_Symbol relsym, 616 Linear_Expression expr, 617 Coefficient denominator); 618 619 /*! \brief 620 Assigns to \p this the preimage of \p this with respect to the 621 \extref{Generalized_Affine_Relations, generalized affine relation} 622 \f$\mathrm{var}' \relsym \frac{\mathrm{expr}}{\mathrm{denominator}}\f$, 623 where \f$\mathord{\relsym}\f$ is the relation symbol encoded 624 by \p relsym. 625 626 \param var 627 The left hand side variable of the generalized affine relation; 628 629 \param relsym 630 The relation symbol; 631 632 \param expr 633 The numerator of the right hand side affine expression; 634 635 \param denominator 636 The denominator of the right hand side affine expression (optional 637 argument with default value 1). 638 639 \exception Invalid_Argument_Exception 640 Thrown if \p denominator is zero or if \p expr and \p this are 641 dimension-incompatible or if \p var is not a space dimension of \p this 642 or if \p this is a C_Polyhedron and \p relsym is a strict 643 relation symbol. 644 */ generalized_affine_preimage(Variable var, Relation_Symbol relsym, Linear_Expression expr, Coefficient denominator)645 public native void generalized_affine_preimage(Variable var, 646 Relation_Symbol relsym, 647 Linear_Expression expr, 648 Coefficient denominator); 649 650 /*! \brief 651 Assigns to \p this the image of \p this with respect to the 652 \extref{Generalized_Affine_Relations, generalized affine relation} 653 \f$\mathrm{lhs}' \relsym \mathrm{rhs}\f$, where 654 \f$\mathord{\relsym}\f$ is the relation symbol encoded by \p relsym. 655 656 \param lhs 657 The left hand side affine expression; 658 659 \param relsym 660 The relation symbol; 661 662 \param rhs 663 The right hand side affine expression. 664 665 \exception Invalid_Argument_Exception 666 Thrown if \p this is dimension-incompatible with \p lhs or \p rhs 667 or if \p this is a C_Polyhedron and \p relsym is a strict 668 relation symbol. 669 */ generalized_affine_image(Linear_Expression lhs, Relation_Symbol relsym, Linear_Expression rhs)670 public native void generalized_affine_image(Linear_Expression lhs, 671 Relation_Symbol relsym, 672 Linear_Expression rhs); 673 674 /*! \brief 675 Assigns to \p this the preimage of \p this with respect to the 676 \extref{Generalized_Affine_Relations, generalized affine relation} 677 \f$\mathrm{lhs}' \relsym \mathrm{rhs}\f$, where 678 \f$\mathord{\relsym}\f$ is the relation symbol encoded by \p relsym. 679 680 \param lhs 681 The left hand side affine expression; 682 683 \param relsym 684 The relation symbol; 685 686 \param rhs 687 The right hand side affine expression. 688 689 \exception Invalid_Argument_Exception 690 Thrown if \p this is dimension-incompatible with \p lhs or \p rhs 691 or if \p this is a C_Polyhedron and \p relsym is a strict 692 relation symbol. 693 */ generalized_affine_preimage(Linear_Expression lhs, Relation_Symbol relsym, Linear_Expression rhs)694 public native void generalized_affine_preimage(Linear_Expression lhs, 695 Relation_Symbol relsym, 696 Linear_Expression rhs); 697 698 /*! \brief 699 Computes the \extref{Cylindrification, cylindrification} of \p this 700 with respect to space dimension \p var, assigning the result to \p this. 701 702 \param var 703 The space dimension that will be unconstrained. 704 705 \exception Invalid_Argument_Exception 706 Thrown if \p var is not a space dimension of \p this. 707 */ unconstrain_space_dimension(Variable var)708 public native void unconstrain_space_dimension(Variable var); 709 710 /*! \brief 711 Computes the \extref{Cylindrification, cylindrification} of \p this 712 with respect to the set of space dimensions \p vars, 713 assigning the result to \p this. 714 715 \param vars 716 The set of space dimension that will be unconstrained. 717 718 \exception Invalid_Argument_Exception 719 Thrown if \p this is dimension-incompatible with one of the 720 Variable objects contained in \p vars. 721 */ unconstrain_space_dimensions(Variables_Set vars)722 public native void unconstrain_space_dimensions(Variables_Set vars); 723 724 /*! \brief 725 Assigns to \p this the result of computing the 726 \extref{H79_widening, H79-widening} between \p this and \p y. 727 728 \param y 729 A polyhedron that <EM>must</EM> be contained in \p this; 730 731 \param tp 732 A reference to an unsigned variable storing the number of 733 available tokens (to be used when applying the 734 \extref{Widening_with_Tokens, widening with tokens} delay technique). 735 736 \exception Invalid_Argument_Exception 737 Thrown if \p this and \p y are topology-incompatible or 738 dimension-incompatible. 739 */ widening_assign(Polyhedron y, By_Reference<Integer> tp)740 public native void widening_assign(Polyhedron y, 741 By_Reference<Integer> tp); 742 743 //@} // Space Dimension Preserving Member Functions that May Modify [...] 744 745 //! \name Member Functions that May Modify the Dimension of the Vector Space 746 //@{ 747 748 /*! \brief 749 Swaps \p this with polyhedron \p y. 750 (\p this and \p y can be dimension-incompatible.) 751 752 \exception Invalid_Argument_Exception 753 Thrown if \p x and \p y are topology-incompatible. 754 */ swap(Polyhedron y)755 public native void swap(Polyhedron y); 756 757 /*! \brief 758 Adds \p m new space dimensions and embeds the old polyhedron 759 in the new vector space. 760 761 \param m 762 The number of dimensions to add. 763 764 \exception Length_Error_Exception 765 Thrown if adding \p m new space dimensions would cause the 766 vector space to exceed dimension <CODE>max_space_dimension()</CODE>. 767 */ add_space_dimensions_and_embed(long m)768 public native void add_space_dimensions_and_embed(long m); 769 770 /*! \brief 771 Adds \p m new space dimensions to the polyhedron 772 and does not embed it in the new vector space. 773 774 \param m 775 The number of space dimensions to add. 776 777 \exception Length_Error_Exception 778 Thrown if adding \p m new space dimensions would cause the 779 vector space to exceed dimension <CODE>max_space_dimension()</CODE>. 780 */ add_space_dimensions_and_project(long m)781 public native void add_space_dimensions_and_project(long m); 782 783 /*! \brief 784 Assigns to \p this the \extref{Concatenating_Polyhedra, concatenation} 785 of \p this and \p y, taken in this order. 786 787 \exception Invalid_Argument_Exception 788 Thrown if \p this and \p y are topology-incompatible. 789 790 \exception Length_Error_Exception 791 Thrown if the concatenation would cause the vector space 792 to exceed dimension <CODE>max_space_dimension()</CODE>. 793 */ concatenate_assign(Polyhedron y)794 public native void concatenate_assign(Polyhedron y); 795 796 //! Removes all the specified dimensions from the vector space. 797 /*! 798 \param vars 799 The set of Variable objects corresponding to the space dimensions 800 to be removed. 801 802 \exception Invalid_Argument_Exception 803 Thrown if \p this is dimension-incompatible with one of the 804 Variable objects contained in \p vars. 805 */ remove_space_dimensions(Variables_Set vars)806 public native void remove_space_dimensions(Variables_Set vars); 807 808 /*! \brief 809 Removes the higher dimensions of the vector space so that 810 the resulting space will have dimension \p new_dimension. 811 812 \exception Invalid_Argument_Exception 813 Thrown if \p new_dimensions is greater than the space dimension of 814 \p this. 815 */ remove_higher_space_dimensions(long new_dimension)816 public native void remove_higher_space_dimensions(long 817 new_dimension); 818 819 //! Creates \p m copies of the space dimension corresponding to \p var. 820 /*! 821 \param var 822 The variable corresponding to the space dimension to be replicated; 823 824 \param m 825 The number of replicas to be created. 826 827 \exception Invalid_Argument_Exception 828 Thrown if \p var does not correspond to a dimension of the vector space. 829 830 \exception Length_Error_Exception 831 Thrown if adding \p m new space dimensions would cause the 832 vector space to exceed dimension <CODE>max_space_dimension()</CODE>. 833 */ expand_space_dimension(Variable var, long m)834 public native void expand_space_dimension(Variable var, long m); 835 836 //! Folds the space dimensions in \p vars into \p dest. 837 /*! 838 \param vars 839 The set of Variable objects corresponding to the space dimensions 840 to be folded; 841 842 \param dest 843 The variable corresponding to the space dimension that is the 844 destination of the folding operation. 845 846 \exception Invalid_Argument_Exception 847 Thrown if \p this is dimension-incompatible with \p dest or with 848 one of the Variable objects contained in \p vars. 849 Also thrown if \p dest is contained in \p vars. 850 */ fold_space_dimensions(Variables_Set vars, Variable dest)851 public native void fold_space_dimensions(Variables_Set vars, 852 Variable dest); 853 854 /*! \brief 855 Remaps the dimensions of the vector space according to 856 a \extref{Mapping_the_Dimensions_of_the_Vector_Space, partial function}. 857 858 \param pfunc 859 The partial function specifying the destiny of each space dimension. 860 */ map_space_dimensions(Partial_Function pfunc)861 public native void map_space_dimensions(Partial_Function pfunc); 862 863 //@} // Member Functions that May Modify the Dimension of the Vector Space 864 865 /*! \name Ad Hoc Functions for (C or NNC) Polyhedra 866 The functions listed here below, being specific of the polyhedron 867 domains, do not have a correspondence in other semantic geometric 868 descriptions. 869 */ 870 //@{ 871 872 //! Returns the system of generators. generators()873 public native Generator_System generators(); 874 875 //! Returns the system of generators, with no redundant generator. minimized_generators()876 public native Generator_System minimized_generators(); 877 878 /*! \brief 879 Adds a copy of generator \p g to the system of generators 880 of \p this (without minimizing the result). 881 882 \exception Invalid_Argument_Exception 883 Thrown if \p this and generator \p g are topology-incompatible or 884 dimension-incompatible, or if \p this is an empty polyhedron and 885 \p g is not a point. 886 */ add_generator(Generator g)887 public native void add_generator(Generator g); 888 889 /*! \brief 890 Adds a copy of the generators in \p gs to the system 891 of generators of \p this (without minimizing the result). 892 893 \param gs 894 Contains the generators that will be added to the system of 895 generators of \p this. 896 897 \exception Invalid_Argument_Exception 898 Thrown if \p this and \p gs are topology-incompatible or 899 dimension-incompatible, or if \p this is empty and the system of 900 generators \p gs is not empty, but has no points. 901 */ add_generators(Generator_System gs)902 public native void add_generators(Generator_System gs); 903 904 //! Same as upper_bound_assign. poly_hull_assign(Polyhedron y)905 public native void poly_hull_assign(Polyhedron y); 906 907 //! Same as difference_assign. poly_difference_assign(Polyhedron y)908 public native void poly_difference_assign(Polyhedron y); 909 910 /*! \brief 911 Assigns to \p this the result of computing the 912 \extref{BHRZ03_widening, BHRZ03-widening} between \p this and \p y. 913 914 \param y 915 A polyhedron that <EM>must</EM> be contained in \p this; 916 917 \param tp 918 A reference to an unsigned variable storing the number of 919 available tokens (to be used when applying the 920 \extref{Widening_with_Tokens, widening with tokens} delay technique). 921 922 \exception Invalid_Argument_Exception 923 Thrown if \p this and \p y are topology-incompatible or 924 dimension-incompatible. 925 */ BHRZ03_widening_assign(Polyhedron y, By_Reference<Integer> tp)926 public native void BHRZ03_widening_assign(Polyhedron y, 927 By_Reference<Integer> tp); 928 929 /*! \brief 930 Assigns to \p this the result of computing the 931 \extref{H79_widening, H79-widening} between \p this and \p y. 932 933 \param y 934 A polyhedron that <EM>must</EM> be contained in \p this; 935 936 \param tp 937 A reference to an unsigned variable storing the number of 938 available tokens (to be used when applying the 939 \extref{Widening_with_Tokens, widening with tokens} delay technique). 940 941 \exception Invalid_Argument_Exception 942 Thrown if \p this and \p y are topology-incompatible or 943 dimension-incompatible. 944 */ H79_widening_assign(Polyhedron y, By_Reference<Integer> tp)945 public native void H79_widening_assign(Polyhedron y, 946 By_Reference<Integer> tp); 947 948 /*! \brief 949 Improves the result of the \extref{BHRZ03_widening, BHRZ03-widening} 950 computation by also enforcing those constraints in \p cs that are 951 satisfied by all the points of \p this. 952 953 \param y 954 A polyhedron that <EM>must</EM> be contained in \p this; 955 956 \param cs 957 The system of constraints used to improve the widened polyhedron; 958 959 \param tp 960 A reference to an unsigned variable storing the number of 961 available tokens (to be used when applying the 962 \extref{Widening_with_Tokens, widening with tokens} delay technique). 963 964 \exception Invalid_Argument_Exception 965 Thrown if \p this, \p y and \p cs are topology-incompatible or 966 dimension-incompatible. 967 */ 968 public native limited_BHRZ03_extrapolation_assign(Polyhedron y, Constraint_System cs, By_Reference<Integer> tp)969 void limited_BHRZ03_extrapolation_assign(Polyhedron y, 970 Constraint_System cs, 971 By_Reference<Integer> tp); 972 973 /*! \brief 974 Improves the result of the \extref{H79_widening, H79-widening} 975 computation by also enforcing those constraints in \p cs that are 976 satisfied by all the points of \p this. 977 978 \param y 979 A polyhedron that <EM>must</EM> be contained in \p this; 980 981 \param cs 982 The system of constraints used to improve the widened polyhedron; 983 984 \param tp 985 A reference to an unsigned variable storing the number of 986 available tokens (to be used when applying the 987 \extref{Widening_with_Tokens, widening with tokens} delay technique). 988 989 \exception Invalid_Argument_Exception 990 Thrown if \p this, \p y and \p cs are topology-incompatible or 991 dimension-incompatible. 992 */ 993 public native limited_H79_extrapolation_assign(Polyhedron y, Constraint_System cs, By_Reference<Integer> tp)994 void limited_H79_extrapolation_assign(Polyhedron y, 995 Constraint_System cs, 996 By_Reference<Integer> tp); 997 998 /*! \brief 999 Improves the result of the \extref{BHRZ03_widening, BHRZ03-widening} 1000 computation by also enforcing those constraints in \p cs that are 1001 satisfied by all the points of \p this, plus all the constraints 1002 of the form \f$\pm x \leq r\f$ and \f$\pm x < r\f$, with 1003 \f$r \in \Qset\f$, that are satisfied by all the points of \p this. 1004 1005 \param y 1006 A polyhedron that <EM>must</EM> be contained in \p this; 1007 1008 \param cs 1009 The system of constraints used to improve the widened polyhedron; 1010 1011 \param tp 1012 A reference to an unsigned variable storing the number of 1013 available tokens (to be used when applying the 1014 \extref{Widening_with_Tokens, widening with tokens} delay technique). 1015 1016 \exception Invalid_Argument_Exception 1017 Thrown if \p this, \p y and \p cs are topology-incompatible or 1018 dimension-incompatible. 1019 */ 1020 public native bounded_BHRZ03_extrapolation_assign(Polyhedron y, Constraint_System cs, By_Reference<Integer> tp)1021 void bounded_BHRZ03_extrapolation_assign(Polyhedron y, 1022 Constraint_System cs, 1023 By_Reference<Integer> tp); 1024 1025 /*! \brief 1026 Improves the result of the \extref{H79_widening, H79-widening} 1027 computation by also enforcing those constraints in \p cs that are 1028 satisfied by all the points of \p this, plus all the constraints 1029 of the form \f$\pm x \leq r\f$ and \f$\pm x < r\f$, with 1030 \f$r \in \Qset\f$, that are satisfied by all the points of \p this. 1031 1032 \param y 1033 A polyhedron that <EM>must</EM> be contained in \p this; 1034 1035 \param cs 1036 The system of constraints used to improve the widened polyhedron; 1037 1038 \param tp 1039 A reference to an unsigned variable storing the number of 1040 available tokens (to be used when applying the 1041 \extref{Widening_with_Tokens, widening with tokens} delay technique). 1042 1043 \exception Invalid_Argument_Exception 1044 Thrown if \p this, \p y and \p cs are topology-incompatible or 1045 dimension-incompatible. 1046 */ 1047 public native bounded_H79_extrapolation_assign(Polyhedron y, Constraint_System cs, By_Reference<Integer> tp)1048 void bounded_H79_extrapolation_assign(Polyhedron y, 1049 Constraint_System cs, 1050 By_Reference<Integer> tp); 1051 1052 //@} // Ad Hoc Functions for (C or NNC) Polyhedra 1053 1054 } // class Polyhedron 1055 1056 1057 //! A topologically closed convex polyhedron. 1058 /*! \ingroup PPL_Java_interface */ 1059 public class C_Polyhedron extends Polyhedron { 1060 1061 //! \name Standard Constructors and Destructor 1062 //@{ 1063 1064 //! Builds a new C polyhedron of dimension \p d. 1065 /*! 1066 If \p kind is \c EMPTY, the newly created polyhedron will be empty; 1067 otherwise, it will be a universe polyhedron. 1068 */ C_Polyhedron(long d, Degenerate_Element kind)1069 public C_Polyhedron(long d, Degenerate_Element kind); 1070 1071 //! Builds a new C polyhedron that is copy of \p y. C_Polyhedron(C_Polyhedron y)1072 public C_Polyhedron(C_Polyhedron y); 1073 1074 //! Builds a new C polyhedron that is a copy of \p ph. 1075 /*! 1076 The complexity argument is ignored. 1077 */ C_Polyhedron(C_Polyhedron y, Complexity_Class complexity)1078 public C_Polyhedron(C_Polyhedron y, Complexity_Class complexity); 1079 1080 //! Builds a new C polyhedron from the system of constraints \p cs. 1081 /*! 1082 The new polyhedron will inherit the space dimension of \p cs. 1083 */ C_Polyhedron(Constraint_System cs)1084 public C_Polyhedron(Constraint_System cs); 1085 1086 //! Builds a new C polyhedron from the system of congruences \p cgs. 1087 /*! 1088 The new polyhedron will inherit the space dimension of \p cgs. 1089 */ C_Polyhedron(Congruence_System cgs)1090 public C_Polyhedron(Congruence_System cgs); 1091 1092 /*! \brief 1093 Releases all resources managed by \p this, 1094 also resetting it to a null reference. 1095 */ free()1096 public native void free(); 1097 1098 //@} // Standard Constructors and Destructor 1099 1100 /*! \name Constructors Behaving as Conversion Operators 1101 Besides the conversions listed here below, the library also 1102 provides conversion operators that build a semantic geometric 1103 description starting from \b any other semantic geometric 1104 description (e.g., <code>Grid(C_Polyhedron y)</code>, 1105 <code>C_Polyhedron(BD_Shape_mpq_class y)</code>, etc.). 1106 Clearly, the conversion operators are only available if both 1107 the source and the target semantic geometric descriptions have 1108 been enabled when configuring the library. 1109 The conversions also taking as argument a complexity class 1110 sometimes provide non-trivial precision/efficiency trade-offs. 1111 */ 1112 //@{ 1113 1114 /*! \brief 1115 Builds a C polyhedron that is a copy of the topological closure 1116 of the NNC polyhedron \p y. 1117 */ C_Polyhedron(NNC_Polyhedron y)1118 public C_Polyhedron(NNC_Polyhedron y); 1119 1120 /*! \brief 1121 Builds a C polyhedron that is a copy of the topological closure 1122 of the NNC polyhedron \p y. 1123 1124 The complexity argument is ignored, since the exact constructor 1125 has polynomial complexity. 1126 */ C_Polyhedron(NNC_Polyhedron y, Complexity_Class complexity)1127 public C_Polyhedron(NNC_Polyhedron y, Complexity_Class complexity); 1128 1129 //! Builds a new C polyhedron from the system of generators \p gs. 1130 /*! 1131 The new polyhedron will inherit the space dimension of \p gs. 1132 */ C_Polyhedron(Generator_System gs)1133 public C_Polyhedron(Generator_System gs); 1134 1135 //@} // Constructors Behaving as Conversion Operators 1136 1137 //! \name Other Methods 1138 //@{ 1139 1140 /*! \brief 1141 If the upper bound of \p this and \p y is exact it is assigned 1142 to \p this and \c true is returned; otherwise \c false is returned. 1143 1144 \exception Invalid_Argument_Exception 1145 Thrown if \p this and \p y are dimension-incompatible. 1146 */ upper_bound_assign_if_exact(C_Polyhedron y)1147 public native boolean upper_bound_assign_if_exact(C_Polyhedron y); 1148 1149 //@} // Other Methods. 1150 1151 //! Partitions \p q with respect to \p p. 1152 /*! 1153 Let \p p and \p q be two polyhedra. 1154 The function returns a pair object \p r such that 1155 - <CODE>r.first</CODE> is the intersection of \p p and \p q; 1156 - <CODE>r.second</CODE> has the property that all its elements are 1157 pairwise disjoint and disjoint from \p p; 1158 - the set-theoretical union of <CODE>r.first</CODE> with all the 1159 elements of <CODE>r.second</CODE> gives \p q (i.e., <CODE>r</CODE> 1160 is the representation of a partition of \p q). 1161 */ 1162 public static native 1163 Pair<C_Polyhedron, Pointset_Powerset_NNC_Polyhedron> linear_partition(C_Polyhedron p, C_Polyhedron q)1164 linear_partition(C_Polyhedron p, C_Polyhedron q); 1165 1166 //! Releases all resources managed by \p this. finalize()1167 protected native void finalize(); 1168 1169 } // class C_Polyhedron 1170 1171 1172 //! A powerset of C_Polyhedron objects. 1173 /*! \ingroup PPL_Java_interface 1174 The powerset domains can be instantiated by taking as a base domain 1175 any fixed semantic geometric description 1176 (C and NNC polyhedra, BD and octagonal shapes, boxes and grids). 1177 An element of the powerset domain represents a disjunctive collection 1178 of base objects (its disjuncts), all having the same space dimension. 1179 1180 Besides the methods that are available in all semantic geometric 1181 descriptions (whose documentation is not repeated here), 1182 the powerset domain also provides several ad hoc methods. 1183 In particular, the iterator types allow for the examination and 1184 manipulation of the collection of disjuncts. 1185 */ 1186 public class Pointset_Powerset_C_Polyhedron extends PPL_Object { 1187 1188 //! \name Ad Hoc Functions for Pointset_Powerset domains 1189 /*@{*/ 1190 1191 /*! \brief 1192 Drops from the sequence of disjuncts in \p this all the non-maximal 1193 elements, so that a non-redundant powerset if obtained. 1194 */ omega_reduce()1195 public native void omega_reduce(); 1196 1197 //! Returns the number of disjuncts. 1198 /*! 1199 If present, Omega-redundant elements will be counted too. 1200 */ size()1201 public native long size(); 1202 1203 //! Returns \c true if and only if \p this geometrically covers \p y. 1204 public native boolean geometrically_covers(Pointset_Powerset_C_Polyhedron y)1205 geometrically_covers(Pointset_Powerset_C_Polyhedron y); 1206 1207 //! Returns \c true if and only if \p this is geometrically equal to \p y. 1208 public native boolean geometrically_equals(Pointset_Powerset_C_Polyhedron y)1209 geometrically_equals(Pointset_Powerset_C_Polyhedron y); 1210 1211 /*! \brief 1212 Returns an iterator referring to the beginning of the sequence 1213 of disjuncts of \p this. 1214 */ begin_iterator()1215 public native Pointset_Powerset_C_Polyhedron_Iterator begin_iterator(); 1216 1217 /*! \brief 1218 Returns an iterator referring to past the end of the sequence 1219 of disjuncts of \p this. 1220 */ end_iterator()1221 public native Pointset_Powerset_C_Polyhedron_Iterator end_iterator(); 1222 1223 //! Adds to \p this a copy of disjunct \p d. add_disjunct(C_Polyhedron d)1224 public native void add_disjunct(C_Polyhedron d); 1225 1226 // FIXME: this method needs correction, as it returns nothing. 1227 /*! \brief 1228 Drops from \p this the disjunct referred by \p iter; returns an 1229 iterator referring to the disjunct following the dropped one. 1230 */ 1231 public native void drop_disjunct(Pointset_Powerset_C_Polyhedron_Iterator iter)1232 drop_disjunct(Pointset_Powerset_C_Polyhedron_Iterator iter); 1233 1234 1235 /*! \brief 1236 Drops from \p this all the disjuncts from \p first to \p last 1237 (excluded). 1238 */ 1239 public native void drop_disjuncts(Pointset_Powerset_C_Polyhedron_Iterator first, Pointset_Powerset_C_Polyhedron_Iterator last)1240 drop_disjuncts(Pointset_Powerset_C_Polyhedron_Iterator first, 1241 Pointset_Powerset_C_Polyhedron_Iterator last); 1242 1243 1244 /*! \brief 1245 Modifies \p this by (recursively) merging together the pairs of 1246 disjuncts whose upper-bound is the same as their set-theoretical union. 1247 */ pairwise_reduce()1248 public native void pairwise_reduce(); 1249 1250 /*@}*/ /* Ad Hoc Functions for Pointset_Powerset domains */ 1251 1252 } // class Pointset_Powerset_C_Polyhedron 1253 1254 1255 //! An iterator class for the disjuncts of a Pointset_Powerset_C_Polyhedron. 1256 /*! \ingroup PPL_Java_interface */ 1257 public class Pointset_Powerset_C_Polyhedron_Iterator extends PPL_Object { 1258 1259 //! Builds a copy of iterator \p y. Pointset_Powerset_C_Polyhedron_Iterator(Pointset_Powerset_C_Polyhedron_Iterator y)1260 public Pointset_Powerset_C_Polyhedron_Iterator 1261 (Pointset_Powerset_C_Polyhedron_Iterator y); 1262 1263 //! Returns \c true if and only if \p this and \p itr are equal. equals(Pointset_Powerset_C_Polyhedron_Iterator itr)1264 public native boolean equals(Pointset_Powerset_C_Polyhedron_Iterator itr); 1265 1266 //! Modifies \p this so that it refers to the next disjunct. next()1267 public native void next(); 1268 1269 //! Modifies \p this so that it refers to the previous disjunct. prev()1270 public native void prev(); 1271 1272 //! Returns the disjunct referenced by \p this. 1273 /*! 1274 \warning 1275 On exit, the C_Polyhedron disjunct is still owned by the powerset 1276 object: any function call on the owning powerset object may 1277 invalidate it. Moreover, the disjunct is meant to be immutable 1278 and should not be modified in any way (its resources will 1279 be released when deleting the owning powerset). If really needed, 1280 the disjunct may be copied into a new object, which will be under 1281 control of the user. 1282 */ get_disjunct()1283 public native C_Polyhedron get_disjunct(); 1284 1285 //! Releases resources and resets \p this to a null reference. free()1286 public native void free(); 1287 1288 //! Releases the resources managed by \p this. finalize()1289 protected native void finalize(); 1290 1291 } // class Pointset_Powerset_C_Polyhedron_Iterator 1292