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