Coverage Report

Created: 2017-10-03 07:32

/Users/buildslave/jenkins/sharedspace/clang-stage2-coverage-R@2/llvm/tools/polly/lib/External/isl/isl_farkas.c
Line
Count
Source (jump to first uncovered line)
1
/*
2
 * Copyright 2010      INRIA Saclay
3
 *
4
 * Use of this software is governed by the MIT license
5
 *
6
 * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
7
 * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
8
 * 91893 Orsay, France 
9
 */
10
11
#include <isl_map_private.h>
12
#include <isl/set.h>
13
#include <isl_space_private.h>
14
#include <isl_seq.h>
15
16
/*
17
 * Let C be a cone and define
18
 *
19
 *  C' := { y | forall x in C : y x >= 0 }
20
 *
21
 * C' contains the coefficients of all linear constraints
22
 * that are valid for C.
23
 * Furthermore, C'' = C.
24
 *
25
 * If C is defined as { x | A x >= 0 }
26
 * then any element in C' must be a non-negative combination
27
 * of the rows of A, i.e., y = t A with t >= 0.  That is,
28
 *
29
 *  C' = { y | exists t >= 0 : y = t A }
30
 *
31
 * If any of the rows in A actually represents an equality, then
32
 * also negative combinations of this row are allowed and so the
33
 * non-negativity constraint on the corresponding element of t
34
 * can be dropped.
35
 *
36
 * A polyhedron P = { x | b + A x >= 0 } can be represented
37
 * in homogeneous coordinates by the cone
38
 * C = { [z,x] | b z + A x >= and z >= 0 }
39
 * The valid linear constraints on C correspond to the valid affine
40
 * constraints on P.
41
 * This is essentially Farkas' lemma.
42
 *
43
 * Since
44
 *          [ 1 0 ]
45
 *    [ w y ] = [t_0 t] [ b A ]
46
 *
47
 * we have
48
 *
49
 *  C' = { w, y | exists t_0, t >= 0 : y = t A and w = t_0 + t b }
50
 * or
51
 *
52
 *  C' = { w, y | exists t >= 0 : y = t A and w - t b >= 0 }
53
 *
54
 * In practice, we introduce an extra variable (w), shifting all
55
 * other variables to the right, and an extra inequality
56
 * (w - t b >= 0) corresponding to the positivity constraint on
57
 * the homogeneous coordinate.
58
 *
59
 * When going back from coefficients to solutions, we immediately
60
 * plug in 1 for z, which corresponds to shifting all variables
61
 * to the left, with the leftmost ending up in the constant position.
62
 */
63
64
/* Add the given prefix to all named isl_dim_set dimensions in "dim".
65
 */
66
static __isl_give isl_space *isl_space_prefix(__isl_take isl_space *dim,
67
  const char *prefix)
68
872
{
69
872
  int i;
70
872
  isl_ctx *ctx;
71
872
  unsigned nvar;
72
872
  size_t prefix_len = strlen(prefix);
73
872
74
872
  if (!dim)
75
0
    return NULL;
76
872
77
872
  ctx = isl_space_get_ctx(dim);
78
872
  nvar = isl_space_dim(dim, isl_dim_set);
79
872
80
2.00k
  for (i = 0; 
i < nvar2.00k
;
++i1.13k
) {
81
1.13k
    const char *name;
82
1.13k
    char *prefix_name;
83
1.13k
84
1.13k
    name = isl_space_get_dim_name(dim, isl_dim_set, i);
85
1.13k
    if (!name)
86
436
      continue;
87
694
88
694
    
prefix_name = 694
isl_alloc_array694
(ctx, char,
89
694
                prefix_len + strlen(name) + 1);
90
694
    if (!prefix_name)
91
0
      goto error;
92
694
    memcpy(prefix_name, prefix, prefix_len);
93
694
    strcpy(prefix_name + prefix_len, name);
94
694
95
694
    dim = isl_space_set_dim_name(dim, isl_dim_set, i, prefix_name);
96
694
    free(prefix_name);
97
694
  }
98
872
99
872
  return dim;
100
0
error:
101
0
  isl_space_free(dim);
102
0
  return NULL;
103
872
}
104
105
/* Given a dimension specification of the solutions space, construct
106
 * a dimension specification for the space of coefficients.
107
 *
108
 * In particular transform
109
 *
110
 *  [params] -> { S }
111
 *
112
 * to
113
 *
114
 *  { coefficients[[cst, params] -> S] }
115
 *
116
 * and prefix each dimension name with "c_".
117
 */
