Coverage Report

Created: 2018-12-09 11:54

/Users/buildslave/jenkins/workspace/clang-stage2-coverage-R/llvm/tools/polly/lib/External/isl/isl_map_simplify.c
Line
Count
Source (jump to first uncovered line)
1
/*
2
 * Copyright 2008-2009 Katholieke Universiteit Leuven
3
 * Copyright 2012-2013 Ecole Normale Superieure
4
 * Copyright 2014-2015 INRIA Rocquencourt
5
 * Copyright 2016      Sven Verdoolaege
6
 *
7
 * Use of this software is governed by the MIT license
8
 *
9
 * Written by Sven Verdoolaege, K.U.Leuven, Departement
10
 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
11
 * and Ecole Normale Superieure, 45 rue d’Ulm, 75230 Paris, France
12
 * and Inria Paris - Rocquencourt, Domaine de Voluceau - Rocquencourt,
13
 * B.P. 105 - 78153 Le Chesnay, France
14
 */
15
16
#include <isl_ctx_private.h>
17
#include <isl_map_private.h>
18
#include "isl_equalities.h"
19
#include <isl/map.h>
20
#include <isl_seq.h>
21
#include "isl_tab.h"
22
#include <isl_space_private.h>
23
#include <isl_mat_private.h>
24
#include <isl_vec_private.h>
25
26
#include <bset_to_bmap.c>
27
#include <bset_from_bmap.c>
28
#include <set_to_map.c>
29
#include <set_from_map.c>
30
31
static void swap_equality(struct isl_basic_map *bmap, int a, int b)
32
950k
{
33
950k
  isl_int *t = bmap->eq[a];
34
950k
  bmap->eq[a] = bmap->eq[b];
35
950k
  bmap->eq[b] = t;
36
950k
}
37
38
static void swap_inequality(struct isl_basic_map *bmap, int a, int b)
39
50.2k
{
40
50.2k
  if (a != b) {
41
50.2k
    isl_int *t = bmap->ineq[a];
42
50.2k
    bmap->ineq[a] = bmap->ineq[b];
43
50.2k
    bmap->ineq[b] = t;
44
50.2k
  }
45
50.2k
}
46
47
__isl_give isl_basic_map *isl_basic_map_normalize_constraints(
48
  __isl_take isl_basic_map *bmap)
49
3.00M
{
50
3.00M
  int i;
51
3.00M
  isl_int gcd;
52
3.00M
  unsigned total = isl_basic_map_total_dim(bmap);
53
3.00M
54
3.00M
  if (!bmap)
55
0
    return NULL;
56
3.00M
57
3.00M
  isl_int_init(gcd);
58
6.37M
  for (i = bmap->n_eq - 1; i >= 0; 
--i3.37M
) {
59
3.37M
    isl_seq_gcd(bmap->eq[i]+1, total, &gcd);
60
3.37M
    if (isl_int_is_zero(gcd)) {
61
282k
      if (!isl_int_is_zero(bmap->eq[i][0])) {
62
541
        bmap = isl_basic_map_set_to_empty(bmap);
63
541
        break;
64
541
      }
65
282k
      isl_basic_map_drop_equality(bmap, i);
66
282k
      continue;
67
282k
    }
68
3.09M
    if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
69
3.09M
      
isl_int_gcd176k
(gcd, gcd, bmap->eq[i][0]);
70
3.09M
    if (isl_int_is_one(gcd))
71
3.09M
      
continue3.06M
;
72
32.1k
    if (!isl_int_is_divisible_by(bmap->eq[i][0], gcd)) {
73
1.38k
      bmap = isl_basic_map_set_to_empty(bmap);
74
1.38k
      break;
75
1.38k
    }
76
30.7k
    isl_seq_scale_down(bmap->eq[i], bmap->eq[i], gcd, 1+total);
77
30.7k
  }
78
3.00M
79
15.2M
  for (i = bmap->n_ineq - 1; i >= 0; 
--i12.2M
) {
80
12.3M
    isl_seq_gcd(bmap->ineq[i]+1, total, &gcd);
81
12.3M
    if (isl_int_is_zero(gcd)) {
82
562k
      if (isl_int_is_neg(bmap->ineq[i][0])) {
83
26.1k
        bmap = isl_basic_map_set_to_empty(bmap);
84
26.1k
        break;
85
26.1k
      }
86
536k
      isl_basic_map_drop_inequality(bmap, i);
87
536k
      continue;
88
536k
    }
89
11.7M
    if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
90
11.7M
      
isl_int_gcd325k
(gcd, gcd, bmap->ineq[i][0]);
91
11.7M
    if (isl_int_is_one(gcd))
92
11.7M
      
continue11.6M
;
93
121k
    isl_int_fdiv_q(bmap->ineq[i][0], bmap->ineq[i][0], gcd);
94
121k
    isl_seq_scale_down(bmap->ineq[i]+1, bmap->ineq[i]+1, gcd, total);
95
121k
  }
96
3.00M
  isl_int_clear(gcd);
97
3.00M
98
3.00M
  return bmap;
99
3.00M
}
100
101
__isl_give isl_basic_set *isl_basic_set_normalize_constraints(
102
  __isl_take isl_basic_set *bset)
103
224k
{
104
224k
  isl_basic_map *bmap = bset_to_bmap(bset);
105
224k
  return bset_from_bmap(isl_basic_map_normalize_constraints(bmap));
106
224k
}
107
108
/* Reduce the coefficient of the variable at position "pos"
109
 * in integer division "div", such that it lies in the half-open
110
 * interval (1/2,1/2], extracting any excess value from this integer division.
111
 * "pos" is as determined by isl_basic_map_offset, i.e., pos == 0
112
 * corresponds to the constant term.
113
 *
114
 * That is, the integer division is of the form
115
 *
116
 *  floor((... + (c * d + r) * x_pos + ...)/d)
117
 *
118
 * with -d < 2 * r <= d.
119
 * Replace it by
120
 *
121
 *  floor((... + r * x_pos + ...)/d) + c * x_pos
122
 *
123
 * If 2 * ((c * d + r) % d) <= d, then c = floor((c * d + r)/d).
124
 * Otherwise, c = floor((c * d + r)/d) + 1.
125
 *
126
 * This is the same normalization that is performed by isl_aff_floor.
127
 */
128
static __isl_give isl_basic_map *reduce_coefficient_in_div(
129
  __isl_take isl_basic_map *bmap, int div, int pos)
130
14.2k
{
131
14.2k
  isl_int shift;
132
14.2k
  int add_one;
133
14.2k
134
14.2k
  isl_int_init(shift);
135
14.2k
  isl_int_fdiv_r(shift, bmap->div[div][1 + pos], bmap->div[div][0]);
136
14.2k
  isl_int_mul_ui(shift, shift, 2);
137
14.2k
  add_one = isl_int_gt(shift, bmap->div[div][0]);
138
14.2k
  isl_int_fdiv_q(shift, bmap->div[div][1 + pos], bmap->div[div][0]);
139
14.2k
  if (add_one)
140
14.2k
    
isl_int_add_ui2.30k
(shift, shift, 1);
141
14.2k
  isl_int_neg(shift, shift);
142
14.2k
  bmap = isl_basic_map_shift_div(bmap, div, pos, shift);
143
14.2k
  isl_int_clear(shift);
144
14.2k
145
14.2k
  return bmap;
146
14.2k
}
147
148
/* Does the coefficient of the variable at position "pos"
149
 * in integer division "div" need to be reduced?
150
 * That is, does it lie outside the half-open interval (1/2,1/2]?
151
 * The coefficient c/d lies outside this interval if abs(2 * c) >= d and
152
 * 2 * c != d.
153
 */
154
static isl_bool needs_reduction(__isl_keep isl_basic_map *bmap, int div,
155
  int pos)
156
1.45M
{
157
1.45M
  isl_bool r;
158
1.45M
159
1.45M
  if (isl_int_is_zero(bmap->div[div][1 + pos]))
160
1.45M
    
return isl_bool_false1.20M
;
161
256k
162
256k
  isl_int_mul_ui(bmap->div[div][1 + pos], bmap->div[div][1 + pos], 2);
163
256k
  r = isl_int_abs_ge(bmap->div[div][1 + pos], bmap->div[div][0]) &&
164
256k
      
!110k
isl_int_eq110k
(bmap->div[div][1 + pos], bmap->div[div][0]);
165
256k
  isl_int_divexact_ui(bmap->div[div][1 + pos],
166
256k
          bmap->div[div][1 + pos], 2);
167
256k
168
256k
  return r;
169
256k
}
170
171
/* Reduce the coefficients (including the constant term) of
172
 * integer division "div", if needed.
173
 * In particular, make sure all coefficients lie in
174
 * the half-open interval (1/2,1/2].
175
 */
176
static __isl_give isl_basic_map *reduce_div_coefficients_of_div(
177
  __isl_take isl_basic_map *bmap, int div)
178
148k
{
179
148k
  int i;
180
148k
  unsigned total = 1 + isl_basic_map_total_dim(bmap);
181
148k
182
1.60M
  for (i = 0; i < total; 
++i1.45M
) {
183
1.45M
    isl_bool reduce;
184
1.45M
185
1.45M
    reduce = needs_reduction(bmap, div, i);
186
1.45M
    if (reduce < 0)
187
0
      return isl_basic_map_free(bmap);
188
1.45M
    if (!reduce)
189
1.44M
      continue;
190
14.2k
    bmap = reduce_coefficient_in_div(bmap, div, i);
191
14.2k
    if (!bmap)
192
0
      break;
193
14.2k
  }
194
148k
195
148k
  return bmap;
196
148k
}
197
198
/* Reduce the coefficients (including the constant term) of
199
 * the known integer divisions, if needed
200
 * In particular, make sure all coefficients lie in
201
 * the half-open interval (1/2,1/2].
202
 */
203
static __isl_give isl_basic_map *reduce_div_coefficients(
204
  __isl_take isl_basic_map *bmap)
205
2.74M
{
206
2.74M
  int i;
207
2.74M
208
2.74M
  if (!bmap)
209
0
    return NULL;
210
2.74M
  if (bmap->n_div == 0)
211
2.46M
    return bmap;
212
281k
213
851k
  
for (i = 0; 281k
i < bmap->n_div;
++i570k
) {
214
570k
    if (isl_int_is_zero(bmap->div[i][0]))
215
570k
      
continue422k
;
216
148k
    bmap = reduce_div_coefficients_of_div(bmap, i);
217
148k
    if (!bmap)
218
0
      break;
219
148k
  }
220
281k
221
281k
  return bmap;
222
281k
}
223
224
/* Remove any common factor in numerator and denominator of the div expression,
225
 * not taking into account the constant term.
226
 * That is, if the div is of the form
227
 *
228
 *  floor((a + m f(x))/(m d))
229
 *
230
 * then replace it by
231
 *
232
 *  floor((floor(a/m) + f(x))/d)
233
 *
234
 * The difference {a/m}/d in the argument satisfies 0 <= {a/m}/d < 1/d
235
 * and can therefore not influence the result of the floor.
236
 */
237
static void normalize_div_expression(__isl_keep isl_basic_map *bmap, int div)
238
590k
{
239
590k
  unsigned total = isl_basic_map_total_dim(bmap);
240
590k
  isl_ctx *ctx = bmap->ctx;
241
590k
242
590k
  if (isl_int_is_zero(bmap->div[div][0]))
243
590k
    
return422k
;
244
168k
  isl_seq_gcd(bmap->div[div] + 2, total, &ctx->normalize_gcd);
245
168k
  isl_int_gcd(ctx->normalize_gcd, ctx->normalize_gcd, bmap->div[div][0]);
246
168k
  if (isl_int_is_one(ctx->normalize_gcd))
247
168k
    
return161k
;
248
7.00k
  isl_int_fdiv_q(bmap->div[div][1], bmap->div[div][1],
249
7.00k
      ctx->normalize_gcd);
250
7.00k
  isl_int_divexact(bmap->div[div][0], bmap->div[div][0],
251
7.00k
      ctx->normalize_gcd);
252
7.00k
  isl_seq_scale_down(bmap->div[div] + 2, bmap->div[div] + 2,
253
7.00k
      ctx->normalize_gcd, total);
254
7.00k
}
255
256
/* Remove any common factor in numerator and denominator of a div expression,
257
 * not taking into account the constant term.
258
 * That is, look for any div of the form
259
 *
260
 *  floor((a + m f(x))/(m d))
261
 *
262
 * and replace it by
263
 *
264
 *  floor((floor(a/m) + f(x))/d)
265
 *
266
 * The difference {a/m}/d in the argument satisfies 0 <= {a/m}/d < 1/d
267
 * and can therefore not influence the result of the floor.
268
 */
269
static __isl_give isl_basic_map *normalize_div_expressions(
270
  __isl_take isl_basic_map *bmap)
271
2.74M
{
272
2.74M
  int i;
273
2.74M
274
2.74M
  if (!bmap)
275
0
    return NULL;
276
2.74M
  if (bmap->n_div == 0)
277
2.46M
    return bmap;
278
281k
279
851k
  
for (i = 0; 281k
i < bmap->n_div;
++i570k
)
280
570k
    normalize_div_expression(bmap, i);
281
281k
282
281k
  return bmap;
283
281k
}
284
285
/* Assumes divs have been ordered if keep_divs is set.
286
 */
287
static void eliminate_var_using_equality(struct isl_basic_map *bmap,
288
  unsigned pos, isl_int *eq, int keep_divs, int *progress)
289
4.66M
{
290
4.66M
  unsigned total;
291
4.66M
  unsigned space_total;
292
4.66M
  int k;
293
4.66M
  int last_div;
294
4.66M
295
4.66M
  total = isl_basic_map_total_dim(bmap);
296
4.66M
  space_total = isl_space_dim(bmap->dim, isl_dim_all);
297
4.66M
  last_div = isl_seq_last_non_zero(eq + 1 + space_total, bmap->n_div);
298
34.7M
  for (k = 0; k < bmap->n_eq; 
++k30.0M
) {
299
30.0M
    if (bmap->eq[k] == eq)
300
4.65M
      continue;
301
25.4M
    if (isl_int_is_zero(bmap->eq[k][1+pos]))
302
25.4M
      
continue24.1M
;
303
1.26M
    if (progress)
304
206k
      *progress = 1;
305
1.26M
    isl_seq_elim(bmap->eq[k], eq, 1+pos, 1+total, NULL);
306
1.26M
    isl_seq_normalize(bmap->ctx, bmap->eq[k], 1 + total);
307
1.26M
  }
308
4.66M
309
23.5M
  for (k = 0; k < bmap->n_ineq; 
++k18.8M
) {
310
18.8M
    if (isl_int_is_zero(bmap->ineq[k][1+pos]))
311
18.8M
      
continue17.9M
;
312
893k
    if (progress)
313
305k
      *progress = 1;
314
893k
    isl_seq_elim(bmap->ineq[k], eq, 1+pos, 1+total, NULL);
315
893k
    isl_seq_normalize(bmap->ctx, bmap->ineq[k], 1 + total);
316
893k
    ISL_F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
317
893k
  }
318
4.66M
319
6.00M
  for (k = 0; k < bmap->n_div; 
++k1.33M
) {
320
1.33M
    if (isl_int_is_zero(bmap->div[k][0]))
321
1.33M
      
continue885k
;
322
451k
    if (isl_int_is_zero(bmap->div[k][1+1+pos]))
323
451k
      
continue431k
;
324
19.8k
    if (progress)
325
11.7k
      *progress = 1;
326
19.8k
    /* We need to be careful about circular definitions,
327
19.8k
     * so for now we just remove the definition of div k
328
19.8k
     * if the equality contains any divs.
329
19.8k
     * If keep_divs is set, then the divs have been ordered
330
19.8k
     * and we can keep the definition as long as the result
331
19.8k
     * is still ordered.
332
19.8k
     */
333
19.8k
    if (last_div == -1 || 
(6.08k
keep_divs6.08k
&&
last_div < k6.08k
)) {
334
19.8k
      isl_seq_elim(bmap->div[k]+1, eq,
335
19.8k
          1+pos, 1+total, &bmap->div[k][0]);
336
19.8k
      normalize_div_expression(bmap, k);
337
19.8k
    } else
338
0
      isl_seq_clr(bmap->div[k], 1 + total);
339
19.8k
    ISL_F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
340
19.8k
  }
341
4.66M
}
342
343
/* Assumes divs have been ordered if keep_divs is set.
344
 */
345
static __isl_give isl_basic_map *eliminate_div(__isl_take isl_basic_map *bmap,
346
  isl_int *eq, unsigned div, int keep_divs)
347
335k
{
348
335k
  unsigned pos = isl_space_dim(bmap->dim, isl_dim_all) + div;
349
335k
350
335k
  eliminate_var_using_equality(bmap, pos, eq, keep_divs, NULL);
351
335k
352
335k
  bmap = isl_basic_map_drop_div(bmap, div);
353
335k
354
335k
  return bmap;
355
335k
}
356
357
/* Check if elimination of div "div" using equality "eq" would not
358
 * result in a div depending on a later div.
359
 */
360
static isl_bool ok_to_eliminate_div(__isl_keep isl_basic_map *bmap, isl_int *eq,
361
  unsigned div)
362
339k
{
363
339k
  int k;
364
339k
  int last_div;
365
339k
  unsigned space_total = isl_space_dim(bmap->dim, isl_dim_all);
366
339k
  unsigned pos = space_total + div;
367
339k
368
339k
  last_div = isl_seq_last_non_zero(eq + 1 + space_total, bmap->n_div);
369
339k
  if (last_div < 0 || last_div <= div)
370
328k
    return isl_bool_true;
371
10.8k
372
36.6k
  
for (k = 0; 10.8k
k <= last_div;
++k25.7k
) {
373
36.1k
    if (isl_int_is_zero(bmap->div[k][0]))
374
36.1k
      
continue14.5k
;
375
21.6k
    if (!isl_int_is_zero(bmap->div[k][1 + 1 + pos]))
376
21.6k
      
return isl_bool_false10.3k
;
377
21.6k
  }
378
10.8k
379
10.8k
  
return isl_bool_true489
;
380
10.8k
}
381
382
/* Eliminate divs based on equalities
383
 */
384
static __isl_give isl_basic_map *eliminate_divs_eq(
385
  __isl_take isl_basic_map *bmap, int *progress)
386
2.89M
{
387
2.89M
  int d;
388
2.89M
  int i;
389
2.89M
  int modified = 0;
390
2.89M
  unsigned off;
391
2.89M
392
2.89M
  bmap = isl_basic_map_order_divs(bmap);
393
2.89M
394
2.89M
  if (!bmap)
395
0
    return NULL;
396
2.89M
397
2.89M
  off = 1 + isl_space_dim(bmap->dim, isl_dim_all);
398
2.89M
399
3.50M
  for (d = bmap->n_div - 1; d >= 0 ; 
--d607k
) {
400
1.57M
    for (i = 0; i < bmap->n_eq; 
++i963k
) {
401
1.29M
      isl_bool ok;
402
1.29M
403
1.29M
      if (!isl_int_is_one(bmap->eq[i][off + d]) &&
404
1.29M
          
!1.02M
isl_int_is_negone1.02M
(bmap->eq[i][off + d]))
405
1.29M
        
continue953k
;
406
339k
      ok = ok_to_eliminate_div(bmap, bmap->eq[i], d);
407
339k
      if (ok < 0)
408
0
        return isl_basic_map_free(bmap);
409
339k
      if (!ok)
410
10.3k
        continue;
411
328k
      modified = 1;
412
328k
      *progress = 1;
413
328k
      bmap = eliminate_div(bmap, bmap->eq[i], d, 1);
414
328k
      if (isl_basic_map_drop_equality(bmap, i) < 0)
415
0
        return isl_basic_map_free(bmap);
416
328k
      break;
417
328k
    }
418
607k
  }
419
2.89M
  if (modified)
420
149k
    return eliminate_divs_eq(bmap, progress);
421
2.74M
  return bmap;
422
2.74M
}
423
424
/* Eliminate divs based on inequalities
425
 */
426
static __isl_give isl_basic_map *eliminate_divs_ineq(
427
  __isl_take isl_basic_map *bmap, int *progress)
428
2.74M
{
429
2.74M
  int d;
430
2.74M
  int i;
431
2.74M
  unsigned off;
432
2.74M
  struct isl_ctx *ctx;
433
2.74M
434
2.74M
  if (!bmap)
435
0
    return NULL;
436
2.74M
437
2.74M
  ctx = bmap->ctx;
438
2.74M
  off = 1 + isl_space_dim(bmap->dim, isl_dim_all);
439
2.74M
440
2.98M
  for (d = bmap->n_div - 1; d >= 0 ; 
--d234k
) {
441
441k
    for (i = 0; i < bmap->n_eq; 
++i206k
)
442
283k
      if (!isl_int_is_zero(bmap->eq[i][off + d]))
443
283k
        
break76.1k
;
444
234k
    if (i < bmap->n_eq)
445
76.1k
      continue;
446
798k
    
for (i = 0; 158k
i < bmap->n_ineq;
++i639k
)
447
718k
      if (isl_int_abs_gt(bmap->ineq[i][off + d], ctx->one))
448
718k
        
break78.9k
;
449
158k
    if (i < bmap->n_ineq)
450
78.9k
      continue;
451
79.8k
    *progress = 1;
452
79.8k
    bmap = isl_basic_map_eliminate_vars(bmap, (off-1)+d, 1);
453
79.8k
    if (!bmap || ISL_F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
454
79.8k
      
break148
;
455
79.7k
    bmap = isl_basic_map_drop_div(bmap, d);
456
79.7k
    if (!bmap)
457
0
      break;
458
79.7k
  }
459
2.74M
  return bmap;
460
2.74M
}
461
462
/* Does the equality constraint at position "eq" in "bmap" involve
463
 * any local variables in the range [first, first + n)
464
 * that are not marked as having an explicit representation?
465
 */
466
static isl_bool bmap_eq_involves_unknown_divs(__isl_keep isl_basic_map *bmap,
467
  int eq, unsigned first, unsigned n)
468
3.06k
{
469
3.06k
  unsigned o_div;
470
3.06k
  int i;
471
3.06k
472
3.06k
  if (!bmap)
473
0
    return isl_bool_error;
474
3.06k
475
3.06k
  o_div = isl_basic_map_offset(bmap, isl_dim_div);
476
4.46k
  for (i = 0; i < n; 
++i1.39k
) {
477
2.04k
    isl_bool unknown;
478
2.04k
479
2.04k
    if (isl_int_is_zero(bmap->eq[eq][o_div + first + i]))
480
2.04k
      
continue1.25k
;
481
797
    unknown = isl_basic_map_div_is_marked_unknown(bmap, first + i);
482
797
    if (unknown < 0)
483
0
      return isl_bool_error;
484
797
    if (unknown)
485
649
      return isl_bool_true;
486
797
  }
487
3.06k
488
3.06k
  
return isl_bool_false2.41k
;
489
3.06k
}
490
491
/* The last local variable involved in the equality constraint
492
 * at position "eq" in "bmap" is the local variable at position "div".
493
 * It can therefore be used to extract an explicit representation
494
 * for that variable.
495
 * Do so unless the local variable already has an explicit representation or
496
 * the explicit representation would involve any other local variables
497
 * that in turn do not have an explicit representation.
498
 * An equality constraint involving local variables without an explicit
499
 * representation can be used in isl_basic_map_drop_redundant_divs
500
 * to separate out an independent local variable.  Introducing
501
 * an explicit representation here would block this transformation,
502
 * while the partial explicit representation in itself is not very useful.
503
 * Set *progress if anything is changed.
504
 *
505
 * The equality constraint is of the form
506
 *
507
 *  f(x) + n e >= 0
508
 *
509
 * with n a positive number.  The explicit representation derived from
510
 * this constraint is
511
 *
512
 *  floor((-f(x))/n)
513
 */
514
static __isl_give isl_basic_map *set_div_from_eq(__isl_take isl_basic_map *bmap,
515
  int div, int eq, int *progress)
516
88.7k
{
517
88.7k
  unsigned total, o_div;
518
88.7k
  isl_bool involves;
519
88.7k
520
88.7k
  if (!bmap)
521
0
    return NULL;
522
88.7k
523
88.7k
  if (!isl_int_is_zero(bmap->div[div][0]))
524
88.7k
    
return bmap85.7k
;
525
3.06k
526
3.06k
  involves = bmap_eq_involves_unknown_divs(bmap, eq, 0, div);
527
3.06k
  if (involves < 0)
528
0
    return isl_basic_map_free(bmap);
529
3.06k
  if (involves)
530
649
    return bmap;
531
2.41k
532
2.41k
  total = isl_basic_map_dim(bmap, isl_dim_all);
533
2.41k
  o_div = isl_basic_map_offset(bmap, isl_dim_div);
534
2.41k
  isl_seq_neg(bmap->div[div] + 1, bmap->eq[eq], 1 + total);
535
2.41k
  isl_int_set_si(bmap->div[div][1 + o_div + div], 0);
536
2.41k
  isl_int_set(bmap->div[div][0], bmap->eq[eq][o_div + div]);
537
2.41k
  if (progress)
538
1.92k
    *progress = 1;
539
2.41k
  ISL_F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
540
2.41k
541
2.41k
  return bmap;
542
2.41k
}
543
544
__isl_give isl_basic_map *isl_basic_map_gauss(__isl_take isl_basic_map *bmap,
545
  int *progress)
546
4.56M
{
547
4.56M
  int k;
548
4.56M
  int done;
549
4.56M
  int last_var;
550
4.56M
  unsigned total_var;
551
4.56M
  unsigned total;
552
4.56M
553
4.56M
  bmap = isl_basic_map_order_divs(bmap);
554
4.56M
555
4.56M
  if (!bmap)
556
0
    return NULL;
557
4.56M
558
4.56M
  total = isl_basic_map_total_dim(bmap);
559
4.56M
  total_var = total - bmap->n_div;
560
4.56M
561
4.56M
  last_var = total - 1;
562
8.89M
  for (done = 0; done < bmap->n_eq; 
++done4.32M
) {
563
9.78M
    for (; last_var >= 0; 
--last_var5.18M
) {
564
34.6M
      for (k = done; k < bmap->n_eq; 
++k25.1M
)
565
29.4M
        if (!isl_int_is_zero(bmap->eq[k][1+last_var]))
566
29.4M
          
break4.32M
;
567
9.50M
      if (k < bmap->n_eq)
568
4.32M
        break;
569
9.50M
    }
570
4.59M
    if (last_var < 0)
571
275k
      break;
572
4.32M
    if (k != done)
573
950k
      swap_equality(bmap, k, done);
574
4.32M
    if (isl_int_is_neg(bmap->eq[done][1+last_var]))
575
4.32M
      
isl_seq_neg(bmap->eq[done], bmap->eq[done], 1+total)422k
;
576
4.32M
577
4.32M
    eliminate_var_using_equality(bmap, last_var, bmap->eq[done], 1,
578
4.32M
            progress);
579
4.32M
580
4.32M
    if (last_var >= total_var)
581
88.7k
      bmap = set_div_from_eq(bmap, last_var - total_var,
582
88.7k
            done, progress);
583
4.32M
    if (!bmap)
584
0
      return NULL;
585
4.32M
  }
586
4.56M
  if (done == bmap->n_eq)
587
4.29M
    return bmap;
588
897k
  
for (k = done; 275k
k < bmap->n_eq;
++k622k
) {
589
685k
    if (isl_int_is_zero(bmap->eq[k][0]))
590
685k
      
continue622k
;
591
62.7k
    return isl_basic_map_set_to_empty(bmap);
592
62.7k
  }
593
275k
  isl_basic_map_free_equality(bmap, bmap->n_eq-done);
594
212k
  return bmap;
595
275k
}
596
597
__isl_give isl_basic_set *isl_basic_set_gauss(
598
  __isl_take isl_basic_set *bset, int *progress)
599
153k
{
600
153k
  return bset_from_bmap(isl_basic_map_gauss(bset_to_bmap(bset),
601
153k
              progress));
602
153k
}
603
604
605
static unsigned int round_up(unsigned int v)
606
1.93M
{
607
1.93M
  int old_v = v;
608
1.93M
609
5.97M
  while (v) {
610
4.04M
    old_v = v;
611
4.04M
    v ^= v & -v;
612
4.04M
  }
613
1.93M
  return old_v << 1;
614
1.93M
}
615
616
/* Hash table of inequalities in a basic map.
617
 * "index" is an array of addresses of inequalities in the basic map, some
618
 * of which are NULL.  The inequalities are hashed on the coefficients
619
 * except the constant term.
620
 * "size" is the number of elements in the array and is always a power of two
621
 * "bits" is the number of bits need to represent an index into the array.
622
 * "total" is the total dimension of the basic map.
623
 */
624
struct isl_constraint_index {
625
  unsigned int size;
626
  int bits;
627
  isl_int ***index;
628
  unsigned total;
629
};
630
631
/* Fill in the "ci" data structure for holding the inequalities of "bmap".
632
 */
633
static isl_stat create_constraint_index(struct isl_constraint_index *ci,
634
  __isl_keep isl_basic_map *bmap)
635
1.89M
{
636
1.89M
  isl_ctx *ctx;
637
1.89M
638
1.89M
  ci->index = NULL;
639
1.89M
  if (!bmap)
640
0
    return isl_stat_error;
641
1.89M
  ci->total = isl_basic_set_total_dim(bmap);
642
1.89M
  if (bmap->n_ineq == 0)
643
0
    return isl_stat_ok;
644
1.89M
  ci->size = round_up(4 * (bmap->n_ineq + 1) / 3 - 1);
645
1.89M
  ci->bits = ffs(ci->size) - 1;
646
1.89M
  ctx = isl_basic_map_get_ctx(bmap);
647
1.89M
  ci->index = isl_calloc_array(ctx, isl_int **, ci->size);
648
1.89M
  if (!ci->index)
649
0
    return isl_stat_error;
650
1.89M
651
1.89M
  return isl_stat_ok;
652
1.89M
}
653
654
/* Free the memory allocated by create_constraint_index.
655
 */
656
static void constraint_index_free(struct isl_constraint_index *ci)
657
1.89M
{
658
1.89M
  free(ci->index);
659
1.89M
}
660
661
/* Return the position in ci->index that contains the address of
662
 * an inequality that is equal to *ineq up to the constant term,
663
 * provided this address is not identical to "ineq".
664
 * If there is no such inequality, then return the position where
665
 * such an inequality should be inserted.
666
 */
667
static int hash_index_ineq(struct isl_constraint_index *ci, isl_int **ineq)
668
17.9M
{
669
17.9M
  int h;
670
17.9M
  uint32_t hash = isl_seq_get_hash_bits((*ineq) + 1, ci->total, ci->bits);
671
25.5M
  for (h = hash; ci->index[h]; 
h = (h+1) % ci->size7.61M
)
672
14.4M
    if (ineq != ci->index[h] &&
673
14.4M
        
isl_seq_eq((*ineq) + 1, ci->index[h][0]+1, ci->total)13.9M
)
674
6.81M
      break;
675
17.9M
  return h;
676
17.9M
}
677
678
/* Return the position in ci->index that contains the address of
679
 * an inequality that is equal to the k'th inequality of "bmap"
680
 * up to the constant term, provided it does not point to the very
681
 * same inequality.
682
 * If there is no such inequality, then return the position where
683
 * such an inequality should be inserted.
684
 */
685
static int hash_index(struct isl_constraint_index *ci,
686
  __isl_keep isl_basic_map *bmap, int k)
687
17.8M
{
688
17.8M
  return hash_index_ineq(ci, &bmap->ineq[k]);
689
17.8M
}
690
691
static int set_hash_index(struct isl_constraint_index *ci,
692
  __isl_keep isl_basic_set *bset, int k)
693
52.4k
{
694
52.4k
  return hash_index(ci, bset, k);
695
52.4k
}
696
697
/* Fill in the "ci" data structure with the inequalities of "bset".
698
 */
699
static isl_stat setup_constraint_index(struct isl_constraint_index *ci,
700
  __isl_keep isl_basic_set *bset)
701
13.4k
{
702
13.4k
  int k, h;
703
13.4k
704
13.4k
  if (create_constraint_index(ci, bset) < 0)
705
0
    return isl_stat_error;
706
13.4k
707
65.9k
  
for (k = 0; 13.4k
k < bset->n_ineq;
++k52.4k
) {
708
52.4k
    h = set_hash_index(ci, bset, k);
709
52.4k
    ci->index[h] = &bset->ineq[k];
710
52.4k
  }
711
13.4k
712
13.4k
  return isl_stat_ok;
713
13.4k
}
714
715
/* Is the inequality ineq (obviously) redundant with respect
716
 * to the constraints in "ci"?
717
 *
718
 * Look for an inequality in "ci" with the same coefficients and then
719
 * check if the contant term of "ineq" is greater than or equal
720
 * to the constant term of that inequality.  If so, "ineq" is clearly
721
 * redundant.
722
 *
723
 * Note that hash_index_ineq ignores a stored constraint if it has
724
 * the same address as the passed inequality.  It is ok to pass
725
 * the address of a local variable here since it will never be
726
 * the same as the address of a constraint in "ci".
727
 */
728
static isl_bool constraint_index_is_redundant(struct isl_constraint_index *ci,
729
  isl_int *ineq)
730
42.0k
{
731
42.0k
  int h;
732
42.0k
733
42.0k
  h = hash_index_ineq(ci, &ineq);
734
42.0k
  if (!ci->index[h])
735
14.2k
    return isl_bool_false;
736
27.8k
  return isl_int_ge(ineq[0], (*ci->index[h])[0]);
737
27.8k
}
738
739
/* If we can eliminate more than one div, then we need to make
740
 * sure we do it from last div to first div, in order not to
741
 * change the position of the other divs that still need to
742
 * be removed.
743
 */
744
static __isl_give isl_basic_map *remove_duplicate_divs(
745
  __isl_take isl_basic_map *bmap, int *progress)
746
2.74M
{
747
2.74M
  unsigned int size;
748
2.74M
  int *index;
749
2.74M
  int *elim_for;
750
2.74M
  int k, l, h;
751
2.74M
  int bits;
752
2.74M
  struct isl_blk eq;
753
2.74M
  unsigned total_var;
754
2.74M
  unsigned total;
755
2.74M
  struct isl_ctx *ctx;
756
2.74M
757
2.74M
  bmap = isl_basic_map_order_divs(bmap);
758
2.74M
  if (!bmap || bmap->n_div <= 1)
759
2.62M
    return bmap;
760
126k
761
126k
  total_var = isl_space_dim(bmap->dim, isl_dim_all);
762
126k
  total = total_var + bmap->n_div;
763
126k
764
126k
  ctx = bmap->ctx;
765
424k
  for (k = bmap->n_div - 1; k >= 0; 
--k297k
)
766
341k
    if (!isl_int_is_zero(bmap->div[k][0]))
767
341k
      
break43.3k
;
768
126k
  if (k <= 0)
769
86.2k
    return bmap;
770
40.3k
771
40.3k
  size = round_up(4 * bmap->n_div / 3 - 1);
772
40.3k
  if (size == 0)
773
0
    return bmap;
774
40.3k
  elim_for = isl_calloc_array(ctx, int, bmap->n_div);
775
40.3k
  bits = ffs(size) - 1;
776
40.3k
  index = isl_calloc_array(ctx, int, size);
777
40.3k
  if (!elim_for || !index)
778
0
    goto out;
779
40.3k
  eq = isl_blk_alloc(ctx, 1+total);
780
40.3k
  if (isl_blk_is_error(eq))
781
0
    goto out;
782
40.3k
783
40.3k
  isl_seq_clr(eq.data, 1+total);
784
40.3k
  index[isl_seq_get_hash_bits(bmap->div[k], 2+total, bits)] = k + 1;
785
115k
  for (--k; k >= 0; 
--k75.2k
) {
786
75.2k
    uint32_t hash;
787
75.2k
788
75.2k
    if (isl_int_is_zero(bmap->div[k][0]))
789
75.2k
      
continue21.6k
;
790
53.6k
791
53.6k
    hash = isl_seq_get_hash_bits(bmap->div[k], 2+total, bits);
792
70.5k
    for (h = hash; index[h]; 
h = (h+1) % size16.9k
)
793
24.0k
      if (isl_seq_eq(bmap->div[k],
794
24.0k
               bmap->div[index[h]-1], 2+total))
795
7.09k
        break;
796
53.6k
    if (index[h]) {
797
7.09k
      *progress = 1;
798
7.09k
      l = index[h] - 1;
799
7.09k
      elim_for[l] = k + 1;
800
7.09k
    }
801
53.6k
    index[h] = k+1;
802
53.6k
  }
803
166k
  for (l = bmap->n_div - 1; l >= 0; 
--l125k
) {
804
125k
    if (!elim_for[l])
805
118k
      continue;
806
7.09k
    k = elim_for[l] - 1;
807
7.09k
    isl_int_set_si(eq.data[1+total_var+k], -1);
808
7.09k
    isl_int_set_si(eq.data[1+total_var+l], 1);
809
7.09k
    bmap = eliminate_div(bmap, eq.data, l, 1);
810
7.09k
    if (!bmap)
811
0
      break;
812
7.09k
    isl_int_set_si(eq.data[1+total_var+k], 0);
813
7.09k
    isl_int_set_si(eq.data[1+total_var+l], 0);
814
7.09k
  }
815
40.3k
816
40.3k
  isl_blk_free(ctx, eq);
817
40.3k
out:
818
40.3k
  free(index);
819
40.3k
  free(elim_for);
820
40.3k
  return bmap;
821
40.3k
}
822
823
static int n_pure_div_eq(struct isl_basic_map *bmap)
824
32.9k
{
825
32.9k
  int i, j;
826
32.9k
  unsigned total;
827
32.9k
828
32.9k
  total = isl_space_dim(bmap->dim, isl_dim_all);
829
58.5k
  for (i = 0, j = bmap->n_div-1; i < bmap->n_eq; 
++i25.6k
) {
830
91.3k
    while (j >= 0 && 
isl_int_is_zero68.2k
(bmap->eq[i][1 + total + j]))
831
51.7k
      
--j39.5k
;
832
51.7k
    if (j < 0)
833
23.0k
      break;
834
28.6k
    if (isl_seq_first_non_zero(bmap->eq[i] + 1 + total, j) != -1)
835
3.08k
      return 0;
836
28.6k
  }
837
32.9k
  
return i29.8k
;
838
32.9k
}
839
840
/* Normalize divs that appear in equalities.
841
 *
842
 * In particular, we assume that bmap contains some equalities
843
 * of the form
844
 *
845
 *  a x = m * e_i
846
 *
847
 * and we want to replace the set of e_i by a minimal set and
848
 * such that the new e_i have a canonical representation in terms
849
 * of the vector x.
850
 * If any of the equalities involves more than one divs, then
851
 * we currently simply bail out.
852
 *
853
 * Let us first additionally assume that all equalities involve
854
 * a div.  The equalities then express modulo constraints on the
855
 * remaining variables and we can use "parameter compression"
856
 * to find a minimal set of constraints.  The result is a transformation
857
 *
858
 *  x = T(x') = x_0 + G x'
859
 *
860
 * with G a lower-triangular matrix with all elements below the diagonal
861
 * non-negative and smaller than the diagonal element on the same row.
862
 * We first normalize x_0 by making the same property hold in the affine
863
 * T matrix.
864
 * The rows i of G with a 1 on the diagonal do not impose any modulo
865
 * constraint and simply express x_i = x'_i.
866
 * For each of the remaining rows i, we introduce a div and a corresponding
867
 * equality.  In particular
868
 *
869
 *  g_ii e_j = x_i - g_i(x')
870
 *
871
 * where each x'_k is replaced either by x_k (if g_kk = 1) or the
872
 * corresponding div (if g_kk != 1).
873
 *
874
 * If there are any equalities not involving any div, then we
875
 * first apply a variable compression on the variables x:
876
 *
877
 *  x = C x'' x'' = C_2 x
878
 *
879
 * and perform the above parameter compression on A C instead of on A.
880
 * The resulting compression is then of the form
881
 *
882
 *  x'' = T(x') = x_0 + G x'
883
 *
884
 * and in constructing the new divs and the corresponding equalities,
885
 * we have to replace each x'', i.e., the x'_k with (g_kk = 1),
886
 * by the corresponding row from C_2.
887
 */
888
static __isl_give isl_basic_map *normalize_divs(__isl_take isl_basic_map *bmap,
889
  int *progress)
890
2.74M
{
891
2.74M
  int i, j, k;
892
2.74M
  int total;
893
2.74M
  int div_eq;
894
2.74M
  struct isl_mat *B;
895
2.74M
  struct isl_vec *d;
896
2.74M
  struct isl_mat *T = NULL;
897
2.74M
  struct isl_mat *C = NULL;
898
2.74M
  struct isl_mat *C2 = NULL;
899
2.74M
  isl_int v;
900
2.74M
  int *pos = NULL;
901
2.74M
  int dropped, needed;
902
2.74M
903
2.74M
  if (!bmap)
904
0
    return NULL;
905
2.74M
906
2.74M
  if (bmap->n_div == 0)
907
2.65M
    return bmap;
908
91.5k
909
91.5k
  if (bmap->n_eq == 0)
910
29.9k
    return bmap;
911
61.5k
912
61.5k
  if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_NORMALIZED_DIVS))
