Coverage Report

Created: 2017-08-21 19:50

/Users/buildslave/jenkins/sharedspace/clang-stage2-coverage-R@2/llvm/tools/polly/lib/External/isl/isl_tab.c
Line
Count
Source (jump to first uncovered line)
1
/*
2
 * Copyright 2008-2009 Katholieke Universiteit Leuven
3
 * Copyright 2013      Ecole Normale Superieure
4
 * Copyright 2014      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_mat_private.h>
18
#include <isl_vec_private.h>
19
#include "isl_map_private.h"
20
#include "isl_tab.h"
21
#include <isl_seq.h>
22
#include <isl_config.h>
23
24
#include <bset_to_bmap.c>
25
#include <bset_from_bmap.c>
26
27
/*
28
 * The implementation of tableaus in this file was inspired by Section 8
29
 * of David Detlefs, Greg Nelson and James B. Saxe, "Simplify: a theorem
30
 * prover for program checking".
31
 */
32
33
struct isl_tab *isl_tab_alloc(struct isl_ctx *ctx,
34
  unsigned n_row, unsigned n_var, unsigned M)
35
607k
{
36
607k
  int i;
37
607k
  struct isl_tab *tab;
38
607k
  unsigned off = 2 + M;
39
607k
40
607k
  tab = isl_calloc_type(ctx, struct isl_tab);
41
607k
  if (!tab)
42
0
    return NULL;
43
607k
  tab->mat = isl_mat_alloc(ctx, n_row, off + n_var);
44
607k
  if (!tab->mat)
45
0
    goto error;
46
607k
  
tab->var = 607k
isl_alloc_array607k
(ctx, struct isl_tab_var, n_var);
47
607k
  if (
n_var && 607k
!tab->var606k
)
48
0
    goto error;
49
607k
  
tab->con = 607k
isl_alloc_array607k
(ctx, struct isl_tab_var, n_row);
50
607k
  if (
n_row && 607k
!tab->con607k
)
51
0
    goto error;
52
607k
  
tab->col_var = 607k
isl_alloc_array607k
(ctx, int, n_var);
53
607k
  if (
n_var && 607k
!tab->col_var606k
)
54
0
    goto error;
55
607k
  
tab->row_var = 607k
isl_alloc_array607k
(ctx, int, n_row);
56
607k
  if (
n_row && 607k
!tab->row_var607k
)
57
0
    goto error;
58
3.17M
  
for (i = 0; 607k
i < n_var3.17M
;
++i2.56M
)
{2.56M
59
2.56M
    tab->var[i].index = i;
60
2.56M
    tab->var[i].is_row = 0;
61
2.56M
    tab->var[i].is_nonneg = 0;
62
2.56M
    tab->var[i].is_zero = 0;
63
2.56M
    tab->var[i].is_redundant = 0;
64
2.56M
    tab->var[i].frozen = 0;
65
2.56M
    tab->var[i].negated = 0;
66
2.56M
    tab->col_var[i] = i;
67
2.56M
  }
68
607k
  tab->n_row = 0;
69
607k
  tab->n_con = 0;
70
607k
  tab->n_eq = 0;
71
607k
  tab->max_con = n_row;
72
607k
  tab->n_col = n_var;
73
607k
  tab->n_var = n_var;
74
607k
  tab->max_var = n_var;
75
607k
  tab->n_param = 0;
76
607k
  tab->n_div = 0;
77
607k
  tab->n_dead = 0;
78
607k
  tab->n_redundant = 0;
79
607k
  tab->strict_redundant = 0;
80
607k
  tab->need_undo = 0;
81
607k
  tab->rational = 0;
82
607k
  tab->empty = 0;
83
607k
  tab->in_undo = 0;
84
607k
  tab->M = M;
85
607k
  tab->cone = 0;
86
607k
  tab->bottom.type = isl_tab_undo_bottom;
87
607k
  tab->bottom.next = NULL;
88
607k
  tab->top = &tab->bottom;
89
607k
90
607k
  tab->n_zero = 0;
91
607k
  tab->n_unbounded = 0;
92
607k
  tab->basis = NULL;
93
607k
94
607k
  return tab;
95
607k
error:
96
0
  isl_tab_free(tab);
97
607k
  return NULL;
98
607k
}
99
100
isl_ctx *isl_tab_get_ctx(struct isl_tab *tab)
101
2.47M
{
102
2.47M
  return tab ? isl_mat_get_ctx(tab->mat) : NULL;
103
2.47M
}
104
105
int isl_tab_extend_cons(struct isl_tab *tab, unsigned n_new)
106
696k
{
107
696k
  unsigned off;
108
696k
109
696k
  if (!tab)
110
0
    return -1;
111
696k
112
696k
  off = 2 + tab->M;
113
696k
114
696k
  if (
tab->max_con < tab->n_con + n_new696k
)
{73.6k
115
73.6k
    struct isl_tab_var *con;
116
73.6k
117
73.6k
    con = isl_realloc_array(tab->mat->ctx, tab->con,
118
73.6k
            struct isl_tab_var, tab->max_con + n_new);
119
73.6k
    if (!con)
120
0
      return -1;
121
73.6k
    tab->con = con;
122
73.6k
    tab->max_con += n_new;
123
696k
  }
124
696k
  
if (696k
tab->mat->n_row < tab->n_row + n_new696k
)
{76.3k
125
76.3k
    int *row_var;
126
76.3k
127
76.3k
    tab->mat = isl_mat_extend(tab->mat,
128
76.3k
          tab->n_row + n_new, off + tab->n_col);
129
76.3k
    if (!tab->mat)
130
0
      return -1;
131
76.3k
    
row_var = 76.3k
isl_realloc_array76.3k
(tab->mat->ctx, tab->row_var,
132
76.3k
              int, tab->mat->n_row);
133
76.3k
    if (!row_var)
134
0
      return -1;
135
76.3k
    tab->row_var = row_var;
136
76.3k
    if (
tab->row_sign76.3k
)
{198
137
198
      enum isl_tab_row_sign *s;
138
198
      s = isl_realloc_array(tab->mat->ctx, tab->row_sign,
139
198
          enum isl_tab_row_sign, tab->mat->n_row);
140
198
      if (!s)
141
0
        return -1;
142
198
      tab->row_sign = s;
143
76.3k
    }
144
696k
  }
145
696k
  return 0;
146
696k
}
147
148
/* Make room for at least n_new extra variables.
149
 * Return -1 if anything went wrong.
150
 */
151
int isl_tab_extend_vars(struct isl_tab *tab, unsigned n_new)
152
5.52k
{
153
5.52k
  struct isl_tab_var *var;
154
5.52k
  unsigned off = 2 + tab->M;
155
5.52k
156
5.52k
  if (
tab->max_var < tab->n_var + n_new5.52k
)
{4.32k
157
4.32k
    var = isl_realloc_array(tab->mat->ctx, tab->var,
158
4.32k
            struct isl_tab_var, tab->n_var + n_new);
159
4.32k
    if (!var)
160
0
      return -1;
161
4.32k
    tab->var = var;
162
4.32k
    tab->max_var = tab->n_var + n_new;
163
5.52k
  }
164
5.52k
165
5.52k
  
if (5.52k
tab->mat->n_col < off + tab->n_col + n_new5.52k
)
{3.04k
166
3.04k
    int *p;
167
3.04k
168
3.04k
    tab->mat = isl_mat_extend(tab->mat,
169
3.04k
            tab->mat->n_row, off + tab->n_col + n_new);
170
3.04k
    if (!tab->mat)
171
0
      return -1;
172
3.04k
    
p = 3.04k
isl_realloc_array3.04k
(tab->mat->ctx, tab->col_var,
173
3.04k
              int, tab->n_col + n_new);
174
3.04k
    if (!p)
175
0
      return -1;
176
3.04k
    tab->col_var = p;
177
5.52k
  }
178
5.52k
179
5.52k
  return 0;
180
5.52k
}
181
182
static void free_undo_record(struct isl_tab_undo *undo)
183
2.67M
{
184
2.67M
  switch (undo->type) {
185
2.67M
  case isl_tab_undo_saved_basis:
186
775
    free(undo->u.col_var);
187
2.67M
    break;
188
2.67M
  default:;
189
2.67M
  }
190
2.67M
  free(undo);
191
2.67M
}
192
193
static void free_undo(struct isl_tab *tab)
194
612k
{
195
612k
  struct isl_tab_undo *undo, *next;
196
612k
197
1.05M
  for (undo = tab->top; 
undo && 1.05M
undo != &tab->bottom1.05M
;
undo = next445k
)
{445k
198
445k
    next = undo->next;
199
445k
    free_undo_record(undo);
200
612k
  }
201
612k
  tab->top = undo;
202
612k
}
203
204
void isl_tab_free(struct isl_tab *tab)
205
640k
{
206
640k
  if (!tab)
207
28.5k
    return;
208
640k
  free_undo(tab);
209
612k
  isl_mat_free(tab->mat);
210
612k
  isl_vec_free(tab->dual);
211
612k
  isl_basic_map_free(tab->bmap);
212
612k
  free(tab->var);
213
612k
  free(tab->con);
214
612k
  free(tab->row_var);
215
612k
  free(tab->col_var);
216
612k
  free(tab->row_sign);
217
612k
  isl_mat_free(tab->samples);
218
612k
  free(tab->sample_index);
219
612k
  isl_mat_free(tab->basis);
220
612k
  free(tab);
221
640k
}
222
223
struct isl_tab *isl_tab_dup(struct isl_tab *tab)
224
2.57k
{
225
2.57k
  int i;
226
2.57k
  struct isl_tab *dup;
227
2.57k
  unsigned off;
228
2.57k
229
2.57k
  if (!tab)
230
0
    return NULL;
231
2.57k
232
2.57k
  off = 2 + tab->M;
233
2.57k
  dup = isl_calloc_type(tab->mat->ctx, struct isl_tab);
234
2.57k
  if (!dup)
235
0
    return NULL;
236
2.57k
  dup->mat = isl_mat_dup(tab->mat);
237
2.57k
  if (!dup->mat)
238
0
    goto error;
239
2.57k
  
dup->var = 2.57k
isl_alloc_array2.57k
(tab->mat->ctx, struct isl_tab_var, tab->max_var);
240
2.57k
  if (
tab->max_var && 2.57k
!dup->var2.57k
)
241
0
    goto error;
242
23.4k
  
for (i = 0; 2.57k
i < tab->n_var23.4k
;
++i20.9k
)
243
20.9k
    dup->var[i] = tab->var[i];
244
2.57k
  dup->con = isl_alloc_array(tab->mat->ctx, struct isl_tab_var, tab->max_con);
245
2.57k
  if (
tab->max_con && 2.57k
!dup->con2.57k
)
246
0
    goto error;
247
26.1k
  
for (i = 0; 2.57k
i < tab->n_con26.1k
;
++i23.5k
)
248
23.5k
    dup->con[i] = tab->con[i];
249
2.57k
  dup->col_var = isl_alloc_array(tab->mat->ctx, int, tab->mat->n_col - off);
250
2.57k
  if (
(tab->mat->n_col - off) && 2.57k
!dup->col_var2.57k
)
251
0
    goto error;
252
11.8k
  
for (i = 0; 2.57k
i < tab->n_col11.8k
;
++i9.32k
)
253
9.32k
    dup->col_var[i] = tab->col_var[i];
254
2.57k
  dup->row_var = isl_alloc_array(tab->mat->ctx, int, tab->mat->n_row);
255
2.57k
  if (
tab->mat->n_row && 2.57k
!dup->row_var2.57k
)
256
0
    goto error;
257
26.0k
  
for (i = 0; 2.57k
i < tab->n_row26.0k
;
++i23.4k
)
258
23.4k
    dup->row_var[i] = tab->row_var[i];
259
2.57k
  if (
tab->row_sign2.57k
)
{2.56k
260
2.56k
    dup->row_sign = isl_alloc_array(tab->mat->ctx, enum isl_tab_row_sign,
261
2.56k
            tab->mat->n_row);
262
2.56k
    if (
tab->mat->n_row && 2.56k
!dup->row_sign2.56k
)
263
0
      goto error;
264
25.9k
    
for (i = 0; 2.56k
i < tab->n_row25.9k
;
++i23.3k
)
265
23.3k
      dup->row_sign[i] = tab->row_sign[i];
266
2.57k
  }
267
2.57k
  
if (2.57k
tab->samples2.57k
)
{0
268
0
    dup->samples = isl_mat_dup(tab->samples);
269
0
    if (!dup->samples)
270
0
      goto error;
271
0
    
dup->sample_index = 0
isl_alloc_array0
(tab->mat->ctx, int,
272
0
              tab->samples->n_row);
273
0
    if (
tab->samples->n_row && 0
!dup->sample_index0
)
274
0
      goto error;
275
0
    dup->n_sample = tab->n_sample;
276
0
    dup->n_outside = tab->n_outside;
277
2.57k
  }
278
2.57k
  dup->n_row = tab->n_row;
279
2.57k
  dup->n_con = tab->n_con;
280
2.57k
  dup->n_eq = tab->n_eq;
281
2.57k
  dup->max_con = tab->max_con;
282
2.57k
  dup->n_col = tab->n_col;
283
2.57k
  dup->n_var = tab->n_var;
284
2.57k
  dup->max_var = tab->max_var;
285
2.57k
  dup->n_param = tab->n_param;
286
2.57k
  dup->n_div = tab->n_div;
287
2.57k
  dup->n_dead = tab->n_dead;
288
2.57k
  dup->n_redundant = tab->n_redundant;
289
2.57k
  dup->rational = tab->rational;
290
2.57k
  dup->empty = tab->empty;
291
2.57k
  dup->strict_redundant = 0;
292
2.57k
  dup->need_undo = 0;
293
2.57k
  dup->in_undo = 0;
294
2.57k
  dup->M = tab->M;
295
2.57k
  tab->cone = tab->cone;
296
2.57k
  dup->bottom.type = isl_tab_undo_bottom;
297
2.57k
  dup->bottom.next = NULL;
298
2.57k
  dup->top = &dup->bottom;
299
2.57k
300
2.57k
  dup->n_zero = tab->n_zero;
301
2.57k
  dup->n_unbounded = tab->n_unbounded;
302
2.57k
  dup->basis = isl_mat_dup(tab->basis);
303
2.57k
304
2.57k
  return dup;
305
2.57k
error:
306
0
  isl_tab_free(dup);
307
2.57k
  return NULL;
308
2.57k
}
309
310
/* Construct the coefficient matrix of the product tableau
311
 * of two tableaus.
312
 * mat{1,2} is the coefficient matrix of tableau {1,2}
313
 * row{1,2} is the number of rows in tableau {1,2}
314
 * col{1,2} is the number of columns in tableau {1,2}
315
 * off is the offset to the coefficient column (skipping the
316
 *  denominator, the constant term and the big parameter if any)
317
 * r{1,2} is the number of redundant rows in tableau {1,2}
318
 * d{1,2} is the number of dead columns in tableau {1,2}
319
 *
320
 * The order of the rows and columns in the result is as explained
321
 * in isl_tab_product.
322
 */
323
static struct isl_mat *tab_mat_product(struct isl_mat *mat1,
324
  struct isl_mat *mat2, unsigned row1, unsigned row2,
325
  unsigned col1, unsigned col2,
326
  unsigned off, unsigned r1, unsigned r2, unsigned d1, unsigned d2)
327
1.82k
{
328
1.82k
  int i;
329
1.82k
  struct isl_mat *prod;
330
1.82k
  unsigned n;
331
1.82k
332
1.82k
  prod = isl_mat_alloc(mat1->ctx, mat1->n_row + mat2->n_row,
333
1.82k
          off + col1 + col2);
334
1.82k
  if (!prod)
335
0
    return NULL;
336
1.82k
337
1.82k
  n = 0;
338
6.89k
  for (i = 0; 
i < r16.89k
;
++i5.07k
)
{5.07k
339
5.07k
    isl_seq_cpy(prod->row[n + i], mat1->row[i], off + d1);
340
5.07k
    isl_seq_clr(prod->row[n + i] + off + d1, d2);
341
5.07k
    isl_seq_cpy(prod->row[n + i] + off + d1 + d2,
342
5.07k
        mat1->row[i] + off + d1, col1 - d1);
343
5.07k
    isl_seq_clr(prod->row[n + i] + off + col1 + d1, col2 - d2);
344
5.07k
  }
345
1.82k
346
1.82k
  n += r1;
347
6.89k
  for (i = 0; 
i < r26.89k
;
++i5.07k
)
{5.07k
348
5.07k
    isl_seq_cpy(prod->row[n + i], mat2->row[i], off);
349
5.07k
    isl_seq_clr(prod->row[n + i] + off, d1);
350
5.07k
    isl_seq_cpy(prod->row[n + i] + off + d1,
351
5.07k
          mat2->row[i] + off, d2);
352
5.07k
    isl_seq_clr(prod->row[n + i] + off + d1 + d2, col1 - d1);
353
5.07k
    isl_seq_cpy(prod->row[n + i] + off + col1 + d1,
354
5.07k
          mat2->row[i] + off + d2, col2 - d2);
355
5.07k
  }
356
1.82k
357
1.82k
  n += r2;
358
18.4k
  for (i = 0; 
i < row1 - r118.4k
;
++i16.6k
)
{16.6k
359
16.6k
    isl_seq_cpy(prod->row[n + i], mat1->row[r1 + i], off + d1);
360
16.6k
    isl_seq_clr(prod->row[n + i] + off + d1, d2);
361
16.6k
    isl_seq_cpy(prod->row[n + i] + off + d1 + d2,
362
16.6k
        mat1->row[r1 + i] + off + d1, col1 - d1);
363
16.6k
    isl_seq_clr(prod->row[n + i] + off + col1 + d1, col2 - d2);
364
16.6k
  }
365
1.82k
366
1.82k
  n += row1 - r1;
367
18.4k
  for (i = 0; 
i < row2 - r218.4k
;
++i16.6k
)
{16.6k
368
16.6k
    isl_seq_cpy(prod->row[n + i], mat2->row[r2 + i], off);
369
16.6k
    isl_seq_clr(prod->row[n + i] + off, d1);
370
16.6k
    isl_seq_cpy(prod->row[n + i] + off + d1,
371
16.6k
          mat2->row[r2 + i] + off, d2);
372
16.6k
    isl_seq_clr(prod->row[n + i] + off + d1 + d2, col1 - d1);
373
16.6k
    isl_seq_cpy(prod->row[n + i] + off + col1 + d1,
374
16.6k
          mat2->row[r2 + i] + off + d2, col2 - d2);
375
16.6k
  }
376
1.82k
377
1.82k
  return prod;
378
1.82k
}
379
380
/* Update the row or column index of a variable that corresponds
381
 * to a variable in the first input tableau.
382
 */
383
static void update_index1(struct isl_tab_var *var,
384
  unsigned r1, unsigned r2, unsigned d1, unsigned d2)
385
30.3k
{
386
30.3k
  if (var->index == -1)
387
213
    return;
388
30.1k
  
if (30.1k
var->is_row && 30.1k
var->index >= r121.6k
)
389
16.6k
    var->index += r2;
390
30.1k
  if (
!var->is_row && 30.1k
var->index >= d18.50k
)
391
7.72k
    var->index += d2;
392
30.3k
}
393
394
/* Update the row or column index of a variable that corresponds
395
 * to a variable in the second input tableau.
396
 */
397
static void update_index2(struct isl_tab_var *var,
398
  unsigned row1, unsigned col1,
399
  unsigned r1, unsigned r2, unsigned d1, unsigned d2)
400
30.3k
{
401
30.3k
  if (var->index == -1)
402
213
    return;
403
30.1k
  
if (30.1k
var->is_row30.1k
)
{21.6k
404
21.6k
    if (var->index < r2)
405
5.07k
      var->index += r1;
406
21.6k
    else
407
16.6k
      var->index += row1;
408
30.1k
  } else {
409
8.50k
    if (var->index < d2)
410
776
      var->index += d1;
411
8.50k
    else
412
7.72k
      var->index += col1;
413
30.1k
  }
414
30.3k
}
415
416
/* Create a tableau that represents the Cartesian product of the sets
417
 * represented by tableaus tab1 and tab2.
418
 * The order of the rows in the product is
419
 *  - redundant rows of tab1
420
 *  - redundant rows of tab2
421
 *  - non-redundant rows of tab1
422
 *  - non-redundant rows of tab2
423
 * The order of the columns is
424
 *  - denominator
425
 *  - constant term
426
 *  - coefficient of big parameter, if any
427
 *  - dead columns of tab1
428
 *  - dead columns of tab2
429
 *  - live columns of tab1
430
 *  - live columns of tab2
431
 * The order of the variables and the constraints is a concatenation
432
 * of order in the two input tableaus.
433
 */
434
struct isl_tab *isl_tab_product(struct isl_tab *tab1, struct isl_tab *tab2)
435
1.82k
{
436
1.82k
  int i;
437
1.82k
  struct isl_tab *prod;
438
1.82k
  unsigned off;
439
1.82k
  unsigned r1, r2, d1, d2;
440
1.82k
441
1.82k
  if (
!tab1 || 1.82k
!tab21.82k
)
442
0
    return NULL;
443
1.82k
444
1.82k
  
isl_assert1.82k
(tab1->mat->ctx, tab1->M == tab2->M, return NULL);1.82k
445
1.82k
  
isl_assert1.82k
(tab1->mat->ctx, tab1->rational == tab2->rational, return NULL);1.82k
446
1.82k
  
isl_assert1.82k
(tab1->mat->ctx, tab1->cone == tab2->cone, return NULL);1.82k
447
1.82k
  
isl_assert1.82k
(tab1->mat->ctx, !tab1->row_sign, return NULL);1.82k
448
1.82k
  
isl_assert1.82k
(tab1->mat->ctx, !tab2->row_sign, return NULL);1.82k
449
1.82k
  
isl_assert1.82k
(tab1->mat->ctx, tab1->n_param == 0, return NULL);1.82k
450
1.82k
  
isl_assert1.82k
(tab1->mat->ctx, tab2->n_param == 0, return NULL);1.82k
451
1.82k
  
isl_assert1.82k
(tab1->mat->ctx, tab1->n_div == 0, return NULL);1.82k
452
1.82k
  
isl_assert1.82k
(tab1->mat->ctx, tab2->n_div == 0, return NULL);1.82k
453
1.82k
454
1.82k
  off = 2 + tab1->M;
455
1.82k
  r1 = tab1->n_redundant;
456
1.82k
  r2 = tab2->n_redundant;
457
1.82k
  d1 = tab1->n_dead;
458
1.82k
  d2 = tab2->n_dead;
459
1.82k
  prod = isl_calloc_type(tab1->mat->ctx, struct isl_tab);
460
1.82k
  if (!prod)
461
0
    return NULL;
462
1.82k
  prod->mat = tab_mat_product(tab1->mat, tab2->mat,
463
1.82k
        tab1->n_row, tab2->n_row,
464
1.82k
        tab1->n_col, tab2->n_col, off, r1, r2, d1, d2);
465
1.82k
  if (!prod->mat)
466
0
    goto error;
467
1.82k
  
prod->var = 1.82k
isl_alloc_array1.82k
(tab1->mat->ctx, struct isl_tab_var,
468
1.82k
          tab1->max_var + tab2->max_var);
469
1.82k
  if (
(tab1->max_var + tab2->max_var) && 1.82k
!prod->var1.82k
)
470
0
    goto error;
471
10.5k
  
for (i = 0; 1.82k
i < tab1->n_var10.5k
;
++i8.71k
)
{8.71k
472
8.71k
    prod->var[i] = tab1->var[i];
473
8.71k
    update_index1(&prod->var[i], r1, r2, d1, d2);
474
8.71k
  }
475
10.5k
  for (i = 0; 
i < tab2->n_var10.5k
;
++i8.71k
)
{8.71k
476
8.71k
    prod->var[tab1->n_var + i] = tab2->var[i];
477
8.71k
    update_index2(&prod->var[tab1->n_var + i],
478
8.71k
        tab1->n_row, tab1->n_col,
479
8.71k
        r1, r2, d1, d2);
480
8.71k
  }
481
1.82k
  prod->con = isl_alloc_array(tab1->mat->ctx, struct isl_tab_var,
482
1.82k
          tab1->max_con +  tab2->max_con);
483
1.82k
  if (
(tab1->max_con + tab2->max_con) && 1.82k
!prod->con1.82k
)
484
0
    goto error;
485
23.4k
  
for (i = 0; 1.82k
i < tab1->n_con23.4k
;
++i21.6k
)
{21.6k
486
21.6k
    prod->con[i] = tab1->con[i];
487
21.6k
    update_index1(&prod->con[i], r1, r2, d1, d2);
488
21.6k
  }
489
23.4k
  for (i = 0; 
i < tab2->n_con23.4k
;
++i21.6k
)
{21.6k
490
21.6k
    prod->con[tab1->n_con + i] = tab2->con[i];
491
21.6k
    update_index2(&prod->con[tab1->n_con + i],
492
21.6k
        tab1->n_row, tab1->n_col,
493
21.6k
        r1, r2, d1, d2);
494
21.6k
  }
495
1.82k
  prod->col_var = isl_alloc_array(tab1->mat->ctx, int,
496
1.82k
          tab1->n_col + tab2->n_col);
497
1.82k
  if (
(tab1->n_col + tab2->n_col) && 1.82k
!prod->col_var1.82k
)
498
0
    goto error;
499
10.3k
  
for (i = 0; 1.82k
i < tab1->n_col10.3k
;
++i8.50k
)
{8.50k
500
8.50k
    int pos = i < d1 ? 
i776
:
i + d27.72k
;
501
8.50k
    prod->col_var[pos] = tab1->col_var[i];
502
8.50k
  }
503
10.3k
  for (i = 0; 
i < tab2->n_col10.3k
;
++i8.50k
)
{8.50k
504
8.50k
    int pos = i < d2 ? 
d1 + i776
:
tab1->n_col + i7.72k
;
505
8.50k
    int t = tab2->col_var[i];
506
8.50k
    if (t >= 0)
507
190
      t += tab1->n_var;
508
8.50k
    else
509
8.31k
      t -= tab1->n_con;
510
8.50k
    prod->col_var[pos] = t;
511
8.50k
  }
512
1.82k
  prod->row_var = isl_alloc_array(tab1->mat->ctx, int,
513
1.82k
          tab1->mat->n_row + tab2->mat->n_row);
514
1.82k
  if (
(tab1->mat->n_row + tab2->mat->n_row) && 1.82k
!prod->row_var1.82k
)
515
0
    goto error;
516
23.4k
  
for (i = 0; 1.82k
i < tab1->n_row23.4k
;
++i21.6k
)
{21.6k
517
21.6k
    int pos = i < r1 ? 
i5.07k
:
i + r216.6k
;
518
21.6k
    prod->row_var[pos] = tab1->row_var[i];
519
21.6k
  }
520
23.4k
  for (i = 0; 
i < tab2->n_row23.4k
;
++i21.6k
)
{21.6k
521
21.6k
    int pos = i < r2 ? 
r1 + i5.07k
:
tab1->n_row + i16.6k
;
522
21.6k
    int t = tab2->row_var[i];
523
21.6k
    if (t >= 0)
524
8.52k
      t += tab1->n_var;
525
21.6k
    else
526
13.1k
      t -= tab1->n_con;
527
21.6k
    prod->row_var[pos] = t;
528
21.6k
  }
529
1.82k
  prod->samples = NULL;
530
1.82k
  prod->sample_index = NULL;
531
1.82k
  prod->n_row = tab1->n_row + tab2->n_row;
532
1.82k
  prod->n_con = tab1->n_con + tab2->n_con;
533
1.82k
  prod->n_eq = 0;
534
1.82k
  prod->max_con = tab1->max_con + tab2->max_con;
535
1.82k
  prod->n_col = tab1->n_col + tab2->n_col;
536
1.82k
  prod->n_var = tab1->n_var + tab2->n_var;
537
1.82k
  prod->max_var = tab1->max_var + tab2->max_var;
538
1.82k
  prod->n_param = 0;
539
1.82k
  prod->n_div = 0;
540
1.82k
  prod->n_dead = tab1->n_dead + tab2->n_dead;
541
1.82k
  prod->n_redundant = tab1->n_redundant + tab2->n_redundant;
542
1.82k
  prod->rational = tab1->rational;
543
1.82k
  prod->empty = tab1->empty || tab2->empty;
544
1.82k
  prod->strict_redundant = tab1->strict_redundant || tab2->strict_redundant;
545
1.82k
  prod->need_undo = 0;
546
1.82k
  prod->in_undo = 0;
547
1.82k
  prod->M = tab1->M;
548
1.82k
  prod->cone = tab1->cone;
549
1.82k
  prod->bottom.type = isl_tab_undo_bottom;
550
1.82k
  prod->bottom.next = NULL;
551
1.82k
  prod->top = &prod->bottom;
552
1.82k
553
1.82k
  prod->n_zero = 0;
554
1.82k
  prod->n_unbounded = 0;
555
1.82k
  prod->basis = NULL;
556
1.82k
557
1.82k
  return prod;
558
1.82k
error:
559
0
  isl_tab_free(prod);
560
1.82k
  return NULL;
561
1.82k
}
562
563
static struct isl_tab_var *var_from_index(struct isl_tab *tab, int i)
564
87.5M
{
565
87.5M
  if (i >= 0)
566
23.7M
    return &tab->var[i];
567
87.5M
  else
568
63.8M
    return &tab->con[~i];
569
87.5M
}
570
571
struct isl_tab_var *isl_tab_var_from_row(struct isl_tab *tab, int i)
572
65.3M
{
573
65.3M
  return var_from_index(tab, tab->row_var[i]);
574
65.3M
}
575
576
static struct isl_tab_var *var_from_col(struct isl_tab *tab, int i)
577
20.3M
{
578
20.3M
  return var_from_index(tab, tab->col_var[i]);
579
20.3M
}
580
581
/* Check if there are any upper bounds on column variable "var",
582
 * i.e., non-negative rows where var appears with a negative coefficient.
583
 * Return 1 if there are no such bounds.
584
 */
