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