?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
blame | history | raw | HEAD
http://gcc.gnu.org/ml/gcc-patches/2008-02/msg01094.html
[official-gcc.git] / gcc / omega.c
blob93b5515108e02c46475d4d3bde0618334ab44163
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 Free Software Foundation, Inc.
9 Contributed by Sebastian Pop <sebastian.pop@inria.fr>
10
11 This file is part of GCC.
12
13 GCC is free software; you can redistribute it and/or modify it under
14 the terms of the GNU General Public License as published by the Free
15 Software Foundation; either version 3, or (at your option) any later
16 version.
17
18 GCC is distributed in the hope that it will be useful, but WITHOUT ANY
19 WARRANTY; without even the implied warranty of MERCHANTABILITY or
20 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
21 for more details.
22
23 You should have received a copy of the GNU General Public License
24 along with GCC; see the file COPYING3. If not see
25 <http://www.gnu.org/licenses/>. */
26
27 /* For a detailed description, see "Constraint-Based Array Dependence
28 Analysis" William Pugh, David Wonnacott, TOPLAS'98 and David
29 Wonnacott's thesis:
30 ftp://ftp.cs.umd.edu/pub/omega/davewThesis/davewThesis.ps.gz
31 */
32
33 #include "config.h"
34 #include "system.h"
35 #include "coretypes.h"
36 #include "tm.h"
37 #include "errors.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);
1309
1310 omega_copy_problem (tmp_problem, pb);
1311 tmp_problem->safe_vars = 0;
1312 tmp_problem->num_subs = 0;
1313
1314 for (e = pb->num_geqs - 1; e >= 0; e--)
1315 if (pb->geqs[e].color == omega_red)
1316 {
1317 any_color = true;
1318 break;
1319 }
1320
1321 if (please_no_equalities_in_simplified_problems)
1322 any_color = true;
1323
1324 if (any_color)
1325 original_problem = no_problem;
1326 else
1327 original_problem = pb;
1328
1329 if (dump_file && (dump_flags & TDF_DETAILS))
1330 {
1331 fprintf (dump_file, "verifying problem");
1332
1333 if (any_color)
1334 fprintf (dump_file, " (color mode)");
1335
1336 fprintf (dump_file, " :\n");
1337 omega_print_problem (dump_file, pb);
1338 }
1339
1340 result = omega_solve_problem (tmp_problem, omega_unknown);
1341 original_problem = no_problem;
1342 free (tmp_problem);
1343
1344 if (dump_file && (dump_flags & TDF_DETAILS))
1345 {
1346 if (result != omega_false)
1347 fprintf (dump_file, "verified problem\n");
1348 else
1349 fprintf (dump_file, "disproved problem\n");
1350 omega_print_problem (dump_file, pb);
1351 }
1352
1353 return result;
1354 }
1355
1356 /* Add a new equality to problem PB at last position E. */
1357
1358 static void
1359 adding_equality_constraint (omega_pb pb, int e)
1360 {
1361 if (original_problem != no_problem
1362 && original_problem != pb
1363 && !conservative)
1364 {
1365 int i, j;
1366 int e2 = original_problem->num_eqs++;
1367
1368 if (dump_file && (dump_flags & TDF_DETAILS))
1369 fprintf (dump_file,
1370 "adding equality constraint %d to outer problem\n", e2);
1371 omega_init_eqn_zero (&original_problem->eqs[e2],
1372 original_problem->num_vars);
1373
1374 for (i = pb->num_vars; i >= 1; i--)
1375 {
1376 for (j = original_problem->num_vars; j >= 1; j--)
1377 if (original_problem->var[j] == pb->var[i])
1378 break;
1379
1380 if (j <= 0)
1381 {
1382 if (dump_file && (dump_flags & TDF_DETAILS))
1383 fprintf (dump_file, "retracting\n");
1384 original_problem->num_eqs--;
1385 return;
1386 }
1387 original_problem->eqs[e2].coef[j] = pb->eqs[e].coef[i];
1388 }
1389
1390 original_problem->eqs[e2].coef[0] = pb->eqs[e].coef[0];
1391
1392 if (dump_file && (dump_flags & TDF_DETAILS))
1393 omega_print_problem (dump_file, original_problem);
1394 }
1395 }
1396
1397 static int *fast_lookup;
1398 static int *fast_lookup_red;
1399
1400 typedef enum {
1401 normalize_false,
1402 normalize_uncoupled,
1403 normalize_coupled
1404 } normalize_return_type;
1405
1406 /* Normalizes PB by removing redundant constraints. Returns
1407 normalize_false when the constraints system has no solution,
1408 otherwise returns normalize_coupled or normalize_uncoupled. */
1409
1410 static normalize_return_type
1411 normalize_omega_problem (omega_pb pb)
1412 {
1413 int e, i, j, k, n_vars;
1414 int coupled_subscripts = 0;
1415
1416 n_vars = pb->num_vars;
1417
1418 for (e = 0; e < pb->num_geqs; e++)
1419 {
1420 if (!pb->geqs[e].touched)
1421 {
1422 if (!single_var_geq (&pb->geqs[e], n_vars))
1423 coupled_subscripts = 1;
1424 }
1425 else
1426 {
1427 int g, top_var, i0, hashCode;
1428 int *p = &packing[0];
1429
1430 for (k = 1; k <= n_vars; k++)
1431 if (pb->geqs[e].coef[k])
1432 *(p++) = k;
1433
1434 top_var = (p - &packing[0]) - 1;
1435
1436 if (top_var == -1)
1437 {
1438 if (pb->geqs[e].coef[0] < 0)
1439 {
1440 if (dump_file && (dump_flags & TDF_DETAILS))
1441 {
1442 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1443 fprintf (dump_file, "\nequations have no solution \n");
1444 }
1445 return normalize_false;
1446 }
1447
1448 omega_delete_geq (pb, e, n_vars);
1449 e--;
1450 continue;
1451 }
1452 else if (top_var == 0)
1453 {
1454 int singlevar = packing[0];
1455
1456 g = pb->geqs[e].coef[singlevar];
1457
1458 if (g > 0)
1459 {
1460 pb->geqs[e].coef[singlevar] = 1;
1461 pb->geqs[e].key = singlevar;
1462 }
1463 else
1464 {
1465 g = -g;
1466 pb->geqs[e].coef[singlevar] = -1;
1467 pb->geqs[e].key = -singlevar;
1468 }
1469
1470 if (g > 1)
1471 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1472 }
1473 else
1474 {
1475 int g2;
1476 int hash_key_multiplier = 31;
1477
1478 coupled_subscripts = 1;
1479 i0 = top_var;
1480 i = packing[i0--];
1481 g = pb->geqs[e].coef[i];
1482 hashCode = g * (i + 3);
1483
1484 if (g < 0)
1485 g = -g;
1486
1487 for (; i0 >= 0; i0--)
1488 {
1489 int x;
1490
1491 i = packing[i0];
1492 x = pb->geqs[e].coef[i];
1493 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1494
1495 if (x < 0)
1496 x = -x;
1497
1498 if (x == 1)
1499 {
1500 g = 1;
1501 i0--;
1502 break;
1503 }
1504 else
1505 g = gcd (x, g);
1506 }
1507
1508 for (; i0 >= 0; i0--)
1509 {
1510 int x;
1511 i = packing[i0];
1512 x = pb->geqs[e].coef[i];
1513 hashCode = hashCode * hash_key_multiplier * (i + 3) + x;
1514 }
1515
1516 if (g > 1)
1517 {
1518 pb->geqs[e].coef[0] = int_div (pb->geqs[e].coef[0], g);
1519 i0 = top_var;
1520 i = packing[i0--];
1521 pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1522 hashCode = pb->geqs[e].coef[i] * (i + 3);
1523
1524 for (; i0 >= 0; i0--)
1525 {
1526 i = packing[i0];
1527 pb->geqs[e].coef[i] = pb->geqs[e].coef[i] / g;
1528 hashCode = hashCode * hash_key_multiplier * (i + 3)
1529 + pb->geqs[e].coef[i];
1530 }
1531 }
1532
1533 g2 = abs (hashCode);
1534
1535 if (dump_file && (dump_flags & TDF_DETAILS))
1536 {
1537 fprintf (dump_file, "Hash code = %d, eqn = ", hashCode);
1538 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1539 fprintf (dump_file, "\n");
1540 }
1541
1542 j = g2 % HASH_TABLE_SIZE;
1543
1544 do {
1545 eqn proto = &(hash_master[j]);
1546
1547 if (proto->touched == g2)
1548 {
1549 if (proto->coef[0] == top_var)
1550 {
1551 if (hashCode >= 0)
1552 for (i0 = top_var; i0 >= 0; i0--)
1553 {
1554 i = packing[i0];
1555
1556 if (pb->geqs[e].coef[i] != proto->coef[i])
1557 break;
1558 }
1559 else
1560 for (i0 = top_var; i0 >= 0; i0--)
1561 {
1562 i = packing[i0];
1563
1564 if (pb->geqs[e].coef[i] != -proto->coef[i])
1565 break;
1566 }
1567
1568 if (i0 < 0)
1569 {
1570 if (hashCode >= 0)
1571 pb->geqs[e].key = proto->key;
1572 else
1573 pb->geqs[e].key = -proto->key;
1574 break;
1575 }
1576 }
1577 }
1578 else if (proto->touched < 0)
1579 {
1580 omega_init_eqn_zero (proto, pb->num_vars);
1581 if (hashCode >= 0)
1582 for (i0 = top_var; i0 >= 0; i0--)
1583 {
1584 i = packing[i0];
1585 proto->coef[i] = pb->geqs[e].coef[i];
1586 }
1587 else
1588 for (i0 = top_var; i0 >= 0; i0--)
1589 {
1590 i = packing[i0];
1591 proto->coef[i] = -pb->geqs[e].coef[i];
1592 }
1593
1594 proto->coef[0] = top_var;
1595 proto->touched = g2;
1596
1597 if (dump_file && (dump_flags & TDF_DETAILS))
1598 fprintf (dump_file, " constraint key = %d\n",
1599 next_key);
1600
1601 proto->key = next_key++;
1602
1603 /* Too many hash keys generated. */
1604 gcc_assert (proto->key <= MAX_KEYS);
1605
1606 if (hashCode >= 0)
1607 pb->geqs[e].key = proto->key;
1608 else
1609 pb->geqs[e].key = -proto->key;
1610
1611 break;
1612 }
1613
1614 j = (j + 1) % HASH_TABLE_SIZE;
1615 } while (1);
1616 }
1617
1618 pb->geqs[e].touched = 0;
1619 }
1620
1621 {
1622 int eKey = pb->geqs[e].key;
1623 int e2;
1624 if (e > 0)
1625 {
1626 int cTerm = pb->geqs[e].coef[0];
1627 e2 = fast_lookup[MAX_KEYS - eKey];
1628
1629 if (e2 < e && pb->geqs[e2].key == -eKey
1630 && pb->geqs[e2].color == omega_black)
1631 {
1632 if (pb->geqs[e2].coef[0] < -cTerm)
1633 {
1634 if (dump_file && (dump_flags & TDF_DETAILS))
1635 {
1636 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1637 fprintf (dump_file, "\n");
1638 omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1639 fprintf (dump_file,
1640 "\nequations have no solution \n");
1641 }
1642 return normalize_false;
1643 }
1644
1645 if (pb->geqs[e2].coef[0] == -cTerm
1646 && (create_color
1647 || pb->geqs[e].color == omega_black))
1648 {
1649 omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1650 pb->num_vars);
1651 if (pb->geqs[e].color == omega_black)
1652 adding_equality_constraint (pb, pb->num_eqs);
1653 pb->num_eqs++;
1654 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1655 }
1656 }
1657
1658 e2 = fast_lookup_red[MAX_KEYS - eKey];
1659
1660 if (e2 < e && pb->geqs[e2].key == -eKey
1661 && pb->geqs[e2].color == omega_red)
1662 {
1663 if (pb->geqs[e2].coef[0] < -cTerm)
1664 {
1665 if (dump_file && (dump_flags & TDF_DETAILS))
1666 {
1667 omega_print_geq (dump_file, pb, &pb->geqs[e]);
1668 fprintf (dump_file, "\n");
1669 omega_print_geq (dump_file, pb, &pb->geqs[e2]);
1670 fprintf (dump_file,
1671 "\nequations have no solution \n");
1672 }
1673 return normalize_false;
1674 }
1675
1676 if (pb->geqs[e2].coef[0] == -cTerm && create_color)
1677 {
1678 omega_copy_eqn (&pb->eqs[pb->num_eqs], &pb->geqs[e],
1679 pb->num_vars);
1680 pb->eqs[pb->num_eqs].color = omega_red;
1681 pb->num_eqs++;
1682 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
1683 }
1684 }
1685
1686 e2 = fast_lookup[MAX_KEYS + eKey];
1687
1688 if (e2 < e && pb->geqs[e2].key == eKey
1689 && pb->geqs[e2].color == omega_black)
1690 {
1691 if (pb->geqs[e2].coef[0] > cTerm)
1692 {
1693 if (pb->geqs[e].color == omega_black)
1694 {
1695 if (dump_file && (dump_flags & TDF_DETAILS))
1696 {
1697 fprintf (dump_file,
1698 "Removing Redundant Equation: ");
1699 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1700 fprintf (dump_file, "\n");
1701 fprintf (dump_file,
1702 "[a] Made Redundant by: ");
1703 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1704 fprintf (dump_file, "\n");
1705 }
1706 pb->geqs[e2].coef[0] = cTerm;
1707 omega_delete_geq (pb, e, n_vars);
1708 e--;
1709 continue;
1710 }
1711 }
1712 else
1713 {
1714 if (dump_file && (dump_flags & TDF_DETAILS))
1715 {
1716 fprintf (dump_file, "Removing Redundant Equation: ");
1717 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1718 fprintf (dump_file, "\n");
1719 fprintf (dump_file, "[b] Made Redundant by: ");
1720 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1721 fprintf (dump_file, "\n");
1722 }
1723 omega_delete_geq (pb, e, n_vars);
1724 e--;
1725 continue;
1726 }
1727 }
1728
1729 e2 = fast_lookup_red[MAX_KEYS + eKey];
1730
1731 if (e2 < e && pb->geqs[e2].key == eKey
1732 && pb->geqs[e2].color == omega_red)
1733 {
1734 if (pb->geqs[e2].coef[0] >= cTerm)
1735 {
1736 if (dump_file && (dump_flags & TDF_DETAILS))
1737 {
1738 fprintf (dump_file, "Removing Redundant Equation: ");
1739 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1740 fprintf (dump_file, "\n");
1741 fprintf (dump_file, "[c] Made Redundant by: ");
1742 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1743 fprintf (dump_file, "\n");
1744 }
1745 pb->geqs[e2].coef[0] = cTerm;
1746 pb->geqs[e2].color = pb->geqs[e].color;
1747 }
1748 else if (pb->geqs[e].color == omega_red)
1749 {
1750 if (dump_file && (dump_flags & TDF_DETAILS))
1751 {
1752 fprintf (dump_file, "Removing Redundant Equation: ");
1753 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
1754 fprintf (dump_file, "\n");
1755 fprintf (dump_file, "[d] Made Redundant by: ");
1756 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
1757 fprintf (dump_file, "\n");
1758 }
1759 }
1760 omega_delete_geq (pb, e, n_vars);
1761 e--;
1762 continue;
1763
1764 }
1765 }
1766
1767 if (pb->geqs[e].color == omega_red)
1768 fast_lookup_red[MAX_KEYS + eKey] = e;
1769 else
1770 fast_lookup[MAX_KEYS + eKey] = e;
1771 }
1772 }
1773
1774 create_color = false;
1775 return coupled_subscripts ? normalize_coupled : normalize_uncoupled;
1776 }
1777
1778 /* Divide the coefficients of EQN by their gcd. N_VARS is the number
1779 of variables in EQN. */
1780
1781 static inline void
1782 divide_eqn_by_gcd (eqn eqn, int n_vars)
1783 {
1784 int var, g = 0;
1785
1786 for (var = n_vars; var >= 0; var--)
1787 g = gcd (abs (eqn->coef[var]), g);
1788
1789 if (g)
1790 for (var = n_vars; var >= 0; var--)
1791 eqn->coef[var] = eqn->coef[var] / g;
1792 }
1793
1794 /* Rewrite some non-safe variables in function of protected
1795 wildcard variables. */
1796
1797 static void
1798 cleanout_wildcards (omega_pb pb)
1799 {
1800 int e, i, j;
1801 int n_vars = pb->num_vars;
1802 bool renormalize = false;
1803
1804 for (e = pb->num_eqs - 1; e >= 0; e--)
1805 for (i = n_vars; !omega_safe_var_p (pb, i); i--)
1806 if (pb->eqs[e].coef[i] != 0)
1807 {
1808 /* i is the last nonzero non-safe variable. */
1809
1810 for (j = i - 1; !omega_safe_var_p (pb, j); j--)
1811 if (pb->eqs[e].coef[j] != 0)
1812 break;
1813
1814 /* j is the next nonzero non-safe variable, or points
1815 to a safe variable: it is then a wildcard variable. */
1816
1817 /* Clean it out. */
1818 if (omega_safe_var_p (pb, j))
1819 {
1820 eqn sub = &(pb->eqs[e]);
1821 int c = pb->eqs[e].coef[i];
1822 int a = abs (c);
1823 int e2;
1824
1825 if (dump_file && (dump_flags & TDF_DETAILS))
1826 {
1827 fprintf (dump_file,
1828 "Found a single wild card equality: ");
1829 omega_print_eq (dump_file, pb, &pb->eqs[e]);
1830 fprintf (dump_file, "\n");
1831 omega_print_problem (dump_file, pb);
1832 }
1833
1834 for (e2 = pb->num_eqs - 1; e2 >= 0; e2--)
1835 if (e != e2 && pb->eqs[e2].coef[i]
1836 && (pb->eqs[e2].color == omega_red
1837 || (pb->eqs[e2].color == omega_black
1838 && pb->eqs[e].color == omega_black)))
1839 {
1840 eqn eqn = &(pb->eqs[e2]);
1841 int var, k;
1842
1843 for (var = n_vars; var >= 0; var--)
1844 eqn->coef[var] *= a;
1845
1846 k = eqn->coef[i];
1847
1848 for (var = n_vars; var >= 0; var--)
1849 eqn->coef[var] -= sub->coef[var] * k / c;
1850
1851 eqn->coef[i] = 0;
1852 divide_eqn_by_gcd (eqn, n_vars);
1853 }
1854
1855 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
1856 if (pb->geqs[e2].coef[i]
1857 && (pb->geqs[e2].color == omega_red
1858 || (pb->eqs[e].color == omega_black
1859 && pb->geqs[e2].color == omega_black)))
1860 {
1861 eqn eqn = &(pb->geqs[e2]);
1862 int var, k;
1863
1864 for (var = n_vars; var >= 0; var--)
1865 eqn->coef[var] *= a;
1866
1867 k = eqn->coef[i];
1868
1869 for (var = n_vars; var >= 0; var--)
1870 eqn->coef[var] -= sub->coef[var] * k / c;
1871
1872 eqn->coef[i] = 0;
1873 eqn->touched = 1;
1874 renormalize = true;
1875 }
1876
1877 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
1878 if (pb->subs[e2].coef[i]
1879 && (pb->subs[e2].color == omega_red
1880 || (pb->subs[e2].color == omega_black
1881 && pb->eqs[e].color == omega_black)))
1882 {
1883 eqn eqn = &(pb->subs[e2]);
1884 int var, k;
1885
1886 for (var = n_vars; var >= 0; var--)
1887 eqn->coef[var] *= a;
1888
1889 k = eqn->coef[i];
1890
1891 for (var = n_vars; var >= 0; var--)
1892 eqn->coef[var] -= sub->coef[var] * k / c;
1893
1894 eqn->coef[i] = 0;
1895 divide_eqn_by_gcd (eqn, n_vars);
1896 }
1897
1898 if (dump_file && (dump_flags & TDF_DETAILS))
1899 {
1900 fprintf (dump_file, "cleaned-out wildcard: ");
1901 omega_print_problem (dump_file, pb);
1902 }
1903 break;
1904 }
1905 }
1906
1907 if (renormalize)
1908 normalize_omega_problem (pb);
1909 }
1910
1911 /* Swap values contained in I and J. */
1912
1913 static inline void
1914 swap (int *i, int *j)
1915 {
1916 int tmp;
1917 tmp = *i;
1918 *i = *j;
1919 *j = tmp;
1920 }
1921
1922 /* Swap values contained in I and J. */
1923
1924 static inline void
1925 bswap (bool *i, bool *j)
1926 {
1927 bool tmp;
1928 tmp = *i;
1929 *i = *j;
1930 *j = tmp;
1931 }
1932
1933 /* Make variable IDX unprotected in PB, by swapping its index at the
1934 PB->safe_vars rank. */
1935
1936 static inline void
1937 omega_unprotect_1 (omega_pb pb, int *idx, bool *unprotect)
1938 {
1939 /* If IDX is protected... */
1940 if (*idx < pb->safe_vars)
1941 {
1942 /* ... swap its index with the last non protected index. */
1943 int j = pb->safe_vars;
1944 int e;
1945
1946 for (e = pb->num_geqs - 1; e >= 0; e--)
1947 {
1948 pb->geqs[e].touched = 1;
1949 swap (&pb->geqs[e].coef[*idx], &pb->geqs[e].coef[j]);
1950 }
1951
1952 for (e = pb->num_eqs - 1; e >= 0; e--)
1953 swap (&pb->eqs[e].coef[*idx], &pb->eqs[e].coef[j]);
1954
1955 for (e = pb->num_subs - 1; e >= 0; e--)
1956 swap (&pb->subs[e].coef[*idx], &pb->subs[e].coef[j]);
1957
1958 if (unprotect)
1959 bswap (&unprotect[*idx], &unprotect[j]);
1960
1961 swap (&pb->var[*idx], &pb->var[j]);
1962 pb->forwarding_address[pb->var[*idx]] = *idx;
1963 pb->forwarding_address[pb->var[j]] = j;
1964 (*idx)--;
1965 }
1966
1967 /* The variable at pb->safe_vars is also unprotected now. */
1968 pb->safe_vars--;
1969 }
1970
1971 /* During the Fourier-Motzkin elimination some variables are
1972 substituted with other variables. This function resurrects the
1973 substituted variables in PB. */
1974
1975 static void
1976 resurrect_subs (omega_pb pb)
1977 {
1978 if (pb->num_subs > 0
1979 && please_no_equalities_in_simplified_problems == 0)
1980 {
1981 int i, e, n, m;
1982
1983 if (dump_file && (dump_flags & TDF_DETAILS))
1984 {
1985 fprintf (dump_file,
1986 "problem reduced, bringing variables back to life\n");
1987 omega_print_problem (dump_file, pb);
1988 }
1989
1990 for (i = 1; omega_safe_var_p (pb, i); i++)
1991 if (omega_wildcard_p (pb, i))
1992 omega_unprotect_1 (pb, &i, NULL);
1993
1994 m = pb->num_subs;
1995 n = MAX (pb->num_vars, pb->safe_vars + m);
1996
1997 for (e = pb->num_geqs - 1; e >= 0; e--)
1998 if (single_var_geq (&pb->geqs[e], pb->num_vars))
1999 {
2000 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
2001 pb->geqs[e].key += (pb->geqs[e].key > 0 ? m : -m);
2002 }
2003 else
2004 {
2005 pb->geqs[e].touched = 1;
2006 pb->geqs[e].key = 0;
2007 }
2008
2009 for (i = pb->num_vars; !omega_safe_var_p (pb, i); i--)
2010 {
2011 pb->var[i + m] = pb->var[i];
2012
2013 for (e = pb->num_geqs - 1; e >= 0; e--)
2014 pb->geqs[e].coef[i + m] = pb->geqs[e].coef[i];
2015
2016 for (e = pb->num_eqs - 1; e >= 0; e--)
2017 pb->eqs[e].coef[i + m] = pb->eqs[e].coef[i];
2018
2019 for (e = pb->num_subs - 1; e >= 0; e--)
2020 pb->subs[e].coef[i + m] = pb->subs[e].coef[i];
2021 }
2022
2023 for (i = pb->safe_vars + m; !omega_safe_var_p (pb, i); i--)
2024 {
2025 for (e = pb->num_geqs - 1; e >= 0; e--)
2026 pb->geqs[e].coef[i] = 0;
2027
2028 for (e = pb->num_eqs - 1; e >= 0; e--)
2029 pb->eqs[e].coef[i] = 0;
2030
2031 for (e = pb->num_subs - 1; e >= 0; e--)
2032 pb->subs[e].coef[i] = 0;
2033 }
2034
2035 pb->num_vars += m;
2036
2037 for (e = pb->num_subs - 1; e >= 0; e--)
2038 {
2039 pb->var[pb->safe_vars + 1 + e] = pb->subs[e].key;
2040 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e]),
2041 pb->num_vars);
2042 pb->eqs[pb->num_eqs].coef[pb->safe_vars + 1 + e] = -1;
2043 pb->eqs[pb->num_eqs].color = omega_black;
2044
2045 if (dump_file && (dump_flags & TDF_DETAILS))
2046 {
2047 fprintf (dump_file, "brought back: ");
2048 omega_print_eq (dump_file, pb, &pb->eqs[pb->num_eqs]);
2049 fprintf (dump_file, "\n");
2050 }
2051
2052 pb->num_eqs++;
2053 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2054 }
2055
2056 pb->safe_vars += m;
2057 pb->num_subs = 0;
2058
2059 if (dump_file && (dump_flags & TDF_DETAILS))
2060 {
2061 fprintf (dump_file, "variables brought back to life\n");
2062 omega_print_problem (dump_file, pb);
2063 }
2064
2065 cleanout_wildcards (pb);
2066 }
2067 }
2068
2069 static inline bool
2070 implies (unsigned int a, unsigned int b)
2071 {
2072 return (a == (a & b));
2073 }
2074
2075 /* Eliminate redundant equations in PB. When EXPENSIVE is true, an
2076 extra step is performed. Returns omega_false when there exist no
2077 solution, omega_true otherwise. */
2078
2079 enum omega_result
2080 omega_eliminate_redundant (omega_pb pb, bool expensive)
2081 {
2082 int c, e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3;
2083 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2084 omega_pb tmp_problem;
2085
2086 /* {P,Z,N}EQS = {Positive,Zero,Negative} Equations. */
2087 unsigned int *peqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2088 unsigned int *zeqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2089 unsigned int *neqs = XNEWVEC (unsigned int, OMEGA_MAX_GEQS);
2090
2091 /* PP = Possible Positives, PZ = Possible Zeros, PN = Possible Negatives */
2092 unsigned int pp, pz, pn;
2093
2094 if (dump_file && (dump_flags & TDF_DETAILS))
2095 {
2096 fprintf (dump_file, "in eliminate Redundant:\n");
2097 omega_print_problem (dump_file, pb);
2098 }
2099
2100 for (e = pb->num_geqs - 1; e >= 0; e--)
2101 {
2102 int tmp = 1;
2103
2104 is_dead[e] = false;
2105 peqs[e] = zeqs[e] = neqs[e] = 0;
2106
2107 for (i = pb->num_vars; i >= 1; i--)
2108 {
2109 if (pb->geqs[e].coef[i] > 0)
2110 peqs[e] |= tmp;
2111 else if (pb->geqs[e].coef[i] < 0)
2112 neqs[e] |= tmp;
2113 else
2114 zeqs[e] |= tmp;
2115
2116 tmp <<= 1;
2117 }
2118 }
2119
2120
2121 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2122 if (!is_dead[e1])
2123 for (e2 = e1 - 1; e2 >= 0; e2--)
2124 if (!is_dead[e2])
2125 {
2126 for (p = pb->num_vars; p > 1; p--)
2127 for (q = p - 1; q > 0; q--)
2128 if ((alpha = pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q]
2129 - pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]) != 0)
2130 goto foundPQ;
2131
2132 continue;
2133
2134 foundPQ:
2135 pz = ((zeqs[e1] & zeqs[e2]) | (peqs[e1] & neqs[e2])
2136 | (neqs[e1] & peqs[e2]));
2137 pp = peqs[e1] | peqs[e2];
2138 pn = neqs[e1] | neqs[e2];
2139
2140 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2141 if (e3 != e1 && e3 != e2)
2142 {
2143 if (!implies (zeqs[e3], pz))
2144 goto nextE3;
2145
2146 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2147 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2148 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2149 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2150 alpha3 = alpha;
2151
2152 if (alpha1 * alpha2 <= 0)
2153 goto nextE3;
2154
2155 if (alpha1 < 0)
2156 {
2157 alpha1 = -alpha1;
2158 alpha2 = -alpha2;
2159 alpha3 = -alpha3;
2160 }
2161
2162 if (alpha3 > 0)
2163 {
2164 /* Trying to prove e3 is redundant. */
2165 if (!implies (peqs[e3], pp)
2166 || !implies (neqs[e3], pn))
2167 goto nextE3;
2168
2169 if (pb->geqs[e3].color == omega_black
2170 && (pb->geqs[e1].color == omega_red
2171 || pb->geqs[e2].color == omega_red))
2172 goto nextE3;
2173
2174 for (k = pb->num_vars; k >= 1; k--)
2175 if (alpha3 * pb->geqs[e3].coef[k]
2176 != (alpha1 * pb->geqs[e1].coef[k]
2177 + alpha2 * pb->geqs[e2].coef[k]))
2178 goto nextE3;
2179
2180 c = (alpha1 * pb->geqs[e1].coef[0]
2181 + alpha2 * pb->geqs[e2].coef[0]);
2182
2183 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2184 {
2185 if (dump_file && (dump_flags & TDF_DETAILS))
2186 {
2187 fprintf (dump_file,
2188 "found redundant inequality\n");
2189 fprintf (dump_file,
2190 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2191 alpha1, alpha2, alpha3);
2192
2193 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2194 fprintf (dump_file, "\n");
2195 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2196 fprintf (dump_file, "\n=> ");
2197 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2198 fprintf (dump_file, "\n\n");
2199 }
2200
2201 is_dead[e3] = true;
2202 }
2203 }
2204 else
2205 {
2206 /* Trying to prove e3 <= 0 and therefore e3 = 0,
2207 or trying to prove e3 < 0, and therefore the
2208 problem has no solutions. */
2209 if (!implies (peqs[e3], pn)
2210 || !implies (neqs[e3], pp))
2211 goto nextE3;
2212
2213 if (pb->geqs[e1].color == omega_red
2214 || pb->geqs[e2].color == omega_red
2215 || pb->geqs[e3].color == omega_red)
2216 goto nextE3;
2217
2218 alpha3 = alpha3;
2219 /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
2220 for (k = pb->num_vars; k >= 1; k--)
2221 if (alpha3 * pb->geqs[e3].coef[k]
2222 != (alpha1 * pb->geqs[e1].coef[k]
2223 + alpha2 * pb->geqs[e2].coef[k]))
2224 goto nextE3;
2225
2226 c = (alpha1 * pb->geqs[e1].coef[0]
2227 + alpha2 * pb->geqs[e2].coef[0]);
2228
2229 if (c < alpha3 * (pb->geqs[e3].coef[0]))
2230 {
2231 /* We just proved e3 < 0, so no solutions exist. */
2232 if (dump_file && (dump_flags & TDF_DETAILS))
2233 {
2234 fprintf (dump_file,
2235 "found implied over tight inequality\n");
2236 fprintf (dump_file,
2237 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2238 alpha1, alpha2, -alpha3);
2239 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2240 fprintf (dump_file, "\n");
2241 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2242 fprintf (dump_file, "\n=> not ");
2243 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2244 fprintf (dump_file, "\n\n");
2245 }
2246 free (is_dead);
2247 free (peqs);
2248 free (zeqs);
2249 free (neqs);
2250 return omega_false;
2251 }
2252 else if (c < alpha3 * (pb->geqs[e3].coef[0] - 1))
2253 {
2254 /* We just proved that e3 <=0, so e3 = 0. */
2255 if (dump_file && (dump_flags & TDF_DETAILS))
2256 {
2257 fprintf (dump_file,
2258 "found implied tight inequality\n");
2259 fprintf (dump_file,
2260 "alpha1, alpha2, alpha3 = %d,%d,%d\n",
2261 alpha1, alpha2, -alpha3);
2262 omega_print_geq (dump_file, pb, &(pb->geqs[e1]));
2263 fprintf (dump_file, "\n");
2264 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2265 fprintf (dump_file, "\n=> inverse ");
2266 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2267 fprintf (dump_file, "\n\n");
2268 }
2269
2270 omega_copy_eqn (&pb->eqs[pb->num_eqs++],
2271 &pb->geqs[e3], pb->num_vars);
2272 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2273 adding_equality_constraint (pb, pb->num_eqs - 1);
2274 is_dead[e3] = true;
2275 }
2276 }
2277 nextE3:;
2278 }
2279 }
2280
2281 /* Delete the inequalities that were marked as dead. */
2282 for (e = pb->num_geqs - 1; e >= 0; e--)
2283 if (is_dead[e])
2284 omega_delete_geq (pb, e, pb->num_vars);
2285
2286 if (!expensive)
2287 goto eliminate_redundant_done;
2288
2289 tmp_problem = XNEW (struct omega_pb);
2290 conservative++;
2291
2292 for (e = pb->num_geqs - 1; e >= 0; e--)
2293 {
2294 if (dump_file && (dump_flags & TDF_DETAILS))
2295 {
2296 fprintf (dump_file,
2297 "checking equation %d to see if it is redundant: ", e);
2298 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2299 fprintf (dump_file, "\n");
2300 }
2301
2302 omega_copy_problem (tmp_problem, pb);
2303 omega_negate_geq (tmp_problem, e);
2304 tmp_problem->safe_vars = 0;
2305 tmp_problem->variables_freed = false;
2306
2307 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2308 omega_delete_geq (pb, e, pb->num_vars);
2309 }
2310
2311 free (tmp_problem);
2312 conservative--;
2313
2314 if (!omega_reduce_with_subs)
2315 {
2316 resurrect_subs (pb);
2317 gcc_assert (please_no_equalities_in_simplified_problems
2318 || pb->num_subs == 0);
2319 }
2320
2321 eliminate_redundant_done:
2322 free (is_dead);
2323 free (peqs);
2324 free (zeqs);
2325 free (neqs);
2326 return omega_true;
2327 }
2328
2329 /* For each inequality that has coefficients bigger than 20, try to
2330 create a new constraint that cannot be derived from the original
2331 constraint and that has smaller coefficients. Add the new
2332 constraint at the end of geqs. Return the number of inequalities
2333 that have been added to PB. */
2334
2335 static int
2336 smooth_weird_equations (omega_pb pb)
2337 {
2338 int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
2339 int c;
2340 int v;
2341 int result = 0;
2342
2343 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
2344 if (pb->geqs[e1].color == omega_black)
2345 {
2346 int g = 999999;
2347
2348 for (v = pb->num_vars; v >= 1; v--)
2349 if (pb->geqs[e1].coef[v] != 0 && abs (pb->geqs[e1].coef[v]) < g)
2350 g = abs (pb->geqs[e1].coef[v]);
2351
2352 /* Magic number. */
2353 if (g > 20)
2354 {
2355 e3 = pb->num_geqs;
2356
2357 for (v = pb->num_vars; v >= 1; v--)
2358 pb->geqs[e3].coef[v] = int_div (6 * pb->geqs[e1].coef[v] + g / 2,
2359 g);
2360
2361 pb->geqs[e3].color = omega_black;
2362 pb->geqs[e3].touched = 1;
2363 /* Magic number. */
2364 pb->geqs[e3].coef[0] = 9997;
2365
2366 if (dump_file && (dump_flags & TDF_DETAILS))
2367 {
2368 fprintf (dump_file, "Checking to see if we can derive: ");
2369 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2370 fprintf (dump_file, "\n from: ");
2371 omega_print_geq (dump_file, pb, &pb->geqs[e1]);
2372 fprintf (dump_file, "\n");
2373 }
2374
2375 for (e2 = pb->num_geqs - 1; e2 >= 0; e2--)
2376 if (e1 != e2 && pb->geqs[e2].color == omega_black)
2377 {
2378 for (p = pb->num_vars; p > 1; p--)
2379 {
2380 for (q = p - 1; q > 0; q--)
2381 {
2382 alpha =
2383 (pb->geqs[e1].coef[p] * pb->geqs[e2].coef[q] -
2384 pb->geqs[e2].coef[p] * pb->geqs[e1].coef[q]);
2385 if (alpha != 0)
2386 goto foundPQ;
2387 }
2388 }
2389 continue;
2390
2391 foundPQ:
2392
2393 alpha1 = (pb->geqs[e2].coef[q] * pb->geqs[e3].coef[p]
2394 - pb->geqs[e2].coef[p] * pb->geqs[e3].coef[q]);
2395 alpha2 = -(pb->geqs[e1].coef[q] * pb->geqs[e3].coef[p]
2396 - pb->geqs[e1].coef[p] * pb->geqs[e3].coef[q]);
2397 alpha3 = alpha;
2398
2399 if (alpha1 * alpha2 <= 0)
2400 continue;
2401
2402 if (alpha1 < 0)
2403 {
2404 alpha1 = -alpha1;
2405 alpha2 = -alpha2;
2406 alpha3 = -alpha3;
2407 }
2408
2409 if (alpha3 > 0)
2410 {
2411 /* Try to prove e3 is redundant: verify
2412 alpha1*v1 + alpha2*v2 = alpha3*v3. */
2413 for (k = pb->num_vars; k >= 1; k--)
2414 if (alpha3 * pb->geqs[e3].coef[k]
2415 != (alpha1 * pb->geqs[e1].coef[k]
2416 + alpha2 * pb->geqs[e2].coef[k]))
2417 goto nextE2;
2418
2419 c = alpha1 * pb->geqs[e1].coef[0]
2420 + alpha2 * pb->geqs[e2].coef[0];
2421
2422 if (c < alpha3 * (pb->geqs[e3].coef[0] + 1))
2423 pb->geqs[e3].coef[0] = int_div (c, alpha3);
2424 }
2425 nextE2:;
2426 }
2427
2428 if (pb->geqs[e3].coef[0] < 9997)
2429 {
2430 result++;
2431 pb->num_geqs++;
2432
2433 if (dump_file && (dump_flags & TDF_DETAILS))
2434 {
2435 fprintf (dump_file,
2436 "Smoothing wierd equations; adding:\n");
2437 omega_print_geq (dump_file, pb, &pb->geqs[e3]);
2438 fprintf (dump_file, "\nto:\n");
2439 omega_print_problem (dump_file, pb);
2440 fprintf (dump_file, "\n\n");
2441 }
2442 }
2443 }
2444 }
2445 return result;
2446 }
2447
2448 /* Replace tuples of inequalities, that define upper and lower half
2449 spaces, with an equation. */
2450
2451 static void
2452 coalesce (omega_pb pb)
2453 {
2454 int e, e2;
2455 int colors = 0;
2456 bool *is_dead;
2457 int found_something = 0;
2458
2459 for (e = 0; e < pb->num_geqs; e++)
2460 if (pb->geqs[e].color == omega_red)
2461 colors++;
2462
2463 if (colors < 2)
2464 return;
2465
2466 is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2467
2468 for (e = 0; e < pb->num_geqs; e++)
2469 is_dead[e] = false;
2470
2471 for (e = 0; e < pb->num_geqs; e++)
2472 if (pb->geqs[e].color == omega_red
2473 && !pb->geqs[e].touched)
2474 for (e2 = e + 1; e2 < pb->num_geqs; e2++)
2475 if (!pb->geqs[e2].touched
2476 && pb->geqs[e].key == -pb->geqs[e2].key
2477 && pb->geqs[e].coef[0] == -pb->geqs[e2].coef[0]
2478 && pb->geqs[e2].color == omega_red)
2479 {
2480 omega_copy_eqn (&pb->eqs[pb->num_eqs++], &pb->geqs[e],
2481 pb->num_vars);
2482 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
2483 found_something++;
2484 is_dead[e] = true;
2485 is_dead[e2] = true;
2486 }
2487
2488 for (e = pb->num_geqs - 1; e >= 0; e--)
2489 if (is_dead[e])
2490 omega_delete_geq (pb, e, pb->num_vars);
2491
2492 if (dump_file && (dump_flags & TDF_DETAILS) && found_something)
2493 {
2494 fprintf (dump_file, "Coalesced pb->geqs into %d EQ's:\n",
2495 found_something);
2496 omega_print_problem (dump_file, pb);
2497 }
2498
2499 free (is_dead);
2500 }
2501
2502 /* Eliminate red inequalities from PB. When ELIMINATE_ALL is
2503 true, continue to eliminate all the red inequalities. */
2504
2505 void
2506 omega_eliminate_red (omega_pb pb, bool eliminate_all)
2507 {
2508 int e, e2, e3, i, j, k, a, alpha1, alpha2;
2509 int c = 0;
2510 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
2511 int dead_count = 0;
2512 int red_found;
2513 omega_pb tmp_problem;
2514
2515 if (dump_file && (dump_flags & TDF_DETAILS))
2516 {
2517 fprintf (dump_file, "in eliminate RED:\n");
2518 omega_print_problem (dump_file, pb);
2519 }
2520
2521 if (pb->num_eqs > 0)
2522 omega_simplify_problem (pb);
2523
2524 for (e = pb->num_geqs - 1; e >= 0; e--)
2525 is_dead[e] = false;
2526
2527 for (e = pb->num_geqs - 1; e >= 0; e--)
2528 if (pb->geqs[e].color == omega_black && !is_dead[e])
2529 for (e2 = e - 1; e2 >= 0; e2--)
2530 if (pb->geqs[e2].color == omega_black
2531 && !is_dead[e2])
2532 {
2533 a = 0;
2534
2535 for (i = pb->num_vars; i > 1; i--)
2536 for (j = i - 1; j > 0; j--)
2537 if ((a = (pb->geqs[e].coef[i] * pb->geqs[e2].coef[j]
2538 - pb->geqs[e2].coef[i] * pb->geqs[e].coef[j])) != 0)
2539 goto found_pair;
2540
2541 continue;
2542
2543 found_pair:
2544 if (dump_file && (dump_flags & TDF_DETAILS))
2545 {
2546 fprintf (dump_file,
2547 "found two equations to combine, i = %s, ",
2548 omega_variable_to_str (pb, i));
2549 fprintf (dump_file, "j = %s, alpha = %d\n",
2550 omega_variable_to_str (pb, j), a);
2551 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2552 fprintf (dump_file, "\n");
2553 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2554 fprintf (dump_file, "\n");
2555 }
2556
2557 for (e3 = pb->num_geqs - 1; e3 >= 0; e3--)
2558 if (pb->geqs[e3].color == omega_red)
2559 {
2560 alpha1 = (pb->geqs[e2].coef[j] * pb->geqs[e3].coef[i]
2561 - pb->geqs[e2].coef[i] * pb->geqs[e3].coef[j]);
2562 alpha2 = -(pb->geqs[e].coef[j] * pb->geqs[e3].coef[i]
2563 - pb->geqs[e].coef[i] * pb->geqs[e3].coef[j]);
2564
2565 if ((a > 0 && alpha1 > 0 && alpha2 > 0)
2566 || (a < 0 && alpha1 < 0 && alpha2 < 0))
2567 {
2568 if (dump_file && (dump_flags & TDF_DETAILS))
2569 {
2570 fprintf (dump_file,
2571 "alpha1 = %d, alpha2 = %d;"
2572 "comparing against: ",
2573 alpha1, alpha2);
2574 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2575 fprintf (dump_file, "\n");
2576 }
2577
2578 for (k = pb->num_vars; k >= 0; k--)
2579 {
2580 c = (alpha1 * pb->geqs[e].coef[k]
2581 + alpha2 * pb->geqs[e2].coef[k]);
2582
2583 if (c != a * pb->geqs[e3].coef[k])
2584 break;
2585
2586 if (dump_file && (dump_flags & TDF_DETAILS) && k > 0)
2587 fprintf (dump_file, " %s: %d, %d\n",
2588 omega_variable_to_str (pb, k), c,
2589 a * pb->geqs[e3].coef[k]);
2590 }
2591
2592 if (k < 0
2593 || (k == 0 &&
2594 ((a > 0 && c < a * pb->geqs[e3].coef[k])
2595 || (a < 0 && c > a * pb->geqs[e3].coef[k]))))
2596 {
2597 if (dump_file && (dump_flags & TDF_DETAILS))
2598 {
2599 dead_count++;
2600 fprintf (dump_file,
2601 "red equation#%d is dead "
2602 "(%d dead so far, %d remain)\n",
2603 e3, dead_count,
2604 pb->num_geqs - dead_count);
2605 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2606 fprintf (dump_file, "\n");
2607 omega_print_geq (dump_file, pb, &(pb->geqs[e2]));
2608 fprintf (dump_file, "\n");
2609 omega_print_geq (dump_file, pb, &(pb->geqs[e3]));
2610 fprintf (dump_file, "\n");
2611 }
2612 is_dead[e3] = true;
2613 }
2614 }
2615 }
2616 }
2617
2618 for (e = pb->num_geqs - 1; e >= 0; e--)
2619 if (is_dead[e])
2620 omega_delete_geq (pb, e, pb->num_vars);
2621
2622 free (is_dead);
2623
2624 if (dump_file && (dump_flags & TDF_DETAILS))
2625 {
2626 fprintf (dump_file, "in eliminate RED, easy tests done:\n");
2627 omega_print_problem (dump_file, pb);
2628 }
2629
2630 for (red_found = 0, e = pb->num_geqs - 1; e >= 0; e--)
2631 if (pb->geqs[e].color == omega_red)
2632 red_found = 1;
2633
2634 if (!red_found)
2635 {
2636 if (dump_file && (dump_flags & TDF_DETAILS))
2637 fprintf (dump_file, "fast checks worked\n");
2638
2639 if (!omega_reduce_with_subs)
2640 gcc_assert (please_no_equalities_in_simplified_problems
2641 || pb->num_subs == 0);
2642
2643 return;
2644 }
2645
2646 if (!omega_verify_simplification
2647 && verify_omega_pb (pb) == omega_false)
2648 return;
2649
2650 conservative++;
2651 tmp_problem = XNEW (struct omega_pb);
2652
2653 for (e = pb->num_geqs - 1; e >= 0; e--)
2654 if (pb->geqs[e].color == omega_red)
2655 {
2656 if (dump_file && (dump_flags & TDF_DETAILS))
2657 {
2658 fprintf (dump_file,
2659 "checking equation %d to see if it is redundant: ", e);
2660 omega_print_geq (dump_file, pb, &(pb->geqs[e]));
2661 fprintf (dump_file, "\n");
2662 }
2663
2664 omega_copy_problem (tmp_problem, pb);
2665 omega_negate_geq (tmp_problem, e);
2666 tmp_problem->safe_vars = 0;
2667 tmp_problem->variables_freed = false;
2668 tmp_problem->num_subs = 0;
2669
2670 if (omega_solve_problem (tmp_problem, omega_false) == omega_false)
2671 {
2672 if (dump_file && (dump_flags & TDF_DETAILS))
2673 fprintf (dump_file, "it is redundant\n");
2674 omega_delete_geq (pb, e, pb->num_vars);
2675 }
2676 else
2677 {
2678 if (dump_file && (dump_flags & TDF_DETAILS))
2679 fprintf (dump_file, "it is not redundant\n");
2680
2681 if (!eliminate_all)
2682 {
2683 if (dump_file && (dump_flags & TDF_DETAILS))
2684 fprintf (dump_file, "no need to check other red equations\n");
2685 break;
2686 }
2687 }
2688 }
2689
2690 conservative--;
2691 free (tmp_problem);
2692 /* omega_simplify_problem (pb); */
2693
2694 if (!omega_reduce_with_subs)
2695 gcc_assert (please_no_equalities_in_simplified_problems
2696 || pb->num_subs == 0);
2697 }
2698
2699 /* Transform some wildcard variables to non-safe variables. */
2700
2701 static void
2702 chain_unprotect (omega_pb pb)
2703 {
2704 int i, e;
2705 bool *unprotect = XNEWVEC (bool, OMEGA_MAX_VARS);
2706
2707 for (i = 1; omega_safe_var_p (pb, i); i++)
2708 {
2709 unprotect[i] = omega_wildcard_p (pb, i);
2710
2711 for (e = pb->num_subs - 1; e >= 0; e--)
2712 if (pb->subs[e].coef[i])
2713 unprotect[i] = false;
2714 }
2715
2716 if (dump_file && (dump_flags & TDF_DETAILS))
2717 {
2718 fprintf (dump_file, "Doing chain reaction unprotection\n");
2719 omega_print_problem (dump_file, pb);
2720
2721 for (i = 1; omega_safe_var_p (pb, i); i++)
2722 if (unprotect[i])
2723 fprintf (dump_file, "unprotecting %s\n",
2724 omega_variable_to_str (pb, i));
2725 }
2726
2727 for (i = 1; omega_safe_var_p (pb, i); i++)
2728 if (unprotect[i])
2729 omega_unprotect_1 (pb, &i, unprotect);
2730
2731 if (dump_file && (dump_flags & TDF_DETAILS))
2732 {
2733 fprintf (dump_file, "After chain reactions\n");
2734 omega_print_problem (dump_file, pb);
2735 }
2736
2737 free (unprotect);
2738 }
2739
2740 /* Reduce problem PB. */
2741
2742 static void
2743 omega_problem_reduced (omega_pb pb)
2744 {
2745 if (omega_verify_simplification
2746 && !in_approximate_mode
2747 && verify_omega_pb (pb) == omega_false)
2748 return;
2749
2750 if (PARAM_VALUE (PARAM_OMEGA_ELIMINATE_REDUNDANT_CONSTRAINTS)
2751 && !omega_eliminate_redundant (pb, true))
2752 return;
2753
2754 omega_found_reduction = omega_true;
2755
2756 if (!please_no_equalities_in_simplified_problems)
2757 coalesce (pb);
2758
2759 if (omega_reduce_with_subs
2760 || please_no_equalities_in_simplified_problems)
2761 chain_unprotect (pb);
2762 else
2763 resurrect_subs (pb);
2764
2765 if (!return_single_result)
2766 {
2767 int i;
2768
2769 for (i = 1; omega_safe_var_p (pb, i); i++)
2770 pb->forwarding_address[pb->var[i]] = i;
2771
2772 for (i = 0; i < pb->num_subs; i++)
2773 pb->forwarding_address[pb->subs[i].key] = -i - 1;
2774
2775 (*omega_when_reduced) (pb);
2776 }
2777
2778 if (dump_file && (dump_flags & TDF_DETAILS))
2779 {
2780 fprintf (dump_file, "-------------------------------------------\n");
2781 fprintf (dump_file, "problem reduced:\n");
2782 omega_print_problem (dump_file, pb);
2783 fprintf (dump_file, "-------------------------------------------\n");
2784 }
2785 }
2786
2787 /* Eliminates all the free variables for problem PB, that is all the
2788 variables from FV to PB->NUM_VARS. */
2789
2790 static void
2791 omega_free_eliminations (omega_pb pb, int fv)
2792 {
2793 bool try_again = true;
2794 int i, e, e2;
2795 int n_vars = pb->num_vars;
2796
2797 while (try_again)
2798 {
2799 try_again = false;
2800
2801 for (i = n_vars; i > fv; i--)
2802 {
2803 for (e = pb->num_geqs - 1; e >= 0; e--)
2804 if (pb->geqs[e].coef[i])
2805 break;
2806
2807 if (e < 0)
2808 e2 = e;
2809 else if (pb->geqs[e].coef[i] > 0)
2810 {
2811 for (e2 = e - 1; e2 >= 0; e2--)
2812 if (pb->geqs[e2].coef[i] < 0)
2813 break;
2814 }
2815 else
2816 {
2817 for (e2 = e - 1; e2 >= 0; e2--)
2818 if (pb->geqs[e2].coef[i] > 0)
2819 break;
2820 }
2821
2822 if (e2 < 0)
2823 {
2824 int e3;
2825 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2826 if (pb->subs[e3].coef[i])
2827 break;
2828
2829 if (e3 >= 0)
2830 continue;
2831
2832 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2833 if (pb->eqs[e3].coef[i])
2834 break;
2835
2836 if (e3 >= 0)
2837 continue;
2838
2839 if (dump_file && (dump_flags & TDF_DETAILS))
2840 fprintf (dump_file, "a free elimination of %s\n",
2841 omega_variable_to_str (pb, i));
2842
2843 if (e >= 0)
2844 {
2845 omega_delete_geq (pb, e, n_vars);
2846
2847 for (e--; e >= 0; e--)
2848 if (pb->geqs[e].coef[i])
2849 omega_delete_geq (pb, e, n_vars);
2850
2851 try_again = (i < n_vars);
2852 }
2853
2854 omega_delete_variable (pb, i);
2855 n_vars = pb->num_vars;
2856 }
2857 }
2858 }
2859
2860 if (dump_file && (dump_flags & TDF_DETAILS))
2861 {
2862 fprintf (dump_file, "\nafter free eliminations:\n");
2863 omega_print_problem (dump_file, pb);
2864 fprintf (dump_file, "\n");
2865 }
2866 }
2867
2868 /* Do free red eliminations. */
2869
2870 static void
2871 free_red_eliminations (omega_pb pb)
2872 {
2873 bool try_again = true;
2874 int i, e, e2;
2875 int n_vars = pb->num_vars;
2876 bool *is_red_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2877 bool *is_dead_var = XNEWVEC (bool, OMEGA_MAX_VARS);
2878 bool *is_dead_geq = XNEWVEC (bool, OMEGA_MAX_GEQS);
2879
2880 for (i = n_vars; i > 0; i--)
2881 {
2882 is_red_var[i] = false;
2883 is_dead_var[i] = false;
2884 }
2885
2886 for (e = pb->num_geqs - 1; e >= 0; e--)
2887 {
2888 is_dead_geq[e] = false;
2889
2890 if (pb->geqs[e].color == omega_red)
2891 for (i = n_vars; i > 0; i--)
2892 if (pb->geqs[e].coef[i] != 0)
2893 is_red_var[i] = true;
2894 }
2895
2896 while (try_again)
2897 {
2898 try_again = false;
2899 for (i = n_vars; i > 0; i--)
2900 if (!is_red_var[i] && !is_dead_var[i])
2901 {
2902 for (e = pb->num_geqs - 1; e >= 0; e--)
2903 if (!is_dead_geq[e] && pb->geqs[e].coef[i])
2904 break;
2905
2906 if (e < 0)
2907 e2 = e;
2908 else if (pb->geqs[e].coef[i] > 0)
2909 {
2910 for (e2 = e - 1; e2 >= 0; e2--)
2911 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] < 0)
2912 break;
2913 }
2914 else
2915 {
2916 for (e2 = e - 1; e2 >= 0; e2--)
2917 if (!is_dead_geq[e2] && pb->geqs[e2].coef[i] > 0)
2918 break;
2919 }
2920
2921 if (e2 < 0)
2922 {
2923 int e3;
2924 for (e3 = pb->num_subs - 1; e3 >= 0; e3--)
2925 if (pb->subs[e3].coef[i])
2926 break;
2927
2928 if (e3 >= 0)
2929 continue;
2930
2931 for (e3 = pb->num_eqs - 1; e3 >= 0; e3--)
2932 if (pb->eqs[e3].coef[i])
2933 break;
2934
2935 if (e3 >= 0)
2936 continue;
2937
2938 if (dump_file && (dump_flags & TDF_DETAILS))
2939 fprintf (dump_file, "a free red elimination of %s\n",
2940 omega_variable_to_str (pb, i));
2941
2942 for (; e >= 0; e--)
2943 if (pb->geqs[e].coef[i])
2944 is_dead_geq[e] = true;
2945
2946 try_again = true;
2947 is_dead_var[i] = true;
2948 }
2949 }
2950 }
2951
2952 for (e = pb->num_geqs - 1; e >= 0; e--)
2953 if (is_dead_geq[e])
2954 omega_delete_geq (pb, e, n_vars);
2955
2956 for (i = n_vars; i > 0; i--)
2957 if (is_dead_var[i])
2958 omega_delete_variable (pb, i);
2959
2960 if (dump_file && (dump_flags & TDF_DETAILS))
2961 {
2962 fprintf (dump_file, "\nafter free red eliminations:\n");
2963 omega_print_problem (dump_file, pb);
2964 fprintf (dump_file, "\n");
2965 }
2966
2967 free (is_red_var);
2968 free (is_dead_var);
2969 free (is_dead_geq);
2970 }
2971
2972 /* For equation EQ of the form "0 = EQN", insert in PB two
2973 inequalities "0 <= EQN" and "0 <= -EQN". */
2974
2975 void
2976 omega_convert_eq_to_geqs (omega_pb pb, int eq)
2977 {
2978 int i;
2979
2980 if (dump_file && (dump_flags & TDF_DETAILS))
2981 fprintf (dump_file, "Converting Eq to Geqs\n");
2982
2983 /* Insert "0 <= EQN". */
2984 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2985 pb->geqs[pb->num_geqs].touched = 1;
2986 pb->num_geqs++;
2987
2988 /* Insert "0 <= -EQN". */
2989 omega_copy_eqn (&pb->geqs[pb->num_geqs], &pb->eqs[eq], pb->num_vars);
2990 pb->geqs[pb->num_geqs].touched = 1;
2991
2992 for (i = 0; i <= pb->num_vars; i++)
2993 pb->geqs[pb->num_geqs].coef[i] *= -1;
2994
2995 pb->num_geqs++;
2996
2997 if (dump_file && (dump_flags & TDF_DETAILS))
2998 omega_print_problem (dump_file, pb);
2999 }
3000
3001 /* Eliminates variable I from PB. */
3002
3003 static void
3004 omega_do_elimination (omega_pb pb, int e, int i)
3005 {
3006 eqn sub = omega_alloc_eqns (0, 1);
3007 int c;
3008 int n_vars = pb->num_vars;
3009
3010 if (dump_file && (dump_flags & TDF_DETAILS))
3011 fprintf (dump_file, "eliminating variable %s\n",
3012 omega_variable_to_str (pb, i));
3013
3014 omega_copy_eqn (sub, &pb->eqs[e], pb->num_vars);
3015 c = sub->coef[i];
3016 sub->coef[i] = 0;
3017 if (c == 1 || c == -1)
3018 {
3019 if (pb->eqs[e].color == omega_red)
3020 {
3021 bool fB;
3022 omega_substitute_red (pb, sub, i, c, &fB);
3023 if (fB)
3024 omega_convert_eq_to_geqs (pb, e);
3025 else
3026 omega_delete_variable (pb, i);
3027 }
3028 else
3029 {
3030 omega_substitute (pb, sub, i, c);
3031 omega_delete_variable (pb, i);
3032 }
3033 }
3034 else
3035 {
3036 int a = abs (c);
3037 int e2 = e;
3038
3039 if (dump_file && (dump_flags & TDF_DETAILS))
3040 fprintf (dump_file, "performing non-exact elimination, c = %d\n", c);
3041
3042 for (e = pb->num_eqs - 1; e >= 0; e--)
3043 if (pb->eqs[e].coef[i])
3044 {
3045 eqn eqn = &(pb->eqs[e]);
3046 int j, k;
3047 for (j = n_vars; j >= 0; j--)
3048 eqn->coef[j] *= a;
3049 k = eqn->coef[i];
3050 eqn->coef[i] = 0;
3051 eqn->color |= sub->color;
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);
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 neweqns = 0;
3726 int best = (INT_MAX);
3727 int j = 0, jLe = 0, jLowerBoundCount = 0;
3728
3729
3730 eliminate_again = false;
3731
3732 if (pb->num_eqs > 0)
3733 return omega_solve_problem (pb, desired_res);
3734
3735 if (!coupled_subscripts)
3736 {
3737 if (pb->safe_vars == 0)
3738 pb->num_geqs = 0;
3739 else
3740 for (e = pb->num_geqs - 1; e >= 0; e--)
3741 if (!omega_safe_var_p (pb, abs (pb->geqs[e].key)))
3742 omega_delete_geq (pb, e, n_vars);
3743
3744 pb->num_vars = pb->safe_vars;
3745
3746 if (desired_res == omega_simplify)
3747 {
3748 omega_problem_reduced (pb);
3749 return omega_false;
3750 }
3751
3752 return omega_true;
3753 }
3754
3755 if (desired_res != omega_simplify)
3756 fv = 0;
3757 else
3758 fv = pb->safe_vars;
3759
3760 if (pb->num_geqs == 0)
3761 {
3762 if (desired_res == omega_simplify)
3763 {
3764 pb->num_vars = pb->safe_vars;
3765 omega_problem_reduced (pb);
3766 return omega_false;
3767 }
3768 return omega_true;
3769 }
3770
3771 if (desired_res == omega_simplify && n_vars == pb->safe_vars)
3772 {
3773 omega_problem_reduced (pb);
3774 return omega_false;
3775 }
3776
3777 if (pb->num_geqs > OMEGA_MAX_GEQS - 30
3778 || pb->num_geqs > 2 * n_vars * n_vars + 4 * n_vars + 10)
3779 {
3780 if (dump_file && (dump_flags & TDF_DETAILS))
3781 fprintf (dump_file,
3782 "TOO MANY EQUATIONS; "
3783 "%d equations, %d variables, "
3784 "ELIMINATING REDUNDANT ONES\n",
3785 pb->num_geqs, n_vars);
3786
3787 if (!omega_eliminate_redundant (pb, false))
3788 return omega_false;
3789
3790 n_vars = pb->num_vars;
3791
3792 if (pb->num_eqs > 0)
3793 return omega_solve_problem (pb, desired_res);
3794
3795 if (dump_file && (dump_flags & TDF_DETAILS))
3796 fprintf (dump_file, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
3797 }
3798
3799 if (desired_res != omega_simplify)
3800 fv = 0;
3801 else
3802 fv = pb->safe_vars;
3803
3804 for (i = n_vars; i != fv; i--)
3805 {
3806 int score;
3807 int ub = -2;
3808 int lb = -2;
3809 bool lucky = false;
3810 int upper_bound_count = 0;
3811
3812 lower_bound_count = 0;
3813 minC = maxC = 0;
3814
3815 for (e = pb->num_geqs - 1; e >= 0; e--)
3816 if (pb->geqs[e].coef[i] < 0)
3817 {
3818 minC = MIN (minC, pb->geqs[e].coef[i]);
3819 upper_bound_count++;
3820 if (pb->geqs[e].coef[i] < -1)
3821 {
3822 if (ub == -2)
3823 ub = e;
3824 else
3825 ub = -1;
3826 }
3827 }
3828 else if (pb->geqs[e].coef[i] > 0)
3829 {
3830 maxC = MAX (maxC, pb->geqs[e].coef[i]);
3831 lower_bound_count++;
3832 Le = e;
3833 if (pb->geqs[e].coef[i] > 1)
3834 {
3835 if (lb == -2)
3836 lb = e;
3837 else
3838 lb = -1;
3839 }
3840 }
3841
3842 if (lower_bound_count == 0
3843 || upper_bound_count == 0)
3844 {
3845 lower_bound_count = 0;
3846 break;
3847 }
3848
3849 if (ub >= 0 && lb >= 0
3850 && pb->geqs[lb].key == -pb->geqs[ub].key)
3851 {
3852 int Lc = pb->geqs[lb].coef[i];
3853 int Uc = -pb->geqs[ub].coef[i];
3854 int diff =
3855 Lc * pb->geqs[ub].coef[0] + Uc * pb->geqs[lb].coef[0];
3856 lucky = (diff >= (Uc - 1) * (Lc - 1));
3857 }
3858
3859 if (maxC == 1
3860 || minC == -1
3861 || lucky
3862 || in_approximate_mode)
3863 {
3864 neweqns = score = upper_bound_count * lower_bound_count;
3865
3866 if (dump_file && (dump_flags & TDF_DETAILS))
3867 fprintf (dump_file,
3868 "For %s, exact, score = %d*%d, range = %d ... %d,"
3869 "\nlucky = %d, in_approximate_mode=%d \n",
3870 omega_variable_to_str (pb, i),
3871 upper_bound_count,
3872 lower_bound_count, minC, maxC, lucky,
3873 in_approximate_mode);
3874
3875 if (!exact
3876 || score < best)
3877 {
3878
3879 best = score;
3880 j = i;
3881 minCj = minC;
3882 jLe = Le;
3883 jLowerBoundCount = lower_bound_count;
3884 exact = true;
3885 lucky_exact = lucky;
3886 if (score == 1)
3887 break;
3888 }
3889 }
3890 else if (!exact)
3891 {
3892 if (dump_file && (dump_flags & TDF_DETAILS))
3893 fprintf (dump_file,
3894 "For %s, non-exact, score = %d*%d,"
3895 "range = %d ... %d \n",
3896 omega_variable_to_str (pb, i),
3897 upper_bound_count,
3898 lower_bound_count, minC, maxC);
3899
3900 neweqns = upper_bound_count * lower_bound_count;
3901 score = maxC - minC;
3902
3903 if (best > score)
3904 {
3905 best = score;
3906 j = i;
3907 minCj = minC;
3908 jLe = Le;
3909 jLowerBoundCount = lower_bound_count;
3910 }
3911 }
3912 }
3913
3914 if (lower_bound_count == 0)
3915 {
3916 omega_free_eliminations (pb, pb->safe_vars);
3917 n_vars = pb->num_vars;
3918 eliminate_again = true;
3919 continue;
3920 }
3921
3922 i = j;
3923 minC = minCj;
3924 Le = jLe;
3925 lower_bound_count = jLowerBoundCount;
3926
3927 for (e = pb->num_geqs - 1; e >= 0; e--)
3928 if (pb->geqs[e].coef[i] > 0)
3929 {
3930 if (pb->geqs[e].coef[i] == -minC)
3931 max_splinters += -minC - 1;
3932 else
3933 max_splinters +=
3934 check_pos_mul ((pb->geqs[e].coef[i] - 1),
3935 (-minC - 1)) / (-minC) + 1;
3936 }
3937
3938 /* #ifdef Omega3 */
3939 /* Trying to produce exact elimination by finding redundant
3940 constraints. */
3941 if (!exact && !tried_eliminating_redundant)
3942 {
3943 omega_eliminate_redundant (pb, false);
3944 tried_eliminating_redundant = true;
3945 eliminate_again = true;
3946 continue;
3947 }
3948 tried_eliminating_redundant = false;
3949 /* #endif */
3950
3951 if (return_single_result && desired_res == omega_simplify && !exact)
3952 {
3953 omega_problem_reduced (pb);
3954 return omega_true;
3955 }
3956
3957 /* #ifndef Omega3 */
3958 /* Trying to produce exact elimination by finding redundant
3959 constraints. */
3960 if (!exact && !tried_eliminating_redundant)
3961 {
3962 omega_eliminate_redundant (pb, false);
3963 tried_eliminating_redundant = true;
3964 continue;
3965 }
3966 tried_eliminating_redundant = false;
3967 /* #endif */
3968
3969 if (!exact)
3970 {
3971 int e1, e2;
3972
3973 for (e1 = pb->num_geqs - 1; e1 >= 0; e1--)
3974 if (pb->geqs[e1].color == omega_black)
3975 for (e2 = e1 - 1; e2 >= 0; e2--)
3976 if (pb->geqs[e2].color == omega_black
3977 && pb->geqs[e1].key == -pb->geqs[e2].key
3978 && ((pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3979 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3980 / 2 < parallel_difference))
3981 {
3982 parallel_difference =
3983 (pb->geqs[e1].coef[0] + pb->geqs[e2].coef[0])
3984 * (3 - single_var_geq (&pb->geqs[e1], pb->num_vars))
3985 / 2;
3986 best_parallel_eqn = e1;
3987 }
3988
3989 if (dump_file && (dump_flags & TDF_DETAILS)
3990 && best_parallel_eqn >= 0)
3991 {
3992 fprintf (dump_file,
3993 "Possible parallel projection, diff = %d, in ",
3994 parallel_difference);
3995 omega_print_geq (dump_file, pb, &(pb->geqs[best_parallel_eqn]));
3996 fprintf (dump_file, "\n");
3997 omega_print_problem (dump_file, pb);
3998 }
3999 }
4000
4001 if (dump_file && (dump_flags & TDF_DETAILS))
4002 {
4003 fprintf (dump_file, "going to eliminate %s, (%d,%d,%d)\n",
4004 omega_variable_to_str (pb, i), i, minC,
4005 lower_bound_count);
4006 omega_print_problem (dump_file, pb);
4007
4008 if (lucky_exact)
4009 fprintf (dump_file, "(a lucky exact elimination)\n");
4010
4011 else if (exact)
4012 fprintf (dump_file, "(an exact elimination)\n");
4013
4014 fprintf (dump_file, "Max # of splinters = %d\n", max_splinters);
4015 }
4016
4017 gcc_assert (max_splinters >= 1);
4018
4019 if (!exact && desired_res == omega_simplify && best_parallel_eqn >= 0
4020 && parallel_difference <= max_splinters)
4021 return parallel_splinter (pb, best_parallel_eqn, parallel_difference,
4022 desired_res);
4023
4024 smoothed = false;
4025
4026 if (i != n_vars)
4027 {
4028 int t;
4029 int j = pb->num_vars;
4030
4031 if (dump_file && (dump_flags & TDF_DETAILS))
4032 {
4033 fprintf (dump_file, "Swapping %d and %d\n", i, j);
4034 omega_print_problem (dump_file, pb);
4035 }
4036
4037 swap (&pb->var[i], &pb->var[j]);
4038
4039 for (e = pb->num_geqs - 1; e >= 0; e--)
4040 if (pb->geqs[e].coef[i] != pb->geqs[e].coef[j])
4041 {
4042 pb->geqs[e].touched = 1;
4043 t = pb->geqs[e].coef[i];
4044 pb->geqs[e].coef[i] = pb->geqs[e].coef[j];
4045 pb->geqs[e].coef[j] = t;
4046 }
4047
4048 for (e = pb->num_subs - 1; e >= 0; e--)
4049 if (pb->subs[e].coef[i] != pb->subs[e].coef[j])
4050 {
4051 t = pb->subs[e].coef[i];
4052 pb->subs[e].coef[i] = pb->subs[e].coef[j];
4053 pb->subs[e].coef[j] = t;
4054 }
4055
4056 if (dump_file && (dump_flags & TDF_DETAILS))
4057 {
4058 fprintf (dump_file, "Swapping complete \n");
4059 omega_print_problem (dump_file, pb);
4060 fprintf (dump_file, "\n");
4061 }
4062
4063 i = j;
4064 }
4065
4066 else if (dump_file && (dump_flags & TDF_DETAILS))
4067 {
4068 fprintf (dump_file, "No swap needed\n");
4069 omega_print_problem (dump_file, pb);
4070 }
4071
4072 pb->num_vars--;
4073 n_vars = pb->num_vars;
4074
4075 if (exact)
4076 {
4077 if (n_vars == 1)
4078 {
4079 int upper_bound = pos_infinity;
4080 int lower_bound = neg_infinity;
4081 enum omega_eqn_color ub_color = omega_black;
4082 enum omega_eqn_color lb_color = omega_black;
4083 int topeqn = pb->num_geqs - 1;
4084 int Lc = pb->geqs[Le].coef[i];
4085
4086 for (Le = topeqn; Le >= 0; Le--)
4087 if ((Lc = pb->geqs[Le].coef[i]) == 0)
4088 {
4089 if (pb->geqs[Le].coef[1] == 1)
4090 {
4091 int constantTerm = -pb->geqs[Le].coef[0];
4092
4093 if (constantTerm > lower_bound ||
4094 (constantTerm == lower_bound &&
4095 !omega_eqn_is_red (&pb->geqs[Le], desired_res)))
4096 {
4097 lower_bound = constantTerm;
4098 lb_color = pb->geqs[Le].color;
4099 }
4100
4101 if (dump_file && (dump_flags & TDF_DETAILS))
4102 {
4103 if (pb->geqs[Le].color == omega_black)
4104 fprintf (dump_file, " :::=> %s >= %d\n",
4105 omega_variable_to_str (pb, 1),
4106 constantTerm);
4107 else
4108 fprintf (dump_file,
4109 " :::=> [%s >= %d]\n",
4110 omega_variable_to_str (pb, 1),
4111 constantTerm);
4112 }
4113 }
4114 else
4115 {
4116 int constantTerm = pb->geqs[Le].coef[0];
4117 if (constantTerm < upper_bound ||
4118 (constantTerm == upper_bound
4119 && !omega_eqn_is_red (&pb->geqs[Le],
4120 desired_res)))
4121 {
4122 upper_bound = constantTerm;
4123 ub_color = pb->geqs[Le].color;
4124 }
4125
4126 if (dump_file && (dump_flags & TDF_DETAILS))
4127 {
4128 if (pb->geqs[Le].color == omega_black)
4129 fprintf (dump_file, " :::=> %s <= %d\n",
4130 omega_variable_to_str (pb, 1),
4131 constantTerm);
4132 else
4133 fprintf (dump_file,
4134 " :::=> [%s <= %d]\n",
4135 omega_variable_to_str (pb, 1),
4136 constantTerm);
4137 }
4138 }
4139 }
4140 else if (Lc > 0)
4141 for (Ue = topeqn; Ue >= 0; Ue--)
4142 if (pb->geqs[Ue].coef[i] < 0
4143 && pb->geqs[Le].key != -pb->geqs[Ue].key)
4144 {
4145 int Uc = -pb->geqs[Ue].coef[i];
4146 int coefficient = pb->geqs[Ue].coef[1] * Lc
4147 + pb->geqs[Le].coef[1] * Uc;
4148 int constantTerm = pb->geqs[Ue].coef[0] * Lc
4149 + pb->geqs[Le].coef[0] * Uc;
4150
4151 if (dump_file && (dump_flags & TDF_DETAILS))
4152 {
4153 omega_print_geq_extra (dump_file, pb,
4154 &(pb->geqs[Ue]));
4155 fprintf (dump_file, "\n");
4156 omega_print_geq_extra (dump_file, pb,
4157 &(pb->geqs[Le]));
4158 fprintf (dump_file, "\n");
4159 }
4160
4161 if (coefficient > 0)
4162 {
4163 constantTerm = -int_div (constantTerm, coefficient);
4164
4165 if (constantTerm > lower_bound
4166 || (constantTerm == lower_bound
4167 && (desired_res != omega_simplify
4168 || (pb->geqs[Ue].color == omega_black
4169 && pb->geqs[Le].color == omega_black))))
4170 {
4171 lower_bound = constantTerm;
4172 lb_color = (pb->geqs[Ue].color == omega_red
4173 || pb->geqs[Le].color == omega_red)
4174 ? omega_red : omega_black;
4175 }
4176
4177 if (dump_file && (dump_flags & TDF_DETAILS))
4178 {
4179 if (pb->geqs[Ue].color == omega_red
4180 || pb->geqs[Le].color == omega_red)
4181 fprintf (dump_file,
4182 " ::=> [%s >= %d]\n",
4183 omega_variable_to_str (pb, 1),
4184 constantTerm);
4185 else
4186 fprintf (dump_file,
4187 " ::=> %s >= %d\n",
4188 omega_variable_to_str (pb, 1),
4189 constantTerm);
4190 }
4191 }
4192 else
4193 {
4194 constantTerm = int_div (constantTerm, -coefficient);
4195 if (constantTerm < upper_bound
4196 || (constantTerm == upper_bound
4197 && pb->geqs[Ue].color == omega_black
4198 && pb->geqs[Le].color == omega_black))
4199 {
4200 upper_bound = constantTerm;
4201 ub_color = (pb->geqs[Ue].color == omega_red
4202 || pb->geqs[Le].color == omega_red)
4203 ? omega_red : omega_black;
4204 }
4205
4206 if (dump_file
4207 && (dump_flags & TDF_DETAILS))
4208 {
4209 if (pb->geqs[Ue].color == omega_red
4210 || pb->geqs[Le].color == omega_red)
4211 fprintf (dump_file,
4212 " ::=> [%s <= %d]\n",
4213 omega_variable_to_str (pb, 1),
4214 constantTerm);
4215 else
4216 fprintf (dump_file,
4217 " ::=> %s <= %d\n",
4218 omega_variable_to_str (pb, 1),
4219 constantTerm);
4220 }
4221 }
4222 }
4223
4224 pb->num_geqs = 0;
4225
4226 if (dump_file && (dump_flags & TDF_DETAILS))
4227 fprintf (dump_file,
4228 " therefore, %c%d <= %c%s%c <= %d%c\n",
4229 lb_color == omega_red ? '[' : ' ', lower_bound,
4230 (lb_color == omega_red && ub_color == omega_black)
4231 ? ']' : ' ',
4232 omega_variable_to_str (pb, 1),
4233 (lb_color == omega_black && ub_color == omega_red)
4234 ? '[' : ' ',
4235 upper_bound, ub_color == omega_red ? ']' : ' ');
4236
4237 if (lower_bound > upper_bound)
4238 return omega_false;
4239
4240 if (pb->safe_vars == 1)
4241 {
4242 if (upper_bound == lower_bound
4243 && !(ub_color == omega_red || lb_color == omega_red)
4244 && !please_no_equalities_in_simplified_problems)
4245 {
4246 pb->num_eqs++;
4247 pb->eqs[0].coef[1] = -1;
4248 pb->eqs[0].coef[0] = upper_bound;
4249
4250 if (ub_color == omega_red
4251 || lb_color == omega_red)
4252 pb->eqs[0].color = omega_red;
4253
4254 if (desired_res == omega_simplify
4255 && pb->eqs[0].color == omega_black)
4256 return omega_solve_problem (pb, desired_res);
4257 }
4258
4259 if (upper_bound != pos_infinity)
4260 {
4261 pb->geqs[0].coef[1] = -1;
4262 pb->geqs[0].coef[0] = upper_bound;
4263 pb->geqs[0].color = ub_color;
4264 pb->geqs[0].key = -1;
4265 pb->geqs[0].touched = 0;
4266 pb->num_geqs++;
4267 }
4268
4269 if (lower_bound != neg_infinity)
4270 {
4271 pb->geqs[pb->num_geqs].coef[1] = 1;
4272 pb->geqs[pb->num_geqs].coef[0] = -lower_bound;
4273 pb->geqs[pb->num_geqs].color = lb_color;
4274 pb->geqs[pb->num_geqs].key = 1;
4275 pb->geqs[pb->num_geqs].touched = 0;
4276 pb->num_geqs++;
4277 }
4278 }
4279
4280 if (desired_res == omega_simplify)
4281 {
4282 omega_problem_reduced (pb);
4283 return omega_false;
4284 }
4285 else
4286 {
4287 if (!conservative
4288 && (desired_res != omega_simplify
4289 || (lb_color == omega_black
4290 && ub_color == omega_black))
4291 && original_problem != no_problem
4292 && lower_bound == upper_bound)
4293 {
4294 for (i = original_problem->num_vars; i >= 0; i--)
4295 if (original_problem->var[i] == pb->var[1])
4296 break;
4297
4298 if (i == 0)
4299 break;
4300
4301 e = original_problem->num_eqs++;
4302 omega_init_eqn_zero (&original_problem->eqs[e],
4303 original_problem->num_vars);
4304 original_problem->eqs[e].coef[i] = -1;
4305 original_problem->eqs[e].coef[0] = upper_bound;
4306
4307 if (dump_file && (dump_flags & TDF_DETAILS))
4308 {
4309 fprintf (dump_file,
4310 "adding equality %d to outer problem\n", e);
4311 omega_print_problem (dump_file, original_problem);
4312 }
4313 }
4314 return omega_true;
4315 }
4316 }
4317
4318 eliminate_again = true;
4319
4320 if (lower_bound_count == 1)
4321 {
4322 eqn lbeqn = omega_alloc_eqns (0, 1);
4323 int Lc = pb->geqs[Le].coef[i];
4324
4325 if (dump_file && (dump_flags & TDF_DETAILS))
4326 fprintf (dump_file, "an inplace elimination\n");
4327
4328 omega_copy_eqn (lbeqn, &pb->geqs[Le], (n_vars + 1));
4329 omega_delete_geq_extra (pb, Le, n_vars + 1);
4330
4331 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4332 if (pb->geqs[Ue].coef[i] < 0)
4333 {
4334 if (lbeqn->key == -pb->geqs[Ue].key)
4335 omega_delete_geq_extra (pb, Ue, n_vars + 1);
4336 else
4337 {
4338 int k;
4339 int Uc = -pb->geqs[Ue].coef[i];
4340 pb->geqs[Ue].touched = 1;
4341 eliminate_again = false;
4342
4343 if (lbeqn->color == omega_red)
4344 pb->geqs[Ue].color = omega_red;
4345
4346 for (k = 0; k <= n_vars; k++)
4347 pb->geqs[Ue].coef[k] =
4348 check_mul (pb->geqs[Ue].coef[k], Lc) +
4349 check_mul (lbeqn->coef[k], Uc);
4350
4351 if (dump_file && (dump_flags & TDF_DETAILS))
4352 {
4353 omega_print_geq (dump_file, pb,
4354 &(pb->geqs[Ue]));
4355 fprintf (dump_file, "\n");
4356 }
4357 }
4358 }
4359
4360 omega_free_eqns (lbeqn, 1);
4361 continue;
4362 }
4363 else
4364 {
4365 int *dead_eqns = XNEWVEC (int, OMEGA_MAX_GEQS);
4366 bool *is_dead = XNEWVEC (bool, OMEGA_MAX_GEQS);
4367 int num_dead = 0;
4368 int top_eqn = pb->num_geqs - 1;
4369 lower_bound_count--;
4370
4371 if (dump_file && (dump_flags & TDF_DETAILS))
4372 fprintf (dump_file, "lower bound count = %d\n",
4373 lower_bound_count);
4374
4375 for (Le = top_eqn; Le >= 0; Le--)
4376 if (pb->geqs[Le].coef[i] > 0)
4377 {
4378 int Lc = pb->geqs[Le].coef[i];
4379 for (Ue = top_eqn; Ue >= 0; Ue--)
4380 if (pb->geqs[Ue].coef[i] < 0)
4381 {
4382 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4383 {
4384 int k;
4385 int Uc = -pb->geqs[Ue].coef[i];
4386
4387 if (num_dead == 0)
4388 e2 = pb->num_geqs++;
4389 else
4390 e2 = dead_eqns[--num_dead];
4391
4392 gcc_assert (e2 < OMEGA_MAX_GEQS);
4393
4394 if (dump_file && (dump_flags & TDF_DETAILS))
4395 {
4396 fprintf (dump_file,
4397 "Le = %d, Ue = %d, gen = %d\n",
4398 Le, Ue, e2);
4399 omega_print_geq_extra (dump_file, pb,
4400 &(pb->geqs[Le]));
4401 fprintf (dump_file, "\n");
4402 omega_print_geq_extra (dump_file, pb,
4403 &(pb->geqs[Ue]));
4404 fprintf (dump_file, "\n");
4405 }
4406
4407 eliminate_again = false;
4408
4409 for (k = n_vars; k >= 0; k--)
4410 pb->geqs[e2].coef[k] =
4411 check_mul (pb->geqs[Ue].coef[k], Lc) +
4412 check_mul (pb->geqs[Le].coef[k], Uc);
4413
4414 pb->geqs[e2].coef[n_vars + 1] = 0;
4415 pb->geqs[e2].touched = 1;
4416
4417 if (pb->geqs[Ue].color == omega_red
4418 || pb->geqs[Le].color == omega_red)
4419 pb->geqs[e2].color = omega_red;
4420 else
4421 pb->geqs[e2].color = omega_black;
4422
4423 if (dump_file && (dump_flags & TDF_DETAILS))
4424 {
4425 omega_print_geq (dump_file, pb,
4426 &(pb->geqs[e2]));
4427 fprintf (dump_file, "\n");
4428 }
4429 }
4430
4431 if (lower_bound_count == 0)
4432 {
4433 dead_eqns[num_dead++] = Ue;
4434
4435 if (dump_file && (dump_flags & TDF_DETAILS))
4436 fprintf (dump_file, "Killed %d\n", Ue);
4437 }
4438 }
4439
4440 lower_bound_count--;
4441 dead_eqns[num_dead++] = Le;
4442
4443 if (dump_file && (dump_flags & TDF_DETAILS))
4444 fprintf (dump_file, "Killed %d\n", Le);
4445 }
4446
4447 for (e = pb->num_geqs - 1; e >= 0; e--)
4448 is_dead[e] = false;
4449
4450 while (num_dead > 0)
4451 is_dead[dead_eqns[--num_dead]] = true;
4452
4453 for (e = pb->num_geqs - 1; e >= 0; e--)
4454 if (is_dead[e])
4455 omega_delete_geq_extra (pb, e, n_vars + 1);
4456
4457 free (dead_eqns);
4458 free (is_dead);
4459 continue;
4460 }
4461 }
4462 else
4463 {
4464 omega_pb rS, iS;
4465
4466 rS = omega_alloc_problem (0, 0);
4467 iS = omega_alloc_problem (0, 0);
4468 e2 = 0;
4469 possible_easy_int_solution = true;
4470
4471 for (e = 0; e < pb->num_geqs; e++)
4472 if (pb->geqs[e].coef[i] == 0)
4473 {
4474 omega_copy_eqn (&(rS->geqs[e2]), &pb->geqs[e],
4475 pb->num_vars);
4476 omega_copy_eqn (&(iS->geqs[e2]), &pb->geqs[e],
4477 pb->num_vars);
4478
4479 if (dump_file && (dump_flags & TDF_DETAILS))
4480 {
4481 int t;
4482 fprintf (dump_file, "Copying (%d, %d): ", i,
4483 pb->geqs[e].coef[i]);
4484 omega_print_geq_extra (dump_file, pb, &pb->geqs[e]);
4485 fprintf (dump_file, "\n");
4486 for (t = 0; t <= n_vars + 1; t++)
4487 fprintf (dump_file, "%d ", pb->geqs[e].coef[t]);
4488 fprintf (dump_file, "\n");
4489
4490 }
4491 e2++;
4492 gcc_assert (e2 < OMEGA_MAX_GEQS);
4493 }
4494
4495 for (Le = pb->num_geqs - 1; Le >= 0; Le--)
4496 if (pb->geqs[Le].coef[i] > 0)
4497 for (Ue = pb->num_geqs - 1; Ue >= 0; Ue--)
4498 if (pb->geqs[Ue].coef[i] < 0)
4499 {
4500 int k;
4501 int Lc = pb->geqs[Le].coef[i];
4502 int Uc = -pb->geqs[Ue].coef[i];
4503
4504 if (pb->geqs[Le].key != -pb->geqs[Ue].key)
4505 {
4506
4507 rS->geqs[e2].touched = iS->geqs[e2].touched = 1;
4508
4509 if (dump_file && (dump_flags & TDF_DETAILS))
4510 {
4511 fprintf (dump_file, "---\n");
4512 fprintf (dump_file,
4513 "Le(Lc) = %d(%d_, Ue(Uc) = %d(%d), gen = %d\n",
4514 Le, Lc, Ue, Uc, e2);
4515 omega_print_geq_extra (dump_file, pb, &pb->geqs[Le]);
4516 fprintf (dump_file, "\n");
4517 omega_print_geq_extra (dump_file, pb, &pb->geqs[Ue]);
4518 fprintf (dump_file, "\n");
4519 }
4520
4521 if (Uc == Lc)
4522 {
4523 for (k = n_vars; k >= 0; k--)
4524 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4525 pb->geqs[Ue].coef[k] + pb->geqs[Le].coef[k];
4526
4527 iS->geqs[e2].coef[0] -= (Uc - 1);
4528 }
4529 else
4530 {
4531 for (k = n_vars; k >= 0; k--)
4532 iS->geqs[e2].coef[k] = rS->geqs[e2].coef[k] =
4533 check_mul (pb->geqs[Ue].coef[k], Lc) +
4534 check_mul (pb->geqs[Le].coef[k], Uc);
4535
4536 iS->geqs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
4537 }
4538
4539 if (pb->geqs[Ue].color == omega_red
4540 || pb->geqs[Le].color == omega_red)
4541 iS->geqs[e2].color = rS->geqs[e2].color = omega_red;
4542 else
4543 iS->geqs[e2].color = rS->geqs[e2].color = omega_black;
4544
4545 if (dump_file && (dump_flags & TDF_DETAILS))
4546 {
4547 omega_print_geq (dump_file, pb, &(rS->geqs[e2]));
4548 fprintf (dump_file, "\n");
4549 }
4550
4551 e2++;
4552 gcc_assert (e2 < OMEGA_MAX_GEQS);
4553 }
4554 else if (pb->geqs[Ue].coef[0] * Lc +
4555 pb->geqs[Le].coef[0] * Uc -
4556 (Uc - 1) * (Lc - 1) < 0)
4557 possible_easy_int_solution = false;
4558 }
4559
4560 iS->variables_initialized = rS->variables_initialized = true;
4561 iS->num_vars = rS->num_vars = pb->num_vars;
4562 iS->num_geqs = rS->num_geqs = e2;
4563 iS->num_eqs = rS->num_eqs = 0;
4564 iS->num_subs = rS->num_subs = pb->num_subs;
4565 iS->safe_vars = rS->safe_vars = pb->safe_vars;
4566
4567 for (e = n_vars; e >= 0; e--)
4568 rS->var[e] = pb->var[e];
4569
4570 for (e = n_vars; e >= 0; e--)
4571 iS->var[e] = pb->var[e];
4572
4573 for (e = pb->num_subs - 1; e >= 0; e--)
4574 {
4575 omega_copy_eqn (&(rS->subs[e]), &(pb->subs[e]), pb->num_vars);
4576 omega_copy_eqn (&(iS->subs[e]), &(pb->subs[e]), pb->num_vars);
4577 }
4578
4579 pb->num_vars++;
4580 n_vars = pb->num_vars;
4581
4582 if (desired_res != omega_true)
4583 {
4584 if (original_problem == no_problem)
4585 {
4586 original_problem = pb;
4587 result = omega_solve_geq (rS, omega_false);
4588 original_problem = no_problem;
4589 }
4590 else
4591 result = omega_solve_geq (rS, omega_false);
4592
4593 if (result == omega_false)
4594 {
4595 free (rS);
4596 free (iS);
4597 return result;
4598 }
4599
4600 if (pb->num_eqs > 0)
4601 {
4602 /* An equality constraint must have been found */
4603 free (rS);
4604 free (iS);
4605 return omega_solve_problem (pb, desired_res);
4606 }
4607 }
4608
4609 if (desired_res != omega_false)
4610 {
4611 int j;
4612 int lower_bounds = 0;
4613 int *lower_bound = XNEWVEC (int, OMEGA_MAX_GEQS);
4614
4615 if (possible_easy_int_solution)
4616 {
4617 conservative++;
4618 result = omega_solve_geq (iS, desired_res);
4619 conservative--;
4620
4621 if (result != omega_false)
4622 {
4623 free (rS);
4624 free (iS);
4625 free (lower_bound);
4626 return result;
4627 }
4628 }
4629
4630 if (!exact && best_parallel_eqn >= 0
4631 && parallel_difference <= max_splinters)
4632 {
4633 free (rS);
4634 free (iS);
4635 free (lower_bound);
4636 return parallel_splinter (pb, best_parallel_eqn,
4637 parallel_difference,
4638 desired_res);
4639 }
4640
4641 if (dump_file && (dump_flags & TDF_DETAILS))
4642 fprintf (dump_file, "have to do exact analysis\n");
4643
4644 conservative++;
4645
4646 for (e = 0; e < pb->num_geqs; e++)
4647 if (pb->geqs[e].coef[i] > 1)
4648 lower_bound[lower_bounds++] = e;
4649
4650 /* Sort array LOWER_BOUND. */
4651 for (j = 0; j < lower_bounds; j++)
4652 {
4653 int k, smallest = j;
4654
4655 for (k = j + 1; k < lower_bounds; k++)
4656 if (pb->geqs[lower_bound[smallest]].coef[i] >
4657 pb->geqs[lower_bound[k]].coef[i])
4658 smallest = k;
4659
4660 k = lower_bound[smallest];
4661 lower_bound[smallest] = lower_bound[j];
4662 lower_bound[j] = k;
4663 }
4664
4665 if (dump_file && (dump_flags & TDF_DETAILS))
4666 {
4667 fprintf (dump_file, "lower bound coefficients = ");
4668
4669 for (j = 0; j < lower_bounds; j++)
4670 fprintf (dump_file, " %d",
4671 pb->geqs[lower_bound[j]].coef[i]);
4672
4673 fprintf (dump_file, "\n");
4674 }
4675
4676 for (j = 0; j < lower_bounds; j++)
4677 {
4678 int max_incr;
4679 int c;
4680 int worst_lower_bound_constant = -minC;
4681
4682 e = lower_bound[j];
4683 max_incr = (((pb->geqs[e].coef[i] - 1) *
4684 (worst_lower_bound_constant - 1) - 1)
4685 / worst_lower_bound_constant);
4686 /* max_incr += 2; */
4687
4688 if (dump_file && (dump_flags & TDF_DETAILS))
4689 {
4690 fprintf (dump_file, "for equation ");
4691 omega_print_geq (dump_file, pb, &pb->geqs[e]);
4692 fprintf (dump_file,
4693 "\ntry decrements from 0 to %d\n",
4694 max_incr);
4695 omega_print_problem (dump_file, pb);
4696 }
4697
4698 if (max_incr > 50 && !smoothed
4699 && smooth_weird_equations (pb))
4700 {
4701 conservative--;
4702 free (rS);
4703 free (iS);
4704 smoothed = true;
4705 goto solve_geq_start;
4706 }
4707
4708 omega_copy_eqn (&pb->eqs[0], &pb->geqs[e],
4709 pb->num_vars);
4710 pb->eqs[0].color = omega_black;
4711 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
4712 pb->geqs[e].touched = 1;
4713 pb->num_eqs = 1;
4714
4715 for (c = max_incr; c >= 0; c--)
4716 {
4717 if (dump_file && (dump_flags & TDF_DETAILS))
4718 {
4719 fprintf (dump_file,
4720 "trying next decrement of %d\n",
4721 max_incr - c);
4722 omega_print_problem (dump_file, pb);
4723 }
4724
4725 omega_copy_problem (rS, pb);
4726
4727 if (dump_file && (dump_flags & TDF_DETAILS))
4728 omega_print_problem (dump_file, rS);
4729
4730 result = omega_solve_problem (rS, desired_res);
4731
4732 if (result == omega_true)
4733 {
4734 free (rS);
4735 free (iS);
4736 free (lower_bound);
4737 conservative--;
4738 return omega_true;
4739 }
4740
4741 pb->eqs[0].coef[0]--;
4742 }
4743
4744 if (j + 1 < lower_bounds)
4745 {
4746 pb->num_eqs = 0;
4747 omega_copy_eqn (&pb->geqs[e], &pb->eqs[0],
4748 pb->num_vars);
4749 pb->geqs[e].touched = 1;
4750 pb->geqs[e].color = omega_black;
4751 omega_copy_problem (rS, pb);
4752
4753 if (dump_file && (dump_flags & TDF_DETAILS))
4754 fprintf (dump_file,
4755 "exhausted lower bound, "
4756 "checking if still feasible ");
4757
4758 result = omega_solve_problem (rS, omega_false);
4759
4760 if (result == omega_false)
4761 break;
4762 }
4763 }
4764
4765 if (dump_file && (dump_flags & TDF_DETAILS))
4766 fprintf (dump_file, "fall-off the end\n");
4767
4768 free (rS);
4769 free (iS);
4770 free (lower_bound);
4771 conservative--;
4772 return omega_false;
4773 }
4774
4775 free (rS);
4776 free (iS);
4777 }
4778 return omega_unknown;
4779 } while (eliminate_again);
4780 } while (1);
4781 }
4782
4783 /* Because the omega solver is recursive, this counter limits the
4784 recursion depth. */
4785 static int omega_solve_depth = 0;
4786
4787 /* Return omega_true when the problem PB has a solution following the
4788 DESIRED_RES. */
4789
4790 enum omega_result
4791 omega_solve_problem (omega_pb pb, enum omega_result desired_res)
4792 {
4793 enum omega_result result;
4794
4795 gcc_assert (pb->num_vars >= pb->safe_vars);
4796 omega_solve_depth++;
4797
4798 if (desired_res != omega_simplify)
4799 pb->safe_vars = 0;
4800
4801 if (omega_solve_depth > 50)
4802 {
4803 if (dump_file && (dump_flags & TDF_DETAILS))
4804 {
4805 fprintf (dump_file,
4806 "Solve depth = %d, in_approximate_mode = %d, aborting\n",
4807 omega_solve_depth, in_approximate_mode);
4808 omega_print_problem (dump_file, pb);
4809 }
4810 gcc_assert (0);
4811 }
4812
4813 if (omega_solve_eq (pb, desired_res) == omega_false)
4814 {
4815 omega_solve_depth--;
4816 return omega_false;
4817 }
4818
4819 if (in_approximate_mode && !pb->num_geqs)
4820 {
4821 result = omega_true;
4822 pb->num_vars = pb->safe_vars;
4823 omega_problem_reduced (pb);
4824 }
4825 else
4826 result = omega_solve_geq (pb, desired_res);
4827
4828 omega_solve_depth--;
4829
4830 if (!omega_reduce_with_subs)
4831 {
4832 resurrect_subs (pb);
4833 gcc_assert (please_no_equalities_in_simplified_problems
4834 || !result || pb->num_subs == 0);
4835 }
4836
4837 return result;
4838 }
4839
4840 /* Return true if red equations constrain the set of possible solutions.
4841 We assume that there are solutions to the black equations by
4842 themselves, so if there is no solution to the combined problem, we
4843 return true. */
4844
4845 bool
4846 omega_problem_has_red_equations (omega_pb pb)
4847 {
4848 bool result;
4849 int e;
4850 int i;
4851
4852 if (dump_file && (dump_flags & TDF_DETAILS))
4853 {
4854 fprintf (dump_file, "Checking for red equations:\n");
4855 omega_print_problem (dump_file, pb);
4856 }
4857
4858 please_no_equalities_in_simplified_problems++;
4859 may_be_red++;
4860
4861 if (omega_single_result)
4862 return_single_result++;
4863
4864 create_color = true;
4865 result = (omega_simplify_problem (pb) == omega_false);
4866
4867 if (omega_single_result)
4868 return_single_result--;
4869
4870 may_be_red--;
4871 please_no_equalities_in_simplified_problems--;
4872
4873 if (result)
4874 {
4875 if (dump_file && (dump_flags & TDF_DETAILS))
4876 fprintf (dump_file, "Gist is FALSE\n");
4877
4878 pb->num_subs = 0;
4879 pb->num_geqs = 0;
4880 pb->num_eqs = 1;
4881 pb->eqs[0].color = omega_red;
4882
4883 for (i = pb->num_vars; i > 0; i--)
4884 pb->eqs[0].coef[i] = 0;
4885
4886 pb->eqs[0].coef[0] = 1;
4887 return true;
4888 }
4889
4890 free_red_eliminations (pb);
4891 gcc_assert (pb->num_eqs == 0);
4892
4893 for (e = pb->num_geqs - 1; e >= 0; e--)
4894 if (pb->geqs[e].color == omega_red)
4895 result = true;
4896
4897 if (!result)
4898 return false;
4899
4900 for (i = pb->safe_vars; i >= 1; i--)
4901 {
4902 int ub = 0;
4903 int lb = 0;
4904
4905 for (e = pb->num_geqs - 1; e >= 0; e--)
4906 {
4907 if (pb->geqs[e].coef[i])
4908 {
4909 if (pb->geqs[e].coef[i] > 0)
4910 lb |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4911
4912 else
4913 ub |= (1 + (pb->geqs[e].color == omega_red ? 1 : 0));
4914 }
4915 }
4916
4917 if (ub == 2 || lb == 2)
4918 {
4919
4920 if (dump_file && (dump_flags & TDF_DETAILS))
4921 fprintf (dump_file, "checks for upper/lower bounds worked!\n");
4922
4923 if (!omega_reduce_with_subs)
4924 {
4925 resurrect_subs (pb);
4926 gcc_assert (pb->num_subs == 0);
4927 }
4928
4929 return true;
4930 }
4931 }
4932
4933
4934 if (dump_file && (dump_flags & TDF_DETAILS))
4935 fprintf (dump_file,
4936 "*** Doing potentially expensive elimination tests "
4937 "for red equations\n");
4938
4939 please_no_equalities_in_simplified_problems++;
4940 omega_eliminate_red (pb, true);
4941 please_no_equalities_in_simplified_problems--;
4942
4943 result = false;
4944 gcc_assert (pb->num_eqs == 0);
4945
4946 for (e = pb->num_geqs - 1; e >= 0; e--)
4947 if (pb->geqs[e].color == omega_red)
4948 result = true;
4949
4950 if (dump_file && (dump_flags & TDF_DETAILS))
4951 {
4952 if (!result)
4953 fprintf (dump_file,
4954 "******************** Redundant Red Equations eliminated!!\n");
4955 else
4956 fprintf (dump_file,
4957 "******************** Red Equations remain\n");
4958
4959 omega_print_problem (dump_file, pb);
4960 }
4961
4962 if (!omega_reduce_with_subs)
4963 {
4964 normalize_return_type r;
4965
4966 resurrect_subs (pb);
4967 r = normalize_omega_problem (pb);
4968 gcc_assert (r != normalize_false);
4969
4970 coalesce (pb);
4971 cleanout_wildcards (pb);
4972 gcc_assert (pb->num_subs == 0);
4973 }
4974
4975 return result;
4976 }
4977
4978 /* Calls omega_simplify_problem in approximate mode. */
4979
4980 enum omega_result
4981 omega_simplify_approximate (omega_pb pb)
4982 {
4983 enum omega_result result;
4984
4985 if (dump_file && (dump_flags & TDF_DETAILS))
4986 fprintf (dump_file, "(Entering approximate mode\n");
4987
4988 in_approximate_mode = true;
4989 result = omega_simplify_problem (pb);
4990 in_approximate_mode = false;
4991
4992 gcc_assert (pb->num_vars == pb->safe_vars);
4993 if (!omega_reduce_with_subs)
4994 gcc_assert (pb->num_subs == 0);
4995
4996 if (dump_file && (dump_flags & TDF_DETAILS))
4997 fprintf (dump_file, "Leaving approximate mode)\n");
4998
4999 return result;
5000 }
5001
5002
5003 /* Simplifies problem PB by eliminating redundant constraints and
5004 reducing the constraints system to a minimal form. Returns
5005 omega_true when the problem was successfully reduced, omega_unknown
5006 when the solver is unable to determine an answer. */
5007
5008 enum omega_result
5009 omega_simplify_problem (omega_pb pb)
5010 {
5011 int i;
5012
5013 omega_found_reduction = omega_false;
5014
5015 if (!pb->variables_initialized)
5016 omega_initialize_variables (pb);
5017
5018 if (next_key * 3 > MAX_KEYS)
5019 {
5020 int e;
5021
5022 hash_version++;
5023 next_key = OMEGA_MAX_VARS + 1;
5024
5025 for (e = pb->num_geqs - 1; e >= 0; e--)
5026 pb->geqs[e].touched = 1;
5027
5028 for (i = 0; i < HASH_TABLE_SIZE; i++)
5029 hash_master[i].touched = -1;
5030
5031 pb->hash_version = hash_version;
5032 }
5033
5034 else if (pb->hash_version != hash_version)
5035 {
5036 int e;
5037
5038 for (e = pb->num_geqs - 1; e >= 0; e--)
5039 pb->geqs[e].touched = 1;
5040
5041 pb->hash_version = hash_version;
5042 }
5043
5044 if (pb->num_vars > pb->num_eqs + 3 * pb->safe_vars)
5045 omega_free_eliminations (pb, pb->safe_vars);
5046
5047 if (!may_be_red && pb->num_subs == 0 && pb->safe_vars == 0)
5048 {
5049 omega_found_reduction = omega_solve_problem (pb, omega_unknown);
5050
5051 if (omega_found_reduction != omega_false
5052 && !return_single_result)
5053 {
5054 pb->num_geqs = 0;
5055 pb->num_eqs = 0;
5056 (*omega_when_reduced) (pb);
5057 }
5058
5059 return omega_found_reduction;
5060 }
5061
5062 omega_solve_problem (pb, omega_simplify);
5063
5064 if (omega_found_reduction != omega_false)
5065 {
5066 for (i = 1; omega_safe_var_p (pb, i); i++)
5067 pb->forwarding_address[pb->var[i]] = i;
5068
5069 for (i = 0; i < pb->num_subs; i++)
5070 pb->forwarding_address[pb->subs[i].key] = -i - 1;
5071 }
5072
5073 if (!omega_reduce_with_subs)
5074 gcc_assert (please_no_equalities_in_simplified_problems
5075 || omega_found_reduction == omega_false
5076 || pb->num_subs == 0);
5077
5078 return omega_found_reduction;
5079 }
5080
5081 /* Make variable VAR unprotected: it then can be eliminated. */
5082
5083 void
5084 omega_unprotect_variable (omega_pb pb, int var)
5085 {
5086 int e, idx;
5087 idx = pb->forwarding_address[var];
5088
5089 if (idx < 0)
5090 {
5091 idx = -1 - idx;
5092 pb->num_subs--;
5093
5094 if (idx < pb->num_subs)
5095 {
5096 omega_copy_eqn (&pb->subs[idx], &pb->subs[pb->num_subs],
5097 pb->num_vars);
5098 pb->forwarding_address[pb->subs[idx].key] = -idx - 1;
5099 }
5100 }
5101 else
5102 {
5103 int *bring_to_life = XNEWVEC (int, OMEGA_MAX_VARS);
5104 int e2;
5105
5106 for (e = pb->num_subs - 1; e >= 0; e--)
5107 bring_to_life[e] = (pb->subs[e].coef[idx] != 0);
5108
5109 for (e2 = pb->num_subs - 1; e2 >= 0; e2--)
5110 if (bring_to_life[e2])
5111 {
5112 pb->num_vars++;
5113 pb->safe_vars++;
5114
5115 if (pb->safe_vars < pb->num_vars)
5116 {
5117 for (e = pb->num_geqs - 1; e >= 0; e--)
5118 {
5119 pb->geqs[e].coef[pb->num_vars] =
5120 pb->geqs[e].coef[pb->safe_vars];
5121
5122 pb->geqs[e].coef[pb->safe_vars] = 0;
5123 }
5124
5125 for (e = pb->num_eqs - 1; e >= 0; e--)
5126 {
5127 pb->eqs[e].coef[pb->num_vars] =
5128 pb->eqs[e].coef[pb->safe_vars];
5129
5130 pb->eqs[e].coef[pb->safe_vars] = 0;
5131 }
5132
5133 for (e = pb->num_subs - 1; e >= 0; e--)
5134 {
5135 pb->subs[e].coef[pb->num_vars] =
5136 pb->subs[e].coef[pb->safe_vars];
5137
5138 pb->subs[e].coef[pb->safe_vars] = 0;
5139 }
5140
5141 pb->var[pb->num_vars] = pb->var[pb->safe_vars];
5142 pb->forwarding_address[pb->var[pb->num_vars]] =
5143 pb->num_vars;
5144 }
5145 else
5146 {
5147 for (e = pb->num_geqs - 1; e >= 0; e--)
5148 pb->geqs[e].coef[pb->safe_vars] = 0;
5149
5150 for (e = pb->num_eqs - 1; e >= 0; e--)
5151 pb->eqs[e].coef[pb->safe_vars] = 0;
5152
5153 for (e = pb->num_subs - 1; e >= 0; e--)
5154 pb->subs[e].coef[pb->safe_vars] = 0;
5155 }
5156
5157 pb->var[pb->safe_vars] = pb->subs[e2].key;
5158 pb->forwarding_address[pb->subs[e2].key] = pb->safe_vars;
5159
5160 omega_copy_eqn (&(pb->eqs[pb->num_eqs]), &(pb->subs[e2]),
5161 pb->num_vars);
5162 pb->eqs[pb->num_eqs++].coef[pb->safe_vars] = -1;
5163 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5164
5165 if (e2 < pb->num_subs - 1)
5166 omega_copy_eqn (&(pb->subs[e2]), &(pb->subs[pb->num_subs - 1]),
5167 pb->num_vars);
5168
5169 pb->num_subs--;
5170 }
5171
5172 omega_unprotect_1 (pb, &idx, NULL);
5173 free (bring_to_life);
5174 }
5175
5176 chain_unprotect (pb);
5177 }
5178
5179 /* Unprotects VAR and simplifies PB. */
5180
5181 enum omega_result
5182 omega_constrain_variable_sign (omega_pb pb, enum omega_eqn_color color,
5183 int var, int sign)
5184 {
5185 int n_vars = pb->num_vars;
5186 int e, j;
5187 int k = pb->forwarding_address[var];
5188
5189 if (k < 0)
5190 {
5191 k = -1 - k;
5192
5193 if (sign != 0)
5194 {
5195 e = pb->num_geqs++;
5196 omega_copy_eqn (&pb->geqs[e], &pb->subs[k], pb->num_vars);
5197
5198 for (j = 0; j <= n_vars; j++)
5199 pb->geqs[e].coef[j] *= sign;
5200
5201 pb->geqs[e].coef[0]--;
5202 pb->geqs[e].touched = 1;
5203 pb->geqs[e].color = color;
5204 }
5205 else
5206 {
5207 e = pb->num_eqs++;
5208 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5209 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5210 pb->eqs[e].color = color;
5211 }
5212 }
5213 else if (sign != 0)
5214 {
5215 e = pb->num_geqs++;
5216 omega_init_eqn_zero (&pb->geqs[e], pb->num_vars);
5217 pb->geqs[e].coef[k] = sign;
5218 pb->geqs[e].coef[0] = -1;
5219 pb->geqs[e].touched = 1;
5220 pb->geqs[e].color = color;
5221 }
5222 else
5223 {
5224 e = pb->num_eqs++;
5225 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5226 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5227 pb->eqs[e].coef[k] = 1;
5228 pb->eqs[e].color = color;
5229 }
5230
5231 omega_unprotect_variable (pb, var);
5232 return omega_simplify_problem (pb);
5233 }
5234
5235 /* Add an equation "VAR = VALUE" with COLOR to PB. */
5236
5237 void
5238 omega_constrain_variable_value (omega_pb pb, enum omega_eqn_color color,
5239 int var, int value)
5240 {
5241 int e;
5242 int k = pb->forwarding_address[var];
5243
5244 if (k < 0)
5245 {
5246 k = -1 - k;
5247 e = pb->num_eqs++;
5248 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
5249 omega_copy_eqn (&pb->eqs[e], &pb->subs[k], pb->num_vars);
5250 pb->eqs[e].coef[0] -= value;
5251 }
5252 else
5253 {
5254 e = pb->num_eqs++;
5255 omega_init_eqn_zero (&pb->eqs[e], pb->num_vars);
5256 pb->eqs[e].coef[k] = 1;
5257 pb->eqs[e].coef[0] = -value;
5258 }
5259
5260 pb->eqs[e].color = color;
5261 }
5262
5263 /* Return false when the upper and lower bounds are not coupled.
5264 Initialize the bounds LOWER_BOUND and UPPER_BOUND for the values of
5265 variable I. */
5266
5267 bool
5268 omega_query_variable (omega_pb pb, int i, int *lower_bound, int *upper_bound)
5269 {
5270 int n_vars = pb->num_vars;
5271 int e, j;
5272 bool is_simple;
5273 bool coupled = false;
5274
5275 *lower_bound = neg_infinity;
5276 *upper_bound = pos_infinity;
5277 i = pb->forwarding_address[i];
5278
5279 if (i < 0)
5280 {
5281 i = -i - 1;
5282
5283 for (j = 1; j <= n_vars; j++)
5284 if (pb->subs[i].coef[j] != 0)
5285 return true;
5286
5287 *upper_bound = *lower_bound = pb->subs[i].coef[0];
5288 return false;
5289 }
5290
5291 for (e = pb->num_subs - 1; e >= 0; e--)
5292 if (pb->subs[e].coef[i] != 0)
5293 coupled = true;
5294
5295 for (e = pb->num_eqs - 1; e >= 0; e--)
5296 if (pb->eqs[e].coef[i] != 0)
5297 {
5298 is_simple = true;
5299
5300 for (j = 1; j <= n_vars; j++)
5301 if (i != j && pb->eqs[e].coef[j] != 0)
5302 {
5303 is_simple = false;
5304 coupled = true;
5305 break;
5306 }
5307
5308 if (!is_simple)
5309 continue;
5310 else
5311 {
5312 *lower_bound = *upper_bound =
5313 -pb->eqs[e].coef[i] * pb->eqs[e].coef[0];
5314 return false;
5315 }
5316 }
5317
5318 for (e = pb->num_geqs - 1; e >= 0; e--)
5319 if (pb->geqs[e].coef[i] != 0)
5320 {
5321 if (pb->geqs[e].key == i)
5322 *lower_bound = MAX (*lower_bound, -pb->geqs[e].coef[0]);
5323
5324 else if (pb->geqs[e].key == -i)
5325 *upper_bound = MIN (*upper_bound, pb->geqs[e].coef[0]);
5326
5327 else
5328 coupled = true;
5329 }
5330
5331 return coupled;
5332 }
5333
5334 /* Sets the lower bound L and upper bound U for the values of variable
5335 I, and sets COULD_BE_ZERO to true if variable I might take value
5336 zero. LOWER_BOUND and UPPER_BOUND are bounds on the values of
5337 variable I. */
5338
5339 static void
5340 query_coupled_variable (omega_pb pb, int i, int *l, int *u,
5341 bool *could_be_zero, int lower_bound, int upper_bound)
5342 {
5343 int e, b1, b2;
5344 eqn eqn;
5345 int sign;
5346 int v;
5347
5348 /* Preconditions. */
5349 gcc_assert (abs (pb->forwarding_address[i]) == 1
5350 && pb->num_vars + pb->num_subs == 2
5351 && pb->num_eqs + pb->num_subs == 1);
5352
5353 /* Define variable I in terms of variable V. */
5354 if (pb->forwarding_address[i] == -1)
5355 {
5356 eqn = &pb->subs[0];
5357 sign = 1;
5358 v = 1;
5359 }
5360 else
5361 {
5362 eqn = &pb->eqs[0];
5363 sign = -eqn->coef[1];
5364 v = 2;
5365 }
5366
5367 for (e = pb->num_geqs - 1; e >= 0; e--)
5368 if (pb->geqs[e].coef[v] != 0)
5369 {
5370 if (pb->geqs[e].coef[v] == 1)
5371 lower_bound = MAX (lower_bound, -pb->geqs[e].coef[0]);
5372
5373 else
5374 upper_bound = MIN (upper_bound, pb->geqs[e].coef[0]);
5375 }
5376
5377 if (lower_bound > upper_bound)
5378 {
5379 *l = pos_infinity;
5380 *u = neg_infinity;
5381 *could_be_zero = 0;
5382 return;
5383 }
5384
5385 if (lower_bound == neg_infinity)
5386 {
5387 if (eqn->coef[v] > 0)
5388 b1 = sign * neg_infinity;
5389
5390 else
5391 b1 = -sign * neg_infinity;
5392 }
5393 else
5394 b1 = sign * (eqn->coef[0] + eqn->coef[v] * lower_bound);
5395
5396 if (upper_bound == pos_infinity)
5397 {
5398 if (eqn->coef[v] > 0)
5399 b2 = sign * pos_infinity;
5400
5401 else
5402 b2 = -sign * pos_infinity;
5403 }
5404 else
5405 b2 = sign * (eqn->coef[0] + eqn->coef[v] * upper_bound);
5406
5407 *l = MAX (*l, b1 <= b2 ? b1 : b2);
5408 *u = MIN (*u, b1 <= b2 ? b2 : b1);
5409
5410 *could_be_zero = (*l <= 0 && 0 <= *u
5411 && int_mod (eqn->coef[0], abs (eqn->coef[v])) == 0);
5412 }
5413
5414 /* Return false when a lower bound L and an upper bound U for variable
5415 I in problem PB have been initialized. */
5416
5417 bool
5418 omega_query_variable_bounds (omega_pb pb, int i, int *l, int *u)
5419 {
5420 *l = neg_infinity;
5421 *u = pos_infinity;
5422
5423 if (!omega_query_variable (pb, i, l, u)
5424 || (pb->num_vars == 1 && pb->forwarding_address[i] == 1))
5425 return false;
5426
5427 if (abs (pb->forwarding_address[i]) == 1
5428 && pb->num_vars + pb->num_subs == 2
5429 && pb->num_eqs + pb->num_subs == 1)
5430 {
5431 bool could_be_zero;
5432 query_coupled_variable (pb, i, l, u, &could_be_zero, neg_infinity,
5433 pos_infinity);
5434 return false;
5435 }
5436
5437 return true;
5438 }
5439
5440 /* For problem PB, return an integer that represents the classic data
5441 dependence direction in function of the DD_LT, DD_EQ and DD_GT bit
5442 masks that are added to the result. When DIST_KNOWN is true, DIST
5443 is set to the classic data dependence distance. LOWER_BOUND and
5444 UPPER_BOUND are bounds on the value of variable I, for example, it
5445 is possible to narrow the iteration domain with safe approximations
5446 of loop counts, and thus discard some data dependences that cannot
5447 occur. */
5448
5449 int
5450 omega_query_variable_signs (omega_pb pb, int i, int dd_lt,
5451 int dd_eq, int dd_gt, int lower_bound,
5452 int upper_bound, bool *dist_known, int *dist)
5453 {
5454 int result;
5455 int l, u;
5456 bool could_be_zero;
5457
5458 l = neg_infinity;
5459 u = pos_infinity;
5460
5461 omega_query_variable (pb, i, &l, &u);
5462 query_coupled_variable (pb, i, &l, &u, &could_be_zero, lower_bound,
5463 upper_bound);
5464 result = 0;
5465
5466 if (l < 0)
5467 result |= dd_gt;
5468
5469 if (u > 0)
5470 result |= dd_lt;
5471
5472 if (could_be_zero)
5473 result |= dd_eq;
5474
5475 if (l == u)
5476 {
5477 *dist_known = true;
5478 *dist = l;
5479 }
5480 else
5481 *dist_known = false;
5482
5483 return result;
5484 }
5485
5486 /* Initialize PB as an Omega problem with NVARS variables and NPROT
5487 safe variables. Safe variables are not eliminated during the
5488 Fourier-Motzkin elimination. Safe variables are all those
5489 variables that are placed at the beginning of the array of
5490 variables: P->var[0, ..., NPROT - 1]. */
5491
5492 omega_pb
5493 omega_alloc_problem (int nvars, int nprot)
5494 {
5495 omega_pb pb;
5496
5497 gcc_assert (nvars <= OMEGA_MAX_VARS);
5498 omega_initialize ();
5499
5500 /* Allocate and initialize PB. */
5501 pb = XCNEW (struct omega_pb);
5502 pb->var = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5503 pb->forwarding_address = XCNEWVEC (int, OMEGA_MAX_VARS + 2);
5504 pb->geqs = omega_alloc_eqns (0, OMEGA_MAX_GEQS);
5505 pb->eqs = omega_alloc_eqns (0, OMEGA_MAX_EQS);
5506 pb->subs = omega_alloc_eqns (0, OMEGA_MAX_VARS + 1);
5507
5508 pb->hash_version = hash_version;
5509 pb->num_vars = nvars;
5510 pb->safe_vars = nprot;
5511 pb->variables_initialized = false;
5512 pb->variables_freed = false;
5513 pb->num_eqs = 0;
5514 pb->num_geqs = 0;
5515 pb->num_subs = 0;
5516 return pb;
5517 }
5518
5519 /* Keeps the state of the initialization. */
5520 static bool omega_initialized = false;
5521
5522 /* Initialization of the Omega solver. */
5523
5524 void
5525 omega_initialize (void)
5526 {
5527 int i;
5528
5529 if (omega_initialized)
5530 return;
5531
5532 next_wild_card = 0;
5533 next_key = OMEGA_MAX_VARS + 1;
5534 packing = XCNEWVEC (int, OMEGA_MAX_VARS);
5535 fast_lookup = XCNEWVEC (int, MAX_KEYS * 2);
5536 fast_lookup_red = XCNEWVEC (int, MAX_KEYS * 2);
5537 hash_master = omega_alloc_eqns (0, HASH_TABLE_SIZE);
5538
5539 for (i = 0; i < HASH_TABLE_SIZE; i++)
5540 hash_master[i].touched = -1;
5541
5542 sprintf (wild_name[0], "1");
5543 sprintf (wild_name[1], "a");
5544 sprintf (wild_name[2], "b");
5545 sprintf (wild_name[3], "c");
5546 sprintf (wild_name[4], "d");
5547 sprintf (wild_name[5], "e");
5548 sprintf (wild_name[6], "f");
5549 sprintf (wild_name[7], "g");
5550 sprintf (wild_name[8], "h");
5551 sprintf (wild_name[9], "i");
5552 sprintf (wild_name[10], "j");
5553 sprintf (wild_name[11], "k");
5554 sprintf (wild_name[12], "l");
5555 sprintf (wild_name[13], "m");
5556 sprintf (wild_name[14], "n");
5557 sprintf (wild_name[15], "o");
5558 sprintf (wild_name[16], "p");
5559 sprintf (wild_name[17], "q");
5560 sprintf (wild_name[18], "r");
5561 sprintf (wild_name[19], "s");
5562 sprintf (wild_name[20], "t");
5563 sprintf (wild_name[40 - 1], "alpha");
5564 sprintf (wild_name[40 - 2], "beta");
5565 sprintf (wild_name[40 - 3], "gamma");
5566 sprintf (wild_name[40 - 4], "delta");
5567 sprintf (wild_name[40 - 5], "tau");
5568 sprintf (wild_name[40 - 6], "sigma");
5569 sprintf (wild_name[40 - 7], "chi");
5570 sprintf (wild_name[40 - 8], "omega");
5571 sprintf (wild_name[40 - 9], "pi");
5572 sprintf (wild_name[40 - 10], "ni");
5573 sprintf (wild_name[40 - 11], "Alpha");
5574 sprintf (wild_name[40 - 12], "Beta");
5575 sprintf (wild_name[40 - 13], "Gamma");
5576 sprintf (wild_name[40 - 14], "Delta");
5577 sprintf (wild_name[40 - 15], "Tau");
5578 sprintf (wild_name[40 - 16], "Sigma");
5579 sprintf (wild_name[40 - 17], "Chi");
5580 sprintf (wild_name[40 - 18], "Omega");
5581 sprintf (wild_name[40 - 19], "xxx");
5582
5583 omega_initialized = true;
5584 }
Mirror of the offical gcc git repository hosted at gcc.gnu.org