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