913
61.5k
    
return bmap28.6k
;
914
32.9k
915
32.9k
  total = isl_space_dim(bmap->dim, isl_dim_all);
916
32.9k
  div_eq = n_pure_div_eq(bmap);
917
32.9k
  if (div_eq == 0)
918
12.5k
    return bmap;
919
20.4k
920
20.4k
  if (div_eq < bmap->n_eq) {
921
13.6k
    B = isl_mat_sub_alloc6(bmap->ctx, bmap->eq, div_eq,
922
13.6k
          bmap->n_eq - div_eq, 0, 1 + total);
923
13.6k
    C = isl_mat_variable_compression(B, &C2);
924
13.6k
    if (!C || !C2)
925
0
      goto error;
926
13.6k
    if (C->n_col == 0) {
927
1
      bmap = isl_basic_map_set_to_empty(bmap);
928
1
      isl_mat_free(C);
929
1
      isl_mat_free(C2);
930
1
      goto done;
931
1
    }
932
20.4k
  }
933
20.4k
934
20.4k
  d = isl_vec_alloc(bmap->ctx, div_eq);
935
20.4k
  if (!d)
936
0
    goto error;
937
45.9k
  
for (i = 0, j = bmap->n_div-1; 20.4k
i < div_eq;
++i25.4k
) {
938
33.1k
    while (j >= 0 && isl_int_is_zero(bmap->eq[i][1 + total + j]))
939
25.4k
      
--j7.65k
;
940
25.4k
    isl_int_set(d->block.data[i], bmap->eq[i][1 + total + j]);
941
25.4k
  }
942
20.4k
  B = isl_mat_sub_alloc6(bmap->ctx, bmap->eq, 0, div_eq, 0, 1 + total);
943
20.4k
944
20.4k
  if (C) {
945
13.6k
    B = isl_mat_product(B, C);
946
13.6k
    C = NULL;
947
13.6k
  }
948
20.4k
949
20.4k
  T = isl_mat_parameter_compression(B, d);
950
20.4k
  if (!T)
951
0
    goto error;
952
20.4k
  if (T->n_col == 0) {
953
1.85k
    bmap = isl_basic_map_set_to_empty(bmap);
954
1.85k
    isl_mat_free(C2);
955
1.85k
    isl_mat_free(T);
956
1.85k
    goto done;
957
1.85k
  }
958
18.5k
  isl_int_init(v);
959
96.6k
  for (i = 0; i < T->n_row - 1; 
++i78.1k
) {
960
78.1k
    isl_int_fdiv_q(v, T->row[1 + i][0], T->row[1 + i][1 + i]);
961
78.1k
    if (isl_int_is_zero(v))
962
78.1k
      
continue71.1k
;
963
7.00k
    isl_mat_col_submul(T, 0, v, 1 + i);
964
7.00k
  }
965
18.5k
  isl_int_clear(v);
966
18.5k
  pos = isl_alloc_array(bmap->ctx, int, T->n_row);
967
18.5k
  if (!pos)
968
0
    goto error;
969
18.5k
  /* We have to be careful because dropping equalities may reorder them */
970
18.5k
  dropped = 0;
971
48.4k
  for (j = bmap->n_div - 1; j >= 0; 
--j29.9k
) {
972
46.9k
    for (i = 0; i < bmap->n_eq; 
++i17.0k
)
973
39.5k
      if (!isl_int_is_zero(bmap->eq[i][1 + total + j]))
974
39.5k
        
break22.5k
;
975
29.9k
    if (i < bmap->n_eq) {
976
22.5k
      bmap = isl_basic_map_drop_div(bmap, j);
977
22.5k
      isl_basic_map_drop_equality(bmap, i);
978
22.5k
      ++dropped;
979
22.5k
    }
980
29.9k
  }
981
18.5k
  pos[0] = 0;
982
18.5k
  needed = 0;
983
96.6k
  for (i = 1; i < T->n_row; 
++i78.1k
) {
984
78.1k
    if (isl_int_is_one(T->row[i][i]))
985
78.1k
      
pos[i] = i58.7k
;
986
19.4k
    else
987
19.4k
      needed++;
988
78.1k
  }
989
18.5k
  if (needed > dropped) {
990
18
    bmap = isl_basic_map_extend_space(bmap, isl_space_copy(bmap->dim),
991
18
        needed, needed, 0);
992
18
    if (!bmap)
993
0
      goto error;
994
18.5k
  }
995
96.6k
  
for (i = 1; 18.5k
i < T->n_row;
++i78.1k
) {
996
78.1k
    if (isl_int_is_one(T->row[i][i]))
997
78.1k
      
continue58.7k
;
998
19.4k
    k = isl_basic_map_alloc_div(bmap);
999
19.4k
    pos[i] = 1 + total + k;
1000
19.4k
    isl_seq_clr(bmap->div[k] + 1, 1 + total + bmap->n_div);
1001
19.4k
    isl_int_set(bmap->div[k][0], T->row[i][i]);
1002
19.4k
    if (C2)
1003
11.9k
      isl_seq_cpy(bmap->div[k] + 1, C2->row[i], 1 + total);
1004
19.4k
    else
1005
19.4k
      
isl_int_set_si7.46k
(bmap->div[k][1 + i], 1);
1006
84.6k
    for (j = 0; j < i; 
++j65.1k
) {
1007
65.1k
      if (isl_int_is_zero(T->row[i][j]))
1008
65.1k
        
continue49.0k
;
1009
16.1k
      if (pos[j] < T->n_row && 
C216.0k
)
1010
9.79k
        isl_seq_submul(bmap->div[k] + 1, T->row[i][j],
1011
9.79k
            C2->row[pos[j]], 1 + total);
1012
16.1k
      else
1013
16.1k
        
isl_int_neg6.35k
(bmap->div[k][1 + pos[j]],
1014
16.1k
                T->row[i][j]);
1015
16.1k
    }
1016
19.4k
    j = isl_basic_map_alloc_equality(bmap);
1017
19.4k
    isl_seq_neg(bmap->eq[j], bmap->div[k]+1, 1+total+bmap->n_div);
1018
19.4k
    isl_int_set(bmap->eq[j][pos[i]], bmap->div[k][0]);
1019
19.4k
  }
1020
18.5k
  free(pos);
1021
18.5k
  isl_mat_free(C2);
1022
18.5k
  isl_mat_free(T);
1023
18.5k
1024
18.5k
  if (progress)
1025
18.5k
    *progress = 1;
1026
20.4k
done:
1027
20.4k
  ISL_F_SET(bmap, ISL_BASIC_MAP_NORMALIZED_DIVS);
1028
20.4k
1029
20.4k
  return bmap;
1030
0
error:
1031
0
  free(pos);
1032
0
  isl_mat_free(C);
1033
0
  isl_mat_free(C2);
1034
0
  isl_mat_free(T);
1035
0
  return bmap;
1036
18.5k
}
1037
1038
static __isl_give isl_basic_map *set_div_from_lower_bound(
1039
  __isl_take isl_basic_map *bmap, int div, int ineq)
1040
2.03k
{
1041
2.03k
  unsigned total = 1 + isl_space_dim(bmap->dim, isl_dim_all);
1042
2.03k
1043
2.03k
  isl_seq_neg(bmap->div[div] + 1, bmap->ineq[ineq], total + bmap->n_div);
1044
2.03k
  isl_int_set(bmap->div[div][0], bmap->ineq[ineq][total + div]);
1045
2.03k
  isl_int_add(bmap->div[div][1], bmap->div[div][1], bmap->div[div][0]);
1046
2.03k
  isl_int_sub_ui(bmap->div[div][1], bmap->div[div][1], 1);
1047
2.03k
  isl_int_set_si(bmap->div[div][1 + total + div], 0);
1048
2.03k
1049
2.03k
  return bmap;
1050
2.03k
}
1051
1052
/* Check whether it is ok to define a div based on an inequality.
1053
 * To avoid the introduction of circular definitions of divs, we
1054
 * do not allow such a definition if the resulting expression would refer to
1055
 * any other undefined divs or if any known div is defined in
1056
 * terms of the unknown div.
1057
 */
1058
static isl_bool ok_to_set_div_from_bound(__isl_keep isl_basic_map *bmap,
1059
  int div, int ineq)
1060
7.34k
{
1061
7.34k
  int j;
1062
7.34k
  unsigned total = 1 + isl_space_dim(bmap->dim, isl_dim_all);
1063
7.34k
1064
7.34k
  /* Not defined in terms of unknown divs */
1065
23.5k
  for (j = 0; j < bmap->n_div; 
++j16.2k
) {
1066
21.3k
    if (div == j)
1067
6.61k
      continue;
1068
14.7k
    if (isl_int_is_zero(bmap->ineq[ineq][total + j]))
1069
14.7k
      
continue9.49k
;
1070
5.26k
    if (isl_int_is_zero(bmap->div[j][0]))
1071
5.26k
      
return isl_bool_false5.14k
;
1072
5.26k
  }
1073
7.34k
1074
7.34k
  /* No other div defined in terms of this one => avoid loops */
1075
8.56k
  
for (j = 0; 2.19k
j < bmap->n_div;
++j6.37k
) {
1076
6.53k
    if (div == j)
1077
2.19k
      continue;
1078
4.34k
    if (isl_int_is_zero(bmap->div[j][0]))
1079
4.34k
      
continue1.35k
;
1080
2.98k
    if (!isl_int_is_zero(bmap->div[j][1 + total + div]))
1081
2.98k
      
return isl_bool_false165
;
1082
2.98k
  }
1083
2.19k
1084
2.19k
  
return isl_bool_true2.03k
;
1085
2.19k
}
1086
1087
/* Would an expression for div "div" based on inequality "ineq" of "bmap"
1088
 * be a better expression than the current one?
1089
 *
1090
 * If we do not have any expression yet, then any expression would be better.
1091
 * Otherwise we check if the last variable involved in the inequality
1092
 * (disregarding the div that it would define) is in an earlier position
1093
 * than the last variable involved in the current div expression.
1094
 */
1095
static isl_bool better_div_constraint(__isl_keep isl_basic_map *bmap,
1096
  int div, int ineq)
1097
103k
{
1098
103k
  unsigned total = 1 + isl_space_dim(bmap->dim, isl_dim_all);
1099
103k
  int last_div;
1100
103k
  int last_ineq;
1101
103k
1102
103k
  if (isl_int_is_zero(bmap->div[div][0]))
1103
103k
    
return isl_bool_true7.13k
;
1104
96.5k
1105
96.5k
  if (isl_seq_last_non_zero(bmap->ineq[ineq] + total + div + 1,
1106
96.5k
          bmap->n_div - (div + 1)) >= 0)
1107
973
    return isl_bool_false;
1108
95.5k
1109
95.5k
  last_ineq = isl_seq_last_non_zero(bmap->ineq[ineq], total + div);
1110
95.5k
  last_div = isl_seq_last_non_zero(bmap->div[div] + 1,
1111
95.5k
           total + bmap->n_div);
1112
95.5k
1113
95.5k
  return last_ineq < last_div;
1114
95.5k
}
1115
1116
/* Given two constraints "k" and "l" that are opposite to each other,
1117
 * except for the constant term, check if we can use them
1118
 * to obtain an expression for one of the hitherto unknown divs or
1119
 * a "better" expression for a div for which we already have an expression.
1120
 * "sum" is the sum of the constant terms of the constraints.
1121
 * If this sum is strictly smaller than the coefficient of one
1122
 * of the divs, then this pair can be used define the div.
1123
 * To avoid the introduction of circular definitions of divs, we
1124
 * do not use the pair if the resulting expression would refer to
1125
 * any other undefined divs or if any known div is defined in
1126
 * terms of the unknown div.
1127
 */
1128
static __isl_give isl_basic_map *check_for_div_constraints(
1129
  __isl_take isl_basic_map *bmap, int k, int l, isl_int sum,
1130
  int *progress)
1131
5.98M
{
1132
5.98M
  int i;
1133
5.98M
  unsigned total = 1 + isl_space_dim(bmap->dim, isl_dim_all);
1134
5.98M
1135
6.40M
  for (i = 0; i < bmap->n_div; 
++i421k
) {
1136
524k
    isl_bool set_div;
1137
524k
1138
524k
    if (isl_int_is_zero(bmap->ineq[k][total + i]))
1139
524k
      
continue399k
;
1140
125k
    if (isl_int_abs_ge(sum, bmap->ineq[k][total + i]))
1141
125k
      
continue21.6k
;
1142
103k
    set_div = better_div_constraint(bmap, i, k);
1143
103k
    if (set_div >= 0 && set_div)
1144
7.33k
      set_div = ok_to_set_div_from_bound(bmap, i, k);
1145
103k
    if (set_div < 0)
1146
0
      return isl_basic_map_free(bmap);
1147
103k
    if (!set_div)
1148
101k
      break;
1149
2.02k
    if (isl_int_is_pos(bmap->ineq[k][total + i]))
1150
2.02k
      
bmap = set_div_from_lower_bound(bmap, i, k)840
;
1151
1.18k
    else
1152
1.18k
      bmap = set_div_from_lower_bound(bmap, i, l);
1153
2.02k
    if (progress)
1154
2.02k
      *progress = 1;
1155
2.02k
    break;
1156
2.02k
  }
1157
5.98M
  return bmap;
1158
5.98M
}
1159
1160
__isl_give isl_basic_map *isl_basic_map_remove_duplicate_constraints(
1161
  __isl_take isl_basic_map *bmap, int *progress, int detect_divs)
1162
2.78M
{
1163
2.78M
  struct isl_constraint_index ci;
1164
2.78M
  int k, l, h;
1165
2.78M
  unsigned total = isl_basic_map_total_dim(bmap);
1166
2.78M
  isl_int sum;
1167
2.78M
1168
2.78M
  if (!bmap || bmap->n_ineq <= 1)
1169
901k
    return bmap;
1170
1.87M
1171
1.87M
  if (create_constraint_index(&ci, bmap) < 0)
1172
0
    return bmap;
1173
1.87M
1174
1.87M
  h = isl_seq_get_hash_bits(bmap->ineq[0] + 1, total, ci.bits);
1175
1.87M
  ci.index[h] = &bmap->ineq[0];
1176
11.3M
  for (k = 1; k < bmap->n_ineq; 
++k9.44M
) {
1177
9.44M
    h = hash_index(&ci, bmap, k);
1178
9.44M
    if (!ci.index[h]) {
1179
8.78M
      ci.index[h] = &bmap->ineq[k];
1180
8.78M
      continue;
1181
8.78M
    }
1182
658k
    if (progress)
1183
648k
      *progress = 1;
1184
658k
    l = ci.index[h] - &bmap->ineq[0];
1185
658k
    if (isl_int_lt(bmap->ineq[k][0], bmap->ineq[l][0]))
1186
658k
      
swap_inequality(bmap, k, l)50.2k
;
1187
658k
    isl_basic_map_drop_inequality(bmap, k);
1188
658k
    --k;
1189
658k
  }
1190
1.87M
  isl_int_init(sum);
1191
10.1M
  for (k = 0; k < bmap->n_ineq-1; 
++k8.26M
) {
1192
8.37M
    isl_seq_neg(bmap->ineq[k]+1, bmap->ineq[k]+1, total);
1193
8.37M
    h = hash_index(&ci, bmap, k);
1194
8.37M
    isl_seq_neg(bmap->ineq[k]+1, bmap->ineq[k]+1, total);
1195
8.37M
    if (!ci.index[h])
1196
2.23M
      continue;
1197
6.13M
    l = ci.index[h] - &bmap->ineq[0];
1198
6.13M
    isl_int_add(sum, bmap->ineq[k][0], bmap->ineq[l][0]);
1199
6.13M
    if (isl_int_is_pos(sum)) {
1200
6.02M
      if (detect_divs)
1201
5.98M
        bmap = check_for_div_constraints(bmap, k, l,
1202
5.98M
                 sum, progress);
1203
6.02M
      continue;
1204
6.02M
    }
1205
105k
    if (isl_int_is_zero(sum)) {
1206
17.8k
      /* We need to break out of the loop after these
1207
17.8k
       * changes since the contents of the hash
1208
17.8k
       * will no longer be valid.
1209
17.8k
       * Plus, we probably we want to regauss first.
1210
17.8k
       */
1211
17.8k
      if (progress)
1212
17.5k
        *progress = 1;
1213
17.8k
      isl_basic_map_drop_inequality(bmap, l);
1214
17.8k
      isl_basic_map_inequality_to_equality(bmap, k);
1215
17.8k
    } else
1216
88.0k
      bmap = isl_basic_map_set_to_empty(bmap);
1217
105k
    break;
1218
105k
  }
1219
1.87M
  isl_int_clear(sum);
1220
1.87M
1221
1.87M
  constraint_index_free(&ci);
1222
1.87M
  return bmap;
1223
1.87M
}
1224
1225
/* Detect all pairs of inequalities that form an equality.
1226
 *
1227
 * isl_basic_map_remove_duplicate_constraints detects at most one such pair.
1228
 * Call it repeatedly while it is making progress.
1229
 */
1230
__isl_give isl_basic_map *isl_basic_map_detect_inequality_pairs(
1231
  __isl_take isl_basic_map *bmap, int *progress)
1232
525
{
1233
525
  int duplicate;
1234
525
1235
952
  do {
1236
952
    duplicate = 0;
1237
952
    bmap = isl_basic_map_remove_duplicate_constraints(bmap,
1238
952
                &duplicate, 0);
1239
952
    if (progress && 
duplicate287
)
1240
75
      *progress = 1;
1241
952
  } while (duplicate);
1242
525
1243
525
  return bmap;
1244
525
}
1245
1246
/* Eliminate knowns divs from constraints where they appear with
1247
 * a (positive or negative) unit coefficient.
1248
 *
1249
 * That is, replace
1250
 *
1251
 *  floor(e/m) + f >= 0
1252
 *
1253
 * by
1254
 *
1255
 *  e + m f >= 0
1256
 *
1257
 * and
1258
 *
1259
 *  -floor(e/m) + f >= 0
1260
 *
1261
 * by
1262
 *
1263
 *  -e + m f + m - 1 >= 0
1264
 *
1265
 * The first conversion is valid because floor(e/m) >= -f is equivalent
1266
 * to e/m >= -f because -f is an integral expression.
1267
 * The second conversion follows from the fact that
1268
 *
1269
 *  -floor(e/m) = ceil(-e/m) = floor((-e + m - 1)/m)
1270
 *
1271
 *
1272
 * Note that one of the div constraints may have been eliminated
1273
 * due to being redundant with respect to the constraint that is
1274
 * being modified by this function.  The modified constraint may
1275
 * no longer imply this div constraint, so we add it back to make
1276
 * sure we do not lose any information.
1277
 *
1278
 * We skip integral divs, i.e., those with denominator 1, as we would
1279
 * risk eliminating the div from the div constraints.  We do not need
1280
 * to handle those divs here anyway since the div constraints will turn
1281
 * out to form an equality and this equality can then be used to eliminate
1282
 * the div from all constraints.
1283
 */
1284
static __isl_give isl_basic_map *eliminate_unit_divs(
1285
  __isl_take isl_basic_map *bmap, int *progress)
