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