streamline isl_multi_*_{gist*,intersect_*}
[isl.git] / isl_ilp.c
blob5aec90639fdc4972b5d730ad8a6be8aebf2922ae
1 /*
2 * Copyright 2008-2009 Katholieke Universiteit Leuven
4 * Use of this software is governed by the MIT license
6 * Written by Sven Verdoolaege, K.U.Leuven, Departement
7 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
8 */
10 #include <isl_ctx_private.h>
11 #include <isl_map_private.h>
12 #include <isl/ilp.h>
13 #include "isl_sample.h"
14 #include <isl_seq.h>
15 #include "isl_equalities.h"
16 #include <isl_aff_private.h>
17 #include <isl_local_space_private.h>
18 #include <isl_mat_private.h>
19 #include <isl_val_private.h>
20 #include <isl_vec_private.h>
21 #include <isl_lp_private.h>
22 #include <isl_ilp_private.h>
23 #include <isl/deprecated/ilp_int.h>
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.
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.
34 static struct isl_basic_set *unit_box_base_points(struct isl_basic_set *bset)
36 int i, j, k;
37 struct isl_basic_set *unit_box = NULL;
38 unsigned total;
40 if (!bset)
41 goto error;
43 if (bset->n_eq != 0) {
44 unit_box = isl_basic_set_empty_like(bset);
45 isl_basic_set_free(bset);
46 return unit_box;
49 total = isl_basic_set_total_dim(bset);
50 unit_box = isl_basic_set_alloc_space(isl_basic_set_get_space(bset),
51 0, 0, bset->n_ineq);
53 for (i = 0; i < bset->n_ineq; ++i) {
54 k = isl_basic_set_alloc_inequality(unit_box);
55 if (k < 0)
56 goto error;
57 isl_seq_cpy(unit_box->ineq[k], bset->ineq[i], 1 + total);
58 for (j = 0; j < total; ++j) {
59 if (isl_int_is_nonneg(unit_box->ineq[k][1 + j]))
60 continue;
61 isl_int_add(unit_box->ineq[k][0],
62 unit_box->ineq[k][0], unit_box->ineq[k][1 + j]);
66 isl_basic_set_free(bset);
67 return unit_box;
68 error:
69 isl_basic_set_free(bset);
70 isl_basic_set_free(unit_box);
71 return NULL;
74 /* Find an integer point in "bset", preferably one that is
75 * close to minimizing "f".
77 * We first check if we can easily put unit boxes inside bset.
78 * If so, we take the best base point of any of the unit boxes we can find
79 * and round it up to the nearest integer.
80 * If not, we simply pick any integer point in "bset".
82 static struct isl_vec *initial_solution(struct isl_basic_set *bset, isl_int *f)
84 enum isl_lp_result res;
85 struct isl_basic_set *unit_box;
86 struct isl_vec *sol;
88 unit_box = unit_box_base_points(isl_basic_set_copy(bset));
90 res = isl_basic_set_solve_lp(unit_box, 0, f, bset->ctx->one,
91 NULL, NULL, &sol);
92 if (res == isl_lp_ok) {
93 isl_basic_set_free(unit_box);
94 return isl_vec_ceil(sol);
97 isl_basic_set_free(unit_box);
99 return isl_basic_set_sample_vec(isl_basic_set_copy(bset));
102 /* Restrict "bset" to those points with values for f in the interval [l, u].
104 static struct isl_basic_set *add_bounds(struct isl_basic_set *bset,
105 isl_int *f, isl_int l, isl_int u)
107 int k;
108 unsigned total;
110 total = isl_basic_set_total_dim(bset);
111 bset = isl_basic_set_extend_constraints(bset, 0, 2);
113 k = isl_basic_set_alloc_inequality(bset);
114 if (k < 0)
115 goto error;
116 isl_seq_cpy(bset->ineq[k], f, 1 + total);
117 isl_int_sub(bset->ineq[k][0], bset->ineq[k][0], l);
119 k = isl_basic_set_alloc_inequality(bset);
120 if (k < 0)
121 goto error;
122 isl_seq_neg(bset->ineq[k], f, 1 + total);
123 isl_int_add(bset->ineq[k][0], bset->ineq[k][0], u);
125 return bset;
126 error:
127 isl_basic_set_free(bset);
128 return NULL;
131 /* Find an integer point in "bset" that minimizes f (in any) such that
132 * the value of f lies inside the interval [l, u].
133 * Return this integer point if it can be found.
134 * Otherwise, return sol.
136 * We perform a number of steps until l > u.
137 * In each step, we look for an integer point with value in either
138 * the whole interval [l, u] or half of the interval [l, l+floor(u-l-1/2)].
139 * The choice depends on whether we have found an integer point in the
140 * previous step. If so, we look for the next point in half of the remaining
141 * interval.
142 * If we find a point, the current solution is updated and u is set
143 * to its value minus 1.
144 * If no point can be found, we update l to the upper bound of the interval
145 * we checked (u or l+floor(u-l-1/2)) plus 1.
147 static struct isl_vec *solve_ilp_search(struct isl_basic_set *bset,
148 isl_int *f, isl_int *opt, struct isl_vec *sol, isl_int l, isl_int u)
150 isl_int tmp;
151 int divide = 1;
153 isl_int_init(tmp);
155 while (isl_int_le(l, u)) {
156 struct isl_basic_set *slice;
157 struct isl_vec *sample;
159 if (!divide)
160 isl_int_set(tmp, u);
161 else {
162 isl_int_sub(tmp, u, l);
163 isl_int_fdiv_q_ui(tmp, tmp, 2);
164 isl_int_add(tmp, tmp, l);
166 slice = add_bounds(isl_basic_set_copy(bset), f, l, tmp);
167 sample = isl_basic_set_sample_vec(slice);
168 if (!sample) {
169 isl_vec_free(sol);
170 sol = NULL;
171 break;
173 if (sample->size > 0) {
174 isl_vec_free(sol);
175 sol = sample;
176 isl_seq_inner_product(f, sol->el, sol->size, opt);
177 isl_int_sub_ui(u, *opt, 1);
178 divide = 1;
179 } else {
180 isl_vec_free(sample);
181 if (!divide)
182 break;
183 isl_int_add_ui(l, tmp, 1);
184 divide = 0;
188 isl_int_clear(tmp);
190 return sol;
193 /* Find an integer point in "bset" that minimizes f (if any).
194 * If sol_p is not NULL then the integer point is returned in *sol_p.
195 * The optimal value of f is returned in *opt.
197 * The algorithm maintains a currently best solution and an interval [l, u]
198 * of values of f for which integer solutions could potentially still be found.
199 * The initial value of the best solution so far is any solution.
200 * The initial value of l is minimal value of f over the rationals
201 * (rounded up to the nearest integer).
202 * The initial value of u is the value of f at the initial solution minus 1.
204 * We then call solve_ilp_search to perform a binary search on the interval.
206 static enum isl_lp_result solve_ilp(struct isl_basic_set *bset,
207 isl_int *f, isl_int *opt,
208 struct isl_vec **sol_p)
210 enum isl_lp_result res;
211 isl_int l, u;
212 struct isl_vec *sol;
214 res = isl_basic_set_solve_lp(bset, 0, f, bset->ctx->one,
215 opt, NULL, &sol);
216 if (res == isl_lp_ok && isl_int_is_one(sol->el[0])) {
217 if (sol_p)
218 *sol_p = sol;
219 else
220 isl_vec_free(sol);
221 return isl_lp_ok;
223 isl_vec_free(sol);
224 if (res == isl_lp_error || res == isl_lp_empty)
225 return res;
227 sol = initial_solution(bset, f);
228 if (!sol)
229 return isl_lp_error;
230 if (sol->size == 0) {
231 isl_vec_free(sol);
232 return isl_lp_empty;
234 if (res == isl_lp_unbounded) {
235 isl_vec_free(sol);
236 return isl_lp_unbounded;
239 isl_int_init(l);
240 isl_int_init(u);
242 isl_int_set(l, *opt);
244 isl_seq_inner_product(f, sol->el, sol->size, opt);
245 isl_int_sub_ui(u, *opt, 1);
247 sol = solve_ilp_search(bset, f, opt, sol, l, u);
248 if (!sol)
249 res = isl_lp_error;
251 isl_int_clear(l);
252 isl_int_clear(u);
254 if (sol_p)
255 *sol_p = sol;
256 else
257 isl_vec_free(sol);
259 return res;
262 static enum isl_lp_result solve_ilp_with_eq(struct isl_basic_set *bset, int max,
263 isl_int *f, isl_int *opt,
264 struct isl_vec **sol_p)
266 unsigned dim;
267 enum isl_lp_result res;
268 struct isl_mat *T = NULL;
269 struct isl_vec *v;
271 bset = isl_basic_set_copy(bset);
272 dim = isl_basic_set_total_dim(bset);
273 v = isl_vec_alloc(bset->ctx, 1 + dim);
274 if (!v)
275 goto error;
276 isl_seq_cpy(v->el, f, 1 + dim);
277 bset = isl_basic_set_remove_equalities(bset, &T, NULL);
278 v = isl_vec_mat_product(v, isl_mat_copy(T));
279 if (!v)
280 goto error;
281 res = isl_basic_set_solve_ilp(bset, max, v->el, opt, sol_p);
282 isl_vec_free(v);
283 if (res == isl_lp_ok && sol_p) {
284 *sol_p = isl_mat_vec_product(T, *sol_p);
285 if (!*sol_p)
286 res = isl_lp_error;
287 } else
288 isl_mat_free(T);
289 isl_basic_set_free(bset);
290 return res;
291 error:
292 isl_mat_free(T);
293 isl_basic_set_free(bset);
294 return isl_lp_error;
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.
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.
305 enum isl_lp_result isl_basic_set_solve_ilp(struct isl_basic_set *bset, int max,
306 isl_int *f, isl_int *opt,
307 struct isl_vec **sol_p)
309 unsigned dim;
310 enum isl_lp_result res;
312 if (!bset)
313 return isl_lp_error;
314 if (sol_p)
315 *sol_p = NULL;
317 isl_assert(bset->ctx, isl_basic_set_n_param(bset) == 0, goto error);
319 if (isl_basic_set_plain_is_empty(bset))
320 return isl_lp_empty;
322 if (bset->n_eq)
323 return solve_ilp_with_eq(bset, max, f, opt, sol_p);
325 dim = isl_basic_set_total_dim(bset);
327 if (max)
328 isl_seq_neg(f, f, 1 + dim);
330 res = solve_ilp(bset, f, opt, sol_p);
332 if (max) {
333 isl_seq_neg(f, f, 1 + dim);
334 isl_int_neg(*opt, *opt);
337 return res;
338 error:
339 isl_basic_set_free(bset);
340 return isl_lp_error;
343 static enum isl_lp_result basic_set_opt(__isl_keep isl_basic_set *bset, int max,
344 __isl_keep isl_aff *obj, isl_int *opt)
346 enum isl_lp_result res;
348 if (!obj)
349 return isl_lp_error;
350 bset = isl_basic_set_copy(bset);
351 bset = isl_basic_set_underlying_set(bset);
352 res = isl_basic_set_solve_ilp(bset, max, obj->v->el + 1, opt, NULL);
353 isl_basic_set_free(bset);
354 return res;
357 static __isl_give isl_mat *extract_divs(__isl_keep isl_basic_set *bset)
359 int i;
360 isl_ctx *ctx = isl_basic_set_get_ctx(bset);
361 isl_mat *div;
363 div = isl_mat_alloc(ctx, bset->n_div,
364 1 + 1 + isl_basic_set_total_dim(bset));
365 if (!div)
366 return NULL;
368 for (i = 0; i < bset->n_div; ++i)
369 isl_seq_cpy(div->row[i], bset->div[i], div->n_col);
371 return div;
374 enum isl_lp_result isl_basic_set_opt(__isl_keep isl_basic_set *bset, int max,
375 __isl_keep isl_aff *obj, isl_int *opt)
377 int *exp1 = NULL;
378 int *exp2 = NULL;
379 isl_ctx *ctx;
380 isl_mat *bset_div = NULL;
381 isl_mat *div = NULL;
382 enum isl_lp_result res;
383 int bset_n_div, obj_n_div;
385 if (!bset || !obj)
386 return isl_lp_error;
388 ctx = isl_aff_get_ctx(obj);
389 if (!isl_space_is_equal(bset->dim, obj->ls->dim))
390 isl_die(ctx, isl_error_invalid,
391 "spaces don't match", return isl_lp_error);
392 if (!isl_int_is_one(obj->v->el[0]))
393 isl_die(ctx, isl_error_unsupported,
394 "expecting integer affine expression",
395 return isl_lp_error);
397 bset_n_div = isl_basic_set_dim(bset, isl_dim_div);
398 obj_n_div = isl_aff_dim(obj, isl_dim_div);
399 if (bset_n_div == 0 && obj_n_div == 0)
400 return basic_set_opt(bset, max, obj, opt);
402 bset = isl_basic_set_copy(bset);
403 obj = isl_aff_copy(obj);
405 bset_div = extract_divs(bset);
406 exp1 = isl_alloc_array(ctx, int, bset_n_div);
407 exp2 = isl_alloc_array(ctx, int, obj_n_div);
408 if (!bset_div || (bset_n_div && !exp1) || (obj_n_div && !exp2))
409 goto error;
411 div = isl_merge_divs(bset_div, obj->ls->div, exp1, exp2);
413 bset = isl_basic_set_expand_divs(bset, isl_mat_copy(div), exp1);
414 obj = isl_aff_expand_divs(obj, isl_mat_copy(div), exp2);
416 res = basic_set_opt(bset, max, obj, opt);
418 isl_mat_free(bset_div);
419 isl_mat_free(div);
420 free(exp1);
421 free(exp2);
422 isl_basic_set_free(bset);
423 isl_aff_free(obj);
425 return res;
426 error:
427 isl_mat_free(div);
428 isl_mat_free(bset_div);
429 free(exp1);
430 free(exp2);
431 isl_basic_set_free(bset);
432 isl_aff_free(obj);
433 return isl_lp_error;
436 /* Compute the minimum (maximum if max is set) of the integer affine
437 * expression obj over the points in set and put the result in *opt.
439 * The parameters are assumed to have been aligned.
441 static enum isl_lp_result isl_set_opt_aligned(__isl_keep isl_set *set, int max,
442 __isl_keep isl_aff *obj, isl_int *opt)
444 int i;
445 enum isl_lp_result res;
446 int empty = 1;
447 isl_int opt_i;
449 if (!set || !obj)
450 return isl_lp_error;
451 if (set->n == 0)
452 return isl_lp_empty;
454 res = isl_basic_set_opt(set->p[0], max, obj, opt);
455 if (res == isl_lp_error || res == isl_lp_unbounded)
456 return res;
457 if (set->n == 1)
458 return res;
459 if (res == isl_lp_ok)
460 empty = 0;
462 isl_int_init(opt_i);
463 for (i = 1; i < set->n; ++i) {
464 res = isl_basic_set_opt(set->p[i], max, obj, &opt_i);
465 if (res == isl_lp_error || res == isl_lp_unbounded) {
466 isl_int_clear(opt_i);
467 return res;
469 if (res == isl_lp_ok)
470 empty = 0;
471 if (max ? isl_int_gt(opt_i, *opt) : isl_int_lt(opt_i, *opt))
472 isl_int_set(*opt, opt_i);
474 isl_int_clear(opt_i);
476 return empty ? isl_lp_empty : isl_lp_ok;
479 /* Compute the minimum (maximum if max is set) of the integer affine
480 * expression obj over the points in set and put the result in *opt.
482 enum isl_lp_result isl_set_opt(__isl_keep isl_set *set, int max,
483 __isl_keep isl_aff *obj, isl_int *opt)
485 enum isl_lp_result res;
487 if (!set || !obj)
488 return isl_lp_error;
490 if (isl_space_match(set->dim, isl_dim_param,
491 obj->ls->dim, isl_dim_param))
492 return isl_set_opt_aligned(set, max, obj, opt);
494 set = isl_set_copy(set);
495 obj = isl_aff_copy(obj);
496 set = isl_set_align_params(set, isl_aff_get_domain_space(obj));
497 obj = isl_aff_align_params(obj, isl_set_get_space(set));
499 res = isl_set_opt_aligned(set, max, obj, opt);
501 isl_set_free(set);
502 isl_aff_free(obj);
504 return res;
507 enum isl_lp_result isl_basic_set_max(__isl_keep isl_basic_set *bset,
508 __isl_keep isl_aff *obj, isl_int *opt)
510 return isl_basic_set_opt(bset, 1, obj, opt);
513 enum isl_lp_result isl_set_max(__isl_keep isl_set *set,
514 __isl_keep isl_aff *obj, isl_int *opt)
516 return isl_set_opt(set, 1, obj, opt);
519 enum isl_lp_result isl_set_min(__isl_keep isl_set *set,
520 __isl_keep isl_aff *obj, isl_int *opt)
522 return isl_set_opt(set, 0, obj, opt);
525 /* Convert the result of a function that returns an isl_lp_result
526 * to an isl_val. The numerator of "v" is set to the optimal value
527 * if lp_res is isl_lp_ok. "max" is set if a maximum was computed.
529 * Return "v" with denominator set to 1 if lp_res is isl_lp_ok.
530 * Return NULL on error.
531 * Return a NaN if lp_res is isl_lp_empty.
532 * Return infinity or negative infinity if lp_res is isl_lp_unbounded,
533 * depending on "max".
535 static __isl_give isl_val *convert_lp_result(enum isl_lp_result lp_res,
536 __isl_take isl_val *v, int max)
538 isl_ctx *ctx;
540 if (lp_res == isl_lp_ok) {
541 isl_int_set_si(v->d, 1);
542 return isl_val_normalize(v);
544 ctx = isl_val_get_ctx(v);
545 isl_val_free(v);
546 if (lp_res == isl_lp_error)
547 return NULL;
548 if (lp_res == isl_lp_empty)
549 return isl_val_nan(ctx);
550 if (max)
551 return isl_val_infty(ctx);
552 else
553 return isl_val_neginfty(ctx);
556 /* Return the minimum (maximum if max is set) of the integer affine
557 * expression "obj" over the points in "bset".
559 * Return infinity or negative infinity if the optimal value is unbounded and
560 * NaN if "bset" is empty.
562 * Call isl_basic_set_opt and translate the results.
564 __isl_give isl_val *isl_basic_set_opt_val(__isl_keep isl_basic_set *bset,
565 int max, __isl_keep isl_aff *obj)
567 isl_ctx *ctx;
568 isl_val *res;
569 enum isl_lp_result lp_res;
571 if (!bset || !obj)
572 return NULL;
574 ctx = isl_aff_get_ctx(obj);
575 res = isl_val_alloc(ctx);
576 if (!res)
577 return NULL;
578 lp_res = isl_basic_set_opt(bset, max, obj, &res->n);
579 return convert_lp_result(lp_res, res, max);
582 /* Return the maximum of the integer affine
583 * expression "obj" over the points in "bset".
585 * Return infinity or negative infinity if the optimal value is unbounded and
586 * NaN if "bset" is empty.
588 __isl_give isl_val *isl_basic_set_max_val(__isl_keep isl_basic_set *bset,
589 __isl_keep isl_aff *obj)
591 return isl_basic_set_opt_val(bset, 1, obj);
594 /* Return the minimum (maximum if max is set) of the integer affine
595 * expression "obj" over the points in "set".
597 * Return infinity or negative infinity if the optimal value is unbounded and
598 * NaN if "bset" is empty.
600 * Call isl_set_opt and translate the results.
602 __isl_give isl_val *isl_set_opt_val(__isl_keep isl_set *set, int max,
603 __isl_keep isl_aff *obj)
605 isl_ctx *ctx;
606 isl_val *res;
607 enum isl_lp_result lp_res;
609 if (!set || !obj)
610 return NULL;
612 ctx = isl_aff_get_ctx(obj);
613 res = isl_val_alloc(ctx);
614 if (!res)
615 return NULL;
616 lp_res = isl_set_opt(set, max, obj, &res->n);
617 return convert_lp_result(lp_res, res, max);
620 /* Return the minimum of the integer affine
621 * expression "obj" over the points in "set".
623 * Return infinity or negative infinity if the optimal value is unbounded and
624 * NaN if "bset" is empty.
626 __isl_give isl_val *isl_set_min_val(__isl_keep isl_set *set,
627 __isl_keep isl_aff *obj)
629 return isl_set_opt_val(set, 0, obj);
632 /* Return the maximum of the integer affine
633 * expression "obj" over the points in "set".
635 * Return infinity or negative infinity if the optimal value is unbounded and
636 * NaN if "bset" is empty.
638 __isl_give isl_val *isl_set_max_val(__isl_keep isl_set *set,
639 __isl_keep isl_aff *obj)
641 return isl_set_opt_val(set, 1, obj);