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