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