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