1286
2.74M
{
1287
2.74M
  int i, j;
1288
2.74M
  isl_ctx *ctx;
1289
2.74M
  unsigned total;
1290
2.74M
1291
2.74M
  if (!bmap)
1292
0
    return NULL;
1293
2.74M
1294
2.74M
  ctx = isl_basic_map_get_ctx(bmap);
1295
2.74M
  total = 1 + isl_space_dim(bmap->dim, isl_dim_all);
1296
2.74M
1297
3.31M
  for (i = 0; i < bmap->n_div; 
++i563k
) {
1298
563k
    if (isl_int_is_zero(bmap->div[i][0]))
1299
563k
      
continue422k
;
1300
141k
    if (isl_int_is_one(bmap->div[i][0]))
1301
141k
      
continue668
;
1302
1.45M
    
for (j = 0; 140k
j < bmap->n_ineq;
++j1.31M
) {
1303
1.31M
      int s;
1304
1.31M
1305
1.31M
      if (!isl_int_is_one(bmap->ineq[j][total + i]) &&
1306
1.31M
          
!1.31M
isl_int_is_negone1.31M
(bmap->ineq[j][total + i]))
1307
1.31M
        
continue1.30M
;
1308
8.71k
1309
8.71k
      *progress = 1;
1310
8.71k
1311
8.71k
      s = isl_int_sgn(bmap->ineq[j][total + i]);
1312
8.71k
      isl_int_set_si(bmap->ineq[j][total + i], 0);
1313
8.71k
      if (s < 0)
1314
4.11k
        isl_seq_combine(bmap->ineq[j],
1315
4.11k
          ctx->negone, bmap->div[i] + 1,
1316
4.11k
          bmap->div[i][0], bmap->ineq[j],
1317
4.11k
          total + bmap->n_div);
1318
4.60k
      else
1319
4.60k
        isl_seq_combine(bmap->ineq[j],
1320
4.60k
          ctx->one, bmap->div[i] + 1,
1321
4.60k
          bmap->div[i][0], bmap->ineq[j],
1322
4.60k
          total + bmap->n_div);
1323
8.71k
      if (s < 0) {
1324
4.11k
        isl_int_add(bmap->ineq[j][0],
1325
4.11k
          bmap->ineq[j][0], bmap->div[i][0]);
1326
4.11k
        isl_int_sub_ui(bmap->ineq[j][0],
1327
4.11k
          bmap->ineq[j][0], 1);
1328
4.11k
      }
1329
8.71k
1330
8.71k
      bmap = isl_basic_map_extend_constraints(bmap, 0, 1);
1331
8.71k
      if (isl_basic_map_add_div_constraint(bmap, i, s) < 0)
1332
0
        return isl_basic_map_free(bmap);
1333
8.71k
    }
1334
140k
  }
1335
2.74M
1336
2.74M
  return bmap;
1337
2.74M
}
1338
1339
__isl_give isl_basic_map *isl_basic_map_simplify(__isl_take isl_basic_map *bmap)
1340
2.33M
{
1341
2.33M
  int progress = 1;
1342
2.33M
  if (!bmap)
1343
1
    return NULL;
1344
5.07M
  
while (2.33M
progress) {
1345
2.82M
    isl_bool empty;
1346
2.82M
1347
2.82M
    progress = 0;
1348
2.82M
    empty = isl_basic_map_plain_is_empty(bmap);
1349
2.82M
    if (empty < 0)
1350
0
      return isl_basic_map_free(bmap);
1351
2.82M
    if (empty)
1352
78.5k
      break;
1353
2.74M
    bmap = isl_basic_map_normalize_constraints(bmap);
1354
2.74M
    bmap = reduce_div_coefficients(bmap);
1355
2.74M
    bmap = normalize_div_expressions(bmap);
1356
2.74M
    bmap = remove_duplicate_divs(bmap, &progress);
1357
2.74M
    bmap = eliminate_unit_divs(bmap, &progress);
1358
2.74M
    bmap = eliminate_divs_eq(bmap, &progress);
1359
2.74M
    bmap = eliminate_divs_ineq(bmap, &progress);
1360
2.74M
    bmap = isl_basic_map_gauss(bmap, &progress);
1361
2.74M
    /* requires equalities in normal form */
1362
2.74M
    bmap = normalize_divs(bmap, &progress);
1363
2.74M
    bmap = isl_basic_map_remove_duplicate_constraints(bmap,
1364
2.74M
                &progress, 1);
1365
2.74M
    if (bmap && progress)
1366
2.74M
      ISL_F_CLR(bmap, ISL_BASIC_MAP_REDUCED_COEFFICIENTS);
1367
2.74M
  }
1368
2.33M
  return bmap;
1369
2.33M
}
1370
1371
struct isl_basic_set *isl_basic_set_simplify(struct isl_basic_set *bset)
1372
836k
{
1373
836k
  return bset_from_bmap(isl_basic_map_simplify(bset_to_bmap(bset)));
1374
836k
}
1375
1376
1377
isl_bool isl_basic_map_is_div_constraint(__isl_keep isl_basic_map *bmap,
1378
  isl_int *constraint, unsigned div)
1379
77.2k
{
1380
77.2k
  unsigned pos;
1381
77.2k
1382
77.2k
  if (!bmap)
1383
0
    return isl_bool_error;
1384
77.2k
1385
77.2k
  pos = 1 + isl_space_dim(bmap->dim, isl_dim_all) + div;
1386
77.2k
1387
77.2k
  if (isl_int_eq(constraint[pos], bmap->div[div][0])) {
1388
37.5k
    int neg;
1389
37.5k
    isl_int_sub(bmap->div[div][1],
1390
37.5k
        bmap->div[div][1], bmap->div[div][0]);
1391
37.5k
    isl_int_add_ui(bmap->div[div][1], bmap->div[div][1], 1);
1392
37.5k
    neg = isl_seq_is_neg(constraint, bmap->div[div]+1, pos);
1393
37.5k
    isl_int_sub_ui(bmap->div[div][1], bmap->div[div][1], 1);
1394
37.5k
    isl_int_add(bmap->div[div][1],
1395
37.5k
        bmap->div[div][1], bmap->div[div][0]);
1396
37.5k
    if (!neg)
1397
12.5k
      return isl_bool_false;
1398
25.0k
    if (isl_seq_first_non_zero(constraint+pos+1,
1399
25.0k
              bmap->n_div-div-1) != -1)
1400
0
      return isl_bool_false;
1401
39.6k
  } else if (isl_int_abs_eq(constraint[pos], bmap->div[div][0])) {
1402
33.5k
    if (!isl_seq_eq(constraint, bmap->div[div]+1, pos))
1403
17.5k
      return isl_bool_false;
1404
16.0k
    if (isl_seq_first_non_zero(constraint+pos+1,
1405
16.0k
              bmap->n_div-div-1) != -1)
1406
1
      return isl_bool_false;
1407
6.12k
  } else
1408
6.12k
    return isl_bool_false;
1409
41.0k
1410
41.0k
  return isl_bool_true;
1411
41.0k
}
1412
1413
isl_bool isl_basic_set_is_div_constraint(__isl_keep isl_basic_set *bset,
1414
  isl_int *constraint, unsigned div)
1415
0
{
1416
0
  return isl_basic_map_is_div_constraint(bset, constraint, div);
1417
0
}
1418
1419
1420
/* If the only constraints a div d=floor(f/m)
1421
 * appears in are its two defining constraints
1422
 *
1423
 *  f - m d >=0
1424
 *  -(f - (m - 1)) + m d >= 0
1425
 *
1426
 * then it can safely be removed.
1427
 */
1428
static isl_bool div_is_redundant(__isl_keep isl_basic_map *bmap, int div)
1429
123k
{
1430
123k
  int i;
1431
123k
  unsigned pos = 1 + isl_space_dim(bmap->dim, isl_dim_all) + div;
1432
123k
1433
172k
  for (i = 0; i < bmap->n_eq; 
++i49.0k
)
1434
104k
    if (!isl_int_is_zero(bmap->eq[i][pos]))
1435
104k
      
return isl_bool_false55.7k
;
1436
123k
1437
352k
  
for (i = 0; 67.2k
i < bmap->n_ineq;
++i285k
) {
1438
321k
    isl_bool red;
1439
321k
1440
321k
    if (isl_int_is_zero(bmap->ineq[i][pos]))
1441
321k
      
continue244k
;
1442
76.8k
    red = isl_basic_map_is_div_constraint(bmap, bmap->ineq[i], div);
1443
76.8k
    if (red < 0 || !red)
1444
35.9k
      return red;
1445
76.8k
  }
1446
67.2k
1447
68.4k
  
for (i = 0; 31.3k
i < bmap->n_div;
++i37.1k
) {
1448
37.1k
    if (isl_int_is_zero(bmap->div[i][0]))
1449
37.1k
      
continue613
;
1450
36.5k
    if (!isl_int_is_zero(bmap->div[i][1+pos]))
1451
36.5k
      
return isl_bool_false1
;
1452
36.5k
  }
1453
31.3k
1454
31.3k
  
return isl_bool_true31.3k
;
1455
31.3k
}
1456
1457
/*
1458
 * Remove divs that don't occur in any of the constraints or other divs.
1459
 * These can arise when dropping constraints from a basic map or
1460
 * when the divs of a basic map have been temporarily aligned
1461
 * with the divs of another basic map.
1462
 */
1463
static __isl_give isl_basic_map *remove_redundant_divs(
1464
  __isl_take isl_basic_map *bmap)
1465
5.09M
{
1466
5.09M
  int i;
1467
5.09M
1468
5.09M
  if (!bmap)
1469
1
    return NULL;
1470
5.09M
1471
5.21M
  
for (i = bmap->n_div-1; 5.09M
i >= 0;
--i123k
) {
1472
123k
    isl_bool redundant;
1473
123k
1474
123k
    redundant = div_is_redundant(bmap, i);
1475
123k
    if (redundant < 0)
1476
0
      return isl_basic_map_free(bmap);
1477
123k
    if (!redundant)
1478
91.6k
      continue;
1479
31.3k
    bmap = isl_basic_map_drop_div(bmap, i);
1480
31.3k
  }
1481
5.09M
  return bmap;
1482
5.09M
}
1483
1484
/* Mark "bmap" as final, without checking for obviously redundant
1485
 * integer divisions.  This function should be used when "bmap"
1486
 * is known not to involve any such integer divisions.
1487
 */
1488
__isl_give isl_basic_map *isl_basic_map_mark_final(
1489
  __isl_take isl_basic_map *bmap)
1490
5.09M
{
1491
5.09M
  if (!bmap)
1492
1
    return NULL;
1493
5.09M
  ISL_F_SET(bmap, ISL_BASIC_SET_FINAL);
1494
5.09M
  return bmap;
1495
5.09M
}
1496
1497
/* Mark "bmap" as final, after removing obviously redundant integer divisions.
1498
 */
1499
__isl_give isl_basic_map *isl_basic_map_finalize(__isl_take isl_basic_map *bmap)
1500
5.09M
{
1501
5.09M
  bmap = remove_redundant_divs(bmap);
1502
5.09M
  bmap = isl_basic_map_mark_final(bmap);
1503
5.09M
  return bmap;
1504
5.09M
}
1505
1506
struct isl_basic_set *isl_basic_set_finalize(struct isl_basic_set *bset)
1507
980k
{
1508
980k
  return bset_from_bmap(isl_basic_map_finalize(bset_to_bmap(bset)));
1509
980k
}
1510
1511
/* Remove definition of any div that is defined in terms of the given variable.
1512
 * The div itself is not removed.  Functions such as
1513
 * eliminate_divs_ineq depend on the other divs remaining in place.
1514
 */
1515
static __isl_give isl_basic_map *remove_dependent_vars(
1516
  __isl_take isl_basic_map *bmap, int pos)
1517
110k
{
1518
110k
  int i;
1519
110k
1520
110k
  if (!bmap)
1521
0
    return NULL;
1522
110k
1523
234k
  
for (i = 0; 110k
i < bmap->n_div;
++i123k
) {
1524
123k
    if (isl_int_is_zero(bmap->div[i][0]))
1525
123k
      
continue119k
;
1526
4.04k
    if (isl_int_is_zero(bmap->div[i][1+1+pos]))
1527
4.04k
      
continue3.97k
;
1528
78
    bmap = isl_basic_map_mark_div_unknown(bmap, i);
1529
78
    if (!bmap)
1530
0
      return NULL;
1531
78
  }
1532
110k
  return bmap;
1533
110k
}
1534
1535
/* Eliminate the specified variables from the constraints using
1536
 * Fourier-Motzkin.  The variables themselves are not removed.
1537
 */
1538
__isl_give isl_basic_map *isl_basic_map_eliminate_vars(
1539
  __isl_take isl_basic_map *bmap, unsigned pos, unsigned n)
1540
111k
{
1541
111k
  int d;
1542
111k
  int i, j, k;
1543
111k
  unsigned total;
1544
111k
  int need_gauss = 0;
1545
111k
1546
111k
  if (n == 0)
1547
2.35k
    return bmap;
1548
108k
  if (!bmap)
1549
0
    return NULL;
1550
108k
  total = isl_basic_map_total_dim(bmap);
1551
108k
1552
108k
  bmap = isl_basic_map_cow(bmap);
1553
219k
  for (d = pos + n - 1; d >= 0 && 
d >= pos200k
;
--d110k
)
1554
110k
    bmap = remove_dependent_vars(bmap, d);
1555
108k
  if (!bmap)
1556
0
    return NULL;
1557
108k
1558
108k
  for (d = pos + n - 1;
1559
190k
       d >= 0 && 
d >= total - bmap->n_div177k
&&
d >= pos103k
;
--d81.9k
)
1560
81.9k
    isl_seq_clr(bmap->div[d-(total-bmap->n_div)], 2+total);
1561
219k
  for (d = pos + n - 1; d >= 0 && 
d >= pos200k
;
--d110k
) {
1562
110k
    int n_lower, n_upper;
1563
110k
    if (!bmap)
1564
0
      return NULL;
1565
149k
    
for (i = 0; 110k
i < bmap->n_eq;
++i38.3k
) {
1566
41.7k
      if (isl_int_is_zero(bmap->eq[i][1+d]))
1567
41.7k
        
continue38.3k
;
1568
3.42k
      eliminate_var_using_equality(bmap, d, bmap->eq[i], 0, NULL);
1569
3.42k
      isl_basic_map_drop_equality(bmap, i);
1570
3.42k
      need_gauss = 1;
1571
3.42k
      break;
1572
3.42k
    }
1573
110k
    if (i < bmap->n_eq)
1574
1.27k
      continue;
1575
109k
    n_lower = 0;
1576
109k
    n_upper = 0;
1577
374k
    for (i = 0; i < bmap->n_ineq; 
++i265k
) {
1578
265k
      if (isl_int_is_pos(bmap->ineq[i][1+d]))
1579
265k
        
n_lower++34.9k
;
1580
230k
      else if (isl_int_is_neg(bmap->ineq[i][1+d]))
1581
230k
        
n_upper++33.8k
;
1582
265k
    }
1583
109k
    bmap = isl_basic_map_extend_constraints(bmap,
1584
109k
        0, n_lower * n_upper);
1585
109k
    if (!bmap)
1586
0
      goto error;
1587
314k
    
for (i = bmap->n_ineq - 1; 109k
i >= 0;
--i204k
) {
1588
204k
      int last;
1589
204k
      if (isl_int_is_zero(bmap->ineq[i][1+d]))
1590
204k
        
continue136k
;
1591
68.8k
      last = -1;
1592
285k
      for (j = 0; j < i; 
++j216k
) {
1593
216k
        if (isl_int_is_zero(bmap->ineq[j][1+d]))
1594
216k
          
continue156k
;
1595
60.5k
        last = j;
1596
60.5k
        if (isl_int_sgn(bmap->ineq[i][1+d]) ==
1597
60.5k
            isl_int_sgn(bmap->ineq[j][1+d]))
1598
60.5k
          
continue14.5k
;
1599
45.9k
        k = isl_basic_map_alloc_inequality(bmap);
1600
45.9k
        if (k < 0)
1601
0
          goto error;
1602
45.9k
        isl_seq_cpy(bmap->ineq[k], bmap->ineq[i],
1603
45.9k
            1+total);
1604
45.9k
        isl_seq_elim(bmap->ineq[k], bmap->ineq[j],
1605
45.9k
            1+d, 1+total, NULL);
1606
45.9k
      }
1607
68.8k
      isl_basic_map_drop_inequality(bmap, i);
1608
68.8k
      i = last + 1;
1609
68.8k
    }
1610
109k
    if (n_lower > 0 && 
n_upper > 029.4k
) {
1611
28.2k
      bmap = isl_basic_map_normalize_constraints(bmap);
1612
28.2k
      bmap = isl_basic_map_remove_duplicate_constraints(bmap,
1613
28.2k
                    NULL, 0);
1614
28.2k
      bmap = isl_basic_map_gauss(bmap, NULL);
1615
28.2k
      bmap = isl_basic_map_remove_redundancies(bmap);
1616
28.2k
      need_gauss = 0;
1617
28.2k
      if (!bmap)
1618
0
        goto error;
1619
28.2k
      if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
1620
28.2k
        
break179
;
1621
28.2k
    }
1622
109k
  }
1623
108k
  ISL_F_CLR(bmap, ISL_BASIC_MAP_NORMALIZED);
1624
108k
  if (need_gauss)
1625
1.67k
    bmap = isl_basic_map_gauss(bmap, NULL);
1626
108k
  return bmap;
1627
0
error:
1628
0
  isl_basic_map_free(bmap);
1629
0
  return NULL;
1630
108k
}
1631
1632
struct isl_basic_set *isl_basic_set_eliminate_vars(
1633
  struct isl_basic_set *bset, unsigned pos, unsigned n)
1634
26.0k
{
1635
26.0k
  return bset_from_bmap(isl_basic_map_eliminate_vars(bset_to_bmap(bset),
1636
26.0k
                pos, n));
1637
26.0k
}
1638
1639
/* Eliminate the specified n dimensions starting at first from the
1640
 * constraints, without removing the dimensions from the space.
1641
 * If the set is rational, the dimensions are eliminated using Fourier-Motzkin.
1642
 * Otherwise, they are projected out and the original space is restored.
1643
 */
1644
__isl_give isl_basic_map *isl_basic_map_eliminate(
1645
  __isl_take isl_basic_map *bmap,
1646
  enum isl_dim_type type, unsigned first, unsigned n)
1647
17.2k
{
1648
17.2k
  isl_space *space;
1649
17.2k
1650
17.2k
  if (!bmap)
1651
0
    return NULL;
1652
17.2k
  if (n == 0)
1653
0
    return bmap;
1654
17.2k
1655
17.2k
  if (first + n > isl_basic_map_dim(bmap, type) || first + n < first)
1656
17.2k
    
isl_die0
(bmap->ctx, isl_error_invalid,
1657
17.2k
      "index out of bounds", goto error);
1658
17.2k
1659
17.2k
  if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL)) {
1660
0
    first += isl_basic_map_offset(bmap, type) - 1;
1661
0
    bmap = isl_basic_map_eliminate_vars(bmap, first, n);
1662
0
    return isl_basic_map_finalize(bmap);
1663
0
  }
1664
17.2k
1665
17.2k
  space = isl_basic_map_get_space(bmap);
1666
17.2k
  bmap = isl_basic_map_project_out(bmap, type, first, n);
1667
17.2k
  bmap = isl_basic_map_insert_dims(bmap, type, first, n);
1668
17.2k
  bmap = isl_basic_map_reset_space(bmap, space);
1669
17.2k
  return bmap;
1670
0
error:
1671
0
  isl_basic_map_free(bmap);
1672
0
  return NULL;
1673
17.2k
}
1674
1675
__isl_give isl_basic_set *isl_basic_set_eliminate(
1676
  __isl_take isl_basic_set *bset,
1677
  enum isl_dim_type type, unsigned first, unsigned n)
1678
5.76k
{
1679
5.76k
  return isl_basic_map_eliminate(bset, type, first, n);
1680
5.76k
}
1681
1682
/* Remove all constraints from "bmap" that reference any unknown local
1683
 * variables (directly or indirectly).
1684
 *
1685
 * Dropping all constraints on a local variable will make it redundant,
1686
 * so it will get removed implicitly by
1687
 * isl_basic_map_drop_constraints_involving_dims.  Some other local
1688
 * variables may also end up becoming redundant if they only appear
1689
 * in constraints together with the unknown local variable.
1690
 * Therefore, start over after calling
1691
 * isl_basic_map_drop_constraints_involving_dims.
1692
 */
1693
__isl_give isl_basic_map *isl_basic_map_drop_constraint_involving_unknown_divs(
1694
  __isl_take isl_basic_map *bmap)
1695
7.92k
{
1696
7.92k
  isl_bool known;
1697
7.92k
  int i, n_div, o_div;
1698
7.92k
1699
7.92k
  known = isl_basic_map_divs_known(bmap);
1700
7.92k
  if (known < 0)
1701
0
    return isl_basic_map_free(bmap);
1702
7.92k
  if (known)
1703
7.92k
    return bmap;
1704
0
1705
0
  n_div = isl_basic_map_dim(bmap, isl_dim_div);
1706
0
  o_div = isl_basic_map_offset(bmap, isl_dim_div) - 1;
1707
0
1708
0
  for (i = 0; i < n_div; ++i) {
1709
0
    known = isl_basic_map_div_is_known(bmap, i);
1710
0
    if (known < 0)
1711
0
      return isl_basic_map_free(bmap);
1712
0
    if (known)
1713
0
      continue;
1714
0
    bmap = remove_dependent_vars(bmap, o_div + i);
1715
0
    bmap = isl_basic_map_drop_constraints_involving_dims(bmap,
1716
0
                  isl_dim_div, i, 1);
1717
0
    if (!bmap)
1718
0
      return NULL;
1719
0
    n_div = isl_basic_map_dim(bmap, isl_dim_div);
1720
0
    i = -1;
1721
0
  }
1722
0
1723
0
  return bmap;
1724
0
}
1725
1726
/* Remove all constraints from "map" that reference any unknown local
1727
 * variables (directly or indirectly).
1728
 *
1729
 * Since constraints may get dropped from the basic maps,
1730
 * they may no longer be disjoint from each other.
1731
 */
1732
__isl_give isl_map *isl_map_drop_constraint_involving_unknown_divs(
1733
  __isl_take isl_map *map)
1734
508
{
1735
508
  int i;
1736
508
  isl_bool known;
1737
508
1738
508
  known = isl_map_divs_known(map);
1739
508
  if (known < 0)
1740
0
    return isl_map_free(map);
1741
508
  if (known)
1742
508
    return map;
1743
0
1744
0
  map = isl_map_cow(map);
1745
0
  if (!map)
1746
0
    return NULL;
1747
0
1748
0
  for (i = 0; i < map->n; ++i) {
1749
0
    map->p[i] =
1750
0
        isl_basic_map_drop_constraint_involving_unknown_divs(
1751
0
                    map->p[i]);
1752
0
    if (!map->p[i])
1753
0
      return isl_map_free(map);
1754
0
  }
1755
0
1756
0
  if (map->n > 1)
1757
0
    ISL_F_CLR(map, ISL_MAP_DISJOINT);
1758
0
1759
0
  return map;
1760
0
}
1761
1762
/* Don't assume equalities are in order, because align_divs
1763
 * may have changed the order of the divs.
1764
 */
1765
static void compute_elimination_index(__isl_keep isl_basic_map *bmap, int *elim)
1766
31.4k
{
1767
31.4k
  int d, i;
1768
31.4k
  unsigned total;
1769
31.4k
1770
31.4k
  total = isl_space_dim(bmap->dim, isl_dim_all);
1771
266k
  for (d = 0; d < total; 
++d235k
)
1772
235k
    elim[d] = -1;
1773
72.8k
  for (i = 0; i < bmap->n_eq; 
++i41.4k
) {
1774
159k
    for (d = total - 1; d >= 0; 
--d117k
) {
1775
159k
      if (isl_int_is_zero(bmap->eq[i][1+d]))
1776
159k
        
continue117k
;
1777
41.4k
      elim[d] = i;
1778
41.4k
      break;
1779
41.4k
    }
1780
41.4k
  }
1781
31.4k
}
1782
1783
static void set_compute_elimination_index(__isl_keep isl_basic_set *bset,
1784
  int *elim)
1785
493
{
1786
493
  compute_elimination_index(bset_to_bmap(bset), elim);
1787
493
}
1788
1789
static int reduced_using_equalities(isl_int *dst, isl_int *src,
1790
  __isl_keep isl_basic_map *bmap, int *elim)
1791
233k
{
1792
233k
  int d;
1793
233k
  int copied = 0;
1794
233k
  unsigned total;
1795
233k
1796
233k
  total = isl_space_dim(bmap->dim, isl_dim_all);
1797
2.20M
  for (d = total - 1; d >= 0; 
--d1.96M
) {
1798
1.96M
    if (isl_int_is_zero(src[1+d]))
1799
1.96M
      
continue1.69M
;
1800
268k
    if (elim[d] == -1)
1801
242k
      continue;
1802
26.8k
    if (!copied) {
1803
26.1k
      isl_seq_cpy(dst, src, 1 + total);
1804
26.1k
      copied = 1;
1805
26.1k
    }
1806
26.8k
    isl_seq_elim(dst, bmap->eq[elim[d]], 1 + d, 1 + total, NULL);
1807
26.8k
  }
1808
233k
  return copied;
1809
233k
}
1810
1811
static int set_reduced_using_equalities(isl_int *dst, isl_int *src,
1812
  __isl_keep isl_basic_set *bset, int *elim)
1813
1.01k
{
1814
1.01k
  return reduced_using_equalities(dst, src,
1815
1.01k
          bset_to_bmap(bset), elim);
1816
1.01k
}
1817
1818
static __isl_give isl_basic_set *isl_basic_set_reduce_using_equalities(
1819
  __isl_take isl_basic_set *bset, __isl_take isl_basic_set *context)
1820
9.88k
{
1821
9.88k
  int i;
1822
9.88k
  int *elim;
1823
9.88k
1824
9.88k
  if (!bset || !context)
1825
0
    goto error;
1826
9.88k
1827
9.88k
  if (context->n_eq == 0) {
1828
9.38k
    isl_basic_set_free(context);
1829
9.38k
    return bset;
1830
9.38k
  }
1831
493
1832
493
  bset = isl_basic_set_cow(bset);
1833
493
  if (!bset)
1834
0
    goto error;
1835
493
1836
493
  elim = isl_alloc_array(bset->ctx, int, isl_basic_set_n_dim(bset));
1837
493
  if (!elim)
1838
0
    goto error;
1839
493
  set_compute_elimination_index(context, elim);
1840
1.25k
  for (i = 0; i < bset->n_eq; 
++i759
)
1841
759
    set_reduced_using_equalities(bset->eq[i], bset->eq[i],
1842
759
              context, elim);
1843
747
  for (i = 0; i < bset->n_ineq; 
++i254
)
1844
254
    set_reduced_using_equalities(bset->ineq[i], bset->ineq[i],
1845
254
              context, elim);
1846
493
  isl_basic_set_free(context);
1847
493
  free(elim);
1848
493
  bset = isl_basic_set_simplify(bset);
1849
493
  bset = isl_basic_set_finalize(bset);
1850
493
  return bset;
1851
0
error:
1852
0
  isl_basic_set_free(bset);
1853
0
  isl_basic_set_free(context);
1854
0
  return NULL;
1855
493
}
1856
1857
/* For each inequality in "ineq" that is a shifted (more relaxed)
1858
 * copy of an inequality in "context", mark the corresponding entry
1859
 * in "row" with -1.
1860
 * If an inequality only has a non-negative constant term, then
1861
 * mark it as well.
1862
 */
1863
static isl_stat mark_shifted_constraints(__isl_keep isl_mat *ineq,
1864
  __isl_keep isl_basic_set *context, int *row)
1865
13.4k
{
1866
13.4k
  struct isl_constraint_index ci;
1867
13.4k
  int n_ineq;
1868
13.4k
  unsigned total;
1869
13.4k
  int k;
1870
13.4k
1871
13.4k
  if (!ineq || !context)
1872
0
    return isl_stat_error;
1873
13.4k
  if (context->n_ineq == 0)
1874
0
    return isl_stat_ok;
1875
13.4k
  if (setup_constraint_index(&ci, context) < 0)
1876
0
    return isl_stat_error;
1877
13.4k
1878
13.4k
  n_ineq = isl_mat_rows(ineq);
1879
13.4k
  total = isl_mat_cols(ineq) - 1;
1880
55.2k
  for (k = 0; k < n_ineq; 
++k41.8k
) {
1881
41.8k
    int l;
1882
41.8k
    isl_bool redundant;
1883
41.8k
1884
41.8k
    l = isl_seq_first_non_zero(ineq->row[k] + 1, total);
1885
41.8k
    if (l < 0 && 
isl_int_is_nonneg4
(ineq->row[k][0])) {
1886
0
      row[k] = -1;
1887
0
      continue;
1888
0
    }
1889
41.8k
    redundant = constraint_index_is_redundant(&ci, ineq->row[k]);
1890
41.8k
    if (redundant < 0)
1891
0
      goto error;
1892
41.8k
    if (!redundant)
1893
22.5k
      continue;
1894
19.3k
    row[k] = -1;
1895
19.3k
  }
1896
13.4k
  constraint_index_free(&ci);
1897
13.4k
  return isl_stat_ok;
1898
0
error:
1899
0
  constraint_index_free(&ci);
1900
0
  return isl_stat_error;
1901
13.4k
}
1902
1903
static __isl_give isl_basic_set *remove_shifted_constraints(
1904
  __isl_take isl_basic_set *bset, __isl_keep isl_basic_set *context)
1905
40
{
1906
40
  struct isl_constraint_index ci;
1907
40
  int k;
1908
40
1909
40
  if (!bset || !context)
1910
0
    return bset;
1911
40
1912
40
  if (context->n_ineq == 0)
1913
0
    return bset;
1914
40
  if (setup_constraint_index(&ci, context) < 0)
1915
0
    return bset;
1916
40
1917
232
  
for (k = 0; 40
k < bset->n_ineq;
++k192
) {
1918
192
    isl_bool redundant;
1919
192
1920
192
    redundant = constraint_index_is_redundant(&ci, bset->ineq[k]);
1921
192
    if (redundant < 0)
1922
0
      goto error;
1923
192
    if (!redundant)
1924
71
      continue;
1925
121
    bset = isl_basic_set_cow(bset);
1926
121
    if (!bset)
1927
0
      goto error;
1928
121
    isl_basic_set_drop_inequality(bset, k);
1929
121
    --k;
1930
121
  }
1931
40
  constraint_index_free(&ci);
1932
40
  return bset;
1933
0
error:
1934
0
  constraint_index_free(&ci);
1935
0
  return bset;
1936
40
}
1937
1938
/* Remove constraints from "bmap" that are identical to constraints
1939
 * in "context" or that are more relaxed (greater constant term).
1940
 *
1941
 * We perform the test for shifted copies on the pure constraints
1942
 * in remove_shifted_constraints.
1943
 */
1944
static __isl_give isl_basic_map *isl_basic_map_remove_shifted_constraints(
1945
  __isl_take isl_basic_map *bmap, __isl_take isl_basic_map *context)
1946
549
{
1947
549
  isl_basic_set *bset, *bset_context;
1948
549
1949
549
  if (!bmap || !context)
1950
0
    goto error;
1951
549
1952
549
  if (bmap->n_ineq == 0 || 
context->n_ineq == 040
) {
1953
509
    isl_basic_map_free(context);
1954
509
    return bmap;
1955
509
  }
1956
40
1957
40
  context = isl_basic_map_align_divs(context, bmap);
1958
40
  bmap = isl_basic_map_align_divs(bmap, context);
1959
40
1960
40
  bset = isl_basic_map_underlying_set(isl_basic_map_copy(bmap));
1961
40
  bset_context = isl_basic_map_underlying_set(context);
1962
40
  bset = remove_shifted_constraints(bset, bset_context);
1963
40
  isl_basic_set_free(bset_context);
1964
40
1965
40
  bmap = isl_basic_map_overlying_set(bset, bmap);
1966
40
1967
40
  return bmap;
1968
0
error:
1969
0
  isl_basic_map_free(bmap);
1970
0
  isl_basic_map_free(context);
1971
0
  return NULL;
1972
40
}
1973
1974
/* Does the (linear part of a) constraint "c" involve any of the "len"
1975
 * "relevant" dimensions?
1976
 */
