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