gcc/
[official-gcc.git] / gcc / omega.c
blob829520a338ad65c1f313140ece256179d2e0fccd
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 "alias.h"
37 #include "symtab.h"
38 #include "options.h"
39 #include "tree.h"
40 #include "diagnostic-core.h"
41 #include "dumpfile.h"
42 #include "omega.h"
44 /* When set to true, keep substitution variables. When set to false,
45 resurrect substitution variables (convert substitutions back to EQs). */
46 static bool omega_reduce_with_subs = true;
48 /* When set to true, omega_simplify_problem checks for problem with no
49 solutions, calling verify_omega_pb. */
50 static bool omega_verify_simplification = false;
52 /* When set to true, only produce a single simplified result. */
53 static bool omega_single_result = false;
55 /* Set return_single_result to 1 when omega_single_result is true. */
56 static int return_single_result = 0;
58 /* Hash table for equations generated by the solver. */
59 #define HASH_TABLE_SIZE PARAM_VALUE (PARAM_OMEGA_HASH_TABLE_SIZE)
60 #define MAX_KEYS PARAM_VALUE (PARAM_OMEGA_MAX_KEYS)
61 static eqn hash_master;
62 static int next_key;
63 static int hash_version = 0;
65 /* Set to true for making the solver enter in approximation mode. */
66 static bool in_approximate_mode = false;
68 /* When set to zero, the solver is allowed to add new equalities to
69 the problem to be solved. */
70 static int conservative = 0;
72 /* Set to omega_true when the problem was successfully reduced, set to
73 omega_unknown when the solver is unable to determine an answer. */
74 static enum omega_result omega_found_reduction;
76 /* Set to true when the solver is allowed to add omega_red equations. */
77 static bool create_color = false;
79 /* Set to nonzero when the problem to be solved can be reduced. */
80 static int may_be_red = 0;
82 /* When false, there should be no substitution equations in the
83 simplified problem. */
84 static int please_no_equalities_in_simplified_problems = 0;
86 /* Variables names for pretty printing. */
87 static char wild_name[200][40];
89 /* Pointer to the void problem. */
90 static omega_pb no_problem = (omega_pb) 0;
92 /* Pointer to the problem to be solved. */
93 static omega_pb original_problem = (omega_pb) 0;
96 /* Return the integer A divided by B. */
98 static inline int
99 int_div (int a, int b)
101 if (a > 0)
102 return a/b;
103 else
104 return -((-a + b - 1)/b);
107 /* Return the integer A modulo B. */
109 static inline int
110 int_mod (int a, int b)
112 return a - b * int_div (a, b);
115 /* Test whether equation E is red. */
117 static inline bool
118 omega_eqn_is_red (eqn e, int desired_res)
120 return (desired_res == omega_simplify && e->color == omega_red);
123 /* Return a string for VARIABLE. */
125 static inline char *
126 omega_var_to_str (int variable)
128 if (0 <= variable && variable <= 20)
129 return wild_name[variable];
131 if (-20 < variable && variable < 0)
132 return wild_name[40 + variable];
134 /* Collapse all the entries that would have overflowed. */
135 return wild_name[21];
138 /* Return a string for variable I in problem PB. */
140 static inline char *
141 omega_variable_to_str (omega_pb pb, int i)
143 return omega_var_to_str (pb->var[i]);
146 /* Do nothing function: used for default initializations. */
148 void
149 omega_no_procedure (omega_pb pb ATTRIBUTE_UNUSED)
153 void (*omega_when_reduced) (omega_pb) = omega_no_procedure;
155 /* Print to FILE from PB equation E with all its coefficients
156 multiplied by C. */
158 static void
159 omega_print_term (FILE *file, omega_pb pb, eqn e, int c)
161 int i;
162 bool first = true;
163 int n = pb->num_vars;
164 int went_first = -1;
166 for (i = 1; i <= n; i++)
167 if (c * e->coef[i] > 0)
169 first = false;
170 went_first = i;
172 if (c * e->coef[i] == 1)
173 fprintf (file, "%s", omega_variable_to_str (pb, i));
174 else
175 fprintf (file, "%d * %s", c * e->coef[i],
176 omega_variable_to_str (pb, i));
177 break;
180 for (i = 1; i <= n; i++)
181 if (i != went_first && c * e->coef[i] != 0)
183 if (!first && c * e->coef[i] > 0)
184 fprintf (file, " + ");
186 first = false;
188 if (c * e->coef[i] == 1)
189 fprintf (file, "%s", omega_variable_to_str (pb, i));
190 else if (c * e->coef[i] == -1)
191 fprintf (file, " - %s", omega_variable_to_str (pb, i));
192 else
193 fprintf (file, "%d * %s", c * e->coef[i],
194 omega_variable_to_str (pb, i));
197 if (!first && c * e->coef[0] > 0)
198 fprintf (file, " + ");
200 if (first || c * e->coef[0] != 0)
201 fprintf (file, "%d", c * e->coef[0]);
204 /* Print to FILE the equation E of problem PB. */
206 void
207 omega_print_eqn (FILE *file, omega_pb pb, eqn e, bool test, int extra)
209 int i;
210 int n = pb->num_vars + extra;
211 bool is_lt = test && e->coef[0] == -1;
212 bool first;
214 if (test)
216 if (e->touched)
217 fprintf (file, "!");
219 else if (e->key != 0)
220 fprintf (file, "%d: ", e->key);
223 if (e->color == omega_red)
224 fprintf (file, "[");
226 first = true;
228 for (i = is_lt ? 1 : 0; i <= n; i++)
229 if (e->coef[i] < 0)
231 if (!first)
232 fprintf (file, " + ");
233 else
234 first = false;
236 if (i == 0)
237 fprintf (file, "%d", -e->coef[i]);
238 else if (e->coef[i] == -1)
239 fprintf (file, "%s", omega_variable_to_str (pb, i));
240 else
241 fprintf (file, "%d * %s", -e->coef[i],
242 omega_variable_to_str (pb, i));
245 if (first)
247 if (is_lt)
249 fprintf (file, "1");
250 is_lt = false;
252 else
253 fprintf (file, "0");
256 if (test == 0)
257 fprintf (file, " = ");
258 else if (is_lt)
259 fprintf (file, " < ");
260 else
261 fprintf (file, " <= ");
263 first = true;
265 for (i = 0; i <= n; i++)
266 if (e->coef[i] > 0)
268 if (!first)
269 fprintf (file, " + ");
270 else
271 first = false;
273 if (i == 0)
274 fprintf (file, "%d", e->coef[i]);
275 else if (e->coef[i] == 1)
276 fprintf (file, "%s", omega_variable_to_str (pb, i));
277 else
278 fprintf (file, "%d * %s", e->coef[i],
279 omega_variable_to_str (pb, i));
282 if (first)
283 fprintf (file, "0");
285 if (e->color == omega_red)
286 fprintf (file, "]");
289 /* Print to FILE all the variables of problem PB. */
291 static void
292 omega_print_vars (FILE *file, omega_pb pb)
294 int i;
296 fprintf (file, "variables = ");
298 if (pb->safe_vars > 0)
299 fprintf (file, "protected (");
301 for (i = 1; i <= pb->num_vars; i++)
303 fprintf (file, "%s", omega_variable_to_str (pb, i));
305 if (i == pb->safe_vars)
306 fprintf (file, ")");
308 if (i < pb->num_vars)
309 fprintf (file, ", ");
312 fprintf (file, "\n");
315 /* Dump problem PB. */
317 DEBUG_FUNCTION void
318 debug (omega_pb_d &ref)
320 omega_print_problem (stderr, &ref);
323 DEBUG_FUNCTION void
324 debug (omega_pb_d *ptr)
326 if (ptr)
327 debug (*ptr);
328 else
329 fprintf (stderr, "<nil>\n");
332 /* Debug problem PB. */
334 DEBUG_FUNCTION void
335 debug_omega_problem (omega_pb pb)
337 omega_print_problem (stderr, pb);
340 /* Print to FILE problem PB. */
342 void
343 omega_print_problem (FILE *file, omega_pb pb)
345 int e;
347 if (!pb->variables_initialized)
348 omega_initialize_variables (pb);
350 omega_print_vars (file, pb);
352 for (e = 0; e < pb->num_eqs; e++)
354 omega_print_eq (file, pb, &pb->eqs[e]);
355 fprintf (file, "\n");
358 fprintf (file, "Done with EQ\n");
360 for (e = 0; e < pb->num_geqs; e++)
362 omega_print_geq (file, pb, &pb->geqs[e]);
363 fprintf (file, "\n");
366 fprintf (file, "Done with GEQ\n");
368 for (e = 0; e < pb->num_subs; e++)
370 eqn eq = &pb->subs[e];
372 if (eq->color == omega_red)
373 fprintf (file, "[");
375 if (eq->key > 0)
376 fprintf (file, "%s := ", omega_var_to_str (eq->key));
377 else
378 fprintf (file, "#%d := ", eq->key);
380 omega_print_term (file, pb, eq, 1);
382 if (eq->color == omega_red)
383 fprintf (file, "]");
385 fprintf (file, "\n");
389 /* Return the number of equations in PB tagged omega_red. */
392 omega_count_red_equations (omega_pb pb)
394 int e, i;
395 int result = 0;
397 for (e = 0; e < pb->num_eqs; e++)
398 if (pb->eqs[e].color == omega_red)
400 for (i = pb->num_vars; i > 0; i--)
401 if (pb->geqs[e].coef[i])
402 break;
404 if (i == 0 && pb->geqs[e].coef[0] == 1)
405 return 0;
406 else
407 result += 2;
410 for (e = 0; e < pb->num_geqs; e++)
411 if (pb->geqs[e].color == omega_red)
412 result += 1;
414 for (e = 0; e < pb->num_subs; e++)
415 if (pb->subs[e].color == omega_red)
416 result += 2;
418 return result;
421 /* Print to FILE all the equations in PB that are tagged omega_red. */
423 void
424 omega_print_red_equations (FILE *file, omega_pb pb)
426 int e;
428 if (!pb->variables_initialized)
429 omega_initialize_variables (pb);
431 omega_print_vars (file, pb);
433 for (e = 0; e < pb->num_eqs; e++)
434 if (pb->eqs[e].color == omega_red)
436 omega_print_eq (file, pb, &pb->eqs[e]);
437 fprintf (file, "\n");
440 for (e = 0; e < pb->num_geqs; e++)
441 if (pb->geqs[e].color == omega_red)
443 omega_print_geq (file, pb, &pb->geqs[e]);
444 fprintf (file, "\n");
447 for (e = 0; e < pb->num_subs; e++)
448 if (pb->subs[e].color == omega_red)
450 eqn eq = &pb->subs[e];
451 fprintf (file, "[");
453 if (eq->key > 0)
454 fprintf (file, "%s := ", omega_var_to_str (eq->key));
455 else
456 fprintf (file, "#%d := ", eq->key);
458 omega_print_term (file, pb, eq, 1);
459 fprintf (file, "]\n");
463 /* Pretty print PB to FILE. */
465 void
466 omega_pretty_print_problem (FILE *file, omega_pb pb)
468 int e, v, v1, v2, v3, t;
469 bool *live = XNEWVEC (bool, OMEGA_MAX_GEQS);
470 int stuffPrinted = 0;
471 bool change;
473 typedef enum {
474 none, le, lt
475 } partial_order_type;
477 partial_order_type **po = XNEWVEC (partial_order_type *,
478 OMEGA_MAX_VARS * OMEGA_MAX_VARS);
479 int **po_eq = XNEWVEC (int *, OMEGA_MAX_VARS * OMEGA_MAX_VARS);
480 int *last_links = XNEWVEC (int, OMEGA_MAX_VARS);
481 int *first_links = XNEWVEC (int, OMEGA_MAX_VARS);
482 int *chain_length = XNEWVEC (int, OMEGA_MAX_VARS);
483 int *chain = XNEWVEC (int, OMEGA_MAX_VARS);
484 int i, m;
485 bool multiprint;
487 if (!pb->variables_initialized)
488 omega_initialize_variables (pb);
490 if (pb->num_vars > 0)
492 omega_eliminate_redundant (pb, false);
494 for (e = 0; e < pb->num_eqs; e++)
496 if (stuffPrinted)
497 fprintf (file, "; ");
499 stuffPrinted = 1;
500 omega_print_eq (file, pb, &pb->eqs[e]);
503 for (e = 0; e < pb->num_geqs; e++)
504 live[e] = true;
506 while (1)
508 for (v = 1; v <= pb->num_vars; v++)
510 last_links[v] = first_links[v] = 0;
511 chain_length[v] = 0;
513 for (v2 = 1; v2 <= pb->num_vars; v2++)
514 po[v][v2] = none;
517 for (e = 0; e < pb->num_geqs; e++)
518 if (live[e])
520 for (v = 1; v <= pb->num_vars; v++)
521 if (pb->geqs[e].coef[v] == 1)
522 first_links[v]++;
523 else if (pb->geqs[e].coef[v] == -1)
524 last_links[v]++;
526 v1 = pb->num_vars;
528 while (v1 > 0 && pb->geqs[e].coef[v1] == 0)
529 v1--;
531 v2 = v1 - 1;
533 while (v2 > 0 && pb->geqs[e].coef[v2] == 0)
534 v2--;
536 v3 = v2 - 1;
538 while (v3 > 0 && pb->geqs[e].coef[v3] == 0)
539 v3--;
541 if (pb->geqs[e].coef[0] > 0 || pb->geqs[e].coef[0] < -1
542 || v2 <= 0 || v3 > 0
543 || pb->geqs[e].coef[v1] * pb->geqs[e].coef[v2] != -1)
545 /* Not a partial order relation. */
547 else
549 if (pb->geqs[e].coef[v1] == 1)
550 std::swap (v1, v2);
552 /* Relation is v1 <= v2 or v1 < v2. */
553 po[v1][v2] = ((pb->geqs[e].coef[0] == 0) ? le : lt);
554 po_eq[v1][v2] = e;
557 for (v = 1; v <= pb->num_vars; v++)
558 chain_length[v] = last_links[v];
560 /* Just in case pb->num_vars <= 0. */
561 change = false;
562 for (t = 0; t < pb->num_vars; t++)
564 change = false;
566 for (v1 = 1; v1 <= pb->num_vars; v1++)
567 for (v2 = 1; v2 <= pb->num_vars; v2++)
568 if (po[v1][v2] != none &&
569 chain_length[v1] <= chain_length[v2])
571 chain_length[v1] = chain_length[v2] + 1;
572 change = true;
576 /* Caught in cycle. */
577 gcc_assert (!change);
579 for (v1 = 1; v1 <= pb->num_vars; v1++)
580 if (chain_length[v1] == 0)
581 first_links[v1] = 0;
583 v = 1;
585 for (v1 = 2; v1 <= pb->num_vars; v1++)
586 if (chain_length[v1] + first_links[v1] >
587 chain_length[v] + first_links[v])
588 v = v1;
590 if (chain_length[v] + first_links[v] == 0)
591 break;
593 if (stuffPrinted)
594 fprintf (file, "; ");
596 stuffPrinted = 1;
598 /* Chain starts at v. */
600 int tmp;
601 bool first = true;
603 for (e = 0; e < pb->num_geqs; e++)
604 if (live[e] && pb->geqs[e].coef[v] == 1)
606 if (!first)
607 fprintf (file, ", ");
609 tmp = pb->geqs[e].coef[v];
610 pb->geqs[e].coef[v] = 0;
611 omega_print_term (file, pb, &pb->geqs[e], -1);
612 pb->geqs[e].coef[v] = tmp;
613 live[e] = false;
614 first = false;
617 if (!first)
618 fprintf (file, " <= ");
621 /* Find chain. */
622 chain[0] = v;
623 m = 1;
624 while (1)
626 /* Print chain. */
627 for (v2 = 1; v2 <= pb->num_vars; v2++)
628 if (po[v][v2] && chain_length[v] == 1 + chain_length[v2])
629 break;
631 if (v2 > pb->num_vars)
632 break;
634 chain[m++] = v2;
635 v = v2;
638 fprintf (file, "%s", omega_variable_to_str (pb, chain[0]));
640 for (multiprint = false, i = 1; i < m; i++)
642 v = chain[i - 1];
643 v2 = chain[i];
645 if (po[v][v2] == le)
646 fprintf (file, " <= ");
647 else
648 fprintf (file, " < ");
650 fprintf (file, "%s", omega_variable_to_str (pb, v2));
651 live[po_eq[v][v2]] = false;
653 if (!multiprint && i < m - 1)
654 for (v3 = 1; v3 <= pb->num_vars; v3++)
656 if (v == v3 || v2 == v3
657 || po[v][v2] != po[v][v3]
658 || po[v2][chain[i + 1]] != po[v3][chain[i + 1]])
659 continue;
661 fprintf (file, ",%s", omega_variable_to_str (pb, v3));
662 live[po_eq[v][v3]] = false;
663 live[po_eq[v3][chain[i + 1]]] = false;
664 multiprint = true;
666 else
667 multiprint = false;
670 v = chain[m - 1];
671 /* Print last_links. */
673 int tmp;
674 bool first = true;
676 for (e = 0; e < pb->num_geqs; e++)
677 if (live[e] && pb->geqs[e].coef[v] == -1)
679 if (!first)
680 fprintf (file, ", ");
681 else
682 fprintf (file, " <= ");
684 tmp = pb->geqs[e].coef[v];
685 pb->geqs[e].coef[v] = 0;
686 omega_print_term (file, pb, &pb->geqs[e], 1);
687 pb->geqs[e].coef[v] = tmp;
688 live[e] = false;
689 first = false;
694 for (e = 0; e < pb->num_geqs; e++)
695 if (live[e])
697 if (stuffPrinted)
698 fprintf (file, "; ");
699 stuffPrinted = 1;
700 omega_print_geq (file, pb, &pb->geqs[e]);
703 for (e = 0; e < pb->num_subs; e++)
705 eqn eq = &pb->subs[e];
707 if (stuffPrinted)
708 fprintf (file, "; ");
710 stuffPrinted = 1;
712 if (eq->key > 0)
713 fprintf (file, "%s := ", omega_var_to_str (eq->key));
714 else
715 fprintf (file, "#%d := ", eq->key);
717 omega_print_term (file, pb, eq, 1);
721 free (live);
722 free (po);
723 free (po_eq);
724 free (last_links);
725 free (first_links);
726 free (chain_length);
727 free (chain);
730 /* Assign to variable I in PB the next wildcard name. The name of a
731 wildcard is a negative number. */
732 static int next_wild_card = 0;
734 static void
735 omega_name_wild_card (omega_pb pb, int i)
737 --next_wild_card;
738 if (next_wild_card < -PARAM_VALUE (PARAM_OMEGA_MAX_WILD_CARDS))
739 next_wild_card = -1;
740 pb->var[i] = next_wild_card;
743 /* Return the index of the last protected (or safe) variable in PB,
744 after having added a new wildcard variable. */
746 static int
747 omega_add_new_wild_card (omega_pb pb)
749 int e;
750 int i = ++pb->safe_vars;
751 pb->num_vars++;
753 /* Make a free place in the protected (safe) variables, by moving
754 the non protected variable pointed by "I" at the end, ie. at
755 offset pb->num_vars. */
756 if (pb->num_vars != i)
758 /* Move "I" for all the inequalities. */
759 for (e = pb->num_geqs - 1; e >= 0; e--)
761 if (pb->geqs[e].coef[i])
762 pb->geqs[e].touched = 1;
764 pb->geqs[e].coef[pb->num_vars] = pb->geqs[e].coef[i];
767 /* Move "I" for all the equalities. */
768 for (e = pb->num_eqs - 1; e >= 0; e--)
769 pb->eqs[e].coef[pb->num_vars] = pb->eqs[e].coef[i];
771 /* Move "I" for all the substitutions. */
772 for (e = pb->num_subs - 1; e >= 0; e--)
773 pb->subs[e].coef[pb->num_vars] = pb->subs[e].coef[i];
775 /* Move the identifier. */
776 pb->var[pb->num_vars] = pb->var[i];
779 /* Initialize at zero all the coefficients */
780 for (e = pb->num_geqs - 1; e >= 0; e--)
781 pb->geqs[e].coef[i] = 0;
783 for (e = pb->num_eqs - 1; e >= 0; e--)
784 pb->eqs[e].coef[i] = 0;
786 for (e = pb->num_subs - 1; e >= 0; e--)
787 pb->subs[e].coef[i] = 0;
789 /* And give it a name. */
790 omega_name_wild_card (pb, i);
791 return i;
794 /* Delete inequality E from problem PB that has N_VARS variables. */
796 static void
797 omega_delete_geq (omega_pb pb, int e, int n_vars)
799 if (dump_file && (dump_flags & TDF_DETAILS))
801 fprintf (dump_file, "Deleting %d (last:%d): ", e, pb->num_geqs - 1);
802 omega_print_geq (dump_file, pb, &pb->geqs[e]);
803 fprintf (dump_file, "\n");
806 if (e < pb->num_geqs - 1)
807 omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
809 pb->num_geqs--;
812 /* Delete extra inequality E from problem PB that has N_VARS
813 variables. */
815 static void
816 omega_delete_geq_extra (omega_pb pb, int e, int n_vars)
818 if (dump_file && (dump_flags & TDF_DETAILS))
820 fprintf (dump_file, "Deleting %d: ",e);
821 omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
822 fprintf (dump_file, "\n");
825 if (e < pb->num_geqs - 1)
826 omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
828 pb->num_geqs--;
832 /* Remove variable I from problem PB. */
834 static void
835 omega_delete_variable (omega_pb pb, int i)
837 int n_vars = pb->num_vars;
838 int e;
840 if (omega_safe_var_p (pb, i))
842 int j = pb->safe_vars;
844 for (e = pb->num_geqs - 1; e >= 0; e--)
846 pb->geqs[e].touched = 1;
847 pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
848 pb->geqs[e].coef[j] = pb->geqs[e].coef[n_vars];
851 for (e = pb->num_eqs - 1; e >= 0; e--)
853 pb->eqs[e].coef[i] = pb->eqs[e].coef[j];
854 pb->eqs[e].coef[j] = pb->eqs[e].coef[n_vars];
857 for (e = pb->num_subs - 1; e >= 0; e--)
859 pb->subs[e].coef[i] = pb->subs[e].coef[j];
860 pb->subs[e].coef[j] = pb->subs[e].coef[n_vars];
863 pb->var[i] = pb->var[j];
864 pb->var[j] = pb->var[n_vars];
866 else if (i < n_vars)
868 for (e = pb->num_geqs - 1; e >= 0; e--)
869 if (pb->geqs[e].coef[n_vars])
871 pb->geqs[e].coef[i] = pb->geqs[e].coef[n_vars];
872 pb->geqs[e].touched = 1;
875 for (e = pb->num_eqs - 1; e >= 0; e--)
876 pb->eqs[e].coef[i] = pb->eqs[e].coef[n_vars];
878 for (e = pb->num_subs - 1; e >= 0; e--)
879 pb->subs[e].coef[i] = pb->subs[e].coef[n_vars];
881 pb->var[i] = pb->var[n_vars];
884 if (omega_safe_var_p (pb, i))
885 pb->safe_vars--;
887 pb->num_vars--;
890 /* Because the coefficients of an equation are sparse, PACKING records
891 indices for non null coefficients. */
892 static int *packing;
894 /* Set up the coefficients of PACKING, following the coefficients of
895 equation EQN that has NUM_VARS variables. */
897 static inline int
898 setup_packing (eqn eqn, int num_vars)
900 int k;
901 int n = 0;
903 for (k = num_vars; k >= 0; k--)
904 if (eqn->coef[k])
905 packing[n++] = k;
907 return n;
910 /* Computes a linear combination of EQ and SUB at VAR with coefficient
911 C, such that EQ->coef[VAR] is set to 0. TOP_VAR is the number of
912 non null indices of SUB stored in PACKING. */
914 static inline void
915 omega_substitute_red_1 (eqn eq, eqn sub, int var, int c, bool *found_black,
916 int top_var)
918 if (eq->coef[var] != 0)
920 if (eq->color == omega_black)
921 *found_black = true;
922 else
924 int j, k = eq->coef[var];
926 eq->coef[var] = 0;
928 for (j = top_var; j >= 0; j--)
929 eq->coef[packing[j]] -= sub->coef[packing[j]] * k * c;
934 /* Substitute in PB variable VAR with "C * SUB". */
936 static void
937 omega_substitute_red (omega_pb pb, eqn sub, int var, int c, bool *found_black)
939 int e, top_var = setup_packing (sub, pb->num_vars);
941 *found_black = false;
943 if (dump_file && (dump_flags & TDF_DETAILS))
945 if (sub->color == omega_red)
946 fprintf (dump_file, "[");
948 fprintf (dump_file, "substituting using %s := ",
949 omega_variable_to_str (pb, var));
950 omega_print_term (dump_file, pb, sub, -c);
952 if (sub->color == omega_red)
953 fprintf (dump_file, "]");
955 fprintf (dump_file, "\n");
956 omega_print_vars (dump_file, pb);
959 for (e = pb->num_eqs - 1; e >= 0; e--)
961 eqn eqn = &(pb->eqs[e]);
963 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
965 if (dump_file && (dump_flags & TDF_DETAILS))
967 omega_print_eq (dump_file, pb, eqn);
968 fprintf (dump_file, "\n");
972 for (e = pb->num_geqs - 1; e >= 0; e--)
974 eqn eqn = &(pb->geqs[e]);
976 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
978 if (eqn->coef[var] && eqn->color == omega_red)
979 eqn->touched = 1;
981 if (dump_file && (dump_flags & TDF_DETAILS))
983 omega_print_geq (dump_file, pb, eqn);
984 fprintf (dump_file, "\n");
988 for (e = pb->num_subs - 1; e >= 0; e--)
990 eqn eqn = &(pb->subs[e]);
992 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
994 if (dump_file && (dump_flags & TDF_DETAILS))
996 fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
997 omega_print_term (dump_file, pb, eqn, 1);
998 fprintf (dump_file, "\n");
1002 if (dump_file && (dump_flags & TDF_DETAILS))
1003 fprintf (dump_file, "---\n\n");
1005 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1006 *found_black = true;
1009 /* Substitute in PB variable VAR with "C * SUB". */
1011 static void
1012 omega_substitute (omega_pb pb, eqn sub, int var, int c)
1014 int e, j, j0;
1015 int top_var = setup_packing (sub, pb->num_vars);
1017 if (dump_file && (dump_flags & TDF_DETAILS))
1019 fprintf (dump_file, "substituting using %s := ",
1020 omega_variable_to_str (pb, var));
1021 omega_print_term (dump_file, pb, sub, -c);
1022 fprintf (dump_file, "\n");
1023 omega_print_vars (dump_file, pb);
1026 if (top_var < 0)
1028 for (e = pb->num_eqs - 1; e >= 0; e--)
1029 pb->eqs[e].coef[var] = 0;
1031 for (e = pb->num_geqs - 1; e >= 0; e--)
1032 if (pb->geqs[e].coef[var] != 0)
1034 pb->geqs[e].touched = 1;
1035 pb->geqs[e].coef[var] = 0;
1038 for (e = pb->num_subs - 1; e >= 0; e--)
1039 pb->subs[e].coef[var] = 0;
1041 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1043 int k;
1044 eqn eqn = &(pb->subs[pb->num_subs++]);
1046 for (k = pb->num_vars; k >= 0; k--)
1047 eqn->coef[k] = 0;
1049 eqn->key = pb->var[var];
1050 eqn->color = omega_black;
1053 else if (top_var == 0 && packing[0] == 0)
1055 c = -sub->coef[0] * c;
1057 for (e = pb->num_eqs - 1; e >= 0; e--)
1059 pb->eqs[e].coef[0] += pb->eqs[e].coef[var] * c;
1060 pb->eqs[e].coef[var] = 0;
1063 for (e = pb->num_geqs - 1; e >= 0; e--)
1064 if (pb->geqs[e].coef[var] != 0)
1066 pb->geqs[e].coef[0] += pb->geqs[e].coef[var] * c;
1067 pb->geqs[e].coef[var] = 0;
1068 pb->geqs[e].touched = 1;
1071 for (e = pb->num_subs - 1; e >= 0; e--)
1073 pb->subs[e].coef[0] += pb->subs[e].coef[var] * c;
1074 pb->subs[e].coef[var] = 0;
1077 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1079 int k;
1080 eqn eqn = &(pb->subs[pb->num_subs++]);
1082 for (k = pb->num_vars; k >= 1; k--)
1083 eqn->coef[k] = 0;
1085 eqn->coef[0] = c;
1086 eqn->key = pb->var[var];
1087 eqn->color = omega_black;
1090 if (dump_file && (dump_flags & TDF_DETAILS))
1092 fprintf (dump_file, "---\n\n");
1093 omega_print_problem (dump_file, pb);
1094 fprintf (dump_file, "===\n\n");
1097 else
1099 for (e = pb->num_eqs - 1; e >= 0; e--)
1101 eqn eqn = &(pb->eqs[e]);
1102 int k = eqn->coef[var];
1104 if (k != 0)
1106 k = c * k;
1107 eqn->coef[var] = 0;
1109 for (j = top_var; j >= 0; j--)
1111 j0 = packing[j];
1112 eqn->coef[j0] -= sub->coef[j0] * k;
1116 if (dump_file && (dump_flags & TDF_DETAILS))
1118 omega_print_eq (dump_file, pb, eqn);
1119 fprintf (dump_file, "\n");
1123 for (e = pb->num_geqs - 1; e >= 0; e--)
1125 eqn eqn = &(pb->geqs[e]);
1126 int k = eqn->coef[var];
1128 if (k != 0)
1130 k = c * k;
1131 eqn->touched = 1;
1132 eqn->coef[var] = 0;
1134 for (j = top_var; j >= 0; j--)
1136 j0 = packing[j];
1137 eqn->coef[j0] -= sub->coef[j0] * k;
1141 if (dump_file && (dump_flags & TDF_DETAILS))
1143 omega_print_geq (dump_file, pb, eqn);
1144 fprintf (dump_file, "\n");
1148 for (e = pb->num_subs - 1; e >= 0; e--)
1150 eqn eqn = &(pb->subs[e]);
1151 int k = eqn->coef[var];
1153 if (k != 0)
1155 k = c * k;
1156 eqn->coef[var] = 0;
1158 for (j = top_var; j >= 0; j--)
1160 j0 = packing[j];
1161 eqn->coef[j0] -= sub->coef[j0] * k;
1165 if (dump_file && (dump_flags & TDF_DETAILS))
1167 fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
1168 omega_print_term (dump_file, pb, eqn, 1);
1169 fprintf (dump_file, "\n");
1173 if (dump_file && (dump_flags & TDF_DETAILS))
1175 fprintf (dump_file, "---\n\n");
1176 omega_print_problem (dump_file, pb);
1177 fprintf (dump_file, "===\n\n");
1180 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1182 int k;
1183 eqn eqn = &(pb->subs[pb->num_subs++]);
1184 c = -c;
1186 for (k = pb->num_vars; k >= 0; k--)
1187 eqn->coef[k] = c * (sub->coef[k]);
1189 eqn->key = pb->var[var];
1190 eqn->color = sub->color;
1195 /* Solve e = factor alpha for x_j and substitute. */
1197 static void
1198 omega_do_mod (omega_pb pb, int factor, int e, int j)
1200 int k, i;
1201 eqn eq = omega_alloc_eqns (0, 1);
1202 int nfactor;
1203 bool kill_j = false;
1205 omega_copy_eqn (eq, &pb->eqs[e], pb->num_vars);
1207 for (k = pb->num_vars; k >= 0; k--)
1209 eq->coef[k] = int_mod (eq->coef[k], factor);
1211 if (2 * eq->coef[k] >= factor)
1212 eq->coef[k] -= factor;
1215 nfactor = eq->coef[j];
1217 if (omega_safe_var_p (pb, j) && !omega_wildcard_p (pb, j))
1219 i = omega_add_new_wild_card (pb);
1220 eq->coef[pb->num_vars] = eq->coef[i];
1221 eq->coef[j] = 0;
1222 eq->coef[i] = -factor;
1223 kill_j = true;
1225 else
1227 eq->coef[j] = -factor;
1228 if (!omega_wildcard_p (pb, j))
1229 omega_name_wild_card (pb, j);
1232 omega_substitute (pb, eq, j, nfactor);
1234 for (k = pb->num_vars; k >= 0; k--)
1235 pb->eqs[e].coef[k] = pb->eqs[e].coef[k] / factor;
1237 if (kill_j)
1238 omega_delete_variable (pb, j);
1240 if (dump_file && (dump_flags & TDF_DETAILS))
1242 fprintf (dump_file, "Mod-ing and normalizing produces:\n");
1243 omega_print_problem (dump_file, pb);
1246 omega_free_eqns (eq, 1);
1249 /* Multiplies by -1 inequality E. */
1251 void
1252 omega_negate_geq (omega_pb pb, int e)
1254 int i;
1256 for (i = pb->num_vars; i >= 0; i--)
1257 pb->geqs[e].coef[i] *= -1;
1259 pb->geqs[e].coef[0]--;
1260 pb->geqs[e].touched = 1;
1263 /* Returns OMEGA_TRUE when problem PB has a solution. */
1265 static enum omega_result
1266 verify_omega_pb (omega_pb pb)
1268 enum omega_result result;
1269 int e;
1270 bool any_color = false;
1271 omega_pb tmp_problem = XNEW (struct omega_pb_d);
1273 omega_copy_problem (tmp_problem, pb);
1274 tmp_problem->safe_vars = 0;
1275 tmp_problem->num_subs = 0;
1277 for (e = pb->num_geqs - 1; e >= 0; e--)
1278 if (pb->geqs[e].color == omega_red)
1280 any_color = true;
1281 break;
1284 if (please_no_equalities_in_simplified_problems)
1285 any_color = true;
1287 if (any_color)
1288 original_problem = no_problem;
1289 else
1290 original_problem = pb;
1292 if (dump_file && (dump_flags & TDF_DETAILS))
1294 fprintf (dump_file, "verifying problem");
1296 if (any_color)
1297 fprintf (dump_file, " (color mode)");
1299 fprintf (dump_file, " :\n");
1300 omega_print_problem (dump_file, pb);
1303 result = omega_solve_problem (tmp_problem, omega_unknown);
1304 original_problem = no_problem;
1305 free (tmp_problem);
1307 if (dump_file && (dump_flags & TDF_DETAILS))
1309 if (result != omega_false)
1310 fprintf (dump_file, "verified problem\n");
1311 else
1312 fprintf (dump_file, "disproved problem\n");
1313 omega_print_problem (dump_file, pb);
1316 return result;
1319 /* Add a new equality to problem PB at last position E. */
1321 static void
1322 adding_equality_constraint (omega_pb pb, int e)
1324 if (original_problem != no_problem
1325 && original_problem != pb
1326 && !conservative)
1328 int i, j;
1329 int e2 = original_problem->num_eqs++;
1331 if (dump_file && (dump_flags & TDF_DETAILS))
1332 fprintf (dump_file,
1333 "adding equality constraint %d to outer problem\n", e2);
1334 omega_init_eqn_zero (&original_problem->eqs[e2],
1335 original_problem->num_vars);
1337 for (i = pb->num_vars; i >= 1; i--)
1339 for (j = original_problem->num_vars; j >= 1; j--)
1340 if (original_problem->var[j] == pb->var[i])
1341 break;
1343 if (j <= 0)
1345 if (dump_file && (dump_flags & TDF_DETAILS))
1346 fprintf (dump_file, "retracting\n");
1347 original_problem->num_eqs--;
1348 return;
1350 original_problem->eqs[e2].coef[j] = pb->eqs[e].coef[i];
1353 original_problem->eqs[e2].coef[0] = pb->eqs[e].coef[0];
1355 if (dump_file && (dump_flags & TDF_DETAILS))
1356 omega_print_problem (dump_file, original_problem);
1360 static int *fast_lookup;
1361 static int *fast_lookup_red;
1363 typedef enum {
1364 normalize_false,
1365 normalize_uncoupled,
1366 normalize_coupled
1367 } normalize_return_type;
1369 /* Normalizes PB by removing redundant constraints. Returns
1370 normalize_false when the constraints system has no solution,
1371 otherwise returns normalize_coupled or normalize_uncoupled. */
1373 static normalize_return_type
1374 normalize_omega_problem (omega_pb pb)
1376 int e, i, j, k, n_vars;
1377 int coupled_subscripts = 0;
1379 n_vars = pb->num_vars;
1381 for (e = 0; e < pb->num_geqs; e++)
1383 if (!pb->geqs[e].touched)
1385 if (!single_var_geq (&pb->geqs[e], n_vars))
1386 coupled_subscripts = 1;
1388 else
1390 int g, top_var, i0, hashCode;
1391 int *p = &packing[0];
1393 for (k = 1; k <= n_vars; k++)
1394 if (pb->geqs[e].coef[k])
1395 *(p++) = k;
1397 top_var = (p - &packing[0]) - 1;
1399 if (top_var == -1)
1401 if (pb->geqs[e].coef[0] < 0)
1403 if (dump_file && (dump_flags & TDF_DETAILS))
1405 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1406 fprintf (dump_file, "\nequations have no solution \n");
1408 return normalize_false;
1411 omega_delete_geq (pb, e, n_vars);
1412 e--;
1413 continue;
1415 else if (top_var == 0)
1417 int singlevar = packing[0];
1419 g = pb->geqs[e].coef[singlevar];
1421 if (g > 0)
1423 pb->geqs[e].coef[singlevar] = 1;
1424 pb->geqs[e].key = singlevar;
1426 else
1428 g = -g;
1429 pb->geqs[e].coef[singlevar] = -1;
1430 pb->geqs[e].key = -singlevar;
1433 if (g > 1)
1434 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1436 else
1438 int g2;
1439 int hash_key_multiplier = 31;
1441 coupled_subscripts = 1;
1442 i0 = top_var;
1443 i = packing[i0--];
1444 g = pb->geqs[e].coef[i];
1445 hashCode = g * (i + 3);
1447 if (g < 0)
1448 g = -g;
1450 for (; i0 >= 0; i0--)
1452 int x;
1454 i = packing[i0];
1455 x = pb->geqs[e].coef[i];
1456 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1458 if (x < 0)
1459 x = -x;
1461 if (x == 1)
1463 g = 1;
1464 i0--;
1465 break;
1467 else
1468 g = gcd (x, g);
1471 for (; i0 >= 0; i0--)
1473 int x;
1474 i = packing[i0];
1475 x = pb->geqs[e].coef[i];
1476 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1479 if (g > 1)
1481 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1482 i0 = top_var;
1483 i = packing[i0--];
1484 pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1485 hashCode = pb->geqs[e].coef[i] * (i + 3);
1487 for (; i0 >= 0; i0--)
1489 i = packing[i0];
1490 pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1491 hashCode = hashCode * hash_key_multiplier * (i + 3)
1492 + pb->geqs[e].coef[i];
1496 g2 = abs (hashCode);
1498 if (dump_file && (dump_flags & TDF_DETAILS))
1500 fprintf (dump_file, "Hash code = %d, eqn = ", hashCode);
1501 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1502 fprintf (dump_file, "\n");
1505 j = g2 % HASH_TABLE_SIZE;
1507 do {
1508 eqn proto = &(hash_master[j]);
1510 if (proto->touched == g2)
1512 if (proto->coef[0] == top_var)
1514 if (hashCode >= 0)
1515 for (i0 = top_var; i0 >= 0; i0--)
1517 i = packing[i0];
1519 if (pb->geqs[e].coef[i] != proto->coef[i])
1520 break;
1522 else
1523 for (i0 = top_var; i0 >= 0; i0--)
1525 i = packing[i0];
1527 if (pb->geqs[e].coef[i] != -proto->coef[i])
1528 break;
1531 if (i0 < 0)
1533 if (hashCode >= 0)
1534 pb->geqs[e].key = proto->key;
1535 else
1536 pb->geqs[e].key = -proto->key;
1537 break;
1541 else if (proto->touched < 0)
1543 omega_init_eqn_zero (proto, pb->num_vars);
1544 if (hashCode >= 0)
1545 for (i0 = top_var; i0 >= 0; i0--)
1547 i = packing[i0];
1548 proto->coef[i] = pb->geqs[e].coef[i];
1550 else
1551 for (i0 = top_var; i0 >= 0; i0--)
1553 i = packing[i0];
1554 proto->coef[i] = -pb->geqs[e].coef[i];
1557 proto->coef[0] = top_var;
1558 proto->touched = g2;
1560 if (dump_file && (dump_flags & TDF_DETAILS))
1561 fprintf (dump_file, " constraint key = %d\n",
1562 next_key);
1564 proto->key = next_key++;
1566 /* Too many hash keys generated. */
1567 gcc_assert (proto->key <= MAX_KEYS);
1569 if (hashCode >= 0)
1570 pb->geqs[e].key = proto->key;
1571 else
1572 pb->geqs[e].key = -proto->key;
1574 break;
1577 j = (j + 1) % HASH_TABLE_SIZE;
1578 } while (1);
1581 pb->geqs[e].touched = 0;
1585 int eKey = pb->geqs[e].key;
1586 int e2;
1587 if (e > 0)
1589 int cTerm = pb->geqs[e].coef[0];
1590 e2 = fast_lookup[MAX_KEYS - eKey];
1592 if (e2 < e && pb->geqs[e2].key == -eKey
1593 && pb->geqs[e2].color == omega_black)
1595 if (pb->geqs[e2].coef[0] < -cTerm)
1597 if (dump_file && (dump_flags & TDF_DETAILS))
1599 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1600 fprintf (dump_file, "\n");
1601 omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1602 fprintf (dump_file,
1603 "\nequations have no solution \n");
1605 return normalize_false;
1608 if (pb->geqs[e2].coef[0] == -cTerm
1609 && (create_color
1610 || pb->geqs[e].color == omega_black))
1612 omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1613 pb->num_vars);
1614 if (pb->geqs[e].color == omega_black)
1615 adding_equality_constraint (pb, pb->num_eqs);
1616 pb->num_eqs++;
1617 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1621 e2 = fast_lookup_red[MAX_KEYS - eKey];
1623 if (e2 < e && pb->geqs[e2].key == -eKey
1624 && pb->geqs[e2].color == omega_red)
1626 if (pb->geqs[e2].coef[0] < -cTerm)
1628 if (dump_file && (dump_flags & TDF_DETAILS))
1630 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1631 fprintf (dump_file, "\n");
1632 omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1633 fprintf (dump_file,
1634 "\nequations have no solution \n");
1636 return normalize_false;
1639 if (pb->geqs[e2].coef[0] == -cTerm && create_color)
1641 omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1642 pb->num_vars);
1643 pb->eqs[pb->num_eqs].color = omega_red;
1644 pb->num_eqs++;
1645 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1649 e2 = fast_lookup[MAX_KEYS + eKey];
1651 if (e2 < e && pb->geqs[e2].key == eKey
1652 && pb->geqs[e2].color == omega_black)
1654 if (pb->geqs[e2].coef[0] > cTerm)
1656 if (pb->geqs[e].color == omega_black)
1658 if (dump_file && (dump_flags & TDF_DETAILS))
1660 fprintf (dump_file,
1661 "Removing Redundant Equation: ");
1662 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1663 fprintf (dump_file, "\n");
1664 fprintf (dump_file,
1665 "[a] Made Redundant by: ");
1666 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1667 fprintf (dump_file, "\n");
1669 pb->geqs[e2].coef[0] = cTerm;
1670 omega_delete_geq (pb, e, n_vars);
1671 e--;
1672 continue;
1675 else
1677 if (dump_file && (dump_flags & TDF_DETAILS))
1679 fprintf (dump_file, "Removing Redundant Equation: ");
1680 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1681 fprintf (dump_file, "\n");
1682 fprintf (dump_file, "[b] Made Redundant by: ");
1683 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1684 fprintf (dump_file, "\n");
1686 omega_delete_geq (pb, e, n_vars);
1687 e--;
1688 continue;
1692 e2 = fast_lookup_red[MAX_KEYS + eKey];
1694 if (e2 < e && pb->geqs[e2].key == eKey
1695 && pb->geqs[e2].color == omega_red)
1697 if (pb->geqs[e2].coef[0] >= cTerm)
1699 if (dump_file && (dump_flags & TDF_DETAILS))
1701 fprintf (dump_file, "Removing Redundant Equation: ");
1702 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1703 fprintf (dump_file, "\n");
1704 fprintf (dump_file, "[c] Made Redundant by: ");
1705 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1706 fprintf (dump_file, "\n");
1708 pb->geqs[e2].coef[0] = cTerm;
1709 pb->geqs[e2].color = pb->geqs[e].color;
1711 else if (pb->geqs[e].color == omega_red)
1713 if (dump_file && (dump_flags & TDF_DETAILS))
1715 fprintf (dump_file, "Removing Redundant Equation: ");
1716 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1717 fprintf (dump_file, "\n");
1718 fprintf (dump_file, "[d] Made Redundant by: ");
1719 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1720 fprintf (dump_file, "\n");
1723 omega_delete_geq (pb, e, n_vars);
1724 e--;
1725 continue;
1730 if (pb->geqs[e].color == omega_red)
1731 fast_lookup_red[MAX_KEYS + eKey] = e;
1732 else
1733 fast_lookup[MAX_KEYS + eKey] = e;
1737 create_color = false;
1738 return coupled_subscripts ? normalize_coupled : normalize_uncoupled;
1741 /* Divide the coefficients of EQN by their gcd. N_VARS is the number
1742 of variables in EQN. */
1744 static inline void
1745 divide_eqn_by_gcd (eqn eqn, int n_vars)
1747 int var, g = 0;
1749 for (var = n_vars; var >= 0; var--)
1750 g = gcd (abs (eqn->coef[var]), g);
1752 if (g)
1753 for (var = n_vars; var >= 0; var--)
1754 eqn->coef[var] = eqn->coef[var] / g;
1757 /* Rewrite some non-safe variables in function of protected
1758 wildcard variables. */
1760 static void
1761 cleanout_wildcards (omega_pb pb)
1763 int e, i, j;
1764 int n_vars = pb->num_vars;
1765 bool renormalize = false;
1767 for (e = pb->num_eqs - 1; e >= 0; e--)
1768 for (i = n_vars; !omega_safe_var_p (pb, i); i--)
1769 if (pb->eqs[e].coef[i] != 0)
1771 /* i is the last nonzero non-safe variable. */
1773 for (j = i - 1; !omega_safe_var_p (pb, j); j--)
1774 if (pb->eqs[e].coef[j] != 0)
1775 break;
1777 /* j is the next nonzero non-safe variable, or points
1778 to a safe variable: it is then a wildcard variable. */
1780 /* Clean it out. */
1781 if (omega_safe_var_p (pb, j))
1783 eqn sub = &(pb->eqs[e]);
1784 int c = pb->eqs[e].coef[i];
1785 int a = abs (c);
1786 int e2;
1788 if (dump_file && (dump_flags & TDF_DETAILS))
1790 fprintf (dump_file,
1791 "Found a single wild card equality: ");
1792 omega_print_eq (dump_file, pb, &pb->eqs[e]);
1793 fprintf (dump_file, "\n");
1794 omega_print_problem (dump_file, pb);
1797 for (e2 = pb->num_eqs - 1; e2 >= 0; e2--)
1798 if (e != e2 && pb->eqs[e2].coef[i]
1799 && (pb->eqs[e2].color == omega_red
1800 || (pb->eqs[e2].color == omega_black
1801 && pb->eqs[e].color == omega_black)))
1803 eqn eqn = &(pb->eqs[e2]);
1804 int var, k;
1806 for (var = n_vars; var >= 0; var--)
1807 eqn->coef[var] *= a;
1809 k = eqn->coef[i];
1811 for (var = n_vars; var >= 0; var--)
1812 eqn->coef[var] -= sub->coef[var] * k / c;
1814 eqn->coef[i] = 0;
1815 divide_eqn_by_gcd (eqn, n_vars);
1818 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
1819 if (pb->geqs[e2].coef[i]
1820 && (pb->geqs[e2].color == omega_red
1821 || (pb->eqs[e].color == omega_black
1822 && pb->geqs[e2].color == omega_black)))
1824 eqn eqn = &(pb->geqs[e2]);
1825 int var, k;
1827 for (var = n_vars; var >= 0; var--)
1828 eqn->coef[var] *= a;
1830 k = eqn->coef[i];
1832 for (var = n_vars; var >= 0; var--)
1833 eqn->coef[var] -= sub->coef[var] * k / c;
1835 eqn->coef[i] = 0;
1836 eqn->touched = 1;
1837 renormalize = true;
1840 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
1841 if (pb->subs[e2].coef[i]
1842 && (pb->subs[e2].color == omega_red
1843 || (pb->subs[e2].color == omega_black
1844 && pb->eqs[e].color == omega_black)))
1846 eqn eqn = &(pb->subs[e2]);
1847 int var, k;
1849 for (var = n_vars; var >= 0; var--)
1850 eqn->coef[var] *= a;
1852 k = eqn->coef[i];
1854 for (var = n_vars; var >= 0; var--)
1855 eqn->coef[var] -= sub->coef[var] * k / c;
1857 eqn->coef[i] = 0;
1858 divide_eqn_by_gcd (eqn, n_vars);
1861 if (dump_file && (dump_flags & TDF_DETAILS))
1863 fprintf (dump_file, "cleaned-out wildcard: ");
1864 omega_print_problem (dump_file, pb);
1866 break;
1870 if (renormalize)
1871 normalize_omega_problem (pb);
1874 /* Make variable IDX unprotected in PB, by swapping its index at the
1875 PB->safe_vars rank. */
1877 static inline void
1878 omega_unprotect_1 (omega_pb pb, int *idx, bool *unprotect)
1880 /* If IDX is protected... */
1881 if (*idx < pb->safe_vars)
1883 /* ... swap its index with the last non protected index. */
1884 int j = pb->safe_vars;
1885 int e;
1887 for (e = pb->num_geqs - 1; e >= 0; e--)
1889 pb->geqs[e].touched = 1;
1890 std::swap (pb->geqs[e].coef[*idx], pb->geqs[e].coef[j]);
1893 for (e = pb->num_eqs - 1; e >= 0; e--)
1894 std::swap (pb->eqs[e].coef[*idx], pb->eqs[e].coef[j]);
1896 for (e = pb->num_subs - 1; e >= 0; e--)
1897 std::swap (pb->subs[e].coef[*idx], pb->subs[e].coef[j]);
1899 if (unprotect)
1900 std::swap (unprotect[*idx], unprotect[j]);
1902 std::swap (pb->var[*idx], pb->var[j]);
1903 pb->forwarding_address[pb->var[*idx]] = *idx;
1904 pb->forwarding_address[pb->var[j]] = j;
1905 (*idx)--;
1908 /* The variable at pb->safe_vars is also unprotected now. */
1909 pb->safe_vars--;
1912 /* During the Fourier-Motzkin elimination some variables are
1913 substituted with other variables. This function resurrects the
1914 substituted variables in PB. */
1916 static void
1917 resurrect_subs (omega_pb pb)
1919 if (pb->num_subs > 0
1920 && please_no_equalities_in_simplified_problems == 0)
1922 int i, e, m;
1924 if (dump_file && (dump_flags & TDF_DETAILS))
1926 fprintf (dump_file,
1927 "problem reduced, bringing variables back to life\n");
1928 omega_print_problem (dump_file, pb);
1931 for (i = 1; omega_safe_var_p (pb, i); i++)
1932 if (omega_wildcard_p (pb, i))
1933 omega_unprotect_1 (pb, &i, NULL);
1935 m = pb->num_subs;
1937 for (e = pb->num_geqs - 1; e >= 0; e--)
1938 if (single_var_geq (&pb->geqs[e], pb->num_vars))
1940 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
1941 pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m);
1943 else
1945 pb->geqs[e].touched = 1;
1946 pb->geqs[e].key = 0;
1949 for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--)
1951 pb->var[i + m] = pb->var[i];
1953 for (e = pb->num_geqs - 1; e >= 0; e--)
1954 pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i];
1956 for (e = pb->num_eqs - 1; e >= 0; e--)
1957 pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i];
1959 for (e = pb->num_subs - 1; e >= 0; e--)
1960 pb->subs[e].coef[i + m] = pb->subs[e].coef[i];
1963 for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--)
1965 for (e = pb->num_geqs - 1; e >= 0; e--)
1966 pb->geqs[e].coef[i] = 0;
1968 for (e = pb->num_eqs - 1; e >= 0; e--)
1969 pb->eqs[e].coef[i] = 0;
1971 for (e = pb->num_subs - 1; e >= 0; e--)
1972 pb->subs[e].coef[i] = 0;
1975 pb->num_vars += m;
1977 for (e = pb->num_subs - 1; e >= 0; e--)
1979 pb->var[pb->safe_vars + 1 + e] = pb->subs[e].key;
1980 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e]),
1981 pb->num_vars);
1982 pb->eqs[pb->num_eqs].coef[pb->safe_vars + 1 + e] = -1;
1983 pb->eqs[pb->num_eqs].color = omega_black;
1985 if (dump_file && (dump_flags & TDF_DETAILS))
1987 fprintf (dump_file, "brought back: ");
1988 omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]);
1989 fprintf (dump_file, "\n");
1992 pb->num_eqs++;
1993 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1996 pb->safe_vars += m;
1997 pb->num_subs = 0;
1999 if (dump_file && (dump_flags & TDF_DETAILS))
2001 fprintf (dump_file, "variables brought back to life\n");
2002 omega_print_problem (dump_file, pb);
2005 cleanout_wildcards (pb);
2009 static inline bool
2010 implies (unsigned int a, unsigned int b)
2012 return (a == (a & b));
2015 /* Eliminate redundant equations in PB. When EXPENSIVE is true, an
2016 extra step is performed. Returns omega_false when there exist no
2017 solution, omega_true otherwise. */
2019 enum omega_result
2020 omega_eliminate_redundant (omega_pb pb, bool expensive)
2022 int c, e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3;
2023 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2024 omega_pb tmp_problem;
2026 /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations. */
2027 unsigned int *peqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2028 unsigned int *zeqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2029 unsigned int *neqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2031 /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
2032 unsigned int pp, pz, pn;
2034 if (dump_file && (dump_flags & TDF_DETAILS))
2036 fprintf (dump_file, "in eliminate Redundant:\n");
2037 omega_print_problem (dump_file, pb);
2040 for (e = pb->num_geqs - 1; e >= 0; e--)
2042 int tmp = 1;
2044 is_dead[e] = false;
2045 peqs[e] = zeqs[e] = neqs[e] = 0;
2047 for (i = pb->num_vars; i >= 1; i--)
2049 if (pb->geqs[e].coef[i] > 0)
2050 peqs[e] |= tmp;
2051 else if (pb->geqs[e].coef[i] < 0)
2052 neqs[e] |= tmp;
2053 else
2054 zeqs[e] |= tmp;
2056 tmp <<= 1;
2061 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2062 if (!is_dead[e1])
2063 for (e2 = e1 - 1; e2 >= 0; e2--)
2064 if (!is_dead[e2])
2066 for (p = pb->num_vars; p > 1; p--)
2067 for (q = p - 1; q > 0; q--)
2068 if ((alpha = pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q]
2069 - pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]) != 0)
2070 goto foundPQ;
2072 continue;
2074 foundPQ:
2075 pz = ((zeqs[e1] & zeqs[e2]) | (peqs[e1] & neqs[e2])
2076 | (neqs[e1] & peqs[e2]));
2077 pp = peqs[e1] | peqs[e2];
2078 pn = neqs[e1] | neqs[e2];
2080 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2081 if (e3 != e1 && e3 != e2)
2083 if (!implies (zeqs[e3], pz))
2084 goto nextE3;
2086 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2087 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2088 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2089 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2090 alpha3 = alpha;
2092 if (alpha1 * alpha2 <= 0)
2093 goto nextE3;
2095 if (alpha1 < 0)
2097 alpha1 = -alpha1;
2098 alpha2 = -alpha2;
2099 alpha3 = -alpha3;
2102 if (alpha3 > 0)
2104 /* Trying to prove e3 is redundant. */
2105 if (!implies (peqs[e3], pp)
2106 || !implies (neqs[e3], pn))
2107 goto nextE3;
2109 if (pb->geqs[e3].color == omega_black
2110 && (pb->geqs[e1].color == omega_red
2111 || pb->geqs[e2].color == omega_red))
2112 goto nextE3;
2114 for (k = pb->num_vars; k >= 1; k--)
2115 if (alpha3 * pb->geqs[e3].coef[k]
2116 != (alpha1 * pb->geqs[e1].coef[k]
2117 + alpha2 * pb->geqs[e2].coef[k]))
2118 goto nextE3;
2120 c = (alpha1 * pb->geqs[e1].coef[0]
2121 + alpha2 * pb->geqs[e2].coef[0]);
2123 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2125 if (dump_file && (dump_flags & TDF_DETAILS))
2127 fprintf (dump_file,
2128 "found redundant inequality\n");
2129 fprintf (dump_file,
2130 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2131 alpha1, alpha2, alpha3);
2133 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2134 fprintf (dump_file, "\n");
2135 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2136 fprintf (dump_file, "\n=> ");
2137 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2138 fprintf (dump_file, "\n\n");
2141 is_dead[e3] = true;
2144 else
2146 /* Trying to prove e3 <= 0 and therefore e3 = 0,
2147 or trying to prove e3 < 0, and therefore the
2148 problem has no solutions. */
2149 if (!implies (peqs[e3], pn)
2150 || !implies (neqs[e3], pp))
2151 goto nextE3;
2153 if (pb->geqs[e1].color == omega_red
2154 || pb->geqs[e2].color == omega_red
2155 || pb->geqs[e3].color == omega_red)
2156 goto nextE3;
2158 /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
2159 for (k = pb->num_vars; k >= 1; k--)
2160 if (alpha3 * pb->geqs[e3].coef[k]
2161 != (alpha1 * pb->geqs[e1].coef[k]
2162 + alpha2 * pb->geqs[e2].coef[k]))
2163 goto nextE3;
2165 c = (alpha1 * pb->geqs[e1].coef[0]
2166 + alpha2 * pb->geqs[e2].coef[0]);
2168 if (c < alpha3 * (pb->geqs[e3].coef[0]))
2170 /* We just proved e3 < 0, so no solutions exist. */
2171 if (dump_file && (dump_flags & TDF_DETAILS))
2173 fprintf (dump_file,
2174 "found implied over tight inequality\n");
2175 fprintf (dump_file,
2176 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2177 alpha1, alpha2, -alpha3);
2178 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2179 fprintf (dump_file, "\n");
2180 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2181 fprintf (dump_file, "\n=> not ");
2182 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2183 fprintf (dump_file, "\n\n");
2185 free (is_dead);
2186 free (peqs);
2187 free (zeqs);
2188 free (neqs);
2189 return omega_false;
2191 else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
2193 /* We just proved that e3 <=0, so e3 = 0. */
2194 if (dump_file && (dump_flags & TDF_DETAILS))
2196 fprintf (dump_file,
2197 "found implied tight inequality\n");
2198 fprintf (dump_file,
2199 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2200 alpha1, alpha2, -alpha3);
2201 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2202 fprintf (dump_file, "\n");
2203 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2204 fprintf (dump_file, "\n=> inverse ");
2205 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2206 fprintf (dump_file, "\n\n");
2209 omega_copy_eqn (&pb->eqs[pb->num_eqs++],
2210 &pb->geqs[e3], pb->num_vars);
2211 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2212 adding_equality_constraint (pb, pb->num_eqs - 1);
2213 is_dead[e3] = true;
2216 nextE3:;
2220 /* Delete the inequalities that were marked as dead. */
2221 for (e = pb->num_geqs - 1; e >= 0; e--)
2222 if (is_dead[e])
2223 omega_delete_geq (pb, e, pb->num_vars);
2225 if (!expensive)
2226 goto eliminate_redundant_done;
2228 tmp_problem = XNEW (struct omega_pb_d);
2229 conservative++;
2231 for (e = pb->num_geqs - 1; e >= 0; e--)
2233 if (dump_file && (dump_flags & TDF_DETAILS))
2235 fprintf (dump_file,
2236 "checking equation %d to see if it is redundant: ", e);
2237 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2238 fprintf (dump_file, "\n");
2241 omega_copy_problem (tmp_problem, pb);
2242 omega_negate_geq (tmp_problem, e);
2243 tmp_problem->safe_vars = 0;
2244 tmp_problem->variables_freed = false;
2246 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2247 omega_delete_geq (pb, e, pb->num_vars);
2250 free (tmp_problem);
2251 conservative--;
2253 if (!omega_reduce_with_subs)
2255 resurrect_subs (pb);
2256 gcc_assert (please_no_equalities_in_simplified_problems
2257 || pb->num_subs == 0);
2260 eliminate_redundant_done:
2261 free (is_dead);
2262 free (peqs);
2263 free (zeqs);
2264 free (neqs);
2265 return omega_true;
2268 /* For each inequality that has coefficients bigger than 20, try to
2269 create a new constraint that cannot be derived from the original
2270 constraint and that has smaller coefficients. Add the new
2271 constraint at the end of geqs. Return the number of inequalities
2272 that have been added to PB. */
2274 static int
2275 smooth_weird_equations (omega_pb pb)
2277 int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
2278 int c;
2279 int v;
2280 int result = 0;
2282 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2283 if (pb->geqs[e1].color == omega_black)
2285 int g = 999999;
2287 for (v = pb->num_vars; v >= 1; v--)
2288 if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g)
2289 g = abs (pb->geqs[e1].coef[v]);
2291 /* Magic number. */
2292 if (g > 20)
2294 e3 = pb->num_geqs;
2296 for (v = pb->num_vars; v >= 1; v--)
2297 pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2,
2300 pb->geqs[e3].color = omega_black;
2301 pb->geqs[e3].touched = 1;
2302 /* Magic number. */
2303 pb->geqs[e3].coef[0] = 9997;
2305 if (dump_file && (dump_flags & TDF_DETAILS))
2307 fprintf (dump_file, "Checking to see if we can derive: ");
2308 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2309 fprintf (dump_file, "\n from: ");
2310 omega_print_geq (dump_file, pb, &pb->geqs[e1]);
2311 fprintf (dump_file, "\n");
2314 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
2315 if (e1 != e2 && pb->geqs[e2].color == omega_black)
2317 for (p = pb->num_vars; p > 1; p--)
2319 for (q = p - 1; q > 0; q--)
2321 alpha =
2322 (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] -
2323 pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]);
2324 if (alpha != 0)
2325 goto foundPQ;
2328 continue;
2330 foundPQ:
2332 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2333 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2334 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2335 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2336 alpha3 = alpha;
2338 if (alpha1 * alpha2 <= 0)
2339 continue;
2341 if (alpha1 < 0)
2343 alpha1 = -alpha1;
2344 alpha2 = -alpha2;
2345 alpha3 = -alpha3;
2348 if (alpha3 > 0)
2350 /* Try to prove e3 is redundant: verify
2351 alpha1*v1 + alpha2*v2 = alpha3*v3. */
2352 for (k = pb->num_vars; k >= 1; k--)
2353 if (alpha3 * pb->geqs[e3].coef[k]
2354 != (alpha1 * pb->geqs[e1].coef[k]
2355 + alpha2 * pb->geqs[e2].coef[k]))
2356 goto nextE2;
2358 c = alpha1 * pb->geqs[e1].coef[0]
2359 + alpha2 * pb->geqs[e2].coef[0];
2361 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2362 pb->geqs[e3].coef[0] = int_div (c, alpha3);
2364 nextE2:;
2367 if (pb->geqs[e3].coef[0] < 9997)
2369 result++;
2370 pb->num_geqs++;
2372 if (dump_file && (dump_flags & TDF_DETAILS))
2374 fprintf (dump_file,
2375 "Smoothing weird equations; adding:\n");
2376 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2377 fprintf (dump_file, "\nto:\n");
2378 omega_print_problem (dump_file, pb);
2379 fprintf (dump_file, "\n\n");
2384 return result;
2387 /* Replace tuples of inequalities, that define upper and lower half
2388 spaces, with an equation. */
2390 static void
2391 coalesce (omega_pb pb)
2393 int e, e2;
2394 int colors = 0;
2395 bool *is_dead;
2396 int found_something = 0;
2398 for (e = 0; e < pb->num_geqs; e++)
2399 if (pb->geqs[e].color == omega_red)
2400 colors++;
2402 if (colors < 2)
2403 return;
2405 is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2407 for (e = 0; e < pb->num_geqs; e++)
2408 is_dead[e] = false;
2410 for (e = 0; e < pb->num_geqs; e++)
2411 if (pb->geqs[e].color == omega_red
2412 && !pb->geqs[e].touched)
2413 for (e2 = e + 1; e2 < pb->num_geqs; e2++)
2414 if (!pb->geqs[e2].touched
2415 && pb->geqs[e].key == -pb->geqs[e2].key
2416 && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0]
2417 && pb->geqs[e2].color == omega_red)
2419 omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e],
2420 pb->num_vars);
2421 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2422 found_something++;
2423 is_dead[e] = true;
2424 is_dead[e2] = true;
2427 for (e = pb->num_geqs - 1; e >= 0; e--)
2428 if (is_dead[e])
2429 omega_delete_geq (pb, e, pb->num_vars);
2431 if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
2433 fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
2434 found_something);
2435 omega_print_problem (dump_file, pb);
2438 free (is_dead);
2441 /* Eliminate red inequalities from PB. When ELIMINATE_ALL is
2442 true, continue to eliminate all the red inequalities. */
2444 void
2445 omega_eliminate_red (omega_pb pb, bool eliminate_all)
2447 int e, e2, e3, i, j, k, a, alpha1, alpha2;
2448 int c = 0;
2449 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2450 int dead_count = 0;
2451 int red_found;
2452 omega_pb tmp_problem;
2454 if (dump_file && (dump_flags & TDF_DETAILS))
2456 fprintf (dump_file, "in eliminate RED:\n");
2457 omega_print_problem (dump_file, pb);
2460 if (pb->num_eqs > 0)
2461 omega_simplify_problem (pb);
2463 for (e = pb->num_geqs - 1; e >= 0; e--)
2464 is_dead[e] = false;
2466 for (e = pb->num_geqs - 1; e >= 0; e--)
2467 if (pb->geqs[e].color == omega_black && !is_dead[e])
2468 for (e2 = e - 1; e2 >= 0; e2--)
2469 if (pb->geqs[e2].color == omega_black
2470 && !is_dead[e2])
2472 a = 0;
2474 for (i = pb->num_vars; i > 1; i--)
2475 for (j = i - 1; j > 0; j--)
2476 if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j]
2477 - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0)
2478 goto found_pair;
2480 continue;
2482 found_pair:
2483 if (dump_file && (dump_flags & TDF_DETAILS))
2485 fprintf (dump_file,
2486 "found two equations to combine, i = %s, ",
2487 omega_variable_to_str (pb, i));
2488 fprintf (dump_file, "j = %s, alpha = %d\n",
2489 omega_variable_to_str (pb, j), a);
2490 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2491 fprintf (dump_file, "\n");
2492 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2493 fprintf (dump_file, "\n");
2496 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2497 if (pb->geqs[e3].color == omega_red)
2499 alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i]
2500 - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]);
2501 alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i]
2502 - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]);
2504 if ((a > 0 && alpha1 > 0 && alpha2 > 0)
2505 || (a < 0 && alpha1 < 0 && alpha2 < 0))
2507 if (dump_file && (dump_flags & TDF_DETAILS))
2509 fprintf (dump_file,
2510 "alpha1 = %d, alpha2 = %d;"
2511 "comparing against: ",
2512 alpha1, alpha2);
2513 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2514 fprintf (dump_file, "\n");
2517 for (k = pb->num_vars; k >= 0; k--)
2519 c = (alpha1 * pb->geqs[e].coef[k]
2520 + alpha2 * pb->geqs[e2].coef[k]);
2522 if (c != a * pb->geqs[e3].coef[k])
2523 break;
2525 if (dump_file && (dump_flags & TDF_DETAILS) && k > 0)
2526 fprintf (dump_file, " %s: %d, %d\n",
2527 omega_variable_to_str (pb, k), c,
2528 a * pb->geqs[e3].coef[k]);
2531 if (k < 0
2532 || (k == 0 &&
2533 ((a > 0 && c < a * pb->geqs[e3].coef[k])
2534 || (a < 0 && c > a * pb->geqs[e3].coef[k]))))
2536 if (dump_file && (dump_flags & TDF_DETAILS))
2538 dead_count++;
2539 fprintf (dump_file,
2540 "red equation#%d is dead "
2541 "(%d dead so far, %d remain)\n",
2542 e3, dead_count,
2543 pb->num_geqs - dead_count);
2544 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2545 fprintf (dump_file, "\n");
2546 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2547 fprintf (dump_file, "\n");
2548 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2549 fprintf (dump_file, "\n");
2551 is_dead[e3] = true;
2557 for (e = pb->num_geqs - 1; e >= 0; e--)
2558 if (is_dead[e])
2559 omega_delete_geq (pb, e, pb->num_vars);
2561 free (is_dead);
2563 if (dump_file && (dump_flags & TDF_DETAILS))
2565 fprintf (dump_file, "in eliminate RED, easy tests done:\n");
2566 omega_print_problem (dump_file, pb);
2569 for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
2570 if (pb->geqs[e].color == omega_red)
2572 red_found = 1;
2573 break;
2576 if (!red_found)
2578 if (dump_file && (dump_flags & TDF_DETAILS))
2579 fprintf (dump_file, "fast checks worked\n");
2581 if (!omega_reduce_with_subs)
2582 gcc_assert (please_no_equalities_in_simplified_problems
2583 || pb->num_subs == 0);
2585 return;
2588 if (!omega_verify_simplification
2589 && verify_omega_pb (pb) == omega_false)
2590 return;
2592 conservative++;
2593 tmp_problem = XNEW (struct omega_pb_d);
2595 for (e = pb->num_geqs - 1; e >= 0; e--)
2596 if (pb->geqs[e].color == omega_red)
2598 if (dump_file && (dump_flags & TDF_DETAILS))
2600 fprintf (dump_file,
2601 "checking equation %d to see if it is redundant: ", e);
2602 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2603 fprintf (dump_file, "\n");
2606 omega_copy_problem (tmp_problem, pb);
2607 omega_negate_geq (tmp_problem, e);
2608 tmp_problem->safe_vars = 0;
2609 tmp_problem->variables_freed = false;
2610 tmp_problem->num_subs = 0;
2612 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2614 if (dump_file && (dump_flags & TDF_DETAILS))
2615 fprintf (dump_file, "it is redundant\n");
2616 omega_delete_geq (pb, e, pb->num_vars);
2618 else
2620 if (dump_file && (dump_flags & TDF_DETAILS))
2621 fprintf (dump_file, "it is not redundant\n");
2623 if (!eliminate_all)
2625 if (dump_file && (dump_flags & TDF_DETAILS))
2626 fprintf (dump_file, "no need to check other red equations\n");
2627 break;
2632 conservative--;
2633 free (tmp_problem);
2634 /* omega_simplify_problem (pb); */
2636 if (!omega_reduce_with_subs)
2637 gcc_assert (please_no_equalities_in_simplified_problems
2638 || pb->num_subs == 0);
2641 /* Transform some wildcard variables to non-safe variables. */
2643 static void
2644 chain_unprotect (omega_pb pb)
2646 int i, e;
2647 bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
2649 for (i = 1; omega_safe_var_p (pb, i); i++)
2651 unprotect[i] = omega_wildcard_p (pb, i);
2653 for (e = pb->num_subs - 1; e >= 0; e--)
2654 if (pb->subs[e].coef[i])
2655 unprotect[i] = false;
2658 if (dump_file && (dump_flags & TDF_DETAILS))
2660 fprintf (dump_file, "Doing chain reaction unprotection\n");
2661 omega_print_problem (dump_file, pb);
2663 for (i = 1; omega_safe_var_p (pb, i); i++)
2664 if (unprotect[i])
2665 fprintf (dump_file, "unprotecting %s\n",
2666 omega_variable_to_str (pb, i));
2669 for (i = 1; omega_safe_var_p (pb, i); i++)
2670 if (unprotect[i])
2671 omega_unprotect_1 (pb, &i, unprotect);
2673 if (dump_file && (dump_flags & TDF_DETAILS))
2675 fprintf (dump_file, "After chain reactions\n");
2676 omega_print_problem (dump_file, pb);
2679 free (unprotect);
2682 /* Reduce problem PB. */
2684 static void
2685 omega_problem_reduced (omega_pb pb)
2687 if (omega_verify_simplification
2688 && !in_approximate_mode
2689 && verify_omega_pb (pb) == omega_false)
2690 return;
2692 if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
2693 && !omega_eliminate_redundant (pb, true))
2694 return;
2696 omega_found_reduction = omega_true;
2698 if (!please_no_equalities_in_simplified_problems)
2699 coalesce (pb);
2701 if (omega_reduce_with_subs
2702 || please_no_equalities_in_simplified_problems)
2703 chain_unprotect (pb);
2704 else
2705 resurrect_subs (pb);
2707 if (!return_single_result)
2709 int i;
2711 for (i = 1; omega_safe_var_p (pb, i); i++)
2712 pb->forwarding_address[pb->var[i]] = i;
2714 for (i = 0; i < pb->num_subs; i++)
2715 pb->forwarding_address[pb->subs[i].key] = -i - 1;
2717 (*omega_when_reduced) (pb);
2720 if (dump_file && (dump_flags & TDF_DETAILS))
2722 fprintf (dump_file, "-------------------------------------------\n");
2723 fprintf (dump_file, "problem reduced:\n");
2724 omega_print_problem (dump_file, pb);
2725 fprintf (dump_file, "-------------------------------------------\n");
2729 /* Eliminates all the free variables for problem PB, that is all the
2730 variables from FV to PB->NUM_VARS. */
2732 static void
2733 omega_free_eliminations (omega_pb pb, int fv)
2735 bool try_again = true;
2736 int i, e, e2;
2737 int n_vars = pb->num_vars;
2739 while (try_again)
2741 try_again = false;
2743 for (i = n_vars; i > fv; i--)
2745 for (e = pb->num_geqs - 1; e >= 0; e--)
2746 if (pb->geqs[e].coef[i])
2747 break;
2749 if (e < 0)
2750 e2 = e;
2751 else if (pb->geqs[e].coef[i] > 0)
2753 for (e2 = e - 1; e2 >= 0; e2--)
2754 if (pb->geqs[e2].coef[i] < 0)
2755 break;
2757 else
2759 for (e2 = e - 1; e2 >= 0; e2--)
2760 if (pb->geqs[e2].coef[i] > 0)
2761 break;
2764 if (e2 < 0)
2766 int e3;
2767 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2768 if (pb->subs[e3].coef[i])
2769 break;
2771 if (e3 >= 0)
2772 continue;
2774 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2775 if (pb->eqs[e3].coef[i])
2776 break;
2778 if (e3 >= 0)
2779 continue;
2781 if (dump_file && (dump_flags & TDF_DETAILS))
2782 fprintf (dump_file, "a free elimination of %s\n",
2783 omega_variable_to_str (pb, i));
2785 if (e >= 0)
2787 omega_delete_geq (pb, e, n_vars);
2789 for (e--; e >= 0; e--)
2790 if (pb->geqs[e].coef[i])
2791 omega_delete_geq (pb, e, n_vars);
2793 try_again = (i < n_vars);
2796 omega_delete_variable (pb, i);
2797 n_vars = pb->num_vars;
2802 if (dump_file && (dump_flags & TDF_DETAILS))
2804 fprintf (dump_file, "\nafter free eliminations:\n");
2805 omega_print_problem (dump_file, pb);
2806 fprintf (dump_file, "\n");
2810 /* Do free red eliminations. */
2812 static void
2813 free_red_eliminations (omega_pb pb)
2815 bool try_again = true;
2816 int i, e, e2;
2817 int n_vars = pb->num_vars;
2818 bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2819 bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2820 bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS);
2822 for (i = n_vars; i > 0; i--)
2824 is_red_var[i] = false;
2825 is_dead_var[i] = false;
2828 for (e = pb->num_geqs - 1; e >= 0; e--)
2830 is_dead_geq[e] = false;
2832 if (pb->geqs[e].color == omega_red)
2833 for (i = n_vars; i > 0; i--)
2834 if (pb->geqs[e].coef[i] != 0)
2835 is_red_var[i] = true;
2838 while (try_again)
2840 try_again = false;
2841 for (i = n_vars; i > 0; i--)
2842 if (!is_red_var[i] && !is_dead_var[i])
2844 for (e = pb->num_geqs - 1; e >= 0; e--)
2845 if (!is_dead_geq[e] && pb->geqs[e].coef[i])
2846 break;
2848 if (e < 0)
2849 e2 = e;
2850 else if (pb->geqs[e].coef[i] > 0)
2852 for (e2 = e - 1; e2 >= 0; e2--)
2853 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
2854 break;
2856 else
2858 for (e2 = e - 1; e2 >= 0; e2--)
2859 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
2860 break;
2863 if (e2 < 0)
2865 int e3;
2866 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2867 if (pb->subs[e3].coef[i])
2868 break;
2870 if (e3 >= 0)
2871 continue;
2873 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2874 if (pb->eqs[e3].coef[i])
2875 break;
2877 if (e3 >= 0)
2878 continue;
2880 if (dump_file && (dump_flags & TDF_DETAILS))
2881 fprintf (dump_file, "a free red elimination of %s\n",
2882 omega_variable_to_str (pb, i));
2884 for (; e >= 0; e--)
2885 if (pb->geqs[e].coef[i])
2886 is_dead_geq[e] = true;
2888 try_again = true;
2889 is_dead_var[i] = true;
2894 for (e = pb->num_geqs - 1; e >= 0; e--)
2895 if (is_dead_geq[e])
2896 omega_delete_geq (pb, e, n_vars);
2898 for (i = n_vars; i > 0; i--)
2899 if (is_dead_var[i])
2900 omega_delete_variable (pb, i);
2902 if (dump_file && (dump_flags & TDF_DETAILS))
2904 fprintf (dump_file, "\nafter free red eliminations:\n");
2905 omega_print_problem (dump_file, pb);
2906 fprintf (dump_file, "\n");
2909 free (is_red_var);
2910 free (is_dead_var);
2911 free (is_dead_geq);
2914 /* For equation EQ of the form "0 = EQN", insert in PB two
2915 inequalities "0 <= EQN" and "0 <= -EQN". */
2917 void
2918 omega_convert_eq_to_geqs (omega_pb pb, int eq)
2920 int i;
2922 if (dump_file && (dump_flags & TDF_DETAILS))
2923 fprintf (dump_file, "Converting Eq to Geqs\n");
2925 /* Insert "0 <= EQN". */
2926 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2927 pb->geqs[pb->num_geqs].touched = 1;
2928 pb->num_geqs++;
2930 /* Insert "0 <= -EQN". */
2931 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2932 pb->geqs[pb->num_geqs].touched = 1;
2934 for (i = 0; i <= pb->num_vars; i++)
2935 pb->geqs[pb->num_geqs].coef[i] *= -1;
2937 pb->num_geqs++;
2939 if (dump_file && (dump_flags & TDF_DETAILS))
2940 omega_print_problem (dump_file, pb);
2943 /* Eliminates variable I from PB. */
2945 static void
2946 omega_do_elimination (omega_pb pb, int e, int i)
2948 eqn sub = omega_alloc_eqns (0, 1);
2949 int c;
2950 int n_vars = pb->num_vars;
2952 if (dump_file && (dump_flags & TDF_DETAILS))
2953 fprintf (dump_file, "eliminating variable %s\n",
2954 omega_variable_to_str (pb, i));
2956 omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars);
2957 c = sub->coef[i];
2958 sub->coef[i] = 0;
2959 if (c == 1 || c == -1)
2961 if (pb->eqs[e].color == omega_red)
2963 bool fB;
2964 omega_substitute_red (pb, sub, i, c, &fB);
2965 if (fB)
2966 omega_convert_eq_to_geqs (pb, e);
2967 else
2968 omega_delete_variable (pb, i);
2970 else
2972 omega_substitute (pb, sub, i, c);
2973 omega_delete_variable (pb, i);
2976 else
2978 int a = abs (c);
2979 int e2 = e;
2981 if (dump_file && (dump_flags & TDF_DETAILS))
2982 fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
2984 for (e = pb->num_eqs - 1; e >= 0; e--)
2985 if (pb->eqs[e].coef[i])
2987 eqn eqn = &(pb->eqs[e]);
2988 int j, k;
2989 for (j = n_vars; j >= 0; j--)
2990 eqn->coef[j] *= a;
2991 k = eqn->coef[i];
2992 eqn->coef[i] = 0;
2993 if (sub->color == omega_red)
2994 eqn->color = omega_red;
2995 for (j = n_vars; j >= 0; j--)
2996 eqn->coef[j] -= sub->coef[j] * k / c;
2999 for (e = pb->num_geqs - 1; e >= 0; e--)
3000 if (pb->geqs[e].coef[i])
3002 eqn eqn = &(pb->geqs[e]);
3003 int j, k;
3005 if (sub->color == omega_red)
3006 eqn->color = omega_red;
3008 for (j = n_vars; j >= 0; j--)
3009 eqn->coef[j] *= a;
3011 eqn->touched = 1;
3012 k = eqn->coef[i];
3013 eqn->coef[i] = 0;
3015 for (j = n_vars; j >= 0; j--)
3016 eqn->coef[j] -= sub->coef[j] * k / c;
3020 for (e = pb->num_subs - 1; e >= 0; e--)
3021 if (pb->subs[e].coef[i])
3023 eqn eqn = &(pb->subs[e]);
3024 int j, k;
3025 gcc_assert (0);
3026 gcc_assert (sub->color == omega_black);
3027 for (j = n_vars; j >= 0; j--)
3028 eqn->coef[j] *= a;
3029 k = eqn->coef[i];
3030 eqn->coef[i] = 0;
3031 for (j = n_vars; j >= 0; j--)
3032 eqn->coef[j] -= sub->coef[j] * k / c;
3035 if (in_approximate_mode)
3036 omega_delete_variable (pb, i);
3037 else
3038 omega_convert_eq_to_geqs (pb, e2);
3041 omega_free_eqns (sub, 1);
3044 /* Helper function for printing "sorry, no solution". */
3046 static inline enum omega_result
3047 omega_problem_has_no_solution (void)
3049 if (dump_file && (dump_flags & TDF_DETAILS))
3050 fprintf (dump_file, "\nequations have no solution \n");
3052 return omega_false;
3055 /* Helper function: solve equations in PB one at a time, following the
3056 DESIRED_RES result. */
3058 static enum omega_result
3059 omega_solve_eq (omega_pb pb, enum omega_result desired_res)
3061 int i, j, e;
3062 int g, g2;
3063 g = 0;
3066 if (dump_file && (dump_flags & TDF_DETAILS) && pb->num_eqs > 0)
3068 fprintf (dump_file, "\nomega_solve_eq (%d, %d)\n",
3069 desired_res, may_be_red);
3070 omega_print_problem (dump_file, pb);
3071 fprintf (dump_file, "\n");
3074 if (may_be_red)
3076 i = 0;
3077 j = pb->num_eqs - 1;
3079 while (1)
3081 eqn eq;
3083 while (i <= j && pb->eqs[i].color == omega_red)
3084 i++;
3086 while (i <= j && pb->eqs[j].color == omega_black)
3087 j--;
3089 if (i >= j)
3090 break;
3092 eq = omega_alloc_eqns (0, 1);
3093 omega_copy_eqn (eq, &pb->eqs[i], pb->num_vars);
3094 omega_copy_eqn (&pb->eqs[i], &pb->eqs[j], pb->num_vars);
3095 omega_copy_eqn (&pb->eqs[j], eq, pb->num_vars);
3096 omega_free_eqns (eq, 1);
3097 i++;
3098 j--;
3102 /* Eliminate all EQ equations */
3103 for (e = pb->num_eqs - 1; e >= 0; e--)
3105 eqn eqn = &(pb->eqs[e]);
3106 int sv;
3108 if (dump_file && (dump_flags & TDF_DETAILS))
3109 fprintf (dump_file, "----\n");
3111 for (i = pb->num_vars; i > 0; i--)
3112 if (eqn->coef[i])
3113 break;
3115 g = eqn->coef[i];
3117 for (j = i - 1; j > 0; j--)
3118 if (eqn->coef[j])
3119 break;
3121 /* i is the position of last nonzero coefficient,
3122 g is the coefficient of i,
3123 j is the position of next nonzero coefficient. */
3125 if (j == 0)
3127 if (eqn->coef[0] % g != 0)
3128 return omega_problem_has_no_solution ();
3130 eqn->coef[0] = eqn->coef[0] / g;
3131 eqn->coef[i] = 1;
3132 pb->num_eqs--;
3133 omega_do_elimination (pb, e, i);
3134 continue;
3137 else if (j == -1)
3139 if (eqn->coef[0] != 0)
3140 return omega_problem_has_no_solution ();
3142 pb->num_eqs--;
3143 continue;
3146 if (g < 0)
3147 g = -g;
3149 if (g == 1)
3151 pb->num_eqs--;
3152 omega_do_elimination (pb, e, i);
3155 else
3157 int k = j;
3158 bool promotion_possible =
3159 (omega_safe_var_p (pb, j)
3160 && pb->safe_vars + 1 == i
3161 && !omega_eqn_is_red (eqn, desired_res)
3162 && !in_approximate_mode);
3164 if (dump_file && (dump_flags & TDF_DETAILS) && promotion_possible)
3165 fprintf (dump_file, " Promotion possible\n");
3167 normalizeEQ:
3168 if (!omega_safe_var_p (pb, j))
3170 for (; g != 1 && !omega_safe_var_p (pb, j); j--)
3171 g = gcd (abs (eqn->coef[j]), g);
3172 g2 = g;
3174 else if (!omega_safe_var_p (pb, i))
3175 g2 = g;
3176 else
3177 g2 = 0;
3179 for (; g != 1 && j > 0; j--)
3180 g = gcd (abs (eqn->coef[j]), g);
3182 if (g > 1)
3184 if (eqn->coef[0] % g != 0)
3185 return omega_problem_has_no_solution ();
3187 for (j = 0; j <= pb->num_vars; j++)
3188 eqn->coef[j] /= g;
3190 g2 = g2 / g;
3193 if (g2 > 1)
3195 int e2;
3197 for (e2 = e - 1; e2 >= 0; e2--)
3198 if (pb->eqs[e2].coef[i])
3199 break;
3201 if (e2 == -1)
3202 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
3203 if (pb->geqs[e2].coef[i])
3204 break;
3206 if (e2 == -1)
3207 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
3208 if (pb->subs[e2].coef[i])
3209 break;
3211 if (e2 == -1)
3213 bool change = false;
3215 if (dump_file && (dump_flags & TDF_DETAILS))
3217 fprintf (dump_file, "Ha! We own it! \n");
3218 omega_print_eq (dump_file, pb, eqn);
3219 fprintf (dump_file, " \n");
3222 g = eqn->coef[i];
3223 g = abs (g);
3225 for (j = i - 1; j >= 0; j--)
3227 int t = int_mod (eqn->coef[j], g);
3229 if (2 * t >= g)
3230 t -= g;
3232 if (t != eqn->coef[j])
3234 eqn->coef[j] = t;
3235 change = true;
3239 if (!change)
3241 if (dump_file && (dump_flags & TDF_DETAILS))
3242 fprintf (dump_file, "So what?\n");
3245 else
3247 omega_name_wild_card (pb, i);
3249 if (dump_file && (dump_flags & TDF_DETAILS))
3251 omega_print_eq (dump_file, pb, eqn);
3252 fprintf (dump_file, " \n");
3255 e++;
3256 continue;
3261 if (promotion_possible)
3263 if (dump_file && (dump_flags & TDF_DETAILS))
3265 fprintf (dump_file, "promoting %s to safety\n",
3266 omega_variable_to_str (pb, i));
3267 omega_print_vars (dump_file, pb);
3270 pb->safe_vars++;
3272 if (!omega_wildcard_p (pb, i))
3273 omega_name_wild_card (pb, i);
3275 promotion_possible = false;
3276 j = k;
3277 goto normalizeEQ;
3280 if (g2 > 1 && !in_approximate_mode)
3282 if (pb->eqs[e].color == omega_red)
3284 if (dump_file && (dump_flags & TDF_DETAILS))
3285 fprintf (dump_file, "handling red equality\n");
3287 pb->num_eqs--;
3288 omega_do_elimination (pb, e, i);
3289 continue;
3292 if (dump_file && (dump_flags & TDF_DETAILS))
3294 fprintf (dump_file,
3295 "adding equation to handle safe variable \n");
3296 omega_print_eq (dump_file, pb, eqn);
3297 fprintf (dump_file, "\n----\n");
3298 omega_print_problem (dump_file, pb);
3299 fprintf (dump_file, "\n----\n");
3300 fprintf (dump_file, "\n----\n");
3303 i = omega_add_new_wild_card (pb);
3304 pb->num_eqs++;
3305 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
3306 omega_init_eqn_zero (&pb->eqs[e + 1], pb->num_vars);
3307 omega_copy_eqn (&pb->eqs[e + 1], eqn, pb->safe_vars);
3309 for (j = pb->num_vars; j >= 0; j--)
3311 pb->eqs[e + 1].coef[j] = int_mod (pb->eqs[e + 1].coef[j], g2);
3313 if (2 * pb->eqs[e + 1].coef[j] >= g2)
3314 pb->eqs[e + 1].coef[j] -= g2;
3317 pb->eqs[e + 1].coef[i] = g2;
3318 e += 2;
3320 if (dump_file && (dump_flags & TDF_DETAILS))
3321 omega_print_problem (dump_file, pb);
3323 continue;
3326 sv = pb->safe_vars;
3327 if (g2 == 0)
3328 sv = 0;
3330 /* Find variable to eliminate. */
3331 if (g2 > 1)
3333 gcc_assert (in_approximate_mode);
3335 if (dump_file && (dump_flags & TDF_DETAILS))
3337 fprintf (dump_file, "non-exact elimination: ");
3338 omega_print_eq (dump_file, pb, eqn);
3339 fprintf (dump_file, "\n");
3340 omega_print_problem (dump_file, pb);
3343 for (i = pb->num_vars; i > sv; i--)
3344 if (pb->eqs[e].coef[i] != 0)
3345 break;
3347 else
3348 for (i = pb->num_vars; i > sv; i--)
3349 if (pb->eqs[e].coef[i] == 1 || pb->eqs[e].coef[i] == -1)
3350 break;
3352 if (i > sv)
3354 pb->num_eqs--;
3355 omega_do_elimination (pb, e, i);
3357 if (dump_file && (dump_flags & TDF_DETAILS) && g2 > 1)
3359 fprintf (dump_file, "result of non-exact elimination:\n");
3360 omega_print_problem (dump_file, pb);
3363 else
3365 int factor = (INT_MAX);
3366 j = 0;
3368 if (dump_file && (dump_flags & TDF_DETAILS))
3369 fprintf (dump_file, "doing moding\n");
3371 for (i = pb->num_vars; i != sv; i--)
3372 if ((pb->eqs[e].coef[i] & 1) != 0)
3374 j = i;
3375 i--;
3377 for (; i != sv; i--)
3378 if ((pb->eqs[e].coef[i] & 1) != 0)
3379 break;
3381 break;
3384 if (j != 0 && i == sv)
3386 omega_do_mod (pb, 2, e, j);
3387 e++;
3388 continue;
3391 j = 0;
3392 for (i = pb->num_vars; i != sv; i--)
3393 if (pb->eqs[e].coef[i] != 0
3394 && factor > abs (pb->eqs[e].coef[i]) + 1)
3396 factor = abs (pb->eqs[e].coef[i]) + 1;
3397 j = i;
3400 if (j == sv)
3402 if (dump_file && (dump_flags & TDF_DETAILS))
3403 fprintf (dump_file, "should not have happened\n");
3404 gcc_assert (0);
3407 omega_do_mod (pb, factor, e, j);
3408 /* Go back and try this equation again. */
3409 e++;
3414 pb->num_eqs = 0;
3415 return omega_unknown;
3418 /* Transform an inequation E to an equality, then solve DIFF problems
3419 based on PB, and only differing by the constant part that is
3420 diminished by one, trying to figure out which of the constants
3421 satisfies PB. */
3423 static enum omega_result
3424 parallel_splinter (omega_pb pb, int e, int diff,
3425 enum omega_result desired_res)
3427 omega_pb tmp_problem;
3428 int i;
3430 if (dump_file && (dump_flags & TDF_DETAILS))
3432 fprintf (dump_file, "Using parallel splintering\n");
3433 omega_print_problem (dump_file, pb);
3436 tmp_problem = XNEW (struct omega_pb_d);
3437 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e], pb->num_vars);
3438 pb->num_eqs = 1;
3440 for (i = 0; i <= diff; i++)
3442 omega_copy_problem (tmp_problem, pb);
3444 if (dump_file && (dump_flags & TDF_DETAILS))
3446 fprintf (dump_file, "Splinter # %i\n", i);
3447 omega_print_problem (dump_file, pb);
3450 if (omega_solve_problem (tmp_problem, desired_res) == omega_true)
3452 free (tmp_problem);
3453 return omega_true;
3456 pb->eqs[0].coef[0]--;
3459 free (tmp_problem);
3460 return omega_false;
3463 /* Helper function: solve equations one at a time. */
3465 static enum omega_result
3466 omega_solve_geq (omega_pb pb, enum omega_result desired_res)
3468 int i, e;
3469 int n_vars, fv;
3470 enum omega_result result;
3471 bool coupled_subscripts = false;
3472 bool smoothed = false;
3473 bool eliminate_again;
3474 bool tried_eliminating_redundant = false;
3476 if (desired_res != omega_simplify)
3478 pb->num_subs = 0;
3479 pb->safe_vars = 0;
3482 solve_geq_start:
3483 do {
3484 gcc_assert (desired_res == omega_simplify || pb->num_subs == 0);
3486 /* Verify that there are not too many inequalities. */
3487 gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
3489 if (dump_file && (dump_flags & TDF_DETAILS))
3491 fprintf (dump_file, "\nomega_solve_geq (%d,%d):\n",
3492 desired_res, please_no_equalities_in_simplified_problems);
3493 omega_print_problem (dump_file, pb);
3494 fprintf (dump_file, "\n");
3497 n_vars = pb->num_vars;
3499 if (n_vars == 1)
3501 enum omega_eqn_color u_color = omega_black;
3502 enum omega_eqn_color l_color = omega_black;
3503 int upper_bound = pos_infinity;
3504 int lower_bound = neg_infinity;
3506 for (e = pb->num_geqs - 1; e >= 0; e--)
3508 int a = pb->geqs[e].coef[1];
3509 int c = pb->geqs[e].coef[0];
3511 /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax. */
3512 if (a == 0)
3514 if (c < 0)
3515 return omega_problem_has_no_solution ();
3517 else if (a > 0)
3519 if (a != 1)
3520 c = int_div (c, a);
3522 if (lower_bound < -c
3523 || (lower_bound == -c
3524 && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3526 lower_bound = -c;
3527 l_color = pb->geqs[e].color;
3530 else
3532 if (a != -1)
3533 c = int_div (c, -a);
3535 if (upper_bound > c
3536 || (upper_bound == c
3537 && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3539 upper_bound = c;
3540 u_color = pb->geqs[e].color;
3545 if (dump_file && (dump_flags & TDF_DETAILS))
3547 fprintf (dump_file, "upper bound = %d\n", upper_bound);
3548 fprintf (dump_file, "lower bound = %d\n", lower_bound);
3551 if (lower_bound > upper_bound)
3552 return omega_problem_has_no_solution ();
3554 if (desired_res == omega_simplify)
3556 pb->num_geqs = 0;
3557 if (pb->safe_vars == 1)
3560 if (lower_bound == upper_bound
3561 && u_color == omega_black
3562 && l_color == omega_black)
3564 pb->eqs[0].coef[0] = -lower_bound;
3565 pb->eqs[0].coef[1] = 1;
3566 pb->eqs[0].color = omega_black;
3567 pb->num_eqs = 1;
3568 return omega_solve_problem (pb, desired_res);
3570 else
3572 if (lower_bound > neg_infinity)
3574 pb->geqs[0].coef[0] = -lower_bound;
3575 pb->geqs[0].coef[1] = 1;
3576 pb->geqs[0].key = 1;
3577 pb->geqs[0].color = l_color;
3578 pb->geqs[0].touched = 0;
3579 pb->num_geqs = 1;
3582 if (upper_bound < pos_infinity)
3584 pb->geqs[pb->num_geqs].coef[0] = upper_bound;
3585 pb->geqs[pb->num_geqs].coef[1] = -1;
3586 pb->geqs[pb->num_geqs].key = -1;
3587 pb->geqs[pb->num_geqs].color = u_color;
3588 pb->geqs[pb->num_geqs].touched = 0;
3589 pb->num_geqs++;
3593 else
3594 pb->num_vars = 0;
3596 omega_problem_reduced (pb);
3597 return omega_false;
3600 if (original_problem != no_problem
3601 && l_color == omega_black
3602 && u_color == omega_black
3603 && !conservative
3604 && lower_bound == upper_bound)
3606 pb->eqs[0].coef[0] = -lower_bound;
3607 pb->eqs[0].coef[1] = 1;
3608 pb->num_eqs = 1;
3609 adding_equality_constraint (pb, 0);
3612 return omega_true;
3615 if (!pb->variables_freed)
3617 pb->variables_freed = true;
3619 if (desired_res != omega_simplify)
3620 omega_free_eliminations (pb, 0);
3621 else
3622 omega_free_eliminations (pb, pb->safe_vars);
3624 n_vars = pb->num_vars;
3626 if (n_vars == 1)
3627 continue;
3630 switch (normalize_omega_problem (pb))
3632 case normalize_false:
3633 return omega_false;
3634 break;
3636 case normalize_coupled:
3637 coupled_subscripts = true;
3638 break;
3640 case normalize_uncoupled:
3641 coupled_subscripts = false;
3642 break;
3644 default:
3645 gcc_unreachable ();
3648 n_vars = pb->num_vars;
3650 if (dump_file && (dump_flags & TDF_DETAILS))
3652 fprintf (dump_file, "\nafter normalization:\n");
3653 omega_print_problem (dump_file, pb);
3654 fprintf (dump_file, "\n");
3655 fprintf (dump_file, "eliminating variable using Fourier-Motzkin.\n");
3658 do {
3659 int parallel_difference = INT_MAX;
3660 int best_parallel_eqn = -1;
3661 int minC, maxC, minCj = 0;
3662 int lower_bound_count = 0;
3663 int e2, Le = 0, Ue;
3664 bool possible_easy_int_solution;
3665 int max_splinters = 1;
3666 bool exact = false;
3667 bool lucky_exact = false;
3668 int best = (INT_MAX);
3669 int j = 0, jLe = 0, jLowerBoundCount = 0;
3672 eliminate_again = false;
3674 if (pb->num_eqs > 0)
3675 return omega_solve_problem (pb, desired_res);
3677 if (!coupled_subscripts)
3679 if (pb->safe_vars == 0)
3680 pb->num_geqs = 0;
3681 else
3682 for (e = pb->num_geqs - 1; e >= 0; e--)
3683 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
3684 omega_delete_geq (pb, e, n_vars);
3686 pb->num_vars = pb->safe_vars;
3688 if (desired_res == omega_simplify)
3690 omega_problem_reduced (pb);
3691 return omega_false;
3694 return omega_true;
3697 if (desired_res != omega_simplify)
3698 fv = 0;
3699 else
3700 fv = pb->safe_vars;
3702 if (pb->num_geqs == 0)
3704 if (desired_res == omega_simplify)
3706 pb->num_vars = pb->safe_vars;
3707 omega_problem_reduced (pb);
3708 return omega_false;
3710 return omega_true;
3713 if (desired_res == omega_simplify && n_vars == pb->safe_vars)
3715 omega_problem_reduced (pb);
3716 return omega_false;
3719 if (pb->num_geqs > OMEGA_MAX_GEQS - 30
3720 || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10)
3722 if (dump_file && (dump_flags & TDF_DETAILS))
3723 fprintf (dump_file,
3724 "TOO MANY EQUATIONS; "
3725 "%d equations, %d variables, "
3726 "ELIMINATING REDUNDANT ONES\n",
3727 pb->num_geqs, n_vars);
3729 if (!omega_eliminate_redundant (pb, false))
3730 return omega_false;
3732 n_vars = pb->num_vars;
3734 if (pb->num_eqs > 0)
3735 return omega_solve_problem (pb, desired_res);
3737 if (dump_file && (dump_flags & TDF_DETAILS))
3738 fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3741 if (desired_res != omega_simplify)
3742 fv = 0;
3743 else
3744 fv = pb->safe_vars;
3746 for (i = n_vars; i != fv; i--)
3748 int score;
3749 int ub = -2;
3750 int lb = -2;
3751 bool lucky = false;
3752 int upper_bound_count = 0;
3754 lower_bound_count = 0;
3755 minC = maxC = 0;
3757 for (e = pb->num_geqs - 1; e >= 0; e--)
3758 if (pb->geqs[e].coef[i] < 0)
3760 minC = MIN (minC, pb->geqs[e].coef[i]);
3761 upper_bound_count++;
3762 if (pb->geqs[e].coef[i] < -1)
3764 if (ub == -2)
3765 ub = e;
3766 else
3767 ub = -1;
3770 else if (pb->geqs[e].coef[i] > 0)
3772 maxC = MAX (maxC, pb->geqs[e].coef[i]);
3773 lower_bound_count++;
3774 Le = e;
3775 if (pb->geqs[e].coef[i] > 1)
3777 if (lb == -2)
3778 lb = e;
3779 else
3780 lb = -1;
3784 if (lower_bound_count == 0
3785 || upper_bound_count == 0)
3787 lower_bound_count = 0;
3788 break;
3791 if (ub >= 0 && lb >= 0
3792 && pb->geqs[lb].key == -pb->geqs[ub].key)
3794 int Lc = pb->geqs[lb].coef[i];
3795 int Uc = -pb->geqs[ub].coef[i];
3796 int diff =
3797 Lc * pb->geqs[ub].coef[0] + Uc * pb->geqs[lb].coef[0];
3798 lucky = (diff >= (Uc - 1) * (Lc - 1));
3801 if (maxC == 1
3802 || minC == -1
3803 || lucky
3804 || in_approximate_mode)
3806 score = upper_bound_count * lower_bound_count;
3808 if (dump_file && (dump_flags & TDF_DETAILS))
3809 fprintf (dump_file,
3810 "For %s, exact, score = %d*%d, range = %d ... %d,"
3811 "\nlucky = %d, in_approximate_mode=%d \n",
3812 omega_variable_to_str (pb, i),
3813 upper_bound_count,
3814 lower_bound_count, minC, maxC, lucky,
3815 in_approximate_mode);
3817 if (!exact
3818 || score < best)
3821 best = score;
3822 j = i;
3823 minCj = minC;
3824 jLe = Le;
3825 jLowerBoundCount = lower_bound_count;
3826 exact = true;
3827 lucky_exact = lucky;
3828 if (score == 1)
3829 break;
3832 else if (!exact)
3834 if (dump_file && (dump_flags & TDF_DETAILS))
3835 fprintf (dump_file,
3836 "For %s, non-exact, score = %d*%d,"
3837 "range = %d ... %d \n",
3838 omega_variable_to_str (pb, i),
3839 upper_bound_count,
3840 lower_bound_count, minC, maxC);
3842 score = maxC - minC;
3844 if (best > score)
3846 best = score;
3847 j = i;
3848 minCj = minC;
3849 jLe = Le;
3850 jLowerBoundCount = lower_bound_count;
3855 if (lower_bound_count == 0)
3857 omega_free_eliminations (pb, pb->safe_vars);
3858 n_vars = pb->num_vars;
3859 eliminate_again = true;
3860 continue;
3863 i = j;
3864 minC = minCj;
3865 Le = jLe;
3866 lower_bound_count = jLowerBoundCount;
3868 for (e = pb->num_geqs - 1; e >= 0; e--)
3869 if (pb->geqs[e].coef[i] > 0)
3871 if (pb->geqs[e].coef[i] == -minC)
3872 max_splinters += -minC - 1;
3873 else
3874 max_splinters +=
3875 pos_mul_hwi ((pb->geqs[e].coef[i] - 1),
3876 (-minC - 1)) / (-minC) + 1;
3879 /* #ifdef Omega3 */
3880 /* Trying to produce exact elimination by finding redundant
3881 constraints. */
3882 if (!exact && !tried_eliminating_redundant)
3884 omega_eliminate_redundant (pb, false);
3885 tried_eliminating_redundant = true;
3886 eliminate_again = true;
3887 continue;
3889 tried_eliminating_redundant = false;
3890 /* #endif */
3892 if (return_single_result && desired_res == omega_simplify && !exact)
3894 omega_problem_reduced (pb);
3895 return omega_true;
3898 /* #ifndef Omega3 */
3899 /* Trying to produce exact elimination by finding redundant
3900 constraints. */
3901 if (!exact && !tried_eliminating_redundant)
3903 omega_eliminate_redundant (pb, false);
3904 tried_eliminating_redundant = true;
3905 continue;
3907 tried_eliminating_redundant = false;
3908 /* #endif */
3910 if (!exact)
3912 int e1, e2;
3914 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
3915 if (pb->geqs[e1].color == omega_black)
3916 for (e2 = e1 - 1; e2 >= 0; e2--)
3917 if (pb->geqs[e2].color == omega_black
3918 && pb->geqs[e1].key == -pb->geqs[e2].key
3919 && ((pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3920 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3921 / 2 < parallel_difference))
3923 parallel_difference =
3924 (pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3925 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3926 / 2;
3927 best_parallel_eqn = e1;
3930 if (dump_file && (dump_flags & TDF_DETAILS)
3931 && best_parallel_eqn >= 0)
3933 fprintf (dump_file,
3934 "Possible parallel projection, diff = %d, in ",
3935 parallel_difference);
3936 omega_print_geq (dump_file, pb, &(pb->geqs[best_parallel_eqn]));
3937 fprintf (dump_file, "\n");
3938 omega_print_problem (dump_file, pb);
3942 if (dump_file && (dump_flags & TDF_DETAILS))
3944 fprintf (dump_file, "going to eliminate %s, (%d,%d,%d)\n",
3945 omega_variable_to_str (pb, i), i, minC,
3946 lower_bound_count);
3947 omega_print_problem (dump_file, pb);
3949 if (lucky_exact)
3950 fprintf (dump_file, "(a lucky exact elimination)\n");
3952 else if (exact)
3953 fprintf (dump_file, "(an exact elimination)\n");
3955 fprintf (dump_file, "Max # of splinters = %d\n", max_splinters);
3958 gcc_assert (max_splinters >= 1);
3960 if (!exact && desired_res == omega_simplify && best_parallel_eqn >= 0
3961 && parallel_difference <= max_splinters)
3962 return parallel_splinter (pb, best_parallel_eqn, parallel_difference,
3963 desired_res);
3965 smoothed = false;
3967 if (i != n_vars)
3969 int j = pb->num_vars;
3971 if (dump_file && (dump_flags & TDF_DETAILS))
3973 fprintf (dump_file, "Swapping %d and %d\n", i, j);
3974 omega_print_problem (dump_file, pb);
3977 std::swap (pb->var[i], pb->var[j]);
3979 for (e = pb->num_geqs - 1; e >= 0; e--)
3980 if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
3982 pb->geqs[e].touched = 1;
3983 std::swap (pb->geqs[e].coef[i], pb->geqs[e].coef[j]);
3986 for (e = pb->num_subs - 1; e >= 0; e--)
3987 if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
3988 std::swap (pb->subs[e].coef[i], pb->subs[e].coef[j]);
3990 if (dump_file && (dump_flags & TDF_DETAILS))
3992 fprintf (dump_file, "Swapping complete \n");
3993 omega_print_problem (dump_file, pb);
3994 fprintf (dump_file, "\n");
3997 i = j;
4000 else if (dump_file && (dump_flags & TDF_DETAILS))
4002 fprintf (dump_file, "No swap needed\n");
4003 omega_print_problem (dump_file, pb);
4006 pb->num_vars--;
4007 n_vars = pb->num_vars;
4009 if (exact)
4011 if (n_vars == 1)
4013 int upper_bound = pos_infinity;
4014 int lower_bound = neg_infinity;
4015 enum omega_eqn_color ub_color = omega_black;
4016 enum omega_eqn_color lb_color = omega_black;
4017 int topeqn = pb->num_geqs - 1;
4018 int Lc = pb->geqs[Le].coef[i];
4020 for (Le = topeqn; Le >= 0; Le--)
4021 if ((Lc = pb->geqs[Le].coef[i]) == 0)
4023 if (pb->geqs[Le].coef[1] == 1)
4025 int constantTerm = -pb->geqs[Le].coef[0];
4027 if (constantTerm > lower_bound ||
4028 (constantTerm == lower_bound &&
4029 !omega_eqn_is_red (&pb->geqs[Le], desired_res)))
4031 lower_bound = constantTerm;
4032 lb_color = pb->geqs[Le].color;
4035 if (dump_file && (dump_flags & TDF_DETAILS))
4037 if (pb->geqs[Le].color == omega_black)
4038 fprintf (dump_file, " :::=> %s >= %d\n",
4039 omega_variable_to_str (pb, 1),
4040 constantTerm);
4041 else
4042 fprintf (dump_file,
4043 " :::=> [%s >= %d]\n",
4044 omega_variable_to_str (pb, 1),
4045 constantTerm);
4048 else
4050 int constantTerm = pb->geqs[Le].coef[0];
4051 if (constantTerm < upper_bound ||
4052 (constantTerm == upper_bound
4053 && !omega_eqn_is_red (&pb->geqs[Le],
4054 desired_res)))
4056 upper_bound = constantTerm;
4057 ub_color = pb->geqs[Le].color;
4060 if (dump_file && (dump_flags & TDF_DETAILS))
4062 if (pb->geqs[Le].color == omega_black)
4063 fprintf (dump_file, " :::=> %s <= %d\n",
4064 omega_variable_to_str (pb, 1),
4065 constantTerm);
4066 else
4067 fprintf (dump_file,
4068 " :::=> [%s <= %d]\n",
4069 omega_variable_to_str (pb, 1),
4070 constantTerm);
4074 else if (Lc > 0)
4075 for (Ue = topeqn; Ue >= 0; Ue--)
4076 if (pb->geqs[Ue].coef[i] < 0
4077 && pb->geqs[Le].key != -pb->geqs[Ue].key)
4079 int Uc = -pb->geqs[Ue].coef[i];
4080 int coefficient = pb->geqs[Ue].coef[1] * Lc
4081 + pb->geqs[Le].coef[1] * Uc;
4082 int constantTerm = pb->geqs[Ue].coef[0] * Lc
4083 + pb->geqs[Le].coef[0] * Uc;
4085 if (dump_file && (dump_flags & TDF_DETAILS))
4087 omega_print_geq_extra (dump_file, pb,
4088 &(pb->geqs[Ue]));
4089 fprintf (dump_file, "\n");
4090 omega_print_geq_extra (dump_file, pb,
4091 &(pb->geqs[Le]));
4092 fprintf (dump_file, "\n");
4095 if (coefficient > 0)
4097 constantTerm = -int_div (constantTerm, coefficient);
4099 if (constantTerm > lower_bound
4100 || (constantTerm == lower_bound
4101 && (desired_res != omega_simplify
4102 || (pb->geqs[Ue].color == omega_black
4103 && pb->geqs[Le].color == omega_black))))
4105 lower_bound = constantTerm;
4106 lb_color = (pb->geqs[Ue].color == omega_red
4107 || pb->geqs[Le].color == omega_red)
4108 ? omega_red : omega_black;
4111 if (dump_file && (dump_flags & TDF_DETAILS))
4113 if (pb->geqs[Ue].color == omega_red
4114 || pb->geqs[Le].color == omega_red)
4115 fprintf (dump_file,
4116 " ::=> [%s >= %d]\n",
4117 omega_variable_to_str (pb, 1),
4118 constantTerm);
4119 else
4120 fprintf (dump_file,
4121 " ::=> %s >= %d\n",
4122 omega_variable_to_str (pb, 1),
4123 constantTerm);
4126 else
4128 constantTerm = int_div (constantTerm, -coefficient);
4129 if (constantTerm < upper_bound
4130 || (constantTerm == upper_bound
4131 && pb->geqs[Ue].color == omega_black
4132 && pb->geqs[Le].color == omega_black))
4134 upper_bound = constantTerm;
4135 ub_color = (pb->geqs[Ue].color == omega_red
4136 || pb->geqs[Le].color == omega_red)
4137 ? omega_red : omega_black;
4140 if (dump_file
4141 && (dump_flags & TDF_DETAILS))
4143 if (pb->geqs[Ue].color == omega_red
4144 || pb->geqs[Le].color == omega_red)
4145 fprintf (dump_file,
4146 " ::=> [%s <= %d]\n",
4147 omega_variable_to_str (pb, 1),
4148 constantTerm);
4149 else
4150 fprintf (dump_file,
4151 " ::=> %s <= %d\n",
4152 omega_variable_to_str (pb, 1),
4153 constantTerm);
4158 pb->num_geqs = 0;
4160 if (dump_file && (dump_flags & TDF_DETAILS))
4161 fprintf (dump_file,
4162 " therefore, %c%d <= %c%s%c <= %d%c\n",
4163 lb_color == omega_red ? '[' : ' ', lower_bound,
4164 (lb_color == omega_red && ub_color == omega_black)
4165 ? ']' : ' ',
4166 omega_variable_to_str (pb, 1),
4167 (lb_color == omega_black && ub_color == omega_red)
4168 ? '[' : ' ',
4169 upper_bound, ub_color == omega_red ? ']' : ' ');
4171 if (lower_bound > upper_bound)
4172 return omega_false;
4174 if (pb->safe_vars == 1)
4176 if (upper_bound == lower_bound
4177 && !(ub_color == omega_red || lb_color == omega_red)
4178 && !please_no_equalities_in_simplified_problems)
4180 pb->num_eqs++;
4181 pb->eqs[0].coef[1] = -1;
4182 pb->eqs[0].coef[0] = upper_bound;
4184 if (ub_color == omega_red
4185 || lb_color == omega_red)
4186 pb->eqs[0].color = omega_red;
4188 if (desired_res == omega_simplify
4189 && pb->eqs[0].color == omega_black)
4190 return omega_solve_problem (pb, desired_res);
4193 if (upper_bound != pos_infinity)
4195 pb->geqs[0].coef[1] = -1;
4196 pb->geqs[0].coef[0] = upper_bound;
4197 pb->geqs[0].color = ub_color;
4198 pb->geqs[0].key = -1;
4199 pb->geqs[0].touched = 0;
4200 pb->num_geqs++;
4203 if (lower_bound != neg_infinity)
4205 pb->geqs[pb->num_geqs].coef[1] = 1;
4206 pb->geqs[pb->num_geqs].coef[0] = -lower_bound;
4207 pb->geqs[pb->num_geqs].color = lb_color;
4208 pb->geqs[pb->num_geqs].key = 1;
4209 pb->geqs[pb->num_geqs].touched = 0;
4210 pb->num_geqs++;
4214 if (desired_res == omega_simplify)
4216 omega_problem_reduced (pb);
4217 return omega_false;
4219 else
4221 if (!conservative
4222 && (desired_res != omega_simplify
4223 || (lb_color == omega_black
4224 && ub_color == omega_black))
4225 && original_problem != no_problem
4226 && lower_bound == upper_bound)
4228 for (i = original_problem->num_vars; i >= 0; i--)
4229 if (original_problem->var[i] == pb->var[1])
4230 break;
4232 if (i == 0)
4233 break;
4235 e = original_problem->num_eqs++;
4236 omega_init_eqn_zero (&original_problem->eqs[e],
4237 original_problem->num_vars);
4238 original_problem->eqs[e].coef[i] = -1;
4239 original_problem->eqs[e].coef[0] = upper_bound;
4241 if (dump_file && (dump_flags & TDF_DETAILS))
4243 fprintf (dump_file,
4244 "adding equality %d to outer problem\n", e);
4245 omega_print_problem (dump_file, original_problem);
4248 return omega_true;
4252 eliminate_again = true;
4254 if (lower_bound_count == 1)
4256 eqn lbeqn = omega_alloc_eqns (0, 1);
4257 int Lc = pb->geqs[Le].coef[i];
4259 if (dump_file && (dump_flags & TDF_DETAILS))
4260 fprintf (dump_file, "an inplace elimination\n");
4262 omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1));
4263 omega_delete_geq_extra (pb, Le, n_vars + 1);
4265 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4266 if (pb->geqs[Ue].coef[i] < 0)
4268 if (lbeqn->key == -pb->geqs[Ue].key)
4269 omega_delete_geq_extra (pb, Ue, n_vars + 1);
4270 else
4272 int k;
4273 int Uc = -pb->geqs[Ue].coef[i];
4274 pb->geqs[Ue].touched = 1;
4275 eliminate_again = false;
4277 if (lbeqn->color == omega_red)
4278 pb->geqs[Ue].color = omega_red;
4280 for (k = 0; k <= n_vars; k++)
4281 pb->geqs[Ue].coef[k] =
4282 mul_hwi (pb->geqs[Ue].coef[k], Lc) +
4283 mul_hwi (lbeqn->coef[k], Uc);
4285 if (dump_file && (dump_flags & TDF_DETAILS))
4287 omega_print_geq (dump_file, pb,
4288 &(pb->geqs[Ue]));
4289 fprintf (dump_file, "\n");
4294 omega_free_eqns (lbeqn, 1);
4295 continue;
4297 else
4299 int *dead_eqns = XNEWVEC (int, OMEGA_MAX_GEQS);
4300 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
4301 int num_dead = 0;
4302 int top_eqn = pb->num_geqs - 1;
4303 lower_bound_count--;
4305 if (dump_file && (dump_flags & TDF_DETAILS))
4306 fprintf (dump_file, "lower bound count = %d\n",
4307 lower_bound_count);
4309 for (Le = top_eqn; Le >= 0; Le--)
4310 if (pb->geqs[Le].coef[i] > 0)
4312 int Lc = pb->geqs[Le].coef[i];
4313 for (Ue = top_eqn; Ue >= 0; Ue--)
4314 if (pb->geqs[Ue].coef[i] < 0)
4316 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4318 int k;
4319 int Uc = -pb->geqs[Ue].coef[i];
4321 if (num_dead == 0)
4322 e2 = pb->num_geqs++;
4323 else
4324 e2 = dead_eqns[--num_dead];
4326 gcc_assert (e2 < OMEGA_MAX_GEQS);
4328 if (dump_file && (dump_flags & TDF_DETAILS))
4330 fprintf (dump_file,
4331 "Le = %d, Ue = %d, gen = %d\n",
4332 Le, Ue, e2);
4333 omega_print_geq_extra (dump_file, pb,
4334 &(pb->geqs[Le]));
4335 fprintf (dump_file, "\n");
4336 omega_print_geq_extra (dump_file, pb,
4337 &(pb->geqs[Ue]));
4338 fprintf (dump_file, "\n");
4341 eliminate_again = false;
4343 for (k = n_vars; k >= 0; k--)
4344 pb->geqs[e2].coef[k] =
4345 mul_hwi (pb->geqs[Ue].coef[k], Lc) +
4346 mul_hwi (pb->geqs[Le].coef[k], Uc);
4348 pb->geqs[e2].coef[n_vars + 1] = 0;
4349 pb->geqs[e2].touched = 1;
4351 if (pb->geqs[Ue].color == omega_red
4352 || pb->geqs[Le].color == omega_red)
4353 pb->geqs[e2].color = omega_red;
4354 else
4355 pb->geqs[e2].color = omega_black;
4357 if (dump_file && (dump_flags & TDF_DETAILS))
4359 omega_print_geq (dump_file, pb,
4360 &(pb->geqs[e2]));
4361 fprintf (dump_file, "\n");
4365 if (lower_bound_count == 0)
4367 dead_eqns[num_dead++] = Ue;
4369 if (dump_file && (dump_flags & TDF_DETAILS))
4370 fprintf (dump_file, "Killed %d\n", Ue);
4374 lower_bound_count--;
4375 dead_eqns[num_dead++] = Le;
4377 if (dump_file && (dump_flags & TDF_DETAILS))
4378 fprintf (dump_file, "Killed %d\n", Le);
4381 for (e = pb->num_geqs - 1; e >= 0; e--)
4382 is_dead[e] = false;
4384 while (num_dead > 0)
4385 is_dead[dead_eqns[--num_dead]] = true;
4387 for (e = pb->num_geqs - 1; e >= 0; e--)
4388 if (is_dead[e])
4389 omega_delete_geq_extra (pb, e, n_vars + 1);
4391 free (dead_eqns);
4392 free (is_dead);
4393 continue;
4396 else
4398 omega_pb rS, iS;
4400 rS = omega_alloc_problem (0, 0);
4401 iS = omega_alloc_problem (0, 0);
4402 e2 = 0;
4403 possible_easy_int_solution = true;
4405 for (e = 0; e < pb->num_geqs; e++)
4406 if (pb->geqs[e].coef[i] == 0)
4408 omega_copy_eqn (&(rS->geqs[e2]), &pb->geqs[e],
4409 pb->num_vars);
4410 omega_copy_eqn (&(iS->geqs[e2]), &pb->geqs[e],
4411 pb->num_vars);
4413 if (dump_file && (dump_flags & TDF_DETAILS))
4415 int t;
4416 fprintf (dump_file, "Copying (%d, %d): ", i,
4417 pb->geqs[e].coef[i]);
4418 omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
4419 fprintf (dump_file, "\n");
4420 for (t = 0; t <= n_vars + 1; t++)
4421 fprintf (dump_file, "%d ", pb->geqs[e].coef[t]);
4422 fprintf (dump_file, "\n");
4425 e2++;
4426 gcc_assert (e2 < OMEGA_MAX_GEQS);
4429 for (Le = pb->num_geqs - 1; Le >= 0; Le--)
4430 if (pb->geqs[Le].coef[i] > 0)
4431 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4432 if (pb->geqs[Ue].coef[i] < 0)
4434 int k;
4435 int Lc = pb->geqs[Le].coef[i];
4436 int Uc = -pb->geqs[Ue].coef[i];
4438 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4441 rS->geqs[e2].touched = iS->geqs[e2].touched = 1;
4443 if (dump_file && (dump_flags & TDF_DETAILS))
4445 fprintf (dump_file, "---\n");
4446 fprintf (dump_file,
4447 "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
4448 Le, Lc, Ue, Uc, e2);
4449 omega_print_geq_extra (dump_file, pb, &pb->geqs[Le]);
4450 fprintf (dump_file, "\n");
4451 omega_print_geq_extra (dump_file, pb, &pb->geqs[Ue]);
4452 fprintf (dump_file, "\n");
4455 if (Uc == Lc)
4457 for (k = n_vars; k >= 0; k--)
4458 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4459 pb->geqs[Ue].coef[k] + pb->geqs[Le].coef[k];
4461 iS->geqs[e2].coef[0] -= (Uc - 1);
4463 else
4465 for (k = n_vars; k >= 0; k--)
4466 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4467 mul_hwi (pb->geqs[Ue].coef[k], Lc) +
4468 mul_hwi (pb->geqs[Le].coef[k], Uc);
4470 iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
4473 if (pb->geqs[Ue].color == omega_red
4474 || pb->geqs[Le].color == omega_red)
4475 iS->geqs[e2].color = rS->geqs[e2].color = omega_red;
4476 else
4477 iS->geqs[e2].color = rS->geqs[e2].color = omega_black;
4479 if (dump_file && (dump_flags & TDF_DETAILS))
4481 omega_print_geq (dump_file, pb, &(rS->geqs[e2]));
4482 fprintf (dump_file, "\n");
4485 e2++;
4486 gcc_assert (e2 < OMEGA_MAX_GEQS);
4488 else if (pb->geqs[Ue].coef[0] * Lc +
4489 pb->geqs[Le].coef[0] * Uc -
4490 (Uc - 1) * (Lc - 1) < 0)
4491 possible_easy_int_solution = false;
4494 iS->variables_initialized = rS->variables_initialized = true;
4495 iS->num_vars = rS->num_vars = pb->num_vars;
4496 iS->num_geqs = rS->num_geqs = e2;
4497 iS->num_eqs = rS->num_eqs = 0;
4498 iS->num_subs = rS->num_subs = pb->num_subs;
4499 iS->safe_vars = rS->safe_vars = pb->safe_vars;
4501 for (e = n_vars; e >= 0; e--)
4502 rS->var[e] = pb->var[e];
4504 for (e = n_vars; e >= 0; e--)
4505 iS->var[e] = pb->var[e];
4507 for (e = pb->num_subs - 1; e >= 0; e--)
4509 omega_copy_eqn (&(rS->subs[e]), &(pb->subs[e]), pb->num_vars);
4510 omega_copy_eqn (&(iS->subs[e]), &(pb->subs[e]), pb->num_vars);
4513 pb->num_vars++;
4514 n_vars = pb->num_vars;
4516 if (desired_res != omega_true)
4518 if (original_problem == no_problem)
4520 original_problem = pb;
4521 result = omega_solve_geq (rS, omega_false);
4522 original_problem = no_problem;
4524 else
4525 result = omega_solve_geq (rS, omega_false);
4527 if (result == omega_false)
4529 free (rS);
4530 free (iS);
4531 return result;
4534 if (pb->num_eqs > 0)
4536 /* An equality constraint must have been found */
4537 free (rS);
4538 free (iS);
4539 return omega_solve_problem (pb, desired_res);
4543 if (desired_res != omega_false)
4545 int j;
4546 int lower_bounds = 0;
4547 int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS);
4549 if (possible_easy_int_solution)
4551 conservative++;
4552 result = omega_solve_geq (iS, desired_res);
4553 conservative--;
4555 if (result != omega_false)
4557 free (rS);
4558 free (iS);
4559 free (lower_bound);
4560 return result;
4564 if (!exact && best_parallel_eqn >= 0
4565 && parallel_difference <= max_splinters)
4567 free (rS);
4568 free (iS);
4569 free (lower_bound);
4570 return parallel_splinter (pb, best_parallel_eqn,
4571 parallel_difference,
4572 desired_res);
4575 if (dump_file && (dump_flags & TDF_DETAILS))
4576 fprintf (dump_file, "have to do exact analysis\n");
4578 conservative++;
4580 for (e = 0; e < pb->num_geqs; e++)
4581 if (pb->geqs[e].coef[i] > 1)
4582 lower_bound[lower_bounds++] = e;
4584 /* Sort array LOWER_BOUND. */
4585 for (j = 0; j < lower_bounds; j++)
4587 int smallest = j;
4589 for (int k = j + 1; k < lower_bounds; k++)
4590 if (pb->geqs[lower_bound[smallest]].coef[i] >
4591 pb->geqs[lower_bound[k]].coef[i])
4592 smallest = k;
4594 std::swap (lower_bound[smallest], lower_bound[j]);
4597 if (dump_file && (dump_flags & TDF_DETAILS))
4599 fprintf (dump_file, "lower bound coefficients = ");
4601 for (j = 0; j < lower_bounds; j++)
4602 fprintf (dump_file, " %d",
4603 pb->geqs[lower_bound[j]].coef[i]);
4605 fprintf (dump_file, "\n");
4608 for (j = 0; j < lower_bounds; j++)
4610 int max_incr;
4611 int c;
4612 int worst_lower_bound_constant = -minC;
4614 e = lower_bound[j];
4615 max_incr = (((pb->geqs[e].coef[i] - 1) *
4616 (worst_lower_bound_constant - 1) - 1)
4617 / worst_lower_bound_constant);
4618 /* max_incr += 2; */
4620 if (dump_file && (dump_flags & TDF_DETAILS))
4622 fprintf (dump_file, "for equation ");
4623 omega_print_geq (dump_file, pb, &pb->geqs[e]);
4624 fprintf (dump_file,
4625 "\ntry decrements from 0 to %d\n",
4626 max_incr);
4627 omega_print_problem (dump_file, pb);
4630 if (max_incr > 50 && !smoothed
4631 && smooth_weird_equations (pb))
4633 conservative--;
4634 free (rS);
4635 free (iS);
4636 smoothed = true;
4637 goto solve_geq_start;
4640 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e],
4641 pb->num_vars);
4642 pb->eqs[0].color = omega_black;
4643 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
4644 pb->geqs[e].touched = 1;
4645 pb->num_eqs = 1;
4647 for (c = max_incr; c >= 0; c--)
4649 if (dump_file && (dump_flags & TDF_DETAILS))
4651 fprintf (dump_file,
4652 "trying next decrement of %d\n",
4653 max_incr - c);
4654 omega_print_problem (dump_file, pb);
4657 omega_copy_problem (rS, pb);
4659 if (dump_file && (dump_flags & TDF_DETAILS))
4660 omega_print_problem (dump_file, rS);
4662 result = omega_solve_problem (rS, desired_res);
4664 if (result == omega_true)
4666 free (rS);
4667 free (iS);
4668 free (lower_bound);
4669 conservative--;
4670 return omega_true;
4673 pb->eqs[0].coef[0]--;
4676 if (j + 1 < lower_bounds)
4678 pb->num_eqs = 0;
4679 omega_copy_eqn (&pb->geqs[e], &pb->eqs[0],
4680 pb->num_vars);
4681 pb->geqs[e].touched = 1;
4682 pb->geqs[e].color = omega_black;
4683 omega_copy_problem (rS, pb);
4685 if (dump_file && (dump_flags & TDF_DETAILS))
4686 fprintf (dump_file,
4687 "exhausted lower bound, "
4688 "checking if still feasible ");
4690 result = omega_solve_problem (rS, omega_false);
4692 if (result == omega_false)
4693 break;
4697 if (dump_file && (dump_flags & TDF_DETAILS))
4698 fprintf (dump_file, "fall-off the end\n");
4700 free (rS);
4701 free (iS);
4702 free (lower_bound);
4703 conservative--;
4704 return omega_false;
4707 free (rS);
4708 free (iS);
4710 return omega_unknown;
4711 } while (eliminate_again);
4712 } while (1);
4715 /* Because the omega solver is recursive, this counter limits the
4716 recursion depth. */
4717 static int omega_solve_depth = 0;
4719 /* Return omega_true when the problem PB has a solution following the
4720 DESIRED_RES. */
4722 enum omega_result
4723 omega_solve_problem (omega_pb pb, enum omega_result desired_res)
4725 enum omega_result result;
4727 gcc_assert (pb->num_vars >= pb->safe_vars);
4728 omega_solve_depth++;
4730 if (desired_res != omega_simplify)
4731 pb->safe_vars = 0;
4733 if (omega_solve_depth > 50)
4735 if (dump_file && (dump_flags & TDF_DETAILS))
4737 fprintf (dump_file,
4738 "Solve depth = %d, in_approximate_mode = %d, aborting\n",
4739 omega_solve_depth, in_approximate_mode);
4740 omega_print_problem (dump_file, pb);
4742 gcc_assert (0);
4745 if (omega_solve_eq (pb, desired_res) == omega_false)
4747 omega_solve_depth--;
4748 return omega_false;
4751 if (in_approximate_mode && !pb->num_geqs)
4753 result = omega_true;
4754 pb->num_vars = pb->safe_vars;
4755 omega_problem_reduced (pb);
4757 else
4758 result = omega_solve_geq (pb, desired_res);
4760 omega_solve_depth--;
4762 if (!omega_reduce_with_subs)
4764 resurrect_subs (pb);
4765 gcc_assert (please_no_equalities_in_simplified_problems
4766 || !result || pb->num_subs == 0);
4769 return result;
4772 /* Return true if red equations constrain the set of possible solutions.
4773 We assume that there are solutions to the black equations by
4774 themselves, so if there is no solution to the combined problem, we
4775 return true. */
4777 bool
4778 omega_problem_has_red_equations (omega_pb pb)
4780 bool result;
4781 int e;
4782 int i;
4784 if (dump_file && (dump_flags & TDF_DETAILS))
4786 fprintf (dump_file, "Checking for red equations:\n");
4787 omega_print_problem (dump_file, pb);
4790 please_no_equalities_in_simplified_problems++;
4791 may_be_red++;
4793 if (omega_single_result)
4794 return_single_result++;
4796 create_color = true;
4797 result = (omega_simplify_problem (pb) == omega_false);
4799 if (omega_single_result)
4800 return_single_result--;
4802 may_be_red--;
4803 please_no_equalities_in_simplified_problems--;
4805 if (result)
4807 if (dump_file && (dump_flags & TDF_DETAILS))
4808 fprintf (dump_file, "Gist is FALSE\n");
4810 pb->num_subs = 0;
4811 pb->num_geqs = 0;
4812 pb->num_eqs = 1;
4813 pb->eqs[0].color = omega_red;
4815 for (i = pb->num_vars; i > 0; i--)
4816 pb->eqs[0].coef[i] = 0;
4818 pb->eqs[0].coef[0] = 1;
4819 return true;
4822 free_red_eliminations (pb);
4823 gcc_assert (pb->num_eqs == 0);
4825 for (e = pb->num_geqs - 1; e >= 0; e--)
4826 if (pb->geqs[e].color == omega_red)
4828 result = true;
4829 break;
4832 if (!result)
4833 return false;
4835 for (i = pb->safe_vars; i >= 1; i--)
4837 int ub = 0;
4838 int lb = 0;
4840 for (e = pb->num_geqs - 1; e >= 0; e--)
4842 if (pb->geqs[e].coef[i])
4844 if (pb->geqs[e].coef[i] > 0)
4845 lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4847 else
4848 ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4852 if (ub == 2 || lb == 2)
4855 if (dump_file && (dump_flags & TDF_DETAILS))
4856 fprintf (dump_file, "checks for upper/lower bounds worked!\n");
4858 if (!omega_reduce_with_subs)
4860 resurrect_subs (pb);
4861 gcc_assert (pb->num_subs == 0);
4864 return true;
4869 if (dump_file && (dump_flags & TDF_DETAILS))
4870 fprintf (dump_file,
4871 "*** Doing potentially expensive elimination tests "
4872 "for red equations\n");
4874 please_no_equalities_in_simplified_problems++;
4875 omega_eliminate_red (pb, true);
4876 please_no_equalities_in_simplified_problems--;
4878 result = false;
4879 gcc_assert (pb->num_eqs == 0);
4881 for (e = pb->num_geqs - 1; e >= 0; e--)
4882 if (pb->geqs[e].color == omega_red)
4884 result = true;
4885 break;
4888 if (dump_file && (dump_flags & TDF_DETAILS))
4890 if (!result)
4891 fprintf (dump_file,
4892 "******************** Redundant Red Equations eliminated!!\n");
4893 else
4894 fprintf (dump_file,
4895 "******************** Red Equations remain\n");
4897 omega_print_problem (dump_file, pb);
4900 if (!omega_reduce_with_subs)
4902 normalize_return_type r;
4904 resurrect_subs (pb);
4905 r = normalize_omega_problem (pb);
4906 gcc_assert (r != normalize_false);
4908 coalesce (pb);
4909 cleanout_wildcards (pb);
4910 gcc_assert (pb->num_subs == 0);
4913 return result;
4916 /* Calls omega_simplify_problem in approximate mode. */
4918 enum omega_result
4919 omega_simplify_approximate (omega_pb pb)
4921 enum omega_result result;
4923 if (dump_file && (dump_flags & TDF_DETAILS))
4924 fprintf (dump_file, "(Entering approximate mode\n");
4926 in_approximate_mode = true;
4927 result = omega_simplify_problem (pb);
4928 in_approximate_mode = false;
4930 gcc_assert (pb->num_vars == pb->safe_vars);
4931 if (!omega_reduce_with_subs)
4932 gcc_assert (pb->num_subs == 0);
4934 if (dump_file && (dump_flags & TDF_DETAILS))
4935 fprintf (dump_file, "Leaving approximate mode)\n");
4937 return result;
4941 /* Simplifies problem PB by eliminating redundant constraints and
4942 reducing the constraints system to a minimal form. Returns
4943 omega_true when the problem was successfully reduced, omega_unknown
4944 when the solver is unable to determine an answer. */
4946 enum omega_result
4947 omega_simplify_problem (omega_pb pb)
4949 int i;
4951 omega_found_reduction = omega_false;
4953 if (!pb->variables_initialized)
4954 omega_initialize_variables (pb);
4956 if (next_key * 3 > MAX_KEYS)
4958 int e;
4960 hash_version++;
4961 next_key = OMEGA_MAX_VARS + 1;
4963 for (e = pb->num_geqs - 1; e >= 0; e--)
4964 pb->geqs[e].touched = 1;
4966 for (i = 0; i < HASH_TABLE_SIZE; i++)
4967 hash_master[i].touched = -1;
4969 pb->hash_version = hash_version;
4972 else if (pb->hash_version != hash_version)
4974 int e;
4976 for (e = pb->num_geqs - 1; e >= 0; e--)
4977 pb->geqs[e].touched = 1;
4979 pb->hash_version = hash_version;
4982 if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars)
4983 omega_free_eliminations (pb, pb->safe_vars);
4985 if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0)
4987 omega_found_reduction = omega_solve_problem (pb, omega_unknown);
4989 if (omega_found_reduction != omega_false
4990 && !return_single_result)
4992 pb->num_geqs = 0;
4993 pb->num_eqs = 0;
4994 (*omega_when_reduced) (pb);
4997 return omega_found_reduction;
5000 omega_solve_problem (pb, omega_simplify);
5002 if (omega_found_reduction != omega_false)
5004 for (i = 1; omega_safe_var_p (pb, i); i++)
5005 pb->forwarding_address[pb->var[i]] = i;
5007 for (i = 0; i < pb->num_subs; i++)
5008 pb->forwarding_address[pb->subs[i].key] = -i - 1;
5011 if (!omega_reduce_with_subs)
5012 gcc_assert (please_no_equalities_in_simplified_problems
5013 || omega_found_reduction == omega_false
5014 || pb->num_subs == 0);
5016 return omega_found_reduction;
5019 /* Make variable VAR unprotected: it then can be eliminated. */
5021 void
5022 omega_unprotect_variable (omega_pb pb, int var)
5024 int e, idx;
5025 idx = pb->forwarding_address[var];
5027 if (idx < 0)
5029 idx = -1 - idx;
5030 pb->num_subs--;
5032 if (idx < pb->num_subs)
5034 omega_copy_eqn (&pb->subs[idx], &pb->subs[pb->num_subs],
5035 pb->num_vars);
5036 pb->forwarding_address[pb->subs[idx].key] = -idx - 1;
5039 else
5041 int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS);
5042 int e2;
5044 for (e = pb->num_subs - 1; e >= 0; e--)
5045 bring_to_life[e] = (pb->subs[e].coef[idx] != 0);
5047 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
5048 if (bring_to_life[e2])
5050 pb->num_vars++;
5051 pb->safe_vars++;
5053 if (pb->safe_vars < pb->num_vars)
5055 for (e = pb->num_geqs - 1; e >= 0; e--)
5057 pb->geqs[e].coef[pb->num_vars] =
5058 pb->geqs[e].coef[pb->safe_vars];
5060 pb->geqs[e].coef[pb->safe_vars] = 0;
5063 for (e = pb->num_eqs - 1; e >= 0; e--)
5065 pb->eqs[e].coef[pb->num_vars] =
5066 pb->eqs[e].coef[pb->safe_vars];
5068 pb->eqs[e].coef[pb->safe_vars] = 0;
5071 for (e = pb->num_subs - 1; e >= 0; e--)
5073 pb->subs[e].coef[pb->num_vars] =
5074 pb->subs[e].coef[pb->safe_vars];
5076 pb->subs[e].coef[pb->safe_vars] = 0;
5079 pb->var[pb->num_vars] = pb->var[pb->safe_vars];
5080 pb->forwarding_address[pb->var[pb->num_vars]] =
5081 pb->num_vars;
5083 else
5085 for (e = pb->num_geqs - 1; e >= 0; e--)
5086 pb->geqs[e].coef[pb->safe_vars] = 0;
5088 for (e = pb->num_eqs - 1; e >= 0; e--)
5089 pb->eqs[e].coef[pb->safe_vars] = 0;
5091 for (e = pb->num_subs - 1; e >= 0; e--)
5092 pb->subs[e].coef[pb->safe_vars] = 0;
5095 pb->var[pb->safe_vars] = pb->subs[e2].key;
5096 pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars;
5098 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e2]),
5099 pb->num_vars);
5100 pb->eqs[pb->num_eqs++].coef[pb->safe_vars] = -1;
5101 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5103 if (e2 < pb->num_subs - 1)
5104 omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]),
5105 pb->num_vars);
5107 pb->num_subs--;
5110 omega_unprotect_1 (pb, &idx, NULL);
5111 free (bring_to_life);
5114 chain_unprotect (pb);
5117 /* Unprotects VAR and simplifies PB. */
5119 enum omega_result
5120 omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color,
5121 int var, int sign)
5123 int n_vars = pb->num_vars;
5124 int e, j;
5125 int k = pb->forwarding_address[var];
5127 if (k < 0)
5129 k = -1 - k;
5131 if (sign != 0)
5133 e = pb->num_geqs++;
5134 omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars);
5136 for (j = 0; j <= n_vars; j++)
5137 pb->geqs[e].coef[j] *= sign;
5139 pb->geqs[e].coef[0]--;
5140 pb->geqs[e].touched = 1;
5141 pb->geqs[e].color = color;
5143 else
5145 e = pb->num_eqs++;
5146 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5147 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5148 pb->eqs[e].color = color;
5151 else if (sign != 0)
5153 e = pb->num_geqs++;
5154 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
5155 pb->geqs[e].coef[k] = sign;
5156 pb->geqs[e].coef[0] = -1;
5157 pb->geqs[e].touched = 1;
5158 pb->geqs[e].color = color;
5160 else
5162 e = pb->num_eqs++;
5163 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5164 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5165 pb->eqs[e].coef[k] = 1;
5166 pb->eqs[e].color = color;
5169 omega_unprotect_variable (pb, var);
5170 return omega_simplify_problem (pb);
5173 /* Add an equation "VAR = VALUE" with COLOR to PB. */
5175 void
5176 omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color,
5177 int var, int value)
5179 int e;
5180 int k = pb->forwarding_address[var];
5182 if (k < 0)
5184 k = -1 - k;
5185 e = pb->num_eqs++;
5186 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5187 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5188 pb->eqs[e].coef[0] -= value;
5190 else
5192 e = pb->num_eqs++;
5193 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5194 pb->eqs[e].coef[k] = 1;
5195 pb->eqs[e].coef[0] = -value;
5198 pb->eqs[e].color = color;
5201 /* Return false when the upper and lower bounds are not coupled.
5202 Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
5203 variable I. */
5205 bool
5206 omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound)
5208 int n_vars = pb->num_vars;
5209 int e, j;
5210 bool is_simple;
5211 bool coupled = false;
5213 *lower_bound = neg_infinity;
5214 *upper_bound = pos_infinity;
5215 i = pb->forwarding_address[i];
5217 if (i < 0)
5219 i = -i - 1;
5221 for (j = 1; j <= n_vars; j++)
5222 if (pb->subs[i].coef[j] != 0)
5223 return true;
5225 *upper_bound = *lower_bound = pb->subs[i].coef[0];
5226 return false;
5229 for (e = pb->num_subs - 1; e >= 0; e--)
5230 if (pb->subs[e].coef[i] != 0)
5232 coupled = true;
5233 break;
5236 for (e = pb->num_eqs - 1; e >= 0; e--)
5237 if (pb->eqs[e].coef[i] != 0)
5239 is_simple = true;
5241 for (j = 1; j <= n_vars; j++)
5242 if (i != j && pb->eqs[e].coef[j] != 0)
5244 is_simple = false;
5245 coupled = true;
5246 break;
5249 if (!is_simple)
5250 continue;
5251 else
5253 *lower_bound = *upper_bound =
5254 -pb->eqs[e].coef[i] * pb->eqs[e].coef[0];
5255 return false;
5259 for (e = pb->num_geqs - 1; e >= 0; e--)
5260 if (pb->geqs[e].coef[i] != 0)
5262 if (pb->geqs[e].key == i)
5263 *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]);
5265 else if (pb->geqs[e].key == -i)
5266 *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]);
5268 else
5269 coupled = true;
5272 return coupled;
5275 /* Sets the lower bound L and upper bound U for the values of variable
5276 I, and sets COULD_BE_ZERO to true if variable I might take value
5277 zero. LOWER_BOUND and UPPER_BOUND are bounds on the values of
5278 variable I. */
5280 static void
5281 query_coupled_variable (omega_pb pb, int i, int *l, int *u,
5282 bool *could_be_zero, int lower_bound, int upper_bound)
5284 int e, b1, b2;
5285 eqn eqn;
5286 int sign;
5287 int v;
5289 /* Preconditions. */
5290 gcc_assert (abs (pb->forwarding_address[i]) == 1
5291 && pb->num_vars + pb->num_subs == 2
5292 && pb->num_eqs + pb->num_subs == 1);
5294 /* Define variable I in terms of variable V. */
5295 if (pb->forwarding_address[i] == -1)
5297 eqn = &pb->subs[0];
5298 sign = 1;
5299 v = 1;
5301 else
5303 eqn = &pb->eqs[0];
5304 sign = -eqn->coef[1];
5305 v = 2;
5308 for (e = pb->num_geqs - 1; e >= 0; e--)
5309 if (pb->geqs[e].coef[v] != 0)
5311 if (pb->geqs[e].coef[v] == 1)
5312 lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]);
5314 else
5315 upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]);
5318 if (lower_bound > upper_bound)
5320 *l = pos_infinity;
5321 *u = neg_infinity;
5322 *could_be_zero = 0;
5323 return;
5326 if (lower_bound == neg_infinity)
5328 if (eqn->coef[v] > 0)
5329 b1 = sign * neg_infinity;
5331 else
5332 b1 = -sign * neg_infinity;
5334 else
5335 b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound);
5337 if (upper_bound == pos_infinity)
5339 if (eqn->coef[v] > 0)
5340 b2 = sign * pos_infinity;
5342 else
5343 b2 = -sign * pos_infinity;
5345 else
5346 b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound);
5348 *l = MAX (*l, b1 <= b2 ? b1 : b2);
5349 *u = MIN (*u, b1 <= b2 ? b2 : b1);
5351 *could_be_zero = (*l <= 0 && 0 <= *u
5352 && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0);
5355 /* Return false when a lower bound L and an upper bound U for variable
5356 I in problem PB have been initialized. */
5358 bool
5359 omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u)
5361 *l = neg_infinity;
5362 *u = pos_infinity;
5364 if (!omega_query_variable (pb, i, l, u)
5365 || (pb->num_vars == 1 && pb->forwarding_address[i] == 1))
5366 return false;
5368 if (abs (pb->forwarding_address[i]) == 1
5369 && pb->num_vars + pb->num_subs == 2
5370 && pb->num_eqs + pb->num_subs == 1)
5372 bool could_be_zero;
5373 query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity,
5374 pos_infinity);
5375 return false;
5378 return true;
5381 /* For problem PB, return an integer that represents the classic data
5382 dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
5383 masks that are added to the result. When DIST_KNOWN is true, DIST
5384 is set to the classic data dependence distance. LOWER_BOUND and
5385 UPPER_BOUND are bounds on the value of variable I, for example, it
5386 is possible to narrow the iteration domain with safe approximations
5387 of loop counts, and thus discard some data dependences that cannot
5388 occur. */
5391 omega_query_variable_signs (omega_pb pb, int i, int dd_lt,
5392 int dd_eq, int dd_gt, int lower_bound,
5393 int upper_bound, bool *dist_known, int *dist)
5395 int result;
5396 int l, u;
5397 bool could_be_zero;
5399 l = neg_infinity;
5400 u = pos_infinity;
5402 omega_query_variable (pb, i, &l, &u);
5403 query_coupled_variable (pb, i, &l, &u, &could_be_zero, lower_bound,
5404 upper_bound);
5405 result = 0;
5407 if (l < 0)
5408 result |= dd_gt;
5410 if (u > 0)
5411 result |= dd_lt;
5413 if (could_be_zero)
5414 result |= dd_eq;
5416 if (l == u)
5418 *dist_known = true;
5419 *dist = l;
5421 else
5422 *dist_known = false;
5424 return result;
5427 /* Initialize PB as an Omega problem with NVARS variables and NPROT
5428 safe variables. Safe variables are not eliminated during the
5429 Fourier-Motzkin elimination. Safe variables are all those
5430 variables that are placed at the beginning of the array of
5431 variables: P->var[0, ..., NPROT - 1]. */
5433 omega_pb
5434 omega_alloc_problem (int nvars, int nprot)
5436 omega_pb pb;
5438 gcc_assert (nvars <= OMEGA_MAX_VARS);
5439 omega_initialize ();
5441 /* Allocate and initialize PB. */
5442 pb = XCNEW (struct omega_pb_d);
5443 pb->var = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5444 pb->forwarding_address = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5445 pb->geqs = omega_alloc_eqns (0, OMEGA_MAX_GEQS);
5446 pb->eqs = omega_alloc_eqns (0, OMEGA_MAX_EQS);
5447 pb->subs = omega_alloc_eqns (0, OMEGA_MAX_VARS + 1);
5449 pb->hash_version = hash_version;
5450 pb->num_vars = nvars;
5451 pb->safe_vars = nprot;
5452 pb->variables_initialized = false;
5453 pb->variables_freed = false;
5454 pb->num_eqs = 0;
5455 pb->num_geqs = 0;
5456 pb->num_subs = 0;
5457 return pb;
5460 /* Keeps the state of the initialization. */
5461 static bool omega_initialized = false;
5463 /* Initialization of the Omega solver. */
5465 void
5466 omega_initialize (void)
5468 int i;
5470 if (omega_initialized)
5471 return;
5473 next_wild_card = 0;
5474 next_key = OMEGA_MAX_VARS + 1;
5475 packing = XCNEWVEC (int, OMEGA_MAX_VARS);
5476 fast_lookup = XCNEWVEC (int, MAX_KEYS * 2);
5477 fast_lookup_red = XCNEWVEC (int, MAX_KEYS * 2);
5478 hash_master = omega_alloc_eqns (0, HASH_TABLE_SIZE);
5480 for (i = 0; i < HASH_TABLE_SIZE; i++)
5481 hash_master[i].touched = -1;
5483 sprintf (wild_name[0], "1");
5484 sprintf (wild_name[1], "a");
5485 sprintf (wild_name[2], "b");
5486 sprintf (wild_name[3], "c");
5487 sprintf (wild_name[4], "d");
5488 sprintf (wild_name[5], "e");
5489 sprintf (wild_name[6], "f");
5490 sprintf (wild_name[7], "g");
5491 sprintf (wild_name[8], "h");
5492 sprintf (wild_name[9], "i");
5493 sprintf (wild_name[10], "j");
5494 sprintf (wild_name[11], "k");
5495 sprintf (wild_name[12], "l");
5496 sprintf (wild_name[13], "m");
5497 sprintf (wild_name[14], "n");
5498 sprintf (wild_name[15], "o");
5499 sprintf (wild_name[16], "p");
5500 sprintf (wild_name[17], "q");
5501 sprintf (wild_name[18], "r");
5502 sprintf (wild_name[19], "s");
5503 sprintf (wild_name[20], "t");
5504 sprintf (wild_name[40 - 1], "alpha");
5505 sprintf (wild_name[40 - 2], "beta");
5506 sprintf (wild_name[40 - 3], "gamma");
5507 sprintf (wild_name[40 - 4], "delta");
5508 sprintf (wild_name[40 - 5], "tau");
5509 sprintf (wild_name[40 - 6], "sigma");
5510 sprintf (wild_name[40 - 7], "chi");
5511 sprintf (wild_name[40 - 8], "omega");
5512 sprintf (wild_name[40 - 9], "pi");
5513 sprintf (wild_name[40 - 10], "ni");
5514 sprintf (wild_name[40 - 11], "Alpha");
5515 sprintf (wild_name[40 - 12], "Beta");
5516 sprintf (wild_name[40 - 13], "Gamma");
5517 sprintf (wild_name[40 - 14], "Delta");
5518 sprintf (wild_name[40 - 15], "Tau");
5519 sprintf (wild_name[40 - 16], "Sigma");
5520 sprintf (wild_name[40 - 17], "Chi");
5521 sprintf (wild_name[40 - 18], "Omega");
5522 sprintf (wild_name[40 - 19], "xxx");
5524 omega_initialized = true;