1977
static int is_related(isl_int *c, int len, int *relevant)
1978
291k
{
1979
291k
  int i;
1980
291k
1981
3.44M
  for (i = 0; i < len; 
++i3.15M
) {
1982
3.30M
    if (!relevant[i])
1983
2.45M
      continue;
1984
856k
    if (!isl_int_is_zero(c[i]))
1985
856k
      
return 1154k
;
1986
856k
  }
1987
291k
1988
291k
  
return 0136k
;
1989
291k
}
1990
1991
/* Drop constraints from "bmap" that do not involve any of
1992
 * the dimensions marked "relevant".
1993
 */
1994
static __isl_give isl_basic_map *drop_unrelated_constraints(
1995
  __isl_take isl_basic_map *bmap, int *relevant)
1996
73.1k
{
1997
73.1k
  int i, dim;
1998
73.1k
1999
73.1k
  dim = isl_basic_map_dim(bmap, isl_dim_all);
2000
373k
  for (i = 0; i < dim; 
++i300k
)
2001
343k
    if (!relevant[i])
2002
43.4k
      break;
2003
73.1k
  if (i >= dim)
2004
29.6k
    return bmap;
2005
43.4k
2006
84.8k
  
for (i = bmap->n_eq - 1; 43.4k
i >= 0;
--i41.4k
)
2007
41.4k
    if (!is_related(bmap->eq[i] + 1, dim, relevant)) {
2008
17.5k
      bmap = isl_basic_map_cow(bmap);
2009
17.5k
      if (isl_basic_map_drop_equality(bmap, i) < 0)
2010
0
        return isl_basic_map_free(bmap);
2011
17.5k
    }
2012
43.4k
2013
293k
  
for (i = bmap->n_ineq - 1; 43.4k
i >= 0;
--i249k
)
2014
249k
    if (!is_related(bmap->ineq[i] + 1, dim, relevant)) {
2015
118k
      bmap = isl_basic_map_cow(bmap);
2016
118k
      if (isl_basic_map_drop_inequality(bmap, i) < 0)
2017
0
        return isl_basic_map_free(bmap);
2018
118k
    }
2019
43.4k
2020
43.4k
  return bmap;
2021
43.4k
}
2022
2023
/* Update the groups in "group" based on the (linear part of a) constraint "c".
2024
 *
2025
 * In particular, for any variable involved in the constraint,
2026
 * find the actual group id from before and replace the group
2027
 * of the corresponding variable by the minimal group of all
2028
 * the variables involved in the constraint considered so far
2029
 * (if this minimum is smaller) or replace the minimum by this group
2030
 * (if the minimum is larger).
2031
 *
2032
 * At the end, all the variables in "c" will (indirectly) point
2033
 * to the minimal of the groups that they referred to originally.
2034
 */
2035
static void update_groups(int dim, int *group, isl_int *c)
2036
557k
{
2037
557k
  int j;
2038
557k
  int min = dim;
2039
557k
2040
7.61M
  for (j = 0; j < dim; 
++j7.05M
) {
2041
7.05M
    if (isl_int_is_zero(c[j]))
2042
7.05M
      
continue6.30M
;
2043
753k
    
while (753k
group[j] >= 0 &&
group[group[j]] != group[j]227k
)
2044
142
      group[j] = group[group[j]];
2045
753k
    if (group[j] == min)
2046
120k
      continue;
2047
632k
    if (group[j] < min) {
2048
565k
      if (min >= 0 && min < dim)
2049
7.33k
        group[min] = group[j];
2050
565k
      min = group[j];
2051
565k
    } else
2052
67.5k
      group[group[j]] = min;
2053
632k
  }
2054
557k
}
2055
2056
/* Allocate an array of groups of variables, one for each variable
2057
 * in "context", initialized to zero.
2058
 */
2059
static int *alloc_groups(__isl_keep isl_basic_set *context)
2060
31.0k
{
2061
31.0k
  isl_ctx *ctx;
2062
31.0k
  int dim;
2063
31.0k
2064
31.0k
  dim = isl_basic_set_dim(context, isl_dim_set);
2065
31.0k
  ctx = isl_basic_set_get_ctx(context);
2066
31.0k
  return isl_calloc_array(ctx, int, dim);
2067
31.0k
}
2068
2069
/* Drop constraints from "bmap" that only involve variables that are
2070
 * not related to any of the variables marked with a "-1" in "group".
2071
 *
2072
 * We construct groups of variables that collect variables that
2073
 * (indirectly) appear in some common constraint of "bmap".
2074
 * Each group is identified by the first variable in the group,
2075
 * except for the special group of variables that was already identified
2076
 * in the input as -1 (or are related to those variables).
2077
 * If group[i] is equal to i (or -1), then the group of i is i (or -1),
2078
 * otherwise the group of i is the group of group[i].
2079
 *
2080
 * We first initialize groups for the remaining variables.
2081
 * Then we iterate over the constraints of "bmap" and update the
2082
 * group of the variables in the constraint by the smallest group.
2083
 * Finally, we resolve indirect references to groups by running over
2084
 * the variables.
2085
 *
2086
 * After computing the groups, we drop constraints that do not involve
2087
 * any variables in the -1 group.
2088
 */
2089
__isl_give isl_basic_map *isl_basic_map_drop_unrelated_constraints(
2090
  __isl_take isl_basic_map *bmap, __isl_take int *group)
2091
86.4k
{
2092
86.4k
  int dim;
2093
86.4k
  int i;
2094
86.4k
  int last;
2095
86.4k
2096
86.4k
  if (!bmap)
2097
0
    return NULL;
2098
86.4k
2099
86.4k
  dim = isl_basic_map_dim(bmap, isl_dim_all);
2100
86.4k
2101
86.4k
  last = -1;
2102
592k
  for (i = 0; i < dim; 
++i506k
)
2103
506k
    if (group[i] >= 0)
2104
200k
      last = group[i] = i;
2105
86.4k
  if (last < 0) {
2106
13.3k
    free(group);
2107
13.3k
    return bmap;
2108
13.3k
  }
2109
73.1k
2110
180k
  
for (i = 0; 73.1k
i < bmap->n_eq;
++i107k
)
2111
107k
    update_groups(dim, group, bmap->eq[i] + 1);
2112
523k
  for (i = 0; i < bmap->n_ineq; 
++i450k
)
2113
450k
    update_groups(dim, group, bmap->ineq[i] + 1);
2114
73.1k
2115
547k
  for (i = 0; i < dim; 
++i474k
)
2116
474k
    if (group[i] >= 0)
2117
130k
      group[i] = group[group[i]];
2118
73.1k
2119
547k
  for (i = 0; i < dim; 
++i474k
)
2120
474k
    group[i] = group[i] == -1;
2121
73.1k
2122
73.1k
  bmap = drop_unrelated_constraints(bmap, group);
2123
73.1k
2124
73.1k
  free(group);
2125
73.1k
  return bmap;
2126
73.1k
}
2127
2128
/* Drop constraints from "context" that are irrelevant for computing
2129
 * the gist of "bset".
2130
 *
2131
 * In particular, drop constraints in variables that are not related
2132
 * to any of the variables involved in the constraints of "bset"
2133
 * in the sense that there is no sequence of constraints that connects them.
2134
 *
2135
 * We first mark all variables that appear in "bset" as belonging
2136
 * to a "-1" group and then continue with group_and_drop_irrelevant_constraints.
2137
 */
2138
static __isl_give isl_basic_set *drop_irrelevant_constraints(
2139
  __isl_take isl_basic_set *context, __isl_keep isl_basic_set *bset)
2140
19.8k
{
2141
19.8k
  int *group;
2142
19.8k
  int dim;
2143
19.8k
  int i, j;
2144
19.8k
2145
19.8k
  if (!context || !bset)
2146
0
    return isl_basic_set_free(context);
2147
19.8k
2148
19.8k
  group = alloc_groups(context);
2149
19.8k
2150
19.8k
  if (!group)
2151
0
    return isl_basic_set_free(context);
2152
19.8k
2153
19.8k
  dim = isl_basic_set_dim(bset, isl_dim_set);
2154
131k
  for (i = 0; i < dim; 
++i111k
) {
2155
176k
    for (j = 0; j < bset->n_eq; 
++j64.3k
)
2156
88.8k
      if (!isl_int_is_zero(bset->eq[j][1 + i]))
2157
88.8k
        
break24.4k
;
2158
111k
    if (j < bset->n_eq) {
2159
24.4k
      group[i] = -1;
2160
24.4k
      continue;
2161
24.4k
    }
2162
300k
    
for (j = 0; 87.3k
j < bset->n_ineq;
++j212k
)
2163
242k
      if (!isl_int_is_zero(bset->ineq[j][1 + i]))
2164
242k
        
break29.8k
;
2165
87.3k
    if (j < bset->n_ineq)
2166
29.8k
      group[i] = -1;
2167
87.3k
  }
2168
19.8k
2169
19.8k
  return isl_basic_map_drop_unrelated_constraints(context, group);
2170
19.8k
}
2171
2172
/* Drop constraints from "context" that are irrelevant for computing
2173
 * the gist of the inequalities "ineq".
2174
 * Inequalities in "ineq" for which the corresponding element of row
2175
 * is set to -1 have already been marked for removal and should be ignored.
2176
 *
2177
 * In particular, drop constraints in variables that are not related
2178
 * to any of the variables involved in "ineq"
2179
 * in the sense that there is no sequence of constraints that connects them.
2180
 *
2181
 * We first mark all variables that appear in "bset" as belonging
2182
 * to a "-1" group and then continue with group_and_drop_irrelevant_constraints.
2183
 */
2184
static __isl_give isl_basic_set *drop_irrelevant_constraints_marked(
2185
  __isl_take isl_basic_set *context, __isl_keep isl_mat *ineq, int *row)
2186
11.2k
{
2187
11.2k
  int *group;
2188
11.2k
  int dim;
2189
11.2k
  int i, j, n;
2190
11.2k
2191
11.2k
  if (!context || !ineq)
2192
0
    return isl_basic_set_free(context);
2193
11.2k
2194
11.2k
  group = alloc_groups(context);
2195
11.2k
2196
11.2k
  if (!group)
2197
0
    return isl_basic_set_free(context);
2198
11.2k
2199
11.2k
  dim = isl_basic_set_dim(context, isl_dim_set);
2200
11.2k
  n = isl_mat_rows(ineq);
2201
74.6k
  for (i = 0; i < dim; 
++i63.3k
) {
2202
279k
    for (j = 0; j < n; 
++j215k
) {
2203
239k
      if (row[j] < 0)
2204
84.8k
        continue;
2205
154k
      if (!isl_int_is_zero(ineq->row[j][1 + i]))
2206
154k
        
break23.4k
;
2207
154k
    }
2208
63.3k
    if (j < n)
2209
23.4k
      group[i] = -1;
2210
63.3k
  }
2211
11.2k
2212
11.2k
  return isl_basic_map_drop_unrelated_constraints(context, group);
2213
11.2k
}
2214
2215
/* Do all "n" entries of "row" contain a negative value?
2216
 */
2217
static int all_neg(int *row, int n)
2218
13.4k
{
2219
13.4k
  int i;
2220
13.4k
2221
27.0k
  for (i = 0; i < n; 
++i13.6k
)
2222
24.8k
    if (row[i] >= 0)
2223
11.2k
      return 0;
2224
13.4k
2225
13.4k
  
return 12.17k
;
2226
13.4k
}
2227
2228
/* Update the inequalities in "bset" based on the information in "row"
2229
 * and "tab".
2230
 *
2231
 * In particular, the array "row" contains either -1, meaning that
2232
 * the corresponding inequality of "bset" is redundant, or the index
2233
 * of an inequality in "tab".
2234
 *
2235
 * If the row entry is -1, then drop the inequality.
2236
 * Otherwise, if the constraint is marked redundant in the tableau,
2237
 * then drop the inequality.  Similarly, if it is marked as an equality
2238
 * in the tableau, then turn the inequality into an equality and
2239
 * perform Gaussian elimination.
2240
 */
2241
static __isl_give isl_basic_set *update_ineq(__isl_take isl_basic_set *bset,
2242
  __isl_keep int *row, struct isl_tab *tab)
2243
13.4k
{
2244
13.4k
  int i;
2245
13.4k
  unsigned n_ineq;
2246
13.4k
  unsigned n_eq;
2247
13.4k
  int found_equality = 0;
2248
13.4k
2249
13.4k
  if (!bset)
2250
0
    return NULL;
2251
13.4k
  if (tab && 
tab->empty10.9k
)
2252
2.49k
    return isl_basic_set_set_to_empty(bset);
2253
10.9k
2254
10.9k
  n_ineq = bset->n_ineq;
2255
46.5k
  for (i = n_ineq - 1; i >= 0; 
--i35.6k
) {
2256
35.6k
    if (row[i] < 0) {
2257
18.7k
      if (isl_basic_set_drop_inequality(bset, i) < 0)
2258
0
        return isl_basic_set_free(bset);
2259
18.7k
      continue;
2260
18.7k
    }
2261
16.9k
    if (!tab)
2262
485
      continue;
2263
16.4k
    n_eq = tab->n_eq;
2264
16.4k
    if (isl_tab_is_equality(tab, n_eq + row[i])) {
2265
190
      isl_basic_map_inequality_to_equality(bset, i);
2266
190
      found_equality = 1;
2267
16.2k
    } else if (isl_tab_is_redundant(tab, n_eq + row[i])) {
2268
490
      if (isl_basic_set_drop_inequality(bset, i) < 0)
2269
0
        return isl_basic_set_free(bset);
2270
490
    }
2271
16.4k
  }
2272
10.9k
2273
10.9k
  if (found_equality)
2274
185
    bset = isl_basic_set_gauss(bset, NULL);
2275
10.9k
  bset = isl_basic_set_finalize(bset);
2276
10.9k
  return bset;
2277
10.9k
}
2278
2279
/* Update the inequalities in "bset" based on the information in "row"
2280
 * and "tab" and free all arguments (other than "bset").
2281
 */
2282
static __isl_give isl_basic_set *update_ineq_free(
2283
  __isl_take isl_basic_set *bset, __isl_take isl_mat *ineq,
2284
  __isl_take isl_basic_set *context, __isl_take int *row,
2285
  struct isl_tab *tab)
2286
13.4k
{
2287
13.4k
  isl_mat_free(ineq);
2288
13.4k
  isl_basic_set_free(context);
2289
13.4k
2290
13.4k
  bset = update_ineq(bset, row, tab);
2291
13.4k
2292
13.4k
  free(row);
2293
13.4k
  isl_tab_free(tab);
2294
13.4k
  return bset;
2295
13.4k
}
2296
2297
/* Remove all information from bset that is redundant in the context
2298
 * of context.
2299
 * "ineq" contains the (possibly transformed) inequalities of "bset",
2300
 * in the same order.
2301
 * The (explicit) equalities of "bset" are assumed to have been taken
2302
 * into account by the transformation such that only the inequalities
2303
 * are relevant.
2304
 * "context" is assumed not to be empty.
2305
 *
2306
 * "row" keeps track of the constraint index of a "bset" inequality in "tab".
2307
 * A value of -1 means that the inequality is obviously redundant and may
2308
 * not even appear in  "tab".
2309
 *
2310
 * We first mark the inequalities of "bset"
2311
 * that are obviously redundant with respect to some inequality in "context".
2312
 * Then we remove those constraints from "context" that have become
2313
 * irrelevant for computing the gist of "bset".
2314
 * Note that this removal of constraints cannot be replaced by
2315
 * a factorization because factors in "bset" may still be connected
2316
 * to each other through constraints in "context".
2317
 *
2318
 * If there are any inequalities left, we construct a tableau for
2319
 * the context and then add the inequalities of "bset".
2320
 * Before adding these inequalities, we freeze all constraints such that
2321
 * they won't be considered redundant in terms of the constraints of "bset".
2322
 * Then we detect all redundant constraints (among the
2323
 * constraints that weren't frozen), first by checking for redundancy in the
2324
 * the tableau and then by checking if replacing a constraint by its negation
2325
 * would lead to an empty set.  This last step is fairly expensive
2326
 * and could be optimized by more reuse of the tableau.
2327
 * Finally, we update bset according to the results.
2328
 */
2329
static __isl_give isl_basic_set *uset_gist_full(__isl_take isl_basic_set *bset,
2330
  __isl_take isl_mat *ineq, __isl_take isl_basic_set *context)
2331
19.8k
{
2332
19.8k
  int i, r;
2333
19.8k
  int *row = NULL;
2334
19.8k
  isl_ctx *ctx;
2335
19.8k
  isl_basic_set *combined = NULL;
2336
19.8k
  struct isl_tab *tab = NULL;
2337
19.8k
  unsigned n_eq, context_ineq;
2338
19.8k
2339
19.8k
  if (!bset || !ineq || !context)
2340
0
    goto error;
2341
19.8k
2342
19.8k
  if (bset->n_ineq == 0 || 
isl_basic_set_plain_is_universe(context)14.0k
) {
2343
6.41k
    isl_basic_set_free(context);
2344
6.41k
    isl_mat_free(ineq);
2345
6.41k
    return bset;
2346
6.41k
  }
2347
13.4k
2348
13.4k
  ctx = isl_basic_set_get_ctx(context);
2349
13.4k
  row = isl_calloc_array(ctx, int, bset->n_ineq);
2350
13.4k
  if (!row)
2351
0
    goto error;
2352
13.4k
2353
13.4k
  if (mark_shifted_constraints(ineq, context, row) < 0)
2354
0
    goto error;
2355
13.4k
  if (all_neg(row, bset->n_ineq))
2356
2.17k
    return update_ineq_free(bset, ineq, context, row, NULL);
2357
11.2k
2358
11.2k
  context = drop_irrelevant_constraints_marked(context, ineq, row);
2359
11.2k
  if (!context)
2360
0
    goto error;
2361
11.2k
  if (isl_basic_set_plain_is_universe(context))
2362
287
    return update_ineq_free(bset, ineq, context, row, NULL);
2363
10.9k
2364
10.9k
  n_eq = context->n_eq;
2365
10.9k
  context_ineq = context->n_ineq;
2366
10.9k
  combined = isl_basic_set_cow(isl_basic_set_copy(context));
2367
10.9k
  combined = isl_basic_set_extend_constraints(combined, 0, bset->n_ineq);
2368
10.9k
  tab = isl_tab_from_basic_set(combined, 0);
2369
46.1k
  for (i = 0; i < context_ineq; 
++i35.2k
)
2370
35.2k
    if (isl_tab_freeze_constraint(tab, n_eq + i) < 0)
2371
0
      goto error;
2372
10.9k
  if (isl_tab_extend_cons(tab, bset->n_ineq) < 0)
2373
0
    goto error;
2374
10.9k
  r = context_ineq;
2375
43.6k
  for (i = 0; i < bset->n_ineq; 
++i32.6k
) {
2376
32.6k
    if (row[i] < 0)
2377
10.6k
      continue;
2378
22.0k
    combined = isl_basic_set_add_ineq(combined, ineq->row[i]);
2379
22.0k
    if (isl_tab_add_ineq(tab, ineq->row[i]) < 0)
2380
0
      goto error;
2381
22.0k
    row[i] = r++;
2382
22.0k
  }
2383
10.9k
  if (isl_tab_detect_implicit_equalities(tab) < 0)
2384
0
    goto error;
2385
10.9k
  if (isl_tab_detect_redundant(tab) < 0)
2386
0
    goto error;
2387
43.6k
  
for (i = bset->n_ineq - 1; 10.9k
i >= 0;
--i32.6k
) {
2388
32.6k
    isl_basic_set *test;
2389
32.6k
    int is_empty;
2390
32.6k
2391
32.6k
    if (row[i] < 0)
2392
10.6k
      continue;
2393
22.0k
    r = row[i];
2394
22.0k
    if (tab->con[n_eq + r].is_redundant)
2395
688
      continue;
2396
21.3k
    test = isl_basic_set_dup(combined);
2397
21.3k
    if (isl_inequality_negate(test, r) < 0)
2398
0
      test = isl_basic_set_free(test);
2399
21.3k
    test = isl_basic_set_update_from_tab(test, tab);
2400
21.3k
    is_empty = isl_basic_set_is_empty(test);
2401
21.3k
    isl_basic_set_free(test);
2402
21.3k
    if (is_empty < 0)
2403
0
      goto error;
2404
21.3k
    if (is_empty)
2405
5.55k
      tab->con[n_eq + r].is_redundant = 1;
2406
21.3k
  }
2407
10.9k
  bset = update_ineq_free(bset, ineq, context, row, tab);
2408
10.9k
  if (bset) {
2409
10.9k
    ISL_F_SET(bset, ISL_BASIC_SET_NO_IMPLICIT);
2410
10.9k
    ISL_F_SET(bset, ISL_BASIC_SET_NO_REDUNDANT);
2411
10.9k
  }
2412
10.9k
2413
10.9k
  isl_basic_set_free(combined);
2414
10.9k
  return bset;
2415
0
error:
2416
0
  free(row);
2417
0
  isl_mat_free(ineq);
2418
0
  isl_tab_free(tab);
2419
0
  isl_basic_set_free(combined);
2420
0
  isl_basic_set_free(context);
2421
0
  isl_basic_set_free(bset);
2422
0
  return NULL;
2423
10.9k
}
2424
2425
/* Extract the inequalities of "bset" as an isl_mat.
2426
 */
2427
static __isl_give isl_mat *extract_ineq(__isl_keep isl_basic_set *bset)
2428
19.8k
{
2429
19.8k
  unsigned total;
2430
19.8k
  isl_ctx *ctx;
2431
19.8k
  isl_mat *ineq;
2432
19.8k
2433
19.8k
  if (!bset)
2434
0
    return NULL;
2435
19.8k
2436
19.8k
  ctx = isl_basic_set_get_ctx(bset);
2437
19.8k
  total = isl_basic_set_total_dim(bset);
2438
19.8k
  ineq = isl_mat_sub_alloc6(ctx, bset->ineq, 0, bset->n_ineq,
2439
19.8k
            0, 1 + total);
2440
19.8k
2441
19.8k
  return ineq;
2442
19.8k
}
2443
2444
/* Remove all information from "bset" that is redundant in the context
2445
 * of "context", for the case where both "bset" and "context" are
2446
 * full-dimensional.
2447
 */
2448
static __isl_give isl_basic_set *uset_gist_uncompressed(
2449
  __isl_take isl_basic_set *bset, __isl_take isl_basic_set *context)
2450
9.94k
{
2451
9.94k
  isl_mat *ineq;
2452
9.94k
2453
9.94k
  ineq = extract_ineq(bset);
2454
9.94k
  return uset_gist_full(bset, ineq, context);
2455
9.94k
}
2456
2457
/* Remove all information from "bset" that is redundant in the context
2458
 * of "context", for the case where the combined equalities of
2459
 * "bset" and "context" allow for a compression that can be obtained
2460
 * by preapplication of "T".
2461
 *
2462
 * "bset" itself is not transformed by "T".  Instead, the inequalities
2463
 * are extracted from "bset" and those are transformed by "T".
2464
 * uset_gist_full then determines which of the transformed inequalities
2465
 * are redundant with respect to the transformed "context" and removes
2466
 * the corresponding inequalities from "bset".
2467
 *
2468
 * After preapplying "T" to the inequalities, any common factor is
2469
 * removed from the coefficients.  If this results in a tightening
2470
 * of the constant term, then the same tightening is applied to
2471
 * the corresponding untransformed inequality in "bset".
2472
 * That is, if after plugging in T, a constraint f(x) >= 0 is of the form
2473
 *
2474
 *  g f'(x) + r >= 0
2475
 *
2476
 * with 0 <= r < g, then it is equivalent to
2477
 *
2478
 *  f'(x) >= 0
2479
 *
2480
 * This means that f(x) >= 0 is equivalent to f(x) - r >= 0 in the affine
2481
 * subspace compressed by T since the latter would be transformed to
2482
 *
2483
 *  g f'(x) >= 0
2484
 */
2485
static __isl_give isl_basic_set *uset_gist_compressed(
2486
  __isl_take isl_basic_set *bset, __isl_take isl_basic_set *context,
2487
  __isl_take isl_mat *T)
2488
9.88k
{
2489
9.88k
  isl_ctx *ctx;
2490
9.88k
  isl_mat *ineq;
2491
9.88k
  int i, n_row, n_col;
2492
9.88k
  isl_int rem;
2493
9.88k
2494
9.88k
  ineq = extract_ineq(bset);
2495
9.88k
  ineq = isl_mat_product(ineq, isl_mat_copy(T));
2496
9.88k
  context = isl_basic_set_preimage(context, T);
2497
9.88k
2498
9.88k
  if (!ineq || !context)
2499
0
    goto error;
2500
9.88k
  if (isl_basic_set_plain_is_empty(context)) {
2501
8
    isl_mat_free(ineq);
2502
8
    isl_basic_set_free(context);
2503
8
    return isl_basic_set_set_to_empty(bset);
2504
8
  }
2505
9.87k
2506
9.87k
  ctx = isl_mat_get_ctx(ineq);
2507
9.87k
  n_row = isl_mat_rows(ineq);
2508
9.87k
  n_col = isl_mat_cols(ineq);
2509
9.87k
  isl_int_init(rem);
2510
24.0k
  for (i = 0; i < n_row; 
++i14.1k
) {
2511
14.1k
    isl_seq_gcd(ineq->row[i] + 1, n_col - 1, &ctx->normalize_gcd);
2512
14.1k
    if (isl_int_is_zero(ctx->normalize_gcd))
2513
14.1k
      
continue33
;
2514
14.1k
    if (isl_int_is_one(ctx->normalize_gcd))
2515
14.1k
      
continue13.4k
;
2516
716
    isl_seq_scale_down(ineq->row[i] + 1, ineq->row[i] + 1,
2517
716
            ctx->normalize_gcd, n_col - 1);
2518
716
    isl_int_fdiv_r(rem, ineq->row[i][0], ctx->normalize_gcd);
2519
716
    isl_int_fdiv_q(ineq->row[i][0],
2520
716
        ineq->row[i][0], ctx->normalize_gcd);
2521
716
    if (isl_int_is_zero(rem))
2522
716
      
continue462
;
2523
254
    bset = isl_basic_set_cow(bset);
2524
254
    if (!bset)
2525
0
      break;
2526
254
    isl_int_sub(bset->ineq[i][0], bset->ineq[i][0], rem);
2527
254
  }
2528
9.87k
  isl_int_clear(rem);
2529
9.87k
2530
9.87k
  return uset_gist_full(bset, ineq, context);
2531
0
error:
2532
0
  isl_mat_free(ineq);
2533
0
  isl_basic_set_free(context);
2534
0
  isl_basic_set_free(bset);
2535
0
  return NULL;
2536
9.87k
}
2537
2538
/* Project "bset" onto the variables that are involved in "template".
2539
 */
2540
static __isl_give isl_basic_set *project_onto_involved(
2541
  __isl_take isl_basic_set *bset, __isl_keep isl_basic_set *template)
2542
9.88k
{
2543
9.88k
  int i, n;
2544
9.88k
2545
9.88k
  if (!bset || !template)
2546
0
    return isl_basic_set_free(bset);
2547
9.88k
2548
9.88k
  n = isl_basic_set_dim(template, isl_dim_set);
2549
9.88k
2550
66.3k
  for (i = 0; i < n; 
++i56.4k
) {
2551
56.4k
    isl_bool involved;
2552
56.4k
2553
56.4k
    involved = isl_basic_set_involves_dims(template,
2554
56.4k
              isl_dim_set, i, 1);
2555
56.4k
    if (involved < 0)
2556
0
      return isl_basic_set_free(bset);
2557
56.4k
    if (involved)
2558
30.3k
      continue;
2559
26.0k
    bset = isl_basic_set_eliminate_vars(bset, i, 1);
2560
26.0k
  }
2561
9.88k
2562
9.88k
  return bset;
2563
9.88k
}
2564
2565
/* Remove all information from bset that is redundant in the context
2566
 * of context.  In particular, equalities that are linear combinations
2567
 * of those in context are removed.  Then the inequalities that are
2568
 * redundant in the context of the equalities and inequalities of
2569
 * context are removed.
2570
 *
2571
 * First of all, we drop those constraints from "context"
2572
 * that are irrelevant for computing the gist of "bset".
2573
 * Alternatively, we could factorize the intersection of "context" and "bset".
2574
 *
2575
 * We first compute the intersection of the integer affine hulls
2576
 * of "bset" and "context",
2577
 * compute the gist inside this intersection and then reduce
2578
 * the constraints with respect to the equalities of the context
2579
 * that only involve variables already involved in the input.
2580
 *
2581
 * If two constraints are mutually redundant, then uset_gist_full
2582
 * will remove the second of those constraints.  We therefore first
2583
 * sort the constraints so that constraints not involving existentially
2584
 * quantified variables are given precedence over those that do.
2585
 * We have to perform this sorting before the variable compression,
2586
 * because that may effect the order of the variables.
2587
 */
2588
static __isl_give isl_basic_set *uset_gist(__isl_take isl_basic_set *bset,
2589
  __isl_take isl_basic_set *context)
2590
19.8k
{
2591
19.8k
  isl_mat *eq;
2592
19.8k
  isl_mat *T;
2593
19.8k
  isl_basic_set *aff;
2594
19.8k
  isl_basic_set *aff_context;
2595
19.8k
  unsigned total;
2596
19.8k
2597
19.8k
  if (!bset || !context)
2598
0
    goto error;
2599
19.8k
2600
19.8k
  context = drop_irrelevant_constraints(context, bset);
2601
19.8k
2602
19.8k
  bset = isl_basic_set_detect_equalities(bset);
2603
19.8k
  aff = isl_basic_set_copy(bset);
2604
19.8k
  aff = isl_basic_set_plain_affine_hull(aff);
2605
19.8k
  context = isl_basic_set_detect_equalities(context);
2606
19.8k
  aff_context = isl_basic_set_copy(context);
2607
19.8k
  aff_context = isl_basic_set_plain_affine_hull(aff_context);
2608
19.8k
  aff = isl_basic_set_intersect(aff, aff_context);
2609
19.8k
  if (!aff)
2610
0
    goto error;
2611
19.8k
  if (isl_basic_set_plain_is_empty(aff)) {
2612
1
    isl_basic_set_free(bset);
2613
1
    isl_basic_set_free(context);
2614
1
    return aff;
2615
1
  }
2616
19.8k
  bset = isl_basic_set_sort_constraints(bset);
2617
19.8k
  if (aff->n_eq == 0) {
2618
9.94k
    isl_basic_set_free(aff);
2619
9.94k
    return uset_gist_uncompressed(bset, context);
2620
9.94k
  }
2621
9.88k
  total = isl_basic_set_total_dim(bset);
2622
9.88k
  eq = isl_mat_sub_alloc6(bset->ctx, aff->eq, 0, aff->n_eq, 0, 1 + total);
2623
9.88k
  eq = isl_mat_cow(eq);
2624
9.88k
  T = isl_mat_variable_compression(eq, NULL);
2625
9.88k
  isl_basic_set_free(aff);
2626
9.88k
  if (T && T->n_col == 0) {
2627
0
    isl_mat_free(T);
2628
0
    isl_basic_set_free(context);
2629
0
    return isl_basic_set_set_to_empty(bset);
2630
0
  }
2631
9.88k
2632
9.88k
  aff_context = isl_basic_set_affine_hull(isl_basic_set_copy(context));
2633
9.88k
  aff_context = project_onto_involved(aff_context, bset);
2634
9.88k
2635
9.88k
  bset = uset_gist_compressed(bset, context, T);
2636
9.88k
  bset = isl_basic_set_reduce_using_equalities(bset, aff_context);
2637
9.88k
2638
9.88k
  if (bset) {
2639
9.88k
    ISL_F_SET(bset, ISL_BASIC_SET_NO_IMPLICIT);
2640
9.88k
    ISL_F_SET(bset, ISL_BASIC_SET_NO_REDUNDANT);
2641
9.88k
  }
2642
9.88k
2643
9.88k
  return bset;
2644
0
error:
2645
0
  isl_basic_set_free(bset);
2646
0
  isl_basic_set_free(context);
2647
0
  return NULL;
2648
9.88k
}
2649
2650
/* Return the number of equality constraints in "bmap" that involve
2651
 * local variables.  This function assumes that Gaussian elimination
2652
 * has been applied to the equality constraints.
2653
 */
