Home | History | Annotate | Line # | Download | only in dist
      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