585
static int max_is_manifestly_unbounded(struct isl_tab *tab,
586
  struct isl_tab_var *var)
587
1.61M
{
588
1.61M
  int i;
589
1.61M
  unsigned off = 2 + tab->M;
590
1.61M
591
1.61M
  if (var->is_row)
592
1.07M
    return 0;
593
2.62M
  
for (i = tab->n_redundant; 544k
i < tab->n_row2.62M
;
++i2.07M
)
{2.20M
594
2.20M
    if (
!2.20M
isl_int_is_neg2.20M
(tab->mat->row[i][off + var->index]))
595
1.87M
      continue;
596
334k
    
if (334k
isl_tab_var_from_row(tab, i)->is_nonneg334k
)
597
129k
      return 0;
598
544k
  }
599
414k
  return 1;
600
1.61M
}
601
602
/* Check if there are any lower bounds on column variable "var",
603
 * i.e., non-negative rows where var appears with a positive coefficient.
604
 * Return 1 if there are no such bounds.
605
 */
606
static int min_is_manifestly_unbounded(struct isl_tab *tab,
607
  struct isl_tab_var *var)
608
1.37M
{
609
1.37M
  int i;
610
1.37M
  unsigned off = 2 + tab->M;
611
1.37M
612
1.37M
  if (var->is_row)
613
679k
    return 0;
614
5.22M
  
for (i = tab->n_redundant; 696k
i < tab->n_row5.22M
;
++i4.52M
)
{4.89M
615
4.89M
    if (
!4.89M
isl_int_is_pos4.89M
(tab->mat->row[i][off + var->index]))
616
4.25M
      continue;
617
642k
    
if (642k
isl_tab_var_from_row(tab, i)->is_nonneg642k
)
618
371k
      return 0;
619
696k
  }
620
325k
  return 1;
621
1.37M
}
622
623
static int row_cmp(struct isl_tab *tab, int r1, int r2, int c, isl_int *t)
624
1.11M
{
625
1.11M
  unsigned off = 2 + tab->M;
626
1.11M
627
1.11M
  if (
tab->M1.11M
)
{0
628
0
    int s;
629
0
    isl_int_mul(*t, tab->mat->row[r1][2], tab->mat->row[r2][off+c]);
630
0
    isl_int_submul(*t, tab->mat->row[r2][2], tab->mat->row[r1][off+c]);
631
0
    s = isl_int_sgn(*t);
632
0
    if (s)
633
0
      return s;
634
1.11M
  }
635
1.11M
  
isl_int_mul1.11M
(*t, tab->mat->row[r1][1], tab->mat->row[r2][off + c]);1.11M
636
1.11M
  isl_int_submul(*t, tab->mat->row[r2][1], tab->mat->row[r1][off + c]);
637
1.11M
  return isl_int_sgn(*t);
638
1.11M
}
639
640
/* Given the index of a column "c", return the index of a row
641
 * that can be used to pivot the column in, with either an increase
642
 * (sgn > 0) or a decrease (sgn < 0) of the corresponding variable.
643
 * If "var" is not NULL, then the row returned will be different from
644
 * the one associated with "var".
645
 *
646
 * Each row in the tableau is of the form
647
 *
648
 *  x_r = a_r0 + \sum_i a_ri x_i
649
 *
650
 * Only rows with x_r >= 0 and with the sign of a_ri opposite to "sgn"
651
 * impose any limit on the increase or decrease in the value of x_c
652
 * and this bound is equal to a_r0 / |a_rc|.  We are therefore looking
653
 * for the row with the smallest (most stringent) such bound.
654
 * Note that the common denominator of each row drops out of the fraction.
655
 * To check if row j has a smaller bound than row r, i.e.,
656
 * a_j0 / |a_jc| < a_r0 / |a_rc| or a_j0 |a_rc| < a_r0 |a_jc|,
657
 * we check if -sign(a_jc) (a_j0 a_rc - a_r0 a_jc) < 0,
658
 * where -sign(a_jc) is equal to "sgn".
659
 */
660
static int pivot_row(struct isl_tab *tab,
661
  struct isl_tab_var *var, int sgn, int c)
662
2.52M
{
663
2.52M
  int j, r, tsgn;
664
2.52M
  isl_int t;
665
2.52M
  unsigned off = 2 + tab->M;
666
2.52M
667
2.52M
  isl_int_init(t);
668
2.52M
  r = -1;
669
31.0M
  for (j = tab->n_redundant; 
j < tab->n_row31.0M
;
++j28.4M
)
{28.4M
670
28.4M
    if (
var && 28.4M
j == var->index25.7M
)
671
2.26M
      continue;
672
26.2M
    
if (26.2M
!isl_tab_var_from_row(tab, j)->is_nonneg26.2M
)
673
5.31M
      continue;
674
20.9M
    
if (20.9M
sgn * 20.9M
isl_int_sgn20.9M
(tab->mat->row[j][off + c]) >= 0)
675
18.2M
      continue;
676
2.69M
    
if (2.69M
r < 02.69M
)
{1.57M
677
1.57M
      r = j;
678
1.57M
      continue;
679
2.69M
    }
680
2.69M
    tsgn = sgn * row_cmp(tab, r, j, c, &t);
681
1.11M
    if (
tsgn < 0 || 1.11M
(tsgn == 0 &&891k
682
891k
              tab->row_var[j] < tab->row_var[r]))
683
483k
      r = j;
684
2.52M
  }
685
2.52M
  isl_int_clear(t);
686
2.52M
  return r;
687
2.52M
}
688
689
/* Find a pivot (row and col) that will increase (sgn > 0) or decrease
690
 * (sgn < 0) the value of row variable var.
691
 * If not NULL, then skip_var is a row variable that should be ignored
692
 * while looking for a pivot row.  It is usually equal to var.
693
 *
694
 * As the given row in the tableau is of the form
695
 *
696
 *  x_r = a_r0 + \sum_i a_ri x_i
697
 *
698
 * we need to find a column such that the sign of a_ri is equal to "sgn"
699
 * (such that an increase in x_i will have the desired effect) or a
700
 * column with a variable that may attain negative values.
701
 * If a_ri is positive, then we need to move x_i in the same direction
702
 * to obtain the desired effect.  Otherwise, x_i has to move in the
703
 * opposite direction.
704
 */
705
static void find_pivot(struct isl_tab *tab,
706
  struct isl_tab_var *var, struct isl_tab_var *skip_var,
707
  int sgn, int *row, int *col)
708
3.21M
{
709
3.21M
  int j, r, c;
710
3.21M
  isl_int *tr;
711
3.21M
712
3.21M
  *row = *col = -1;
713
3.21M
714
3.21M
  isl_assert(tab->mat->ctx, var->is_row, return);
715
3.21M
  tr = tab->mat->row[var->index] + 2 + tab->M;
716
3.21M
717
3.21M
  c = -1;
718
25.9M
  for (j = tab->n_dead; 
j < tab->n_col25.9M
;
++j22.7M
)
{22.7M
719
22.7M
    if (isl_int_is_zero(tr[j]))
720
17.9M
      continue;
721
4.76M
    
if (4.76M
isl_int_sgn4.76M
(tr[j]) != sgn &&4.76M
722
2.67M
        var_from_col(tab, j)->is_nonneg)
723
1.70M
      continue;
724
3.05M
    
if (3.05M
c < 0 || 3.05M
tab->col_var[j] < tab->col_var[c]743k
)
725
2.47M
      c = j;
726
3.21M
  }
727
3.21M
  if (c < 0)
728
905k
    return;
729
3.21M
730
2.30M
  
sgn *= 2.30M
isl_int_sgn2.30M
(tr[c]);
731
2.30M
  r = pivot_row(tab, skip_var, sgn, c);
732
2.30M
  *row = r < 0 ? 
var->index947k
:
r1.36M
;
733
2.30M
  *col = c;
734
3.21M
}
735
736
/* Return 1 if row "row" represents an obviously redundant inequality.
737
 * This means
738
 *  - it represents an inequality or a variable
739
 *  - that is the sum of a non-negative sample value and a positive
740
 *    combination of zero or more non-negative constraints.
741
 */
742
int isl_tab_row_is_redundant(struct isl_tab *tab, int row)
743
14.0M
{
744
14.0M
  int i;
745
14.0M
  unsigned off = 2 + tab->M;
746
14.0M
747
14.0M
  if (
tab->row_var[row] < 0 && 14.0M
!isl_tab_var_from_row(tab, row)->is_nonneg10.9M
)
748
707k
    return 0;
749
14.0M
750
13.3M
  
if (13.3M
isl_int_is_neg13.3M
(tab->mat->row[row][1]))
751
1.24M
    return 0;
752
12.1M
  
if (12.1M
tab->strict_redundant && 12.1M
isl_int_is_zero43
(tab->mat->row[row][1]))
753
42
    return 0;
754
12.1M
  
if (12.1M
tab->M && 12.1M
isl_int_is_neg33.8k
(tab->mat->row[row][2]))
755
1.80k
    return 0;
756
12.1M
757
49.9M
  
for (i = tab->n_dead; 12.1M
i < tab->n_col49.9M
;
++i37.8M
)
{48.6M
758
48.6M
    if (isl_int_is_zero(tab->mat->row[row][off + i]))
759
33.7M
      continue;
760
14.8M
    
if (14.8M
tab->col_var[i] >= 014.8M
)
761
5.74M
      return 0;
762
9.13M
    
if (9.13M
isl_int_is_neg9.13M
(tab->mat->row[row][off + i]))
763
4.95M
      return 0;
764
4.18M
    
if (4.18M
!var_from_col(tab, i)->is_nonneg4.18M
)
765
138k
      return 0;
766
12.1M
  }
767
1.28M
  return 1;
768
14.0M
}
769
770
static void swap_rows(struct isl_tab *tab, int row1, int row2)
771
1.23M
{
772
1.23M
  int t;
773
1.23M
  enum isl_tab_row_sign s;
774
1.23M
775
1.23M
  t = tab->row_var[row1];
776
1.23M
  tab->row_var[row1] = tab->row_var[row2];
777
1.23M
  tab->row_var[row2] = t;
778
1.23M
  isl_tab_var_from_row(tab, row1)->index = row1;
779
1.23M
  isl_tab_var_from_row(tab, row2)->index = row2;
780
1.23M
  tab->mat = isl_mat_swap_rows(tab->mat, row1, row2);
781
1.23M
782
1.23M
  if (!tab->row_sign)
783
1.22M
    return;
784
1.23M
  s = tab->row_sign[row1];
785
8.20k
  tab->row_sign[row1] = tab->row_sign[row2];
786
8.20k
  tab->row_sign[row2] = s;
787
1.23M
}
788
789
static int push_union(struct isl_tab *tab,
790
  enum isl_tab_undo_type type, union isl_tab_undo_val u) WARN_UNUSED;
791
static int push_union(struct isl_tab *tab,
792
  enum isl_tab_undo_type type, union isl_tab_undo_val u)
793
9.99M
{
794
9.99M
  struct isl_tab_undo *undo;
795
9.99M
796
9.99M
  if (!tab)
797
0
    return -1;
798
9.99M
  
if (9.99M
!tab->need_undo9.99M
)
799
7.32M
    return 0;
800
9.99M
801
2.67M
  
undo = 2.67M
isl_alloc_type2.67M
(tab->mat->ctx, struct isl_tab_undo);
802
2.67M
  if (!undo)
803
0
    return -1;
804
2.67M
  undo->type = type;
805
2.67M
  undo->u = u;
806
2.67M
  undo->next = tab->top;
807
2.67M
  tab->top = undo;
808
2.67M
809
2.67M
  return 0;
810
9.99M
}
811
812
int isl_tab_push_var(struct isl_tab *tab,
813
  enum isl_tab_undo_type type, struct isl_tab_var *var)
814
9.56M
{
815
9.56M
  union isl_tab_undo_val u;
816
9.56M
  if (var->is_row)
817
9.37M
    u.var_index = tab->row_var[var->index];
818
9.56M
  else
819
188k
    u.var_index = tab->col_var[var->index];
820
9.56M
  return push_union(tab, type, u);
821
9.56M
}
822
823
int isl_tab_push(struct isl_tab *tab, enum isl_tab_undo_type type)
824
385k
{
825
385k
  union isl_tab_undo_val u = { 0 };
826
385k
  return push_union(tab, type, u);
827
385k
}
828
829
/* Push a record on the undo stack describing the current basic
830
 * variables, so that the this state can be restored during rollback.
831
 */
832
int isl_tab_push_basis(struct isl_tab *tab)
833
775
{
834
775
  int i;
835
775
  union isl_tab_undo_val u;
836
775
837
775
  u.col_var = isl_alloc_array(tab->mat->ctx, int, tab->n_col);
838
775
  if (
tab->n_col && 775
!u.col_var775
)
839
0
    return -1;
840
8.92k
  
for (i = 0; 775
i < tab->n_col8.92k
;
++i8.14k
)
841
8.14k
    u.col_var[i] = tab->col_var[i];
842
775
  return push_union(tab, isl_tab_undo_saved_basis, u);
843
775
}
844
845
int isl_tab_push_callback(struct isl_tab *tab, struct isl_tab_callback *callback)
846
18.7k
{
847
18.7k
  union isl_tab_undo_val u;
848
18.7k
  u.callback = callback;
849
18.7k
  return push_union(tab, isl_tab_undo_callback, u);
850
18.7k
}
851
852
struct isl_tab *isl_tab_init_samples(struct isl_tab *tab)
853
6.71k
{
854
6.71k
  if (!tab)
855
0
    return NULL;
856
6.71k
857
6.71k
  tab->n_sample = 0;
858
6.71k
  tab->n_outside = 0;
859
6.71k
  tab->samples = isl_mat_alloc(tab->mat->ctx, 1, 1 + tab->n_var);
860
6.71k
  if (!tab->samples)
861
0
    goto error;
862
6.71k
  
tab->sample_index = 6.71k
isl_alloc_array6.71k
(tab->mat->ctx, int, 1);
863
6.71k
  if (!tab->sample_index)
864
0
    goto error;
865
6.71k
  return tab;
866
6.71k
error:
867
0
  isl_tab_free(tab);
868
6.71k
  return NULL;
869
6.71k
}
870
871
int isl_tab_add_sample(struct isl_tab *tab, __isl_take isl_vec *sample)
872
10.5k
{
873
10.5k
  if (
!tab || 10.5k
!sample10.5k
)
874
0
    goto error;
875
10.5k
876
10.5k
  
if (10.5k
tab->n_sample + 1 > tab->samples->n_row10.5k
)
{3.60k
877
3.60k
    int *t = isl_realloc_array(tab->mat->ctx,
878
3.60k
          tab->sample_index, int, tab->n_sample + 1);
879
3.60k
    if (!t)
880
0
      goto error;
881
3.60k
    tab->sample_index = t;
882
10.5k
  }
883
10.5k
884
10.5k
  tab->samples = isl_mat_extend(tab->samples,
885
10.5k
        tab->n_sample + 1, tab->samples->n_col);
886
10.5k
  if (!tab->samples)
887
0
    goto error;
888
10.5k
889
10.5k
  isl_seq_cpy(tab->samples->row[tab->n_sample], sample->el, sample->size);
890
10.5k
  isl_vec_free(sample);
891
10.5k
  tab->sample_index[tab->n_sample] = tab->n_sample;
892
10.5k
  tab->n_sample++;
893
10.5k
894
10.5k
  return 0;
895
10.5k
error:
896
0
  isl_vec_free(sample);
897
10.5k
  return -1;
898
10.5k
}
899
900
struct isl_tab *isl_tab_drop_sample(struct isl_tab *tab, int s)
901
5.96k
{
902
5.96k
  if (
s != tab->n_outside5.96k
)
{3.76k
903
3.76k
    int t = tab->sample_index[tab->n_outside];
904
3.76k
    tab->sample_index[tab->n_outside] = tab->sample_index[s];
905
3.76k
    tab->sample_index[s] = t;
906
3.76k
    isl_mat_swap_rows(tab->samples, tab->n_outside, s);
907
5.96k
  }
908
5.96k
  tab->n_outside++;
909
5.96k
  if (
isl_tab_push(tab, isl_tab_undo_drop_sample) < 05.96k
)
{0
910
0
    isl_tab_free(tab);
911
0
    return NULL;
912
5.96k
  }
913
5.96k
914
5.96k
  return tab;
915
5.96k
}
916
917
/* Record the current number of samples so that we can remove newer
918
 * samples during a rollback.
919
 */
920
int isl_tab_save_samples(struct isl_tab *tab)
921
24.4k
{
922
24.4k
  union isl_tab_undo_val u;
923
24.4k
924
24.4k
  if (!tab)
925
0
    return -1;
926
24.4k
927
24.4k
  u.n = tab->n_sample;
928
24.4k
  return push_union(tab, isl_tab_undo_saved_samples, u);
929
24.4k
}
930
931
/* Mark row with index "row" as being redundant.
932
 * If we may need to undo the operation or if the row represents
933
 * a variable of the original problem, the row is kept,
934
 * but no longer considered when looking for a pivot row.
935
 * Otherwise, the row is simply removed.
936
 *
937
 * The row may be interchanged with some other row.  If it
938
 * is interchanged with a later row, return 1.  Otherwise return 0.
939
 * If the rows are checked in order in the calling function,
940
 * then a return value of 1 means that the row with the given
941
 * row number may now contain a different row that hasn't been checked yet.
942
 */
943
int isl_tab_mark_redundant(struct isl_tab *tab, int row)
944
1.70M
{
945
1.70M
  struct isl_tab_var *var = isl_tab_var_from_row(tab, row);
946
1.70M
  var->is_redundant = 1;
947
1.70M
  isl_assert(tab->mat->ctx, row >= tab->n_redundant, return -1);
948
1.70M
  
if (1.70M
tab->preserve || 1.70M
tab->need_undo1.21M
||
tab->row_var[row] >= 01.14M
)
{1.17M
949
1.17M
    if (
tab->row_var[row] >= 0 && 1.17M
!var->is_nonneg904k
)
{897k
950
897k
      var->is_nonneg = 1;
951
897k
      if (isl_tab_push_var(tab, isl_tab_undo_nonneg, var) < 0)
952
0
        return -1;
953
1.17M
    }
954
1.17M
    
if (1.17M
row != tab->n_redundant1.17M
)
955
794k
      swap_rows(tab, row, tab->n_redundant);
956
1.17M
    tab->n_redundant++;
957
1.17M
    return isl_tab_push_var(tab, isl_tab_undo_redundant, var);
958
1.70M
  } else {
959
532k
    if (row != tab->n_row - 1)
960
326k
      swap_rows(tab, row, tab->n_row - 1);
961
532k
    isl_tab_var_from_row(tab, tab->n_row - 1)->index = -1;
962
532k
    tab->n_row--;
963
532k
    return 1;
964
1.70M
  }
965
1.70M
}
966
967
/* Mark "tab" as a rational tableau.
968
 * If it wasn't marked as a rational tableau already and if we may
969
 * need to undo changes, then arrange for the marking to be undone
970
 * during the undo.
971
 */
972
int isl_tab_mark_rational(struct isl_tab *tab)
973
10.2k
{
974
10.2k
  if (!tab)
975
0
    return -1;
976
10.2k
  
if (10.2k
!tab->rational && 10.2k
tab->need_undo10.1k
)
977
10.1k
    
if (10.1k
isl_tab_push(tab, isl_tab_undo_rational) < 010.1k
)
978
0
      return -1;
979
10.2k
  tab->rational = 1;
980
10.2k
  return 0;
981
10.2k
}
982
983
isl_stat isl_tab_mark_empty(struct isl_tab *tab)
984
66.1k
{
985
66.1k
  if (!tab)
986
0
    return isl_stat_error;
987
66.1k
  
if (66.1k
!tab->empty && 66.1k
tab->need_undo65.4k
)
988
55.4k
    
if (55.4k
isl_tab_push(tab, isl_tab_undo_empty) < 055.4k
)
989
0
      return isl_stat_error;
990
66.1k
  tab->empty = 1;
991
66.1k
  return isl_stat_ok;
992
66.1k
}
993
994
int isl_tab_freeze_constraint(struct isl_tab *tab, int con)
995
354k
{
996
354k
  struct isl_tab_var *var;
997
354k
998
354k
  if (!tab)
999
0
    return -1;
1000
354k
1001
354k
  var = &tab->con[con];
1002
354k
  if (var->frozen)
1003
0
    return 0;
1004
354k
  
if (354k
var->index < 0354k
)
1005
25.4k
    return 0;
1006
354k
  var->frozen = 1;
1007
328k
1008
328k
  if (tab->need_undo)
1009
300k
    return isl_tab_push_var(tab, isl_tab_undo_freeze, var);
1010
328k
1011
27.9k
  return 0;
1012
354k
}
1013
1014
/* Update the rows signs after a pivot of "row" and "col", with "row_sgn"
1015
 * the original sign of the pivot element.
1016
 * We only keep track of row signs during PILP solving and in this case
1017
 * we only pivot a row with negative sign (meaning the value is always
1018
 * non-positive) using a positive pivot element.
1019
 *
1020
 * For each row j, the new value of the parametric constant is equal to
1021
 *
1022
 *  a_j0 - a_jc a_r0/a_rc
1023
 *
1024
 * where a_j0 is the original parametric constant, a_rc is the pivot element,
1025
 * a_r0 is the parametric constant of the pivot row and a_jc is the
1026
 * pivot column entry of the row j.
1027
 * Since a_r0 is non-positive and a_rc is positive, the sign of row j
1028
 * remains the same if a_jc has the same sign as the row j or if
1029
 * a_jc is zero.  In all other cases, we reset the sign to "unknown".
1030
 */