2654
static int n_div_eq(__isl_keep isl_basic_map *bmap)
2655
1.09k
{
2656
1.09k
  int i;
2657
1.09k
  int total, n_div;
2658
1.09k
2659
1.09k
  if (!bmap)
2660
0
    return -1;
2661
1.09k
2662
1.09k
  if (bmap->n_eq == 0)
2663
433
    return 0;
2664
665
2665
665
  total = isl_basic_map_dim(bmap, isl_dim_all);
2666
665
  n_div = isl_basic_map_dim(bmap, isl_dim_div);
2667
665
  total -= n_div;
2668
665
2669
1.16k
  for (i = 0; i < bmap->n_eq; 
++i498
)
2670
768
    if (isl_seq_first_non_zero(bmap->eq[i] + 1 + total,
2671
768
              n_div) == -1)
2672
270
      return i;
2673
665
2674
665
  
return bmap->n_eq395
;
2675
665
}
2676
2677
/* Construct a basic map in "space" defined by the equality constraints in "eq".
2678
 * The constraints are assumed not to involve any local variables.
2679
 */
2680
static __isl_give isl_basic_map *basic_map_from_equalities(
2681
  __isl_take isl_space *space, __isl_take isl_mat *eq)
2682
2
{
2683
2
  int i, k;
2684
2
  isl_basic_map *bmap = NULL;
2685
2
2686
2
  if (!space || !eq)
2687
0
    goto error;
2688
2
2689
2
  if (1 + isl_space_dim(space, isl_dim_all) != eq->n_col)
2690
2
    
isl_die0
(isl_space_get_ctx(space), isl_error_internal,
2691
2
      "unexpected number of columns", goto error);
2692
2
2693
2
  bmap = isl_basic_map_alloc_space(isl_space_copy(space),
2694
2
              0, eq->n_row, 0);
2695
6
  for (i = 0; i < eq->n_row; 
++i4
) {
2696
4
    k = isl_basic_map_alloc_equality(bmap);
2697
4
    if (k < 0)
2698
0
      goto error;
2699
4
    isl_seq_cpy(bmap->eq[k], eq->row[i], eq->n_col);
2700
4
  }
2701
2
2702
2
  isl_space_free(space);
2703
2
  isl_mat_free(eq);
2704
2
  return bmap;
2705
0
error:
2706
0
  isl_space_free(space);
2707
0
  isl_mat_free(eq);
2708
0
  isl_basic_map_free(bmap);
2709
0
  return NULL;
2710
2
}
2711
2712
/* Construct and return a variable compression based on the equality
2713
 * constraints in "bmap1" and "bmap2" that do not involve the local variables.
2714
 * "n1" is the number of (initial) equality constraints in "bmap1"
2715
 * that do involve local variables.
2716
 * "n2" is the number of (initial) equality constraints in "bmap2"
2717
 * that do involve local variables.
2718
 * "total" is the total number of other variables.
2719
 * This function assumes that Gaussian elimination
2720
 * has been applied to the equality constraints in both "bmap1" and "bmap2"
2721
 * such that the equality constraints not involving local variables
2722
 * are those that start at "n1" or "n2".
2723
 *
2724
 * If either of "bmap1" and "bmap2" does not have such equality constraints,
2725
 * then simply compute the compression based on the equality constraints
2726
 * in the other basic map.
2727
 * Otherwise, combine the equality constraints from both into a new
2728
 * basic map such that Gaussian elimination can be applied to this combination
2729
 * and then construct a variable compression from the resulting
2730
 * equality constraints.
2731
 */
2732
static __isl_give isl_mat *combined_variable_compression(
2733
  __isl_keep isl_basic_map *bmap1, int n1,
2734
  __isl_keep isl_basic_map *bmap2, int n2, int total)
2735
7
{
2736
7
  isl_ctx *ctx;
2737
7
  isl_mat *E1, *E2, *V;
2738
7
  isl_basic_map *bmap;
2739
7
2740
7
  ctx = isl_basic_map_get_ctx(bmap1);
2741
7
  if (bmap1->n_eq == n1) {
2742
3
    E2 = isl_mat_sub_alloc6(ctx, bmap2->eq,
2743
3
          n2, bmap2->n_eq - n2, 0, 1 + total);
2744
3
    return isl_mat_variable_compression(E2, NULL);
2745
3
  }
2746
4
  if (bmap2->n_eq == n2) {
2747
2
    E1 = isl_mat_sub_alloc6(ctx, bmap1->eq,
2748
2
          n1, bmap1->n_eq - n1, 0, 1 + total);
2749
2
    return isl_mat_variable_compression(E1, NULL);
2750
2
  }
2751
2
  E1 = isl_mat_sub_alloc6(ctx, bmap1->eq,
2752
2
        n1, bmap1->n_eq - n1, 0, 1 + total);
2753
2
  E2 = isl_mat_sub_alloc6(ctx, bmap2->eq,
2754
2
        n2, bmap2->n_eq - n2, 0, 1 + total);
2755
2
  E1 = isl_mat_concat(E1, E2);
2756
2
  bmap = basic_map_from_equalities(isl_basic_map_get_space(bmap1), E1);
2757
2
  bmap = isl_basic_map_gauss(bmap, NULL);
2758
2
  if (!bmap)
2759
0
    return NULL;
2760
2
  E1 = isl_mat_sub_alloc6(ctx, bmap->eq, 0, bmap->n_eq, 0, 1 + total);
2761
2
  V = isl_mat_variable_compression(E1, NULL);
2762
2
  isl_basic_map_free(bmap);
2763
2
2764
2
  return V;
2765
2
}
2766
2767
/* Extract the stride constraints from "bmap", compressed
2768
 * with respect to both the stride constraints in "context" and
2769
 * the remaining equality constraints in both "bmap" and "context".
2770
 * "bmap_n_eq" is the number of (initial) stride constraints in "bmap".
2771
 * "context_n_eq" is the number of (initial) stride constraints in "context".
2772
 *
2773
 * Let x be all variables in "bmap" (and "context") other than the local
2774
 * variables.  First compute a variable compression
2775
 *
2776
 *  x = V x'
2777
 *
2778
 * based on the non-stride equality constraints in "bmap" and "context".
2779
 * Consider the stride constraints of "context",
2780
 *
2781
 *  A(x) + B(y) = 0
2782
 *
2783
 * with y the local variables and plug in the variable compression,
2784
 * resulting in
2785
 *
2786
 *  A(V x') + B(y) = 0
2787
 *
2788
 * Use these constraints to compute a parameter compression on x'
2789
 *
2790
 *  x' = T x''
2791
 *
2792
 * Now consider the stride constraints of "bmap"
2793
 *
2794
 *  C(x) + D(y) = 0
2795
 *
2796
 * and plug in x = V*T x''.
2797
 * That is, return A = [C*V*T D].
2798
 */
2799
static __isl_give isl_mat *extract_compressed_stride_constraints(
2800
  __isl_keep isl_basic_map *bmap, int bmap_n_eq,
2801
  __isl_keep isl_basic_map *context, int context_n_eq)
2802
7
{
2803
7
  int total, n_div;
2804
7
  isl_ctx *ctx;
2805
7
  isl_mat *A, *B, *T, *V;
2806
7
2807
7
  total = isl_basic_map_dim(context, isl_dim_all);
2808
7
  n_div = isl_basic_map_dim(context, isl_dim_div);
2809
7
  total -= n_div;
2810
7
2811
7
  ctx = isl_basic_map_get_ctx(bmap);
2812
7
2813
7
  V = combined_variable_compression(bmap, bmap_n_eq,
2814
7
            context, context_n_eq, total);
2815
7
2816
7
  A = isl_mat_sub_alloc6(ctx, context->eq, 0, context_n_eq, 0, 1 + total);
2817
7
  B = isl_mat_sub_alloc6(ctx, context->eq,
2818
7
        0, context_n_eq, 1 + total, n_div);
2819
7
  A = isl_mat_product(A, isl_mat_copy(V));
2820
7
  T = isl_mat_parameter_compression_ext(A, B);
2821
7
  T = isl_mat_product(V, T);
2822
7
2823
7
  n_div = isl_basic_map_dim(bmap, isl_dim_div);
2824
7
  T = isl_mat_diagonal(T, isl_mat_identity(ctx, n_div));
2825
7
2826
7
  A = isl_mat_sub_alloc6(ctx, bmap->eq,
2827
7
        0, bmap_n_eq, 0, 1 + total + n_div);
2828
7
  A = isl_mat_product(A, T);
2829
7
2830
7
  return A;
2831
7
}
2832
2833
/* Remove the prime factors from *g that have an exponent that
2834
 * is strictly smaller than the exponent in "c".
2835
 * All exponents in *g are known to be smaller than or equal
2836
 * to those in "c".
2837
 *
2838
 * That is, if *g is equal to
2839
 *
2840
 *  p_1^{e_1} p_2^{e_2} ... p_n^{e_n}
2841
 *
2842
 * and "c" is equal to
2843
 *
2844
 *  p_1^{f_1} p_2^{f_2} ... p_n^{f_n}
2845
 *
2846
 * then update *g to
2847
 *
2848
 *  p_1^{e_1 * (e_1 = f_1)} p_2^{e_2 * (e_2 = f_2)} ...
2849
 *    p_n^{e_n * (e_n = f_n)}
2850
 *
2851
 * If e_i = f_i, then c / *g does not have any p_i factors and therefore
2852
 * neither does the gcd of *g and c / *g.
2853
 * If e_i < f_i, then the gcd of *g and c / *g has a positive
2854
 * power min(e_i, s_i) of p_i with s_i = f_i - e_i among its factors.
2855
 * Dividing *g by this gcd therefore strictly reduces the exponent
2856
 * of the prime factors that need to be removed, while leaving the
2857
 * other prime factors untouched.
2858
 * Repeating this process until gcd(*g, c / *g) = 1 therefore
2859
 * removes all undesired factors, without removing any others.
2860
 */
2861
static void remove_incomplete_powers(isl_int *g, isl_int c)
2862
6
{
2863
6
  isl_int t;
2864
6
2865
6
  isl_int_init(t);
2866
9
  for (;;) {
2867
9
    isl_int_divexact(t, c, *g);
2868
9
    isl_int_gcd(t, t, *g);
2869
9
    if (isl_int_is_one(t))
2870
9
      
break6
;
2871
3
    isl_int_divexact(*g, *g, t);
2872
3
  }
2873
6
  isl_int_clear(t);
2874
6
}
2875
2876
/* Reduce the "n" stride constraints in "bmap" based on a copy "A"
2877
 * of the same stride constraints in a compressed space that exploits
2878
 * all equalities in the context and the other equalities in "bmap".
2879
 *
2880
 * If the stride constraints of "bmap" are of the form
2881
 *
2882
 *  C(x) + D(y) = 0
2883
 *
2884
 * then A is of the form
2885
 *
2886
 *  B(x') + D(y) = 0
2887
 *
2888
 * If any of these constraints involves only a single local variable y,
2889
 * then the constraint appears as
2890
 *
2891
 *  f(x) + m y_i = 0
2892
 *
2893
 * in "bmap" and as
2894
 *
2895
 *  h(x') + m y_i = 0
2896
 *
2897
 * in "A".
2898
 *
2899
 * Let g be the gcd of m and the coefficients of h.
2900
 * Then, in particular, g is a divisor of the coefficients of h and
2901
 *
2902
 *  f(x) = h(x')
2903
 *
2904
 * is known to be a multiple of g.
2905
 * If some prime factor in m appears with the same exponent in g,
2906
 * then it can be removed from m because f(x) is already known
2907
 * to be a multiple of g and therefore in particular of this power
2908
 * of the prime factors.
2909
 * Prime factors that appear with a smaller exponent in g cannot
2910
 * be removed from m.
2911
 * Let g' be the divisor of g containing all prime factors that
2912
 * appear with the same exponent in m and g, then
2913
 *
2914
 *  f(x) + m y_i = 0
2915
 *
2916
 * can be replaced by
2917
 *
2918
 *  f(x) + m/g' y_i' = 0
2919
 *
2920
 * Note that (if g' != 1) this changes the explicit representation
2921
 * of y_i to that of y_i', so the integer division at position i
2922
 * is marked unknown and later recomputed by a call to
2923
 * isl_basic_map_gauss.
2924
 */
2925
static __isl_give isl_basic_map *reduce_stride_constraints(
2926
  __isl_take isl_basic_map *bmap, int n, __isl_keep isl_mat *A)
2927
7
{
2928
7
  int i;
2929
7
  int total, n_div;
2930
7
  int any = 0;
2931
7
  isl_int gcd;
2932
7
2933
7
  if (!bmap || !A)
2934
0
    return isl_basic_map_free(bmap);
2935
7
2936
7
  total = isl_basic_map_dim(bmap, isl_dim_all);
2937
7
  n_div = isl_basic_map_dim(bmap, isl_dim_div);
2938
7
  total -= n_div;
2939
7
2940
7
  isl_int_init(gcd);
2941
14
  for (i = 0; i < n; 
++i7
) {
2942
7
    int div;
2943
7
2944
7
    div = isl_seq_first_non_zero(bmap->eq[i] + 1 + total, n_div);
2945
7
    if (div < 0)
2946
7
      
isl_die0
(isl_basic_map_get_ctx(bmap), isl_error_internal,
2947
7
        "equality constraints modified unexpectedly",
2948
7
        goto error);
2949
7
    if (isl_seq_first_non_zero(bmap->eq[i] + 1 + total + div + 1,
2950
7
            n_div - div - 1) != -1)
2951
0
      continue;
2952
7
    if (isl_mat_row_gcd(A, i, &gcd) < 0)
2953
0
      goto error;
2954
7
    if (isl_int_is_one(gcd))
2955
7
      
continue1
;
2956
6
    remove_incomplete_powers(&gcd, bmap->eq[i][1 + total + div]);
2957
6
    if (isl_int_is_one(gcd))
2958
6
      
continue1
;
2959
5
    isl_int_divexact(bmap->eq[i][1 + total + div],
2960
5
        bmap->eq[i][1 + total + div], gcd);
2961
5
    bmap = isl_basic_map_mark_div_unknown(bmap, div);
2962
5
    if (!bmap)
2963
0
      goto error;
2964
5
    any = 1;
2965
5
  }
2966
7
  isl_int_clear(gcd);
2967
7
2968
7
  if (any)
2969
5
    bmap = isl_basic_map_gauss(bmap, NULL);
2970
7
2971
7
  return bmap;
2972
0
error:
2973
0
  isl_int_clear(gcd);
2974
0
  isl_basic_map_free(bmap);
2975
0
  return NULL;
2976
7
}
2977
2978
/* Simplify the stride constraints in "bmap" based on
2979
 * the remaining equality constraints in "bmap" and all equality
2980
 * constraints in "context".
2981
 * Only do this if both "bmap" and "context" have stride constraints.
2982
 *
2983
 * First extract a copy of the stride constraints in "bmap" in a compressed
2984
 * space exploiting all the other equality constraints and then
2985
 * use this compressed copy to simplify the original stride constraints.
2986
 */
2987
static __isl_give isl_basic_map *gist_strides(__isl_take isl_basic_map *bmap,
2988
  __isl_keep isl_basic_map *context)
2989
549
{
2990
549
  int bmap_n_eq, context_n_eq;
2991
549
  isl_mat *A;
2992
549
2993
549
  if (!bmap || !context)
2994
0
    return isl_basic_map_free(bmap);
2995
549
2996
549
  bmap_n_eq = n_div_eq(bmap);
2997
549
  context_n_eq = n_div_eq(context);
2998
549
2999
549
  if (bmap_n_eq < 0 || context_n_eq < 0)
3000
0
    return isl_basic_map_free(bmap);
3001
549
  if (bmap_n_eq == 0 || 
context_n_eq == 0349
)
3002
542
    return bmap;
3003
7
3004
7
  A = extract_compressed_stride_constraints(bmap, bmap_n_eq,
3005
7
                context, context_n_eq);
3006
7
  bmap = reduce_stride_constraints(bmap, bmap_n_eq, A);
3007
7
3008
7
  isl_mat_free(A);
3009
7
3010
7
  return bmap;
3011
7
}
3012
3013
/* Return a basic map that has the same intersection with "context" as "bmap"
3014
 * and that is as "simple" as possible.
3015
 *
3016
 * The core computation is performed on the pure constraints.
3017
 * When we add back the meaning of the integer divisions, we need
3018
 * to (re)introduce the div constraints.  If we happen to have
3019
 * discovered that some of these integer divisions are equal to
3020
 * some affine combination of other variables, then these div
3021
 * constraints may end up getting simplified in terms of the equalities,
3022
 * resulting in extra inequalities on the other variables that
3023
 * may have been removed already or that may not even have been
3024
 * part of the input.  We try and remove those constraints of
3025
 * this form that are most obviously redundant with respect to
3026
 * the context.  We also remove those div constraints that are
3027
 * redundant with respect to the other constraints in the result.
3028
 *
3029
 * The stride constraints among the equality constraints in "bmap" are
3030
 * also simplified with respecting to the other equality constraints
3031
 * in "bmap" and with respect to all equality constraints in "context".
3032
 */
3033
__isl_give isl_basic_map *isl_basic_map_gist(__isl_take isl_basic_map *bmap,
3034
  __isl_take isl_basic_map *context)
3035
21.5k
{
3036
21.5k
  isl_basic_set *bset, *eq;
3037
21.5k
  isl_basic_map *eq_bmap;
3038
21.5k
  unsigned total, n_div, extra, n_eq, n_ineq;
3039
21.5k
3040
21.5k
  if (!bmap || !context)
3041
0
    goto error;
3042
21.5k
3043
21.5k
  if (isl_basic_map_plain_is_universe(bmap)) {
3044
1.68k
    isl_basic_map_free(context);
3045
1.68k
    return bmap;
3046
1.68k
  }
3047
19.8k
  if (isl_basic_map_plain_is_empty(context)) {
3048
0
    isl_space *space = isl_basic_map_get_space(bmap);
3049
0
    isl_basic_map_free(bmap);
3050
0
    isl_basic_map_free(context);
3051
0
    return isl_basic_map_universe(space);
3052
0
  }
3053
19.8k
  if (isl_basic_map_plain_is_empty(bmap)) {
3054
0
    isl_basic_map_free(context);
3055
0
    return bmap;
3056
0
  }
3057
19.8k
3058
19.8k
  bmap = isl_basic_map_remove_redundancies(bmap);
3059
19.8k
  context = isl_basic_map_remove_redundancies(context);
3060
19.8k
  context = isl_basic_map_align_divs(context, bmap);
3061
19.8k
  if (!context)
3062
1
    goto error;
3063
19.8k
3064
19.8k
  n_div = isl_basic_map_dim(context, isl_dim_div);
3065
19.8k
  total = isl_basic_map_dim(bmap, isl_dim_all);
3066
19.8k
  extra = n_div - isl_basic_map_dim(bmap, isl_dim_div);
3067
19.8k
3068
19.8k
  bset = isl_basic_map_underlying_set(isl_basic_map_copy(bmap));
3069
19.8k
  bset = isl_basic_set_add_dims(bset, isl_dim_set, extra);
3070
19.8k
  bset = uset_gist(bset,
3071
19.8k
        isl_basic_map_underlying_set(isl_basic_map_copy(context)));
3072
19.8k
  bset = isl_basic_set_project_out(bset, isl_dim_set, total, extra);
3073
19.8k
3074
19.8k
  if (!bset || bset->n_eq == 0 || 
n_div == 011.7k
||
3075
19.8k
      
isl_basic_set_plain_is_empty(bset)671
) {
3076
19.2k
    isl_basic_map_free(context);
3077
19.2k
    return isl_basic_map_overlying_set(bset, bmap);
3078
19.2k
  }
3079
549
3080
549
  n_eq = bset->n_eq;
3081
549
  n_ineq = bset->n_ineq;
3082
549
  eq = isl_basic_set_copy(bset);
3083
549
  eq = isl_basic_set_cow(eq);
3084
549
  if (isl_basic_set_free_inequality(eq, n_ineq) < 0)
3085
0
    eq = isl_basic_set_free(eq);
3086
549
  if (isl_basic_set_free_equality(bset, n_eq) < 0)
3087
0
    bset = isl_basic_set_free(bset);
3088
549
3089
549
  eq_bmap = isl_basic_map_overlying_set(eq, isl_basic_map_copy(bmap));
3090
549
  eq_bmap = gist_strides(eq_bmap, context);
3091
549
  eq_bmap = isl_basic_map_remove_shifted_constraints(eq_bmap, context);
3092
549
  bmap = isl_basic_map_overlying_set(bset, bmap);
3093
549
  bmap = isl_basic_map_intersect(bmap, eq_bmap);
3094
549
  bmap = isl_basic_map_remove_redundancies(bmap);
3095
549
3096
549
  return bmap;
3097
1
error:
3098
1
  isl_basic_map_free(bmap);
3099
1
  isl_basic_map_free(context);
3100
1
  return NULL;
3101
549
}
3102
3103
/*
3104
 * Assumes context has no implicit divs.
3105
 */
3106
__isl_give isl_map *isl_map_gist_basic_map(__isl_take isl_map *map,
3107
  __isl_take isl_basic_map *context)
3108
20.7k
{
3109
20.7k
  int i;
3110
20.7k
3111
20.7k
  if (!map || !context)
3112
0
    goto error;
3113
20.7k
3114
20.7k
  if (isl_basic_map_plain_is_empty(context)) {
3115
0
    isl_space *space = isl_map_get_space(map);
3116
0
    isl_map_free(map);
3117
0
    isl_basic_map_free(context);
3118
0
    return isl_map_universe(space);
3119
0
  }
3120
20.7k
3121
20.7k
  context = isl_basic_map_remove_redundancies(context);
3122
20.7k
  map = isl_map_cow(map);
3123
20.7k
  if (!map || !context)
3124
0
    goto error;
3125
20.7k
  isl_assert(map->ctx, isl_space_is_equal(map->dim, context->dim), goto error);
3126
20.7k
  map = isl_map_compute_divs(map);
3127
20.7k
  if (!map)
3128
0
    goto error;
3129
41.4k
  
for (i = map->n - 1; 20.7k
i >= 0;
--i20.6k
) {
3130
20.6k
    map->p[i] = isl_basic_map_gist(map->p[i],
3131
20.6k
            isl_basic_map_copy(context));
3132
20.6k
    if (!map->p[i])
3133
0
      goto error;
3134
20.6k
    if (isl_basic_map_plain_is_empty(map->p[i])) {
3135
2.53k
      isl_basic_map_free(map->p[i]);
3136
2.53k
      if (i != map->n - 1)
3137
1.09k
        map->p[i] = map->p[map->n - 1];
3138
2.53k
      map->n--;
3139
2.53k
    }
3140
20.6k
  }
3141
20.7k
  isl_basic_map_free(context);
3142
20.7k
  ISL_F_CLR(map, ISL_MAP_NORMALIZED);
3143
20.7k
  return map;
3144
0
error:
3145
0
  isl_map_free(map);
3146
0
  isl_basic_map_free(context);
3147
0
  return NULL;
3148
20.7k
}
3149
3150
/* Drop all inequalities from "bmap" that also appear in "context".
3151
 * "context" is assumed to have only known local variables and
3152
 * the initial local variables of "bmap" are assumed to be the same
3153
 * as those of "context".
3154
 * The constraints of both "bmap" and "context" are assumed
3155
 * to have been sorted using isl_basic_map_sort_constraints.
3156
 *
3157
 * Run through the inequality constraints of "bmap" and "context"
3158
 * in sorted order.
3159
 * If a constraint of "bmap" involves variables not in "context",
3160
 * then it cannot appear in "context".
3161
 * If a matching constraint is found, it is removed from "bmap".
3162
 */
3163
static __isl_give isl_basic_map *drop_inequalities(
3164
  __isl_take isl_basic_map *bmap, __isl_keep isl_basic_map *context)
3165
379
{
3166
379
  int i1, i2;
3167
379
  unsigned total, extra;
3168
379
3169
379
  if (!bmap || !context)
3170
0
    return isl_basic_map_free(bmap);
3171
379
3172
379
  total = isl_basic_map_total_dim(context);
3173
379
  extra = isl_basic_map_total_dim(bmap) - total;
3174
379
3175
379
  i1 = bmap->n_ineq - 1;
3176
379
  i2 = context->n_ineq - 1;
3177
1.46k
  while (bmap && i1 >= 0 && 
i2 >= 01.22k
) {
3178
1.08k
    int cmp;
3179
1.08k
3180
1.08k
    if (isl_seq_first_non_zero(bmap->ineq[i1] + 1 + total,
3181
1.08k
              extra) != -1) {
3182
18
      --i1;
3183
18
      continue;
3184
18
    }
3185
1.06k
    cmp = isl_basic_map_constraint_cmp(context, bmap->ineq[i1],
3186
1.06k
              context->ineq[i2]);
3187
1.06k
    if (cmp < 0) {
3188
0
      --i2;
3189
0
      continue;
3190
0
    }
3191
1.06k
    if (cmp > 0) {
3192
303
      --i1;
3193
303
      continue;
3194
303
    }
3195
763
    if (isl_int_eq(bmap->ineq[i1][0], context->ineq[i2][0])) {
3196
692
      bmap = isl_basic_map_cow(bmap);
3197
692
      if (isl_basic_map_drop_inequality(bmap, i1) < 0)
3198
0
        bmap = isl_basic_map_free(bmap);
3199
692
    }
3200
763
    --i1;
3201
763
    --i2;
3202
763
  }
3203
379
3204
379
  return bmap;
3205
379
}
3206
3207
/* Drop all equalities from "bmap" that also appear in "context".
3208
 * "context" is assumed to have only known local variables and
3209
 * the initial local variables of "bmap" are assumed to be the same
3210
 * as those of "context".
3211
 *
3212
 * Run through the equality constraints of "bmap" and "context"
3213
 * in sorted order.
3214
 * If a constraint of "bmap" involves variables not in "context",
3215
 * then it cannot appear in "context".
3216
 * If a matching constraint is found, it is removed from "bmap".
3217
 */
3218
static __isl_give isl_basic_map *drop_equalities(
3219
  __isl_take isl_basic_map *bmap, __isl_keep isl_basic_map *context)
3220
379
{
3221
379
  int i1, i2;
3222
379
  unsigned total, extra;
3223
379
3224
379
  if (!bmap || !context)
3225
0
    return isl_basic_map_free(bmap);
3226
379
3227
379
  total = isl_basic_map_total_dim(context);
3228
379
  extra = isl_basic_map_total_dim(bmap) - total;
3229
379
3230
379
  i1 = bmap->n_eq - 1;
3231
379
  i2 = context->n_eq - 1;
3232
379
3233
411
  while (bmap && i1 >= 0 && 
i2 >= 071
) {
3234
32
    int last1, last2;
3235
32
3236
32
    if (isl_seq_first_non_zero(bmap->eq[i1] + 1 + total,
3237
32
              extra) != -1)
3238
0
      break;
3239
32
    last1 = isl_seq_last_non_zero(bmap->eq[i1] + 1, total);
3240
32
    last2 = isl_seq_last_non_zero(context->eq[i2] + 1, total);
3241
32
    if (last1 > last2) {
3242
0
      --i2;
3243
0
      continue;
3244
0
    }
3245
32
    if (last1 < last2) {
3246
3
      --i1;
3247
3
      continue;
3248
3
    }
3249
29
    if (isl_seq_eq(bmap->eq[i1], context->eq[i2], 1 + total)) {
3250
29
      bmap = isl_basic_map_cow(bmap);
3251
29
      if (isl_basic_map_drop_equality(bmap, i1) < 0)
3252
0
        bmap = isl_basic_map_free(bmap);
3253
29
    }
3254
29
    --i1;
3255
29
    --i2;
3256
29
  }
3257
379
3258
379
  return bmap;
3259
379
}
3260
3261
/* Remove the constraints in "context" from "bmap".
3262
 * "context" is assumed to have explicit representations
3263
 * for all local variables.
3264
 *
3265
 * First align the divs of "bmap" to those of "context" and
3266
 * sort the constraints.  Then drop all constraints from "bmap"
3267
 * that appear in "context".
3268
 */
3269
__isl_give isl_basic_map *isl_basic_map_plain_gist(
3270
  __isl_take isl_basic_map *bmap, __isl_take isl_basic_map *context)
3271
379
{
3272
379
  isl_bool done, known;
3273
379
3274
379
  done = isl_basic_map_plain_is_universe(context);
3275
379
  if (done == isl_bool_false)
3276
379
    done = isl_basic_map_plain_is_universe(bmap);
3277
379
  if (done == isl_bool_false)
3278
379
    done = isl_basic_map_plain_is_empty(context);
3279
379
  if (done == isl_bool_false)
3280
379
    done = isl_basic_map_plain_is_empty(bmap);
3281
379
  if (done < 0)
3282
0
    goto error;
3283
379
  if (done) {
3284
0
    isl_basic_map_free(context);
3285
0
    return bmap;
3286
0
  }
3287
379
  known = isl_basic_map_divs_known(context);
3288
379
  if (known < 0)
3289
0
    goto error;
3290
379
  if (!known)
3291
379
    
isl_die0
(isl_basic_map_get_ctx(bmap), isl_error_invalid,
3292
379
      "context has unknown divs", goto error);
3293
379
3294
379
  bmap = isl_basic_map_align_divs(bmap, context);
3295
379
  bmap = isl_basic_map_gauss(bmap, NULL);
3296
379
  bmap = isl_basic_map_sort_constraints(bmap);
3297
379
  context = isl_basic_map_sort_constraints(context);
3298
379
3299
379
  bmap = drop_inequalities(bmap, context);
3300
379
  bmap = drop_equalities(bmap, context);
3301
379
3302
379
  isl_basic_map_free(context);
3303
379
  bmap = isl_basic_map_finalize(bmap);
3304
379
  return bmap;
3305
0
error:
3306
0
  isl_basic_map_free(bmap);
3307
0
  isl_basic_map_free(context);
3308
0
  return NULL;
3309
379
}
3310
3311
/* Replace "map" by the disjunct at position "pos" and free "context".
3312
 */