118
static __isl_give isl_space *isl_space_coefficients(__isl_take isl_space *dim)
119
436
{
120
436
  isl_space *dim_param;
121
436
  unsigned nvar;
122
436
  unsigned nparam;
123
436
124
436
  nvar = isl_space_dim(dim, isl_dim_set);
125
436
  nparam = isl_space_dim(dim, isl_dim_param);
126
436
  dim_param = isl_space_copy(dim);
127
436
  dim_param = isl_space_drop_dims(dim_param, isl_dim_set, 0, nvar);
128
436
  dim_param = isl_space_move_dims(dim_param, isl_dim_set, 0,
129
436
         isl_dim_param, 0, nparam);
130
436
  dim_param = isl_space_prefix(dim_param, "c_");
131
436
  dim_param = isl_space_insert_dims(dim_param, isl_dim_set, 0, 1);
132
436
  dim_param = isl_space_set_dim_name(dim_param, isl_dim_set, 0, "c_cst");
133
436
  dim = isl_space_drop_dims(dim, isl_dim_param, 0, nparam);
134
436
  dim = isl_space_prefix(dim, "c_");
135
436
  dim = isl_space_join(isl_space_from_domain(dim_param),
136
436
         isl_space_from_range(dim));
137
436
  dim = isl_space_wrap(dim);
138
436
  dim = isl_space_set_tuple_name(dim, isl_dim_set, "coefficients");
139
436
140
436
  return dim;
141
436
}
142
143
/* Drop the given prefix from all named dimensions of type "type" in "dim".
144
 */
145
static __isl_give isl_space *isl_space_unprefix(__isl_take isl_space *dim,
146
  enum isl_dim_type type, const char *prefix)
147
6
{
148
6
  int i;
149
6
  unsigned n;
150
6
  size_t prefix_len = strlen(prefix);
151
6
152
6
  n = isl_space_dim(dim, type);
153
6
154
9
  for (i = 0; 
i < n9
;
++i3
) {
155
3
    const char *name;
156
3
157
3
    name = isl_space_get_dim_name(dim, type, i);
158
3
    if (!name)
159
0
      continue;
160
3
    
if (3
strncmp(name, prefix, prefix_len)3
)
161
3
      continue;
162
0
163
0
    dim = isl_space_set_dim_name(dim, type, i, name + prefix_len);
164
0
  }
165
6
166
6
  return dim;
167
6
}
168
169
/* Given a dimension specification of the space of coefficients, construct
170
 * a dimension specification for the space of solutions.
171
 *
172
 * In particular transform
173
 *
174
 *  { coefficients[[cst, params] -> S] }
175
 *
176
 * to
177
 *
178
 *  [params] -> { S }
179
 *
180
 * and drop the "c_" prefix from the dimension names.
181
 */
182
static __isl_give isl_space *isl_space_solutions(__isl_take isl_space *dim)
183
3
{
184
3
  unsigned nparam;
185
3
186
3
  dim = isl_space_unwrap(dim);
187
3
  dim = isl_space_drop_dims(dim, isl_dim_in, 0, 1);
188
3
  dim = isl_space_unprefix(dim, isl_dim_in, "c_");
189
3
  dim = isl_space_unprefix(dim, isl_dim_out, "c_");
190
3
  nparam = isl_space_dim(dim, isl_dim_in);
191
3
  dim = isl_space_move_dims(dim, isl_dim_param, 0, isl_dim_in, 0, nparam);
192
3
  dim = isl_space_range(dim);
193
3
194
3
  return dim;
195
3
}
196
197
/* Return the rational universe basic set in the given space.
198
 */
199
static __isl_give isl_basic_set *rational_universe(__isl_take isl_space *space)
200
7
{
201
7
  isl_basic_set *bset;
202
7
203
7
  bset = isl_basic_set_universe(space);
204
7
  bset = isl_basic_set_set_rational(bset);
205
7
206
7
  return bset;
207
7
}
208
209
/* Compute the dual of "bset" by applying Farkas' lemma.
210
 * As explained above, we add an extra dimension to represent
211
 * the coefficient of the constant term when going from solutions
212
 * to coefficients (shift == 1) and we drop the extra dimension when going
213
 * in the opposite direction (shift == -1).  "dim" is the space in which
214
 * the dual should be created.
215
 *
216
 * If "bset" is (obviously) empty, then the way this emptiness
217
 * is represented by the constraints does not allow for the application
218
 * of the standard farkas algorithm.  We therefore handle this case
219
 * specifically and return the universe basic set.
220
 */
