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