3313
static __isl_give isl_map *replace_by_disjunct(__isl_take isl_map *map,
3314
  int pos, __isl_take isl_basic_map *context)
3315
4
{
3316
4
  isl_basic_map *bmap;
3317
4
3318
4
  bmap = isl_basic_map_copy(map->p[pos]);
3319
4
  isl_map_free(map);
3320
4
  isl_basic_map_free(context);
3321
4
  return isl_map_from_basic_map(bmap);
3322
4
}
3323
3324
/* Remove the constraints in "context" from "map".
3325
 * If any of the disjuncts in the result turns out to be the universe,
3326
 * then return this universe.
3327
 * "context" is assumed to have explicit representations
3328
 * for all local variables.
3329
 */
3330
__isl_give isl_map *isl_map_plain_gist_basic_map(__isl_take isl_map *map,
3331
  __isl_take isl_basic_map *context)
3332
280
{
3333
280
  int i;
3334
280
  isl_bool univ, known;
3335
280
3336
280
  univ = isl_basic_map_plain_is_universe(context);
3337
280
  if (univ < 0)
3338
0
    goto error;
3339
280
  if (univ) {
3340
89
    isl_basic_map_free(context);
3341
89
    return map;
3342
89
  }
3343
191
  known = isl_basic_map_divs_known(context);
3344
191
  if (known < 0)
3345
0
    goto error;
3346
191
  if (!known)
3347
191
    
isl_die0
(isl_map_get_ctx(map), isl_error_invalid,
3348
191
      "context has unknown divs", goto error);
3349
191
3350
191
  map = isl_map_cow(map);
3351
191
  if (!map)
3352
0
    goto error;
3353
566
  
for (i = 0; 191
i < map->n;
++i375
) {
3354
379
    map->p[i] = isl_basic_map_plain_gist(map->p[i],
3355
379
            isl_basic_map_copy(context));
3356
379
    univ = isl_basic_map_plain_is_universe(map->p[i]);
3357
379
    if (univ < 0)
3358
0
      goto error;
3359
379
    if (univ && 
map->n > 14
)
3360
4
      return replace_by_disjunct(map, i, context);
3361
379
  }
3362
191
3363
191
  isl_basic_map_free(context);
3364
187
  ISL_F_CLR(map, ISL_MAP_NORMALIZED);
3365
187
  if (map->n > 1)
3366
187
    ISL_F_CLR(map, ISL_MAP_DISJOINT);
3367
187
  return map;
3368
0
error:
3369
0
  isl_map_free(map);
3370
0
  isl_basic_map_free(context);
3371
0
  return NULL;
3372
191
}
3373
3374
/* Remove the constraints in "context" from "set".
3375
 * If any of the disjuncts in the result turns out to be the universe,
3376
 * then return this universe.
3377
 * "context" is assumed to have explicit representations
3378
 * for all local variables.
3379
 */
3380
__isl_give isl_set *isl_set_plain_gist_basic_set(__isl_take isl_set *set,
3381
  __isl_take isl_basic_set *context)
3382
101
{
3383
101
  return set_from_map(isl_map_plain_gist_basic_map(set_to_map(set),
3384
101
              bset_to_bmap(context)));
3385
101
}
3386
3387
/* Remove the constraints in "context" from "map".
3388
 * If any of the disjuncts in the result turns out to be the universe,
3389
 * then return this universe.
3390
 * "context" is assumed to consist of a single disjunct and
3391
 * to have explicit representations for all local variables.
3392
 */
3393
__isl_give isl_map *isl_map_plain_gist(__isl_take isl_map *map,
3394
  __isl_take isl_map *context)
3395
20
{
3396
20
  isl_basic_map *hull;
3397
20
3398
20
  hull = isl_map_unshifted_simple_hull(context);
3399
20
  return isl_map_plain_gist_basic_map(map, hull);
3400
20
}
3401
3402
/* Replace "map" by a universe map in the same space and free "drop".
3403
 */
3404
static __isl_give isl_map *replace_by_universe(__isl_take isl_map *map,
3405
  __isl_take isl_map *drop)
3406
10.1k
{
3407
10.1k
  isl_map *res;
3408
10.1k
3409
10.1k
  res = isl_map_universe(isl_map_get_space(map));
3410
10.1k
  isl_map_free(map);
3411
10.1k
  isl_map_free(drop);
3412
10.1k
  return res;
3413
10.1k
}
3414
3415
/* Return a map that has the same intersection with "context" as "map"
3416
 * and that is as "simple" as possible.
3417
 *
3418
 * If "map" is already the universe, then we cannot make it any simpler.
3419
 * Similarly, if "context" is the universe, then we cannot exploit it
3420
 * to simplify "map"
3421
 * If "map" and "context" are identical to each other, then we can
3422
 * return the corresponding universe.
3423
 *
3424
 * If either "map" or "context" consists of multiple disjuncts,
3425
 * then check if "context" happens to be a subset of "map",
3426
 * in which case all constraints can be removed.
3427
 * In case of multiple disjuncts, the standard procedure
3428
 * may not be able to detect that all constraints can be removed.
3429
 *
3430
 * If none of these cases apply, we have to work a bit harder.
3431
 * During this computation, we make use of a single disjunct context,
3432
 * so if the original context consists of more than one disjunct
3433
 * then we need to approximate the context by a single disjunct set.
3434
 * Simply taking the simple hull may drop constraints that are
3435
 * only implicitly available in each disjunct.  We therefore also
3436
 * look for constraints among those defining "map" that are valid
3437
 * for the context.  These can then be used to simplify away
3438
 * the corresponding constraints in "map".
3439
 */
3440
static __isl_give isl_map *map_gist(__isl_take isl_map *map,
3441
  __isl_take isl_map *context)
3442
58.4k
{
3443
58.4k
  int equal;
3444
58.4k
  int is_universe;
3445
58.4k
  int single_disjunct_map, single_disjunct_context;
3446
58.4k
  isl_bool subset;
3447
58.4k
  isl_basic_map *hull;
3448
58.4k
3449
58.4k
  is_universe = isl_map_plain_is_universe(map);
3450
58.4k
  if (is_universe >= 0 && !is_universe)
3451
37.0k
    is_universe = isl_map_plain_is_universe(context);
3452
58.4k
  if (is_universe < 0)
3453
0
    goto error;
3454
58.4k
  if (is_universe) {
3455
30.0k
    isl_map_free(context);
3456
30.0k
    return map;
3457
30.0k
  }
3458
28.4k
3459
28.4k
  equal = isl_map_plain_is_equal(map, context);
3460
28.4k
  if (equal < 0)
3461
0
    goto error;
3462
28.4k
  if (equal)
3463
10.0k
    return replace_by_universe(map, context);
3464
18.4k
3465
18.4k
  single_disjunct_map = isl_map_n_basic_map(map) == 1;
3466
18.4k
  single_disjunct_context = isl_map_n_basic_map(context) == 1;
3467
18.4k
  if (!single_disjunct_map || 
!single_disjunct_context13.0k
) {
3468
5.91k
    subset = isl_map_is_subset(context, map);
3469
5.91k
    if (subset < 0)
3470
0
      goto error;
3471
5.91k
    if (subset)
3472
29
      return replace_by_universe(map, context);
3473
18.3k
  }
3474
18.3k
3475
18.3k
  context = isl_map_compute_divs(context);
3476
18.3k
  if (!context)
3477
0
    goto error;
3478
18.3k
  if (single_disjunct_context) {
3479
17.5k
    hull = isl_map_simple_hull(context);
3480
17.5k
  } else {
3481
798
    isl_ctx *ctx;
3482
798
    isl_map_list *list;
3483
798
3484
798
    ctx = isl_map_get_ctx(map);
3485
798
    list = isl_map_list_alloc(ctx, 2);
3486
798
    list = isl_map_list_add(list, isl_map_copy(context));
3487
798
    list = isl_map_list_add(list, isl_map_copy(map));
3488
798
    hull = isl_map_unshifted_simple_hull_from_map_list(context,
3489
798
                    list);
3490
798
  }
3491
18.3k
  return isl_map_gist_basic_map(map, hull);
3492
0
error:
3493
0
  isl_map_free(map);
3494
0
  isl_map_free(context);
3495
0
  return NULL;
3496
18.3k
}
3497
3498
__isl_give isl_map *isl_map_gist(__isl_take isl_map *map,
3499
  __isl_take isl_map *context)
3500
58.4k
{
3501
58.4k
  return isl_map_align_params_map_map_and(map, context, &map_gist);
3502
58.4k
}
3503
3504
struct isl_basic_set *isl_basic_set_gist(struct isl_basic_set *bset,
3505
            struct isl_basic_set *context)
3506
834
{
3507
834
  return bset_from_bmap(isl_basic_map_gist(bset_to_bmap(bset),
3508
834
            bset_to_bmap(context)));
3509
834
}
3510
3511
__isl_give isl_set *isl_set_gist_basic_set(__isl_take isl_set *set,
3512
  __isl_take isl_basic_set *context)
3513
2.42k
{
3514
2.42k
  return set_from_map(isl_map_gist_basic_map(set_to_map(set),
3515
2.42k
          bset_to_bmap(context)));
3516
2.42k
}
3517
3518
__isl_give isl_set *isl_set_gist_params_basic_set(__isl_take isl_set *set,
3519
  __isl_take isl_basic_set *context)
3520
0
{
3521
0
  isl_space *space = isl_set_get_space(set);
3522
0
  isl_basic_set *dom_context = isl_basic_set_universe(space);
3523
0
  dom_context = isl_basic_set_intersect_params(dom_context, context);
3524
0
  return isl_set_gist_basic_set(set, dom_context);
3525
0
}
3526
3527
__isl_give isl_set *isl_set_gist(__isl_take isl_set *set,
3528
  __isl_take isl_set *context)
3529
14.4k
{
3530
14.4k
  return set_from_map(isl_map_gist(set_to_map(set), set_to_map(context)));
3531
14.4k
}
3532
3533
/* Compute the gist of "bmap" with respect to the constraints "context"
3534
 * on the domain.
3535
 */
3536
__isl_give isl_basic_map *isl_basic_map_gist_domain(
3537
  __isl_take isl_basic_map *bmap, __isl_take isl_basic_set *context)
3538
0
{
3539
0
  isl_space *space = isl_basic_map_get_space(bmap);
3540
0
  isl_basic_map *bmap_context = isl_basic_map_universe(space);
3541
0
3542
0
  bmap_context = isl_basic_map_intersect_domain(bmap_context, context);
3543
0
  return isl_basic_map_gist(bmap, bmap_context);
3544
0
}
3545
3546
__isl_give isl_map *isl_map_gist_domain(__isl_take isl_map *map,
3547
  __isl_take isl_set *context)
3548
6.85k
{
3549
6.85k
  isl_map *map_context = isl_map_universe(isl_map_get_space(map));
3550
6.85k
  map_context = isl_map_intersect_domain(map_context, context);
3551
6.85k
  return isl_map_gist(map, map_context);
3552
6.85k
}
3553
3554
__isl_give isl_map *isl_map_gist_range(__isl_take isl_map *map,
3555
  __isl_take isl_set *context)
3556
100
{
3557
100
  isl_map *map_context = isl_map_universe(isl_map_get_space(map));
3558
100
  map_context = isl_map_intersect_range(map_context, context);
3559
100
  return isl_map_gist(map, map_context);
3560
100
}
3561
3562
__isl_give isl_map *isl_map_gist_params(__isl_take isl_map *map,
3563
  __isl_take isl_set *context)
3564
31.4k
{
3565
31.4k
  isl_map *map_context = isl_map_universe(isl_map_get_space(map));
3566
31.4k
  map_context = isl_map_intersect_params(map_context, context);
3567
31.4k
  return isl_map_gist(map, map_context);
3568
31.4k
}
3569
3570
__isl_give isl_set *isl_set_gist_params(__isl_take isl_set *set,
3571
  __isl_take isl_set *context)
3572
24.4k
{
3573
24.4k
  return isl_map_gist_params(set, context);
3574
24.4k
}
3575
3576
/* Quick check to see if two basic maps are disjoint.
3577
 * In particular, we reduce the equalities and inequalities of
3578
 * one basic map in the context of the equalities of the other
3579
 * basic map and check if we get a contradiction.
3580
 */
3581
isl_bool isl_basic_map_plain_is_disjoint(__isl_keep isl_basic_map *bmap1,
3582
  __isl_keep isl_basic_map *bmap2)
3583
30.1k
{
3584
30.1k
  struct isl_vec *v = NULL;
3585
30.1k
  int *elim = NULL;
3586
30.1k
  unsigned total;
3587
30.1k
  int i;
3588
30.1k
3589
30.1k
  if (!bmap1 || !bmap2)
3590
0
    return isl_bool_error;
3591
30.1k
  isl_assert(bmap1->ctx, isl_space_is_equal(bmap1->dim, bmap2->dim),
3592
30.1k
      return isl_bool_error);
3593
30.1k
  if (bmap1->n_div || 
bmap2->n_div25.8k
)
3594
5.77k
    return isl_bool_false;
3595
24.3k
  if (!bmap1->n_eq && 
!bmap2->n_eq6.54k
)
3596
5.09k
    return isl_bool_false;
3597
19.2k
3598
19.2k
  total = isl_space_dim(bmap1->dim, isl_dim_all);
3599
19.2k
  if (total == 0)
3600
0
    return isl_bool_false;
3601
19.2k
  v = isl_vec_alloc(bmap1->ctx, 1 + total);
3602
19.2k
  if (!v)
3603
0
    goto error;
3604
19.2k
  elim = isl_alloc_array(bmap1->ctx, int, total);
3605
19.2k
  if (!elim)
3606
0
    goto error;
3607
19.2k
  compute_elimination_index(bmap1, elim);
3608
42.9k
  for (i = 0; i < bmap2->n_eq; 
++i23.7k
) {
3609
26.2k
    int reduced;
3610
26.2k
    reduced = reduced_using_equalities(v->block.data, bmap2->eq[i],
3611
26.2k
              bmap1, elim);
3612
26.2k
    if (reduced && 
!11.9k
isl_int_is_zero11.9k
(v->block.data[0]) &&
3613
26.2k
        
isl_seq_first_non_zero(v->block.data + 1, total) == -13.31k
)
3614
2.47k
      goto disjoint;
3615
26.2k
  }
3616
142k
  
for (i = 0; 16.7k
i < bmap2->n_ineq;
++i125k
) {
3617
130k
    int reduced;
3618
130k
    reduced = reduced_using_equalities(v->block.data,
3619
130k
            bmap2->ineq[i], bmap1, elim);
3620
130k
    if (reduced && 
isl_int_is_neg8.60k
(v->block.data[0]) &&
3621
130k
        
isl_seq_first_non_zero(v->block.data + 1, total) == -15.64k
)
3622
5.06k
      goto disjoint;
3623
130k
  }
3624
16.7k
  compute_elimination_index(bmap2, elim);
3625
83.6k
  for (i = 0; i < bmap1->n_ineq; 
++i71.8k
) {
3626
75.8k
    int reduced;
3627
75.8k
    reduced = reduced_using_equalities(v->block.data,
3628
75.8k
            bmap1->ineq[i], bmap2, elim);
3629
75.8k
    if (reduced && 
isl_int_is_neg5.11k
(v->block.data[0]) &&
3630
75.8k
        
isl_seq_first_non_zero(v->block.data + 1, total) == -14.16k
)
3631
3.92k
      goto disjoint;
3632
75.8k
  }
3633
11.7k
  isl_vec_free(v);
3634
7.77k
  free(elim);
3635
7.77k
  return isl_bool_false;
3636
11.4k
disjoint:
3637
11.4k
  isl_vec_free(v);
3638
11.4k
  free(elim);
3639
11.4k
  return isl_bool_true;
3640
0
error:
3641
0
  isl_vec_free(v);
3642
0
  free(elim);
3643
0
  return isl_bool_error;
3644
11.7k
}
3645
3646
int isl_basic_set_plain_is_disjoint(__isl_keep isl_basic_set *bset1,
3647
  __isl_keep isl_basic_set *bset2)
3648
0
{
3649
0
  return isl_basic_map_plain_is_disjoint(bset_to_bmap(bset1),
3650
0
                bset_to_bmap(bset2));
3651
0
}
3652
3653
/* Does "test" hold for all pairs of basic maps in "map1" and "map2"?
3654
 */
3655
static isl_bool all_pairs(__isl_keep isl_map *map1, __isl_keep isl_map *map2,
3656
  isl_bool (*test)(__isl_keep isl_basic_map *bmap1,
3657
    __isl_keep isl_basic_map *bmap2))
3658
19.2k
{
3659
19.2k
  int i, j;
3660
19.2k
3661
19.2k
  if (!map1 || !map2)
3662
0
    return isl_bool_error;
3663
19.2k
3664
37.5k
  
for (i = 0; 19.2k
i < map1->n;
++i18.3k
) {
3665
48.4k
    for (j = 0; j < map2->n; 
++j19.5k
) {
3666
30.1k
      isl_bool d = test(map1->p[i], map2->p[j]);
3667
30.1k
      if (d != isl_bool_true)
3668
10.5k
        return d;
3669
30.1k
    }
3670
28.8k
  }
3671
19.2k
3672
19.2k
  
return isl_bool_true8.67k
;
3673
19.2k
}
3674
3675
/* Are "map1" and "map2" obviously disjoint, based on information
3676
 * that can be derived without looking at the individual basic maps?
3677
 *
3678
 * In particular, if one of them is empty or if they live in different spaces
3679
 * (ignoring parameters), then they are clearly disjoint.
3680
 */
3681
static isl_bool isl_map_plain_is_disjoint_global(__isl_keep isl_map *map1,
3682
  __isl_keep isl_map *map2)
3683
43.7k
{
3684
43.7k
  isl_bool disjoint;
3685
43.7k
  isl_bool match;
3686
43.7k
3687
43.7k
  if (!map1 || !map2)
3688
0
    return isl_bool_error;
3689
43.7k
3690
43.7k
  disjoint = isl_map_plain_is_empty(map1);
3691
43.7k
  if (disjoint < 0 || disjoint)
3692
5.63k
    return disjoint;
3693
38.0k
3694
38.0k
  disjoint = isl_map_plain_is_empty(map2);
3695
38.0k
  if (disjoint < 0 || disjoint)
3696
9.61k
    return disjoint;
3697
28.4k
3698
28.4k
  match = isl_space_tuple_is_equal(map1->dim, isl_dim_in,
3699
28.4k
        map2->dim, isl_dim_in);
3700
28.4k
  if (match < 0 || !match)
3701
0
    return match < 0 ? isl_bool_error : isl_bool_true;
3702
28.4k
3703
28.4k
  match = isl_space_tuple_is_equal(map1->dim, isl_dim_out,
3704
28.4k
        map2->dim, isl_dim_out);
3705
28.4k
  if (match < 0 || !match)
3706
0
    return match < 0 ? isl_bool_error : isl_bool_true;
3707
28.4k
3708
28.4k
  return isl_bool_false;
3709
28.4k
}
3710
3711
/* Are "map1" and "map2" obviously disjoint?
3712
 *
3713
 * If one of them is empty or if they live in different spaces (ignoring
3714
 * parameters), then they are clearly disjoint.
3715
 * This is checked by isl_map_plain_is_disjoint_global.
3716
 *
3717
 * If they have different parameters, then we skip any further tests.
3718
 *
3719
 * If they are obviously equal, but not obviously empty, then we will
3720
 * not be able to detect if they are disjoint.
3721
 *
3722
 * Otherwise we check if each basic map in "map1" is obviously disjoint
3723
 * from each basic map in "map2".
3724
 */
3725
isl_bool isl_map_plain_is_disjoint(__isl_keep isl_map *map1,
3726
  __isl_keep isl_map *map2)
3727
0
{
3728
0
  isl_bool disjoint;
3729
0
  isl_bool intersect;
3730
0
  isl_bool match;
3731
0
3732
0
  disjoint = isl_map_plain_is_disjoint_global(map1, map2);
3733
0
  if (disjoint < 0 || disjoint)
3734
0
    return disjoint;
3735
0
3736
0
  match = isl_map_has_equal_params(map1, map2);
3737
0
  if (match < 0 || !match)
3738
0
    return match < 0 ? isl_bool_error : isl_bool_false;
3739
0
3740
0
  intersect = isl_map_plain_is_equal(map1, map2);
3741
0
  if (intersect < 0 || intersect)
3742
0
    return intersect < 0 ? isl_bool_error : isl_bool_false;
3743
0
3744
0
  return all_pairs(map1, map2, &isl_basic_map_plain_is_disjoint);
3745
0
}
3746
3747
/* Are "map1" and "map2" disjoint?
3748
 * The parameters are assumed to have been aligned.
3749
 *
3750
 * In particular, check whether all pairs of basic maps are disjoint.
3751
 */
3752
static isl_bool isl_map_is_disjoint_aligned(__isl_keep isl_map *map1,
3753
  __isl_keep isl_map *map2)
3754
19.2k
{
3755
19.2k
  return all_pairs(map1, map2, &isl_basic_map_is_disjoint);
3756
19.2k
}
3757
3758
/* Are "map1" and "map2" disjoint?
3759
 *
3760
 * They are disjoint if they are "obviously disjoint" or if one of them
3761
 * is empty.  Otherwise, they are not disjoint if one of them is universal.
3762
 * If the two inputs are (obviously) equal and not empty, then they are
3763
 * not disjoint.
3764
 * If none of these cases apply, then check if all pairs of basic maps
3765
 * are disjoint after aligning the parameters.
3766
 */
3767
isl_bool isl_map_is_disjoint(__isl_keep isl_map *map1, __isl_keep isl_map *map2)
3768
43.7k
{
3769
43.7k
  isl_bool disjoint;
3770
43.7k
  isl_bool intersect;
3771
43.7k
3772
43.7k
  disjoint = isl_map_plain_is_disjoint_global(map1, map2);
3773
43.7k
  if (disjoint < 0 || disjoint)
3774
15.2k
    return disjoint;
3775
28.4k
3776
28.4k
  disjoint = isl_map_is_empty(map1);
3777
28.4k
  if (disjoint < 0 || disjoint)
3778
0
    return disjoint;
3779
28.4k
3780
28.4k
  disjoint = isl_map_is_empty(map2);
3781
28.4k
  if (disjoint < 0 || disjoint)
3782
0
    return disjoint;
3783
28.4k
3784
28.4k
  intersect = isl_map_plain_is_universe(map1);
3785
28.4k
  if (intersect < 0 || intersect)
3786
6.60k
    return intersect < 0 ? 
isl_bool_error0
: isl_bool_false;
3787
21.8k
3788
21.8k
  intersect = isl_map_plain_is_universe(map2);
3789
21.8k
  if (intersect < 0 || intersect)
3790
2.10k
    return intersect < 0 ? 
isl_bool_error0
: isl_bool_false;
3791
19.7k
3792
19.7k
  intersect = isl_map_plain_is_equal(map1, map2);
3793
19.7k
  if (intersect < 0 || intersect)
3794
546
    return isl_bool_not(intersect);
3795
19.2k
3796
19.2k
  return isl_map_align_params_map_map_and_test(map1, map2,
3797
19.2k
            &isl_map_is_disjoint_aligned);
3798
19.2k
}
3799
3800
/* Are "bmap1" and "bmap2" disjoint?
3801
 *
3802
 * They are disjoint if they are "obviously disjoint" or if one of them
3803
 * is empty.  Otherwise, they are not disjoint if one of them is universal.
3804
 * If none of these cases apply, we compute the intersection and see if
3805
 * the result is empty.
3806
 */
3807
isl_bool isl_basic_map_is_disjoint(__isl_keep isl_basic_map *bmap1,
3808
  __isl_keep isl_basic_map *bmap2)
3809
30.1k
{
3810
30.1k
  isl_bool disjoint;
3811
30.1k
  isl_bool intersect;
3812
30.1k
  isl_basic_map *test;
3813
30.1k
3814
30.1k
  disjoint = isl_basic_map_plain_is_disjoint(bmap1, bmap2);
3815
30.1k
  if (disjoint < 0 || disjoint)
3816
11.4k
    return disjoint;
3817
18.6k
3818
18.6k
  disjoint = isl_basic_map_is_empty(bmap1);
3819
18.6k
  if (disjoint < 0 || disjoint)
3820
0
    return disjoint;
3821
18.6k
3822
18.6k
  disjoint = isl_basic_map_is_empty(bmap2);
3823
18.6k
  if (disjoint < 0 || disjoint)
3824
0
    return disjoint;
3825
18.6k
3826
18.6k
  intersect = isl_basic_map_plain_is_universe(bmap1);
3827
18.6k
  if (intersect < 0 || intersect)
3828
0
    return intersect < 0 ? isl_bool_error : isl_bool_false;
3829
18.6k
3830
18.6k
  intersect = isl_basic_map_plain_is_universe(bmap2);
3831
18.6k
  if (intersect < 0 || intersect)
3832
0
    return intersect < 0 ? isl_bool_error : isl_bool_false;
3833
18.6k
3834
18.6k
  test = isl_basic_map_intersect(isl_basic_map_copy(bmap1),
3835
18.6k
    isl_basic_map_copy(bmap2));
3836
18.6k
  disjoint = isl_basic_map_is_empty(test);
3837
18.6k
  isl_basic_map_free(test);
3838
18.6k
3839
18.6k
  return disjoint;
3840
18.6k
}
3841
3842
/* Are "bset1" and "bset2" disjoint?
3843
 */
3844
isl_bool isl_basic_set_is_disjoint(__isl_keep isl_basic_set *bset1,
3845
  __isl_keep isl_basic_set *bset2)
3846
21
{
3847
21
  return isl_basic_map_is_disjoint(bset1, bset2);
3848
21
}
3849
3850
isl_bool isl_set_plain_is_disjoint(__isl_keep isl_set *set1,
3851
  __isl_keep isl_set *set2)
3852
0
{
3853
0
  return isl_map_plain_is_disjoint(set_to_map(set1), set_to_map(set2));
3854
0
}
3855
3856
/* Are "set1" and "set2" disjoint?
3857
 */
3858
isl_bool isl_set_is_disjoint(__isl_keep isl_set *set1, __isl_keep isl_set *set2)
3859
16.0k
{
3860
16.0k
  return isl_map_is_disjoint(set1, set2);
3861
16.0k
}
3862
3863
/* Is "v" equal to 0, 1 or -1?
3864
 */
3865
static int is_zero_or_one(isl_int v)
3866
310
{
3867
310
  return isl_int_is_zero(v) || 
isl_int_is_one73
(v) ||
isl_int_is_negone48
(v);
3868
310
}
3869
3870
/* Check if we can combine a given div with lower bound l and upper
3871
 * bound u with some other div and if so return that other div.
3872
 * Otherwise return -1.
3873
 *
3874
 * We first check that
3875
 *  - the bounds are opposites of each other (except for the constant
3876
 *    term)
3877
 *  - the bounds do not reference any other div
3878
 *  - no div is defined in terms of this div
3879
 *
3880
 * Let m be the size of the range allowed on the div by the bounds.
3881
 * That is, the bounds are of the form
3882
 *
3883
 *  e <= a <= e + m - 1
3884
 *
3885
 * with e some expression in the other variables.
3886
 * We look for another div b such that no third div is defined in terms
3887
 * of this second div b and such that in any constraint that contains
3888
 * a (except for the given lower and upper bound), also contains b
3889
 * with a coefficient that is m times that of b.
3890
 * That is, all constraints (except for the lower and upper bound)
3891
 * are of the form
3892
 *
3893
 *  e + f (a + m b) >= 0
3894
 *
3895
 * Furthermore, in the constraints that only contain b, the coefficient
3896
 * of b should be equal to 1 or -1.
3897
 * If so, we return b so that "a + m b" can be replaced by
3898
 * a single div "c = a + m b".
3899
 */
3900
static int div_find_coalesce(struct isl_basic_map *bmap, int *pairs,
3901
  unsigned div, unsigned l, unsigned u)
3902
1.15k
{
3903
1.15k
  int i, j;
3904
1.15k
  unsigned dim;
3905
1.15k
  int coalesce = -1;
3906
1.15k
3907
1.15k
  if (bmap->n_div <= 1)
3908
334
    return -1;
3909
820
  dim = isl_space_dim(bmap->dim, isl_dim_all);
3910
820
  if (isl_seq_first_non_zero(bmap->ineq[l] + 1 + dim, div) != -1)
3911
582
    return -1;
3912
238
  if (isl_seq_first_non_zero(bmap->ineq[l] + 1 + dim + div + 1,
3913
238
           bmap->n_div - div - 1) != -1)
3914
28
    return -1;
3915
210
  if (!isl_seq_is_neg(bmap->ineq[l] + 1, bmap->ineq[u] + 1,
3916
210
          dim + bmap->n_div))
3917
92
    return -1;
3918
118
3919
430
  
for (i = 0; 118
i < bmap->n_div;
++i312
) {
3920
312
    if (isl_int_is_zero(bmap->div[i][0]))
3921
312
      
continue231
;
3922
81
    if (!isl_int_is_zero(bmap->div[i][1 + 1 + dim + div]))
3923
81
      
return -10
;
3924
81
  }
3925
118
3926
118
  isl_int_add(bmap->ineq[l][0], bmap->ineq[l][0], bmap->ineq[u][0]);
3927
118
  if (isl_int_is_neg(bmap->ineq[l][0])) {
3928
0
    isl_int_sub(bmap->ineq[l][0],
3929
0
          bmap->ineq[l][0], bmap->ineq[u][0]);
3930
0
    bmap = isl_basic_map_copy(bmap);
3931
0
    bmap = isl_basic_map_set_to_empty(bmap);
3932
0
    isl_basic_map_free(bmap);
3933
0
    return -1;
3934
0
  }
3935
118
  isl_int_add_ui(bmap->ineq[l][0], bmap->ineq[l][0], 1);
3936
420
  for (i = 0; i < bmap->n_div; 
++i302
) {
3937
307
    if (i == div)
3938
113
      continue;
3939
194
    if (!pairs[i])
3940
103
      continue;
3941
415
    
for (j = 0; 91
j < bmap->n_div;
++j324
) {
3942
324
      if (isl_int_is_zero(bmap->div[j][0]))
3943
324
        
continue231
;
3944
93
      if (!isl_int_is_zero(bmap->div[j][1 + 1 + dim + i]))
3945
93
        
break0
;
3946
93
    }
3947
91
    if (j < bmap->n_div)
3948
0
      continue;
3949
490
    
for (j = 0; 91
j < bmap->n_ineq;
++j399
) {
3950
485
      int valid;
3951
485
      if (j == l || 
j == u434
)
3952
97
        continue;
3953
388
      if (isl_int_is_zero(bmap->ineq[j][1 + dim + div])) {
3954
310
        if (is_zero_or_one(bmap->ineq[j][1 + dim + i]))
3955
286
          continue;
3956
24
        break;
3957
24
      }
3958
78
      if (isl_int_is_zero(bmap->ineq[j][1 + dim + i]))
3959
78
        
break43
;
3960
35
      isl_int_mul(bmap->ineq[j][1 + dim + div],
3961
35
            bmap->ineq[j][1 + dim + div],
3962
35
            bmap->ineq[l][0]);
3963
35
      valid = isl_int_eq(bmap->ineq[j][1 + dim + div],
3964
35
             bmap->ineq[j][1 + dim + i]);
3965
35
      isl_int_divexact(bmap->ineq[j][1 + dim + div],
3966
35
           bmap->ineq[j][1 + dim + div],
3967
35
           bmap->ineq[l][0]);
3968
35
      if (!valid)
3969
19
        break;
3970
35
    }
3971
91
    if (j < bmap->n_ineq)
3972
86
      continue;
3973
5
    coalesce = i;
3974
5
    break;
3975
5
  }
3976
118
  isl_int_sub_ui(bmap->ineq[l][0], bmap->ineq[l][0], 1);
3977
118
  isl_int_sub(bmap->ineq[l][0], bmap->ineq[l][0], bmap->ineq[u][0]);
3978
118
  return coalesce;
3979
118
}
3980
3981
/* Internal data structure used during the construction and/or evaluation of
3982
 * an inequality that ensures that a pair of bounds always allows
3983
 * for an integer value.
3984
 *
3985
 * "tab" is the tableau in which the inequality is evaluated.  It may
3986
 * be NULL until it is actually needed.
3987
 * "v" contains the inequality coefficients.
3988
 * "g", "fl" and "fu" are temporary scalars used during the construction and
3989
 * evaluation.
3990
 */
