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