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