X-Git-Url: http://review.tizen.org/git/?a=blobdiff_plain;f=isl_sample.c;h=c6a0f314425b0bc2d4683589997a3034b652abe0;hb=de51a9bc4da5dd3f1f9f57c2362da6f9752c44e0;hp=d19d585b2933a1bee38d0eaa8842b327f872dc35;hpb=7eb3527926a43d4163e68936adbb2db20af2b251;p=platform%2Fupstream%2Fisl.git diff --git a/isl_sample.c b/isl_sample.c index d19d585..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,179 +274,476 @@ static struct isl_vec *sample_eq(struct isl_basic_set *bset, return sample; } -/* Given a basic set "bset" and an affine function "f"/"denom", - * check if bset is bounded and non-empty and if so, return the minimal - * and maximal value attained by the affine function in "min" and "max". - * The minimal value is rounded up to the nearest integer, while the - * maximal value is rounded down. - * The return value indicates whether the set was empty or unbounded. - * - * If we happen to find an integer point while looking for the minimal - * or maximal value, then we record that value in "bset" and return early. +/* 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 enum isl_lp_result basic_set_range(struct isl_basic_set *bset, - isl_int *f, isl_int denom, isl_int *min, isl_int *max) +static struct isl_mat *tab_equalities(struct isl_tab *tab) { - unsigned dim; - struct isl_tab *tab; - enum isl_lp_result res; + int i, j; + int n_eq; + struct isl_mat *eq; + struct isl_basic_set *bset; - if (!bset) - return isl_lp_error; - if (isl_basic_set_fast_is_empty(bset)) - return isl_lp_empty; + if (!tab) + return NULL; - tab = isl_tab_from_basic_set(bset); - res = isl_tab_min(tab, f, denom, min, NULL, 0); - if (res != isl_lp_ok) - goto done; + bset = isl_tab_peek_bset(tab); + isl_assert(tab->mat->ctx, bset, return NULL); - if (isl_tab_sample_is_integer(tab)) { - isl_vec_free(bset->sample); - bset->sample = isl_tab_get_sample_value(tab); - if (!bset->sample) - goto error; - isl_int_set(*max, *min); - goto done; + 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; +} - dim = isl_basic_set_total_dim(bset); - isl_seq_neg(f, f, 1 + dim); - res = isl_tab_min(tab, f, denom, max, NULL, 0); - isl_seq_neg(f, f, 1 + dim); - isl_int_neg(*max, *max); +/* Compute and return an initial basis for the bounded tableau "tab". + * + * 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); - if (isl_tab_sample_is_integer(tab)) { - isl_vec_free(bset->sample); - bset->sample = isl_tab_get_sample_value(tab); - if (!bset->sample) - goto error; - } + 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]); -done: - isl_tab_free(tab); return res; -error: - isl_tab_free(tab); - return isl_lp_error; } -/* Perform a basis reduction on "bset" and return the inverse of - * the new basis, i.e., an affine mapping from the new coordinates to the old, - * in *T. +/* 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 struct isl_basic_set *basic_set_reduced(struct isl_basic_set *bset, - struct isl_mat **T) +static int greedy_search(isl_ctx *ctx, struct isl_tab *tab, + __isl_keep isl_vec *min, __isl_keep isl_vec *max, int level) { - unsigned gbr_only_first; + struct isl_tab_undo *snap; + enum isl_lp_result res; - *T = NULL; - if (!bset) + 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, 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->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->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. + */ +struct isl_vec *isl_tab_sample(struct isl_tab *tab) +{ + unsigned dim; + unsigned gbr; + struct isl_ctx *ctx; + struct isl_vec *sample; + struct isl_vec *min; + struct isl_vec *max; + enum isl_lp_result res; + int level; + int init; + int reduced; + struct isl_tab_undo **snap; + + if (!tab) return NULL; + if (tab->empty) + return isl_vec_alloc(tab->mat->ctx, 0); + + 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 = tab->mat->ctx; + dim = tab->n_var; + gbr = ctx->opt->gbr; + + 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; + } - gbr_only_first = bset->ctx->gbr_only_first; - bset->ctx->gbr_only_first = bset->ctx->gbr == ISL_GBR_ONCE; - *T = isl_basic_set_reduced_basis(bset); - bset->ctx->gbr_only_first = gbr_only_first; + if (isl_tab_extend_cons(tab, dim + 1) < 0) + return NULL; - *T = isl_mat_lin_to_aff(*T); - *T = isl_mat_right_inverse(*T); + min = isl_vec_alloc(ctx, dim); + max = isl_vec_alloc(ctx, dim); + snap = isl_alloc_array(ctx, struct isl_tab_undo *, dim); - bset = isl_basic_set_preimage(bset, isl_mat_copy(*T)); - if (!bset) + if (!min || !max || !snap) goto error; - return bset; + level = 0; + init = 1; + reduced = 0; + + while (level >= 0) { + if (init) { + int choice; + + res = compute_min(ctx, tab, min, level); + if (res == isl_lp_error) + goto error; + 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; + res = compute_max(ctx, tab, max, level); + if (res == isl_lp_error) + goto error; + 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; + 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->opt->gbr == ISL_GBR_ONCE) + ctx->opt->gbr = ISL_GBR_NEVER; + tab->n_zero = level; + 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); + ctx->opt->gbr_only_first = gbr_only_first; + if (!tab || !tab->basis) + goto error; + reduced = 1; + continue; + } + reduced = 0; + snap[level] = isl_tab_snap(tab); + } else + isl_int_add_ui(min->el[level], min->el[level], 1); + + if (isl_int_gt(min->el[level], max->el[level])) { + level--; + init = 0; + if (level >= 0) + if (isl_tab_rollback(tab, snap[level]) < 0) + goto error; + continue; + } + isl_int_neg(tab->basis->row[1 + level][0], min->el[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 + tab->n_unbounded < dim - 1) { + ++level; + init = 1; + continue; + } + break; + } + + if (level >= 0) { + sample = isl_tab_get_sample_value(tab); + 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 = isl_vec_alloc(ctx, 0); + + ctx->opt->gbr = gbr; + isl_vec_free(min); + isl_vec_free(max); + free(snap); + return sample; error: - isl_mat_free(*T); - *T = NULL; + 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); -/* Given a basic set "bset" whose first coordinate ranges between - * "min" and "max", step through all values from min to max, until - * the slice of bset with the first coordinate fixed to one of these - * values contains an integer point. If such a point is found, return it. - * If none of the slices contains any integer point, then bset itself - * doesn't contain any integer point and an empty sample is returned. +/* Compute a sample point of the given basic set, based on the given, + * non-trivial factorization. */ -static struct isl_vec *sample_scan(struct isl_basic_set *bset, - isl_int min, isl_int max) +static __isl_give isl_vec *factored_sample(__isl_take isl_basic_set *bset, + __isl_take isl_factorizer *f) { - unsigned total; - struct isl_basic_set *slice = NULL; - struct isl_vec *sample = NULL; - isl_int tmp; + 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; - total = isl_basic_set_total_dim(bset); + nparam = isl_basic_set_dim(bset, isl_dim_param); + nvar = isl_basic_set_dim(bset, isl_dim_set); - isl_int_init(tmp); - for (isl_int_set(tmp, min); isl_int_le(tmp, max); - isl_int_add_ui(tmp, tmp, 1)) { - int k; + sample = isl_vec_alloc(ctx, 1 + isl_basic_set_total_dim(bset)); + if (!sample) + goto error; + isl_int_set_si(sample->el[0], 1); - slice = isl_basic_set_copy(bset); - slice = isl_basic_set_cow(slice); - slice = isl_basic_set_extend_constraints(slice, 1, 0); - k = isl_basic_set_alloc_equality(slice); - if (k < 0) - goto error; - isl_int_set(slice->eq[k][0], tmp); - isl_int_set_si(slice->eq[k][1], -1); - isl_seq_clr(slice->eq[k] + 2, total - 1); - slice = isl_basic_set_simplify(slice); - sample = sample_bounded(slice); - slice = NULL; - if (!sample) + 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->size > 0) - break; - isl_vec_free(sample); - sample = NULL; + 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]; } - if (!sample) - sample = empty_sample(bset); - else - isl_basic_set_free(bset); - isl_int_clear(tmp); + + 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_basic_set_free(slice); - isl_int_clear(tmp); + 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 check the range of the - * first coordinate. If this coordinate can only attain one integer - * value, we are happy. Otherwise, we perform basis reduction and - * determine the new range. - * - * Then we step through all possible values in the range in sample_scan. - * - * If any basis reduction was performed, the sample value found, if any, - * is transformed back to the original space. + * 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; - unsigned gbr; struct isl_ctx *ctx; struct isl_vec *sample; - struct isl_vec *obj = NULL; - struct isl_mat *T = NULL; - isl_int min, max; - enum isl_lp_result res; + struct isl_tab *tab = NULL; + isl_factorizer *f; if (!bset) return NULL; - if (isl_basic_set_fast_is_empty(bset)) + if (isl_basic_set_plain_is_empty(bset)) return empty_sample(bset); dim = isl_basic_set_total_dim(bset); @@ -440,74 +754,43 @@ static struct isl_vec *sample_bounded(struct isl_basic_set *bset) if (bset->n_eq > 0) return sample_eq(bset, sample_bounded); - ctx = bset->ctx; - gbr = ctx->gbr; - - isl_int_init(min); - isl_int_init(max); - obj = isl_vec_alloc(bset->ctx, 1 + dim); - if (!obj) + f = isl_basic_set_factorizer(bset); + if (!f) goto error; - isl_seq_clr(obj->el, 1+ dim); - isl_int_set_si(obj->el[1], 1); + if (f->n_group != 0) + return factored_sample(bset, f); + isl_factorizer_free(f); + + ctx = bset->ctx; - res = basic_set_range(bset, obj->el, bset->ctx->one, &min, &max); - if (res == isl_lp_error) - goto error; - isl_assert(bset->ctx, res != isl_lp_unbounded, goto error); - if (bset->sample) { - sample = isl_vec_copy(bset->sample); + 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); - goto out; - } - if (res == isl_lp_empty || isl_int_lt(max, min)) { - sample = empty_sample(bset); - goto out; + return sample; } - if (ctx->gbr != ISL_GBR_NEVER && isl_int_ne(min, max)) { - if (ctx->gbr == ISL_GBR_ONCE) - ctx->gbr = ISL_GBR_NEVER; - - bset = basic_set_reduced(bset, &T); - if (!bset) + if (!ISL_F_ISSET(bset, ISL_BASIC_SET_NO_IMPLICIT)) + if (isl_tab_detect_implicit_equalities(tab) < 0) goto error; - res = basic_set_range(bset, obj->el, bset->ctx->one, &min, &max); - if (res == isl_lp_error) - goto error; - isl_assert(bset->ctx, res != isl_lp_unbounded, goto error); - if (bset->sample) { - sample = isl_vec_copy(bset->sample); - isl_basic_set_free(bset); - goto out; - } - if (res == isl_lp_empty || isl_int_lt(max, min)) { - sample = empty_sample(bset); - goto out; - } - } + sample = isl_tab_sample(tab); + if (!sample) + goto error; - sample = sample_scan(bset, min, max); -out: - if (T) { - if (!sample || sample->size == 0) - isl_mat_free(T); - else - sample = isl_mat_vec_product(T, sample); + if (sample->size > 0) { + isl_vec_free(bset->sample); + bset->sample = isl_vec_copy(sample); } - isl_vec_free(obj); - isl_int_clear(min); - isl_int_clear(max); - ctx->gbr = gbr; + + isl_basic_set_free(bset); + isl_tab_free(tab); return sample; error: - ctx->gbr = gbr; - isl_mat_free(T); isl_basic_set_free(bset); - isl_vec_free(obj); - isl_int_clear(min); - isl_int_clear(max); + isl_tab_free(tab); return NULL; } @@ -567,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); @@ -624,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) { @@ -684,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); @@ -729,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. * @@ -788,8 +1050,8 @@ static struct isl_basic_set *drop_constraints_involving * then combined into a single sample point and transformed back * to the original space. */ -static struct isl_vec *sample_with_cone(struct isl_basic_set *bset, - struct isl_basic_set *cone) +__isl_give isl_vec *isl_basic_set_sample_with_cone( + __isl_take isl_basic_set *bset, __isl_take isl_basic_set *cone) { unsigned total; unsigned cone_dim; @@ -806,7 +1068,7 @@ static struct isl_vec *sample_with_cone(struct isl_basic_set *bset, 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; @@ -816,7 +1078,8 @@ static struct isl_vec *sample_with_cone(struct isl_basic_set *bset, 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) { @@ -837,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 @@ -851,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 sample_with_cone(bset, cone); + 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) @@ -888,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); @@ -909,13 +1304,14 @@ static struct isl_vec *basic_set_sample(struct isl_basic_set *bset, int bounded) bset->sample = NULL; if (bset->n_eq > 0) - return sample_eq(bset, isl_basic_set_sample_vec); + return sample_eq(bset, bounded ? isl_basic_set_sample_bounded + : isl_basic_set_sample_vec); if (dim == 0) return zero_sample(bset); 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: @@ -965,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: @@ -997,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; @@ -1026,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; +}