3991
struct test_ineq_data {
3992
  struct isl_tab *tab;
3993
  isl_vec *v;
3994
  isl_int g;
3995
  isl_int fl;
3996
  isl_int fu;
3997
};
3998
3999
/* Free all the memory allocated by the fields of "data".
4000
 */
4001
static void test_ineq_data_clear(struct test_ineq_data *data)
4002
1.95k
{
4003
1.95k
  isl_tab_free(data->tab);
4004
1.95k
  isl_vec_free(data->v);
4005
1.95k
  isl_int_clear(data->g);
4006
1.95k
  isl_int_clear(data->fl);
4007
1.95k
  isl_int_clear(data->fu);
4008
1.95k
}
4009
4010
/* Is the inequality stored in data->v satisfied by "bmap"?
4011
 * That is, does it only attain non-negative values?
4012
 * data->tab is a tableau corresponding to "bmap".
4013
 */
4014
static isl_bool test_ineq_is_satisfied(__isl_keep isl_basic_map *bmap,
4015
  struct test_ineq_data *data)
4016
1.91k
{
4017
1.91k
  isl_ctx *ctx;
4018
1.91k
  enum isl_lp_result res;
4019
1.91k
4020
1.91k
  ctx = isl_basic_map_get_ctx(bmap);
4021
1.91k
  if (!data->tab)
4022
1.46k
    data->tab = isl_tab_from_basic_map(bmap, 0);
4023
1.91k
  res = isl_tab_min(data->tab, data->v->el, ctx->one, &data->g, NULL, 0);
4024
1.91k
  if (res == isl_lp_error)
4025
0
    return isl_bool_error;
4026
1.91k
  return res == isl_lp_ok && 
isl_int_is_nonneg1.90k
(data->g);
4027
1.91k
}
4028
4029
/* Given a lower and an upper bound on div i, do they always allow
4030
 * for an integer value of the given div?
4031
 * Determine this property by constructing an inequality
4032
 * such that the property is guaranteed when the inequality is nonnegative.
4033
 * The lower bound is inequality l, while the upper bound is inequality u.
4034
 * The constructed inequality is stored in data->v.
4035
 *
4036
 * Let the upper bound be
4037
 *
4038
 *  -n_u a + e_u >= 0
4039
 *
4040
 * and the lower bound
4041
 *
4042
 *  n_l a + e_l >= 0
4043
 *
4044
 * Let n_u = f_u g and n_l = f_l g, with g = gcd(n_u, n_l).
4045
 * We have
4046
 *
4047
 *  - f_u e_l <= f_u f_l g a <= f_l e_u
4048
 *
4049
 * Since all variables are integer valued, this is equivalent to
4050
 *
4051
 *  - f_u e_l - (f_u - 1) <= f_u f_l g a <= f_l e_u + (f_l - 1)
4052
 *
4053
 * If this interval is at least f_u f_l g, then it contains at least
4054
 * one integer value for a.
4055
 * That is, the test constraint is
4056
 *
4057
 *  f_l e_u + f_u e_l + f_l - 1 + f_u - 1 + 1 >= f_u f_l g
4058
 *
4059
 * or
4060
 *
4061
 *  f_l e_u + f_u e_l + f_l - 1 + f_u - 1 + 1 - f_u f_l g >= 0
4062
 *
4063
 * If the coefficients of f_l e_u + f_u e_l have a common divisor g',
4064
 * then the constraint can be scaled down by a factor g',
4065
 * with the constant term replaced by
4066
 * floor((f_l e_{u,0} + f_u e_{l,0} + f_l - 1 + f_u - 1 + 1 - f_u f_l g)/g').
4067
 * Note that the result of applying Fourier-Motzkin to this pair
4068
 * of constraints is
4069
 *
4070
 *  f_l e_u + f_u e_l >= 0
4071
 *
4072
 * If the constant term of the scaled down version of this constraint,
4073
 * i.e., floor((f_l e_{u,0} + f_u e_{l,0})/g') is equal to the constant
4074
 * term of the scaled down test constraint, then the test constraint
4075
 * is known to hold and no explicit evaluation is required.
4076
 * This is essentially the Omega test.
4077
 *
4078
 * If the test constraint consists of only a constant term, then
4079
 * it is sufficient to look at the sign of this constant term.
4080
 */
4081
static isl_bool int_between_bounds(__isl_keep isl_basic_map *bmap, int i,
4082
  int l, int u, struct test_ineq_data *data)
4083
3.89k
{
4084
3.89k
  unsigned offset, n_div;
4085
3.89k
  offset = isl_basic_map_offset(bmap, isl_dim_div);
4086
3.89k
  n_div = isl_basic_map_dim(bmap, isl_dim_div);
4087
3.89k
4088
3.89k
  isl_int_gcd(data->g,
4089
3.89k
        bmap->ineq[l][offset + i], bmap->ineq[u][offset + i]);
4090
3.89k
  isl_int_divexact(data->fl, bmap->ineq[l][offset + i], data->g);
4091
3.89k
  isl_int_divexact(data->fu, bmap->ineq[u][offset + i], data->g);
4092
3.89k
  isl_int_neg(data->fu, data->fu);
4093
3.89k
  isl_seq_combine(data->v->el, data->fl, bmap->ineq[u],
4094
3.89k
      data->fu, bmap->ineq[l], offset + n_div);
4095
3.89k
  isl_int_mul(data->g, data->g, data->fl);
4096
3.89k
  isl_int_mul(data->g, data->g, data->fu);
4097
3.89k
  isl_int_sub(data->g, data->g, data->fl);
4098
3.89k
  isl_int_sub(data->g, data->g, data->fu);
4099
3.89k
  isl_int_add_ui(data->g, data->g, 1);
4100
3.89k
  isl_int_sub(data->fl, data->v->el[0], data->g);
4101
3.89k
4102
3.89k
  isl_seq_gcd(data->v->el + 1, offset - 1 + n_div, &data->g);
4103
3.89k
  if (isl_int_is_zero(data->g))
4104
3.89k
    
return 1.18k
isl_int_is_nonneg1.18k
(data->fl);
4105
2.70k
  if (isl_int_is_one(data->g)) {
4106
1.56k
    isl_int_set(data->v->el[0], data->fl);
4107
1.56k
    return test_ineq_is_satisfied(bmap, data);
4108
1.56k
  }
4109
1.14k
  isl_int_fdiv_q(data->fl, data->fl, data->g);
4110
1.14k
  isl_int_fdiv_q(data->v->el[0], data->v->el[0], data->g);
4111
1.14k
  if (isl_int_eq(data->fl, data->v->el[0]))
4112
1.14k
    
return isl_bool_true795
;
4113
353
  isl_int_set(data->v->el[0], data->fl);
4114
353
  isl_seq_scale_down(data->v->el + 1, data->v->el + 1, data->g,
4115
353
          offset - 1 + n_div);
4116
353
4117
353
  return test_ineq_is_satisfied(bmap, data);
4118
353
}
4119
4120
/* Remove more kinds of divs that are not strictly needed.
4121
 * In particular, if all pairs of lower and upper bounds on a div
4122
 * are such that they allow at least one integer value of the div,
4123
 * then we can eliminate the div using Fourier-Motzkin without
4124
 * introducing any spurious solutions.
4125
 *
4126
 * If at least one of the two constraints has a unit coefficient for the div,
4127
 * then the presence of such a value is guaranteed so there is no need to check.
4128
 * In particular, the value attained by the bound with unit coefficient
4129
 * can serve as this intermediate value.
4130
 */
4131
static __isl_give isl_basic_map *drop_more_redundant_divs(
4132
  __isl_take isl_basic_map *bmap, __isl_take int *pairs, int n)
4133
1.95k
{
4134
1.95k
  isl_ctx *ctx;
4135
1.95k
  struct test_ineq_data data = { NULL, NULL };
4136
1.95k
  unsigned off, n_div;
4137
1.95k
  int remove = -1;
4138
1.95k
4139
1.95k
  isl_int_init(data.g);
4140
1.95k
  isl_int_init(data.fl);
4141
1.95k
  isl_int_init(data.fu);
4142
1.95k
4143
1.95k
  if (!bmap)
4144
0
    goto error;
4145
1.95k
4146
1.95k
  ctx = isl_basic_map_get_ctx(bmap);
4147
1.95k
  off = isl_basic_map_offset(bmap, isl_dim_div);
4148
1.95k
  n_div = isl_basic_map_dim(bmap, isl_dim_div);
4149
1.95k
  data.v = isl_vec_alloc(ctx, off + n_div);
4150
1.95k
  if (!data.v)
4151
0
    goto error;
4152
1.95k
4153
3.69k
  
while (1.95k
n > 0) {
4154
2.46k
    int i, l, u;
4155
2.46k
    int best = -1;
4156
2.46k
    isl_bool has_int;
4157
2.46k
4158
8.98k
    for (i = 0; i < n_div; 
++i6.51k
) {
4159
6.51k
      if (!pairs[i])
4160
3.27k
        continue;
4161
3.24k
      if (best >= 0 && 
pairs[best] <= pairs[i]774
)
4162
588
        continue;
4163
2.65k
      best = i;
4164
2.65k
    }
4165
2.46k
4166
2.46k
    i = best;
4167
19.2k
    for (l = 0; l < bmap->n_ineq; 
++l16.8k
) {
4168
18.5k
      if (!isl_int_is_pos(bmap->ineq[l][off + i]))
4169
18.5k
        
continue14.9k
;
4170
3.65k
      if (isl_int_is_one(bmap->ineq[l][off + i]))
4171
3.65k
        
continue850
;
4172
25.9k
      
for (u = 0; 2.80k
u < bmap->n_ineq;
++u23.1k
) {
4173
24.8k
        if (!isl_int_is_neg(bmap->ineq[u][off + i]))
4174
24.8k
          
continue20.0k
;
4175
4.80k
        if (isl_int_is_negone(bmap->ineq[u][off + i]))
4176
4.80k
          
continue912
;
4177
3.89k
        has_int = int_between_bounds(bmap, i, l, u,
4178
3.89k
                &data);
4179
3.89k
        if (has_int < 0)
4180
0
          goto error;
4181
3.89k
        if (data.tab && 
data.tab->empty2.98k
)
4182
7
          break;
4183
3.88k
        if (!has_int)
4184
1.74k
          break;
4185
3.88k
      }
4186
2.80k
      if (u < bmap->n_ineq)
4187
1.74k
        break;
4188
2.80k
    }
4189
2.46k
    if (data.tab && 
data.tab->empty1.96k
) {
4190
7
      bmap = isl_basic_map_set_to_empty(bmap);
4191
7
      break;
4192
7
    }
4193
2.46k
    if (l == bmap->n_ineq) {
4194
721
      remove = i;
4195
721
      break;
4196
721
    }
4197
1.74k
    pairs[i] = 0;
4198
1.74k
    --n;
4199
1.74k
  }
4200
1.95k
4201
1.95k
  test_ineq_data_clear(&data);
4202
1.95k
4203
1.95k
  free(pairs);
4204
1.95k
4205
1.95k
  if (remove < 0)
4206
1.22k
    return bmap;
4207
721
4208
721
  bmap = isl_basic_map_remove_dims(bmap, isl_dim_div, remove, 1);
4209
721
  return isl_basic_map_drop_redundant_divs(bmap);
4210
0
error:
4211
0
  free(pairs);
4212
0
  isl_basic_map_free(bmap);
4213
0
  test_ineq_data_clear(&data);
4214
0
  return NULL;
4215
721
}
4216
4217
/* Given a pair of divs div1 and div2 such that, except for the lower bound l
4218
 * and the upper bound u, div1 always occurs together with div2 in the form
4219
 * (div1 + m div2), where m is the constant range on the variable div1
4220
 * allowed by l and u, replace the pair div1 and div2 by a single
4221
 * div that is equal to div1 + m div2.
4222
 *
4223
 * The new div will appear in the location that contains div2.
4224
 * We need to modify all constraints that contain
4225
 * div2 = (div - div1) / m
4226
 * The coefficient of div2 is known to be equal to 1 or -1.
4227
 * (If a constraint does not contain div2, it will also not contain div1.)
4228
 * If the constraint also contains div1, then we know they appear
4229
 * as f (div1 + m div2) and we can simply replace (div1 + m div2) by div,
4230
 * i.e., the coefficient of div is f.
4231
 *
4232
 * Otherwise, we first need to introduce div1 into the constraint.
4233
 * Let l be
4234
 *
4235
 *  div1 + f >=0
4236
 *
4237
 * and u
4238
 *
4239
 *  -div1 + f' >= 0
4240
 *
4241
 * A lower bound on div2
4242
 *
4243
 *  div2 + t >= 0
4244
 *
4245
 * can be replaced by
4246
 *
4247
 *  m div2 + div1 + m t + f >= 0
4248
 *
4249
 * An upper bound
4250
 *
4251
 *  -div2 + t >= 0
4252
 *
4253
 * can be replaced by
4254
 *
4255
 *  -(m div2 + div1) + m t + f' >= 0
4256
 *
4257
 * These constraint are those that we would obtain from eliminating
4258
 * div1 using Fourier-Motzkin.
4259
 *
4260
 * After all constraints have been modified, we drop the lower and upper
4261
 * bound and then drop div1.
4262
 * Since the new div is only placed in the same location that used
4263
 * to store div2, but otherwise has a different meaning, any possible
4264
 * explicit representation of the original div2 is removed.
4265
 */
4266
static __isl_give isl_basic_map *coalesce_divs(__isl_take isl_basic_map *bmap,
4267
  unsigned div1, unsigned div2, unsigned l, unsigned u)
4268
5
{
4269
5
  isl_ctx *ctx;
4270
5
  isl_int m;
4271
5
  unsigned dim, total;
4272
5
  int i;
4273
5
4274
5
  ctx = isl_basic_map_get_ctx(bmap);
4275
5
4276
5
  dim = isl_space_dim(bmap->dim, isl_dim_all);
4277
5
  total = 1 + dim + bmap->n_div;
4278
5
4279
5
  isl_int_init(m);
4280
5
  isl_int_add(m, bmap->ineq[l][0], bmap->ineq[u][0]);
4281
5
  isl_int_add_ui(m, m, 1);
4282
5
4283
72
  for (i = 0; i < bmap->n_ineq; 
++i67
) {
4284
67
    if (i == l || 
i == u62
)
4285
10
      continue;
4286
57
    if (isl_int_is_zero(bmap->ineq[i][1 + dim + div2]))
4287
57
      
continue40
;
4288
17
    if (isl_int_is_zero(bmap->ineq[i][1 + dim + div1])) {
4289
3
      if (isl_int_is_pos(bmap->ineq[i][1 + dim + div2]))
4290
3
        isl_seq_combine(bmap->ineq[i], m, bmap->ineq[i],
4291
2
            ctx->one, bmap->ineq[l], total);
4292
1
      else
4293
1
        isl_seq_combine(bmap->ineq[i], m, bmap->ineq[i],
4294
1
            ctx->one, bmap->ineq[u], total);
4295
3
    }
4296
17
    isl_int_set(bmap->ineq[i][1 + dim + div2],
4297
17
          bmap->ineq[i][1 + dim + div1]);
4298
17
    isl_int_set_si(bmap->ineq[i][1 + dim + div1], 0);
4299
17
  }
4300
5
4301
5
  isl_int_clear(m);
4302
5
  if (l > u) {
4303
0
    isl_basic_map_drop_inequality(bmap, l);
4304
0
    isl_basic_map_drop_inequality(bmap, u);
4305
5
  } else {
4306
5
    isl_basic_map_drop_inequality(bmap, u);
4307
5
    isl_basic_map_drop_inequality(bmap, l);
4308
5
  }
4309
5
  bmap = isl_basic_map_mark_div_unknown(bmap, div2);
4310
5
  bmap = isl_basic_map_drop_div(bmap, div1);
4311
5
  return bmap;
4312
5
}
4313
4314
/* First check if we can coalesce any pair of divs and
4315
 * then continue with dropping more redundant divs.
4316
 *
4317
 * We loop over all pairs of lower and upper bounds on a div
4318
 * with coefficient 1 and -1, respectively, check if there
4319
 * is any other div "c" with which we can coalesce the div
4320
 * and if so, perform the coalescing.
4321
 */
4322
static __isl_give isl_basic_map *coalesce_or_drop_more_redundant_divs(
4323
  __isl_take isl_basic_map *bmap, int *pairs, int n)
4324
1.95k
{
4325
1.95k
  int i, l, u;
4326
1.95k
  unsigned dim;
4327
1.95k
4328
1.95k
  dim = isl_space_dim(bmap->dim, isl_dim_all);
4329
1.95k
4330
6.54k
  for (i = 0; i < bmap->n_div; 
++i4.58k
) {
4331
4.59k
    if (!pairs[i])
4332
2.00k
      continue;
4333
32.9k
    
for (l = 0; 2.58k
l < bmap->n_ineq;
++l30.3k
) {
4334
30.3k
      if (!isl_int_is_one(bmap->ineq[l][1 + dim + i]))
4335
30.3k
        
continue29.2k
;
4336
13.3k
      
for (u = 0; 1.16k
u < bmap->n_ineq;
++u12.1k
) {
4337
12.1k
        int c;
4338
12.1k
4339
12.1k
        if (!isl_int_is_negone(bmap->ineq[u][1+dim+i]))
4340
12.1k
          
continue11.0k
;
4341
1.15k
        c = div_find_coalesce(bmap, pairs, i, l, u);
4342
1.15k
        if (c < 0)
4343
1.14k
          continue;
4344
5
        free(pairs);
4345
5
        bmap = coalesce_divs(bmap, i, c, l, u);
4346
5
        return isl_basic_map_drop_redundant_divs(bmap);
4347
5
      }
4348
1.16k
    }
4349
2.58k
  }
4350
1.95k
4351
1.95k
  
if (1.95k
ISL_F_ISSET1.95k
(bmap, ISL_BASIC_MAP_EMPTY)) {
4352
0
    free(pairs);
4353
0
    return bmap;
4354
0
  }
4355
1.95k
4356
1.95k
  return drop_more_redundant_divs(bmap, pairs, n);
4357
1.95k
}
4358
4359
/* Are the "n" coefficients starting at "first" of inequality constraints
4360
 * "i" and "j" of "bmap" equal to each other?
4361
 */
4362
static int is_parallel_part(__isl_keep isl_basic_map *bmap, int i, int j,
4363
  int first, int n)
4364
522
{
4365
522
  return isl_seq_eq(bmap->ineq[i] + first, bmap->ineq[j] + first, n);
4366
522
}
4367
4368
/* Are the "n" coefficients starting at "first" of inequality constraints
4369
 * "i" and "j" of "bmap" opposite to each other?
4370
 */
4371
static int is_opposite_part(__isl_keep isl_basic_map *bmap, int i, int j,
4372
  int first, int n)
4373
5.69k
{
4374
5.69k
  return isl_seq_is_neg(bmap->ineq[i] + first, bmap->ineq[j] + first, n);
4375
5.69k
}
4376
4377
/* Are inequality constraints "i" and "j" of "bmap" opposite to each other,
4378
 * apart from the constant term?
4379
 */
4380
static isl_bool is_opposite(__isl_keep isl_basic_map *bmap, int i, int j)
4381
5.11k
{
4382
5.11k
  unsigned total;
4383
5.11k
4384
5.11k
  total = isl_basic_map_dim(bmap, isl_dim_all);
4385
5.11k
  return is_opposite_part(bmap, i, j, 1, total);
4386
5.11k
}
4387
4388
/* Are inequality constraints "i" and "j" of "bmap" equal to each other,
4389
 * apart from the constant term and the coefficient at position "pos"?
4390
 */
4391
static int is_parallel_except(__isl_keep isl_basic_map *bmap, int i, int j,
4392
  int pos)
4393
499
{
4394
499
  unsigned total;
4395
499
4396
499
  total = isl_basic_map_dim(bmap, isl_dim_all);
4397
499
  return is_parallel_part(bmap, i, j, 1, pos - 1) &&
4398
499
    
is_parallel_part(bmap, i, j, pos + 1, total - pos)23
;
4399
499
}
4400
4401
/* Are inequality constraints "i" and "j" of "bmap" opposite to each other,
4402
 * apart from the constant term and the coefficient at position "pos"?
4403
 */
4404
static int is_opposite_except(__isl_keep isl_basic_map *bmap, int i, int j,
4405
  int pos)
4406
487
{
4407
487
  unsigned total;
4408
487
4409
487
  total = isl_basic_map_dim(bmap, isl_dim_all);
4410
487
  return is_opposite_part(bmap, i, j, 1, pos - 1) &&
4411
487
    
is_opposite_part(bmap, i, j, pos + 1, total - pos)93
;
4412
487
}
4413
4414
/* Restart isl_basic_map_drop_redundant_divs after "bmap" has
4415
 * been modified, simplying it if "simplify" is set.
4416
 * Free the temporary data structure "pairs" that was associated
4417
 * to the old version of "bmap".
4418
 */
4419
static __isl_give isl_basic_map *drop_redundant_divs_again(
4420
  __isl_take isl_basic_map *bmap, __isl_take int *pairs, int simplify)
4421
4.61k
{
4422
4.61k
  if (simplify)
4423
1.57k
    bmap = isl_basic_map_simplify(bmap);
4424
4.61k
  free(pairs);
4425
4.61k
  return isl_basic_map_drop_redundant_divs(bmap);
4426
4.61k
}
4427
4428
/* Is "div" the single unknown existentially quantified variable
4429
 * in inequality constraint "ineq" of "bmap"?
4430
 * "div" is known to have a non-zero coefficient in "ineq".
4431
 */
4432
static isl_bool single_unknown(__isl_keep isl_basic_map *bmap, int ineq,
4433
  int div)
4434
2.04k
{
4435
2.04k
  int i;
4436
2.04k
  unsigned n_div, o_div;
4437
2.04k
  isl_bool known;
4438
2.04k
4439
2.04k
  known = isl_basic_map_div_is_known(bmap, div);
4440
2.04k
  if (known < 0 || known)
4441
258
    return isl_bool_not(known);
4442
1.78k
  n_div = isl_basic_map_dim(bmap, isl_dim_div);
4443
1.78k
  if (n_div == 1)
4444
1.12k
    return isl_bool_true;
4445
660
  o_div = isl_basic_map_offset(bmap, isl_dim_div);
4446
2.28k
  for (i = 0; i < n_div; 
++i1.62k
) {
4447
1.66k
    isl_bool known;
4448
1.66k
4449
1.66k
    if (i == div)
4450
641
      continue;
4451
1.02k
    if (isl_int_is_zero(bmap->ineq[ineq][o_div + i]))
4452
1.02k
      
continue950
;
4453
71
    known = isl_basic_map_div_is_known(bmap, i);
4454
71
    if (known < 0 || !known)
4455
40
      return known;
4456
71
  }
4457
660
4458
660
  
return isl_bool_true620
;
4459
660
}
4460
4461
/* Does integer division "div" have coefficient 1 in inequality constraint
4462
 * "ineq" of "map"?
4463
 */
4464
static isl_bool has_coef_one(__isl_keep isl_basic_map *bmap, int div, int ineq)
4465
1.74k
{
4466
1.74k
  unsigned o_div;
4467
1.74k
4468
1.74k
  o_div = isl_basic_map_offset(bmap, isl_dim_div);
4469
1.74k
  if (isl_int_is_one(bmap->ineq[ineq][o_div + div]))
4470
1.74k
    
return isl_bool_true1.57k
;
4471
171
4472
171
  return isl_bool_false;
4473
171
}
4474
4475
/* Turn inequality constraint "ineq" of "bmap" into an equality and
4476
 * then try and drop redundant divs again,
4477
 * freeing the temporary data structure "pairs" that was associated
4478
 * to the old version of "bmap".
4479
 */
4480
static __isl_give isl_basic_map *set_eq_and_try_again(
4481
  __isl_take isl_basic_map *bmap, int ineq, __isl_take int *pairs)
4482
1.57k
{
4483
1.57k
  bmap = isl_basic_map_cow(bmap);
4484
1.57k
  isl_basic_map_inequality_to_equality(bmap, ineq);
4485
1.57k
  return drop_redundant_divs_again(bmap, pairs, 1);
4486
1.57k
}
4487
4488
/* Drop the integer division at position "div", along with the two
4489
 * inequality constraints "ineq1" and "ineq2" in which it appears
4490
 * from "bmap" and then try and drop redundant divs again,
4491
 * freeing the temporary data structure "pairs" that was associated
4492
 * to the old version of "bmap".
4493
 */
4494
static __isl_give isl_basic_map *drop_div_and_try_again(
4495
  __isl_take isl_basic_map *bmap, int div, int ineq1, int ineq2,
4496
  __isl_take int *pairs)
4497
1.27k
{
4498
1.27k
  if (ineq1 > ineq2) {
4499
590
    isl_basic_map_drop_inequality(bmap, ineq1);
4500
590
    isl_basic_map_drop_inequality(bmap, ineq2);
4501
685
  } else {
4502
685
    isl_basic_map_drop_inequality(bmap, ineq2);
4503
685
    isl_basic_map_drop_inequality(bmap, ineq1);
4504
685
  }
4505
1.27k
  bmap = isl_basic_map_drop_div(bmap, div);
4506
1.27k
  return drop_redundant_divs_again(bmap, pairs, 0);
4507
1.27k
}
4508
4509
/* Given two inequality constraints
4510
 *
4511
 *  f(x) + n d + c >= 0,    (ineq)
4512
 *
4513
 * with d the variable at position "pos", and
4514
 *
4515
 *  f(x) + c0 >= 0,     (lower)
4516
 *
4517
 * compute the maximal value of the lower bound ceil((-f(x) - c)/n)
4518
 * determined by the first constraint.
4519
 * That is, store
4520
 *
4521
 *  ceil((c0 - c)/n)
4522
 *
4523
 * in *l.
4524
 */
4525
static void lower_bound_from_parallel(__isl_keep isl_basic_map *bmap,
4526
  int ineq, int lower, int pos, isl_int *l)
4527
24
{
4528
24
  isl_int_neg(*l, bmap->ineq[ineq][0]);
4529
24
  isl_int_add(*l, *l, bmap->ineq[lower][0]);
4530
24
  isl_int_cdiv_q(*l, *l, bmap->ineq[ineq][pos]);
4531
24
}
4532
4533
/* Given two inequality constraints
4534
 *
4535
 *  f(x) + n d + c >= 0,    (ineq)
4536
 *
4537
 * with d the variable at position "pos", and
4538
 *
4539
 *  -f(x) - c0 >= 0,    (upper)
4540
 *
4541
 * compute the minimal value of the lower bound ceil((-f(x) - c)/n)
4542
 * determined by the first constraint.
4543
 * That is, store
4544
 *
4545
 *  ceil((-c1 - c)/n)
4546
 *
4547
 * in *u.
4548
 */
4549
static void lower_bound_from_opposite(__isl_keep isl_basic_map *bmap,
4550
  int ineq, int upper, int pos, isl_int *u)
4551
17
{
4552
17
  isl_int_neg(*u, bmap->ineq[ineq][0]);
4553
17
  isl_int_sub(*u, *u, bmap->ineq[upper][0]);
4554
17
  isl_int_cdiv_q(*u, *u, bmap->ineq[ineq][pos]);
4555
17
}
4556
4557
/* Given a lower bound constraint "ineq" on "div" in "bmap",
4558
 * does the corresponding lower bound have a fixed value in "bmap"?
4559
 *
4560
 * In particular, "ineq" is of the form
4561
 *
4562
 *  f(x) + n d + c >= 0
4563
 *
4564
 * with n > 0, c the constant term and
4565
 * d the existentially quantified variable "div".
4566
 * That is, the lower bound is
4567
 *
4568
 *  ceil((-f(x) - c)/n)
4569
 *
4570
 * Look for a pair of constraints
4571
 *
4572
 *  f(x) + c0 >= 0
4573
 *  -f(x) + c1 >= 0
4574
 *
4575
 * i.e., -c1 <= -f(x) <= c0, that fix ceil((-f(x) - c)/n) to a constant value.
4576
 * That is, check that
4577
 *
4578
 *  ceil((-c1 - c)/n) = ceil((c0 - c)/n)
4579
 *
4580
 * If so, return the index of inequality f(x) + c0 >= 0.
4581
 * Otherwise, return -1.
4582
 */
