hide undocumented *_solve_lp functions
[isl.git] / isl_ilp.c
blob35e8eb5289fbaa060ab3758ed988ce0487507ac2
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>
23 /* Given a basic set "bset", construct a basic set U such that for
24 * each element x in U, the whole unit box positioned at x is inside
25 * the given basic set.
26 * Note that U may not contain all points that satisfy this property.
28 * We simply add the sum of all negative coefficients to the constant
29 * term. This ensures that if x satisfies the resulting constraints,
30 * then x plus any sum of unit vectors satisfies the original constraints.
32 static struct isl_basic_set *unit_box_base_points(struct isl_basic_set *bset)
34 int i, j, k;
35 struct isl_basic_set *unit_box = NULL;
36 unsigned total;
38 if (!bset)
39 goto error;
41 if (bset->n_eq != 0) {
42 unit_box = isl_basic_set_empty_like(bset);
43 isl_basic_set_free(bset);
44 return unit_box;
47 total = isl_basic_set_total_dim(bset);
48 unit_box = isl_basic_set_alloc_space(isl_basic_set_get_space(bset),
49 0, 0, bset->n_ineq);
51 for (i = 0; i < bset->n_ineq; ++i) {
52 k = isl_basic_set_alloc_inequality(unit_box);
53 if (k < 0)
54 goto error;
55 isl_seq_cpy(unit_box->ineq[k], bset->ineq[i], 1 + total);
56 for (j = 0; j < total; ++j) {
57 if (isl_int_is_nonneg(unit_box->ineq[k][1 + j]))
58 continue;
59 isl_int_add(unit_box->ineq[k][0],
60 unit_box->ineq[k][0], unit_box->ineq[k][1 + j]);
64 isl_basic_set_free(bset);
65 return unit_box;
66 error:
67 isl_basic_set_free(bset);
68 isl_basic_set_free(unit_box);
69 return NULL;
72 /* Find an integer point in "bset", preferably one that is
73 * close to minimizing "f".
75 * We first check if we can easily put unit boxes inside bset.
76 * If so, we take the best base point of any of the unit boxes we can find
77 * and round it up to the nearest integer.
78 * If not, we simply pick any integer point in "bset".
80 static struct isl_vec *initial_solution(struct isl_basic_set *bset, isl_int *f)
82 enum isl_lp_result res;
83 struct isl_basic_set *unit_box;
84 struct isl_vec *sol;
86 unit_box = unit_box_base_points(isl_basic_set_copy(bset));
88 res = isl_basic_set_solve_lp(unit_box, 0, f, bset->ctx->one,
89 NULL, NULL, &sol);
90 if (res == isl_lp_ok) {
91 isl_basic_set_free(unit_box);
92 return isl_vec_ceil(sol);
95 isl_basic_set_free(unit_box);
97 return isl_basic_set_sample_vec(isl_basic_set_copy(bset));
100 /* Restrict "bset" to those points with values for f in the interval [l, u].
102 static struct isl_basic_set *add_bounds(struct isl_basic_set *bset,
103 isl_int *f, isl_int l, isl_int u)
105 int k;
106 unsigned total;
108 total = isl_basic_set_total_dim(bset);
109 bset = isl_basic_set_extend_constraints(bset, 0, 2);
111 k = isl_basic_set_alloc_inequality(bset);
112 if (k < 0)
113 goto error;
114 isl_seq_cpy(bset->ineq[k], f, 1 + total);
115 isl_int_sub(bset->ineq[k][0], bset->ineq[k][0], l);
117 k = isl_basic_set_alloc_inequality(bset);
118 if (k < 0)
119 goto error;
120 isl_seq_neg(bset->ineq[k], f, 1 + total);
121 isl_int_add(bset->ineq[k][0], bset->ineq[k][0], u);
123 return bset;
124 error:
125 isl_basic_set_free(bset);
126 return NULL;
129 /* Find an integer point in "bset" that minimizes f (in any) such that
130 * the value of f lies inside the interval [l, u].
131 * Return this integer point if it can be found.
132 * Otherwise, return sol.
134 * We perform a number of steps until l > u.
135 * In each step, we look for an integer point with value in either
136 * the whole interval [l, u] or half of the interval [l, l+floor(u-l-1/2)].
137 * The choice depends on whether we have found an integer point in the
138 * previous step. If so, we look for the next point in half of the remaining
139 * interval.
140 * If we find a point, the current solution is updated and u is set
141 * to its value minus 1.
142 * If no point can be found, we update l to the upper bound of the interval
143 * we checked (u or l+floor(u-l-1/2)) plus 1.
145 static struct isl_vec *solve_ilp_search(struct isl_basic_set *bset,
146 isl_int *f, isl_int *opt, struct isl_vec *sol, isl_int l, isl_int u)
148 isl_int tmp;
149 int divide = 1;
151 isl_int_init(tmp);
153 while (isl_int_le(l, u)) {
154 struct isl_basic_set *slice;
155 struct isl_vec *sample;
157 if (!divide)
158 isl_int_set(tmp, u);
159 else {
160 isl_int_sub(tmp, u, l);
161 isl_int_fdiv_q_ui(tmp, tmp, 2);
162 isl_int_add(tmp, tmp, l);
164 slice = add_bounds(isl_basic_set_copy(bset), f, l, tmp);
165 sample = isl_basic_set_sample_vec(slice);
166 if (!sample) {
167 isl_vec_free(sol);
168 sol = NULL;
169 break;
171 if (sample->size > 0) {
172 isl_vec_free(sol);
173 sol = sample;
174 isl_seq_inner_product(f, sol->el, sol->size, opt);
175 isl_int_sub_ui(u, *opt, 1);
176 divide = 1;
177 } else {
178 isl_vec_free(sample);
179 if (!divide)
180 break;
181 isl_int_add_ui(l, tmp, 1);
182 divide = 0;
186 isl_int_clear(tmp);
188 return sol;
191 /* Find an integer point in "bset" that minimizes f (if any).
192 * If sol_p is not NULL then the integer point is returned in *sol_p.
193 * The optimal value of f is returned in *opt.
195 * The algorithm maintains a currently best solution and an interval [l, u]
196 * of values of f for which integer solutions could potentially still be found.
197 * The initial value of the best solution so far is any solution.
198 * The initial value of l is minimal value of f over the rationals
199 * (rounded up to the nearest integer).
200 * The initial value of u is the value of f at the initial solution minus 1.
202 * We then call solve_ilp_search to perform a binary search on the interval.
204 static enum isl_lp_result solve_ilp(struct isl_basic_set *bset,
205 isl_int *f, isl_int *opt,
206 struct isl_vec **sol_p)
208 enum isl_lp_result res;
209 isl_int l, u;
210 struct isl_vec *sol;
212 res = isl_basic_set_solve_lp(bset, 0, f, bset->ctx->one,
213 opt, NULL, &sol);
214 if (res == isl_lp_ok && isl_int_is_one(sol->el[0])) {
215 if (sol_p)
216 *sol_p = sol;
217 else
218 isl_vec_free(sol);
219 return isl_lp_ok;
221 isl_vec_free(sol);
222 if (res == isl_lp_error || res == isl_lp_empty)
223 return res;
225 sol = initial_solution(bset, f);
226 if (!sol)
227 return isl_lp_error;
228 if (sol->size == 0) {
229 isl_vec_free(sol);
230 return isl_lp_empty;
232 if (res == isl_lp_unbounded) {
233 isl_vec_free(sol);
234 return isl_lp_unbounded;
237 isl_int_init(l);
238 isl_int_init(u);
240 isl_int_set(l, *opt);
242 isl_seq_inner_product(f, sol->el, sol->size, opt);
243 isl_int_sub_ui(u, *opt, 1);
245 sol = solve_ilp_search(bset, f, opt, sol, l, u);
246 if (!sol)
247 res = isl_lp_error;
249 isl_int_clear(l);
250 isl_int_clear(u);
252 if (sol_p)
253 *sol_p = sol;
254 else
255 isl_vec_free(sol);
257 return res;
260 static enum isl_lp_result solve_ilp_with_eq(struct isl_basic_set *bset, int max,
261 isl_int *f, isl_int *opt,
262 struct isl_vec **sol_p)
264 unsigned dim;
265 enum isl_lp_result res;
266 struct isl_mat *T = NULL;
267 struct isl_vec *v;
269 bset = isl_basic_set_copy(bset);
270 dim = isl_basic_set_total_dim(bset);
271 v = isl_vec_alloc(bset->ctx, 1 + dim);
272 if (!v)
273 goto error;
274 isl_seq_cpy(v->el, f, 1 + dim);
275 bset = isl_basic_set_remove_equalities(bset, &T, NULL);
276 v = isl_vec_mat_product(v, isl_mat_copy(T));
277 if (!v)
278 goto error;
279 res = isl_basic_set_solve_ilp(bset, max, v->el, opt, sol_p);
280 isl_vec_free(v);
281 if (res == isl_lp_ok && sol_p) {
282 *sol_p = isl_mat_vec_product(T, *sol_p);
283 if (!*sol_p)
284 res = isl_lp_error;
285 } else
286 isl_mat_free(T);
287 isl_basic_set_free(bset);
288 return res;
289 error:
290 isl_mat_free(T);
291 isl_basic_set_free(bset);
292 return isl_lp_error;
295 /* Find an integer point in "bset" that minimizes (or maximizes if max is set)
296 * f (if any).
297 * If sol_p is not NULL then the integer point is returned in *sol_p.
298 * The optimal value of f is returned in *opt.
300 * If there is any equality among the points in "bset", then we first
301 * project it out. Otherwise, we continue with solve_ilp above.
303 enum isl_lp_result isl_basic_set_solve_ilp(struct isl_basic_set *bset, int max,
304 isl_int *f, isl_int *opt,
305 struct isl_vec **sol_p)
307 unsigned dim;
308 enum isl_lp_result res;
310 if (!bset)
311 return isl_lp_error;
312 if (sol_p)
313 *sol_p = NULL;
315 isl_assert(bset->ctx, isl_basic_set_n_param(bset) == 0, goto error);
317 if (isl_basic_set_plain_is_empty(bset))
318 return isl_lp_empty;
320 if (bset->n_eq)
321 return solve_ilp_with_eq(bset, max, f, opt, sol_p);
323 dim = isl_basic_set_total_dim(bset);
325 if (max)
326 isl_seq_neg(f, f, 1 + dim);
328 res = solve_ilp(bset, f, opt, sol_p);
330 if (max) {
331 isl_seq_neg(f, f, 1 + dim);
332 isl_int_neg(*opt, *opt);
335 return res;
336 error:
337 isl_basic_set_free(bset);
338 return isl_lp_error;
341 static enum isl_lp_result basic_set_opt(__isl_keep isl_basic_set *bset, int max,
342 __isl_keep isl_aff *obj, isl_int *opt)
344 enum isl_lp_result res;
346 if (!obj)
347 return isl_lp_error;
348 bset = isl_basic_set_copy(bset);
349 bset = isl_basic_set_underlying_set(bset);
350 res = isl_basic_set_solve_ilp(bset, max, obj->v->el + 1, opt, NULL);
351 isl_basic_set_free(bset);
352 return res;
355 static __isl_give isl_mat *extract_divs(__isl_keep isl_basic_set *bset)
357 int i;
358 isl_ctx *ctx = isl_basic_set_get_ctx(bset);
359 isl_mat *div;
361 div = isl_mat_alloc(ctx, bset->n_div,
362 1 + 1 + isl_basic_set_total_dim(bset));
363 if (!div)
364 return NULL;
366 for (i = 0; i < bset->n_div; ++i)
367 isl_seq_cpy(div->row[i], bset->div[i], div->n_col);
369 return div;
372 enum isl_lp_result isl_basic_set_opt(__isl_keep isl_basic_set *bset, int max,
373 __isl_keep isl_aff *obj, isl_int *opt)
375 int *exp1 = NULL;
376 int *exp2 = NULL;
377 isl_ctx *ctx;
378 isl_mat *bset_div = NULL;
379 isl_mat *div = NULL;
380 enum isl_lp_result res;
381 int bset_n_div;
383 if (!bset || !obj)
384 return isl_lp_error;
386 ctx = isl_aff_get_ctx(obj);
387 if (!isl_space_is_equal(bset->dim, obj->ls->dim))
388 isl_die(ctx, isl_error_invalid,
389 "spaces don't match", return isl_lp_error);
390 if (!isl_int_is_one(obj->v->el[0]))
391 isl_die(ctx, isl_error_unsupported,
392 "expecting integer affine expression",
393 return isl_lp_error);
395 bset_n_div = isl_basic_set_dim(bset, isl_dim_div);
396 if (bset_n_div == 0 && obj->ls->div->n_row == 0)
397 return basic_set_opt(bset, max, obj, opt);
399 bset = isl_basic_set_copy(bset);
400 obj = isl_aff_copy(obj);
402 bset_div = extract_divs(bset);
403 exp1 = isl_alloc_array(ctx, int, bset_n_div);
404 exp2 = isl_alloc_array(ctx, int, obj->ls->div->n_row);
405 if (!bset_div || !exp1 || !exp2)
406 goto error;
408 div = isl_merge_divs(bset_div, obj->ls->div, exp1, exp2);
410 bset = isl_basic_set_expand_divs(bset, isl_mat_copy(div), exp1);
411 obj = isl_aff_expand_divs(obj, isl_mat_copy(div), exp2);
413 res = basic_set_opt(bset, max, obj, opt);
415 isl_mat_free(bset_div);
416 isl_mat_free(div);
417 free(exp1);
418 free(exp2);
419 isl_basic_set_free(bset);
420 isl_aff_free(obj);
422 return res;
423 error:
424 isl_mat_free(div);
425 isl_mat_free(bset_div);
426 free(exp1);
427 free(exp2);
428 isl_basic_set_free(bset);
429 isl_aff_free(obj);
430 return isl_lp_error;
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.
436 * The parameters are assumed to have been aligned.
438 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)
441 int i;
442 enum isl_lp_result res;
443 int empty = 1;
444 isl_int opt_i;
446 if (!set || !obj)
447 return isl_lp_error;
448 if (set->n == 0)
449 return isl_lp_empty;
451 res = isl_basic_set_opt(set->p[0], max, obj, opt);
452 if (res == isl_lp_error || res == isl_lp_unbounded)
453 return res;
454 if (set->n == 1)
455 return res;
456 if (res == isl_lp_ok)
457 empty = 0;
459 isl_int_init(opt_i);
460 for (i = 1; i < set->n; ++i) {
461 res = isl_basic_set_opt(set->p[i], max, obj, &opt_i);
462 if (res == isl_lp_error || res == isl_lp_unbounded) {
463 isl_int_clear(opt_i);
464 return res;
466 if (res == isl_lp_ok)
467 empty = 0;
468 if (isl_int_gt(opt_i, *opt))
469 isl_int_set(*opt, opt_i);
471 isl_int_clear(opt_i);
473 return empty ? isl_lp_empty : isl_lp_ok;
476 /* Compute the minimum (maximum if max is set) of the integer affine
477 * expression obj over the points in set and put the result in *opt.
479 enum isl_lp_result isl_set_opt(__isl_keep isl_set *set, int max,
480 __isl_keep isl_aff *obj, isl_int *opt)
482 enum isl_lp_result res;
484 if (!set || !obj)
485 return isl_lp_error;
487 if (isl_space_match(set->dim, isl_dim_param,
488 obj->ls->dim, isl_dim_param))
489 return isl_set_opt_aligned(set, max, obj, opt);
491 set = isl_set_copy(set);
492 obj = isl_aff_copy(obj);
493 set = isl_set_align_params(set, isl_aff_get_domain_space(obj));
494 obj = isl_aff_align_params(obj, isl_set_get_space(set));
496 res = isl_set_opt_aligned(set, max, obj, opt);
498 isl_set_free(set);
499 isl_aff_free(obj);
501 return res;
504 enum isl_lp_result isl_basic_set_max(__isl_keep isl_basic_set *bset,
505 __isl_keep isl_aff *obj, isl_int *opt)
507 return isl_basic_set_opt(bset, 1, obj, opt);
510 enum isl_lp_result isl_set_max(__isl_keep isl_set *set,
511 __isl_keep isl_aff *obj, isl_int *opt)
513 return isl_set_opt(set, 1, obj, opt);
516 enum isl_lp_result isl_set_min(__isl_keep isl_set *set,
517 __isl_keep isl_aff *obj, isl_int *opt)
519 return isl_set_opt(set, 0, obj, opt);
522 /* Convert the result of a function that returns an isl_lp_result
523 * to an isl_val. The numerator of "v" is set to the optimal value
524 * if lp_res is isl_lp_ok. "max" is set if a maximum was computed.
526 * Return "v" with denominator set to 1 if lp_res is isl_lp_ok.
527 * Return NULL on error.
528 * Return a NaN if lp_res is isl_lp_empty.
529 * Return infinity or negative infinity if lp_res is isl_lp_unbounded,
530 * depending on "max".
532 static __isl_give isl_val *convert_lp_result(enum isl_lp_result lp_res,
533 __isl_take isl_val *v, int max)
535 isl_ctx *ctx;
537 if (lp_res == isl_lp_ok) {
538 isl_int_set_si(v->d, 1);
539 return isl_val_normalize(v);
541 ctx = isl_val_get_ctx(v);
542 isl_val_free(v);
543 if (lp_res == isl_lp_error)
544 return NULL;
545 if (lp_res == isl_lp_empty)
546 return isl_val_nan(ctx);
547 if (max)
548 return isl_val_infty(ctx);
549 else
550 return isl_val_neginfty(ctx);
553 /* Return the minimum (maximum if max is set) of the integer affine
554 * expression "obj" over the points in "bset".
556 * Return infinity or negative infinity if the optimal value is unbounded and
557 * NaN if "bset" is empty.
559 * Call isl_basic_set_opt and translate the results.
561 __isl_give isl_val *isl_basic_set_opt_val(__isl_keep isl_basic_set *bset,
562 int max, __isl_keep isl_aff *obj)
564 isl_ctx *ctx;
565 isl_val *res;
566 enum isl_lp_result lp_res;
568 if (!bset || !obj)
569 return NULL;
571 ctx = isl_aff_get_ctx(obj);
572 res = isl_val_alloc(ctx);
573 if (!res)
574 return NULL;
575 lp_res = isl_basic_set_opt(bset, max, obj, &res->n);
576 return convert_lp_result(lp_res, res, max);
579 /* Return the maximum of the integer affine
580 * expression "obj" over the points in "bset".
582 * Return infinity or negative infinity if the optimal value is unbounded and
583 * NaN if "bset" is empty.
585 __isl_give isl_val *isl_basic_set_max_val(__isl_keep isl_basic_set *bset,
586 __isl_keep isl_aff *obj)
588 return isl_basic_set_opt_val(bset, 1, obj);
591 /* Return the minimum (maximum if max is set) of the integer affine
592 * expression "obj" over the points in "set".
594 * Return infinity or negative infinity if the optimal value is unbounded and
595 * NaN if "bset" is empty.
597 * Call isl_set_opt and translate the results.
599 __isl_give isl_val *isl_set_opt_val(__isl_keep isl_set *set, int max,
600 __isl_keep isl_aff *obj)
602 isl_ctx *ctx;
603 isl_val *res;
604 enum isl_lp_result lp_res;
606 if (!set || !obj)
607 return NULL;
609 ctx = isl_aff_get_ctx(obj);
610 res = isl_val_alloc(ctx);
611 if (!res)
612 return NULL;
613 lp_res = isl_set_opt(set, max, obj, &res->n);
614 return convert_lp_result(lp_res, res, max);
617 /* Return the minimum of the integer affine
618 * expression "obj" over the points in "set".
620 * Return infinity or negative infinity if the optimal value is unbounded and
621 * NaN if "bset" is empty.
623 __isl_give isl_val *isl_set_min_val(__isl_keep isl_set *set,
624 __isl_keep isl_aff *obj)
626 return isl_set_opt_val(set, 0, obj);
629 /* Return the maximum of the integer affine
630 * expression "obj" over the points in "set".
632 * Return infinity or negative infinity if the optimal value is unbounded and
633 * NaN if "bset" is empty.
635 __isl_give isl_val *isl_set_max_val(__isl_keep isl_set *set,
636 __isl_keep isl_aff *obj)
638 return isl_set_opt_val(set, 1, obj);