1031
static void update_row_sign(struct isl_tab *tab, int row, int col, int row_sgn)
1032
2.46M
{
1033
2.46M
  int i;
1034
2.46M
  struct isl_mat *mat = tab->mat;
1035
2.46M
  unsigned off = 2 + tab->M;
1036
2.46M
1037
2.46M
  if (!tab->row_sign)
1038
2.44M
    return;
1039
2.46M
1040
23.1k
  
if (23.1k
tab->row_sign[row] == 023.1k
)
1041
17.8k
    return;
1042
5.23k
  
isl_assert5.23k
(mat->ctx, row_sgn > 0, return);5.23k
1043
5.23k
  
isl_assert5.23k
(mat->ctx, tab->row_sign[row] == isl_tab_row_neg, return);5.23k
1044
5.23k
  tab->row_sign[row] = isl_tab_row_pos;
1045
47.8k
  for (i = 0; 
i < tab->n_row47.8k
;
++i42.6k
)
{42.6k
1046
42.6k
    int s;
1047
42.6k
    if (i == row)
1048
5.23k
      continue;
1049
37.3k
    
s = 37.3k
isl_int_sgn37.3k
(mat->row[i][off + col]);
1050
37.3k
    if (!s)
1051
21.0k
      continue;
1052
16.3k
    
if (16.3k
!tab->row_sign[i]16.3k
)
1053
6.03k
      continue;
1054
10.3k
    
if (10.3k
s < 0 && 10.3k
tab->row_sign[i] == isl_tab_row_neg5.81k
)
1055
0
      continue;
1056
10.3k
    
if (10.3k
s > 0 && 10.3k
tab->row_sign[i] == isl_tab_row_pos4.52k
)
1057
4.52k
      continue;
1058
10.3k
    tab->row_sign[i] = isl_tab_row_unknown;
1059
5.81k
  }
1060
2.46M
}
1061
1062
/* Given a row number "row" and a column number "col", pivot the tableau
1063
 * such that the associated variables are interchanged.
1064
 * The given row in the tableau expresses
1065
 *
1066
 *  x_r = a_r0 + \sum_i a_ri x_i
1067
 *
1068
 * or
1069
 *
1070
 *  x_c = 1/a_rc x_r - a_r0/a_rc + sum_{i \ne r} -a_ri/a_rc
1071
 *
1072
 * Substituting this equality into the other rows
1073
 *
1074
 *  x_j = a_j0 + \sum_i a_ji x_i
1075
 *
1076
 * with a_jc \ne 0, we obtain
1077
 *
1078
 *  x_j = a_jc/a_rc x_r + a_j0 - a_jc a_r0/a_rc + sum a_ji - a_jc a_ri/a_rc 
1079
 *
1080
 * The tableau
1081
 *
1082
 *  n_rc/d_r    n_ri/d_r
1083
 *  n_jc/d_j    n_ji/d_j
1084
 *
1085
 * where i is any other column and j is any other row,
1086
 * is therefore transformed into
1087
 *
1088
 * s(n_rc)d_r/|n_rc|    -s(n_rc)n_ri/|n_rc|
1089
 * s(n_rc)d_r n_jc/(|n_rc| d_j) (n_ji |n_rc| - s(n_rc)n_jc n_ri)/(|n_rc| d_j)
1090
 *
1091
 * The transformation is performed along the following steps
1092
 *
1093
 *  d_r/n_rc    n_ri/n_rc
1094
 *  n_jc/d_j    n_ji/d_j
1095
 *
1096
 *  s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc|
1097
 *  n_jc/d_j    n_ji/d_j
1098
 *
1099
 *  s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc|
1100
 *  n_jc/(|n_rc| d_j) n_ji/(|n_rc| d_j)
1101
 *
1102
 *  s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc|
1103
 *  n_jc/(|n_rc| d_j) (n_ji |n_rc|)/(|n_rc| d_j)
1104
 *
1105
 *  s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc|
1106
 *  n_jc/(|n_rc| d_j) (n_ji |n_rc| - s(n_rc)n_jc n_ri)/(|n_rc| d_j)
1107
 *
1108
 * s(n_rc)d_r/|n_rc|    -s(n_rc)n_ri/|n_rc|
1109
 * s(n_rc)d_r n_jc/(|n_rc| d_j) (n_ji |n_rc| - s(n_rc)n_jc n_ri)/(|n_rc| d_j)
1110
 *
1111
 */
1112
int isl_tab_pivot(struct isl_tab *tab, int row, int col)
1113
2.46M
{
1114
2.46M
  int i, j;
1115
2.46M
  int sgn;
1116
2.46M
  int t;
1117
2.46M
  isl_ctx *ctx;
1118
2.46M
  struct isl_mat *mat = tab->mat;
1119
2.46M
  struct isl_tab_var *var;
1120
2.46M
  unsigned off = 2 + tab->M;
1121
2.46M
1122
2.46M
  ctx = isl_tab_get_ctx(tab);
1123
2.46M
  if (isl_ctx_next_operation(ctx) < 0)
1124
0
    return -1;
1125
2.46M
1126
2.46M
  
isl_int_swap2.46M
(mat->row[row][0], mat->row[row][off + col]);2.46M
1127
2.46M
  sgn = isl_int_sgn(mat->row[row][0]);
1128
2.46M
  if (
sgn < 02.46M
)
{1.32M
1129
1.32M
    isl_int_neg(mat->row[row][0], mat->row[row][0]);
1130
1.32M
    isl_int_neg(mat->row[row][off + col], mat->row[row][off + col]);
1131
2.46M
  } else
1132
9.44M
    
for (j = 0; 1.14M
j < off - 1 + tab->n_col9.44M
;
++j8.29M
)
{8.29M
1133
8.29M
      if (j == off - 1 + col)
1134
1.14M
        continue;
1135
7.14M
      
isl_int_neg7.14M
(mat->row[row][1 + j], mat->row[row][1 + j]);7.14M
1136
7.14M
    }
1137
2.46M
  if (
!2.46M
isl_int_is_one2.46M
(mat->row[row][0]))
1138
439k
    isl_seq_normalize(mat->ctx, mat->row[row], off + tab->n_col);
1139
28.6M
  for (i = 0; 
i < tab->n_row28.6M
;
++i26.2M
)
{26.2M
1140
26.2M
    if (i == row)
1141
2.46M
      continue;
1142
23.7M
    
if (23.7M
isl_int_is_zero23.7M
(mat->row[i][off + col]))
1143
17.1M
      continue;
1144
6.64M
    
isl_int_mul6.64M
(mat->row[i][0], mat->row[i][0], mat->row[row][0]);6.64M
1145
71.9M
    for (j = 0; 
j < off - 1 + tab->n_col71.9M
;
++j65.3M
)
{65.3M
1146
65.3M
      if (j == off - 1 + col)
1147
6.64M
        continue;
1148
58.6M
      
isl_int_mul58.6M
(mat->row[i][1 + j],58.6M
1149
58.6M
            mat->row[i][1 + j], mat->row[row][0]);
1150
58.6M
      isl_int_addmul(mat->row[i][1 + j],
1151
58.6M
            mat->row[i][off + col], mat->row[row][1 + j]);
1152
58.6M
    }
1153
6.64M
    isl_int_mul(mat->row[i][off + col],
1154
6.64M
          mat->row[i][off + col], mat->row[row][off + col]);
1155
6.64M
    if (
!6.64M
isl_int_is_one6.64M
(mat->row[i][0]))
1156
3.11M
      isl_seq_normalize(mat->ctx, mat->row[i], off + tab->n_col);
1157
6.64M
  }
1158
2.46M
  t = tab->row_var[row];
1159
2.46M
  tab->row_var[row] = tab->col_var[col];
1160
2.46M
  tab->col_var[col] = t;
1161
2.46M
  var = isl_tab_var_from_row(tab, row);
1162
2.46M
  var->is_row = 1;
1163
2.46M
  var->index = row;
1164
2.46M
  var = var_from_col(tab, col);
1165
2.46M
  var->is_row = 0;
1166
2.46M
  var->index = col;
1167
2.46M
  update_row_sign(tab, row, col, sgn);
1168
2.46M
  if (tab->in_undo)
1169
73.2k
    return 0;
1170
23.3M
  
for (i = tab->n_redundant; 2.39M
i < tab->n_row23.3M
;
++i20.9M
)
{20.9M
1171
20.9M
    if (isl_int_is_zero(mat->row[i][off + col]))
1172
12.7M
      continue;
1173
8.20M
    
if (8.20M
!isl_tab_var_from_row(tab, i)->frozen &&8.20M
1174
8.20M
        
isl_tab_row_is_redundant(tab, i)7.94M
)
{1.18M
1175
1.18M
      int redo = isl_tab_mark_redundant(tab, i);
1176
1.18M
      if (redo < 0)
1177
0
        return -1;
1178
1.18M
      
if (1.18M
redo1.18M
)
1179
98.2k
        --i;
1180
8.20M
    }
1181
8.20M
  }
1182
2.39M
  return 0;
1183
2.46M
}
1184
1185
/* If "var" represents a column variable, then pivot is up (sgn > 0)
1186
 * or down (sgn < 0) to a row.  The variable is assumed not to be
1187
 * unbounded in the specified direction.
1188
 * If sgn = 0, then the variable is unbounded in both directions,
1189
 * and we pivot with any row we can find.
1190
 */
1191
static int to_row(struct isl_tab *tab, struct isl_tab_var *var, int sign) WARN_UNUSED;
1192
static int to_row(struct isl_tab *tab, struct isl_tab_var *var, int sign)
1193
1.23M
{
1194
1.23M
  int r;
1195
1.23M
  unsigned off = 2 + tab->M;
1196
1.23M
1197
1.23M
  if (var->is_row)
1198
1.07M
    return 0;
1199
1.23M
1200
161k
  
if (161k
sign == 0161k
)
{17.7k
1201
47.2k
    for (r = tab->n_redundant; 
r < tab->n_row47.2k
;
++r29.5k
)
1202
47.2k
      
if (47.2k
!47.2k
isl_int_is_zero47.2k
(tab->mat->row[r][off+var->index]))
1203
17.7k
        break;
1204
17.7k
    isl_assert(tab->mat->ctx, r < tab->n_row, return -1);
1205
161k
  } else {
1206
143k
    r = pivot_row(tab, NULL, sign, var->index);
1207
143k
    isl_assert(tab->mat->ctx, r >= 0, return -1);
1208
161k
  }
1209
161k
1210
161k
  return isl_tab_pivot(tab, r, var->index);
1211
1.23M
}
1212
1213
/* Check whether all variables that are marked as non-negative
1214
 * also have a non-negative sample value.  This function is not
1215
 * called from the current code but is useful during debugging.
1216
 */
1217
static void check_table(struct isl_tab *tab) __attribute__ ((unused));
1218
static void check_table(struct isl_tab *tab)
1219
0
{
1220
0
  int i;
1221
0
1222
0
  if (tab->empty)
1223
0
    return;
1224
0
  for (i = tab->n_redundant; i < tab->n_row; ++i) {
1225
0
    struct isl_tab_var *var;
1226
0
    var = isl_tab_var_from_row(tab, i);
1227
0
    if (!var->is_nonneg)
1228
0
      continue;
1229
0
    if (tab->M) {
1230
0
      isl_assert(tab->mat->ctx,
1231
0
        !isl_int_is_neg(tab->mat->row[i][2]), abort());
1232
0
      if (isl_int_is_pos(tab->mat->row[i][2]))
1233
0
        continue;
1234
0
    }
1235
0
    isl_assert(tab->mat->ctx, !isl_int_is_neg(tab->mat->row[i][1]),
1236
0
        abort());
1237
0
  }
1238
0
}
1239
1240
/* Return the sign of the maximal value of "var".
1241
 * If the sign is not negative, then on return from this function,
1242
 * the sample value will also be non-negative.
1243
 *
1244
 * If "var" is manifestly unbounded wrt positive values, we are done.
1245
 * Otherwise, we pivot the variable up to a row if needed
1246
 * Then we continue pivoting down until either
1247
 *  - no more down pivots can be performed
1248
 *  - the sample value is positive
1249
 *  - the variable is pivoted into a manifestly unbounded column
1250
 */
1251
static int sign_of_max(struct isl_tab *tab, struct isl_tab_var *var)
1252
986k
{
1253
986k
  int row, col;
1254
986k
1255
986k
  if (max_is_manifestly_unbounded(tab, var))
1256
90.7k
    return 1;
1257
895k
  
if (895k
to_row(tab, var, 1) < 0895k
)
1258
0
    return -2;
1259
1.50M
  
while (895k
!1.50M
isl_int_is_pos1.50M
(tab->mat->row[var->index][1]))
{1.21M
1260
1.21M
    find_pivot(tab, var, var, 1, &row, &col);
1261
1.21M
    if (row == -1)
1262
403k
      
return 403k
isl_int_sgn403k
(tab->mat->row[var->index][1]);
1263
810k
    
if (810k
isl_tab_pivot(tab, row, col) < 0810k
)
1264
0
      return -2;
1265
810k
    
if (810k
!var->is_row810k
) /* manifestly unbounded */
1266
202k
      return 1;
1267
895k
  }
1268
290k
  return 1;
1269
986k
}
1270
1271
int isl_tab_sign_of_max(struct isl_tab *tab, int con)
1272
130
{
1273
130
  struct isl_tab_var *var;
1274
130
1275
130
  if (!tab)
1276
0
    return -2;
1277
130
1278
130
  var = &tab->con[con];
1279
130
  isl_assert(tab->mat->ctx, !var->is_redundant, return -2);
1280
130
  
isl_assert130
(tab->mat->ctx, !var->is_zero, return -2);130
1281
130
1282
130
  return sign_of_max(tab, var);
1283
130
}
1284
1285
static int row_is_neg(struct isl_tab *tab, int row)
1286
3.97M
{
1287
3.97M
  if (!tab->M)
1288
3.97M
    
return 3.97M
isl_int_is_neg3.97M
(tab->mat->row[row][1]);
1289
0
  
if (0
isl_int_is_pos0
(tab->mat->row[row][2]))
1290
0
    return 0;
1291
0
  
if (0
isl_int_is_neg0
(tab->mat->row[row][2]))
1292
0
    return 1;
1293
0
  
return 0
isl_int_is_neg0
(tab->mat->row[row][1]);
1294
3.97M
}
1295
1296
static int row_sgn(struct isl_tab *tab, int row)
1297
3.47M
{
1298
3.47M
  if (!tab->M)
1299
3.47M
    
return 3.47M
isl_int_sgn3.47M
(tab->mat->row[row][1]);
1300
0
  
if (0
!0
isl_int_is_zero0
(tab->mat->row[row][2]))
1301
0
    
return 0
isl_int_sgn0
(tab->mat->row[row][2]);
1302
0
  else
1303
0
    
return 0
isl_int_sgn0
(tab->mat->row[row][1]);
1304
3.47M
}
1305
1306
/* Perform pivots until the row variable "var" has a non-negative
1307
 * sample value or until no more upward pivots can be performed.
1308
 * Return the sign of the sample value after the pivots have been
1309
 * performed.
1310
 */
1311
static int restore_row(struct isl_tab *tab, struct isl_tab_var *var)
1312
3.79M
{
1313
3.79M
  int row, col;
1314
3.79M
1315
3.97M
  while (
row_is_neg(tab, var->index)3.97M
)
{565k
1316
565k
    find_pivot(tab, var, var, 1, &row, &col);
1317
565k
    if (row == -1)
1318
63.0k
      break;
1319
502k
    
if (502k
isl_tab_pivot(tab, row, col) < 0502k
)
1320
0
      return -2;
1321
502k
    
if (502k
!var->is_row502k
) /* manifestly unbounded */
1322
325k
      return 1;
1323
3.79M
  }
1324
3.47M
  return row_sgn(tab, var->index);
1325
3.79M
}
1326
1327
/* Perform pivots until we are sure that the row variable "var"
1328
 * can attain non-negative values.  After return from this
1329
 * function, "var" is still a row variable, but its sample
1330
 * value may not be non-negative, even if the function returns 1.
1331
 */
1332
static int at_least_zero(struct isl_tab *tab, struct isl_tab_var *var)
1333
143k
{
1334
143k
  int row, col;
1335
143k
1336
160k
  while (
isl_int_is_neg160k
(tab->mat->row[var->index][1]))
{153k
1337
153k
    find_pivot(tab, var, var, 1, &row, &col);
1338
153k
    if (row == -1)
1339
67.5k
      break;
1340
85.4k
    
if (85.4k
row == var->index85.4k
) /* manifestly unbounded */
1341
68.0k
      return 1;
1342
17.3k
    
if (17.3k
isl_tab_pivot(tab, row, col) < 017.3k
)
1343
0
      return -1;
1344
143k
  }
1345
75.3k
  
return !75.3k
isl_int_is_neg75.3k
(tab->mat->row[var->index][1]);
1346
143k
}
1347
1348
/* Return a negative value if "var" can attain negative values.
1349
 * Return a non-negative value otherwise.
1350
 *
1351
 * If "var" is manifestly unbounded wrt negative values, we are done.
1352
 * Otherwise, if var is in a column, we can pivot it down to a row.
1353
 * Then we continue pivoting down until either
1354
 *  - the pivot would result in a manifestly unbounded column
1355
 *    => we don't perform the pivot, but simply return -1
1356
 *  - no more down pivots can be performed
1357
 *  - the sample value is negative
1358
 * If the sample value becomes negative and the variable is supposed
1359
 * to be nonnegative, then we undo the last pivot.
1360
 * However, if the last pivot has made the pivoting variable
1361
 * obviously redundant, then it may have moved to another row.
1362
 * In that case we look for upward pivots until we reach a non-negative
1363
 * value again.
1364
 */
1365
static int sign_of_min(struct isl_tab *tab, struct isl_tab_var *var)
1366
70.5k
{
1367
70.5k
  int row, col;
1368
70.5k
  struct isl_tab_var *pivot_var = NULL;
1369
70.5k
1370
70.5k
  if (min_is_manifestly_unbounded(tab, var))
1371
0
    return -1;
1372
70.5k
  
if (70.5k
!var->is_row70.5k
)
{1.86k
1373
1.86k
    col = var->index;
1374
1.86k
    row = pivot_row(tab, NULL, -1, col);
1375
1.86k
    pivot_var = var_from_col(tab, col);
1376
1.86k
    if (isl_tab_pivot(tab, row, col) < 0)
1377
0
      return -2;
1378
1.86k
    
if (1.86k
var->is_redundant1.86k
)
1379
317
      return 0;
1380
1.54k
    
if (1.54k
isl_int_is_neg1.54k
(tab->mat->row[var->index][1]))
{693
1381
693
      if (
var->is_nonneg693
)
{693
1382
693
        if (!pivot_var->is_redundant &&
1383
693
            
pivot_var->index == row693
)
{680
1384
680
          if (isl_tab_pivot(tab, row, col) < 0)
1385
0
            return -2;
1386
693
        } else
1387
13
          
if (13
restore_row(tab, var) < -113
)
1388
0
            return -2;
1389
693
      }
1390
693
      return -1;
1391
1.54k
    }
1392
70.5k
  }
1393
69.5k
  
if (69.5k
var->is_redundant69.5k
)
1394
0
    return 0;
1395
106k
  
while (69.5k
!106k
isl_int_is_neg106k
(tab->mat->row[var->index][1]))
{93.6k
1396
93.6k
    find_pivot(tab, var, var, -1, &row, &col);
1397
93.6k
    if (row == var->index)
1398
16.2k
      return -1;
1399
77.4k
    
if (77.4k
row == -177.4k
)
1400
38.7k
      
return 38.7k
isl_int_sgn38.7k
(tab->mat->row[var->index][1]);
1401
77.4k
    pivot_var = var_from_col(tab, col);
1402
38.6k
    if (isl_tab_pivot(tab, row, col) < 0)
1403
0
      return -2;
1404
38.6k
    
if (38.6k
var->is_redundant38.6k
)
1405
1.14k
      return 0;
1406
69.5k
  }
1407
13.3k
  
if (13.3k
pivot_var && 13.3k
var->is_nonneg13.3k
)
{968
1408
968
    /* pivot back to non-negative value */
1409
968
    if (
!pivot_var->is_redundant && 968
pivot_var->index == row968
)
{955
1410
955
      if (isl_tab_pivot(tab, row, col) < 0)
1411
0
        return -2;
1412
968
    } else
1413
13
      
if (13
restore_row(tab, var) < -113
)
1414
0
        return -2;
1415
13.3k
  }
1416
13.3k
  return -1;
1417
70.5k
}
1418
1419
static int row_at_most_neg_one(struct isl_tab *tab, int row)
1420
228k
{
1421
228k
  if (
tab->M228k
)
{0
1422
0
    if (isl_int_is_pos(tab->mat->row[row][2]))
1423
0
      return 0;
1424
0
    
if (0
isl_int_is_neg0
(tab->mat->row[row][2]))
1425
0
      return 1;
1426
228k
  }
1427
228k
  
return 228k
isl_int_is_neg228k
(tab->mat->row[row][1]) &&
1428
124k
         isl_int_abs_ge(tab->mat->row[row][1],
1429
228k
            tab->mat->row[row][0]);
1430
228k
}
1431
1432
/* Return 1 if "var" can attain values <= -1.
1433
 * Return 0 otherwise.
1434
 *
1435
 * If the variable "var" is supposed to be non-negative (is_nonneg is set),
1436
 * then the sample value of "var" is assumed to be non-negative when the
1437
 * the function is called.  If 1 is returned then the constraint
1438
 * is not redundant and the sample value is made non-negative again before
1439
 * the function returns.
1440
 */
1441
int isl_tab_min_at_most_neg_one(struct isl_tab *tab, struct isl_tab_var *var)
1442
680k
{
1443
680k
  int row, col;
1444
680k
  struct isl_tab_var *pivot_var;
1445
680k
1446
680k
  if (min_is_manifestly_unbounded(tab, var))
1447
361
    return 1;
1448
680k
  
if (680k
!var->is_row680k
)
{70.6k
1449
70.6k
    col = var->index;
1450
70.6k
    row = pivot_row(tab, NULL, -1, col);
1451
70.6k
    pivot_var = var_from_col(tab, col);
1452
70.6k
    if (isl_tab_pivot(tab, row, col) < 0)
1453
0
      return -1;
1454
70.6k
    
if (70.6k
var->is_redundant70.6k
)
1455
10.1k
      return 0;
1456
60.4k
    
if (60.4k
row_at_most_neg_one(tab, var->index)60.4k
)
{44.2k
1457
44.2k
      if (
var->is_nonneg44.2k
)
{44.2k
1458
44.2k
        if (!pivot_var->is_redundant &&
1459
44.2k
            
pivot_var->index == row44.2k
)
{41.6k
1460
41.6k
          if (isl_tab_pivot(tab, row, col) < 0)
1461
0
            return -1;
1462
44.2k
        } else
1463
2.64k
          
if (2.64k
restore_row(tab, var) < -12.64k
)
1464
0
            return -1;
1465
44.2k
      }
1466
44.2k
      return 1;
1467
60.4k
    }
1468
680k
  }
1469
626k
  
if (626k
var->is_redundant626k
)
1470
9.49k
    return 0;
1471
616k
  
do 616k
{727k
1472
727k
    find_pivot(tab, var, var, -1, &row, &col);
1473
727k
    if (
row == var->index727k
)
{328k
1474
328k
      if (
var->is_nonneg && 328k
restore_row(tab, var) < -1280k
)
1475
0
        return -1;
1476
328k
      return 1;
1477
727k
    }
1478
398k
    
if (398k
row == -1398k
)
1479
152k
      return 0;
1480
398k
    pivot_var = var_from_col(tab, col);
1481
246k
    if (isl_tab_pivot(tab, row, col) < 0)
1482
0
      return -1;
1483
246k
    
if (246k
var->is_redundant246k
)
1484
79.0k
      return 0;
1485
616k
  } while (!row_at_most_neg_one(tab, var->index));
1486
56.7k
  
if (56.7k
var->is_nonneg56.7k
)
{47.3k
1487
47.3k
    /* pivot back to non-negative value */
1488
47.3k
    if (
!pivot_var->is_redundant && 47.3k
pivot_var->index == row47.3k
)
1489
44.3k
      
if (44.3k
isl_tab_pivot(tab, row, col) < 044.3k
)
1490
0
        return -1;
1491
47.3k
    
if (47.3k
restore_row(tab, var) < -147.3k
)
1492
0
      return -1;
1493
56.7k
  }
1494
56.7k
  return 1;
1495
680k
}
1496
1497
/* Return 1 if "var" can attain values >= 1.
1498
 * Return 0 otherwise.
1499
 */
