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/ilp.h>
     13 #include <isl/union_set.h>
     14 #include "isl_sample.h"
     15 #include <isl_seq.h>
     16 #include "isl_equalities.h"
     17 #include <isl_aff_private.h>
     18 #include <isl_local_space_private.h>
     19 #include <isl_mat_private.h>
     20 #include <isl_val_private.h>
     21 #include <isl_vec_private.h>
     22 #include <isl_lp_private.h>
     23 #include <isl_ilp_private.h>
     24 
     25 /* Given a basic set "bset", construct a basic set U such that for
     26  * each element x in U, the whole unit box positioned at x is inside
     27  * the given basic set.
     28  * Note that U may not contain all points that satisfy this property.
     29  *
     30  * We simply add the sum of all negative coefficients to the constant
     31  * term.  This ensures that if x satisfies the resulting constraints,
     32  * then x plus any sum of unit vectors satisfies the original constraints.
     33  */
     34 static __isl_give isl_basic_set *unit_box_base_points(
     35 	__isl_take isl_basic_set *bset)
     36 {
     37 	int i, j, k;
     38 	struct isl_basic_set *unit_box = NULL;
     39 	isl_size total;
     40 
     41 	if (!bset)
     42 		goto error;
     43 
     44 	if (bset->n_eq != 0) {
     45 		isl_space *space = isl_basic_set_get_space(bset);
     46 		isl_basic_set_free(bset);
     47 		return isl_basic_set_empty(space);
     48 	}
     49 
     50 	total = isl_basic_set_dim(bset, isl_dim_all);
     51 	if (total < 0)
     52 		goto error;
     53 	unit_box = isl_basic_set_alloc_space(isl_basic_set_get_space(bset),
     54 					0, 0, bset->n_ineq);
     55 
     56 	for (i = 0; i < bset->n_ineq; ++i) {
     57 		k = isl_basic_set_alloc_inequality(unit_box);
     58 		if (k < 0)
     59 			goto error;
     60 		isl_seq_cpy(unit_box->ineq[k], bset->ineq[i], 1 + total);
     61 		for (j = 0; j < total; ++j) {
     62 			if (isl_int_is_nonneg(unit_box->ineq[k][1 + j]))
     63 				continue;
     64 			isl_int_add(unit_box->ineq[k][0],
     65 				unit_box->ineq[k][0], unit_box->ineq[k][1 + j]);
     66 		}
     67 	}
     68 
     69 	isl_basic_set_free(bset);
     70 	return unit_box;
     71 error:
     72 	isl_basic_set_free(bset);
     73 	isl_basic_set_free(unit_box);
     74 	return NULL;
     75 }
     76 
     77 /* Find an integer point in "bset", preferably one that is
     78  * close to minimizing "f".
     79  *
     80  * We first check if we can easily put unit boxes inside bset.
     81  * If so, we take the best base point of any of the unit boxes we can find
     82  * and round it up to the nearest integer.
     83  * If not, we simply pick any integer point in "bset".
     84  */
     85 static __isl_give isl_vec *initial_solution(__isl_keep isl_basic_set *bset,
     86 	isl_int *f)
     87 {
     88 	enum isl_lp_result res;
     89 	struct isl_basic_set *unit_box;
     90 	struct isl_vec *sol;
     91 
     92 	unit_box = unit_box_base_points(isl_basic_set_copy(bset));
     93 
     94 	res = isl_basic_set_solve_lp(unit_box, 0, f, bset->ctx->one,
     95 					NULL, NULL, &sol);
     96 	if (res == isl_lp_ok) {
     97 		isl_basic_set_free(unit_box);
     98 		return isl_vec_ceil(sol);
     99 	}
    100 
    101 	isl_basic_set_free(unit_box);
    102 
    103 	return isl_basic_set_sample_vec(isl_basic_set_copy(bset));
    104 }
    105 
    106 /* Restrict "bset" to those points with values for f in the interval [l, u].
    107  */
    108 static __isl_give isl_basic_set *add_bounds(__isl_take isl_basic_set *bset,
    109 	isl_int *f, isl_int l, isl_int u)
    110 {
    111 	int k;
    112 	isl_size total;
    113 
    114 	total = isl_basic_set_dim(bset, isl_dim_all);
    115 	if (total < 0)
    116 		return isl_basic_set_free(bset);
    117 	bset = isl_basic_set_extend_constraints(bset, 0, 2);
    118 
    119 	k = isl_basic_set_alloc_inequality(bset);
    120 	if (k < 0)
    121 		goto error;
    122 	isl_seq_cpy(bset->ineq[k], f, 1 + total);
    123 	isl_int_sub(bset->ineq[k][0], bset->ineq[k][0], l);
    124 
    125 	k = isl_basic_set_alloc_inequality(bset);
    126 	if (k < 0)
    127 		goto error;
    128 	isl_seq_neg(bset->ineq[k], f, 1 + total);
    129 	isl_int_add(bset->ineq[k][0], bset->ineq[k][0], u);
    130 
    131 	return bset;
    132 error:
    133 	isl_basic_set_free(bset);
    134 	return NULL;
    135 }
    136 
    137 /* Find an integer point in "bset" that minimizes f (in any) such that
    138  * the value of f lies inside the interval [l, u].
    139  * Return this integer point if it can be found.
    140  * Otherwise, return sol.
    141  *
    142  * We perform a number of steps until l > u.
    143  * In each step, we look for an integer point with value in either
    144  * the whole interval [l, u] or half of the interval [l, l+floor(u-l-1/2)].
    145  * The choice depends on whether we have found an integer point in the
    146  * previous step.  If so, we look for the next point in half of the remaining
    147  * interval.
    148  * If we find a point, the current solution is updated and u is set
    149  * to its value minus 1.
    150  * If no point can be found, we update l to the upper bound of the interval
    151  * we checked (u or l+floor(u-l-1/2)) plus 1.
    152  */
    153 static __isl_give isl_vec *solve_ilp_search(__isl_keep isl_basic_set *bset,
    154 	isl_int *f, isl_int *opt, __isl_take isl_vec *sol, isl_int l, isl_int u)
    155 {
    156 	isl_int tmp;
    157 	int divide = 1;
    158 
    159 	isl_int_init(tmp);
    160 
    161 	while (isl_int_le(l, u)) {
    162 		struct isl_basic_set *slice;
    163 		struct isl_vec *sample;
    164 
    165 		if (!divide)
    166 			isl_int_set(tmp, u);
    167 		else {
    168 			isl_int_sub(tmp, u, l);
    169 			isl_int_fdiv_q_ui(tmp, tmp, 2);
    170 			isl_int_add(tmp, tmp, l);
    171 		}
    172 		slice = add_bounds(isl_basic_set_copy(bset), f, l, tmp);
    173 		sample = isl_basic_set_sample_vec(slice);
    174 		if (!sample) {
    175 			isl_vec_free(sol);
    176 			sol = NULL;
    177 			break;
    178 		}
    179 		if (sample->size > 0) {
    180 			isl_vec_free(sol);
    181 			sol = sample;
    182 			isl_seq_inner_product(f, sol->el, sol->size, opt);
    183 			isl_int_sub_ui(u, *opt, 1);
    184 			divide = 1;
    185 		} else {
    186 			isl_vec_free(sample);
    187 			if (!divide)
    188 				break;
    189 			isl_int_add_ui(l, tmp, 1);
    190 			divide = 0;
    191 		}
    192 	}
    193 
    194 	isl_int_clear(tmp);
    195 
    196 	return sol;
    197 }
    198 
    199 /* Find an integer point in "bset" that minimizes f (if any).
    200  * If sol_p is not NULL then the integer point is returned in *sol_p.
    201  * The optimal value of f is returned in *opt.
    202  *
    203  * The algorithm maintains a currently best solution and an interval [l, u]
    204  * of values of f for which integer solutions could potentially still be found.
    205  * The initial value of the best solution so far is any solution.
    206  * The initial value of l is minimal value of f over the rationals
    207  * (rounded up to the nearest integer).
    208  * The initial value of u is the value of f at the initial solution minus 1.
    209  *
    210  * We then call solve_ilp_search to perform a binary search on the interval.
    211  */
    212 static enum isl_lp_result solve_ilp(__isl_keep isl_basic_set *bset,
    213 	isl_int *f, isl_int *opt, __isl_give isl_vec **sol_p)
    214 {
    215 	enum isl_lp_result res;
    216 	isl_int l, u;
    217 	struct isl_vec *sol;
    218 
    219 	res = isl_basic_set_solve_lp(bset, 0, f, bset->ctx->one,
    220 					opt, NULL, &sol);
    221 	if (res == isl_lp_ok && isl_int_is_one(sol->el[0])) {
    222 		if (sol_p)
    223 			*sol_p = sol;
    224 		else
    225 			isl_vec_free(sol);
    226 		return isl_lp_ok;
    227 	}
    228 	isl_vec_free(sol);
    229 	if (res == isl_lp_error || res == isl_lp_empty)
    230 		return res;
    231 
    232 	sol = initial_solution(bset, f);
    233 	if (!sol)
    234 		return isl_lp_error;
    235 	if (sol->size == 0) {
    236 		isl_vec_free(sol);
    237 		return isl_lp_empty;
    238 	}
    239 	if (res == isl_lp_unbounded) {
    240 		isl_vec_free(sol);
    241 		return isl_lp_unbounded;
    242 	}
    243 
    244 	isl_int_init(l);
    245 	isl_int_init(u);
    246 
    247 	isl_int_set(l, *opt);
    248 
    249 	isl_seq_inner_product(f, sol->el, sol->size, opt);
    250 	isl_int_sub_ui(u, *opt, 1);
    251 
    252 	sol = solve_ilp_search(bset, f, opt, sol, l, u);
    253 	if (!sol)
    254 		res = isl_lp_error;
    255 
    256 	isl_int_clear(l);
    257 	isl_int_clear(u);
    258 
    259 	if (sol_p)
    260 		*sol_p = sol;
    261 	else
    262 		isl_vec_free(sol);
    263 
    264 	return res;
    265 }
    266 
    267 static enum isl_lp_result solve_ilp_with_eq(__isl_keep isl_basic_set *bset,
    268 	int max, isl_int *f, isl_int *opt, __isl_give isl_vec **sol_p)
    269 {
    270 	isl_size dim;
    271 	enum isl_lp_result res;
    272 	struct isl_mat *T = NULL;
    273 	struct isl_vec *v;
    274 
    275 	bset = isl_basic_set_copy(bset);
    276 	dim = isl_basic_set_dim(bset, isl_dim_all);
    277 	if (dim < 0)
    278 		goto error;
    279 	v = isl_vec_alloc(bset->ctx, 1 + dim);
    280 	if (!v)
    281 		goto error;
    282 	isl_seq_cpy(v->el, f, 1 + dim);
    283 	bset = isl_basic_set_remove_equalities(bset, &T, NULL);
    284 	v = isl_vec_mat_product(v, isl_mat_copy(T));
    285 	if (!v)
    286 		goto error;
    287 	res = isl_basic_set_solve_ilp(bset, max, v->el, opt, sol_p);
    288 	isl_vec_free(v);
    289 	if (res == isl_lp_ok && sol_p) {
    290 		*sol_p = isl_mat_vec_product(T, *sol_p);
    291 		if (!*sol_p)
    292 			res = isl_lp_error;
    293 	} else
    294 		isl_mat_free(T);
    295 	isl_basic_set_free(bset);
    296 	return res;
    297 error:
    298 	isl_mat_free(T);
    299 	isl_basic_set_free(bset);
    300 	return isl_lp_error;
    301 }
    302 
    303 /* Find an integer point in "bset" that minimizes (or maximizes if max is set)
    304  * f (if any).
    305  * If sol_p is not NULL then the integer point is returned in *sol_p.
    306  * The optimal value of f is returned in *opt.
    307  *
    308  * If there is any equality among the points in "bset", then we first
    309  * project it out.  Otherwise, we continue with solve_ilp above.
    310  */
    311 enum isl_lp_result isl_basic_set_solve_ilp(__isl_keep isl_basic_set *bset,
    312 	int max, isl_int *f, isl_int *opt, __isl_give isl_vec **sol_p)
    313 {
    314 	isl_size dim;
    315 	enum isl_lp_result res;
    316 
    317 	if (sol_p)
    318 		*sol_p = NULL;
    319 
    320 	if (isl_basic_set_check_no_params(bset) < 0)
    321 		return isl_lp_error;
    322 
    323 	if (isl_basic_set_plain_is_empty(bset))
    324 		return isl_lp_empty;
    325 
    326 	if (bset->n_eq)
    327 		return solve_ilp_with_eq(bset, max, f, opt, sol_p);
    328 
    329 	dim = isl_basic_set_dim(bset, isl_dim_all);
    330 	if (dim < 0)
    331 		return isl_lp_error;
    332 
    333 	if (max)
    334 		isl_seq_neg(f, f, 1 + dim);
    335 
    336 	res = solve_ilp(bset, f, opt, sol_p);
    337 
    338 	if (max) {
    339 		isl_seq_neg(f, f, 1 + dim);
    340 		isl_int_neg(*opt, *opt);
    341 	}
    342 
    343 	return res;
    344 }
    345 
    346 static enum isl_lp_result basic_set_opt(__isl_keep isl_basic_set *bset, int max,
    347 	__isl_keep isl_aff *obj, isl_int *opt)
    348 {
    349 	enum isl_lp_result res;
    350 
    351 	if (!obj)
    352 		return isl_lp_error;
    353 	bset = isl_basic_set_copy(bset);
    354 	bset = isl_basic_set_underlying_set(bset);
    355 	res = isl_basic_set_solve_ilp(bset, max, obj->v->el + 1, opt, NULL);
    356 	isl_basic_set_free(bset);
    357 	return res;
    358 }
    359 
    360 enum isl_lp_result isl_basic_set_opt(__isl_keep isl_basic_set *bset, int max,
    361 	__isl_keep isl_aff *obj, isl_int *opt)
    362 {
    363 	int *exp1 = NULL;
    364 	int *exp2 = NULL;
    365 	isl_ctx *ctx;
    366 	isl_mat *bset_div = NULL;
    367 	isl_mat *div = NULL;
    368 	enum isl_lp_result res;
    369 	isl_size bset_n_div, obj_n_div;
    370 
    371 	if (!bset || !obj)
    372 		return isl_lp_error;
    373 
    374 	ctx = isl_aff_get_ctx(obj);
    375 	if (!isl_space_is_equal(bset->dim, obj->ls->dim))
    376 		isl_die(ctx, isl_error_invalid,
    377 			"spaces don't match", return isl_lp_error);
    378 	if (!isl_int_is_one(obj->v->el[0]))
    379 		isl_die(ctx, isl_error_unsupported,
    380 			"expecting integer affine expression",
    381 			return isl_lp_error);
    382 
    383 	bset_n_div = isl_basic_set_dim(bset, isl_dim_div);
    384 	obj_n_div = isl_aff_dim(obj, isl_dim_div);
    385 	if (bset_n_div < 0 || obj_n_div < 0)
    386 		return isl_lp_error;
    387 	if (bset_n_div == 0 && obj_n_div == 0)
    388 		return basic_set_opt(bset, max, obj, opt);
    389 
    390 	bset = isl_basic_set_copy(bset);
    391 	obj = isl_aff_copy(obj);
    392 
    393 	bset_div = isl_basic_set_get_divs(bset);
    394 	exp1 = isl_alloc_array(ctx, int, bset_n_div);
    395 	exp2 = isl_alloc_array(ctx, int, obj_n_div);
    396 	if (!bset_div || (bset_n_div && !exp1) || (obj_n_div && !exp2))
    397 		goto error;
    398 
    399 	div = isl_merge_divs(bset_div, obj->ls->div, exp1, exp2);
    400 
    401 	bset = isl_basic_set_expand_divs(bset, isl_mat_copy(div), exp1);
    402 	obj = isl_aff_expand_divs(obj, isl_mat_copy(div), exp2);
    403 
    404 	res = basic_set_opt(bset, max, obj, opt);
    405 
    406 	isl_mat_free(bset_div);
    407 	isl_mat_free(div);
    408 	free(exp1);
    409 	free(exp2);
    410 	isl_basic_set_free(bset);
    411 	isl_aff_free(obj);
    412 
    413 	return res;
    414 error:
    415 	isl_mat_free(div);
    416 	isl_mat_free(bset_div);
    417 	free(exp1);
    418 	free(exp2);
    419 	isl_basic_set_free(bset);
    420 	isl_aff_free(obj);
    421 	return isl_lp_error;
    422 }
    423 
    424 /* Compute the minimum (maximum if max is set) of the integer affine
    425  * expression obj over the points in set and put the result in *opt.
    426  *
    427  * The parameters are assumed to have been aligned.
    428  */
    429 static enum isl_lp_result isl_set_opt_aligned(__isl_keep isl_set *set, int max,
    430 	__isl_keep isl_aff *obj, isl_int *opt)
    431 {
    432 	int i;
    433 	enum isl_lp_result res;
    434 	int empty = 1;
    435 	isl_int opt_i;
    436 
    437 	if (!set || !obj)
    438 		return isl_lp_error;
    439 	if (set->n == 0)
    440 		return isl_lp_empty;
    441 
    442 	res = isl_basic_set_opt(set->p[0], max, obj, opt);
    443 	if (res == isl_lp_error || res == isl_lp_unbounded)
    444 		return res;
    445 	if (set->n == 1)
    446 		return res;
    447 	if (res == isl_lp_ok)
    448 		empty = 0;
    449 
    450 	isl_int_init(opt_i);
    451 	for (i = 1; i < set->n; ++i) {
    452 		res = isl_basic_set_opt(set->p[i], max, obj, &opt_i);
    453 		if (res == isl_lp_error || res == isl_lp_unbounded) {
    454 			isl_int_clear(opt_i);
    455 			return res;
    456 		}
    457 		if (res == isl_lp_empty)
    458 			continue;
    459 		empty = 0;
    460 		if (max ? isl_int_gt(opt_i, *opt) : isl_int_lt(opt_i, *opt))
    461 			isl_int_set(*opt, opt_i);
    462 	}
    463 	isl_int_clear(opt_i);
    464 
    465 	return empty ? isl_lp_empty : isl_lp_ok;
    466 }
    467 
    468 /* Compute the minimum (maximum if max is set) of the integer affine
    469  * expression obj over the points in set and put the result in *opt.
    470  */
    471 enum isl_lp_result isl_set_opt(__isl_keep isl_set *set, int max,
    472 	__isl_keep isl_aff *obj, isl_int *opt)
    473 {
    474 	enum isl_lp_result res;
    475 	isl_bool aligned;
    476 
    477 	if (!set || !obj)
    478 		return isl_lp_error;
    479 
    480 	aligned = isl_set_space_has_equal_params(set, obj->ls->dim);
    481 	if (aligned < 0)
    482 		return isl_lp_error;
    483 	if (aligned)
    484 		return isl_set_opt_aligned(set, max, obj, opt);
    485 
    486 	set = isl_set_copy(set);
    487 	obj = isl_aff_copy(obj);
    488 	set = isl_set_align_params(set, isl_aff_get_domain_space(obj));
    489 	obj = isl_aff_align_params(obj, isl_set_get_space(set));
    490 
    491 	res = isl_set_opt_aligned(set, max, obj, opt);
    492 
    493 	isl_set_free(set);
    494 	isl_aff_free(obj);
    495 
    496 	return res;
    497 }
    498 
    499 /* Convert the result of a function that returns an isl_lp_result
    500  * to an isl_val.  The numerator of "v" is set to the optimal value
    501  * if lp_res is isl_lp_ok.  "max" is set if a maximum was computed.
    502  *
    503  * Return "v" with denominator set to 1 if lp_res is isl_lp_ok.
    504  * Return NULL on error.
    505  * Return a NaN if lp_res is isl_lp_empty.
    506  * Return infinity or negative infinity if lp_res is isl_lp_unbounded,
    507  * depending on "max".
    508  */
    509 static __isl_give isl_val *convert_lp_result(enum isl_lp_result lp_res,
    510 	__isl_take isl_val *v, int max)
    511 {
    512 	isl_ctx *ctx;
    513 
    514 	if (lp_res == isl_lp_ok) {
    515 		isl_int_set_si(v->d, 1);
    516 		return isl_val_normalize(v);
    517 	}
    518 	ctx = isl_val_get_ctx(v);
    519 	isl_val_free(v);
    520 	if (lp_res == isl_lp_error)
    521 		return NULL;
    522 	if (lp_res == isl_lp_empty)
    523 		return isl_val_nan(ctx);
    524 	if (max)
    525 		return isl_val_infty(ctx);
    526 	else
    527 		return isl_val_neginfty(ctx);
    528 }
    529 
    530 /* Return the minimum (maximum if max is set) of the integer affine
    531  * expression "obj" over the points in "bset".
    532  *
    533  * Return infinity or negative infinity if the optimal value is unbounded and
    534  * NaN if "bset" is empty.
    535  *
    536  * Call isl_basic_set_opt and translate the results.
    537  */
    538 __isl_give isl_val *isl_basic_set_opt_val(__isl_keep isl_basic_set *bset,
    539 	int max, __isl_keep isl_aff *obj)
    540 {
    541 	isl_ctx *ctx;
    542 	isl_val *res;
    543 	enum isl_lp_result lp_res;
    544 
    545 	if (!bset || !obj)
    546 		return NULL;
    547 
    548 	ctx = isl_aff_get_ctx(obj);
    549 	res = isl_val_alloc(ctx);
    550 	if (!res)
    551 		return NULL;
    552 	lp_res = isl_basic_set_opt(bset, max, obj, &res->n);
    553 	return convert_lp_result(lp_res, res, max);
    554 }
    555 
    556 /* Return the maximum of the integer affine
    557  * expression "obj" over the points in "bset".
    558  *
    559  * Return infinity or negative infinity if the optimal value is unbounded and
    560  * NaN if "bset" is empty.
    561  */
    562 __isl_give isl_val *isl_basic_set_max_val(__isl_keep isl_basic_set *bset,
    563 	__isl_keep isl_aff *obj)
    564 {
    565 	return isl_basic_set_opt_val(bset, 1, obj);
    566 }
    567 
    568 /* Return the minimum (maximum if max is set) of the integer affine
    569  * expression "obj" over the points in "set".
    570  *
    571  * Return infinity or negative infinity if the optimal value is unbounded and
    572  * NaN if "set" is empty.
    573  *
    574  * Call isl_set_opt and translate the results.
    575  */
    576 __isl_give isl_val *isl_set_opt_val(__isl_keep isl_set *set, int max,
    577 	__isl_keep isl_aff *obj)
    578 {
    579 	isl_ctx *ctx;
    580 	isl_val *res;
    581 	enum isl_lp_result lp_res;
    582 
    583 	if (!set || !obj)
    584 		return NULL;
    585 
    586 	ctx = isl_aff_get_ctx(obj);
    587 	res = isl_val_alloc(ctx);
    588 	if (!res)
    589 		return NULL;
    590 	lp_res = isl_set_opt(set, max, obj, &res->n);
    591 	return convert_lp_result(lp_res, res, max);
    592 }
    593 
    594 /* Return the minimum of the integer affine
    595  * expression "obj" over the points in "set".
    596  *
    597  * Return infinity or negative infinity if the optimal value is unbounded and
    598  * NaN if "set" is empty.
    599  */
    600 __isl_give isl_val *isl_set_min_val(__isl_keep isl_set *set,
    601 	__isl_keep isl_aff *obj)
    602 {
    603 	return isl_set_opt_val(set, 0, obj);
    604 }
    605 
    606 /* Return the maximum of the integer affine
    607  * expression "obj" over the points in "set".
    608  *
    609  * Return infinity or negative infinity if the optimal value is unbounded and
    610  * NaN if "set" is empty.
    611  */
    612 __isl_give isl_val *isl_set_max_val(__isl_keep isl_set *set,
    613 	__isl_keep isl_aff *obj)
    614 {
    615 	return isl_set_opt_val(set, 1, obj);
    616 }
    617 
    618 /* Return the optimum (min or max depending on "max") of "v1" and "v2",
    619  * where either may be NaN, signifying an uninitialized value.
    620  * That is, if either is NaN, then return the other one.
    621  */
    622 static __isl_give isl_val *val_opt(__isl_take isl_val *v1,
    623 	__isl_take isl_val *v2, int max)
    624 {
    625 	if (!v1 || !v2)
    626 		goto error;
    627 	if (isl_val_is_nan(v1)) {
    628 		isl_val_free(v1);
    629 		return v2;
    630 	}
    631 	if (isl_val_is_nan(v2)) {
    632 		isl_val_free(v2);
    633 		return v1;
    634 	}
    635 	if (max)
    636 		return isl_val_max(v1, v2);
    637 	else
    638 		return isl_val_min(v1, v2);
    639 error:
    640 	isl_val_free(v1);
    641 	isl_val_free(v2);
    642 	return NULL;
    643 }
    644 
    645 /* Internal data structure for isl_pw_aff_opt_val.
    646  *
    647  * "max" is set if the maximum should be computed.
    648  * "res" contains the current optimum and is initialized to NaN.
    649  */
    650 struct isl_pw_aff_opt_data {
    651 	int max;
    652 
    653 	isl_val *res;
    654 };
    655 
    656 /* Update the optimum in data->res with respect to the affine function
    657  * "aff" defined over "set".
    658  */
    659 static isl_stat piece_opt(__isl_take isl_set *set, __isl_take isl_aff *aff,
    660 	void *user)
    661 {
    662 	struct isl_pw_aff_opt_data *data = user;
    663 	isl_val *opt;
    664 
    665 	opt = isl_set_opt_val(set, data->max, aff);
    666 	isl_set_free(set);
    667 	isl_aff_free(aff);
    668 
    669 	data->res = val_opt(data->res, opt, data->max);
    670 	if (!data->res)
    671 		return isl_stat_error;
    672 
    673 	return isl_stat_ok;
    674 }
    675 
    676 /* Return the minimum (maximum if "max" is set) of the integer piecewise affine
    677  * expression "pa" over its definition domain.
    678  *
    679  * Return infinity or negative infinity if the optimal value is unbounded and
    680  * NaN if the domain of "pa" is empty.
    681  *
    682  * Initialize the result to NaN and then update it for each of the pieces
    683  * in "pa".
    684  */
    685 static __isl_give isl_val *isl_pw_aff_opt_val(__isl_take isl_pw_aff *pa,
    686 	int max)
    687 {
    688 	struct isl_pw_aff_opt_data data = { max };
    689 
    690 	data.res = isl_val_nan(isl_pw_aff_get_ctx(pa));
    691 	if (isl_pw_aff_foreach_piece(pa, &piece_opt, &data) < 0)
    692 		data.res = isl_val_free(data.res);
    693 
    694 	isl_pw_aff_free(pa);
    695 	return data.res;
    696 }
    697 
    698 #undef TYPE
    699 #define TYPE isl_pw_aff
    700 #include "isl_ilp_opt_fn_val_templ.c"
    701 
    702 #undef TYPE
    703 #define TYPE isl_pw_multi_aff
    704 #include "isl_ilp_opt_multi_val_templ.c"
    705 
    706 #undef TYPE
    707 #define TYPE isl_multi_pw_aff
    708 #include "isl_ilp_opt_multi_val_templ.c"
    709 
    710 /* Internal data structure for isl_union_pw_aff_opt_val.
    711  *
    712  * "max" is set if the maximum should be computed.
    713  * "res" contains the current optimum and is initialized to NaN.
    714  */
    715 struct isl_union_pw_aff_opt_data {
    716 	int max;
    717 
    718 	isl_val *res;
    719 };
    720 
    721 /* Update the optimum in data->res with the optimum of "pa".
    722  */
    723 static isl_stat pw_aff_opt(__isl_take isl_pw_aff *pa, void *user)
    724 {
    725 	struct isl_union_pw_aff_opt_data *data = user;
    726 	isl_val *opt;
    727 
    728 	opt = isl_pw_aff_opt_val(pa, data->max);
    729 
    730 	data->res = val_opt(data->res, opt, data->max);
    731 	if (!data->res)
    732 		return isl_stat_error;
    733 
    734 	return isl_stat_ok;
    735 }
    736 
    737 /* Return the minimum (maximum if "max" is set) of the integer piecewise affine
    738  * expression "upa" over its definition domain.
    739  *
    740  * Return infinity or negative infinity if the optimal value is unbounded and
    741  * NaN if the domain of the expression is empty.
    742  *
    743  * Initialize the result to NaN and then update it
    744  * for each of the piecewise affine expressions in "upa".
    745  */
    746 static __isl_give isl_val *isl_union_pw_aff_opt_val(
    747 	__isl_take isl_union_pw_aff *upa, int max)
    748 {
    749 	struct isl_union_pw_aff_opt_data data = { max };
    750 
    751 	data.res = isl_val_nan(isl_union_pw_aff_get_ctx(upa));
    752 	if (isl_union_pw_aff_foreach_pw_aff(upa, &pw_aff_opt, &data) < 0)
    753 		data.res = isl_val_free(data.res);
    754 	isl_union_pw_aff_free(upa);
    755 
    756 	return data.res;
    757 }
    758 
    759 #undef TYPE
    760 #define TYPE isl_union_pw_aff
    761 #include "isl_ilp_opt_fn_val_templ.c"
    762 
    763 /* Return a list of minima (maxima if "max" is set)
    764  * for each of the expressions in "mupa" over their domains.
    765  *
    766  * An element in the list is infinity or negative infinity if the optimal
    767  * value of the corresponding expression is unbounded and
    768  * NaN if the domain of the expression is empty.
    769  *
    770  * Iterate over all the expressions in "mupa" and collect the results.
    771  */
    772 static __isl_give isl_multi_val *isl_multi_union_pw_aff_opt_multi_val(
    773 	__isl_take isl_multi_union_pw_aff *mupa, int max)
    774 {
    775 	int i;
    776 	isl_size n;
    777 	isl_multi_val *mv;
    778 
    779 	n = isl_multi_union_pw_aff_size(mupa);
    780 	if (n < 0)
    781 		mupa = isl_multi_union_pw_aff_free(mupa);
    782 	if (!mupa)
    783 		return NULL;
    784 
    785 	mv = isl_multi_val_zero(isl_multi_union_pw_aff_get_space(mupa));
    786 
    787 	for (i = 0; i < n; ++i) {
    788 		isl_val *v;
    789 		isl_union_pw_aff *upa;
    790 
    791 		upa = isl_multi_union_pw_aff_get_union_pw_aff(mupa, i);
    792 		v = isl_union_pw_aff_opt_val(upa, max);
    793 		mv = isl_multi_val_set_val(mv, i, v);
    794 	}
    795 
    796 	isl_multi_union_pw_aff_free(mupa);
    797 	return mv;
    798 }
    799 
    800 /* Return a list of minima (maxima if "max" is set) over the points in "uset"
    801  * for each of the expressions in "obj".
    802  *
    803  * An element in the list is infinity or negative infinity if the optimal
    804  * value of the corresponding expression is unbounded and
    805  * NaN if the intersection of "uset" with the domain of the expression
    806  * is empty.
    807  */
    808 static __isl_give isl_multi_val *isl_union_set_opt_multi_union_pw_aff(
    809 	__isl_keep isl_union_set *uset, int max,
    810 	__isl_keep isl_multi_union_pw_aff *obj)
    811 {
    812 	uset = isl_union_set_copy(uset);
    813 	obj = isl_multi_union_pw_aff_copy(obj);
    814 	obj = isl_multi_union_pw_aff_intersect_domain(obj, uset);
    815 	return isl_multi_union_pw_aff_opt_multi_val(obj, max);
    816 }
    817 
    818 /* Return a list of minima over the points in "uset"
    819  * for each of the expressions in "obj".
    820  *
    821  * An element in the list is infinity or negative infinity if the optimal
    822  * value of the corresponding expression is unbounded and
    823  * NaN if the intersection of "uset" with the domain of the expression
    824  * is empty.
    825  */
    826 __isl_give isl_multi_val *isl_union_set_min_multi_union_pw_aff(
    827 	__isl_keep isl_union_set *uset, __isl_keep isl_multi_union_pw_aff *obj)
    828 {
    829 	return isl_union_set_opt_multi_union_pw_aff(uset, 0, obj);
    830 }
    831 
    832 /* Return a list of minima
    833  * for each of the expressions in "mupa" over their domains.
    834  *
    835  * An element in the list is negative infinity if the optimal
    836  * value of the corresponding expression is unbounded and
    837  * NaN if the domain of the expression is empty.
    838  */
    839 __isl_give isl_multi_val *isl_multi_union_pw_aff_min_multi_val(
    840 	__isl_take isl_multi_union_pw_aff *mupa)
    841 {
    842 	return isl_multi_union_pw_aff_opt_multi_val(mupa, 0);
    843 }
    844 
    845 /* Return a list of maxima
    846  * for each of the expressions in "mupa" over their domains.
    847  *
    848  * An element in the list is infinity if the optimal
    849  * value of the corresponding expression is unbounded and
    850  * NaN if the domain of the expression is empty.
    851  */
    852 __isl_give isl_multi_val *isl_multi_union_pw_aff_max_multi_val(
    853 	__isl_take isl_multi_union_pw_aff *mupa)
    854 {
    855 	return isl_multi_union_pw_aff_opt_multi_val(mupa, 1);
    856 }
    857 
    858 #undef BASE
    859 #define BASE	basic_set
    860 #include "isl_ilp_opt_val_templ.c"
    861 
    862 /* Return the maximal value attained by the given set dimension,
    863  * independently of the parameter values and of any other dimensions.
    864  *
    865  * Return infinity if the optimal value is unbounded and
    866  * NaN if "bset" is empty.
    867  */
    868 __isl_give isl_val *isl_basic_set_dim_max_val(__isl_take isl_basic_set *bset,
    869 	int pos)
    870 {
    871 	return isl_basic_set_dim_opt_val(bset, 1, pos);
    872 }
    873 
    874 #undef BASE
    875 #define BASE	set
    876 #include "isl_ilp_opt_val_templ.c"
    877 
    878 /* Return the minimal value attained by the given set dimension,
    879  * independently of the parameter values and of any other dimensions.
    880  *
    881  * Return negative infinity if the optimal value is unbounded and
    882  * NaN if "set" is empty.
    883  */
    884 __isl_give isl_val *isl_set_dim_min_val(__isl_take isl_set *set, int pos)
    885 {
    886 	return isl_set_dim_opt_val(set, 0, pos);
    887 }
    888 
    889 /* Return the maximal value attained by the given set dimension,
    890  * independently of the parameter values and of any other dimensions.
    891  *
    892  * Return infinity if the optimal value is unbounded and
    893  * NaN if "set" is empty.
    894  */
    895 __isl_give isl_val *isl_set_dim_max_val(__isl_take isl_set *set, int pos)
    896 {
    897 	return isl_set_dim_opt_val(set, 1, pos);
    898 }
    899