4583
static int lower_bound_is_cst(__isl_keep isl_basic_map *bmap, int div, int ineq)
4584
171
{
4585
171
  int i;
4586
171
  int lower = -1, upper = -1;
4587
171
  unsigned o_div;
4588
171
  isl_int l, u;
4589
171
  int equal;
4590
171
4591
171
  o_div = isl_basic_map_offset(bmap, isl_dim_div);
4592
1.07k
  for (i = 0; i < bmap->n_ineq && 
(914
lower < 0914
||
upper < 055
);
++i899
) {
4593
899
    if (i == ineq)
4594
156
      continue;
4595
743
    if (!isl_int_is_zero(bmap->ineq[i][o_div + div]))
4596
743
      
continue217
;
4597
526
    if (lower < 0 &&
4598
526
        
is_parallel_except(bmap, ineq, i, o_div + div)499
) {
4599
22
      lower = i;
4600
22
      continue;
4601
22
    }
4602
504
    if (upper < 0 &&
4603
504
        
is_opposite_except(bmap, ineq, i, o_div + div)487
) {
4604
92
      upper = i;
4605
92
    }
4606
504
  }
4607
171
4608
171
  if (lower < 0 || 
upper < 022
)
4609
154
    return -1;
4610
17
4611
17
  isl_int_init(l);
4612
17
  isl_int_init(u);
4613
17
4614
17
  lower_bound_from_parallel(bmap, ineq, lower, o_div + div, &l);
4615
17
  lower_bound_from_opposite(bmap, ineq, upper, o_div + div, &u);
4616
17
4617
17
  equal = isl_int_eq(l, u);
4618
17
4619
17
  isl_int_clear(l);
4620
17
  isl_int_clear(u);
4621
17
4622
17
  return equal ? 
lower7
:
-110
;
4623
17
}
4624
4625
/* Given a lower bound constraint "ineq" on the existentially quantified
4626
 * variable "div", such that the corresponding lower bound has
4627
 * a fixed value in "bmap", assign this fixed value to the variable and
4628
 * then try and drop redundant divs again,
4629
 * freeing the temporary data structure "pairs" that was associated
4630
 * to the old version of "bmap".
4631
 * "lower" determines the constant value for the lower bound.
4632
 *
4633
 * In particular, "ineq" is of the form
4634
 *
4635
 *  f(x) + n d + c >= 0,
4636
 *
4637
 * while "lower" is of the form
4638
 *
4639
 *  f(x) + c0 >= 0
4640
 *
4641
 * The lower bound is ceil((-f(x) - c)/n) and its constant value
4642
 * is ceil((c0 - c)/n).
4643
 */
4644
static __isl_give isl_basic_map *fix_cst_lower(__isl_take isl_basic_map *bmap,
4645
  int div, int ineq, int lower, int *pairs)
4646
7
{
4647
7
  isl_int c;
4648
7
  unsigned o_div;
4649
7
4650
7
  isl_int_init(c);
4651
7
4652
7
  o_div = isl_basic_map_offset(bmap, isl_dim_div);
4653
7
  lower_bound_from_parallel(bmap, ineq, lower, o_div + div, &c);
4654
7
  bmap = isl_basic_map_fix(bmap, isl_dim_div, div, c);
4655
7
  free(pairs);
4656
7
4657
7
  isl_int_clear(c);
4658
7
4659
7
  return isl_basic_map_drop_redundant_divs(bmap);
4660
7
}
4661
4662
/* Remove divs that are not strictly needed based on the inequality
4663
 * constraints.
4664
 * In particular, if a div only occurs positively (or negatively)
4665
 * in constraints, then it can simply be dropped.
4666
 * Also, if a div occurs in only two constraints and if moreover
4667
 * those two constraints are opposite to each other, except for the constant
4668
 * term and if the sum of the constant terms is such that for any value
4669
 * of the other values, there is always at least one integer value of the
4670
 * div, i.e., if one plus this sum is greater than or equal to
4671
 * the (absolute value) of the coefficient of the div in the constraints,
4672
 * then we can also simply drop the div.
4673
 *
4674
 * If an existentially quantified variable does not have an explicit
4675
 * representation, appears in only a single lower bound that does not
4676
 * involve any other such existentially quantified variables and appears
4677
 * in this lower bound with coefficient 1,
4678
 * then fix the variable to the value of the lower bound.  That is,
4679
 * turn the inequality into an equality.
4680
 * If for any value of the other variables, there is any value
4681
 * for the existentially quantified variable satisfying the constraints,
4682
 * then this lower bound also satisfies the constraints.
4683
 * It is therefore safe to pick this lower bound.
4684
 *
4685
 * The same reasoning holds even if the coefficient is not one.
4686
 * However, fixing the variable to the value of the lower bound may
4687
 * in general introduce an extra integer division, in which case
4688
 * it may be better to pick another value.
4689
 * If this integer division has a known constant value, then plugging
4690
 * in this constant value removes the existentially quantified variable
4691
 * completely.  In particular, if the lower bound is of the form
4692
 * ceil((-f(x) - c)/n) and there are two constraints, f(x) + c0 >= 0 and
4693
 * -f(x) + c1 >= 0 such that ceil((-c1 - c)/n) = ceil((c0 - c)/n),
4694
 * then the existentially quantified variable can be assigned this
4695
 * shared value.
4696
 *
4697
 * We skip divs that appear in equalities or in the definition of other divs.
4698
 * Divs that appear in the definition of other divs usually occur in at least
4699
 * 4 constraints, but the constraints may have been simplified.
4700
 *
4701
 * If any divs are left after these simple checks then we move on
4702
 * to more complicated cases in drop_more_redundant_divs.
4703
 */
4704
static __isl_give isl_basic_map *isl_basic_map_drop_redundant_divs_ineq(
4705
  __isl_take isl_basic_map *bmap)
4706
227k
{
4707
227k
  int i, j;
4708
227k
  unsigned off;
4709
227k
  int *pairs = NULL;
4710
227k
  int n = 0;
4711
227k
4712
227k
  if (!bmap)
4713
0
    goto error;
4714
227k
  if (bmap->n_div == 0)
4715
214k
    return bmap;
4716
12.8k
4717
12.8k
  off = isl_space_dim(bmap->dim, isl_dim_all);
4718
12.8k
  pairs = isl_calloc_array(bmap->ctx, int, bmap->n_div);
4719
12.8k
  if (!pairs)
4720
0
    goto error;
4721
12.8k
4722
26.0k
  
for (i = 0; 12.8k
i < bmap->n_div;
++i13.2k
) {
4723
17.8k
    int pos, neg;
4724
17.8k
    int last_pos, last_neg;
4725
17.8k
    int redundant;
4726
17.8k
    int defined;
4727
17.8k
    isl_bool opp, set_div;
4728
17.8k
4729
17.8k
    defined = !isl_int_is_zero(bmap->div[i][0]);
4730
43.5k
    for (j = i; j < bmap->n_div; 
++j25.7k
)
4731
26.8k
      if (!isl_int_is_zero(bmap->div[j][1 + 1 + off + i]))
4732
26.8k
        
break1.10k
;
4733
17.8k
    if (j < bmap->n_div)
4734
1.10k
      continue;
4735
27.1k
    
for (j = 0; 16.7k
j < bmap->n_eq;
++j10.3k
)
4736
17.3k
      if (!isl_int_is_zero(bmap->eq[j][1 + off + i]))
4737
17.3k
        
break6.90k
;
4738
16.7k
    if (j < bmap->n_eq)
4739
6.90k
      continue;
4740
9.82k
    ++n;
4741
9.82k
    pos = neg = 0;
4742
91.3k
    for (j = 0; j < bmap->n_ineq; 
++j81.5k
) {
4743
81.5k
      if (isl_int_is_pos(bmap->ineq[j][1 + off + i])) {
4744
11.3k
        last_pos = j;
4745
11.3k
        ++pos;
4746
11.3k
      }
4747
81.5k
      if (isl_int_is_neg(bmap->ineq[j][1 + off + i])) {
4748
11.3k
        last_neg = j;
4749
11.3k
        ++neg;
4750
11.3k
      }
4751
81.5k
    }
4752
9.82k
    pairs[i] = pos * neg;
4753
9.82k
    if (pairs[i] == 0) {
4754
1.84k
      for (j = bmap->n_ineq - 1; j >= 0; 
--j81
)
4755
81
        if (!isl_int_is_zero(bmap->ineq[j][1+off+i]))
4756
81
          
isl_basic_map_drop_inequality(bmap, j)35
;
4757
1.76k
      bmap = isl_basic_map_drop_div(bmap, i);
4758
1.76k
      return drop_redundant_divs_again(bmap, pairs, 0);
4759
1.76k
    }
4760
8.06k
    if (pairs[i] != 1)
4761
2.94k
      opp = isl_bool_false;
4762
5.11k
    else
4763
5.11k
      opp = is_opposite(bmap, last_pos, last_neg);
4764
8.06k
    if (opp < 0)
4765
0
      goto error;
4766
8.06k
    if (!opp) {
4767
4.43k
      int lower;
4768
4.43k
      isl_bool single, one;
4769
4.43k
4770
4.43k
      if (pos != 1)
4771
2.38k
        continue;
4772
2.04k
      single = single_unknown(bmap, last_pos, i);
4773
2.04k
      if (single < 0)
4774
0
        goto error;
4775
2.04k
      if (!single)
4776
298
        continue;
4777
1.74k
      one = has_coef_one(bmap, i, last_pos);
4778
1.74k
      if (one < 0)
4779
0
        goto error;
4780
1.74k
      if (one)
4781
1.57k
        return set_eq_and_try_again(bmap, last_pos,
4782
1.57k
                  pairs);
4783
171
      lower = lower_bound_is_cst(bmap, i, last_pos);
4784
171
      if (lower >= 0)
4785
7
        return fix_cst_lower(bmap, i, last_pos, lower,
4786
7
            pairs);
4787
164
      continue;
4788
164
    }
4789
3.63k
4790
3.63k
    isl_int_add(bmap->ineq[last_pos][0],
4791
3.63k
          bmap->ineq[last_pos][0], bmap->ineq[last_neg][0]);
4792
3.63k
    isl_int_add_ui(bmap->ineq[last_pos][0],
4793
3.63k
             bmap->ineq[last_pos][0], 1);
4794
3.63k
    redundant = isl_int_ge(bmap->ineq[last_pos][0],
4795
3.63k
        bmap->ineq[last_pos][1+off+i]);
4796
3.63k
    isl_int_sub_ui(bmap->ineq[last_pos][0],
4797
3.63k
             bmap->ineq[last_pos][0], 1);
4798
3.63k
    isl_int_sub(bmap->ineq[last_pos][0],
4799
3.63k
          bmap->ineq[last_pos][0], bmap->ineq[last_neg][0]);
4800
3.63k
    if (redundant)
4801
1.27k
      return drop_div_and_try_again(bmap, i,
4802
1.27k
                last_pos, last_neg, pairs);
4803
2.35k
    if (defined)
4804
2.34k
      set_div = isl_bool_false;
4805
7
    else
4806
7
      set_div = ok_to_set_div_from_bound(bmap, i, last_pos);
4807
2.35k
    if (set_div < 0)
4808
0
      return isl_basic_map_free(bmap);
4809
2.35k
    if (set_div) {
4810
1
      bmap = set_div_from_lower_bound(bmap, i, last_pos);
4811
1
      return drop_redundant_divs_again(bmap, pairs, 1);
4812
1
    }
4813
2.35k
    pairs[i] = 0;
4814
2.35k
    --n;
4815
2.35k
  }
4816
12.8k
4817
12.8k
  
if (8.19k
n > 08.19k
)
4818
1.95k
    return coalesce_or_drop_more_redundant_divs(bmap, pairs, n);
4819
6.24k
4820
6.24k
  free(pairs);
4821
6.24k
  return bmap;
4822
0
error:
4823
0
  free(pairs);
4824
0
  isl_basic_map_free(bmap);
4825
0
  return NULL;
4826
6.24k
}
4827
4828
/* Consider the coefficients at "c" as a row vector and replace
4829
 * them with their product with "T".  "T" is assumed to be a square matrix.
4830
 */
4831
static isl_stat preimage(isl_int *c, __isl_keep isl_mat *T)
4832
22.2k
{
4833
22.2k
  int n;
4834
22.2k
  isl_ctx *ctx;
4835
22.2k
  isl_vec *v;
4836
22.2k
4837
22.2k
  if (!T)
4838
0
    return isl_stat_error;
4839
22.2k
  n = isl_mat_rows(T);
4840
22.2k
  if (isl_seq_first_non_zero(c, n) == -1)
4841
12.4k
    return isl_stat_ok;
4842
9.70k
  ctx = isl_mat_get_ctx(T);
4843
9.70k
  v = isl_vec_alloc(ctx, n);
4844
9.70k
  if (!v)
4845
0
    return isl_stat_error;
4846
9.70k
  isl_seq_swp_or_cpy(v->el, c, n);
4847
9.70k
  v = isl_vec_mat_product(v, isl_mat_copy(T));
4848
9.70k
  if (!v)
4849
0
    return isl_stat_error;
4850
9.70k
  isl_seq_swp_or_cpy(c, v->el, n);
4851
9.70k
  isl_vec_free(v);
4852
9.70k
4853
9.70k
  return isl_stat_ok;
4854
9.70k
}
4855
4856
/* Plug in T for the variables in "bmap" starting at "pos".
4857
 * T is a linear unimodular matrix, i.e., without constant term.
4858
 */
4859
static __isl_give isl_basic_map *isl_basic_map_preimage_vars(
4860
  __isl_take isl_basic_map *bmap, unsigned pos, __isl_take isl_mat *T)
4861
2.09k
{
4862
2.09k
  int i;
4863
2.09k
  unsigned n, total;
4864
2.09k
4865
2.09k
  bmap = isl_basic_map_cow(bmap);
4866
2.09k
  if (!bmap || !T)
4867
0
    goto error;
4868
2.09k
4869
2.09k
  n = isl_mat_cols(T);
4870
2.09k
  if (n != isl_mat_rows(T))
4871
2.09k
    
isl_die0
(isl_mat_get_ctx(T), isl_error_invalid,
4872
2.09k
      "expecting square matrix", goto error);
4873
2.09k
4874
2.09k
  total = isl_basic_map_dim(bmap, isl_dim_all);
4875
2.09k
  if (pos + n > total || pos + n < pos)
4876
2.09k
    
isl_die0
(isl_mat_get_ctx(T), isl_error_invalid,
4877
2.09k
      "invalid range", goto error);
4878
2.09k
4879
5.70k
  
for (i = 0; 2.09k
i < bmap->n_eq;
++i3.60k
)
4880
3.60k
    if (preimage(bmap->eq[i] + 1 + pos, T) < 0)
4881
0
      goto error;
4882
19.8k
  
for (i = 0; 2.09k
i < bmap->n_ineq;
++i17.7k
)
4883
17.7k
    if (preimage(bmap->ineq[i] + 1 + pos, T) < 0)
4884
0
      goto error;
4885
7.92k
  
for (i = 0; 2.09k
i < bmap->n_div;
++i5.83k
) {
4886
5.83k
    if (isl_basic_map_div_is_marked_unknown(bmap, i))
4887
4.95k
      continue;
4888
880
    if (preimage(bmap->div[i] + 1 + 1 + pos, T) < 0)
4889
0
      goto error;
4890
880
  }
4891
2.09k
4892
2.09k
  isl_mat_free(T);
4893
2.09k
  return bmap;
4894
0
error:
4895
0
  isl_basic_map_free(bmap);
4896
0
  isl_mat_free(T);
4897
0
  return NULL;
4898
2.09k
}
4899
4900
/* Remove divs that are not strictly needed.
4901
 *
4902
 * First look for an equality constraint involving two or more
4903
 * existentially quantified variables without an explicit
4904
 * representation.  Replace the combination that appears
4905
 * in the equality constraint by a single existentially quantified
4906
 * variable such that the equality can be used to derive
4907
 * an explicit representation for the variable.
4908
 * If there are no more such equality constraints, then continue
4909
 * with isl_basic_map_drop_redundant_divs_ineq.
4910
 *
4911
 * In particular, if the equality constraint is of the form
4912
 *
4913
 *  f(x) + \sum_i c_i a_i = 0
4914
 *
4915
 * with a_i existentially quantified variable without explicit
4916
 * representation, then apply a transformation on the existentially
4917
 * quantified variables to turn the constraint into
4918
 *
4919
 *  f(x) + g a_1' = 0
4920
 *
4921
 * with g the gcd of the c_i.
4922
 * In order to easily identify which existentially quantified variables
4923
 * have a complete explicit representation, i.e., without being defined
4924
 * in terms of other existentially quantified variables without
4925
 * an explicit representation, the existentially quantified variables
4926
 * are first sorted.
4927
 *
4928
 * The variable transformation is computed by extending the row
4929
 * [c_1/g ... c_n/g] to a unimodular matrix, obtaining the transformation
4930
 *
4931
 *  [a_1']   [c_1/g ... c_n/g]   [ a_1 ]
4932
 *  [a_2']                       [ a_2 ]
4933
 *   ...   =         U             ....
4934
 *  [a_n']                   [ a_n ]
4935
 *
4936
 * with [c_1/g ... c_n/g] representing the first row of U.
4937
 * The inverse of U is then plugged into the original constraints.
4938
 * The call to isl_basic_map_simplify makes sure the explicit
4939
 * representation for a_1' is extracted from the equality constraint.
4940
 */
4941
__isl_give isl_basic_map *isl_basic_map_drop_redundant_divs(
4942
  __isl_take isl_basic_map *bmap)
4943
229k
{
4944
229k
  int first;
4945
229k
  int i;
4946
229k
  unsigned o_div, n_div;
4947
229k
  int l;
4948
229k
  isl_ctx *ctx;
4949
229k
  isl_mat *T;
4950
229k
4951
229k
  if (!bmap)
4952
0
    return NULL;
4953
229k
  if (isl_basic_map_divs_known(bmap))
4954
222k
    return isl_basic_map_drop_redundant_divs_ineq(bmap);
4955
6.83k
  if (bmap->n_eq == 0)
4956
1.67k
    return isl_basic_map_drop_redundant_divs_ineq(bmap);
4957
5.16k
  bmap = isl_basic_map_sort_divs(bmap);
4958
5.16k
  if (!bmap)
4959
0
    return NULL;
4960
5.16k
4961
5.16k
  first = isl_basic_map_first_unknown_div(bmap);
4962
5.16k
  if (first < 0)
4963
0
    return isl_basic_map_free(bmap);
4964
5.16k
4965
5.16k
  o_div = isl_basic_map_offset(bmap, isl_dim_div);
4966
5.16k
  n_div = isl_basic_map_dim(bmap, isl_dim_div);
4967
5.16k
4968
9.14k
  for (i = 0; i < bmap->n_eq; 
++i3.98k
) {
4969
6.07k
    l = isl_seq_first_non_zero(bmap->eq[i] + o_div + first,
4970
6.07k
              n_div - (first));
4971
6.07k
    if (l < 0)
4972
3.98k
      continue;
4973
2.09k
    l += first;
4974
2.09k
    if (isl_seq_first_non_zero(bmap->eq[i] + o_div + l + 1,
4975
2.09k
              n_div - (l + 1)) == -1)
4976
0
      continue;
4977
2.09k
    break;
4978
2.09k
  }
4979
5.16k
  if (i >= bmap->n_eq)
4980
3.06k
    return isl_basic_map_drop_redundant_divs_ineq(bmap);
4981
2.09k
4982
2.09k
  ctx = isl_basic_map_get_ctx(bmap);
4983
2.09k
  T = isl_mat_alloc(ctx, n_div - l, n_div - l);
4984
2.09k
  if (!T)
4985
0
    return isl_basic_map_free(bmap);
4986
2.09k
  isl_seq_cpy(T->row[0], bmap->eq[i] + o_div + l, n_div - l);
4987
2.09k
  T = isl_mat_normalize_row(T, 0);
4988
2.09k
  T = isl_mat_unimodular_complete(T, 1);
4989
2.09k
  T = isl_mat_right_inverse(T);
4990
2.09k
4991
6.99k
  for (i = l; i < n_div; 
++i4.89k
)
4992
4.89k
    bmap = isl_basic_map_mark_div_unknown(bmap, i);
4993
2.09k
  bmap = isl_basic_map_preimage_vars(bmap, o_div - 1 + l, T);
4994
2.09k
  bmap = isl_basic_map_simplify(bmap);
4995
2.09k
4996
2.09k
  return isl_basic_map_drop_redundant_divs(bmap);
4997
2.09k
}
4998
4999
/* Does "bmap" satisfy any equality that involves more than 2 variables
5000
 * and/or has coefficients different from -1 and 1?
5001
 */
5002
static int has_multiple_var_equality(__isl_keep isl_basic_map *bmap)
5003
8.03k
{
5004
8.03k
  int i;
5005
8.03k
  unsigned total;
5006
8.03k
5007
8.03k
  total = isl_basic_map_dim(bmap, isl_dim_all);
5008
8.03k
5009
23.2k
  for (i = 0; i < bmap->n_eq; 
++i15.2k
) {
5010
16.2k
    int j, k;
5011
16.2k
5012
16.2k
    j = isl_seq_first_non_zero(bmap->eq[i] + 1, total);
5013
16.2k
    if (j < 0)
5014
0
      continue;
5015
16.2k
    if (!isl_int_is_one(bmap->eq[i][1 + j]) &&
5016
16.2k
        
!6.09k
isl_int_is_negone6.09k
(bmap->eq[i][1 + j]))
5017
16.2k
      
return 1323
;
5018
15.9k
5019
15.9k
    j += 1;
5020
15.9k
    k = isl_seq_first_non_zero(bmap->eq[i] + 1 + j, total - j);
5021
15.9k
    if (k < 0)
5022
9.96k
      continue;
5023
5.99k
    j += k;
5024
5.99k
    if (!isl_int_is_one(bmap->eq[i][1 + j]) &&
5025
5.99k
        
!627
isl_int_is_negone627
(bmap->eq[i][1 + j]))
5026
5.99k
      
return 1370
;
5027
5.62k
5028
5.62k
    j += 1;
5029
5.62k
    k = isl_seq_first_non_zero(bmap->eq[i] + 1 + j, total - j);
5030
5.62k
    if (k >= 0)
5031
331
      return 1;
5032
5.62k
  }
5033
8.03k
5034
8.03k
  
return 07.01k
;
5035
8.03k
}
5036
5037
/* Remove any common factor g from the constraint coefficients in "v".
5038
 * The constant term is stored in the first position and is replaced
5039
 * by floor(c/g).  If any common factor is removed and if this results
5040
 * in a tightening of the constraint, then set *tightened.
5041
 */
5042
static __isl_give isl_vec *normalize_constraint(__isl_take isl_vec *v,
5043
  int *tightened)
5044
3.94k
{
5045
3.94k
  isl_ctx *ctx;
5046
3.94k
5047
3.94k
  if (!v)
5048
0
    return NULL;
5049
3.94k
  ctx = isl_vec_get_ctx(v);
5050
3.94k
  isl_seq_gcd(v->el + 1, v->size - 1, &ctx->normalize_gcd);
5051
3.94k
  if (isl_int_is_zero(ctx->normalize_gcd))
5052
3.94k
    
return v0
;
5053
3.94k
  if (isl_int_is_one(ctx->normalize_gcd))
5054
3.94k
    
return v2.94k
;
5055
998
  v = isl_vec_cow(v);
5056
998
  if (!v)
5057
0
    return NULL;
5058
998
  if (tightened && !isl_int_is_divisible_by(v->el[0], ctx->normalize_gcd))
5059
998
    
*tightened = 1262
;
5060
998
  isl_int_fdiv_q(v->el[0], v->el[0], ctx->normalize_gcd);
5061
998
  isl_seq_scale_down(v->el + 1, v->el + 1, ctx->normalize_gcd,
5062
998
        v->size - 1);
5063
998
  return v;
5064
998
}
5065
5066
/* If "bmap" is an integer set that satisfies any equality involving
5067
 * more than 2 variables and/or has coefficients different from -1 and 1,
5068
 * then use variable compression to reduce the coefficients by removing
5069
 * any (hidden) common factor.
5070
 * In particular, apply the variable compression to each constraint,
5071
 * factor out any common factor in the non-constant coefficients and
5072
 * then apply the inverse of the compression.
5073
 * At the end, we mark the basic map as having reduced constants.
5074
 * If this flag is still set on the next invocation of this function,
5075
 * then we skip the computation.
5076
 *
5077
 * Removing a common factor may result in a tightening of some of
5078
 * the constraints.  If this happens, then we may end up with two
5079
 * opposite inequalities that can be replaced by an equality.
5080
 * We therefore call isl_basic_map_detect_inequality_pairs,
5081
 * which checks for such pairs of inequalities as well as eliminate_divs_eq
5082
 * and isl_basic_map_gauss if such a pair was found.
5083
 *
5084
 * Note that this function may leave the result in an inconsistent state.
5085
 * In particular, the constraints may not be gaussed.
5086
 * Unfortunately, isl_map_coalesce actually depends on this inconsistent state
5087
 * for some of the test cases to pass successfully.
5088
 * Any potential modification of the representation is therefore only
5089
 * performed on a single copy of the basic map.
5090
 */
5091
__isl_give isl_basic_map *isl_basic_map_reduce_coefficients(
5092
  __isl_take isl_basic_map *bmap)
5093
58.4k
{
5094
58.4k
  unsigned total;
5095
58.4k
  isl_ctx *ctx;
5096
58.4k
  isl_vec *v;
5097
58.4k
  isl_mat *eq, *T, *T2;
5098
58.4k
  int i;
5099
58.4k
  int tightened;
5100
58.4k
5101
58.4k
  if (!bmap)
5102
0
    return NULL;
5103
58.4k
  if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_REDUCED_COEFFICIENTS))
5104
58.4k
    
return bmap124
;
5105
58.3k
  if (isl_basic_map_is_rational(bmap))
5106
24.5k
    return bmap;
5107
33.8k
  if (bmap->n_eq == 0)
5108
25.7k
    return bmap;
5109
8.03k
  if (!has_multiple_var_equality(bmap))
5110
7.01k
    return bmap;
5111
1.02k
5112
1.02k
  total = isl_basic_map_dim(bmap, isl_dim_all);
5113
1.02k
  ctx = isl_basic_map_get_ctx(bmap);
5114
1.02k
  v = isl_vec_alloc(ctx, 1 + total);
5115
1.02k
  if (!v)
5116
0
    return isl_basic_map_free(bmap);
5117
1.02k
5118
1.02k
  eq = isl_mat_sub_alloc6(ctx, bmap->eq, 0, bmap->n_eq, 0, 1 + total);
5119
1.02k
  T = isl_mat_variable_compression(eq, &T2);
5120
1.02k
  if (!T || !T2)
5121
0
    goto error;
5122
1.02k
  if (T->n_col == 0) {
5123
1
    isl_mat_free(T);
5124
1
    isl_mat_free(T2);
5125
1
    isl_vec_free(v);
5126
1
    return isl_basic_map_set_to_empty(bmap);
5127
1
  }
5128
1.02k
5129
1.02k
  bmap = isl_basic_map_cow(bmap);
5130
1.02k
  if (!bmap)
5131
0
    goto error;
5132
1.02k
5133
1.02k
  tightened = 0;
5134
4.96k
  for (i = 0; i < bmap->n_ineq; 
++i3.94k
) {
5135
3.94k
    isl_seq_cpy(v->el, bmap->ineq[i], 1 + total);
5136
3.94k
    v = isl_vec_mat_product(v, isl_mat_copy(T));
5137
3.94k
    v = normalize_constraint(v, &tightened);
5138
3.94k
    v = isl_vec_mat_product(v, isl_mat_copy(T2));
5139
3.94k
    if (!v)
5140
0
      goto error;
5141
3.94k
    isl_seq_cpy(bmap->ineq[i], v->el, 1 + total);
5142
3.94k
  }
5143
1.02k
5144
1.02k
  isl_mat_free(T);
5145
1.02k
  isl_mat_free(T2);
5146
1.02k
  isl_vec_free(v);
5147
1.02k
5148
1.02k
  ISL_F_SET(bmap, ISL_BASIC_MAP_REDUCED_COEFFICIENTS);
5149
1.02k
5150
1.02k
  if (tightened) {
5151
212
    int progress = 0;
5152
212
5153
212
    bmap = isl_basic_map_detect_inequality_pairs(bmap, &progress);
5154
212
    if (progress) {
5155
49
      bmap = eliminate_divs_eq(bmap, &progress);
5156
49
      bmap = isl_basic_map_gauss(bmap, NULL);
5157
49
    }
5158
212
  }
5159
1.02k
5160
1.02k
  return bmap;
5161
0
error:
5162
0
  isl_mat_free(T);
5163
0
  isl_mat_free(T2);
5164
0
  isl_vec_free(v);
5165
0
  return isl_basic_map_free(bmap);
5166
1.02k
}
5167
5168
/* Shift the integer division at position "div" of "bmap"
5169
 * by "shift" times the variable at position "pos".
5170
 * "pos" is as determined by isl_basic_map_offset, i.e., pos == 0
5171
 * corresponds to the constant term.
5172
 *
5173
 * That is, if the integer division has the form
5174
 *
5175
 *  floor(f(x)/d)
5176
 *
5177
 * then replace it by
5178
 *
5179
 *  floor((f(x) + shift * d * x_pos)/d) - shift * x_pos
5180
 */
5181
__isl_give isl_basic_map *isl_basic_map_shift_div(
5182
  __isl_take isl_basic_map *bmap, int div, int pos, isl_int shift)
5183
14.3k
{
5184
14.3k
  int i;
5185
14.3k
  unsigned total;
5186
14.3k
5187
14.3k
  if (isl_int_is_zero(shift))
5188
14.3k
    
return bmap75
;
5189
14.2k
  if (!bmap)
5190
0
    return NULL;
5191
14.2k
5192
14.2k
  total = isl_basic_map_dim(bmap, isl_dim_all);
5193
14.2k
  total -= isl_basic_map_dim(bmap, isl_dim_div);
5194
14.2k
5195
14.2k
  isl_int_addmul(bmap->div[div][1 + pos], shift, bmap->div[div][0]);
5196
14.2k
5197
55.5k
  for (i = 0; i < bmap->n_eq; 
++i41.2k
) {
5198
41.2k
    if (isl_int_is_zero(bmap->eq[i][1 + total + div]))
5199
41.2k
      
continue28.9k
;
5200
12.3k
    isl_int_submul(bmap->eq[i][pos],
5201
12.3k
        shift, bmap->eq[i][1 + total + div]);
5202
12.3k
  }
5203
105k
  for (i = 0; i < bmap->n_ineq; 
++i91.0k
) {
5204
91.0k
    if (isl_int_is_zero(bmap->ineq[i][1 + total + div]))
5205
91.0k
      
continue82.2k
;
5206
8.77k
    isl_int_submul(bmap->ineq[i][pos],
5207
8.77k
        shift, bmap->ineq[i][1 + total + div]);
5208
8.77k
  }
5209
44.4k
  for (i = 0; i < bmap->n_div; 
++i30.1k
) {
5210
30.1k
    if (isl_int_is_zero(bmap->div[i][0]))
5211
30.1k
      
continue2.56k
;
5212
27.5k
    if (isl_int_is_zero(bmap->div[i][1 + 1 + total + div]))
5213
27.5k
      
continue27.0k
;
5214
488
    isl_int_submul(bmap->div[i][1 + pos],
5215
488
        shift, bmap->div[i][1 + 1 + total + div]);
5216
488
  }
5217
14.2k
5218
14.2k
  return bmap;
5219
14.2k
}