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