221
static __isl_give isl_basic_set *farkas(__isl_take isl_space *space,
222
  __isl_take isl_basic_set *bset, int shift)
223
434
{
224
434
  int i, j, k;
225
434
  isl_basic_set *dual = NULL;
226
434
  unsigned total;
227
434
228
434
  if (
isl_basic_set_plain_is_empty(bset)434
) {
229
2
    isl_basic_set_free(bset);
230
2
    return rational_universe(space);
231
2
  }
232
432
233
432
  total = isl_basic_set_total_dim(bset);
234
432
235
432
  dual = isl_basic_set_alloc_space(space, bset->n_eq + bset->n_ineq,
236
432
          total, bset->n_ineq + (shift > 0));
237
432
  dual = isl_basic_set_set_rational(dual);
238
432
239
1.56k
  for (i = 0; 
i < bset->n_eq + bset->n_ineq1.56k
;
++i1.12k
) {
240
1.12k
    k = isl_basic_set_alloc_div(dual);
241
1.12k
    if (k < 0)
242
0
      goto error;
243
1.12k
    
isl_int_set_si1.12k
(dual->div[k][0], 0);
244
1.12k
  }
245
432
246
1.55k
  
for (i = 0; 432
i < total1.55k
;
++i1.12k
) {
247
1.12k
    k = isl_basic_set_alloc_equality(dual);
248
1.12k
    if (k < 0)
249
0
      goto error;
250
1.12k
    isl_seq_clr(dual->eq[k], 1 + shift + total);
251
1.12k
    isl_int_set_si(dual->eq[k][1 + shift + i], -1);
252
3.39k
    for (j = 0; 
j < bset->n_eq3.39k
;
++j2.27k
)
253
2.27k
      isl_int_set(dual->eq[k][1 + shift + total + j],
254
1.12k
            bset->eq[j][1 + i]);
255
2.41k
    for (j = 0; 
j < bset->n_ineq2.41k
;
++j1.29k
)
256
1.29k
      isl_int_set(dual->eq[k][1 + shift + total + bset->n_eq + j],
257
1.12k
            bset->ineq[j][1 + i]);
258
1.12k
  }
259
432
260
782
  
for (i = 0; 432
i < bset->n_ineq782
;
++i350
) {
261
350
    k = isl_basic_set_alloc_inequality(dual);
262
350
    if (k < 0)
263
0
      goto error;
264
350
    isl_seq_clr(dual->ineq[k],
265
350
          1 + shift + total + bset->n_eq + bset->n_ineq);
266
350
    isl_int_set_si(dual->ineq[k][1 + shift + total + bset->n_eq + i], 1);
267
350
  }
268
432
269
432
  
if (432
shift > 0432
) {
270
430
    k = isl_basic_set_alloc_inequality(dual);
271
430
    if (k < 0)
272
0
      goto error;
273
430
    isl_seq_clr(dual->ineq[k], 2 + total);
274
430
    isl_int_set_si(dual->ineq[k][1], 1);
275
1.20k
    for (j = 0; 
j < bset->n_eq1.20k
;
++j778
)
276
778
      isl_int_neg(dual->ineq[k][2 + total + j],
277
430
            bset->eq[j][0]);
278
778
    for (j = 0; 
j < bset->n_ineq778
;
++j348
)
279
348
      isl_int_neg(dual->ineq[k][2 + total + bset->n_eq + j],
280
430
            bset->ineq[j][0]);
281
430
  }
282
432
283
432
  dual = isl_basic_set_remove_divs(dual);
284
432
  dual = isl_basic_set_simplify(dual);
285
432
  dual = isl_basic_set_finalize(dual);
286
432
287
432
  isl_basic_set_free(bset);
288
432
  return dual;
289
0
error:
290
0
  isl_basic_set_free(bset);
291
0
  isl_basic_set_free(dual);
292
0
  return NULL;
293
434
}
294
295
/* Construct a basic set containing the tuples of coefficients of all
296
 * valid affine constraints on the given basic set.
297
 */
298
__isl_give isl_basic_set *isl_basic_set_coefficients(
299
  __isl_take isl_basic_set *bset)
