projects / gcc.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
re PR tree-optimization/43833 (false warning: array subscript is above array bounds...
[gcc.git] / gcc / omega.c
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, 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
1996 for (e = pb->num_geqs - 1; e >= 0; e--)
1997 if (single_var_geq (&pb->geqs[e], pb->num_vars))
1998 {
1999 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
2000 pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m);
2001 }
2002 else
2003 {
2004 pb->geqs[e].touched = 1;
2005 pb->geqs[e].key = 0;
2006 }
2007
2008 for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--)
2009 {
2010 pb->var[i + m] = pb->var[i];
2011
2012 for (e = pb->num_geqs - 1; e >= 0; e--)
2013 pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i];
2014
2015 for (e = pb->num_eqs - 1; e >= 0; e--)
2016 pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i];
2017
2018 for (e = pb->num_subs - 1; e >= 0; e--)
2019 pb->subs[e].coef[i + m] = pb->subs[e].coef[i];
2020 }
2021
2022 for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--)
2023 {
2024 for (e = pb->num_geqs - 1; e >= 0; e--)
2025 pb->geqs[e].coef[i] = 0;
2026
2027 for (e = pb->num_eqs - 1; e >= 0; e--)
2028 pb->eqs[e].coef[i] = 0;
2029
2030 for (e = pb->num_subs - 1; e >= 0; e--)
2031 pb->subs[e].coef[i] = 0;
2032 }
2033
2034 pb->num_vars += m;
2035
2036 for (e = pb->num_subs - 1; e >= 0; e--)
2037 {
2038 pb->var[pb->safe_vars + 1 + e] = pb->subs[e].key;
2039 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e]),
2040 pb->num_vars);
2041 pb->eqs[pb->num_eqs].coef[pb->safe_vars + 1 + e] = -1;
2042 pb->eqs[pb->num_eqs].color = omega_black;
2043
2044 if (dump_file && (dump_flags & TDF_DETAILS))
2045 {
2046 fprintf (dump_file, "brought back: ");
2047 omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]);
2048 fprintf (dump_file, "\n");
2049 }
2050
2051 pb->num_eqs++;
2052 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2053 }
2054
2055 pb->safe_vars += m;
2056 pb->num_subs = 0;
2057
2058 if (dump_file && (dump_flags & TDF_DETAILS))
2059 {
2060 fprintf (dump_file, "variables brought back to life\n");
2061 omega_print_problem (dump_file, pb);
2062 }
2063
2064 cleanout_wildcards (pb);
2065 }
2066 }
2067
2068 static inline bool
2069 implies (unsigned int a, unsigned int b)
2070 {
2071 return (a == (a & b));
2072 }
2073
2074 /* Eliminate redundant equations in PB. When EXPENSIVE is true, an
2075 extra step is performed. Returns omega_false when there exist no
2076 solution, omega_true otherwise. */
2077
2078 enum omega_result
2079 omega_eliminate_redundant (omega_pb pb, bool expensive)
2080 {
2081 int c, e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3;
2082 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2083 omega_pb tmp_problem;
2084
2085 /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations. */
2086 unsigned int *peqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2087 unsigned int *zeqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2088 unsigned int *neqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2089
2090 /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
2091 unsigned int pp, pz, pn;
2092
2093 if (dump_file && (dump_flags & TDF_DETAILS))
2094 {
2095 fprintf (dump_file, "in eliminate Redundant:\n");
2096 omega_print_problem (dump_file, pb);
2097 }
2098
2099 for (e = pb->num_geqs - 1; e >= 0; e--)
2100 {
2101 int tmp = 1;
2102
2103 is_dead[e] = false;
2104 peqs[e] = zeqs[e] = neqs[e] = 0;
2105
2106 for (i = pb->num_vars; i >= 1; i--)
2107 {
2108 if (pb->geqs[e].coef[i] > 0)
2109 peqs[e] |= tmp;
2110 else if (pb->geqs[e].coef[i] < 0)
2111 neqs[e] |= tmp;
2112 else
2113 zeqs[e] |= tmp;
2114
2115 tmp <<= 1;
2116 }
2117 }
2118
2119
2120 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2121 if (!is_dead[e1])
2122 for (e2 = e1 - 1; e2 >= 0; e2--)
2123 if (!is_dead[e2])
2124 {
2125 for (p = pb->num_vars; p > 1; p--)
2126 for (q = p - 1; q > 0; q--)
2127 if ((alpha = pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q]
2128 - pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]) != 0)
2129 goto foundPQ;
2130
2131 continue;
2132
2133 foundPQ:
2134 pz = ((zeqs[e1] & zeqs[e2]) | (peqs[e1] & neqs[e2])
2135 | (neqs[e1] & peqs[e2]));
2136 pp = peqs[e1] | peqs[e2];
2137 pn = neqs[e1] | neqs[e2];
2138
2139 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2140 if (e3 != e1 && e3 != e2)
2141 {
2142 if (!implies (zeqs[e3], pz))
2143 goto nextE3;
2144
2145 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2146 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2147 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2148 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2149 alpha3 = alpha;
2150
2151 if (alpha1 * alpha2 <= 0)
2152 goto nextE3;
2153
2154 if (alpha1 < 0)
2155 {
2156 alpha1 = -alpha1;
2157 alpha2 = -alpha2;
2158 alpha3 = -alpha3;
2159 }
2160
2161 if (alpha3 > 0)
2162 {
2163 /* Trying to prove e3 is redundant. */
2164 if (!implies (peqs[e3], pp)
2165 || !implies (neqs[e3], pn))
2166 goto nextE3;
2167
2168 if (pb->geqs[e3].color == omega_black
2169 && (pb->geqs[e1].color == omega_red
2170 || pb->geqs[e2].color == omega_red))
2171 goto nextE3;
2172
2173 for (k = pb->num_vars; k >= 1; k--)
2174 if (alpha3 * pb->geqs[e3].coef[k]
2175 != (alpha1 * pb->geqs[e1].coef[k]
2176 + alpha2 * pb->geqs[e2].coef[k]))
2177 goto nextE3;
2178
2179 c = (alpha1 * pb->geqs[e1].coef[0]
2180 + alpha2 * pb->geqs[e2].coef[0]);
2181
2182 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2183 {
2184 if (dump_file && (dump_flags & TDF_DETAILS))
2185 {
2186 fprintf (dump_file,
2187 "found redundant inequality\n");
2188 fprintf (dump_file,
2189 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2190 alpha1, alpha2, alpha3);
2191
2192 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2193 fprintf (dump_file, "\n");
2194 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2195 fprintf (dump_file, "\n=> ");
2196 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2197 fprintf (dump_file, "\n\n");
2198 }
2199
2200 is_dead[e3] = true;
2201 }
2202 }
2203 else
2204 {
2205 /* Trying to prove e3 <= 0 and therefore e3 = 0,
2206 or trying to prove e3 < 0, and therefore the
2207 problem has no solutions. */
2208 if (!implies (peqs[e3], pn)
2209 || !implies (neqs[e3], pp))
2210 goto nextE3;
2211
2212 if (pb->geqs[e1].color == omega_red
2213 || pb->geqs[e2].color == omega_red
2214 || pb->geqs[e3].color == omega_red)
2215 goto nextE3;
2216
2217 alpha3 = alpha3;
2218 /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
2219 for (k = pb->num_vars; k >= 1; k--)
2220 if (alpha3 * pb->geqs[e3].coef[k]
2221 != (alpha1 * pb->geqs[e1].coef[k]
2222 + alpha2 * pb->geqs[e2].coef[k]))
2223 goto nextE3;
2224
2225 c = (alpha1 * pb->geqs[e1].coef[0]
2226 + alpha2 * pb->geqs[e2].coef[0]);
2227
2228 if (c < alpha3 * (pb->geqs[e3].coef[0]))
2229 {
2230 /* We just proved e3 < 0, so no solutions exist. */
2231 if (dump_file && (dump_flags & TDF_DETAILS))
2232 {
2233 fprintf (dump_file,
2234 "found implied over tight inequality\n");
2235 fprintf (dump_file,
2236 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2237 alpha1, alpha2, -alpha3);
2238 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2239 fprintf (dump_file, "\n");
2240 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2241 fprintf (dump_file, "\n=> not ");
2242 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2243 fprintf (dump_file, "\n\n");
2244 }
2245 free (is_dead);
2246 free (peqs);
2247 free (zeqs);
2248 free (neqs);
2249 return omega_false;
2250 }
2251 else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
2252 {
2253 /* We just proved that e3 <=0, so e3 = 0. */
2254 if (dump_file && (dump_flags & TDF_DETAILS))
2255 {
2256 fprintf (dump_file,
2257 "found implied tight inequality\n");
2258 fprintf (dump_file,
2259 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2260 alpha1, alpha2, -alpha3);
2261 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2262 fprintf (dump_file, "\n");
2263 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2264 fprintf (dump_file, "\n=> inverse ");
2265 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2266 fprintf (dump_file, "\n\n");
2267 }
2268
2269 omega_copy_eqn (&pb->eqs[pb->num_eqs++],
2270 &pb->geqs[e3], pb->num_vars);
2271 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2272 adding_equality_constraint (pb, pb->num_eqs - 1);
2273 is_dead[e3] = true;
2274 }
2275 }
2276 nextE3:;
2277 }
2278 }
2279
2280 /* Delete the inequalities that were marked as dead. */
2281 for (e = pb->num_geqs - 1; e >= 0; e--)
2282 if (is_dead[e])
2283 omega_delete_geq (pb, e, pb->num_vars);
2284
2285 if (!expensive)
2286 goto eliminate_redundant_done;
2287
2288 tmp_problem = XNEW (struct omega_pb_d);
2289 conservative++;
2290
2291 for (e = pb->num_geqs - 1; e >= 0; e--)
2292 {
2293 if (dump_file && (dump_flags & TDF_DETAILS))
2294 {
2295 fprintf (dump_file,
2296 "checking equation %d to see if it is redundant: ", e);
2297 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2298 fprintf (dump_file, "\n");
2299 }
2300
2301 omega_copy_problem (tmp_problem, pb);
2302 omega_negate_geq (tmp_problem, e);
2303 tmp_problem->safe_vars = 0;
2304 tmp_problem->variables_freed = false;
2305
2306 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2307 omega_delete_geq (pb, e, pb->num_vars);
2308 }
2309
2310 free (tmp_problem);
2311 conservative--;
2312
2313 if (!omega_reduce_with_subs)
2314 {
2315 resurrect_subs (pb);
2316 gcc_assert (please_no_equalities_in_simplified_problems
2317 || pb->num_subs == 0);
2318 }
2319
2320 eliminate_redundant_done:
2321 free (is_dead);
2322 free (peqs);
2323 free (zeqs);
2324 free (neqs);
2325 return omega_true;
2326 }
2327
2328 /* For each inequality that has coefficients bigger than 20, try to
2329 create a new constraint that cannot be derived from the original
2330 constraint and that has smaller coefficients. Add the new
2331 constraint at the end of geqs. Return the number of inequalities
2332 that have been added to PB. */
2333
2334 static int
2335 smooth_weird_equations (omega_pb pb)
2336 {
2337 int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
2338 int c;
2339 int v;
2340 int result = 0;
2341
2342 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2343 if (pb->geqs[e1].color == omega_black)
2344 {
2345 int g = 999999;
2346
2347 for (v = pb->num_vars; v >= 1; v--)
2348 if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g)
2349 g = abs (pb->geqs[e1].coef[v]);
2350
2351 /* Magic number. */
2352 if (g > 20)
2353 {
2354 e3 = pb->num_geqs;
2355
2356 for (v = pb->num_vars; v >= 1; v--)
2357 pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2,
2358 g);
2359
2360 pb->geqs[e3].color = omega_black;
2361 pb->geqs[e3].touched = 1;
2362 /* Magic number. */
2363 pb->geqs[e3].coef[0] = 9997;
2364
2365 if (dump_file && (dump_flags & TDF_DETAILS))
2366 {
2367 fprintf (dump_file, "Checking to see if we can derive: ");
2368 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2369 fprintf (dump_file, "\n from: ");
2370 omega_print_geq (dump_file, pb, &pb->geqs[e1]);
2371 fprintf (dump_file, "\n");
2372 }
2373
2374 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
2375 if (e1 != e2 && pb->geqs[e2].color == omega_black)
2376 {
2377 for (p = pb->num_vars; p > 1; p--)
2378 {
2379 for (q = p - 1; q > 0; q--)
2380 {
2381 alpha =
2382 (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] -
2383 pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]);
2384 if (alpha != 0)
2385 goto foundPQ;
2386 }
2387 }
2388 continue;
2389
2390 foundPQ:
2391
2392 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2393 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2394 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2395 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2396 alpha3 = alpha;
2397
2398 if (alpha1 * alpha2 <= 0)
2399 continue;
2400
2401 if (alpha1 < 0)
2402 {
2403 alpha1 = -alpha1;
2404 alpha2 = -alpha2;
2405 alpha3 = -alpha3;
2406 }
2407
2408 if (alpha3 > 0)
2409 {
2410 /* Try to prove e3 is redundant: verify
2411 alpha1*v1 + alpha2*v2 = alpha3*v3. */
2412 for (k = pb->num_vars; k >= 1; k--)
2413 if (alpha3 * pb->geqs[e3].coef[k]
2414 != (alpha1 * pb->geqs[e1].coef[k]
2415 + alpha2 * pb->geqs[e2].coef[k]))
2416 goto nextE2;
2417
2418 c = alpha1 * pb->geqs[e1].coef[0]
2419 + alpha2 * pb->geqs[e2].coef[0];
2420
2421 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2422 pb->geqs[e3].coef[0] = int_div (c, alpha3);
2423 }
2424 nextE2:;
2425 }
2426
2427 if (pb->geqs[e3].coef[0] < 9997)
2428 {
2429 result++;
2430 pb->num_geqs++;
2431
2432 if (dump_file && (dump_flags & TDF_DETAILS))
2433 {
2434 fprintf (dump_file,
2435 "Smoothing weird equations; adding:\n");
2436 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2437 fprintf (dump_file, "\nto:\n");
2438 omega_print_problem (dump_file, pb);
2439 fprintf (dump_file, "\n\n");
2440 }
2441 }
2442 }
2443 }
2444 return result;
2445 }
2446
2447 /* Replace tuples of inequalities, that define upper and lower half
2448 spaces, with an equation. */
2449
2450 static void
2451 coalesce (omega_pb pb)
2452 {
2453 int e, e2;
2454 int colors = 0;
2455 bool *is_dead;
2456 int found_something = 0;
2457
2458 for (e = 0; e < pb->num_geqs; e++)
2459 if (pb->geqs[e].color == omega_red)
2460 colors++;
2461
2462 if (colors < 2)
2463 return;
2464
2465 is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2466
2467 for (e = 0; e < pb->num_geqs; e++)
2468 is_dead[e] = false;
2469
2470 for (e = 0; e < pb->num_geqs; e++)
2471 if (pb->geqs[e].color == omega_red
2472 && !pb->geqs[e].touched)
2473 for (e2 = e + 1; e2 < pb->num_geqs; e2++)
2474 if (!pb->geqs[e2].touched
2475 && pb->geqs[e].key == -pb->geqs[e2].key
2476 && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0]
2477 && pb->geqs[e2].color == omega_red)
2478 {
2479 omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e],
2480 pb->num_vars);
2481 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2482 found_something++;
2483 is_dead[e] = true;
2484 is_dead[e2] = true;
2485 }
2486
2487 for (e = pb->num_geqs - 1; e >= 0; e--)
2488 if (is_dead[e])
2489 omega_delete_geq (pb, e, pb->num_vars);
2490
2491 if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
2492 {
2493 fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
2494 found_something);
2495 omega_print_problem (dump_file, pb);
2496 }
2497
2498 free (is_dead);
2499 }
2500
2501 /* Eliminate red inequalities from PB. When ELIMINATE_ALL is
2502 true, continue to eliminate all the red inequalities. */
2503
2504 void
2505 omega_eliminate_red (omega_pb pb, bool eliminate_all)
2506 {
2507 int e, e2, e3, i, j, k, a, alpha1, alpha2;
2508 int c = 0;
2509 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2510 int dead_count = 0;
2511 int red_found;
2512 omega_pb tmp_problem;
2513
2514 if (dump_file && (dump_flags & TDF_DETAILS))
2515 {
2516 fprintf (dump_file, "in eliminate RED:\n");
2517 omega_print_problem (dump_file, pb);
2518 }
2519
2520 if (pb->num_eqs > 0)
2521 omega_simplify_problem (pb);
2522
2523 for (e = pb->num_geqs - 1; e >= 0; e--)
2524 is_dead[e] = false;
2525
2526 for (e = pb->num_geqs - 1; e >= 0; e--)
2527 if (pb->geqs[e].color == omega_black && !is_dead[e])
2528 for (e2 = e - 1; e2 >= 0; e2--)
2529 if (pb->geqs[e2].color == omega_black
2530 && !is_dead[e2])
2531 {
2532 a = 0;
2533
2534 for (i = pb->num_vars; i > 1; i--)
2535 for (j = i - 1; j > 0; j--)
2536 if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j]
2537 - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0)
2538 goto found_pair;
2539
2540 continue;
2541
2542 found_pair:
2543 if (dump_file && (dump_flags & TDF_DETAILS))
2544 {
2545 fprintf (dump_file,
2546 "found two equations to combine, i = %s, ",
2547 omega_variable_to_str (pb, i));
2548 fprintf (dump_file, "j = %s, alpha = %d\n",
2549 omega_variable_to_str (pb, j), a);
2550 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2551 fprintf (dump_file, "\n");
2552 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2553 fprintf (dump_file, "\n");
2554 }
2555
2556 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2557 if (pb->geqs[e3].color == omega_red)
2558 {
2559 alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i]
2560 - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]);
2561 alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i]
2562 - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]);
2563
2564 if ((a > 0 && alpha1 > 0 && alpha2 > 0)
2565 || (a < 0 && alpha1 < 0 && alpha2 < 0))
2566 {
2567 if (dump_file && (dump_flags & TDF_DETAILS))
2568 {
2569 fprintf (dump_file,
2570 "alpha1 = %d, alpha2 = %d;"
2571 "comparing against: ",
2572 alpha1, alpha2);
2573 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2574 fprintf (dump_file, "\n");
2575 }
2576
2577 for (k = pb->num_vars; k >= 0; k--)
2578 {
2579 c = (alpha1 * pb->geqs[e].coef[k]
2580 + alpha2 * pb->geqs[e2].coef[k]);
2581
2582 if (c != a * pb->geqs[e3].coef[k])
2583 break;
2584
2585 if (dump_file && (dump_flags & TDF_DETAILS) && k > 0)
2586 fprintf (dump_file, " %s: %d, %d\n",
2587 omega_variable_to_str (pb, k), c,
2588 a * pb->geqs[e3].coef[k]);
2589 }
2590
2591 if (k < 0
2592 || (k == 0 &&
2593 ((a > 0 && c < a * pb->geqs[e3].coef[k])
2594 || (a < 0 && c > a * pb->geqs[e3].coef[k]))))
2595 {
2596 if (dump_file && (dump_flags & TDF_DETAILS))
2597 {
2598 dead_count++;
2599 fprintf (dump_file,
2600 "red equation#%d is dead "
2601 "(%d dead so far, %d remain)\n",
2602 e3, dead_count,
2603 pb->num_geqs - dead_count);
2604 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2605 fprintf (dump_file, "\n");
2606 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2607 fprintf (dump_file, "\n");
2608 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2609 fprintf (dump_file, "\n");
2610 }
2611 is_dead[e3] = true;
2612 }
2613 }
2614 }
2615 }
2616
2617 for (e = pb->num_geqs - 1; e >= 0; e--)
2618 if (is_dead[e])
2619 omega_delete_geq (pb, e, pb->num_vars);
2620
2621 free (is_dead);
2622
2623 if (dump_file && (dump_flags & TDF_DETAILS))
2624 {
2625 fprintf (dump_file, "in eliminate RED, easy tests done:\n");
2626 omega_print_problem (dump_file, pb);
2627 }
2628
2629 for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
2630 if (pb->geqs[e].color == omega_red)
2631 red_found = 1;
2632
2633 if (!red_found)
2634 {
2635 if (dump_file && (dump_flags & TDF_DETAILS))
2636 fprintf (dump_file, "fast checks worked\n");
2637
2638 if (!omega_reduce_with_subs)
2639 gcc_assert (please_no_equalities_in_simplified_problems
2640 || pb->num_subs == 0);
2641
2642 return;
2643 }
2644
2645 if (!omega_verify_simplification
2646 && verify_omega_pb (pb) == omega_false)
2647 return;
2648
2649 conservative++;
2650 tmp_problem = XNEW (struct omega_pb_d);
2651
2652 for (e = pb->num_geqs - 1; e >= 0; e--)
2653 if (pb->geqs[e].color == omega_red)
2654 {
2655 if (dump_file && (dump_flags & TDF_DETAILS))
2656 {
2657 fprintf (dump_file,
2658 "checking equation %d to see if it is redundant: ", e);
2659 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2660 fprintf (dump_file, "\n");
2661 }
2662
2663 omega_copy_problem (tmp_problem, pb);
2664 omega_negate_geq (tmp_problem, e);
2665 tmp_problem->safe_vars = 0;
2666 tmp_problem->variables_freed = false;
2667 tmp_problem->num_subs = 0;
2668
2669 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2670 {
2671 if (dump_file && (dump_flags & TDF_DETAILS))
2672 fprintf (dump_file, "it is redundant\n");
2673 omega_delete_geq (pb, e, pb->num_vars);
2674 }
2675 else
2676 {
2677 if (dump_file && (dump_flags & TDF_DETAILS))
2678 fprintf (dump_file, "it is not redundant\n");
2679
2680 if (!eliminate_all)
2681 {
2682 if (dump_file && (dump_flags & TDF_DETAILS))
2683 fprintf (dump_file, "no need to check other red equations\n");
2684 break;
2685 }
2686 }
2687 }
2688
2689 conservative--;
2690 free (tmp_problem);
2691 /* omega_simplify_problem (pb); */
2692
2693 if (!omega_reduce_with_subs)
2694 gcc_assert (please_no_equalities_in_simplified_problems
2695 || pb->num_subs == 0);
2696 }
2697
2698 /* Transform some wildcard variables to non-safe variables. */
2699
2700 static void
2701 chain_unprotect (omega_pb pb)
2702 {
2703 int i, e;
2704 bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
2705
2706 for (i = 1; omega_safe_var_p (pb, i); i++)
2707 {
2708 unprotect[i] = omega_wildcard_p (pb, i);
2709
2710 for (e = pb->num_subs - 1; e >= 0; e--)
2711 if (pb->subs[e].coef[i])
2712 unprotect[i] = false;
2713 }
2714
2715 if (dump_file && (dump_flags & TDF_DETAILS))
2716 {
2717 fprintf (dump_file, "Doing chain reaction unprotection\n");
2718 omega_print_problem (dump_file, pb);
2719
2720 for (i = 1; omega_safe_var_p (pb, i); i++)
2721 if (unprotect[i])
2722 fprintf (dump_file, "unprotecting %s\n",
2723 omega_variable_to_str (pb, i));
2724 }
2725
2726 for (i = 1; omega_safe_var_p (pb, i); i++)
2727 if (unprotect[i])
2728 omega_unprotect_1 (pb, &i, unprotect);
2729
2730 if (dump_file && (dump_flags & TDF_DETAILS))
2731 {
2732 fprintf (dump_file, "After chain reactions\n");
2733 omega_print_problem (dump_file, pb);
2734 }
2735
2736 free (unprotect);
2737 }
2738
2739 /* Reduce problem PB. */
2740
2741 static void
2742 omega_problem_reduced (omega_pb pb)
2743 {
2744 if (omega_verify_simplification
2745 && !in_approximate_mode
2746 && verify_omega_pb (pb) == omega_false)
2747 return;
2748
2749 if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
2750 && !omega_eliminate_redundant (pb, true))
2751 return;
2752
2753 omega_found_reduction = omega_true;
2754
2755 if (!please_no_equalities_in_simplified_problems)
2756 coalesce (pb);
2757
2758 if (omega_reduce_with_subs
2759 || please_no_equalities_in_simplified_problems)
2760 chain_unprotect (pb);
2761 else
2762 resurrect_subs (pb);
2763
2764 if (!return_single_result)
2765 {
2766 int i;
2767
2768 for (i = 1; omega_safe_var_p (pb, i); i++)
2769 pb->forwarding_address[pb->var[i]] = i;
2770
2771 for (i = 0; i < pb->num_subs; i++)
2772 pb->forwarding_address[pb->subs[i].key] = -i - 1;
2773
2774 (*omega_when_reduced) (pb);
2775 }
2776
2777 if (dump_file && (dump_flags & TDF_DETAILS))
2778 {
2779 fprintf (dump_file, "-------------------------------------------\n");
2780 fprintf (dump_file, "problem reduced:\n");
2781 omega_print_problem (dump_file, pb);
2782 fprintf (dump_file, "-------------------------------------------\n");
2783 }
2784 }
2785
2786 /* Eliminates all the free variables for problem PB, that is all the
2787 variables from FV to PB->NUM_VARS. */
2788
2789 static void
2790 omega_free_eliminations (omega_pb pb, int fv)
2791 {
2792 bool try_again = true;
2793 int i, e, e2;
2794 int n_vars = pb->num_vars;
2795
2796 while (try_again)
2797 {
2798 try_again = false;
2799
2800 for (i = n_vars; i > fv; i--)
2801 {
2802 for (e = pb->num_geqs - 1; e >= 0; e--)
2803 if (pb->geqs[e].coef[i])
2804 break;
2805
2806 if (e < 0)
2807 e2 = e;
2808 else if (pb->geqs[e].coef[i] > 0)
2809 {
2810 for (e2 = e - 1; e2 >= 0; e2--)
2811 if (pb->geqs[e2].coef[i] < 0)
2812 break;
2813 }
2814 else
2815 {
2816 for (e2 = e - 1; e2 >= 0; e2--)
2817 if (pb->geqs[e2].coef[i] > 0)
2818 break;
2819 }
2820
2821 if (e2 < 0)
2822 {
2823 int e3;
2824 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2825 if (pb->subs[e3].coef[i])
2826 break;
2827
2828 if (e3 >= 0)
2829 continue;
2830
2831 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2832 if (pb->eqs[e3].coef[i])
2833 break;
2834
2835 if (e3 >= 0)
2836 continue;
2837
2838 if (dump_file && (dump_flags & TDF_DETAILS))
2839 fprintf (dump_file, "a free elimination of %s\n",
2840 omega_variable_to_str (pb, i));
2841
2842 if (e >= 0)
2843 {
2844 omega_delete_geq (pb, e, n_vars);
2845
2846 for (e--; e >= 0; e--)
2847 if (pb->geqs[e].coef[i])
2848 omega_delete_geq (pb, e, n_vars);
2849
2850 try_again = (i < n_vars);
2851 }
2852
2853 omega_delete_variable (pb, i);
2854 n_vars = pb->num_vars;
2855 }
2856 }
2857 }
2858
2859 if (dump_file && (dump_flags & TDF_DETAILS))
2860 {
2861 fprintf (dump_file, "\nafter free eliminations:\n");
2862 omega_print_problem (dump_file, pb);
2863 fprintf (dump_file, "\n");
2864 }
2865 }
2866
2867 /* Do free red eliminations. */
2868
2869 static void
2870 free_red_eliminations (omega_pb pb)
2871 {
2872 bool try_again = true;
2873 int i, e, e2;
2874 int n_vars = pb->num_vars;
2875 bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2876 bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2877 bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS);
2878
2879 for (i = n_vars; i > 0; i--)
2880 {
2881 is_red_var[i] = false;
2882 is_dead_var[i] = false;
2883 }
2884
2885 for (e = pb->num_geqs - 1; e >= 0; e--)
2886 {
2887 is_dead_geq[e] = false;
2888
2889 if (pb->geqs[e].color == omega_red)
2890 for (i = n_vars; i > 0; i--)
2891 if (pb->geqs[e].coef[i] != 0)
2892 is_red_var[i] = true;
2893 }
2894
2895 while (try_again)
2896 {
2897 try_again = false;
2898 for (i = n_vars; i > 0; i--)
2899 if (!is_red_var[i] && !is_dead_var[i])
2900 {
2901 for (e = pb->num_geqs - 1; e >= 0; e--)
2902 if (!is_dead_geq[e] && pb->geqs[e].coef[i])
2903 break;
2904
2905 if (e < 0)
2906 e2 = e;
2907 else if (pb->geqs[e].coef[i] > 0)
2908 {
2909 for (e2 = e - 1; e2 >= 0; e2--)
2910 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
2911 break;
2912 }
2913 else
2914 {
2915 for (e2 = e - 1; e2 >= 0; e2--)
2916 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
2917 break;
2918 }
2919
2920 if (e2 < 0)
2921 {
2922 int e3;
2923 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2924 if (pb->subs[e3].coef[i])
2925 break;
2926
2927 if (e3 >= 0)
2928 continue;
2929
2930 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2931 if (pb->eqs[e3].coef[i])
2932 break;
2933
2934 if (e3 >= 0)
2935 continue;
2936
2937 if (dump_file && (dump_flags & TDF_DETAILS))
2938 fprintf (dump_file, "a free red elimination of %s\n",
2939 omega_variable_to_str (pb, i));
2940
2941 for (; e >= 0; e--)
2942 if (pb->geqs[e].coef[i])
2943 is_dead_geq[e] = true;
2944
2945 try_again = true;
2946 is_dead_var[i] = true;
2947 }
2948 }
2949 }
2950
2951 for (e = pb->num_geqs - 1; e >= 0; e--)
2952 if (is_dead_geq[e])
2953 omega_delete_geq (pb, e, n_vars);
2954
2955 for (i = n_vars; i > 0; i--)
2956 if (is_dead_var[i])
2957 omega_delete_variable (pb, i);
2958
2959 if (dump_file && (dump_flags & TDF_DETAILS))
2960 {
2961 fprintf (dump_file, "\nafter free red eliminations:\n");
2962 omega_print_problem (dump_file, pb);
2963 fprintf (dump_file, "\n");
2964 }
2965
2966 free (is_red_var);
2967 free (is_dead_var);
2968 free (is_dead_geq);
2969 }
2970
2971 /* For equation EQ of the form "0 = EQN", insert in PB two
2972 inequalities "0 <= EQN" and "0 <= -EQN". */
2973
2974 void
2975 omega_convert_eq_to_geqs (omega_pb pb, int eq)
2976 {
2977 int i;
2978
2979 if (dump_file && (dump_flags & TDF_DETAILS))
2980 fprintf (dump_file, "Converting Eq to Geqs\n");
2981
2982 /* Insert "0 <= EQN". */
2983 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2984 pb->geqs[pb->num_geqs].touched = 1;
2985 pb->num_geqs++;
2986
2987 /* Insert "0 <= -EQN". */
2988 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2989 pb->geqs[pb->num_geqs].touched = 1;
2990
2991 for (i = 0; i <= pb->num_vars; i++)
2992 pb->geqs[pb->num_geqs].coef[i] *= -1;
2993
2994 pb->num_geqs++;
2995
2996 if (dump_file && (dump_flags & TDF_DETAILS))
2997 omega_print_problem (dump_file, pb);
2998 }
2999
3000 /* Eliminates variable I from PB. */
3001
3002 static void
3003 omega_do_elimination (omega_pb pb, int e, int i)
3004 {
3005 eqn sub = omega_alloc_eqns (0, 1);
3006 int c;
3007 int n_vars = pb->num_vars;
3008
3009 if (dump_file && (dump_flags & TDF_DETAILS))
3010 fprintf (dump_file, "eliminating variable %s\n",
3011 omega_variable_to_str (pb, i));
3012
3013 omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars);
3014 c = sub->coef[i];
3015 sub->coef[i] = 0;
3016 if (c == 1 || c == -1)
3017 {
3018 if (pb->eqs[e].color == omega_red)
3019 {
3020 bool fB;
3021 omega_substitute_red (pb, sub, i, c, &fB);
3022 if (fB)
3023 omega_convert_eq_to_geqs (pb, e);
3024 else
3025 omega_delete_variable (pb, i);
3026 }
3027 else
3028 {
3029 omega_substitute (pb, sub, i, c);
3030 omega_delete_variable (pb, i);
3031 }
3032 }
3033 else
3034 {
3035 int a = abs (c);
3036 int e2 = e;
3037
3038 if (dump_file && (dump_flags & TDF_DETAILS))
3039 fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
3040
3041 for (e = pb->num_eqs - 1; e >= 0; e--)
3042 if (pb->eqs[e].coef[i])
3043 {
3044 eqn eqn = &(pb->eqs[e]);
3045 int j, k;
3046 for (j = n_vars; j >= 0; j--)
3047 eqn->coef[j] *= a;
3048 k = eqn->coef[i];
3049 eqn->coef[i] = 0;
3050 if (sub->color == omega_red)
3051 eqn->color = omega_red;
3052 for (j = n_vars; j >= 0; j--)
3053 eqn->coef[j] -= sub->coef[j] * k / c;
3054 }
3055
3056 for (e = pb->num_geqs - 1; e >= 0; e--)
3057 if (pb->geqs[e].coef[i])
3058 {
3059 eqn eqn = &(pb->geqs[e]);
3060 int j, k;
3061
3062 if (sub->color == omega_red)
3063 eqn->color = omega_red;
3064
3065 for (j = n_vars; j >= 0; j--)
3066 eqn->coef[j] *= a;
3067
3068 eqn->touched = 1;
3069 k = eqn->coef[i];
3070 eqn->coef[i] = 0;
3071
3072 for (j = n_vars; j >= 0; j--)
3073 eqn->coef[j] -= sub->coef[j] * k / c;
3074
3075 }
3076
3077 for (e = pb->num_subs - 1; e >= 0; e--)
3078 if (pb->subs[e].coef[i])
3079 {
3080 eqn eqn = &(pb->subs[e]);
3081 int j, k;
3082 gcc_assert (0);
3083 gcc_assert (sub->color == omega_black);
3084 for (j = n_vars; j >= 0; j--)
3085 eqn->coef[j] *= a;
3086 k = eqn->coef[i];
3087 eqn->coef[i] = 0;
3088 for (j = n_vars; j >= 0; j--)
3089 eqn->coef[j] -= sub->coef[j] * k / c;
3090 }
3091
3092 if (in_approximate_mode)
3093 omega_delete_variable (pb, i);
3094 else
3095 omega_convert_eq_to_geqs (pb, e2);
3096 }
3097
3098 omega_free_eqns (sub, 1);
3099 }
3100
3101 /* Helper function for printing "sorry, no solution". */
3102
3103 static inline enum omega_result
3104 omega_problem_has_no_solution (void)
3105 {
3106 if (dump_file && (dump_flags & TDF_DETAILS))
3107 fprintf (dump_file, "\nequations have no solution \n");
3108
3109 return omega_false;
3110 }
3111
3112 /* Helper function: solve equations in PB one at a time, following the
3113 DESIRED_RES result. */
3114
3115 static enum omega_result
3116 omega_solve_eq (omega_pb pb, enum omega_result desired_res)
3117 {
3118 int i, j, e;
3119 int g, g2;
3120 g = 0;
3121
3122
3123 if (dump_file && (dump_flags & TDF_DETAILS) && pb->num_eqs > 0)
3124 {
3125 fprintf (dump_file, "\nomega_solve_eq (%d, %d)\n",
3126 desired_res, may_be_red);
3127 omega_print_problem (dump_file, pb);
3128 fprintf (dump_file, "\n");
3129 }
3130
3131 if (may_be_red)
3132 {
3133 i = 0;
3134 j = pb->num_eqs - 1;
3135
3136 while (1)
3137 {
3138 eqn eq;
3139
3140 while (i <= j && pb->eqs[i].color == omega_red)
3141 i++;
3142
3143 while (i <= j && pb->eqs[j].color == omega_black)
3144 j--;
3145
3146 if (i >= j)
3147 break;
3148
3149 eq = omega_alloc_eqns (0, 1);
3150 omega_copy_eqn (eq, &pb->eqs[i], pb->num_vars);
3151 omega_copy_eqn (&pb->eqs[i], &pb->eqs[j], pb->num_vars);
3152 omega_copy_eqn (&pb->eqs[j], eq, pb->num_vars);
3153 omega_free_eqns (eq, 1);
3154 i++;
3155 j--;
3156 }
3157 }
3158
3159 /* Eliminate all EQ equations */
3160 for (e = pb->num_eqs - 1; e >= 0; e--)
3161 {
3162 eqn eqn = &(pb->eqs[e]);
3163 int sv;
3164
3165 if (dump_file && (dump_flags & TDF_DETAILS))
3166 fprintf (dump_file, "----\n");
3167
3168 for (i = pb->num_vars; i > 0; i--)
3169 if (eqn->coef[i])
3170 break;
3171
3172 g = eqn->coef[i];
3173
3174 for (j = i - 1; j > 0; j--)
3175 if (eqn->coef[j])
3176 break;
3177
3178 /* i is the position of last nonzero coefficient,
3179 g is the coefficient of i,
3180 j is the position of next nonzero coefficient. */
3181
3182 if (j == 0)
3183 {
3184 if (eqn->coef[0] % g != 0)
3185 return omega_problem_has_no_solution ();
3186
3187 eqn->coef[0] = eqn->coef[0] / g;
3188 eqn->coef[i] = 1;
3189 pb->num_eqs--;
3190 omega_do_elimination (pb, e, i);
3191 continue;
3192 }
3193
3194 else if (j == -1)
3195 {
3196 if (eqn->coef[0] != 0)
3197 return omega_problem_has_no_solution ();
3198
3199 pb->num_eqs--;
3200 continue;
3201 }
3202
3203 if (g < 0)
3204 g = -g;
3205
3206 if (g == 1)
3207 {
3208 pb->num_eqs--;
3209 omega_do_elimination (pb, e, i);
3210 }
3211
3212 else
3213 {
3214 int k = j;
3215 bool promotion_possible =
3216 (omega_safe_var_p (pb, j)
3217 && pb->safe_vars + 1 == i
3218 && !omega_eqn_is_red (eqn, desired_res)
3219 && !in_approximate_mode);
3220
3221 if (dump_file && (dump_flags & TDF_DETAILS) && promotion_possible)
3222 fprintf (dump_file, " Promotion possible\n");
3223
3224 normalizeEQ:
3225 if (!omega_safe_var_p (pb, j))
3226 {
3227 for (; g != 1 && !omega_safe_var_p (pb, j); j--)
3228 g = gcd (abs (eqn->coef[j]), g);
3229 g2 = g;
3230 }
3231 else if (!omega_safe_var_p (pb, i))
3232 g2 = g;
3233 else
3234 g2 = 0;
3235
3236 for (; g != 1 && j > 0; j--)
3237 g = gcd (abs (eqn->coef[j]), g);
3238
3239 if (g > 1)
3240 {
3241 if (eqn->coef[0] % g != 0)
3242 return omega_problem_has_no_solution ();
3243
3244 for (j = 0; j <= pb->num_vars; j++)
3245 eqn->coef[j] /= g;
3246
3247 g2 = g2 / g;
3248 }
3249
3250 if (g2 > 1)
3251 {
3252 int e2;
3253
3254 for (e2 = e - 1; e2 >= 0; e2--)
3255 if (pb->eqs[e2].coef[i])
3256 break;
3257
3258 if (e2 == -1)
3259 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
3260 if (pb->geqs[e2].coef[i])
3261 break;
3262
3263 if (e2 == -1)
3264 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
3265 if (pb->subs[e2].coef[i])
3266 break;
3267
3268 if (e2 == -1)
3269 {
3270 bool change = false;
3271
3272 if (dump_file && (dump_flags & TDF_DETAILS))
3273 {
3274 fprintf (dump_file, "Ha! We own it! \n");
3275 omega_print_eq (dump_file, pb, eqn);
3276 fprintf (dump_file, " \n");
3277 }
3278
3279 g = eqn->coef[i];
3280 g = abs (g);
3281
3282 for (j = i - 1; j >= 0; j--)
3283 {
3284 int t = int_mod (eqn->coef[j], g);
3285
3286 if (2 * t >= g)
3287 t -= g;
3288
3289 if (t != eqn->coef[j])
3290 {
3291 eqn->coef[j] = t;
3292 change = true;
3293 }
3294 }
3295
3296 if (!change)
3297 {
3298 if (dump_file && (dump_flags & TDF_DETAILS))
3299 fprintf (dump_file, "So what?\n");
3300 }
3301
3302 else
3303 {
3304 omega_name_wild_card (pb, i);
3305
3306 if (dump_file && (dump_flags & TDF_DETAILS))
3307 {
3308 omega_print_eq (dump_file, pb, eqn);
3309 fprintf (dump_file, " \n");
3310 }
3311
3312 e++;
3313 continue;
3314 }
3315 }
3316 }
3317
3318 if (promotion_possible)
3319 {
3320 if (dump_file && (dump_flags & TDF_DETAILS))
3321 {
3322 fprintf (dump_file, "promoting %s to safety\n",
3323 omega_variable_to_str (pb, i));
3324 omega_print_vars (dump_file, pb);
3325 }
3326
3327 pb->safe_vars++;
3328
3329 if (!omega_wildcard_p (pb, i))
3330 omega_name_wild_card (pb, i);
3331
3332 promotion_possible = false;
3333 j = k;
3334 goto normalizeEQ;
3335 }
3336
3337 if (g2 > 1 && !in_approximate_mode)
3338 {
3339 if (pb->eqs[e].color == omega_red)
3340 {
3341 if (dump_file && (dump_flags & TDF_DETAILS))
3342 fprintf (dump_file, "handling red equality\n");
3343
3344 pb->num_eqs--;
3345 omega_do_elimination (pb, e, i);
3346 continue;
3347 }
3348
3349 if (dump_file && (dump_flags & TDF_DETAILS))
3350 {
3351 fprintf (dump_file,
3352 "adding equation to handle safe variable \n");
3353 omega_print_eq (dump_file, pb, eqn);
3354 fprintf (dump_file, "\n----\n");
3355 omega_print_problem (dump_file, pb);
3356 fprintf (dump_file, "\n----\n");
3357 fprintf (dump_file, "\n----\n");
3358 }
3359
3360 i = omega_add_new_wild_card (pb);
3361 pb->num_eqs++;
3362 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
3363 omega_init_eqn_zero (&pb->eqs[e + 1], pb->num_vars);
3364 omega_copy_eqn (&pb->eqs[e + 1], eqn, pb->safe_vars);
3365
3366 for (j = pb->num_vars; j >= 0; j--)
3367 {
3368 pb->eqs[e + 1].coef[j] = int_mod (pb->eqs[e + 1].coef[j], g2);
3369
3370 if (2 * pb->eqs[e + 1].coef[j] >= g2)
3371 pb->eqs[e + 1].coef[j] -= g2;
3372 }
3373
3374 pb->eqs[e + 1].coef[i] = g2;
3375 e += 2;
3376
3377 if (dump_file && (dump_flags & TDF_DETAILS))
3378 omega_print_problem (dump_file, pb);
3379
3380 continue;
3381 }
3382
3383 sv = pb->safe_vars;
3384 if (g2 == 0)
3385 sv = 0;
3386
3387 /* Find variable to eliminate. */
3388 if (g2 > 1)
3389 {
3390 gcc_assert (in_approximate_mode);
3391
3392 if (dump_file && (dump_flags & TDF_DETAILS))
3393 {
3394 fprintf (dump_file, "non-exact elimination: ");
3395 omega_print_eq (dump_file, pb, eqn);
3396 fprintf (dump_file, "\n");
3397 omega_print_problem (dump_file, pb);
3398 }
3399
3400 for (i = pb->num_vars; i > sv; i--)
3401 if (pb->eqs[e].coef[i] != 0)
3402 break;
3403 }
3404 else
3405 for (i = pb->num_vars; i > sv; i--)
3406 if (pb->eqs[e].coef[i] == 1 || pb->eqs[e].coef[i] == -1)
3407 break;
3408
3409 if (i > sv)
3410 {
3411 pb->num_eqs--;
3412 omega_do_elimination (pb, e, i);
3413
3414 if (dump_file && (dump_flags & TDF_DETAILS) && g2 > 1)
3415 {
3416 fprintf (dump_file, "result of non-exact elimination:\n");
3417 omega_print_problem (dump_file, pb);
3418 }
3419 }
3420 else
3421 {
3422 int factor = (INT_MAX);
3423 j = 0;
3424
3425 if (dump_file && (dump_flags & TDF_DETAILS))
3426 fprintf (dump_file, "doing moding\n");
3427
3428 for (i = pb->num_vars; i != sv; i--)
3429 if ((pb->eqs[e].coef[i] & 1) != 0)
3430 {
3431 j = i;
3432 i--;
3433
3434 for (; i != sv; i--)
3435 if ((pb->eqs[e].coef[i] & 1) != 0)
3436 break;
3437
3438 break;
3439 }
3440
3441 if (j != 0 && i == sv)
3442 {
3443 omega_do_mod (pb, 2, e, j);
3444 e++;
3445 continue;
3446 }
3447
3448 j = 0;
3449 for (i = pb->num_vars; i != sv; i--)
3450 if (pb->eqs[e].coef[i] != 0
3451 && factor > abs (pb->eqs[e].coef[i]) + 1)
3452 {
3453 factor = abs (pb->eqs[e].coef[i]) + 1;
3454 j = i;
3455 }
3456
3457 if (j == sv)
3458 {
3459 if (dump_file && (dump_flags & TDF_DETAILS))
3460 fprintf (dump_file, "should not have happened\n");
3461 gcc_assert (0);
3462 }
3463
3464 omega_do_mod (pb, factor, e, j);
3465 /* Go back and try this equation again. */
3466 e++;
3467 }
3468 }
3469 }
3470
3471 pb->num_eqs = 0;
3472 return omega_unknown;
3473 }
3474
3475 /* Transform an inequation E to an equality, then solve DIFF problems
3476 based on PB, and only differing by the constant part that is
3477 diminished by one, trying to figure out which of the constants
3478 satisfies PB. */
3479
3480 static enum omega_result
3481 parallel_splinter (omega_pb pb, int e, int diff,
3482 enum omega_result desired_res)
3483 {
3484 omega_pb tmp_problem;
3485 int i;
3486
3487 if (dump_file && (dump_flags & TDF_DETAILS))
3488 {
3489 fprintf (dump_file, "Using parallel splintering\n");
3490 omega_print_problem (dump_file, pb);
3491 }
3492
3493 tmp_problem = XNEW (struct omega_pb_d);
3494 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e], pb->num_vars);
3495 pb->num_eqs = 1;
3496
3497 for (i = 0; i <= diff; i++)
3498 {
3499 omega_copy_problem (tmp_problem, pb);
3500
3501 if (dump_file && (dump_flags & TDF_DETAILS))
3502 {
3503 fprintf (dump_file, "Splinter # %i\n", i);
3504 omega_print_problem (dump_file, pb);
3505 }
3506
3507 if (omega_solve_problem (tmp_problem, desired_res) == omega_true)
3508 {
3509 free (tmp_problem);
3510 return omega_true;
3511 }
3512
3513 pb->eqs[0].coef[0]--;
3514 }
3515
3516 free (tmp_problem);
3517 return omega_false;
3518 }
3519
3520 /* Helper function: solve equations one at a time. */
3521
3522 static enum omega_result
3523 omega_solve_geq (omega_pb pb, enum omega_result desired_res)
3524 {
3525 int i, e;
3526 int n_vars, fv;
3527 enum omega_result result;
3528 bool coupled_subscripts = false;
3529 bool smoothed = false;
3530 bool eliminate_again;
3531 bool tried_eliminating_redundant = false;
3532
3533 if (desired_res != omega_simplify)
3534 {
3535 pb->num_subs = 0;
3536 pb->safe_vars = 0;
3537 }
3538
3539 solve_geq_start:
3540 do {
3541 gcc_assert (desired_res == omega_simplify || pb->num_subs == 0);
3542
3543 /* Verify that there are not too many inequalities. */
3544 gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
3545
3546 if (dump_file && (dump_flags & TDF_DETAILS))
3547 {
3548 fprintf (dump_file, "\nomega_solve_geq (%d,%d):\n",
3549 desired_res, please_no_equalities_in_simplified_problems);
3550 omega_print_problem (dump_file, pb);
3551 fprintf (dump_file, "\n");
3552 }
3553
3554 n_vars = pb->num_vars;
3555
3556 if (n_vars == 1)
3557 {
3558 enum omega_eqn_color u_color = omega_black;
3559 enum omega_eqn_color l_color = omega_black;
3560 int upper_bound = pos_infinity;
3561 int lower_bound = neg_infinity;
3562
3563 for (e = pb->num_geqs - 1; e >= 0; e--)
3564 {
3565 int a = pb->geqs[e].coef[1];
3566 int c = pb->geqs[e].coef[0];
3567
3568 /* Our equation is ax + c >= 0, or ax >= -c, or c >= -ax. */
3569 if (a == 0)
3570 {
3571 if (c < 0)
3572 return omega_problem_has_no_solution ();
3573 }
3574 else if (a > 0)
3575 {
3576 if (a != 1)
3577 c = int_div (c, a);
3578
3579 if (lower_bound < -c
3580 || (lower_bound == -c
3581 && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3582 {
3583 lower_bound = -c;
3584 l_color = pb->geqs[e].color;
3585 }
3586 }
3587 else
3588 {
3589 if (a != -1)
3590 c = int_div (c, -a);
3591
3592 if (upper_bound > c
3593 || (upper_bound == c
3594 && !omega_eqn_is_red (&pb->geqs[e], desired_res)))
3595 {
3596 upper_bound = c;
3597 u_color = pb->geqs[e].color;
3598 }
3599 }
3600 }
3601
3602 if (dump_file && (dump_flags & TDF_DETAILS))
3603 {
3604 fprintf (dump_file, "upper bound = %d\n", upper_bound);
3605 fprintf (dump_file, "lower bound = %d\n", lower_bound);
3606 }
3607
3608 if (lower_bound > upper_bound)
3609 return omega_problem_has_no_solution ();
3610
3611 if (desired_res == omega_simplify)
3612 {
3613 pb->num_geqs = 0;
3614 if (pb->safe_vars == 1)
3615 {
3616
3617 if (lower_bound == upper_bound
3618 && u_color == omega_black
3619 && l_color == omega_black)
3620 {
3621 pb->eqs[0].coef[0] = -lower_bound;
3622 pb->eqs[0].coef[1] = 1;
3623 pb->eqs[0].color = omega_black;
3624 pb->num_eqs = 1;
3625 return omega_solve_problem (pb, desired_res);
3626 }
3627 else
3628 {
3629 if (lower_bound > neg_infinity)
3630 {
3631 pb->geqs[0].coef[0] = -lower_bound;
3632 pb->geqs[0].coef[1] = 1;
3633 pb->geqs[0].key = 1;
3634 pb->geqs[0].color = l_color;
3635 pb->geqs[0].touched = 0;
3636 pb->num_geqs = 1;
3637 }
3638
3639 if (upper_bound < pos_infinity)
3640 {
3641 pb->geqs[pb->num_geqs].coef[0] = upper_bound;
3642 pb->geqs[pb->num_geqs].coef[1] = -1;
3643 pb->geqs[pb->num_geqs].key = -1;
3644 pb->geqs[pb->num_geqs].color = u_color;
3645 pb->geqs[pb->num_geqs].touched = 0;
3646 pb->num_geqs++;
3647 }
3648 }
3649 }
3650 else
3651 pb->num_vars = 0;
3652
3653 omega_problem_reduced (pb);
3654 return omega_false;
3655 }
3656
3657 if (original_problem != no_problem
3658 && l_color == omega_black
3659 && u_color == omega_black
3660 && !conservative
3661 && lower_bound == upper_bound)
3662 {
3663 pb->eqs[0].coef[0] = -lower_bound;
3664 pb->eqs[0].coef[1] = 1;
3665 pb->num_eqs = 1;
3666 adding_equality_constraint (pb, 0);
3667 }
3668
3669 return omega_true;
3670 }
3671
3672 if (!pb->variables_freed)
3673 {
3674 pb->variables_freed = true;
3675
3676 if (desired_res != omega_simplify)
3677 omega_free_eliminations (pb, 0);
3678 else
3679 omega_free_eliminations (pb, pb->safe_vars);
3680
3681 n_vars = pb->num_vars;
3682
3683 if (n_vars == 1)
3684 continue;
3685 }
3686
3687 switch (normalize_omega_problem (pb))
3688 {
3689 case normalize_false:
3690 return omega_false;
3691 break;
3692
3693 case normalize_coupled:
3694 coupled_subscripts = true;
3695 break;
3696
3697 case normalize_uncoupled:
3698 coupled_subscripts = false;
3699 break;
3700
3701 default:
3702 gcc_unreachable ();
3703 }
3704
3705 n_vars = pb->num_vars;
3706
3707 if (dump_file && (dump_flags & TDF_DETAILS))
3708 {
3709 fprintf (dump_file, "\nafter normalization:\n");
3710 omega_print_problem (dump_file, pb);
3711 fprintf (dump_file, "\n");
3712 fprintf (dump_file, "eliminating variable using Fourier-Motzkin.\n");
3713 }
3714
3715 do {
3716 int parallel_difference = INT_MAX;
3717 int best_parallel_eqn = -1;
3718 int minC, maxC, minCj = 0;
3719 int lower_bound_count = 0;
3720 int e2, Le = 0, Ue;
3721 bool possible_easy_int_solution;
3722 int max_splinters = 1;
3723 bool exact = false;
3724 bool lucky_exact = false;
3725 int best = (INT_MAX);
3726 int j = 0, jLe = 0, jLowerBoundCount = 0;
3727
3728
3729 eliminate_again = false;
3730
3731 if (pb->num_eqs > 0)
3732 return omega_solve_problem (pb, desired_res);
3733
3734 if (!coupled_subscripts)
3735 {
3736 if (pb->safe_vars == 0)
3737 pb->num_geqs = 0;
3738 else
3739 for (e = pb->num_geqs - 1; e >= 0; e--)
3740 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
3741 omega_delete_geq (pb, e, n_vars);
3742
3743 pb->num_vars = pb->safe_vars;
3744
3745 if (desired_res == omega_simplify)
3746 {
3747 omega_problem_reduced (pb);
3748 return omega_false;
3749 }
3750
3751 return omega_true;
3752 }
3753
3754 if (desired_res != omega_simplify)
3755 fv = 0;
3756 else
3757 fv = pb->safe_vars;
3758
3759 if (pb->num_geqs == 0)
3760 {
3761 if (desired_res == omega_simplify)
3762 {
3763 pb->num_vars = pb->safe_vars;
3764 omega_problem_reduced (pb);
3765 return omega_false;
3766 }
3767 return omega_true;
3768 }
3769
3770 if (desired_res == omega_simplify && n_vars == pb->safe_vars)
3771 {
3772 omega_problem_reduced (pb);
3773 return omega_false;
3774 }
3775
3776 if (pb->num_geqs > OMEGA_MAX_GEQS - 30
3777 || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10)
3778 {
3779 if (dump_file && (dump_flags & TDF_DETAILS))
3780 fprintf (dump_file,
3781 "TOO MANY EQUATIONS; "
3782 "%d equations, %d variables, "
3783 "ELIMINATING REDUNDANT ONES\n",
3784 pb->num_geqs, n_vars);
3785
3786 if (!omega_eliminate_redundant (pb, false))
3787 return omega_false;
3788
3789 n_vars = pb->num_vars;
3790
3791 if (pb->num_eqs > 0)
3792 return omega_solve_problem (pb, desired_res);
3793
3794 if (dump_file && (dump_flags & TDF_DETAILS))
3795 fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3796 }
3797
3798 if (desired_res != omega_simplify)
3799 fv = 0;
3800 else
3801 fv = pb->safe_vars;
3802
3803 for (i = n_vars; i != fv; i--)
3804 {
3805 int score;
3806 int ub = -2;
3807 int lb = -2;
3808 bool lucky = false;
3809 int upper_bound_count = 0;
3810
3811 lower_bound_count = 0;
3812 minC = maxC = 0;
3813
3814 for (e = pb->num_geqs - 1; e >= 0; e--)
3815 if (pb->geqs[e].coef[i] < 0)
3816 {
3817 minC = MIN (minC, pb->geqs[e].coef[i]);
3818 upper_bound_count++;
3819 if (pb->geqs[e].coef[i] < -1)
3820 {
3821 if (ub == -2)
3822 ub = e;
3823 else
3824 ub = -1;
3825 }
3826 }
3827 else if (pb->geqs[e].coef[i] > 0)
3828 {
3829 maxC = MAX (maxC, pb->geqs[e].coef[i]);
3830 lower_bound_count++;
3831 Le = e;
3832 if (pb->geqs[e].coef[i] > 1)
3833 {
3834 if (lb == -2)
3835 lb = e;
3836 else
3837 lb = -1;
3838 }
3839 }
3840
3841 if (lower_bound_count == 0
3842 || upper_bound_count == 0)
3843 {
3844 lower_bound_count = 0;
3845 break;
3846 }
3847
3848 if (ub >= 0 && lb >= 0
3849 && pb->geqs[lb].key == -pb->geqs[ub].key)
3850 {
3851 int Lc = pb->geqs[lb].coef[i];
3852 int Uc = -pb->geqs[ub].coef[i];
3853 int diff =
3854 Lc * pb->geqs[ub].coef[0] + Uc * pb->geqs[lb].coef[0];
3855 lucky = (diff >= (Uc - 1) * (Lc - 1));
3856 }
3857
3858 if (maxC == 1
3859 || minC == -1
3860 || lucky
3861 || in_approximate_mode)
3862 {
3863 score = upper_bound_count * lower_bound_count;
3864
3865 if (dump_file && (dump_flags & TDF_DETAILS))
3866 fprintf (dump_file,
3867 "For %s, exact, score = %d*%d, range = %d ... %d,"
3868 "\nlucky = %d, in_approximate_mode=%d \n",
3869 omega_variable_to_str (pb, i),
3870 upper_bound_count,
3871 lower_bound_count, minC, maxC, lucky,
3872 in_approximate_mode);
3873
3874 if (!exact
3875 || score < best)
3876 {
3877
3878 best = score;
3879 j = i;
3880 minCj = minC;
3881 jLe = Le;
3882 jLowerBoundCount = lower_bound_count;
3883 exact = true;
3884 lucky_exact = lucky;
3885 if (score == 1)
3886 break;
3887 }
3888 }
3889 else if (!exact)
3890 {
3891 if (dump_file && (dump_flags & TDF_DETAILS))
3892 fprintf (dump_file,
3893 "For %s, non-exact, score = %d*%d,"
3894 "range = %d ... %d \n",
3895 omega_variable_to_str (pb, i),
3896 upper_bound_count,
3897 lower_bound_count, minC, maxC);
3898
3899 score = maxC - minC;
3900
3901 if (best > score)
3902 {
3903 best = score;
3904 j = i;
3905 minCj = minC;
3906 jLe = Le;
3907 jLowerBoundCount = lower_bound_count;
3908 }
3909 }
3910 }
3911
3912 if (lower_bound_count == 0)
3913 {
3914 omega_free_eliminations (pb, pb->safe_vars);
3915 n_vars = pb->num_vars;
3916 eliminate_again = true;
3917 continue;
3918 }
3919
3920 i = j;
3921 minC = minCj;
3922 Le = jLe;
3923 lower_bound_count = jLowerBoundCount;
3924
3925 for (e = pb->num_geqs - 1; e >= 0; e--)
3926 if (pb->geqs[e].coef[i] > 0)
3927 {
3928 if (pb->geqs[e].coef[i] == -minC)
3929 max_splinters += -minC - 1;
3930 else
3931 max_splinters +=
3932 check_pos_mul ((pb->geqs[e].coef[i] - 1),
3933 (-minC - 1)) / (-minC) + 1;
3934 }
3935
3936 /* #ifdef Omega3 */
3937 /* Trying to produce exact elimination by finding redundant
3938 constraints. */
3939 if (!exact && !tried_eliminating_redundant)
3940 {
3941 omega_eliminate_redundant (pb, false);
3942 tried_eliminating_redundant = true;
3943 eliminate_again = true;
3944 continue;
3945 }
3946 tried_eliminating_redundant = false;
3947 /* #endif */
3948
3949 if (return_single_result && desired_res == omega_simplify && !exact)
3950 {
3951 omega_problem_reduced (pb);
3952 return omega_true;
3953 }
3954
3955 /* #ifndef Omega3 */
3956 /* Trying to produce exact elimination by finding redundant
3957 constraints. */
3958 if (!exact && !tried_eliminating_redundant)
3959 {
3960 omega_eliminate_redundant (pb, false);
3961 tried_eliminating_redundant = true;
3962 continue;
3963 }
3964 tried_eliminating_redundant = false;
3965 /* #endif */
3966
3967 if (!exact)
3968 {
3969 int e1, e2;
3970
3971 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
3972 if (pb->geqs[e1].color == omega_black)
3973 for (e2 = e1 - 1; e2 >= 0; e2--)
3974 if (pb->geqs[e2].color == omega_black
3975 && pb->geqs[e1].key == -pb->geqs[e2].key
3976 && ((pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3977 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3978 / 2 < parallel_difference))
3979 {
3980 parallel_difference =
3981 (pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3982 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3983 / 2;
3984 best_parallel_eqn = e1;
3985 }
3986
3987 if (dump_file && (dump_flags & TDF_DETAILS)
3988 && best_parallel_eqn >= 0)
3989 {
3990 fprintf (dump_file,
3991 "Possible parallel projection, diff = %d, in ",
3992 parallel_difference);
3993 omega_print_geq (dump_file, pb, &(pb->geqs[best_parallel_eqn]));
3994 fprintf (dump_file, "\n");
3995 omega_print_problem (dump_file, pb);
3996 }
3997 }
3998
3999 if (dump_file && (dump_flags & TDF_DETAILS))
4000 {
4001 fprintf (dump_file, "going to eliminate %s, (%d,%d,%d)\n",
4002 omega_variable_to_str (pb, i), i, minC,
4003 lower_bound_count);
4004 omega_print_problem (dump_file, pb);
4005
4006 if (lucky_exact)
4007 fprintf (dump_file, "(a lucky exact elimination)\n");
4008
4009 else if (exact)
4010 fprintf (dump_file, "(an exact elimination)\n");
4011
4012 fprintf (dump_file, "Max # of splinters = %d\n", max_splinters);
4013 }
4014
4015 gcc_assert (max_splinters >= 1);
4016
4017 if (!exact && desired_res == omega_simplify && best_parallel_eqn >= 0
4018 && parallel_difference <= max_splinters)
4019 return parallel_splinter (pb, best_parallel_eqn, parallel_difference,
4020 desired_res);
4021
4022 smoothed = false;
4023
4024 if (i != n_vars)
4025 {
4026 int t;
4027 int j = pb->num_vars;
4028
4029 if (dump_file && (dump_flags & TDF_DETAILS))
4030 {
4031 fprintf (dump_file, "Swapping %d and %d\n", i, j);
4032 omega_print_problem (dump_file, pb);
4033 }
4034
4035 swap (&pb->var[i], &pb->var[j]);
4036
4037 for (e = pb->num_geqs - 1; e >= 0; e--)
4038 if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
4039 {
4040 pb->geqs[e].touched = 1;
4041 t = pb->geqs[e].coef[i];
4042 pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
4043 pb->geqs[e].coef[j] = t;
4044 }
4045
4046 for (e = pb->num_subs - 1; e >= 0; e--)
4047 if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
4048 {
4049 t = pb->subs[e].coef[i];
4050 pb->subs[e].coef[i] = pb->subs[e].coef[j];
4051 pb->subs[e].coef[j] = t;
4052 }
4053
4054 if (dump_file && (dump_flags & TDF_DETAILS))
4055 {
4056 fprintf (dump_file, "Swapping complete \n");
4057 omega_print_problem (dump_file, pb);
4058 fprintf (dump_file, "\n");
4059 }
4060
4061 i = j;
4062 }
4063
4064 else if (dump_file && (dump_flags & TDF_DETAILS))
4065 {
4066 fprintf (dump_file, "No swap needed\n");
4067 omega_print_problem (dump_file, pb);
4068 }
4069
4070 pb->num_vars--;
4071 n_vars = pb->num_vars;
4072
4073 if (exact)
4074 {
4075 if (n_vars == 1)
4076 {
4077 int upper_bound = pos_infinity;
4078 int lower_bound = neg_infinity;
4079 enum omega_eqn_color ub_color = omega_black;
4080 enum omega_eqn_color lb_color = omega_black;
4081 int topeqn = pb->num_geqs - 1;
4082 int Lc = pb->geqs[Le].coef[i];
4083
4084 for (Le = topeqn; Le >= 0; Le--)
4085 if ((Lc = pb->geqs[Le].coef[i]) == 0)
4086 {
4087 if (pb->geqs[Le].coef[1] == 1)
4088 {
4089 int constantTerm = -pb->geqs[Le].coef[0];
4090
4091 if (constantTerm > lower_bound ||
4092 (constantTerm == lower_bound &&
4093 !omega_eqn_is_red (&pb->geqs[Le], desired_res)))
4094 {
4095 lower_bound = constantTerm;
4096 lb_color = pb->geqs[Le].color;
4097 }
4098
4099 if (dump_file && (dump_flags & TDF_DETAILS))
4100 {
4101 if (pb->geqs[Le].color == omega_black)
4102 fprintf (dump_file, " :::=> %s >= %d\n",
4103 omega_variable_to_str (pb, 1),
4104 constantTerm);
4105 else
4106 fprintf (dump_file,
4107 " :::=> [%s >= %d]\n",
4108 omega_variable_to_str (pb, 1),
4109 constantTerm);
4110 }
4111 }
4112 else
4113 {
4114 int constantTerm = pb->geqs[Le].coef[0];
4115 if (constantTerm < upper_bound ||
4116 (constantTerm == upper_bound
4117 && !omega_eqn_is_red (&pb->geqs[Le],
4118 desired_res)))
4119 {
4120 upper_bound = constantTerm;
4121 ub_color = pb->geqs[Le].color;
4122 }
4123
4124 if (dump_file && (dump_flags & TDF_DETAILS))
4125 {
4126 if (pb->geqs[Le].color == omega_black)
4127 fprintf (dump_file, " :::=> %s <= %d\n",
4128 omega_variable_to_str (pb, 1),
4129 constantTerm);
4130 else
4131 fprintf (dump_file,
4132 " :::=> [%s <= %d]\n",
4133 omega_variable_to_str (pb, 1),
4134 constantTerm);
4135 }
4136 }
4137 }
4138 else if (Lc > 0)
4139 for (Ue = topeqn; Ue >= 0; Ue--)
4140 if (pb->geqs[Ue].coef[i] < 0
4141 && pb->geqs[Le].key != -pb->geqs[Ue].key)
4142 {
4143 int Uc = -pb->geqs[Ue].coef[i];
4144 int coefficient = pb->geqs[Ue].coef[1] * Lc
4145 + pb->geqs[Le].coef[1] * Uc;
4146 int constantTerm = pb->geqs[Ue].coef[0] * Lc
4147 + pb->geqs[Le].coef[0] * Uc;
4148
4149 if (dump_file && (dump_flags & TDF_DETAILS))
4150 {
4151 omega_print_geq_extra (dump_file, pb,
4152 &(pb->geqs[Ue]));
4153 fprintf (dump_file, "\n");
4154 omega_print_geq_extra (dump_file, pb,
4155 &(pb->geqs[Le]));
4156 fprintf (dump_file, "\n");
4157 }
4158
4159 if (coefficient > 0)
4160 {
4161 constantTerm = -int_div (constantTerm, coefficient);
4162
4163 if (constantTerm > lower_bound
4164 || (constantTerm == lower_bound
4165 && (desired_res != omega_simplify
4166 || (pb->geqs[Ue].color == omega_black
4167 && pb->geqs[Le].color == omega_black))))
4168 {
4169 lower_bound = constantTerm;
4170 lb_color = (pb->geqs[Ue].color == omega_red
4171 || pb->geqs[Le].color == omega_red)
4172 ? omega_red : omega_black;
4173 }
4174
4175 if (dump_file && (dump_flags & TDF_DETAILS))
4176 {
4177 if (pb->geqs[Ue].color == omega_red
4178 || pb->geqs[Le].color == omega_red)
4179 fprintf (dump_file,
4180 " ::=> [%s >= %d]\n",
4181 omega_variable_to_str (pb, 1),
4182 constantTerm);
4183 else
4184 fprintf (dump_file,
4185 " ::=> %s >= %d\n",
4186 omega_variable_to_str (pb, 1),
4187 constantTerm);
4188 }
4189 }
4190 else
4191 {
4192 constantTerm = int_div (constantTerm, -coefficient);
4193 if (constantTerm < upper_bound
4194 || (constantTerm == upper_bound
4195 && pb->geqs[Ue].color == omega_black
4196 && pb->geqs[Le].color == omega_black))
4197 {
4198 upper_bound = constantTerm;
4199 ub_color = (pb->geqs[Ue].color == omega_red
4200 || pb->geqs[Le].color == omega_red)
4201 ? omega_red : omega_black;
4202 }
4203
4204 if (dump_file
4205 && (dump_flags & TDF_DETAILS))
4206 {
4207 if (pb->geqs[Ue].color == omega_red
4208 || pb->geqs[Le].color == omega_red)
4209 fprintf (dump_file,
4210 " ::=> [%s <= %d]\n",
4211 omega_variable_to_str (pb, 1),
4212 constantTerm);
4213 else
4214 fprintf (dump_file,
4215 " ::=> %s <= %d\n",
4216 omega_variable_to_str (pb, 1),
4217 constantTerm);
4218 }
4219 }
4220 }
4221
4222 pb->num_geqs = 0;
4223
4224 if (dump_file && (dump_flags & TDF_DETAILS))
4225 fprintf (dump_file,
4226 " therefore, %c%d <= %c%s%c <= %d%c\n",
4227 lb_color == omega_red ? '[' : ' ', lower_bound,
4228 (lb_color == omega_red && ub_color == omega_black)
4229 ? ']' : ' ',
4230 omega_variable_to_str (pb, 1),
4231 (lb_color == omega_black && ub_color == omega_red)
4232 ? '[' : ' ',
4233 upper_bound, ub_color == omega_red ? ']' : ' ');
4234
4235 if (lower_bound > upper_bound)
4236 return omega_false;
4237
4238 if (pb->safe_vars == 1)
4239 {
4240 if (upper_bound == lower_bound
4241 && !(ub_color == omega_red || lb_color == omega_red)
4242 && !please_no_equalities_in_simplified_problems)
4243 {
4244 pb->num_eqs++;
4245 pb->eqs[0].coef[1] = -1;
4246 pb->eqs[0].coef[0] = upper_bound;
4247
4248 if (ub_color == omega_red
4249 || lb_color == omega_red)
4250 pb->eqs[0].color = omega_red;
4251
4252 if (desired_res == omega_simplify
4253 && pb->eqs[0].color == omega_black)
4254 return omega_solve_problem (pb, desired_res);
4255 }
4256
4257 if (upper_bound != pos_infinity)
4258 {
4259 pb->geqs[0].coef[1] = -1;
4260 pb->geqs[0].coef[0] = upper_bound;
4261 pb->geqs[0].color = ub_color;
4262 pb->geqs[0].key = -1;
4263 pb->geqs[0].touched = 0;
4264 pb->num_geqs++;
4265 }
4266
4267 if (lower_bound != neg_infinity)
4268 {
4269 pb->geqs[pb->num_geqs].coef[1] = 1;
4270 pb->geqs[pb->num_geqs].coef[0] = -lower_bound;
4271 pb->geqs[pb->num_geqs].color = lb_color;
4272 pb->geqs[pb->num_geqs].key = 1;
4273 pb->geqs[pb->num_geqs].touched = 0;
4274 pb->num_geqs++;
4275 }
4276 }
4277
4278 if (desired_res == omega_simplify)
4279 {
4280 omega_problem_reduced (pb);
4281 return omega_false;
4282 }
4283 else
4284 {
4285 if (!conservative
4286 && (desired_res != omega_simplify
4287 || (lb_color == omega_black
4288 && ub_color == omega_black))
4289 && original_problem != no_problem
4290 && lower_bound == upper_bound)
4291 {
4292 for (i = original_problem->num_vars; i >= 0; i--)
4293 if (original_problem->var[i] == pb->var[1])
4294 break;
4295
4296 if (i == 0)
4297 break;
4298
4299 e = original_problem->num_eqs++;
4300 omega_init_eqn_zero (&original_problem->eqs[e],
4301 original_problem->num_vars);
4302 original_problem->eqs[e].coef[i] = -1;
4303 original_problem->eqs[e].coef[0] = upper_bound;
4304
4305 if (dump_file && (dump_flags & TDF_DETAILS))
4306 {
4307 fprintf (dump_file,
4308 "adding equality %d to outer problem\n", e);
4309 omega_print_problem (dump_file, original_problem);
4310 }
4311 }
4312 return omega_true;
4313 }
4314 }
4315
4316 eliminate_again = true;
4317
4318 if (lower_bound_count == 1)
4319 {
4320 eqn lbeqn = omega_alloc_eqns (0, 1);
4321 int Lc = pb->geqs[Le].coef[i];
4322
4323 if (dump_file && (dump_flags & TDF_DETAILS))
4324 fprintf (dump_file, "an inplace elimination\n");
4325
4326 omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1));
4327 omega_delete_geq_extra (pb, Le, n_vars + 1);
4328
4329 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4330 if (pb->geqs[Ue].coef[i] < 0)
4331 {
4332 if (lbeqn->key == -pb->geqs[Ue].key)
4333 omega_delete_geq_extra (pb, Ue, n_vars + 1);
4334 else
4335 {
4336 int k;
4337 int Uc = -pb->geqs[Ue].coef[i];
4338 pb->geqs[Ue].touched = 1;
4339 eliminate_again = false;
4340
4341 if (lbeqn->color == omega_red)
4342 pb->geqs[Ue].color = omega_red;
4343
4344 for (k = 0; k <= n_vars; k++)
4345 pb->geqs[Ue].coef[k] =
4346 check_mul (pb->geqs[Ue].coef[k], Lc) +
4347 check_mul (lbeqn->coef[k], Uc);
4348
4349 if (dump_file && (dump_flags & TDF_DETAILS))
4350 {
4351 omega_print_geq (dump_file, pb,
4352 &(pb->geqs[Ue]));
4353 fprintf (dump_file, "\n");
4354 }
4355 }
4356 }
4357
4358 omega_free_eqns (lbeqn, 1);
4359 continue;
4360 }
4361 else
4362 {
4363 int *dead_eqns = XNEWVEC (int, OMEGA_MAX_GEQS);
4364 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
4365 int num_dead = 0;
4366 int top_eqn = pb->num_geqs - 1;
4367 lower_bound_count--;
4368
4369 if (dump_file && (dump_flags & TDF_DETAILS))
4370 fprintf (dump_file, "lower bound count = %d\n",
4371 lower_bound_count);
4372
4373 for (Le = top_eqn; Le >= 0; Le--)
4374 if (pb->geqs[Le].coef[i] > 0)
4375 {
4376 int Lc = pb->geqs[Le].coef[i];
4377 for (Ue = top_eqn; Ue >= 0; Ue--)
4378 if (pb->geqs[Ue].coef[i] < 0)
4379 {
4380 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4381 {
4382 int k;
4383 int Uc = -pb->geqs[Ue].coef[i];
4384
4385 if (num_dead == 0)
4386 e2 = pb->num_geqs++;
4387 else
4388 e2 = dead_eqns[--num_dead];
4389
4390 gcc_assert (e2 < OMEGA_MAX_GEQS);
4391
4392 if (dump_file && (dump_flags & TDF_DETAILS))
4393 {
4394 fprintf (dump_file,
4395 "Le = %d, Ue = %d, gen = %d\n",
4396 Le, Ue, e2);
4397 omega_print_geq_extra (dump_file, pb,
4398 &(pb->geqs[Le]));
4399 fprintf (dump_file, "\n");
4400 omega_print_geq_extra (dump_file, pb,
4401 &(pb->geqs[Ue]));
4402 fprintf (dump_file, "\n");
4403 }
4404
4405 eliminate_again = false;
4406
4407 for (k = n_vars; k >= 0; k--)
4408 pb->geqs[e2].coef[k] =
4409 check_mul (pb->geqs[Ue].coef[k], Lc) +
4410 check_mul (pb->geqs[Le].coef[k], Uc);
4411
4412 pb->geqs[e2].coef[n_vars + 1] = 0;
4413 pb->geqs[e2].touched = 1;
4414
4415 if (pb->geqs[Ue].color == omega_red
4416 || pb->geqs[Le].color == omega_red)
4417 pb->geqs[e2].color = omega_red;
4418 else
4419 pb->geqs[e2].color = omega_black;
4420
4421 if (dump_file && (dump_flags & TDF_DETAILS))
4422 {
4423 omega_print_geq (dump_file, pb,
4424 &(pb->geqs[e2]));
4425 fprintf (dump_file, "\n");
4426 }
4427 }
4428
4429 if (lower_bound_count == 0)
4430 {
4431 dead_eqns[num_dead++] = Ue;
4432
4433 if (dump_file && (dump_flags & TDF_DETAILS))
4434 fprintf (dump_file, "Killed %d\n", Ue);
4435 }
4436 }
4437
4438 lower_bound_count--;
4439 dead_eqns[num_dead++] = Le;
4440
4441 if (dump_file && (dump_flags & TDF_DETAILS))
4442 fprintf (dump_file, "Killed %d\n", Le);
4443 }
4444
4445 for (e = pb->num_geqs - 1; e >= 0; e--)
4446 is_dead[e] = false;
4447
4448 while (num_dead > 0)
4449 is_dead[dead_eqns[--num_dead]] = true;
4450
4451 for (e = pb->num_geqs - 1; e >= 0; e--)
4452 if (is_dead[e])
4453 omega_delete_geq_extra (pb, e, n_vars + 1);
4454
4455 free (dead_eqns);
4456 free (is_dead);
4457 continue;
4458 }
4459 }
4460 else
4461 {
4462 omega_pb rS, iS;
4463
4464 rS = omega_alloc_problem (0, 0);
4465 iS = omega_alloc_problem (0, 0);
4466 e2 = 0;
4467 possible_easy_int_solution = true;
4468
4469 for (e = 0; e < pb->num_geqs; e++)
4470 if (pb->geqs[e].coef[i] == 0)
4471 {
4472 omega_copy_eqn (&(rS->geqs[e2]), &pb->geqs[e],
4473 pb->num_vars);
4474 omega_copy_eqn (&(iS->geqs[e2]), &pb->geqs[e],
4475 pb->num_vars);
4476
4477 if (dump_file && (dump_flags & TDF_DETAILS))
4478 {
4479 int t;
4480 fprintf (dump_file, "Copying (%d, %d): ", i,
4481 pb->geqs[e].coef[i]);
4482 omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
4483 fprintf (dump_file, "\n");
4484 for (t = 0; t <= n_vars + 1; t++)
4485 fprintf (dump_file, "%d ", pb->geqs[e].coef[t]);
4486 fprintf (dump_file, "\n");
4487
4488 }
4489 e2++;
4490 gcc_assert (e2 < OMEGA_MAX_GEQS);
4491 }
4492
4493 for (Le = pb->num_geqs - 1; Le >= 0; Le--)
4494 if (pb->geqs[Le].coef[i] > 0)
4495 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4496 if (pb->geqs[Ue].coef[i] < 0)
4497 {
4498 int k;
4499 int Lc = pb->geqs[Le].coef[i];
4500 int Uc = -pb->geqs[Ue].coef[i];
4501
4502 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4503 {
4504
4505 rS->geqs[e2].touched = iS->geqs[e2].touched = 1;
4506
4507 if (dump_file && (dump_flags & TDF_DETAILS))
4508 {
4509 fprintf (dump_file, "---\n");
4510 fprintf (dump_file,
4511 "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
4512 Le, Lc, Ue, Uc, e2);
4513 omega_print_geq_extra (dump_file, pb, &pb->geqs[Le]);
4514 fprintf (dump_file, "\n");
4515 omega_print_geq_extra (dump_file, pb, &pb->geqs[Ue]);
4516 fprintf (dump_file, "\n");
4517 }
4518
4519 if (Uc == Lc)
4520 {
4521 for (k = n_vars; k >= 0; k--)
4522 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4523 pb->geqs[Ue].coef[k] + pb->geqs[Le].coef[k];
4524
4525 iS->geqs[e2].coef[0] -= (Uc - 1);
4526 }
4527 else
4528 {
4529 for (k = n_vars; k >= 0; k--)
4530 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4531 check_mul (pb->geqs[Ue].coef[k], Lc) +
4532 check_mul (pb->geqs[Le].coef[k], Uc);
4533
4534 iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
4535 }
4536
4537 if (pb->geqs[Ue].color == omega_red
4538 || pb->geqs[Le].color == omega_red)
4539 iS->geqs[e2].color = rS->geqs[e2].color = omega_red;
4540 else
4541 iS->geqs[e2].color = rS->geqs[e2].color = omega_black;
4542
4543 if (dump_file && (dump_flags & TDF_DETAILS))
4544 {
4545 omega_print_geq (dump_file, pb, &(rS->geqs[e2]));
4546 fprintf (dump_file, "\n");
4547 }
4548
4549 e2++;
4550 gcc_assert (e2 < OMEGA_MAX_GEQS);
4551 }
4552 else if (pb->geqs[Ue].coef[0] * Lc +
4553 pb->geqs[Le].coef[0] * Uc -
4554 (Uc - 1) * (Lc - 1) < 0)
4555 possible_easy_int_solution = false;
4556 }
4557
4558 iS->variables_initialized = rS->variables_initialized = true;
4559 iS->num_vars = rS->num_vars = pb->num_vars;
4560 iS->num_geqs = rS->num_geqs = e2;
4561 iS->num_eqs = rS->num_eqs = 0;
4562 iS->num_subs = rS->num_subs = pb->num_subs;
4563 iS->safe_vars = rS->safe_vars = pb->safe_vars;
4564
4565 for (e = n_vars; e >= 0; e--)
4566 rS->var[e] = pb->var[e];
4567
4568 for (e = n_vars; e >= 0; e--)
4569 iS->var[e] = pb->var[e];
4570
4571 for (e = pb->num_subs - 1; e >= 0; e--)
4572 {
4573 omega_copy_eqn (&(rS->subs[e]), &(pb->subs[e]), pb->num_vars);
4574 omega_copy_eqn (&(iS->subs[e]), &(pb->subs[e]), pb->num_vars);
4575 }
4576
4577 pb->num_vars++;
4578 n_vars = pb->num_vars;
4579
4580 if (desired_res != omega_true)
4581 {
4582 if (original_problem == no_problem)
4583 {
4584 original_problem = pb;
4585 result = omega_solve_geq (rS, omega_false);
4586 original_problem = no_problem;
4587 }
4588 else
4589 result = omega_solve_geq (rS, omega_false);
4590
4591 if (result == omega_false)
4592 {
4593 free (rS);
4594 free (iS);
4595 return result;
4596 }
4597
4598 if (pb->num_eqs > 0)
4599 {
4600 /* An equality constraint must have been found */
4601 free (rS);
4602 free (iS);
4603 return omega_solve_problem (pb, desired_res);
4604 }
4605 }
4606
4607 if (desired_res != omega_false)
4608 {
4609 int j;
4610 int lower_bounds = 0;
4611 int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS);
4612
4613 if (possible_easy_int_solution)
4614 {
4615 conservative++;
4616 result = omega_solve_geq (iS, desired_res);
4617 conservative--;
4618
4619 if (result != omega_false)
4620 {
4621 free (rS);
4622 free (iS);
4623 free (lower_bound);
4624 return result;
4625 }
4626 }
4627
4628 if (!exact && best_parallel_eqn >= 0
4629 && parallel_difference <= max_splinters)
4630 {
4631 free (rS);
4632 free (iS);
4633 free (lower_bound);
4634 return parallel_splinter (pb, best_parallel_eqn,
4635 parallel_difference,
4636 desired_res);
4637 }
4638
4639 if (dump_file && (dump_flags & TDF_DETAILS))
4640 fprintf (dump_file, "have to do exact analysis\n");
4641
4642 conservative++;
4643
4644 for (e = 0; e < pb->num_geqs; e++)
4645 if (pb->geqs[e].coef[i] > 1)
4646 lower_bound[lower_bounds++] = e;
4647
4648 /* Sort array LOWER_BOUND. */
4649 for (j = 0; j < lower_bounds; j++)
4650 {
4651 int k, smallest = j;
4652
4653 for (k = j + 1; k < lower_bounds; k++)
4654 if (pb->geqs[lower_bound[smallest]].coef[i] >
4655 pb->geqs[lower_bound[k]].coef[i])
4656 smallest = k;
4657
4658 k = lower_bound[smallest];
4659 lower_bound[smallest] = lower_bound[j];
4660 lower_bound[j] = k;
4661 }
4662
4663 if (dump_file && (dump_flags & TDF_DETAILS))
4664 {
4665 fprintf (dump_file, "lower bound coefficients = ");
4666
4667 for (j = 0; j < lower_bounds; j++)
4668 fprintf (dump_file, " %d",
4669 pb->geqs[lower_bound[j]].coef[i]);
4670
4671 fprintf (dump_file, "\n");
4672 }
4673
4674 for (j = 0; j < lower_bounds; j++)
4675 {
4676 int max_incr;
4677 int c;
4678 int worst_lower_bound_constant = -minC;
4679
4680 e = lower_bound[j];
4681 max_incr = (((pb->geqs[e].coef[i] - 1) *
4682 (worst_lower_bound_constant - 1) - 1)
4683 / worst_lower_bound_constant);
4684 /* max_incr += 2; */
4685
4686 if (dump_file && (dump_flags & TDF_DETAILS))
4687 {
4688 fprintf (dump_file, "for equation ");
4689 omega_print_geq (dump_file, pb, &pb->geqs[e]);
4690 fprintf (dump_file,
4691 "\ntry decrements from 0 to %d\n",
4692 max_incr);
4693 omega_print_problem (dump_file, pb);
4694 }
4695
4696 if (max_incr > 50 && !smoothed
4697 && smooth_weird_equations (pb))
4698 {
4699 conservative--;
4700 free (rS);
4701 free (iS);
4702 smoothed = true;
4703 goto solve_geq_start;
4704 }
4705
4706 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e],
4707 pb->num_vars);
4708 pb->eqs[0].color = omega_black;
4709 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
4710 pb->geqs[e].touched = 1;
4711 pb->num_eqs = 1;
4712
4713 for (c = max_incr; c >= 0; c--)
4714 {
4715 if (dump_file && (dump_flags & TDF_DETAILS))
4716 {
4717 fprintf (dump_file,
4718 "trying next decrement of %d\n",
4719 max_incr - c);
4720 omega_print_problem (dump_file, pb);
4721 }
4722
4723 omega_copy_problem (rS, pb);
4724
4725 if (dump_file && (dump_flags & TDF_DETAILS))
4726 omega_print_problem (dump_file, rS);
4727
4728 result = omega_solve_problem (rS, desired_res);
4729
4730 if (result == omega_true)
4731 {
4732 free (rS);
4733 free (iS);
4734 free (lower_bound);
4735 conservative--;
4736 return omega_true;
4737 }
4738
4739 pb->eqs[0].coef[0]--;
4740 }
4741
4742 if (j + 1 < lower_bounds)
4743 {
4744 pb->num_eqs = 0;
4745 omega_copy_eqn (&pb->geqs[e], &pb->eqs[0],
4746 pb->num_vars);
4747 pb->geqs[e].touched = 1;
4748 pb->geqs[e].color = omega_black;
4749 omega_copy_problem (rS, pb);
4750
4751 if (dump_file && (dump_flags & TDF_DETAILS))
4752 fprintf (dump_file,
4753 "exhausted lower bound, "
4754 "checking if still feasible ");
4755
4756 result = omega_solve_problem (rS, omega_false);
4757
4758 if (result == omega_false)
4759 break;
4760 }
4761 }
4762
4763 if (dump_file && (dump_flags & TDF_DETAILS))
4764 fprintf (dump_file, "fall-off the end\n");
4765
4766 free (rS);
4767 free (iS);
4768 free (lower_bound);
4769 conservative--;
4770 return omega_false;
4771 }
4772
4773 free (rS);
4774 free (iS);
4775 }
4776 return omega_unknown;
4777 } while (eliminate_again);
4778 } while (1);
4779 }
4780
4781 /* Because the omega solver is recursive, this counter limits the
4782 recursion depth. */
4783 static int omega_solve_depth = 0;
4784
4785 /* Return omega_true when the problem PB has a solution following the
4786 DESIRED_RES. */
4787
4788 enum omega_result
4789 omega_solve_problem (omega_pb pb, enum omega_result desired_res)
4790 {
4791 enum omega_result result;
4792
4793 gcc_assert (pb->num_vars >= pb->safe_vars);
4794 omega_solve_depth++;
4795
4796 if (desired_res != omega_simplify)
4797 pb->safe_vars = 0;
4798
4799 if (omega_solve_depth > 50)
4800 {
4801 if (dump_file && (dump_flags & TDF_DETAILS))
4802 {
4803 fprintf (dump_file,
4804 "Solve depth = %d, in_approximate_mode = %d, aborting\n",
4805 omega_solve_depth, in_approximate_mode);
4806 omega_print_problem (dump_file, pb);
4807 }
4808 gcc_assert (0);
4809 }
4810
4811 if (omega_solve_eq (pb, desired_res) == omega_false)
4812 {
4813 omega_solve_depth--;
4814 return omega_false;
4815 }
4816
4817 if (in_approximate_mode && !pb->num_geqs)
4818 {
4819 result = omega_true;
4820 pb->num_vars = pb->safe_vars;
4821 omega_problem_reduced (pb);
4822 }
4823 else
4824 result = omega_solve_geq (pb, desired_res);
4825
4826 omega_solve_depth--;
4827
4828 if (!omega_reduce_with_subs)
4829 {
4830 resurrect_subs (pb);
4831 gcc_assert (please_no_equalities_in_simplified_problems
4832 || !result || pb->num_subs == 0);
4833 }
4834
4835 return result;
4836 }
4837
4838 /* Return true if red equations constrain the set of possible solutions.
4839 We assume that there are solutions to the black equations by
4840 themselves, so if there is no solution to the combined problem, we
4841 return true. */
4842
4843 bool
4844 omega_problem_has_red_equations (omega_pb pb)
4845 {
4846 bool result;
4847 int e;
4848 int i;
4849
4850 if (dump_file && (dump_flags & TDF_DETAILS))
4851 {
4852 fprintf (dump_file, "Checking for red equations:\n");
4853 omega_print_problem (dump_file, pb);
4854 }
4855
4856 please_no_equalities_in_simplified_problems++;
4857 may_be_red++;
4858
4859 if (omega_single_result)
4860 return_single_result++;
4861
4862 create_color = true;
4863 result = (omega_simplify_problem (pb) == omega_false);
4864
4865 if (omega_single_result)
4866 return_single_result--;
4867
4868 may_be_red--;
4869 please_no_equalities_in_simplified_problems--;
4870
4871 if (result)
4872 {
4873 if (dump_file && (dump_flags & TDF_DETAILS))
4874 fprintf (dump_file, "Gist is FALSE\n");
4875
4876 pb->num_subs = 0;
4877 pb->num_geqs = 0;
4878 pb->num_eqs = 1;
4879 pb->eqs[0].color = omega_red;
4880
4881 for (i = pb->num_vars; i > 0; i--)
4882 pb->eqs[0].coef[i] = 0;
4883
4884 pb->eqs[0].coef[0] = 1;
4885 return true;
4886 }
4887
4888 free_red_eliminations (pb);
4889 gcc_assert (pb->num_eqs == 0);
4890
4891 for (e = pb->num_geqs - 1; e >= 0; e--)
4892 if (pb->geqs[e].color == omega_red)
4893 result = true;
4894
4895 if (!result)
4896 return false;
4897
4898 for (i = pb->safe_vars; i >= 1; i--)
4899 {
4900 int ub = 0;
4901 int lb = 0;
4902
4903 for (e = pb->num_geqs - 1; e >= 0; e--)
4904 {
4905 if (pb->geqs[e].coef[i])
4906 {
4907 if (pb->geqs[e].coef[i] > 0)
4908 lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4909
4910 else
4911 ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4912 }
4913 }
4914
4915 if (ub == 2 || lb == 2)
4916 {
4917
4918 if (dump_file && (dump_flags & TDF_DETAILS))
4919 fprintf (dump_file, "checks for upper/lower bounds worked!\n");
4920
4921 if (!omega_reduce_with_subs)
4922 {
4923 resurrect_subs (pb);
4924 gcc_assert (pb->num_subs == 0);
4925 }
4926
4927 return true;
4928 }
4929 }
4930
4931
4932 if (dump_file && (dump_flags & TDF_DETAILS))
4933 fprintf (dump_file,
4934 "*** Doing potentially expensive elimination tests "
4935 "for red equations\n");
4936
4937 please_no_equalities_in_simplified_problems++;
4938 omega_eliminate_red (pb, true);
4939 please_no_equalities_in_simplified_problems--;
4940
4941 result = false;
4942 gcc_assert (pb->num_eqs == 0);
4943
4944 for (e = pb->num_geqs - 1; e >= 0; e--)
4945 if (pb->geqs[e].color == omega_red)
4946 result = true;
4947
4948 if (dump_file && (dump_flags & TDF_DETAILS))
4949 {
4950 if (!result)
4951 fprintf (dump_file,
4952 "******************** Redundant Red Equations eliminated!!\n");
4953 else
4954 fprintf (dump_file,
4955 "******************** Red Equations remain\n");
4956
4957 omega_print_problem (dump_file, pb);
4958 }
4959
4960 if (!omega_reduce_with_subs)
4961 {
4962 normalize_return_type r;
4963
4964 resurrect_subs (pb);
4965 r = normalize_omega_problem (pb);
4966 gcc_assert (r != normalize_false);
4967
4968 coalesce (pb);
4969 cleanout_wildcards (pb);
4970 gcc_assert (pb->num_subs == 0);
4971 }
4972
4973 return result;
4974 }
4975
4976 /* Calls omega_simplify_problem in approximate mode. */
4977
4978 enum omega_result
4979 omega_simplify_approximate (omega_pb pb)
4980 {
4981 enum omega_result result;
4982
4983 if (dump_file && (dump_flags & TDF_DETAILS))
4984 fprintf (dump_file, "(Entering approximate mode\n");
4985
4986 in_approximate_mode = true;
4987 result = omega_simplify_problem (pb);
4988 in_approximate_mode = false;
4989
4990 gcc_assert (pb->num_vars == pb->safe_vars);
4991 if (!omega_reduce_with_subs)
4992 gcc_assert (pb->num_subs == 0);
4993
4994 if (dump_file && (dump_flags & TDF_DETAILS))
4995 fprintf (dump_file, "Leaving approximate mode)\n");
4996
4997 return result;
4998 }
4999
5000
5001 /* Simplifies problem PB by eliminating redundant constraints and
5002 reducing the constraints system to a minimal form. Returns
5003 omega_true when the problem was successfully reduced, omega_unknown
5004 when the solver is unable to determine an answer. */
5005
5006 enum omega_result
5007 omega_simplify_problem (omega_pb pb)
5008 {
5009 int i;
5010
5011 omega_found_reduction = omega_false;
5012
5013 if (!pb->variables_initialized)
5014 omega_initialize_variables (pb);
5015
5016 if (next_key * 3 > MAX_KEYS)
5017 {
5018 int e;
5019
5020 hash_version++;
5021 next_key = OMEGA_MAX_VARS + 1;
5022
5023 for (e = pb->num_geqs - 1; e >= 0; e--)
5024 pb->geqs[e].touched = 1;
5025
5026 for (i = 0; i < HASH_TABLE_SIZE; i++)
5027 hash_master[i].touched = -1;
5028
5029 pb->hash_version = hash_version;
5030 }
5031
5032 else if (pb->hash_version != hash_version)
5033 {
5034 int e;
5035
5036 for (e = pb->num_geqs - 1; e >= 0; e--)
5037 pb->geqs[e].touched = 1;
5038
5039 pb->hash_version = hash_version;
5040 }
5041
5042 if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars)
5043 omega_free_eliminations (pb, pb->safe_vars);
5044
5045 if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0)
5046 {
5047 omega_found_reduction = omega_solve_problem (pb, omega_unknown);
5048
5049 if (omega_found_reduction != omega_false
5050 && !return_single_result)
5051 {
5052 pb->num_geqs = 0;
5053 pb->num_eqs = 0;
5054 (*omega_when_reduced) (pb);
5055 }
5056
5057 return omega_found_reduction;
5058 }
5059
5060 omega_solve_problem (pb, omega_simplify);
5061
5062 if (omega_found_reduction != omega_false)
5063 {
5064 for (i = 1; omega_safe_var_p (pb, i); i++)
5065 pb->forwarding_address[pb->var[i]] = i;
5066
5067 for (i = 0; i < pb->num_subs; i++)
5068 pb->forwarding_address[pb->subs[i].key] = -i - 1;
5069 }
5070
5071 if (!omega_reduce_with_subs)
5072 gcc_assert (please_no_equalities_in_simplified_problems
5073 || omega_found_reduction == omega_false
5074 || pb->num_subs == 0);
5075
5076 return omega_found_reduction;
5077 }
5078
5079 /* Make variable VAR unprotected: it then can be eliminated. */
5080
5081 void
5082 omega_unprotect_variable (omega_pb pb, int var)
5083 {
5084 int e, idx;
5085 idx = pb->forwarding_address[var];
5086
5087 if (idx < 0)
5088 {
5089 idx = -1 - idx;
5090 pb->num_subs--;
5091
5092 if (idx < pb->num_subs)
5093 {
5094 omega_copy_eqn (&pb->subs[idx], &pb->subs[pb->num_subs],
5095 pb->num_vars);
5096 pb->forwarding_address[pb->subs[idx].key] = -idx - 1;
5097 }
5098 }
5099 else
5100 {
5101 int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS);
5102 int e2;
5103
5104 for (e = pb->num_subs - 1; e >= 0; e--)
5105 bring_to_life[e] = (pb->subs[e].coef[idx] != 0);
5106
5107 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
5108 if (bring_to_life[e2])
5109 {
5110 pb->num_vars++;
5111 pb->safe_vars++;
5112
5113 if (pb->safe_vars < pb->num_vars)
5114 {
5115 for (e = pb->num_geqs - 1; e >= 0; e--)
5116 {
5117 pb->geqs[e].coef[pb->num_vars] =
5118 pb->geqs[e].coef[pb->safe_vars];
5119
5120 pb->geqs[e].coef[pb->safe_vars] = 0;
5121 }
5122
5123 for (e = pb->num_eqs - 1; e >= 0; e--)
5124 {
5125 pb->eqs[e].coef[pb->num_vars] =
5126 pb->eqs[e].coef[pb->safe_vars];
5127
5128 pb->eqs[e].coef[pb->safe_vars] = 0;
5129 }
5130
5131 for (e = pb->num_subs - 1; e >= 0; e--)
5132 {
5133 pb->subs[e].coef[pb->num_vars] =
5134 pb->subs[e].coef[pb->safe_vars];
5135
5136 pb->subs[e].coef[pb->safe_vars] = 0;
5137 }
5138
5139 pb->var[pb->num_vars] = pb->var[pb->safe_vars];
5140 pb->forwarding_address[pb->var[pb->num_vars]] =
5141 pb->num_vars;
5142 }
5143 else
5144 {
5145 for (e = pb->num_geqs - 1; e >= 0; e--)
5146 pb->geqs[e].coef[pb->safe_vars] = 0;
5147
5148 for (e = pb->num_eqs - 1; e >= 0; e--)
5149 pb->eqs[e].coef[pb->safe_vars] = 0;
5150
5151 for (e = pb->num_subs - 1; e >= 0; e--)
5152 pb->subs[e].coef[pb->safe_vars] = 0;
5153 }
5154
5155 pb->var[pb->safe_vars] = pb->subs[e2].key;
5156 pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars;
5157
5158 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e2]),
5159 pb->num_vars);
5160 pb->eqs[pb->num_eqs++].coef[pb->safe_vars] = -1;
5161 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5162
5163 if (e2 < pb->num_subs - 1)
5164 omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]),
5165 pb->num_vars);
5166
5167 pb->num_subs--;
5168 }
5169
5170 omega_unprotect_1 (pb, &idx, NULL);
5171 free (bring_to_life);
5172 }
5173
5174 chain_unprotect (pb);
5175 }
5176
5177 /* Unprotects VAR and simplifies PB. */
5178
5179 enum omega_result
5180 omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color,
5181 int var, int sign)
5182 {
5183 int n_vars = pb->num_vars;
5184 int e, j;
5185 int k = pb->forwarding_address[var];
5186
5187 if (k < 0)
5188 {
5189 k = -1 - k;
5190
5191 if (sign != 0)
5192 {
5193 e = pb->num_geqs++;
5194 omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars);
5195
5196 for (j = 0; j <= n_vars; j++)
5197 pb->geqs[e].coef[j] *= sign;
5198
5199 pb->geqs[e].coef[0]--;
5200 pb->geqs[e].touched = 1;
5201 pb->geqs[e].color = color;
5202 }
5203 else
5204 {
5205 e = pb->num_eqs++;
5206 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5207 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5208 pb->eqs[e].color = color;
5209 }
5210 }
5211 else if (sign != 0)
5212 {
5213 e = pb->num_geqs++;
5214 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
5215 pb->geqs[e].coef[k] = sign;
5216 pb->geqs[e].coef[0] = -1;
5217 pb->geqs[e].touched = 1;
5218 pb->geqs[e].color = color;
5219 }
5220 else
5221 {
5222 e = pb->num_eqs++;
5223 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5224 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5225 pb->eqs[e].coef[k] = 1;
5226 pb->eqs[e].color = color;
5227 }
5228
5229 omega_unprotect_variable (pb, var);
5230 return omega_simplify_problem (pb);
5231 }
5232
5233 /* Add an equation "VAR = VALUE" with COLOR to PB. */
5234
5235 void
5236 omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color,
5237 int var, int value)
5238 {
5239 int e;
5240 int k = pb->forwarding_address[var];
5241
5242 if (k < 0)
5243 {
5244 k = -1 - k;
5245 e = pb->num_eqs++;
5246 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5247 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5248 pb->eqs[e].coef[0] -= value;
5249 }
5250 else
5251 {
5252 e = pb->num_eqs++;
5253 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5254 pb->eqs[e].coef[k] = 1;
5255 pb->eqs[e].coef[0] = -value;
5256 }
5257
5258 pb->eqs[e].color = color;
5259 }
5260
5261 /* Return false when the upper and lower bounds are not coupled.
5262 Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
5263 variable I. */
5264
5265 bool
5266 omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound)
5267 {
5268 int n_vars = pb->num_vars;
5269 int e, j;
5270 bool is_simple;
5271 bool coupled = false;
5272
5273 *lower_bound = neg_infinity;
5274 *upper_bound = pos_infinity;
5275 i = pb->forwarding_address[i];
5276
5277 if (i < 0)
5278 {
5279 i = -i - 1;
5280
5281 for (j = 1; j <= n_vars; j++)
5282 if (pb->subs[i].coef[j] != 0)
5283 return true;
5284
5285 *upper_bound = *lower_bound = pb->subs[i].coef[0];
5286 return false;
5287 }
5288
5289 for (e = pb->num_subs - 1; e >= 0; e--)
5290 if (pb->subs[e].coef[i] != 0)
5291 coupled = true;
5292
5293 for (e = pb->num_eqs - 1; e >= 0; e--)
5294 if (pb->eqs[e].coef[i] != 0)
5295 {
5296 is_simple = true;
5297
5298 for (j = 1; j <= n_vars; j++)
5299 if (i != j && pb->eqs[e].coef[j] != 0)
5300 {
5301 is_simple = false;
5302 coupled = true;
5303 break;
5304 }
5305
5306 if (!is_simple)
5307 continue;
5308 else
5309 {
5310 *lower_bound = *upper_bound =
5311 -pb->eqs[e].coef[i] * pb->eqs[e].coef[0];
5312 return false;
5313 }
5314 }
5315
5316 for (e = pb->num_geqs - 1; e >= 0; e--)
5317 if (pb->geqs[e].coef[i] != 0)
5318 {
5319 if (pb->geqs[e].key == i)
5320 *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]);
5321
5322 else if (pb->geqs[e].key == -i)
5323 *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]);
5324
5325 else
5326 coupled = true;
5327 }
5328
5329 return coupled;
5330 }
5331
5332 /* Sets the lower bound L and upper bound U for the values of variable
5333 I, and sets COULD_BE_ZERO to true if variable I might take value
5334 zero. LOWER_BOUND and UPPER_BOUND are bounds on the values of
5335 variable I. */
5336
5337 static void
5338 query_coupled_variable (omega_pb pb, int i, int *l, int *u,
5339 bool *could_be_zero, int lower_bound, int upper_bound)
5340 {
5341 int e, b1, b2;
5342 eqn eqn;
5343 int sign;
5344 int v;
5345
5346 /* Preconditions. */
5347 gcc_assert (abs (pb->forwarding_address[i]) == 1
5348 && pb->num_vars + pb->num_subs == 2
5349 && pb->num_eqs + pb->num_subs == 1);
5350
5351 /* Define variable I in terms of variable V. */
5352 if (pb->forwarding_address[i] == -1)
5353 {
5354 eqn = &pb->subs[0];
5355 sign = 1;
5356 v = 1;
5357 }
5358 else
5359 {
5360 eqn = &pb->eqs[0];
5361 sign = -eqn->coef[1];
5362 v = 2;
5363 }
5364
5365 for (e = pb->num_geqs - 1; e >= 0; e--)
5366 if (pb->geqs[e].coef[v] != 0)
5367 {
5368 if (pb->geqs[e].coef[v] == 1)
5369 lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]);
5370
5371 else
5372 upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]);
5373 }
5374
5375 if (lower_bound > upper_bound)
5376 {
5377 *l = pos_infinity;
5378 *u = neg_infinity;
5379 *could_be_zero = 0;
5380 return;
5381 }
5382
5383 if (lower_bound == neg_infinity)
5384 {
5385 if (eqn->coef[v] > 0)
5386 b1 = sign * neg_infinity;
5387
5388 else
5389 b1 = -sign * neg_infinity;
5390 }
5391 else
5392 b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound);
5393
5394 if (upper_bound == pos_infinity)
5395 {
5396 if (eqn->coef[v] > 0)
5397 b2 = sign * pos_infinity;
5398
5399 else
5400 b2 = -sign * pos_infinity;
5401 }
5402 else
5403 b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound);
5404
5405 *l = MAX (*l, b1 <= b2 ? b1 : b2);
5406 *u = MIN (*u, b1 <= b2 ? b2 : b1);
5407
5408 *could_be_zero = (*l <= 0 && 0 <= *u
5409 && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0);
5410 }
5411
5412 /* Return false when a lower bound L and an upper bound U for variable
5413 I in problem PB have been initialized. */
5414
5415 bool
5416 omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u)
5417 {
5418 *l = neg_infinity;
5419 *u = pos_infinity;
5420
5421 if (!omega_query_variable (pb, i, l, u)
5422 || (pb->num_vars == 1 && pb->forwarding_address[i] == 1))
5423 return false;
5424
5425 if (abs (pb->forwarding_address[i]) == 1
5426 && pb->num_vars + pb->num_subs == 2
5427 && pb->num_eqs + pb->num_subs == 1)
5428 {
5429 bool could_be_zero;
5430 query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity,
5431 pos_infinity);
5432 return false;
5433 }
5434
5435 return true;
5436 }
5437
5438 /* For problem PB, return an integer that represents the classic data
5439 dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
5440 masks that are added to the result. When DIST_KNOWN is true, DIST
5441 is set to the classic data dependence distance. LOWER_BOUND and
5442 UPPER_BOUND are bounds on the value of variable I, for example, it
5443 is possible to narrow the iteration domain with safe approximations
5444 of loop counts, and thus discard some data dependences that cannot
5445 occur. */
5446
5447 int
5448 omega_query_variable_signs (omega_pb pb, int i, int dd_lt,
5449 int dd_eq, int dd_gt, int lower_bound,
5450 int upper_bound, bool *dist_known, int *dist)
5451 {
5452 int result;
5453 int l, u;
5454 bool could_be_zero;
5455
5456 l = neg_infinity;
5457 u = pos_infinity;
5458
5459 omega_query_variable (pb, i, &l, &u);
5460 query_coupled_variable (pb, i, &l, &u, &could_be_zero, lower_bound,
5461 upper_bound);
5462 result = 0;
5463
5464 if (l < 0)
5465 result |= dd_gt;
5466
5467 if (u > 0)
5468 result |= dd_lt;
5469
5470 if (could_be_zero)
5471 result |= dd_eq;
5472
5473 if (l == u)
5474 {
5475 *dist_known = true;
5476 *dist = l;
5477 }
5478 else
5479 *dist_known = false;
5480
5481 return result;
5482 }
5483
5484 /* Initialize PB as an Omega problem with NVARS variables and NPROT
5485 safe variables. Safe variables are not eliminated during the
5486 Fourier-Motzkin elimination. Safe variables are all those
5487 variables that are placed at the beginning of the array of
5488 variables: P->var[0, ..., NPROT - 1]. */
5489
5490 omega_pb
5491 omega_alloc_problem (int nvars, int nprot)
5492 {
5493 omega_pb pb;
5494
5495 gcc_assert (nvars <= OMEGA_MAX_VARS);
5496 omega_initialize ();
5497
5498 /* Allocate and initialize PB. */
5499 pb = XCNEW (struct omega_pb_d);
5500 pb->var = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5501 pb->forwarding_address = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5502 pb->geqs = omega_alloc_eqns (0, OMEGA_MAX_GEQS);
5503 pb->eqs = omega_alloc_eqns (0, OMEGA_MAX_EQS);
5504 pb->subs = omega_alloc_eqns (0, OMEGA_MAX_VARS + 1);
5505
5506 pb->hash_version = hash_version;
5507 pb->num_vars = nvars;
5508 pb->safe_vars = nprot;
5509 pb->variables_initialized = false;
5510 pb->variables_freed = false;
5511 pb->num_eqs = 0;
5512 pb->num_geqs = 0;
5513 pb->num_subs = 0;
5514 return pb;
5515 }
5516
5517 /* Keeps the state of the initialization. */
5518 static bool omega_initialized = false;
5519
5520 /* Initialization of the Omega solver. */
5521
5522 void
5523 omega_initialize (void)
5524 {
5525 int i;
5526
5527 if (omega_initialized)
5528 return;
5529
5530 next_wild_card = 0;
5531 next_key = OMEGA_MAX_VARS + 1;
5532 packing = XCNEWVEC (int, OMEGA_MAX_VARS);
5533 fast_lookup = XCNEWVEC (int, MAX_KEYS * 2);
5534 fast_lookup_red = XCNEWVEC (int, MAX_KEYS * 2);
5535 hash_master = omega_alloc_eqns (0, HASH_TABLE_SIZE);
5536
5537 for (i = 0; i < HASH_TABLE_SIZE; i++)
5538 hash_master[i].touched = -1;
5539
5540 sprintf (wild_name[0], "1");
5541 sprintf (wild_name[1], "a");
5542 sprintf (wild_name[2], "b");
5543 sprintf (wild_name[3], "c");
5544 sprintf (wild_name[4], "d");
5545 sprintf (wild_name[5], "e");
5546 sprintf (wild_name[6], "f");
5547 sprintf (wild_name[7], "g");
5548 sprintf (wild_name[8], "h");
5549 sprintf (wild_name[9], "i");
5550 sprintf (wild_name[10], "j");
5551 sprintf (wild_name[11], "k");
5552 sprintf (wild_name[12], "l");
5553 sprintf (wild_name[13], "m");
5554 sprintf (wild_name[14], "n");
5555 sprintf (wild_name[15], "o");
5556 sprintf (wild_name[16], "p");
5557 sprintf (wild_name[17], "q");
5558 sprintf (wild_name[18], "r");
5559 sprintf (wild_name[19], "s");
5560 sprintf (wild_name[20], "t");
5561 sprintf (wild_name[40 - 1], "alpha");
5562 sprintf (wild_name[40 - 2], "beta");
5563 sprintf (wild_name[40 - 3], "gamma");
5564 sprintf (wild_name[40 - 4], "delta");
5565 sprintf (wild_name[40 - 5], "tau");
5566 sprintf (wild_name[40 - 6], "sigma");
5567 sprintf (wild_name[40 - 7], "chi");
5568 sprintf (wild_name[40 - 8], "omega");
5569 sprintf (wild_name[40 - 9], "pi");
5570 sprintf (wild_name[40 - 10], "ni");
5571 sprintf (wild_name[40 - 11], "Alpha");
5572 sprintf (wild_name[40 - 12], "Beta");
5573 sprintf (wild_name[40 - 13], "Gamma");
5574 sprintf (wild_name[40 - 14], "Delta");
5575 sprintf (wild_name[40 - 15], "Tau");
5576 sprintf (wild_name[40 - 16], "Sigma");
5577 sprintf (wild_name[40 - 17], "Chi");
5578 sprintf (wild_name[40 - 18], "Omega");
5579 sprintf (wild_name[40 - 19], "xxx");
5580
5581 omega_initialized = true;
5582 }