X-Git-Url: http://review.tizen.org/git/?a=blobdiff_plain;f=isl_sample.c;h=c6a0f314425b0bc2d4683589997a3034b652abe0;hb=de51a9bc4da5dd3f1f9f57c2362da6f9752c44e0;hp=847f0de5e608eee2d7c9926bd8d5a28447ff2ce9;hpb=98ac0c5d9475e69afe5fb456b2d1af70feaaf013;p=platform%2Fupstream%2Fisl.git diff --git a/isl_sample.c b/isl_sample.c index 847f0de..c6a0f31 100644 --- a/isl_sample.c +++ b/isl_sample.c @@ -1,12 +1,25 @@ +/* + * Copyright 2008-2009 Katholieke Universiteit Leuven + * + * Use of this software is governed by the MIT license + * + * Written by Sven Verdoolaege, K.U.Leuven, Departement + * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium + */ + +#include +#include #include "isl_sample.h" #include "isl_sample_piplib.h" -#include "isl_vec.h" -#include "isl_mat.h" -#include "isl_seq.h" -#include "isl_map_private.h" +#include +#include +#include #include "isl_equalities.h" #include "isl_tab.h" #include "isl_basis_reduction.h" +#include +#include +#include static struct isl_vec *empty_sample(struct isl_basic_set *bset) { @@ -45,12 +58,16 @@ static struct isl_vec *interval_sample(struct isl_basic_set *bset) bset = isl_basic_set_simplify(bset); if (!bset) return NULL; - if (isl_basic_set_fast_is_empty(bset)) + if (isl_basic_set_plain_is_empty(bset)) return empty_sample(bset); if (bset->n_eq == 0 && bset->n_ineq == 0) return zero_sample(bset); sample = isl_vec_alloc(bset->ctx, 2); + if (!sample) + goto error; + if (!bset) + return NULL; isl_int_set_si(sample->block.data[0], 1); if (bset->n_eq > 0) { @@ -257,31 +274,234 @@ static struct isl_vec *sample_eq(struct isl_basic_set *bset, return sample; } -/* Given a basic set that is known to be bounded, find and return - * an integer point in the basic set, if there is any. +/* Return a matrix containing the equalities of the tableau + * in constraint form. The tableau is assumed to have + * an associated bset that has been kept up-to-date. + */ +static struct isl_mat *tab_equalities(struct isl_tab *tab) +{ + int i, j; + int n_eq; + struct isl_mat *eq; + struct isl_basic_set *bset; + + if (!tab) + return NULL; + + bset = isl_tab_peek_bset(tab); + isl_assert(tab->mat->ctx, bset, return NULL); + + n_eq = tab->n_var - tab->n_col + tab->n_dead; + if (tab->empty || n_eq == 0) + return isl_mat_alloc(tab->mat->ctx, 0, tab->n_var); + if (n_eq == tab->n_var) + return isl_mat_identity(tab->mat->ctx, tab->n_var); + + eq = isl_mat_alloc(tab->mat->ctx, n_eq, tab->n_var); + if (!eq) + return NULL; + for (i = 0, j = 0; i < tab->n_con; ++i) { + if (tab->con[i].is_row) + continue; + if (tab->con[i].index >= 0 && tab->con[i].index >= tab->n_dead) + continue; + if (i < bset->n_eq) + isl_seq_cpy(eq->row[j], bset->eq[i] + 1, tab->n_var); + else + isl_seq_cpy(eq->row[j], + bset->ineq[i - bset->n_eq] + 1, tab->n_var); + ++j; + } + isl_assert(bset->ctx, j == n_eq, goto error); + return eq; +error: + isl_mat_free(eq); + return NULL; +} + +/* Compute and return an initial basis for the bounded tableau "tab". * - * After handling some trivial cases, we perform a depth first search + * If the tableau is either full-dimensional or zero-dimensional, + * the we simply return an identity matrix. + * Otherwise, we construct a basis whose first directions correspond + * to equalities. + */ +static struct isl_mat *initial_basis(struct isl_tab *tab) +{ + int n_eq; + struct isl_mat *eq; + struct isl_mat *Q; + + tab->n_unbounded = 0; + tab->n_zero = n_eq = tab->n_var - tab->n_col + tab->n_dead; + if (tab->empty || n_eq == 0 || n_eq == tab->n_var) + return isl_mat_identity(tab->mat->ctx, 1 + tab->n_var); + + eq = tab_equalities(tab); + eq = isl_mat_left_hermite(eq, 0, NULL, &Q); + if (!eq) + return NULL; + isl_mat_free(eq); + + Q = isl_mat_lin_to_aff(Q); + return Q; +} + +/* Compute the minimum of the current ("level") basis row over "tab" + * and store the result in position "level" of "min". + */ +static enum isl_lp_result compute_min(isl_ctx *ctx, struct isl_tab *tab, + __isl_keep isl_vec *min, int level) +{ + return isl_tab_min(tab, tab->basis->row[1 + level], + ctx->one, &min->el[level], NULL, 0); +} + +/* Compute the maximum of the current ("level") basis row over "tab" + * and store the result in position "level" of "max". + */ +static enum isl_lp_result compute_max(isl_ctx *ctx, struct isl_tab *tab, + __isl_keep isl_vec *max, int level) +{ + enum isl_lp_result res; + unsigned dim = tab->n_var; + + isl_seq_neg(tab->basis->row[1 + level] + 1, + tab->basis->row[1 + level] + 1, dim); + res = isl_tab_min(tab, tab->basis->row[1 + level], + ctx->one, &max->el[level], NULL, 0); + isl_seq_neg(tab->basis->row[1 + level] + 1, + tab->basis->row[1 + level] + 1, dim); + isl_int_neg(max->el[level], max->el[level]); + + return res; +} + +/* Perform a greedy search for an integer point in the set represented + * by "tab", given that the minimal rational value (rounded up to the + * nearest integer) at "level" is smaller than the maximal rational + * value (rounded down to the nearest integer). + * + * Return 1 if we have found an integer point (if tab->n_unbounded > 0 + * then we may have only found integer values for the bounded dimensions + * and it is the responsibility of the caller to extend this solution + * to the unbounded dimensions). + * Return 0 if greedy search did not result in a solution. + * Return -1 if some error occurred. + * + * We assign a value half-way between the minimum and the maximum + * to the current dimension and check if the minimal value of the + * next dimension is still smaller than (or equal) to the maximal value. + * We continue this process until either + * - the minimal value (rounded up) is greater than the maximal value + * (rounded down). In this case, greedy search has failed. + * - we have exhausted all bounded dimensions, meaning that we have + * found a solution. + * - the sample value of the tableau is integral. + * - some error has occurred. + */ +static int greedy_search(isl_ctx *ctx, struct isl_tab *tab, + __isl_keep isl_vec *min, __isl_keep isl_vec *max, int level) +{ + struct isl_tab_undo *snap; + enum isl_lp_result res; + + snap = isl_tab_snap(tab); + + do { + isl_int_add(tab->basis->row[1 + level][0], + min->el[level], max->el[level]); + isl_int_fdiv_q_ui(tab->basis->row[1 + level][0], + tab->basis->row[1 + level][0], 2); + isl_int_neg(tab->basis->row[1 + level][0], + tab->basis->row[1 + level][0]); + if (isl_tab_add_valid_eq(tab, tab->basis->row[1 + level]) < 0) + return -1; + isl_int_set_si(tab->basis->row[1 + level][0], 0); + + if (++level >= tab->n_var - tab->n_unbounded) + return 1; + if (isl_tab_sample_is_integer(tab)) + return 1; + + res = compute_min(ctx, tab, min, level); + if (res == isl_lp_error) + return -1; + if (res != isl_lp_ok) + isl_die(ctx, isl_error_internal, + "expecting bounded rational solution", + return -1); + res = compute_max(ctx, tab, max, level); + if (res == isl_lp_error) + return -1; + if (res != isl_lp_ok) + isl_die(ctx, isl_error_internal, + "expecting bounded rational solution", + return -1); + } while (isl_int_le(min->el[level], max->el[level])); + + if (isl_tab_rollback(tab, snap) < 0) + return -1; + + return 0; +} + +/* Given a tableau representing a set, find and return + * an integer point in the set, if there is any. + * + * We perform a depth first search * for an integer point, by scanning all possible values in the range - * attained by a basis vector. + * attained by a basis vector, where an initial basis may have been set + * by the calling function. Otherwise an initial basis that exploits + * the equalities in the tableau is created. + * tab->n_zero is currently ignored and is clobbered by this function. + * + * The tableau is allowed to have unbounded direction, but then + * the calling function needs to set an initial basis, with the + * unbounded directions last and with tab->n_unbounded set + * to the number of unbounded directions. + * Furthermore, the calling functions needs to add shifted copies + * of all constraints involving unbounded directions to ensure + * that any feasible rational value in these directions can be rounded + * up to yield a feasible integer value. + * In particular, let B define the given basis x' = B x + * and let T be the inverse of B, i.e., X = T x'. + * Let a x + c >= 0 be a constraint of the set represented by the tableau, + * or a T x' + c >= 0 in terms of the given basis. Assume that + * the bounded directions have an integer value, then we can safely + * round up the values for the unbounded directions if we make sure + * that x' not only satisfies the original constraint, but also + * the constraint "a T x' + c + s >= 0" with s the sum of all + * negative values in the last n_unbounded entries of "a T". + * The calling function therefore needs to add the constraint + * a x + c + s >= 0. The current function then scans the first + * directions for an integer value and once those have been found, + * it can compute "T ceil(B x)" to yield an integer point in the set. + * Note that during the search, the first rows of B may be changed + * by a basis reduction, but the last n_unbounded rows of B remain + * unaltered and are also not mixed into the first rows. * * The search is implemented iteratively. "level" identifies the current * basis vector. "init" is true if we want the first value at the current * level and false if we want the next value. * + * At the start of each level, we first check if we can find a solution + * using greedy search. If not, we continue with the exhaustive search. + * * The initial basis is the identity matrix. If the range in some direction * contains more than one integer value, we perform basis reduction based - * on the value of ctx->gbr + * on the value of ctx->opt->gbr * - ISL_GBR_NEVER: never perform basis reduction * - ISL_GBR_ONCE: only perform basis reduction the first * time such a range is encountered * - ISL_GBR_ALWAYS: always perform basis reduction when * such a range is encountered * - * When ctx->gbr is set to ISL_GBR_ALWAYS, then we allow the basis + * When ctx->opt->gbr is set to ISL_GBR_ALWAYS, then we allow the basis * reduction computation to return early. That is, as soon as it * finds a reasonable first direction. */ -static struct isl_vec *sample_bounded(struct isl_basic_set *bset) +struct isl_vec *isl_tab_sample(struct isl_tab *tab) { unsigned dim; unsigned gbr; @@ -294,38 +514,42 @@ static struct isl_vec *sample_bounded(struct isl_basic_set *bset) int init; int reduced; struct isl_tab_undo **snap; - struct isl_tab *tab = NULL; - if (!bset) + if (!tab) return NULL; + if (tab->empty) + return isl_vec_alloc(tab->mat->ctx, 0); - if (isl_basic_set_fast_is_empty(bset)) - return empty_sample(bset); - - dim = isl_basic_set_total_dim(bset); - if (dim == 0) - return zero_sample(bset); - if (dim == 1) - return interval_sample(bset); - if (bset->n_eq > 0) - return sample_eq(bset, sample_bounded); + if (!tab->basis) + tab->basis = initial_basis(tab); + if (!tab->basis) + return NULL; + isl_assert(tab->mat->ctx, tab->basis->n_row == tab->n_var + 1, + return NULL); + isl_assert(tab->mat->ctx, tab->basis->n_col == tab->n_var + 1, + return NULL); - ctx = bset->ctx; - gbr = ctx->gbr; + ctx = tab->mat->ctx; + dim = tab->n_var; + gbr = ctx->opt->gbr; - min = isl_vec_alloc(bset->ctx, dim); - max = isl_vec_alloc(bset->ctx, dim); - snap = isl_alloc_array(bset->ctx, struct isl_tab_undo *, dim); + if (tab->n_unbounded == tab->n_var) { + sample = isl_tab_get_sample_value(tab); + sample = isl_mat_vec_product(isl_mat_copy(tab->basis), sample); + sample = isl_vec_ceil(sample); + sample = isl_mat_vec_inverse_product(isl_mat_copy(tab->basis), + sample); + return sample; + } - if (!min || !max || !snap) - goto error; + if (isl_tab_extend_cons(tab, dim + 1) < 0) + return NULL; - tab = isl_tab_from_basic_set(bset); - if (!tab) - goto error; + min = isl_vec_alloc(ctx, dim); + max = isl_vec_alloc(ctx, dim); + snap = isl_alloc_array(ctx, struct isl_tab_undo *, dim); - tab->basis = isl_mat_identity(bset->ctx, 1 + dim); - if (!tab->basis) + if (!min || !max || !snap) goto error; level = 0; @@ -333,40 +557,47 @@ static struct isl_vec *sample_bounded(struct isl_basic_set *bset) reduced = 0; while (level >= 0) { - int empty = 0; if (init) { - res = isl_tab_min(tab, tab->basis->row[1 + level], - bset->ctx->one, &min->el[level], NULL, 0); - if (res == isl_lp_empty) - empty = 1; - if (res == isl_lp_error || res == isl_lp_unbounded) + int choice; + + res = compute_min(ctx, tab, min, level); + if (res == isl_lp_error) goto error; - if (!empty && isl_tab_sample_is_integer(tab)) + if (res != isl_lp_ok) + isl_die(ctx, isl_error_internal, + "expecting bounded rational solution", + goto error); + if (isl_tab_sample_is_integer(tab)) break; - isl_seq_neg(tab->basis->row[1 + level] + 1, - tab->basis->row[1 + level] + 1, dim); - res = isl_tab_min(tab, tab->basis->row[1 + level], - bset->ctx->one, &max->el[level], NULL, 0); - isl_seq_neg(tab->basis->row[1 + level] + 1, - tab->basis->row[1 + level] + 1, dim); - isl_int_neg(max->el[level], max->el[level]); - if (res == isl_lp_empty) - empty = 1; - if (res == isl_lp_error || res == isl_lp_unbounded) + res = compute_max(ctx, tab, max, level); + if (res == isl_lp_error) goto error; - if (!empty && isl_tab_sample_is_integer(tab)) + if (res != isl_lp_ok) + isl_die(ctx, isl_error_internal, + "expecting bounded rational solution", + goto error); + if (isl_tab_sample_is_integer(tab)) break; - if (!empty && !reduced && ctx->gbr != ISL_GBR_NEVER && - isl_int_lt(min->el[level], max->el[level])) { + choice = isl_int_lt(min->el[level], max->el[level]); + if (choice) { + int g; + g = greedy_search(ctx, tab, min, max, level); + if (g < 0) + goto error; + if (g) + break; + } + if (!reduced && choice && + ctx->opt->gbr != ISL_GBR_NEVER) { unsigned gbr_only_first; - if (ctx->gbr == ISL_GBR_ONCE) - ctx->gbr = ISL_GBR_NEVER; + if (ctx->opt->gbr == ISL_GBR_ONCE) + ctx->opt->gbr = ISL_GBR_NEVER; tab->n_zero = level; - gbr_only_first = bset->ctx->gbr_only_first; - bset->ctx->gbr_only_first = - bset->ctx->gbr == ISL_GBR_ALWAYS; + gbr_only_first = ctx->opt->gbr_only_first; + ctx->opt->gbr_only_first = + ctx->opt->gbr == ISL_GBR_ALWAYS; tab = isl_tab_compute_reduced_basis(tab); - bset->ctx->gbr_only_first = gbr_only_first; + ctx->opt->gbr_only_first = gbr_only_first; if (!tab || !tab->basis) goto error; reduced = 1; @@ -377,43 +608,188 @@ static struct isl_vec *sample_bounded(struct isl_basic_set *bset) } else isl_int_add_ui(min->el[level], min->el[level], 1); - if (empty || isl_int_gt(min->el[level], max->el[level])) { + if (isl_int_gt(min->el[level], max->el[level])) { level--; init = 0; if (level >= 0) - isl_tab_rollback(tab, snap[level]); + if (isl_tab_rollback(tab, snap[level]) < 0) + goto error; continue; } isl_int_neg(tab->basis->row[1 + level][0], min->el[level]); - tab = isl_tab_add_valid_eq(tab, tab->basis->row[1 + level]); + if (isl_tab_add_valid_eq(tab, tab->basis->row[1 + level]) < 0) + goto error; isl_int_set_si(tab->basis->row[1 + level][0], 0); - if (level < dim - 1) { + if (level + tab->n_unbounded < dim - 1) { ++level; init = 1; continue; } break; } + if (level >= 0) { sample = isl_tab_get_sample_value(tab); - isl_vec_free(bset->sample); - bset->sample = isl_vec_copy(sample); - isl_basic_set_free(bset); + if (!sample) + goto error; + if (tab->n_unbounded && !isl_int_is_one(sample->el[0])) { + sample = isl_mat_vec_product(isl_mat_copy(tab->basis), + sample); + sample = isl_vec_ceil(sample); + sample = isl_mat_vec_inverse_product( + isl_mat_copy(tab->basis), sample); + } } else - sample = empty_sample(bset); + sample = isl_vec_alloc(ctx, 0); + ctx->opt->gbr = gbr; isl_vec_free(min); isl_vec_free(max); free(snap); - ctx->gbr = gbr; - isl_tab_free(tab); return sample; error: - ctx->gbr = gbr; - isl_basic_set_free(bset); + ctx->opt->gbr = gbr; isl_vec_free(min); isl_vec_free(max); free(snap); + return NULL; +} + +static struct isl_vec *sample_bounded(struct isl_basic_set *bset); + +/* Compute a sample point of the given basic set, based on the given, + * non-trivial factorization. + */ +static __isl_give isl_vec *factored_sample(__isl_take isl_basic_set *bset, + __isl_take isl_factorizer *f) +{ + int i, n; + isl_vec *sample = NULL; + isl_ctx *ctx; + unsigned nparam; + unsigned nvar; + + ctx = isl_basic_set_get_ctx(bset); + if (!ctx) + goto error; + + nparam = isl_basic_set_dim(bset, isl_dim_param); + nvar = isl_basic_set_dim(bset, isl_dim_set); + + sample = isl_vec_alloc(ctx, 1 + isl_basic_set_total_dim(bset)); + if (!sample) + goto error; + isl_int_set_si(sample->el[0], 1); + + bset = isl_morph_basic_set(isl_morph_copy(f->morph), bset); + + for (i = 0, n = 0; i < f->n_group; ++i) { + isl_basic_set *bset_i; + isl_vec *sample_i; + + bset_i = isl_basic_set_copy(bset); + bset_i = isl_basic_set_drop_constraints_involving(bset_i, + nparam + n + f->len[i], nvar - n - f->len[i]); + bset_i = isl_basic_set_drop_constraints_involving(bset_i, + nparam, n); + bset_i = isl_basic_set_drop(bset_i, isl_dim_set, + n + f->len[i], nvar - n - f->len[i]); + bset_i = isl_basic_set_drop(bset_i, isl_dim_set, 0, n); + + sample_i = sample_bounded(bset_i); + if (!sample_i) + goto error; + if (sample_i->size == 0) { + isl_basic_set_free(bset); + isl_factorizer_free(f); + isl_vec_free(sample); + return sample_i; + } + isl_seq_cpy(sample->el + 1 + nparam + n, + sample_i->el + 1, f->len[i]); + isl_vec_free(sample_i); + + n += f->len[i]; + } + + f->morph = isl_morph_inverse(f->morph); + sample = isl_morph_vec(isl_morph_copy(f->morph), sample); + + isl_basic_set_free(bset); + isl_factorizer_free(f); + return sample; +error: + isl_basic_set_free(bset); + isl_factorizer_free(f); + isl_vec_free(sample); + return NULL; +} + +/* Given a basic set that is known to be bounded, find and return + * an integer point in the basic set, if there is any. + * + * After handling some trivial cases, we construct a tableau + * and then use isl_tab_sample to find a sample, passing it + * the identity matrix as initial basis. + */ +static struct isl_vec *sample_bounded(struct isl_basic_set *bset) +{ + unsigned dim; + struct isl_ctx *ctx; + struct isl_vec *sample; + struct isl_tab *tab = NULL; + isl_factorizer *f; + + if (!bset) + return NULL; + + if (isl_basic_set_plain_is_empty(bset)) + return empty_sample(bset); + + dim = isl_basic_set_total_dim(bset); + if (dim == 0) + return zero_sample(bset); + if (dim == 1) + return interval_sample(bset); + if (bset->n_eq > 0) + return sample_eq(bset, sample_bounded); + + f = isl_basic_set_factorizer(bset); + if (!f) + goto error; + if (f->n_group != 0) + return factored_sample(bset, f); + isl_factorizer_free(f); + + ctx = bset->ctx; + + tab = isl_tab_from_basic_set(bset, 1); + if (tab && tab->empty) { + isl_tab_free(tab); + ISL_F_SET(bset, ISL_BASIC_SET_EMPTY); + sample = isl_vec_alloc(bset->ctx, 0); + isl_basic_set_free(bset); + return sample; + } + + if (!ISL_F_ISSET(bset, ISL_BASIC_SET_NO_IMPLICIT)) + if (isl_tab_detect_implicit_equalities(tab) < 0) + goto error; + + sample = isl_tab_sample(tab); + if (!sample) + goto error; + + if (sample->size > 0) { + isl_vec_free(bset->sample); + bset->sample = isl_vec_copy(sample); + } + + isl_basic_set_free(bset); + isl_tab_free(tab); + return sample; +error: + isl_basic_set_free(bset); isl_tab_free(tab); return NULL; } @@ -474,7 +850,7 @@ static struct isl_vec *rational_sample(struct isl_basic_set *bset) if (!bset) return NULL; - tab = isl_tab_from_basic_set(bset); + tab = isl_tab_from_basic_set(bset, 0); sample = isl_tab_get_sample_value(tab); isl_tab_free(tab); @@ -531,7 +907,7 @@ static struct isl_basic_set *shift_cone(struct isl_basic_set *cone, total = isl_basic_set_total_dim(cone); - shift = isl_basic_set_alloc_dim(isl_basic_set_get_dim(cone), + shift = isl_basic_set_alloc_space(isl_basic_set_get_space(cone), 0, 0, cone->n_ineq); for (i = 0; i < cone->n_ineq; ++i) { @@ -591,7 +967,8 @@ static struct isl_vec *round_up_in_cone(struct isl_vec *vec, total = isl_basic_set_total_dim(cone); cone = isl_basic_set_preimage(cone, U); - cone = isl_basic_set_remove_dims(cone, 0, total - (vec->size - 1)); + cone = isl_basic_set_remove_dims(cone, isl_dim_set, + 0, total - (vec->size - 1)); cone = shift_cone(cone, vec); @@ -636,28 +1013,6 @@ error: return NULL; } -/* Drop all constraints in bset that involve any of the dimensions - * first to first+n-1. - */ -static struct isl_basic_set *drop_constraints_involving - (struct isl_basic_set *bset, unsigned first, unsigned n) -{ - int i; - - if (!bset) - return NULL; - - bset = isl_basic_set_cow(bset); - - for (i = bset->n_ineq - 1; i >= 0; --i) { - if (isl_seq_first_non_zero(bset->ineq[i] + 1 + first, n) == -1) - continue; - isl_basic_set_drop_inequality(bset, i); - } - - return bset; -} - /* Give a basic set "bset" with recession cone "cone", compute and * return an integer point in bset, if any. * @@ -713,7 +1068,7 @@ __isl_give isl_vec *isl_basic_set_sample_with_cone( total = isl_basic_set_total_dim(cone); cone_dim = total - cone->n_eq; - M = isl_mat_sub_alloc(bset->ctx, cone->eq, 0, cone->n_eq, 1, total); + M = isl_mat_sub_alloc6(bset->ctx, cone->eq, 0, cone->n_eq, 1, total); M = isl_mat_left_hermite(M, 0, &U, NULL); if (!M) goto error; @@ -723,7 +1078,8 @@ __isl_give isl_vec *isl_basic_set_sample_with_cone( bset = isl_basic_set_preimage(bset, isl_mat_copy(U)); bounded = isl_basic_set_copy(bset); - bounded = drop_constraints_involving(bounded, total - cone_dim, cone_dim); + bounded = isl_basic_set_drop_constraints_involving(bounded, + total - cone_dim, cone_dim); bounded = isl_basic_set_drop_dims(bounded, total - cone_dim, cone_dim); sample = sample_bounded(bounded); if (!sample || sample->size == 0) { @@ -744,6 +1100,133 @@ error: return NULL; } +static void vec_sum_of_neg(struct isl_vec *v, isl_int *s) +{ + int i; + + isl_int_set_si(*s, 0); + + for (i = 0; i < v->size; ++i) + if (isl_int_is_neg(v->el[i])) + isl_int_add(*s, *s, v->el[i]); +} + +/* Given a tableau "tab", a tableau "tab_cone" that corresponds + * to the recession cone and the inverse of a new basis U = inv(B), + * with the unbounded directions in B last, + * add constraints to "tab" that ensure any rational value + * in the unbounded directions can be rounded up to an integer value. + * + * The new basis is given by x' = B x, i.e., x = U x'. + * For any rational value of the last tab->n_unbounded coordinates + * in the update tableau, the value that is obtained by rounding + * up this value should be contained in the original tableau. + * For any constraint "a x + c >= 0", we therefore need to add + * a constraint "a x + c + s >= 0", with s the sum of all negative + * entries in the last elements of "a U". + * + * Since we are not interested in the first entries of any of the "a U", + * we first drop the columns of U that correpond to bounded directions. + */ +static int tab_shift_cone(struct isl_tab *tab, + struct isl_tab *tab_cone, struct isl_mat *U) +{ + int i; + isl_int v; + struct isl_basic_set *bset = NULL; + + if (tab && tab->n_unbounded == 0) { + isl_mat_free(U); + return 0; + } + isl_int_init(v); + if (!tab || !tab_cone || !U) + goto error; + bset = isl_tab_peek_bset(tab_cone); + U = isl_mat_drop_cols(U, 0, tab->n_var - tab->n_unbounded); + for (i = 0; i < bset->n_ineq; ++i) { + int ok; + struct isl_vec *row = NULL; + if (isl_tab_is_equality(tab_cone, tab_cone->n_eq + i)) + continue; + row = isl_vec_alloc(bset->ctx, tab_cone->n_var); + if (!row) + goto error; + isl_seq_cpy(row->el, bset->ineq[i] + 1, tab_cone->n_var); + row = isl_vec_mat_product(row, isl_mat_copy(U)); + if (!row) + goto error; + vec_sum_of_neg(row, &v); + isl_vec_free(row); + if (isl_int_is_zero(v)) + continue; + tab = isl_tab_extend(tab, 1); + isl_int_add(bset->ineq[i][0], bset->ineq[i][0], v); + ok = isl_tab_add_ineq(tab, bset->ineq[i]) >= 0; + isl_int_sub(bset->ineq[i][0], bset->ineq[i][0], v); + if (!ok) + goto error; + } + + isl_mat_free(U); + isl_int_clear(v); + return 0; +error: + isl_mat_free(U); + isl_int_clear(v); + return -1; +} + +/* Compute and return an initial basis for the possibly + * unbounded tableau "tab". "tab_cone" is a tableau + * for the corresponding recession cone. + * Additionally, add constraints to "tab" that ensure + * that any rational value for the unbounded directions + * can be rounded up to an integer value. + * + * If the tableau is bounded, i.e., if the recession cone + * is zero-dimensional, then we just use inital_basis. + * Otherwise, we construct a basis whose first directions + * correspond to equalities, followed by bounded directions, + * i.e., equalities in the recession cone. + * The remaining directions are then unbounded. + */ +int isl_tab_set_initial_basis_with_cone(struct isl_tab *tab, + struct isl_tab *tab_cone) +{ + struct isl_mat *eq; + struct isl_mat *cone_eq; + struct isl_mat *U, *Q; + + if (!tab || !tab_cone) + return -1; + + if (tab_cone->n_col == tab_cone->n_dead) { + tab->basis = initial_basis(tab); + return tab->basis ? 0 : -1; + } + + eq = tab_equalities(tab); + if (!eq) + return -1; + tab->n_zero = eq->n_row; + cone_eq = tab_equalities(tab_cone); + eq = isl_mat_concat(eq, cone_eq); + if (!eq) + return -1; + tab->n_unbounded = tab->n_var - (eq->n_row - tab->n_zero); + eq = isl_mat_left_hermite(eq, 0, &U, &Q); + if (!eq) + return -1; + isl_mat_free(eq); + tab->basis = isl_mat_lin_to_aff(Q); + if (tab_shift_cone(tab, tab_cone, U) < 0) + return -1; + if (!tab->basis) + return -1; + return 0; +} + /* Compute and return a sample point in bset using generalized basis * reduction. We first check if the input set has a non-trivial * recession cone. If so, we perform some extra preprocessing in @@ -758,12 +1241,17 @@ static struct isl_vec *gbr_sample(struct isl_basic_set *bset) dim = isl_basic_set_total_dim(bset); cone = isl_basic_set_recession_cone(isl_basic_set_copy(bset)); + if (!cone) + goto error; if (cone->n_eq < dim) return isl_basic_set_sample_with_cone(bset, cone); isl_basic_set_free(cone); return sample_bounded(bset); +error: + isl_basic_set_free(bset); + return NULL; } static struct isl_vec *pip_sample(struct isl_basic_set *bset) @@ -795,7 +1283,7 @@ static struct isl_vec *basic_set_sample(struct isl_basic_set *bset, int bounded) return NULL; ctx = bset->ctx; - if (isl_basic_set_fast_is_empty(bset)) + if (isl_basic_set_plain_is_empty(bset)) return empty_sample(bset); dim = isl_basic_set_n_dim(bset); @@ -823,7 +1311,7 @@ static struct isl_vec *basic_set_sample(struct isl_basic_set *bset, int bounded) if (dim == 1) return interval_sample(bset); - switch (bset->ctx->ilp_solver) { + switch (bset->ctx->opt->ilp_solver) { case ISL_ILP_PIP: return pip_sample(bset); case ISL_ILP_GBR: @@ -873,7 +1361,7 @@ __isl_give isl_basic_set *isl_basic_set_from_vec(__isl_take isl_vec *vec) isl_int_neg(bset->eq[k][0], vec->el[1 + i]); isl_int_set(bset->eq[k][1 + i], vec->el[0]); } - isl_vec_free(vec); + bset->sample = vec; return bset; error: @@ -905,6 +1393,11 @@ error: return NULL; } +__isl_give isl_basic_set *isl_basic_set_sample(__isl_take isl_basic_set *bset) +{ + return isl_basic_map_sample(bset); +} + __isl_give isl_basic_map *isl_map_sample(__isl_take isl_map *map) { int i; @@ -934,3 +1427,41 @@ __isl_give isl_basic_set *isl_set_sample(__isl_take isl_set *set) { return (isl_basic_set *) isl_map_sample((isl_map *)set); } + +__isl_give isl_point *isl_basic_set_sample_point(__isl_take isl_basic_set *bset) +{ + isl_vec *vec; + isl_space *dim; + + dim = isl_basic_set_get_space(bset); + bset = isl_basic_set_underlying_set(bset); + vec = isl_basic_set_sample_vec(bset); + + return isl_point_alloc(dim, vec); +} + +__isl_give isl_point *isl_set_sample_point(__isl_take isl_set *set) +{ + int i; + isl_point *pnt; + + if (!set) + return NULL; + + for (i = 0; i < set->n; ++i) { + pnt = isl_basic_set_sample_point(isl_basic_set_copy(set->p[i])); + if (!pnt) + goto error; + if (!isl_point_is_void(pnt)) + break; + isl_point_free(pnt); + } + if (i == set->n) + pnt = isl_point_void(isl_set_get_space(set)); + + isl_set_free(set); + return pnt; +error: + isl_set_free(set); + return NULL; +}