300
431
{
301
431
  isl_space *dim;
302
431
303
431
  if (!bset)
304
0
    return NULL;
305
431
  
if (431
bset->n_div431
)
306
0
    isl_die(bset->ctx, isl_error_invalid,
307
431
      "input set not allowed to have local variables",
308
431
      goto error);
309
431
310
431
  dim = isl_basic_set_get_space(bset);
311
431
  dim = isl_space_coefficients(dim);
312
431
313
431
  return farkas(dim, bset, 1);
314
0
error:
315
0
  isl_basic_set_free(bset);
316
0
  return NULL;
317
431
}
318
319
/* Construct a basic set containing the elements that satisfy all
320
 * affine constraints whose coefficient tuples are
321
 * contained in the given basic set.
322
 */
323
__isl_give isl_basic_set *isl_basic_set_solutions(
324
  __isl_take isl_basic_set *bset)
325
3
{
326
3
  isl_space *dim;
327
3
328
3
  if (!bset)
329
0
    return NULL;
330
3
  
if (3
bset->n_div3
)
331
0
    isl_die(bset->ctx, isl_error_invalid,
332
3
      "input set not allowed to have local variables",
333
3
      goto error);
334
3
335
3
  dim = isl_basic_set_get_space(bset);
336
3
  dim = isl_space_solutions(dim);
337
3
338
3
  return farkas(dim, bset, -1);
339
0
error:
340
0
  isl_basic_set_free(bset);
341
0
  return NULL;
342
3
}
343
344
/* Construct a basic set containing the tuples of coefficients of all
345
 * valid affine constraints on the given set.
346
 */
347
__isl_give isl_basic_set *isl_set_coefficients(__isl_take isl_set *set)
348
281
{
349
281
  int i;
350
281
  isl_basic_set *coeff;
351
281
352
281
  if (!set)
353
0
    return NULL;
354
281
  
if (281
set->n == 0281
) {
355
5
    isl_space *space = isl_set_get_space(set);
356
5
    space = isl_space_coefficients(space);
357
5
    isl_set_free(set);
358
5
    return rational_universe(space);
359
5
  }
360
276
361
276
  coeff = isl_basic_set_coefficients(isl_basic_set_copy(set->p[0]));
362
276
363
364
  for (i = 1; 
i < set->n364
;
++i88
) {
364
88
    isl_basic_set *bset, *coeff_i;
365
88
    bset = isl_basic_set_copy(set->p[i]);
366
88
    coeff_i = isl_basic_set_coefficients(bset);
367
88
    coeff = isl_basic_set_intersect(coeff, coeff_i);
368
88
  }
369
281
370
281
  isl_set_free(set);
371
281
  return coeff;
372
281
}
373
374
/* Wrapper around isl_basic_set_coefficients for use
375
 * as a isl_basic_set_list_map callback.
376
 */
377
static __isl_give isl_basic_set *coefficients_wrap(
378
  __isl_take isl_basic_set *bset, void *user)
379
64
{
380
64
  return isl_basic_set_coefficients(bset);
381
64
}
382
383
/* Replace the elements of "list" by the result of applying
384
 * isl_basic_set_coefficients to them.
385
 */
386
__isl_give isl_basic_set_list *isl_basic_set_list_coefficients(
387
  __isl_take isl_basic_set_list *list)
388
64
{
389
64
  return isl_basic_set_list_map(list, &coefficients_wrap, NULL);
390
64
}
391
392
/* Construct a basic set containing the elements that satisfy all
393
 * affine constraints whose coefficient tuples are
394
 * contained in the given set.
395
 */
396
__isl_give isl_basic_set *isl_set_solutions(__isl_take isl_set *set)
397
0
{
398
0
  int i;
399
0
  isl_basic_set *sol;
400
0
401
0
  if (!set)
402
0
    return NULL;
403
0
  
if (0
set->n == 00
) {
404
0
    isl_space *space = isl_set_get_space(set);
405
0
    space = isl_space_solutions(space);
406
0
    isl_set_free(set);
407
0
    return rational_universe(space);
408
0
  }
409
0
410
0
  sol = isl_basic_set_solutions(isl_basic_set_copy(set->p[0]));
411
0
412
0
  for (i = 1; 
i < set->n0
;
++i0
) {
413
0
    isl_basic_set *bset, *sol_i;
414
0
    bset = isl_basic_set_copy(set->p[i]);
415
0
    sol_i = isl_basic_set_solutions(bset);
416
0
    sol = isl_basic_set_intersect(sol, sol_i);
417
0
  }
418
0
419
0
  isl_set_free(set);
420
0
  return sol;
421
0
}