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