Daily bump.
[official-gcc.git] / gcc / omega.c
blob766cb73fff64c3fa4a3128051c94a45a54545f5c
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-2014 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 "tree.h"
37 #include "diagnostic-core.h"
38 #include "dumpfile.h"
39 #include "omega.h"
41 /* When set to true, keep substitution variables. When set to false,
42 resurrect substitution variables (convert substitutions back to EQs). */
43 static bool omega_reduce_with_subs = true;
45 /* When set to true, omega_simplify_problem checks for problem with no
46 solutions, calling verify_omega_pb. */
47 static bool omega_verify_simplification = false;
49 /* When set to true, only produce a single simplified result. */
50 static bool omega_single_result = false;
52 /* Set return_single_result to 1 when omega_single_result is true. */
53 static int return_single_result = 0;
55 /* Hash table for equations generated by the solver. */
56 #define HASH_TABLE_SIZE PARAM_VALUE (PARAM_OMEGA_HASH_TABLE_SIZE)
57 #define MAX_KEYS PARAM_VALUE (PARAM_OMEGA_MAX_KEYS)
58 static eqn hash_master;
59 static int next_key;
60 static int hash_version = 0;
62 /* Set to true for making the solver enter in approximation mode. */
63 static bool in_approximate_mode = false;
65 /* When set to zero, the solver is allowed to add new equalities to
66 the problem to be solved. */
67 static int conservative = 0;
69 /* Set to omega_true when the problem was successfully reduced, set to
70 omega_unknown when the solver is unable to determine an answer. */
71 static enum omega_result omega_found_reduction;
73 /* Set to true when the solver is allowed to add omega_red equations. */
74 static bool create_color = false;
76 /* Set to nonzero when the problem to be solved can be reduced. */
77 static int may_be_red = 0;
79 /* When false, there should be no substitution equations in the
80 simplified problem. */
81 static int please_no_equalities_in_simplified_problems = 0;
83 /* Variables names for pretty printing. */
84 static char wild_name[200][40];
86 /* Pointer to the void problem. */
87 static omega_pb no_problem = (omega_pb) 0;
89 /* Pointer to the problem to be solved. */
90 static omega_pb original_problem = (omega_pb) 0;
93 /* Return the integer A divided by B. */
95 static inline int
96 int_div (int a, int b)
98 if (a > 0)
99 return a/b;
100 else
101 return -((-a + b - 1)/b);
104 /* Return the integer A modulo B. */
106 static inline int
107 int_mod (int a, int b)
109 return a - b * int_div (a, b);
112 /* Test whether equation E is red. */
114 static inline bool
115 omega_eqn_is_red (eqn e, int desired_res)
117 return (desired_res == omega_simplify && e->color == omega_red);
120 /* Return a string for VARIABLE. */
122 static inline char *
123 omega_var_to_str (int variable)
125 if (0 <= variable && variable <= 20)
126 return wild_name[variable];
128 if (-20 < variable && variable < 0)
129 return wild_name[40 + variable];
131 /* Collapse all the entries that would have overflowed. */
132 return wild_name[21];
135 /* Return a string for variable I in problem PB. */
137 static inline char *
138 omega_variable_to_str (omega_pb pb, int i)
140 return omega_var_to_str (pb->var[i]);
143 /* Do nothing function: used for default initializations. */
145 void
146 omega_no_procedure (omega_pb pb ATTRIBUTE_UNUSED)
150 void (*omega_when_reduced) (omega_pb) = omega_no_procedure;
152 /* Print to FILE from PB equation E with all its coefficients
153 multiplied by C. */
155 static void
156 omega_print_term (FILE *file, omega_pb pb, eqn e, int c)
158 int i;
159 bool first = true;
160 int n = pb->num_vars;
161 int went_first = -1;
163 for (i = 1; i <= n; i++)
164 if (c * e->coef[i] > 0)
166 first = false;
167 went_first = i;
169 if (c * e->coef[i] == 1)
170 fprintf (file, "%s", omega_variable_to_str (pb, i));
171 else
172 fprintf (file, "%d * %s", c * e->coef[i],
173 omega_variable_to_str (pb, i));
174 break;
177 for (i = 1; i <= n; i++)
178 if (i != went_first && c * e->coef[i] != 0)
180 if (!first && c * e->coef[i] > 0)
181 fprintf (file, " + ");
183 first = false;
185 if (c * e->coef[i] == 1)
186 fprintf (file, "%s", omega_variable_to_str (pb, i));
187 else if (c * e->coef[i] == -1)
188 fprintf (file, " - %s", omega_variable_to_str (pb, i));
189 else
190 fprintf (file, "%d * %s", c * e->coef[i],
191 omega_variable_to_str (pb, i));
194 if (!first && c * e->coef[0] > 0)
195 fprintf (file, " + ");
197 if (first || c * e->coef[0] != 0)
198 fprintf (file, "%d", c * e->coef[0]);
201 /* Print to FILE the equation E of problem PB. */
203 void
204 omega_print_eqn (FILE *file, omega_pb pb, eqn e, bool test, int extra)
206 int i;
207 int n = pb->num_vars + extra;
208 bool is_lt = test && e->coef[0] == -1;
209 bool first;
211 if (test)
213 if (e->touched)
214 fprintf (file, "!");
216 else if (e->key != 0)
217 fprintf (file, "%d: ", e->key);
220 if (e->color == omega_red)
221 fprintf (file, "[");
223 first = true;
225 for (i = is_lt ? 1 : 0; i <= n; i++)
226 if (e->coef[i] < 0)
228 if (!first)
229 fprintf (file, " + ");
230 else
231 first = false;
233 if (i == 0)
234 fprintf (file, "%d", -e->coef[i]);
235 else if (e->coef[i] == -1)
236 fprintf (file, "%s", omega_variable_to_str (pb, i));
237 else
238 fprintf (file, "%d * %s", -e->coef[i],
239 omega_variable_to_str (pb, i));
242 if (first)
244 if (is_lt)
246 fprintf (file, "1");
247 is_lt = false;
249 else
250 fprintf (file, "0");
253 if (test == 0)
254 fprintf (file, " = ");
255 else if (is_lt)
256 fprintf (file, " < ");
257 else
258 fprintf (file, " <= ");
260 first = true;
262 for (i = 0; i <= n; i++)
263 if (e->coef[i] > 0)
265 if (!first)
266 fprintf (file, " + ");
267 else
268 first = false;
270 if (i == 0)
271 fprintf (file, "%d", e->coef[i]);
272 else if (e->coef[i] == 1)
273 fprintf (file, "%s", omega_variable_to_str (pb, i));
274 else
275 fprintf (file, "%d * %s", e->coef[i],
276 omega_variable_to_str (pb, i));
279 if (first)
280 fprintf (file, "0");
282 if (e->color == omega_red)
283 fprintf (file, "]");
286 /* Print to FILE all the variables of problem PB. */
288 static void
289 omega_print_vars (FILE *file, omega_pb pb)
291 int i;
293 fprintf (file, "variables = ");
295 if (pb->safe_vars > 0)
296 fprintf (file, "protected (");
298 for (i = 1; i <= pb->num_vars; i++)
300 fprintf (file, "%s", omega_variable_to_str (pb, i));
302 if (i == pb->safe_vars)
303 fprintf (file, ")");
305 if (i < pb->num_vars)
306 fprintf (file, ", ");
309 fprintf (file, "\n");
312 /* Dump problem PB. */
314 DEBUG_FUNCTION void
315 debug (omega_pb_d &ref)
317 omega_print_problem (stderr, &ref);
320 DEBUG_FUNCTION void
321 debug (omega_pb_d *ptr)
323 if (ptr)
324 debug (*ptr);
325 else
326 fprintf (stderr, "<nil>\n");
329 /* Debug problem PB. */
331 DEBUG_FUNCTION void
332 debug_omega_problem (omega_pb pb)
334 omega_print_problem (stderr, pb);
337 /* Print to FILE problem PB. */
339 void
340 omega_print_problem (FILE *file, omega_pb pb)
342 int e;
344 if (!pb->variables_initialized)
345 omega_initialize_variables (pb);
347 omega_print_vars (file, pb);
349 for (e = 0; e < pb->num_eqs; e++)
351 omega_print_eq (file, pb, &pb->eqs[e]);
352 fprintf (file, "\n");
355 fprintf (file, "Done with EQ\n");
357 for (e = 0; e < pb->num_geqs; e++)
359 omega_print_geq (file, pb, &pb->geqs[e]);
360 fprintf (file, "\n");
363 fprintf (file, "Done with GEQ\n");
365 for (e = 0; e < pb->num_subs; e++)
367 eqn eq = &pb->subs[e];
369 if (eq->color == omega_red)
370 fprintf (file, "[");
372 if (eq->key > 0)
373 fprintf (file, "%s := ", omega_var_to_str (eq->key));
374 else
375 fprintf (file, "#%d := ", eq->key);
377 omega_print_term (file, pb, eq, 1);
379 if (eq->color == omega_red)
380 fprintf (file, "]");
382 fprintf (file, "\n");
386 /* Return the number of equations in PB tagged omega_red. */
389 omega_count_red_equations (omega_pb pb)
391 int e, i;
392 int result = 0;
394 for (e = 0; e < pb->num_eqs; e++)
395 if (pb->eqs[e].color == omega_red)
397 for (i = pb->num_vars; i > 0; i--)
398 if (pb->geqs[e].coef[i])
399 break;
401 if (i == 0 && pb->geqs[e].coef[0] == 1)
402 return 0;
403 else
404 result += 2;
407 for (e = 0; e < pb->num_geqs; e++)
408 if (pb->geqs[e].color == omega_red)
409 result += 1;
411 for (e = 0; e < pb->num_subs; e++)
412 if (pb->subs[e].color == omega_red)
413 result += 2;
415 return result;
418 /* Print to FILE all the equations in PB that are tagged omega_red. */
420 void
421 omega_print_red_equations (FILE *file, omega_pb pb)
423 int e;
425 if (!pb->variables_initialized)
426 omega_initialize_variables (pb);
428 omega_print_vars (file, pb);
430 for (e = 0; e < pb->num_eqs; e++)
431 if (pb->eqs[e].color == omega_red)
433 omega_print_eq (file, pb, &pb->eqs[e]);
434 fprintf (file, "\n");
437 for (e = 0; e < pb->num_geqs; e++)
438 if (pb->geqs[e].color == omega_red)
440 omega_print_geq (file, pb, &pb->geqs[e]);
441 fprintf (file, "\n");
444 for (e = 0; e < pb->num_subs; e++)
445 if (pb->subs[e].color == omega_red)
447 eqn eq = &pb->subs[e];
448 fprintf (file, "[");
450 if (eq->key > 0)
451 fprintf (file, "%s := ", omega_var_to_str (eq->key));
452 else
453 fprintf (file, "#%d := ", eq->key);
455 omega_print_term (file, pb, eq, 1);
456 fprintf (file, "]\n");
460 /* Pretty print PB to FILE. */
462 void
463 omega_pretty_print_problem (FILE *file, omega_pb pb)
465 int e, v, v1, v2, v3, t;
466 bool *live = XNEWVEC (bool, OMEGA_MAX_GEQS);
467 int stuffPrinted = 0;
468 bool change;
470 typedef enum {
471 none, le, lt
472 } partial_order_type;
474 partial_order_type **po = XNEWVEC (partial_order_type *,
475 OMEGA_MAX_VARS * OMEGA_MAX_VARS);
476 int **po_eq = XNEWVEC (int *, OMEGA_MAX_VARS * OMEGA_MAX_VARS);
477 int *last_links = XNEWVEC (int, OMEGA_MAX_VARS);
478 int *first_links = XNEWVEC (int, OMEGA_MAX_VARS);
479 int *chain_length = XNEWVEC (int, OMEGA_MAX_VARS);
480 int *chain = XNEWVEC (int, OMEGA_MAX_VARS);
481 int i, m;
482 bool multiprint;
484 if (!pb->variables_initialized)
485 omega_initialize_variables (pb);
487 if (pb->num_vars > 0)
489 omega_eliminate_redundant (pb, false);
491 for (e = 0; e < pb->num_eqs; e++)
493 if (stuffPrinted)
494 fprintf (file, "; ");
496 stuffPrinted = 1;
497 omega_print_eq (file, pb, &pb->eqs[e]);
500 for (e = 0; e < pb->num_geqs; e++)
501 live[e] = true;
503 while (1)
505 for (v = 1; v <= pb->num_vars; v++)
507 last_links[v] = first_links[v] = 0;
508 chain_length[v] = 0;
510 for (v2 = 1; v2 <= pb->num_vars; v2++)
511 po[v][v2] = none;
514 for (e = 0; e < pb->num_geqs; e++)
515 if (live[e])
517 for (v = 1; v <= pb->num_vars; v++)
518 if (pb->geqs[e].coef[v] == 1)
519 first_links[v]++;
520 else if (pb->geqs[e].coef[v] == -1)
521 last_links[v]++;
523 v1 = pb->num_vars;
525 while (v1 > 0 && pb->geqs[e].coef[v1] == 0)
526 v1--;
528 v2 = v1 - 1;
530 while (v2 > 0 && pb->geqs[e].coef[v2] == 0)
531 v2--;
533 v3 = v2 - 1;
535 while (v3 > 0 && pb->geqs[e].coef[v3] == 0)
536 v3--;
538 if (pb->geqs[e].coef[0] > 0 || pb->geqs[e].coef[0] < -1
539 || v2 <= 0 || v3 > 0
540 || pb->geqs[e].coef[v1] * pb->geqs[e].coef[v2] != -1)
542 /* Not a partial order relation. */
544 else
546 if (pb->geqs[e].coef[v1] == 1)
548 v3 = v2;
549 v2 = v1;
550 v1 = v3;
553 /* Relation is v1 <= v2 or v1 < v2. */
554 po[v1][v2] = ((pb->geqs[e].coef[0] == 0) ? le : lt);
555 po_eq[v1][v2] = e;
558 for (v = 1; v <= pb->num_vars; v++)
559 chain_length[v] = last_links[v];
561 /* Just in case pb->num_vars <= 0. */
562 change = false;
563 for (t = 0; t < pb->num_vars; t++)
565 change = false;
567 for (v1 = 1; v1 <= pb->num_vars; v1++)
568 for (v2 = 1; v2 <= pb->num_vars; v2++)
569 if (po[v1][v2] != none &&
570 chain_length[v1] <= chain_length[v2])
572 chain_length[v1] = chain_length[v2] + 1;
573 change = true;
577 /* Caught in cycle. */
578 gcc_assert (!change);
580 for (v1 = 1; v1 <= pb->num_vars; v1++)
581 if (chain_length[v1] == 0)
582 first_links[v1] = 0;
584 v = 1;
586 for (v1 = 2; v1 <= pb->num_vars; v1++)
587 if (chain_length[v1] + first_links[v1] >
588 chain_length[v] + first_links[v])
589 v = v1;
591 if (chain_length[v] + first_links[v] == 0)
592 break;
594 if (stuffPrinted)
595 fprintf (file, "; ");
597 stuffPrinted = 1;
599 /* Chain starts at v. */
601 int tmp;
602 bool first = true;
604 for (e = 0; e < pb->num_geqs; e++)
605 if (live[e] && pb->geqs[e].coef[v] == 1)
607 if (!first)
608 fprintf (file, ", ");
610 tmp = pb->geqs[e].coef[v];
611 pb->geqs[e].coef[v] = 0;
612 omega_print_term (file, pb, &pb->geqs[e], -1);
613 pb->geqs[e].coef[v] = tmp;
614 live[e] = false;
615 first = false;
618 if (!first)
619 fprintf (file, " <= ");
622 /* Find chain. */
623 chain[0] = v;
624 m = 1;
625 while (1)
627 /* Print chain. */
628 for (v2 = 1; v2 <= pb->num_vars; v2++)
629 if (po[v][v2] && chain_length[v] == 1 + chain_length[v2])
630 break;
632 if (v2 > pb->num_vars)
633 break;
635 chain[m++] = v2;
636 v = v2;
639 fprintf (file, "%s", omega_variable_to_str (pb, chain[0]));
641 for (multiprint = false, i = 1; i < m; i++)
643 v = chain[i - 1];
644 v2 = chain[i];
646 if (po[v][v2] == le)
647 fprintf (file, " <= ");
648 else
649 fprintf (file, " < ");
651 fprintf (file, "%s", omega_variable_to_str (pb, v2));
652 live[po_eq[v][v2]] = false;
654 if (!multiprint && i < m - 1)
655 for (v3 = 1; v3 <= pb->num_vars; v3++)
657 if (v == v3 || v2 == v3
658 || po[v][v2] != po[v][v3]
659 || po[v2][chain[i + 1]] != po[v3][chain[i + 1]])
660 continue;
662 fprintf (file, ",%s", omega_variable_to_str (pb, v3));
663 live[po_eq[v][v3]] = false;
664 live[po_eq[v3][chain[i + 1]]] = false;
665 multiprint = true;
667 else
668 multiprint = false;
671 v = chain[m - 1];
672 /* Print last_links. */
674 int tmp;
675 bool first = true;
677 for (e = 0; e < pb->num_geqs; e++)
678 if (live[e] && pb->geqs[e].coef[v] == -1)
680 if (!first)
681 fprintf (file, ", ");
682 else
683 fprintf (file, " <= ");
685 tmp = pb->geqs[e].coef[v];
686 pb->geqs[e].coef[v] = 0;
687 omega_print_term (file, pb, &pb->geqs[e], 1);
688 pb->geqs[e].coef[v] = tmp;
689 live[e] = false;
690 first = false;
695 for (e = 0; e < pb->num_geqs; e++)
696 if (live[e])
698 if (stuffPrinted)
699 fprintf (file, "; ");
700 stuffPrinted = 1;
701 omega_print_geq (file, pb, &pb->geqs[e]);
704 for (e = 0; e < pb->num_subs; e++)
706 eqn eq = &pb->subs[e];
708 if (stuffPrinted)
709 fprintf (file, "; ");
711 stuffPrinted = 1;
713 if (eq->key > 0)
714 fprintf (file, "%s := ", omega_var_to_str (eq->key));
715 else
716 fprintf (file, "#%d := ", eq->key);
718 omega_print_term (file, pb, eq, 1);
722 free (live);
723 free (po);
724 free (po_eq);
725 free (last_links);
726 free (first_links);
727 free (chain_length);
728 free (chain);
731 /* Assign to variable I in PB the next wildcard name. The name of a
732 wildcard is a negative number. */
733 static int next_wild_card = 0;
735 static void
736 omega_name_wild_card (omega_pb pb, int i)
738 --next_wild_card;
739 if (next_wild_card < -PARAM_VALUE (PARAM_OMEGA_MAX_WILD_CARDS))
740 next_wild_card = -1;
741 pb->var[i] = next_wild_card;
744 /* Return the index of the last protected (or safe) variable in PB,
745 after having added a new wildcard variable. */
747 static int
748 omega_add_new_wild_card (omega_pb pb)
750 int e;
751 int i = ++pb->safe_vars;
752 pb->num_vars++;
754 /* Make a free place in the protected (safe) variables, by moving
755 the non protected variable pointed by "I" at the end, ie. at
756 offset pb->num_vars. */
757 if (pb->num_vars != i)
759 /* Move "I" for all the inequalities. */
760 for (e = pb->num_geqs - 1; e >= 0; e--)
762 if (pb->geqs[e].coef[i])
763 pb->geqs[e].touched = 1;
765 pb->geqs[e].coef[pb->num_vars] = pb->geqs[e].coef[i];
768 /* Move "I" for all the equalities. */
769 for (e = pb->num_eqs - 1; e >= 0; e--)
770 pb->eqs[e].coef[pb->num_vars] = pb->eqs[e].coef[i];
772 /* Move "I" for all the substitutions. */
773 for (e = pb->num_subs - 1; e >= 0; e--)
774 pb->subs[e].coef[pb->num_vars] = pb->subs[e].coef[i];
776 /* Move the identifier. */
777 pb->var[pb->num_vars] = pb->var[i];
780 /* Initialize at zero all the coefficients */
781 for (e = pb->num_geqs - 1; e >= 0; e--)
782 pb->geqs[e].coef[i] = 0;
784 for (e = pb->num_eqs - 1; e >= 0; e--)
785 pb->eqs[e].coef[i] = 0;
787 for (e = pb->num_subs - 1; e >= 0; e--)
788 pb->subs[e].coef[i] = 0;
790 /* And give it a name. */
791 omega_name_wild_card (pb, i);
792 return i;
795 /* Delete inequality E from problem PB that has N_VARS variables. */
797 static void
798 omega_delete_geq (omega_pb pb, int e, int n_vars)
800 if (dump_file && (dump_flags & TDF_DETAILS))
802 fprintf (dump_file, "Deleting %d (last:%d): ", e, pb->num_geqs - 1);
803 omega_print_geq (dump_file, pb, &pb->geqs[e]);
804 fprintf (dump_file, "\n");
807 if (e < pb->num_geqs - 1)
808 omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
810 pb->num_geqs--;
813 /* Delete extra inequality E from problem PB that has N_VARS
814 variables. */
816 static void
817 omega_delete_geq_extra (omega_pb pb, int e, int n_vars)
819 if (dump_file && (dump_flags & TDF_DETAILS))
821 fprintf (dump_file, "Deleting %d: ",e);
822 omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
823 fprintf (dump_file, "\n");
826 if (e < pb->num_geqs - 1)
827 omega_copy_eqn (&pb->geqs[e], &pb->geqs[pb->num_geqs - 1], n_vars);
829 pb->num_geqs--;
833 /* Remove variable I from problem PB. */
835 static void
836 omega_delete_variable (omega_pb pb, int i)
838 int n_vars = pb->num_vars;
839 int e;
841 if (omega_safe_var_p (pb, i))
843 int j = pb->safe_vars;
845 for (e = pb->num_geqs - 1; e >= 0; e--)
847 pb->geqs[e].touched = 1;
848 pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
849 pb->geqs[e].coef[j] = pb->geqs[e].coef[n_vars];
852 for (e = pb->num_eqs - 1; e >= 0; e--)
854 pb->eqs[e].coef[i] = pb->eqs[e].coef[j];
855 pb->eqs[e].coef[j] = pb->eqs[e].coef[n_vars];
858 for (e = pb->num_subs - 1; e >= 0; e--)
860 pb->subs[e].coef[i] = pb->subs[e].coef[j];
861 pb->subs[e].coef[j] = pb->subs[e].coef[n_vars];
864 pb->var[i] = pb->var[j];
865 pb->var[j] = pb->var[n_vars];
867 else if (i < n_vars)
869 for (e = pb->num_geqs - 1; e >= 0; e--)
870 if (pb->geqs[e].coef[n_vars])
872 pb->geqs[e].coef[i] = pb->geqs[e].coef[n_vars];
873 pb->geqs[e].touched = 1;
876 for (e = pb->num_eqs - 1; e >= 0; e--)
877 pb->eqs[e].coef[i] = pb->eqs[e].coef[n_vars];
879 for (e = pb->num_subs - 1; e >= 0; e--)
880 pb->subs[e].coef[i] = pb->subs[e].coef[n_vars];
882 pb->var[i] = pb->var[n_vars];
885 if (omega_safe_var_p (pb, i))
886 pb->safe_vars--;
888 pb->num_vars--;
891 /* Because the coefficients of an equation are sparse, PACKING records
892 indices for non null coefficients. */
893 static int *packing;
895 /* Set up the coefficients of PACKING, following the coefficients of
896 equation EQN that has NUM_VARS variables. */
898 static inline int
899 setup_packing (eqn eqn, int num_vars)
901 int k;
902 int n = 0;
904 for (k = num_vars; k >= 0; k--)
905 if (eqn->coef[k])
906 packing[n++] = k;
908 return n;
911 /* Computes a linear combination of EQ and SUB at VAR with coefficient
912 C, such that EQ->coef[VAR] is set to 0. TOP_VAR is the number of
913 non null indices of SUB stored in PACKING. */
915 static inline void
916 omega_substitute_red_1 (eqn eq, eqn sub, int var, int c, bool *found_black,
917 int top_var)
919 if (eq->coef[var] != 0)
921 if (eq->color == omega_black)
922 *found_black = true;
923 else
925 int j, k = eq->coef[var];
927 eq->coef[var] = 0;
929 for (j = top_var; j >= 0; j--)
930 eq->coef[packing[j]] -= sub->coef[packing[j]] * k * c;
935 /* Substitute in PB variable VAR with "C * SUB". */
937 static void
938 omega_substitute_red (omega_pb pb, eqn sub, int var, int c, bool *found_black)
940 int e, top_var = setup_packing (sub, pb->num_vars);
942 *found_black = false;
944 if (dump_file && (dump_flags & TDF_DETAILS))
946 if (sub->color == omega_red)
947 fprintf (dump_file, "[");
949 fprintf (dump_file, "substituting using %s := ",
950 omega_variable_to_str (pb, var));
951 omega_print_term (dump_file, pb, sub, -c);
953 if (sub->color == omega_red)
954 fprintf (dump_file, "]");
956 fprintf (dump_file, "\n");
957 omega_print_vars (dump_file, pb);
960 for (e = pb->num_eqs - 1; e >= 0; e--)
962 eqn eqn = &(pb->eqs[e]);
964 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
966 if (dump_file && (dump_flags & TDF_DETAILS))
968 omega_print_eq (dump_file, pb, eqn);
969 fprintf (dump_file, "\n");
973 for (e = pb->num_geqs - 1; e >= 0; e--)
975 eqn eqn = &(pb->geqs[e]);
977 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
979 if (eqn->coef[var] && eqn->color == omega_red)
980 eqn->touched = 1;
982 if (dump_file && (dump_flags & TDF_DETAILS))
984 omega_print_geq (dump_file, pb, eqn);
985 fprintf (dump_file, "\n");
989 for (e = pb->num_subs - 1; e >= 0; e--)
991 eqn eqn = &(pb->subs[e]);
993 omega_substitute_red_1 (eqn, sub, var, c, found_black, top_var);
995 if (dump_file && (dump_flags & TDF_DETAILS))
997 fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
998 omega_print_term (dump_file, pb, eqn, 1);
999 fprintf (dump_file, "\n");
1003 if (dump_file && (dump_flags & TDF_DETAILS))
1004 fprintf (dump_file, "---\n\n");
1006 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1007 *found_black = true;
1010 /* Substitute in PB variable VAR with "C * SUB". */
1012 static void
1013 omega_substitute (omega_pb pb, eqn sub, int var, int c)
1015 int e, j, j0;
1016 int top_var = setup_packing (sub, pb->num_vars);
1018 if (dump_file && (dump_flags & TDF_DETAILS))
1020 fprintf (dump_file, "substituting using %s := ",
1021 omega_variable_to_str (pb, var));
1022 omega_print_term (dump_file, pb, sub, -c);
1023 fprintf (dump_file, "\n");
1024 omega_print_vars (dump_file, pb);
1027 if (top_var < 0)
1029 for (e = pb->num_eqs - 1; e >= 0; e--)
1030 pb->eqs[e].coef[var] = 0;
1032 for (e = pb->num_geqs - 1; e >= 0; e--)
1033 if (pb->geqs[e].coef[var] != 0)
1035 pb->geqs[e].touched = 1;
1036 pb->geqs[e].coef[var] = 0;
1039 for (e = pb->num_subs - 1; e >= 0; e--)
1040 pb->subs[e].coef[var] = 0;
1042 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1044 int k;
1045 eqn eqn = &(pb->subs[pb->num_subs++]);
1047 for (k = pb->num_vars; k >= 0; k--)
1048 eqn->coef[k] = 0;
1050 eqn->key = pb->var[var];
1051 eqn->color = omega_black;
1054 else if (top_var == 0 && packing[0] == 0)
1056 c = -sub->coef[0] * c;
1058 for (e = pb->num_eqs - 1; e >= 0; e--)
1060 pb->eqs[e].coef[0] += pb->eqs[e].coef[var] * c;
1061 pb->eqs[e].coef[var] = 0;
1064 for (e = pb->num_geqs - 1; e >= 0; e--)
1065 if (pb->geqs[e].coef[var] != 0)
1067 pb->geqs[e].coef[0] += pb->geqs[e].coef[var] * c;
1068 pb->geqs[e].coef[var] = 0;
1069 pb->geqs[e].touched = 1;
1072 for (e = pb->num_subs - 1; e >= 0; e--)
1074 pb->subs[e].coef[0] += pb->subs[e].coef[var] * c;
1075 pb->subs[e].coef[var] = 0;
1078 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1080 int k;
1081 eqn eqn = &(pb->subs[pb->num_subs++]);
1083 for (k = pb->num_vars; k >= 1; k--)
1084 eqn->coef[k] = 0;
1086 eqn->coef[0] = c;
1087 eqn->key = pb->var[var];
1088 eqn->color = omega_black;
1091 if (dump_file && (dump_flags & TDF_DETAILS))
1093 fprintf (dump_file, "---\n\n");
1094 omega_print_problem (dump_file, pb);
1095 fprintf (dump_file, "===\n\n");
1098 else
1100 for (e = pb->num_eqs - 1; e >= 0; e--)
1102 eqn eqn = &(pb->eqs[e]);
1103 int k = eqn->coef[var];
1105 if (k != 0)
1107 k = c * k;
1108 eqn->coef[var] = 0;
1110 for (j = top_var; j >= 0; j--)
1112 j0 = packing[j];
1113 eqn->coef[j0] -= sub->coef[j0] * k;
1117 if (dump_file && (dump_flags & TDF_DETAILS))
1119 omega_print_eq (dump_file, pb, eqn);
1120 fprintf (dump_file, "\n");
1124 for (e = pb->num_geqs - 1; e >= 0; e--)
1126 eqn eqn = &(pb->geqs[e]);
1127 int k = eqn->coef[var];
1129 if (k != 0)
1131 k = c * k;
1132 eqn->touched = 1;
1133 eqn->coef[var] = 0;
1135 for (j = top_var; j >= 0; j--)
1137 j0 = packing[j];
1138 eqn->coef[j0] -= sub->coef[j0] * k;
1142 if (dump_file && (dump_flags & TDF_DETAILS))
1144 omega_print_geq (dump_file, pb, eqn);
1145 fprintf (dump_file, "\n");
1149 for (e = pb->num_subs - 1; e >= 0; e--)
1151 eqn eqn = &(pb->subs[e]);
1152 int k = eqn->coef[var];
1154 if (k != 0)
1156 k = c * k;
1157 eqn->coef[var] = 0;
1159 for (j = top_var; j >= 0; j--)
1161 j0 = packing[j];
1162 eqn->coef[j0] -= sub->coef[j0] * k;
1166 if (dump_file && (dump_flags & TDF_DETAILS))
1168 fprintf (dump_file, "%s := ", omega_var_to_str (eqn->key));
1169 omega_print_term (dump_file, pb, eqn, 1);
1170 fprintf (dump_file, "\n");
1174 if (dump_file && (dump_flags & TDF_DETAILS))
1176 fprintf (dump_file, "---\n\n");
1177 omega_print_problem (dump_file, pb);
1178 fprintf (dump_file, "===\n\n");
1181 if (omega_safe_var_p (pb, var) && !omega_wildcard_p (pb, var))
1183 int k;
1184 eqn eqn = &(pb->subs[pb->num_subs++]);
1185 c = -c;
1187 for (k = pb->num_vars; k >= 0; k--)
1188 eqn->coef[k] = c * (sub->coef[k]);
1190 eqn->key = pb->var[var];
1191 eqn->color = sub->color;
1196 /* Solve e = factor alpha for x_j and substitute. */
1198 static void
1199 omega_do_mod (omega_pb pb, int factor, int e, int j)
1201 int k, i;
1202 eqn eq = omega_alloc_eqns (0, 1);
1203 int nfactor;
1204 bool kill_j = false;
1206 omega_copy_eqn (eq, &pb->eqs[e], pb->num_vars);
1208 for (k = pb->num_vars; k >= 0; k--)
1210 eq->coef[k] = int_mod (eq->coef[k], factor);
1212 if (2 * eq->coef[k] >= factor)
1213 eq->coef[k] -= factor;
1216 nfactor = eq->coef[j];
1218 if (omega_safe_var_p (pb, j) && !omega_wildcard_p (pb, j))
1220 i = omega_add_new_wild_card (pb);
1221 eq->coef[pb->num_vars] = eq->coef[i];
1222 eq->coef[j] = 0;
1223 eq->coef[i] = -factor;
1224 kill_j = true;
1226 else
1228 eq->coef[j] = -factor;
1229 if (!omega_wildcard_p (pb, j))
1230 omega_name_wild_card (pb, j);
1233 omega_substitute (pb, eq, j, nfactor);
1235 for (k = pb->num_vars; k >= 0; k--)
1236 pb->eqs[e].coef[k] = pb->eqs[e].coef[k] / factor;
1238 if (kill_j)
1239 omega_delete_variable (pb, j);
1241 if (dump_file && (dump_flags & TDF_DETAILS))
1243 fprintf (dump_file, "Mod-ing and normalizing produces:\n");
1244 omega_print_problem (dump_file, pb);
1247 omega_free_eqns (eq, 1);
1250 /* Multiplies by -1 inequality E. */
1252 void
1253 omega_negate_geq (omega_pb pb, int e)
1255 int i;
1257 for (i = pb->num_vars; i >= 0; i--)
1258 pb->geqs[e].coef[i] *= -1;
1260 pb->geqs[e].coef[0]--;
1261 pb->geqs[e].touched = 1;
1264 /* Returns OMEGA_TRUE when problem PB has a solution. */
1266 static enum omega_result
1267 verify_omega_pb (omega_pb pb)
1269 enum omega_result result;
1270 int e;
1271 bool any_color = false;
1272 omega_pb tmp_problem = XNEW (struct omega_pb_d);
1274 omega_copy_problem (tmp_problem, pb);
1275 tmp_problem->safe_vars = 0;
1276 tmp_problem->num_subs = 0;
1278 for (e = pb->num_geqs - 1; e >= 0; e--)
1279 if (pb->geqs[e].color == omega_red)
1281 any_color = true;
1282 break;
1285 if (please_no_equalities_in_simplified_problems)
1286 any_color = true;
1288 if (any_color)
1289 original_problem = no_problem;
1290 else
1291 original_problem = pb;
1293 if (dump_file && (dump_flags & TDF_DETAILS))
1295 fprintf (dump_file, "verifying problem");
1297 if (any_color)
1298 fprintf (dump_file, " (color mode)");
1300 fprintf (dump_file, " :\n");
1301 omega_print_problem (dump_file, pb);
1304 result = omega_solve_problem (tmp_problem, omega_unknown);
1305 original_problem = no_problem;
1306 free (tmp_problem);
1308 if (dump_file && (dump_flags & TDF_DETAILS))
1310 if (result != omega_false)
1311 fprintf (dump_file, "verified problem\n");
1312 else
1313 fprintf (dump_file, "disproved problem\n");
1314 omega_print_problem (dump_file, pb);
1317 return result;
1320 /* Add a new equality to problem PB at last position E. */
1322 static void
1323 adding_equality_constraint (omega_pb pb, int e)
1325 if (original_problem != no_problem
1326 && original_problem != pb
1327 && !conservative)
1329 int i, j;
1330 int e2 = original_problem->num_eqs++;
1332 if (dump_file && (dump_flags & TDF_DETAILS))
1333 fprintf (dump_file,
1334 "adding equality constraint %d to outer problem\n", e2);
1335 omega_init_eqn_zero (&original_problem->eqs[e2],
1336 original_problem->num_vars);
1338 for (i = pb->num_vars; i >= 1; i--)
1340 for (j = original_problem->num_vars; j >= 1; j--)
1341 if (original_problem->var[j] == pb->var[i])
1342 break;
1344 if (j <= 0)
1346 if (dump_file && (dump_flags & TDF_DETAILS))
1347 fprintf (dump_file, "retracting\n");
1348 original_problem->num_eqs--;
1349 return;
1351 original_problem->eqs[e2].coef[j] = pb->eqs[e].coef[i];
1354 original_problem->eqs[e2].coef[0] = pb->eqs[e].coef[0];
1356 if (dump_file && (dump_flags & TDF_DETAILS))
1357 omega_print_problem (dump_file, original_problem);
1361 static int *fast_lookup;
1362 static int *fast_lookup_red;
1364 typedef enum {
1365 normalize_false,
1366 normalize_uncoupled,
1367 normalize_coupled
1368 } normalize_return_type;
1370 /* Normalizes PB by removing redundant constraints. Returns
1371 normalize_false when the constraints system has no solution,
1372 otherwise returns normalize_coupled or normalize_uncoupled. */
1374 static normalize_return_type
1375 normalize_omega_problem (omega_pb pb)
1377 int e, i, j, k, n_vars;
1378 int coupled_subscripts = 0;
1380 n_vars = pb->num_vars;
1382 for (e = 0; e < pb->num_geqs; e++)
1384 if (!pb->geqs[e].touched)
1386 if (!single_var_geq (&pb->geqs[e], n_vars))
1387 coupled_subscripts = 1;
1389 else
1391 int g, top_var, i0, hashCode;
1392 int *p = &packing[0];
1394 for (k = 1; k <= n_vars; k++)
1395 if (pb->geqs[e].coef[k])
1396 *(p++) = k;
1398 top_var = (p - &packing[0]) - 1;
1400 if (top_var == -1)
1402 if (pb->geqs[e].coef[0] < 0)
1404 if (dump_file && (dump_flags & TDF_DETAILS))
1406 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1407 fprintf (dump_file, "\nequations have no solution \n");
1409 return normalize_false;
1412 omega_delete_geq (pb, e, n_vars);
1413 e--;
1414 continue;
1416 else if (top_var == 0)
1418 int singlevar = packing[0];
1420 g = pb->geqs[e].coef[singlevar];
1422 if (g > 0)
1424 pb->geqs[e].coef[singlevar] = 1;
1425 pb->geqs[e].key = singlevar;
1427 else
1429 g = -g;
1430 pb->geqs[e].coef[singlevar] = -1;
1431 pb->geqs[e].key = -singlevar;
1434 if (g > 1)
1435 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1437 else
1439 int g2;
1440 int hash_key_multiplier = 31;
1442 coupled_subscripts = 1;
1443 i0 = top_var;
1444 i = packing[i0--];
1445 g = pb->geqs[e].coef[i];
1446 hashCode = g * (i + 3);
1448 if (g < 0)
1449 g = -g;
1451 for (; i0 >= 0; i0--)
1453 int x;
1455 i = packing[i0];
1456 x = pb->geqs[e].coef[i];
1457 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1459 if (x < 0)
1460 x = -x;
1462 if (x == 1)
1464 g = 1;
1465 i0--;
1466 break;
1468 else
1469 g = gcd (x, g);
1472 for (; i0 >= 0; i0--)
1474 int x;
1475 i = packing[i0];
1476 x = pb->geqs[e].coef[i];
1477 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1480 if (g > 1)
1482 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1483 i0 = top_var;
1484 i = packing[i0--];
1485 pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1486 hashCode = pb->geqs[e].coef[i] * (i + 3);
1488 for (; i0 >= 0; i0--)
1490 i = packing[i0];
1491 pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1492 hashCode = hashCode * hash_key_multiplier * (i + 3)
1493 + pb->geqs[e].coef[i];
1497 g2 = abs (hashCode);
1499 if (dump_file && (dump_flags & TDF_DETAILS))
1501 fprintf (dump_file, "Hash code = %d, eqn = ", hashCode);
1502 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1503 fprintf (dump_file, "\n");
1506 j = g2 % HASH_TABLE_SIZE;
1508 do {
1509 eqn proto = &(hash_master[j]);
1511 if (proto->touched == g2)
1513 if (proto->coef[0] == top_var)
1515 if (hashCode >= 0)
1516 for (i0 = top_var; i0 >= 0; i0--)
1518 i = packing[i0];
1520 if (pb->geqs[e].coef[i] != proto->coef[i])
1521 break;
1523 else
1524 for (i0 = top_var; i0 >= 0; i0--)
1526 i = packing[i0];
1528 if (pb->geqs[e].coef[i] != -proto->coef[i])
1529 break;
1532 if (i0 < 0)
1534 if (hashCode >= 0)
1535 pb->geqs[e].key = proto->key;
1536 else
1537 pb->geqs[e].key = -proto->key;
1538 break;
1542 else if (proto->touched < 0)
1544 omega_init_eqn_zero (proto, pb->num_vars);
1545 if (hashCode >= 0)
1546 for (i0 = top_var; i0 >= 0; i0--)
1548 i = packing[i0];
1549 proto->coef[i] = pb->geqs[e].coef[i];
1551 else
1552 for (i0 = top_var; i0 >= 0; i0--)
1554 i = packing[i0];
1555 proto->coef[i] = -pb->geqs[e].coef[i];
1558 proto->coef[0] = top_var;
1559 proto->touched = g2;
1561 if (dump_file && (dump_flags & TDF_DETAILS))
1562 fprintf (dump_file, " constraint key = %d\n",
1563 next_key);
1565 proto->key = next_key++;
1567 /* Too many hash keys generated. */
1568 gcc_assert (proto->key <= MAX_KEYS);
1570 if (hashCode >= 0)
1571 pb->geqs[e].key = proto->key;
1572 else
1573 pb->geqs[e].key = -proto->key;
1575 break;
1578 j = (j + 1) % HASH_TABLE_SIZE;
1579 } while (1);
1582 pb->geqs[e].touched = 0;
1586 int eKey = pb->geqs[e].key;
1587 int e2;
1588 if (e > 0)
1590 int cTerm = pb->geqs[e].coef[0];
1591 e2 = fast_lookup[MAX_KEYS - eKey];
1593 if (e2 < e && pb->geqs[e2].key == -eKey
1594 && pb->geqs[e2].color == omega_black)
1596 if (pb->geqs[e2].coef[0] < -cTerm)
1598 if (dump_file && (dump_flags & TDF_DETAILS))
1600 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1601 fprintf (dump_file, "\n");
1602 omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1603 fprintf (dump_file,
1604 "\nequations have no solution \n");
1606 return normalize_false;
1609 if (pb->geqs[e2].coef[0] == -cTerm
1610 && (create_color
1611 || pb->geqs[e].color == omega_black))
1613 omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1614 pb->num_vars);
1615 if (pb->geqs[e].color == omega_black)
1616 adding_equality_constraint (pb, pb->num_eqs);
1617 pb->num_eqs++;
1618 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1622 e2 = fast_lookup_red[MAX_KEYS - eKey];
1624 if (e2 < e && pb->geqs[e2].key == -eKey
1625 && pb->geqs[e2].color == omega_red)
1627 if (pb->geqs[e2].coef[0] < -cTerm)
1629 if (dump_file && (dump_flags & TDF_DETAILS))
1631 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1632 fprintf (dump_file, "\n");
1633 omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1634 fprintf (dump_file,
1635 "\nequations have no solution \n");
1637 return normalize_false;
1640 if (pb->geqs[e2].coef[0] == -cTerm && create_color)
1642 omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1643 pb->num_vars);
1644 pb->eqs[pb->num_eqs].color = omega_red;
1645 pb->num_eqs++;
1646 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1650 e2 = fast_lookup[MAX_KEYS + eKey];
1652 if (e2 < e && pb->geqs[e2].key == eKey
1653 && pb->geqs[e2].color == omega_black)
1655 if (pb->geqs[e2].coef[0] > cTerm)
1657 if (pb->geqs[e].color == omega_black)
1659 if (dump_file && (dump_flags & TDF_DETAILS))
1661 fprintf (dump_file,
1662 "Removing Redundant Equation: ");
1663 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1664 fprintf (dump_file, "\n");
1665 fprintf (dump_file,
1666 "[a] Made Redundant by: ");
1667 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1668 fprintf (dump_file, "\n");
1670 pb->geqs[e2].coef[0] = cTerm;
1671 omega_delete_geq (pb, e, n_vars);
1672 e--;
1673 continue;
1676 else
1678 if (dump_file && (dump_flags & TDF_DETAILS))
1680 fprintf (dump_file, "Removing Redundant Equation: ");
1681 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1682 fprintf (dump_file, "\n");
1683 fprintf (dump_file, "[b] Made Redundant by: ");
1684 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1685 fprintf (dump_file, "\n");
1687 omega_delete_geq (pb, e, n_vars);
1688 e--;
1689 continue;
1693 e2 = fast_lookup_red[MAX_KEYS + eKey];
1695 if (e2 < e && pb->geqs[e2].key == eKey
1696 && pb->geqs[e2].color == omega_red)
1698 if (pb->geqs[e2].coef[0] >= cTerm)
1700 if (dump_file && (dump_flags & TDF_DETAILS))
1702 fprintf (dump_file, "Removing Redundant Equation: ");
1703 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1704 fprintf (dump_file, "\n");
1705 fprintf (dump_file, "[c] Made Redundant by: ");
1706 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1707 fprintf (dump_file, "\n");
1709 pb->geqs[e2].coef[0] = cTerm;
1710 pb->geqs[e2].color = pb->geqs[e].color;
1712 else if (pb->geqs[e].color == omega_red)
1714 if (dump_file && (dump_flags & TDF_DETAILS))
1716 fprintf (dump_file, "Removing Redundant Equation: ");
1717 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1718 fprintf (dump_file, "\n");
1719 fprintf (dump_file, "[d] Made Redundant by: ");
1720 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1721 fprintf (dump_file, "\n");
1724 omega_delete_geq (pb, e, n_vars);
1725 e--;
1726 continue;
1731 if (pb->geqs[e].color == omega_red)
1732 fast_lookup_red[MAX_KEYS + eKey] = e;
1733 else
1734 fast_lookup[MAX_KEYS + eKey] = e;
1738 create_color = false;
1739 return coupled_subscripts ? normalize_coupled : normalize_uncoupled;
1742 /* Divide the coefficients of EQN by their gcd. N_VARS is the number
1743 of variables in EQN. */
1745 static inline void
1746 divide_eqn_by_gcd (eqn eqn, int n_vars)
1748 int var, g = 0;
1750 for (var = n_vars; var >= 0; var--)
1751 g = gcd (abs (eqn->coef[var]), g);
1753 if (g)
1754 for (var = n_vars; var >= 0; var--)
1755 eqn->coef[var] = eqn->coef[var] / g;
1758 /* Rewrite some non-safe variables in function of protected
1759 wildcard variables. */
1761 static void
1762 cleanout_wildcards (omega_pb pb)
1764 int e, i, j;
1765 int n_vars = pb->num_vars;
1766 bool renormalize = false;
1768 for (e = pb->num_eqs - 1; e >= 0; e--)
1769 for (i = n_vars; !omega_safe_var_p (pb, i); i--)
1770 if (pb->eqs[e].coef[i] != 0)
1772 /* i is the last nonzero non-safe variable. */
1774 for (j = i - 1; !omega_safe_var_p (pb, j); j--)
1775 if (pb->eqs[e].coef[j] != 0)
1776 break;
1778 /* j is the next nonzero non-safe variable, or points
1779 to a safe variable: it is then a wildcard variable. */
1781 /* Clean it out. */
1782 if (omega_safe_var_p (pb, j))
1784 eqn sub = &(pb->eqs[e]);
1785 int c = pb->eqs[e].coef[i];
1786 int a = abs (c);
1787 int e2;
1789 if (dump_file && (dump_flags & TDF_DETAILS))
1791 fprintf (dump_file,
1792 "Found a single wild card equality: ");
1793 omega_print_eq (dump_file, pb, &pb->eqs[e]);
1794 fprintf (dump_file, "\n");
1795 omega_print_problem (dump_file, pb);
1798 for (e2 = pb->num_eqs - 1; e2 >= 0; e2--)
1799 if (e != e2 && pb->eqs[e2].coef[i]
1800 && (pb->eqs[e2].color == omega_red
1801 || (pb->eqs[e2].color == omega_black
1802 && pb->eqs[e].color == omega_black)))
1804 eqn eqn = &(pb->eqs[e2]);
1805 int var, k;
1807 for (var = n_vars; var >= 0; var--)
1808 eqn->coef[var] *= a;
1810 k = eqn->coef[i];
1812 for (var = n_vars; var >= 0; var--)
1813 eqn->coef[var] -= sub->coef[var] * k / c;
1815 eqn->coef[i] = 0;
1816 divide_eqn_by_gcd (eqn, n_vars);
1819 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
1820 if (pb->geqs[e2].coef[i]
1821 && (pb->geqs[e2].color == omega_red
1822 || (pb->eqs[e].color == omega_black
1823 && pb->geqs[e2].color == omega_black)))
1825 eqn eqn = &(pb->geqs[e2]);
1826 int var, k;
1828 for (var = n_vars; var >= 0; var--)
1829 eqn->coef[var] *= a;
1831 k = eqn->coef[i];
1833 for (var = n_vars; var >= 0; var--)
1834 eqn->coef[var] -= sub->coef[var] * k / c;
1836 eqn->coef[i] = 0;
1837 eqn->touched = 1;
1838 renormalize = true;
1841 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
1842 if (pb->subs[e2].coef[i]
1843 && (pb->subs[e2].color == omega_red
1844 || (pb->subs[e2].color == omega_black
1845 && pb->eqs[e].color == omega_black)))
1847 eqn eqn = &(pb->subs[e2]);
1848 int var, k;
1850 for (var = n_vars; var >= 0; var--)
1851 eqn->coef[var] *= a;
1853 k = eqn->coef[i];
1855 for (var = n_vars; var >= 0; var--)
1856 eqn->coef[var] -= sub->coef[var] * k / c;
1858 eqn->coef[i] = 0;
1859 divide_eqn_by_gcd (eqn, n_vars);
1862 if (dump_file && (dump_flags & TDF_DETAILS))
1864 fprintf (dump_file, "cleaned-out wildcard: ");
1865 omega_print_problem (dump_file, pb);
1867 break;
1871 if (renormalize)
1872 normalize_omega_problem (pb);
1875 /* Swap values contained in I and J. */
1877 static inline void
1878 swap (int *i, int *j)
1880 int tmp;
1881 tmp = *i;
1882 *i = *j;
1883 *j = tmp;
1886 /* Swap values contained in I and J. */
1888 static inline void
1889 bswap (bool *i, bool *j)
1891 bool tmp;
1892 tmp = *i;
1893 *i = *j;
1894 *j = tmp;
1897 /* Make variable IDX unprotected in PB, by swapping its index at the
1898 PB->safe_vars rank. */
1900 static inline void
1901 omega_unprotect_1 (omega_pb pb, int *idx, bool *unprotect)
1903 /* If IDX is protected... */
1904 if (*idx < pb->safe_vars)
1906 /* ... swap its index with the last non protected index. */
1907 int j = pb->safe_vars;
1908 int e;
1910 for (e = pb->num_geqs - 1; e >= 0; e--)
1912 pb->geqs[e].touched = 1;
1913 swap (&pb->geqs[e].coef[*idx], &pb->geqs[e].coef[j]);
1916 for (e = pb->num_eqs - 1; e >= 0; e--)
1917 swap (&pb->eqs[e].coef[*idx], &pb->eqs[e].coef[j]);
1919 for (e = pb->num_subs - 1; e >= 0; e--)
1920 swap (&pb->subs[e].coef[*idx], &pb->subs[e].coef[j]);
1922 if (unprotect)
1923 bswap (&unprotect[*idx], &unprotect[j]);
1925 swap (&pb->var[*idx], &pb->var[j]);
1926 pb->forwarding_address[pb->var[*idx]] = *idx;
1927 pb->forwarding_address[pb->var[j]] = j;
1928 (*idx)--;
1931 /* The variable at pb->safe_vars is also unprotected now. */
1932 pb->safe_vars--;
1935 /* During the Fourier-Motzkin elimination some variables are
1936 substituted with other variables. This function resurrects the
1937 substituted variables in PB. */
1939 static void
1940 resurrect_subs (omega_pb pb)
1942 if (pb->num_subs > 0
1943 && please_no_equalities_in_simplified_problems == 0)
1945 int i, e, m;
1947 if (dump_file && (dump_flags & TDF_DETAILS))
1949 fprintf (dump_file,
1950 "problem reduced, bringing variables back to life\n");
1951 omega_print_problem (dump_file, pb);
1954 for (i = 1; omega_safe_var_p (pb, i); i++)
1955 if (omega_wildcard_p (pb, i))
1956 omega_unprotect_1 (pb, &i, NULL);
1958 m = pb->num_subs;
1960 for (e = pb->num_geqs - 1; e >= 0; e--)
1961 if (single_var_geq (&pb->geqs[e], pb->num_vars))
1963 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
1964 pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m);
1966 else
1968 pb->geqs[e].touched = 1;
1969 pb->geqs[e].key = 0;
1972 for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--)
1974 pb->var[i + m] = pb->var[i];
1976 for (e = pb->num_geqs - 1; e >= 0; e--)
1977 pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i];
1979 for (e = pb->num_eqs - 1; e >= 0; e--)
1980 pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i];
1982 for (e = pb->num_subs - 1; e >= 0; e--)
1983 pb->subs[e].coef[i + m] = pb->subs[e].coef[i];
1986 for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--)
1988 for (e = pb->num_geqs - 1; e >= 0; e--)
1989 pb->geqs[e].coef[i] = 0;
1991 for (e = pb->num_eqs - 1; e >= 0; e--)
1992 pb->eqs[e].coef[i] = 0;
1994 for (e = pb->num_subs - 1; e >= 0; e--)
1995 pb->subs[e].coef[i] = 0;
1998 pb->num_vars += m;
2000 for (e = pb->num_subs - 1; e >= 0; e--)
2002 pb->var[pb->safe_vars + 1 + e] = pb->subs[e].key;
2003 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e]),
2004 pb->num_vars);
2005 pb->eqs[pb->num_eqs].coef[pb->safe_vars + 1 + e] = -1;
2006 pb->eqs[pb->num_eqs].color = omega_black;
2008 if (dump_file && (dump_flags & TDF_DETAILS))
2010 fprintf (dump_file, "brought back: ");
2011 omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]);
2012 fprintf (dump_file, "\n");
2015 pb->num_eqs++;
2016 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2019 pb->safe_vars += m;
2020 pb->num_subs = 0;
2022 if (dump_file && (dump_flags & TDF_DETAILS))
2024 fprintf (dump_file, "variables brought back to life\n");
2025 omega_print_problem (dump_file, pb);
2028 cleanout_wildcards (pb);
2032 static inline bool
2033 implies (unsigned int a, unsigned int b)
2035 return (a == (a & b));
2038 /* Eliminate redundant equations in PB. When EXPENSIVE is true, an
2039 extra step is performed. Returns omega_false when there exist no
2040 solution, omega_true otherwise. */
2042 enum omega_result
2043 omega_eliminate_redundant (omega_pb pb, bool expensive)
2045 int c, e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3;
2046 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2047 omega_pb tmp_problem;
2049 /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations. */
2050 unsigned int *peqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2051 unsigned int *zeqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2052 unsigned int *neqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2054 /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
2055 unsigned int pp, pz, pn;
2057 if (dump_file && (dump_flags & TDF_DETAILS))
2059 fprintf (dump_file, "in eliminate Redundant:\n");
2060 omega_print_problem (dump_file, pb);
2063 for (e = pb->num_geqs - 1; e >= 0; e--)
2065 int tmp = 1;
2067 is_dead[e] = false;
2068 peqs[e] = zeqs[e] = neqs[e] = 0;
2070 for (i = pb->num_vars; i >= 1; i--)
2072 if (pb->geqs[e].coef[i] > 0)
2073 peqs[e] |= tmp;
2074 else if (pb->geqs[e].coef[i] < 0)
2075 neqs[e] |= tmp;
2076 else
2077 zeqs[e] |= tmp;
2079 tmp <<= 1;
2084 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2085 if (!is_dead[e1])
2086 for (e2 = e1 - 1; e2 >= 0; e2--)
2087 if (!is_dead[e2])
2089 for (p = pb->num_vars; p > 1; p--)
2090 for (q = p - 1; q > 0; q--)
2091 if ((alpha = pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q]
2092 - pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]) != 0)
2093 goto foundPQ;
2095 continue;
2097 foundPQ:
2098 pz = ((zeqs[e1] & zeqs[e2]) | (peqs[e1] & neqs[e2])
2099 | (neqs[e1] & peqs[e2]));
2100 pp = peqs[e1] | peqs[e2];
2101 pn = neqs[e1] | neqs[e2];
2103 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2104 if (e3 != e1 && e3 != e2)
2106 if (!implies (zeqs[e3], pz))
2107 goto nextE3;
2109 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2110 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2111 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2112 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2113 alpha3 = alpha;
2115 if (alpha1 * alpha2 <= 0)
2116 goto nextE3;
2118 if (alpha1 < 0)
2120 alpha1 = -alpha1;
2121 alpha2 = -alpha2;
2122 alpha3 = -alpha3;
2125 if (alpha3 > 0)
2127 /* Trying to prove e3 is redundant. */
2128 if (!implies (peqs[e3], pp)
2129 || !implies (neqs[e3], pn))
2130 goto nextE3;
2132 if (pb->geqs[e3].color == omega_black
2133 && (pb->geqs[e1].color == omega_red
2134 || pb->geqs[e2].color == omega_red))
2135 goto nextE3;
2137 for (k = pb->num_vars; k >= 1; k--)
2138 if (alpha3 * pb->geqs[e3].coef[k]
2139 != (alpha1 * pb->geqs[e1].coef[k]
2140 + alpha2 * pb->geqs[e2].coef[k]))
2141 goto nextE3;
2143 c = (alpha1 * pb->geqs[e1].coef[0]
2144 + alpha2 * pb->geqs[e2].coef[0]);
2146 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2148 if (dump_file && (dump_flags & TDF_DETAILS))
2150 fprintf (dump_file,
2151 "found redundant inequality\n");
2152 fprintf (dump_file,
2153 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2154 alpha1, alpha2, alpha3);
2156 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2157 fprintf (dump_file, "\n");
2158 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2159 fprintf (dump_file, "\n=> ");
2160 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2161 fprintf (dump_file, "\n\n");
2164 is_dead[e3] = true;
2167 else
2169 /* Trying to prove e3 <= 0 and therefore e3 = 0,
2170 or trying to prove e3 < 0, and therefore the
2171 problem has no solutions. */
2172 if (!implies (peqs[e3], pn)
2173 || !implies (neqs[e3], pp))
2174 goto nextE3;
2176 if (pb->geqs[e1].color == omega_red
2177 || pb->geqs[e2].color == omega_red
2178 || pb->geqs[e3].color == omega_red)
2179 goto nextE3;
2181 /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
2182 for (k = pb->num_vars; k >= 1; k--)
2183 if (alpha3 * pb->geqs[e3].coef[k]
2184 != (alpha1 * pb->geqs[e1].coef[k]
2185 + alpha2 * pb->geqs[e2].coef[k]))
2186 goto nextE3;
2188 c = (alpha1 * pb->geqs[e1].coef[0]
2189 + alpha2 * pb->geqs[e2].coef[0]);
2191 if (c < alpha3 * (pb->geqs[e3].coef[0]))
2193 /* We just proved e3 < 0, so no solutions exist. */
2194 if (dump_file && (dump_flags & TDF_DETAILS))
2196 fprintf (dump_file,
2197 "found implied over 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=> not ");
2205 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2206 fprintf (dump_file, "\n\n");
2208 free (is_dead);
2209 free (peqs);
2210 free (zeqs);
2211 free (neqs);
2212 return omega_false;
2214 else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
2216 /* We just proved that e3 <=0, so e3 = 0. */
2217 if (dump_file && (dump_flags & TDF_DETAILS))
2219 fprintf (dump_file,
2220 "found implied tight inequality\n");
2221 fprintf (dump_file,
2222 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2223 alpha1, alpha2, -alpha3);
2224 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2225 fprintf (dump_file, "\n");
2226 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2227 fprintf (dump_file, "\n=> inverse ");
2228 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2229 fprintf (dump_file, "\n\n");
2232 omega_copy_eqn (&pb->eqs[pb->num_eqs++],
2233 &pb->geqs[e3], pb->num_vars);
2234 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2235 adding_equality_constraint (pb, pb->num_eqs - 1);
2236 is_dead[e3] = true;
2239 nextE3:;
2243 /* Delete the inequalities that were marked as dead. */
2244 for (e = pb->num_geqs - 1; e >= 0; e--)
2245 if (is_dead[e])
2246 omega_delete_geq (pb, e, pb->num_vars);
2248 if (!expensive)
2249 goto eliminate_redundant_done;
2251 tmp_problem = XNEW (struct omega_pb_d);
2252 conservative++;
2254 for (e = pb->num_geqs - 1; e >= 0; e--)
2256 if (dump_file && (dump_flags & TDF_DETAILS))
2258 fprintf (dump_file,
2259 "checking equation %d to see if it is redundant: ", e);
2260 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2261 fprintf (dump_file, "\n");
2264 omega_copy_problem (tmp_problem, pb);
2265 omega_negate_geq (tmp_problem, e);
2266 tmp_problem->safe_vars = 0;
2267 tmp_problem->variables_freed = false;
2269 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2270 omega_delete_geq (pb, e, pb->num_vars);
2273 free (tmp_problem);
2274 conservative--;
2276 if (!omega_reduce_with_subs)
2278 resurrect_subs (pb);
2279 gcc_assert (please_no_equalities_in_simplified_problems
2280 || pb->num_subs == 0);
2283 eliminate_redundant_done:
2284 free (is_dead);
2285 free (peqs);
2286 free (zeqs);
2287 free (neqs);
2288 return omega_true;
2291 /* For each inequality that has coefficients bigger than 20, try to
2292 create a new constraint that cannot be derived from the original
2293 constraint and that has smaller coefficients. Add the new
2294 constraint at the end of geqs. Return the number of inequalities
2295 that have been added to PB. */
2297 static int
2298 smooth_weird_equations (omega_pb pb)
2300 int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
2301 int c;
2302 int v;
2303 int result = 0;
2305 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2306 if (pb->geqs[e1].color == omega_black)
2308 int g = 999999;
2310 for (v = pb->num_vars; v >= 1; v--)
2311 if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g)
2312 g = abs (pb->geqs[e1].coef[v]);
2314 /* Magic number. */
2315 if (g > 20)
2317 e3 = pb->num_geqs;
2319 for (v = pb->num_vars; v >= 1; v--)
2320 pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2,
2323 pb->geqs[e3].color = omega_black;
2324 pb->geqs[e3].touched = 1;
2325 /* Magic number. */
2326 pb->geqs[e3].coef[0] = 9997;
2328 if (dump_file && (dump_flags & TDF_DETAILS))
2330 fprintf (dump_file, "Checking to see if we can derive: ");
2331 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2332 fprintf (dump_file, "\n from: ");
2333 omega_print_geq (dump_file, pb, &pb->geqs[e1]);
2334 fprintf (dump_file, "\n");
2337 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
2338 if (e1 != e2 && pb->geqs[e2].color == omega_black)
2340 for (p = pb->num_vars; p > 1; p--)
2342 for (q = p - 1; q > 0; q--)
2344 alpha =
2345 (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] -
2346 pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]);
2347 if (alpha != 0)
2348 goto foundPQ;
2351 continue;
2353 foundPQ:
2355 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2356 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2357 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2358 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2359 alpha3 = alpha;
2361 if (alpha1 * alpha2 <= 0)
2362 continue;
2364 if (alpha1 < 0)
2366 alpha1 = -alpha1;
2367 alpha2 = -alpha2;
2368 alpha3 = -alpha3;
2371 if (alpha3 > 0)
2373 /* Try to prove e3 is redundant: verify
2374 alpha1*v1 + alpha2*v2 = alpha3*v3. */
2375 for (k = pb->num_vars; k >= 1; k--)
2376 if (alpha3 * pb->geqs[e3].coef[k]
2377 != (alpha1 * pb->geqs[e1].coef[k]
2378 + alpha2 * pb->geqs[e2].coef[k]))
2379 goto nextE2;
2381 c = alpha1 * pb->geqs[e1].coef[0]
2382 + alpha2 * pb->geqs[e2].coef[0];
2384 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2385 pb->geqs[e3].coef[0] = int_div (c, alpha3);
2387 nextE2:;
2390 if (pb->geqs[e3].coef[0] < 9997)
2392 result++;
2393 pb->num_geqs++;
2395 if (dump_file && (dump_flags & TDF_DETAILS))
2397 fprintf (dump_file,
2398 "Smoothing weird equations; adding:\n");
2399 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2400 fprintf (dump_file, "\nto:\n");
2401 omega_print_problem (dump_file, pb);
2402 fprintf (dump_file, "\n\n");
2407 return result;
2410 /* Replace tuples of inequalities, that define upper and lower half
2411 spaces, with an equation. */
2413 static void
2414 coalesce (omega_pb pb)
2416 int e, e2;
2417 int colors = 0;
2418 bool *is_dead;
2419 int found_something = 0;
2421 for (e = 0; e < pb->num_geqs; e++)
2422 if (pb->geqs[e].color == omega_red)
2423 colors++;
2425 if (colors < 2)
2426 return;
2428 is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2430 for (e = 0; e < pb->num_geqs; e++)
2431 is_dead[e] = false;
2433 for (e = 0; e < pb->num_geqs; e++)
2434 if (pb->geqs[e].color == omega_red
2435 && !pb->geqs[e].touched)
2436 for (e2 = e + 1; e2 < pb->num_geqs; e2++)
2437 if (!pb->geqs[e2].touched
2438 && pb->geqs[e].key == -pb->geqs[e2].key
2439 && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0]
2440 && pb->geqs[e2].color == omega_red)
2442 omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e],
2443 pb->num_vars);
2444 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2445 found_something++;
2446 is_dead[e] = true;
2447 is_dead[e2] = true;
2450 for (e = pb->num_geqs - 1; e >= 0; e--)
2451 if (is_dead[e])
2452 omega_delete_geq (pb, e, pb->num_vars);
2454 if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
2456 fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
2457 found_something);
2458 omega_print_problem (dump_file, pb);
2461 free (is_dead);
2464 /* Eliminate red inequalities from PB. When ELIMINATE_ALL is
2465 true, continue to eliminate all the red inequalities. */
2467 void
2468 omega_eliminate_red (omega_pb pb, bool eliminate_all)
2470 int e, e2, e3, i, j, k, a, alpha1, alpha2;
2471 int c = 0;
2472 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2473 int dead_count = 0;
2474 int red_found;
2475 omega_pb tmp_problem;
2477 if (dump_file && (dump_flags & TDF_DETAILS))
2479 fprintf (dump_file, "in eliminate RED:\n");
2480 omega_print_problem (dump_file, pb);
2483 if (pb->num_eqs > 0)
2484 omega_simplify_problem (pb);
2486 for (e = pb->num_geqs - 1; e >= 0; e--)
2487 is_dead[e] = false;
2489 for (e = pb->num_geqs - 1; e >= 0; e--)
2490 if (pb->geqs[e].color == omega_black && !is_dead[e])
2491 for (e2 = e - 1; e2 >= 0; e2--)
2492 if (pb->geqs[e2].color == omega_black
2493 && !is_dead[e2])
2495 a = 0;
2497 for (i = pb->num_vars; i > 1; i--)
2498 for (j = i - 1; j > 0; j--)
2499 if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j]
2500 - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0)
2501 goto found_pair;
2503 continue;
2505 found_pair:
2506 if (dump_file && (dump_flags & TDF_DETAILS))
2508 fprintf (dump_file,
2509 "found two equations to combine, i = %s, ",
2510 omega_variable_to_str (pb, i));
2511 fprintf (dump_file, "j = %s, alpha = %d\n",
2512 omega_variable_to_str (pb, j), a);
2513 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2514 fprintf (dump_file, "\n");
2515 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2516 fprintf (dump_file, "\n");
2519 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2520 if (pb->geqs[e3].color == omega_red)
2522 alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i]
2523 - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]);
2524 alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i]
2525 - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]);
2527 if ((a > 0 && alpha1 > 0 && alpha2 > 0)
2528 || (a < 0 && alpha1 < 0 && alpha2 < 0))
2530 if (dump_file && (dump_flags & TDF_DETAILS))
2532 fprintf (dump_file,
2533 "alpha1 = %d, alpha2 = %d;"
2534 "comparing against: ",
2535 alpha1, alpha2);
2536 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2537 fprintf (dump_file, "\n");
2540 for (k = pb->num_vars; k >= 0; k--)
2542 c = (alpha1 * pb->geqs[e].coef[k]
2543 + alpha2 * pb->geqs[e2].coef[k]);
2545 if (c != a * pb->geqs[e3].coef[k])
2546 break;
2548 if (dump_file && (dump_flags & TDF_DETAILS) && k > 0)
2549 fprintf (dump_file, " %s: %d, %d\n",
2550 omega_variable_to_str (pb, k), c,
2551 a * pb->geqs[e3].coef[k]);
2554 if (k < 0
2555 || (k == 0 &&
2556 ((a > 0 && c < a * pb->geqs[e3].coef[k])
2557 || (a < 0 && c > a * pb->geqs[e3].coef[k]))))
2559 if (dump_file && (dump_flags & TDF_DETAILS))
2561 dead_count++;
2562 fprintf (dump_file,
2563 "red equation#%d is dead "
2564 "(%d dead so far, %d remain)\n",
2565 e3, dead_count,
2566 pb->num_geqs - dead_count);
2567 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2568 fprintf (dump_file, "\n");
2569 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2570 fprintf (dump_file, "\n");
2571 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2572 fprintf (dump_file, "\n");
2574 is_dead[e3] = true;
2580 for (e = pb->num_geqs - 1; e >= 0; e--)
2581 if (is_dead[e])
2582 omega_delete_geq (pb, e, pb->num_vars);
2584 free (is_dead);
2586 if (dump_file && (dump_flags & TDF_DETAILS))
2588 fprintf (dump_file, "in eliminate RED, easy tests done:\n");
2589 omega_print_problem (dump_file, pb);
2592 for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
2593 if (pb->geqs[e].color == omega_red)
2595 red_found = 1;
2596 break;
2599 if (!red_found)
2601 if (dump_file && (dump_flags & TDF_DETAILS))
2602 fprintf (dump_file, "fast checks worked\n");
2604 if (!omega_reduce_with_subs)
2605 gcc_assert (please_no_equalities_in_simplified_problems
2606 || pb->num_subs == 0);
2608 return;
2611 if (!omega_verify_simplification
2612 && verify_omega_pb (pb) == omega_false)
2613 return;
2615 conservative++;
2616 tmp_problem = XNEW (struct omega_pb_d);
2618 for (e = pb->num_geqs - 1; e >= 0; e--)
2619 if (pb->geqs[e].color == omega_red)
2621 if (dump_file && (dump_flags & TDF_DETAILS))
2623 fprintf (dump_file,
2624 "checking equation %d to see if it is redundant: ", e);
2625 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2626 fprintf (dump_file, "\n");
2629 omega_copy_problem (tmp_problem, pb);
2630 omega_negate_geq (tmp_problem, e);
2631 tmp_problem->safe_vars = 0;
2632 tmp_problem->variables_freed = false;
2633 tmp_problem->num_subs = 0;
2635 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2637 if (dump_file && (dump_flags & TDF_DETAILS))
2638 fprintf (dump_file, "it is redundant\n");
2639 omega_delete_geq (pb, e, pb->num_vars);
2641 else
2643 if (dump_file && (dump_flags & TDF_DETAILS))
2644 fprintf (dump_file, "it is not redundant\n");
2646 if (!eliminate_all)
2648 if (dump_file && (dump_flags & TDF_DETAILS))
2649 fprintf (dump_file, "no need to check other red equations\n");
2650 break;
2655 conservative--;
2656 free (tmp_problem);
2657 /* omega_simplify_problem (pb); */
2659 if (!omega_reduce_with_subs)
2660 gcc_assert (please_no_equalities_in_simplified_problems
2661 || pb->num_subs == 0);
2664 /* Transform some wildcard variables to non-safe variables. */
2666 static void
2667 chain_unprotect (omega_pb pb)
2669 int i, e;
2670 bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
2672 for (i = 1; omega_safe_var_p (pb, i); i++)
2674 unprotect[i] = omega_wildcard_p (pb, i);
2676 for (e = pb->num_subs - 1; e >= 0; e--)
2677 if (pb->subs[e].coef[i])
2678 unprotect[i] = false;
2681 if (dump_file && (dump_flags & TDF_DETAILS))
2683 fprintf (dump_file, "Doing chain reaction unprotection\n");
2684 omega_print_problem (dump_file, pb);
2686 for (i = 1; omega_safe_var_p (pb, i); i++)
2687 if (unprotect[i])
2688 fprintf (dump_file, "unprotecting %s\n",
2689 omega_variable_to_str (pb, i));
2692 for (i = 1; omega_safe_var_p (pb, i); i++)
2693 if (unprotect[i])
2694 omega_unprotect_1 (pb, &i, unprotect);
2696 if (dump_file && (dump_flags & TDF_DETAILS))
2698 fprintf (dump_file, "After chain reactions\n");
2699 omega_print_problem (dump_file, pb);
2702 free (unprotect);
2705 /* Reduce problem PB. */
2707 static void
2708 omega_problem_reduced (omega_pb pb)
2710 if (omega_verify_simplification
2711 && !in_approximate_mode
2712 && verify_omega_pb (pb) == omega_false)
2713 return;
2715 if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
2716 && !omega_eliminate_redundant (pb, true))
2717 return;
2719 omega_found_reduction = omega_true;
2721 if (!please_no_equalities_in_simplified_problems)
2722 coalesce (pb);
2724 if (omega_reduce_with_subs
2725 || please_no_equalities_in_simplified_problems)
2726 chain_unprotect (pb);
2727 else
2728 resurrect_subs (pb);
2730 if (!return_single_result)
2732 int i;
2734 for (i = 1; omega_safe_var_p (pb, i); i++)
2735 pb->forwarding_address[pb->var[i]] = i;
2737 for (i = 0; i < pb->num_subs; i++)
2738 pb->forwarding_address[pb->subs[i].key] = -i - 1;
2740 (*omega_when_reduced) (pb);
2743 if (dump_file && (dump_flags & TDF_DETAILS))
2745 fprintf (dump_file, "-------------------------------------------\n");
2746 fprintf (dump_file, "problem reduced:\n");
2747 omega_print_problem (dump_file, pb);
2748 fprintf (dump_file, "-------------------------------------------\n");
2752 /* Eliminates all the free variables for problem PB, that is all the
2753 variables from FV to PB->NUM_VARS. */
2755 static void
2756 omega_free_eliminations (omega_pb pb, int fv)
2758 bool try_again = true;
2759 int i, e, e2;
2760 int n_vars = pb->num_vars;
2762 while (try_again)
2764 try_again = false;
2766 for (i = n_vars; i > fv; i--)
2768 for (e = pb->num_geqs - 1; e >= 0; e--)
2769 if (pb->geqs[e].coef[i])
2770 break;
2772 if (e < 0)
2773 e2 = e;
2774 else if (pb->geqs[e].coef[i] > 0)
2776 for (e2 = e - 1; e2 >= 0; e2--)
2777 if (pb->geqs[e2].coef[i] < 0)
2778 break;
2780 else
2782 for (e2 = e - 1; e2 >= 0; e2--)
2783 if (pb->geqs[e2].coef[i] > 0)
2784 break;
2787 if (e2 < 0)
2789 int e3;
2790 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2791 if (pb->subs[e3].coef[i])
2792 break;
2794 if (e3 >= 0)
2795 continue;
2797 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2798 if (pb->eqs[e3].coef[i])
2799 break;
2801 if (e3 >= 0)
2802 continue;
2804 if (dump_file && (dump_flags & TDF_DETAILS))
2805 fprintf (dump_file, "a free elimination of %s\n",
2806 omega_variable_to_str (pb, i));
2808 if (e >= 0)
2810 omega_delete_geq (pb, e, n_vars);
2812 for (e--; e >= 0; e--)
2813 if (pb->geqs[e].coef[i])
2814 omega_delete_geq (pb, e, n_vars);
2816 try_again = (i < n_vars);
2819 omega_delete_variable (pb, i);
2820 n_vars = pb->num_vars;
2825 if (dump_file && (dump_flags & TDF_DETAILS))
2827 fprintf (dump_file, "\nafter free eliminations:\n");
2828 omega_print_problem (dump_file, pb);
2829 fprintf (dump_file, "\n");
2833 /* Do free red eliminations. */
2835 static void
2836 free_red_eliminations (omega_pb pb)
2838 bool try_again = true;
2839 int i, e, e2;
2840 int n_vars = pb->num_vars;
2841 bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2842 bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2843 bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS);
2845 for (i = n_vars; i > 0; i--)
2847 is_red_var[i] = false;
2848 is_dead_var[i] = false;
2851 for (e = pb->num_geqs - 1; e >= 0; e--)
2853 is_dead_geq[e] = false;
2855 if (pb->geqs[e].color == omega_red)
2856 for (i = n_vars; i > 0; i--)
2857 if (pb->geqs[e].coef[i] != 0)
2858 is_red_var[i] = true;
2861 while (try_again)
2863 try_again = false;
2864 for (i = n_vars; i > 0; i--)
2865 if (!is_red_var[i] && !is_dead_var[i])
2867 for (e = pb->num_geqs - 1; e >= 0; e--)
2868 if (!is_dead_geq[e] && pb->geqs[e].coef[i])
2869 break;
2871 if (e < 0)
2872 e2 = e;
2873 else if (pb->geqs[e].coef[i] > 0)
2875 for (e2 = e - 1; e2 >= 0; e2--)
2876 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
2877 break;
2879 else
2881 for (e2 = e - 1; e2 >= 0; e2--)
2882 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
2883 break;
2886 if (e2 < 0)
2888 int e3;
2889 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2890 if (pb->subs[e3].coef[i])
2891 break;
2893 if (e3 >= 0)
2894 continue;
2896 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2897 if (pb->eqs[e3].coef[i])
2898 break;
2900 if (e3 >= 0)
2901 continue;
2903 if (dump_file && (dump_flags & TDF_DETAILS))
2904 fprintf (dump_file, "a free red elimination of %s\n",
2905 omega_variable_to_str (pb, i));
2907 for (; e >= 0; e--)
2908 if (pb->geqs[e].coef[i])
2909 is_dead_geq[e] = true;
2911 try_again = true;
2912 is_dead_var[i] = true;
2917 for (e = pb->num_geqs - 1; e >= 0; e--)
2918 if (is_dead_geq[e])
2919 omega_delete_geq (pb, e, n_vars);
2921 for (i = n_vars; i > 0; i--)
2922 if (is_dead_var[i])
2923 omega_delete_variable (pb, i);
2925 if (dump_file && (dump_flags & TDF_DETAILS))
2927 fprintf (dump_file, "\nafter free red eliminations:\n");
2928 omega_print_problem (dump_file, pb);
2929 fprintf (dump_file, "\n");
2932 free (is_red_var);
2933 free (is_dead_var);
2934 free (is_dead_geq);
2937 /* For equation EQ of the form "0 = EQN", insert in PB two
2938 inequalities "0 <= EQN" and "0 <= -EQN". */
2940 void
2941 omega_convert_eq_to_geqs (omega_pb pb, int eq)
2943 int i;
2945 if (dump_file && (dump_flags & TDF_DETAILS))
2946 fprintf (dump_file, "Converting Eq to Geqs\n");
2948 /* Insert "0 <= EQN". */
2949 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2950 pb->geqs[pb->num_geqs].touched = 1;
2951 pb->num_geqs++;
2953 /* Insert "0 <= -EQN". */
2954 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2955 pb->geqs[pb->num_geqs].touched = 1;
2957 for (i = 0; i <= pb->num_vars; i++)
2958 pb->geqs[pb->num_geqs].coef[i] *= -1;
2960 pb->num_geqs++;
2962 if (dump_file && (dump_flags & TDF_DETAILS))
2963 omega_print_problem (dump_file, pb);
2966 /* Eliminates variable I from PB. */
2968 static void
2969 omega_do_elimination (omega_pb pb, int e, int i)
2971 eqn sub = omega_alloc_eqns (0, 1);
2972 int c;
2973 int n_vars = pb->num_vars;
2975 if (dump_file && (dump_flags & TDF_DETAILS))
2976 fprintf (dump_file, "eliminating variable %s\n",
2977 omega_variable_to_str (pb, i));
2979 omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars);
2980 c = sub->coef[i];
2981 sub->coef[i] = 0;
2982 if (c == 1 || c == -1)
2984 if (pb->eqs[e].color == omega_red)
2986 bool fB;
2987 omega_substitute_red (pb, sub, i, c, &fB);
2988 if (fB)
2989 omega_convert_eq_to_geqs (pb, e);
2990 else
2991 omega_delete_variable (pb, i);
2993 else
2995 omega_substitute (pb, sub, i, c);
2996 omega_delete_variable (pb, i);
2999 else
3001 int a = abs (c);
3002 int e2 = e;
3004 if (dump_file && (dump_flags & TDF_DETAILS))
3005 fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
3007 for (e = pb->num_eqs - 1; e >= 0; e--)
3008 if (pb->eqs[e].coef[i])
3010 eqn eqn = &(pb->eqs[e]);
3011 int j, k;
3012 for (j = n_vars; j >= 0; j--)
3013 eqn->coef[j] *= a;
3014 k = eqn->coef[i];
3015 eqn->coef[i] = 0;
3016 if (sub->color == omega_red)
3017 eqn->color = omega_red;
3018 for (j = n_vars; j >= 0; j--)
3019 eqn->coef[j] -= sub->coef[j] * k / c;
3022 for (e = pb->num_geqs - 1; e >= 0; e--)
3023 if (pb->geqs[e].coef[i])
3025 eqn eqn = &(pb->geqs[e]);
3026 int j, k;
3028 if (sub->color == omega_red)
3029 eqn->color = omega_red;
3031 for (j = n_vars; j >= 0; j--)
3032 eqn->coef[j] *= a;
3034 eqn->touched = 1;
3035 k = eqn->coef[i];
3036 eqn->coef[i] = 0;
3038 for (j = n_vars; j >= 0; j--)
3039 eqn->coef[j] -= sub->coef[j] * k / c;
3043 for (e = pb->num_subs - 1; e >= 0; e--)
3044 if (pb->subs[e].coef[i])
3046 eqn eqn = &(pb->subs[e]);
3047 int j, k;
3048 gcc_assert (0);
3049 gcc_assert (sub->color == omega_black);
3050 for (j = n_vars; j >= 0; j--)
3051 eqn->coef[j] *= a;
3052 k = eqn->coef[i];
3053 eqn->coef[i] = 0;
3054 for (j = n_vars; j >= 0; j--)
3055 eqn->coef[j] -= sub->coef[j] * k / c;
3058 if (in_approximate_mode)
3059 omega_delete_variable (pb, i);
3060 else
3061 omega_convert_eq_to_geqs (pb, e2);
3064 omega_free_eqns (sub, 1);
3067 /* Helper function for printing "sorry, no solution". */
3069 static inline enum omega_result
3070 omega_problem_has_no_solution (void)
3072 if (dump_file && (dump_flags & TDF_DETAILS))
3073 fprintf (dump_file, "\nequations have no solution \n");
3075 return omega_false;
3078 /* Helper function: solve equations in PB one at a time, following the
3079 DESIRED_RES result. */
3081 static enum omega_result
3082 omega_solve_eq (omega_pb pb, enum omega_result desired_res)
3084 int i, j, e;
3085 int g, g2;
3086 g = 0;
3089 if (dump_file && (dump_flags & TDF_DETAILS) && pb->num_eqs > 0)
3091 fprintf (dump_file, "\nomega_solve_eq (%d, %d)\n",
3092 desired_res, may_be_red);
3093 omega_print_problem (dump_file, pb);
3094 fprintf (dump_file, "\n");
3097 if (may_be_red)
3099 i = 0;
3100 j = pb->num_eqs - 1;
3102 while (1)
3104 eqn eq;
3106 while (i <= j && pb->eqs[i].color == omega_red)
3107 i++;
3109 while (i <= j && pb->eqs[j].color == omega_black)
3110 j--;
3112 if (i >= j)
3113 break;
3115 eq = omega_alloc_eqns (0, 1);
3116 omega_copy_eqn (eq, &pb->eqs[i], pb->num_vars);
3117 omega_copy_eqn (&pb->eqs[i], &pb->eqs[j], pb->num_vars);
3118 omega_copy_eqn (&pb->eqs[j], eq, pb->num_vars);
3119 omega_free_eqns (eq, 1);
3120 i++;
3121 j--;
3125 /* Eliminate all EQ equations */
3126 for (e = pb->num_eqs - 1; e >= 0; e--)
3128 eqn eqn = &(pb->eqs[e]);
3129 int sv;
3131 if (dump_file && (dump_flags & TDF_DETAILS))
3132 fprintf (dump_file, "----\n");
3134 for (i = pb->num_vars; i > 0; i--)
3135 if (eqn->coef[i])
3136 break;
3138 g = eqn->coef[i];
3140 for (j = i - 1; j > 0; j--)
3141 if (eqn->coef[j])
3142 break;
3144 /* i is the position of last nonzero coefficient,
3145 g is the coefficient of i,
3146 j is the position of next nonzero coefficient. */
3148 if (j == 0)
3150 if (eqn->coef[0] % g != 0)
3151 return omega_problem_has_no_solution ();
3153 eqn->coef[0] = eqn->coef[0] / g;
3154 eqn->coef[i] = 1;
3155 pb->num_eqs--;
3156 omega_do_elimination (pb, e, i);
3157 continue;
3160 else if (j == -1)
3162 if (eqn->coef[0] != 0)
3163 return omega_problem_has_no_solution ();
3165 pb->num_eqs--;
3166 continue;
3169 if (g < 0)
3170 g = -g;
3172 if (g == 1)
3174 pb->num_eqs--;
3175 omega_do_elimination (pb, e, i);
3178 else
3180 int k = j;
3181 bool promotion_possible =
3182 (omega_safe_var_p (pb, j)
3183 && pb->safe_vars + 1 == i
3184 && !omega_eqn_is_red (eqn, desired_res)
3185 && !in_approximate_mode);
3187 if (dump_file && (dump_flags & TDF_DETAILS) && promotion_possible)
3188 fprintf (dump_file, " Promotion possible\n");
3190 normalizeEQ:
3191 if (!omega_safe_var_p (pb, j))
3193 for (; g != 1 && !omega_safe_var_p (pb, j); j--)
3194 g = gcd (abs (eqn->coef[j]), g);
3195 g2 = g;
3197 else if (!omega_safe_var_p (pb, i))
3198 g2 = g;
3199 else
3200 g2 = 0;
3202 for (; g != 1 && j > 0; j--)
3203 g = gcd (abs (eqn->coef[j]), g);
3205 if (g > 1)
3207 if (eqn->coef[0] % g != 0)
3208 return omega_problem_has_no_solution ();
3210 for (j = 0; j <= pb->num_vars; j++)
3211 eqn->coef[j] /= g;
3213 g2 = g2 / g;
3216 if (g2 > 1)
3218 int e2;
3220 for (e2 = e - 1; e2 >= 0; e2--)
3221 if (pb->eqs[e2].coef[i])
3222 break;
3224 if (e2 == -1)
3225 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
3226 if (pb->geqs[e2].coef[i])
3227 break;
3229 if (e2 == -1)
3230 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
3231 if (pb->subs[e2].coef[i])
3232 break;
3234 if (e2 == -1)
3236 bool change = false;
3238 if (dump_file && (dump_flags & TDF_DETAILS))
3240 fprintf (dump_file, "Ha! We own it! \n");
3241 omega_print_eq (dump_file, pb, eqn);
3242 fprintf (dump_file, " \n");
3245 g = eqn->coef[i];
3246 g = abs (g);
3248 for (j = i - 1; j >= 0; j--)
3250 int t = int_mod (eqn->coef[j], g);
3252 if (2 * t >= g)
3253 t -= g;
3255 if (t != eqn->coef[j])
3257 eqn->coef[j] = t;
3258 change = true;
3262 if (!change)
3264 if (dump_file && (dump_flags & TDF_DETAILS))
3265 fprintf (dump_file, "So what?\n");
3268 else
3270 omega_name_wild_card (pb, i);
3272 if (dump_file && (dump_flags & TDF_DETAILS))
3274 omega_print_eq (dump_file, pb, eqn);
3275 fprintf (dump_file, " \n");
3278 e++;
3279 continue;
3284 if (promotion_possible)
3286 if (dump_file && (dump_flags & TDF_DETAILS))
3288 fprintf (dump_file, "promoting %s to safety\n",
3289 omega_variable_to_str (pb, i));
3290 omega_print_vars (dump_file, pb);
3293 pb->safe_vars++;
3295 if (!omega_wildcard_p (pb, i))
3296 omega_name_wild_card (pb, i);
3298 promotion_possible = false;
3299 j = k;
3300 goto normalizeEQ;
3303 if (g2 > 1 && !in_approximate_mode)
3305 if (pb->eqs[e].color == omega_red)
3307 if (dump_file && (dump_flags & TDF_DETAILS))
3308 fprintf (dump_file, "handling red equality\n");
3310 pb->num_eqs--;
3311 omega_do_elimination (pb, e, i);
3312 continue;
3315 if (dump_file && (dump_flags & TDF_DETAILS))
3317 fprintf (dump_file,
3318 "adding equation to handle safe variable \n");
3319 omega_print_eq (dump_file, pb, eqn);
3320 fprintf (dump_file, "\n----\n");
3321 omega_print_problem (dump_file, pb);
3322 fprintf (dump_file, "\n----\n");
3323 fprintf (dump_file, "\n----\n");
3326 i = omega_add_new_wild_card (pb);
3327 pb->num_eqs++;
3328 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
3329 omega_init_eqn_zero (&pb->eqs[e + 1], pb->num_vars);
3330 omega_copy_eqn (&pb->eqs[e + 1], eqn, pb->safe_vars);
3332 for (j = pb->num_vars; j >= 0; j--)
3334 pb->eqs[e + 1].coef[j] = int_mod (pb->eqs[e + 1].coef[j], g2);
3336 if (2 * pb->eqs[e + 1].coef[j] >= g2)
3337 pb->eqs[e + 1].coef[j] -= g2;
3340 pb->eqs[e + 1].coef[i] = g2;
3341 e += 2;
3343 if (dump_file && (dump_flags & TDF_DETAILS))
3344 omega_print_problem (dump_file, pb);
3346 continue;
3349 sv = pb->safe_vars;
3350 if (g2 == 0)
3351 sv = 0;
3353 /* Find variable to eliminate. */
3354 if (g2 > 1)
3356 gcc_assert (in_approximate_mode);
3358 if (dump_file && (dump_flags & TDF_DETAILS))
3360 fprintf (dump_file, "non-exact elimination: ");
3361 omega_print_eq (dump_file, pb, eqn);
3362 fprintf (dump_file, "\n");
3363 omega_print_problem (dump_file, pb);
3366 for (i = pb->num_vars; i > sv; i--)
3367 if (pb->eqs[e].coef[i] != 0)
3368 break;
3370 else
3371 for (i = pb->num_vars; i > sv; i--)
3372 if (pb->eqs[e].coef[i] == 1 || pb->eqs[e].coef[i] == -1)
3373 break;
3375 if (i > sv)
3377 pb->num_eqs--;
3378 omega_do_elimination (pb, e, i);
3380 if (dump_file && (dump_flags & TDF_DETAILS) && g2 > 1)
3382 fprintf (dump_file, "result of non-exact elimination:\n");
3383 omega_print_problem (dump_file, pb);
3386 else
3388 int factor = (INT_MAX);
3389 j = 0;
3391 if (dump_file && (dump_flags & TDF_DETAILS))
3392 fprintf (dump_file, "doing moding\n");
3394 for (i = pb->num_vars; i != sv; i--)
3395 if ((pb->eqs[e].coef[i] & 1) != 0)
3397 j = i;
3398 i--;
3400 for (; i != sv; i--)
3401 if ((pb->eqs[e].coef[i] & 1) != 0)
3402 break;
3404 break;
3407 if (j != 0 && i == sv)
3409 omega_do_mod (pb, 2, e, j);
3410 e++;
3411 continue;
3414 j = 0;
3415 for (i = pb->num_vars; i != sv; i--)
3416 if (pb->eqs[e].coef[i] != 0
3417 && factor > abs (pb->eqs[e].coef[i]) + 1)
3419 factor = abs (pb->eqs[e].coef[i]) + 1;
3420 j = i;
3423 if (j == sv)
3425 if (dump_file && (dump_flags & TDF_DETAILS))
3426 fprintf (dump_file, "should not have happened\n");
3427 gcc_assert (0);
3430 omega_do_mod (pb, factor, e, j);
3431 /* Go back and try this equation again. */
3432 e++;
3437 pb->num_eqs = 0;
3438 return omega_unknown;
3441 /* Transform an inequation E to an equality, then solve DIFF problems
3442 based on PB, and only differing by the constant part that is
3443 diminished by one, trying to figure out which of the constants
3444 satisfies PB. */
3446 static enum omega_result
3447 parallel_splinter (omega_pb pb, int e, int diff,
3448 enum omega_result desired_res)
3450 omega_pb tmp_problem;
3451 int i;
3453 if (dump_file && (dump_flags & TDF_DETAILS))
3455 fprintf (dump_file, "Using parallel splintering\n");
3456 omega_print_problem (dump_file, pb);
3459 tmp_problem = XNEW (struct omega_pb_d);
3460 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e], pb->num_vars);
3461 pb->num_eqs = 1;
3463 for (i = 0; i <= diff; i++)
3465 omega_copy_problem (tmp_problem, pb);
3467 if (dump_file && (dump_flags & TDF_DETAILS))
3469 fprintf (dump_file, "Splinter # %i\n", i);
3470 omega_print_problem (dump_file, pb);
3473 if (omega_solve_problem (tmp_problem, desired_res) == omega_true)
3475 free (tmp_problem);
3476 return omega_true;
3479 pb->eqs[0].coef[0]--;
3482 free (tmp_problem);
3483 return omega_false;
3486 /* Helper function: solve equations one at a time. */
3488 static enum omega_result
3489 omega_solve_geq (omega_pb pb, enum omega_result desired_res)
3491 int i, e;
3492 int n_vars, fv;
3493 enum omega_result result;
3494 bool coupled_subscripts = false;
3495 bool smoothed = false;
3496 bool eliminate_again;
3497 bool tried_eliminating_redundant = false;
3499 if (desired_res != omega_simplify)
3501 pb->num_subs = 0;
3502 pb->safe_vars = 0;
3505 solve_geq_start:
3506 do {
3507 gcc_assert (desired_res == omega_simplify || pb->num_subs == 0);
3509 /* Verify that there are not too many inequalities. */
3510 gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
3512 if (dump_file && (dump_flags & TDF_DETAILS))
3514 fprintf (dump_file, "\nomega_solve_geq (%d,%d):\n",
3515 desired_res, please_no_equalities_in_simplified_problems);
3516 omega_print_problem (dump_file, pb);
3517 fprintf (dump_file, "\n");
3520 n_vars = pb->num_vars;
3522 if (n_vars == 1)
3524 enum omega_eqn_color u_color = omega_black;
3525 enum omega_eqn_color l_color = omega_black;
3526 int upper_bound = pos_infinity;
3527 int lower_bound = neg_infinity;
3529 for (e = pb->num_geqs - 1; e >= 0; e--)
3531 int a = pb->geqs[e].coef[1];
3532 int c = pb->geqs[e].coef[0];
3534 /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax. */
3535 if (a == 0)
3537 if (c < 0)
3538 return omega_problem_has_no_solution ();
3540 else if (a > 0)
3542 if (a != 1)
3543 c = int_div (c, a);
3545 if (lower_bound < -c
3546 || (lower_bound == -c
3547 && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3549 lower_bound = -c;
3550 l_color = pb->geqs[e].color;
3553 else
3555 if (a != -1)
3556 c = int_div (c, -a);
3558 if (upper_bound > c
3559 || (upper_bound == c
3560 && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3562 upper_bound = c;
3563 u_color = pb->geqs[e].color;
3568 if (dump_file && (dump_flags & TDF_DETAILS))
3570 fprintf (dump_file, "upper bound = %d\n", upper_bound);
3571 fprintf (dump_file, "lower bound = %d\n", lower_bound);
3574 if (lower_bound > upper_bound)
3575 return omega_problem_has_no_solution ();
3577 if (desired_res == omega_simplify)
3579 pb->num_geqs = 0;
3580 if (pb->safe_vars == 1)
3583 if (lower_bound == upper_bound
3584 && u_color == omega_black
3585 && l_color == omega_black)
3587 pb->eqs[0].coef[0] = -lower_bound;
3588 pb->eqs[0].coef[1] = 1;
3589 pb->eqs[0].color = omega_black;
3590 pb->num_eqs = 1;
3591 return omega_solve_problem (pb, desired_res);
3593 else
3595 if (lower_bound > neg_infinity)
3597 pb->geqs[0].coef[0] = -lower_bound;
3598 pb->geqs[0].coef[1] = 1;
3599 pb->geqs[0].key = 1;
3600 pb->geqs[0].color = l_color;
3601 pb->geqs[0].touched = 0;
3602 pb->num_geqs = 1;
3605 if (upper_bound < pos_infinity)
3607 pb->geqs[pb->num_geqs].coef[0] = upper_bound;
3608 pb->geqs[pb->num_geqs].coef[1] = -1;
3609 pb->geqs[pb->num_geqs].key = -1;
3610 pb->geqs[pb->num_geqs].color = u_color;
3611 pb->geqs[pb->num_geqs].touched = 0;
3612 pb->num_geqs++;
3616 else
3617 pb->num_vars = 0;
3619 omega_problem_reduced (pb);
3620 return omega_false;
3623 if (original_problem != no_problem
3624 && l_color == omega_black
3625 && u_color == omega_black
3626 && !conservative
3627 && lower_bound == upper_bound)
3629 pb->eqs[0].coef[0] = -lower_bound;
3630 pb->eqs[0].coef[1] = 1;
3631 pb->num_eqs = 1;
3632 adding_equality_constraint (pb, 0);
3635 return omega_true;
3638 if (!pb->variables_freed)
3640 pb->variables_freed = true;
3642 if (desired_res != omega_simplify)
3643 omega_free_eliminations (pb, 0);
3644 else
3645 omega_free_eliminations (pb, pb->safe_vars);
3647 n_vars = pb->num_vars;
3649 if (n_vars == 1)
3650 continue;
3653 switch (normalize_omega_problem (pb))
3655 case normalize_false:
3656 return omega_false;
3657 break;
3659 case normalize_coupled:
3660 coupled_subscripts = true;
3661 break;
3663 case normalize_uncoupled:
3664 coupled_subscripts = false;
3665 break;
3667 default:
3668 gcc_unreachable ();
3671 n_vars = pb->num_vars;
3673 if (dump_file && (dump_flags & TDF_DETAILS))
3675 fprintf (dump_file, "\nafter normalization:\n");
3676 omega_print_problem (dump_file, pb);
3677 fprintf (dump_file, "\n");
3678 fprintf (dump_file, "eliminating variable using Fourier-Motzkin.\n");
3681 do {
3682 int parallel_difference = INT_MAX;
3683 int best_parallel_eqn = -1;
3684 int minC, maxC, minCj = 0;
3685 int lower_bound_count = 0;
3686 int e2, Le = 0, Ue;
3687 bool possible_easy_int_solution;
3688 int max_splinters = 1;
3689 bool exact = false;
3690 bool lucky_exact = false;
3691 int best = (INT_MAX);
3692 int j = 0, jLe = 0, jLowerBoundCount = 0;
3695 eliminate_again = false;
3697 if (pb->num_eqs > 0)
3698 return omega_solve_problem (pb, desired_res);
3700 if (!coupled_subscripts)
3702 if (pb->safe_vars == 0)
3703 pb->num_geqs = 0;
3704 else
3705 for (e = pb->num_geqs - 1; e >= 0; e--)
3706 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
3707 omega_delete_geq (pb, e, n_vars);
3709 pb->num_vars = pb->safe_vars;
3711 if (desired_res == omega_simplify)
3713 omega_problem_reduced (pb);
3714 return omega_false;
3717 return omega_true;
3720 if (desired_res != omega_simplify)
3721 fv = 0;
3722 else
3723 fv = pb->safe_vars;
3725 if (pb->num_geqs == 0)
3727 if (desired_res == omega_simplify)
3729 pb->num_vars = pb->safe_vars;
3730 omega_problem_reduced (pb);
3731 return omega_false;
3733 return omega_true;
3736 if (desired_res == omega_simplify && n_vars == pb->safe_vars)
3738 omega_problem_reduced (pb);
3739 return omega_false;
3742 if (pb->num_geqs > OMEGA_MAX_GEQS - 30
3743 || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10)
3745 if (dump_file && (dump_flags & TDF_DETAILS))
3746 fprintf (dump_file,
3747 "TOO MANY EQUATIONS; "
3748 "%d equations, %d variables, "
3749 "ELIMINATING REDUNDANT ONES\n",
3750 pb->num_geqs, n_vars);
3752 if (!omega_eliminate_redundant (pb, false))
3753 return omega_false;
3755 n_vars = pb->num_vars;
3757 if (pb->num_eqs > 0)
3758 return omega_solve_problem (pb, desired_res);
3760 if (dump_file && (dump_flags & TDF_DETAILS))
3761 fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3764 if (desired_res != omega_simplify)
3765 fv = 0;
3766 else
3767 fv = pb->safe_vars;
3769 for (i = n_vars; i != fv; i--)
3771 int score;
3772 int ub = -2;
3773 int lb = -2;
3774 bool lucky = false;
3775 int upper_bound_count = 0;
3777 lower_bound_count = 0;
3778 minC = maxC = 0;
3780 for (e = pb->num_geqs - 1; e >= 0; e--)
3781 if (pb->geqs[e].coef[i] < 0)
3783 minC = MIN (minC, pb->geqs[e].coef[i]);
3784 upper_bound_count++;
3785 if (pb->geqs[e].coef[i] < -1)
3787 if (ub == -2)
3788 ub = e;
3789 else
3790 ub = -1;
3793 else if (pb->geqs[e].coef[i] > 0)
3795 maxC = MAX (maxC, pb->geqs[e].coef[i]);
3796 lower_bound_count++;
3797 Le = e;
3798 if (pb->geqs[e].coef[i] > 1)
3800 if (lb == -2)
3801 lb = e;
3802 else
3803 lb = -1;
3807 if (lower_bound_count == 0
3808 || upper_bound_count == 0)
3810 lower_bound_count = 0;
3811 break;
3814 if (ub >= 0 && lb >= 0
3815 && pb->geqs[lb].key == -pb->geqs[ub].key)
3817 int Lc = pb->geqs[lb].coef[i];
3818 int Uc = -pb->geqs[ub].coef[i];
3819 int diff =
3820 Lc * pb->geqs[ub].coef[0] + Uc * pb->geqs[lb].coef[0];
3821 lucky = (diff >= (Uc - 1) * (Lc - 1));
3824 if (maxC == 1
3825 || minC == -1
3826 || lucky
3827 || in_approximate_mode)
3829 score = upper_bound_count * lower_bound_count;
3831 if (dump_file && (dump_flags & TDF_DETAILS))
3832 fprintf (dump_file,
3833 "For %s, exact, score = %d*%d, range = %d ... %d,"
3834 "\nlucky = %d, in_approximate_mode=%d \n",
3835 omega_variable_to_str (pb, i),
3836 upper_bound_count,
3837 lower_bound_count, minC, maxC, lucky,
3838 in_approximate_mode);
3840 if (!exact
3841 || score < best)
3844 best = score;
3845 j = i;
3846 minCj = minC;
3847 jLe = Le;
3848 jLowerBoundCount = lower_bound_count;
3849 exact = true;
3850 lucky_exact = lucky;
3851 if (score == 1)
3852 break;
3855 else if (!exact)
3857 if (dump_file && (dump_flags & TDF_DETAILS))
3858 fprintf (dump_file,
3859 "For %s, non-exact, score = %d*%d,"
3860 "range = %d ... %d \n",
3861 omega_variable_to_str (pb, i),
3862 upper_bound_count,
3863 lower_bound_count, minC, maxC);
3865 score = maxC - minC;
3867 if (best > score)
3869 best = score;
3870 j = i;
3871 minCj = minC;
3872 jLe = Le;
3873 jLowerBoundCount = lower_bound_count;
3878 if (lower_bound_count == 0)
3880 omega_free_eliminations (pb, pb->safe_vars);
3881 n_vars = pb->num_vars;
3882 eliminate_again = true;
3883 continue;
3886 i = j;
3887 minC = minCj;
3888 Le = jLe;
3889 lower_bound_count = jLowerBoundCount;
3891 for (e = pb->num_geqs - 1; e >= 0; e--)
3892 if (pb->geqs[e].coef[i] > 0)
3894 if (pb->geqs[e].coef[i] == -minC)
3895 max_splinters += -minC - 1;
3896 else
3897 max_splinters +=
3898 pos_mul_hwi ((pb->geqs[e].coef[i] - 1),
3899 (-minC - 1)) / (-minC) + 1;
3902 /* #ifdef Omega3 */
3903 /* Trying to produce exact elimination by finding redundant
3904 constraints. */
3905 if (!exact && !tried_eliminating_redundant)
3907 omega_eliminate_redundant (pb, false);
3908 tried_eliminating_redundant = true;
3909 eliminate_again = true;
3910 continue;
3912 tried_eliminating_redundant = false;
3913 /* #endif */
3915 if (return_single_result && desired_res == omega_simplify && !exact)
3917 omega_problem_reduced (pb);
3918 return omega_true;
3921 /* #ifndef Omega3 */
3922 /* Trying to produce exact elimination by finding redundant
3923 constraints. */
3924 if (!exact && !tried_eliminating_redundant)
3926 omega_eliminate_redundant (pb, false);
3927 tried_eliminating_redundant = true;
3928 continue;
3930 tried_eliminating_redundant = false;
3931 /* #endif */
3933 if (!exact)
3935 int e1, e2;
3937 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
3938 if (pb->geqs[e1].color == omega_black)
3939 for (e2 = e1 - 1; e2 >= 0; e2--)
3940 if (pb->geqs[e2].color == omega_black
3941 && pb->geqs[e1].key == -pb->geqs[e2].key
3942 && ((pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3943 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3944 / 2 < parallel_difference))
3946 parallel_difference =
3947 (pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3948 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3949 / 2;
3950 best_parallel_eqn = e1;
3953 if (dump_file && (dump_flags & TDF_DETAILS)
3954 && best_parallel_eqn >= 0)
3956 fprintf (dump_file,
3957 "Possible parallel projection, diff = %d, in ",
3958 parallel_difference);
3959 omega_print_geq (dump_file, pb, &(pb->geqs[best_parallel_eqn]));
3960 fprintf (dump_file, "\n");
3961 omega_print_problem (dump_file, pb);
3965 if (dump_file && (dump_flags & TDF_DETAILS))
3967 fprintf (dump_file, "going to eliminate %s, (%d,%d,%d)\n",
3968 omega_variable_to_str (pb, i), i, minC,
3969 lower_bound_count);
3970 omega_print_problem (dump_file, pb);
3972 if (lucky_exact)
3973 fprintf (dump_file, "(a lucky exact elimination)\n");
3975 else if (exact)
3976 fprintf (dump_file, "(an exact elimination)\n");
3978 fprintf (dump_file, "Max # of splinters = %d\n", max_splinters);
3981 gcc_assert (max_splinters >= 1);
3983 if (!exact && desired_res == omega_simplify && best_parallel_eqn >= 0
3984 && parallel_difference <= max_splinters)
3985 return parallel_splinter (pb, best_parallel_eqn, parallel_difference,
3986 desired_res);
3988 smoothed = false;
3990 if (i != n_vars)
3992 int t;
3993 int j = pb->num_vars;
3995 if (dump_file && (dump_flags & TDF_DETAILS))
3997 fprintf (dump_file, "Swapping %d and %d\n", i, j);
3998 omega_print_problem (dump_file, pb);
4001 swap (&pb->var[i], &pb->var[j]);
4003 for (e = pb->num_geqs - 1; e >= 0; e--)
4004 if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
4006 pb->geqs[e].touched = 1;
4007 t = pb->geqs[e].coef[i];
4008 pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
4009 pb->geqs[e].coef[j] = t;
4012 for (e = pb->num_subs - 1; e >= 0; e--)
4013 if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
4015 t = pb->subs[e].coef[i];
4016 pb->subs[e].coef[i] = pb->subs[e].coef[j];
4017 pb->subs[e].coef[j] = t;
4020 if (dump_file && (dump_flags & TDF_DETAILS))
4022 fprintf (dump_file, "Swapping complete \n");
4023 omega_print_problem (dump_file, pb);
4024 fprintf (dump_file, "\n");
4027 i = j;
4030 else if (dump_file && (dump_flags & TDF_DETAILS))
4032 fprintf (dump_file, "No swap needed\n");
4033 omega_print_problem (dump_file, pb);
4036 pb->num_vars--;
4037 n_vars = pb->num_vars;
4039 if (exact)
4041 if (n_vars == 1)
4043 int upper_bound = pos_infinity;
4044 int lower_bound = neg_infinity;
4045 enum omega_eqn_color ub_color = omega_black;
4046 enum omega_eqn_color lb_color = omega_black;
4047 int topeqn = pb->num_geqs - 1;
4048 int Lc = pb->geqs[Le].coef[i];
4050 for (Le = topeqn; Le >= 0; Le--)
4051 if ((Lc = pb->geqs[Le].coef[i]) == 0)
4053 if (pb->geqs[Le].coef[1] == 1)
4055 int constantTerm = -pb->geqs[Le].coef[0];
4057 if (constantTerm > lower_bound ||
4058 (constantTerm == lower_bound &&
4059 !omega_eqn_is_red (&pb->geqs[Le], desired_res)))
4061 lower_bound = constantTerm;
4062 lb_color = pb->geqs[Le].color;
4065 if (dump_file && (dump_flags & TDF_DETAILS))
4067 if (pb->geqs[Le].color == omega_black)
4068 fprintf (dump_file, " :::=> %s >= %d\n",
4069 omega_variable_to_str (pb, 1),
4070 constantTerm);
4071 else
4072 fprintf (dump_file,
4073 " :::=> [%s >= %d]\n",
4074 omega_variable_to_str (pb, 1),
4075 constantTerm);
4078 else
4080 int constantTerm = pb->geqs[Le].coef[0];
4081 if (constantTerm < upper_bound ||
4082 (constantTerm == upper_bound
4083 && !omega_eqn_is_red (&pb->geqs[Le],
4084 desired_res)))
4086 upper_bound = constantTerm;
4087 ub_color = pb->geqs[Le].color;
4090 if (dump_file && (dump_flags & TDF_DETAILS))
4092 if (pb->geqs[Le].color == omega_black)
4093 fprintf (dump_file, " :::=> %s <= %d\n",
4094 omega_variable_to_str (pb, 1),
4095 constantTerm);
4096 else
4097 fprintf (dump_file,
4098 " :::=> [%s <= %d]\n",
4099 omega_variable_to_str (pb, 1),
4100 constantTerm);
4104 else if (Lc > 0)
4105 for (Ue = topeqn; Ue >= 0; Ue--)
4106 if (pb->geqs[Ue].coef[i] < 0
4107 && pb->geqs[Le].key != -pb->geqs[Ue].key)
4109 int Uc = -pb->geqs[Ue].coef[i];
4110 int coefficient = pb->geqs[Ue].coef[1] * Lc
4111 + pb->geqs[Le].coef[1] * Uc;
4112 int constantTerm = pb->geqs[Ue].coef[0] * Lc
4113 + pb->geqs[Le].coef[0] * Uc;
4115 if (dump_file && (dump_flags & TDF_DETAILS))
4117 omega_print_geq_extra (dump_file, pb,
4118 &(pb->geqs[Ue]));
4119 fprintf (dump_file, "\n");
4120 omega_print_geq_extra (dump_file, pb,
4121 &(pb->geqs[Le]));
4122 fprintf (dump_file, "\n");
4125 if (coefficient > 0)
4127 constantTerm = -int_div (constantTerm, coefficient);
4129 if (constantTerm > lower_bound
4130 || (constantTerm == lower_bound
4131 && (desired_res != omega_simplify
4132 || (pb->geqs[Ue].color == omega_black
4133 && pb->geqs[Le].color == omega_black))))
4135 lower_bound = constantTerm;
4136 lb_color = (pb->geqs[Ue].color == omega_red
4137 || pb->geqs[Le].color == omega_red)
4138 ? omega_red : omega_black;
4141 if (dump_file && (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);
4156 else
4158 constantTerm = int_div (constantTerm, -coefficient);
4159 if (constantTerm < upper_bound
4160 || (constantTerm == upper_bound
4161 && pb->geqs[Ue].color == omega_black
4162 && pb->geqs[Le].color == omega_black))
4164 upper_bound = constantTerm;
4165 ub_color = (pb->geqs[Ue].color == omega_red
4166 || pb->geqs[Le].color == omega_red)
4167 ? omega_red : omega_black;
4170 if (dump_file
4171 && (dump_flags & TDF_DETAILS))
4173 if (pb->geqs[Ue].color == omega_red
4174 || pb->geqs[Le].color == omega_red)
4175 fprintf (dump_file,
4176 " ::=> [%s <= %d]\n",
4177 omega_variable_to_str (pb, 1),
4178 constantTerm);
4179 else
4180 fprintf (dump_file,
4181 " ::=> %s <= %d\n",
4182 omega_variable_to_str (pb, 1),
4183 constantTerm);
4188 pb->num_geqs = 0;
4190 if (dump_file && (dump_flags & TDF_DETAILS))
4191 fprintf (dump_file,
4192 " therefore, %c%d <= %c%s%c <= %d%c\n",
4193 lb_color == omega_red ? '[' : ' ', lower_bound,
4194 (lb_color == omega_red && ub_color == omega_black)
4195 ? ']' : ' ',
4196 omega_variable_to_str (pb, 1),
4197 (lb_color == omega_black && ub_color == omega_red)
4198 ? '[' : ' ',
4199 upper_bound, ub_color == omega_red ? ']' : ' ');
4201 if (lower_bound > upper_bound)
4202 return omega_false;
4204 if (pb->safe_vars == 1)
4206 if (upper_bound == lower_bound
4207 && !(ub_color == omega_red || lb_color == omega_red)
4208 && !please_no_equalities_in_simplified_problems)
4210 pb->num_eqs++;
4211 pb->eqs[0].coef[1] = -1;
4212 pb->eqs[0].coef[0] = upper_bound;
4214 if (ub_color == omega_red
4215 || lb_color == omega_red)
4216 pb->eqs[0].color = omega_red;
4218 if (desired_res == omega_simplify
4219 && pb->eqs[0].color == omega_black)
4220 return omega_solve_problem (pb, desired_res);
4223 if (upper_bound != pos_infinity)
4225 pb->geqs[0].coef[1] = -1;
4226 pb->geqs[0].coef[0] = upper_bound;
4227 pb->geqs[0].color = ub_color;
4228 pb->geqs[0].key = -1;
4229 pb->geqs[0].touched = 0;
4230 pb->num_geqs++;
4233 if (lower_bound != neg_infinity)
4235 pb->geqs[pb->num_geqs].coef[1] = 1;
4236 pb->geqs[pb->num_geqs].coef[0] = -lower_bound;
4237 pb->geqs[pb->num_geqs].color = lb_color;
4238 pb->geqs[pb->num_geqs].key = 1;
4239 pb->geqs[pb->num_geqs].touched = 0;
4240 pb->num_geqs++;
4244 if (desired_res == omega_simplify)
4246 omega_problem_reduced (pb);
4247 return omega_false;
4249 else
4251 if (!conservative
4252 && (desired_res != omega_simplify
4253 || (lb_color == omega_black
4254 && ub_color == omega_black))
4255 && original_problem != no_problem
4256 && lower_bound == upper_bound)
4258 for (i = original_problem->num_vars; i >= 0; i--)
4259 if (original_problem->var[i] == pb->var[1])
4260 break;
4262 if (i == 0)
4263 break;
4265 e = original_problem->num_eqs++;
4266 omega_init_eqn_zero (&original_problem->eqs[e],
4267 original_problem->num_vars);
4268 original_problem->eqs[e].coef[i] = -1;
4269 original_problem->eqs[e].coef[0] = upper_bound;
4271 if (dump_file && (dump_flags & TDF_DETAILS))
4273 fprintf (dump_file,
4274 "adding equality %d to outer problem\n", e);
4275 omega_print_problem (dump_file, original_problem);
4278 return omega_true;
4282 eliminate_again = true;
4284 if (lower_bound_count == 1)
4286 eqn lbeqn = omega_alloc_eqns (0, 1);
4287 int Lc = pb->geqs[Le].coef[i];
4289 if (dump_file && (dump_flags & TDF_DETAILS))
4290 fprintf (dump_file, "an inplace elimination\n");
4292 omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1));
4293 omega_delete_geq_extra (pb, Le, n_vars + 1);
4295 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4296 if (pb->geqs[Ue].coef[i] < 0)
4298 if (lbeqn->key == -pb->geqs[Ue].key)
4299 omega_delete_geq_extra (pb, Ue, n_vars + 1);
4300 else
4302 int k;
4303 int Uc = -pb->geqs[Ue].coef[i];
4304 pb->geqs[Ue].touched = 1;
4305 eliminate_again = false;
4307 if (lbeqn->color == omega_red)
4308 pb->geqs[Ue].color = omega_red;
4310 for (k = 0; k <= n_vars; k++)
4311 pb->geqs[Ue].coef[k] =
4312 mul_hwi (pb->geqs[Ue].coef[k], Lc) +
4313 mul_hwi (lbeqn->coef[k], Uc);
4315 if (dump_file && (dump_flags & TDF_DETAILS))
4317 omega_print_geq (dump_file, pb,
4318 &(pb->geqs[Ue]));
4319 fprintf (dump_file, "\n");
4324 omega_free_eqns (lbeqn, 1);
4325 continue;
4327 else
4329 int *dead_eqns = XNEWVEC (int, OMEGA_MAX_GEQS);
4330 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
4331 int num_dead = 0;
4332 int top_eqn = pb->num_geqs - 1;
4333 lower_bound_count--;
4335 if (dump_file && (dump_flags & TDF_DETAILS))
4336 fprintf (dump_file, "lower bound count = %d\n",
4337 lower_bound_count);
4339 for (Le = top_eqn; Le >= 0; Le--)
4340 if (pb->geqs[Le].coef[i] > 0)
4342 int Lc = pb->geqs[Le].coef[i];
4343 for (Ue = top_eqn; Ue >= 0; Ue--)
4344 if (pb->geqs[Ue].coef[i] < 0)
4346 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4348 int k;
4349 int Uc = -pb->geqs[Ue].coef[i];
4351 if (num_dead == 0)
4352 e2 = pb->num_geqs++;
4353 else
4354 e2 = dead_eqns[--num_dead];
4356 gcc_assert (e2 < OMEGA_MAX_GEQS);
4358 if (dump_file && (dump_flags & TDF_DETAILS))
4360 fprintf (dump_file,
4361 "Le = %d, Ue = %d, gen = %d\n",
4362 Le, Ue, e2);
4363 omega_print_geq_extra (dump_file, pb,
4364 &(pb->geqs[Le]));
4365 fprintf (dump_file, "\n");
4366 omega_print_geq_extra (dump_file, pb,
4367 &(pb->geqs[Ue]));
4368 fprintf (dump_file, "\n");
4371 eliminate_again = false;
4373 for (k = n_vars; k >= 0; k--)
4374 pb->geqs[e2].coef[k] =
4375 mul_hwi (pb->geqs[Ue].coef[k], Lc) +
4376 mul_hwi (pb->geqs[Le].coef[k], Uc);
4378 pb->geqs[e2].coef[n_vars + 1] = 0;
4379 pb->geqs[e2].touched = 1;
4381 if (pb->geqs[Ue].color == omega_red
4382 || pb->geqs[Le].color == omega_red)
4383 pb->geqs[e2].color = omega_red;
4384 else
4385 pb->geqs[e2].color = omega_black;
4387 if (dump_file && (dump_flags & TDF_DETAILS))
4389 omega_print_geq (dump_file, pb,
4390 &(pb->geqs[e2]));
4391 fprintf (dump_file, "\n");
4395 if (lower_bound_count == 0)
4397 dead_eqns[num_dead++] = Ue;
4399 if (dump_file && (dump_flags & TDF_DETAILS))
4400 fprintf (dump_file, "Killed %d\n", Ue);
4404 lower_bound_count--;
4405 dead_eqns[num_dead++] = Le;
4407 if (dump_file && (dump_flags & TDF_DETAILS))
4408 fprintf (dump_file, "Killed %d\n", Le);
4411 for (e = pb->num_geqs - 1; e >= 0; e--)
4412 is_dead[e] = false;
4414 while (num_dead > 0)
4415 is_dead[dead_eqns[--num_dead]] = true;
4417 for (e = pb->num_geqs - 1; e >= 0; e--)
4418 if (is_dead[e])
4419 omega_delete_geq_extra (pb, e, n_vars + 1);
4421 free (dead_eqns);
4422 free (is_dead);
4423 continue;
4426 else
4428 omega_pb rS, iS;
4430 rS = omega_alloc_problem (0, 0);
4431 iS = omega_alloc_problem (0, 0);
4432 e2 = 0;
4433 possible_easy_int_solution = true;
4435 for (e = 0; e < pb->num_geqs; e++)
4436 if (pb->geqs[e].coef[i] == 0)
4438 omega_copy_eqn (&(rS->geqs[e2]), &pb->geqs[e],
4439 pb->num_vars);
4440 omega_copy_eqn (&(iS->geqs[e2]), &pb->geqs[e],
4441 pb->num_vars);
4443 if (dump_file && (dump_flags & TDF_DETAILS))
4445 int t;
4446 fprintf (dump_file, "Copying (%d, %d): ", i,
4447 pb->geqs[e].coef[i]);
4448 omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
4449 fprintf (dump_file, "\n");
4450 for (t = 0; t <= n_vars + 1; t++)
4451 fprintf (dump_file, "%d ", pb->geqs[e].coef[t]);
4452 fprintf (dump_file, "\n");
4455 e2++;
4456 gcc_assert (e2 < OMEGA_MAX_GEQS);
4459 for (Le = pb->num_geqs - 1; Le >= 0; Le--)
4460 if (pb->geqs[Le].coef[i] > 0)
4461 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4462 if (pb->geqs[Ue].coef[i] < 0)
4464 int k;
4465 int Lc = pb->geqs[Le].coef[i];
4466 int Uc = -pb->geqs[Ue].coef[i];
4468 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4471 rS->geqs[e2].touched = iS->geqs[e2].touched = 1;
4473 if (dump_file && (dump_flags & TDF_DETAILS))
4475 fprintf (dump_file, "---\n");
4476 fprintf (dump_file,
4477 "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
4478 Le, Lc, Ue, Uc, e2);
4479 omega_print_geq_extra (dump_file, pb, &pb->geqs[Le]);
4480 fprintf (dump_file, "\n");
4481 omega_print_geq_extra (dump_file, pb, &pb->geqs[Ue]);
4482 fprintf (dump_file, "\n");
4485 if (Uc == Lc)
4487 for (k = n_vars; k >= 0; k--)
4488 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4489 pb->geqs[Ue].coef[k] + pb->geqs[Le].coef[k];
4491 iS->geqs[e2].coef[0] -= (Uc - 1);
4493 else
4495 for (k = n_vars; k >= 0; k--)
4496 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4497 mul_hwi (pb->geqs[Ue].coef[k], Lc) +
4498 mul_hwi (pb->geqs[Le].coef[k], Uc);
4500 iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
4503 if (pb->geqs[Ue].color == omega_red
4504 || pb->geqs[Le].color == omega_red)
4505 iS->geqs[e2].color = rS->geqs[e2].color = omega_red;
4506 else
4507 iS->geqs[e2].color = rS->geqs[e2].color = omega_black;
4509 if (dump_file && (dump_flags & TDF_DETAILS))
4511 omega_print_geq (dump_file, pb, &(rS->geqs[e2]));
4512 fprintf (dump_file, "\n");
4515 e2++;
4516 gcc_assert (e2 < OMEGA_MAX_GEQS);
4518 else if (pb->geqs[Ue].coef[0] * Lc +
4519 pb->geqs[Le].coef[0] * Uc -
4520 (Uc - 1) * (Lc - 1) < 0)
4521 possible_easy_int_solution = false;
4524 iS->variables_initialized = rS->variables_initialized = true;
4525 iS->num_vars = rS->num_vars = pb->num_vars;
4526 iS->num_geqs = rS->num_geqs = e2;
4527 iS->num_eqs = rS->num_eqs = 0;
4528 iS->num_subs = rS->num_subs = pb->num_subs;
4529 iS->safe_vars = rS->safe_vars = pb->safe_vars;
4531 for (e = n_vars; e >= 0; e--)
4532 rS->var[e] = pb->var[e];
4534 for (e = n_vars; e >= 0; e--)
4535 iS->var[e] = pb->var[e];
4537 for (e = pb->num_subs - 1; e >= 0; e--)
4539 omega_copy_eqn (&(rS->subs[e]), &(pb->subs[e]), pb->num_vars);
4540 omega_copy_eqn (&(iS->subs[e]), &(pb->subs[e]), pb->num_vars);
4543 pb->num_vars++;
4544 n_vars = pb->num_vars;
4546 if (desired_res != omega_true)
4548 if (original_problem == no_problem)
4550 original_problem = pb;
4551 result = omega_solve_geq (rS, omega_false);
4552 original_problem = no_problem;
4554 else
4555 result = omega_solve_geq (rS, omega_false);
4557 if (result == omega_false)
4559 free (rS);
4560 free (iS);
4561 return result;
4564 if (pb->num_eqs > 0)
4566 /* An equality constraint must have been found */
4567 free (rS);
4568 free (iS);
4569 return omega_solve_problem (pb, desired_res);
4573 if (desired_res != omega_false)
4575 int j;
4576 int lower_bounds = 0;
4577 int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS);
4579 if (possible_easy_int_solution)
4581 conservative++;
4582 result = omega_solve_geq (iS, desired_res);
4583 conservative--;
4585 if (result != omega_false)
4587 free (rS);
4588 free (iS);
4589 free (lower_bound);
4590 return result;
4594 if (!exact && best_parallel_eqn >= 0
4595 && parallel_difference <= max_splinters)
4597 free (rS);
4598 free (iS);
4599 free (lower_bound);
4600 return parallel_splinter (pb, best_parallel_eqn,
4601 parallel_difference,
4602 desired_res);
4605 if (dump_file && (dump_flags & TDF_DETAILS))
4606 fprintf (dump_file, "have to do exact analysis\n");
4608 conservative++;
4610 for (e = 0; e < pb->num_geqs; e++)
4611 if (pb->geqs[e].coef[i] > 1)
4612 lower_bound[lower_bounds++] = e;
4614 /* Sort array LOWER_BOUND. */
4615 for (j = 0; j < lower_bounds; j++)
4617 int k, smallest = j;
4619 for (k = j + 1; k < lower_bounds; k++)
4620 if (pb->geqs[lower_bound[smallest]].coef[i] >
4621 pb->geqs[lower_bound[k]].coef[i])
4622 smallest = k;
4624 k = lower_bound[smallest];
4625 lower_bound[smallest] = lower_bound[j];
4626 lower_bound[j] = k;
4629 if (dump_file && (dump_flags & TDF_DETAILS))
4631 fprintf (dump_file, "lower bound coefficients = ");
4633 for (j = 0; j < lower_bounds; j++)
4634 fprintf (dump_file, " %d",
4635 pb->geqs[lower_bound[j]].coef[i]);
4637 fprintf (dump_file, "\n");
4640 for (j = 0; j < lower_bounds; j++)
4642 int max_incr;
4643 int c;
4644 int worst_lower_bound_constant = -minC;
4646 e = lower_bound[j];
4647 max_incr = (((pb->geqs[e].coef[i] - 1) *
4648 (worst_lower_bound_constant - 1) - 1)
4649 / worst_lower_bound_constant);
4650 /* max_incr += 2; */
4652 if (dump_file && (dump_flags & TDF_DETAILS))
4654 fprintf (dump_file, "for equation ");
4655 omega_print_geq (dump_file, pb, &pb->geqs[e]);
4656 fprintf (dump_file,
4657 "\ntry decrements from 0 to %d\n",
4658 max_incr);
4659 omega_print_problem (dump_file, pb);
4662 if (max_incr > 50 && !smoothed
4663 && smooth_weird_equations (pb))
4665 conservative--;
4666 free (rS);
4667 free (iS);
4668 smoothed = true;
4669 goto solve_geq_start;
4672 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e],
4673 pb->num_vars);
4674 pb->eqs[0].color = omega_black;
4675 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
4676 pb->geqs[e].touched = 1;
4677 pb->num_eqs = 1;
4679 for (c = max_incr; c >= 0; c--)
4681 if (dump_file && (dump_flags & TDF_DETAILS))
4683 fprintf (dump_file,
4684 "trying next decrement of %d\n",
4685 max_incr - c);
4686 omega_print_problem (dump_file, pb);
4689 omega_copy_problem (rS, pb);
4691 if (dump_file && (dump_flags & TDF_DETAILS))
4692 omega_print_problem (dump_file, rS);
4694 result = omega_solve_problem (rS, desired_res);
4696 if (result == omega_true)
4698 free (rS);
4699 free (iS);
4700 free (lower_bound);
4701 conservative--;
4702 return omega_true;
4705 pb->eqs[0].coef[0]--;
4708 if (j + 1 < lower_bounds)
4710 pb->num_eqs = 0;
4711 omega_copy_eqn (&pb->geqs[e], &pb->eqs[0],
4712 pb->num_vars);
4713 pb->geqs[e].touched = 1;
4714 pb->geqs[e].color = omega_black;
4715 omega_copy_problem (rS, pb);
4717 if (dump_file && (dump_flags & TDF_DETAILS))
4718 fprintf (dump_file,
4719 "exhausted lower bound, "
4720 "checking if still feasible ");
4722 result = omega_solve_problem (rS, omega_false);
4724 if (result == omega_false)
4725 break;
4729 if (dump_file && (dump_flags & TDF_DETAILS))
4730 fprintf (dump_file, "fall-off the end\n");
4732 free (rS);
4733 free (iS);
4734 free (lower_bound);
4735 conservative--;
4736 return omega_false;
4739 free (rS);
4740 free (iS);
4742 return omega_unknown;
4743 } while (eliminate_again);
4744 } while (1);
4747 /* Because the omega solver is recursive, this counter limits the
4748 recursion depth. */
4749 static int omega_solve_depth = 0;
4751 /* Return omega_true when the problem PB has a solution following the
4752 DESIRED_RES. */
4754 enum omega_result
4755 omega_solve_problem (omega_pb pb, enum omega_result desired_res)
4757 enum omega_result result;
4759 gcc_assert (pb->num_vars >= pb->safe_vars);
4760 omega_solve_depth++;
4762 if (desired_res != omega_simplify)
4763 pb->safe_vars = 0;
4765 if (omega_solve_depth > 50)
4767 if (dump_file && (dump_flags & TDF_DETAILS))
4769 fprintf (dump_file,
4770 "Solve depth = %d, in_approximate_mode = %d, aborting\n",
4771 omega_solve_depth, in_approximate_mode);
4772 omega_print_problem (dump_file, pb);
4774 gcc_assert (0);
4777 if (omega_solve_eq (pb, desired_res) == omega_false)
4779 omega_solve_depth--;
4780 return omega_false;
4783 if (in_approximate_mode && !pb->num_geqs)
4785 result = omega_true;
4786 pb->num_vars = pb->safe_vars;
4787 omega_problem_reduced (pb);
4789 else
4790 result = omega_solve_geq (pb, desired_res);
4792 omega_solve_depth--;
4794 if (!omega_reduce_with_subs)
4796 resurrect_subs (pb);
4797 gcc_assert (please_no_equalities_in_simplified_problems
4798 || !result || pb->num_subs == 0);
4801 return result;
4804 /* Return true if red equations constrain the set of possible solutions.
4805 We assume that there are solutions to the black equations by
4806 themselves, so if there is no solution to the combined problem, we
4807 return true. */
4809 bool
4810 omega_problem_has_red_equations (omega_pb pb)
4812 bool result;
4813 int e;
4814 int i;
4816 if (dump_file && (dump_flags & TDF_DETAILS))
4818 fprintf (dump_file, "Checking for red equations:\n");
4819 omega_print_problem (dump_file, pb);
4822 please_no_equalities_in_simplified_problems++;
4823 may_be_red++;
4825 if (omega_single_result)
4826 return_single_result++;
4828 create_color = true;
4829 result = (omega_simplify_problem (pb) == omega_false);
4831 if (omega_single_result)
4832 return_single_result--;
4834 may_be_red--;
4835 please_no_equalities_in_simplified_problems--;
4837 if (result)
4839 if (dump_file && (dump_flags & TDF_DETAILS))
4840 fprintf (dump_file, "Gist is FALSE\n");
4842 pb->num_subs = 0;
4843 pb->num_geqs = 0;
4844 pb->num_eqs = 1;
4845 pb->eqs[0].color = omega_red;
4847 for (i = pb->num_vars; i > 0; i--)
4848 pb->eqs[0].coef[i] = 0;
4850 pb->eqs[0].coef[0] = 1;
4851 return true;
4854 free_red_eliminations (pb);
4855 gcc_assert (pb->num_eqs == 0);
4857 for (e = pb->num_geqs - 1; e >= 0; e--)
4858 if (pb->geqs[e].color == omega_red)
4860 result = true;
4861 break;
4864 if (!result)
4865 return false;
4867 for (i = pb->safe_vars; i >= 1; i--)
4869 int ub = 0;
4870 int lb = 0;
4872 for (e = pb->num_geqs - 1; e >= 0; e--)
4874 if (pb->geqs[e].coef[i])
4876 if (pb->geqs[e].coef[i] > 0)
4877 lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4879 else
4880 ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4884 if (ub == 2 || lb == 2)
4887 if (dump_file && (dump_flags & TDF_DETAILS))
4888 fprintf (dump_file, "checks for upper/lower bounds worked!\n");
4890 if (!omega_reduce_with_subs)
4892 resurrect_subs (pb);
4893 gcc_assert (pb->num_subs == 0);
4896 return true;
4901 if (dump_file && (dump_flags & TDF_DETAILS))
4902 fprintf (dump_file,
4903 "*** Doing potentially expensive elimination tests "
4904 "for red equations\n");
4906 please_no_equalities_in_simplified_problems++;
4907 omega_eliminate_red (pb, true);
4908 please_no_equalities_in_simplified_problems--;
4910 result = false;
4911 gcc_assert (pb->num_eqs == 0);
4913 for (e = pb->num_geqs - 1; e >= 0; e--)
4914 if (pb->geqs[e].color == omega_red)
4916 result = true;
4917 break;
4920 if (dump_file && (dump_flags & TDF_DETAILS))
4922 if (!result)
4923 fprintf (dump_file,
4924 "******************** Redundant Red Equations eliminated!!\n");
4925 else
4926 fprintf (dump_file,
4927 "******************** Red Equations remain\n");
4929 omega_print_problem (dump_file, pb);
4932 if (!omega_reduce_with_subs)
4934 normalize_return_type r;
4936 resurrect_subs (pb);
4937 r = normalize_omega_problem (pb);
4938 gcc_assert (r != normalize_false);
4940 coalesce (pb);
4941 cleanout_wildcards (pb);
4942 gcc_assert (pb->num_subs == 0);
4945 return result;
4948 /* Calls omega_simplify_problem in approximate mode. */
4950 enum omega_result
4951 omega_simplify_approximate (omega_pb pb)
4953 enum omega_result result;
4955 if (dump_file && (dump_flags & TDF_DETAILS))
4956 fprintf (dump_file, "(Entering approximate mode\n");
4958 in_approximate_mode = true;
4959 result = omega_simplify_problem (pb);
4960 in_approximate_mode = false;
4962 gcc_assert (pb->num_vars == pb->safe_vars);
4963 if (!omega_reduce_with_subs)
4964 gcc_assert (pb->num_subs == 0);
4966 if (dump_file && (dump_flags & TDF_DETAILS))
4967 fprintf (dump_file, "Leaving approximate mode)\n");
4969 return result;
4973 /* Simplifies problem PB by eliminating redundant constraints and
4974 reducing the constraints system to a minimal form. Returns
4975 omega_true when the problem was successfully reduced, omega_unknown
4976 when the solver is unable to determine an answer. */
4978 enum omega_result
4979 omega_simplify_problem (omega_pb pb)
4981 int i;
4983 omega_found_reduction = omega_false;
4985 if (!pb->variables_initialized)
4986 omega_initialize_variables (pb);
4988 if (next_key * 3 > MAX_KEYS)
4990 int e;
4992 hash_version++;
4993 next_key = OMEGA_MAX_VARS + 1;
4995 for (e = pb->num_geqs - 1; e >= 0; e--)
4996 pb->geqs[e].touched = 1;
4998 for (i = 0; i < HASH_TABLE_SIZE; i++)
4999 hash_master[i].touched = -1;
5001 pb->hash_version = hash_version;
5004 else if (pb->hash_version != hash_version)
5006 int e;
5008 for (e = pb->num_geqs - 1; e >= 0; e--)
5009 pb->geqs[e].touched = 1;
5011 pb->hash_version = hash_version;
5014 if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars)
5015 omega_free_eliminations (pb, pb->safe_vars);
5017 if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0)
5019 omega_found_reduction = omega_solve_problem (pb, omega_unknown);
5021 if (omega_found_reduction != omega_false
5022 && !return_single_result)
5024 pb->num_geqs = 0;
5025 pb->num_eqs = 0;
5026 (*omega_when_reduced) (pb);
5029 return omega_found_reduction;
5032 omega_solve_problem (pb, omega_simplify);
5034 if (omega_found_reduction != omega_false)
5036 for (i = 1; omega_safe_var_p (pb, i); i++)
5037 pb->forwarding_address[pb->var[i]] = i;
5039 for (i = 0; i < pb->num_subs; i++)
5040 pb->forwarding_address[pb->subs[i].key] = -i - 1;
5043 if (!omega_reduce_with_subs)
5044 gcc_assert (please_no_equalities_in_simplified_problems
5045 || omega_found_reduction == omega_false
5046 || pb->num_subs == 0);
5048 return omega_found_reduction;
5051 /* Make variable VAR unprotected: it then can be eliminated. */
5053 void
5054 omega_unprotect_variable (omega_pb pb, int var)
5056 int e, idx;
5057 idx = pb->forwarding_address[var];
5059 if (idx < 0)
5061 idx = -1 - idx;
5062 pb->num_subs--;
5064 if (idx < pb->num_subs)
5066 omega_copy_eqn (&pb->subs[idx], &pb->subs[pb->num_subs],
5067 pb->num_vars);
5068 pb->forwarding_address[pb->subs[idx].key] = -idx - 1;
5071 else
5073 int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS);
5074 int e2;
5076 for (e = pb->num_subs - 1; e >= 0; e--)
5077 bring_to_life[e] = (pb->subs[e].coef[idx] != 0);
5079 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
5080 if (bring_to_life[e2])
5082 pb->num_vars++;
5083 pb->safe_vars++;
5085 if (pb->safe_vars < pb->num_vars)
5087 for (e = pb->num_geqs - 1; e >= 0; e--)
5089 pb->geqs[e].coef[pb->num_vars] =
5090 pb->geqs[e].coef[pb->safe_vars];
5092 pb->geqs[e].coef[pb->safe_vars] = 0;
5095 for (e = pb->num_eqs - 1; e >= 0; e--)
5097 pb->eqs[e].coef[pb->num_vars] =
5098 pb->eqs[e].coef[pb->safe_vars];
5100 pb->eqs[e].coef[pb->safe_vars] = 0;
5103 for (e = pb->num_subs - 1; e >= 0; e--)
5105 pb->subs[e].coef[pb->num_vars] =
5106 pb->subs[e].coef[pb->safe_vars];
5108 pb->subs[e].coef[pb->safe_vars] = 0;
5111 pb->var[pb->num_vars] = pb->var[pb->safe_vars];
5112 pb->forwarding_address[pb->var[pb->num_vars]] =
5113 pb->num_vars;
5115 else
5117 for (e = pb->num_geqs - 1; e >= 0; e--)
5118 pb->geqs[e].coef[pb->safe_vars] = 0;
5120 for (e = pb->num_eqs - 1; e >= 0; e--)
5121 pb->eqs[e].coef[pb->safe_vars] = 0;
5123 for (e = pb->num_subs - 1; e >= 0; e--)
5124 pb->subs[e].coef[pb->safe_vars] = 0;
5127 pb->var[pb->safe_vars] = pb->subs[e2].key;
5128 pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars;
5130 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e2]),
5131 pb->num_vars);
5132 pb->eqs[pb->num_eqs++].coef[pb->safe_vars] = -1;
5133 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5135 if (e2 < pb->num_subs - 1)
5136 omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]),
5137 pb->num_vars);
5139 pb->num_subs--;
5142 omega_unprotect_1 (pb, &idx, NULL);
5143 free (bring_to_life);
5146 chain_unprotect (pb);
5149 /* Unprotects VAR and simplifies PB. */
5151 enum omega_result
5152 omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color,
5153 int var, int sign)
5155 int n_vars = pb->num_vars;
5156 int e, j;
5157 int k = pb->forwarding_address[var];
5159 if (k < 0)
5161 k = -1 - k;
5163 if (sign != 0)
5165 e = pb->num_geqs++;
5166 omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars);
5168 for (j = 0; j <= n_vars; j++)
5169 pb->geqs[e].coef[j] *= sign;
5171 pb->geqs[e].coef[0]--;
5172 pb->geqs[e].touched = 1;
5173 pb->geqs[e].color = color;
5175 else
5177 e = pb->num_eqs++;
5178 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5179 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5180 pb->eqs[e].color = color;
5183 else if (sign != 0)
5185 e = pb->num_geqs++;
5186 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
5187 pb->geqs[e].coef[k] = sign;
5188 pb->geqs[e].coef[0] = -1;
5189 pb->geqs[e].touched = 1;
5190 pb->geqs[e].color = color;
5192 else
5194 e = pb->num_eqs++;
5195 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5196 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5197 pb->eqs[e].coef[k] = 1;
5198 pb->eqs[e].color = color;
5201 omega_unprotect_variable (pb, var);
5202 return omega_simplify_problem (pb);
5205 /* Add an equation "VAR = VALUE" with COLOR to PB. */
5207 void
5208 omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color,
5209 int var, int value)
5211 int e;
5212 int k = pb->forwarding_address[var];
5214 if (k < 0)
5216 k = -1 - k;
5217 e = pb->num_eqs++;
5218 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5219 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5220 pb->eqs[e].coef[0] -= value;
5222 else
5224 e = pb->num_eqs++;
5225 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5226 pb->eqs[e].coef[k] = 1;
5227 pb->eqs[e].coef[0] = -value;
5230 pb->eqs[e].color = color;
5233 /* Return false when the upper and lower bounds are not coupled.
5234 Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
5235 variable I. */
5237 bool
5238 omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound)
5240 int n_vars = pb->num_vars;
5241 int e, j;
5242 bool is_simple;
5243 bool coupled = false;
5245 *lower_bound = neg_infinity;
5246 *upper_bound = pos_infinity;
5247 i = pb->forwarding_address[i];
5249 if (i < 0)
5251 i = -i - 1;
5253 for (j = 1; j <= n_vars; j++)
5254 if (pb->subs[i].coef[j] != 0)
5255 return true;
5257 *upper_bound = *lower_bound = pb->subs[i].coef[0];
5258 return false;
5261 for (e = pb->num_subs - 1; e >= 0; e--)
5262 if (pb->subs[e].coef[i] != 0)
5264 coupled = true;
5265 break;
5268 for (e = pb->num_eqs - 1; e >= 0; e--)
5269 if (pb->eqs[e].coef[i] != 0)
5271 is_simple = true;
5273 for (j = 1; j <= n_vars; j++)
5274 if (i != j && pb->eqs[e].coef[j] != 0)
5276 is_simple = false;
5277 coupled = true;
5278 break;
5281 if (!is_simple)
5282 continue;
5283 else
5285 *lower_bound = *upper_bound =
5286 -pb->eqs[e].coef[i] * pb->eqs[e].coef[0];
5287 return false;
5291 for (e = pb->num_geqs - 1; e >= 0; e--)
5292 if (pb->geqs[e].coef[i] != 0)
5294 if (pb->geqs[e].key == i)
5295 *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]);
5297 else if (pb->geqs[e].key == -i)
5298 *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]);
5300 else
5301 coupled = true;
5304 return coupled;
5307 /* Sets the lower bound L and upper bound U for the values of variable
5308 I, and sets COULD_BE_ZERO to true if variable I might take value
5309 zero. LOWER_BOUND and UPPER_BOUND are bounds on the values of
5310 variable I. */
5312 static void
5313 query_coupled_variable (omega_pb pb, int i, int *l, int *u,
5314 bool *could_be_zero, int lower_bound, int upper_bound)
5316 int e, b1, b2;
5317 eqn eqn;
5318 int sign;
5319 int v;
5321 /* Preconditions. */
5322 gcc_assert (abs (pb->forwarding_address[i]) == 1
5323 && pb->num_vars + pb->num_subs == 2
5324 && pb->num_eqs + pb->num_subs == 1);
5326 /* Define variable I in terms of variable V. */
5327 if (pb->forwarding_address[i] == -1)
5329 eqn = &pb->subs[0];
5330 sign = 1;
5331 v = 1;
5333 else
5335 eqn = &pb->eqs[0];
5336 sign = -eqn->coef[1];
5337 v = 2;
5340 for (e = pb->num_geqs - 1; e >= 0; e--)
5341 if (pb->geqs[e].coef[v] != 0)
5343 if (pb->geqs[e].coef[v] == 1)
5344 lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]);
5346 else
5347 upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]);
5350 if (lower_bound > upper_bound)
5352 *l = pos_infinity;
5353 *u = neg_infinity;
5354 *could_be_zero = 0;
5355 return;
5358 if (lower_bound == neg_infinity)
5360 if (eqn->coef[v] > 0)
5361 b1 = sign * neg_infinity;
5363 else
5364 b1 = -sign * neg_infinity;
5366 else
5367 b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound);
5369 if (upper_bound == pos_infinity)
5371 if (eqn->coef[v] > 0)
5372 b2 = sign * pos_infinity;
5374 else
5375 b2 = -sign * pos_infinity;
5377 else
5378 b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound);
5380 *l = MAX (*l, b1 <= b2 ? b1 : b2);
5381 *u = MIN (*u, b1 <= b2 ? b2 : b1);
5383 *could_be_zero = (*l <= 0 && 0 <= *u
5384 && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0);
5387 /* Return false when a lower bound L and an upper bound U for variable
5388 I in problem PB have been initialized. */
5390 bool
5391 omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u)
5393 *l = neg_infinity;
5394 *u = pos_infinity;
5396 if (!omega_query_variable (pb, i, l, u)
5397 || (pb->num_vars == 1 && pb->forwarding_address[i] == 1))
5398 return false;
5400 if (abs (pb->forwarding_address[i]) == 1
5401 && pb->num_vars + pb->num_subs == 2
5402 && pb->num_eqs + pb->num_subs == 1)
5404 bool could_be_zero;
5405 query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity,
5406 pos_infinity);
5407 return false;
5410 return true;
5413 /* For problem PB, return an integer that represents the classic data
5414 dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
5415 masks that are added to the result. When DIST_KNOWN is true, DIST
5416 is set to the classic data dependence distance. LOWER_BOUND and
5417 UPPER_BOUND are bounds on the value of variable I, for example, it
5418 is possible to narrow the iteration domain with safe approximations
5419 of loop counts, and thus discard some data dependences that cannot
5420 occur. */
5423 omega_query_variable_signs (omega_pb pb, int i, int dd_lt,
5424 int dd_eq, int dd_gt, int lower_bound,
5425 int upper_bound, bool *dist_known, int *dist)
5427 int result;
5428 int l, u;
5429 bool could_be_zero;
5431 l = neg_infinity;
5432 u = pos_infinity;
5434 omega_query_variable (pb, i, &l, &u);
5435 query_coupled_variable (pb, i, &l, &u, &could_be_zero, lower_bound,
5436 upper_bound);
5437 result = 0;
5439 if (l < 0)
5440 result |= dd_gt;
5442 if (u > 0)
5443 result |= dd_lt;
5445 if (could_be_zero)
5446 result |= dd_eq;
5448 if (l == u)
5450 *dist_known = true;
5451 *dist = l;
5453 else
5454 *dist_known = false;
5456 return result;
5459 /* Initialize PB as an Omega problem with NVARS variables and NPROT
5460 safe variables. Safe variables are not eliminated during the
5461 Fourier-Motzkin elimination. Safe variables are all those
5462 variables that are placed at the beginning of the array of
5463 variables: P->var[0, ..., NPROT - 1]. */
5465 omega_pb
5466 omega_alloc_problem (int nvars, int nprot)
5468 omega_pb pb;
5470 gcc_assert (nvars <= OMEGA_MAX_VARS);
5471 omega_initialize ();
5473 /* Allocate and initialize PB. */
5474 pb = XCNEW (struct omega_pb_d);
5475 pb->var = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5476 pb->forwarding_address = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5477 pb->geqs = omega_alloc_eqns (0, OMEGA_MAX_GEQS);
5478 pb->eqs = omega_alloc_eqns (0, OMEGA_MAX_EQS);
5479 pb->subs = omega_alloc_eqns (0, OMEGA_MAX_VARS + 1);
5481 pb->hash_version = hash_version;
5482 pb->num_vars = nvars;
5483 pb->safe_vars = nprot;
5484 pb->variables_initialized = false;
5485 pb->variables_freed = false;
5486 pb->num_eqs = 0;
5487 pb->num_geqs = 0;
5488 pb->num_subs = 0;
5489 return pb;
5492 /* Keeps the state of the initialization. */
5493 static bool omega_initialized = false;
5495 /* Initialization of the Omega solver. */
5497 void
5498 omega_initialize (void)
5500 int i;
5502 if (omega_initialized)
5503 return;
5505 next_wild_card = 0;
5506 next_key = OMEGA_MAX_VARS + 1;
5507 packing = XCNEWVEC (int, OMEGA_MAX_VARS);
5508 fast_lookup = XCNEWVEC (int, MAX_KEYS * 2);
5509 fast_lookup_red = XCNEWVEC (int, MAX_KEYS * 2);
5510 hash_master = omega_alloc_eqns (0, HASH_TABLE_SIZE);
5512 for (i = 0; i < HASH_TABLE_SIZE; i++)
5513 hash_master[i].touched = -1;
5515 sprintf (wild_name[0], "1");
5516 sprintf (wild_name[1], "a");
5517 sprintf (wild_name[2], "b");
5518 sprintf (wild_name[3], "c");
5519 sprintf (wild_name[4], "d");
5520 sprintf (wild_name[5], "e");
5521 sprintf (wild_name[6], "f");
5522 sprintf (wild_name[7], "g");
5523 sprintf (wild_name[8], "h");
5524 sprintf (wild_name[9], "i");
5525 sprintf (wild_name[10], "j");
5526 sprintf (wild_name[11], "k");
5527 sprintf (wild_name[12], "l");
5528 sprintf (wild_name[13], "m");
5529 sprintf (wild_name[14], "n");
5530 sprintf (wild_name[15], "o");
5531 sprintf (wild_name[16], "p");
5532 sprintf (wild_name[17], "q");
5533 sprintf (wild_name[18], "r");
5534 sprintf (wild_name[19], "s");
5535 sprintf (wild_name[20], "t");
5536 sprintf (wild_name[40 - 1], "alpha");
5537 sprintf (wild_name[40 - 2], "beta");
5538 sprintf (wild_name[40 - 3], "gamma");
5539 sprintf (wild_name[40 - 4], "delta");
5540 sprintf (wild_name[40 - 5], "tau");
5541 sprintf (wild_name[40 - 6], "sigma");
5542 sprintf (wild_name[40 - 7], "chi");
5543 sprintf (wild_name[40 - 8], "omega");
5544 sprintf (wild_name[40 - 9], "pi");
5545 sprintf (wild_name[40 - 10], "ni");
5546 sprintf (wild_name[40 - 11], "Alpha");
5547 sprintf (wild_name[40 - 12], "Beta");
5548 sprintf (wild_name[40 - 13], "Gamma");
5549 sprintf (wild_name[40 - 14], "Delta");
5550 sprintf (wild_name[40 - 15], "Tau");
5551 sprintf (wild_name[40 - 16], "Sigma");
5552 sprintf (wild_name[40 - 17], "Chi");
5553 sprintf (wild_name[40 - 18], "Omega");
5554 sprintf (wild_name[40 - 19], "xxx");
5556 omega_initialized = true;