OpenCores
URL https://opencores.org/ocsvn/openrisc_me/openrisc_me/trunk

Subversion Repositories openrisc_me

[/] [openrisc/] [trunk/] [gnu-src/] [gcc-4.5.1/] [gcc/] [omega.c] - Blame information for rev 280

Details | Compare with Previous | View Log

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

powered by: WebSVN 2.1.0

© copyright 1999-2024 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.