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