nexmon – Blame information for rev 1
?pathlinks?
Rev | Author | Line No. | Line |
---|---|---|---|
1 | office | 1 | /* |
2 | * Copyright 2008-2009 Katholieke Universiteit Leuven |
||
3 | * |
||
4 | * Use of this software is governed by the GNU LGPLv2.1 license |
||
5 | * |
||
6 | * Written by Sven Verdoolaege, K.U.Leuven, Departement |
||
7 | * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium |
||
8 | */ |
||
9 | |||
10 | #include <isl_ctx_private.h> |
||
11 | #include <isl_map_private.h> |
||
12 | #include "isl_sample.h" |
||
13 | #include "isl_sample_piplib.h" |
||
14 | #include <isl/vec.h> |
||
15 | #include <isl/mat.h> |
||
16 | #include <isl/seq.h> |
||
17 | #include "isl_equalities.h" |
||
18 | #include "isl_tab.h" |
||
19 | #include "isl_basis_reduction.h" |
||
20 | #include <isl_factorization.h> |
||
21 | #include <isl_point_private.h> |
||
22 | #include <isl_options_private.h> |
||
23 | |||
24 | static struct isl_vec *empty_sample(struct isl_basic_set *bset) |
||
25 | { |
||
26 | struct isl_vec *vec; |
||
27 | |||
28 | vec = isl_vec_alloc(bset->ctx, 0); |
||
29 | isl_basic_set_free(bset); |
||
30 | return vec; |
||
31 | } |
||
32 | |||
33 | /* Construct a zero sample of the same dimension as bset. |
||
34 | * As a special case, if bset is zero-dimensional, this |
||
35 | * function creates a zero-dimensional sample point. |
||
36 | */ |
||
37 | static struct isl_vec *zero_sample(struct isl_basic_set *bset) |
||
38 | { |
||
39 | unsigned dim; |
||
40 | struct isl_vec *sample; |
||
41 | |||
42 | dim = isl_basic_set_total_dim(bset); |
||
43 | sample = isl_vec_alloc(bset->ctx, 1 + dim); |
||
44 | if (sample) { |
||
45 | isl_int_set_si(sample->el[0], 1); |
||
46 | isl_seq_clr(sample->el + 1, dim); |
||
47 | } |
||
48 | isl_basic_set_free(bset); |
||
49 | return sample; |
||
50 | } |
||
51 | |||
52 | static struct isl_vec *interval_sample(struct isl_basic_set *bset) |
||
53 | { |
||
54 | int i; |
||
55 | isl_int t; |
||
56 | struct isl_vec *sample; |
||
57 | |||
58 | bset = isl_basic_set_simplify(bset); |
||
59 | if (!bset) |
||
60 | return NULL; |
||
61 | if (isl_basic_set_plain_is_empty(bset)) |
||
62 | return empty_sample(bset); |
||
63 | if (bset->n_eq == 0 && bset->n_ineq == 0) |
||
64 | return zero_sample(bset); |
||
65 | |||
66 | sample = isl_vec_alloc(bset->ctx, 2); |
||
67 | if (!sample) |
||
68 | goto error; |
||
69 | if (!bset) |
||
70 | return NULL; |
||
71 | isl_int_set_si(sample->block.data[0], 1); |
||
72 | |||
73 | if (bset->n_eq > 0) { |
||
74 | isl_assert(bset->ctx, bset->n_eq == 1, goto error); |
||
75 | isl_assert(bset->ctx, bset->n_ineq == 0, goto error); |
||
76 | if (isl_int_is_one(bset->eq[0][1])) |
||
77 | isl_int_neg(sample->el[1], bset->eq[0][0]); |
||
78 | else { |
||
79 | isl_assert(bset->ctx, isl_int_is_negone(bset->eq[0][1]), |
||
80 | goto error); |
||
81 | isl_int_set(sample->el[1], bset->eq[0][0]); |
||
82 | } |
||
83 | isl_basic_set_free(bset); |
||
84 | return sample; |
||
85 | } |
||
86 | |||
87 | isl_int_init(t); |
||
88 | if (isl_int_is_one(bset->ineq[0][1])) |
||
89 | isl_int_neg(sample->block.data[1], bset->ineq[0][0]); |
||
90 | else |
||
91 | isl_int_set(sample->block.data[1], bset->ineq[0][0]); |
||
92 | for (i = 1; i < bset->n_ineq; ++i) { |
||
93 | isl_seq_inner_product(sample->block.data, |
||
94 | bset->ineq[i], 2, &t); |
||
95 | if (isl_int_is_neg(t)) |
||
96 | break; |
||
97 | } |
||
98 | isl_int_clear(t); |
||
99 | if (i < bset->n_ineq) { |
||
100 | isl_vec_free(sample); |
||
101 | return empty_sample(bset); |
||
102 | } |
||
103 | |||
104 | isl_basic_set_free(bset); |
||
105 | return sample; |
||
106 | error: |
||
107 | isl_basic_set_free(bset); |
||
108 | isl_vec_free(sample); |
||
109 | return NULL; |
||
110 | } |
||
111 | |||
112 | static struct isl_mat *independent_bounds(struct isl_basic_set *bset) |
||
113 | { |
||
114 | int i, j, n; |
||
115 | struct isl_mat *dirs = NULL; |
||
116 | struct isl_mat *bounds = NULL; |
||
117 | unsigned dim; |
||
118 | |||
119 | if (!bset) |
||
120 | return NULL; |
||
121 | |||
122 | dim = isl_basic_set_n_dim(bset); |
||
123 | bounds = isl_mat_alloc(bset->ctx, 1+dim, 1+dim); |
||
124 | if (!bounds) |
||
125 | return NULL; |
||
126 | |||
127 | isl_int_set_si(bounds->row[0][0], 1); |
||
128 | isl_seq_clr(bounds->row[0]+1, dim); |
||
129 | bounds->n_row = 1; |
||
130 | |||
131 | if (bset->n_ineq == 0) |
||
132 | return bounds; |
||
133 | |||
134 | dirs = isl_mat_alloc(bset->ctx, dim, dim); |
||
135 | if (!dirs) { |
||
136 | isl_mat_free(bounds); |
||
137 | return NULL; |
||
138 | } |
||
139 | isl_seq_cpy(dirs->row[0], bset->ineq[0]+1, dirs->n_col); |
||
140 | isl_seq_cpy(bounds->row[1], bset->ineq[0], bounds->n_col); |
||
141 | for (j = 1, n = 1; n < dim && j < bset->n_ineq; ++j) { |
||
142 | int pos; |
||
143 | |||
144 | isl_seq_cpy(dirs->row[n], bset->ineq[j]+1, dirs->n_col); |
||
145 | |||
146 | pos = isl_seq_first_non_zero(dirs->row[n], dirs->n_col); |
||
147 | if (pos < 0) |
||
148 | continue; |
||
149 | for (i = 0; i < n; ++i) { |
||
150 | int pos_i; |
||
151 | pos_i = isl_seq_first_non_zero(dirs->row[i], dirs->n_col); |
||
152 | if (pos_i < pos) |
||
153 | continue; |
||
154 | if (pos_i > pos) |
||
155 | break; |
||
156 | isl_seq_elim(dirs->row[n], dirs->row[i], pos, |
||
157 | dirs->n_col, NULL); |
||
158 | pos = isl_seq_first_non_zero(dirs->row[n], dirs->n_col); |
||
159 | if (pos < 0) |
||
160 | break; |
||
161 | } |
||
162 | if (pos < 0) |
||
163 | continue; |
||
164 | if (i < n) { |
||
165 | int k; |
||
166 | isl_int *t = dirs->row[n]; |
||
167 | for (k = n; k > i; --k) |
||
168 | dirs->row[k] = dirs->row[k-1]; |
||
169 | dirs->row[i] = t; |
||
170 | } |
||
171 | ++n; |
||
172 | isl_seq_cpy(bounds->row[n], bset->ineq[j], bounds->n_col); |
||
173 | } |
||
174 | isl_mat_free(dirs); |
||
175 | bounds->n_row = 1+n; |
||
176 | return bounds; |
||
177 | } |
||
178 | |||
179 | static void swap_inequality(struct isl_basic_set *bset, int a, int b) |
||
180 | { |
||
181 | isl_int *t = bset->ineq[a]; |
||
182 | bset->ineq[a] = bset->ineq[b]; |
||
183 | bset->ineq[b] = t; |
||
184 | } |
||
185 | |||
186 | /* Skew into positive orthant and project out lineality space. |
||
187 | * |
||
188 | * We perform a unimodular transformation that turns a selected |
||
189 | * maximal set of linearly independent bounds into constraints |
||
190 | * on the first dimensions that impose that these first dimensions |
||
191 | * are non-negative. In particular, the constraint matrix is lower |
||
192 | * triangular with positive entries on the diagonal and negative |
||
193 | * entries below. |
||
194 | * If "bset" has a lineality space then these constraints (and therefore |
||
195 | * all constraints in bset) only involve the first dimensions. |
||
196 | * The remaining dimensions then do not appear in any constraints and |
||
197 | * we can select any value for them, say zero. We therefore project |
||
198 | * out this final dimensions and plug in the value zero later. This |
||
199 | * is accomplished by simply dropping the final columns of |
||
200 | * the unimodular transformation. |
||
201 | */ |
||
202 | static struct isl_basic_set *isl_basic_set_skew_to_positive_orthant( |
||
203 | struct isl_basic_set *bset, struct isl_mat **T) |
||
204 | { |
||
205 | struct isl_mat *U = NULL; |
||
206 | struct isl_mat *bounds = NULL; |
||
207 | int i, j; |
||
208 | unsigned old_dim, new_dim; |
||
209 | |||
210 | *T = NULL; |
||
211 | if (!bset) |
||
212 | return NULL; |
||
213 | |||
214 | isl_assert(bset->ctx, isl_basic_set_n_param(bset) == 0, goto error); |
||
215 | isl_assert(bset->ctx, bset->n_div == 0, goto error); |
||
216 | isl_assert(bset->ctx, bset->n_eq == 0, goto error); |
||
217 | |||
218 | old_dim = isl_basic_set_n_dim(bset); |
||
219 | /* Try to move (multiples of) unit rows up. */ |
||
220 | for (i = 0, j = 0; i < bset->n_ineq; ++i) { |
||
221 | int pos = isl_seq_first_non_zero(bset->ineq[i]+1, old_dim); |
||
222 | if (pos < 0) |
||
223 | continue; |
||
224 | if (isl_seq_first_non_zero(bset->ineq[i]+1+pos+1, |
||
225 | old_dim-pos-1) >= 0) |
||
226 | continue; |
||
227 | if (i != j) |
||
228 | swap_inequality(bset, i, j); |
||
229 | ++j; |
||
230 | } |
||
231 | bounds = independent_bounds(bset); |
||
232 | if (!bounds) |
||
233 | goto error; |
||
234 | new_dim = bounds->n_row - 1; |
||
235 | bounds = isl_mat_left_hermite(bounds, 1, &U, NULL); |
||
236 | if (!bounds) |
||
237 | goto error; |
||
238 | U = isl_mat_drop_cols(U, 1 + new_dim, old_dim - new_dim); |
||
239 | bset = isl_basic_set_preimage(bset, isl_mat_copy(U)); |
||
240 | if (!bset) |
||
241 | goto error; |
||
242 | *T = U; |
||
243 | isl_mat_free(bounds); |
||
244 | return bset; |
||
245 | error: |
||
246 | isl_mat_free(bounds); |
||
247 | isl_mat_free(U); |
||
248 | isl_basic_set_free(bset); |
||
249 | return NULL; |
||
250 | } |
||
251 | |||
252 | /* Find a sample integer point, if any, in bset, which is known |
||
253 | * to have equalities. If bset contains no integer points, then |
||
254 | * return a zero-length vector. |
||
255 | * We simply remove the known equalities, compute a sample |
||
256 | * in the resulting bset, using the specified recurse function, |
||
257 | * and then transform the sample back to the original space. |
||
258 | */ |
||
259 | static struct isl_vec *sample_eq(struct isl_basic_set *bset, |
||
260 | struct isl_vec *(*recurse)(struct isl_basic_set *)) |
||
261 | { |
||
262 | struct isl_mat *T; |
||
263 | struct isl_vec *sample; |
||
264 | |||
265 | if (!bset) |
||
266 | return NULL; |
||
267 | |||
268 | bset = isl_basic_set_remove_equalities(bset, &T, NULL); |
||
269 | sample = recurse(bset); |
||
270 | if (!sample || sample->size == 0) |
||
271 | isl_mat_free(T); |
||
272 | else |
||
273 | sample = isl_mat_vec_product(T, sample); |
||
274 | return sample; |
||
275 | } |
||
276 | |||
277 | /* Return a matrix containing the equalities of the tableau |
||
278 | * in constraint form. The tableau is assumed to have |
||
279 | * an associated bset that has been kept up-to-date. |
||
280 | */ |
||
281 | static struct isl_mat *tab_equalities(struct isl_tab *tab) |
||
282 | { |
||
283 | int i, j; |
||
284 | int n_eq; |
||
285 | struct isl_mat *eq; |
||
286 | struct isl_basic_set *bset; |
||
287 | |||
288 | if (!tab) |
||
289 | return NULL; |
||
290 | |||
291 | bset = isl_tab_peek_bset(tab); |
||
292 | isl_assert(tab->mat->ctx, bset, return NULL); |
||
293 | |||
294 | n_eq = tab->n_var - tab->n_col + tab->n_dead; |
||
295 | if (tab->empty || n_eq == 0) |
||
296 | return isl_mat_alloc(tab->mat->ctx, 0, tab->n_var); |
||
297 | if (n_eq == tab->n_var) |
||
298 | return isl_mat_identity(tab->mat->ctx, tab->n_var); |
||
299 | |||
300 | eq = isl_mat_alloc(tab->mat->ctx, n_eq, tab->n_var); |
||
301 | if (!eq) |
||
302 | return NULL; |
||
303 | for (i = 0, j = 0; i < tab->n_con; ++i) { |
||
304 | if (tab->con[i].is_row) |
||
305 | continue; |
||
306 | if (tab->con[i].index >= 0 && tab->con[i].index >= tab->n_dead) |
||
307 | continue; |
||
308 | if (i < bset->n_eq) |
||
309 | isl_seq_cpy(eq->row[j], bset->eq[i] + 1, tab->n_var); |
||
310 | else |
||
311 | isl_seq_cpy(eq->row[j], |
||
312 | bset->ineq[i - bset->n_eq] + 1, tab->n_var); |
||
313 | ++j; |
||
314 | } |
||
315 | isl_assert(bset->ctx, j == n_eq, goto error); |
||
316 | return eq; |
||
317 | error: |
||
318 | isl_mat_free(eq); |
||
319 | return NULL; |
||
320 | } |
||
321 | |||
322 | /* Compute and return an initial basis for the bounded tableau "tab". |
||
323 | * |
||
324 | * If the tableau is either full-dimensional or zero-dimensional, |
||
325 | * the we simply return an identity matrix. |
||
326 | * Otherwise, we construct a basis whose first directions correspond |
||
327 | * to equalities. |
||
328 | */ |
||
329 | static struct isl_mat *initial_basis(struct isl_tab *tab) |
||
330 | { |
||
331 | int n_eq; |
||
332 | struct isl_mat *eq; |
||
333 | struct isl_mat *Q; |
||
334 | |||
335 | tab->n_unbounded = 0; |
||
336 | tab->n_zero = n_eq = tab->n_var - tab->n_col + tab->n_dead; |
||
337 | if (tab->empty || n_eq == 0 || n_eq == tab->n_var) |
||
338 | return isl_mat_identity(tab->mat->ctx, 1 + tab->n_var); |
||
339 | |||
340 | eq = tab_equalities(tab); |
||
341 | eq = isl_mat_left_hermite(eq, 0, NULL, &Q); |
||
342 | if (!eq) |
||
343 | return NULL; |
||
344 | isl_mat_free(eq); |
||
345 | |||
346 | Q = isl_mat_lin_to_aff(Q); |
||
347 | return Q; |
||
348 | } |
||
349 | |||
350 | /* Given a tableau representing a set, find and return |
||
351 | * an integer point in the set, if there is any. |
||
352 | * |
||
353 | * We perform a depth first search |
||
354 | * for an integer point, by scanning all possible values in the range |
||
355 | * attained by a basis vector, where an initial basis may have been set |
||
356 | * by the calling function. Otherwise an initial basis that exploits |
||
357 | * the equalities in the tableau is created. |
||
358 | * tab->n_zero is currently ignored and is clobbered by this function. |
||
359 | * |
||
360 | * The tableau is allowed to have unbounded direction, but then |
||
361 | * the calling function needs to set an initial basis, with the |
||
362 | * unbounded directions last and with tab->n_unbounded set |
||
363 | * to the number of unbounded directions. |
||
364 | * Furthermore, the calling functions needs to add shifted copies |
||
365 | * of all constraints involving unbounded directions to ensure |
||
366 | * that any feasible rational value in these directions can be rounded |
||
367 | * up to yield a feasible integer value. |
||
368 | * In particular, let B define the given basis x' = B x |
||
369 | * and let T be the inverse of B, i.e., X = T x'. |
||
370 | * Let a x + c >= 0 be a constraint of the set represented by the tableau, |
||
371 | * or a T x' + c >= 0 in terms of the given basis. Assume that |
||
372 | * the bounded directions have an integer value, then we can safely |
||
373 | * round up the values for the unbounded directions if we make sure |
||
374 | * that x' not only satisfies the original constraint, but also |
||
375 | * the constraint "a T x' + c + s >= 0" with s the sum of all |
||
376 | * negative values in the last n_unbounded entries of "a T". |
||
377 | * The calling function therefore needs to add the constraint |
||
378 | * a x + c + s >= 0. The current function then scans the first |
||
379 | * directions for an integer value and once those have been found, |
||
380 | * it can compute "T ceil(B x)" to yield an integer point in the set. |
||
381 | * Note that during the search, the first rows of B may be changed |
||
382 | * by a basis reduction, but the last n_unbounded rows of B remain |
||
383 | * unaltered and are also not mixed into the first rows. |
||
384 | * |
||
385 | * The search is implemented iteratively. "level" identifies the current |
||
386 | * basis vector. "init" is true if we want the first value at the current |
||
387 | * level and false if we want the next value. |
||
388 | * |
||
389 | * The initial basis is the identity matrix. If the range in some direction |
||
390 | * contains more than one integer value, we perform basis reduction based |
||
391 | * on the value of ctx->opt->gbr |
||
392 | * - ISL_GBR_NEVER: never perform basis reduction |
||
393 | * - ISL_GBR_ONCE: only perform basis reduction the first |
||
394 | * time such a range is encountered |
||
395 | * - ISL_GBR_ALWAYS: always perform basis reduction when |
||
396 | * such a range is encountered |
||
397 | * |
||
398 | * When ctx->opt->gbr is set to ISL_GBR_ALWAYS, then we allow the basis |
||
399 | * reduction computation to return early. That is, as soon as it |
||
400 | * finds a reasonable first direction. |
||
401 | */ |
||
402 | struct isl_vec *isl_tab_sample(struct isl_tab *tab) |
||
403 | { |
||
404 | unsigned dim; |
||
405 | unsigned gbr; |
||
406 | struct isl_ctx *ctx; |
||
407 | struct isl_vec *sample; |
||
408 | struct isl_vec *min; |
||
409 | struct isl_vec *max; |
||
410 | enum isl_lp_result res; |
||
411 | int level; |
||
412 | int init; |
||
413 | int reduced; |
||
414 | struct isl_tab_undo **snap; |
||
415 | |||
416 | if (!tab) |
||
417 | return NULL; |
||
418 | if (tab->empty) |
||
419 | return isl_vec_alloc(tab->mat->ctx, 0); |
||
420 | |||
421 | if (!tab->basis) |
||
422 | tab->basis = initial_basis(tab); |
||
423 | if (!tab->basis) |
||
424 | return NULL; |
||
425 | isl_assert(tab->mat->ctx, tab->basis->n_row == tab->n_var + 1, |
||
426 | return NULL); |
||
427 | isl_assert(tab->mat->ctx, tab->basis->n_col == tab->n_var + 1, |
||
428 | return NULL); |
||
429 | |||
430 | ctx = tab->mat->ctx; |
||
431 | dim = tab->n_var; |
||
432 | gbr = ctx->opt->gbr; |
||
433 | |||
434 | if (tab->n_unbounded == tab->n_var) { |
||
435 | sample = isl_tab_get_sample_value(tab); |
||
436 | sample = isl_mat_vec_product(isl_mat_copy(tab->basis), sample); |
||
437 | sample = isl_vec_ceil(sample); |
||
438 | sample = isl_mat_vec_inverse_product(isl_mat_copy(tab->basis), |
||
439 | sample); |
||
440 | return sample; |
||
441 | } |
||
442 | |||
443 | if (isl_tab_extend_cons(tab, dim + 1) < 0) |
||
444 | return NULL; |
||
445 | |||
446 | min = isl_vec_alloc(ctx, dim); |
||
447 | max = isl_vec_alloc(ctx, dim); |
||
448 | snap = isl_alloc_array(ctx, struct isl_tab_undo *, dim); |
||
449 | |||
450 | if (!min || !max || !snap) |
||
451 | goto error; |
||
452 | |||
453 | level = 0; |
||
454 | init = 1; |
||
455 | reduced = 0; |
||
456 | |||
457 | while (level >= 0) { |
||
458 | int empty = 0; |
||
459 | if (init) { |
||
460 | res = isl_tab_min(tab, tab->basis->row[1 + level], |
||
461 | ctx->one, &min->el[level], NULL, 0); |
||
462 | if (res == isl_lp_empty) |
||
463 | empty = 1; |
||
464 | isl_assert(ctx, res != isl_lp_unbounded, goto error); |
||
465 | if (res == isl_lp_error) |
||
466 | goto error; |
||
467 | if (!empty && isl_tab_sample_is_integer(tab)) |
||
468 | break; |
||
469 | isl_seq_neg(tab->basis->row[1 + level] + 1, |
||
470 | tab->basis->row[1 + level] + 1, dim); |
||
471 | res = isl_tab_min(tab, tab->basis->row[1 + level], |
||
472 | ctx->one, &max->el[level], NULL, 0); |
||
473 | isl_seq_neg(tab->basis->row[1 + level] + 1, |
||
474 | tab->basis->row[1 + level] + 1, dim); |
||
475 | isl_int_neg(max->el[level], max->el[level]); |
||
476 | if (res == isl_lp_empty) |
||
477 | empty = 1; |
||
478 | isl_assert(ctx, res != isl_lp_unbounded, goto error); |
||
479 | if (res == isl_lp_error) |
||
480 | goto error; |
||
481 | if (!empty && isl_tab_sample_is_integer(tab)) |
||
482 | break; |
||
483 | if (!empty && !reduced && |
||
484 | ctx->opt->gbr != ISL_GBR_NEVER && |
||
485 | isl_int_lt(min->el[level], max->el[level])) { |
||
486 | unsigned gbr_only_first; |
||
487 | if (ctx->opt->gbr == ISL_GBR_ONCE) |
||
488 | ctx->opt->gbr = ISL_GBR_NEVER; |
||
489 | tab->n_zero = level; |
||
490 | gbr_only_first = ctx->opt->gbr_only_first; |
||
491 | ctx->opt->gbr_only_first = |
||
492 | ctx->opt->gbr == ISL_GBR_ALWAYS; |
||
493 | tab = isl_tab_compute_reduced_basis(tab); |
||
494 | ctx->opt->gbr_only_first = gbr_only_first; |
||
495 | if (!tab || !tab->basis) |
||
496 | goto error; |
||
497 | reduced = 1; |
||
498 | continue; |
||
499 | } |
||
500 | reduced = 0; |
||
501 | snap[level] = isl_tab_snap(tab); |
||
502 | } else |
||
503 | isl_int_add_ui(min->el[level], min->el[level], 1); |
||
504 | |||
505 | if (empty || isl_int_gt(min->el[level], max->el[level])) { |
||
506 | level--; |
||
507 | init = 0; |
||
508 | if (level >= 0) |
||
509 | if (isl_tab_rollback(tab, snap[level]) < 0) |
||
510 | goto error; |
||
511 | continue; |
||
512 | } |
||
513 | isl_int_neg(tab->basis->row[1 + level][0], min->el[level]); |
||
514 | if (isl_tab_add_valid_eq(tab, tab->basis->row[1 + level]) < 0) |
||
515 | goto error; |
||
516 | isl_int_set_si(tab->basis->row[1 + level][0], 0); |
||
517 | if (level + tab->n_unbounded < dim - 1) { |
||
518 | ++level; |
||
519 | init = 1; |
||
520 | continue; |
||
521 | } |
||
522 | break; |
||
523 | } |
||
524 | |||
525 | if (level >= 0) { |
||
526 | sample = isl_tab_get_sample_value(tab); |
||
527 | if (!sample) |
||
528 | goto error; |
||
529 | if (tab->n_unbounded && !isl_int_is_one(sample->el[0])) { |
||
530 | sample = isl_mat_vec_product(isl_mat_copy(tab->basis), |
||
531 | sample); |
||
532 | sample = isl_vec_ceil(sample); |
||
533 | sample = isl_mat_vec_inverse_product( |
||
534 | isl_mat_copy(tab->basis), sample); |
||
535 | } |
||
536 | } else |
||
537 | sample = isl_vec_alloc(ctx, 0); |
||
538 | |||
539 | ctx->opt->gbr = gbr; |
||
540 | isl_vec_free(min); |
||
541 | isl_vec_free(max); |
||
542 | free(snap); |
||
543 | return sample; |
||
544 | error: |
||
545 | ctx->opt->gbr = gbr; |
||
546 | isl_vec_free(min); |
||
547 | isl_vec_free(max); |
||
548 | free(snap); |
||
549 | return NULL; |
||
550 | } |
||
551 | |||
552 | static struct isl_vec *sample_bounded(struct isl_basic_set *bset); |
||
553 | |||
554 | /* Compute a sample point of the given basic set, based on the given, |
||
555 | * non-trivial factorization. |
||
556 | */ |
||
557 | static __isl_give isl_vec *factored_sample(__isl_take isl_basic_set *bset, |
||
558 | __isl_take isl_factorizer *f) |
||
559 | { |
||
560 | int i, n; |
||
561 | isl_vec *sample = NULL; |
||
562 | isl_ctx *ctx; |
||
563 | unsigned nparam; |
||
564 | unsigned nvar; |
||
565 | |||
566 | ctx = isl_basic_set_get_ctx(bset); |
||
567 | if (!ctx) |
||
568 | goto error; |
||
569 | |||
570 | nparam = isl_basic_set_dim(bset, isl_dim_param); |
||
571 | nvar = isl_basic_set_dim(bset, isl_dim_set); |
||
572 | |||
573 | sample = isl_vec_alloc(ctx, 1 + isl_basic_set_total_dim(bset)); |
||
574 | if (!sample) |
||
575 | goto error; |
||
576 | isl_int_set_si(sample->el[0], 1); |
||
577 | |||
578 | bset = isl_morph_basic_set(isl_morph_copy(f->morph), bset); |
||
579 | |||
580 | for (i = 0, n = 0; i < f->n_group; ++i) { |
||
581 | isl_basic_set *bset_i; |
||
582 | isl_vec *sample_i; |
||
583 | |||
584 | bset_i = isl_basic_set_copy(bset); |
||
585 | bset_i = isl_basic_set_drop_constraints_involving(bset_i, |
||
586 | nparam + n + f->len[i], nvar - n - f->len[i]); |
||
587 | bset_i = isl_basic_set_drop_constraints_involving(bset_i, |
||
588 | nparam, n); |
||
589 | bset_i = isl_basic_set_drop(bset_i, isl_dim_set, |
||
590 | n + f->len[i], nvar - n - f->len[i]); |
||
591 | bset_i = isl_basic_set_drop(bset_i, isl_dim_set, 0, n); |
||
592 | |||
593 | sample_i = sample_bounded(bset_i); |
||
594 | if (!sample_i) |
||
595 | goto error; |
||
596 | if (sample_i->size == 0) { |
||
597 | isl_basic_set_free(bset); |
||
598 | isl_factorizer_free(f); |
||
599 | isl_vec_free(sample); |
||
600 | return sample_i; |
||
601 | } |
||
602 | isl_seq_cpy(sample->el + 1 + nparam + n, |
||
603 | sample_i->el + 1, f->len[i]); |
||
604 | isl_vec_free(sample_i); |
||
605 | |||
606 | n += f->len[i]; |
||
607 | } |
||
608 | |||
609 | f->morph = isl_morph_inverse(f->morph); |
||
610 | sample = isl_morph_vec(isl_morph_copy(f->morph), sample); |
||
611 | |||
612 | isl_basic_set_free(bset); |
||
613 | isl_factorizer_free(f); |
||
614 | return sample; |
||
615 | error: |
||
616 | isl_basic_set_free(bset); |
||
617 | isl_factorizer_free(f); |
||
618 | isl_vec_free(sample); |
||
619 | return NULL; |
||
620 | } |
||
621 | |||
622 | /* Given a basic set that is known to be bounded, find and return |
||
623 | * an integer point in the basic set, if there is any. |
||
624 | * |
||
625 | * After handling some trivial cases, we construct a tableau |
||
626 | * and then use isl_tab_sample to find a sample, passing it |
||
627 | * the identity matrix as initial basis. |
||
628 | */ |
||
629 | static struct isl_vec *sample_bounded(struct isl_basic_set *bset) |
||
630 | { |
||
631 | unsigned dim; |
||
632 | struct isl_ctx *ctx; |
||
633 | struct isl_vec *sample; |
||
634 | struct isl_tab *tab = NULL; |
||
635 | isl_factorizer *f; |
||
636 | |||
637 | if (!bset) |
||
638 | return NULL; |
||
639 | |||
640 | if (isl_basic_set_plain_is_empty(bset)) |
||
641 | return empty_sample(bset); |
||
642 | |||
643 | dim = isl_basic_set_total_dim(bset); |
||
644 | if (dim == 0) |
||
645 | return zero_sample(bset); |
||
646 | if (dim == 1) |
||
647 | return interval_sample(bset); |
||
648 | if (bset->n_eq > 0) |
||
649 | return sample_eq(bset, sample_bounded); |
||
650 | |||
651 | f = isl_basic_set_factorizer(bset); |
||
652 | if (!f) |
||
653 | goto error; |
||
654 | if (f->n_group != 0) |
||
655 | return factored_sample(bset, f); |
||
656 | isl_factorizer_free(f); |
||
657 | |||
658 | ctx = bset->ctx; |
||
659 | |||
660 | tab = isl_tab_from_basic_set(bset, 1); |
||
661 | if (tab && tab->empty) { |
||
662 | isl_tab_free(tab); |
||
663 | ISL_F_SET(bset, ISL_BASIC_SET_EMPTY); |
||
664 | sample = isl_vec_alloc(bset->ctx, 0); |
||
665 | isl_basic_set_free(bset); |
||
666 | return sample; |
||
667 | } |
||
668 | |||
669 | if (!ISL_F_ISSET(bset, ISL_BASIC_SET_NO_IMPLICIT)) |
||
670 | if (isl_tab_detect_implicit_equalities(tab) < 0) |
||
671 | goto error; |
||
672 | |||
673 | sample = isl_tab_sample(tab); |
||
674 | if (!sample) |
||
675 | goto error; |
||
676 | |||
677 | if (sample->size > 0) { |
||
678 | isl_vec_free(bset->sample); |
||
679 | bset->sample = isl_vec_copy(sample); |
||
680 | } |
||
681 | |||
682 | isl_basic_set_free(bset); |
||
683 | isl_tab_free(tab); |
||
684 | return sample; |
||
685 | error: |
||
686 | isl_basic_set_free(bset); |
||
687 | isl_tab_free(tab); |
||
688 | return NULL; |
||
689 | } |
||
690 | |||
691 | /* Given a basic set "bset" and a value "sample" for the first coordinates |
||
692 | * of bset, plug in these values and drop the corresponding coordinates. |
||
693 | * |
||
694 | * We do this by computing the preimage of the transformation |
||
695 | * |
||
696 | * [ 1 0 ] |
||
697 | * x = [ s 0 ] x' |
||
698 | * [ 0 I ] |
||
699 | * |
||
700 | * where [1 s] is the sample value and I is the identity matrix of the |
||
701 | * appropriate dimension. |
||
702 | */ |
||
703 | static struct isl_basic_set *plug_in(struct isl_basic_set *bset, |
||
704 | struct isl_vec *sample) |
||
705 | { |
||
706 | int i; |
||
707 | unsigned total; |
||
708 | struct isl_mat *T; |
||
709 | |||
710 | if (!bset || !sample) |
||
711 | goto error; |
||
712 | |||
713 | total = isl_basic_set_total_dim(bset); |
||
714 | T = isl_mat_alloc(bset->ctx, 1 + total, 1 + total - (sample->size - 1)); |
||
715 | if (!T) |
||
716 | goto error; |
||
717 | |||
718 | for (i = 0; i < sample->size; ++i) { |
||
719 | isl_int_set(T->row[i][0], sample->el[i]); |
||
720 | isl_seq_clr(T->row[i] + 1, T->n_col - 1); |
||
721 | } |
||
722 | for (i = 0; i < T->n_col - 1; ++i) { |
||
723 | isl_seq_clr(T->row[sample->size + i], T->n_col); |
||
724 | isl_int_set_si(T->row[sample->size + i][1 + i], 1); |
||
725 | } |
||
726 | isl_vec_free(sample); |
||
727 | |||
728 | bset = isl_basic_set_preimage(bset, T); |
||
729 | return bset; |
||
730 | error: |
||
731 | isl_basic_set_free(bset); |
||
732 | isl_vec_free(sample); |
||
733 | return NULL; |
||
734 | } |
||
735 | |||
736 | /* Given a basic set "bset", return any (possibly non-integer) point |
||
737 | * in the basic set. |
||
738 | */ |
||
739 | static struct isl_vec *rational_sample(struct isl_basic_set *bset) |
||
740 | { |
||
741 | struct isl_tab *tab; |
||
742 | struct isl_vec *sample; |
||
743 | |||
744 | if (!bset) |
||
745 | return NULL; |
||
746 | |||
747 | tab = isl_tab_from_basic_set(bset, 0); |
||
748 | sample = isl_tab_get_sample_value(tab); |
||
749 | isl_tab_free(tab); |
||
750 | |||
751 | isl_basic_set_free(bset); |
||
752 | |||
753 | return sample; |
||
754 | } |
||
755 | |||
756 | /* Given a linear cone "cone" and a rational point "vec", |
||
757 | * construct a polyhedron with shifted copies of the constraints in "cone", |
||
758 | * i.e., a polyhedron with "cone" as its recession cone, such that each |
||
759 | * point x in this polyhedron is such that the unit box positioned at x |
||
760 | * lies entirely inside the affine cone 'vec + cone'. |
||
761 | * Any rational point in this polyhedron may therefore be rounded up |
||
762 | * to yield an integer point that lies inside said affine cone. |
||
763 | * |
||
764 | * Denote the constraints of cone by "<a_i, x> >= 0" and the rational |
||
765 | * point "vec" by v/d. |
||
766 | * Let b_i = <a_i, v>. Then the affine cone 'vec + cone' is given |
||
767 | * by <a_i, x> - b/d >= 0. |
||
768 | * The polyhedron <a_i, x> - ceil{b/d} >= 0 is a subset of this affine cone. |
||
769 | * We prefer this polyhedron over the actual affine cone because it doesn't |
||
770 | * require a scaling of the constraints. |
||
771 | * If each of the vertices of the unit cube positioned at x lies inside |
||
772 | * this polyhedron, then the whole unit cube at x lies inside the affine cone. |
||
773 | * We therefore impose that x' = x + \sum e_i, for any selection of unit |
||
774 | * vectors lies inside the polyhedron, i.e., |
||
775 | * |
||
776 | * <a_i, x'> - ceil{b/d} = <a_i, x> + sum a_i - ceil{b/d} >= 0 |
||
777 | * |
||
778 | * The most stringent of these constraints is the one that selects |
||
779 | * all negative a_i, so the polyhedron we are looking for has constraints |
||
780 | * |
||
781 | * <a_i, x> + sum_{a_i < 0} a_i - ceil{b/d} >= 0 |
||
782 | * |
||
783 | * Note that if cone were known to have only non-negative rays |
||
784 | * (which can be accomplished by a unimodular transformation), |
||
785 | * then we would only have to check the points x' = x + e_i |
||
786 | * and we only have to add the smallest negative a_i (if any) |
||
787 | * instead of the sum of all negative a_i. |
||
788 | */ |
||
789 | static struct isl_basic_set *shift_cone(struct isl_basic_set *cone, |
||
790 | struct isl_vec *vec) |
||
791 | { |
||
792 | int i, j, k; |
||
793 | unsigned total; |
||
794 | |||
795 | struct isl_basic_set *shift = NULL; |
||
796 | |||
797 | if (!cone || !vec) |
||
798 | goto error; |
||
799 | |||
800 | isl_assert(cone->ctx, cone->n_eq == 0, goto error); |
||
801 | |||
802 | total = isl_basic_set_total_dim(cone); |
||
803 | |||
804 | shift = isl_basic_set_alloc_space(isl_basic_set_get_space(cone), |
||
805 | 0, 0, cone->n_ineq); |
||
806 | |||
807 | for (i = 0; i < cone->n_ineq; ++i) { |
||
808 | k = isl_basic_set_alloc_inequality(shift); |
||
809 | if (k < 0) |
||
810 | goto error; |
||
811 | isl_seq_cpy(shift->ineq[k] + 1, cone->ineq[i] + 1, total); |
||
812 | isl_seq_inner_product(shift->ineq[k] + 1, vec->el + 1, total, |
||
813 | &shift->ineq[k][0]); |
||
814 | isl_int_cdiv_q(shift->ineq[k][0], |
||
815 | shift->ineq[k][0], vec->el[0]); |
||
816 | isl_int_neg(shift->ineq[k][0], shift->ineq[k][0]); |
||
817 | for (j = 0; j < total; ++j) { |
||
818 | if (isl_int_is_nonneg(shift->ineq[k][1 + j])) |
||
819 | continue; |
||
820 | isl_int_add(shift->ineq[k][0], |
||
821 | shift->ineq[k][0], shift->ineq[k][1 + j]); |
||
822 | } |
||
823 | } |
||
824 | |||
825 | isl_basic_set_free(cone); |
||
826 | isl_vec_free(vec); |
||
827 | |||
828 | return isl_basic_set_finalize(shift); |
||
829 | error: |
||
830 | isl_basic_set_free(shift); |
||
831 | isl_basic_set_free(cone); |
||
832 | isl_vec_free(vec); |
||
833 | return NULL; |
||
834 | } |
||
835 | |||
836 | /* Given a rational point vec in a (transformed) basic set, |
||
837 | * such that cone is the recession cone of the original basic set, |
||
838 | * "round up" the rational point to an integer point. |
||
839 | * |
||
840 | * We first check if the rational point just happens to be integer. |
||
841 | * If not, we transform the cone in the same way as the basic set, |
||
842 | * pick a point x in this cone shifted to the rational point such that |
||
843 | * the whole unit cube at x is also inside this affine cone. |
||
844 | * Then we simply round up the coordinates of x and return the |
||
845 | * resulting integer point. |
||
846 | */ |
||
847 | static struct isl_vec *round_up_in_cone(struct isl_vec *vec, |
||
848 | struct isl_basic_set *cone, struct isl_mat *U) |
||
849 | { |
||
850 | unsigned total; |
||
851 | |||
852 | if (!vec || !cone || !U) |
||
853 | goto error; |
||
854 | |||
855 | isl_assert(vec->ctx, vec->size != 0, goto error); |
||
856 | if (isl_int_is_one(vec->el[0])) { |
||
857 | isl_mat_free(U); |
||
858 | isl_basic_set_free(cone); |
||
859 | return vec; |
||
860 | } |
||
861 | |||
862 | total = isl_basic_set_total_dim(cone); |
||
863 | cone = isl_basic_set_preimage(cone, U); |
||
864 | cone = isl_basic_set_remove_dims(cone, isl_dim_set, |
||
865 | 0, total - (vec->size - 1)); |
||
866 | |||
867 | cone = shift_cone(cone, vec); |
||
868 | |||
869 | vec = rational_sample(cone); |
||
870 | vec = isl_vec_ceil(vec); |
||
871 | return vec; |
||
872 | error: |
||
873 | isl_mat_free(U); |
||
874 | isl_vec_free(vec); |
||
875 | isl_basic_set_free(cone); |
||
876 | return NULL; |
||
877 | } |
||
878 | |||
879 | /* Concatenate two integer vectors, i.e., two vectors with denominator |
||
880 | * (stored in element 0) equal to 1. |
||
881 | */ |
||
882 | static struct isl_vec *vec_concat(struct isl_vec *vec1, struct isl_vec *vec2) |
||
883 | { |
||
884 | struct isl_vec *vec; |
||
885 | |||
886 | if (!vec1 || !vec2) |
||
887 | goto error; |
||
888 | isl_assert(vec1->ctx, vec1->size > 0, goto error); |
||
889 | isl_assert(vec2->ctx, vec2->size > 0, goto error); |
||
890 | isl_assert(vec1->ctx, isl_int_is_one(vec1->el[0]), goto error); |
||
891 | isl_assert(vec2->ctx, isl_int_is_one(vec2->el[0]), goto error); |
||
892 | |||
893 | vec = isl_vec_alloc(vec1->ctx, vec1->size + vec2->size - 1); |
||
894 | if (!vec) |
||
895 | goto error; |
||
896 | |||
897 | isl_seq_cpy(vec->el, vec1->el, vec1->size); |
||
898 | isl_seq_cpy(vec->el + vec1->size, vec2->el + 1, vec2->size - 1); |
||
899 | |||
900 | isl_vec_free(vec1); |
||
901 | isl_vec_free(vec2); |
||
902 | |||
903 | return vec; |
||
904 | error: |
||
905 | isl_vec_free(vec1); |
||
906 | isl_vec_free(vec2); |
||
907 | return NULL; |
||
908 | } |
||
909 | |||
910 | /* Give a basic set "bset" with recession cone "cone", compute and |
||
911 | * return an integer point in bset, if any. |
||
912 | * |
||
913 | * If the recession cone is full-dimensional, then we know that |
||
914 | * bset contains an infinite number of integer points and it is |
||
915 | * fairly easy to pick one of them. |
||
916 | * If the recession cone is not full-dimensional, then we first |
||
917 | * transform bset such that the bounded directions appear as |
||
918 | * the first dimensions of the transformed basic set. |
||
919 | * We do this by using a unimodular transformation that transforms |
||
920 | * the equalities in the recession cone to equalities on the first |
||
921 | * dimensions. |
||
922 | * |
||
923 | * The transformed set is then projected onto its bounded dimensions. |
||
924 | * Note that to compute this projection, we can simply drop all constraints |
||
925 | * involving any of the unbounded dimensions since these constraints |
||
926 | * cannot be combined to produce a constraint on the bounded dimensions. |
||
927 | * To see this, assume that there is such a combination of constraints |
||
928 | * that produces a constraint on the bounded dimensions. This means |
||
929 | * that some combination of the unbounded dimensions has both an upper |
||
930 | * bound and a lower bound in terms of the bounded dimensions, but then |
||
931 | * this combination would be a bounded direction too and would have been |
||
932 | * transformed into a bounded dimensions. |
||
933 | * |
||
934 | * We then compute a sample value in the bounded dimensions. |
||
935 | * If no such value can be found, then the original set did not contain |
||
936 | * any integer points and we are done. |
||
937 | * Otherwise, we plug in the value we found in the bounded dimensions, |
||
938 | * project out these bounded dimensions and end up with a set with |
||
939 | * a full-dimensional recession cone. |
||
940 | * A sample point in this set is computed by "rounding up" any |
||
941 | * rational point in the set. |
||
942 | * |
||
943 | * The sample points in the bounded and unbounded dimensions are |
||
944 | * then combined into a single sample point and transformed back |
||
945 | * to the original space. |
||
946 | */ |
||
947 | __isl_give isl_vec *isl_basic_set_sample_with_cone( |
||
948 | __isl_take isl_basic_set *bset, __isl_take isl_basic_set *cone) |
||
949 | { |
||
950 | unsigned total; |
||
951 | unsigned cone_dim; |
||
952 | struct isl_mat *M, *U; |
||
953 | struct isl_vec *sample; |
||
954 | struct isl_vec *cone_sample; |
||
955 | struct isl_ctx *ctx; |
||
956 | struct isl_basic_set *bounded; |
||
957 | |||
958 | if (!bset || !cone) |
||
959 | goto error; |
||
960 | |||
961 | ctx = bset->ctx; |
||
962 | total = isl_basic_set_total_dim(cone); |
||
963 | cone_dim = total - cone->n_eq; |
||
964 | |||
965 | M = isl_mat_sub_alloc6(bset->ctx, cone->eq, 0, cone->n_eq, 1, total); |
||
966 | M = isl_mat_left_hermite(M, 0, &U, NULL); |
||
967 | if (!M) |
||
968 | goto error; |
||
969 | isl_mat_free(M); |
||
970 | |||
971 | U = isl_mat_lin_to_aff(U); |
||
972 | bset = isl_basic_set_preimage(bset, isl_mat_copy(U)); |
||
973 | |||
974 | bounded = isl_basic_set_copy(bset); |
||
975 | bounded = isl_basic_set_drop_constraints_involving(bounded, |
||
976 | total - cone_dim, cone_dim); |
||
977 | bounded = isl_basic_set_drop_dims(bounded, total - cone_dim, cone_dim); |
||
978 | sample = sample_bounded(bounded); |
||
979 | if (!sample || sample->size == 0) { |
||
980 | isl_basic_set_free(bset); |
||
981 | isl_basic_set_free(cone); |
||
982 | isl_mat_free(U); |
||
983 | return sample; |
||
984 | } |
||
985 | bset = plug_in(bset, isl_vec_copy(sample)); |
||
986 | cone_sample = rational_sample(bset); |
||
987 | cone_sample = round_up_in_cone(cone_sample, cone, isl_mat_copy(U)); |
||
988 | sample = vec_concat(sample, cone_sample); |
||
989 | sample = isl_mat_vec_product(U, sample); |
||
990 | return sample; |
||
991 | error: |
||
992 | isl_basic_set_free(cone); |
||
993 | isl_basic_set_free(bset); |
||
994 | return NULL; |
||
995 | } |
||
996 | |||
997 | static void vec_sum_of_neg(struct isl_vec *v, isl_int *s) |
||
998 | { |
||
999 | int i; |
||
1000 | |||
1001 | isl_int_set_si(*s, 0); |
||
1002 | |||
1003 | for (i = 0; i < v->size; ++i) |
||
1004 | if (isl_int_is_neg(v->el[i])) |
||
1005 | isl_int_add(*s, *s, v->el[i]); |
||
1006 | } |
||
1007 | |||
1008 | /* Given a tableau "tab", a tableau "tab_cone" that corresponds |
||
1009 | * to the recession cone and the inverse of a new basis U = inv(B), |
||
1010 | * with the unbounded directions in B last, |
||
1011 | * add constraints to "tab" that ensure any rational value |
||
1012 | * in the unbounded directions can be rounded up to an integer value. |
||
1013 | * |
||
1014 | * The new basis is given by x' = B x, i.e., x = U x'. |
||
1015 | * For any rational value of the last tab->n_unbounded coordinates |
||
1016 | * in the update tableau, the value that is obtained by rounding |
||
1017 | * up this value should be contained in the original tableau. |
||
1018 | * For any constraint "a x + c >= 0", we therefore need to add |
||
1019 | * a constraint "a x + c + s >= 0", with s the sum of all negative |
||
1020 | * entries in the last elements of "a U". |
||
1021 | * |
||
1022 | * Since we are not interested in the first entries of any of the "a U", |
||
1023 | * we first drop the columns of U that correpond to bounded directions. |
||
1024 | */ |
||
1025 | static int tab_shift_cone(struct isl_tab *tab, |
||
1026 | struct isl_tab *tab_cone, struct isl_mat *U) |
||
1027 | { |
||
1028 | int i; |
||
1029 | isl_int v; |
||
1030 | struct isl_basic_set *bset = NULL; |
||
1031 | |||
1032 | if (tab && tab->n_unbounded == 0) { |
||
1033 | isl_mat_free(U); |
||
1034 | return 0; |
||
1035 | } |
||
1036 | isl_int_init(v); |
||
1037 | if (!tab || !tab_cone || !U) |
||
1038 | goto error; |
||
1039 | bset = isl_tab_peek_bset(tab_cone); |
||
1040 | U = isl_mat_drop_cols(U, 0, tab->n_var - tab->n_unbounded); |
||
1041 | for (i = 0; i < bset->n_ineq; ++i) { |
||
1042 | int ok; |
||
1043 | struct isl_vec *row = NULL; |
||
1044 | if (isl_tab_is_equality(tab_cone, tab_cone->n_eq + i)) |
||
1045 | continue; |
||
1046 | row = isl_vec_alloc(bset->ctx, tab_cone->n_var); |
||
1047 | if (!row) |
||
1048 | goto error; |
||
1049 | isl_seq_cpy(row->el, bset->ineq[i] + 1, tab_cone->n_var); |
||
1050 | row = isl_vec_mat_product(row, isl_mat_copy(U)); |
||
1051 | if (!row) |
||
1052 | goto error; |
||
1053 | vec_sum_of_neg(row, &v); |
||
1054 | isl_vec_free(row); |
||
1055 | if (isl_int_is_zero(v)) |
||
1056 | continue; |
||
1057 | tab = isl_tab_extend(tab, 1); |
||
1058 | isl_int_add(bset->ineq[i][0], bset->ineq[i][0], v); |
||
1059 | ok = isl_tab_add_ineq(tab, bset->ineq[i]) >= 0; |
||
1060 | isl_int_sub(bset->ineq[i][0], bset->ineq[i][0], v); |
||
1061 | if (!ok) |
||
1062 | goto error; |
||
1063 | } |
||
1064 | |||
1065 | isl_mat_free(U); |
||
1066 | isl_int_clear(v); |
||
1067 | return 0; |
||
1068 | error: |
||
1069 | isl_mat_free(U); |
||
1070 | isl_int_clear(v); |
||
1071 | return -1; |
||
1072 | } |
||
1073 | |||
1074 | /* Compute and return an initial basis for the possibly |
||
1075 | * unbounded tableau "tab". "tab_cone" is a tableau |
||
1076 | * for the corresponding recession cone. |
||
1077 | * Additionally, add constraints to "tab" that ensure |
||
1078 | * that any rational value for the unbounded directions |
||
1079 | * can be rounded up to an integer value. |
||
1080 | * |
||
1081 | * If the tableau is bounded, i.e., if the recession cone |
||
1082 | * is zero-dimensional, then we just use inital_basis. |
||
1083 | * Otherwise, we construct a basis whose first directions |
||
1084 | * correspond to equalities, followed by bounded directions, |
||
1085 | * i.e., equalities in the recession cone. |
||
1086 | * The remaining directions are then unbounded. |
||
1087 | */ |
||
1088 | int isl_tab_set_initial_basis_with_cone(struct isl_tab *tab, |
||
1089 | struct isl_tab *tab_cone) |
||
1090 | { |
||
1091 | struct isl_mat *eq; |
||
1092 | struct isl_mat *cone_eq; |
||
1093 | struct isl_mat *U, *Q; |
||
1094 | |||
1095 | if (!tab || !tab_cone) |
||
1096 | return -1; |
||
1097 | |||
1098 | if (tab_cone->n_col == tab_cone->n_dead) { |
||
1099 | tab->basis = initial_basis(tab); |
||
1100 | return tab->basis ? 0 : -1; |
||
1101 | } |
||
1102 | |||
1103 | eq = tab_equalities(tab); |
||
1104 | if (!eq) |
||
1105 | return -1; |
||
1106 | tab->n_zero = eq->n_row; |
||
1107 | cone_eq = tab_equalities(tab_cone); |
||
1108 | eq = isl_mat_concat(eq, cone_eq); |
||
1109 | if (!eq) |
||
1110 | return -1; |
||
1111 | tab->n_unbounded = tab->n_var - (eq->n_row - tab->n_zero); |
||
1112 | eq = isl_mat_left_hermite(eq, 0, &U, &Q); |
||
1113 | if (!eq) |
||
1114 | return -1; |
||
1115 | isl_mat_free(eq); |
||
1116 | tab->basis = isl_mat_lin_to_aff(Q); |
||
1117 | if (tab_shift_cone(tab, tab_cone, U) < 0) |
||
1118 | return -1; |
||
1119 | if (!tab->basis) |
||
1120 | return -1; |
||
1121 | return 0; |
||
1122 | } |
||
1123 | |||
1124 | /* Compute and return a sample point in bset using generalized basis |
||
1125 | * reduction. We first check if the input set has a non-trivial |
||
1126 | * recession cone. If so, we perform some extra preprocessing in |
||
1127 | * sample_with_cone. Otherwise, we directly perform generalized basis |
||
1128 | * reduction. |
||
1129 | */ |
||
1130 | static struct isl_vec *gbr_sample(struct isl_basic_set *bset) |
||
1131 | { |
||
1132 | unsigned dim; |
||
1133 | struct isl_basic_set *cone; |
||
1134 | |||
1135 | dim = isl_basic_set_total_dim(bset); |
||
1136 | |||
1137 | cone = isl_basic_set_recession_cone(isl_basic_set_copy(bset)); |
||
1138 | if (!cone) |
||
1139 | goto error; |
||
1140 | |||
1141 | if (cone->n_eq < dim) |
||
1142 | return isl_basic_set_sample_with_cone(bset, cone); |
||
1143 | |||
1144 | isl_basic_set_free(cone); |
||
1145 | return sample_bounded(bset); |
||
1146 | error: |
||
1147 | isl_basic_set_free(bset); |
||
1148 | return NULL; |
||
1149 | } |
||
1150 | |||
1151 | static struct isl_vec *pip_sample(struct isl_basic_set *bset) |
||
1152 | { |
||
1153 | struct isl_mat *T; |
||
1154 | struct isl_ctx *ctx; |
||
1155 | struct isl_vec *sample; |
||
1156 | |||
1157 | bset = isl_basic_set_skew_to_positive_orthant(bset, &T); |
||
1158 | if (!bset) |
||
1159 | return NULL; |
||
1160 | |||
1161 | ctx = bset->ctx; |
||
1162 | sample = isl_pip_basic_set_sample(bset); |
||
1163 | |||
1164 | if (sample && sample->size != 0) |
||
1165 | sample = isl_mat_vec_product(T, sample); |
||
1166 | else |
||
1167 | isl_mat_free(T); |
||
1168 | |||
1169 | return sample; |
||
1170 | } |
||
1171 | |||
1172 | static struct isl_vec *basic_set_sample(struct isl_basic_set *bset, int bounded) |
||
1173 | { |
||
1174 | struct isl_ctx *ctx; |
||
1175 | unsigned dim; |
||
1176 | if (!bset) |
||
1177 | return NULL; |
||
1178 | |||
1179 | ctx = bset->ctx; |
||
1180 | if (isl_basic_set_plain_is_empty(bset)) |
||
1181 | return empty_sample(bset); |
||
1182 | |||
1183 | dim = isl_basic_set_n_dim(bset); |
||
1184 | isl_assert(ctx, isl_basic_set_n_param(bset) == 0, goto error); |
||
1185 | isl_assert(ctx, bset->n_div == 0, goto error); |
||
1186 | |||
1187 | if (bset->sample && bset->sample->size == 1 + dim) { |
||
1188 | int contains = isl_basic_set_contains(bset, bset->sample); |
||
1189 | if (contains < 0) |
||
1190 | goto error; |
||
1191 | if (contains) { |
||
1192 | struct isl_vec *sample = isl_vec_copy(bset->sample); |
||
1193 | isl_basic_set_free(bset); |
||
1194 | return sample; |
||
1195 | } |
||
1196 | } |
||
1197 | isl_vec_free(bset->sample); |
||
1198 | bset->sample = NULL; |
||
1199 | |||
1200 | if (bset->n_eq > 0) |
||
1201 | return sample_eq(bset, bounded ? isl_basic_set_sample_bounded |
||
1202 | : isl_basic_set_sample_vec); |
||
1203 | if (dim == 0) |
||
1204 | return zero_sample(bset); |
||
1205 | if (dim == 1) |
||
1206 | return interval_sample(bset); |
||
1207 | |||
1208 | switch (bset->ctx->opt->ilp_solver) { |
||
1209 | case ISL_ILP_PIP: |
||
1210 | return pip_sample(bset); |
||
1211 | case ISL_ILP_GBR: |
||
1212 | return bounded ? sample_bounded(bset) : gbr_sample(bset); |
||
1213 | } |
||
1214 | isl_assert(bset->ctx, 0, ); |
||
1215 | error: |
||
1216 | isl_basic_set_free(bset); |
||
1217 | return NULL; |
||
1218 | } |
||
1219 | |||
1220 | __isl_give isl_vec *isl_basic_set_sample_vec(__isl_take isl_basic_set *bset) |
||
1221 | { |
||
1222 | return basic_set_sample(bset, 0); |
||
1223 | } |
||
1224 | |||
1225 | /* Compute an integer sample in "bset", where the caller guarantees |
||
1226 | * that "bset" is bounded. |
||
1227 | */ |
||
1228 | struct isl_vec *isl_basic_set_sample_bounded(struct isl_basic_set *bset) |
||
1229 | { |
||
1230 | return basic_set_sample(bset, 1); |
||
1231 | } |
||
1232 | |||
1233 | __isl_give isl_basic_set *isl_basic_set_from_vec(__isl_take isl_vec *vec) |
||
1234 | { |
||
1235 | int i; |
||
1236 | int k; |
||
1237 | struct isl_basic_set *bset = NULL; |
||
1238 | struct isl_ctx *ctx; |
||
1239 | unsigned dim; |
||
1240 | |||
1241 | if (!vec) |
||
1242 | return NULL; |
||
1243 | ctx = vec->ctx; |
||
1244 | isl_assert(ctx, vec->size != 0, goto error); |
||
1245 | |||
1246 | bset = isl_basic_set_alloc(ctx, 0, vec->size - 1, 0, vec->size - 1, 0); |
||
1247 | if (!bset) |
||
1248 | goto error; |
||
1249 | dim = isl_basic_set_n_dim(bset); |
||
1250 | for (i = dim - 1; i >= 0; --i) { |
||
1251 | k = isl_basic_set_alloc_equality(bset); |
||
1252 | if (k < 0) |
||
1253 | goto error; |
||
1254 | isl_seq_clr(bset->eq[k], 1 + dim); |
||
1255 | isl_int_neg(bset->eq[k][0], vec->el[1 + i]); |
||
1256 | isl_int_set(bset->eq[k][1 + i], vec->el[0]); |
||
1257 | } |
||
1258 | bset->sample = vec; |
||
1259 | |||
1260 | return bset; |
||
1261 | error: |
||
1262 | isl_basic_set_free(bset); |
||
1263 | isl_vec_free(vec); |
||
1264 | return NULL; |
||
1265 | } |
||
1266 | |||
1267 | __isl_give isl_basic_map *isl_basic_map_sample(__isl_take isl_basic_map *bmap) |
||
1268 | { |
||
1269 | struct isl_basic_set *bset; |
||
1270 | struct isl_vec *sample_vec; |
||
1271 | |||
1272 | bset = isl_basic_map_underlying_set(isl_basic_map_copy(bmap)); |
||
1273 | sample_vec = isl_basic_set_sample_vec(bset); |
||
1274 | if (!sample_vec) |
||
1275 | goto error; |
||
1276 | if (sample_vec->size == 0) { |
||
1277 | struct isl_basic_map *sample; |
||
1278 | sample = isl_basic_map_empty_like(bmap); |
||
1279 | isl_vec_free(sample_vec); |
||
1280 | isl_basic_map_free(bmap); |
||
1281 | return sample; |
||
1282 | } |
||
1283 | bset = isl_basic_set_from_vec(sample_vec); |
||
1284 | return isl_basic_map_overlying_set(bset, bmap); |
||
1285 | error: |
||
1286 | isl_basic_map_free(bmap); |
||
1287 | return NULL; |
||
1288 | } |
||
1289 | |||
1290 | __isl_give isl_basic_set *isl_basic_set_sample(__isl_take isl_basic_set *bset) |
||
1291 | { |
||
1292 | return isl_basic_map_sample(bset); |
||
1293 | } |
||
1294 | |||
1295 | __isl_give isl_basic_map *isl_map_sample(__isl_take isl_map *map) |
||
1296 | { |
||
1297 | int i; |
||
1298 | isl_basic_map *sample = NULL; |
||
1299 | |||
1300 | if (!map) |
||
1301 | goto error; |
||
1302 | |||
1303 | for (i = 0; i < map->n; ++i) { |
||
1304 | sample = isl_basic_map_sample(isl_basic_map_copy(map->p[i])); |
||
1305 | if (!sample) |
||
1306 | goto error; |
||
1307 | if (!ISL_F_ISSET(sample, ISL_BASIC_MAP_EMPTY)) |
||
1308 | break; |
||
1309 | isl_basic_map_free(sample); |
||
1310 | } |
||
1311 | if (i == map->n) |
||
1312 | sample = isl_basic_map_empty_like_map(map); |
||
1313 | isl_map_free(map); |
||
1314 | return sample; |
||
1315 | error: |
||
1316 | isl_map_free(map); |
||
1317 | return NULL; |
||
1318 | } |
||
1319 | |||
1320 | __isl_give isl_basic_set *isl_set_sample(__isl_take isl_set *set) |
||
1321 | { |
||
1322 | return (isl_basic_set *) isl_map_sample((isl_map *)set); |
||
1323 | } |
||
1324 | |||
1325 | __isl_give isl_point *isl_basic_set_sample_point(__isl_take isl_basic_set *bset) |
||
1326 | { |
||
1327 | isl_vec *vec; |
||
1328 | isl_space *dim; |
||
1329 | |||
1330 | dim = isl_basic_set_get_space(bset); |
||
1331 | bset = isl_basic_set_underlying_set(bset); |
||
1332 | vec = isl_basic_set_sample_vec(bset); |
||
1333 | |||
1334 | return isl_point_alloc(dim, vec); |
||
1335 | } |
||
1336 | |||
1337 | __isl_give isl_point *isl_set_sample_point(__isl_take isl_set *set) |
||
1338 | { |
||
1339 | int i; |
||
1340 | isl_point *pnt; |
||
1341 | |||
1342 | if (!set) |
||
1343 | return NULL; |
||
1344 | |||
1345 | for (i = 0; i < set->n; ++i) { |
||
1346 | pnt = isl_basic_set_sample_point(isl_basic_set_copy(set->p[i])); |
||
1347 | if (!pnt) |
||
1348 | goto error; |
||
1349 | if (!isl_point_is_void(pnt)) |
||
1350 | break; |
||
1351 | isl_point_free(pnt); |
||
1352 | } |
||
1353 | if (i == set->n) |
||
1354 | pnt = isl_point_void(isl_set_get_space(set)); |
||
1355 | |||
1356 | isl_set_free(set); |
||
1357 | return pnt; |
||
1358 | error: |
||
1359 | isl_set_free(set); |
||
1360 | return NULL; |
||
1361 | } |