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