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 | 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, type: isl_dim_all); |
51 | if (total < 0) |
52 | goto error; |
53 | unit_box = isl_basic_set_alloc_space(space: isl_basic_set_get_space(bset), |
54 | extra: 0, n_eq: 0, n_ineq: bset->n_ineq); |
55 | |
56 | for (i = 0; i < bset->n_ineq; ++i) { |
57 | k = isl_basic_set_alloc_inequality(bset: unit_box); |
58 | if (k < 0) |
59 | goto error; |
60 | isl_seq_cpy(dst: unit_box->ineq[k], src: bset->ineq[i], len: 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(bset: 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 | */ |
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(bset: isl_basic_set_copy(bset)); |
93 | |
94 | res = isl_basic_set_solve_lp(bset: unit_box, max: 0, f, denom: bset->ctx->one, |
95 | NULL, NULL, sol: &sol); |
96 | if (res == isl_lp_ok) { |
97 | isl_basic_set_free(bset: unit_box); |
98 | return isl_vec_ceil(vec: sol); |
99 | } |
100 | |
101 | isl_basic_set_free(bset: unit_box); |
102 | |
103 | return isl_basic_set_sample_vec(bset: isl_basic_set_copy(bset)); |
104 | } |
105 | |
106 | /* Restrict "bset" to those points with values for f in the interval [l, u]. |
107 | */ |
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, type: isl_dim_all); |
115 | if (total < 0) |
116 | return isl_basic_set_free(bset); |
117 | bset = isl_basic_set_extend_constraints(base: bset, n_eq: 0, n_ineq: 2); |
118 | |
119 | k = isl_basic_set_alloc_inequality(bset); |
120 | if (k < 0) |
121 | goto error; |
122 | isl_seq_cpy(dst: bset->ineq[k], src: f, len: 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(dst: bset->ineq[k], src: f, len: 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 | */ |
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(bset: isl_basic_set_copy(bset), f, l, u: tmp); |
173 | sample = isl_basic_set_sample_vec(bset: slice); |
174 | if (!sample) { |
175 | isl_vec_free(vec: sol); |
176 | sol = NULL; |
177 | break; |
178 | } |
179 | if (sample->size > 0) { |
180 | isl_vec_free(vec: sol); |
181 | sol = sample; |
182 | isl_seq_inner_product(p1: f, p2: sol->el, len: sol->size, prod: opt); |
183 | isl_int_sub_ui(u, *opt, 1); |
184 | divide = 1; |
185 | } else { |
186 | isl_vec_free(vec: 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 | */ |
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, max: 0, f, denom: bset->ctx->one, |
220 | opt, NULL, sol: &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(vec: sol); |
226 | return isl_lp_ok; |
227 | } |
228 | isl_vec_free(vec: 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(vec: sol); |
237 | return isl_lp_empty; |
238 | } |
239 | if (res == isl_lp_unbounded) { |
240 | isl_vec_free(vec: 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(p1: f, p2: sol->el, len: sol->size, prod: 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(vec: sol); |
263 | |
264 | return res; |
265 | } |
266 | |
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, type: isl_dim_all); |
277 | if (dim < 0) |
278 | goto error; |
279 | v = isl_vec_alloc(ctx: bset->ctx, size: 1 + dim); |
280 | if (!v) |
281 | goto error; |
282 | isl_seq_cpy(dst: v->el, src: f, len: 1 + dim); |
283 | bset = isl_basic_set_remove_equalities(bset, T: &T, NULL); |
284 | v = isl_vec_mat_product(vec: v, mat: isl_mat_copy(mat: T)); |
285 | if (!v) |
286 | goto error; |
287 | res = isl_basic_set_solve_ilp(bset, max, f: v->el, opt, sol_p); |
288 | isl_vec_free(vec: v); |
289 | if (res == isl_lp_ok && sol_p) { |
290 | *sol_p = isl_mat_vec_product(mat: T, vec: *sol_p); |
291 | if (!*sol_p) |
292 | res = isl_lp_error; |
293 | } else |
294 | isl_mat_free(mat: T); |
295 | isl_basic_set_free(bset); |
296 | return res; |
297 | error: |
298 | isl_mat_free(mat: 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 | */ |
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, type: isl_dim_all); |
330 | if (dim < 0) |
331 | return isl_lp_error; |
332 | |
333 | if (max) |
334 | isl_seq_neg(dst: f, src: f, len: 1 + dim); |
335 | |
336 | res = solve_ilp(bset, f, opt, sol_p); |
337 | |
338 | if (max) { |
339 | isl_seq_neg(dst: f, src: f, len: 1 + dim); |
340 | isl_int_neg(*opt, *opt); |
341 | } |
342 | |
343 | return res; |
344 | } |
345 | |
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, f: obj->v->el + 1, opt, NULL); |
356 | isl_basic_set_free(bset); |
357 | return res; |
358 | } |
359 | |
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(aff: obj); |
375 | if (!isl_space_is_equal(space1: bset->dim, space2: 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, type: isl_dim_div); |
384 | obj_n_div = isl_aff_dim(aff: obj, type: 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(aff: 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(div1: bset_div, div2: obj->ls->div, exp1, exp2); |
400 | |
401 | bset = isl_basic_set_expand_divs(bset, div: isl_mat_copy(mat: div), exp: exp1); |
402 | obj = isl_aff_expand_divs(aff: obj, div: isl_mat_copy(mat: div), exp: exp2); |
403 | |
404 | res = basic_set_opt(bset, max, obj, opt); |
405 | |
406 | isl_mat_free(mat: bset_div); |
407 | isl_mat_free(mat: div); |
408 | free(ptr: exp1); |
409 | free(ptr: exp2); |
410 | isl_basic_set_free(bset); |
411 | isl_aff_free(aff: obj); |
412 | |
413 | return res; |
414 | error: |
415 | isl_mat_free(mat: div); |
416 | isl_mat_free(mat: bset_div); |
417 | free(ptr: exp1); |
418 | free(ptr: exp2); |
419 | isl_basic_set_free(bset); |
420 | isl_aff_free(aff: 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 | */ |
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(bset: 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(bset: set->p[i], max, obj, opt: &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 | */ |
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, space: 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(aff: obj); |
488 | set = isl_set_align_params(set, model: isl_aff_get_domain_space(aff: obj)); |
489 | obj = isl_aff_align_params(aff: obj, model: 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(aff: 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 | */ |
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(val: 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 | */ |
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(aff: obj); |
549 | res = isl_val_alloc(ctx); |
550 | if (!res) |
551 | return NULL; |
552 | lp_res = isl_basic_set_opt(bset, max, obj, opt: &res->n); |
553 | return convert_lp_result(lp_res, v: 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 | */ |
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, max: 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 | */ |
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(aff: obj); |
587 | res = isl_val_alloc(ctx); |
588 | if (!res) |
589 | return NULL; |
590 | lp_res = isl_set_opt(set, max, obj, opt: &res->n); |
591 | return convert_lp_result(lp_res, v: 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 | */ |
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, max: 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 | */ |
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, max: 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 | */ |
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(v: v1)) { |
628 | isl_val_free(v: v1); |
629 | return v2; |
630 | } |
631 | if (isl_val_is_nan(v: v2)) { |
632 | isl_val_free(v: 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(v: v1); |
641 | isl_val_free(v: 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 | */ |
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, max: data->max, obj: aff); |
666 | isl_set_free(set); |
667 | isl_aff_free(aff); |
668 | |
669 | data->res = val_opt(v1: data->res, v2: opt, max: 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 | */ |
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(ctx: isl_pw_aff_get_ctx(pwaff: pa)); |
691 | if (isl_pw_aff_foreach_piece(pwaff: pa, fn: &piece_opt, user: &data) < 0) |
692 | data.res = isl_val_free(v: data.res); |
693 | |
694 | isl_pw_aff_free(pwaff: pa); |
695 | return data.res; |
696 | } |
697 | |
698 | #undef TYPE |
699 | #define TYPE isl_pw_aff |
700 | #include "isl_ilp_opt_fn_val_templ.c" |
701 | |
702 | #undef TYPE |
703 | #define TYPE isl_pw_multi_aff |
704 | #include "isl_ilp_opt_multi_val_templ.c" |
705 | |
706 | #undef TYPE |
707 | #define TYPE isl_multi_pw_aff |
708 | #include "isl_ilp_opt_multi_val_templ.c" |
709 | |
710 | /* Internal data structure for isl_union_pw_aff_opt_val. |
711 | * |
712 | * "max" is set if the maximum should be computed. |
713 | * "res" contains the current optimum and is initialized to NaN. |
714 | */ |
715 | struct isl_union_pw_aff_opt_data { |
716 | int max; |
717 | |
718 | isl_val *res; |
719 | }; |
720 | |
721 | /* Update the optimum in data->res with the optimum of "pa". |
722 | */ |
723 | static isl_stat pw_aff_opt(__isl_take isl_pw_aff *pa, void *user) |
724 | { |
725 | struct isl_union_pw_aff_opt_data *data = user; |
726 | isl_val *opt; |
727 | |
728 | opt = isl_pw_aff_opt_val(pa, max: data->max); |
729 | |
730 | data->res = val_opt(v1: data->res, v2: opt, max: data->max); |
731 | if (!data->res) |
732 | return isl_stat_error; |
733 | |
734 | return isl_stat_ok; |
735 | } |
736 | |
737 | /* Return the minimum (maximum if "max" is set) of the integer piecewise affine |
738 | * expression "upa" over its definition domain. |
739 | * |
740 | * Return infinity or negative infinity if the optimal value is unbounded and |
741 | * NaN if the domain of the expression is empty. |
742 | * |
743 | * Initialize the result to NaN and then update it |
744 | * for each of the piecewise affine expressions in "upa". |
745 | */ |
746 | static __isl_give isl_val *isl_union_pw_aff_opt_val( |
747 | __isl_take isl_union_pw_aff *upa, int max) |
748 | { |
749 | struct isl_union_pw_aff_opt_data data = { max }; |
750 | |
751 | data.res = isl_val_nan(ctx: isl_union_pw_aff_get_ctx(upa)); |
752 | if (isl_union_pw_aff_foreach_pw_aff(upa, fn: &pw_aff_opt, user: &data) < 0) |
753 | data.res = isl_val_free(v: data.res); |
754 | isl_union_pw_aff_free(upa); |
755 | |
756 | return data.res; |
757 | } |
758 | |
759 | #undef TYPE |
760 | #define TYPE isl_union_pw_aff |
761 | #include "isl_ilp_opt_fn_val_templ.c" |
762 | |
763 | /* Return a list of minima (maxima if "max" is set) |
764 | * for each of the expressions in "mupa" over their domains. |
765 | * |
766 | * An element in the list is infinity or negative infinity if the optimal |
767 | * value of the corresponding expression is unbounded and |
768 | * NaN if the domain of the expression is empty. |
769 | * |
770 | * Iterate over all the expressions in "mupa" and collect the results. |
771 | */ |
772 | static __isl_give isl_multi_val *isl_multi_union_pw_aff_opt_multi_val( |
773 | __isl_take isl_multi_union_pw_aff *mupa, int max) |
774 | { |
775 | int i; |
776 | isl_size n; |
777 | isl_multi_val *mv; |
778 | |
779 | n = isl_multi_union_pw_aff_size(multi: mupa); |
780 | if (n < 0) |
781 | mupa = isl_multi_union_pw_aff_free(multi: mupa); |
782 | if (!mupa) |
783 | return NULL; |
784 | |
785 | mv = isl_multi_val_zero(space: isl_multi_union_pw_aff_get_space(multi: mupa)); |
786 | |
787 | for (i = 0; i < n; ++i) { |
788 | isl_val *v; |
789 | isl_union_pw_aff *upa; |
790 | |
791 | upa = isl_multi_union_pw_aff_get_union_pw_aff(multi: mupa, pos: i); |
792 | v = isl_union_pw_aff_opt_val(upa, max); |
793 | mv = isl_multi_val_set_val(multi: mv, pos: i, el: v); |
794 | } |
795 | |
796 | isl_multi_union_pw_aff_free(multi: mupa); |
797 | return mv; |
798 | } |
799 | |
800 | /* Return a list of minima (maxima if "max" is set) over the points in "uset" |
801 | * for each of the expressions in "obj". |
802 | * |
803 | * An element in the list is infinity or negative infinity if the optimal |
804 | * value of the corresponding expression is unbounded and |
805 | * NaN if the intersection of "uset" with the domain of the expression |
806 | * is empty. |
807 | */ |
808 | static __isl_give isl_multi_val *isl_union_set_opt_multi_union_pw_aff( |
809 | __isl_keep isl_union_set *uset, int max, |
810 | __isl_keep isl_multi_union_pw_aff *obj) |
811 | { |
812 | uset = isl_union_set_copy(uset); |
813 | obj = isl_multi_union_pw_aff_copy(multi: obj); |
814 | obj = isl_multi_union_pw_aff_intersect_domain(mupa: obj, uset); |
815 | return isl_multi_union_pw_aff_opt_multi_val(mupa: obj, max); |
816 | } |
817 | |
818 | /* Return a list of minima over the points in "uset" |
819 | * for each of the expressions in "obj". |
820 | * |
821 | * An element in the list is infinity or negative infinity if the optimal |
822 | * value of the corresponding expression is unbounded and |
823 | * NaN if the intersection of "uset" with the domain of the expression |
824 | * is empty. |
825 | */ |
826 | __isl_give isl_multi_val *isl_union_set_min_multi_union_pw_aff( |
827 | __isl_keep isl_union_set *uset, __isl_keep isl_multi_union_pw_aff *obj) |
828 | { |
829 | return isl_union_set_opt_multi_union_pw_aff(uset, max: 0, obj); |
830 | } |
831 | |
832 | /* Return a list of minima |
833 | * for each of the expressions in "mupa" over their domains. |
834 | * |
835 | * An element in the list is negative infinity if the optimal |
836 | * value of the corresponding expression is unbounded and |
837 | * NaN if the domain of the expression is empty. |
838 | */ |
839 | __isl_give isl_multi_val *isl_multi_union_pw_aff_min_multi_val( |
840 | __isl_take isl_multi_union_pw_aff *mupa) |
841 | { |
842 | return isl_multi_union_pw_aff_opt_multi_val(mupa, max: 0); |
843 | } |
844 | |
845 | /* Return a list of maxima |
846 | * for each of the expressions in "mupa" over their domains. |
847 | * |
848 | * An element in the list is infinity if the optimal |
849 | * value of the corresponding expression is unbounded and |
850 | * NaN if the domain of the expression is empty. |
851 | */ |
852 | __isl_give isl_multi_val *isl_multi_union_pw_aff_max_multi_val( |
853 | __isl_take isl_multi_union_pw_aff *mupa) |
854 | { |
855 | return isl_multi_union_pw_aff_opt_multi_val(mupa, max: 1); |
856 | } |
857 | |
858 | #undef BASE |
859 | #define BASE basic_set |
860 | #include "isl_ilp_opt_val_templ.c" |
861 | |
862 | /* Return the maximal value attained by the given set dimension, |
863 | * independently of the parameter values and of any other dimensions. |
864 | * |
865 | * Return infinity if the optimal value is unbounded and |
866 | * NaN if "bset" is empty. |
867 | */ |
868 | __isl_give isl_val *isl_basic_set_dim_max_val(__isl_take isl_basic_set *bset, |
869 | int pos) |
870 | { |
871 | return isl_basic_set_dim_opt_val(set: bset, max: 1, pos); |
872 | } |
873 | |
874 | #undef BASE |
875 | #define BASE set |
876 | #include "isl_ilp_opt_val_templ.c" |
877 | |
878 | /* Return the minimal value attained by the given set dimension, |
879 | * independently of the parameter values and of any other dimensions. |
880 | * |
881 | * Return negative infinity if the optimal value is unbounded and |
882 | * NaN if "set" is empty. |
883 | */ |
884 | __isl_give isl_val *isl_set_dim_min_val(__isl_take isl_set *set, int pos) |
885 | { |
886 | return isl_set_dim_opt_val(set, max: 0, pos); |
887 | } |
888 | |
889 | /* Return the maximal value attained by the given set dimension, |
890 | * independently of the parameter values and of any other dimensions. |
891 | * |
892 | * Return infinity if the optimal value is unbounded and |
893 | * NaN if "set" is empty. |
894 | */ |
895 | __isl_give isl_val *isl_set_dim_max_val(__isl_take isl_set *set, int pos) |
896 | { |
897 | return isl_set_dim_opt_val(set, max: 1, pos); |
898 | } |
899 | |