gcc/
[official-gcc.git] / gcc / omega.c
blob321fa61d0d215be0e07b6bbab10833eb301e3af9
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.
5 This code has no license restrictions, and is considered public
6 domain.
8 Changes copyright (C) 2005-2015 Free Software Foundation, Inc.
9 Contributed by Sebastian Pop <sebastian.pop@inria.fr>
11 This file is part of GCC.
13 GCC is free software; you can redistribute it and/or modify it under
14 the terms of the GNU General Public License as published by the Free
15 Software Foundation; either version 3, or (at your option) any later
16 version.
18 GCC is distributed in the hope that it will be useful, but WITHOUT ANY
19 WARRANTY; without even the implied warranty of MERCHANTABILITY or
20 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
21 for more details.
23 You should have received a copy of the GNU General Public License
24 along with GCC; see the file COPYING3. If not see
25 <http://www.gnu.org/licenses/>. */
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
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"
51 /* When set to true, keep substitution variables. When set to false,
52 resurrect substitution variables (convert substitutions back to EQs). */
53 static bool omega_reduce_with_subs = true;
55 /* When set to true, omega_simplify_problem checks for problem with no
56 solutions, calling verify_omega_pb. */
57 static bool omega_verify_simplification = false;
59 /* When set to true, only produce a single simplified result. */
60 static bool omega_single_result = false;
62 /* Set return_single_result to 1 when omega_single_result is true. */
63 static int return_single_result = 0;
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)
68 static eqn hash_master;
69 static int next_key;
70 static int hash_version = 0;
72 /* Set to true for making the solver enter in approximation mode. */
73 static bool in_approximate_mode = false;
75 /* When set to zero, the solver is allowed to add new equalities to
76 the problem to be solved. */
77 static int conservative = 0;
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. */
81 static enum omega_result omega_found_reduction;
83 /* Set to true when the solver is allowed to add omega_red equations. */
84 static bool create_color = false;
86 /* Set to nonzero when the problem to be solved can be reduced. */
87 static int may_be_red = 0;
89 /* When false, there should be no substitution equations in the
90 simplified problem. */
91 static int please_no_equalities_in_simplified_problems = 0;
93 /* Variables names for pretty printing. */
94 static char wild_name[200][40];
96 /* Pointer to the void problem. */
97 static omega_pb no_problem = (omega_pb) 0;
99 /* Pointer to the problem to be solved. */
100 static omega_pb original_problem = (omega_pb) 0;
103 /* Return the integer A divided by B. */
105 static inline int
106 int_div (int a, int b)
108 if (a > 0)
109 return a/b;
110 else
111 return -((-a + b - 1)/b);
114 /* Return the integer A modulo B. */
116 static inline int
117 int_mod (int a, int b)
119 return a - b * int_div (a, b);
122 /* Test whether equation E is red. */
124 static inline bool
125 omega_eqn_is_red (eqn e, int desired_res)
127 return (desired_res == omega_simplify && e->color == omega_red);
130 /* Return a string for VARIABLE. */
132 static inline char *
133 omega_var_to_str (int variable)
135 if (0 <= variable && variable <= 20)
136 return wild_name[variable];
138 if (-20 < variable && variable < 0)
139 return wild_name[40 + variable];
141 /* Collapse all the entries that would have overflowed. */
142 return wild_name[21];
145 /* Return a string for variable I in problem PB. */
147 static inline char *
148 omega_variable_to_str (omega_pb pb, int i)
150 return omega_var_to_str (pb->var[i]);
153 /* Do nothing function: used for default initializations. */
155 void
156 omega_no_procedure (omega_pb pb ATTRIBUTE_UNUSED)
160 void (*omega_when_reduced) (omega_pb) = omega_no_procedure;
162 /* Print to FILE from PB equation E with all its coefficients
163 multiplied by C. */
165 static void
166 omega_print_term (FILE *file, omega_pb pb, eqn e, int c)
168 int i;
169 bool first = true;
170 int n = pb->num_vars;
171 int went_first = -1;
173 for (i = 1; i <= n; i++)
174 if (c * e->coef[i] > 0)
176 first = false;
177 went_first = i;
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;
187 for (i = 1; i <= n; i++)
188 if (i != went_first && c * e->coef[i] != 0)
190 if (!first && c * e->coef[i] > 0)
191 fprintf (file, " + ");
193 first = false;
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));
204 if (!first && c * e->coef[0] > 0)
205 fprintf (file, " + ");
207 if (first || c * e->coef[0] != 0)
208 fprintf (file, "%d", c * e->coef[0]);
211 /* Print to FILE the equation E of problem PB. */
213 void
214 omega_print_eqn (FILE *file, omega_pb pb, eqn e, bool test, int extra)
216 int i;
217 int n = pb->num_vars + extra;
218 bool is_lt = test && e->coef[0] == -1;
219 bool first;
221 if (test)
223 if (e->touched)
224 fprintf (file, "!");
226 else if (e->key != 0)
227 fprintf (file, "%d: ", e->key);
230 if (e->color == omega_red)
231 fprintf (file, "[");
233 first = true;
235 for (i = is_lt ? 1 : 0; i <= n; i++)
236 if (e->coef[i] < 0)
238 if (!first)
239 fprintf (file, " + ");
240 else
241 first = false;
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));
252 if (first)
254 if (is_lt)
256 fprintf (file, "1");
257 is_lt = false;
259 else
260 fprintf (file, "0");
263 if (test == 0)
264 fprintf (file, " = ");
265 else if (is_lt)
266 fprintf (file, " < ");
267 else
268 fprintf (file, " <= ");
270 first = true;
272 for (i = 0; i <= n; i++)
273 if (e->coef[i] > 0)
275 if (!first)
276 fprintf (file, " + ");
277 else
278 first = false;
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));
289 if (first)
290 fprintf (file, "0");
292 if (e->color == omega_red)
293 fprintf (file, "]");
296 /* Print to FILE all the variables of problem PB. */
298 static void
299 omega_print_vars (FILE *file, omega_pb pb)
301 int i;
303 fprintf (file, "variables = ");
305 if (pb->safe_vars > 0)
306 fprintf (file, "protected (");
308 for (i = 1; i <= pb->num_vars; i++)
310 fprintf (file, "%s", omega_variable_to_str (pb, i));
312 if (i == pb->safe_vars)
313 fprintf (file, ")");
315 if (i < pb->num_vars)
316 fprintf (file, ", ");
319 fprintf (file, "\n");
322 /* Dump problem PB. */
324 DEBUG_FUNCTION void
325 debug (omega_pb_d &ref)
327 omega_print_problem (stderr, &ref);
330 DEBUG_FUNCTION void
331 debug (omega_pb_d *ptr)
333 if (ptr)
334 debug (*ptr);
335 else
336 fprintf (stderr, "<nil>\n");
339 /* Debug problem PB. */
341 DEBUG_FUNCTION void
342 debug_omega_problem (omega_pb pb)
344 omega_print_problem (stderr, pb);
347 /* Print to FILE problem PB. */
349 void
350 omega_print_problem (FILE *file, omega_pb pb)
352 int e;
354 if (!pb->variables_initialized)
355 omega_initialize_variables (pb);
357 omega_print_vars (file, pb);
359 for (e = 0; e < pb->num_eqs; e++)
361 omega_print_eq (file, pb, &pb->eqs[e]);
362 fprintf (file, "\n");
365 fprintf (file, "Done with EQ\n");
367 for (e = 0; e < pb->num_geqs; e++)
369 omega_print_geq (file, pb, &pb->geqs[e]);
370 fprintf (file, "\n");
373 fprintf (file, "Done with GEQ\n");
375 for (e = 0; e < pb->num_subs; e++)
377 eqn eq = &pb->subs[e];
379 if (eq->color == omega_red)
380 fprintf (file, "[");
382 if (eq->key > 0)
383 fprintf (file, "%s := ", omega_var_to_str (eq->key));
384 else
385 fprintf (file, "#%d := ", eq->key);
387 omega_print_term (file, pb, eq, 1);
389 if (eq->color == omega_red)
390 fprintf (file, "]");
392 fprintf (file, "\n");
396 /* Return the number of equations in PB tagged omega_red. */
399 omega_count_red_equations (omega_pb pb)
401 int e, i;
402 int result = 0;
404 for (e = 0; e < pb->num_eqs; e++)
405 if (pb->eqs[e].color == omega_red)
407 for (i = pb->num_vars; i > 0; i--)
408 if (pb->geqs[e].coef[i])
409 break;
411 if (i == 0 && pb->geqs[e].coef[0] == 1)
412 return 0;
413 else
414 result += 2;
417 for (e = 0; e < pb->num_geqs; e++)
418 if (pb->geqs[e].color == omega_red)
419 result += 1;
421 for (e = 0; e < pb->num_subs; e++)
422 if (pb->subs[e].color == omega_red)
423 result += 2;
425 return result;
428 /* Print to FILE all the equations in PB that are tagged omega_red. */
430 void
431 omega_print_red_equations (FILE *file, omega_pb pb)
433 int e;
435 if (!pb->variables_initialized)
436 omega_initialize_variables (pb);
438 omega_print_vars (file, pb);
440 for (e = 0; e < pb->num_eqs; e++)
441 if (pb->eqs[e].color == omega_red)
443 omega_print_eq (file, pb, &pb->eqs[e]);
444 fprintf (file, "\n");
447 for (e = 0; e < pb->num_geqs; e++)
448 if (pb->geqs[e].color == omega_red)
450 omega_print_geq (file, pb, &pb->geqs[e]);
451 fprintf (file, "\n");
454 for (e = 0; e < pb->num_subs; e++)
455 if (pb->subs[e].color == omega_red)
457 eqn eq = &pb->subs[e];
458 fprintf (file, "[");
460 if (eq->key > 0)
461 fprintf (file, "%s := ", omega_var_to_str (eq->key));
462 else
463 fprintf (file, "#%d := ", eq->key);
465 omega_print_term (file, pb, eq, 1);
466 fprintf (file, "]\n");
470 /* Pretty print PB to FILE. */
472 void
473 omega_pretty_print_problem (FILE *file, omega_pb pb)
475 int e, v, v1, v2, v3, t;
476 bool *live = XNEWVEC (bool, OMEGA_MAX_GEQS);
477 int stuffPrinted = 0;
478 bool change;
480 typedef enum {
481 none, le, lt
482 } partial_order_type;
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;
494 if (!pb->variables_initialized)
495 omega_initialize_variables (pb);
497 if (pb->num_vars > 0)
499 omega_eliminate_redundant (pb, false);
501 for (e = 0; e < pb->num_eqs; e++)
503 if (stuffPrinted)
504 fprintf (file, "; ");
506 stuffPrinted = 1;
507 omega_print_eq (file, pb, &pb->eqs[e]);
510 for (e = 0; e < pb->num_geqs; e++)
511 live[e] = true;
513 while (1)
515 for (v = 1; v <= pb->num_vars; v++)
517 last_links[v] = first_links[v] = 0;
518 chain_length[v] = 0;
520 for (v2 = 1; v2 <= pb->num_vars; v2++)
521 po[v][v2] = none;
524 for (e = 0; e < pb->num_geqs; e++)
525 if (live[e])
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]++;
533 v1 = pb->num_vars;
535 while (v1 > 0 && pb->geqs[e].coef[v1] == 0)
536 v1--;
538 v2 = v1 - 1;
540 while (v2 > 0 && pb->geqs[e].coef[v2] == 0)
541 v2--;
543 v3 = v2 - 1;
545 while (v3 > 0 && pb->geqs[e].coef[v3] == 0)
546 v3--;
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)
552 /* Not a partial order relation. */
554 else
556 if (pb->geqs[e].coef[v1] == 1)
558 v3 = v2;
559 v2 = v1;
560 v1 = v3;
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;
568 for (v = 1; v <= pb->num_vars; v++)
569 chain_length[v] = last_links[v];
571 /* Just in case pb->num_vars <= 0. */
572 change = false;
573 for (t = 0; t < pb->num_vars; t++)
575 change = false;
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])
582 chain_length[v1] = chain_length[v2] + 1;
583 change = true;
587 /* Caught in cycle. */
588 gcc_assert (!change);
590 for (v1 = 1; v1 <= pb->num_vars; v1++)
591 if (chain_length[v1] == 0)
592 first_links[v1] = 0;
594 v = 1;
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;
601 if (chain_length[v] + first_links[v] == 0)
602 break;
604 if (stuffPrinted)
605 fprintf (file, "; ");
607 stuffPrinted = 1;
609 /* Chain starts at v. */
611 int tmp;
612 bool first = true;
614 for (e = 0; e < pb->num_geqs; e++)
615 if (live[e] && pb->geqs[e].coef[v] == 1)
617 if (!first)
618 fprintf (file, ", ");
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;
628 if (!first)
629 fprintf (file, " <= ");
632 /* Find chain. */
633 chain[0] = v;
634 m = 1;
635 while (1)
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;
642 if (v2 > pb->num_vars)
643 break;
645 chain[m++] = v2;
646 v = v2;
649 fprintf (file, "%s", omega_variable_to_str (pb, chain[0]));
651 for (multiprint = false, i = 1; i < m; i++)
653 v = chain[i - 1];
654 v2 = chain[i];
656 if (po[v][v2] == le)
657 fprintf (file, " <= ");
658 else
659 fprintf (file, " < ");
661 fprintf (file, "%s", omega_variable_to_str (pb, v2));
662 live[po_eq[v][v2]] = false;
664 if (!multiprint && i < m - 1)
665 for (v3 = 1; v3 <= pb->num_vars; v3++)
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;
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;
677 else
678 multiprint = false;
681 v = chain[m - 1];
682 /* Print last_links. */
684 int tmp;
685 bool first = true;
687 for (e = 0; e < pb->num_geqs; e++)
688 if (live[e] && pb->geqs[e].coef[v] == -1)
690 if (!first)
691 fprintf (file, ", ");
692 else
693 fprintf (file, " <= ");
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;
705 for (e = 0; e < pb->num_geqs; e++)
706 if (live[e])
708 if (stuffPrinted)
709 fprintf (file, "; ");
710 stuffPrinted = 1;
711 omega_print_geq (file, pb, &pb->geqs[e]);
714 for (e = 0; e < pb->num_subs; e++)
716 eqn eq = &pb->subs[e];
718 if (stuffPrinted)
719 fprintf (file, "; ");
721 stuffPrinted = 1;
723 if (eq->key > 0)
724 fprintf (file, "%s := ", omega_var_to_str (eq->key));
725 else
726 fprintf (file, "#%d := ", eq->key);
728 omega_print_term (file, pb, eq, 1);
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);
741 /* Assign to variable I in PB the next wildcard name. The name of a
742 wildcard is a negative number. */
743 static int next_wild_card = 0;
745 static void
746 omega_name_wild_card (omega_pb pb, int i)
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;
754 /* Return the index of the last protected (or safe) variable in PB,
755 after having added a new wildcard variable. */
757 static int
758 omega_add_new_wild_card (omega_pb pb)
760 int e;
761 int i = ++pb->safe_vars;
762 pb->num_vars++;
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)
769 /* Move "I" for all the inequalities. */
770 for (e = pb->num_geqs - 1; e >= 0; e--)
772 if (pb->geqs[e].coef[i])
773 pb->geqs[e].touched = 1;
775 pb->geqs[e].coef[pb->num_vars] = pb->geqs[e].coef[i];
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];
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];
786 /* Move the identifier. */
787 pb->var[pb->num_vars] = pb->var[i];
790 /* Initialize at zero all the coefficients */
791 for (e = pb->num_geqs - 1; e >= 0; e--)
792 pb->geqs[e].coef[i] = 0;
794 for (e = pb->num_eqs - 1; e >= 0; e--)
795 pb->eqs[e].coef[i] = 0;
797 for (e = pb->num_subs - 1; e >= 0; e--)
798 pb->subs[e].coef[i] = 0;
800 /* And give it a name. */
801 omega_name_wild_card (pb, i);
802 return i;
805 /* Delete inequality E from problem PB that has N_VARS variables. */
807 static void
808 omega_delete_geq (omega_pb pb, int e, int n_vars)
810 if (dump_file && (dump_flags & TDF_DETAILS))
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");
817 if (e < pb->num_geqs - 1)
818 omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
820 pb->num_geqs--;
823 /* Delete extra inequality E from problem PB that has N_VARS
824 variables. */
826 static void
827 omega_delete_geq_extra (omega_pb pb, int e, int n_vars)
829 if (dump_file && (dump_flags & TDF_DETAILS))
831 fprintf (dump_file, "Deleting %d: ",e);
832 omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
833 fprintf (dump_file, "\n");
836 if (e < pb->num_geqs - 1)
837 omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
839 pb->num_geqs--;
843 /* Remove variable I from problem PB. */
845 static void
846 omega_delete_variable (omega_pb pb, int i)
848 int n_vars = pb->num_vars;
849 int e;
851 if (omega_safe_var_p (pb, i))
853 int j = pb->safe_vars;
855 for (e = pb->num_geqs - 1; e >= 0; e--)
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];
862 for (e = pb->num_eqs - 1; e >= 0; e--)
864 pb->eqs[e].coef[i] = pb->eqs[e].coef[j];
865 pb->eqs[e].coef[j] = pb->eqs[e].coef[n_vars];
868 for (e = pb->num_subs - 1; e >= 0; e--)
870 pb->subs[e].coef[i] = pb->subs[e].coef[j];
871 pb->subs[e].coef[j] = pb->subs[e].coef[n_vars];
874 pb->var[i] = pb->var[j];
875 pb->var[j] = pb->var[n_vars];
877 else if (i < n_vars)
879 for (e = pb->num_geqs - 1; e >= 0; e--)
880 if (pb->geqs[e].coef[n_vars])
882 pb->geqs[e].coef[i] = pb->geqs[e].coef[n_vars];
883 pb->geqs[e].touched = 1;
886 for (e = pb->num_eqs - 1; e >= 0; e--)
887 pb->eqs[e].coef[i] = pb->eqs[e].coef[n_vars];
889 for (e = pb->num_subs - 1; e >= 0; e--)
890 pb->subs[e].coef[i] = pb->subs[e].coef[n_vars];
892 pb->var[i] = pb->var[n_vars];
895 if (omega_safe_var_p (pb, i))
896 pb->safe_vars--;
898 pb->num_vars--;
901 /* Because the coefficients of an equation are sparse, PACKING records
902 indices for non null coefficients. */
903 static int *packing;
905 /* Set up the coefficients of PACKING, following the coefficients of
906 equation EQN that has NUM_VARS variables. */
908 static inline int
909 setup_packing (eqn eqn, int num_vars)
911 int k;
912 int n = 0;
914 for (k = num_vars; k >= 0; k--)
915 if (eqn->coef[k])
916 packing[n++] = k;
918 return n;
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. */
925 static inline void
926 omega_substitute_red_1 (eqn eq, eqn sub, int var, int c, bool *found_black,
927 int top_var)
929 if (eq->coef[var] != 0)
931 if (eq->color == omega_black)
932 *found_black = true;
933 else
935 int j, k = eq->coef[var];
937 eq->coef[var] = 0;
939 for (j = top_var; j >= 0; j--)
940 eq->coef[packing[j]] -= sub->coef[packing[j]] * k * c;
945 /* Substitute in PB variable VAR with "C * SUB". */
947 static void
948 omega_substitute_red (omega_pb pb, eqn sub, int var, int c, bool *found_black)
950 int e, top_var = setup_packing (sub, pb->num_vars);
952 *found_black = false;
954 if (dump_file && (dump_flags & TDF_DETAILS))
956 if (sub->color == omega_red)
957 fprintf (dump_file, "[");
959 fprintf (dump_file, "substituting using %s := ",
960 omega_variable_to_str (pb, var));
961 omega_print_term (dump_file, pb, sub, -c);
963 if (sub->color == omega_red)
964 fprintf (dump_file, "]");
966 fprintf (dump_file, "\n");
967 omega_print_vars (dump_file, pb);
970 for (e = pb->num_eqs - 1; e >= 0; e--)
972 eqn eqn = &(pb->eqs[e]);
974 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
976 if (dump_file && (dump_flags & TDF_DETAILS))
978 omega_print_eq (dump_file, pb, eqn);
979 fprintf (dump_file, "\n");
983 for (e = pb->num_geqs - 1; e >= 0; e--)
985 eqn eqn = &(pb->geqs[e]);
987 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
989 if (eqn->coef[var] && eqn->color == omega_red)
990 eqn->touched = 1;
992 if (dump_file && (dump_flags & TDF_DETAILS))
994 omega_print_geq (dump_file, pb, eqn);
995 fprintf (dump_file, "\n");
999 for (e = pb->num_subs - 1; e >= 0; e--)
1001 eqn eqn = &(pb->subs[e]);
1003 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
1005 if (dump_file && (dump_flags & TDF_DETAILS))
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");
1013 if (dump_file && (dump_flags & TDF_DETAILS))
1014 fprintf (dump_file, "---\n\n");
1016 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1017 *found_black = true;
1020 /* Substitute in PB variable VAR with "C * SUB". */
1022 static void
1023 omega_substitute (omega_pb pb, eqn sub, int var, int c)
1025 int e, j, j0;
1026 int top_var = setup_packing (sub, pb->num_vars);
1028 if (dump_file && (dump_flags & TDF_DETAILS))
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);
1037 if (top_var < 0)
1039 for (e = pb->num_eqs - 1; e >= 0; e--)
1040 pb->eqs[e].coef[var] = 0;
1042 for (e = pb->num_geqs - 1; e >= 0; e--)
1043 if (pb->geqs[e].coef[var] != 0)
1045 pb->geqs[e].touched = 1;
1046 pb->geqs[e].coef[var] = 0;
1049 for (e = pb->num_subs - 1; e >= 0; e--)
1050 pb->subs[e].coef[var] = 0;
1052 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1054 int k;
1055 eqn eqn = &(pb->subs[pb->num_subs++]);
1057 for (k = pb->num_vars; k >= 0; k--)
1058 eqn->coef[k] = 0;
1060 eqn->key = pb->var[var];
1061 eqn->color = omega_black;
1064 else if (top_var == 0 && packing[0] == 0)
1066 c = -sub->coef[0] * c;
1068 for (e = pb->num_eqs - 1; e >= 0; e--)
1070 pb->eqs[e].coef[0] += pb->eqs[e].coef[var] * c;
1071 pb->eqs[e].coef[var] = 0;
1074 for (e = pb->num_geqs - 1; e >= 0; e--)
1075 if (pb->geqs[e].coef[var] != 0)
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;
1082 for (e = pb->num_subs - 1; e >= 0; e--)
1084 pb->subs[e].coef[0] += pb->subs[e].coef[var] * c;
1085 pb->subs[e].coef[var] = 0;
1088 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1090 int k;
1091 eqn eqn = &(pb->subs[pb->num_subs++]);
1093 for (k = pb->num_vars; k >= 1; k--)
1094 eqn->coef[k] = 0;
1096 eqn->coef[0] = c;
1097 eqn->key = pb->var[var];
1098 eqn->color = omega_black;
1101 if (dump_file && (dump_flags & TDF_DETAILS))
1103 fprintf (dump_file, "---\n\n");
1104 omega_print_problem (dump_file, pb);
1105 fprintf (dump_file, "===\n\n");
1108 else
1110 for (e = pb->num_eqs - 1; e >= 0; e--)
1112 eqn eqn = &(pb->eqs[e]);
1113 int k = eqn->coef[var];
1115 if (k != 0)
1117 k = c * k;
1118 eqn->coef[var] = 0;
1120 for (j = top_var; j >= 0; j--)
1122 j0 = packing[j];
1123 eqn->coef[j0] -= sub->coef[j0] * k;
1127 if (dump_file && (dump_flags & TDF_DETAILS))
1129 omega_print_eq (dump_file, pb, eqn);
1130 fprintf (dump_file, "\n");
1134 for (e = pb->num_geqs - 1; e >= 0; e--)
1136 eqn eqn = &(pb->geqs[e]);
1137 int k = eqn->coef[var];
1139 if (k != 0)
1141 k = c * k;
1142 eqn->touched = 1;
1143 eqn->coef[var] = 0;
1145 for (j = top_var; j >= 0; j--)
1147 j0 = packing[j];
1148 eqn->coef[j0] -= sub->coef[j0] * k;
1152 if (dump_file && (dump_flags & TDF_DETAILS))
1154 omega_print_geq (dump_file, pb, eqn);
1155 fprintf (dump_file, "\n");
1159 for (e = pb->num_subs - 1; e >= 0; e--)
1161 eqn eqn = &(pb->subs[e]);
1162 int k = eqn->coef[var];
1164 if (k != 0)
1166 k = c * k;
1167 eqn->coef[var] = 0;
1169 for (j = top_var; j >= 0; j--)
1171 j0 = packing[j];
1172 eqn->coef[j0] -= sub->coef[j0] * k;
1176 if (dump_file && (dump_flags & TDF_DETAILS))
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");
1184 if (dump_file && (dump_flags & TDF_DETAILS))
1186 fprintf (dump_file, "---\n\n");
1187 omega_print_problem (dump_file, pb);
1188 fprintf (dump_file, "===\n\n");
1191 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1193 int k;
1194 eqn eqn = &(pb->subs[pb->num_subs++]);
1195 c = -c;
1197 for (k = pb->num_vars; k >= 0; k--)
1198 eqn->coef[k] = c * (sub->coef[k]);
1200 eqn->key = pb->var[var];
1201 eqn->color = sub->color;
1206 /* Solve e = factor alpha for x_j and substitute. */
1208 static void
1209 omega_do_mod (omega_pb pb, int factor, int e, int j)
1211 int k, i;
1212 eqn eq = omega_alloc_eqns (0, 1);
1213 int nfactor;
1214 bool kill_j = false;
1216 omega_copy_eqn (eq, &pb->eqs[e], pb->num_vars);
1218 for (k = pb->num_vars; k >= 0; k--)
1220 eq->coef[k] = int_mod (eq->coef[k], factor);
1222 if (2 * eq->coef[k] >= factor)
1223 eq->coef[k] -= factor;
1226 nfactor = eq->coef[j];
1228 if (omega_safe_var_p (pb, j) && !omega_wildcard_p (pb, j))
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;
1236 else
1238 eq->coef[j] = -factor;
1239 if (!omega_wildcard_p (pb, j))
1240 omega_name_wild_card (pb, j);
1243 omega_substitute (pb, eq, j, nfactor);
1245 for (k = pb->num_vars; k >= 0; k--)
1246 pb->eqs[e].coef[k] = pb->eqs[e].coef[k] / factor;
1248 if (kill_j)
1249 omega_delete_variable (pb, j);
1251 if (dump_file && (dump_flags & TDF_DETAILS))
1253 fprintf (dump_file, "Mod-ing and normalizing produces:\n");
1254 omega_print_problem (dump_file, pb);
1257 omega_free_eqns (eq, 1);
1260 /* Multiplies by -1 inequality E. */
1262 void
1263 omega_negate_geq (omega_pb pb, int e)
1265 int i;
1267 for (i = pb->num_vars; i >= 0; i--)
1268 pb->geqs[e].coef[i] *= -1;
1270 pb->geqs[e].coef[0]--;
1271 pb->geqs[e].touched = 1;
1274 /* Returns OMEGA_TRUE when problem PB has a solution. */
1276 static enum omega_result
1277 verify_omega_pb (omega_pb pb)
1279 enum omega_result result;
1280 int e;
1281 bool any_color = false;
1282 omega_pb tmp_problem = XNEW (struct omega_pb_d);
1284 omega_copy_problem (tmp_problem, pb);
1285 tmp_problem->safe_vars = 0;
1286 tmp_problem->num_subs = 0;
1288 for (e = pb->num_geqs - 1; e >= 0; e--)
1289 if (pb->geqs[e].color == omega_red)
1291 any_color = true;
1292 break;
1295 if (please_no_equalities_in_simplified_problems)
1296 any_color = true;
1298 if (any_color)
1299 original_problem = no_problem;
1300 else
1301 original_problem = pb;
1303 if (dump_file && (dump_flags & TDF_DETAILS))
1305 fprintf (dump_file, "verifying problem");
1307 if (any_color)
1308 fprintf (dump_file, " (color mode)");
1310 fprintf (dump_file, " :\n");
1311 omega_print_problem (dump_file, pb);
1314 result = omega_solve_problem (tmp_problem, omega_unknown);
1315 original_problem = no_problem;
1316 free (tmp_problem);
1318 if (dump_file && (dump_flags & TDF_DETAILS))
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);
1327 return result;
1330 /* Add a new equality to problem PB at last position E. */
1332 static void
1333 adding_equality_constraint (omega_pb pb, int e)
1335 if (original_problem != no_problem
1336 && original_problem != pb
1337 && !conservative)
1339 int i, j;
1340 int e2 = original_problem->num_eqs++;
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);
1348 for (i = pb->num_vars; i >= 1; i--)
1350 for (j = original_problem->num_vars; j >= 1; j--)
1351 if (original_problem->var[j] == pb->var[i])
1352 break;
1354 if (j <= 0)
1356 if (dump_file && (dump_flags & TDF_DETAILS))
1357 fprintf (dump_file, "retracting\n");
1358 original_problem->num_eqs--;
1359 return;
1361 original_problem->eqs[e2].coef[j] = pb->eqs[e].coef[i];
1364 original_problem->eqs[e2].coef[0] = pb->eqs[e].coef[0];
1366 if (dump_file && (dump_flags & TDF_DETAILS))
1367 omega_print_problem (dump_file, original_problem);
1371 static int *fast_lookup;
1372 static int *fast_lookup_red;
1374 typedef enum {
1375 normalize_false,
1376 normalize_uncoupled,
1377 normalize_coupled
1378 } normalize_return_type;
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. */
1384 static normalize_return_type
1385 normalize_omega_problem (omega_pb pb)
1387 int e, i, j, k, n_vars;
1388 int coupled_subscripts = 0;
1390 n_vars = pb->num_vars;
1392 for (e = 0; e < pb->num_geqs; e++)
1394 if (!pb->geqs[e].touched)
1396 if (!single_var_geq (&pb->geqs[e], n_vars))
1397 coupled_subscripts = 1;
1399 else
1401 int g, top_var, i0, hashCode;
1402 int *p = &packing[0];
1404 for (k = 1; k <= n_vars; k++)
1405 if (pb->geqs[e].coef[k])
1406 *(p++) = k;
1408 top_var = (p - &packing[0]) - 1;
1410 if (top_var == -1)
1412 if (pb->geqs[e].coef[0] < 0)
1414 if (dump_file && (dump_flags & TDF_DETAILS))
1416 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1417 fprintf (dump_file, "\nequations have no solution \n");
1419 return normalize_false;
1422 omega_delete_geq (pb, e, n_vars);
1423 e--;
1424 continue;
1426 else if (top_var == 0)
1428 int singlevar = packing[0];
1430 g = pb->geqs[e].coef[singlevar];
1432 if (g > 0)
1434 pb->geqs[e].coef[singlevar] = 1;
1435 pb->geqs[e].key = singlevar;
1437 else
1439 g = -g;
1440 pb->geqs[e].coef[singlevar] = -1;
1441 pb->geqs[e].key = -singlevar;
1444 if (g > 1)
1445 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1447 else
1449 int g2;
1450 int hash_key_multiplier = 31;
1452 coupled_subscripts = 1;
1453 i0 = top_var;
1454 i = packing[i0--];
1455 g = pb->geqs[e].coef[i];
1456 hashCode = g * (i + 3);
1458 if (g < 0)
1459 g = -g;
1461 for (; i0 >= 0; i0--)
1463 int x;
1465 i = packing[i0];
1466 x = pb->geqs[e].coef[i];
1467 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1469 if (x < 0)
1470 x = -x;
1472 if (x == 1)
1474 g = 1;
1475 i0--;
1476 break;
1478 else
1479 g = gcd (x, g);
1482 for (; i0 >= 0; i0--)
1484 int x;
1485 i = packing[i0];
1486 x = pb->geqs[e].coef[i];
1487 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1490 if (g > 1)
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);
1498 for (; i0 >= 0; i0--)
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];
1507 g2 = abs (hashCode);
1509 if (dump_file && (dump_flags & TDF_DETAILS))
1511 fprintf (dump_file, "Hash code = %d, eqn = ", hashCode);
1512 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1513 fprintf (dump_file, "\n");
1516 j = g2 % HASH_TABLE_SIZE;
1518 do {
1519 eqn proto = &(hash_master[j]);
1521 if (proto->touched == g2)
1523 if (proto->coef[0] == top_var)
1525 if (hashCode >= 0)
1526 for (i0 = top_var; i0 >= 0; i0--)
1528 i = packing[i0];
1530 if (pb->geqs[e].coef[i] != proto->coef[i])
1531 break;
1533 else
1534 for (i0 = top_var; i0 >= 0; i0--)
1536 i = packing[i0];
1538 if (pb->geqs[e].coef[i] != -proto->coef[i])
1539 break;
1542 if (i0 < 0)
1544 if (hashCode >= 0)
1545 pb->geqs[e].key = proto->key;
1546 else
1547 pb->geqs[e].key = -proto->key;
1548 break;
1552 else if (proto->touched < 0)
1554 omega_init_eqn_zero (proto, pb->num_vars);
1555 if (hashCode >= 0)
1556 for (i0 = top_var; i0 >= 0; i0--)
1558 i = packing[i0];
1559 proto->coef[i] = pb->geqs[e].coef[i];
1561 else
1562 for (i0 = top_var; i0 >= 0; i0--)
1564 i = packing[i0];
1565 proto->coef[i] = -pb->geqs[e].coef[i];
1568 proto->coef[0] = top_var;
1569 proto->touched = g2;
1571 if (dump_file && (dump_flags & TDF_DETAILS))
1572 fprintf (dump_file, " constraint key = %d\n",
1573 next_key);
1575 proto->key = next_key++;
1577 /* Too many hash keys generated. */
1578 gcc_assert (proto->key <= MAX_KEYS);
1580 if (hashCode >= 0)
1581 pb->geqs[e].key = proto->key;
1582 else
1583 pb->geqs[e].key = -proto->key;
1585 break;
1588 j = (j + 1) % HASH_TABLE_SIZE;
1589 } while (1);
1592 pb->geqs[e].touched = 0;
1596 int eKey = pb->geqs[e].key;
1597 int e2;
1598 if (e > 0)
1600 int cTerm = pb->geqs[e].coef[0];
1601 e2 = fast_lookup[MAX_KEYS - eKey];
1603 if (e2 < e && pb->geqs[e2].key == -eKey
1604 && pb->geqs[e2].color == omega_black)
1606 if (pb->geqs[e2].coef[0] < -cTerm)
1608 if (dump_file && (dump_flags & TDF_DETAILS))
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");
1616 return normalize_false;
1619 if (pb->geqs[e2].coef[0] == -cTerm
1620 && (create_color
1621 || pb->geqs[e].color == omega_black))
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);
1632 e2 = fast_lookup_red[MAX_KEYS - eKey];
1634 if (e2 < e && pb->geqs[e2].key == -eKey
1635 && pb->geqs[e2].color == omega_red)
1637 if (pb->geqs[e2].coef[0] < -cTerm)
1639 if (dump_file && (dump_flags & TDF_DETAILS))
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");
1647 return normalize_false;
1650 if (pb->geqs[e2].coef[0] == -cTerm && create_color)
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);
1660 e2 = fast_lookup[MAX_KEYS + eKey];
1662 if (e2 < e && pb->geqs[e2].key == eKey
1663 && pb->geqs[e2].color == omega_black)
1665 if (pb->geqs[e2].coef[0] > cTerm)
1667 if (pb->geqs[e].color == omega_black)
1669 if (dump_file && (dump_flags & TDF_DETAILS))
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");
1680 pb->geqs[e2].coef[0] = cTerm;
1681 omega_delete_geq (pb, e, n_vars);
1682 e--;
1683 continue;
1686 else
1688 if (dump_file && (dump_flags & TDF_DETAILS))
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");
1697 omega_delete_geq (pb, e, n_vars);
1698 e--;
1699 continue;
1703 e2 = fast_lookup_red[MAX_KEYS + eKey];
1705 if (e2 < e && pb->geqs[e2].key == eKey
1706 && pb->geqs[e2].color == omega_red)
1708 if (pb->geqs[e2].coef[0] >= cTerm)
1710 if (dump_file && (dump_flags & TDF_DETAILS))
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");
1719 pb->geqs[e2].coef[0] = cTerm;
1720 pb->geqs[e2].color = pb->geqs[e].color;
1722 else if (pb->geqs[e].color == omega_red)
1724 if (dump_file && (dump_flags & TDF_DETAILS))
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");
1734 omega_delete_geq (pb, e, n_vars);
1735 e--;
1736 continue;
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;
1748 create_color = false;
1749 return coupled_subscripts ? normalize_coupled : normalize_uncoupled;
1752 /* Divide the coefficients of EQN by their gcd. N_VARS is the number
1753 of variables in EQN. */
1755 static inline void
1756 divide_eqn_by_gcd (eqn eqn, int n_vars)
1758 int var, g = 0;
1760 for (var = n_vars; var >= 0; var--)
1761 g = gcd (abs (eqn->coef[var]), g);
1763 if (g)
1764 for (var = n_vars; var >= 0; var--)
1765 eqn->coef[var] = eqn->coef[var] / g;
1768 /* Rewrite some non-safe variables in function of protected
1769 wildcard variables. */
1771 static void
1772 cleanout_wildcards (omega_pb pb)
1774 int e, i, j;
1775 int n_vars = pb->num_vars;
1776 bool renormalize = false;
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)
1782 /* i is the last nonzero non-safe variable. */
1784 for (j = i - 1; !omega_safe_var_p (pb, j); j--)
1785 if (pb->eqs[e].coef[j] != 0)
1786 break;
1788 /* j is the next nonzero non-safe variable, or points
1789 to a safe variable: it is then a wildcard variable. */
1791 /* Clean it out. */
1792 if (omega_safe_var_p (pb, j))
1794 eqn sub = &(pb->eqs[e]);
1795 int c = pb->eqs[e].coef[i];
1796 int a = abs (c);
1797 int e2;
1799 if (dump_file && (dump_flags & TDF_DETAILS))
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);
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)))
1814 eqn eqn = &(pb->eqs[e2]);
1815 int var, k;
1817 for (var = n_vars; var >= 0; var--)
1818 eqn->coef[var] *= a;
1820 k = eqn->coef[i];
1822 for (var = n_vars; var >= 0; var--)
1823 eqn->coef[var] -= sub->coef[var] * k / c;
1825 eqn->coef[i] = 0;
1826 divide_eqn_by_gcd (eqn, n_vars);
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)))
1835 eqn eqn = &(pb->geqs[e2]);
1836 int var, k;
1838 for (var = n_vars; var >= 0; var--)
1839 eqn->coef[var] *= a;
1841 k = eqn->coef[i];
1843 for (var = n_vars; var >= 0; var--)
1844 eqn->coef[var] -= sub->coef[var] * k / c;
1846 eqn->coef[i] = 0;
1847 eqn->touched = 1;
1848 renormalize = true;
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)))
1857 eqn eqn = &(pb->subs[e2]);
1858 int var, k;
1860 for (var = n_vars; var >= 0; var--)
1861 eqn->coef[var] *= a;
1863 k = eqn->coef[i];
1865 for (var = n_vars; var >= 0; var--)
1866 eqn->coef[var] -= sub->coef[var] * k / c;
1868 eqn->coef[i] = 0;
1869 divide_eqn_by_gcd (eqn, n_vars);
1872 if (dump_file && (dump_flags & TDF_DETAILS))
1874 fprintf (dump_file, "cleaned-out wildcard: ");
1875 omega_print_problem (dump_file, pb);
1877 break;
1881 if (renormalize)
1882 normalize_omega_problem (pb);
1885 /* Swap values contained in I and J. */
1887 static inline void
1888 swap (int *i, int *j)
1890 int tmp;
1891 tmp = *i;
1892 *i = *j;
1893 *j = tmp;
1896 /* Swap values contained in I and J. */
1898 static inline void
1899 bswap (bool *i, bool *j)
1901 bool tmp;
1902 tmp = *i;
1903 *i = *j;
1904 *j = tmp;
1907 /* Make variable IDX unprotected in PB, by swapping its index at the
1908 PB->safe_vars rank. */
1910 static inline void
1911 omega_unprotect_1 (omega_pb pb, int *idx, bool *unprotect)
1913 /* If IDX is protected... */
1914 if (*idx < pb->safe_vars)
1916 /* ... swap its index with the last non protected index. */
1917 int j = pb->safe_vars;
1918 int e;
1920 for (e = pb->num_geqs - 1; e >= 0; e--)
1922 pb->geqs[e].touched = 1;
1923 swap (&pb->geqs[e].coef[*idx], &pb->geqs[e].coef[j]);
1926 for (e = pb->num_eqs - 1; e >= 0; e--)
1927 swap (&pb->eqs[e].coef[*idx], &pb->eqs[e].coef[j]);
1929 for (e = pb->num_subs - 1; e >= 0; e--)
1930 swap (&pb->subs[e].coef[*idx], &pb->subs[e].coef[j]);
1932 if (unprotect)
1933 bswap (&unprotect[*idx], &unprotect[j]);
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)--;
1941 /* The variable at pb->safe_vars is also unprotected now. */
1942 pb->safe_vars--;
1945 /* During the Fourier-Motzkin elimination some variables are
1946 substituted with other variables. This function resurrects the
1947 substituted variables in PB. */
1949 static void
1950 resurrect_subs (omega_pb pb)
1952 if (pb->num_subs > 0
1953 && please_no_equalities_in_simplified_problems == 0)
1955 int i, e, m;
1957 if (dump_file && (dump_flags & TDF_DETAILS))
1959 fprintf (dump_file,
1960 "problem reduced, bringing variables back to life\n");
1961 omega_print_problem (dump_file, pb);
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);
1968 m = pb->num_subs;
1970 for (e = pb->num_geqs - 1; e >= 0; e--)
1971 if (single_var_geq (&pb->geqs[e], pb->num_vars))
1973 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
1974 pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m);
1976 else
1978 pb->geqs[e].touched = 1;
1979 pb->geqs[e].key = 0;
1982 for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--)
1984 pb->var[i + m] = pb->var[i];
1986 for (e = pb->num_geqs - 1; e >= 0; e--)
1987 pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i];
1989 for (e = pb->num_eqs - 1; e >= 0; e--)
1990 pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i];
1992 for (e = pb->num_subs - 1; e >= 0; e--)
1993 pb->subs[e].coef[i + m] = pb->subs[e].coef[i];
1996 for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--)
1998 for (e = pb->num_geqs - 1; e >= 0; e--)
1999 pb->geqs[e].coef[i] = 0;
2001 for (e = pb->num_eqs - 1; e >= 0; e--)
2002 pb->eqs[e].coef[i] = 0;
2004 for (e = pb->num_subs - 1; e >= 0; e--)
2005 pb->subs[e].coef[i] = 0;
2008 pb->num_vars += m;
2010 for (e = pb->num_subs - 1; e >= 0; e--)
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;
2018 if (dump_file && (dump_flags & TDF_DETAILS))
2020 fprintf (dump_file, "brought back: ");
2021 omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]);
2022 fprintf (dump_file, "\n");
2025 pb->num_eqs++;
2026 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2029 pb->safe_vars += m;
2030 pb->num_subs = 0;
2032 if (dump_file && (dump_flags & TDF_DETAILS))
2034 fprintf (dump_file, "variables brought back to life\n");
2035 omega_print_problem (dump_file, pb);
2038 cleanout_wildcards (pb);
2042 static inline bool
2043 implies (unsigned int a, unsigned int b)
2045 return (a == (a & b));
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. */
2052 enum omega_result
2053 omega_eliminate_redundant (omega_pb pb, bool expensive)
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;
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);
2064 /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
2065 unsigned int pp, pz, pn;
2067 if (dump_file && (dump_flags & TDF_DETAILS))
2069 fprintf (dump_file, "in eliminate Redundant:\n");
2070 omega_print_problem (dump_file, pb);
2073 for (e = pb->num_geqs - 1; e >= 0; e--)
2075 int tmp = 1;
2077 is_dead[e] = false;
2078 peqs[e] = zeqs[e] = neqs[e] = 0;
2080 for (i = pb->num_vars; i >= 1; i--)
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;
2089 tmp <<= 1;
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])
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;
2105 continue;
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];
2113 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2114 if (e3 != e1 && e3 != e2)
2116 if (!implies (zeqs[e3], pz))
2117 goto nextE3;
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;
2125 if (alpha1 * alpha2 <= 0)
2126 goto nextE3;
2128 if (alpha1 < 0)
2130 alpha1 = -alpha1;
2131 alpha2 = -alpha2;
2132 alpha3 = -alpha3;
2135 if (alpha3 > 0)
2137 /* Trying to prove e3 is redundant. */
2138 if (!implies (peqs[e3], pp)
2139 || !implies (neqs[e3], pn))
2140 goto nextE3;
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;
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;
2153 c = (alpha1 * pb->geqs[e1].coef[0]
2154 + alpha2 * pb->geqs[e2].coef[0]);
2156 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2158 if (dump_file && (dump_flags & TDF_DETAILS))
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);
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");
2174 is_dead[e3] = true;
2177 else
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;
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;
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;
2198 c = (alpha1 * pb->geqs[e1].coef[0]
2199 + alpha2 * pb->geqs[e2].coef[0]);
2201 if (c < alpha3 * (pb->geqs[e3].coef[0]))
2203 /* We just proved e3 < 0, so no solutions exist. */
2204 if (dump_file && (dump_flags & TDF_DETAILS))
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");
2218 free (is_dead);
2219 free (peqs);
2220 free (zeqs);
2221 free (neqs);
2222 return omega_false;
2224 else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
2226 /* We just proved that e3 <=0, so e3 = 0. */
2227 if (dump_file && (dump_flags & TDF_DETAILS))
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");
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;
2249 nextE3:;
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);
2258 if (!expensive)
2259 goto eliminate_redundant_done;
2261 tmp_problem = XNEW (struct omega_pb_d);
2262 conservative++;
2264 for (e = pb->num_geqs - 1; e >= 0; e--)
2266 if (dump_file && (dump_flags & TDF_DETAILS))
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");
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;
2279 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2280 omega_delete_geq (pb, e, pb->num_vars);
2283 free (tmp_problem);
2284 conservative--;
2286 if (!omega_reduce_with_subs)
2288 resurrect_subs (pb);
2289 gcc_assert (please_no_equalities_in_simplified_problems
2290 || pb->num_subs == 0);
2293 eliminate_redundant_done:
2294 free (is_dead);
2295 free (peqs);
2296 free (zeqs);
2297 free (neqs);
2298 return omega_true;
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. */
2307 static int
2308 smooth_weird_equations (omega_pb pb)
2310 int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
2311 int c;
2312 int v;
2313 int result = 0;
2315 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2316 if (pb->geqs[e1].color == omega_black)
2318 int g = 999999;
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]);
2324 /* Magic number. */
2325 if (g > 20)
2327 e3 = pb->num_geqs;
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,
2333 pb->geqs[e3].color = omega_black;
2334 pb->geqs[e3].touched = 1;
2335 /* Magic number. */
2336 pb->geqs[e3].coef[0] = 9997;
2338 if (dump_file && (dump_flags & TDF_DETAILS))
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");
2347 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
2348 if (e1 != e2 && pb->geqs[e2].color == omega_black)
2350 for (p = pb->num_vars; p > 1; p--)
2352 for (q = p - 1; q > 0; q--)
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;
2361 continue;
2363 foundPQ:
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;
2371 if (alpha1 * alpha2 <= 0)
2372 continue;
2374 if (alpha1 < 0)
2376 alpha1 = -alpha1;
2377 alpha2 = -alpha2;
2378 alpha3 = -alpha3;
2381 if (alpha3 > 0)
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;
2391 c = alpha1 * pb->geqs[e1].coef[0]
2392 + alpha2 * pb->geqs[e2].coef[0];
2394 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2395 pb->geqs[e3].coef[0] = int_div (c, alpha3);
2397 nextE2:;
2400 if (pb->geqs[e3].coef[0] < 9997)
2402 result++;
2403 pb->num_geqs++;
2405 if (dump_file && (dump_flags & TDF_DETAILS))
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");
2417 return result;
2420 /* Replace tuples of inequalities, that define upper and lower half
2421 spaces, with an equation. */
2423 static void
2424 coalesce (omega_pb pb)
2426 int e, e2;
2427 int colors = 0;
2428 bool *is_dead;
2429 int found_something = 0;
2431 for (e = 0; e < pb->num_geqs; e++)
2432 if (pb->geqs[e].color == omega_red)
2433 colors++;
2435 if (colors < 2)
2436 return;
2438 is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2440 for (e = 0; e < pb->num_geqs; e++)
2441 is_dead[e] = false;
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)
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;
2460 for (e = pb->num_geqs - 1; e >= 0; e--)
2461 if (is_dead[e])
2462 omega_delete_geq (pb, e, pb->num_vars);
2464 if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
2466 fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
2467 found_something);
2468 omega_print_problem (dump_file, pb);
2471 free (is_dead);
2474 /* Eliminate red inequalities from PB. When ELIMINATE_ALL is
2475 true, continue to eliminate all the red inequalities. */
2477 void
2478 omega_eliminate_red (omega_pb pb, bool eliminate_all)
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;
2487 if (dump_file && (dump_flags & TDF_DETAILS))
2489 fprintf (dump_file, "in eliminate RED:\n");
2490 omega_print_problem (dump_file, pb);
2493 if (pb->num_eqs > 0)
2494 omega_simplify_problem (pb);
2496 for (e = pb->num_geqs - 1; e >= 0; e--)
2497 is_dead[e] = false;
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])
2505 a = 0;
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;
2513 continue;
2515 found_pair:
2516 if (dump_file && (dump_flags & TDF_DETAILS))
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");
2529 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2530 if (pb->geqs[e3].color == omega_red)
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]);
2537 if ((a > 0 && alpha1 > 0 && alpha2 > 0)
2538 || (a < 0 && alpha1 < 0 && alpha2 < 0))
2540 if (dump_file && (dump_flags & TDF_DETAILS))
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");
2550 for (k = pb->num_vars; k >= 0; k--)
2552 c = (alpha1 * pb->geqs[e].coef[k]
2553 + alpha2 * pb->geqs[e2].coef[k]);
2555 if (c != a * pb->geqs[e3].coef[k])
2556 break;
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]);
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]))))
2569 if (dump_file && (dump_flags & TDF_DETAILS))
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");
2584 is_dead[e3] = true;
2590 for (e = pb->num_geqs - 1; e >= 0; e--)
2591 if (is_dead[e])
2592 omega_delete_geq (pb, e, pb->num_vars);
2594 free (is_dead);
2596 if (dump_file && (dump_flags & TDF_DETAILS))
2598 fprintf (dump_file, "in eliminate RED, easy tests done:\n");
2599 omega_print_problem (dump_file, pb);
2602 for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
2603 if (pb->geqs[e].color == omega_red)
2605 red_found = 1;
2606 break;
2609 if (!red_found)
2611 if (dump_file && (dump_flags & TDF_DETAILS))
2612 fprintf (dump_file, "fast checks worked\n");
2614 if (!omega_reduce_with_subs)
2615 gcc_assert (please_no_equalities_in_simplified_problems
2616 || pb->num_subs == 0);
2618 return;
2621 if (!omega_verify_simplification
2622 && verify_omega_pb (pb) == omega_false)
2623 return;
2625 conservative++;
2626 tmp_problem = XNEW (struct omega_pb_d);
2628 for (e = pb->num_geqs - 1; e >= 0; e--)
2629 if (pb->geqs[e].color == omega_red)
2631 if (dump_file && (dump_flags & TDF_DETAILS))
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");
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;
2645 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
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);
2651 else
2653 if (dump_file && (dump_flags & TDF_DETAILS))
2654 fprintf (dump_file, "it is not redundant\n");
2656 if (!eliminate_all)
2658 if (dump_file && (dump_flags & TDF_DETAILS))
2659 fprintf (dump_file, "no need to check other red equations\n");
2660 break;
2665 conservative--;
2666 free (tmp_problem);
2667 /* omega_simplify_problem (pb); */
2669 if (!omega_reduce_with_subs)
2670 gcc_assert (please_no_equalities_in_simplified_problems
2671 || pb->num_subs == 0);
2674 /* Transform some wildcard variables to non-safe variables. */
2676 static void
2677 chain_unprotect (omega_pb pb)
2679 int i, e;
2680 bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
2682 for (i = 1; omega_safe_var_p (pb, i); i++)
2684 unprotect[i] = omega_wildcard_p (pb, i);
2686 for (e = pb->num_subs - 1; e >= 0; e--)
2687 if (pb->subs[e].coef[i])
2688 unprotect[i] = false;
2691 if (dump_file && (dump_flags & TDF_DETAILS))
2693 fprintf (dump_file, "Doing chain reaction unprotection\n");
2694 omega_print_problem (dump_file, pb);
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));
2702 for (i = 1; omega_safe_var_p (pb, i); i++)
2703 if (unprotect[i])
2704 omega_unprotect_1 (pb, &i, unprotect);
2706 if (dump_file && (dump_flags & TDF_DETAILS))
2708 fprintf (dump_file, "After chain reactions\n");
2709 omega_print_problem (dump_file, pb);
2712 free (unprotect);
2715 /* Reduce problem PB. */
2717 static void
2718 omega_problem_reduced (omega_pb pb)
2720 if (omega_verify_simplification
2721 && !in_approximate_mode
2722 && verify_omega_pb (pb) == omega_false)
2723 return;
2725 if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
2726 && !omega_eliminate_redundant (pb, true))
2727 return;
2729 omega_found_reduction = omega_true;
2731 if (!please_no_equalities_in_simplified_problems)
2732 coalesce (pb);
2734 if (omega_reduce_with_subs
2735 || please_no_equalities_in_simplified_problems)
2736 chain_unprotect (pb);
2737 else
2738 resurrect_subs (pb);
2740 if (!return_single_result)
2742 int i;
2744 for (i = 1; omega_safe_var_p (pb, i); i++)
2745 pb->forwarding_address[pb->var[i]] = i;
2747 for (i = 0; i < pb->num_subs; i++)
2748 pb->forwarding_address[pb->subs[i].key] = -i - 1;
2750 (*omega_when_reduced) (pb);
2753 if (dump_file && (dump_flags & TDF_DETAILS))
2755 fprintf (dump_file, "-------------------------------------------\n");
2756 fprintf (dump_file, "problem reduced:\n");
2757 omega_print_problem (dump_file, pb);
2758 fprintf (dump_file, "-------------------------------------------\n");
2762 /* Eliminates all the free variables for problem PB, that is all the
2763 variables from FV to PB->NUM_VARS. */
2765 static void
2766 omega_free_eliminations (omega_pb pb, int fv)
2768 bool try_again = true;
2769 int i, e, e2;
2770 int n_vars = pb->num_vars;
2772 while (try_again)
2774 try_again = false;
2776 for (i = n_vars; i > fv; i--)
2778 for (e = pb->num_geqs - 1; e >= 0; e--)
2779 if (pb->geqs[e].coef[i])
2780 break;
2782 if (e < 0)
2783 e2 = e;
2784 else if (pb->geqs[e].coef[i] > 0)
2786 for (e2 = e - 1; e2 >= 0; e2--)
2787 if (pb->geqs[e2].coef[i] < 0)
2788 break;
2790 else
2792 for (e2 = e - 1; e2 >= 0; e2--)
2793 if (pb->geqs[e2].coef[i] > 0)
2794 break;
2797 if (e2 < 0)
2799 int e3;
2800 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2801 if (pb->subs[e3].coef[i])
2802 break;
2804 if (e3 >= 0)
2805 continue;
2807 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2808 if (pb->eqs[e3].coef[i])
2809 break;
2811 if (e3 >= 0)
2812 continue;
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));
2818 if (e >= 0)
2820 omega_delete_geq (pb, e, n_vars);
2822 for (e--; e >= 0; e--)
2823 if (pb->geqs[e].coef[i])
2824 omega_delete_geq (pb, e, n_vars);
2826 try_again = (i < n_vars);
2829 omega_delete_variable (pb, i);
2830 n_vars = pb->num_vars;
2835 if (dump_file && (dump_flags & TDF_DETAILS))
2837 fprintf (dump_file, "\nafter free eliminations:\n");
2838 omega_print_problem (dump_file, pb);
2839 fprintf (dump_file, "\n");
2843 /* Do free red eliminations. */
2845 static void
2846 free_red_eliminations (omega_pb pb)
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);
2855 for (i = n_vars; i > 0; i--)
2857 is_red_var[i] = false;
2858 is_dead_var[i] = false;
2861 for (e = pb->num_geqs - 1; e >= 0; e--)
2863 is_dead_geq[e] = false;
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;
2871 while (try_again)
2873 try_again = false;
2874 for (i = n_vars; i > 0; i--)
2875 if (!is_red_var[i] && !is_dead_var[i])
2877 for (e = pb->num_geqs - 1; e >= 0; e--)
2878 if (!is_dead_geq[e] && pb->geqs[e].coef[i])
2879 break;
2881 if (e < 0)
2882 e2 = e;
2883 else if (pb->geqs[e].coef[i] > 0)
2885 for (e2 = e - 1; e2 >= 0; e2--)
2886 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
2887 break;
2889 else
2891 for (e2 = e - 1; e2 >= 0; e2--)
2892 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
2893 break;
2896 if (e2 < 0)
2898 int e3;
2899 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2900 if (pb->subs[e3].coef[i])
2901 break;
2903 if (e3 >= 0)
2904 continue;
2906 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2907 if (pb->eqs[e3].coef[i])
2908 break;
2910 if (e3 >= 0)
2911 continue;
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));
2917 for (; e >= 0; e--)
2918 if (pb->geqs[e].coef[i])
2919 is_dead_geq[e] = true;
2921 try_again = true;
2922 is_dead_var[i] = true;
2927 for (e = pb->num_geqs - 1; e >= 0; e--)
2928 if (is_dead_geq[e])
2929 omega_delete_geq (pb, e, n_vars);
2931 for (i = n_vars; i > 0; i--)
2932 if (is_dead_var[i])
2933 omega_delete_variable (pb, i);
2935 if (dump_file && (dump_flags & TDF_DETAILS))
2937 fprintf (dump_file, "\nafter free red eliminations:\n");
2938 omega_print_problem (dump_file, pb);
2939 fprintf (dump_file, "\n");
2942 free (is_red_var);
2943 free (is_dead_var);
2944 free (is_dead_geq);
2947 /* For equation EQ of the form "0 = EQN", insert in PB two
2948 inequalities "0 <= EQN" and "0 <= -EQN". */
2950 void
2951 omega_convert_eq_to_geqs (omega_pb pb, int eq)
2953 int i;
2955 if (dump_file && (dump_flags & TDF_DETAILS))
2956 fprintf (dump_file, "Converting Eq to Geqs\n");
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++;
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;
2967 for (i = 0; i <= pb->num_vars; i++)
2968 pb->geqs[pb->num_geqs].coef[i] *= -1;
2970 pb->num_geqs++;
2972 if (dump_file && (dump_flags & TDF_DETAILS))
2973 omega_print_problem (dump_file, pb);
2976 /* Eliminates variable I from PB. */
2978 static void
2979 omega_do_elimination (omega_pb pb, int e, int i)
2981 eqn sub = omega_alloc_eqns (0, 1);
2982 int c;
2983 int n_vars = pb->num_vars;
2985 if (dump_file && (dump_flags & TDF_DETAILS))
2986 fprintf (dump_file, "eliminating variable %s\n",
2987 omega_variable_to_str (pb, i));
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)
2994 if (pb->eqs[e].color == omega_red)
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);
3003 else
3005 omega_substitute (pb, sub, i, c);
3006 omega_delete_variable (pb, i);
3009 else
3011 int a = abs (c);
3012 int e2 = e;
3014 if (dump_file && (dump_flags & TDF_DETAILS))
3015 fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
3017 for (e = pb->num_eqs - 1; e >= 0; e--)
3018 if (pb->eqs[e].coef[i])
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;
3032 for (e = pb->num_geqs - 1; e >= 0; e--)
3033 if (pb->geqs[e].coef[i])
3035 eqn eqn = &(pb->geqs[e]);
3036 int j, k;
3038 if (sub->color == omega_red)
3039 eqn->color = omega_red;
3041 for (j = n_vars; j >= 0; j--)
3042 eqn->coef[j] *= a;
3044 eqn->touched = 1;
3045 k = eqn->coef[i];
3046 eqn->coef[i] = 0;
3048 for (j = n_vars; j >= 0; j--)
3049 eqn->coef[j] -= sub->coef[j] * k / c;
3053 for (e = pb->num_subs - 1; e >= 0; e--)
3054 if (pb->subs[e].coef[i])
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;
3068 if (in_approximate_mode)
3069 omega_delete_variable (pb, i);
3070 else
3071 omega_convert_eq_to_geqs (pb, e2);
3074 omega_free_eqns (sub, 1);
3077 /* Helper function for printing "sorry, no solution". */
3079 static inline enum omega_result
3080 omega_problem_has_no_solution (void)
3082 if (dump_file && (dump_flags & TDF_DETAILS))
3083 fprintf (dump_file, "\nequations have no solution \n");
3085 return omega_false;
3088 /* Helper function: solve equations in PB one at a time, following the
3089 DESIRED_RES result. */
3091 static enum omega_result
3092 omega_solve_eq (omega_pb pb, enum omega_result desired_res)
3094 int i, j, e;
3095 int g, g2;
3096 g = 0;
3099 if (dump_file && (dump_flags & TDF_DETAILS) && pb->num_eqs > 0)
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");
3107 if (may_be_red)
3109 i = 0;
3110 j = pb->num_eqs - 1;
3112 while (1)
3114 eqn eq;
3116 while (i <= j && pb->eqs[i].color == omega_red)
3117 i++;
3119 while (i <= j && pb->eqs[j].color == omega_black)
3120 j--;
3122 if (i >= j)
3123 break;
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--;
3135 /* Eliminate all EQ equations */
3136 for (e = pb->num_eqs - 1; e >= 0; e--)
3138 eqn eqn = &(pb->eqs[e]);
3139 int sv;
3141 if (dump_file && (dump_flags & TDF_DETAILS))
3142 fprintf (dump_file, "----\n");
3144 for (i = pb->num_vars; i > 0; i--)
3145 if (eqn->coef[i])
3146 break;
3148 g = eqn->coef[i];
3150 for (j = i - 1; j > 0; j--)
3151 if (eqn->coef[j])
3152 break;
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. */
3158 if (j == 0)
3160 if (eqn->coef[0] % g != 0)
3161 return omega_problem_has_no_solution ();
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;
3170 else if (j == -1)
3172 if (eqn->coef[0] != 0)
3173 return omega_problem_has_no_solution ();
3175 pb->num_eqs--;
3176 continue;
3179 if (g < 0)
3180 g = -g;
3182 if (g == 1)
3184 pb->num_eqs--;
3185 omega_do_elimination (pb, e, i);
3188 else
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);
3197 if (dump_file && (dump_flags & TDF_DETAILS) && promotion_possible)
3198 fprintf (dump_file, " Promotion possible\n");
3200 normalizeEQ:
3201 if (!omega_safe_var_p (pb, j))
3203 for (; g != 1 && !omega_safe_var_p (pb, j); j--)
3204 g = gcd (abs (eqn->coef[j]), g);
3205 g2 = g;
3207 else if (!omega_safe_var_p (pb, i))
3208 g2 = g;
3209 else
3210 g2 = 0;
3212 for (; g != 1 && j > 0; j--)
3213 g = gcd (abs (eqn->coef[j]), g);
3215 if (g > 1)
3217 if (eqn->coef[0] % g != 0)
3218 return omega_problem_has_no_solution ();
3220 for (j = 0; j <= pb->num_vars; j++)
3221 eqn->coef[j] /= g;
3223 g2 = g2 / g;
3226 if (g2 > 1)
3228 int e2;
3230 for (e2 = e - 1; e2 >= 0; e2--)
3231 if (pb->eqs[e2].coef[i])
3232 break;
3234 if (e2 == -1)
3235 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
3236 if (pb->geqs[e2].coef[i])
3237 break;
3239 if (e2 == -1)
3240 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
3241 if (pb->subs[e2].coef[i])
3242 break;
3244 if (e2 == -1)
3246 bool change = false;
3248 if (dump_file && (dump_flags & TDF_DETAILS))
3250 fprintf (dump_file, "Ha! We own it! \n");
3251 omega_print_eq (dump_file, pb, eqn);
3252 fprintf (dump_file, " \n");
3255 g = eqn->coef[i];
3256 g = abs (g);
3258 for (j = i - 1; j >= 0; j--)
3260 int t = int_mod (eqn->coef[j], g);
3262 if (2 * t >= g)
3263 t -= g;
3265 if (t != eqn->coef[j])
3267 eqn->coef[j] = t;
3268 change = true;
3272 if (!change)
3274 if (dump_file && (dump_flags & TDF_DETAILS))
3275 fprintf (dump_file, "So what?\n");
3278 else
3280 omega_name_wild_card (pb, i);
3282 if (dump_file && (dump_flags & TDF_DETAILS))
3284 omega_print_eq (dump_file, pb, eqn);
3285 fprintf (dump_file, " \n");
3288 e++;
3289 continue;
3294 if (promotion_possible)
3296 if (dump_file && (dump_flags & TDF_DETAILS))
3298 fprintf (dump_file, "promoting %s to safety\n",
3299 omega_variable_to_str (pb, i));
3300 omega_print_vars (dump_file, pb);
3303 pb->safe_vars++;
3305 if (!omega_wildcard_p (pb, i))
3306 omega_name_wild_card (pb, i);
3308 promotion_possible = false;
3309 j = k;
3310 goto normalizeEQ;
3313 if (g2 > 1 && !in_approximate_mode)
3315 if (pb->eqs[e].color == omega_red)
3317 if (dump_file && (dump_flags & TDF_DETAILS))
3318 fprintf (dump_file, "handling red equality\n");
3320 pb->num_eqs--;
3321 omega_do_elimination (pb, e, i);
3322 continue;
3325 if (dump_file && (dump_flags & TDF_DETAILS))
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");
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);
3342 for (j = pb->num_vars; j >= 0; j--)
3344 pb->eqs[e + 1].coef[j] = int_mod (pb->eqs[e + 1].coef[j], g2);
3346 if (2 * pb->eqs[e + 1].coef[j] >= g2)
3347 pb->eqs[e + 1].coef[j] -= g2;
3350 pb->eqs[e + 1].coef[i] = g2;
3351 e += 2;
3353 if (dump_file && (dump_flags & TDF_DETAILS))
3354 omega_print_problem (dump_file, pb);
3356 continue;
3359 sv = pb->safe_vars;
3360 if (g2 == 0)
3361 sv = 0;
3363 /* Find variable to eliminate. */
3364 if (g2 > 1)
3366 gcc_assert (in_approximate_mode);
3368 if (dump_file && (dump_flags & TDF_DETAILS))
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);
3376 for (i = pb->num_vars; i > sv; i--)
3377 if (pb->eqs[e].coef[i] != 0)
3378 break;
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;
3385 if (i > sv)
3387 pb->num_eqs--;
3388 omega_do_elimination (pb, e, i);
3390 if (dump_file && (dump_flags & TDF_DETAILS) && g2 > 1)
3392 fprintf (dump_file, "result of non-exact elimination:\n");
3393 omega_print_problem (dump_file, pb);
3396 else
3398 int factor = (INT_MAX);
3399 j = 0;
3401 if (dump_file && (dump_flags & TDF_DETAILS))
3402 fprintf (dump_file, "doing moding\n");
3404 for (i = pb->num_vars; i != sv; i--)
3405 if ((pb->eqs[e].coef[i] & 1) != 0)
3407 j = i;
3408 i--;
3410 for (; i != sv; i--)
3411 if ((pb->eqs[e].coef[i] & 1) != 0)
3412 break;
3414 break;
3417 if (j != 0 && i == sv)
3419 omega_do_mod (pb, 2, e, j);
3420 e++;
3421 continue;
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)
3429 factor = abs (pb->eqs[e].coef[i]) + 1;
3430 j = i;
3433 if (j == sv)
3435 if (dump_file && (dump_flags & TDF_DETAILS))
3436 fprintf (dump_file, "should not have happened\n");
3437 gcc_assert (0);
3440 omega_do_mod (pb, factor, e, j);
3441 /* Go back and try this equation again. */
3442 e++;
3447 pb->num_eqs = 0;
3448 return omega_unknown;
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. */
3456 static enum omega_result
3457 parallel_splinter (omega_pb pb, int e, int diff,
3458 enum omega_result desired_res)
3460 omega_pb tmp_problem;
3461 int i;
3463 if (dump_file && (dump_flags & TDF_DETAILS))
3465 fprintf (dump_file, "Using parallel splintering\n");
3466 omega_print_problem (dump_file, pb);
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;
3473 for (i = 0; i <= diff; i++)
3475 omega_copy_problem (tmp_problem, pb);
3477 if (dump_file && (dump_flags & TDF_DETAILS))
3479 fprintf (dump_file, "Splinter # %i\n", i);
3480 omega_print_problem (dump_file, pb);
3483 if (omega_solve_problem (tmp_problem, desired_res) == omega_true)
3485 free (tmp_problem);
3486 return omega_true;
3489 pb->eqs[0].coef[0]--;
3492 free (tmp_problem);
3493 return omega_false;
3496 /* Helper function: solve equations one at a time. */
3498 static enum omega_result
3499 omega_solve_geq (omega_pb pb, enum omega_result desired_res)
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;
3509 if (desired_res != omega_simplify)
3511 pb->num_subs = 0;
3512 pb->safe_vars = 0;
3515 solve_geq_start:
3516 do {
3517 gcc_assert (desired_res == omega_simplify || pb->num_subs == 0);
3519 /* Verify that there are not too many inequalities. */
3520 gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
3522 if (dump_file && (dump_flags & TDF_DETAILS))
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");
3530 n_vars = pb->num_vars;
3532 if (n_vars == 1)
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;
3539 for (e = pb->num_geqs - 1; e >= 0; e--)
3541 int a = pb->geqs[e].coef[1];
3542 int c = pb->geqs[e].coef[0];
3544 /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax. */
3545 if (a == 0)
3547 if (c < 0)
3548 return omega_problem_has_no_solution ();
3550 else if (a > 0)
3552 if (a != 1)
3553 c = int_div (c, a);
3555 if (lower_bound < -c
3556 || (lower_bound == -c
3557 && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3559 lower_bound = -c;
3560 l_color = pb->geqs[e].color;
3563 else
3565 if (a != -1)
3566 c = int_div (c, -a);
3568 if (upper_bound > c
3569 || (upper_bound == c
3570 && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3572 upper_bound = c;
3573 u_color = pb->geqs[e].color;
3578 if (dump_file && (dump_flags & TDF_DETAILS))
3580 fprintf (dump_file, "upper bound = %d\n", upper_bound);
3581 fprintf (dump_file, "lower bound = %d\n", lower_bound);
3584 if (lower_bound > upper_bound)
3585 return omega_problem_has_no_solution ();
3587 if (desired_res == omega_simplify)
3589 pb->num_geqs = 0;
3590 if (pb->safe_vars == 1)
3593 if (lower_bound == upper_bound
3594 && u_color == omega_black
3595 && l_color == omega_black)
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);
3603 else
3605 if (lower_bound > neg_infinity)
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;
3615 if (upper_bound < pos_infinity)
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++;
3626 else
3627 pb->num_vars = 0;
3629 omega_problem_reduced (pb);
3630 return omega_false;
3633 if (original_problem != no_problem
3634 && l_color == omega_black
3635 && u_color == omega_black
3636 && !conservative
3637 && lower_bound == upper_bound)
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);
3645 return omega_true;
3648 if (!pb->variables_freed)
3650 pb->variables_freed = true;
3652 if (desired_res != omega_simplify)
3653 omega_free_eliminations (pb, 0);
3654 else
3655 omega_free_eliminations (pb, pb->safe_vars);
3657 n_vars = pb->num_vars;
3659 if (n_vars == 1)
3660 continue;
3663 switch (normalize_omega_problem (pb))
3665 case normalize_false:
3666 return omega_false;
3667 break;
3669 case normalize_coupled:
3670 coupled_subscripts = true;
3671 break;
3673 case normalize_uncoupled:
3674 coupled_subscripts = false;
3675 break;
3677 default:
3678 gcc_unreachable ();
3681 n_vars = pb->num_vars;
3683 if (dump_file && (dump_flags & TDF_DETAILS))
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");
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;
3705 eliminate_again = false;
3707 if (pb->num_eqs > 0)
3708 return omega_solve_problem (pb, desired_res);
3710 if (!coupled_subscripts)
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);
3719 pb->num_vars = pb->safe_vars;
3721 if (desired_res == omega_simplify)
3723 omega_problem_reduced (pb);
3724 return omega_false;
3727 return omega_true;
3730 if (desired_res != omega_simplify)
3731 fv = 0;
3732 else
3733 fv = pb->safe_vars;
3735 if (pb->num_geqs == 0)
3737 if (desired_res == omega_simplify)
3739 pb->num_vars = pb->safe_vars;
3740 omega_problem_reduced (pb);
3741 return omega_false;
3743 return omega_true;
3746 if (desired_res == omega_simplify && n_vars == pb->safe_vars)
3748 omega_problem_reduced (pb);
3749 return omega_false;
3752 if (pb->num_geqs > OMEGA_MAX_GEQS - 30
3753 || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10)
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);
3762 if (!omega_eliminate_redundant (pb, false))
3763 return omega_false;
3765 n_vars = pb->num_vars;
3767 if (pb->num_eqs > 0)
3768 return omega_solve_problem (pb, desired_res);
3770 if (dump_file && (dump_flags & TDF_DETAILS))
3771 fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3774 if (desired_res != omega_simplify)
3775 fv = 0;
3776 else
3777 fv = pb->safe_vars;
3779 for (i = n_vars; i != fv; i--)
3781 int score;
3782 int ub = -2;
3783 int lb = -2;
3784 bool lucky = false;
3785 int upper_bound_count = 0;
3787 lower_bound_count = 0;
3788 minC = maxC = 0;
3790 for (e = pb->num_geqs - 1; e >= 0; e--)
3791 if (pb->geqs[e].coef[i] < 0)
3793 minC = MIN (minC, pb->geqs[e].coef[i]);
3794 upper_bound_count++;
3795 if (pb->geqs[e].coef[i] < -1)
3797 if (ub == -2)
3798 ub = e;
3799 else
3800 ub = -1;
3803 else if (pb->geqs[e].coef[i] > 0)
3805 maxC = MAX (maxC, pb->geqs[e].coef[i]);
3806 lower_bound_count++;
3807 Le = e;
3808 if (pb->geqs[e].coef[i] > 1)
3810 if (lb == -2)
3811 lb = e;
3812 else
3813 lb = -1;
3817 if (lower_bound_count == 0
3818 || upper_bound_count == 0)
3820 lower_bound_count = 0;
3821 break;
3824 if (ub >= 0 && lb >= 0
3825 && pb->geqs[lb].key == -pb->geqs[ub].key)
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));
3834 if (maxC == 1
3835 || minC == -1
3836 || lucky
3837 || in_approximate_mode)
3839 score = upper_bound_count * lower_bound_count;
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);
3850 if (!exact
3851 || score < best)
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;
3865 else if (!exact)
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);
3875 score = maxC - minC;
3877 if (best > score)
3879 best = score;
3880 j = i;
3881 minCj = minC;
3882 jLe = Le;
3883 jLowerBoundCount = lower_bound_count;
3888 if (lower_bound_count == 0)
3890 omega_free_eliminations (pb, pb->safe_vars);
3891 n_vars = pb->num_vars;
3892 eliminate_again = true;
3893 continue;
3896 i = j;
3897 minC = minCj;
3898 Le = jLe;
3899 lower_bound_count = jLowerBoundCount;
3901 for (e = pb->num_geqs - 1; e >= 0; e--)
3902 if (pb->geqs[e].coef[i] > 0)
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;
3912 /* #ifdef Omega3 */
3913 /* Trying to produce exact elimination by finding redundant
3914 constraints. */
3915 if (!exact && !tried_eliminating_redundant)
3917 omega_eliminate_redundant (pb, false);
3918 tried_eliminating_redundant = true;
3919 eliminate_again = true;
3920 continue;
3922 tried_eliminating_redundant = false;
3923 /* #endif */
3925 if (return_single_result && desired_res == omega_simplify && !exact)
3927 omega_problem_reduced (pb);
3928 return omega_true;
3931 /* #ifndef Omega3 */
3932 /* Trying to produce exact elimination by finding redundant
3933 constraints. */
3934 if (!exact && !tried_eliminating_redundant)
3936 omega_eliminate_redundant (pb, false);
3937 tried_eliminating_redundant = true;
3938 continue;
3940 tried_eliminating_redundant = false;
3941 /* #endif */
3943 if (!exact)
3945 int e1, e2;
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))
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;
3963 if (dump_file && (dump_flags & TDF_DETAILS)
3964 && best_parallel_eqn >= 0)
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);
3975 if (dump_file && (dump_flags & TDF_DETAILS))
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);
3982 if (lucky_exact)
3983 fprintf (dump_file, "(a lucky exact elimination)\n");
3985 else if (exact)
3986 fprintf (dump_file, "(an exact elimination)\n");
3988 fprintf (dump_file, "Max # of splinters = %d\n", max_splinters);
3991 gcc_assert (max_splinters >= 1);
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);
3998 smoothed = false;
4000 if (i != n_vars)
4002 int t;
4003 int j = pb->num_vars;
4005 if (dump_file && (dump_flags & TDF_DETAILS))
4007 fprintf (dump_file, "Swapping %d and %d\n", i, j);
4008 omega_print_problem (dump_file, pb);
4011 swap (&pb->var[i], &pb->var[j]);
4013 for (e = pb->num_geqs - 1; e >= 0; e--)
4014 if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
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;
4022 for (e = pb->num_subs - 1; e >= 0; e--)
4023 if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
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;
4030 if (dump_file && (dump_flags & TDF_DETAILS))
4032 fprintf (dump_file, "Swapping complete \n");
4033 omega_print_problem (dump_file, pb);
4034 fprintf (dump_file, "\n");
4037 i = j;
4040 else if (dump_file && (dump_flags & TDF_DETAILS))
4042 fprintf (dump_file, "No swap needed\n");
4043 omega_print_problem (dump_file, pb);
4046 pb->num_vars--;
4047 n_vars = pb->num_vars;
4049 if (exact)
4051 if (n_vars == 1)
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];
4060 for (Le = topeqn; Le >= 0; Le--)
4061 if ((Lc = pb->geqs[Le].coef[i]) == 0)
4063 if (pb->geqs[Le].coef[1] == 1)
4065 int constantTerm = -pb->geqs[Le].coef[0];
4067 if (constantTerm > lower_bound ||
4068 (constantTerm == lower_bound &&
4069 !omega_eqn_is_red (&pb->geqs[Le], desired_res)))
4071 lower_bound = constantTerm;
4072 lb_color = pb->geqs[Le].color;
4075 if (dump_file && (dump_flags & TDF_DETAILS))
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);
4088 else
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)))
4096 upper_bound = constantTerm;
4097 ub_color = pb->geqs[Le].color;
4100 if (dump_file && (dump_flags & TDF_DETAILS))
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);
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)
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;
4125 if (dump_file && (dump_flags & TDF_DETAILS))
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");
4135 if (coefficient > 0)
4137 constantTerm = -int_div (constantTerm, coefficient);
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))))
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;
4151 if (dump_file && (dump_flags & TDF_DETAILS))
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);
4166 else
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))
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;
4180 if (dump_file
4181 && (dump_flags & TDF_DETAILS))
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);
4198 pb->num_geqs = 0;
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 ? ']' : ' ');
4211 if (lower_bound > upper_bound)
4212 return omega_false;
4214 if (pb->safe_vars == 1)
4216 if (upper_bound == lower_bound
4217 && !(ub_color == omega_red || lb_color == omega_red)
4218 && !please_no_equalities_in_simplified_problems)
4220 pb->num_eqs++;
4221 pb->eqs[0].coef[1] = -1;
4222 pb->eqs[0].coef[0] = upper_bound;
4224 if (ub_color == omega_red
4225 || lb_color == omega_red)
4226 pb->eqs[0].color = omega_red;
4228 if (desired_res == omega_simplify
4229 && pb->eqs[0].color == omega_black)
4230 return omega_solve_problem (pb, desired_res);
4233 if (upper_bound != pos_infinity)
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++;
4243 if (lower_bound != neg_infinity)
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++;
4254 if (desired_res == omega_simplify)
4256 omega_problem_reduced (pb);
4257 return omega_false;
4259 else
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)
4268 for (i = original_problem->num_vars; i >= 0; i--)
4269 if (original_problem->var[i] == pb->var[1])
4270 break;
4272 if (i == 0)
4273 break;
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;
4281 if (dump_file && (dump_flags & TDF_DETAILS))
4283 fprintf (dump_file,
4284 "adding equality %d to outer problem\n", e);
4285 omega_print_problem (dump_file, original_problem);
4288 return omega_true;
4292 eliminate_again = true;
4294 if (lower_bound_count == 1)
4296 eqn lbeqn = omega_alloc_eqns (0, 1);
4297 int Lc = pb->geqs[Le].coef[i];
4299 if (dump_file && (dump_flags & TDF_DETAILS))
4300 fprintf (dump_file, "an inplace elimination\n");
4302 omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1));
4303 omega_delete_geq_extra (pb, Le, n_vars + 1);
4305 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4306 if (pb->geqs[Ue].coef[i] < 0)
4308 if (lbeqn->key == -pb->geqs[Ue].key)
4309 omega_delete_geq_extra (pb, Ue, n_vars + 1);
4310 else
4312 int k;
4313 int Uc = -pb->geqs[Ue].coef[i];
4314 pb->geqs[Ue].touched = 1;
4315 eliminate_again = false;
4317 if (lbeqn->color == omega_red)
4318 pb->geqs[Ue].color = omega_red;
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);
4325 if (dump_file && (dump_flags & TDF_DETAILS))
4327 omega_print_geq (dump_file, pb,
4328 &(pb->geqs[Ue]));
4329 fprintf (dump_file, "\n");
4334 omega_free_eqns (lbeqn, 1);
4335 continue;
4337 else
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--;
4345 if (dump_file && (dump_flags & TDF_DETAILS))
4346 fprintf (dump_file, "lower bound count = %d\n",
4347 lower_bound_count);
4349 for (Le = top_eqn; Le >= 0; Le--)
4350 if (pb->geqs[Le].coef[i] > 0)
4352 int Lc = pb->geqs[Le].coef[i];
4353 for (Ue = top_eqn; Ue >= 0; Ue--)
4354 if (pb->geqs[Ue].coef[i] < 0)
4356 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4358 int k;
4359 int Uc = -pb->geqs[Ue].coef[i];
4361 if (num_dead == 0)
4362 e2 = pb->num_geqs++;
4363 else
4364 e2 = dead_eqns[--num_dead];
4366 gcc_assert (e2 < OMEGA_MAX_GEQS);
4368 if (dump_file && (dump_flags & TDF_DETAILS))
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");
4381 eliminate_again = false;
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);
4388 pb->geqs[e2].coef[n_vars + 1] = 0;
4389 pb->geqs[e2].touched = 1;
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;
4397 if (dump_file && (dump_flags & TDF_DETAILS))
4399 omega_print_geq (dump_file, pb,
4400 &(pb->geqs[e2]));
4401 fprintf (dump_file, "\n");
4405 if (lower_bound_count == 0)
4407 dead_eqns[num_dead++] = Ue;
4409 if (dump_file && (dump_flags & TDF_DETAILS))
4410 fprintf (dump_file, "Killed %d\n", Ue);
4414 lower_bound_count--;
4415 dead_eqns[num_dead++] = Le;
4417 if (dump_file && (dump_flags & TDF_DETAILS))
4418 fprintf (dump_file, "Killed %d\n", Le);
4421 for (e = pb->num_geqs - 1; e >= 0; e--)
4422 is_dead[e] = false;
4424 while (num_dead > 0)
4425 is_dead[dead_eqns[--num_dead]] = true;
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);
4431 free (dead_eqns);
4432 free (is_dead);
4433 continue;
4436 else
4438 omega_pb rS, iS;
4440 rS = omega_alloc_problem (0, 0);
4441 iS = omega_alloc_problem (0, 0);
4442 e2 = 0;
4443 possible_easy_int_solution = true;
4445 for (e = 0; e < pb->num_geqs; e++)
4446 if (pb->geqs[e].coef[i] == 0)
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);
4453 if (dump_file && (dump_flags & TDF_DETAILS))
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");
4465 e2++;
4466 gcc_assert (e2 < OMEGA_MAX_GEQS);
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)
4474 int k;
4475 int Lc = pb->geqs[Le].coef[i];
4476 int Uc = -pb->geqs[Ue].coef[i];
4478 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4481 rS->geqs[e2].touched = iS->geqs[e2].touched = 1;
4483 if (dump_file && (dump_flags & TDF_DETAILS))
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");
4495 if (Uc == Lc)
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];
4501 iS->geqs[e2].coef[0] -= (Uc - 1);
4503 else
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);
4510 iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
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;
4519 if (dump_file && (dump_flags & TDF_DETAILS))
4521 omega_print_geq (dump_file, pb, &(rS->geqs[e2]));
4522 fprintf (dump_file, "\n");
4525 e2++;
4526 gcc_assert (e2 < OMEGA_MAX_GEQS);
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;
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;
4541 for (e = n_vars; e >= 0; e--)
4542 rS->var[e] = pb->var[e];
4544 for (e = n_vars; e >= 0; e--)
4545 iS->var[e] = pb->var[e];
4547 for (e = pb->num_subs - 1; e >= 0; e--)
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);
4553 pb->num_vars++;
4554 n_vars = pb->num_vars;
4556 if (desired_res != omega_true)
4558 if (original_problem == no_problem)
4560 original_problem = pb;
4561 result = omega_solve_geq (rS, omega_false);
4562 original_problem = no_problem;
4564 else
4565 result = omega_solve_geq (rS, omega_false);
4567 if (result == omega_false)
4569 free (rS);
4570 free (iS);
4571 return result;
4574 if (pb->num_eqs > 0)
4576 /* An equality constraint must have been found */
4577 free (rS);
4578 free (iS);
4579 return omega_solve_problem (pb, desired_res);
4583 if (desired_res != omega_false)
4585 int j;
4586 int lower_bounds = 0;
4587 int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS);
4589 if (possible_easy_int_solution)
4591 conservative++;
4592 result = omega_solve_geq (iS, desired_res);
4593 conservative--;
4595 if (result != omega_false)
4597 free (rS);
4598 free (iS);
4599 free (lower_bound);
4600 return result;
4604 if (!exact && best_parallel_eqn >= 0
4605 && parallel_difference <= max_splinters)
4607 free (rS);
4608 free (iS);
4609 free (lower_bound);
4610 return parallel_splinter (pb, best_parallel_eqn,
4611 parallel_difference,
4612 desired_res);
4615 if (dump_file && (dump_flags & TDF_DETAILS))
4616 fprintf (dump_file, "have to do exact analysis\n");
4618 conservative++;
4620 for (e = 0; e < pb->num_geqs; e++)
4621 if (pb->geqs[e].coef[i] > 1)
4622 lower_bound[lower_bounds++] = e;
4624 /* Sort array LOWER_BOUND. */
4625 for (j = 0; j < lower_bounds; j++)
4627 int k, smallest = j;
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;
4634 k = lower_bound[smallest];
4635 lower_bound[smallest] = lower_bound[j];
4636 lower_bound[j] = k;
4639 if (dump_file && (dump_flags & TDF_DETAILS))
4641 fprintf (dump_file, "lower bound coefficients = ");
4643 for (j = 0; j < lower_bounds; j++)
4644 fprintf (dump_file, " %d",
4645 pb->geqs[lower_bound[j]].coef[i]);
4647 fprintf (dump_file, "\n");
4650 for (j = 0; j < lower_bounds; j++)
4652 int max_incr;
4653 int c;
4654 int worst_lower_bound_constant = -minC;
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; */
4662 if (dump_file && (dump_flags & TDF_DETAILS))
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);
4672 if (max_incr > 50 && !smoothed
4673 && smooth_weird_equations (pb))
4675 conservative--;
4676 free (rS);
4677 free (iS);
4678 smoothed = true;
4679 goto solve_geq_start;
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;
4689 for (c = max_incr; c >= 0; c--)
4691 if (dump_file && (dump_flags & TDF_DETAILS))
4693 fprintf (dump_file,
4694 "trying next decrement of %d\n",
4695 max_incr - c);
4696 omega_print_problem (dump_file, pb);
4699 omega_copy_problem (rS, pb);
4701 if (dump_file && (dump_flags & TDF_DETAILS))
4702 omega_print_problem (dump_file, rS);
4704 result = omega_solve_problem (rS, desired_res);
4706 if (result == omega_true)
4708 free (rS);
4709 free (iS);
4710 free (lower_bound);
4711 conservative--;
4712 return omega_true;
4715 pb->eqs[0].coef[0]--;
4718 if (j + 1 < lower_bounds)
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);
4727 if (dump_file && (dump_flags & TDF_DETAILS))
4728 fprintf (dump_file,
4729 "exhausted lower bound, "
4730 "checking if still feasible ");
4732 result = omega_solve_problem (rS, omega_false);
4734 if (result == omega_false)
4735 break;
4739 if (dump_file && (dump_flags & TDF_DETAILS))
4740 fprintf (dump_file, "fall-off the end\n");
4742 free (rS);
4743 free (iS);
4744 free (lower_bound);
4745 conservative--;
4746 return omega_false;
4749 free (rS);
4750 free (iS);
4752 return omega_unknown;
4753 } while (eliminate_again);
4754 } while (1);
4757 /* Because the omega solver is recursive, this counter limits the
4758 recursion depth. */
4759 static int omega_solve_depth = 0;
4761 /* Return omega_true when the problem PB has a solution following the
4762 DESIRED_RES. */
4764 enum omega_result
4765 omega_solve_problem (omega_pb pb, enum omega_result desired_res)
4767 enum omega_result result;
4769 gcc_assert (pb->num_vars >= pb->safe_vars);
4770 omega_solve_depth++;
4772 if (desired_res != omega_simplify)
4773 pb->safe_vars = 0;
4775 if (omega_solve_depth > 50)
4777 if (dump_file && (dump_flags & TDF_DETAILS))
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);
4784 gcc_assert (0);
4787 if (omega_solve_eq (pb, desired_res) == omega_false)
4789 omega_solve_depth--;
4790 return omega_false;
4793 if (in_approximate_mode && !pb->num_geqs)
4795 result = omega_true;
4796 pb->num_vars = pb->safe_vars;
4797 omega_problem_reduced (pb);
4799 else
4800 result = omega_solve_geq (pb, desired_res);
4802 omega_solve_depth--;
4804 if (!omega_reduce_with_subs)
4806 resurrect_subs (pb);
4807 gcc_assert (please_no_equalities_in_simplified_problems
4808 || !result || pb->num_subs == 0);
4811 return result;
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. */
4819 bool
4820 omega_problem_has_red_equations (omega_pb pb)
4822 bool result;
4823 int e;
4824 int i;
4826 if (dump_file && (dump_flags & TDF_DETAILS))
4828 fprintf (dump_file, "Checking for red equations:\n");
4829 omega_print_problem (dump_file, pb);
4832 please_no_equalities_in_simplified_problems++;
4833 may_be_red++;
4835 if (omega_single_result)
4836 return_single_result++;
4838 create_color = true;
4839 result = (omega_simplify_problem (pb) == omega_false);
4841 if (omega_single_result)
4842 return_single_result--;
4844 may_be_red--;
4845 please_no_equalities_in_simplified_problems--;
4847 if (result)
4849 if (dump_file && (dump_flags & TDF_DETAILS))
4850 fprintf (dump_file, "Gist is FALSE\n");
4852 pb->num_subs = 0;
4853 pb->num_geqs = 0;
4854 pb->num_eqs = 1;
4855 pb->eqs[0].color = omega_red;
4857 for (i = pb->num_vars; i > 0; i--)
4858 pb->eqs[0].coef[i] = 0;
4860 pb->eqs[0].coef[0] = 1;
4861 return true;
4864 free_red_eliminations (pb);
4865 gcc_assert (pb->num_eqs == 0);
4867 for (e = pb->num_geqs - 1; e >= 0; e--)
4868 if (pb->geqs[e].color == omega_red)
4870 result = true;
4871 break;
4874 if (!result)
4875 return false;
4877 for (i = pb->safe_vars; i >= 1; i--)
4879 int ub = 0;
4880 int lb = 0;
4882 for (e = pb->num_geqs - 1; e >= 0; e--)
4884 if (pb->geqs[e].coef[i])
4886 if (pb->geqs[e].coef[i] > 0)
4887 lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4889 else
4890 ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4894 if (ub == 2 || lb == 2)
4897 if (dump_file && (dump_flags & TDF_DETAILS))
4898 fprintf (dump_file, "checks for upper/lower bounds worked!\n");
4900 if (!omega_reduce_with_subs)
4902 resurrect_subs (pb);
4903 gcc_assert (pb->num_subs == 0);
4906 return true;
4911 if (dump_file && (dump_flags & TDF_DETAILS))
4912 fprintf (dump_file,
4913 "*** Doing potentially expensive elimination tests "
4914 "for red equations\n");
4916 please_no_equalities_in_simplified_problems++;
4917 omega_eliminate_red (pb, true);
4918 please_no_equalities_in_simplified_problems--;
4920 result = false;
4921 gcc_assert (pb->num_eqs == 0);
4923 for (e = pb->num_geqs - 1; e >= 0; e--)
4924 if (pb->geqs[e].color == omega_red)
4926 result = true;
4927 break;
4930 if (dump_file && (dump_flags & TDF_DETAILS))
4932 if (!result)
4933 fprintf (dump_file,
4934 "******************** Redundant Red Equations eliminated!!\n");
4935 else
4936 fprintf (dump_file,
4937 "******************** Red Equations remain\n");
4939 omega_print_problem (dump_file, pb);
4942 if (!omega_reduce_with_subs)
4944 normalize_return_type r;
4946 resurrect_subs (pb);
4947 r = normalize_omega_problem (pb);
4948 gcc_assert (r != normalize_false);
4950 coalesce (pb);
4951 cleanout_wildcards (pb);
4952 gcc_assert (pb->num_subs == 0);
4955 return result;
4958 /* Calls omega_simplify_problem in approximate mode. */
4960 enum omega_result
4961 omega_simplify_approximate (omega_pb pb)
4963 enum omega_result result;
4965 if (dump_file && (dump_flags & TDF_DETAILS))
4966 fprintf (dump_file, "(Entering approximate mode\n");
4968 in_approximate_mode = true;
4969 result = omega_simplify_problem (pb);
4970 in_approximate_mode = false;
4972 gcc_assert (pb->num_vars == pb->safe_vars);
4973 if (!omega_reduce_with_subs)
4974 gcc_assert (pb->num_subs == 0);
4976 if (dump_file && (dump_flags & TDF_DETAILS))
4977 fprintf (dump_file, "Leaving approximate mode)\n");
4979 return result;
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. */
4988 enum omega_result
4989 omega_simplify_problem (omega_pb pb)
4991 int i;
4993 omega_found_reduction = omega_false;
4995 if (!pb->variables_initialized)
4996 omega_initialize_variables (pb);
4998 if (next_key * 3 > MAX_KEYS)
5000 int e;
5002 hash_version++;
5003 next_key = OMEGA_MAX_VARS + 1;
5005 for (e = pb->num_geqs - 1; e >= 0; e--)
5006 pb->geqs[e].touched = 1;
5008 for (i = 0; i < HASH_TABLE_SIZE; i++)
5009 hash_master[i].touched = -1;
5011 pb->hash_version = hash_version;
5014 else if (pb->hash_version != hash_version)
5016 int e;
5018 for (e = pb->num_geqs - 1; e >= 0; e--)
5019 pb->geqs[e].touched = 1;
5021 pb->hash_version = hash_version;
5024 if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars)
5025 omega_free_eliminations (pb, pb->safe_vars);
5027 if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0)
5029 omega_found_reduction = omega_solve_problem (pb, omega_unknown);
5031 if (omega_found_reduction != omega_false
5032 && !return_single_result)
5034 pb->num_geqs = 0;
5035 pb->num_eqs = 0;
5036 (*omega_when_reduced) (pb);
5039 return omega_found_reduction;
5042 omega_solve_problem (pb, omega_simplify);
5044 if (omega_found_reduction != omega_false)
5046 for (i = 1; omega_safe_var_p (pb, i); i++)
5047 pb->forwarding_address[pb->var[i]] = i;
5049 for (i = 0; i < pb->num_subs; i++)
5050 pb->forwarding_address[pb->subs[i].key] = -i - 1;
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);
5058 return omega_found_reduction;
5061 /* Make variable VAR unprotected: it then can be eliminated. */
5063 void
5064 omega_unprotect_variable (omega_pb pb, int var)
5066 int e, idx;
5067 idx = pb->forwarding_address[var];
5069 if (idx < 0)
5071 idx = -1 - idx;
5072 pb->num_subs--;
5074 if (idx < pb->num_subs)
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;
5081 else
5083 int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS);
5084 int e2;
5086 for (e = pb->num_subs - 1; e >= 0; e--)
5087 bring_to_life[e] = (pb->subs[e].coef[idx] != 0);
5089 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
5090 if (bring_to_life[e2])
5092 pb->num_vars++;
5093 pb->safe_vars++;
5095 if (pb->safe_vars < pb->num_vars)
5097 for (e = pb->num_geqs - 1; e >= 0; e--)
5099 pb->geqs[e].coef[pb->num_vars] =
5100 pb->geqs[e].coef[pb->safe_vars];
5102 pb->geqs[e].coef[pb->safe_vars] = 0;
5105 for (e = pb->num_eqs - 1; e >= 0; e--)
5107 pb->eqs[e].coef[pb->num_vars] =
5108 pb->eqs[e].coef[pb->safe_vars];
5110 pb->eqs[e].coef[pb->safe_vars] = 0;
5113 for (e = pb->num_subs - 1; e >= 0; e--)
5115 pb->subs[e].coef[pb->num_vars] =
5116 pb->subs[e].coef[pb->safe_vars];
5118 pb->subs[e].coef[pb->safe_vars] = 0;
5121 pb->var[pb->num_vars] = pb->var[pb->safe_vars];
5122 pb->forwarding_address[pb->var[pb->num_vars]] =
5123 pb->num_vars;
5125 else
5127 for (e = pb->num_geqs - 1; e >= 0; e--)
5128 pb->geqs[e].coef[pb->safe_vars] = 0;
5130 for (e = pb->num_eqs - 1; e >= 0; e--)
5131 pb->eqs[e].coef[pb->safe_vars] = 0;
5133 for (e = pb->num_subs - 1; e >= 0; e--)
5134 pb->subs[e].coef[pb->safe_vars] = 0;
5137 pb->var[pb->safe_vars] = pb->subs[e2].key;
5138 pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars;
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);
5145 if (e2 < pb->num_subs - 1)
5146 omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]),
5147 pb->num_vars);
5149 pb->num_subs--;
5152 omega_unprotect_1 (pb, &idx, NULL);
5153 free (bring_to_life);
5156 chain_unprotect (pb);
5159 /* Unprotects VAR and simplifies PB. */
5161 enum omega_result
5162 omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color,
5163 int var, int sign)
5165 int n_vars = pb->num_vars;
5166 int e, j;
5167 int k = pb->forwarding_address[var];
5169 if (k < 0)
5171 k = -1 - k;
5173 if (sign != 0)
5175 e = pb->num_geqs++;
5176 omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars);
5178 for (j = 0; j <= n_vars; j++)
5179 pb->geqs[e].coef[j] *= sign;
5181 pb->geqs[e].coef[0]--;
5182 pb->geqs[e].touched = 1;
5183 pb->geqs[e].color = color;
5185 else
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;
5193 else if (sign != 0)
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;
5202 else
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;
5211 omega_unprotect_variable (pb, var);
5212 return omega_simplify_problem (pb);
5215 /* Add an equation "VAR = VALUE" with COLOR to PB. */
5217 void
5218 omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color,
5219 int var, int value)
5221 int e;
5222 int k = pb->forwarding_address[var];
5224 if (k < 0)
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;
5232 else
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;
5240 pb->eqs[e].color = color;
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. */
5247 bool
5248 omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound)
5250 int n_vars = pb->num_vars;
5251 int e, j;
5252 bool is_simple;
5253 bool coupled = false;
5255 *lower_bound = neg_infinity;
5256 *upper_bound = pos_infinity;
5257 i = pb->forwarding_address[i];
5259 if (i < 0)
5261 i = -i - 1;
5263 for (j = 1; j <= n_vars; j++)
5264 if (pb->subs[i].coef[j] != 0)
5265 return true;
5267 *upper_bound = *lower_bound = pb->subs[i].coef[0];
5268 return false;
5271 for (e = pb->num_subs - 1; e >= 0; e--)
5272 if (pb->subs[e].coef[i] != 0)
5274 coupled = true;
5275 break;
5278 for (e = pb->num_eqs - 1; e >= 0; e--)
5279 if (pb->eqs[e].coef[i] != 0)
5281 is_simple = true;
5283 for (j = 1; j <= n_vars; j++)
5284 if (i != j && pb->eqs[e].coef[j] != 0)
5286 is_simple = false;
5287 coupled = true;
5288 break;
5291 if (!is_simple)
5292 continue;
5293 else
5295 *lower_bound = *upper_bound =
5296 -pb->eqs[e].coef[i] * pb->eqs[e].coef[0];
5297 return false;
5301 for (e = pb->num_geqs - 1; e >= 0; e--)
5302 if (pb->geqs[e].coef[i] != 0)
5304 if (pb->geqs[e].key == i)
5305 *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]);
5307 else if (pb->geqs[e].key == -i)
5308 *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]);
5310 else
5311 coupled = true;
5314 return coupled;
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. */
5322 static void
5323 query_coupled_variable (omega_pb pb, int i, int *l, int *u,
5324 bool *could_be_zero, int lower_bound, int upper_bound)
5326 int e, b1, b2;
5327 eqn eqn;
5328 int sign;
5329 int v;
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);
5336 /* Define variable I in terms of variable V. */
5337 if (pb->forwarding_address[i] == -1)
5339 eqn = &pb->subs[0];
5340 sign = 1;
5341 v = 1;
5343 else
5345 eqn = &pb->eqs[0];
5346 sign = -eqn->coef[1];
5347 v = 2;
5350 for (e = pb->num_geqs - 1; e >= 0; e--)
5351 if (pb->geqs[e].coef[v] != 0)
5353 if (pb->geqs[e].coef[v] == 1)
5354 lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]);
5356 else
5357 upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]);
5360 if (lower_bound > upper_bound)
5362 *l = pos_infinity;
5363 *u = neg_infinity;
5364 *could_be_zero = 0;
5365 return;
5368 if (lower_bound == neg_infinity)
5370 if (eqn->coef[v] > 0)
5371 b1 = sign * neg_infinity;
5373 else
5374 b1 = -sign * neg_infinity;
5376 else
5377 b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound);
5379 if (upper_bound == pos_infinity)
5381 if (eqn->coef[v] > 0)
5382 b2 = sign * pos_infinity;
5384 else
5385 b2 = -sign * pos_infinity;
5387 else
5388 b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound);
5390 *l = MAX (*l, b1 <= b2 ? b1 : b2);
5391 *u = MIN (*u, b1 <= b2 ? b2 : b1);
5393 *could_be_zero = (*l <= 0 && 0 <= *u
5394 && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0);
5397 /* Return false when a lower bound L and an upper bound U for variable
5398 I in problem PB have been initialized. */
5400 bool
5401 omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u)
5403 *l = neg_infinity;
5404 *u = pos_infinity;
5406 if (!omega_query_variable (pb, i, l, u)
5407 || (pb->num_vars == 1 && pb->forwarding_address[i] == 1))
5408 return false;
5410 if (abs (pb->forwarding_address[i]) == 1
5411 && pb->num_vars + pb->num_subs == 2
5412 && pb->num_eqs + pb->num_subs == 1)
5414 bool could_be_zero;
5415 query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity,
5416 pos_infinity);
5417 return false;
5420 return true;
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. */
5433 omega_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)
5437 int result;
5438 int l, u;
5439 bool could_be_zero;
5441 l = neg_infinity;
5442 u = pos_infinity;
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;
5449 if (l < 0)
5450 result |= dd_gt;
5452 if (u > 0)
5453 result |= dd_lt;
5455 if (could_be_zero)
5456 result |= dd_eq;
5458 if (l == u)
5460 *dist_known = true;
5461 *dist = l;
5463 else
5464 *dist_known = false;
5466 return result;
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]. */
5475 omega_pb
5476 omega_alloc_problem (int nvars, int nprot)
5478 omega_pb pb;
5480 gcc_assert (nvars <= OMEGA_MAX_VARS);
5481 omega_initialize ();
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);
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;
5502 /* Keeps the state of the initialization. */
5503 static bool omega_initialized = false;
5505 /* Initialization of the Omega solver. */
5507 void
5508 omega_initialize (void)
5510 int i;
5512 if (omega_initialized)
5513 return;
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);
5522 for (i = 0; i < HASH_TABLE_SIZE; i++)
5523 hash_master[i].touched = -1;
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");
5566 omega_initialized = true;