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
10 #include <isl_ctx_private.h>
11 #include <isl_map_private.h>
13 #include "isl_lp_piplib.h"
16 #include <isl_options_private.h>
17 #include <isl_local_space_private.h>
18 #include <isl_aff_private.h>
19 #include <isl_mat_private.h>
20 #include <isl_val_private.h>
22 enum isl_lp_result isl_tab_solve_lp(struct isl_basic_map *bmap, int maximize,
23 isl_int *f, isl_int denom, isl_int *opt,
28 enum isl_lp_result res;
29 unsigned dim = isl_basic_map_total_dim(bmap);
32 isl_seq_neg(f, f, 1 + dim);
34 bmap = isl_basic_map_gauss(bmap, NULL);
35 tab = isl_tab_from_basic_map(bmap, 0);
36 res = isl_tab_min(tab, f, denom, opt, opt_denom, 0);
37 if (res == isl_lp_ok && sol) {
38 *sol = isl_tab_get_sample_value(tab);
45 isl_seq_neg(f, f, 1 + dim);
47 isl_int_neg(*opt, *opt);
52 /* Given a basic map "bmap" and an affine combination of the variables "f"
53 * with denominator "denom", set *opt / *opt_denom to the minimal
54 * (or maximal if "maximize" is true) value attained by f/d over "bmap",
55 * assuming the basic map is not empty and the expression cannot attain
56 * arbitrarily small (or large) values.
57 * If opt_denom is NULL, then *opt is rounded up (or down)
58 * to the nearest integer.
59 * The return value reflects the nature of the result (empty, unbounded,
60 * minmimal or maximal value returned in *opt).
62 enum isl_lp_result isl_basic_map_solve_lp(struct isl_basic_map *bmap, int max,
63 isl_int *f, isl_int d, isl_int *opt,
73 switch (bmap->ctx->opt->lp_solver) {
75 return isl_pip_solve_lp(bmap, max, f, d, opt, opt_denom, sol);
77 return isl_tab_solve_lp(bmap, max, f, d, opt, opt_denom, sol);
83 enum isl_lp_result isl_basic_set_solve_lp(struct isl_basic_set *bset, int max,
84 isl_int *f, isl_int d, isl_int *opt,
88 return isl_basic_map_solve_lp((struct isl_basic_map *)bset, max,
89 f, d, opt, opt_denom, sol);
92 enum isl_lp_result isl_map_solve_lp(__isl_keep isl_map *map, int max,
93 isl_int *f, isl_int d, isl_int *opt,
102 enum isl_lp_result res;
112 for (i = 0; i < map->n; ++i)
113 if (map->p[i]->n_div > max_div)
114 max_div = map->p[i]->n_div;
116 unsigned total = isl_space_dim(map->dim, isl_dim_all);
117 v = isl_vec_alloc(map->ctx, 1 + total + max_div);
120 isl_seq_cpy(v->el, f, 1 + total);
121 isl_seq_clr(v->el + 1 + total, max_div);
125 if (!opt && map->n > 1 && sol) {
131 if (map->n > 0 && opt_denom) {
132 isl_int_init(opt_denom_i);
136 res = isl_basic_map_solve_lp(map->p[0], max, f, d,
137 opt, opt_denom, sol);
138 if (res == isl_lp_error || res == isl_lp_unbounded)
144 for (i = 1; i < map->n; ++i) {
145 isl_vec *sol_i = NULL;
146 enum isl_lp_result res_i;
149 res_i = isl_basic_map_solve_lp(map->p[i], max, f, d,
151 opt_denom ? &opt_denom_i : NULL,
152 sol ? &sol_i : NULL);
153 if (res_i == isl_lp_error || res_i == isl_lp_unbounded) {
157 if (res_i == isl_lp_empty)
159 if (res == isl_lp_empty) {
161 } else if (!opt_denom) {
163 better = isl_int_gt(opt_i, *opt);
165 better = isl_int_lt(opt_i, *opt);
167 isl_int_mul(t, opt_i, *opt_denom);
168 isl_int_submul(t, *opt, opt_denom_i);
170 better = isl_int_is_pos(t);
172 better = isl_int_is_neg(t);
177 isl_int_set(*opt, opt_i);
179 isl_int_set(*opt_denom, opt_denom_i);
190 if (map->n > 0 && opt_denom) {
191 isl_int_clear(opt_denom_i);
195 isl_int_clear(opt_i);
201 enum isl_lp_result isl_set_solve_lp(__isl_keep isl_set *set, int max,
202 isl_int *f, isl_int d, isl_int *opt,
204 struct isl_vec **sol)
206 return isl_map_solve_lp((struct isl_map *)set, max,
207 f, d, opt, opt_denom, sol);
210 /* Return the optimal (rational) value of "obj" over "bset", assuming
211 * that "obj" and "bset" have aligned parameters and divs.
212 * If "max" is set, then the maximal value is computed.
213 * Otherwise, the minimal value is computed.
215 * Return infinity or negative infinity if the optimal value is unbounded and
216 * NaN if "bset" is empty.
218 * Call isl_basic_set_solve_lp and translate the results.
220 static __isl_give isl_val *basic_set_opt_lp(
221 __isl_keep isl_basic_set *bset, int max, __isl_keep isl_aff *obj)
225 enum isl_lp_result lp_res;
230 ctx = isl_aff_get_ctx(obj);
231 res = isl_val_alloc(ctx);
234 lp_res = isl_basic_set_solve_lp(bset, max, obj->v->el + 1,
235 obj->v->el[0], &res->n, &res->d, NULL);
236 if (lp_res == isl_lp_ok)
237 return isl_val_normalize(res);
239 if (lp_res == isl_lp_error)
241 if (lp_res == isl_lp_empty)
242 return isl_val_nan(ctx);
244 return isl_val_infty(ctx);
246 return isl_val_neginfty(ctx);
249 /* Return the optimal (rational) value of "obj" over "bset", assuming
250 * that "obj" and "bset" have aligned parameters.
251 * If "max" is set, then the maximal value is computed.
252 * Otherwise, the minimal value is computed.
254 * Return infinity or negative infinity if the optimal value is unbounded and
255 * NaN if "bset" is empty.
257 * Align the divs of "bset" and "obj" and call basic_set_opt_lp.
259 static __isl_give isl_val *isl_basic_set_opt_lp_val_aligned(
260 __isl_keep isl_basic_set *bset, int max, __isl_keep isl_aff *obj)
265 isl_mat *bset_div = NULL;
272 ctx = isl_aff_get_ctx(obj);
273 if (!isl_space_is_equal(bset->dim, obj->ls->dim))
274 isl_die(ctx, isl_error_invalid,
275 "spaces don't match", return NULL);
277 if (bset->n_div == 0 && obj->ls->div->n_row == 0)
278 return basic_set_opt_lp(bset, max, obj);
280 bset = isl_basic_set_copy(bset);
281 obj = isl_aff_copy(obj);
283 bset_div = isl_basic_set_get_divs(bset);
284 exp1 = isl_alloc_array(ctx, int, bset_div->n_row);
285 exp2 = isl_alloc_array(ctx, int, obj->ls->div->n_row);
286 if (!bset_div || !exp1 || !exp2)
289 div = isl_merge_divs(bset_div, obj->ls->div, exp1, exp2);
291 bset = isl_basic_set_expand_divs(bset, isl_mat_copy(div), exp1);
292 obj = isl_aff_expand_divs(obj, isl_mat_copy(div), exp2);
294 res = basic_set_opt_lp(bset, max, obj);
296 isl_mat_free(bset_div);
300 isl_basic_set_free(bset);
306 isl_mat_free(bset_div);
309 isl_basic_set_free(bset);
314 /* Return the optimal (rational) value of "obj" over "bset".
315 * If "max" is set, then the maximal value is computed.
316 * Otherwise, the minimal value is computed.
318 * Return infinity or negative infinity if the optimal value is unbounded and
319 * NaN if "bset" is empty.
321 static __isl_give isl_val *isl_basic_set_opt_lp_val(
322 __isl_keep isl_basic_set *bset, int max, __isl_keep isl_aff *obj)
329 if (isl_space_match(bset->dim, isl_dim_param,
330 obj->ls->dim, isl_dim_param))
331 return isl_basic_set_opt_lp_val_aligned(bset, max, obj);
333 bset = isl_basic_set_copy(bset);
334 obj = isl_aff_copy(obj);
335 bset = isl_basic_set_align_params(bset, isl_aff_get_domain_space(obj));
336 obj = isl_aff_align_params(obj, isl_basic_set_get_space(bset));
338 res = isl_basic_set_opt_lp_val_aligned(bset, max, obj);
340 isl_basic_set_free(bset);
346 /* Return the minimal (rational) value of "obj" over "bset".
348 * Return negative infinity if the minimal value is unbounded and
349 * NaN if "bset" is empty.
351 __isl_give isl_val *isl_basic_set_min_lp_val(__isl_keep isl_basic_set *bset,
352 __isl_keep isl_aff *obj)
354 return isl_basic_set_opt_lp_val(bset, 0, obj);
357 /* Return the maximal (rational) value of "obj" over "bset".
359 * Return infinity if the maximal value is unbounded and
360 * NaN if "bset" is empty.
362 __isl_give isl_val *isl_basic_set_max_lp_val(__isl_keep isl_basic_set *bset,
363 __isl_keep isl_aff *obj)
365 return isl_basic_set_opt_lp_val(bset, 1, obj);