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/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 25 static 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 minimal 58 * (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 attain 60 * 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 */ 66 enum 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 79 enum 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 87 enum 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 else 162 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 else 169 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 } else 182 isl_vec_free(sol_i); 183 } 184 185 done: 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 198 enum 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", assuming 208 * 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 and 213 * NaN if "bset" is empty. 214 * 215 * Call isl_basic_set_solve_lp and translate the results. 216 */ 217 static __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 else 243 return isl_val_neginfty(ctx); 244 } 245 246 /* Return the optimal (rational) value of "obj" over "bset", assuming 247 * 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 and 252 * NaN if "bset" is empty. 253 * 254 * Align the divs of "bset" and "obj" and call basic_set_opt_lp. 255 */ 256 static __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; 306 error: 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 and 321 * NaN if "bset" is empty. 322 */ 323 static __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 and 354 * 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 and 365 * 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