1500
static int at_least_one(struct isl_tab *tab, struct isl_tab_var *var)
1501
558k
{
1502
558k
  int row, col;
1503
558k
  isl_int *r;
1504
558k
1505
558k
  if (max_is_manifestly_unbounded(tab, var))
1506
292k
    return 1;
1507
266k
  
if (266k
to_row(tab, var, 1) < 0266k
)
1508
0
    return -1;
1509
266k
  r = tab->mat->row[var->index];
1510
273k
  while (
isl_int_lt273k
(r[1], r[0]))
{8.32k
1511
8.32k
    find_pivot(tab, var, var, 1, &row, &col);
1512
8.32k
    if (row == -1)
1513
405
      
return 405
isl_int_ge405
(r[1], r[0]);
1514
7.91k
    
if (7.91k
row == var->index7.91k
) /* manifestly unbounded */
1515
84
      return 1;
1516
7.83k
    
if (7.83k
isl_tab_pivot(tab, row, col) < 07.83k
)
1517
0
      return -1;
1518
266k
  }
1519
265k
  return 1;
1520
558k
}
1521
1522
static void swap_cols(struct isl_tab *tab, int col1, int col2)
1523
450k
{
1524
450k
  int t;
1525
450k
  unsigned off = 2 + tab->M;
1526
450k
  t = tab->col_var[col1];
1527
450k
  tab->col_var[col1] = tab->col_var[col2];
1528
450k
  tab->col_var[col2] = t;
1529
450k
  var_from_col(tab, col1)->index = col1;
1530
450k
  var_from_col(tab, col2)->index = col2;
1531
450k
  tab->mat = isl_mat_swap_cols(tab->mat, off + col1, off + col2);
1532
450k
}
1533
1534
/* Mark column with index "col" as representing a zero variable.
1535
 * If we may need to undo the operation the column is kept,
1536
 * but no longer considered.
1537
 * Otherwise, the column is simply removed.
1538
 *
1539
 * The column may be interchanged with some other column.  If it
1540
 * is interchanged with a later column, return 1.  Otherwise return 0.
1541
 * If the columns are checked in order in the calling function,
1542
 * then a return value of 1 means that the column with the given
1543
 * column number may now contain a different column that
1544
 * hasn't been checked yet.
1545
 */
1546
int isl_tab_kill_col(struct isl_tab *tab, int col)
1547
652k
{
1548
652k
  var_from_col(tab, col)->is_zero = 1;
1549
652k
  if (
tab->need_undo652k
)
{51.8k
1550
51.8k
    if (isl_tab_push_var(tab, isl_tab_undo_zero,
1551
51.8k
              var_from_col(tab, col)) < 0)
1552
0
      return -1;
1553
51.8k
    
if (51.8k
col != tab->n_dead51.8k
)
1554
19.5k
      swap_cols(tab, col, tab->n_dead);
1555
51.8k
    tab->n_dead++;
1556
51.8k
    return 0;
1557
652k
  } else {
1558
600k
    if (col != tab->n_col - 1)
1559
430k
      swap_cols(tab, col, tab->n_col - 1);
1560
600k
    var_from_col(tab, tab->n_col - 1)->index = -1;
1561
600k
    tab->n_col--;
1562
600k
    return 1;
1563
652k
  }
1564
652k
}
1565
1566
static int row_is_manifestly_non_integral(struct isl_tab *tab, int row)
1567
2.38M
{
1568
2.38M
  unsigned off = 2 + tab->M;
1569
2.38M
1570
2.38M
  if (
tab->M && 2.38M
!0
isl_int_eq0
(tab->mat->row[row][2],
1571
2.38M
          tab->mat->row[row][0]))
1572
0
    return 0;
1573
2.38M
  
if (2.38M
isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,2.38M
1574
2.38M
            tab->n_col - tab->n_dead) != -1)
1575
139k
    return 0;
1576
2.38M
1577
2.24M
  
return !2.24M
isl_int_is_divisible_by2.24M
(tab->mat->row[row][1],
1578
2.38M
          tab->mat->row[row][0]);
1579
2.38M
}
1580
1581
/* For integer tableaus, check if any of the coordinates are stuck
1582
 * at a non-integral value.
1583
 */
1584
static int tab_is_manifestly_empty(struct isl_tab *tab)
1585
402k
{
1586
402k
  int i;
1587
402k
1588
402k
  if (tab->empty)
1589
0
    return 1;
1590
402k
  
if (402k
tab->rational402k
)
1591
12.2k
    return 0;
1592
402k
1593
5.10M
  
for (i = 0; 390k
i < tab->n_var5.10M
;
++i4.71M
)
{4.71M
1594
4.71M
    if (!tab->var[i].is_row)
1595
2.32M
      continue;
1596
2.38M
    
if (2.38M
row_is_manifestly_non_integral(tab, tab->var[i].index)2.38M
)
1597
34
      return 1;
1598
2.38M
  }
1599
390k
1600
390k
  return 0;
1601
402k
}
1602
1603
/* Row variable "var" is non-negative and cannot attain any values
1604
 * larger than zero.  This means that the coefficients of the unrestricted
1605
 * column variables are zero and that the coefficients of the non-negative
1606
 * column variables are zero or negative.
1607
 * Each of the non-negative variables with a negative coefficient can
1608
 * then also be written as the negative sum of non-negative variables
1609
 * and must therefore also be zero.
1610
 *
1611
 * If "temp_var" is set, then "var" is a temporary variable that
1612
 * will be removed after this function returns and for which
1613
 * no information is recorded on the undo stack.
1614
 * Do not add any undo records involving this variable in this case
1615
 * since the variable will have been removed before any future undo
1616
 * operations.  Also avoid marking the variable as redundant,
1617
 * since that either adds an undo record or needlessly removes the row
1618
 * (the caller will take care of removing the row).
1619
 */
1620
static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var,
1621
  int temp_var) WARN_UNUSED;
1622
static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var,
1623
  int temp_var)
1624
402k
{
1625
402k
  int j;
1626
402k
  struct isl_mat *mat = tab->mat;
1627
402k
  unsigned off = 2 + tab->M;
1628
402k
1629
402k
  if (!var->is_nonneg)
1630
0
    isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1631
402k
      "expecting non-negative variable",
1632
402k
      return isl_stat_error);
1633
402k
  var->is_zero = 1;
1634
402k
  if (
!temp_var && 402k
tab->need_undo390k
)
1635
392
    
if (392
isl_tab_push_var(tab, isl_tab_undo_zero, var) < 0392
)
1636
0
      return isl_stat_error;
1637
3.20M
  
for (j = tab->n_dead; 402k
j < tab->n_col3.20M
;
++j2.80M
)
{2.80M
1638
2.80M
    int recheck;
1639
2.80M
    if (isl_int_is_zero(mat->row[var->index][off + j]))
1640
2.43M
      continue;
1641
366k
    
if (366k
isl_int_is_pos366k
(mat->row[var->index][off + j]))
1642
0
      isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1643
366k
        "row cannot have positive coefficients",
1644
366k
        return isl_stat_error);
1645
366k
    recheck = isl_tab_kill_col(tab, j);
1646
366k
    if (recheck < 0)
1647
0
      return isl_stat_error;
1648
366k
    
if (366k
recheck366k
)
1649
353k
      --j;
1650
402k
  }
1651
402k
  
if (402k
!temp_var && 402k
isl_tab_mark_redundant(tab, var->index) < 0390k
)
1652
0
    return isl_stat_error;
1653
402k
  
if (402k
tab_is_manifestly_empty(tab) && 402k
isl_tab_mark_empty(tab) < 034
)
1654
0
    return isl_stat_error;
1655
402k
  return isl_stat_ok;
1656
402k
}
1657
1658
/* Add a constraint to the tableau and allocate a row for it.
1659
 * Return the index into the constraint array "con".
1660
 *
1661
 * This function assumes that at least one more row and at least
1662
 * one more element in the constraint array are available in the tableau.
1663
 */
1664
int isl_tab_allocate_con(struct isl_tab *tab)
1665
4.00M
{
1666
4.00M
  int r;
1667
4.00M
1668
4.00M
  isl_assert(tab->mat->ctx, tab->n_row < tab->mat->n_row, return -1);
1669
4.00M
  
isl_assert4.00M
(tab->mat->ctx, tab->n_con < tab->max_con, return -1);4.00M
1670
4.00M
1671
4.00M
  r = tab->n_con;
1672
4.00M
  tab->con[r].index = tab->n_row;
1673
4.00M
  tab->con[r].is_row = 1;
1674
4.00M
  tab->con[r].is_nonneg = 0;
1675
4.00M
  tab->con[r].is_zero = 0;
1676
4.00M
  tab->con[r].is_redundant = 0;
1677
4.00M
  tab->con[r].frozen = 0;
1678
4.00M
  tab->con[r].negated = 0;
1679
4.00M
  tab->row_var[tab->n_row] = ~r;
1680
4.00M
1681
4.00M
  tab->n_row++;
1682
4.00M
  tab->n_con++;
1683
4.00M
  if (isl_tab_push_var(tab, isl_tab_undo_allocate, &tab->con[r]) < 0)
1684
0
    return -1;
1685
4.00M
1686
4.00M
  return r;
1687
4.00M
}
1688
1689
/* Move the entries in tab->var up one position, starting at "first",
1690
 * creating room for an extra entry at position "first".
1691
 * Since some of the entries of tab->row_var and tab->col_var contain
1692
 * indices into this array, they have to be updated accordingly.
1693
 */
1694
static int var_insert_entry(struct isl_tab *tab, int first)
1695
5.58k
{
1696
5.58k
  int i;
1697
5.58k
1698
5.58k
  if (tab->n_var >= tab->max_var)
1699
0
    isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1700
5.58k
      "not enough room for new variable", return -1);
1701
5.58k
  
if (5.58k
first > tab->n_var5.58k
)
1702
0
    isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1703
5.58k
      "invalid initial position", return -1);
1704
5.58k
1705
6.36k
  
for (i = tab->n_var - 1; 5.58k
i >= first6.36k
;
--i785
)
{785
1706
785
    tab->var[i + 1] = tab->var[i];
1707
785
    if (tab->var[i + 1].is_row)
1708
527
      tab->row_var[tab->var[i + 1].index]++;
1709
785
    else
1710
258
      tab->col_var[tab->var[i + 1].index]++;
1711
5.58k
  }
1712
5.58k
1713
5.58k
  tab->n_var++;
1714
5.58k
1715
5.58k
  return 0;
1716
5.58k
}
1717
1718
/* Drop the entry at position "first" in tab->var, moving all
1719
 * subsequent entries down.
1720
 * Since some of the entries of tab->row_var and tab->col_var contain
1721
 * indices into this array, they have to be updated accordingly.
1722
 */
1723
static int var_drop_entry(struct isl_tab *tab, int first)
1724
3.24k
{
1725
3.24k
  int i;
1726
3.24k
1727
3.24k
  if (first >= tab->n_var)
1728
0
    isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1729
3.24k
      "invalid initial position", return -1);
1730
3.24k
1731
3.24k
  tab->n_var--;
1732
3.24k
1733
3.75k
  for (i = first; 
i < tab->n_var3.75k
;
++i513
)
{513
1734
513
    tab->var[i] = tab->var[i + 1];
1735
513
    if (tab->var[i + 1].is_row)
1736
507
      tab->row_var[tab->var[i].index]--;
1737
513
    else
1738
6
      tab->col_var[tab->var[i].index]--;
1739
3.24k
  }
1740
3.24k
1741
3.24k
  return 0;
1742
3.24k
}
1743
1744
/* Add a variable to the tableau at position "r" and allocate a column for it.
1745
 * Return the index into the variable array "var", i.e., "r",
1746
 * or -1 on error.
1747
 */
1748
int isl_tab_insert_var(struct isl_tab *tab, int r)
1749
5.58k
{
1750
5.58k
  int i;
1751
5.58k
  unsigned off = 2 + tab->M;
1752
5.58k
1753
5.58k
  isl_assert(tab->mat->ctx, tab->n_col < tab->mat->n_col, return -1);
1754
5.58k
1755
5.58k
  
if (5.58k
var_insert_entry(tab, r) < 05.58k
)
1756
0
    return -1;
1757
5.58k
1758
5.58k
  tab->var[r].index = tab->n_col;
1759
5.58k
  tab->var[r].is_row = 0;
1760
5.58k
  tab->var[r].is_nonneg = 0;
1761
5.58k
  tab->var[r].is_zero = 0;
1762
5.58k
  tab->var[r].is_redundant = 0;
1763
5.58k
  tab->var[r].frozen = 0;
1764
5.58k
  tab->var[r].negated = 0;
1765
5.58k
  tab->col_var[tab->n_col] = r;
1766
5.58k
1767
26.2k
  for (i = 0; 
i < tab->n_row26.2k
;
++i20.7k
)
1768
20.7k
    isl_int_set_si(tab->mat->row[i][off + tab->n_col], 0);
1769
5.58k
1770
5.58k
  tab->n_col++;
1771
5.58k
  if (isl_tab_push_var(tab, isl_tab_undo_allocate, &tab->var[r]) < 0)
1772
0
    return -1;
1773
5.58k
1774
5.58k
  return r;
1775
5.58k
}
1776
1777
/* Add a variable to the tableau and allocate a column for it.
1778
 * Return the index into the variable array "var".
1779
 */
1780
int isl_tab_allocate_var(struct isl_tab *tab)
1781
0
{
1782
0
  if (!tab)
1783
0
    return -1;
1784
0
1785
0
  return isl_tab_insert_var(tab, tab->n_var);
1786
0
}
1787
1788
/* Add a row to the tableau.  The row is given as an affine combination
1789
 * of the original variables and needs to be expressed in terms of the
1790
 * column variables.
1791
 *
1792
 * This function assumes that at least one more row and at least
1793
 * one more element in the constraint array are available in the tableau.
1794
 *
1795
 * We add each term in turn.
1796
 * If r = n/d_r is the current sum and we need to add k x, then
1797
 *  if x is a column variable, we increase the numerator of
1798
 *    this column by k d_r
1799
 *  if x = f/d_x is a row variable, then the new representation of r is
1800
 *
1801
 *     n    k f   d_x/g n + d_r/g k f   m/d_r n + m/d_g k f
1802
 *    --- + --- = ------------------- = -------------------
1803
 *    d_r   d_r        d_r d_x/g                m
1804
 *
1805
 *  with g the gcd of d_r and d_x and m the lcm of d_r and d_x.
1806
 *
1807
 * If tab->M is set, then, internally, each variable x is represented
1808
 * as x' - M.  We then also need no subtract k d_r from the coefficient of M.
1809
 */
1810
int isl_tab_add_row(struct isl_tab *tab, isl_int *line)
1811
3.99M
{
1812
3.99M
  int i;
1813
3.99M
  int r;
1814
3.99M
  isl_int *row;
1815
3.99M
  isl_int a, b;
1816
3.99M
  unsigned off = 2 + tab->M;
1817
3.99M
1818
3.99M
  r = isl_tab_allocate_con(tab);
1819
3.99M
  if (r < 0)
1820
0
    return -1;
1821
3.99M
1822
3.99M
  
isl_int_init3.99M
(a);3.99M
1823
3.99M
  isl_int_init(b);
1824
3.99M
  row = tab->mat->row[tab->con[r].index];
1825
3.99M
  isl_int_set_si(row[0], 1);
1826
3.99M
  isl_int_set(row[1], line[0]);
1827
3.99M
  isl_seq_clr(row + 2, tab->M + tab->n_col);
1828
37.3M
  for (i = 0; 
i < tab->n_var37.3M
;
++i33.3M
)
{33.3M
1829
33.3M
    if (tab->var[i].is_zero)
1830
0
      continue;
1831
33.3M
    
if (33.3M
tab->var[i].is_row33.3M
)
{5.64M
1832
5.64M
      isl_int_lcm(a,
1833
5.64M
        row[0], tab->mat->row[tab->var[i].index][0]);
1834
5.64M
      isl_int_swap(a, row[0]);
1835
5.64M
      isl_int_divexact(a, row[0], a);
1836
5.64M
      isl_int_divexact(b,
1837
5.64M
        row[0], tab->mat->row[tab->var[i].index][0]);
1838
5.64M
      isl_int_mul(b, b, line[1 + i]);
1839
5.64M
      isl_seq_combine(row + 1, a, row + 1,
1840
5.64M
          b, tab->mat->row[tab->var[i].index] + 1,
1841
5.64M
          1 + tab->M + tab->n_col);
1842
33.3M
    } else
1843
27.7M
      isl_int_addmul(row[off + tab->var[i].index],
1844
33.3M
              line[1 + i], row[0]);
1845
33.3M
    if (
tab->M && 33.3M
i >= tab->n_param269k
&&
i < tab->n_var - tab->n_div116k
)
1846
114k
      isl_int_submul(row[2], line[1 + i], row[0]);
1847
33.3M
  }
1848
3.99M
  isl_seq_normalize(tab->mat->ctx, row, off + tab->n_col);
1849
3.99M
  isl_int_clear(a);
1850
3.99M
  isl_int_clear(b);
1851
3.99M
1852
3.99M
  if (tab->row_sign)
1853
32.6k
    tab->row_sign[tab->con[r].index] = isl_tab_row_unknown;
1854
3.99M
1855
3.99M
  return r;
1856
3.99M
}
1857
1858
static isl_stat drop_row(struct isl_tab *tab, int row)
1859
860k
{
1860
860k
  isl_assert(tab->mat->ctx, ~tab->row_var[row] == tab->n_con - 1,
1861
860k
    return isl_stat_error);
1862
860k
  
if (860k
row != tab->n_row - 1860k
)
1863
110k
    swap_rows(tab, row, tab->n_row - 1);
1864
860k
  tab->n_row--;
1865
860k
  tab->n_con--;
1866
860k
  return isl_stat_ok;
1867
860k
}
1868
1869
/* Drop the variable in column "col" along with the column.
1870
 * The column is removed first because it may need to be moved
1871
 * into the last position and this process requires
1872
 * the contents of the col_var array in a state
1873
 * before the removal of the variable.
1874
 */
1875
static isl_stat drop_col(struct isl_tab *tab, int col)
1876
3.24k
{
1877
3.24k
  int var;
1878
3.24k
1879
3.24k
  var = tab->col_var[col];
1880
3.24k
  if (col != tab->n_col - 1)
1881
582
    swap_cols(tab, col, tab->n_col - 1);
1882
3.24k
  tab->n_col--;
1883
3.24k
  if (var_drop_entry(tab, var) < 0)
1884
0
    return isl_stat_error;
1885
3.24k
  return isl_stat_ok;
1886
3.24k
}
1887
1888
/* Add inequality "ineq" and check if it conflicts with the
1889
 * previously added constraints or if it is obviously redundant.
1890
 *
1891
 * This function assumes that at least one more row and at least
1892
 * one more element in the constraint array are available in the tableau.
1893
 */
1894
isl_stat isl_tab_add_ineq(struct isl_tab *tab, isl_int *ineq)
1895
3.09M
{
1896
3.09M
  int r;
1897
3.09M
  int sgn;
1898
3.09M
  isl_int cst;
1899
3.09M
1900
3.09M
  if (!tab)
1901
0
    return isl_stat_error;
1902
3.09M
  
if (3.09M
tab->bmap3.09M
)
{309k
1903
309k
    struct isl_basic_map *bmap = tab->bmap;
1904
309k
1905
309k
    isl_assert(tab->mat->ctx, tab->n_eq == bmap->n_eq,
1906
309k
      return isl_stat_error);
1907
309k
    
isl_assert309k
(tab->mat->ctx,309k
1908
309k
          tab->n_con == bmap->n_eq + bmap->n_ineq,
1909
309k
          return isl_stat_error);
1910
309k
    tab->bmap = isl_basic_map_add_ineq(tab->bmap, ineq);
1911
309k
    if (isl_tab_push(tab, isl_tab_undo_bmap_ineq) < 0)
1912
0
      return isl_stat_error;
1913
309k
    
if (309k
!tab->bmap309k
)
1914
0
      return isl_stat_error;
1915
3.09M
  }
1916
3.09M
  
if (3.09M
tab->cone3.09M
)
{3.17k
1917
3.17k
    isl_int_init(cst);
1918
3.17k
    isl_int_set_si(cst, 0);
1919
3.17k
    isl_int_swap(ineq[0], cst);
1920
3.09M
  }
1921
3.09M
  r = isl_tab_add_row(tab, ineq);
1922
3.09M
  if (
tab->cone3.09M
)
{3.17k
1923
3.17k
    isl_int_swap(ineq[0], cst);
1924
3.17k
    isl_int_clear(cst);
1925
3.09M
  }
1926
3.09M
  if (r < 0)
1927
0
    return isl_stat_error;
1928
3.09M
  tab->con[r].is_nonneg = 1;
1929
3.09M
  if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0)
1930
0
    return isl_stat_error;
1931
3.09M
  
if (3.09M
isl_tab_row_is_redundant(tab, tab->con[r].index)3.09M
)
{100k
1932
100k
    if (isl_tab_mark_redundant(tab, tab->con[r].index) < 0)
1933
0
      return isl_stat_error;
1934
100k
    return isl_stat_ok;
1935
3.09M
  }
1936
3.09M
1937
3.09M
  sgn = restore_row(tab, &tab->con[r]);
1938
2.99M
  if (sgn < -1)
1939
0
    return isl_stat_error;
1940
2.99M
  
if (2.99M
sgn < 02.99M
)
1941
63.0k
    return isl_tab_mark_empty(tab);
1942
2.93M
  
if (2.93M
tab->con[r].is_row && 2.93M
isl_tab_row_is_redundant(tab, tab->con[r].index)2.61M
)
1943
0
    
if (0
isl_tab_mark_redundant(tab, tab->con[r].index) < 00
)
1944
0
      return isl_stat_error;
1945
2.93M
  return isl_stat_ok;
1946
3.09M
}
1947
1948
/* Pivot a non-negative variable down until it reaches the value zero
1949
 * and then pivot the variable into a column position.
1950
 */
1951
static int to_col(struct isl_tab *tab, struct isl_tab_var *var) WARN_UNUSED;
1952
static int to_col(struct isl_tab *tab, struct isl_tab_var *var)
1953
40.2k
{
1954
40.2k
  int i;
1955
40.2k
  int row, col;
1956
40.2k
  unsigned off = 2 + tab->M;
1957
40.2k
1958
40.2k
  if (!var->is_row)
1959
112
    return 0;
1960
40.2k
1961
50.4k
  
while (40.1k
isl_int_is_pos50.4k
(tab->mat->row[var->index][1]))
{47.5k
1962
47.5k
    find_pivot(tab, var, NULL, -1, &row, &col);
1963
47.5k
    isl_assert(tab->mat->ctx, row != -1, return -1);
1964
47.5k
    
if (47.5k
isl_tab_pivot(tab, row, col) < 047.5k
)
1965
0
      return -1;
1966
47.5k
    
if (47.5k
!var->is_row47.5k
)
1967
37.2k
      return 0;
1968
47.5k
  }
1969
40.1k
1970
4.80k
  
for (i = tab->n_dead; 2.89k
i < tab->n_col4.80k
;
++i1.90k
)
1971
4.80k
    
if (4.80k
!4.80k
isl_int_is_zero4.80k
(tab->mat->row[var->index][off + i]))
1972
2.89k
      break;
1973
2.89k
1974
2.89k
  isl_assert(tab->mat->ctx, i < tab->n_col, return -1);
1975
2.89k
  
if (2.89k
isl_tab_pivot(tab, var->index, i) < 02.89k
)
1976
0
    return -1;
1977
2.89k
1978
2.89k
  return 0;
1979
40.2k
}
1980
1981
/* We assume Gaussian elimination has been performed on the equalities.
1982
 * The equalities can therefore never conflict.
1983
 * Adding the equalities is currently only really useful for a later call
1984
 * to isl_tab_ineq_type.
1985
 *
1986
 * This function assumes that at least one more row and at least
1987
 * one more element in the constraint array are available in the tableau.
1988
 */
1989
static struct isl_tab *add_eq(struct isl_tab *tab, isl_int *eq)
1990
226k
{
1991
226k
  int i;
1992
226k
  int r;
1993
226k
1994
226k
  if (!tab)
1995
0
    return NULL;
1996
226k
  r = isl_tab_add_row(tab, eq);
1997
226k
  if (r < 0)
1998
0
    goto error;
1999
226k
2000
226k
  r = tab->con[r].index;
2001
226k
  i = isl_seq_first_non_zero(tab->mat->row[r] + 2 + tab->M + tab->n_dead,
2002
226k
          tab->n_col - tab->n_dead);
2003
226k
  isl_assert(tab->mat->ctx, i >= 0, goto error);
2004
226k
  i += tab->n_dead;
2005
226k
  if (isl_tab_pivot(tab, r, i) < 0)
2006
0
    goto error;
2007
226k
  
if (226k
isl_tab_kill_col(tab, i) < 0226k
)
2008
0
    goto error;
2009
226k
  tab->n_eq++;
2010
226k
2011
226k
  return tab;
2012
226k
error:
2013
0
  isl_tab_free(tab);
2014
226k
  return NULL;
2015
226k
}
2016
2017
/* Does the sample value of row "row" of "tab" involve the big parameter,
2018
 * if any?
2019
 */
