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