Line data Source code
1 : /*
2 : * Copyright 2008-2009 Katholieke Universiteit Leuven
3 : *
4 : * Use of this software is governed by the MIT 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/ilp.h>
13 : #include <isl/union_set.h>
14 : #include "isl_sample.h"
15 : #include <isl_seq.h>
16 : #include "isl_equalities.h"
17 : #include <isl_aff_private.h>
18 : #include <isl_local_space_private.h>
19 : #include <isl_mat_private.h>
20 : #include <isl_val_private.h>
21 : #include <isl_vec_private.h>
22 : #include <isl_lp_private.h>
23 : #include <isl_ilp_private.h>
24 :
25 : /* Given a basic set "bset", construct a basic set U such that for
26 : * each element x in U, the whole unit box positioned at x is inside
27 : * the given basic set.
28 : * Note that U may not contain all points that satisfy this property.
29 : *
30 : * We simply add the sum of all negative coefficients to the constant
31 : * term. This ensures that if x satisfies the resulting constraints,
32 : * then x plus any sum of unit vectors satisfies the original constraints.
33 : */
34 0 : static __isl_give isl_basic_set *unit_box_base_points(
35 : __isl_take isl_basic_set *bset)
36 : {
37 : int i, j, k;
38 0 : struct isl_basic_set *unit_box = NULL;
39 : unsigned total;
40 :
41 0 : if (!bset)
42 0 : goto error;
43 :
44 0 : if (bset->n_eq != 0) {
45 0 : isl_space *space = isl_basic_set_get_space(bset);
46 0 : isl_basic_set_free(bset);
47 0 : return isl_basic_set_empty(space);
48 : }
49 :
50 0 : total = isl_basic_set_total_dim(bset);
51 0 : unit_box = isl_basic_set_alloc_space(isl_basic_set_get_space(bset),
52 : 0, 0, bset->n_ineq);
53 :
54 0 : for (i = 0; i < bset->n_ineq; ++i) {
55 0 : k = isl_basic_set_alloc_inequality(unit_box);
56 0 : if (k < 0)
57 0 : goto error;
58 0 : isl_seq_cpy(unit_box->ineq[k], bset->ineq[i], 1 + total);
59 0 : for (j = 0; j < total; ++j) {
60 0 : if (isl_int_is_nonneg(unit_box->ineq[k][1 + j]))
61 0 : continue;
62 0 : isl_int_add(unit_box->ineq[k][0],
63 : unit_box->ineq[k][0], unit_box->ineq[k][1 + j]);
64 : }
65 : }
66 :
67 0 : isl_basic_set_free(bset);
68 0 : return unit_box;
69 : error:
70 0 : isl_basic_set_free(bset);
71 0 : isl_basic_set_free(unit_box);
72 0 : return NULL;
73 : }
74 :
75 : /* Find an integer point in "bset", preferably one that is
76 : * close to minimizing "f".
77 : *
78 : * We first check if we can easily put unit boxes inside bset.
79 : * If so, we take the best base point of any of the unit boxes we can find
80 : * and round it up to the nearest integer.
81 : * If not, we simply pick any integer point in "bset".
82 : */
83 0 : static __isl_give isl_vec *initial_solution(__isl_keep isl_basic_set *bset,
84 : isl_int *f)
85 : {
86 : enum isl_lp_result res;
87 : struct isl_basic_set *unit_box;
88 : struct isl_vec *sol;
89 :
90 0 : unit_box = unit_box_base_points(isl_basic_set_copy(bset));
91 :
92 0 : res = isl_basic_set_solve_lp(unit_box, 0, f, bset->ctx->one,
93 : NULL, NULL, &sol);
94 0 : if (res == isl_lp_ok) {
95 0 : isl_basic_set_free(unit_box);
96 0 : return isl_vec_ceil(sol);
97 : }
98 :
99 0 : isl_basic_set_free(unit_box);
100 :
101 0 : return isl_basic_set_sample_vec(isl_basic_set_copy(bset));
102 : }
103 :
104 : /* Restrict "bset" to those points with values for f in the interval [l, u].
105 : */
106 0 : static __isl_give isl_basic_set *add_bounds(__isl_take isl_basic_set *bset,
107 : isl_int *f, isl_int l, isl_int u)
108 : {
109 : int k;
110 : unsigned total;
111 :
112 0 : total = isl_basic_set_total_dim(bset);
113 0 : bset = isl_basic_set_extend_constraints(bset, 0, 2);
114 :
115 0 : k = isl_basic_set_alloc_inequality(bset);
116 0 : if (k < 0)
117 0 : goto error;
118 0 : isl_seq_cpy(bset->ineq[k], f, 1 + total);
119 0 : isl_int_sub(bset->ineq[k][0], bset->ineq[k][0], l);
120 :
121 0 : k = isl_basic_set_alloc_inequality(bset);
122 0 : if (k < 0)
123 0 : goto error;
124 0 : isl_seq_neg(bset->ineq[k], f, 1 + total);
125 0 : isl_int_add(bset->ineq[k][0], bset->ineq[k][0], u);
126 :
127 0 : return bset;
128 : error:
129 0 : isl_basic_set_free(bset);
130 0 : return NULL;
131 : }
132 :
133 : /* Find an integer point in "bset" that minimizes f (in any) such that
134 : * the value of f lies inside the interval [l, u].
135 : * Return this integer point if it can be found.
136 : * Otherwise, return sol.
137 : *
138 : * We perform a number of steps until l > u.
139 : * In each step, we look for an integer point with value in either
140 : * the whole interval [l, u] or half of the interval [l, l+floor(u-l-1/2)].
141 : * The choice depends on whether we have found an integer point in the
142 : * previous step. If so, we look for the next point in half of the remaining
143 : * interval.
144 : * If we find a point, the current solution is updated and u is set
145 : * to its value minus 1.
146 : * If no point can be found, we update l to the upper bound of the interval
147 : * we checked (u or l+floor(u-l-1/2)) plus 1.
148 : */
149 0 : static __isl_give isl_vec *solve_ilp_search(__isl_keep isl_basic_set *bset,
150 : isl_int *f, isl_int *opt, __isl_take isl_vec *sol, isl_int l, isl_int u)
151 : {
152 : isl_int tmp;
153 0 : int divide = 1;
154 :
155 0 : isl_int_init(tmp);
156 :
157 0 : while (isl_int_le(l, u)) {
158 : struct isl_basic_set *slice;
159 : struct isl_vec *sample;
160 :
161 0 : if (!divide)
162 0 : isl_int_set(tmp, u);
163 : else {
164 0 : isl_int_sub(tmp, u, l);
165 0 : isl_int_fdiv_q_ui(tmp, tmp, 2);
166 0 : isl_int_add(tmp, tmp, l);
167 : }
168 0 : slice = add_bounds(isl_basic_set_copy(bset), f, l, tmp);
169 0 : sample = isl_basic_set_sample_vec(slice);
170 0 : if (!sample) {
171 0 : isl_vec_free(sol);
172 0 : sol = NULL;
173 0 : break;
174 : }
175 0 : if (sample->size > 0) {
176 0 : isl_vec_free(sol);
177 0 : sol = sample;
178 0 : isl_seq_inner_product(f, sol->el, sol->size, opt);
179 0 : isl_int_sub_ui(u, *opt, 1);
180 0 : divide = 1;
181 : } else {
182 0 : isl_vec_free(sample);
183 0 : if (!divide)
184 0 : break;
185 0 : isl_int_add_ui(l, tmp, 1);
186 0 : divide = 0;
187 : }
188 : }
189 :
190 0 : isl_int_clear(tmp);
191 :
192 0 : return sol;
193 : }
194 :
195 : /* Find an integer point in "bset" that minimizes f (if any).
196 : * If sol_p is not NULL then the integer point is returned in *sol_p.
197 : * The optimal value of f is returned in *opt.
198 : *
199 : * The algorithm maintains a currently best solution and an interval [l, u]
200 : * of values of f for which integer solutions could potentially still be found.
201 : * The initial value of the best solution so far is any solution.
202 : * The initial value of l is minimal value of f over the rationals
203 : * (rounded up to the nearest integer).
204 : * The initial value of u is the value of f at the initial solution minus 1.
205 : *
206 : * We then call solve_ilp_search to perform a binary search on the interval.
207 : */
208 0 : static enum isl_lp_result solve_ilp(__isl_keep isl_basic_set *bset,
209 : isl_int *f, isl_int *opt, __isl_give isl_vec **sol_p)
210 : {
211 : enum isl_lp_result res;
212 : isl_int l, u;
213 : struct isl_vec *sol;
214 :
215 0 : res = isl_basic_set_solve_lp(bset, 0, f, bset->ctx->one,
216 : opt, NULL, &sol);
217 0 : if (res == isl_lp_ok && isl_int_is_one(sol->el[0])) {
218 0 : if (sol_p)
219 0 : *sol_p = sol;
220 : else
221 0 : isl_vec_free(sol);
222 0 : return isl_lp_ok;
223 : }
224 0 : isl_vec_free(sol);
225 0 : if (res == isl_lp_error || res == isl_lp_empty)
226 0 : return res;
227 :
228 0 : sol = initial_solution(bset, f);
229 0 : if (!sol)
230 0 : return isl_lp_error;
231 0 : if (sol->size == 0) {
232 0 : isl_vec_free(sol);
233 0 : return isl_lp_empty;
234 : }
235 0 : if (res == isl_lp_unbounded) {
236 0 : isl_vec_free(sol);
237 0 : return isl_lp_unbounded;
238 : }
239 :
240 0 : isl_int_init(l);
241 0 : isl_int_init(u);
242 :
243 0 : isl_int_set(l, *opt);
244 :
245 0 : isl_seq_inner_product(f, sol->el, sol->size, opt);
246 0 : isl_int_sub_ui(u, *opt, 1);
247 :
248 0 : sol = solve_ilp_search(bset, f, opt, sol, l, u);
249 0 : if (!sol)
250 0 : res = isl_lp_error;
251 :
252 0 : isl_int_clear(l);
253 0 : isl_int_clear(u);
254 :
255 0 : if (sol_p)
256 0 : *sol_p = sol;
257 : else
258 0 : isl_vec_free(sol);
259 :
260 0 : return res;
261 : }
262 :
263 0 : static enum isl_lp_result solve_ilp_with_eq(__isl_keep isl_basic_set *bset,
264 : int max, isl_int *f, isl_int *opt, __isl_give isl_vec **sol_p)
265 : {
266 : unsigned dim;
267 : enum isl_lp_result res;
268 0 : struct isl_mat *T = NULL;
269 : struct isl_vec *v;
270 :
271 0 : bset = isl_basic_set_copy(bset);
272 0 : dim = isl_basic_set_total_dim(bset);
273 0 : v = isl_vec_alloc(bset->ctx, 1 + dim);
274 0 : if (!v)
275 0 : goto error;
276 0 : isl_seq_cpy(v->el, f, 1 + dim);
277 0 : bset = isl_basic_set_remove_equalities(bset, &T, NULL);
278 0 : v = isl_vec_mat_product(v, isl_mat_copy(T));
279 0 : if (!v)
280 0 : goto error;
281 0 : res = isl_basic_set_solve_ilp(bset, max, v->el, opt, sol_p);
282 0 : isl_vec_free(v);
283 0 : if (res == isl_lp_ok && sol_p) {
284 0 : *sol_p = isl_mat_vec_product(T, *sol_p);
285 0 : if (!*sol_p)
286 0 : res = isl_lp_error;
287 : } else
288 0 : isl_mat_free(T);
289 0 : isl_basic_set_free(bset);
290 0 : return res;
291 : error:
292 0 : isl_mat_free(T);
293 0 : isl_basic_set_free(bset);
294 0 : return isl_lp_error;
295 : }
296 :
297 : /* Find an integer point in "bset" that minimizes (or maximizes if max is set)
298 : * f (if any).
299 : * If sol_p is not NULL then the integer point is returned in *sol_p.
300 : * The optimal value of f is returned in *opt.
301 : *
302 : * If there is any equality among the points in "bset", then we first
303 : * project it out. Otherwise, we continue with solve_ilp above.
304 : */
305 0 : enum isl_lp_result isl_basic_set_solve_ilp(__isl_keep isl_basic_set *bset,
306 : int max, isl_int *f, isl_int *opt, __isl_give isl_vec **sol_p)
307 : {
308 : unsigned dim;
309 : enum isl_lp_result res;
310 :
311 0 : if (!bset)
312 0 : return isl_lp_error;
313 0 : if (sol_p)
314 0 : *sol_p = NULL;
315 :
316 0 : isl_assert(bset->ctx, isl_basic_set_n_param(bset) == 0,
317 : return isl_lp_error);
318 :
319 0 : if (isl_basic_set_plain_is_empty(bset))
320 0 : return isl_lp_empty;
321 :
322 0 : if (bset->n_eq)
323 0 : return solve_ilp_with_eq(bset, max, f, opt, sol_p);
324 :
325 0 : dim = isl_basic_set_total_dim(bset);
326 :
327 0 : if (max)
328 0 : isl_seq_neg(f, f, 1 + dim);
329 :
330 0 : res = solve_ilp(bset, f, opt, sol_p);
331 :
332 0 : if (max) {
333 0 : isl_seq_neg(f, f, 1 + dim);
334 0 : isl_int_neg(*opt, *opt);
335 : }
336 :
337 0 : return res;
338 : }
339 :
340 0 : static enum isl_lp_result basic_set_opt(__isl_keep isl_basic_set *bset, int max,
341 : __isl_keep isl_aff *obj, isl_int *opt)
342 : {
343 : enum isl_lp_result res;
344 :
345 0 : if (!obj)
346 0 : return isl_lp_error;
347 0 : bset = isl_basic_set_copy(bset);
348 0 : bset = isl_basic_set_underlying_set(bset);
349 0 : res = isl_basic_set_solve_ilp(bset, max, obj->v->el + 1, opt, NULL);
350 0 : isl_basic_set_free(bset);
351 0 : return res;
352 : }
353 :
354 0 : static __isl_give isl_mat *extract_divs(__isl_keep isl_basic_set *bset)
355 : {
356 : int i;
357 0 : isl_ctx *ctx = isl_basic_set_get_ctx(bset);
358 : isl_mat *div;
359 :
360 0 : div = isl_mat_alloc(ctx, bset->n_div,
361 0 : 1 + 1 + isl_basic_set_total_dim(bset));
362 0 : if (!div)
363 0 : return NULL;
364 :
365 0 : for (i = 0; i < bset->n_div; ++i)
366 0 : isl_seq_cpy(div->row[i], bset->div[i], div->n_col);
367 :
368 0 : return div;
369 : }
370 :
371 0 : enum isl_lp_result isl_basic_set_opt(__isl_keep isl_basic_set *bset, int max,
372 : __isl_keep isl_aff *obj, isl_int *opt)
373 : {
374 0 : int *exp1 = NULL;
375 0 : int *exp2 = NULL;
376 : isl_ctx *ctx;
377 0 : isl_mat *bset_div = NULL;
378 0 : isl_mat *div = NULL;
379 : enum isl_lp_result res;
380 : int bset_n_div, obj_n_div;
381 :
382 0 : if (!bset || !obj)
383 0 : return isl_lp_error;
384 :
385 0 : ctx = isl_aff_get_ctx(obj);
386 0 : if (!isl_space_is_equal(bset->dim, obj->ls->dim))
387 0 : isl_die(ctx, isl_error_invalid,
388 : "spaces don't match", return isl_lp_error);
389 0 : if (!isl_int_is_one(obj->v->el[0]))
390 0 : isl_die(ctx, isl_error_unsupported,
391 : "expecting integer affine expression",
392 : return isl_lp_error);
393 :
394 0 : bset_n_div = isl_basic_set_dim(bset, isl_dim_div);
395 0 : obj_n_div = isl_aff_dim(obj, isl_dim_div);
396 0 : if (bset_n_div == 0 && obj_n_div == 0)
397 0 : return basic_set_opt(bset, max, obj, opt);
398 :
399 0 : bset = isl_basic_set_copy(bset);
400 0 : obj = isl_aff_copy(obj);
401 :
402 0 : bset_div = extract_divs(bset);
403 0 : exp1 = isl_alloc_array(ctx, int, bset_n_div);
404 0 : exp2 = isl_alloc_array(ctx, int, obj_n_div);
405 0 : if (!bset_div || (bset_n_div && !exp1) || (obj_n_div && !exp2))
406 : goto error;
407 :
408 0 : div = isl_merge_divs(bset_div, obj->ls->div, exp1, exp2);
409 :
410 0 : bset = isl_basic_set_expand_divs(bset, isl_mat_copy(div), exp1);
411 0 : obj = isl_aff_expand_divs(obj, isl_mat_copy(div), exp2);
412 :
413 0 : res = basic_set_opt(bset, max, obj, opt);
414 :
415 0 : isl_mat_free(bset_div);
416 0 : isl_mat_free(div);
417 0 : free(exp1);
418 0 : free(exp2);
419 0 : isl_basic_set_free(bset);
420 0 : isl_aff_free(obj);
421 :
422 0 : return res;
423 : error:
424 0 : isl_mat_free(div);
425 0 : isl_mat_free(bset_div);
426 0 : free(exp1);
427 0 : free(exp2);
428 0 : isl_basic_set_free(bset);
429 0 : isl_aff_free(obj);
430 0 : return isl_lp_error;
431 : }
432 :
433 : /* Compute the minimum (maximum if max is set) of the integer affine
434 : * expression obj over the points in set and put the result in *opt.
435 : *
436 : * The parameters are assumed to have been aligned.
437 : */
438 0 : static enum isl_lp_result isl_set_opt_aligned(__isl_keep isl_set *set, int max,
439 : __isl_keep isl_aff *obj, isl_int *opt)
440 : {
441 : int i;
442 : enum isl_lp_result res;
443 0 : int empty = 1;
444 : isl_int opt_i;
445 :
446 0 : if (!set || !obj)
447 0 : return isl_lp_error;
448 0 : if (set->n == 0)
449 0 : return isl_lp_empty;
450 :
451 0 : res = isl_basic_set_opt(set->p[0], max, obj, opt);
452 0 : if (res == isl_lp_error || res == isl_lp_unbounded)
453 0 : return res;
454 0 : if (set->n == 1)
455 0 : return res;
456 0 : if (res == isl_lp_ok)
457 0 : empty = 0;
458 :
459 0 : isl_int_init(opt_i);
460 0 : for (i = 1; i < set->n; ++i) {
461 0 : res = isl_basic_set_opt(set->p[i], max, obj, &opt_i);
462 0 : if (res == isl_lp_error || res == isl_lp_unbounded) {
463 0 : isl_int_clear(opt_i);
464 0 : return res;
465 : }
466 0 : if (res == isl_lp_empty)
467 0 : continue;
468 0 : empty = 0;
469 0 : if (max ? isl_int_gt(opt_i, *opt) : isl_int_lt(opt_i, *opt))
470 0 : isl_int_set(*opt, opt_i);
471 : }
472 0 : isl_int_clear(opt_i);
473 :
474 0 : return empty ? isl_lp_empty : isl_lp_ok;
475 : }
476 :
477 : /* Compute the minimum (maximum if max is set) of the integer affine
478 : * expression obj over the points in set and put the result in *opt.
479 : */
480 0 : enum isl_lp_result isl_set_opt(__isl_keep isl_set *set, int max,
481 : __isl_keep isl_aff *obj, isl_int *opt)
482 : {
483 : enum isl_lp_result res;
484 : isl_bool aligned;
485 :
486 0 : if (!set || !obj)
487 0 : return isl_lp_error;
488 :
489 0 : aligned = isl_set_space_has_equal_params(set, obj->ls->dim);
490 0 : if (aligned < 0)
491 0 : return isl_lp_error;
492 0 : if (aligned)
493 0 : return isl_set_opt_aligned(set, max, obj, opt);
494 :
495 0 : set = isl_set_copy(set);
496 0 : obj = isl_aff_copy(obj);
497 0 : set = isl_set_align_params(set, isl_aff_get_domain_space(obj));
498 0 : obj = isl_aff_align_params(obj, isl_set_get_space(set));
499 :
500 0 : res = isl_set_opt_aligned(set, max, obj, opt);
501 :
502 0 : isl_set_free(set);
503 0 : isl_aff_free(obj);
504 :
505 0 : return res;
506 : }
507 :
508 : /* Convert the result of a function that returns an isl_lp_result
509 : * to an isl_val. The numerator of "v" is set to the optimal value
510 : * if lp_res is isl_lp_ok. "max" is set if a maximum was computed.
511 : *
512 : * Return "v" with denominator set to 1 if lp_res is isl_lp_ok.
513 : * Return NULL on error.
514 : * Return a NaN if lp_res is isl_lp_empty.
515 : * Return infinity or negative infinity if lp_res is isl_lp_unbounded,
516 : * depending on "max".
517 : */
518 0 : static __isl_give isl_val *convert_lp_result(enum isl_lp_result lp_res,
519 : __isl_take isl_val *v, int max)
520 : {
521 : isl_ctx *ctx;
522 :
523 0 : if (lp_res == isl_lp_ok) {
524 0 : isl_int_set_si(v->d, 1);
525 0 : return isl_val_normalize(v);
526 : }
527 0 : ctx = isl_val_get_ctx(v);
528 0 : isl_val_free(v);
529 0 : if (lp_res == isl_lp_error)
530 0 : return NULL;
531 0 : if (lp_res == isl_lp_empty)
532 0 : return isl_val_nan(ctx);
533 0 : if (max)
534 0 : return isl_val_infty(ctx);
535 : else
536 0 : return isl_val_neginfty(ctx);
537 : }
538 :
539 : /* Return the minimum (maximum if max is set) of the integer affine
540 : * expression "obj" over the points in "bset".
541 : *
542 : * Return infinity or negative infinity if the optimal value is unbounded and
543 : * NaN if "bset" is empty.
544 : *
545 : * Call isl_basic_set_opt and translate the results.
546 : */
547 0 : __isl_give isl_val *isl_basic_set_opt_val(__isl_keep isl_basic_set *bset,
548 : int max, __isl_keep isl_aff *obj)
549 : {
550 : isl_ctx *ctx;
551 : isl_val *res;
552 : enum isl_lp_result lp_res;
553 :
554 0 : if (!bset || !obj)
555 0 : return NULL;
556 :
557 0 : ctx = isl_aff_get_ctx(obj);
558 0 : res = isl_val_alloc(ctx);
559 0 : if (!res)
560 0 : return NULL;
561 0 : lp_res = isl_basic_set_opt(bset, max, obj, &res->n);
562 0 : return convert_lp_result(lp_res, res, max);
563 : }
564 :
565 : /* Return the maximum of the integer affine
566 : * expression "obj" over the points in "bset".
567 : *
568 : * Return infinity or negative infinity if the optimal value is unbounded and
569 : * NaN if "bset" is empty.
570 : */
571 0 : __isl_give isl_val *isl_basic_set_max_val(__isl_keep isl_basic_set *bset,
572 : __isl_keep isl_aff *obj)
573 : {
574 0 : return isl_basic_set_opt_val(bset, 1, obj);
575 : }
576 :
577 : /* Return the minimum (maximum if max is set) of the integer affine
578 : * expression "obj" over the points in "set".
579 : *
580 : * Return infinity or negative infinity if the optimal value is unbounded and
581 : * NaN if "set" is empty.
582 : *
583 : * Call isl_set_opt and translate the results.
584 : */
585 0 : __isl_give isl_val *isl_set_opt_val(__isl_keep isl_set *set, int max,
586 : __isl_keep isl_aff *obj)
587 : {
588 : isl_ctx *ctx;
589 : isl_val *res;
590 : enum isl_lp_result lp_res;
591 :
592 0 : if (!set || !obj)
593 0 : return NULL;
594 :
595 0 : ctx = isl_aff_get_ctx(obj);
596 0 : res = isl_val_alloc(ctx);
597 0 : if (!res)
598 0 : return NULL;
599 0 : lp_res = isl_set_opt(set, max, obj, &res->n);
600 0 : return convert_lp_result(lp_res, res, max);
601 : }
602 :
603 : /* Return the minimum of the integer affine
604 : * expression "obj" over the points in "set".
605 : *
606 : * Return infinity or negative infinity if the optimal value is unbounded and
607 : * NaN if "set" is empty.
608 : */
609 0 : __isl_give isl_val *isl_set_min_val(__isl_keep isl_set *set,
610 : __isl_keep isl_aff *obj)
611 : {
612 0 : return isl_set_opt_val(set, 0, obj);
613 : }
614 :
615 : /* Return the maximum of the integer affine
616 : * expression "obj" over the points in "set".
617 : *
618 : * Return infinity or negative infinity if the optimal value is unbounded and
619 : * NaN if "set" is empty.
620 : */
621 0 : __isl_give isl_val *isl_set_max_val(__isl_keep isl_set *set,
622 : __isl_keep isl_aff *obj)
623 : {
624 0 : return isl_set_opt_val(set, 1, obj);
625 : }
626 :
627 : /* Return the optimum (min or max depending on "max") of "v1" and "v2",
628 : * where either may be NaN, signifying an uninitialized value.
629 : * That is, if either is NaN, then return the other one.
630 : */
631 0 : static __isl_give isl_val *val_opt(__isl_take isl_val *v1,
632 : __isl_take isl_val *v2, int max)
633 : {
634 0 : if (!v1 || !v2)
635 : goto error;
636 0 : if (isl_val_is_nan(v1)) {
637 0 : isl_val_free(v1);
638 0 : return v2;
639 : }
640 0 : if (isl_val_is_nan(v2)) {
641 0 : isl_val_free(v2);
642 0 : return v1;
643 : }
644 0 : if (max)
645 0 : return isl_val_max(v1, v2);
646 : else
647 0 : return isl_val_min(v1, v2);
648 : error:
649 0 : isl_val_free(v1);
650 0 : isl_val_free(v2);
651 0 : return NULL;
652 : }
653 :
654 : /* Internal data structure for isl_pw_aff_opt_val.
655 : *
656 : * "max" is set if the maximum should be computed.
657 : * "res" contains the current optimum and is initialized to NaN.
658 : */
659 : struct isl_pw_aff_opt_data {
660 : int max;
661 :
662 : isl_val *res;
663 : };
664 :
665 : /* Update the optimum in data->res with respect to the affine function
666 : * "aff" defined over "set".
667 : */
668 0 : static isl_stat piece_opt(__isl_take isl_set *set, __isl_take isl_aff *aff,
669 : void *user)
670 : {
671 0 : struct isl_pw_aff_opt_data *data = user;
672 : isl_val *opt;
673 :
674 0 : opt = isl_set_opt_val(set, data->max, aff);
675 0 : isl_set_free(set);
676 0 : isl_aff_free(aff);
677 :
678 0 : data->res = val_opt(data->res, opt, data->max);
679 0 : if (!data->res)
680 0 : return isl_stat_error;
681 :
682 0 : return isl_stat_ok;
683 : }
684 :
685 : /* Return the minimum (maximum if "max" is set) of the integer piecewise affine
686 : * expression "pa" over its definition domain.
687 : *
688 : * Return infinity or negative infinity if the optimal value is unbounded and
689 : * NaN if the domain of "pa" is empty.
690 : *
691 : * Initialize the result to NaN and then update it for each of the pieces
692 : * in "pa".
693 : */
694 0 : static __isl_give isl_val *isl_pw_aff_opt_val(__isl_take isl_pw_aff *pa,
695 : int max)
696 : {
697 0 : struct isl_pw_aff_opt_data data = { max };
698 :
699 0 : data.res = isl_val_nan(isl_pw_aff_get_ctx(pa));
700 0 : if (isl_pw_aff_foreach_piece(pa, &piece_opt, &data) < 0)
701 0 : data.res = isl_val_free(data.res);
702 :
703 0 : isl_pw_aff_free(pa);
704 0 : return data.res;
705 : }
706 :
707 : /* Internal data structure for isl_union_pw_aff_opt_val.
708 : *
709 : * "max" is set if the maximum should be computed.
710 : * "res" contains the current optimum and is initialized to NaN.
711 : */
712 : struct isl_union_pw_aff_opt_data {
713 : int max;
714 :
715 : isl_val *res;
716 : };
717 :
718 : /* Update the optimum in data->res with the optimum of "pa".
719 : */
720 0 : static isl_stat pw_aff_opt(__isl_take isl_pw_aff *pa, void *user)
721 : {
722 0 : struct isl_union_pw_aff_opt_data *data = user;
723 : isl_val *opt;
724 :
725 0 : opt = isl_pw_aff_opt_val(pa, data->max);
726 :
727 0 : data->res = val_opt(data->res, opt, data->max);
728 0 : if (!data->res)
729 0 : return isl_stat_error;
730 :
731 0 : return isl_stat_ok;
732 : }
733 :
734 : /* Return the minimum (maximum if "max" is set) of the integer piecewise affine
735 : * expression "upa" over its definition domain.
736 : *
737 : * Return infinity or negative infinity if the optimal value is unbounded and
738 : * NaN if the domain of the expression is empty.
739 : *
740 : * Initialize the result to NaN and then update it
741 : * for each of the piecewise affine expressions in "upa".
742 : */
743 0 : static __isl_give isl_val *isl_union_pw_aff_opt_val(
744 : __isl_take isl_union_pw_aff *upa, int max)
745 : {
746 0 : struct isl_union_pw_aff_opt_data data = { max };
747 :
748 0 : data.res = isl_val_nan(isl_union_pw_aff_get_ctx(upa));
749 0 : if (isl_union_pw_aff_foreach_pw_aff(upa, &pw_aff_opt, &data) < 0)
750 0 : data.res = isl_val_free(data.res);
751 0 : isl_union_pw_aff_free(upa);
752 :
753 0 : return data.res;
754 : }
755 :
756 : /* Return the minimum of the integer piecewise affine
757 : * expression "upa" over its definition domain.
758 : *
759 : * Return negative infinity if the optimal value is unbounded and
760 : * NaN if the domain of the expression is empty.
761 : */
762 0 : __isl_give isl_val *isl_union_pw_aff_min_val(__isl_take isl_union_pw_aff *upa)
763 : {
764 0 : return isl_union_pw_aff_opt_val(upa, 0);
765 : }
766 :
767 : /* Return the maximum of the integer piecewise affine
768 : * expression "upa" over its definition domain.
769 : *
770 : * Return infinity if the optimal value is unbounded and
771 : * NaN if the domain of the expression is empty.
772 : */
773 0 : __isl_give isl_val *isl_union_pw_aff_max_val(__isl_take isl_union_pw_aff *upa)
774 : {
775 0 : return isl_union_pw_aff_opt_val(upa, 1);
776 : }
777 :
778 : /* Return a list of minima (maxima if "max" is set)
779 : * for each of the expressions in "mupa" over their domains.
780 : *
781 : * An element in the list is infinity or negative infinity if the optimal
782 : * value of the corresponding expression is unbounded and
783 : * NaN if the domain of the expression is empty.
784 : *
785 : * Iterate over all the expressions in "mupa" and collect the results.
786 : */
787 0 : static __isl_give isl_multi_val *isl_multi_union_pw_aff_opt_multi_val(
788 : __isl_take isl_multi_union_pw_aff *mupa, int max)
789 : {
790 : int i, n;
791 : isl_multi_val *mv;
792 :
793 0 : if (!mupa)
794 0 : return NULL;
795 :
796 0 : n = isl_multi_union_pw_aff_dim(mupa, isl_dim_set);
797 0 : mv = isl_multi_val_zero(isl_multi_union_pw_aff_get_space(mupa));
798 :
799 0 : for (i = 0; i < n; ++i) {
800 : isl_val *v;
801 : isl_union_pw_aff *upa;
802 :
803 0 : upa = isl_multi_union_pw_aff_get_union_pw_aff(mupa, i);
804 0 : v = isl_union_pw_aff_opt_val(upa, max);
805 0 : mv = isl_multi_val_set_val(mv, i, v);
806 : }
807 :
808 0 : isl_multi_union_pw_aff_free(mupa);
809 0 : return mv;
810 : }
811 :
812 : /* Return a list of minima (maxima if "max" is set) over the points in "uset"
813 : * for each of the expressions in "obj".
814 : *
815 : * An element in the list is infinity or negative infinity if the optimal
816 : * value of the corresponding expression is unbounded and
817 : * NaN if the intersection of "uset" with the domain of the expression
818 : * is empty.
819 : */
820 0 : static __isl_give isl_multi_val *isl_union_set_opt_multi_union_pw_aff(
821 : __isl_keep isl_union_set *uset, int max,
822 : __isl_keep isl_multi_union_pw_aff *obj)
823 : {
824 0 : uset = isl_union_set_copy(uset);
825 0 : obj = isl_multi_union_pw_aff_copy(obj);
826 0 : obj = isl_multi_union_pw_aff_intersect_domain(obj, uset);
827 0 : return isl_multi_union_pw_aff_opt_multi_val(obj, max);
828 : }
829 :
830 : /* Return a list of minima over the points in "uset"
831 : * for each of the expressions in "obj".
832 : *
833 : * An element in the list is infinity or negative infinity if the optimal
834 : * value of the corresponding expression is unbounded and
835 : * NaN if the intersection of "uset" with the domain of the expression
836 : * is empty.
837 : */
838 0 : __isl_give isl_multi_val *isl_union_set_min_multi_union_pw_aff(
839 : __isl_keep isl_union_set *uset, __isl_keep isl_multi_union_pw_aff *obj)
840 : {
841 0 : return isl_union_set_opt_multi_union_pw_aff(uset, 0, obj);
842 : }
843 :
844 : /* Return a list of minima
845 : * for each of the expressions in "mupa" over their domains.
846 : *
847 : * An element in the list is negative infinity if the optimal
848 : * value of the corresponding expression is unbounded and
849 : * NaN if the domain of the expression is empty.
850 : */
851 0 : __isl_give isl_multi_val *isl_multi_union_pw_aff_min_multi_val(
852 : __isl_take isl_multi_union_pw_aff *mupa)
853 : {
854 0 : return isl_multi_union_pw_aff_opt_multi_val(mupa, 0);
855 : }
856 :
857 : /* Return a list of maxima
858 : * for each of the expressions in "mupa" over their domains.
859 : *
860 : * An element in the list is infinity if the optimal
861 : * value of the corresponding expression is unbounded and
862 : * NaN if the domain of the expression is empty.
863 : */
864 0 : __isl_give isl_multi_val *isl_multi_union_pw_aff_max_multi_val(
865 : __isl_take isl_multi_union_pw_aff *mupa)
866 : {
867 0 : return isl_multi_union_pw_aff_opt_multi_val(mupa, 1);
868 : }
869 :
870 : /* Return the maximal value attained by the given set dimension,
871 : * independently of the parameter values and of any other dimensions.
872 : *
873 : * Return infinity if the optimal value is unbounded and
874 : * NaN if "bset" is empty.
875 : */
876 0 : __isl_give isl_val *isl_basic_set_dim_max_val(__isl_take isl_basic_set *bset,
877 : int pos)
878 : {
879 : isl_local_space *ls;
880 : isl_aff *obj;
881 : isl_val *v;
882 :
883 0 : if (!bset)
884 0 : return NULL;
885 0 : if (pos < 0 || pos >= isl_basic_set_dim(bset, isl_dim_set))
886 0 : isl_die(isl_basic_set_get_ctx(bset), isl_error_invalid,
887 : "position out of bounds", goto error);
888 0 : ls = isl_local_space_from_space(isl_basic_set_get_space(bset));
889 0 : obj = isl_aff_var_on_domain(ls, isl_dim_set, pos);
890 0 : v = isl_basic_set_max_val(bset, obj);
891 0 : isl_aff_free(obj);
892 0 : isl_basic_set_free(bset);
893 :
894 0 : return v;
895 : error:
896 0 : isl_basic_set_free(bset);
897 0 : return NULL;
898 : }
|