2020
static int row_is_big(struct isl_tab *tab, int row)
2021
81.1k
{
2022
0
  return tab->M && 
!0
isl_int_is_zero0
(tab->mat->row[row][2]);
2023
81.1k
}
2024
2025
static int row_is_manifestly_zero(struct isl_tab *tab, int row)
2026
49.8k
{
2027
49.8k
  unsigned off = 2 + tab->M;
2028
49.8k
2029
49.8k
  if (
!49.8k
isl_int_is_zero49.8k
(tab->mat->row[row][1]))
2030
37.6k
    return 0;
2031
12.2k
  
if (12.2k
row_is_big(tab, row)12.2k
)
2032
0
    return 0;
2033
12.2k
  return isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
2034
12.2k
          tab->n_col - tab->n_dead) == -1;
2035
49.8k
}
2036
2037
/* Add an equality that is known to be valid for the given tableau.
2038
 *
2039
 * This function assumes that at least one more row and at least
2040
 * one more element in the constraint array are available in the tableau.
2041
 */
2042
int isl_tab_add_valid_eq(struct isl_tab *tab, isl_int *eq)
2043
37.8k
{
2044
37.8k
  struct isl_tab_var *var;
2045
37.8k
  int r;
2046
37.8k
2047
37.8k
  if (!tab)
2048
0
    return -1;
2049
37.8k
  r = isl_tab_add_row(tab, eq);
2050
37.8k
  if (r < 0)
2051
0
    return -1;
2052
37.8k
2053
37.8k
  var = &tab->con[r];
2054
37.8k
  r = var->index;
2055
37.8k
  if (
row_is_manifestly_zero(tab, r)37.8k
)
{532
2056
532
    var->is_zero = 1;
2057
532
    if (isl_tab_mark_redundant(tab, r) < 0)
2058
0
      return -1;
2059
532
    return 0;
2060
37.8k
  }
2061
37.8k
2062
37.2k
  
if (37.2k
isl_int_is_neg37.2k
(tab->mat->row[r][1]))
{11.1k
2063
11.1k
    isl_seq_neg(tab->mat->row[r] + 1, tab->mat->row[r] + 1,
2064
11.1k
          1 + tab->n_col);
2065
11.1k
    var->negated = 1;
2066
37.2k
  }
2067
37.2k
  var->is_nonneg = 1;
2068
37.2k
  if (to_col(tab, var) < 0)
2069
0
    return -1;
2070
37.2k
  var->is_nonneg = 0;
2071
37.2k
  if (isl_tab_kill_col(tab, var->index) < 0)
2072
0
    return -1;
2073
37.2k
2074
37.2k
  return 0;
2075
37.8k
}
2076
2077
/* Add a zero row to "tab" and return the corresponding index
2078
 * in the constraint array.
2079
 *
2080
 * This function assumes that at least one more row and at least
2081
 * one more element in the constraint array are available in the tableau.
2082
 */
2083
static int add_zero_row(struct isl_tab *tab)
2084
2.15k
{
2085
2.15k
  int r;
2086
2.15k
  isl_int *row;
2087
2.15k
2088
2.15k
  r = isl_tab_allocate_con(tab);
2089
2.15k
  if (r < 0)
2090
0
    return -1;
2091
2.15k
2092
2.15k
  row = tab->mat->row[tab->con[r].index];
2093
2.15k
  isl_seq_clr(row + 1, 1 + tab->M + tab->n_col);
2094
2.15k
  isl_int_set_si(row[0], 1);
2095
2.15k
2096
2.15k
  return r;
2097
2.15k
}
2098
2099
/* Add equality "eq" and check if it conflicts with the
2100
 * previously added constraints or if it is obviously redundant.
2101
 *
2102
 * This function assumes that at least one more row and at least
2103
 * one more element in the constraint array are available in the tableau.
2104
 * If tab->bmap is set, then two rows are needed instead of one.
2105
 */
2106
int isl_tab_add_eq(struct isl_tab *tab, isl_int *eq)
2107
12.0k
{
2108
12.0k
  struct isl_tab_undo *snap = NULL;
2109
12.0k
  struct isl_tab_var *var;
2110
12.0k
  int r;
2111
12.0k
  int row;
2112
12.0k
  int sgn;
2113
12.0k
  isl_int cst;
2114
12.0k
2115
12.0k
  if (!tab)
2116
0
    return -1;
2117
12.0k
  
isl_assert12.0k
(tab->mat->ctx, !tab->M, return -1);12.0k
2118
12.0k
2119
12.0k
  
if (12.0k
tab->need_undo12.0k
)
2120
11.3k
    snap = isl_tab_snap(tab);
2121
12.0k
2122
12.0k
  if (
tab->cone12.0k
)
{1.10k
2123
1.10k
    isl_int_init(cst);
2124
1.10k
    isl_int_set_si(cst, 0);
2125
1.10k
    isl_int_swap(eq[0], cst);
2126
12.0k
  }
2127
12.0k
  r = isl_tab_add_row(tab, eq);
2128
12.0k
  if (
tab->cone12.0k
)
{1.10k
2129
1.10k
    isl_int_swap(eq[0], cst);
2130
1.10k
    isl_int_clear(cst);
2131
12.0k
  }
2132
12.0k
  if (r < 0)
2133
0
    return -1;
2134
12.0k
2135
12.0k
  var = &tab->con[r];
2136
12.0k
  row = var->index;
2137
12.0k
  if (
row_is_manifestly_zero(tab, row)12.0k
)
{9.05k
2138
9.05k
    if (snap)
2139
8.97k
      return isl_tab_rollback(tab, snap);
2140
76
    return drop_row(tab, row);
2141
12.0k
  }
2142
12.0k
2143
3.00k
  
if (3.00k
tab->bmap3.00k
)
{2.15k
2144
2.15k
    tab->bmap = isl_basic_map_add_ineq(tab->bmap, eq);
2145
2.15k
    if (isl_tab_push(tab, isl_tab_undo_bmap_ineq) < 0)
2146
0
      return -1;
2147
2.15k
    isl_seq_neg(eq, eq, 1 + tab->n_var);
2148
2.15k
    tab->bmap = isl_basic_map_add_ineq(tab->bmap, eq);
2149
2.15k
    isl_seq_neg(eq, eq, 1 + tab->n_var);
2150
2.15k
    if (isl_tab_push(tab, isl_tab_undo_bmap_ineq) < 0)
2151
0
      return -1;
2152
2.15k
    
if (2.15k
!tab->bmap2.15k
)
2153
0
      return -1;
2154
2.15k
    
if (2.15k
add_zero_row(tab) < 02.15k
)
2155
0
      return -1;
2156
3.00k
  }
2157
3.00k
2158
3.00k
  
sgn = 3.00k
isl_int_sgn3.00k
(tab->mat->row[row][1]);
2159
3.00k
2160
3.00k
  if (
sgn > 03.00k
)
{122
2161
122
    isl_seq_neg(tab->mat->row[row] + 1, tab->mat->row[row] + 1,
2162
122
          1 + tab->n_col);
2163
122
    var->negated = 1;
2164
122
    sgn = -1;
2165
3.00k
  }
2166
3.00k
2167
3.00k
  if (
sgn < 03.00k
)
{1.89k
2168
1.89k
    sgn = sign_of_max(tab, var);
2169
1.89k
    if (sgn < -1)
2170
0
      return -1;
2171
1.89k
    
if (1.89k
sgn < 01.89k
)
{0
2172
0
      if (isl_tab_mark_empty(tab) < 0)
2173
0
        return -1;
2174
0
      return 0;
2175
1.89k
    }
2176
3.00k
  }
2177
3.00k
2178
3.00k
  var->is_nonneg = 1;
2179
3.00k
  if (to_col(tab, var) < 0)
2180
0
    return -1;
2181
3.00k
  var->is_nonneg = 0;
2182
3.00k
  if (isl_tab_kill_col(tab, var->index) < 0)
2183
0
    return -1;
2184
3.00k
2185
3.00k
  return 0;
2186
12.0k
}
2187
2188
/* Construct and return an inequality that expresses an upper bound
2189
 * on the given div.
2190
 * In particular, if the div is given by
2191
 *
2192
 *  d = floor(e/m)
2193
 *
2194
 * then the inequality expresses
2195
 *
2196
 *  m d <= e
2197
 */
2198
static struct isl_vec *ineq_for_div(struct isl_basic_map *bmap, unsigned div)
2199
1.85k
{
2200
1.85k
  unsigned total;
2201
1.85k
  unsigned div_pos;
2202
1.85k
  struct isl_vec *ineq;
2203
1.85k
2204
1.85k
  if (!bmap)
2205
0
    return NULL;
2206
1.85k
2207
1.85k
  total = isl_basic_map_total_dim(bmap);
2208
1.85k
  div_pos = 1 + total - bmap->n_div + div;
2209
1.85k
2210
1.85k
  ineq = isl_vec_alloc(bmap->ctx, 1 + total);
2211
1.85k
  if (!ineq)
2212
0
    return NULL;
2213
1.85k
2214
1.85k
  isl_seq_cpy(ineq->el, bmap->div[div] + 1, 1 + total);
2215
1.85k
  isl_int_neg(ineq->el[div_pos], bmap->div[div][0]);
2216
1.85k
  return ineq;
2217
1.85k
}
2218
2219
/* For a div d = floor(f/m), add the constraints
2220
 *
2221
 *    f - m d >= 0
2222
 *    -(f-(m-1)) + m d >= 0
2223
 *
2224
 * Note that the second constraint is the negation of
2225
 *
2226
 *    f - m d >= m
2227
 *
2228
 * If add_ineq is not NULL, then this function is used
2229
 * instead of isl_tab_add_ineq to effectively add the inequalities.
2230
 *
2231
 * This function assumes that at least two more rows and at least
2232
 * two more elements in the constraint array are available in the tableau.
2233
 */
2234
static isl_stat add_div_constraints(struct isl_tab *tab, unsigned div,
2235
  isl_stat (*add_ineq)(void *user, isl_int *), void *user)
2236
1.85k
{
2237
1.85k
  unsigned total;
2238
1.85k
  unsigned div_pos;
2239
1.85k
  struct isl_vec *ineq;
2240
1.85k
2241
1.85k
  total = isl_basic_map_total_dim(tab->bmap);
2242
1.85k
  div_pos = 1 + total - tab->bmap->n_div + div;
2243
1.85k
2244
1.85k
  ineq = ineq_for_div(tab->bmap, div);
2245
1.85k
  if (!ineq)
2246
0
    goto error;
2247
1.85k
2248
1.85k
  
if (1.85k
add_ineq1.85k
)
{571
2249
571
    if (add_ineq(user, ineq->el) < 0)
2250
0
      goto error;
2251
1.85k
  } else {
2252
1.28k
    if (isl_tab_add_ineq(tab, ineq->el) < 0)
2253
0
      goto error;
2254
1.85k
  }
2255
1.85k
2256
1.85k
  isl_seq_neg(ineq->el, tab->bmap->div[div] + 1, 1 + total);
2257
1.85k
  isl_int_set(ineq->el[div_pos], tab->bmap->div[div][0]);
2258
1.85k
  isl_int_add(ineq->el[0], ineq->el[0], ineq->el[div_pos]);
2259
1.85k
  isl_int_sub_ui(ineq->el[0], ineq->el[0], 1);
2260
1.85k
2261
1.85k
  if (
add_ineq1.85k
)
{571
2262
571
    if (add_ineq(user, ineq->el) < 0)
2263
0
      goto error;
2264
1.85k
  } else {
2265
1.28k
    if (isl_tab_add_ineq(tab, ineq->el) < 0)
2266
0
      goto error;
2267
1.85k
  }
2268
1.85k
2269
1.85k
  isl_vec_free(ineq);
2270
1.85k
2271
1.85k
  return 0;
2272
1.85k
error:
2273
0
  isl_vec_free(ineq);
2274
1.85k
  return -1;
2275
1.85k
}
2276
2277
/* Check whether the div described by "div" is obviously non-negative.
2278
 * If we are using a big parameter, then we will encode the div
2279
 * as div' = M + div, which is always non-negative.
2280
 * Otherwise, we check whether div is a non-negative affine combination
2281
 * of non-negative variables.
2282
 */
2283
static int div_is_nonneg(struct isl_tab *tab, __isl_keep isl_vec *div)
2284
1.85k
{
2285
1.85k
  int i;
2286
1.85k
2287
1.85k
  if (tab->M)
2288
0
    return 1;
2289
1.85k
2290
1.85k
  
if (1.85k
isl_int_is_neg1.85k
(div->el[1]))
2291
200
    return 0;
2292
1.85k
2293
3.64k
  
for (i = 0; 1.65k
i < tab->n_var3.64k
;
++i1.99k
)
{3.38k
2294
3.38k
    if (isl_int_is_neg(div->el[2 + i]))
2295
337
      return 0;
2296
3.05k
    
if (3.05k
isl_int_is_zero3.05k
(div->el[2 + i]))
2297
1.70k
      continue;
2298
1.34k
    
if (1.34k
!tab->var[i].is_nonneg1.34k
)
2299
1.05k
      return 0;
2300
1.65k
  }
2301
1.65k
2302
257
  return 1;
2303
1.85k
}
2304
2305
/* Insert an extra div, prescribed by "div", to the tableau and
2306
 * the associated bmap (which is assumed to be non-NULL).
2307
 * The extra integer division is inserted at (tableau) position "pos".
2308
 * Return "pos" or -1 if an error occurred.
2309
 *
2310
 * If add_ineq is not NULL, then this function is used instead
2311
 * of isl_tab_add_ineq to add the div constraints.
2312
 * This complication is needed because the code in isl_tab_pip
2313
 * wants to perform some extra processing when an inequality
2314
 * is added to the tableau.
2315
 */
2316
int isl_tab_insert_div(struct isl_tab *tab, int pos, __isl_keep isl_vec *div,
2317
  isl_stat (*add_ineq)(void *user, isl_int *), void *user)
2318
1.85k
{
2319
1.85k
  int r;
2320
1.85k
  int nonneg;
2321
1.85k
  int n_div, o_div;
2322
1.85k
2323
1.85k
  if (
!tab || 1.85k
!div1.85k
)
2324
0
    return -1;
2325
1.85k
2326
1.85k
  
if (1.85k
div->size != 1 + 1 + tab->n_var1.85k
)
2327
0
    isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
2328
1.85k
      "unexpected size", return -1);
2329
1.85k
2330
1.85k
  
isl_assert1.85k
(tab->mat->ctx, tab->bmap, return -1);1.85k
2331
1.85k
  n_div = isl_basic_map_dim(tab->bmap, isl_dim_div);
2332
1.85k
  o_div = tab->n_var - n_div;
2333
1.85k
  if (
pos < o_div || 1.85k
pos > tab->n_var1.85k
)
2334
0
    isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
2335
1.85k
      "invalid position", return -1);
2336
1.85k
2337
1.85k
  nonneg = div_is_nonneg(tab, div);
2338
1.85k
2339
1.85k
  if (isl_tab_extend_cons(tab, 3) < 0)
2340
0
    return -1;
2341
1.85k
  
if (1.85k
isl_tab_extend_vars(tab, 1) < 01.85k
)
2342
0
    return -1;
2343
1.85k
  r = isl_tab_insert_var(tab, pos);
2344
1.85k
  if (r < 0)
2345
0
    return -1;
2346
1.85k
2347
1.85k
  
if (1.85k
nonneg1.85k
)
2348
257
    tab->var[r].is_nonneg = 1;
2349
1.85k
2350
1.85k
  tab->bmap = isl_basic_map_insert_div(tab->bmap, pos - o_div, div);
2351
1.85k
  if (!tab->bmap)
2352
0
    return -1;
2353
1.85k
  
if (1.85k
isl_tab_push_var(tab, isl_tab_undo_bmap_div, &tab->var[r]) < 01.85k
)
2354
0
    return -1;
2355
1.85k
2356
1.85k
  
if (1.85k
add_div_constraints(tab, pos - o_div, add_ineq, user) < 01.85k
)
2357
0
    return -1;
2358
1.85k
2359
1.85k
  return r;
2360
1.85k
}
2361
2362
/* Add an extra div, prescribed by "div", to the tableau and
2363
 * the associated bmap (which is assumed to be non-NULL).
2364
 */
2365
int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div)
2366
1.28k
{
2367
1.28k
  if (!tab)
2368
0
    return -1;
2369
1.28k
  return isl_tab_insert_div(tab, tab->n_var, div, NULL, NULL);
2370
1.28k
}
2371
2372
/* If "track" is set, then we want to keep track of all constraints in tab
2373
 * in its bmap field.  This field is initialized from a copy of "bmap",
2374
 * so we need to make sure that all constraints in "bmap" also appear
2375
 * in the constructed tab.
2376
 */
2377
__isl_give struct isl_tab *isl_tab_from_basic_map(
2378
  __isl_keep isl_basic_map *bmap, int track)
2379
597k
{
2380
597k
  int i;
2381
597k
  struct isl_tab *tab;
2382
597k
2383
597k
  if (!bmap)
2384
0
    return NULL;
2385
597k
  tab = isl_tab_alloc(bmap->ctx,
2386
597k
          isl_basic_map_total_dim(bmap) + bmap->n_ineq + 1,
2387
597k
          isl_basic_map_total_dim(bmap), 0);
2388
597k
  if (!tab)
2389
0
    return NULL;
2390
597k
  tab->preserve = track;
2391
597k
  tab->rational = ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL);
2392
597k
  if (
ISL_F_ISSET597k
(bmap, ISL_BASIC_MAP_EMPTY))
{19
2393
19
    if (isl_tab_mark_empty(tab) < 0)
2394
0
      goto error;
2395
19
    goto done;
2396
597k
  }
2397
822k
  
for (i = 0; 597k
i < bmap->n_eq822k
;
++i224k
)
{224k
2398
224k
    tab = add_eq(tab, bmap->eq[i]);
2399
224k
    if (!tab)
2400
0
      return tab;
2401
597k
  }
2402
3.35M
  
for (i = 0; 597k
i < bmap->n_ineq3.35M
;
++i2.75M
)
{2.76M
2403
2.76M
    if (isl_tab_add_ineq(tab, bmap->ineq[i]) < 0)
2404
0
      goto error;
2405
2.76M
    
if (2.76M
tab->empty2.76M
)
2406
5.13k
      goto done;
2407
2.76M
  }
2408
597k
done:
2409
597k
  if (
track && 597k
isl_tab_track_bmap(tab, isl_basic_map_copy(bmap)) < 0145k
)
2410
0
    goto error;
2411
597k
  return tab;
2412
597k
error:
2413
0
  isl_tab_free(tab);
2414
597k
  return NULL;
2415
597k
}
2416
2417
__isl_give struct isl_tab *isl_tab_from_basic_set(
2418
  __isl_keep isl_basic_set *bset, int track)
2419
210k
{
2420
210k
  return isl_tab_from_basic_map(bset, track);
2421
210k
}
2422
2423
/* Construct a tableau corresponding to the recession cone of "bset".
2424
 */
2425
struct isl_tab *isl_tab_from_recession_cone(__isl_keep isl_basic_set *bset,
2426
  int parametric)
2427
3.73k
{
2428
3.73k
  isl_int cst;
2429
3.73k
  int i;
2430
3.73k
  struct isl_tab *tab;
2431
3.73k
  unsigned offset = 0;
2432
3.73k
2433
3.73k
  if (!bset)
2434
0
    return NULL;
2435
3.73k
  
if (3.73k
parametric3.73k
)
2436
2.77k
    offset = isl_basic_set_dim(bset, isl_dim_param);
2437
3.73k
  tab = isl_tab_alloc(bset->ctx, bset->n_eq + bset->n_ineq,
2438
3.73k
        isl_basic_set_total_dim(bset) - offset, 0);
2439
3.73k
  if (!tab)
2440
0
    return NULL;
2441
3.73k
  
tab->rational = 3.73k
ISL_F_ISSET3.73k
(bset, ISL_BASIC_SET_RATIONAL);
2442
3.73k
  tab->cone = 1;
2443
3.73k
2444
3.73k
  isl_int_init(cst);
2445
3.73k
  isl_int_set_si(cst, 0);
2446
6.13k
  for (i = 0; 
i < bset->n_eq6.13k
;
++i2.40k
)
{2.40k
2447
2.40k
    isl_int_swap(bset->eq[i][offset], cst);
2448
2.40k
    if (
offset > 02.40k
)
{662
2449
662
      if (isl_tab_add_eq(tab, bset->eq[i] + offset) < 0)
2450
0
        goto error;
2451
2.40k
    } else
2452
1.74k
      tab = add_eq(tab, bset->eq[i]);
2453
2.40k
    
isl_int_swap2.40k
(bset->eq[i][offset], cst);2.40k
2454
2.40k
    if (!tab)
2455
0
      goto done;
2456
3.73k
  }
2457
15.7k
  
for (i = 0; 3.73k
i < bset->n_ineq15.7k
;
++i12.0k
)
{12.0k
2458
12.0k
    int r;
2459
12.0k
    isl_int_swap(bset->ineq[i][offset], cst);
2460
12.0k
    r = isl_tab_add_row(tab, bset->ineq[i] + offset);
2461
12.0k
    isl_int_swap(bset->ineq[i][offset], cst);
2462
12.0k
    if (r < 0)
2463
0
      goto error;
2464
12.0k
    tab->con[r].is_nonneg = 1;
2465
12.0k
    if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0)
2466
0
      goto error;
2467
12.0k
  }
2468
3.73k
done:
2469
3.73k
  isl_int_clear(cst);
2470
3.73k
  return tab;
2471
3.73k
error:
2472
0
  isl_int_clear(cst);
2473
0
  isl_tab_free(tab);
2474
3.73k
  return NULL;
2475
3.73k
}
2476
2477
/* Assuming "tab" is the tableau of a cone, check if the cone is
2478
 * bounded, i.e., if it is empty or only contains the origin.
2479
 */
2480
isl_bool isl_tab_cone_is_bounded(struct isl_tab *tab)
2481
2.77k
{
2482
2.77k
  int i;
2483
2.77k
2484
2.77k
  if (!tab)
2485
0
    return isl_bool_error;
2486
2.77k
  
if (2.77k
tab->empty2.77k
)
2487
0
    return isl_bool_true;
2488
2.77k
  
if (2.77k
tab->n_dead == tab->n_col2.77k
)
2489
744
    return isl_bool_true;
2490
2.77k
2491
2.02k
  
for (;;) 2.02k
{2.95k
2492
3.22k
    for (i = tab->n_redundant; 
i < tab->n_row3.22k
;
++i268
)
{3.21k
2493
3.21k
      struct isl_tab_var *var;
2494
3.21k
      int sgn;
2495
3.21k
      var = isl_tab_var_from_row(tab, i);
2496
3.21k
      if (!var->is_nonneg)
2497
268
        continue;
2498
3.21k
      sgn = sign_of_max(tab, var);
2499
2.95k
      if (sgn < -1)
2500
0
        return isl_bool_error;
2501
2.95k
      
if (2.95k
sgn != 02.95k
)
2502
302
        return isl_bool_false;
2503
2.64k
      
if (2.64k
close_row(tab, var, 0) < 02.64k
)
2504
0
        return isl_bool_error;
2505
2.64k
      break;
2506
2.95k
    }
2507
2.65k
    
if (2.65k
tab->n_dead == tab->n_col2.65k
)
2508
1.72k
      return isl_bool_true;
2509
930
    
if (930
i == tab->n_row930
)
2510
3
      return isl_bool_false;
2511
2.02k
  }
2512
2.77k
}
2513
2514
int isl_tab_sample_is_integer(struct isl_tab *tab)
2515
319k
{
2516
319k
  int i;
2517
319k
2518
319k
  if (!tab)
2519
0
    return -1;
2520
319k
2521
1.53M
  
for (i = 0; 319k
i < tab->n_var1.53M
;
++i1.21M
)
{1.27M
2522
1.27M
    int row;
2523
1.27M
    if (!tab->var[i].is_row)
2524
388k
      continue;
2525
1.27M
    row = tab->var[i].index;
2526
888k
    if (
!888k
isl_int_is_divisible_by888k
(tab->mat->row[row][1],
2527
888k
            tab->mat->row[row][0]))
2528
56.8k
      return 0;
2529
888k
  }
2530
262k
  return 1;
2531
319k
}
2532
2533
static struct isl_vec *extract_integer_sample(struct isl_tab *tab)
2534
172k
{
2535
172k
  int i;
2536
172k
  struct isl_vec *vec;
2537
172k
2538
172k
  vec = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_var);
2539
172k
  if (!vec)
2540
0
    return NULL;
2541
172k
2542
172k
  
isl_int_set_si172k
(vec->block.data[0], 1);172k
2543
1.05M
  for (i = 0; 
i < tab->n_var1.05M
;
++i883k
)
{883k
2544
883k
    if (!tab->var[i].is_row)
2545
322k
      isl_int_set_si(vec->block.data[1 + i], 0);
2546
883k
    else {
2547
560k
      int row = tab->var[i].index;
2548
560k
      isl_int_divexact(vec->block.data[1 + i],
2549
560k
        tab->mat->row[row][1], tab->mat->row[row][0]);
2550
883k
    }
2551
883k
  }
2552
172k
2553
172k
  return vec;
2554
172k
}
2555
2556
struct isl_vec *isl_tab_get_sample_value(struct isl_tab *tab)
2557
190k
{
2558
190k
  int i;
2559
190k
  struct isl_vec *vec;
2560
190k
  isl_int m;
2561
190k
2562
190k
  if (!tab)
2563
0
    return NULL;
2564
190k
2565
190k
  vec = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_var);
