1 /* Source code for an implementation of the Omega test, an integer 2 programming algorithm for dependence analysis, by William Pugh, 3 appeared in Supercomputing '91 and CACM Aug 92. 4 5 This code has no license restrictions, and is considered public 6 domain. 7 8 Changes copyright (C) 2005, 2006, 2007, 2008, 2009, 9 2010 Free Software Foundation, Inc. 10 Contributed by Sebastian Pop <sebastian.pop@inria.fr> 11 12 This file is part of GCC. 13 14 GCC is free software; you can redistribute it and/or modify it under 15 the terms of the GNU General Public License as published by the Free 16 Software Foundation; either version 3, or (at your option) any later 17 version. 18 19 GCC is distributed in the hope that it will be useful, but WITHOUT ANY 20 WARRANTY; without even the implied warranty of MERCHANTABILITY or 21 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 22 for more details. 23 24 You should have received a copy of the GNU General Public License 25 along with GCC; see the file COPYING3. If not see 26 <http://www.gnu.org/licenses/>. */ 27 28 /* For a detailed description, see "Constraint-Based Array Dependence 29 Analysis" William Pugh, David Wonnacott, TOPLAS'98 and David 30 Wonnacott's thesis: 31 ftp://ftp.cs.umd.edu/pub/omega/davewThesis/davewThesis.ps.gz 32 */ 33 34 #include "config.h" 35 #include "system.h" 36 #include "coretypes.h" 37 #include "tree.h" 38 #include "diagnostic-core.h" 39 #include "tree-pass.h" 40 #include "omega.h" 41 42 /* When set to true, keep substitution variables. When set to false, 43 resurrect substitution variables (convert substitutions back to EQs). */ 44 static bool omega_reduce_with_subs = true; 45 46 /* When set to true, omega_simplify_problem checks for problem with no 47 solutions, calling verify_omega_pb. */ 48 static bool omega_verify_simplification = false; 49 50 /* When set to true, only produce a single simplified result. */ 51 static bool omega_single_result = false; 52 53 /* Set return_single_result to 1 when omega_single_result is true. */ 54 static int return_single_result = 0; 55 56 /* Hash table for equations generated by the solver. */ 57 #define HASH_TABLE_SIZE PARAM_VALUE (PARAM_OMEGA_HASH_TABLE_SIZE) 58 #define MAX_KEYS PARAM_VALUE (PARAM_OMEGA_MAX_KEYS) 59 static eqn hash_master; 60 static int next_key; 61 static int hash_version = 0; 62 63 /* Set to true for making the solver enter in approximation mode. */ 64 static bool in_approximate_mode = false; 65 66 /* When set to zero, the solver is allowed to add new equalities to 67 the problem to be solved. */ 68 static int conservative = 0; 69 70 /* Set to omega_true when the problem was successfully reduced, set to 71 omega_unknown when the solver is unable to determine an answer. */ 72 static enum omega_result omega_found_reduction; 73 74 /* Set to true when the solver is allowed to add omega_red equations. */ 75 static bool create_color = false; 76 77 /* Set to nonzero when the problem to be solved can be reduced. */ 78 static int may_be_red = 0; 79 80 /* When false, there should be no substitution equations in the 81 simplified problem. */ 82 static int please_no_equalities_in_simplified_problems = 0; 83 84 /* Variables names for pretty printing. */ 85 static char wild_name[200][40]; 86 87 /* Pointer to the void problem. */ 88 static omega_pb no_problem = (omega_pb) 0; 89 90 /* Pointer to the problem to be solved. */ 91 static omega_pb original_problem = (omega_pb) 0; 92 93 94 /* Return the integer A divided by B. */ 95 96 static inline int 97 int_div (int a, int b) 98 { 99 if (a > 0) 100 return a/b; 101 else 102 return -((-a + b - 1)/b); 103 } 104 105 /* Return the integer A modulo B. */ 106 107 static inline int 108 int_mod (int a, int b) 109 { 110 return a - b * int_div (a, b); 111 } 112 113 /* Test whether equation E is red. */ 114 115 static inline bool 116 omega_eqn_is_red (eqn e, int desired_res) 117 { 118 return (desired_res == omega_simplify && e->color == omega_red); 119 } 120 121 /* Return a string for VARIABLE. */ 122 123 static inline char * 124 omega_var_to_str (int variable) 125 { 126 if (0 <= variable && variable <= 20) 127 return wild_name[variable]; 128 129 if (-20 < variable && variable < 0) 130 return wild_name[40 + variable]; 131 132 /* Collapse all the entries that would have overflowed. */ 133 return wild_name[21]; 134 } 135 136 /* Return a string for variable I in problem PB. */ 137 138 static inline char * 139 omega_variable_to_str (omega_pb pb, int i) 140 { 141 return omega_var_to_str (pb->var[i]); 142 } 143 144 /* Do nothing function: used for default initializations. */ 145 146 void 147 omega_no_procedure (omega_pb pb ATTRIBUTE_UNUSED) 148 { 149 } 150 151 void (*omega_when_reduced) (omega_pb) = omega_no_procedure; 152 153 /* Print to FILE from PB equation E with all its coefficients 154 multiplied by C. */ 155 156 static void 157 omega_print_term (FILE *file, omega_pb pb, eqn e, int c) 158 { 159 int i; 160 bool first = true; 161 int n = pb->num_vars; 162 int went_first = -1; 163 164 for (i = 1; i <= n; i++) 165 if (c * e->coef[i] > 0) 166 { 167 first = false; 168 went_first = i; 169 170 if (c * e->coef[i] == 1) 171 fprintf (file, "%s", omega_variable_to_str (pb, i)); 172 else 173 fprintf (file, "%d * %s", c * e->coef[i], 174 omega_variable_to_str (pb, i)); 175 break; 176 } 177 178 for (i = 1; i <= n; i++) 179 if (i != went_first && c * e->coef[i] != 0) 180 { 181 if (!first && c * e->coef[i] > 0) 182 fprintf (file, " + "); 183 184 first = false; 185 186 if (c * e->coef[i] == 1) 187 fprintf (file, "%s", omega_variable_to_str (pb, i)); 188 else if (c * e->coef[i] == -1) 189 fprintf (file, " - %s", omega_variable_to_str (pb, i)); 190 else 191 fprintf (file, "%d * %s", c * e->coef[i], 192 omega_variable_to_str (pb, i)); 193 } 194 195 if (!first && c * e->coef[0] > 0) 196 fprintf (file, " + "); 197 198 if (first || c * e->coef[0] != 0) 199 fprintf (file, "%d", c * e->coef[0]); 200 } 201 202 /* Print to FILE the equation E of problem PB. */ 203 204 void 205 omega_print_eqn (FILE *file, omega_pb pb, eqn e, bool test, int extra) 206 { 207 int i; 208 int n = pb->num_vars + extra; 209 bool is_lt = test && e->coef[0] == -1; 210 bool first; 211 212 if (test) 213 { 214 if (e->touched) 215 fprintf (file, "!"); 216 217 else if (e->key != 0) 218 fprintf (file, "%d: ", e->key); 219 } 220 221 if (e->color == omega_red) 222 fprintf (file, "["); 223 224 first = true; 225 226 for (i = is_lt ? 1 : 0; i <= n; i++) 227 if (e->coef[i] < 0) 228 { 229 if (!first) 230 fprintf (file, " + "); 231 else 232 first = false; 233 234 if (i == 0) 235 fprintf (file, "%d", -e->coef[i]); 236 else if (e->coef[i] == -1) 237 fprintf (file, "%s", omega_variable_to_str (pb, i)); 238 else 239 fprintf (file, "%d * %s", -e->coef[i], 240 omega_variable_to_str (pb, i)); 241 } 242 243 if (first) 244 { 245 if (is_lt) 246 { 247 fprintf (file, "1"); 248 is_lt = false; 249 } 250 else 251 fprintf (file, "0"); 252 } 253 254 if (test == 0) 255 fprintf (file, " = "); 256 else if (is_lt) 257 fprintf (file, " < "); 258 else 259 fprintf (file, " <= "); 260 261 first = true; 262 263 for (i = 0; i <= n; i++) 264 if (e->coef[i] > 0) 265 { 266 if (!first) 267 fprintf (file, " + "); 268 else 269 first = false; 270 271 if (i == 0) 272 fprintf (file, "%d", e->coef[i]); 273 else if (e->coef[i] == 1) 274 fprintf (file, "%s", omega_variable_to_str (pb, i)); 275 else 276 fprintf (file, "%d * %s", e->coef[i], 277 omega_variable_to_str (pb, i)); 278 } 279 280 if (first) 281 fprintf (file, "0"); 282 283 if (e->color == omega_red) 284 fprintf (file, "]"); 285 } 286 287 /* Print to FILE all the variables of problem PB. */ 288 289 static void 290 omega_print_vars (FILE *file, omega_pb pb) 291 { 292 int i; 293 294 fprintf (file, "variables = "); 295 296 if (pb->safe_vars > 0) 297 fprintf (file, "protected ("); 298 299 for (i = 1; i <= pb->num_vars; i++) 300 { 301 fprintf (file, "%s", omega_variable_to_str (pb, i)); 302 303 if (i == pb->safe_vars) 304 fprintf (file, ")"); 305 306 if (i < pb->num_vars) 307 fprintf (file, ", "); 308 } 309 310 fprintf (file, "\n"); 311 } 312 313 /* Debug problem PB. */ 314 315 DEBUG_FUNCTION void 316 debug_omega_problem (omega_pb pb) 317 { 318 omega_print_problem (stderr, pb); 319 } 320 321 /* Print to FILE problem PB. */ 322 323 void 324 omega_print_problem (FILE *file, omega_pb pb) 325 { 326 int e; 327 328 if (!pb->variables_initialized) 329 omega_initialize_variables (pb); 330 331 omega_print_vars (file, pb); 332 333 for (e = 0; e < pb->num_eqs; e++) 334 { 335 omega_print_eq (file, pb, &pb->eqs[e]); 336 fprintf (file, "\n"); 337 } 338 339 fprintf (file, "Done with EQ\n"); 340 341 for (e = 0; e < pb->num_geqs; e++) 342 { 343 omega_print_geq (file, pb, &pb->geqs[e]); 344 fprintf (file, "\n"); 345 } 346 347 fprintf (file, "Done with GEQ\n"); 348 349 for (e = 0; e < pb->num_subs; e++) 350 { 351 eqn eq = &pb->subs[e]; 352 353 if (eq->color == omega_red) 354 fprintf (file, "["); 355 356 if (eq->key > 0) 357 fprintf (file, "%s := ", omega_var_to_str (eq->key)); 358 else 359 fprintf (file, "#%d := ", eq->key); 360 361 omega_print_term (file, pb, eq, 1); 362 363 if (eq->color == omega_red) 364 fprintf (file, "]"); 365 366 fprintf (file, "\n"); 367 } 368 } 369 370 /* Return the number of equations in PB tagged omega_red. */ 371 372 int 373 omega_count_red_equations (omega_pb pb) 374 { 375 int e, i; 376 int result = 0; 377 378 for (e = 0; e < pb->num_eqs; e++) 379 if (pb->eqs[e].color == omega_red) 380 { 381 for (i = pb->num_vars; i > 0; i--) 382 if (pb->geqs[e].coef[i]) 383 break; 384 385 if (i == 0 && pb->geqs[e].coef[0] == 1) 386 return 0; 387 else 388 result += 2; 389 } 390 391 for (e = 0; e < pb->num_geqs; e++) 392 if (pb->geqs[e].color == omega_red) 393 result += 1; 394 395 for (e = 0; e < pb->num_subs; e++) 396 if (pb->subs[e].color == omega_red) 397 result += 2; 398 399 return result; 400 } 401 402 /* Print to FILE all the equations in PB that are tagged omega_red. */ 403 404 void 405 omega_print_red_equations (FILE *file, omega_pb pb) 406 { 407 int e; 408 409 if (!pb->variables_initialized) 410 omega_initialize_variables (pb); 411 412 omega_print_vars (file, pb); 413 414 for (e = 0; e < pb->num_eqs; e++) 415 if (pb->eqs[e].color == omega_red) 416 { 417 omega_print_eq (file, pb, &pb->eqs[e]); 418 fprintf (file, "\n"); 419 } 420 421 for (e = 0; e < pb->num_geqs; e++) 422 if (pb->geqs[e].color == omega_red) 423 { 424 omega_print_geq (file, pb, &pb->geqs[e]); 425 fprintf (file, "\n"); 426 } 427 428 for (e = 0; e < pb->num_subs; e++) 429 if (pb->subs[e].color == omega_red) 430 { 431 eqn eq = &pb->subs[e]; 432 fprintf (file, "["); 433 434 if (eq->key > 0) 435 fprintf (file, "%s := ", omega_var_to_str (eq->key)); 436 else 437 fprintf (file, "#%d := ", eq->key); 438 439 omega_print_term (file, pb, eq, 1); 440 fprintf (file, "]\n"); 441 } 442 } 443 444 /* Pretty print PB to FILE. */ 445 446 void 447 omega_pretty_print_problem (FILE *file, omega_pb pb) 448 { 449 int e, v, v1, v2, v3, t; 450 bool *live = XNEWVEC (bool, OMEGA_MAX_GEQS); 451 int stuffPrinted = 0; 452 bool change; 453 454 typedef enum { 455 none, le, lt 456 } partial_order_type; 457 458 partial_order_type **po = XNEWVEC (partial_order_type *, 459 OMEGA_MAX_VARS * OMEGA_MAX_VARS); 460 int **po_eq = XNEWVEC (int *, OMEGA_MAX_VARS * OMEGA_MAX_VARS); 461 int *last_links = XNEWVEC (int, OMEGA_MAX_VARS); 462 int *first_links = XNEWVEC (int, OMEGA_MAX_VARS); 463 int *chain_length = XNEWVEC (int, OMEGA_MAX_VARS); 464 int *chain = XNEWVEC (int, OMEGA_MAX_VARS); 465 int i, m; 466 bool multiprint; 467 468 if (!pb->variables_initialized) 469 omega_initialize_variables (pb); 470 471 if (pb->num_vars > 0) 472 { 473 omega_eliminate_redundant (pb, false); 474 475 for (e = 0; e < pb->num_eqs; e++) 476 { 477 if (stuffPrinted) 478 fprintf (file, "; "); 479 480 stuffPrinted = 1; 481 omega_print_eq (file, pb, &pb->eqs[e]); 482 } 483 484 for (e = 0; e < pb->num_geqs; e++) 485 live[e] = true; 486 487 while (1) 488 { 489 for (v = 1; v <= pb->num_vars; v++) 490 { 491 last_links[v] = first_links[v] = 0; 492 chain_length[v] = 0; 493 494 for (v2 = 1; v2 <= pb->num_vars; v2++) 495 po[v][v2] = none; 496 } 497 498 for (e = 0; e < pb->num_geqs; e++) 499 if (live[e]) 500 { 501 for (v = 1; v <= pb->num_vars; v++) 502 if (pb->geqs[e].coef[v] == 1) 503 first_links[v]++; 504 else if (pb->geqs[e].coef[v] == -1) 505 last_links[v]++; 506 507 v1 = pb->num_vars; 508 509 while (v1 > 0 && pb->geqs[e].coef[v1] == 0) 510 v1--; 511 512 v2 = v1 - 1; 513 514 while (v2 > 0 && pb->geqs[e].coef[v2] == 0) 515 v2--; 516 517 v3 = v2 - 1; 518 519 while (v3 > 0 && pb->geqs[e].coef[v3] == 0) 520 v3--; 521 522 if (pb->geqs[e].coef[0] > 0 || pb->geqs[e].coef[0] < -1 523 || v2 <= 0 || v3 > 0 524 || pb->geqs[e].coef[v1] * pb->geqs[e].coef[v2] != -1) 525 { 526 /* Not a partial order relation. */ 527 } 528 else 529 { 530 if (pb->geqs[e].coef[v1] == 1) 531 { 532 v3 = v2; 533 v2 = v1; 534 v1 = v3; 535 } 536 537 /* Relation is v1 <= v2 or v1 < v2. */ 538 po[v1][v2] = ((pb->geqs[e].coef[0] == 0) ? le : lt); 539 po_eq[v1][v2] = e; 540 } 541 } 542 for (v = 1; v <= pb->num_vars; v++) 543 chain_length[v] = last_links[v]; 544 545 /* Just in case pb->num_vars <= 0. */ 546 change = false; 547 for (t = 0; t < pb->num_vars; t++) 548 { 549 change = false; 550 551 for (v1 = 1; v1 <= pb->num_vars; v1++) 552 for (v2 = 1; v2 <= pb->num_vars; v2++) 553 if (po[v1][v2] != none && 554 chain_length[v1] <= chain_length[v2]) 555 { 556 chain_length[v1] = chain_length[v2] + 1; 557 change = true; 558 } 559 } 560 561 /* Caught in cycle. */ 562 gcc_assert (!change); 563 564 for (v1 = 1; v1 <= pb->num_vars; v1++) 565 if (chain_length[v1] == 0) 566 first_links[v1] = 0; 567 568 v = 1; 569 570 for (v1 = 2; v1 <= pb->num_vars; v1++) 571 if (chain_length[v1] + first_links[v1] > 572 chain_length[v] + first_links[v]) 573 v = v1; 574 575 if (chain_length[v] + first_links[v] == 0) 576 break; 577 578 if (stuffPrinted) 579 fprintf (file, "; "); 580 581 stuffPrinted = 1; 582 583 /* Chain starts at v. */ 584 { 585 int tmp; 586 bool first = true; 587 588 for (e = 0; e < pb->num_geqs; e++) 589 if (live[e] && pb->geqs[e].coef[v] == 1) 590 { 591 if (!first) 592 fprintf (file, ", "); 593 594 tmp = pb->geqs[e].coef[v]; 595 pb->geqs[e].coef[v] = 0; 596 omega_print_term (file, pb, &pb->geqs[e], -1); 597 pb->geqs[e].coef[v] = tmp; 598 live[e] = false; 599 first = false; 600 } 601 602 if (!first) 603 fprintf (file, " <= "); 604 } 605 606 /* Find chain. */ 607 chain[0] = v; 608 m = 1; 609 while (1) 610 { 611 /* Print chain. */ 612 for (v2 = 1; v2 <= pb->num_vars; v2++) 613 if (po[v][v2] && chain_length[v] == 1 + chain_length[v2]) 614 break; 615 616 if (v2 > pb->num_vars) 617 break; 618 619 chain[m++] = v2; 620 v = v2; 621 } 622 623 fprintf (file, "%s", omega_variable_to_str (pb, chain[0])); 624 625 for (multiprint = false, i = 1; i < m; i++) 626 { 627 v = chain[i - 1]; 628 v2 = chain[i]; 629 630 if (po[v][v2] == le) 631 fprintf (file, " <= "); 632 else 633 fprintf (file, " < "); 634 635 fprintf (file, "%s", omega_variable_to_str (pb, v2)); 636 live[po_eq[v][v2]] = false; 637 638 if (!multiprint && i < m - 1) 639 for (v3 = 1; v3 <= pb->num_vars; v3++) 640 { 641 if (v == v3 || v2 == v3 642 || po[v][v2] != po[v][v3] 643 || po[v2][chain[i + 1]] != po[v3][chain[i + 1]]) 644 continue; 645 646 fprintf (file, ",%s", omega_variable_to_str (pb, v3)); 647 live[po_eq[v][v3]] = false; 648 live[po_eq[v3][chain[i + 1]]] = false; 649 multiprint = true; 650 } 651 else 652 multiprint = false; 653 } 654 655 v = chain[m - 1]; 656 /* Print last_links. */ 657 { 658 int tmp; 659 bool first = true; 660 661 for (e = 0; e < pb->num_geqs; e++) 662 if (live[e] && pb->geqs[e].coef[v] == -1) 663 { 664 if (!first) 665 fprintf (file, ", "); 666 else 667 fprintf (file, " <= "); 668 669 tmp = pb->geqs[e].coef[v]; 670 pb->geqs[e].coef[v] = 0; 671 omega_print_term (file, pb, &pb->geqs[e], 1); 672 pb->geqs[e].coef[v] = tmp; 673 live[e] = false; 674 first = false; 675 } 676 } 677 } 678 679 for (e = 0; e < pb->num_geqs; e++) 680 if (live[e]) 681 { 682 if (stuffPrinted) 683 fprintf (file, "; "); 684 stuffPrinted = 1; 685 omega_print_geq (file, pb, &pb->geqs[e]); 686 } 687 688 for (e = 0; e < pb->num_subs; e++) 689 { 690 eqn eq = &pb->subs[e]; 691 692 if (stuffPrinted) 693 fprintf (file, "; "); 694 695 stuffPrinted = 1; 696 697 if (eq->key > 0) 698 fprintf (file, "%s := ", omega_var_to_str (eq->key)); 699 else 700 fprintf (file, "#%d := ", eq->key); 701 702 omega_print_term (file, pb, eq, 1); 703 } 704 } 705 706 free (live); 707 free (po); 708 free (po_eq); 709 free (last_links); 710 free (first_links); 711 free (chain_length); 712 free (chain); 713 } 714 715 /* Assign to variable I in PB the next wildcard name. The name of a 716 wildcard is a negative number. */ 717 static int next_wild_card = 0; 718 719 static void 720 omega_name_wild_card (omega_pb pb, int i) 721 { 722 --next_wild_card; 723 if (next_wild_card < -PARAM_VALUE (PARAM_OMEGA_MAX_WILD_CARDS)) 724 next_wild_card = -1; 725 pb->var[i] = next_wild_card; 726 } 727 728 /* Return the index of the last protected (or safe) variable in PB, 729 after having added a new wildcard variable. */ 730 731 static int 732 omega_add_new_wild_card (omega_pb pb) 733 { 734 int e; 735 int i = ++pb->safe_vars; 736 pb->num_vars++; 737 738 /* Make a free place in the protected (safe) variables, by moving 739 the non protected variable pointed by "I" at the end, ie. at 740 offset pb->num_vars. */ 741 if (pb->num_vars != i) 742 { 743 /* Move "I" for all the inequalities. */ 744 for (e = pb->num_geqs - 1; e >= 0; e--) 745 { 746 if (pb->geqs[e].coef[i]) 747 pb->geqs[e].touched = 1; 748 749 pb->geqs[e].coef[pb->num_vars] = pb->geqs[e].coef[i]; 750 } 751 752 /* Move "I" for all the equalities. */ 753 for (e = pb->num_eqs - 1; e >= 0; e--) 754 pb->eqs[e].coef[pb->num_vars] = pb->eqs[e].coef[i]; 755 756 /* Move "I" for all the substitutions. */ 757 for (e = pb->num_subs - 1; e >= 0; e--) 758 pb->subs[e].coef[pb->num_vars] = pb->subs[e].coef[i]; 759 760 /* Move the identifier. */ 761 pb->var[pb->num_vars] = pb->var[i]; 762 } 763 764 /* Initialize at zero all the coefficients */ 765 for (e = pb->num_geqs - 1; e >= 0; e--) 766 pb->geqs[e].coef[i] = 0; 767 768 for (e = pb->num_eqs - 1; e >= 0; e--) 769 pb->eqs[e].coef[i] = 0; 770 771 for (e = pb->num_subs - 1; e >= 0; e--) 772 pb->subs[e].coef[i] = 0; 773 774 /* And give it a name. */ 775 omega_name_wild_card (pb, i); 776 return i; 777 } 778 779 /* Delete inequality E from problem PB that has N_VARS variables. */ 780 781 static void 782 omega_delete_geq (omega_pb pb, int e, int n_vars) 783 { 784 if (dump_file && (dump_flags & TDF_DETAILS)) 785 { 786 fprintf (dump_file, "Deleting %d (last:%d): ", e, pb->num_geqs - 1); 787 omega_print_geq (dump_file, pb, &pb->geqs[e]); 788 fprintf (dump_file, "\n"); 789 } 790 791 if (e < pb->num_geqs - 1) 792 omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars); 793 794 pb->num_geqs--; 795 } 796 797 /* Delete extra inequality E from problem PB that has N_VARS 798 variables. */ 799 800 static void 801 omega_delete_geq_extra (omega_pb pb, int e, int n_vars) 802 { 803 if (dump_file && (dump_flags & TDF_DETAILS)) 804 { 805 fprintf (dump_file, "Deleting %d: ",e); 806 omega_print_geq_extra (dump_file, pb, &pb->geqs[e]); 807 fprintf (dump_file, "\n"); 808 } 809 810 if (e < pb->num_geqs - 1) 811 omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars); 812 813 pb->num_geqs--; 814 } 815 816 817 /* Remove variable I from problem PB. */ 818 819 static void 820 omega_delete_variable (omega_pb pb, int i) 821 { 822 int n_vars = pb->num_vars; 823 int e; 824 825 if (omega_safe_var_p (pb, i)) 826 { 827 int j = pb->safe_vars; 828 829 for (e = pb->num_geqs - 1; e >= 0; e--) 830 { 831 pb->geqs[e].touched = 1; 832 pb->geqs[e].coef[i] = pb->geqs[e].coef[j]; 833 pb->geqs[e].coef[j] = pb->geqs[e].coef[n_vars]; 834 } 835 836 for (e = pb->num_eqs - 1; e >= 0; e--) 837 { 838 pb->eqs[e].coef[i] = pb->eqs[e].coef[j]; 839 pb->eqs[e].coef[j] = pb->eqs[e].coef[n_vars]; 840 } 841 842 for (e = pb->num_subs - 1; e >= 0; e--) 843 { 844 pb->subs[e].coef[i] = pb->subs[e].coef[j]; 845 pb->subs[e].coef[j] = pb->subs[e].coef[n_vars]; 846 } 847 848 pb->var[i] = pb->var[j]; 849 pb->var[j] = pb->var[n_vars]; 850 } 851 else if (i < n_vars) 852 { 853 for (e = pb->num_geqs - 1; e >= 0; e--) 854 if (pb->geqs[e].coef[n_vars]) 855 { 856 pb->geqs[e].coef[i] = pb->geqs[e].coef[n_vars]; 857 pb->geqs[e].touched = 1; 858 } 859 860 for (e = pb->num_eqs - 1; e >= 0; e--) 861 pb->eqs[e].coef[i] = pb->eqs[e].coef[n_vars]; 862 863 for (e = pb->num_subs - 1; e >= 0; e--) 864 pb->subs[e].coef[i] = pb->subs[e].coef[n_vars]; 865 866 pb->var[i] = pb->var[n_vars]; 867 } 868 869 if (omega_safe_var_p (pb, i)) 870 pb->safe_vars--; 871 872 pb->num_vars--; 873 } 874 875 /* Because the coefficients of an equation are sparse, PACKING records 876 indices for non null coefficients. */ 877 static int *packing; 878 879 /* Set up the coefficients of PACKING, following the coefficients of 880 equation EQN that has NUM_VARS variables. */ 881 882 static inline int 883 setup_packing (eqn eqn, int num_vars) 884 { 885 int k; 886 int n = 0; 887 888 for (k = num_vars; k >= 0; k--) 889 if (eqn->coef[k]) 890 packing[n++] = k; 891 892 return n; 893 } 894 895 /* Computes a linear combination of EQ and SUB at VAR with coefficient 896 C, such that EQ->coef[VAR] is set to 0. TOP_VAR is the number of 897 non null indices of SUB stored in PACKING. */ 898 899 static inline void 900 omega_substitute_red_1 (eqn eq, eqn sub, int var, int c, bool *found_black, 901 int top_var) 902 { 903 if (eq->coef[var] != 0) 904 { 905 if (eq->color == omega_black) 906 *found_black = true; 907 else 908 { 909 int j, k = eq->coef[var]; 910 911 eq->coef[var] = 0; 912 913 for (j = top_var; j >= 0; j--) 914 eq->coef[packing[j]] -= sub->coef[packing[j]] * k * c; 915 } 916 } 917 } 918 919 /* Substitute in PB variable VAR with "C * SUB". */ 920 921 static void 922 omega_substitute_red (omega_pb pb, eqn sub, int var, int c, bool *found_black) 923 { 924 int e, top_var = setup_packing (sub, pb->num_vars); 925 926 *found_black = false; 927 928 if (dump_file && (dump_flags & TDF_DETAILS)) 929 { 930 if (sub->color == omega_red) 931 fprintf (dump_file, "["); 932 933 fprintf (dump_file, "substituting using %s := ", 934 omega_variable_to_str (pb, var)); 935 omega_print_term (dump_file, pb, sub, -c); 936 937 if (sub->color == omega_red) 938 fprintf (dump_file, "]"); 939 940 fprintf (dump_file, "\n"); 941 omega_print_vars (dump_file, pb); 942 } 943 944 for (e = pb->num_eqs - 1; e >= 0; e--) 945 { 946 eqn eqn = &(pb->eqs[e]); 947 948 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var); 949 950 if (dump_file && (dump_flags & TDF_DETAILS)) 951 { 952 omega_print_eq (dump_file, pb, eqn); 953 fprintf (dump_file, "\n"); 954 } 955 } 956 957 for (e = pb->num_geqs - 1; e >= 0; e--) 958 { 959 eqn eqn = &(pb->geqs[e]); 960 961 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var); 962 963 if (eqn->coef[var] && eqn->color == omega_red) 964 eqn->touched = 1; 965 966 if (dump_file && (dump_flags & TDF_DETAILS)) 967 { 968 omega_print_geq (dump_file, pb, eqn); 969 fprintf (dump_file, "\n"); 970 } 971 } 972 973 for (e = pb->num_subs - 1; e >= 0; e--) 974 { 975 eqn eqn = &(pb->subs[e]); 976 977 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var); 978 979 if (dump_file && (dump_flags & TDF_DETAILS)) 980 { 981 fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key)); 982 omega_print_term (dump_file, pb, eqn, 1); 983 fprintf (dump_file, "\n"); 984 } 985 } 986 987 if (dump_file && (dump_flags & TDF_DETAILS)) 988 fprintf (dump_file, "---\n\n"); 989 990 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var)) 991 *found_black = true; 992 } 993 994 /* Substitute in PB variable VAR with "C * SUB". */ 995 996 static void 997 omega_substitute (omega_pb pb, eqn sub, int var, int c) 998 { 999 int e, j, j0; 1000 int top_var = setup_packing (sub, pb->num_vars); 1001 1002 if (dump_file && (dump_flags & TDF_DETAILS)) 1003 { 1004 fprintf (dump_file, "substituting using %s := ", 1005 omega_variable_to_str (pb, var)); 1006 omega_print_term (dump_file, pb, sub, -c); 1007 fprintf (dump_file, "\n"); 1008 omega_print_vars (dump_file, pb); 1009 } 1010 1011 if (top_var < 0) 1012 { 1013 for (e = pb->num_eqs - 1; e >= 0; e--) 1014 pb->eqs[e].coef[var] = 0; 1015 1016 for (e = pb->num_geqs - 1; e >= 0; e--) 1017 if (pb->geqs[e].coef[var] != 0) 1018 { 1019 pb->geqs[e].touched = 1; 1020 pb->geqs[e].coef[var] = 0; 1021 } 1022 1023 for (e = pb->num_subs - 1; e >= 0; e--) 1024 pb->subs[e].coef[var] = 0; 1025 1026 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var)) 1027 { 1028 int k; 1029 eqn eqn = &(pb->subs[pb->num_subs++]); 1030 1031 for (k = pb->num_vars; k >= 0; k--) 1032 eqn->coef[k] = 0; 1033 1034 eqn->key = pb->var[var]; 1035 eqn->color = omega_black; 1036 } 1037 } 1038 else if (top_var == 0 && packing[0] == 0) 1039 { 1040 c = -sub->coef[0] * c; 1041 1042 for (e = pb->num_eqs - 1; e >= 0; e--) 1043 { 1044 pb->eqs[e].coef[0] += pb->eqs[e].coef[var] * c; 1045 pb->eqs[e].coef[var] = 0; 1046 } 1047 1048 for (e = pb->num_geqs - 1; e >= 0; e--) 1049 if (pb->geqs[e].coef[var] != 0) 1050 { 1051 pb->geqs[e].coef[0] += pb->geqs[e].coef[var] * c; 1052 pb->geqs[e].coef[var] = 0; 1053 pb->geqs[e].touched = 1; 1054 } 1055 1056 for (e = pb->num_subs - 1; e >= 0; e--) 1057 { 1058 pb->subs[e].coef[0] += pb->subs[e].coef[var] * c; 1059 pb->subs[e].coef[var] = 0; 1060 } 1061 1062 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var)) 1063 { 1064 int k; 1065 eqn eqn = &(pb->subs[pb->num_subs++]); 1066 1067 for (k = pb->num_vars; k >= 1; k--) 1068 eqn->coef[k] = 0; 1069 1070 eqn->coef[0] = c; 1071 eqn->key = pb->var[var]; 1072 eqn->color = omega_black; 1073 } 1074 1075 if (dump_file && (dump_flags & TDF_DETAILS)) 1076 { 1077 fprintf (dump_file, "---\n\n"); 1078 omega_print_problem (dump_file, pb); 1079 fprintf (dump_file, "===\n\n"); 1080 } 1081 } 1082 else 1083 { 1084 for (e = pb->num_eqs - 1; e >= 0; e--) 1085 { 1086 eqn eqn = &(pb->eqs[e]); 1087 int k = eqn->coef[var]; 1088 1089 if (k != 0) 1090 { 1091 k = c * k; 1092 eqn->coef[var] = 0; 1093 1094 for (j = top_var; j >= 0; j--) 1095 { 1096 j0 = packing[j]; 1097 eqn->coef[j0] -= sub->coef[j0] * k; 1098 } 1099 } 1100 1101 if (dump_file && (dump_flags & TDF_DETAILS)) 1102 { 1103 omega_print_eq (dump_file, pb, eqn); 1104 fprintf (dump_file, "\n"); 1105 } 1106 } 1107 1108 for (e = pb->num_geqs - 1; e >= 0; e--) 1109 { 1110 eqn eqn = &(pb->geqs[e]); 1111 int k = eqn->coef[var]; 1112 1113 if (k != 0) 1114 { 1115 k = c * k; 1116 eqn->touched = 1; 1117 eqn->coef[var] = 0; 1118 1119 for (j = top_var; j >= 0; j--) 1120 { 1121 j0 = packing[j]; 1122 eqn->coef[j0] -= sub->coef[j0] * k; 1123 } 1124 } 1125 1126 if (dump_file && (dump_flags & TDF_DETAILS)) 1127 { 1128 omega_print_geq (dump_file, pb, eqn); 1129 fprintf (dump_file, "\n"); 1130 } 1131 } 1132 1133 for (e = pb->num_subs - 1; e >= 0; e--) 1134 { 1135 eqn eqn = &(pb->subs[e]); 1136 int k = eqn->coef[var]; 1137 1138 if (k != 0) 1139 { 1140 k = c * k; 1141 eqn->coef[var] = 0; 1142 1143 for (j = top_var; j >= 0; j--) 1144 { 1145 j0 = packing[j]; 1146 eqn->coef[j0] -= sub->coef[j0] * k; 1147 } 1148 } 1149 1150 if (dump_file && (dump_flags & TDF_DETAILS)) 1151 { 1152 fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key)); 1153 omega_print_term (dump_file, pb, eqn, 1); 1154 fprintf (dump_file, "\n"); 1155 } 1156 } 1157 1158 if (dump_file && (dump_flags & TDF_DETAILS)) 1159 { 1160 fprintf (dump_file, "---\n\n"); 1161 omega_print_problem (dump_file, pb); 1162 fprintf (dump_file, "===\n\n"); 1163 } 1164 1165 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var)) 1166 { 1167 int k; 1168 eqn eqn = &(pb->subs[pb->num_subs++]); 1169 c = -c; 1170 1171 for (k = pb->num_vars; k >= 0; k--) 1172 eqn->coef[k] = c * (sub->coef[k]); 1173 1174 eqn->key = pb->var[var]; 1175 eqn->color = sub->color; 1176 } 1177 } 1178 } 1179 1180 /* Solve e = factor alpha for x_j and substitute. */ 1181 1182 static void 1183 omega_do_mod (omega_pb pb, int factor, int e, int j) 1184 { 1185 int k, i; 1186 eqn eq = omega_alloc_eqns (0, 1); 1187 int nfactor; 1188 bool kill_j = false; 1189 1190 omega_copy_eqn (eq, &pb->eqs[e], pb->num_vars); 1191 1192 for (k = pb->num_vars; k >= 0; k--) 1193 { 1194 eq->coef[k] = int_mod (eq->coef[k], factor); 1195 1196 if (2 * eq->coef[k] >= factor) 1197 eq->coef[k] -= factor; 1198 } 1199 1200 nfactor = eq->coef[j]; 1201 1202 if (omega_safe_var_p (pb, j) && !omega_wildcard_p (pb, j)) 1203 { 1204 i = omega_add_new_wild_card (pb); 1205 eq->coef[pb->num_vars] = eq->coef[i]; 1206 eq->coef[j] = 0; 1207 eq->coef[i] = -factor; 1208 kill_j = true; 1209 } 1210 else 1211 { 1212 eq->coef[j] = -factor; 1213 if (!omega_wildcard_p (pb, j)) 1214 omega_name_wild_card (pb, j); 1215 } 1216 1217 omega_substitute (pb, eq, j, nfactor); 1218 1219 for (k = pb->num_vars; k >= 0; k--) 1220 pb->eqs[e].coef[k] = pb->eqs[e].coef[k] / factor; 1221 1222 if (kill_j) 1223 omega_delete_variable (pb, j); 1224 1225 if (dump_file && (dump_flags & TDF_DETAILS)) 1226 { 1227 fprintf (dump_file, "Mod-ing and normalizing produces:\n"); 1228 omega_print_problem (dump_file, pb); 1229 } 1230 1231 omega_free_eqns (eq, 1); 1232 } 1233 1234 /* Multiplies by -1 inequality E. */ 1235 1236 void 1237 omega_negate_geq (omega_pb pb, int e) 1238 { 1239 int i; 1240 1241 for (i = pb->num_vars; i >= 0; i--) 1242 pb->geqs[e].coef[i] *= -1; 1243 1244 pb->geqs[e].coef[0]--; 1245 pb->geqs[e].touched = 1; 1246 } 1247 1248 /* Returns OMEGA_TRUE when problem PB has a solution. */ 1249 1250 static enum omega_result 1251 verify_omega_pb (omega_pb pb) 1252 { 1253 enum omega_result result; 1254 int e; 1255 bool any_color = false; 1256 omega_pb tmp_problem = XNEW (struct omega_pb_d); 1257 1258 omega_copy_problem (tmp_problem, pb); 1259 tmp_problem->safe_vars = 0; 1260 tmp_problem->num_subs = 0; 1261 1262 for (e = pb->num_geqs - 1; e >= 0; e--) 1263 if (pb->geqs[e].color == omega_red) 1264 { 1265 any_color = true; 1266 break; 1267 } 1268 1269 if (please_no_equalities_in_simplified_problems) 1270 any_color = true; 1271 1272 if (any_color) 1273 original_problem = no_problem; 1274 else 1275 original_problem = pb; 1276 1277 if (dump_file && (dump_flags & TDF_DETAILS)) 1278 { 1279 fprintf (dump_file, "verifying problem"); 1280 1281 if (any_color) 1282 fprintf (dump_file, " (color mode)"); 1283 1284 fprintf (dump_file, " :\n"); 1285 omega_print_problem (dump_file, pb); 1286 } 1287 1288 result = omega_solve_problem (tmp_problem, omega_unknown); 1289 original_problem = no_problem; 1290 free (tmp_problem); 1291 1292 if (dump_file && (dump_flags & TDF_DETAILS)) 1293 { 1294 if (result != omega_false) 1295 fprintf (dump_file, "verified problem\n"); 1296 else 1297 fprintf (dump_file, "disproved problem\n"); 1298 omega_print_problem (dump_file, pb); 1299 } 1300 1301 return result; 1302 } 1303 1304 /* Add a new equality to problem PB at last position E. */ 1305 1306 static void 1307 adding_equality_constraint (omega_pb pb, int e) 1308 { 1309 if (original_problem != no_problem 1310 && original_problem != pb 1311 && !conservative) 1312 { 1313 int i, j; 1314 int e2 = original_problem->num_eqs++; 1315 1316 if (dump_file && (dump_flags & TDF_DETAILS)) 1317 fprintf (dump_file, 1318 "adding equality constraint %d to outer problem\n", e2); 1319 omega_init_eqn_zero (&original_problem->eqs[e2], 1320 original_problem->num_vars); 1321 1322 for (i = pb->num_vars; i >= 1; i--) 1323 { 1324 for (j = original_problem->num_vars; j >= 1; j--) 1325 if (original_problem->var[j] == pb->var[i]) 1326 break; 1327 1328 if (j <= 0) 1329 { 1330 if (dump_file && (dump_flags & TDF_DETAILS)) 1331 fprintf (dump_file, "retracting\n"); 1332 original_problem->num_eqs--; 1333 return; 1334 } 1335 original_problem->eqs[e2].coef[j] = pb->eqs[e].coef[i]; 1336 } 1337 1338 original_problem->eqs[e2].coef[0] = pb->eqs[e].coef[0]; 1339 1340 if (dump_file && (dump_flags & TDF_DETAILS)) 1341 omega_print_problem (dump_file, original_problem); 1342 } 1343 } 1344 1345 static int *fast_lookup; 1346 static int *fast_lookup_red; 1347 1348 typedef enum { 1349 normalize_false, 1350 normalize_uncoupled, 1351 normalize_coupled 1352 } normalize_return_type; 1353 1354 /* Normalizes PB by removing redundant constraints. Returns 1355 normalize_false when the constraints system has no solution, 1356 otherwise returns normalize_coupled or normalize_uncoupled. */ 1357 1358 static normalize_return_type 1359 normalize_omega_problem (omega_pb pb) 1360 { 1361 int e, i, j, k, n_vars; 1362 int coupled_subscripts = 0; 1363 1364 n_vars = pb->num_vars; 1365 1366 for (e = 0; e < pb->num_geqs; e++) 1367 { 1368 if (!pb->geqs[e].touched) 1369 { 1370 if (!single_var_geq (&pb->geqs[e], n_vars)) 1371 coupled_subscripts = 1; 1372 } 1373 else 1374 { 1375 int g, top_var, i0, hashCode; 1376 int *p = &packing[0]; 1377 1378 for (k = 1; k <= n_vars; k++) 1379 if (pb->geqs[e].coef[k]) 1380 *(p++) = k; 1381 1382 top_var = (p - &packing[0]) - 1; 1383 1384 if (top_var == -1) 1385 { 1386 if (pb->geqs[e].coef[0] < 0) 1387 { 1388 if (dump_file && (dump_flags & TDF_DETAILS)) 1389 { 1390 omega_print_geq (dump_file, pb, &pb->geqs[e]); 1391 fprintf (dump_file, "\nequations have no solution \n"); 1392 } 1393 return normalize_false; 1394 } 1395 1396 omega_delete_geq (pb, e, n_vars); 1397 e--; 1398 continue; 1399 } 1400 else if (top_var == 0) 1401 { 1402 int singlevar = packing[0]; 1403 1404 g = pb->geqs[e].coef[singlevar]; 1405 1406 if (g > 0) 1407 { 1408 pb->geqs[e].coef[singlevar] = 1; 1409 pb->geqs[e].key = singlevar; 1410 } 1411 else 1412 { 1413 g = -g; 1414 pb->geqs[e].coef[singlevar] = -1; 1415 pb->geqs[e].key = -singlevar; 1416 } 1417 1418 if (g > 1) 1419 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g); 1420 } 1421 else 1422 { 1423 int g2; 1424 int hash_key_multiplier = 31; 1425 1426 coupled_subscripts = 1; 1427 i0 = top_var; 1428 i = packing[i0--]; 1429 g = pb->geqs[e].coef[i]; 1430 hashCode = g * (i + 3); 1431 1432 if (g < 0) 1433 g = -g; 1434 1435 for (; i0 >= 0; i0--) 1436 { 1437 int x; 1438 1439 i = packing[i0]; 1440 x = pb->geqs[e].coef[i]; 1441 hashCode = hashCode * hash_key_multiplier * (i + 3) + x; 1442 1443 if (x < 0) 1444 x = -x; 1445 1446 if (x == 1) 1447 { 1448 g = 1; 1449 i0--; 1450 break; 1451 } 1452 else 1453 g = gcd (x, g); 1454 } 1455 1456 for (; i0 >= 0; i0--) 1457 { 1458 int x; 1459 i = packing[i0]; 1460 x = pb->geqs[e].coef[i]; 1461 hashCode = hashCode * hash_key_multiplier * (i + 3) + x; 1462 } 1463 1464 if (g > 1) 1465 { 1466 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g); 1467 i0 = top_var; 1468 i = packing[i0--]; 1469 pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g; 1470 hashCode = pb->geqs[e].coef[i] * (i + 3); 1471 1472 for (; i0 >= 0; i0--) 1473 { 1474 i = packing[i0]; 1475 pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g; 1476 hashCode = hashCode * hash_key_multiplier * (i + 3) 1477 + pb->geqs[e].coef[i]; 1478 } 1479 } 1480 1481 g2 = abs (hashCode); 1482 1483 if (dump_file && (dump_flags & TDF_DETAILS)) 1484 { 1485 fprintf (dump_file, "Hash code = %d, eqn = ", hashCode); 1486 omega_print_geq (dump_file, pb, &pb->geqs[e]); 1487 fprintf (dump_file, "\n"); 1488 } 1489 1490 j = g2 % HASH_TABLE_SIZE; 1491 1492 do { 1493 eqn proto = &(hash_master[j]); 1494 1495 if (proto->touched == g2) 1496 { 1497 if (proto->coef[0] == top_var) 1498 { 1499 if (hashCode >= 0) 1500 for (i0 = top_var; i0 >= 0; i0--) 1501 { 1502 i = packing[i0]; 1503 1504 if (pb->geqs[e].coef[i] != proto->coef[i]) 1505 break; 1506 } 1507 else 1508 for (i0 = top_var; i0 >= 0; i0--) 1509 { 1510 i = packing[i0]; 1511 1512 if (pb->geqs[e].coef[i] != -proto->coef[i]) 1513 break; 1514 } 1515 1516 if (i0 < 0) 1517 { 1518 if (hashCode >= 0) 1519 pb->geqs[e].key = proto->key; 1520 else 1521 pb->geqs[e].key = -proto->key; 1522 break; 1523 } 1524 } 1525 } 1526 else if (proto->touched < 0) 1527 { 1528 omega_init_eqn_zero (proto, pb->num_vars); 1529 if (hashCode >= 0) 1530 for (i0 = top_var; i0 >= 0; i0--) 1531 { 1532 i = packing[i0]; 1533 proto->coef[i] = pb->geqs[e].coef[i]; 1534 } 1535 else 1536 for (i0 = top_var; i0 >= 0; i0--) 1537 { 1538 i = packing[i0]; 1539 proto->coef[i] = -pb->geqs[e].coef[i]; 1540 } 1541 1542 proto->coef[0] = top_var; 1543 proto->touched = g2; 1544 1545 if (dump_file && (dump_flags & TDF_DETAILS)) 1546 fprintf (dump_file, " constraint key = %d\n", 1547 next_key); 1548 1549 proto->key = next_key++; 1550 1551 /* Too many hash keys generated. */ 1552 gcc_assert (proto->key <= MAX_KEYS); 1553 1554 if (hashCode >= 0) 1555 pb->geqs[e].key = proto->key; 1556 else 1557 pb->geqs[e].key = -proto->key; 1558 1559 break; 1560 } 1561 1562 j = (j + 1) % HASH_TABLE_SIZE; 1563 } while (1); 1564 } 1565 1566 pb->geqs[e].touched = 0; 1567 } 1568 1569 { 1570 int eKey = pb->geqs[e].key; 1571 int e2; 1572 if (e > 0) 1573 { 1574 int cTerm = pb->geqs[e].coef[0]; 1575 e2 = fast_lookup[MAX_KEYS - eKey]; 1576 1577 if (e2 < e && pb->geqs[e2].key == -eKey 1578 && pb->geqs[e2].color == omega_black) 1579 { 1580 if (pb->geqs[e2].coef[0] < -cTerm) 1581 { 1582 if (dump_file && (dump_flags & TDF_DETAILS)) 1583 { 1584 omega_print_geq (dump_file, pb, &pb->geqs[e]); 1585 fprintf (dump_file, "\n"); 1586 omega_print_geq (dump_file, pb, &pb->geqs[e2]); 1587 fprintf (dump_file, 1588 "\nequations have no solution \n"); 1589 } 1590 return normalize_false; 1591 } 1592 1593 if (pb->geqs[e2].coef[0] == -cTerm 1594 && (create_color 1595 || pb->geqs[e].color == omega_black)) 1596 { 1597 omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e], 1598 pb->num_vars); 1599 if (pb->geqs[e].color == omega_black) 1600 adding_equality_constraint (pb, pb->num_eqs); 1601 pb->num_eqs++; 1602 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 1603 } 1604 } 1605 1606 e2 = fast_lookup_red[MAX_KEYS - eKey]; 1607 1608 if (e2 < e && pb->geqs[e2].key == -eKey 1609 && pb->geqs[e2].color == omega_red) 1610 { 1611 if (pb->geqs[e2].coef[0] < -cTerm) 1612 { 1613 if (dump_file && (dump_flags & TDF_DETAILS)) 1614 { 1615 omega_print_geq (dump_file, pb, &pb->geqs[e]); 1616 fprintf (dump_file, "\n"); 1617 omega_print_geq (dump_file, pb, &pb->geqs[e2]); 1618 fprintf (dump_file, 1619 "\nequations have no solution \n"); 1620 } 1621 return normalize_false; 1622 } 1623 1624 if (pb->geqs[e2].coef[0] == -cTerm && create_color) 1625 { 1626 omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e], 1627 pb->num_vars); 1628 pb->eqs[pb->num_eqs].color = omega_red; 1629 pb->num_eqs++; 1630 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 1631 } 1632 } 1633 1634 e2 = fast_lookup[MAX_KEYS + eKey]; 1635 1636 if (e2 < e && pb->geqs[e2].key == eKey 1637 && pb->geqs[e2].color == omega_black) 1638 { 1639 if (pb->geqs[e2].coef[0] > cTerm) 1640 { 1641 if (pb->geqs[e].color == omega_black) 1642 { 1643 if (dump_file && (dump_flags & TDF_DETAILS)) 1644 { 1645 fprintf (dump_file, 1646 "Removing Redundant Equation: "); 1647 omega_print_geq (dump_file, pb, &(pb->geqs[e2])); 1648 fprintf (dump_file, "\n"); 1649 fprintf (dump_file, 1650 "[a] Made Redundant by: "); 1651 omega_print_geq (dump_file, pb, &(pb->geqs[e])); 1652 fprintf (dump_file, "\n"); 1653 } 1654 pb->geqs[e2].coef[0] = cTerm; 1655 omega_delete_geq (pb, e, n_vars); 1656 e--; 1657 continue; 1658 } 1659 } 1660 else 1661 { 1662 if (dump_file && (dump_flags & TDF_DETAILS)) 1663 { 1664 fprintf (dump_file, "Removing Redundant Equation: "); 1665 omega_print_geq (dump_file, pb, &(pb->geqs[e])); 1666 fprintf (dump_file, "\n"); 1667 fprintf (dump_file, "[b] Made Redundant by: "); 1668 omega_print_geq (dump_file, pb, &(pb->geqs[e2])); 1669 fprintf (dump_file, "\n"); 1670 } 1671 omega_delete_geq (pb, e, n_vars); 1672 e--; 1673 continue; 1674 } 1675 } 1676 1677 e2 = fast_lookup_red[MAX_KEYS + eKey]; 1678 1679 if (e2 < e && pb->geqs[e2].key == eKey 1680 && pb->geqs[e2].color == omega_red) 1681 { 1682 if (pb->geqs[e2].coef[0] >= cTerm) 1683 { 1684 if (dump_file && (dump_flags & TDF_DETAILS)) 1685 { 1686 fprintf (dump_file, "Removing Redundant Equation: "); 1687 omega_print_geq (dump_file, pb, &(pb->geqs[e2])); 1688 fprintf (dump_file, "\n"); 1689 fprintf (dump_file, "[c] Made Redundant by: "); 1690 omega_print_geq (dump_file, pb, &(pb->geqs[e])); 1691 fprintf (dump_file, "\n"); 1692 } 1693 pb->geqs[e2].coef[0] = cTerm; 1694 pb->geqs[e2].color = pb->geqs[e].color; 1695 } 1696 else if (pb->geqs[e].color == omega_red) 1697 { 1698 if (dump_file && (dump_flags & TDF_DETAILS)) 1699 { 1700 fprintf (dump_file, "Removing Redundant Equation: "); 1701 omega_print_geq (dump_file, pb, &(pb->geqs[e])); 1702 fprintf (dump_file, "\n"); 1703 fprintf (dump_file, "[d] Made Redundant by: "); 1704 omega_print_geq (dump_file, pb, &(pb->geqs[e2])); 1705 fprintf (dump_file, "\n"); 1706 } 1707 } 1708 omega_delete_geq (pb, e, n_vars); 1709 e--; 1710 continue; 1711 1712 } 1713 } 1714 1715 if (pb->geqs[e].color == omega_red) 1716 fast_lookup_red[MAX_KEYS + eKey] = e; 1717 else 1718 fast_lookup[MAX_KEYS + eKey] = e; 1719 } 1720 } 1721 1722 create_color = false; 1723 return coupled_subscripts ? normalize_coupled : normalize_uncoupled; 1724 } 1725 1726 /* Divide the coefficients of EQN by their gcd. N_VARS is the number 1727 of variables in EQN. */ 1728 1729 static inline void 1730 divide_eqn_by_gcd (eqn eqn, int n_vars) 1731 { 1732 int var, g = 0; 1733 1734 for (var = n_vars; var >= 0; var--) 1735 g = gcd (abs (eqn->coef[var]), g); 1736 1737 if (g) 1738 for (var = n_vars; var >= 0; var--) 1739 eqn->coef[var] = eqn->coef[var] / g; 1740 } 1741 1742 /* Rewrite some non-safe variables in function of protected 1743 wildcard variables. */ 1744 1745 static void 1746 cleanout_wildcards (omega_pb pb) 1747 { 1748 int e, i, j; 1749 int n_vars = pb->num_vars; 1750 bool renormalize = false; 1751 1752 for (e = pb->num_eqs - 1; e >= 0; e--) 1753 for (i = n_vars; !omega_safe_var_p (pb, i); i--) 1754 if (pb->eqs[e].coef[i] != 0) 1755 { 1756 /* i is the last nonzero non-safe variable. */ 1757 1758 for (j = i - 1; !omega_safe_var_p (pb, j); j--) 1759 if (pb->eqs[e].coef[j] != 0) 1760 break; 1761 1762 /* j is the next nonzero non-safe variable, or points 1763 to a safe variable: it is then a wildcard variable. */ 1764 1765 /* Clean it out. */ 1766 if (omega_safe_var_p (pb, j)) 1767 { 1768 eqn sub = &(pb->eqs[e]); 1769 int c = pb->eqs[e].coef[i]; 1770 int a = abs (c); 1771 int e2; 1772 1773 if (dump_file && (dump_flags & TDF_DETAILS)) 1774 { 1775 fprintf (dump_file, 1776 "Found a single wild card equality: "); 1777 omega_print_eq (dump_file, pb, &pb->eqs[e]); 1778 fprintf (dump_file, "\n"); 1779 omega_print_problem (dump_file, pb); 1780 } 1781 1782 for (e2 = pb->num_eqs - 1; e2 >= 0; e2--) 1783 if (e != e2 && pb->eqs[e2].coef[i] 1784 && (pb->eqs[e2].color == omega_red 1785 || (pb->eqs[e2].color == omega_black 1786 && pb->eqs[e].color == omega_black))) 1787 { 1788 eqn eqn = &(pb->eqs[e2]); 1789 int var, k; 1790 1791 for (var = n_vars; var >= 0; var--) 1792 eqn->coef[var] *= a; 1793 1794 k = eqn->coef[i]; 1795 1796 for (var = n_vars; var >= 0; var--) 1797 eqn->coef[var] -= sub->coef[var] * k / c; 1798 1799 eqn->coef[i] = 0; 1800 divide_eqn_by_gcd (eqn, n_vars); 1801 } 1802 1803 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--) 1804 if (pb->geqs[e2].coef[i] 1805 && (pb->geqs[e2].color == omega_red 1806 || (pb->eqs[e].color == omega_black 1807 && pb->geqs[e2].color == omega_black))) 1808 { 1809 eqn eqn = &(pb->geqs[e2]); 1810 int var, k; 1811 1812 for (var = n_vars; var >= 0; var--) 1813 eqn->coef[var] *= a; 1814 1815 k = eqn->coef[i]; 1816 1817 for (var = n_vars; var >= 0; var--) 1818 eqn->coef[var] -= sub->coef[var] * k / c; 1819 1820 eqn->coef[i] = 0; 1821 eqn->touched = 1; 1822 renormalize = true; 1823 } 1824 1825 for (e2 = pb->num_subs - 1; e2 >= 0; e2--) 1826 if (pb->subs[e2].coef[i] 1827 && (pb->subs[e2].color == omega_red 1828 || (pb->subs[e2].color == omega_black 1829 && pb->eqs[e].color == omega_black))) 1830 { 1831 eqn eqn = &(pb->subs[e2]); 1832 int var, k; 1833 1834 for (var = n_vars; var >= 0; var--) 1835 eqn->coef[var] *= a; 1836 1837 k = eqn->coef[i]; 1838 1839 for (var = n_vars; var >= 0; var--) 1840 eqn->coef[var] -= sub->coef[var] * k / c; 1841 1842 eqn->coef[i] = 0; 1843 divide_eqn_by_gcd (eqn, n_vars); 1844 } 1845 1846 if (dump_file && (dump_flags & TDF_DETAILS)) 1847 { 1848 fprintf (dump_file, "cleaned-out wildcard: "); 1849 omega_print_problem (dump_file, pb); 1850 } 1851 break; 1852 } 1853 } 1854 1855 if (renormalize) 1856 normalize_omega_problem (pb); 1857 } 1858 1859 /* Swap values contained in I and J. */ 1860 1861 static inline void 1862 swap (int *i, int *j) 1863 { 1864 int tmp; 1865 tmp = *i; 1866 *i = *j; 1867 *j = tmp; 1868 } 1869 1870 /* Swap values contained in I and J. */ 1871 1872 static inline void 1873 bswap (bool *i, bool *j) 1874 { 1875 bool tmp; 1876 tmp = *i; 1877 *i = *j; 1878 *j = tmp; 1879 } 1880 1881 /* Make variable IDX unprotected in PB, by swapping its index at the 1882 PB->safe_vars rank. */ 1883 1884 static inline void 1885 omega_unprotect_1 (omega_pb pb, int *idx, bool *unprotect) 1886 { 1887 /* If IDX is protected... */ 1888 if (*idx < pb->safe_vars) 1889 { 1890 /* ... swap its index with the last non protected index. */ 1891 int j = pb->safe_vars; 1892 int e; 1893 1894 for (e = pb->num_geqs - 1; e >= 0; e--) 1895 { 1896 pb->geqs[e].touched = 1; 1897 swap (&pb->geqs[e].coef[*idx], &pb->geqs[e].coef[j]); 1898 } 1899 1900 for (e = pb->num_eqs - 1; e >= 0; e--) 1901 swap (&pb->eqs[e].coef[*idx], &pb->eqs[e].coef[j]); 1902 1903 for (e = pb->num_subs - 1; e >= 0; e--) 1904 swap (&pb->subs[e].coef[*idx], &pb->subs[e].coef[j]); 1905 1906 if (unprotect) 1907 bswap (&unprotect[*idx], &unprotect[j]); 1908 1909 swap (&pb->var[*idx], &pb->var[j]); 1910 pb->forwarding_address[pb->var[*idx]] = *idx; 1911 pb->forwarding_address[pb->var[j]] = j; 1912 (*idx)--; 1913 } 1914 1915 /* The variable at pb->safe_vars is also unprotected now. */ 1916 pb->safe_vars--; 1917 } 1918 1919 /* During the Fourier-Motzkin elimination some variables are 1920 substituted with other variables. This function resurrects the 1921 substituted variables in PB. */ 1922 1923 static void 1924 resurrect_subs (omega_pb pb) 1925 { 1926 if (pb->num_subs > 0 1927 && please_no_equalities_in_simplified_problems == 0) 1928 { 1929 int i, e, m; 1930 1931 if (dump_file && (dump_flags & TDF_DETAILS)) 1932 { 1933 fprintf (dump_file, 1934 "problem reduced, bringing variables back to life\n"); 1935 omega_print_problem (dump_file, pb); 1936 } 1937 1938 for (i = 1; omega_safe_var_p (pb, i); i++) 1939 if (omega_wildcard_p (pb, i)) 1940 omega_unprotect_1 (pb, &i, NULL); 1941 1942 m = pb->num_subs; 1943 1944 for (e = pb->num_geqs - 1; e >= 0; e--) 1945 if (single_var_geq (&pb->geqs[e], pb->num_vars)) 1946 { 1947 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key))) 1948 pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m); 1949 } 1950 else 1951 { 1952 pb->geqs[e].touched = 1; 1953 pb->geqs[e].key = 0; 1954 } 1955 1956 for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--) 1957 { 1958 pb->var[i + m] = pb->var[i]; 1959 1960 for (e = pb->num_geqs - 1; e >= 0; e--) 1961 pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i]; 1962 1963 for (e = pb->num_eqs - 1; e >= 0; e--) 1964 pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i]; 1965 1966 for (e = pb->num_subs - 1; e >= 0; e--) 1967 pb->subs[e].coef[i + m] = pb->subs[e].coef[i]; 1968 } 1969 1970 for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--) 1971 { 1972 for (e = pb->num_geqs - 1; e >= 0; e--) 1973 pb->geqs[e].coef[i] = 0; 1974 1975 for (e = pb->num_eqs - 1; e >= 0; e--) 1976 pb->eqs[e].coef[i] = 0; 1977 1978 for (e = pb->num_subs - 1; e >= 0; e--) 1979 pb->subs[e].coef[i] = 0; 1980 } 1981 1982 pb->num_vars += m; 1983 1984 for (e = pb->num_subs - 1; e >= 0; e--) 1985 { 1986 pb->var[pb->safe_vars + 1 + e] = pb->subs[e].key; 1987 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e]), 1988 pb->num_vars); 1989 pb->eqs[pb->num_eqs].coef[pb->safe_vars + 1 + e] = -1; 1990 pb->eqs[pb->num_eqs].color = omega_black; 1991 1992 if (dump_file && (dump_flags & TDF_DETAILS)) 1993 { 1994 fprintf (dump_file, "brought back: "); 1995 omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]); 1996 fprintf (dump_file, "\n"); 1997 } 1998 1999 pb->num_eqs++; 2000 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 2001 } 2002 2003 pb->safe_vars += m; 2004 pb->num_subs = 0; 2005 2006 if (dump_file && (dump_flags & TDF_DETAILS)) 2007 { 2008 fprintf (dump_file, "variables brought back to life\n"); 2009 omega_print_problem (dump_file, pb); 2010 } 2011 2012 cleanout_wildcards (pb); 2013 } 2014 } 2015 2016 static inline bool 2017 implies (unsigned int a, unsigned int b) 2018 { 2019 return (a == (a & b)); 2020 } 2021 2022 /* Eliminate redundant equations in PB. When EXPENSIVE is true, an 2023 extra step is performed. Returns omega_false when there exist no 2024 solution, omega_true otherwise. */ 2025 2026 enum omega_result 2027 omega_eliminate_redundant (omega_pb pb, bool expensive) 2028 { 2029 int c, e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3; 2030 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS); 2031 omega_pb tmp_problem; 2032 2033 /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations. */ 2034 unsigned int *peqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS); 2035 unsigned int *zeqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS); 2036 unsigned int *neqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS); 2037 2038 /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */ 2039 unsigned int pp, pz, pn; 2040 2041 if (dump_file && (dump_flags & TDF_DETAILS)) 2042 { 2043 fprintf (dump_file, "in eliminate Redundant:\n"); 2044 omega_print_problem (dump_file, pb); 2045 } 2046 2047 for (e = pb->num_geqs - 1; e >= 0; e--) 2048 { 2049 int tmp = 1; 2050 2051 is_dead[e] = false; 2052 peqs[e] = zeqs[e] = neqs[e] = 0; 2053 2054 for (i = pb->num_vars; i >= 1; i--) 2055 { 2056 if (pb->geqs[e].coef[i] > 0) 2057 peqs[e] |= tmp; 2058 else if (pb->geqs[e].coef[i] < 0) 2059 neqs[e] |= tmp; 2060 else 2061 zeqs[e] |= tmp; 2062 2063 tmp <<= 1; 2064 } 2065 } 2066 2067 2068 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--) 2069 if (!is_dead[e1]) 2070 for (e2 = e1 - 1; e2 >= 0; e2--) 2071 if (!is_dead[e2]) 2072 { 2073 for (p = pb->num_vars; p > 1; p--) 2074 for (q = p - 1; q > 0; q--) 2075 if ((alpha = pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] 2076 - pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]) != 0) 2077 goto foundPQ; 2078 2079 continue; 2080 2081 foundPQ: 2082 pz = ((zeqs[e1] & zeqs[e2]) | (peqs[e1] & neqs[e2]) 2083 | (neqs[e1] & peqs[e2])); 2084 pp = peqs[e1] | peqs[e2]; 2085 pn = neqs[e1] | neqs[e2]; 2086 2087 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--) 2088 if (e3 != e1 && e3 != e2) 2089 { 2090 if (!implies (zeqs[e3], pz)) 2091 goto nextE3; 2092 2093 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p] 2094 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]); 2095 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p] 2096 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]); 2097 alpha3 = alpha; 2098 2099 if (alpha1 * alpha2 <= 0) 2100 goto nextE3; 2101 2102 if (alpha1 < 0) 2103 { 2104 alpha1 = -alpha1; 2105 alpha2 = -alpha2; 2106 alpha3 = -alpha3; 2107 } 2108 2109 if (alpha3 > 0) 2110 { 2111 /* Trying to prove e3 is redundant. */ 2112 if (!implies (peqs[e3], pp) 2113 || !implies (neqs[e3], pn)) 2114 goto nextE3; 2115 2116 if (pb->geqs[e3].color == omega_black 2117 && (pb->geqs[e1].color == omega_red 2118 || pb->geqs[e2].color == omega_red)) 2119 goto nextE3; 2120 2121 for (k = pb->num_vars; k >= 1; k--) 2122 if (alpha3 * pb->geqs[e3].coef[k] 2123 != (alpha1 * pb->geqs[e1].coef[k] 2124 + alpha2 * pb->geqs[e2].coef[k])) 2125 goto nextE3; 2126 2127 c = (alpha1 * pb->geqs[e1].coef[0] 2128 + alpha2 * pb->geqs[e2].coef[0]); 2129 2130 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1)) 2131 { 2132 if (dump_file && (dump_flags & TDF_DETAILS)) 2133 { 2134 fprintf (dump_file, 2135 "found redundant inequality\n"); 2136 fprintf (dump_file, 2137 "alpha1, alpha2, alpha3 = %d,%d,%d\n", 2138 alpha1, alpha2, alpha3); 2139 2140 omega_print_geq (dump_file, pb, &(pb->geqs[e1])); 2141 fprintf (dump_file, "\n"); 2142 omega_print_geq (dump_file, pb, &(pb->geqs[e2])); 2143 fprintf (dump_file, "\n=> "); 2144 omega_print_geq (dump_file, pb, &(pb->geqs[e3])); 2145 fprintf (dump_file, "\n\n"); 2146 } 2147 2148 is_dead[e3] = true; 2149 } 2150 } 2151 else 2152 { 2153 /* Trying to prove e3 <= 0 and therefore e3 = 0, 2154 or trying to prove e3 < 0, and therefore the 2155 problem has no solutions. */ 2156 if (!implies (peqs[e3], pn) 2157 || !implies (neqs[e3], pp)) 2158 goto nextE3; 2159 2160 if (pb->geqs[e1].color == omega_red 2161 || pb->geqs[e2].color == omega_red 2162 || pb->geqs[e3].color == omega_red) 2163 goto nextE3; 2164 2165 /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */ 2166 for (k = pb->num_vars; k >= 1; k--) 2167 if (alpha3 * pb->geqs[e3].coef[k] 2168 != (alpha1 * pb->geqs[e1].coef[k] 2169 + alpha2 * pb->geqs[e2].coef[k])) 2170 goto nextE3; 2171 2172 c = (alpha1 * pb->geqs[e1].coef[0] 2173 + alpha2 * pb->geqs[e2].coef[0]); 2174 2175 if (c < alpha3 * (pb->geqs[e3].coef[0])) 2176 { 2177 /* We just proved e3 < 0, so no solutions exist. */ 2178 if (dump_file && (dump_flags & TDF_DETAILS)) 2179 { 2180 fprintf (dump_file, 2181 "found implied over tight inequality\n"); 2182 fprintf (dump_file, 2183 "alpha1, alpha2, alpha3 = %d,%d,%d\n", 2184 alpha1, alpha2, -alpha3); 2185 omega_print_geq (dump_file, pb, &(pb->geqs[e1])); 2186 fprintf (dump_file, "\n"); 2187 omega_print_geq (dump_file, pb, &(pb->geqs[e2])); 2188 fprintf (dump_file, "\n=> not "); 2189 omega_print_geq (dump_file, pb, &(pb->geqs[e3])); 2190 fprintf (dump_file, "\n\n"); 2191 } 2192 free (is_dead); 2193 free (peqs); 2194 free (zeqs); 2195 free (neqs); 2196 return omega_false; 2197 } 2198 else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1)) 2199 { 2200 /* We just proved that e3 <=0, so e3 = 0. */ 2201 if (dump_file && (dump_flags & TDF_DETAILS)) 2202 { 2203 fprintf (dump_file, 2204 "found implied tight inequality\n"); 2205 fprintf (dump_file, 2206 "alpha1, alpha2, alpha3 = %d,%d,%d\n", 2207 alpha1, alpha2, -alpha3); 2208 omega_print_geq (dump_file, pb, &(pb->geqs[e1])); 2209 fprintf (dump_file, "\n"); 2210 omega_print_geq (dump_file, pb, &(pb->geqs[e2])); 2211 fprintf (dump_file, "\n=> inverse "); 2212 omega_print_geq (dump_file, pb, &(pb->geqs[e3])); 2213 fprintf (dump_file, "\n\n"); 2214 } 2215 2216 omega_copy_eqn (&pb->eqs[pb->num_eqs++], 2217 &pb->geqs[e3], pb->num_vars); 2218 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 2219 adding_equality_constraint (pb, pb->num_eqs - 1); 2220 is_dead[e3] = true; 2221 } 2222 } 2223 nextE3:; 2224 } 2225 } 2226 2227 /* Delete the inequalities that were marked as dead. */ 2228 for (e = pb->num_geqs - 1; e >= 0; e--) 2229 if (is_dead[e]) 2230 omega_delete_geq (pb, e, pb->num_vars); 2231 2232 if (!expensive) 2233 goto eliminate_redundant_done; 2234 2235 tmp_problem = XNEW (struct omega_pb_d); 2236 conservative++; 2237 2238 for (e = pb->num_geqs - 1; e >= 0; e--) 2239 { 2240 if (dump_file && (dump_flags & TDF_DETAILS)) 2241 { 2242 fprintf (dump_file, 2243 "checking equation %d to see if it is redundant: ", e); 2244 omega_print_geq (dump_file, pb, &(pb->geqs[e])); 2245 fprintf (dump_file, "\n"); 2246 } 2247 2248 omega_copy_problem (tmp_problem, pb); 2249 omega_negate_geq (tmp_problem, e); 2250 tmp_problem->safe_vars = 0; 2251 tmp_problem->variables_freed = false; 2252 2253 if (omega_solve_problem (tmp_problem, omega_false) == omega_false) 2254 omega_delete_geq (pb, e, pb->num_vars); 2255 } 2256 2257 free (tmp_problem); 2258 conservative--; 2259 2260 if (!omega_reduce_with_subs) 2261 { 2262 resurrect_subs (pb); 2263 gcc_assert (please_no_equalities_in_simplified_problems 2264 || pb->num_subs == 0); 2265 } 2266 2267 eliminate_redundant_done: 2268 free (is_dead); 2269 free (peqs); 2270 free (zeqs); 2271 free (neqs); 2272 return omega_true; 2273 } 2274 2275 /* For each inequality that has coefficients bigger than 20, try to 2276 create a new constraint that cannot be derived from the original 2277 constraint and that has smaller coefficients. Add the new 2278 constraint at the end of geqs. Return the number of inequalities 2279 that have been added to PB. */ 2280 2281 static int 2282 smooth_weird_equations (omega_pb pb) 2283 { 2284 int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3; 2285 int c; 2286 int v; 2287 int result = 0; 2288 2289 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--) 2290 if (pb->geqs[e1].color == omega_black) 2291 { 2292 int g = 999999; 2293 2294 for (v = pb->num_vars; v >= 1; v--) 2295 if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g) 2296 g = abs (pb->geqs[e1].coef[v]); 2297 2298 /* Magic number. */ 2299 if (g > 20) 2300 { 2301 e3 = pb->num_geqs; 2302 2303 for (v = pb->num_vars; v >= 1; v--) 2304 pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2, 2305 g); 2306 2307 pb->geqs[e3].color = omega_black; 2308 pb->geqs[e3].touched = 1; 2309 /* Magic number. */ 2310 pb->geqs[e3].coef[0] = 9997; 2311 2312 if (dump_file && (dump_flags & TDF_DETAILS)) 2313 { 2314 fprintf (dump_file, "Checking to see if we can derive: "); 2315 omega_print_geq (dump_file, pb, &pb->geqs[e3]); 2316 fprintf (dump_file, "\n from: "); 2317 omega_print_geq (dump_file, pb, &pb->geqs[e1]); 2318 fprintf (dump_file, "\n"); 2319 } 2320 2321 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--) 2322 if (e1 != e2 && pb->geqs[e2].color == omega_black) 2323 { 2324 for (p = pb->num_vars; p > 1; p--) 2325 { 2326 for (q = p - 1; q > 0; q--) 2327 { 2328 alpha = 2329 (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] - 2330 pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]); 2331 if (alpha != 0) 2332 goto foundPQ; 2333 } 2334 } 2335 continue; 2336 2337 foundPQ: 2338 2339 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p] 2340 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]); 2341 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p] 2342 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]); 2343 alpha3 = alpha; 2344 2345 if (alpha1 * alpha2 <= 0) 2346 continue; 2347 2348 if (alpha1 < 0) 2349 { 2350 alpha1 = -alpha1; 2351 alpha2 = -alpha2; 2352 alpha3 = -alpha3; 2353 } 2354 2355 if (alpha3 > 0) 2356 { 2357 /* Try to prove e3 is redundant: verify 2358 alpha1*v1 + alpha2*v2 = alpha3*v3. */ 2359 for (k = pb->num_vars; k >= 1; k--) 2360 if (alpha3 * pb->geqs[e3].coef[k] 2361 != (alpha1 * pb->geqs[e1].coef[k] 2362 + alpha2 * pb->geqs[e2].coef[k])) 2363 goto nextE2; 2364 2365 c = alpha1 * pb->geqs[e1].coef[0] 2366 + alpha2 * pb->geqs[e2].coef[0]; 2367 2368 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1)) 2369 pb->geqs[e3].coef[0] = int_div (c, alpha3); 2370 } 2371 nextE2:; 2372 } 2373 2374 if (pb->geqs[e3].coef[0] < 9997) 2375 { 2376 result++; 2377 pb->num_geqs++; 2378 2379 if (dump_file && (dump_flags & TDF_DETAILS)) 2380 { 2381 fprintf (dump_file, 2382 "Smoothing weird equations; adding:\n"); 2383 omega_print_geq (dump_file, pb, &pb->geqs[e3]); 2384 fprintf (dump_file, "\nto:\n"); 2385 omega_print_problem (dump_file, pb); 2386 fprintf (dump_file, "\n\n"); 2387 } 2388 } 2389 } 2390 } 2391 return result; 2392 } 2393 2394 /* Replace tuples of inequalities, that define upper and lower half 2395 spaces, with an equation. */ 2396 2397 static void 2398 coalesce (omega_pb pb) 2399 { 2400 int e, e2; 2401 int colors = 0; 2402 bool *is_dead; 2403 int found_something = 0; 2404 2405 for (e = 0; e < pb->num_geqs; e++) 2406 if (pb->geqs[e].color == omega_red) 2407 colors++; 2408 2409 if (colors < 2) 2410 return; 2411 2412 is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS); 2413 2414 for (e = 0; e < pb->num_geqs; e++) 2415 is_dead[e] = false; 2416 2417 for (e = 0; e < pb->num_geqs; e++) 2418 if (pb->geqs[e].color == omega_red 2419 && !pb->geqs[e].touched) 2420 for (e2 = e + 1; e2 < pb->num_geqs; e2++) 2421 if (!pb->geqs[e2].touched 2422 && pb->geqs[e].key == -pb->geqs[e2].key 2423 && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0] 2424 && pb->geqs[e2].color == omega_red) 2425 { 2426 omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e], 2427 pb->num_vars); 2428 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 2429 found_something++; 2430 is_dead[e] = true; 2431 is_dead[e2] = true; 2432 } 2433 2434 for (e = pb->num_geqs - 1; e >= 0; e--) 2435 if (is_dead[e]) 2436 omega_delete_geq (pb, e, pb->num_vars); 2437 2438 if (dump_file && (dump_flags & TDF_DETAILS) && found_something) 2439 { 2440 fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n", 2441 found_something); 2442 omega_print_problem (dump_file, pb); 2443 } 2444 2445 free (is_dead); 2446 } 2447 2448 /* Eliminate red inequalities from PB. When ELIMINATE_ALL is 2449 true, continue to eliminate all the red inequalities. */ 2450 2451 void 2452 omega_eliminate_red (omega_pb pb, bool eliminate_all) 2453 { 2454 int e, e2, e3, i, j, k, a, alpha1, alpha2; 2455 int c = 0; 2456 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS); 2457 int dead_count = 0; 2458 int red_found; 2459 omega_pb tmp_problem; 2460 2461 if (dump_file && (dump_flags & TDF_DETAILS)) 2462 { 2463 fprintf (dump_file, "in eliminate RED:\n"); 2464 omega_print_problem (dump_file, pb); 2465 } 2466 2467 if (pb->num_eqs > 0) 2468 omega_simplify_problem (pb); 2469 2470 for (e = pb->num_geqs - 1; e >= 0; e--) 2471 is_dead[e] = false; 2472 2473 for (e = pb->num_geqs - 1; e >= 0; e--) 2474 if (pb->geqs[e].color == omega_black && !is_dead[e]) 2475 for (e2 = e - 1; e2 >= 0; e2--) 2476 if (pb->geqs[e2].color == omega_black 2477 && !is_dead[e2]) 2478 { 2479 a = 0; 2480 2481 for (i = pb->num_vars; i > 1; i--) 2482 for (j = i - 1; j > 0; j--) 2483 if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j] 2484 - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0) 2485 goto found_pair; 2486 2487 continue; 2488 2489 found_pair: 2490 if (dump_file && (dump_flags & TDF_DETAILS)) 2491 { 2492 fprintf (dump_file, 2493 "found two equations to combine, i = %s, ", 2494 omega_variable_to_str (pb, i)); 2495 fprintf (dump_file, "j = %s, alpha = %d\n", 2496 omega_variable_to_str (pb, j), a); 2497 omega_print_geq (dump_file, pb, &(pb->geqs[e])); 2498 fprintf (dump_file, "\n"); 2499 omega_print_geq (dump_file, pb, &(pb->geqs[e2])); 2500 fprintf (dump_file, "\n"); 2501 } 2502 2503 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--) 2504 if (pb->geqs[e3].color == omega_red) 2505 { 2506 alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i] 2507 - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]); 2508 alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i] 2509 - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]); 2510 2511 if ((a > 0 && alpha1 > 0 && alpha2 > 0) 2512 || (a < 0 && alpha1 < 0 && alpha2 < 0)) 2513 { 2514 if (dump_file && (dump_flags & TDF_DETAILS)) 2515 { 2516 fprintf (dump_file, 2517 "alpha1 = %d, alpha2 = %d;" 2518 "comparing against: ", 2519 alpha1, alpha2); 2520 omega_print_geq (dump_file, pb, &(pb->geqs[e3])); 2521 fprintf (dump_file, "\n"); 2522 } 2523 2524 for (k = pb->num_vars; k >= 0; k--) 2525 { 2526 c = (alpha1 * pb->geqs[e].coef[k] 2527 + alpha2 * pb->geqs[e2].coef[k]); 2528 2529 if (c != a * pb->geqs[e3].coef[k]) 2530 break; 2531 2532 if (dump_file && (dump_flags & TDF_DETAILS) && k > 0) 2533 fprintf (dump_file, " %s: %d, %d\n", 2534 omega_variable_to_str (pb, k), c, 2535 a * pb->geqs[e3].coef[k]); 2536 } 2537 2538 if (k < 0 2539 || (k == 0 && 2540 ((a > 0 && c < a * pb->geqs[e3].coef[k]) 2541 || (a < 0 && c > a * pb->geqs[e3].coef[k])))) 2542 { 2543 if (dump_file && (dump_flags & TDF_DETAILS)) 2544 { 2545 dead_count++; 2546 fprintf (dump_file, 2547 "red equation#%d is dead " 2548 "(%d dead so far, %d remain)\n", 2549 e3, dead_count, 2550 pb->num_geqs - dead_count); 2551 omega_print_geq (dump_file, pb, &(pb->geqs[e])); 2552 fprintf (dump_file, "\n"); 2553 omega_print_geq (dump_file, pb, &(pb->geqs[e2])); 2554 fprintf (dump_file, "\n"); 2555 omega_print_geq (dump_file, pb, &(pb->geqs[e3])); 2556 fprintf (dump_file, "\n"); 2557 } 2558 is_dead[e3] = true; 2559 } 2560 } 2561 } 2562 } 2563 2564 for (e = pb->num_geqs - 1; e >= 0; e--) 2565 if (is_dead[e]) 2566 omega_delete_geq (pb, e, pb->num_vars); 2567 2568 free (is_dead); 2569 2570 if (dump_file && (dump_flags & TDF_DETAILS)) 2571 { 2572 fprintf (dump_file, "in eliminate RED, easy tests done:\n"); 2573 omega_print_problem (dump_file, pb); 2574 } 2575 2576 for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--) 2577 if (pb->geqs[e].color == omega_red) 2578 red_found = 1; 2579 2580 if (!red_found) 2581 { 2582 if (dump_file && (dump_flags & TDF_DETAILS)) 2583 fprintf (dump_file, "fast checks worked\n"); 2584 2585 if (!omega_reduce_with_subs) 2586 gcc_assert (please_no_equalities_in_simplified_problems 2587 || pb->num_subs == 0); 2588 2589 return; 2590 } 2591 2592 if (!omega_verify_simplification 2593 && verify_omega_pb (pb) == omega_false) 2594 return; 2595 2596 conservative++; 2597 tmp_problem = XNEW (struct omega_pb_d); 2598 2599 for (e = pb->num_geqs - 1; e >= 0; e--) 2600 if (pb->geqs[e].color == omega_red) 2601 { 2602 if (dump_file && (dump_flags & TDF_DETAILS)) 2603 { 2604 fprintf (dump_file, 2605 "checking equation %d to see if it is redundant: ", e); 2606 omega_print_geq (dump_file, pb, &(pb->geqs[e])); 2607 fprintf (dump_file, "\n"); 2608 } 2609 2610 omega_copy_problem (tmp_problem, pb); 2611 omega_negate_geq (tmp_problem, e); 2612 tmp_problem->safe_vars = 0; 2613 tmp_problem->variables_freed = false; 2614 tmp_problem->num_subs = 0; 2615 2616 if (omega_solve_problem (tmp_problem, omega_false) == omega_false) 2617 { 2618 if (dump_file && (dump_flags & TDF_DETAILS)) 2619 fprintf (dump_file, "it is redundant\n"); 2620 omega_delete_geq (pb, e, pb->num_vars); 2621 } 2622 else 2623 { 2624 if (dump_file && (dump_flags & TDF_DETAILS)) 2625 fprintf (dump_file, "it is not redundant\n"); 2626 2627 if (!eliminate_all) 2628 { 2629 if (dump_file && (dump_flags & TDF_DETAILS)) 2630 fprintf (dump_file, "no need to check other red equations\n"); 2631 break; 2632 } 2633 } 2634 } 2635 2636 conservative--; 2637 free (tmp_problem); 2638 /* omega_simplify_problem (pb); */ 2639 2640 if (!omega_reduce_with_subs) 2641 gcc_assert (please_no_equalities_in_simplified_problems 2642 || pb->num_subs == 0); 2643 } 2644 2645 /* Transform some wildcard variables to non-safe variables. */ 2646 2647 static void 2648 chain_unprotect (omega_pb pb) 2649 { 2650 int i, e; 2651 bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS); 2652 2653 for (i = 1; omega_safe_var_p (pb, i); i++) 2654 { 2655 unprotect[i] = omega_wildcard_p (pb, i); 2656 2657 for (e = pb->num_subs - 1; e >= 0; e--) 2658 if (pb->subs[e].coef[i]) 2659 unprotect[i] = false; 2660 } 2661 2662 if (dump_file && (dump_flags & TDF_DETAILS)) 2663 { 2664 fprintf (dump_file, "Doing chain reaction unprotection\n"); 2665 omega_print_problem (dump_file, pb); 2666 2667 for (i = 1; omega_safe_var_p (pb, i); i++) 2668 if (unprotect[i]) 2669 fprintf (dump_file, "unprotecting %s\n", 2670 omega_variable_to_str (pb, i)); 2671 } 2672 2673 for (i = 1; omega_safe_var_p (pb, i); i++) 2674 if (unprotect[i]) 2675 omega_unprotect_1 (pb, &i, unprotect); 2676 2677 if (dump_file && (dump_flags & TDF_DETAILS)) 2678 { 2679 fprintf (dump_file, "After chain reactions\n"); 2680 omega_print_problem (dump_file, pb); 2681 } 2682 2683 free (unprotect); 2684 } 2685 2686 /* Reduce problem PB. */ 2687 2688 static void 2689 omega_problem_reduced (omega_pb pb) 2690 { 2691 if (omega_verify_simplification 2692 && !in_approximate_mode 2693 && verify_omega_pb (pb) == omega_false) 2694 return; 2695 2696 if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS) 2697 && !omega_eliminate_redundant (pb, true)) 2698 return; 2699 2700 omega_found_reduction = omega_true; 2701 2702 if (!please_no_equalities_in_simplified_problems) 2703 coalesce (pb); 2704 2705 if (omega_reduce_with_subs 2706 || please_no_equalities_in_simplified_problems) 2707 chain_unprotect (pb); 2708 else 2709 resurrect_subs (pb); 2710 2711 if (!return_single_result) 2712 { 2713 int i; 2714 2715 for (i = 1; omega_safe_var_p (pb, i); i++) 2716 pb->forwarding_address[pb->var[i]] = i; 2717 2718 for (i = 0; i < pb->num_subs; i++) 2719 pb->forwarding_address[pb->subs[i].key] = -i - 1; 2720 2721 (*omega_when_reduced) (pb); 2722 } 2723 2724 if (dump_file && (dump_flags & TDF_DETAILS)) 2725 { 2726 fprintf (dump_file, "-------------------------------------------\n"); 2727 fprintf (dump_file, "problem reduced:\n"); 2728 omega_print_problem (dump_file, pb); 2729 fprintf (dump_file, "-------------------------------------------\n"); 2730 } 2731 } 2732 2733 /* Eliminates all the free variables for problem PB, that is all the 2734 variables from FV to PB->NUM_VARS. */ 2735 2736 static void 2737 omega_free_eliminations (omega_pb pb, int fv) 2738 { 2739 bool try_again = true; 2740 int i, e, e2; 2741 int n_vars = pb->num_vars; 2742 2743 while (try_again) 2744 { 2745 try_again = false; 2746 2747 for (i = n_vars; i > fv; i--) 2748 { 2749 for (e = pb->num_geqs - 1; e >= 0; e--) 2750 if (pb->geqs[e].coef[i]) 2751 break; 2752 2753 if (e < 0) 2754 e2 = e; 2755 else if (pb->geqs[e].coef[i] > 0) 2756 { 2757 for (e2 = e - 1; e2 >= 0; e2--) 2758 if (pb->geqs[e2].coef[i] < 0) 2759 break; 2760 } 2761 else 2762 { 2763 for (e2 = e - 1; e2 >= 0; e2--) 2764 if (pb->geqs[e2].coef[i] > 0) 2765 break; 2766 } 2767 2768 if (e2 < 0) 2769 { 2770 int e3; 2771 for (e3 = pb->num_subs - 1; e3 >= 0; e3--) 2772 if (pb->subs[e3].coef[i]) 2773 break; 2774 2775 if (e3 >= 0) 2776 continue; 2777 2778 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--) 2779 if (pb->eqs[e3].coef[i]) 2780 break; 2781 2782 if (e3 >= 0) 2783 continue; 2784 2785 if (dump_file && (dump_flags & TDF_DETAILS)) 2786 fprintf (dump_file, "a free elimination of %s\n", 2787 omega_variable_to_str (pb, i)); 2788 2789 if (e >= 0) 2790 { 2791 omega_delete_geq (pb, e, n_vars); 2792 2793 for (e--; e >= 0; e--) 2794 if (pb->geqs[e].coef[i]) 2795 omega_delete_geq (pb, e, n_vars); 2796 2797 try_again = (i < n_vars); 2798 } 2799 2800 omega_delete_variable (pb, i); 2801 n_vars = pb->num_vars; 2802 } 2803 } 2804 } 2805 2806 if (dump_file && (dump_flags & TDF_DETAILS)) 2807 { 2808 fprintf (dump_file, "\nafter free eliminations:\n"); 2809 omega_print_problem (dump_file, pb); 2810 fprintf (dump_file, "\n"); 2811 } 2812 } 2813 2814 /* Do free red eliminations. */ 2815 2816 static void 2817 free_red_eliminations (omega_pb pb) 2818 { 2819 bool try_again = true; 2820 int i, e, e2; 2821 int n_vars = pb->num_vars; 2822 bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS); 2823 bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS); 2824 bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS); 2825 2826 for (i = n_vars; i > 0; i--) 2827 { 2828 is_red_var[i] = false; 2829 is_dead_var[i] = false; 2830 } 2831 2832 for (e = pb->num_geqs - 1; e >= 0; e--) 2833 { 2834 is_dead_geq[e] = false; 2835 2836 if (pb->geqs[e].color == omega_red) 2837 for (i = n_vars; i > 0; i--) 2838 if (pb->geqs[e].coef[i] != 0) 2839 is_red_var[i] = true; 2840 } 2841 2842 while (try_again) 2843 { 2844 try_again = false; 2845 for (i = n_vars; i > 0; i--) 2846 if (!is_red_var[i] && !is_dead_var[i]) 2847 { 2848 for (e = pb->num_geqs - 1; e >= 0; e--) 2849 if (!is_dead_geq[e] && pb->geqs[e].coef[i]) 2850 break; 2851 2852 if (e < 0) 2853 e2 = e; 2854 else if (pb->geqs[e].coef[i] > 0) 2855 { 2856 for (e2 = e - 1; e2 >= 0; e2--) 2857 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0) 2858 break; 2859 } 2860 else 2861 { 2862 for (e2 = e - 1; e2 >= 0; e2--) 2863 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0) 2864 break; 2865 } 2866 2867 if (e2 < 0) 2868 { 2869 int e3; 2870 for (e3 = pb->num_subs - 1; e3 >= 0; e3--) 2871 if (pb->subs[e3].coef[i]) 2872 break; 2873 2874 if (e3 >= 0) 2875 continue; 2876 2877 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--) 2878 if (pb->eqs[e3].coef[i]) 2879 break; 2880 2881 if (e3 >= 0) 2882 continue; 2883 2884 if (dump_file && (dump_flags & TDF_DETAILS)) 2885 fprintf (dump_file, "a free red elimination of %s\n", 2886 omega_variable_to_str (pb, i)); 2887 2888 for (; e >= 0; e--) 2889 if (pb->geqs[e].coef[i]) 2890 is_dead_geq[e] = true; 2891 2892 try_again = true; 2893 is_dead_var[i] = true; 2894 } 2895 } 2896 } 2897 2898 for (e = pb->num_geqs - 1; e >= 0; e--) 2899 if (is_dead_geq[e]) 2900 omega_delete_geq (pb, e, n_vars); 2901 2902 for (i = n_vars; i > 0; i--) 2903 if (is_dead_var[i]) 2904 omega_delete_variable (pb, i); 2905 2906 if (dump_file && (dump_flags & TDF_DETAILS)) 2907 { 2908 fprintf (dump_file, "\nafter free red eliminations:\n"); 2909 omega_print_problem (dump_file, pb); 2910 fprintf (dump_file, "\n"); 2911 } 2912 2913 free (is_red_var); 2914 free (is_dead_var); 2915 free (is_dead_geq); 2916 } 2917 2918 /* For equation EQ of the form "0 = EQN", insert in PB two 2919 inequalities "0 <= EQN" and "0 <= -EQN". */ 2920 2921 void 2922 omega_convert_eq_to_geqs (omega_pb pb, int eq) 2923 { 2924 int i; 2925 2926 if (dump_file && (dump_flags & TDF_DETAILS)) 2927 fprintf (dump_file, "Converting Eq to Geqs\n"); 2928 2929 /* Insert "0 <= EQN". */ 2930 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars); 2931 pb->geqs[pb->num_geqs].touched = 1; 2932 pb->num_geqs++; 2933 2934 /* Insert "0 <= -EQN". */ 2935 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars); 2936 pb->geqs[pb->num_geqs].touched = 1; 2937 2938 for (i = 0; i <= pb->num_vars; i++) 2939 pb->geqs[pb->num_geqs].coef[i] *= -1; 2940 2941 pb->num_geqs++; 2942 2943 if (dump_file && (dump_flags & TDF_DETAILS)) 2944 omega_print_problem (dump_file, pb); 2945 } 2946 2947 /* Eliminates variable I from PB. */ 2948 2949 static void 2950 omega_do_elimination (omega_pb pb, int e, int i) 2951 { 2952 eqn sub = omega_alloc_eqns (0, 1); 2953 int c; 2954 int n_vars = pb->num_vars; 2955 2956 if (dump_file && (dump_flags & TDF_DETAILS)) 2957 fprintf (dump_file, "eliminating variable %s\n", 2958 omega_variable_to_str (pb, i)); 2959 2960 omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars); 2961 c = sub->coef[i]; 2962 sub->coef[i] = 0; 2963 if (c == 1 || c == -1) 2964 { 2965 if (pb->eqs[e].color == omega_red) 2966 { 2967 bool fB; 2968 omega_substitute_red (pb, sub, i, c, &fB); 2969 if (fB) 2970 omega_convert_eq_to_geqs (pb, e); 2971 else 2972 omega_delete_variable (pb, i); 2973 } 2974 else 2975 { 2976 omega_substitute (pb, sub, i, c); 2977 omega_delete_variable (pb, i); 2978 } 2979 } 2980 else 2981 { 2982 int a = abs (c); 2983 int e2 = e; 2984 2985 if (dump_file && (dump_flags & TDF_DETAILS)) 2986 fprintf (dump_file, "performing non-exact elimination, c = %d\n", c); 2987 2988 for (e = pb->num_eqs - 1; e >= 0; e--) 2989 if (pb->eqs[e].coef[i]) 2990 { 2991 eqn eqn = &(pb->eqs[e]); 2992 int j, k; 2993 for (j = n_vars; j >= 0; j--) 2994 eqn->coef[j] *= a; 2995 k = eqn->coef[i]; 2996 eqn->coef[i] = 0; 2997 if (sub->color == omega_red) 2998 eqn->color = omega_red; 2999 for (j = n_vars; j >= 0; j--) 3000 eqn->coef[j] -= sub->coef[j] * k / c; 3001 } 3002 3003 for (e = pb->num_geqs - 1; e >= 0; e--) 3004 if (pb->geqs[e].coef[i]) 3005 { 3006 eqn eqn = &(pb->geqs[e]); 3007 int j, k; 3008 3009 if (sub->color == omega_red) 3010 eqn->color = omega_red; 3011 3012 for (j = n_vars; j >= 0; j--) 3013 eqn->coef[j] *= a; 3014 3015 eqn->touched = 1; 3016 k = eqn->coef[i]; 3017 eqn->coef[i] = 0; 3018 3019 for (j = n_vars; j >= 0; j--) 3020 eqn->coef[j] -= sub->coef[j] * k / c; 3021 3022 } 3023 3024 for (e = pb->num_subs - 1; e >= 0; e--) 3025 if (pb->subs[e].coef[i]) 3026 { 3027 eqn eqn = &(pb->subs[e]); 3028 int j, k; 3029 gcc_assert (0); 3030 gcc_assert (sub->color == omega_black); 3031 for (j = n_vars; j >= 0; j--) 3032 eqn->coef[j] *= a; 3033 k = eqn->coef[i]; 3034 eqn->coef[i] = 0; 3035 for (j = n_vars; j >= 0; j--) 3036 eqn->coef[j] -= sub->coef[j] * k / c; 3037 } 3038 3039 if (in_approximate_mode) 3040 omega_delete_variable (pb, i); 3041 else 3042 omega_convert_eq_to_geqs (pb, e2); 3043 } 3044 3045 omega_free_eqns (sub, 1); 3046 } 3047 3048 /* Helper function for printing "sorry, no solution". */ 3049 3050 static inline enum omega_result 3051 omega_problem_has_no_solution (void) 3052 { 3053 if (dump_file && (dump_flags & TDF_DETAILS)) 3054 fprintf (dump_file, "\nequations have no solution \n"); 3055 3056 return omega_false; 3057 } 3058 3059 /* Helper function: solve equations in PB one at a time, following the 3060 DESIRED_RES result. */ 3061 3062 static enum omega_result 3063 omega_solve_eq (omega_pb pb, enum omega_result desired_res) 3064 { 3065 int i, j, e; 3066 int g, g2; 3067 g = 0; 3068 3069 3070 if (dump_file && (dump_flags & TDF_DETAILS) && pb->num_eqs > 0) 3071 { 3072 fprintf (dump_file, "\nomega_solve_eq (%d, %d)\n", 3073 desired_res, may_be_red); 3074 omega_print_problem (dump_file, pb); 3075 fprintf (dump_file, "\n"); 3076 } 3077 3078 if (may_be_red) 3079 { 3080 i = 0; 3081 j = pb->num_eqs - 1; 3082 3083 while (1) 3084 { 3085 eqn eq; 3086 3087 while (i <= j && pb->eqs[i].color == omega_red) 3088 i++; 3089 3090 while (i <= j && pb->eqs[j].color == omega_black) 3091 j--; 3092 3093 if (i >= j) 3094 break; 3095 3096 eq = omega_alloc_eqns (0, 1); 3097 omega_copy_eqn (eq, &pb->eqs[i], pb->num_vars); 3098 omega_copy_eqn (&pb->eqs[i], &pb->eqs[j], pb->num_vars); 3099 omega_copy_eqn (&pb->eqs[j], eq, pb->num_vars); 3100 omega_free_eqns (eq, 1); 3101 i++; 3102 j--; 3103 } 3104 } 3105 3106 /* Eliminate all EQ equations */ 3107 for (e = pb->num_eqs - 1; e >= 0; e--) 3108 { 3109 eqn eqn = &(pb->eqs[e]); 3110 int sv; 3111 3112 if (dump_file && (dump_flags & TDF_DETAILS)) 3113 fprintf (dump_file, "----\n"); 3114 3115 for (i = pb->num_vars; i > 0; i--) 3116 if (eqn->coef[i]) 3117 break; 3118 3119 g = eqn->coef[i]; 3120 3121 for (j = i - 1; j > 0; j--) 3122 if (eqn->coef[j]) 3123 break; 3124 3125 /* i is the position of last nonzero coefficient, 3126 g is the coefficient of i, 3127 j is the position of next nonzero coefficient. */ 3128 3129 if (j == 0) 3130 { 3131 if (eqn->coef[0] % g != 0) 3132 return omega_problem_has_no_solution (); 3133 3134 eqn->coef[0] = eqn->coef[0] / g; 3135 eqn->coef[i] = 1; 3136 pb->num_eqs--; 3137 omega_do_elimination (pb, e, i); 3138 continue; 3139 } 3140 3141 else if (j == -1) 3142 { 3143 if (eqn->coef[0] != 0) 3144 return omega_problem_has_no_solution (); 3145 3146 pb->num_eqs--; 3147 continue; 3148 } 3149 3150 if (g < 0) 3151 g = -g; 3152 3153 if (g == 1) 3154 { 3155 pb->num_eqs--; 3156 omega_do_elimination (pb, e, i); 3157 } 3158 3159 else 3160 { 3161 int k = j; 3162 bool promotion_possible = 3163 (omega_safe_var_p (pb, j) 3164 && pb->safe_vars + 1 == i 3165 && !omega_eqn_is_red (eqn, desired_res) 3166 && !in_approximate_mode); 3167 3168 if (dump_file && (dump_flags & TDF_DETAILS) && promotion_possible) 3169 fprintf (dump_file, " Promotion possible\n"); 3170 3171 normalizeEQ: 3172 if (!omega_safe_var_p (pb, j)) 3173 { 3174 for (; g != 1 && !omega_safe_var_p (pb, j); j--) 3175 g = gcd (abs (eqn->coef[j]), g); 3176 g2 = g; 3177 } 3178 else if (!omega_safe_var_p (pb, i)) 3179 g2 = g; 3180 else 3181 g2 = 0; 3182 3183 for (; g != 1 && j > 0; j--) 3184 g = gcd (abs (eqn->coef[j]), g); 3185 3186 if (g > 1) 3187 { 3188 if (eqn->coef[0] % g != 0) 3189 return omega_problem_has_no_solution (); 3190 3191 for (j = 0; j <= pb->num_vars; j++) 3192 eqn->coef[j] /= g; 3193 3194 g2 = g2 / g; 3195 } 3196 3197 if (g2 > 1) 3198 { 3199 int e2; 3200 3201 for (e2 = e - 1; e2 >= 0; e2--) 3202 if (pb->eqs[e2].coef[i]) 3203 break; 3204 3205 if (e2 == -1) 3206 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--) 3207 if (pb->geqs[e2].coef[i]) 3208 break; 3209 3210 if (e2 == -1) 3211 for (e2 = pb->num_subs - 1; e2 >= 0; e2--) 3212 if (pb->subs[e2].coef[i]) 3213 break; 3214 3215 if (e2 == -1) 3216 { 3217 bool change = false; 3218 3219 if (dump_file && (dump_flags & TDF_DETAILS)) 3220 { 3221 fprintf (dump_file, "Ha! We own it! \n"); 3222 omega_print_eq (dump_file, pb, eqn); 3223 fprintf (dump_file, " \n"); 3224 } 3225 3226 g = eqn->coef[i]; 3227 g = abs (g); 3228 3229 for (j = i - 1; j >= 0; j--) 3230 { 3231 int t = int_mod (eqn->coef[j], g); 3232 3233 if (2 * t >= g) 3234 t -= g; 3235 3236 if (t != eqn->coef[j]) 3237 { 3238 eqn->coef[j] = t; 3239 change = true; 3240 } 3241 } 3242 3243 if (!change) 3244 { 3245 if (dump_file && (dump_flags & TDF_DETAILS)) 3246 fprintf (dump_file, "So what?\n"); 3247 } 3248 3249 else 3250 { 3251 omega_name_wild_card (pb, i); 3252 3253 if (dump_file && (dump_flags & TDF_DETAILS)) 3254 { 3255 omega_print_eq (dump_file, pb, eqn); 3256 fprintf (dump_file, " \n"); 3257 } 3258 3259 e++; 3260 continue; 3261 } 3262 } 3263 } 3264 3265 if (promotion_possible) 3266 { 3267 if (dump_file && (dump_flags & TDF_DETAILS)) 3268 { 3269 fprintf (dump_file, "promoting %s to safety\n", 3270 omega_variable_to_str (pb, i)); 3271 omega_print_vars (dump_file, pb); 3272 } 3273 3274 pb->safe_vars++; 3275 3276 if (!omega_wildcard_p (pb, i)) 3277 omega_name_wild_card (pb, i); 3278 3279 promotion_possible = false; 3280 j = k; 3281 goto normalizeEQ; 3282 } 3283 3284 if (g2 > 1 && !in_approximate_mode) 3285 { 3286 if (pb->eqs[e].color == omega_red) 3287 { 3288 if (dump_file && (dump_flags & TDF_DETAILS)) 3289 fprintf (dump_file, "handling red equality\n"); 3290 3291 pb->num_eqs--; 3292 omega_do_elimination (pb, e, i); 3293 continue; 3294 } 3295 3296 if (dump_file && (dump_flags & TDF_DETAILS)) 3297 { 3298 fprintf (dump_file, 3299 "adding equation to handle safe variable \n"); 3300 omega_print_eq (dump_file, pb, eqn); 3301 fprintf (dump_file, "\n----\n"); 3302 omega_print_problem (dump_file, pb); 3303 fprintf (dump_file, "\n----\n"); 3304 fprintf (dump_file, "\n----\n"); 3305 } 3306 3307 i = omega_add_new_wild_card (pb); 3308 pb->num_eqs++; 3309 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 3310 omega_init_eqn_zero (&pb->eqs[e + 1], pb->num_vars); 3311 omega_copy_eqn (&pb->eqs[e + 1], eqn, pb->safe_vars); 3312 3313 for (j = pb->num_vars; j >= 0; j--) 3314 { 3315 pb->eqs[e + 1].coef[j] = int_mod (pb->eqs[e + 1].coef[j], g2); 3316 3317 if (2 * pb->eqs[e + 1].coef[j] >= g2) 3318 pb->eqs[e + 1].coef[j] -= g2; 3319 } 3320 3321 pb->eqs[e + 1].coef[i] = g2; 3322 e += 2; 3323 3324 if (dump_file && (dump_flags & TDF_DETAILS)) 3325 omega_print_problem (dump_file, pb); 3326 3327 continue; 3328 } 3329 3330 sv = pb->safe_vars; 3331 if (g2 == 0) 3332 sv = 0; 3333 3334 /* Find variable to eliminate. */ 3335 if (g2 > 1) 3336 { 3337 gcc_assert (in_approximate_mode); 3338 3339 if (dump_file && (dump_flags & TDF_DETAILS)) 3340 { 3341 fprintf (dump_file, "non-exact elimination: "); 3342 omega_print_eq (dump_file, pb, eqn); 3343 fprintf (dump_file, "\n"); 3344 omega_print_problem (dump_file, pb); 3345 } 3346 3347 for (i = pb->num_vars; i > sv; i--) 3348 if (pb->eqs[e].coef[i] != 0) 3349 break; 3350 } 3351 else 3352 for (i = pb->num_vars; i > sv; i--) 3353 if (pb->eqs[e].coef[i] == 1 || pb->eqs[e].coef[i] == -1) 3354 break; 3355 3356 if (i > sv) 3357 { 3358 pb->num_eqs--; 3359 omega_do_elimination (pb, e, i); 3360 3361 if (dump_file && (dump_flags & TDF_DETAILS) && g2 > 1) 3362 { 3363 fprintf (dump_file, "result of non-exact elimination:\n"); 3364 omega_print_problem (dump_file, pb); 3365 } 3366 } 3367 else 3368 { 3369 int factor = (INT_MAX); 3370 j = 0; 3371 3372 if (dump_file && (dump_flags & TDF_DETAILS)) 3373 fprintf (dump_file, "doing moding\n"); 3374 3375 for (i = pb->num_vars; i != sv; i--) 3376 if ((pb->eqs[e].coef[i] & 1) != 0) 3377 { 3378 j = i; 3379 i--; 3380 3381 for (; i != sv; i--) 3382 if ((pb->eqs[e].coef[i] & 1) != 0) 3383 break; 3384 3385 break; 3386 } 3387 3388 if (j != 0 && i == sv) 3389 { 3390 omega_do_mod (pb, 2, e, j); 3391 e++; 3392 continue; 3393 } 3394 3395 j = 0; 3396 for (i = pb->num_vars; i != sv; i--) 3397 if (pb->eqs[e].coef[i] != 0 3398 && factor > abs (pb->eqs[e].coef[i]) + 1) 3399 { 3400 factor = abs (pb->eqs[e].coef[i]) + 1; 3401 j = i; 3402 } 3403 3404 if (j == sv) 3405 { 3406 if (dump_file && (dump_flags & TDF_DETAILS)) 3407 fprintf (dump_file, "should not have happened\n"); 3408 gcc_assert (0); 3409 } 3410 3411 omega_do_mod (pb, factor, e, j); 3412 /* Go back and try this equation again. */ 3413 e++; 3414 } 3415 } 3416 } 3417 3418 pb->num_eqs = 0; 3419 return omega_unknown; 3420 } 3421 3422 /* Transform an inequation E to an equality, then solve DIFF problems 3423 based on PB, and only differing by the constant part that is 3424 diminished by one, trying to figure out which of the constants 3425 satisfies PB. */ 3426 3427 static enum omega_result 3428 parallel_splinter (omega_pb pb, int e, int diff, 3429 enum omega_result desired_res) 3430 { 3431 omega_pb tmp_problem; 3432 int i; 3433 3434 if (dump_file && (dump_flags & TDF_DETAILS)) 3435 { 3436 fprintf (dump_file, "Using parallel splintering\n"); 3437 omega_print_problem (dump_file, pb); 3438 } 3439 3440 tmp_problem = XNEW (struct omega_pb_d); 3441 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e], pb->num_vars); 3442 pb->num_eqs = 1; 3443 3444 for (i = 0; i <= diff; i++) 3445 { 3446 omega_copy_problem (tmp_problem, pb); 3447 3448 if (dump_file && (dump_flags & TDF_DETAILS)) 3449 { 3450 fprintf (dump_file, "Splinter # %i\n", i); 3451 omega_print_problem (dump_file, pb); 3452 } 3453 3454 if (omega_solve_problem (tmp_problem, desired_res) == omega_true) 3455 { 3456 free (tmp_problem); 3457 return omega_true; 3458 } 3459 3460 pb->eqs[0].coef[0]--; 3461 } 3462 3463 free (tmp_problem); 3464 return omega_false; 3465 } 3466 3467 /* Helper function: solve equations one at a time. */ 3468 3469 static enum omega_result 3470 omega_solve_geq (omega_pb pb, enum omega_result desired_res) 3471 { 3472 int i, e; 3473 int n_vars, fv; 3474 enum omega_result result; 3475 bool coupled_subscripts = false; 3476 bool smoothed = false; 3477 bool eliminate_again; 3478 bool tried_eliminating_redundant = false; 3479 3480 if (desired_res != omega_simplify) 3481 { 3482 pb->num_subs = 0; 3483 pb->safe_vars = 0; 3484 } 3485 3486 solve_geq_start: 3487 do { 3488 gcc_assert (desired_res == omega_simplify || pb->num_subs == 0); 3489 3490 /* Verify that there are not too many inequalities. */ 3491 gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS); 3492 3493 if (dump_file && (dump_flags & TDF_DETAILS)) 3494 { 3495 fprintf (dump_file, "\nomega_solve_geq (%d,%d):\n", 3496 desired_res, please_no_equalities_in_simplified_problems); 3497 omega_print_problem (dump_file, pb); 3498 fprintf (dump_file, "\n"); 3499 } 3500 3501 n_vars = pb->num_vars; 3502 3503 if (n_vars == 1) 3504 { 3505 enum omega_eqn_color u_color = omega_black; 3506 enum omega_eqn_color l_color = omega_black; 3507 int upper_bound = pos_infinity; 3508 int lower_bound = neg_infinity; 3509 3510 for (e = pb->num_geqs - 1; e >= 0; e--) 3511 { 3512 int a = pb->geqs[e].coef[1]; 3513 int c = pb->geqs[e].coef[0]; 3514 3515 /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax. */ 3516 if (a == 0) 3517 { 3518 if (c < 0) 3519 return omega_problem_has_no_solution (); 3520 } 3521 else if (a > 0) 3522 { 3523 if (a != 1) 3524 c = int_div (c, a); 3525 3526 if (lower_bound < -c 3527 || (lower_bound == -c 3528 && !omega_eqn_is_red (&pb->geqs[e], desired_res))) 3529 { 3530 lower_bound = -c; 3531 l_color = pb->geqs[e].color; 3532 } 3533 } 3534 else 3535 { 3536 if (a != -1) 3537 c = int_div (c, -a); 3538 3539 if (upper_bound > c 3540 || (upper_bound == c 3541 && !omega_eqn_is_red (&pb->geqs[e], desired_res))) 3542 { 3543 upper_bound = c; 3544 u_color = pb->geqs[e].color; 3545 } 3546 } 3547 } 3548 3549 if (dump_file && (dump_flags & TDF_DETAILS)) 3550 { 3551 fprintf (dump_file, "upper bound = %d\n", upper_bound); 3552 fprintf (dump_file, "lower bound = %d\n", lower_bound); 3553 } 3554 3555 if (lower_bound > upper_bound) 3556 return omega_problem_has_no_solution (); 3557 3558 if (desired_res == omega_simplify) 3559 { 3560 pb->num_geqs = 0; 3561 if (pb->safe_vars == 1) 3562 { 3563 3564 if (lower_bound == upper_bound 3565 && u_color == omega_black 3566 && l_color == omega_black) 3567 { 3568 pb->eqs[0].coef[0] = -lower_bound; 3569 pb->eqs[0].coef[1] = 1; 3570 pb->eqs[0].color = omega_black; 3571 pb->num_eqs = 1; 3572 return omega_solve_problem (pb, desired_res); 3573 } 3574 else 3575 { 3576 if (lower_bound > neg_infinity) 3577 { 3578 pb->geqs[0].coef[0] = -lower_bound; 3579 pb->geqs[0].coef[1] = 1; 3580 pb->geqs[0].key = 1; 3581 pb->geqs[0].color = l_color; 3582 pb->geqs[0].touched = 0; 3583 pb->num_geqs = 1; 3584 } 3585 3586 if (upper_bound < pos_infinity) 3587 { 3588 pb->geqs[pb->num_geqs].coef[0] = upper_bound; 3589 pb->geqs[pb->num_geqs].coef[1] = -1; 3590 pb->geqs[pb->num_geqs].key = -1; 3591 pb->geqs[pb->num_geqs].color = u_color; 3592 pb->geqs[pb->num_geqs].touched = 0; 3593 pb->num_geqs++; 3594 } 3595 } 3596 } 3597 else 3598 pb->num_vars = 0; 3599 3600 omega_problem_reduced (pb); 3601 return omega_false; 3602 } 3603 3604 if (original_problem != no_problem 3605 && l_color == omega_black 3606 && u_color == omega_black 3607 && !conservative 3608 && lower_bound == upper_bound) 3609 { 3610 pb->eqs[0].coef[0] = -lower_bound; 3611 pb->eqs[0].coef[1] = 1; 3612 pb->num_eqs = 1; 3613 adding_equality_constraint (pb, 0); 3614 } 3615 3616 return omega_true; 3617 } 3618 3619 if (!pb->variables_freed) 3620 { 3621 pb->variables_freed = true; 3622 3623 if (desired_res != omega_simplify) 3624 omega_free_eliminations (pb, 0); 3625 else 3626 omega_free_eliminations (pb, pb->safe_vars); 3627 3628 n_vars = pb->num_vars; 3629 3630 if (n_vars == 1) 3631 continue; 3632 } 3633 3634 switch (normalize_omega_problem (pb)) 3635 { 3636 case normalize_false: 3637 return omega_false; 3638 break; 3639 3640 case normalize_coupled: 3641 coupled_subscripts = true; 3642 break; 3643 3644 case normalize_uncoupled: 3645 coupled_subscripts = false; 3646 break; 3647 3648 default: 3649 gcc_unreachable (); 3650 } 3651 3652 n_vars = pb->num_vars; 3653 3654 if (dump_file && (dump_flags & TDF_DETAILS)) 3655 { 3656 fprintf (dump_file, "\nafter normalization:\n"); 3657 omega_print_problem (dump_file, pb); 3658 fprintf (dump_file, "\n"); 3659 fprintf (dump_file, "eliminating variable using Fourier-Motzkin.\n"); 3660 } 3661 3662 do { 3663 int parallel_difference = INT_MAX; 3664 int best_parallel_eqn = -1; 3665 int minC, maxC, minCj = 0; 3666 int lower_bound_count = 0; 3667 int e2, Le = 0, Ue; 3668 bool possible_easy_int_solution; 3669 int max_splinters = 1; 3670 bool exact = false; 3671 bool lucky_exact = false; 3672 int best = (INT_MAX); 3673 int j = 0, jLe = 0, jLowerBoundCount = 0; 3674 3675 3676 eliminate_again = false; 3677 3678 if (pb->num_eqs > 0) 3679 return omega_solve_problem (pb, desired_res); 3680 3681 if (!coupled_subscripts) 3682 { 3683 if (pb->safe_vars == 0) 3684 pb->num_geqs = 0; 3685 else 3686 for (e = pb->num_geqs - 1; e >= 0; e--) 3687 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key))) 3688 omega_delete_geq (pb, e, n_vars); 3689 3690 pb->num_vars = pb->safe_vars; 3691 3692 if (desired_res == omega_simplify) 3693 { 3694 omega_problem_reduced (pb); 3695 return omega_false; 3696 } 3697 3698 return omega_true; 3699 } 3700 3701 if (desired_res != omega_simplify) 3702 fv = 0; 3703 else 3704 fv = pb->safe_vars; 3705 3706 if (pb->num_geqs == 0) 3707 { 3708 if (desired_res == omega_simplify) 3709 { 3710 pb->num_vars = pb->safe_vars; 3711 omega_problem_reduced (pb); 3712 return omega_false; 3713 } 3714 return omega_true; 3715 } 3716 3717 if (desired_res == omega_simplify && n_vars == pb->safe_vars) 3718 { 3719 omega_problem_reduced (pb); 3720 return omega_false; 3721 } 3722 3723 if (pb->num_geqs > OMEGA_MAX_GEQS - 30 3724 || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10) 3725 { 3726 if (dump_file && (dump_flags & TDF_DETAILS)) 3727 fprintf (dump_file, 3728 "TOO MANY EQUATIONS; " 3729 "%d equations, %d variables, " 3730 "ELIMINATING REDUNDANT ONES\n", 3731 pb->num_geqs, n_vars); 3732 3733 if (!omega_eliminate_redundant (pb, false)) 3734 return omega_false; 3735 3736 n_vars = pb->num_vars; 3737 3738 if (pb->num_eqs > 0) 3739 return omega_solve_problem (pb, desired_res); 3740 3741 if (dump_file && (dump_flags & TDF_DETAILS)) 3742 fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n"); 3743 } 3744 3745 if (desired_res != omega_simplify) 3746 fv = 0; 3747 else 3748 fv = pb->safe_vars; 3749 3750 for (i = n_vars; i != fv; i--) 3751 { 3752 int score; 3753 int ub = -2; 3754 int lb = -2; 3755 bool lucky = false; 3756 int upper_bound_count = 0; 3757 3758 lower_bound_count = 0; 3759 minC = maxC = 0; 3760 3761 for (e = pb->num_geqs - 1; e >= 0; e--) 3762 if (pb->geqs[e].coef[i] < 0) 3763 { 3764 minC = MIN (minC, pb->geqs[e].coef[i]); 3765 upper_bound_count++; 3766 if (pb->geqs[e].coef[i] < -1) 3767 { 3768 if (ub == -2) 3769 ub = e; 3770 else 3771 ub = -1; 3772 } 3773 } 3774 else if (pb->geqs[e].coef[i] > 0) 3775 { 3776 maxC = MAX (maxC, pb->geqs[e].coef[i]); 3777 lower_bound_count++; 3778 Le = e; 3779 if (pb->geqs[e].coef[i] > 1) 3780 { 3781 if (lb == -2) 3782 lb = e; 3783 else 3784 lb = -1; 3785 } 3786 } 3787 3788 if (lower_bound_count == 0 3789 || upper_bound_count == 0) 3790 { 3791 lower_bound_count = 0; 3792 break; 3793 } 3794 3795 if (ub >= 0 && lb >= 0 3796 && pb->geqs[lb].key == -pb->geqs[ub].key) 3797 { 3798 int Lc = pb->geqs[lb].coef[i]; 3799 int Uc = -pb->geqs[ub].coef[i]; 3800 int diff = 3801 Lc * pb->geqs[ub].coef[0] + Uc * pb->geqs[lb].coef[0]; 3802 lucky = (diff >= (Uc - 1) * (Lc - 1)); 3803 } 3804 3805 if (maxC == 1 3806 || minC == -1 3807 || lucky 3808 || in_approximate_mode) 3809 { 3810 score = upper_bound_count * lower_bound_count; 3811 3812 if (dump_file && (dump_flags & TDF_DETAILS)) 3813 fprintf (dump_file, 3814 "For %s, exact, score = %d*%d, range = %d ... %d," 3815 "\nlucky = %d, in_approximate_mode=%d \n", 3816 omega_variable_to_str (pb, i), 3817 upper_bound_count, 3818 lower_bound_count, minC, maxC, lucky, 3819 in_approximate_mode); 3820 3821 if (!exact 3822 || score < best) 3823 { 3824 3825 best = score; 3826 j = i; 3827 minCj = minC; 3828 jLe = Le; 3829 jLowerBoundCount = lower_bound_count; 3830 exact = true; 3831 lucky_exact = lucky; 3832 if (score == 1) 3833 break; 3834 } 3835 } 3836 else if (!exact) 3837 { 3838 if (dump_file && (dump_flags & TDF_DETAILS)) 3839 fprintf (dump_file, 3840 "For %s, non-exact, score = %d*%d," 3841 "range = %d ... %d \n", 3842 omega_variable_to_str (pb, i), 3843 upper_bound_count, 3844 lower_bound_count, minC, maxC); 3845 3846 score = maxC - minC; 3847 3848 if (best > score) 3849 { 3850 best = score; 3851 j = i; 3852 minCj = minC; 3853 jLe = Le; 3854 jLowerBoundCount = lower_bound_count; 3855 } 3856 } 3857 } 3858 3859 if (lower_bound_count == 0) 3860 { 3861 omega_free_eliminations (pb, pb->safe_vars); 3862 n_vars = pb->num_vars; 3863 eliminate_again = true; 3864 continue; 3865 } 3866 3867 i = j; 3868 minC = minCj; 3869 Le = jLe; 3870 lower_bound_count = jLowerBoundCount; 3871 3872 for (e = pb->num_geqs - 1; e >= 0; e--) 3873 if (pb->geqs[e].coef[i] > 0) 3874 { 3875 if (pb->geqs[e].coef[i] == -minC) 3876 max_splinters += -minC - 1; 3877 else 3878 max_splinters += 3879 pos_mul_hwi ((pb->geqs[e].coef[i] - 1), 3880 (-minC - 1)) / (-minC) + 1; 3881 } 3882 3883 /* #ifdef Omega3 */ 3884 /* Trying to produce exact elimination by finding redundant 3885 constraints. */ 3886 if (!exact && !tried_eliminating_redundant) 3887 { 3888 omega_eliminate_redundant (pb, false); 3889 tried_eliminating_redundant = true; 3890 eliminate_again = true; 3891 continue; 3892 } 3893 tried_eliminating_redundant = false; 3894 /* #endif */ 3895 3896 if (return_single_result && desired_res == omega_simplify && !exact) 3897 { 3898 omega_problem_reduced (pb); 3899 return omega_true; 3900 } 3901 3902 /* #ifndef Omega3 */ 3903 /* Trying to produce exact elimination by finding redundant 3904 constraints. */ 3905 if (!exact && !tried_eliminating_redundant) 3906 { 3907 omega_eliminate_redundant (pb, false); 3908 tried_eliminating_redundant = true; 3909 continue; 3910 } 3911 tried_eliminating_redundant = false; 3912 /* #endif */ 3913 3914 if (!exact) 3915 { 3916 int e1, e2; 3917 3918 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--) 3919 if (pb->geqs[e1].color == omega_black) 3920 for (e2 = e1 - 1; e2 >= 0; e2--) 3921 if (pb->geqs[e2].color == omega_black 3922 && pb->geqs[e1].key == -pb->geqs[e2].key 3923 && ((pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0]) 3924 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars)) 3925 / 2 < parallel_difference)) 3926 { 3927 parallel_difference = 3928 (pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0]) 3929 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars)) 3930 / 2; 3931 best_parallel_eqn = e1; 3932 } 3933 3934 if (dump_file && (dump_flags & TDF_DETAILS) 3935 && best_parallel_eqn >= 0) 3936 { 3937 fprintf (dump_file, 3938 "Possible parallel projection, diff = %d, in ", 3939 parallel_difference); 3940 omega_print_geq (dump_file, pb, &(pb->geqs[best_parallel_eqn])); 3941 fprintf (dump_file, "\n"); 3942 omega_print_problem (dump_file, pb); 3943 } 3944 } 3945 3946 if (dump_file && (dump_flags & TDF_DETAILS)) 3947 { 3948 fprintf (dump_file, "going to eliminate %s, (%d,%d,%d)\n", 3949 omega_variable_to_str (pb, i), i, minC, 3950 lower_bound_count); 3951 omega_print_problem (dump_file, pb); 3952 3953 if (lucky_exact) 3954 fprintf (dump_file, "(a lucky exact elimination)\n"); 3955 3956 else if (exact) 3957 fprintf (dump_file, "(an exact elimination)\n"); 3958 3959 fprintf (dump_file, "Max # of splinters = %d\n", max_splinters); 3960 } 3961 3962 gcc_assert (max_splinters >= 1); 3963 3964 if (!exact && desired_res == omega_simplify && best_parallel_eqn >= 0 3965 && parallel_difference <= max_splinters) 3966 return parallel_splinter (pb, best_parallel_eqn, parallel_difference, 3967 desired_res); 3968 3969 smoothed = false; 3970 3971 if (i != n_vars) 3972 { 3973 int t; 3974 int j = pb->num_vars; 3975 3976 if (dump_file && (dump_flags & TDF_DETAILS)) 3977 { 3978 fprintf (dump_file, "Swapping %d and %d\n", i, j); 3979 omega_print_problem (dump_file, pb); 3980 } 3981 3982 swap (&pb->var[i], &pb->var[j]); 3983 3984 for (e = pb->num_geqs - 1; e >= 0; e--) 3985 if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j]) 3986 { 3987 pb->geqs[e].touched = 1; 3988 t = pb->geqs[e].coef[i]; 3989 pb->geqs[e].coef[i] = pb->geqs[e].coef[j]; 3990 pb->geqs[e].coef[j] = t; 3991 } 3992 3993 for (e = pb->num_subs - 1; e >= 0; e--) 3994 if (pb->subs[e].coef[i] != pb->subs[e].coef[j]) 3995 { 3996 t = pb->subs[e].coef[i]; 3997 pb->subs[e].coef[i] = pb->subs[e].coef[j]; 3998 pb->subs[e].coef[j] = t; 3999 } 4000 4001 if (dump_file && (dump_flags & TDF_DETAILS)) 4002 { 4003 fprintf (dump_file, "Swapping complete \n"); 4004 omega_print_problem (dump_file, pb); 4005 fprintf (dump_file, "\n"); 4006 } 4007 4008 i = j; 4009 } 4010 4011 else if (dump_file && (dump_flags & TDF_DETAILS)) 4012 { 4013 fprintf (dump_file, "No swap needed\n"); 4014 omega_print_problem (dump_file, pb); 4015 } 4016 4017 pb->num_vars--; 4018 n_vars = pb->num_vars; 4019 4020 if (exact) 4021 { 4022 if (n_vars == 1) 4023 { 4024 int upper_bound = pos_infinity; 4025 int lower_bound = neg_infinity; 4026 enum omega_eqn_color ub_color = omega_black; 4027 enum omega_eqn_color lb_color = omega_black; 4028 int topeqn = pb->num_geqs - 1; 4029 int Lc = pb->geqs[Le].coef[i]; 4030 4031 for (Le = topeqn; Le >= 0; Le--) 4032 if ((Lc = pb->geqs[Le].coef[i]) == 0) 4033 { 4034 if (pb->geqs[Le].coef[1] == 1) 4035 { 4036 int constantTerm = -pb->geqs[Le].coef[0]; 4037 4038 if (constantTerm > lower_bound || 4039 (constantTerm == lower_bound && 4040 !omega_eqn_is_red (&pb->geqs[Le], desired_res))) 4041 { 4042 lower_bound = constantTerm; 4043 lb_color = pb->geqs[Le].color; 4044 } 4045 4046 if (dump_file && (dump_flags & TDF_DETAILS)) 4047 { 4048 if (pb->geqs[Le].color == omega_black) 4049 fprintf (dump_file, " :::=> %s >= %d\n", 4050 omega_variable_to_str (pb, 1), 4051 constantTerm); 4052 else 4053 fprintf (dump_file, 4054 " :::=> [%s >= %d]\n", 4055 omega_variable_to_str (pb, 1), 4056 constantTerm); 4057 } 4058 } 4059 else 4060 { 4061 int constantTerm = pb->geqs[Le].coef[0]; 4062 if (constantTerm < upper_bound || 4063 (constantTerm == upper_bound 4064 && !omega_eqn_is_red (&pb->geqs[Le], 4065 desired_res))) 4066 { 4067 upper_bound = constantTerm; 4068 ub_color = pb->geqs[Le].color; 4069 } 4070 4071 if (dump_file && (dump_flags & TDF_DETAILS)) 4072 { 4073 if (pb->geqs[Le].color == omega_black) 4074 fprintf (dump_file, " :::=> %s <= %d\n", 4075 omega_variable_to_str (pb, 1), 4076 constantTerm); 4077 else 4078 fprintf (dump_file, 4079 " :::=> [%s <= %d]\n", 4080 omega_variable_to_str (pb, 1), 4081 constantTerm); 4082 } 4083 } 4084 } 4085 else if (Lc > 0) 4086 for (Ue = topeqn; Ue >= 0; Ue--) 4087 if (pb->geqs[Ue].coef[i] < 0 4088 && pb->geqs[Le].key != -pb->geqs[Ue].key) 4089 { 4090 int Uc = -pb->geqs[Ue].coef[i]; 4091 int coefficient = pb->geqs[Ue].coef[1] * Lc 4092 + pb->geqs[Le].coef[1] * Uc; 4093 int constantTerm = pb->geqs[Ue].coef[0] * Lc 4094 + pb->geqs[Le].coef[0] * Uc; 4095 4096 if (dump_file && (dump_flags & TDF_DETAILS)) 4097 { 4098 omega_print_geq_extra (dump_file, pb, 4099 &(pb->geqs[Ue])); 4100 fprintf (dump_file, "\n"); 4101 omega_print_geq_extra (dump_file, pb, 4102 &(pb->geqs[Le])); 4103 fprintf (dump_file, "\n"); 4104 } 4105 4106 if (coefficient > 0) 4107 { 4108 constantTerm = -int_div (constantTerm, coefficient); 4109 4110 if (constantTerm > lower_bound 4111 || (constantTerm == lower_bound 4112 && (desired_res != omega_simplify 4113 || (pb->geqs[Ue].color == omega_black 4114 && pb->geqs[Le].color == omega_black)))) 4115 { 4116 lower_bound = constantTerm; 4117 lb_color = (pb->geqs[Ue].color == omega_red 4118 || pb->geqs[Le].color == omega_red) 4119 ? omega_red : omega_black; 4120 } 4121 4122 if (dump_file && (dump_flags & TDF_DETAILS)) 4123 { 4124 if (pb->geqs[Ue].color == omega_red 4125 || pb->geqs[Le].color == omega_red) 4126 fprintf (dump_file, 4127 " ::=> [%s >= %d]\n", 4128 omega_variable_to_str (pb, 1), 4129 constantTerm); 4130 else 4131 fprintf (dump_file, 4132 " ::=> %s >= %d\n", 4133 omega_variable_to_str (pb, 1), 4134 constantTerm); 4135 } 4136 } 4137 else 4138 { 4139 constantTerm = int_div (constantTerm, -coefficient); 4140 if (constantTerm < upper_bound 4141 || (constantTerm == upper_bound 4142 && pb->geqs[Ue].color == omega_black 4143 && pb->geqs[Le].color == omega_black)) 4144 { 4145 upper_bound = constantTerm; 4146 ub_color = (pb->geqs[Ue].color == omega_red 4147 || pb->geqs[Le].color == omega_red) 4148 ? omega_red : omega_black; 4149 } 4150 4151 if (dump_file 4152 && (dump_flags & TDF_DETAILS)) 4153 { 4154 if (pb->geqs[Ue].color == omega_red 4155 || pb->geqs[Le].color == omega_red) 4156 fprintf (dump_file, 4157 " ::=> [%s <= %d]\n", 4158 omega_variable_to_str (pb, 1), 4159 constantTerm); 4160 else 4161 fprintf (dump_file, 4162 " ::=> %s <= %d\n", 4163 omega_variable_to_str (pb, 1), 4164 constantTerm); 4165 } 4166 } 4167 } 4168 4169 pb->num_geqs = 0; 4170 4171 if (dump_file && (dump_flags & TDF_DETAILS)) 4172 fprintf (dump_file, 4173 " therefore, %c%d <= %c%s%c <= %d%c\n", 4174 lb_color == omega_red ? '[' : ' ', lower_bound, 4175 (lb_color == omega_red && ub_color == omega_black) 4176 ? ']' : ' ', 4177 omega_variable_to_str (pb, 1), 4178 (lb_color == omega_black && ub_color == omega_red) 4179 ? '[' : ' ', 4180 upper_bound, ub_color == omega_red ? ']' : ' '); 4181 4182 if (lower_bound > upper_bound) 4183 return omega_false; 4184 4185 if (pb->safe_vars == 1) 4186 { 4187 if (upper_bound == lower_bound 4188 && !(ub_color == omega_red || lb_color == omega_red) 4189 && !please_no_equalities_in_simplified_problems) 4190 { 4191 pb->num_eqs++; 4192 pb->eqs[0].coef[1] = -1; 4193 pb->eqs[0].coef[0] = upper_bound; 4194 4195 if (ub_color == omega_red 4196 || lb_color == omega_red) 4197 pb->eqs[0].color = omega_red; 4198 4199 if (desired_res == omega_simplify 4200 && pb->eqs[0].color == omega_black) 4201 return omega_solve_problem (pb, desired_res); 4202 } 4203 4204 if (upper_bound != pos_infinity) 4205 { 4206 pb->geqs[0].coef[1] = -1; 4207 pb->geqs[0].coef[0] = upper_bound; 4208 pb->geqs[0].color = ub_color; 4209 pb->geqs[0].key = -1; 4210 pb->geqs[0].touched = 0; 4211 pb->num_geqs++; 4212 } 4213 4214 if (lower_bound != neg_infinity) 4215 { 4216 pb->geqs[pb->num_geqs].coef[1] = 1; 4217 pb->geqs[pb->num_geqs].coef[0] = -lower_bound; 4218 pb->geqs[pb->num_geqs].color = lb_color; 4219 pb->geqs[pb->num_geqs].key = 1; 4220 pb->geqs[pb->num_geqs].touched = 0; 4221 pb->num_geqs++; 4222 } 4223 } 4224 4225 if (desired_res == omega_simplify) 4226 { 4227 omega_problem_reduced (pb); 4228 return omega_false; 4229 } 4230 else 4231 { 4232 if (!conservative 4233 && (desired_res != omega_simplify 4234 || (lb_color == omega_black 4235 && ub_color == omega_black)) 4236 && original_problem != no_problem 4237 && lower_bound == upper_bound) 4238 { 4239 for (i = original_problem->num_vars; i >= 0; i--) 4240 if (original_problem->var[i] == pb->var[1]) 4241 break; 4242 4243 if (i == 0) 4244 break; 4245 4246 e = original_problem->num_eqs++; 4247 omega_init_eqn_zero (&original_problem->eqs[e], 4248 original_problem->num_vars); 4249 original_problem->eqs[e].coef[i] = -1; 4250 original_problem->eqs[e].coef[0] = upper_bound; 4251 4252 if (dump_file && (dump_flags & TDF_DETAILS)) 4253 { 4254 fprintf (dump_file, 4255 "adding equality %d to outer problem\n", e); 4256 omega_print_problem (dump_file, original_problem); 4257 } 4258 } 4259 return omega_true; 4260 } 4261 } 4262 4263 eliminate_again = true; 4264 4265 if (lower_bound_count == 1) 4266 { 4267 eqn lbeqn = omega_alloc_eqns (0, 1); 4268 int Lc = pb->geqs[Le].coef[i]; 4269 4270 if (dump_file && (dump_flags & TDF_DETAILS)) 4271 fprintf (dump_file, "an inplace elimination\n"); 4272 4273 omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1)); 4274 omega_delete_geq_extra (pb, Le, n_vars + 1); 4275 4276 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--) 4277 if (pb->geqs[Ue].coef[i] < 0) 4278 { 4279 if (lbeqn->key == -pb->geqs[Ue].key) 4280 omega_delete_geq_extra (pb, Ue, n_vars + 1); 4281 else 4282 { 4283 int k; 4284 int Uc = -pb->geqs[Ue].coef[i]; 4285 pb->geqs[Ue].touched = 1; 4286 eliminate_again = false; 4287 4288 if (lbeqn->color == omega_red) 4289 pb->geqs[Ue].color = omega_red; 4290 4291 for (k = 0; k <= n_vars; k++) 4292 pb->geqs[Ue].coef[k] = 4293 mul_hwi (pb->geqs[Ue].coef[k], Lc) + 4294 mul_hwi (lbeqn->coef[k], Uc); 4295 4296 if (dump_file && (dump_flags & TDF_DETAILS)) 4297 { 4298 omega_print_geq (dump_file, pb, 4299 &(pb->geqs[Ue])); 4300 fprintf (dump_file, "\n"); 4301 } 4302 } 4303 } 4304 4305 omega_free_eqns (lbeqn, 1); 4306 continue; 4307 } 4308 else 4309 { 4310 int *dead_eqns = XNEWVEC (int, OMEGA_MAX_GEQS); 4311 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS); 4312 int num_dead = 0; 4313 int top_eqn = pb->num_geqs - 1; 4314 lower_bound_count--; 4315 4316 if (dump_file && (dump_flags & TDF_DETAILS)) 4317 fprintf (dump_file, "lower bound count = %d\n", 4318 lower_bound_count); 4319 4320 for (Le = top_eqn; Le >= 0; Le--) 4321 if (pb->geqs[Le].coef[i] > 0) 4322 { 4323 int Lc = pb->geqs[Le].coef[i]; 4324 for (Ue = top_eqn; Ue >= 0; Ue--) 4325 if (pb->geqs[Ue].coef[i] < 0) 4326 { 4327 if (pb->geqs[Le].key != -pb->geqs[Ue].key) 4328 { 4329 int k; 4330 int Uc = -pb->geqs[Ue].coef[i]; 4331 4332 if (num_dead == 0) 4333 e2 = pb->num_geqs++; 4334 else 4335 e2 = dead_eqns[--num_dead]; 4336 4337 gcc_assert (e2 < OMEGA_MAX_GEQS); 4338 4339 if (dump_file && (dump_flags & TDF_DETAILS)) 4340 { 4341 fprintf (dump_file, 4342 "Le = %d, Ue = %d, gen = %d\n", 4343 Le, Ue, e2); 4344 omega_print_geq_extra (dump_file, pb, 4345 &(pb->geqs[Le])); 4346 fprintf (dump_file, "\n"); 4347 omega_print_geq_extra (dump_file, pb, 4348 &(pb->geqs[Ue])); 4349 fprintf (dump_file, "\n"); 4350 } 4351 4352 eliminate_again = false; 4353 4354 for (k = n_vars; k >= 0; k--) 4355 pb->geqs[e2].coef[k] = 4356 mul_hwi (pb->geqs[Ue].coef[k], Lc) + 4357 mul_hwi (pb->geqs[Le].coef[k], Uc); 4358 4359 pb->geqs[e2].coef[n_vars + 1] = 0; 4360 pb->geqs[e2].touched = 1; 4361 4362 if (pb->geqs[Ue].color == omega_red 4363 || pb->geqs[Le].color == omega_red) 4364 pb->geqs[e2].color = omega_red; 4365 else 4366 pb->geqs[e2].color = omega_black; 4367 4368 if (dump_file && (dump_flags & TDF_DETAILS)) 4369 { 4370 omega_print_geq (dump_file, pb, 4371 &(pb->geqs[e2])); 4372 fprintf (dump_file, "\n"); 4373 } 4374 } 4375 4376 if (lower_bound_count == 0) 4377 { 4378 dead_eqns[num_dead++] = Ue; 4379 4380 if (dump_file && (dump_flags & TDF_DETAILS)) 4381 fprintf (dump_file, "Killed %d\n", Ue); 4382 } 4383 } 4384 4385 lower_bound_count--; 4386 dead_eqns[num_dead++] = Le; 4387 4388 if (dump_file && (dump_flags & TDF_DETAILS)) 4389 fprintf (dump_file, "Killed %d\n", Le); 4390 } 4391 4392 for (e = pb->num_geqs - 1; e >= 0; e--) 4393 is_dead[e] = false; 4394 4395 while (num_dead > 0) 4396 is_dead[dead_eqns[--num_dead]] = true; 4397 4398 for (e = pb->num_geqs - 1; e >= 0; e--) 4399 if (is_dead[e]) 4400 omega_delete_geq_extra (pb, e, n_vars + 1); 4401 4402 free (dead_eqns); 4403 free (is_dead); 4404 continue; 4405 } 4406 } 4407 else 4408 { 4409 omega_pb rS, iS; 4410 4411 rS = omega_alloc_problem (0, 0); 4412 iS = omega_alloc_problem (0, 0); 4413 e2 = 0; 4414 possible_easy_int_solution = true; 4415 4416 for (e = 0; e < pb->num_geqs; e++) 4417 if (pb->geqs[e].coef[i] == 0) 4418 { 4419 omega_copy_eqn (&(rS->geqs[e2]), &pb->geqs[e], 4420 pb->num_vars); 4421 omega_copy_eqn (&(iS->geqs[e2]), &pb->geqs[e], 4422 pb->num_vars); 4423 4424 if (dump_file && (dump_flags & TDF_DETAILS)) 4425 { 4426 int t; 4427 fprintf (dump_file, "Copying (%d, %d): ", i, 4428 pb->geqs[e].coef[i]); 4429 omega_print_geq_extra (dump_file, pb, &pb->geqs[e]); 4430 fprintf (dump_file, "\n"); 4431 for (t = 0; t <= n_vars + 1; t++) 4432 fprintf (dump_file, "%d ", pb->geqs[e].coef[t]); 4433 fprintf (dump_file, "\n"); 4434 4435 } 4436 e2++; 4437 gcc_assert (e2 < OMEGA_MAX_GEQS); 4438 } 4439 4440 for (Le = pb->num_geqs - 1; Le >= 0; Le--) 4441 if (pb->geqs[Le].coef[i] > 0) 4442 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--) 4443 if (pb->geqs[Ue].coef[i] < 0) 4444 { 4445 int k; 4446 int Lc = pb->geqs[Le].coef[i]; 4447 int Uc = -pb->geqs[Ue].coef[i]; 4448 4449 if (pb->geqs[Le].key != -pb->geqs[Ue].key) 4450 { 4451 4452 rS->geqs[e2].touched = iS->geqs[e2].touched = 1; 4453 4454 if (dump_file && (dump_flags & TDF_DETAILS)) 4455 { 4456 fprintf (dump_file, "---\n"); 4457 fprintf (dump_file, 4458 "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n", 4459 Le, Lc, Ue, Uc, e2); 4460 omega_print_geq_extra (dump_file, pb, &pb->geqs[Le]); 4461 fprintf (dump_file, "\n"); 4462 omega_print_geq_extra (dump_file, pb, &pb->geqs[Ue]); 4463 fprintf (dump_file, "\n"); 4464 } 4465 4466 if (Uc == Lc) 4467 { 4468 for (k = n_vars; k >= 0; k--) 4469 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] = 4470 pb->geqs[Ue].coef[k] + pb->geqs[Le].coef[k]; 4471 4472 iS->geqs[e2].coef[0] -= (Uc - 1); 4473 } 4474 else 4475 { 4476 for (k = n_vars; k >= 0; k--) 4477 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] = 4478 mul_hwi (pb->geqs[Ue].coef[k], Lc) + 4479 mul_hwi (pb->geqs[Le].coef[k], Uc); 4480 4481 iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1); 4482 } 4483 4484 if (pb->geqs[Ue].color == omega_red 4485 || pb->geqs[Le].color == omega_red) 4486 iS->geqs[e2].color = rS->geqs[e2].color = omega_red; 4487 else 4488 iS->geqs[e2].color = rS->geqs[e2].color = omega_black; 4489 4490 if (dump_file && (dump_flags & TDF_DETAILS)) 4491 { 4492 omega_print_geq (dump_file, pb, &(rS->geqs[e2])); 4493 fprintf (dump_file, "\n"); 4494 } 4495 4496 e2++; 4497 gcc_assert (e2 < OMEGA_MAX_GEQS); 4498 } 4499 else if (pb->geqs[Ue].coef[0] * Lc + 4500 pb->geqs[Le].coef[0] * Uc - 4501 (Uc - 1) * (Lc - 1) < 0) 4502 possible_easy_int_solution = false; 4503 } 4504 4505 iS->variables_initialized = rS->variables_initialized = true; 4506 iS->num_vars = rS->num_vars = pb->num_vars; 4507 iS->num_geqs = rS->num_geqs = e2; 4508 iS->num_eqs = rS->num_eqs = 0; 4509 iS->num_subs = rS->num_subs = pb->num_subs; 4510 iS->safe_vars = rS->safe_vars = pb->safe_vars; 4511 4512 for (e = n_vars; e >= 0; e--) 4513 rS->var[e] = pb->var[e]; 4514 4515 for (e = n_vars; e >= 0; e--) 4516 iS->var[e] = pb->var[e]; 4517 4518 for (e = pb->num_subs - 1; e >= 0; e--) 4519 { 4520 omega_copy_eqn (&(rS->subs[e]), &(pb->subs[e]), pb->num_vars); 4521 omega_copy_eqn (&(iS->subs[e]), &(pb->subs[e]), pb->num_vars); 4522 } 4523 4524 pb->num_vars++; 4525 n_vars = pb->num_vars; 4526 4527 if (desired_res != omega_true) 4528 { 4529 if (original_problem == no_problem) 4530 { 4531 original_problem = pb; 4532 result = omega_solve_geq (rS, omega_false); 4533 original_problem = no_problem; 4534 } 4535 else 4536 result = omega_solve_geq (rS, omega_false); 4537 4538 if (result == omega_false) 4539 { 4540 free (rS); 4541 free (iS); 4542 return result; 4543 } 4544 4545 if (pb->num_eqs > 0) 4546 { 4547 /* An equality constraint must have been found */ 4548 free (rS); 4549 free (iS); 4550 return omega_solve_problem (pb, desired_res); 4551 } 4552 } 4553 4554 if (desired_res != omega_false) 4555 { 4556 int j; 4557 int lower_bounds = 0; 4558 int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS); 4559 4560 if (possible_easy_int_solution) 4561 { 4562 conservative++; 4563 result = omega_solve_geq (iS, desired_res); 4564 conservative--; 4565 4566 if (result != omega_false) 4567 { 4568 free (rS); 4569 free (iS); 4570 free (lower_bound); 4571 return result; 4572 } 4573 } 4574 4575 if (!exact && best_parallel_eqn >= 0 4576 && parallel_difference <= max_splinters) 4577 { 4578 free (rS); 4579 free (iS); 4580 free (lower_bound); 4581 return parallel_splinter (pb, best_parallel_eqn, 4582 parallel_difference, 4583 desired_res); 4584 } 4585 4586 if (dump_file && (dump_flags & TDF_DETAILS)) 4587 fprintf (dump_file, "have to do exact analysis\n"); 4588 4589 conservative++; 4590 4591 for (e = 0; e < pb->num_geqs; e++) 4592 if (pb->geqs[e].coef[i] > 1) 4593 lower_bound[lower_bounds++] = e; 4594 4595 /* Sort array LOWER_BOUND. */ 4596 for (j = 0; j < lower_bounds; j++) 4597 { 4598 int k, smallest = j; 4599 4600 for (k = j + 1; k < lower_bounds; k++) 4601 if (pb->geqs[lower_bound[smallest]].coef[i] > 4602 pb->geqs[lower_bound[k]].coef[i]) 4603 smallest = k; 4604 4605 k = lower_bound[smallest]; 4606 lower_bound[smallest] = lower_bound[j]; 4607 lower_bound[j] = k; 4608 } 4609 4610 if (dump_file && (dump_flags & TDF_DETAILS)) 4611 { 4612 fprintf (dump_file, "lower bound coefficients = "); 4613 4614 for (j = 0; j < lower_bounds; j++) 4615 fprintf (dump_file, " %d", 4616 pb->geqs[lower_bound[j]].coef[i]); 4617 4618 fprintf (dump_file, "\n"); 4619 } 4620 4621 for (j = 0; j < lower_bounds; j++) 4622 { 4623 int max_incr; 4624 int c; 4625 int worst_lower_bound_constant = -minC; 4626 4627 e = lower_bound[j]; 4628 max_incr = (((pb->geqs[e].coef[i] - 1) * 4629 (worst_lower_bound_constant - 1) - 1) 4630 / worst_lower_bound_constant); 4631 /* max_incr += 2; */ 4632 4633 if (dump_file && (dump_flags & TDF_DETAILS)) 4634 { 4635 fprintf (dump_file, "for equation "); 4636 omega_print_geq (dump_file, pb, &pb->geqs[e]); 4637 fprintf (dump_file, 4638 "\ntry decrements from 0 to %d\n", 4639 max_incr); 4640 omega_print_problem (dump_file, pb); 4641 } 4642 4643 if (max_incr > 50 && !smoothed 4644 && smooth_weird_equations (pb)) 4645 { 4646 conservative--; 4647 free (rS); 4648 free (iS); 4649 smoothed = true; 4650 goto solve_geq_start; 4651 } 4652 4653 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e], 4654 pb->num_vars); 4655 pb->eqs[0].color = omega_black; 4656 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars); 4657 pb->geqs[e].touched = 1; 4658 pb->num_eqs = 1; 4659 4660 for (c = max_incr; c >= 0; c--) 4661 { 4662 if (dump_file && (dump_flags & TDF_DETAILS)) 4663 { 4664 fprintf (dump_file, 4665 "trying next decrement of %d\n", 4666 max_incr - c); 4667 omega_print_problem (dump_file, pb); 4668 } 4669 4670 omega_copy_problem (rS, pb); 4671 4672 if (dump_file && (dump_flags & TDF_DETAILS)) 4673 omega_print_problem (dump_file, rS); 4674 4675 result = omega_solve_problem (rS, desired_res); 4676 4677 if (result == omega_true) 4678 { 4679 free (rS); 4680 free (iS); 4681 free (lower_bound); 4682 conservative--; 4683 return omega_true; 4684 } 4685 4686 pb->eqs[0].coef[0]--; 4687 } 4688 4689 if (j + 1 < lower_bounds) 4690 { 4691 pb->num_eqs = 0; 4692 omega_copy_eqn (&pb->geqs[e], &pb->eqs[0], 4693 pb->num_vars); 4694 pb->geqs[e].touched = 1; 4695 pb->geqs[e].color = omega_black; 4696 omega_copy_problem (rS, pb); 4697 4698 if (dump_file && (dump_flags & TDF_DETAILS)) 4699 fprintf (dump_file, 4700 "exhausted lower bound, " 4701 "checking if still feasible "); 4702 4703 result = omega_solve_problem (rS, omega_false); 4704 4705 if (result == omega_false) 4706 break; 4707 } 4708 } 4709 4710 if (dump_file && (dump_flags & TDF_DETAILS)) 4711 fprintf (dump_file, "fall-off the end\n"); 4712 4713 free (rS); 4714 free (iS); 4715 free (lower_bound); 4716 conservative--; 4717 return omega_false; 4718 } 4719 4720 free (rS); 4721 free (iS); 4722 } 4723 return omega_unknown; 4724 } while (eliminate_again); 4725 } while (1); 4726 } 4727 4728 /* Because the omega solver is recursive, this counter limits the 4729 recursion depth. */ 4730 static int omega_solve_depth = 0; 4731 4732 /* Return omega_true when the problem PB has a solution following the 4733 DESIRED_RES. */ 4734 4735 enum omega_result 4736 omega_solve_problem (omega_pb pb, enum omega_result desired_res) 4737 { 4738 enum omega_result result; 4739 4740 gcc_assert (pb->num_vars >= pb->safe_vars); 4741 omega_solve_depth++; 4742 4743 if (desired_res != omega_simplify) 4744 pb->safe_vars = 0; 4745 4746 if (omega_solve_depth > 50) 4747 { 4748 if (dump_file && (dump_flags & TDF_DETAILS)) 4749 { 4750 fprintf (dump_file, 4751 "Solve depth = %d, in_approximate_mode = %d, aborting\n", 4752 omega_solve_depth, in_approximate_mode); 4753 omega_print_problem (dump_file, pb); 4754 } 4755 gcc_assert (0); 4756 } 4757 4758 if (omega_solve_eq (pb, desired_res) == omega_false) 4759 { 4760 omega_solve_depth--; 4761 return omega_false; 4762 } 4763 4764 if (in_approximate_mode && !pb->num_geqs) 4765 { 4766 result = omega_true; 4767 pb->num_vars = pb->safe_vars; 4768 omega_problem_reduced (pb); 4769 } 4770 else 4771 result = omega_solve_geq (pb, desired_res); 4772 4773 omega_solve_depth--; 4774 4775 if (!omega_reduce_with_subs) 4776 { 4777 resurrect_subs (pb); 4778 gcc_assert (please_no_equalities_in_simplified_problems 4779 || !result || pb->num_subs == 0); 4780 } 4781 4782 return result; 4783 } 4784 4785 /* Return true if red equations constrain the set of possible solutions. 4786 We assume that there are solutions to the black equations by 4787 themselves, so if there is no solution to the combined problem, we 4788 return true. */ 4789 4790 bool 4791 omega_problem_has_red_equations (omega_pb pb) 4792 { 4793 bool result; 4794 int e; 4795 int i; 4796 4797 if (dump_file && (dump_flags & TDF_DETAILS)) 4798 { 4799 fprintf (dump_file, "Checking for red equations:\n"); 4800 omega_print_problem (dump_file, pb); 4801 } 4802 4803 please_no_equalities_in_simplified_problems++; 4804 may_be_red++; 4805 4806 if (omega_single_result) 4807 return_single_result++; 4808 4809 create_color = true; 4810 result = (omega_simplify_problem (pb) == omega_false); 4811 4812 if (omega_single_result) 4813 return_single_result--; 4814 4815 may_be_red--; 4816 please_no_equalities_in_simplified_problems--; 4817 4818 if (result) 4819 { 4820 if (dump_file && (dump_flags & TDF_DETAILS)) 4821 fprintf (dump_file, "Gist is FALSE\n"); 4822 4823 pb->num_subs = 0; 4824 pb->num_geqs = 0; 4825 pb->num_eqs = 1; 4826 pb->eqs[0].color = omega_red; 4827 4828 for (i = pb->num_vars; i > 0; i--) 4829 pb->eqs[0].coef[i] = 0; 4830 4831 pb->eqs[0].coef[0] = 1; 4832 return true; 4833 } 4834 4835 free_red_eliminations (pb); 4836 gcc_assert (pb->num_eqs == 0); 4837 4838 for (e = pb->num_geqs - 1; e >= 0; e--) 4839 if (pb->geqs[e].color == omega_red) 4840 result = true; 4841 4842 if (!result) 4843 return false; 4844 4845 for (i = pb->safe_vars; i >= 1; i--) 4846 { 4847 int ub = 0; 4848 int lb = 0; 4849 4850 for (e = pb->num_geqs - 1; e >= 0; e--) 4851 { 4852 if (pb->geqs[e].coef[i]) 4853 { 4854 if (pb->geqs[e].coef[i] > 0) 4855 lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0)); 4856 4857 else 4858 ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0)); 4859 } 4860 } 4861 4862 if (ub == 2 || lb == 2) 4863 { 4864 4865 if (dump_file && (dump_flags & TDF_DETAILS)) 4866 fprintf (dump_file, "checks for upper/lower bounds worked!\n"); 4867 4868 if (!omega_reduce_with_subs) 4869 { 4870 resurrect_subs (pb); 4871 gcc_assert (pb->num_subs == 0); 4872 } 4873 4874 return true; 4875 } 4876 } 4877 4878 4879 if (dump_file && (dump_flags & TDF_DETAILS)) 4880 fprintf (dump_file, 4881 "*** Doing potentially expensive elimination tests " 4882 "for red equations\n"); 4883 4884 please_no_equalities_in_simplified_problems++; 4885 omega_eliminate_red (pb, true); 4886 please_no_equalities_in_simplified_problems--; 4887 4888 result = false; 4889 gcc_assert (pb->num_eqs == 0); 4890 4891 for (e = pb->num_geqs - 1; e >= 0; e--) 4892 if (pb->geqs[e].color == omega_red) 4893 result = true; 4894 4895 if (dump_file && (dump_flags & TDF_DETAILS)) 4896 { 4897 if (!result) 4898 fprintf (dump_file, 4899 "******************** Redundant Red Equations eliminated!!\n"); 4900 else 4901 fprintf (dump_file, 4902 "******************** Red Equations remain\n"); 4903 4904 omega_print_problem (dump_file, pb); 4905 } 4906 4907 if (!omega_reduce_with_subs) 4908 { 4909 normalize_return_type r; 4910 4911 resurrect_subs (pb); 4912 r = normalize_omega_problem (pb); 4913 gcc_assert (r != normalize_false); 4914 4915 coalesce (pb); 4916 cleanout_wildcards (pb); 4917 gcc_assert (pb->num_subs == 0); 4918 } 4919 4920 return result; 4921 } 4922 4923 /* Calls omega_simplify_problem in approximate mode. */ 4924 4925 enum omega_result 4926 omega_simplify_approximate (omega_pb pb) 4927 { 4928 enum omega_result result; 4929 4930 if (dump_file && (dump_flags & TDF_DETAILS)) 4931 fprintf (dump_file, "(Entering approximate mode\n"); 4932 4933 in_approximate_mode = true; 4934 result = omega_simplify_problem (pb); 4935 in_approximate_mode = false; 4936 4937 gcc_assert (pb->num_vars == pb->safe_vars); 4938 if (!omega_reduce_with_subs) 4939 gcc_assert (pb->num_subs == 0); 4940 4941 if (dump_file && (dump_flags & TDF_DETAILS)) 4942 fprintf (dump_file, "Leaving approximate mode)\n"); 4943 4944 return result; 4945 } 4946 4947 4948 /* Simplifies problem PB by eliminating redundant constraints and 4949 reducing the constraints system to a minimal form. Returns 4950 omega_true when the problem was successfully reduced, omega_unknown 4951 when the solver is unable to determine an answer. */ 4952 4953 enum omega_result 4954 omega_simplify_problem (omega_pb pb) 4955 { 4956 int i; 4957 4958 omega_found_reduction = omega_false; 4959 4960 if (!pb->variables_initialized) 4961 omega_initialize_variables (pb); 4962 4963 if (next_key * 3 > MAX_KEYS) 4964 { 4965 int e; 4966 4967 hash_version++; 4968 next_key = OMEGA_MAX_VARS + 1; 4969 4970 for (e = pb->num_geqs - 1; e >= 0; e--) 4971 pb->geqs[e].touched = 1; 4972 4973 for (i = 0; i < HASH_TABLE_SIZE; i++) 4974 hash_master[i].touched = -1; 4975 4976 pb->hash_version = hash_version; 4977 } 4978 4979 else if (pb->hash_version != hash_version) 4980 { 4981 int e; 4982 4983 for (e = pb->num_geqs - 1; e >= 0; e--) 4984 pb->geqs[e].touched = 1; 4985 4986 pb->hash_version = hash_version; 4987 } 4988 4989 if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars) 4990 omega_free_eliminations (pb, pb->safe_vars); 4991 4992 if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0) 4993 { 4994 omega_found_reduction = omega_solve_problem (pb, omega_unknown); 4995 4996 if (omega_found_reduction != omega_false 4997 && !return_single_result) 4998 { 4999 pb->num_geqs = 0; 5000 pb->num_eqs = 0; 5001 (*omega_when_reduced) (pb); 5002 } 5003 5004 return omega_found_reduction; 5005 } 5006 5007 omega_solve_problem (pb, omega_simplify); 5008 5009 if (omega_found_reduction != omega_false) 5010 { 5011 for (i = 1; omega_safe_var_p (pb, i); i++) 5012 pb->forwarding_address[pb->var[i]] = i; 5013 5014 for (i = 0; i < pb->num_subs; i++) 5015 pb->forwarding_address[pb->subs[i].key] = -i - 1; 5016 } 5017 5018 if (!omega_reduce_with_subs) 5019 gcc_assert (please_no_equalities_in_simplified_problems 5020 || omega_found_reduction == omega_false 5021 || pb->num_subs == 0); 5022 5023 return omega_found_reduction; 5024 } 5025 5026 /* Make variable VAR unprotected: it then can be eliminated. */ 5027 5028 void 5029 omega_unprotect_variable (omega_pb pb, int var) 5030 { 5031 int e, idx; 5032 idx = pb->forwarding_address[var]; 5033 5034 if (idx < 0) 5035 { 5036 idx = -1 - idx; 5037 pb->num_subs--; 5038 5039 if (idx < pb->num_subs) 5040 { 5041 omega_copy_eqn (&pb->subs[idx], &pb->subs[pb->num_subs], 5042 pb->num_vars); 5043 pb->forwarding_address[pb->subs[idx].key] = -idx - 1; 5044 } 5045 } 5046 else 5047 { 5048 int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS); 5049 int e2; 5050 5051 for (e = pb->num_subs - 1; e >= 0; e--) 5052 bring_to_life[e] = (pb->subs[e].coef[idx] != 0); 5053 5054 for (e2 = pb->num_subs - 1; e2 >= 0; e2--) 5055 if (bring_to_life[e2]) 5056 { 5057 pb->num_vars++; 5058 pb->safe_vars++; 5059 5060 if (pb->safe_vars < pb->num_vars) 5061 { 5062 for (e = pb->num_geqs - 1; e >= 0; e--) 5063 { 5064 pb->geqs[e].coef[pb->num_vars] = 5065 pb->geqs[e].coef[pb->safe_vars]; 5066 5067 pb->geqs[e].coef[pb->safe_vars] = 0; 5068 } 5069 5070 for (e = pb->num_eqs - 1; e >= 0; e--) 5071 { 5072 pb->eqs[e].coef[pb->num_vars] = 5073 pb->eqs[e].coef[pb->safe_vars]; 5074 5075 pb->eqs[e].coef[pb->safe_vars] = 0; 5076 } 5077 5078 for (e = pb->num_subs - 1; e >= 0; e--) 5079 { 5080 pb->subs[e].coef[pb->num_vars] = 5081 pb->subs[e].coef[pb->safe_vars]; 5082 5083 pb->subs[e].coef[pb->safe_vars] = 0; 5084 } 5085 5086 pb->var[pb->num_vars] = pb->var[pb->safe_vars]; 5087 pb->forwarding_address[pb->var[pb->num_vars]] = 5088 pb->num_vars; 5089 } 5090 else 5091 { 5092 for (e = pb->num_geqs - 1; e >= 0; e--) 5093 pb->geqs[e].coef[pb->safe_vars] = 0; 5094 5095 for (e = pb->num_eqs - 1; e >= 0; e--) 5096 pb->eqs[e].coef[pb->safe_vars] = 0; 5097 5098 for (e = pb->num_subs - 1; e >= 0; e--) 5099 pb->subs[e].coef[pb->safe_vars] = 0; 5100 } 5101 5102 pb->var[pb->safe_vars] = pb->subs[e2].key; 5103 pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars; 5104 5105 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e2]), 5106 pb->num_vars); 5107 pb->eqs[pb->num_eqs++].coef[pb->safe_vars] = -1; 5108 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 5109 5110 if (e2 < pb->num_subs - 1) 5111 omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]), 5112 pb->num_vars); 5113 5114 pb->num_subs--; 5115 } 5116 5117 omega_unprotect_1 (pb, &idx, NULL); 5118 free (bring_to_life); 5119 } 5120 5121 chain_unprotect (pb); 5122 } 5123 5124 /* Unprotects VAR and simplifies PB. */ 5125 5126 enum omega_result 5127 omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color, 5128 int var, int sign) 5129 { 5130 int n_vars = pb->num_vars; 5131 int e, j; 5132 int k = pb->forwarding_address[var]; 5133 5134 if (k < 0) 5135 { 5136 k = -1 - k; 5137 5138 if (sign != 0) 5139 { 5140 e = pb->num_geqs++; 5141 omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars); 5142 5143 for (j = 0; j <= n_vars; j++) 5144 pb->geqs[e].coef[j] *= sign; 5145 5146 pb->geqs[e].coef[0]--; 5147 pb->geqs[e].touched = 1; 5148 pb->geqs[e].color = color; 5149 } 5150 else 5151 { 5152 e = pb->num_eqs++; 5153 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 5154 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars); 5155 pb->eqs[e].color = color; 5156 } 5157 } 5158 else if (sign != 0) 5159 { 5160 e = pb->num_geqs++; 5161 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars); 5162 pb->geqs[e].coef[k] = sign; 5163 pb->geqs[e].coef[0] = -1; 5164 pb->geqs[e].touched = 1; 5165 pb->geqs[e].color = color; 5166 } 5167 else 5168 { 5169 e = pb->num_eqs++; 5170 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 5171 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars); 5172 pb->eqs[e].coef[k] = 1; 5173 pb->eqs[e].color = color; 5174 } 5175 5176 omega_unprotect_variable (pb, var); 5177 return omega_simplify_problem (pb); 5178 } 5179 5180 /* Add an equation "VAR = VALUE" with COLOR to PB. */ 5181 5182 void 5183 omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color, 5184 int var, int value) 5185 { 5186 int e; 5187 int k = pb->forwarding_address[var]; 5188 5189 if (k < 0) 5190 { 5191 k = -1 - k; 5192 e = pb->num_eqs++; 5193 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 5194 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars); 5195 pb->eqs[e].coef[0] -= value; 5196 } 5197 else 5198 { 5199 e = pb->num_eqs++; 5200 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars); 5201 pb->eqs[e].coef[k] = 1; 5202 pb->eqs[e].coef[0] = -value; 5203 } 5204 5205 pb->eqs[e].color = color; 5206 } 5207 5208 /* Return false when the upper and lower bounds are not coupled. 5209 Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of 5210 variable I. */ 5211 5212 bool 5213 omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound) 5214 { 5215 int n_vars = pb->num_vars; 5216 int e, j; 5217 bool is_simple; 5218 bool coupled = false; 5219 5220 *lower_bound = neg_infinity; 5221 *upper_bound = pos_infinity; 5222 i = pb->forwarding_address[i]; 5223 5224 if (i < 0) 5225 { 5226 i = -i - 1; 5227 5228 for (j = 1; j <= n_vars; j++) 5229 if (pb->subs[i].coef[j] != 0) 5230 return true; 5231 5232 *upper_bound = *lower_bound = pb->subs[i].coef[0]; 5233 return false; 5234 } 5235 5236 for (e = pb->num_subs - 1; e >= 0; e--) 5237 if (pb->subs[e].coef[i] != 0) 5238 coupled = true; 5239 5240 for (e = pb->num_eqs - 1; e >= 0; e--) 5241 if (pb->eqs[e].coef[i] != 0) 5242 { 5243 is_simple = true; 5244 5245 for (j = 1; j <= n_vars; j++) 5246 if (i != j && pb->eqs[e].coef[j] != 0) 5247 { 5248 is_simple = false; 5249 coupled = true; 5250 break; 5251 } 5252 5253 if (!is_simple) 5254 continue; 5255 else 5256 { 5257 *lower_bound = *upper_bound = 5258 -pb->eqs[e].coef[i] * pb->eqs[e].coef[0]; 5259 return false; 5260 } 5261 } 5262 5263 for (e = pb->num_geqs - 1; e >= 0; e--) 5264 if (pb->geqs[e].coef[i] != 0) 5265 { 5266 if (pb->geqs[e].key == i) 5267 *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]); 5268 5269 else if (pb->geqs[e].key == -i) 5270 *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]); 5271 5272 else 5273 coupled = true; 5274 } 5275 5276 return coupled; 5277 } 5278 5279 /* Sets the lower bound L and upper bound U for the values of variable 5280 I, and sets COULD_BE_ZERO to true if variable I might take value 5281 zero. LOWER_BOUND and UPPER_BOUND are bounds on the values of 5282 variable I. */ 5283 5284 static void 5285 query_coupled_variable (omega_pb pb, int i, int *l, int *u, 5286 bool *could_be_zero, int lower_bound, int upper_bound) 5287 { 5288 int e, b1, b2; 5289 eqn eqn; 5290 int sign; 5291 int v; 5292 5293 /* Preconditions. */ 5294 gcc_assert (abs (pb->forwarding_address[i]) == 1 5295 && pb->num_vars + pb->num_subs == 2 5296 && pb->num_eqs + pb->num_subs == 1); 5297 5298 /* Define variable I in terms of variable V. */ 5299 if (pb->forwarding_address[i] == -1) 5300 { 5301 eqn = &pb->subs[0]; 5302 sign = 1; 5303 v = 1; 5304 } 5305 else 5306 { 5307 eqn = &pb->eqs[0]; 5308 sign = -eqn->coef[1]; 5309 v = 2; 5310 } 5311 5312 for (e = pb->num_geqs - 1; e >= 0; e--) 5313 if (pb->geqs[e].coef[v] != 0) 5314 { 5315 if (pb->geqs[e].coef[v] == 1) 5316 lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]); 5317 5318 else 5319 upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]); 5320 } 5321 5322 if (lower_bound > upper_bound) 5323 { 5324 *l = pos_infinity; 5325 *u = neg_infinity; 5326 *could_be_zero = 0; 5327 return; 5328 } 5329 5330 if (lower_bound == neg_infinity) 5331 { 5332 if (eqn->coef[v] > 0) 5333 b1 = sign * neg_infinity; 5334 5335 else 5336 b1 = -sign * neg_infinity; 5337 } 5338 else 5339 b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound); 5340 5341 if (upper_bound == pos_infinity) 5342 { 5343 if (eqn->coef[v] > 0) 5344 b2 = sign * pos_infinity; 5345 5346 else 5347 b2 = -sign * pos_infinity; 5348 } 5349 else 5350 b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound); 5351 5352 *l = MAX (*l, b1 <= b2 ? b1 : b2); 5353 *u = MIN (*u, b1 <= b2 ? b2 : b1); 5354 5355 *could_be_zero = (*l <= 0 && 0 <= *u 5356 && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0); 5357 } 5358 5359 /* Return false when a lower bound L and an upper bound U for variable 5360 I in problem PB have been initialized. */ 5361 5362 bool 5363 omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u) 5364 { 5365 *l = neg_infinity; 5366 *u = pos_infinity; 5367 5368 if (!omega_query_variable (pb, i, l, u) 5369 || (pb->num_vars == 1 && pb->forwarding_address[i] == 1)) 5370 return false; 5371 5372 if (abs (pb->forwarding_address[i]) == 1 5373 && pb->num_vars + pb->num_subs == 2 5374 && pb->num_eqs + pb->num_subs == 1) 5375 { 5376 bool could_be_zero; 5377 query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity, 5378 pos_infinity); 5379 return false; 5380 } 5381 5382 return true; 5383 } 5384 5385 /* For problem PB, return an integer that represents the classic data 5386 dependence direction in function of the DD_LT, DD_EQ and DD_GT bit 5387 masks that are added to the result. When DIST_KNOWN is true, DIST 5388 is set to the classic data dependence distance. LOWER_BOUND and 5389 UPPER_BOUND are bounds on the value of variable I, for example, it 5390 is possible to narrow the iteration domain with safe approximations 5391 of loop counts, and thus discard some data dependences that cannot 5392 occur. */ 5393 5394 int 5395 omega_query_variable_signs (omega_pb pb, int i, int dd_lt, 5396 int dd_eq, int dd_gt, int lower_bound, 5397 int upper_bound, bool *dist_known, int *dist) 5398 { 5399 int result; 5400 int l, u; 5401 bool could_be_zero; 5402 5403 l = neg_infinity; 5404 u = pos_infinity; 5405 5406 omega_query_variable (pb, i, &l, &u); 5407 query_coupled_variable (pb, i, &l, &u, &could_be_zero, lower_bound, 5408 upper_bound); 5409 result = 0; 5410 5411 if (l < 0) 5412 result |= dd_gt; 5413 5414 if (u > 0) 5415 result |= dd_lt; 5416 5417 if (could_be_zero) 5418 result |= dd_eq; 5419 5420 if (l == u) 5421 { 5422 *dist_known = true; 5423 *dist = l; 5424 } 5425 else 5426 *dist_known = false; 5427 5428 return result; 5429 } 5430 5431 /* Initialize PB as an Omega problem with NVARS variables and NPROT 5432 safe variables. Safe variables are not eliminated during the 5433 Fourier-Motzkin elimination. Safe variables are all those 5434 variables that are placed at the beginning of the array of 5435 variables: P->var[0, ..., NPROT - 1]. */ 5436 5437 omega_pb 5438 omega_alloc_problem (int nvars, int nprot) 5439 { 5440 omega_pb pb; 5441 5442 gcc_assert (nvars <= OMEGA_MAX_VARS); 5443 omega_initialize (); 5444 5445 /* Allocate and initialize PB. */ 5446 pb = XCNEW (struct omega_pb_d); 5447 pb->var = XCNEWVEC (int, OMEGA_MAX_VARS + 2); 5448 pb->forwarding_address = XCNEWVEC (int, OMEGA_MAX_VARS + 2); 5449 pb->geqs = omega_alloc_eqns (0, OMEGA_MAX_GEQS); 5450 pb->eqs = omega_alloc_eqns (0, OMEGA_MAX_EQS); 5451 pb->subs = omega_alloc_eqns (0, OMEGA_MAX_VARS + 1); 5452 5453 pb->hash_version = hash_version; 5454 pb->num_vars = nvars; 5455 pb->safe_vars = nprot; 5456 pb->variables_initialized = false; 5457 pb->variables_freed = false; 5458 pb->num_eqs = 0; 5459 pb->num_geqs = 0; 5460 pb->num_subs = 0; 5461 return pb; 5462 } 5463 5464 /* Keeps the state of the initialization. */ 5465 static bool omega_initialized = false; 5466 5467 /* Initialization of the Omega solver. */ 5468 5469 void 5470 omega_initialize (void) 5471 { 5472 int i; 5473 5474 if (omega_initialized) 5475 return; 5476 5477 next_wild_card = 0; 5478 next_key = OMEGA_MAX_VARS + 1; 5479 packing = XCNEWVEC (int, OMEGA_MAX_VARS); 5480 fast_lookup = XCNEWVEC (int, MAX_KEYS * 2); 5481 fast_lookup_red = XCNEWVEC (int, MAX_KEYS * 2); 5482 hash_master = omega_alloc_eqns (0, HASH_TABLE_SIZE); 5483 5484 for (i = 0; i < HASH_TABLE_SIZE; i++) 5485 hash_master[i].touched = -1; 5486 5487 sprintf (wild_name[0], "1"); 5488 sprintf (wild_name[1], "a"); 5489 sprintf (wild_name[2], "b"); 5490 sprintf (wild_name[3], "c"); 5491 sprintf (wild_name[4], "d"); 5492 sprintf (wild_name[5], "e"); 5493 sprintf (wild_name[6], "f"); 5494 sprintf (wild_name[7], "g"); 5495 sprintf (wild_name[8], "h"); 5496 sprintf (wild_name[9], "i"); 5497 sprintf (wild_name[10], "j"); 5498 sprintf (wild_name[11], "k"); 5499 sprintf (wild_name[12], "l"); 5500 sprintf (wild_name[13], "m"); 5501 sprintf (wild_name[14], "n"); 5502 sprintf (wild_name[15], "o"); 5503 sprintf (wild_name[16], "p"); 5504 sprintf (wild_name[17], "q"); 5505 sprintf (wild_name[18], "r"); 5506 sprintf (wild_name[19], "s"); 5507 sprintf (wild_name[20], "t"); 5508 sprintf (wild_name[40 - 1], "alpha"); 5509 sprintf (wild_name[40 - 2], "beta"); 5510 sprintf (wild_name[40 - 3], "gamma"); 5511 sprintf (wild_name[40 - 4], "delta"); 5512 sprintf (wild_name[40 - 5], "tau"); 5513 sprintf (wild_name[40 - 6], "sigma"); 5514 sprintf (wild_name[40 - 7], "chi"); 5515 sprintf (wild_name[40 - 8], "omega"); 5516 sprintf (wild_name[40 - 9], "pi"); 5517 sprintf (wild_name[40 - 10], "ni"); 5518 sprintf (wild_name[40 - 11], "Alpha"); 5519 sprintf (wild_name[40 - 12], "Beta"); 5520 sprintf (wild_name[40 - 13], "Gamma"); 5521 sprintf (wild_name[40 - 14], "Delta"); 5522 sprintf (wild_name[40 - 15], "Tau"); 5523 sprintf (wild_name[40 - 16], "Sigma"); 5524 sprintf (wild_name[40 - 17], "Chi"); 5525 sprintf (wild_name[40 - 18], "Omega"); 5526 sprintf (wild_name[40 - 19], "xxx"); 5527 5528 omega_initialized = true; 5529 } 5530