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