2566
190k
  if (!vec)
2567
0
    return NULL;
2568
190k
2569
190k
  
isl_int_init190k
(m);190k
2570
190k
2571
190k
  isl_int_set_si(vec->block.data[0], 1);
2572
807k
  for (i = 0; 
i < tab->n_var807k
;
++i617k
)
{617k
2573
617k
    int row;
2574
617k
    if (
!tab->var[i].is_row617k
)
{304k
2575
304k
      isl_int_set_si(vec->block.data[1 + i], 0);
2576
304k
      continue;
2577
617k
    }
2578
617k
    row = tab->var[i].index;
2579
312k
    isl_int_gcd(m, vec->block.data[0], tab->mat->row[row][0]);
2580
312k
    isl_int_divexact(m, tab->mat->row[row][0], m);
2581
312k
    isl_seq_scale(vec->block.data, vec->block.data, m, 1 + i);
2582
312k
    isl_int_divexact(m, vec->block.data[0], tab->mat->row[row][0]);
2583
312k
    isl_int_mul(vec->block.data[1 + i], m, tab->mat->row[row][1]);
2584
312k
  }
2585
190k
  vec = isl_vec_normalize(vec);
2586
190k
2587
190k
  isl_int_clear(m);
2588
190k
  return vec;
2589
190k
}
2590
2591
/* Store the sample value of "var" of "tab" rounded up (if sgn > 0)
2592
 * or down (if sgn < 0) to the nearest integer in *v.
2593
 */
2594
static void get_rounded_sample_value(struct isl_tab *tab,
2595
  struct isl_tab_var *var, int sgn, isl_int *v)
2596
147k
{
2597
147k
  if (!var->is_row)
2598
2.85k
    isl_int_set_si(*v, 0);
2599
144k
  else 
if (144k
sgn > 0144k
)
2600
143k
    isl_int_cdiv_q(*v, tab->mat->row[var->index][1],
2601
144k
           tab->mat->row[var->index][0]);
2602
144k
  else
2603
1.49k
    isl_int_fdiv_q(*v, tab->mat->row[var->index][1],
2604
147k
           tab->mat->row[var->index][0]);
2605
147k
}
2606
2607
/* Update "bmap" based on the results of the tableau "tab".
2608
 * In particular, implicit equalities are made explicit, redundant constraints
2609
 * are removed and if the sample value happens to be integer, it is stored
2610
 * in "bmap" (unless "bmap" already had an integer sample).
2611
 *
2612
 * The tableau is assumed to have been created from "bmap" using
2613
 * isl_tab_from_basic_map.
2614
 */
2615
struct isl_basic_map *isl_basic_map_update_from_tab(struct isl_basic_map *bmap,
2616
  struct isl_tab *tab)
2617
370k
{
2618
370k
  int i;
2619
370k
  unsigned n_eq;
2620
370k
2621
370k
  if (!bmap)
2622
0
    return NULL;
2623
370k
  
if (370k
!tab370k
)
2624
0
    return bmap;
2625
370k
2626
370k
  n_eq = tab->n_eq;
2627
370k
  if (tab->empty)
2628
6.48k
    bmap = isl_basic_map_set_to_empty(bmap);
2629
370k
  else
2630
2.36M
    
for (i = bmap->n_ineq - 1; 363k
i >= 02.36M
;
--i1.99M
)
{1.99M
2631
1.99M
      if (isl_tab_is_equality(tab, n_eq + i))
2632
738k
        isl_basic_map_inequality_to_equality(bmap, i);
2633
1.25M
      else 
if (1.25M
isl_tab_is_redundant(tab, n_eq + i)1.25M
)
2634
135k
        isl_basic_map_drop_inequality(bmap, i);
2635
1.99M
    }
2636
370k
  if (bmap->n_eq != n_eq)
2637
125k
    bmap = isl_basic_map_gauss(bmap, NULL);
2638
370k
  if (!tab->rational &&
2639
370k
      
bmap336k
&&
!bmap->sample336k
&&
isl_tab_sample_is_integer(tab)186k
)
2640
172k
    bmap->sample = extract_integer_sample(tab);
2641
370k
  return bmap;
2642
370k
}
2643
2644
struct isl_basic_set *isl_basic_set_update_from_tab(struct isl_basic_set *bset,
2645
  struct isl_tab *tab)
2646
31.5k
{
2647
31.5k
  return bset_from_bmap(isl_basic_map_update_from_tab(bset_to_bmap(bset),
2648
31.5k
                tab));
2649
31.5k
}
2650
2651
/* Drop the last constraint added to "tab" in position "r".
2652
 * The constraint is expected to have remained in a row.
2653
 */
2654
static isl_stat drop_last_con_in_row(struct isl_tab *tab, int r)
2655
12.0k
{
2656
12.0k
  if (!tab->con[r].is_row)
2657
0
    isl_die(isl_tab_get_ctx(tab), isl_error_internal,
2658
12.0k
      "row unexpectedly moved to column",
2659
12.0k
      return isl_stat_error);
2660
12.0k
  
if (12.0k
r + 1 != tab->n_con12.0k
)
2661
0
    isl_die(isl_tab_get_ctx(tab), isl_error_internal,
2662
12.0k
      "additional constraints added", return isl_stat_error);
2663
12.0k
  
if (12.0k
drop_row(tab, tab->con[r].index) < 012.0k
)
2664
0
    return isl_stat_error;
2665
12.0k
2666
12.0k
  return isl_stat_ok;
2667
12.0k
}
2668
2669
/* Given a non-negative variable "var", temporarily add a new non-negative
2670
 * variable that is the opposite of "var", ensuring that "var" can only attain
2671
 * the value zero.  The new variable is removed again before this function
2672
 * returns.  However, the effect of forcing "var" to be zero remains.
2673
 * If var = n/d is a row variable, then the new variable = -n/d.
2674
 * If var is a column variables, then the new variable = -var.
2675
 * If the new variable cannot attain non-negative values, then
2676
 * the resulting tableau is empty.
2677
 * Otherwise, we know the value will be zero and we close the row.
2678
 */
2679
static isl_stat cut_to_hyperplane(struct isl_tab *tab, struct isl_tab_var *var)
2680
12.0k
{
2681
12.0k
  unsigned r;
2682
12.0k
  isl_int *row;
2683
12.0k
  int sgn;
2684
12.0k
  unsigned off = 2 + tab->M;
2685
12.0k
2686
12.0k
  if (var->is_zero)
2687
0
    return isl_stat_ok;
2688
12.0k
  
if (12.0k
var->is_redundant || 12.0k
!var->is_nonneg12.0k
)
2689
0
    isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
2690
12.0k
      "expecting non-redundant non-negative variable",
2691
12.0k
      return isl_stat_error);
2692
12.0k
2693
12.0k
  
if (12.0k
isl_tab_extend_cons(tab, 1) < 012.0k
)
2694
0
    return isl_stat_error;
2695
12.0k
2696
12.0k
  r = tab->n_con;
2697
12.0k
  tab->con[r].index = tab->n_row;
2698
12.0k
  tab->con[r].is_row = 1;
2699
12.0k
  tab->con[r].is_nonneg = 0;
2700
12.0k
  tab->con[r].is_zero = 0;
2701
12.0k
  tab->con[r].is_redundant = 0;
2702
12.0k
  tab->con[r].frozen = 0;
2703
12.0k
  tab->con[r].negated = 0;
2704
12.0k
  tab->row_var[tab->n_row] = ~r;
2705
12.0k
  row = tab->mat->row[tab->n_row];
2706
12.0k
2707
12.0k
  if (
var->is_row12.0k
)
{1.03k
2708
1.03k
    isl_int_set(row[0], tab->mat->row[var->index][0]);
2709
1.03k
    isl_seq_neg(row + 1,
2710
1.03k
          tab->mat->row[var->index] + 1, 1 + tab->n_col);
2711
12.0k
  } else {
2712
11.0k
    isl_int_set_si(row[0], 1);
2713
11.0k
    isl_seq_clr(row + 1, 1 + tab->n_col);
2714
11.0k
    isl_int_set_si(row[off + var->index], -1);
2715
12.0k
  }
2716
12.0k
2717
12.0k
  tab->n_row++;
2718
12.0k
  tab->n_con++;
2719
12.0k
2720
12.0k
  sgn = sign_of_max(tab, &tab->con[r]);
2721
12.0k
  if (sgn < -1)
2722
0
    return isl_stat_error;
2723
12.0k
  
if (12.0k
sgn < 012.0k
)
{48
2724
48
    if (drop_last_con_in_row(tab, r) < 0)
2725
0
      return isl_stat_error;
2726
48
    
if (48
isl_tab_mark_empty(tab) < 048
)
2727
0
      return isl_stat_error;
2728
48
    return isl_stat_ok;
2729
12.0k
  }
2730
12.0k
  tab->con[r].is_nonneg = 1;
2731
12.0k
  /* sgn == 0 */
2732
12.0k
  if (close_row(tab, &tab->con[r], 1) < 0)
2733
0
    return isl_stat_error;
2734
12.0k
  
if (12.0k
drop_last_con_in_row(tab, r) < 012.0k
)
2735
0
    return isl_stat_error;
2736
12.0k
2737
12.0k
  return isl_stat_ok;
2738
12.0k
}
2739
2740
/* Given a tableau "tab" and an inequality constraint "con" of the tableau,
2741
 * relax the inequality by one.  That is, the inequality r >= 0 is replaced
2742
 * by r' = r + 1 >= 0.
2743
 * If r is a row variable, we simply increase the constant term by one
2744
 * (taking into account the denominator).
2745
 * If r is a column variable, then we need to modify each row that
2746
 * refers to r = r' - 1 by substituting this equality, effectively
2747
 * subtracting the coefficient of the column from the constant.
2748
 * We should only do this if the minimum is manifestly unbounded,
2749
 * however.  Otherwise, we may end up with negative sample values
2750
 * for non-negative variables.
2751
 * So, if r is a column variable with a minimum that is not
2752
 * manifestly unbounded, then we need to move it to a row.
2753
 * However, the sample value of this row may be negative,
2754
 * even after the relaxation, so we need to restore it.
2755
 * We therefore prefer to pivot a column up to a row, if possible.
2756
 */
2757
int isl_tab_relax(struct isl_tab *tab, int con)
2758
1.10k
{
2759
1.10k
  struct isl_tab_var *var;
2760
1.10k
2761
1.10k
  if (!tab)
2762
0
    return -1;
2763
1.10k
2764
1.10k
  var = &tab->con[con];
2765
1.10k
2766
1.10k
  if (
var->is_row && 1.10k
(var->index < 0 || 51
var->index < tab->n_redundant51
))
2767
0
    isl_die(tab->mat->ctx, isl_error_invalid,
2768
1.10k
      "cannot relax redundant constraint", return -1);
2769
1.10k
  
if (1.10k
!var->is_row && 1.10k
(var->index < 0 || 1.05k
var->index < tab->n_dead1.05k
))
2770
0
    isl_die(tab->mat->ctx, isl_error_invalid,
2771
1.10k
      "cannot relax dead constraint", return -1);
2772
1.10k
2773
1.10k
  
if (1.10k
!var->is_row && 1.10k
!max_is_manifestly_unbounded(tab, var)1.05k
)
2774
371
    
if (371
to_row(tab, var, 1) < 0371
)
2775
0
      return -1;
2776
1.10k
  
if (1.10k
!var->is_row && 1.10k
!min_is_manifestly_unbounded(tab, var)680
)
2777
18
    
if (18
to_row(tab, var, -1) < 018
)
2778
0
      return -1;
2779
1.10k
2780
1.10k
  
if (1.10k
var->is_row1.10k
)
{440
2781
440
    isl_int_add(tab->mat->row[var->index][1],
2782
440
        tab->mat->row[var->index][1], tab->mat->row[var->index][0]);
2783
440
    if (restore_row(tab, var) < 0)
2784
0
      return -1;
2785
1.10k
  } else {
2786
662
    int i;
2787
662
    unsigned off = 2 + tab->M;
2788
662
2789
3.32k
    for (i = 0; 
i < tab->n_row3.32k
;
++i2.65k
)
{2.65k
2790
2.65k
      if (isl_int_is_zero(tab->mat->row[i][off + var->index]))
2791
1.88k
        continue;
2792
771
      
isl_int_sub771
(tab->mat->row[i][1], tab->mat->row[i][1],771
2793
771
          tab->mat->row[i][off + var->index]);
2794
771
    }
2795
662
2796
1.10k
  }
2797
1.10k
2798
1.10k
  
if (1.10k
isl_tab_push_var(tab, isl_tab_undo_relax, var) < 01.10k
)
2799
0
    return -1;
2800
1.10k
2801
1.10k
  return 0;
2802
1.10k
}
2803
2804
/* Replace the variable v at position "pos" in the tableau "tab"
2805
 * by v' = v + shift.
2806
 *
2807
 * If the variable is in a column, then we first check if we can
2808
 * simply plug in v = v' - shift.  The effect on a row with
2809
 * coefficient f/d for variable v is that the constant term c/d
2810
 * is replaced by (c - f * shift)/d.  If shift is positive and
2811
 * f is negative for each row that needs to remain non-negative,
2812
 * then this is clearly safe.  In other words, if the minimum of v
2813
 * is manifestly unbounded, then we can keep v in a column position.
2814
 * Otherwise, we can pivot it down to a row.
2815
 * Similarly, if shift is negative, we need to check if the maximum
2816
 * of is manifestly unbounded.
2817
 *
2818
 * If the variable is in a row (from the start or after pivoting),
2819
 * then the constant term c/d is replaced by (c + d * shift)/d.
2820
 */
2821
int isl_tab_shift_var(struct isl_tab *tab, int pos, isl_int shift)
2822
136
{
2823
136
  struct isl_tab_var *var;
2824
136
2825
136
  if (!tab)
2826
0
    return -1;
2827
136
  
if (136
isl_int_is_zero136
(shift))
2828
70
    return 0;
2829
136
2830
136
  var = &tab->var[pos];
2831
66
  if (
!var->is_row66
)
{9
2832
9
    if (
isl_int_is_neg9
(shift))
{6
2833
6
      if (!max_is_manifestly_unbounded(tab, var))
2834
3
        
if (3
to_row(tab, var, 1) < 03
)
2835
0
          return -1;
2836
9
    } else {
2837
3
      if (!min_is_manifestly_unbounded(tab, var))
2838
0
        
if (0
to_row(tab, var, -1) < 00
)
2839
0
          return -1;
2840
9
    }
2841
66
  }
2842
66
2843
66
  
if (66
var->is_row66
)
{60
2844
60
    isl_int_addmul(tab->mat->row[var->index][1],
2845
60
        shift, tab->mat->row[var->index][0]);
2846
66
  } else {
2847
6
    int i;
2848
6
    unsigned off = 2 + tab->M;
2849
6
2850
30
    for (i = 0; 
i < tab->n_row30
;
++i24
)
{24
2851
24
      if (isl_int_is_zero(tab->mat->row[i][off + var->index]))
2852
16
        continue;
2853
8
      
isl_int_submul8
(tab->mat->row[i][1],8
2854
8
            shift, tab->mat->row[i][off + var->index]);
2855
8
    }
2856
6
2857
66
  }
2858
66
2859
66
  return 0;
2860
136
}
2861
2862
/* Remove the sign constraint from constraint "con".
2863
 *
2864
 * If the constraint variable was originally marked non-negative,
2865
 * then we make sure we mark it non-negative again during rollback.
2866
 */
2867
int isl_tab_unrestrict(struct isl_tab *tab, int con)
2868
299
{
2869
299
  struct isl_tab_var *var;
2870
299
2871
299
  if (!tab)
2872
0
    return -1;
2873
299
2874
299
  var = &tab->con[con];
2875
299
  if (!var->is_nonneg)
2876
0
    return 0;
2877
299
2878
299
  var->is_nonneg = 0;
2879
299
  if (isl_tab_push_var(tab, isl_tab_undo_unrestrict, var) < 0)
2880
0
    return -1;
2881
299
2882
299
  return 0;
2883
299
}
2884
2885
int isl_tab_select_facet(struct isl_tab *tab, int con)
2886
11.6k
{
2887
11.6k
  if (!tab)
2888
0
    return -1;
2889
11.6k
2890
11.6k
  return cut_to_hyperplane(tab, &tab->con[con]);
2891
11.6k
}
2892
2893
static int may_be_equality(struct isl_tab *tab, int row)
2894
6.14M
{
2895
36.3k
  return tab->rational ? isl_int_is_zero(tab->mat->row[row][1])
2896
6.10M
           : isl_int_lt(tab->mat->row[row][1],
2897
6.14M
              tab->mat->row[row][0]);
2898
6.14M
}
2899
2900
/* Return an isl_tab_var that has been marked or NULL if no such
2901
 * variable can be found.
2902
 * The marked field has only been set for variables that
2903
 * appear in non-redundant rows or non-dead columns.
2904
 *
2905
 * Pick the last constraint variable that is marked and
2906
 * that appears in either a non-redundant row or a non-dead columns.
2907
 * Since the returned variable is tested for being a redundant constraint or
2908
 * an implicit equality, there is no need to return any tab variable that
2909
 * corresponds to a variable.
2910
 */
2911
static struct isl_tab_var *select_marked(struct isl_tab *tab)
2912
1.58M
{
2913
1.58M
  int i;
2914
1.58M
  struct isl_tab_var *var;
2915
1.58M
2916
13.2M
  for (i = tab->n_con - 1; 
i >= 013.2M
;
--i11.6M
)
{13.1M
2917
13.1M
    var = &tab->con[i];
2918
13.1M
    if (var->index < 0)
2919
4.88M
      continue;
2920
8.22M
    
if (8.22M
var->is_row && 8.22M
var->index < tab->n_redundant6.46M
)
2921
584k
      continue;
2922
7.63M
    
if (7.63M
!var->is_row && 7.63M
var->index < tab->n_dead1.75M
)
2923
1.57k
      continue;
2924
7.63M
    
if (7.63M
var->marked7.63M
)
2925
1.46M
      return var;
2926
7.63M
  }
2927
1.58M
2928
129k
  return NULL;
2929
1.58M
}
2930
2931
/* Check for (near) equalities among the constraints.
2932
 * A constraint is an equality if it is non-negative and if
2933
 * its maximal value is either
2934
 *  - zero (in case of rational tableaus), or
2935
 *  - strictly less than 1 (in case of integer tableaus)
2936
 *
2937
 * We first mark all non-redundant and non-dead variables that
2938
 * are not frozen and not obviously not an equality.
2939
 * Then we iterate over all marked variables if they can attain
2940
 * any values larger than zero or at least one.
2941
 * If the maximal value is zero, we mark any column variables
2942
 * that appear in the row as being zero and mark the row as being redundant.
2943
 * Otherwise, if the maximal value is strictly less than one (and the
2944
 * tableau is integer), then we restrict the value to being zero
2945
 * by adding an opposite non-negative variable.
2946
 * The order in which the variables are considered is not important.
2947
 */
2948
int isl_tab_detect_implicit_equalities(struct isl_tab *tab)
2949
349k
{
2950
349k
  int i;
2951
349k
  unsigned n_marked;
2952
349k
2953
349k
  if (!tab)
2954
0
    return -1;
2955
349k
  
if (349k
tab->empty349k
)
2956
3.64k
    return 0;
2957
345k
  
if (345k
tab->n_dead == tab->n_col345k
)
2958
18.0k
    return 0;
2959
345k
2960
345k
  n_marked = 0;
2961
2.26M
  for (i = tab->n_redundant; 
i < tab->n_row2.26M
;
++i1.94M
)
{1.94M
2962
1.94M
    struct isl_tab_var *var = isl_tab_var_from_row(tab, i);
2963
1.92M
    var->marked = !var->frozen && var->is_nonneg &&
2964
1.74M
      may_be_equality(tab, i);
2965
1.94M
    if (var->marked)
2966
1.26M
      n_marked++;
2967
1.94M
  }
2968
1.78M
  for (i = tab->n_dead; 
i < tab->n_col1.78M
;
++i1.45M
)
{1.45M
2969
1.45M
    struct isl_tab_var *var = var_from_col(tab, i);
2970
1.45M
    var->marked = !var->frozen && var->is_nonneg;
2971
1.45M
    if (var->marked)
2972
146k
      n_marked++;
2973
1.45M
  }
2974
1.29M
  while (
n_marked1.29M
)
{1.09M
2975
1.09M
    struct isl_tab_var *var;
2976
1.09M
    int sgn;
2977
1.09M
    var = select_marked(tab);
2978
1.09M
    if (!var)
2979
124k
      break;
2980
1.09M
    var->marked = 0;
2981
969k
    n_marked--;
2982
969k
    sgn = sign_of_max(tab, var);
2983
969k
    if (sgn < 0)
2984
0
      return -1;
2985
969k
    
if (969k
sgn == 0969k
)
{388k
2986
388k
      if (close_row(tab, var, 0) < 0)
2987
0
        return -1;
2988
969k
    } else 
if (581k
!tab->rational && 581k
!at_least_one(tab, var)558k
)
{405
2989
405
      if (cut_to_hyperplane(tab, var) < 0)
2990
0
        return -1;
2991
405
      return isl_tab_detect_implicit_equalities(tab);
2992
969k
    }
2993
8.65M
    
for (i = tab->n_redundant; 968k
i < tab->n_row8.65M
;
++i7.68M
)
{7.68M
2994
7.68M
      var = isl_tab_var_from_row(tab, i);
2995
7.68M
      if (!var->marked)
2996
3.29M
        continue;
2997
4.39M
      
if (4.39M
may_be_equality(tab, i)4.39M
)
2998
4.34M
        continue;
2999
4.39M
      var->marked = 0;
3000
48.6k
      n_marked--;
3001
968k
    }
3002
968k
  }
3003
327k
3004
327k
  return 0;
3005
349k
}
3006
3007
/* Update the element of row_var or col_var that corresponds to
3008
 * constraint tab->con[i] to a move from position "old" to position "i".
3009
 */
3010
static int update_con_after_move(struct isl_tab *tab, int i, int old)
3011
6.38k
{
3012
6.38k
  int *p;
3013
6.38k
  int index;
3014
6.38k
3015
6.38k
  index = tab->con[i].index;
3016
6.38k
  if (index == -1)
3017
4.21k
    return 0;
3018
2.17k
  
p = tab->con[i].is_row ? 2.17k
tab->row_var1.48k
:
tab->col_var682
;
3019
2.17k
  if (p[index] != ~old)
3020
0
    isl_die(tab->mat->ctx, isl_error_internal,
3021
2.17k
      "broken internal state", return -1);
3022
2.17k
  p[index] = ~i;
3023
2.17k
3024
2.17k
  return 0;
3025
6.38k
}
3026
3027
/* Rotate the "n" constraints starting at "first" to the right,
3028
 * putting the last constraint in the position of the first constraint.
3029
 */
3030
static int rotate_constraints(struct isl_tab *tab, int first, int n)
3031
1.83k
{
3032
1.83k
  int i, last;
3033
1.83k
  struct isl_tab_var var;
3034
1.83k
3035
1.83k
  if (n <= 1)
3036
596
    return 0;
3037
1.83k
3038
1.83k
  last = first + n - 1;
3039
1.24k
  var = tab->con[last];
3040
6.38k
  for (i = last; 
i > first6.38k
;
--i5.13k
)
{5.13k
3041
5.13k
    tab->con[i] = tab->con[i - 1];
3042
5.13k
    if (update_con_after_move(tab, i, i - 1) < 0)
3043
0
      return -1;
3044
5.13k
  }
3045
1.24k
  tab->con[first] = var;
3046
1.24k
  if (update_con_after_move(tab, first, last) < 0)
3047
0
    return -1;
3048
1.24k
3049
1.24k
  return 0;
3050
1.83k
}
3051
3052
/* Make the equalities that are implicit in "bmap" but that have been
3053
 * detected in the corresponding "tab" explicit in "bmap" and update
3054
 * "tab" to reflect the new order of the constraints.
3055
 *
3056
 * In particular, if inequality i is an implicit equality then
3057
 * isl_basic_map_inequality_to_equality will move the inequality
3058
 * in front of the other equality and it will move the last inequality
3059
 * in the position of inequality i.
3060
 * In the tableau, the inequalities of "bmap" are stored after the equalities
3061
 * and so the original order
3062
 *
3063
 *    E E E E E A A A I B B B B L
3064
 *
3065
 * is changed into
3066
 *
3067
 *    I E E E E E A A A L B B B B
3068
 *
3069
 * where I is the implicit equality, the E are equalities,
3070
 * the A inequalities before I, the B inequalities after I and
3071
 * L the last inequality.
3072
 * We therefore need to rotate to the right two sets of constraints,
3073
 * those up to and including I and those after I.
3074
 *
3075
 * If "tab" contains any constraints that are not in "bmap" then they
3076
 * appear after those in "bmap" and they should be left untouched.
3077
 *
3078
 * Note that this function leaves "bmap" in a temporary state
3079
 * as it does not call isl_basic_map_gauss.  Calling this function
3080
 * is the responsibility of the caller.
3081
 */
3082
__isl_give isl_basic_map *isl_tab_make_equalities_explicit(struct isl_tab *tab,
3083
  __isl_take isl_basic_map *bmap)
