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