372 lines · c
1/*2 * Copyright 2008-2009 Katholieke Universiteit Leuven3 *4 * Use of this software is governed by the MIT license5 *6 * Written by Sven Verdoolaege, K.U.Leuven, Departement7 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium8 */9 10#include <isl_ctx_private.h>11#include <isl_map_private.h>12#include <isl/lp.h>13#include <isl_seq.h>14#include "isl_tab.h"15#include <isl_options_private.h>16#include <isl_local_space_private.h>17#include <isl_aff_private.h>18#include <isl_mat_private.h>19#include <isl_val_private.h>20#include <isl_vec_private.h>21 22#include <bset_to_bmap.c>23#include <set_to_map.c>24 25static enum isl_lp_result isl_tab_solve_lp(__isl_keep isl_basic_map *bmap,26 int maximize, isl_int *f, isl_int denom, isl_int *opt,27 isl_int *opt_denom, __isl_give isl_vec **sol)28{29 struct isl_tab *tab;30 enum isl_lp_result res;31 isl_size dim = isl_basic_map_dim(bmap, isl_dim_all);32 33 if (dim < 0)34 return isl_lp_error;35 if (maximize)36 isl_seq_neg(f, f, 1 + dim);37 38 bmap = isl_basic_map_gauss(bmap, NULL);39 tab = isl_tab_from_basic_map(bmap, 0);40 res = isl_tab_min(tab, f, denom, opt, opt_denom, 0);41 if (res == isl_lp_ok && sol) {42 *sol = isl_tab_get_sample_value(tab);43 if (!*sol)44 res = isl_lp_error;45 }46 isl_tab_free(tab);47 48 if (maximize)49 isl_seq_neg(f, f, 1 + dim);50 if (maximize && opt)51 isl_int_neg(*opt, *opt);52 53 return res;54}55 56/* Given a basic map "bmap" and an affine combination of the variables "f"57 * with denominator "denom", set *opt / *opt_denom to the minimal58 * (or maximal if "maximize" is true) value attained by f/d over "bmap",59 * assuming the basic map is not empty and the expression cannot attain60 * arbitrarily small (or large) values.61 * If opt_denom is NULL, then *opt is rounded up (or down)62 * to the nearest integer.63 * The return value reflects the nature of the result (empty, unbounded,64 * minimal or maximal value returned in *opt).65 */66enum isl_lp_result isl_basic_map_solve_lp(__isl_keep isl_basic_map *bmap,67 int max, isl_int *f, isl_int d, isl_int *opt, isl_int *opt_denom,68 __isl_give isl_vec **sol)69{70 if (sol)71 *sol = NULL;72 73 if (!bmap)74 return isl_lp_error;75 76 return isl_tab_solve_lp(bmap, max, f, d, opt, opt_denom, sol);77}78 79enum isl_lp_result isl_basic_set_solve_lp(__isl_keep isl_basic_set *bset,80 int max, isl_int *f, isl_int d, isl_int *opt, isl_int *opt_denom,81 __isl_give isl_vec **sol)82{83 return isl_basic_map_solve_lp(bset_to_bmap(bset), max,84 f, d, opt, opt_denom, sol);85}86 87enum isl_lp_result isl_map_solve_lp(__isl_keep isl_map *map, int max,88 isl_int *f, isl_int d, isl_int *opt,89 isl_int *opt_denom,90 __isl_give isl_vec **sol)91{92 int i;93 isl_int o;94 isl_int t;95 isl_int opt_i;96 isl_int opt_denom_i;97 enum isl_lp_result res;98 int max_div;99 isl_vec *v = NULL;100 101 if (!map)102 return isl_lp_error;103 if (map->n == 0)104 return isl_lp_empty;105 106 max_div = 0;107 for (i = 0; i < map->n; ++i)108 if (map->p[i]->n_div > max_div)109 max_div = map->p[i]->n_div;110 if (max_div > 0) {111 isl_size total = isl_map_dim(map, isl_dim_all);112 if (total < 0)113 return isl_lp_error;114 v = isl_vec_alloc(map->ctx, 1 + total + max_div);115 if (!v)116 return isl_lp_error;117 isl_seq_cpy(v->el, f, 1 + total);118 isl_seq_clr(v->el + 1 + total, max_div);119 f = v->el;120 }121 122 if (!opt && map->n > 1 && sol) {123 isl_int_init(o);124 opt = &o;125 }126 if (map->n > 0)127 isl_int_init(opt_i);128 if (map->n > 0 && opt_denom) {129 isl_int_init(opt_denom_i);130 isl_int_init(t);131 }132 133 res = isl_basic_map_solve_lp(map->p[0], max, f, d,134 opt, opt_denom, sol);135 if (res == isl_lp_error || res == isl_lp_unbounded)136 goto done;137 138 if (sol)139 *sol = NULL;140 141 for (i = 1; i < map->n; ++i) {142 isl_vec *sol_i = NULL;143 enum isl_lp_result res_i;144 int better;145 146 res_i = isl_basic_map_solve_lp(map->p[i], max, f, d,147 &opt_i,148 opt_denom ? &opt_denom_i : NULL,149 sol ? &sol_i : NULL);150 if (res_i == isl_lp_error || res_i == isl_lp_unbounded) {151 res = res_i;152 goto done;153 }154 if (res_i == isl_lp_empty)155 continue;156 if (res == isl_lp_empty) {157 better = 1;158 } else if (!opt_denom) {159 if (max)160 better = isl_int_gt(opt_i, *opt);161 else162 better = isl_int_lt(opt_i, *opt);163 } else {164 isl_int_mul(t, opt_i, *opt_denom);165 isl_int_submul(t, *opt, opt_denom_i);166 if (max)167 better = isl_int_is_pos(t);168 else169 better = isl_int_is_neg(t);170 }171 if (better) {172 res = res_i;173 if (opt)174 isl_int_set(*opt, opt_i);175 if (opt_denom)176 isl_int_set(*opt_denom, opt_denom_i);177 if (sol) {178 isl_vec_free(*sol);179 *sol = sol_i;180 }181 } else182 isl_vec_free(sol_i);183 }184 185done:186 isl_vec_free(v);187 if (map->n > 0 && opt_denom) {188 isl_int_clear(opt_denom_i);189 isl_int_clear(t);190 }191 if (map->n > 0)192 isl_int_clear(opt_i);193 if (opt == &o)194 isl_int_clear(o);195 return res;196}197 198enum isl_lp_result isl_set_solve_lp(__isl_keep isl_set *set, int max,199 isl_int *f, isl_int d, isl_int *opt,200 isl_int *opt_denom,201 __isl_give isl_vec **sol)202{203 return isl_map_solve_lp(set_to_map(set), max,204 f, d, opt, opt_denom, sol);205}206 207/* Return the optimal (rational) value of "obj" over "bset", assuming208 * that "obj" and "bset" have aligned parameters and divs.209 * If "max" is set, then the maximal value is computed.210 * Otherwise, the minimal value is computed.211 *212 * Return infinity or negative infinity if the optimal value is unbounded and213 * NaN if "bset" is empty.214 *215 * Call isl_basic_set_solve_lp and translate the results.216 */217static __isl_give isl_val *basic_set_opt_lp(218 __isl_keep isl_basic_set *bset, int max, __isl_keep isl_aff *obj)219{220 isl_ctx *ctx;221 isl_val *res;222 enum isl_lp_result lp_res;223 224 if (!bset || !obj)225 return NULL;226 227 ctx = isl_aff_get_ctx(obj);228 res = isl_val_alloc(ctx);229 if (!res)230 return NULL;231 lp_res = isl_basic_set_solve_lp(bset, max, obj->v->el + 1,232 obj->v->el[0], &res->n, &res->d, NULL);233 if (lp_res == isl_lp_ok)234 return isl_val_normalize(res);235 isl_val_free(res);236 if (lp_res == isl_lp_error)237 return NULL;238 if (lp_res == isl_lp_empty)239 return isl_val_nan(ctx);240 if (max)241 return isl_val_infty(ctx);242 else243 return isl_val_neginfty(ctx);244}245 246/* Return the optimal (rational) value of "obj" over "bset", assuming247 * that "obj" and "bset" have aligned parameters.248 * If "max" is set, then the maximal value is computed.249 * Otherwise, the minimal value is computed.250 *251 * Return infinity or negative infinity if the optimal value is unbounded and252 * NaN if "bset" is empty.253 *254 * Align the divs of "bset" and "obj" and call basic_set_opt_lp.255 */256static __isl_give isl_val *isl_basic_set_opt_lp_val_aligned(257 __isl_keep isl_basic_set *bset, int max, __isl_keep isl_aff *obj)258{259 int *exp1 = NULL;260 int *exp2 = NULL;261 isl_ctx *ctx;262 isl_mat *bset_div = NULL;263 isl_mat *div = NULL;264 isl_val *res;265 isl_size bset_n_div, obj_n_div;266 267 if (!bset || !obj)268 return NULL;269 270 ctx = isl_aff_get_ctx(obj);271 if (!isl_space_is_equal(bset->dim, obj->ls->dim))272 isl_die(ctx, isl_error_invalid,273 "spaces don't match", return NULL);274 275 bset_n_div = isl_basic_set_dim(bset, isl_dim_div);276 obj_n_div = isl_aff_dim(obj, isl_dim_div);277 if (bset_n_div < 0 || obj_n_div < 0)278 return NULL;279 if (bset_n_div == 0 && obj_n_div == 0)280 return basic_set_opt_lp(bset, max, obj);281 282 bset = isl_basic_set_copy(bset);283 obj = isl_aff_copy(obj);284 285 bset_div = isl_basic_set_get_divs(bset);286 exp1 = isl_alloc_array(ctx, int, bset_n_div);287 exp2 = isl_alloc_array(ctx, int, obj_n_div);288 if (!bset_div || (bset_n_div && !exp1) || (obj_n_div && !exp2))289 goto error;290 291 div = isl_merge_divs(bset_div, obj->ls->div, exp1, exp2);292 293 bset = isl_basic_set_expand_divs(bset, isl_mat_copy(div), exp1);294 obj = isl_aff_expand_divs(obj, isl_mat_copy(div), exp2);295 296 res = basic_set_opt_lp(bset, max, obj);297 298 isl_mat_free(bset_div);299 isl_mat_free(div);300 free(exp1);301 free(exp2);302 isl_basic_set_free(bset);303 isl_aff_free(obj);304 305 return res;306error:307 isl_mat_free(div);308 isl_mat_free(bset_div);309 free(exp1);310 free(exp2);311 isl_basic_set_free(bset);312 isl_aff_free(obj);313 return NULL;314}315 316/* Return the optimal (rational) value of "obj" over "bset".317 * If "max" is set, then the maximal value is computed.318 * Otherwise, the minimal value is computed.319 *320 * Return infinity or negative infinity if the optimal value is unbounded and321 * NaN if "bset" is empty.322 */323static __isl_give isl_val *isl_basic_set_opt_lp_val(324 __isl_keep isl_basic_set *bset, int max, __isl_keep isl_aff *obj)325{326 isl_bool equal;327 isl_val *res;328 329 if (!bset || !obj)330 return NULL;331 332 equal = isl_basic_set_space_has_equal_params(bset, obj->ls->dim);333 if (equal < 0)334 return NULL;335 if (equal)336 return isl_basic_set_opt_lp_val_aligned(bset, max, obj);337 338 bset = isl_basic_set_copy(bset);339 obj = isl_aff_copy(obj);340 bset = isl_basic_set_align_params(bset, isl_aff_get_domain_space(obj));341 obj = isl_aff_align_params(obj, isl_basic_set_get_space(bset));342 343 res = isl_basic_set_opt_lp_val_aligned(bset, max, obj);344 345 isl_basic_set_free(bset);346 isl_aff_free(obj);347 348 return res;349}350 351/* Return the minimal (rational) value of "obj" over "bset".352 *353 * Return negative infinity if the minimal value is unbounded and354 * NaN if "bset" is empty.355 */356__isl_give isl_val *isl_basic_set_min_lp_val(__isl_keep isl_basic_set *bset,357 __isl_keep isl_aff *obj)358{359 return isl_basic_set_opt_lp_val(bset, 0, obj);360}361 362/* Return the maximal (rational) value of "obj" over "bset".363 *364 * Return infinity if the maximal value is unbounded and365 * NaN if "bset" is empty.366 */367__isl_give isl_val *isl_basic_set_max_lp_val(__isl_keep isl_basic_set *bset,368 __isl_keep isl_aff *obj)369{370 return isl_basic_set_opt_lp_val(bset, 1, obj);371}372