3084
57.5k
{
3085
57.5k
  int i;
3086
57.5k
3087
57.5k
  if (
!tab || 57.5k
!bmap57.5k
)
3088
0
    return isl_basic_map_free(bmap);
3089
57.5k
  
if (57.5k
tab->empty57.5k
)
3090
75
    return bmap;
3091
57.5k
3092
189k
  
for (i = bmap->n_ineq - 1; 57.4k
i >= 0189k
;
--i131k
)
{131k
3093
131k
    if (!isl_tab_is_equality(tab, bmap->n_eq + i))
3094
131k
      continue;
3095
131k
    isl_basic_map_inequality_to_equality(bmap, i);
3096
919
    if (rotate_constraints(tab, 0, tab->n_eq + i + 1) < 0)
3097
0
      return isl_basic_map_free(bmap);
3098
919
    
if (919
rotate_constraints(tab, tab->n_eq + i + 1,919
3099
919
          bmap->n_ineq - i) < 0)
3100
0
      return isl_basic_map_free(bmap);
3101
919
    tab->n_eq++;
3102
57.4k
  }
3103
57.4k
3104
57.4k
  return bmap;
3105
57.5k
}
3106
3107
static int con_is_redundant(struct isl_tab *tab, struct isl_tab_var *var)
3108
732k
{
3109
732k
  if (!tab)
3110
0
    return -1;
3111
732k
  
if (732k
tab->rational732k
)
{70.5k
3112
70.5k
    int sgn = sign_of_min(tab, var);
3113
70.5k
    if (sgn < -1)
3114
0
      return -1;
3115
70.5k
    return sgn >= 0;
3116
732k
  } else {
3117
662k
    int irred = isl_tab_min_at_most_neg_one(tab, var);
3118
662k
    if (irred < 0)
3119
0
      return -1;
3120
662k
    return !irred;
3121
732k
  }
3122
732k
}
3123
3124
/* Check for (near) redundant constraints.
3125
 * A constraint is redundant if it is non-negative and if
3126
 * its minimal value (temporarily ignoring the non-negativity) is either
3127
 *  - zero (in case of rational tableaus), or
3128
 *  - strictly larger than -1 (in case of integer tableaus)
3129
 *
3130
 * We first mark all non-redundant and non-dead variables that
3131
 * are not frozen and not obviously negatively unbounded.
3132
 * Then we iterate over all marked variables if they can attain
3133
 * any values smaller than zero or at most negative one.
3134
 * If not, we mark the row as being redundant (assuming it hasn't
3135
 * been detected as being obviously redundant in the mean time).
3136
 */
3137
int isl_tab_detect_redundant(struct isl_tab *tab)
3138
180k
{
3139
180k
  int i;
3140
180k
  unsigned n_marked;
3141
180k
3142
180k
  if (!tab)
3143
0
    return -1;
3144
180k
  
if (180k
tab->empty180k
)
3145
2.64k
    return 0;
3146
177k
  
if (177k
tab->n_redundant == tab->n_row177k
)
3147
3.33k
    return 0;
3148
177k
3149
177k
  n_marked = 0;
3150
1.24M
  for (i = tab->n_redundant; 
i < tab->n_row1.24M
;
++i1.07M
)
{1.07M
3151
1.07M
    struct isl_tab_var *var = isl_tab_var_from_row(tab, i);
3152
942k
    var->marked = !var->frozen && var->is_nonneg;
3153
1.07M
    if (var->marked)
3154
486k
      n_marked++;
3155
1.07M
  }
3156
928k
  for (i = tab->n_dead; 
i < tab->n_col928k
;
++i753k
)
{753k
3157
753k
    struct isl_tab_var *var = var_from_col(tab, i);
3158
700k
    var->marked = !var->frozen && var->is_nonneg &&
3159
316k
      !min_is_manifestly_unbounded(tab, var);
3160
753k
    if (var->marked)
3161
88.0k
      n_marked++;
3162
753k
  }
3163
665k
  while (
n_marked665k
)
{496k
3164
496k
    struct isl_tab_var *var;
3165
496k
    int red;
3166
496k
    var = select_marked(tab);
3167
496k
    if (!var)
3168
5.75k
      break;
3169
496k
    var->marked = 0;
3170
490k
    n_marked--;
3171
490k
    red = con_is_redundant(tab, var);
3172
490k
    if (red < 0)
3173
0
      return -1;
3174
490k
    
if (490k
red && 490k
!var->is_redundant107k
)
3175
20.3k
      
if (20.3k
isl_tab_mark_redundant(tab, var->index) < 020.3k
)
3176
0
        return -1;
3177
6.74M
    
for (i = tab->n_dead; 490k
i < tab->n_col6.74M
;
++i6.25M
)
{6.25M
3178
6.25M
      var = var_from_col(tab, i);
3179
6.25M
      if (!var->marked)
3180
5.97M
        continue;
3181
272k
      
if (272k
!min_is_manifestly_unbounded(tab, var)272k
)
3182
197k
        continue;
3183
272k
      var->marked = 0;
3184
75.7k
      n_marked--;
3185
490k
    }
3186
490k
  }
3187
174k
3188
174k
  return 0;
3189
180k
}
3190
3191
int isl_tab_is_equality(struct isl_tab *tab, int con)
3192
2.14M
{
3193
2.14M
  int row;
3194
2.14M
  unsigned off;
3195
2.14M
3196
2.14M
  if (!tab)
3197
0
    return -1;
3198
2.14M
  
if (2.14M
tab->con[con].is_zero2.14M
)
3199
741k
    return 1;
3200
1.40M
  
if (1.40M
tab->con[con].is_redundant1.40M
)
3201
137k
    return 0;
3202
1.26M
  
if (1.26M
!tab->con[con].is_row1.26M
)
3203
698k
    return tab->con[con].index < tab->n_dead;
3204
1.26M
3205
1.26M
  row = tab->con[con].index;
3206
569k
3207
569k
  off = 2 + tab->M;
3208
569k
  return isl_int_is_zero(tab->mat->row[row][1]) &&
3209
60.9k
    !row_is_big(tab, row) &&
3210
569k
    isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
3211
1.26M
          tab->n_col - tab->n_dead) == -1;
3212
2.14M
}
3213
3214
/* Return the minimal value of the affine expression "f" with denominator
3215
 * "denom" in *opt, *opt_denom, assuming the tableau is not empty and
3216
 * the expression cannot attain arbitrarily small values.
3217
 * If opt_denom is NULL, then *opt is rounded up to the nearest integer.
3218
 * The return value reflects the nature of the result (empty, unbounded,
3219
 * minimal value returned in *opt).
3220
 *
3221
 * This function assumes that at least one more row and at least
3222
 * one more element in the constraint array are available in the tableau.
3223
 */
3224
enum isl_lp_result isl_tab_min(struct isl_tab *tab,
3225
  isl_int *f, isl_int denom, isl_int *opt, isl_int *opt_denom,
3226
  unsigned flags)
3227
184k
{
3228
184k
  int r;
3229
184k
  enum isl_lp_result res = isl_lp_ok;
3230
184k
  struct isl_tab_var *var;
3231
184k
  struct isl_tab_undo *snap;
3232
184k
3233
184k
  if (!tab)
3234
0
    return isl_lp_error;
3235
184k
3236
184k
  
if (184k
tab->empty184k
)
3237
14
    return isl_lp_empty;
3238
184k
3239
184k
  snap = isl_tab_snap(tab);
3240
184k
  r = isl_tab_add_row(tab, f);
3241
184k
  if (r < 0)
3242
0
    return isl_lp_error;
3243
184k
  var = &tab->con[r];
3244
401k
  for (;;) {
3245
401k
    int row, col;
3246
401k
    find_pivot(tab, var, var, -1, &row, &col);
3247
401k
    if (
row == var->index401k
)
{5.27k
3248
5.27k
      res = isl_lp_unbounded;
3249
5.27k
      break;
3250
401k
    }
3251
396k
    
if (396k
row == -1396k
)
3252
179k
      break;
3253
217k
    
if (217k
isl_tab_pivot(tab, row, col) < 0217k
)
3254
0
      return isl_lp_error;
3255
217k
  }
3256
184k
  
isl_int_mul184k
(tab->mat->row[var->index][0],184k
3257
184k
        tab->mat->row[var->index][0], denom);
3258
184k
  if (
ISL_FL_ISSET184k
(flags, ISL_TAB_SAVE_DUAL))
{9.90k
3259
9.90k
    int i;
3260
9.90k
3261
9.90k
    isl_vec_free(tab->dual);
3262
9.90k
    tab->dual = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_con);
3263
9.90k
    if (!tab->dual)
3264
0
      return isl_lp_error;
3265
9.90k
    
isl_int_set9.90k
(tab->dual->el[0], tab->mat->row[var->index][0]);9.90k
3266
354k
    for (i = 0; 
i < tab->n_con354k
;
++i344k
)
{344k
3267
344k
      int pos;
3268
344k
      if (
tab->con[i].is_row344k
)
{218k
3269
218k
        isl_int_set_si(tab->dual->el[1 + i], 0);
3270
218k
        continue;
3271
344k
      }
3272
344k
      pos = 2 + tab->M + tab->con[i].index;
3273
125k
      if (tab->con[i].negated)
3274
22.4k
        isl_int_neg(tab->dual->el[1 + i],
3275
125k
              tab->mat->row[var->index][pos]);
3276
125k
      else
3277
103k
        isl_int_set(tab->dual->el[1 + i],
3278
125k
              tab->mat->row[var->index][pos]);
3279
125k
    }
3280
184k
  }
3281
184k
  
if (184k
opt && 184k
res == isl_lp_ok184k
)
{179k
3282
179k
    if (
opt_denom179k
)
{37.0k
3283
37.0k
      isl_int_set(*opt, tab->mat->row[var->index][1]);
3284
37.0k
      isl_int_set(*opt_denom, tab->mat->row[var->index][0]);
3285
179k
    } else
3286
142k
      get_rounded_sample_value(tab, var, 1, opt);
3287
184k
  }
3288
184k
  if (isl_tab_rollback(tab, snap) < 0)
3289
0
    return isl_lp_error;
3290
184k
  return res;
3291
184k
}
3292
3293
/* Is the constraint at position "con" marked as being redundant?
3294
 * If it is marked as representing an equality, then it is not
3295
 * considered to be redundant.
3296
 * Note that isl_tab_mark_redundant marks both the isl_tab_var as
3297
 * redundant and moves the corresponding row into the first
3298
 * tab->n_redundant positions (or removes the row, assigning it index -1),
3299
 * so the final test is actually redundant itself.
3300
 */
3301
int isl_tab_is_redundant(struct isl_tab *tab, int con)
3302
1.66M
{
3303
1.66M
  if (!tab)
3304
0
    return -1;
3305
1.66M
  
if (1.66M
con < 0 || 1.66M
con >= tab->n_con1.66M
)
3306
0
    isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
3307
1.66M
      "position out of bounds", return -1);
3308
1.66M
  
if (1.66M
tab->con[con].is_zero1.66M
)
3309
100
    return 0;
3310
1.66M
  
if (1.66M
tab->con[con].is_redundant1.66M
)
3311
242k
    return 1;
3312
1.41M
  
return tab->con[con].is_row && 1.41M
tab->con[con].index < tab->n_redundant580k
;
3313
1.66M
}
3314
3315
/* Is variable "var" of "tab" fixed to a constant value by its row
3316
 * in the tableau?
3317
 * If so and if "value" is not NULL, then store this constant value
3318
 * in "value".
3319
 *
3320
 * That is, is it a row variable that only has non-zero coefficients
3321
 * for dead columns?
3322
 */
3323
static isl_bool is_constant(struct isl_tab *tab, struct isl_tab_var *var,
3324
  isl_int *value)
3325
4.30k
{
3326
4.30k
  unsigned off = 2 + tab->M;
3327
4.30k
  isl_mat *mat = tab->mat;
3328
4.30k
  int n;
3329
4.30k
  int row;
3330
4.30k
  int pos;
3331
4.30k
3332
4.30k
  if (!var->is_row)
3333
2.85k
    return isl_bool_false;
3334
4.30k
  row = var->index;
3335
1.44k
  if (row_is_big(tab, row))
3336
0
    return isl_bool_false;
3337
1.44k
  n = tab->n_col - tab->n_dead;
3338
1.44k
  pos = isl_seq_first_non_zero(mat->row[row] + off + tab->n_dead, n);
3339
1.44k
  if (pos != -1)
3340
1.36k
    return isl_bool_false;
3341
77
  
if (77
value77
)
3342
0
    isl_int_divexact(*value, mat->row[row][1], mat->row[row][0]);
3343
1.44k
  return isl_bool_true;
3344
4.30k
}
3345
3346
/* Has the variable "var' of "tab" reached a value that is greater than
3347
 * or equal (if sgn > 0) or smaller than or equal (if sgn < 0) to "target"?
3348
 * "tmp" has been initialized by the caller and can be used
3349
 * to perform local computations.
3350
 *
3351
 * If the sample value involves the big parameter, then any value
3352
 * is reached.
3353
 * Otherwise check if n/d >= t, i.e., n >= d * t (if sgn > 0)
3354
 * or n/d <= t, i.e., n <= d * t (if sgn < 0).
3355
 */
3356
static int reached(struct isl_tab *tab, struct isl_tab_var *var, int sgn,
3357
  isl_int target, isl_int *tmp)
3358
5.12k
{
3359
5.12k
  if (row_is_big(tab, var->index))
3360
0
    return 1;
3361
5.12k
  
isl_int_mul5.12k
(*tmp, tab->mat->row[var->index][0], target);5.12k
3362
5.12k
  if (sgn > 0)
3363
2.03k
    
return 2.03k
isl_int_ge2.03k
(tab->mat->row[var->index][1], *tmp);
3364
5.12k
  else
3365
3.09k
    
return 3.09k
isl_int_le3.09k
(tab->mat->row[var->index][1], *tmp);
3366
5.12k
}
3367
3368
/* Can variable "var" of "tab" attain the value "target" by
3369
 * pivoting up (if sgn > 0) or down (if sgn < 0)?
3370
 * If not, then pivot up [down] to the greatest [smallest]
3371
 * rational value.
3372
 * "tmp" has been initialized by the caller and can be used
3373
 * to perform local computations.
3374
 *
3375
 * If the variable is manifestly unbounded in the desired direction,
3376
 * then it can attain any value.
3377
 * Otherwise, it can be moved to a row.
3378
 * Continue pivoting until the target is reached.
3379
 * If no more pivoting can be performed, the maximal [minimal]
3380
 * rational value has been reached and the target cannot be reached.
3381
 * If the variable would be pivoted into a manifestly unbounded column,
3382
 * then the target can be reached.
3383
 */
3384
static isl_bool var_reaches(struct isl_tab *tab, struct isl_tab_var *var,
3385
  int sgn, isl_int target, isl_int *tmp)
3386
5.26k
{
3387
5.26k
  int row, col;
3388
5.26k
3389
5.26k
  if (
sgn < 0 && 5.26k
min_is_manifestly_unbounded(tab, var)4.22k
)
3390
1.99k
    return isl_bool_true;
3391
3.27k
  
if (3.27k
sgn > 0 && 3.27k
max_is_manifestly_unbounded(tab, var)1.04k
)
3392
0
    return isl_bool_true;
3393
3.27k
  
if (3.27k
to_row(tab, var, sgn) < 03.27k
)
3394
0
    return isl_bool_error;
3395
5.12k
  
while (3.27k
!reached(tab, var, sgn, target, tmp)5.12k
)
{4.64k
3396
4.64k
    find_pivot(tab, var, var, sgn, &row, &col);
3397
4.64k
    if (row == -1)
3398
1.16k
      return isl_bool_false;
3399
3.48k
    
if (3.48k
row == var->index3.48k
)
3400
1.62k
      return isl_bool_true;
3401
1.85k
    
if (1.85k
isl_tab_pivot(tab, row, col) < 01.85k
)
3402
0
      return isl_bool_error;
3403
3.27k
  }
3404
3.27k
3405
486
  return isl_bool_true;
3406
5.26k
}
3407
3408
/* Check if variable "var" of "tab" can only attain a single (integer)
3409
 * value, and, if so, add an equality constraint to fix the variable
3410
 * to this single value and store the result in "target".
3411
 * "target" and "tmp" have been initialized by the caller.
3412
 *
3413
 * Given the current sample value, round it down and check
3414
 * whether it is possible to attain a strictly smaller integer value.
3415
 * If so, the variable is not restricted to a single integer value.
3416
 * Otherwise, the search stops at the smallest rational value.
3417
 * Round up this value and check whether it is possible to attain
3418
 * a strictly greater integer value.
3419
 * If so, the variable is not restricted to a single integer value.
3420
 * Otherwise, the search stops at the greatest rational value.
3421
 * If rounding down this value yields a value that is different
3422
 * from rounding up the smallest rational value, then the variable
3423
 * cannot attain any integer value.  Mark the tableau empty.
3424
 * Otherwise, add an equality constraint that fixes the variable
3425
 * to the single integer value found.
3426
 */
3427
static isl_bool detect_constant_with_tmp(struct isl_tab *tab,
3428
  struct isl_tab_var *var, isl_int *target, isl_int *tmp)
3429
4.22k
{
3430
4.22k
  isl_bool reached;
3431
4.22k
  isl_vec *eq;
3432
4.22k
  int pos;
3433
4.22k
  isl_stat r;
3434
4.22k
3435
4.22k
  get_rounded_sample_value(tab, var, -1, target);
3436
4.22k
  isl_int_sub_ui(*target, *target, 1);
3437
4.22k
  reached = var_reaches(tab, var, -1, *target, tmp);
3438
4.22k
  if (
reached < 0 || 4.22k
reached4.22k
)
3439
3.18k
    return isl_bool_not(reached);
3440
4.22k
  get_rounded_sample_value(tab, var, 1, target);
3441
1.04k
  isl_int_add_ui(*target, *target, 1);
3442
1.04k
  reached = var_reaches(tab, var, 1, *target, tmp);
3443
1.04k
  if (
reached < 0 || 1.04k
reached1.04k
)
3444
919
    return isl_bool_not(reached);
3445
1.04k
  get_rounded_sample_value(tab, var, -1, tmp);
3446
122
  isl_int_sub_ui(*target, *target, 1);
3447
122
  if (
isl_int_ne122
(*target, *tmp))
{0
3448
0
    if (isl_tab_mark_empty(tab) < 0)
3449
0
      return isl_bool_error;
3450
0
    return isl_bool_false;
3451
122
  }
3452
122
3453
122
  
if (122
isl_tab_extend_cons(tab, 1) < 0122
)
3454
0
    return isl_bool_error;
3455
122
  eq = isl_vec_alloc(isl_tab_get_ctx(tab), 1 + tab->n_var);
3456
122
  if (!eq)
3457
0
    return isl_bool_error;
3458
122
  pos = var - tab->var;
3459
122
  isl_seq_clr(eq->el + 1, tab->n_var);
3460
122
  isl_int_set_si(eq->el[1 + pos], -1);
3461
122
  isl_int_set(eq->el[0], *target);
3462
122
  r = isl_tab_add_eq(tab, eq->el);
3463
122
  isl_vec_free(eq);
3464
122
3465
122
  return r < 0 ? 
isl_bool_error0
:
isl_bool_true122
;
3466
4.22k
}
3467
3468
/* Check if variable "var" of "tab" can only attain a single (integer)
3469
 * value, and, if so, add an equality constraint to fix the variable
3470
 * to this single value and store the result in "value" (if "value"
3471
 * is not NULL).
3472
 *
3473
 * If the current sample value involves the big parameter,
3474
 * then the variable cannot have a fixed integer value.
3475
 * If the variable is already fixed to a single value by its row, then
3476
 * there is no need to add another equality constraint.
3477
 *
3478
 * Otherwise, allocate some temporary variables and continue
3479
 * with detect_constant_with_tmp.
3480
 */
3481
static isl_bool get_constant(struct isl_tab *tab, struct isl_tab_var *var,
3482
  isl_int *value)
3483
4.30k
{
3484
4.30k
  isl_int target, tmp;
3485
4.30k
  isl_bool is_cst;
3486
4.30k
3487
4.30k
  if (
var->is_row && 4.30k
row_is_big(tab, var->index)1.44k
)
3488
0
    return isl_bool_false;
3489
4.30k
  is_cst = is_constant(tab, var, value);
3490
4.30k
  if (
is_cst < 0 || 4.30k
is_cst4.30k
)
3491
77
    return is_cst;
3492
4.30k
3493
4.22k
  
if (4.22k
!value4.22k
)
3494
1.41k
    isl_int_init(target);
3495
4.22k
  isl_int_init(tmp);
3496
4.22k
3497
4.22k
  is_cst = detect_constant_with_tmp(tab, var,
3498
4.22k
              value ? 
value2.81k
:
&target1.41k
, &tmp);
3499
4.22k
3500
4.22k
  isl_int_clear(tmp);
3501
4.22k
  if (!value)
3502
1.41k
    isl_int_clear(target);
3503
4.22k
3504
4.30k
  return is_cst;
3505
4.30k
}
3506
3507
/* Check if variable "var" of "tab" can only attain a single (integer)
3508
 * value, and, if so, add an equality constraint to fix the variable
3509
 * to this single value and store the result in "value" (if "value"
3510
 * is not NULL).
3511
 *
3512
 * For rational tableaus, nothing needs to be done.
3513
 */
3514
isl_bool isl_tab_is_constant(struct isl_tab *tab, int var, isl_int *value)
3515
2.81k
{
3516
2.81k
  if (!tab)
3517
0
    return isl_bool_error;
3518
2.81k
  
if (2.81k
var < 0 || 2.81k
var >= tab->n_var2.81k
)
3519
0
    isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
3520
2.81k
      "position out of bounds", return isl_bool_error);
3521
2.81k
  
if (2.81k
tab->rational2.81k
)
3522
0
    return isl_bool_false;
3523
2.81k
3524
2.81k
  return get_constant(tab, &tab->var[var], value);
3525
2.81k
}
3526
3527
/* Check if any of the variables of "tab" can only attain a single (integer)
3528
 * value, and, if so, add equality constraints to fix those variables
3529
 * to these single values.
3530
 *
3531
 * For rational tableaus, nothing needs to be done.
3532
 */
3533
isl_stat isl_tab_detect_constants(struct isl_tab *tab)
3534
299
{
3535
299
  int i;
3536
299
3537
299
  if (!tab)
3538
0
    return isl_stat_error;
3539
299
  
if (299
tab->rational299
)
3540
0
    return isl_stat_ok;
3541
299
3542
1.78k
  
for (i = 0; 299
i < tab->n_var1.78k
;
++i1.48k
)
{1.48k
3543
1.48k
    if (get_constant(tab, &tab->var[i], NULL) < 0)
3544
0
      return isl_stat_error;
3545
1.48k
  }
3546
299
3547
299
  return isl_stat_ok;
3548
299
}
3549
3550
/* Take a snapshot of the tableau that can be restored by a call to
3551
 * isl_tab_rollback.
3552
 */
3553
struct isl_tab_undo *isl_tab_snap(struct isl_tab *tab)
3554
867k
{
3555
867k
  if (!tab)
3556
0
    return NULL;
3557
867k
  tab->need_undo = 1;
3558
867k
  return tab->top;
3559
867k
}
3560
3561
/* Does "tab" need to keep track of undo information?
3562
 * That is, was a snapshot taken that may need to be restored?
3563
 */
3564
isl_bool isl_tab_need_undo(struct isl_tab *tab)
3565
106
{
3566
106
  if (!tab)
3567
0
    return isl_bool_error;
3568
106
3569
106
  return tab->need_undo;
3570
106
}
3571
3572
/* Remove all tracking of undo information from "tab", invalidating
3573
 * any snapshots that may have been taken of the tableau.
3574
 * Since all snapshots have been invalidated, there is also
3575
 * no need to start keeping track of undo information again.
3576
 */
3577
void isl_tab_clear_undo(struct isl_tab *tab)
3578
106
{
3579
106
  if (!tab)
3580
0
    return;
3581
106
3582
106
  free_undo(tab);
3583
106
  tab->need_undo = 0;
3584
106
}
3585
3586
/* Undo the operation performed by isl_tab_relax.
3587
 */
3588
static isl_stat unrelax(struct isl_tab *tab, struct isl_tab_var *var)
3589
  WARN_UNUSED;
3590
static isl_stat unrelax(struct isl_tab *tab, struct isl_tab_var *var)
3591
605
{
3592
605
  unsigned off = 2 + tab->M;
3593
605
3594
605
  if (
!var->is_row && 605
!max_is_manifestly_unbounded(tab, var)602
)
3595
78
    
if (78
to_row(tab, var, 1) < 078
)
3596
0
      return isl_stat_error;
3597
605
3598
605
  
if (605
var->is_row605
)
{81
3599
81
    isl_int_sub(tab->mat->row[var->index][1],
3600
81
        tab->mat->row[var->index][1], tab->mat->row[var->index][0]);
3601
81
    if (
var->is_nonneg81
)
{81
3602
81
      int sgn = restore_row(tab, var);
3603
81
      isl_assert(tab->mat->ctx, sgn >= 0,
3604
81
        return isl_stat_error);
3605
81
    }
3606
605
  } else {
3607
524
    int i;
3608
524
3609
2.69k
    for (i = 0; 
i < tab->n_row2.69k
;
++i2.16k
)
{2.16k
3610
2.16k
      if (isl_int_is_zero(tab->mat->row[i][off + var->index]))
3611
1.60k
        continue;
3612
569
      
isl_int_add569
(tab->mat->row[i][1], tab->mat->row[i][1],569
3613
569
          tab->mat->row[i][off + var->index]);
3614
569
    }
3615
524
3616
605
  }
3617
605
3618
605
  return isl_stat_ok;
3619
605
}
3620
3621
/* Undo the operation performed by isl_tab_unrestrict.
3622
 *
3623
 * In particular, mark the variable as being non-negative and make
3624
 * sure the sample value respects this constraint.
3625
 */
