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