3626
static isl_stat ununrestrict(struct isl_tab *tab, struct isl_tab_var *var)
3627
282
{
3628
282
  var->is_nonneg = 1;
3629
282
3630
282
  if (
var->is_row && 282
restore_row(tab, var) < -1249
)
3631
0
    return isl_stat_error;
3632
282
3633
282
  return isl_stat_ok;
3634
282
}
3635
3636
/* Unmark the last redundant row in "tab" as being redundant.
3637
 * This undoes part of the modifications performed by isl_tab_mark_redundant.
3638
 * In particular, remove the redundant mark and make
3639
 * sure the sample value respects the constraint again.
3640
 * A variable that is marked non-negative by isl_tab_mark_redundant
3641
 * is covered by a separate undo record.
3642
 */
3643
static isl_stat restore_last_redundant(struct isl_tab *tab)
3644
467k
{
3645
467k
  struct isl_tab_var *var;
3646
467k
3647
467k
  if (tab->n_redundant < 1)
3648
0
    isl_die(isl_tab_get_ctx(tab), isl_error_internal,
3649
467k
      "no redundant rows", return isl_stat_error);
3650
467k
3651
467k
  var = isl_tab_var_from_row(tab, tab->n_redundant - 1);
3652
467k
  var->is_redundant = 0;
3653
467k
  tab->n_redundant--;
3654
467k
  restore_row(tab, var);
3655
467k
3656
467k
  return isl_stat_ok;
3657
467k
}
3658
3659
static isl_stat perform_undo_var(struct isl_tab *tab, struct isl_tab_undo *undo)
3660
  WARN_UNUSED;
3661
static isl_stat perform_undo_var(struct isl_tab *tab, struct isl_tab_undo *undo)
3662
1.89M
{
3663
1.89M
  struct isl_tab_var *var = var_from_index(tab, undo->u.var_index);
3664
1.89M
  switch (undo->type) {
3665
1.89M
  case isl_tab_undo_nonneg:
3666
408k
    var->is_nonneg = 0;
3667
1.89M
    break;
3668
1.89M
  case isl_tab_undo_redundant:
3669
345k
    if (
!var->is_row || 345k
var->index != tab->n_redundant - 1345k
)
3670
0
      isl_die(isl_tab_get_ctx(tab), isl_error_internal,
3671
345k
        "not undoing last redundant row", return -1);
3672
345k
    return restore_last_redundant(tab);
3673
345k
  case isl_tab_undo_freeze:
3674
249k
    var->frozen = 0;
3675
345k
    break;
3676
345k
  case isl_tab_undo_zero:
3677
40.5k
    var->is_zero = 0;
3678
40.5k
    if (!var->is_row)
3679
40.3k
      tab->n_dead--;
3680
345k
    break;
3681
851k
  case isl_tab_undo_allocate:
3682
851k
    if (
undo->u.var_index >= 0851k
)
{3.24k
3683
3.24k
      isl_assert(tab->mat->ctx, !var->is_row,
3684
3.24k
        return isl_stat_error);
3685
3.24k
      return drop_col(tab, var->index);
3686
851k
    }
3687
848k
    
if (848k
!var->is_row848k
)
{71.4k
3688
71.4k
      if (
!max_is_manifestly_unbounded(tab, var)71.4k
)
{40.5k
3689
40.5k
        if (to_row(tab, var, 1) < 0)
3690
0
          return isl_stat_error;
3691
71.4k
      } else 
if (30.9k
!min_is_manifestly_unbounded(tab, var)30.9k
)
{13.1k
3692
13.1k
        if (to_row(tab, var, -1) < 0)
3693
0
          return isl_stat_error;
3694
30.9k
      } else
3695
17.7k
        
if (17.7k
to_row(tab, var, 0) < 017.7k
)
3696
0
          return isl_stat_error;
3697
848k
    }
3698
848k
    return drop_row(tab, var->index);
3699
848k
  case isl_tab_undo_relax:
3700
848k
    return unrelax(tab, var);
3701
848k
  case isl_tab_undo_unrestrict:
3702
848k
    return ununrestrict(tab, var);
3703
848k
  default:
3704
0
    isl_die(tab->mat->ctx, isl_error_internal,
3705
1.89M
      "perform_undo_var called on invalid undo record",
3706
1.89M
      return isl_stat_error);
3707
1.89M
  }
3708
1.89M
3709
698k
  return isl_stat_ok;
3710
1.89M
}
3711
3712
/* Restore all rows that have been marked redundant by isl_tab_mark_redundant
3713
 * and that have been preserved in the tableau.
3714
 * Note that isl_tab_mark_redundant may also have marked some variables
3715
 * as being non-negative before marking them redundant.  These need
3716
 * to be removed as well as otherwise some constraints could end up
3717
 * getting marked redundant with respect to the variable.
3718
 */
3719
isl_stat isl_tab_restore_redundant(struct isl_tab *tab)
3720
95.9k
{
3721
95.9k
  if (!tab)
3722
0
    return isl_stat_error;
3723
95.9k
3724
95.9k
  
if (95.9k
tab->need_undo95.9k
)
3725
0
    isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
3726
95.9k
      "manually restoring redundant constraints "
3727
95.9k
      "interferes with undo history",
3728
95.9k
      return isl_stat_error);
3729
95.9k
3730
217k
  
while (95.9k
tab->n_redundant > 0217k
)
{121k
3731
121k
    if (
tab->row_var[tab->n_redundant - 1] >= 0121k
)
{107k
3732
107k
      struct isl_tab_var *var;
3733
107k
3734
107k
      var = isl_tab_var_from_row(tab, tab->n_redundant - 1);
3735
107k
      var->is_nonneg = 0;
3736
121k
    }
3737
121k
    restore_last_redundant(tab);
3738
121k
  }
3739
95.9k
  return isl_stat_ok;
3740
95.9k
}
3741
3742
/* Undo the addition of an integer division to the basic map representation
3743
 * of "tab" in position "pos".
3744
 */
3745
static isl_stat drop_bmap_div(struct isl_tab *tab, int pos)
3746
1.08k
{
3747
1.08k
  int off;
3748
1.08k
3749
1.08k
  off = tab->n_var - isl_basic_map_dim(tab->bmap, isl_dim_div);
3750
1.08k
  if (isl_basic_map_drop_div(tab->bmap, pos - off) < 0)
3751
0
    return isl_stat_error;
3752
1.08k
  
if (1.08k
tab->samples1.08k
)
{444
3753
444
    tab->samples = isl_mat_drop_cols(tab->samples, 1 + pos, 1);
3754
444
    if (!tab->samples)
3755
0
      return isl_stat_error;
3756
1.08k
  }
3757
1.08k
3758
1.08k
  return isl_stat_ok;
3759
1.08k
}
3760
3761
/* Restore the tableau to the state where the basic variables
3762
 * are those in "col_var".
3763
 * We first construct a list of variables that are currently in
3764
 * the basis, but shouldn't.  Then we iterate over all variables
3765
 * that should be in the basis and for each one that is currently
3766
 * not in the basis, we exchange it with one of the elements of the
3767
 * list constructed before.
3768
 * We can always find an appropriate variable to pivot with because
3769
 * the current basis is mapped to the old basis by a non-singular
3770
 * matrix and so we can never end up with a zero row.
3771
 */
3772
static int restore_basis(struct isl_tab *tab, int *col_var)
3773
583
{
3774
583
  int i, j;
3775
583
  int n_extra = 0;
3776
583
  int *extra = NULL;  /* current columns that contain bad stuff */
3777
583
  unsigned off = 2 + tab->M;
3778
583
3779
583
  extra = isl_alloc_array(tab->mat->ctx, int, tab->n_col);
3780
583
  if (
tab->n_col && 583
!extra583
)
3781
0
    goto error;
3782
6.99k
  
for (i = 0; 583
i < tab->n_col6.99k
;
++i6.41k
)
{6.41k
3783
52.8k
    for (j = 0; 
j < tab->n_col52.8k
;
++j46.4k
)
3784
51.4k
      
if (51.4k
tab->col_var[i] == col_var[j]51.4k
)
3785
4.95k
        break;
3786
6.41k
    if (j < tab->n_col)
3787
4.95k
      continue;
3788
6.41k
    extra[n_extra++] = i;
3789
1.46k
  }
3790
5.32k
  for (i = 0; 
i < tab->n_col && 5.32k
n_extra > 05.21k
;
++i4.74k
)
{4.74k
3791
4.74k
    struct isl_tab_var *var;
3792
4.74k
    int row;
3793
4.74k
3794
36.6k
    for (j = 0; 
j < tab->n_col36.6k
;
++j31.9k
)
3795
35.2k
      
if (35.2k
col_var[i] == tab->col_var[j]35.2k
)
3796
3.28k
        break;
3797
4.74k
    if (j < tab->n_col)
3798
3.28k
      continue;
3799
4.74k
    var = var_from_index(tab, col_var[i]);
3800
1.46k
    row = var->index;
3801
1.86k
    for (j = 0; 
j < n_extra1.86k
;
++j400
)
3802
1.86k
      
if (1.86k
!1.86k
isl_int_is_zero1.86k
(tab->mat->row[row][off+extra[j]]))
3803
1.46k
        break;
3804
1.46k
    isl_assert(tab->mat->ctx, j < n_extra, goto error);
3805
1.46k
    
if (1.46k
isl_tab_pivot(tab, row, extra[j]) < 01.46k
)
3806
0
      goto error;
3807
1.46k
    extra[j] = extra[--n_extra];
3808
1.46k
  }
3809
583
3810
583
  free(extra);
3811
583
  return 0;
3812
583
error:
3813
0
  free(extra);
3814
583
  return -1;
3815
583
}
3816
3817
/* Remove all samples with index n or greater, i.e., those samples
3818
 * that were added since we saved this number of samples in
3819
 * isl_tab_save_samples.
3820
 */
3821
static void drop_samples_since(struct isl_tab *tab, int n)
3822
20.4k
{
3823
20.4k
  int i;
3824
20.4k
3825
25.1k
  for (i = tab->n_sample - 1; 
i >= 0 && 25.1k
tab->n_sample > n23.6k
;
--i4.72k
)
{4.72k
3826
4.72k
    if (tab->sample_index[i] < n)
3827
1.78k
      continue;
3828
4.72k
3829
2.94k
    
if (2.94k
i != tab->n_sample - 12.94k
)
{1.94k
3830
1.94k
      int t = tab->sample_index[tab->n_sample-1];
3831
1.94k
      tab->sample_index[tab->n_sample-1] = tab->sample_index[i];
3832
1.94k
      tab->sample_index[i] = t;
3833
1.94k
      isl_mat_swap_rows(tab->samples, tab->n_sample-1, i);
3834
2.94k
    }
3835
2.94k
    tab->n_sample--;
3836
20.4k
  }
3837
20.4k
}
3838
3839
static isl_stat perform_undo(struct isl_tab *tab, struct isl_tab_undo *undo)
3840
  WARN_UNUSED;
3841
static isl_stat perform_undo(struct isl_tab *tab, struct isl_tab_undo *undo)
3842
2.22M
{
3843
2.22M
  switch (undo->type) {
3844
2.22M
  case isl_tab_undo_rational:
3845
10.1k
    tab->rational = 0;
3846
2.22M
    break;
3847
2.22M
  case isl_tab_undo_empty:
3848
55.4k
    tab->empty = 0;
3849
2.22M
    break;
3850
2.22M
  case isl_tab_undo_nonneg:
3851
1.89M
  case isl_tab_undo_redundant:
3852
1.89M
  case isl_tab_undo_freeze:
3853
1.89M
  case isl_tab_undo_zero:
3854
1.89M
  case isl_tab_undo_allocate:
3855
1.89M
  case isl_tab_undo_relax:
3856
1.89M
  case isl_tab_undo_unrestrict:
3857
1.89M
    return perform_undo_var(tab, undo);
3858
1.89M
  case isl_tab_undo_bmap_eq:
3859
1.89M
    return isl_basic_map_free_equality(tab->bmap, 1);
3860
1.89M
  case isl_tab_undo_bmap_ineq:
3861
1.89M
    return isl_basic_map_free_inequality(tab->bmap, 1);
3862
1.89M
  case isl_tab_undo_bmap_div:
3863
1.89M
    return drop_bmap_div(tab, undo->u.var_index);
3864
1.89M
  case isl_tab_undo_saved_basis:
3865
583
    if (restore_basis(tab, undo->u.col_var) < 0)
3866
0
      return isl_stat_error;
3867
583
    break;
3868
5.25k
  case isl_tab_undo_drop_sample:
3869
5.25k
    tab->n_outside--;
3870
5.25k
    break;
3871
20.4k
  case isl_tab_undo_saved_samples:
3872
20.4k
    drop_samples_since(tab, undo->u.n);
3873
20.4k
    break;
3874
2.17k
  case isl_tab_undo_callback:
3875
2.17k
    return undo->u.callback->run(undo->u.callback);
3876
583
  default:
3877
0
    isl_assert(tab->mat->ctx, 0, return isl_stat_error);
3878
2.22M
  }
3879
91.7k
  return isl_stat_ok;
3880
2.22M
}
3881
3882
/* Return the tableau to the state it was in when the snapshot "snap"
3883
 * was taken.
3884
 */
3885
int isl_tab_rollback(struct isl_tab *tab, struct isl_tab_undo *snap)
3886
782k
{
3887
782k
  struct isl_tab_undo *undo, *next;
3888
782k
3889
782k
  if (!tab)
3890
0
    return -1;
3891
782k
3892
782k
  tab->in_undo = 1;
3893
3.00M
  for (undo = tab->top; 
undo && 3.00M
undo != &tab->bottom3.00M
;
undo = next2.22M
)
{2.41M
3894
2.41M
    next = undo->next;
3895
2.41M
    if (undo == snap)
3896
184k
      break;
3897
2.22M
    
if (2.22M
perform_undo(tab, undo) < 02.22M
)
{0
3898
0
      tab->top = undo;
3899
0
      free_undo(tab);
3900
0
      tab->in_undo = 0;
3901
0
      return -1;
3902
2.22M
    }
3903
2.22M
    free_undo_record(undo);
3904
2.22M
  }
3905
782k
  tab->in_undo = 0;
3906
782k
  tab->top = undo;
3907
782k
  if (!undo)
3908
0
    return -1;
3909
782k
  return 0;
3910
782k
}
3911
3912
/* The given row "row" represents an inequality violated by all
3913
 * points in the tableau.  Check for some special cases of such
3914
 * separating constraints.
3915
 * In particular, if the row has been reduced to the constant -1,
3916
 * then we know the inequality is adjacent (but opposite) to
3917
 * an equality in the tableau.
3918
 * If the row has been reduced to r = c*(-1 -r'), with r' an inequality
3919
 * of the tableau and c a positive constant, then the inequality
3920
 * is adjacent (but opposite) to the inequality r'.
3921
 */
3922
static enum isl_ineq_type separation_type(struct isl_tab *tab, unsigned row)
3923
67.5k
{
3924
67.5k
  int pos;
3925
67.5k
  unsigned off = 2 + tab->M;
3926
67.5k
3927
67.5k
  if (tab->rational)
3928
9.20k
    return isl_ineq_separate;
3929
67.5k
3930
58.3k
  
if (58.3k
!58.3k
isl_int_is_one58.3k
(tab->mat->row[row][0]))
3931
147
    return isl_ineq_separate;
3932
58.3k
3933
58.3k
  pos = isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
3934
58.2k
          tab->n_col - tab->n_dead);
3935
58.2k
  if (
pos == -158.2k
)
{7.17k
3936
7.17k
    if (isl_int_is_negone(tab->mat->row[row][1]))
3937
6.02k
      return isl_ineq_adj_eq;
3938
7.17k
    else
3939
1.15k
      return isl_ineq_separate;
3940
58.2k
  }
3941
58.2k
3942
51.0k
  
if (51.0k
!51.0k
isl_int_eq51.0k
(tab->mat->row[row][1],
3943
51.0k
      tab->mat->row[row][off + tab->n_dead + pos]))
3944
20.5k
    return isl_ineq_separate;
3945
51.0k
3946
51.0k
  pos = isl_seq_first_non_zero(
3947
30.4k
      tab->mat->row[row] + off + tab->n_dead + pos + 1,
3948
30.4k
      tab->n_col - tab->n_dead - pos - 1);
3949
30.4k
3950
30.4k
  return pos == -1 ? 
isl_ineq_adj_ineq28.3k
:
isl_ineq_separate2.08k
;
3951
67.5k
}
3952
3953
/* Check the effect of inequality "ineq" on the tableau "tab".
3954
 * The result may be
3955
 *  isl_ineq_redundant: satisfied by all points in the tableau
3956
 *  isl_ineq_separate:  satisfied by no point in the tableau
3957
 *  isl_ineq_cut:   satisfied by some by not all points
3958
 *  isl_ineq_adj_eq:  adjacent to an equality
3959
 *  isl_ineq_adj_ineq:  adjacent to an inequality.
3960
 */
3961
enum isl_ineq_type isl_tab_ineq_type(struct isl_tab *tab, isl_int *ineq)
3962
385k
{
3963
385k
  enum isl_ineq_type type = isl_ineq_error;
3964
385k
  struct isl_tab_undo *snap = NULL;
3965
385k
  int con;
3966
385k
  int row;
3967
385k
3968
385k
  if (!tab)
3969
0
    return isl_ineq_error;
3970
385k
3971
385k
  
if (385k
isl_tab_extend_cons(tab, 1) < 0385k
)
3972
0
    return isl_ineq_error;
3973
385k
3974
385k
  snap = isl_tab_snap(tab);
3975
385k
3976
385k
  con = isl_tab_add_row(tab, ineq);
3977
385k
  if (con < 0)
3978
0
    goto error;
3979
385k
3980
385k
  row = tab->con[con].index;
3981
385k
  if (isl_tab_row_is_redundant(tab, row))
3982
0
    type = isl_ineq_redundant;
3983
385k
  else 
if (385k
isl_int_is_neg385k
(tab->mat->row[row][1]) &&385k
3984
385k
     (tab->rational ||
3985
121k
        isl_int_abs_ge(tab->mat->row[row][1],
3986
385k
           tab->mat->row[row][0]))) {
3987
143k
    int nonneg = at_least_zero(tab, &tab->con[con]);
3988
143k
    if (nonneg < 0)
3989
0
      goto error;
3990
143k
    
if (143k
nonneg143k
)
3991
75.8k
      type = isl_ineq_cut;
3992
143k
    else
3993
67.5k
      type = separation_type(tab, row);
3994
385k
  } else {
3995
242k
    int red = con_is_redundant(tab, &tab->con[con]);
3996
242k
    if (red < 0)
3997
0
      goto error;
3998
242k
    
if (242k
!red242k
)
3999
71.8k
      type = isl_ineq_cut;
4000
242k
    else
4001
170k
      type = isl_ineq_redundant;
4002
385k
  }
4003
385k
4004
385k
  
if (385k
isl_tab_rollback(tab, snap)385k
)
4005
0
    return isl_ineq_error;
4006
385k
  return type;
4007
385k
error:
4008
385k
  return isl_ineq_error;
4009
385k
}
4010
4011
isl_stat isl_tab_track_bmap(struct isl_tab *tab, __isl_take isl_basic_map *bmap)
4012
146k
{
4013
146k
  bmap = isl_basic_map_cow(bmap);
4014
146k
  if (
!tab || 146k
!bmap146k
)
4015
0
    goto error;
4016
146k
4017
146k
  
if (146k
tab->empty146k
)
{3.90k
4018
3.90k
    bmap = isl_basic_map_set_to_empty(bmap);
4019
3.90k
    if (!bmap)
4020
0
      goto error;
4021
3.90k
    tab->bmap = bmap;
4022
3.90k
    return isl_stat_ok;
4023
146k
  }
4024
146k
4025
142k
  
isl_assert142k
(tab->mat->ctx, tab->n_eq == bmap->n_eq, goto error);142k
4026
142k
  
isl_assert142k
(tab->mat->ctx,142k
4027
142k
        tab->n_con == bmap->n_eq + bmap->n_ineq, goto error);
4028
142k
4029
142k
  tab->bmap = bmap;
4030
142k
4031
142k
  return isl_stat_ok;
4032
142k
error:
4033
0
  isl_basic_map_free(bmap);
4034
142k
  return isl_stat_error;
4035
146k
}
4036
4037
isl_stat isl_tab_track_bset(struct isl_tab *tab, __isl_take isl_basic_set *bset)
4038
963
{
4039
963
  return isl_tab_track_bmap(tab, bset_to_bmap(bset));
4040
963
}
4041
4042
__isl_keep isl_basic_set *isl_tab_peek_bset(struct isl_tab *tab)
4043
25.4k
{
4044
25.4k
  if (!tab)
4045
0
    return NULL;
4046
25.4k
4047
25.4k
  return bset_from_bmap(tab->bmap);
4048
25.4k
}
4049
4050
static void isl_tab_print_internal(__isl_keep struct isl_tab *tab,
4051
  FILE *out, int indent)
4052
0
{
4053
0
  unsigned r, c;
4054
0
  int i;
4055
0
4056
0
  if (
!tab0
)
{0
4057
0
    fprintf(out, "%*snull tab\n", indent, "");
4058
0
    return;
4059
0
  }
4060
0
  fprintf(out, "%*sn_redundant: %d, n_dead: %d", indent, "",
4061
0
    tab->n_redundant, tab->n_dead);
4062
0
  if (tab->rational)
4063
0
    fprintf(out, ", rational");
4064
0
  if (tab->empty)
4065
0
    fprintf(out, ", empty");
4066
0
  fprintf(out, "\n");
4067
0
  fprintf(out, "%*s[", indent, "");
4068
0
  for (i = 0; 
i < tab->n_var0
;
++i0
)
{0
4069
0
    if (i)
4070
0
      fprintf(out, (i == tab->n_param ||
4071
0
              
i == tab->n_var - tab->n_div0
) ?
"; "0
4072
0
                    : ", ");
4073
0
    fprintf(out, "%c%d%s", tab->var[i].is_row ? 
'r'0
:
'c'0
,
4074
0
          tab->var[i].index,
4075
0
          tab->var[i].is_zero ? " [=0]" :
4076
0
          
tab->var[i].is_redundant ? 0
" [R]"0
:
""0
);
4077
0
  }
4078
0
  fprintf(out, "]\n");
4079
0
  fprintf(out, "%*s[", indent, "");
4080
0
  for (i = 0; 
i < tab->n_con0
;
++i0
)
{0
4081
0
    if (i)
4082
0
      fprintf(out, ", ");
4083
0
    fprintf(out, "%c%d%s", tab->con[i].is_row ? 
'r'0
:
'c'0
,
4084
0
          tab->con[i].index,
4085
0
          tab->con[i].is_zero ? " [=0]" :
4086
0
          
tab->con[i].is_redundant ? 0
" [R]"0
:
""0
);
4087
0
  }
4088
0
  fprintf(out, "]\n");
4089
0
  fprintf(out, "%*s[", indent, "");
4090
0
  for (i = 0; 
i < tab->n_row0
;
++i0
)
{0
4091
0
    const char *sign = "";
4092
0
    if (i)
4093
0
      fprintf(out, ", ");
4094
0
    if (
tab->row_sign0
)
{0
4095
0
      if (tab->row_sign[i] == isl_tab_row_unknown)
4096
0
        sign = "?";
4097
0
      else 
if (0
tab->row_sign[i] == isl_tab_row_neg0
)
4098
0
        sign = "-";
4099
0
      else 
if (0
tab->row_sign[i] == isl_tab_row_pos0
)
4100
0
        sign = "+";
4101
0
      else
4102
0
        sign = "+-";
4103
0
    }
4104
0
    fprintf(out, "r%d: %d%s%s", i, tab->row_var[i],
4105
0
        isl_tab_var_from_row(tab, i)->is_nonneg ? 
" [>=0]"0
:
""0
, sign);
4106
0
  }
4107
0
  fprintf(out, "]\n");
4108
0
  fprintf(out, "%*s[", indent, "");
4109
0
  for (i = 0; 
i < tab->n_col0
;
++i0
)
{0
4110
0
    if (i)
4111
0
      fprintf(out, ", ");
4112
0
    fprintf(out, "c%d: %d%s", i, tab->col_var[i],
4113
0
        var_from_col(tab, i)->is_nonneg ? 
" [>=0]"0
:
""0
);
4114
0
  }
4115
0
  fprintf(out, "]\n");
4116
0
  r = tab->mat->n_row;
4117
0
  tab->mat->n_row = tab->n_row;
4118
0
  c = tab->mat->n_col;
4119
0
  tab->mat->n_col = 2 + tab->M + tab->n_col;
4120
0
  isl_mat_print_internal(tab->mat, out, indent);
4121
0
  tab->mat->n_row = r;
4122
0
  tab->mat->n_col = c;
4123
0
  if (tab->bmap)
4124
0
    isl_basic_map_print_internal(tab->bmap, out, indent);
4125
0
}
4126
4127
void isl_tab_dump(__isl_keep struct isl_tab *tab)
4128
0
{
4129
0
  isl_tab_print_internal(tab, stderr, 0);
4130
0
}