From 14578ca228e38f9d45688cbf2c14bc855500f9a8 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Fri, 22 Aug 2008 16:31:44 +0200 Subject: [PATCH] sample: remove lineality and skew into positive orthant These changes are needed if we want isl_basic_set_sample to always return an actual point. Without them, the lexmin may be unbounded and we effectively get a ray. --- isl_convex_hull.c | 6 +- isl_equalities.c | 2 +- isl_mat.c | 25 +++++---- isl_mat.h | 6 +- isl_sample.c | 97 ++++++++++++++++++++++++++++++++ isl_sample_piplib.c | 159 +++++++++++++++++++++++++++++++++++++++++++++++----- 6 files changed, 264 insertions(+), 31 deletions(-) diff --git a/isl_convex_hull.c b/isl_convex_hull.c index b140b47..8c7ea3f 100644 --- a/isl_convex_hull.c +++ b/isl_convex_hull.c @@ -610,10 +610,10 @@ static struct isl_basic_set *compute_facet(struct isl_ctx *ctx, isl_int_set_si(m->row[0][0], 1); isl_seq_clr(m->row[0]+1, set->dim); isl_seq_cpy(m->row[1], c, 1+set->dim); - m = isl_mat_left_hermite(ctx, m, &U, &Q); + m = isl_mat_left_hermite(ctx, m, 0, &U, &Q); if (!m) goto error; - U = isl_mat_drop_col(ctx, U, 1); + U = isl_mat_drop_cols(ctx, U, 1, 1); Q = isl_mat_drop_rows(ctx, Q, 1, 1); set = isl_set_preimage(ctx, set, U); facet = uset_convex_hull(ctx, set); @@ -857,7 +857,7 @@ static struct isl_basic_set *modulo_lineality(struct isl_ctx *ctx, old_dim = set->dim; new_dim = bounds->n_row; H = isl_mat_sub_alloc(ctx, bounds->row, 0, bounds->n_row, 1, set->dim); - H = isl_mat_left_hermite(ctx, H, &U, &Q); + H = isl_mat_left_hermite(ctx, H, 0, &U, &Q); if (!H) goto error; U = isl_mat_lin_to_aff(ctx, U); diff --git a/isl_equalities.c b/isl_equalities.c index 408d2dd..a4aeac4 100644 --- a/isl_equalities.c +++ b/isl_equalities.c @@ -60,7 +60,7 @@ static struct isl_basic_set *compress_variables(struct isl_ctx *ctx, return bset; H = isl_mat_sub_alloc(ctx, bset->eq, 0, bset->n_eq, 1, bset->dim); - H = isl_mat_left_hermite(ctx, H, &U, T2); + H = isl_mat_left_hermite(ctx, H, 0, &U, T2); if (!H || !U || (T2 && !*T2)) goto error; if (T2) { diff --git a/isl_mat.c b/isl_mat.c index 9b4558c..4b3b20a 100644 --- a/isl_mat.c +++ b/isl_mat.c @@ -275,11 +275,13 @@ static void oppose(struct isl_ctx *ctx, struct isl_mat *M, struct isl_mat **U, * * with U and Q unimodular matrices and H a matrix in column echelon form * such that on each echelon row the entries in the non-echelon column - * are non-negative and stricly smaller than the entries in the echelon - * column. If U or Q are NULL, then these matrices are not computed. + * are non-negative (if neg == 0) or non-positive (if neg == 1) + * and stricly smaller (in absolute value) than the entries in the echelon + * column. + * If U or Q are NULL, then these matrices are not computed. */ struct isl_mat *isl_mat_left_hermite(struct isl_ctx *ctx, - struct isl_mat *M, struct isl_mat **U, struct isl_mat **Q) + struct isl_mat *M, int neg, struct isl_mat **U, struct isl_mat **Q) { isl_int c; int row, col; @@ -330,7 +332,10 @@ struct isl_mat *isl_mat_left_hermite(struct isl_ctx *ctx, for (i = 0; i < col; ++i) { if (isl_int_is_zero(M->row[row][i])) continue; - isl_int_fdiv_q(c, M->row[row][i], M->row[row][col]); + if (neg) + isl_int_cdiv_q(c, M->row[row][i], M->row[row][col]); + else + isl_int_fdiv_q(c, M->row[row][i], M->row[row][col]); if (isl_int_is_zero(c)) continue; subtract(ctx, M, U, Q, row, col, i, c); @@ -780,20 +785,20 @@ void isl_mat_dump(struct isl_ctx *ctx, struct isl_mat *mat, } } -struct isl_mat *isl_mat_drop_col(struct isl_ctx *ctx, struct isl_mat *mat, - unsigned col) +struct isl_mat *isl_mat_drop_cols(struct isl_ctx *ctx, struct isl_mat *mat, + unsigned col, unsigned n) { int r; if (!mat) return NULL; - if (col != mat->n_col-1) { + if (col != mat->n_col-n) { for (r = 0; r < mat->n_row; ++r) - isl_seq_cpy(mat->row[r]+col, mat->row[r]+col+1, - mat->n_col - col - 1); + isl_seq_cpy(mat->row[r]+col, mat->row[r]+col+n, + mat->n_col - col - n); } - mat->n_col--; + mat->n_col -= n; return mat; } diff --git a/isl_mat.h b/isl_mat.h index dc17fd2..ba8ac07 100644 --- a/isl_mat.h +++ b/isl_mat.h @@ -49,7 +49,7 @@ struct isl_vec *isl_mat_vec_product(struct isl_ctx *ctx, struct isl_mat *isl_mat_aff_direct_sum(struct isl_ctx *ctx, struct isl_mat *left, struct isl_mat *right); struct isl_mat *isl_mat_left_hermite(struct isl_ctx *ctx, - struct isl_mat *M, struct isl_mat **U, struct isl_mat **Q); + struct isl_mat *M, int neg, struct isl_mat **U, struct isl_mat **Q); struct isl_mat *isl_mat_lin_to_aff(struct isl_ctx *ctx, struct isl_mat *mat); struct isl_mat *isl_mat_inverse_product(struct isl_ctx *ctx, struct isl_mat *left, struct isl_mat *right); @@ -58,8 +58,8 @@ struct isl_mat *isl_mat_product(struct isl_ctx *ctx, struct isl_mat *isl_mat_right_inverse(struct isl_ctx *ctx, struct isl_mat *mat); -struct isl_mat *isl_mat_drop_col(struct isl_ctx *ctx, struct isl_mat *mat, - unsigned col); +struct isl_mat *isl_mat_drop_cols(struct isl_ctx *ctx, struct isl_mat *mat, + unsigned col, unsigned n); struct isl_mat *isl_mat_drop_rows(struct isl_ctx *ctx, struct isl_mat *mat, unsigned row, unsigned n); diff --git a/isl_sample.c b/isl_sample.c index 75514d2..35f08f6 100644 --- a/isl_sample.c +++ b/isl_sample.c @@ -55,9 +55,89 @@ static struct isl_vec *interval_sample(struct isl_ctx *ctx, return sample; } +static struct isl_mat *independent_bounds(struct isl_ctx *ctx, + struct isl_basic_set *bset) +{ + int i, j, n; + struct isl_mat *dirs = NULL; + + if (!bset) + return NULL; + + if (bset->n_ineq == 0) + return isl_mat_alloc(ctx, 0, bset->dim); + + dirs = isl_mat_alloc(ctx, bset->dim, bset->dim); + if (!dirs) + return NULL; + isl_seq_cpy(dirs->row[0], bset->ineq[0]+1, dirs->n_col); + for (j = 1, n = 1; n < bset->dim && j < bset->n_ineq; ++j) { + int pos; + + isl_seq_cpy(dirs->row[n], bset->ineq[j]+1, dirs->n_col); + + pos = isl_seq_first_non_zero(dirs->row[n], dirs->n_col); + if (pos < 0) + continue; + for (i = 0; i < n; ++i) { + int pos_i; + pos_i = isl_seq_first_non_zero(dirs->row[i], dirs->n_col); + if (pos_i < pos) + continue; + if (pos_i > pos) + break; + isl_seq_elim(dirs->row[n], dirs->row[i], pos, + dirs->n_col, NULL); + pos = isl_seq_first_non_zero(dirs->row[n], dirs->n_col); + if (pos < 0) + break; + } + if (pos < 0) + continue; + if (i < n) { + int k; + isl_int *t = dirs->row[n]; + for (k = n; k > i; --k) + dirs->row[k] = dirs->row[k-1]; + dirs->row[i] = t; + } + ++n; + } + dirs->n_row = n; + return dirs; +} + +static struct isl_basic_set *remove_lineality(struct isl_ctx *ctx, + struct isl_basic_set *bset, struct isl_mat *bounds, struct isl_mat **T) +{ + struct isl_mat *U = NULL; + unsigned old_dim, new_dim; + + old_dim = bset->dim; + new_dim = bounds->n_row; + *T = NULL; + bounds = isl_mat_left_hermite(ctx, bounds, 0, &U, NULL); + if (!bounds) + goto error; + U = isl_mat_lin_to_aff(ctx, U); + U = isl_mat_drop_cols(ctx, U, 1 + new_dim, old_dim - new_dim); + bset = isl_basic_set_preimage(ctx, bset, isl_mat_copy(ctx, U)); + if (!bset) + goto error; + *T = U; + isl_mat_free(ctx, bounds); + return bset; +error: + isl_mat_free(ctx, bounds); + isl_mat_free(ctx, U); + isl_basic_set_free(ctx, bset); + return NULL; +} + struct isl_vec *isl_basic_set_sample(struct isl_ctx *ctx, struct isl_basic_set *bset) { + struct isl_mat *bounds; if (!bset) return NULL; @@ -85,6 +165,23 @@ struct isl_vec *isl_basic_set_sample(struct isl_ctx *ctx, return point_sample(ctx, bset); if (bset->dim == 1) return interval_sample(ctx, bset); + bounds = independent_bounds(ctx, bset); + if (!bounds) + goto error; + if (bounds->n_row == bset->dim) + isl_mat_free(ctx, bounds); + else { + struct isl_mat *T; + struct isl_vec *sample; + + bset = remove_lineality(ctx, bset, bounds, &T); + sample = isl_basic_set_sample(ctx, bset); + if (sample && sample->size != 0) + sample = isl_mat_vec_product(ctx, T, sample); + else + isl_mat_free(ctx, T); + return sample; + } return isl_pip_basic_set_sample(ctx, bset); error: isl_basic_set_free(ctx, bset); diff --git a/isl_sample_piplib.c b/isl_sample_piplib.c index 19aa601..b0bf2cf 100644 --- a/isl_sample_piplib.c +++ b/isl_sample_piplib.c @@ -1,35 +1,166 @@ +#include "isl_mat.h" #include "isl_vec.h" #include "isl_piplib.h" #include "isl_sample_piplib.h" +static void swap_inequality(struct isl_basic_set *bset, int a, int b) +{ + isl_int *t = bset->ineq[a]; + bset->ineq[a] = bset->ineq[b]; + bset->ineq[b] = t; +} + +static struct isl_mat *independent_bounds(struct isl_ctx *ctx, + struct isl_basic_set *bset) +{ + int i, j, n; + struct isl_mat *dirs = NULL; + struct isl_mat *bounds = NULL; + + if (!bset) + return NULL; + + bounds = isl_mat_alloc(ctx, 1+bset->dim, 1+bset->dim); + if (!bounds) + return NULL; + + isl_int_set_si(bounds->row[0][0], 1); + isl_seq_clr(bounds->row[0]+1, bset->dim); + bounds->n_row = 1; + + if (bset->n_ineq == 0) + return bounds; + + dirs = isl_mat_alloc(ctx, bset->dim, bset->dim); + if (!dirs) { + isl_mat_free(ctx, bounds); + return NULL; + } + isl_seq_cpy(dirs->row[0], bset->ineq[0]+1, dirs->n_col); + isl_seq_cpy(bounds->row[1], bset->ineq[0], bounds->n_col); + for (j = 1, n = 1; n < bset->dim && j < bset->n_ineq; ++j) { + int pos; + + isl_seq_cpy(dirs->row[n], bset->ineq[j]+1, dirs->n_col); + + pos = isl_seq_first_non_zero(dirs->row[n], dirs->n_col); + if (pos < 0) + continue; + for (i = 0; i < n; ++i) { + int pos_i; + pos_i = isl_seq_first_non_zero(dirs->row[i], dirs->n_col); + if (pos_i < pos) + continue; + if (pos_i > pos) + break; + isl_seq_elim(dirs->row[n], dirs->row[i], pos, + dirs->n_col, NULL); + pos = isl_seq_first_non_zero(dirs->row[n], dirs->n_col); + if (pos < 0) + break; + } + if (pos < 0) + continue; + if (i < n) { + int k; + isl_int *t = dirs->row[n]; + for (k = n; k > i; --k) + dirs->row[k] = dirs->row[k-1]; + dirs->row[i] = t; + } + ++n; + isl_seq_cpy(bounds->row[n], bset->ineq[j], bounds->n_col); + } + isl_mat_free(ctx, dirs); + bounds->n_row = 1+n; + return bounds; +} + +/* Skew into positive orthant and project out lineality space */ +static struct isl_basic_set *isl_basic_set_skew_to_positive_orthant( + struct isl_ctx *ctx, struct isl_basic_set *bset, + struct isl_mat **T) +{ + struct isl_mat *U = NULL; + struct isl_mat *bounds = NULL; + int i, j; + unsigned old_dim, new_dim; + + *T = NULL; + if (!bset) + return NULL; + + isl_assert(ctx, bset->nparam == 0, goto error); + isl_assert(ctx, bset->n_div == 0, goto error); + isl_assert(ctx, bset->n_eq == 0, goto error); + + /* Try to move (multiples of) unit rows up. */ + for (i = 0, j = 0; i < bset->n_ineq; ++i) { + int pos = isl_seq_first_non_zero(bset->ineq[i]+1, + bset->dim); + if (pos < 0) + continue; + if (isl_seq_first_non_zero(bset->ineq[i]+1+pos+1, + bset->dim-pos-1) >= 0) + continue; + if (i != j) + swap_inequality(bset, i, j); + ++j; + } + bounds = independent_bounds(ctx, bset); + if (!bounds) + goto error; + old_dim = bset->dim; + new_dim = bounds->n_row - 1; + bounds = isl_mat_left_hermite(ctx, bounds, 1, &U, NULL); + if (!bounds) + goto error; + U = isl_mat_drop_cols(ctx, U, 1 + new_dim, old_dim - new_dim); + bset = isl_basic_set_preimage(ctx, bset, isl_mat_copy(ctx, U)); + if (!bset) + goto error; + *T = U; + isl_mat_free(ctx, bounds); + return bset; +error: + isl_mat_free(ctx, bounds); + isl_mat_free(ctx, U); + isl_basic_set_free(ctx, bset); + return NULL; +} + struct isl_vec *isl_pip_basic_set_sample(struct isl_ctx *ctx, struct isl_basic_set *bset) { PipOptions *options = NULL; PipMatrix *domain = NULL; PipQuast *sol = NULL; - struct isl_basic_map *bmap = (struct isl_basic_map *)bset; struct isl_vec *vec = NULL; unsigned dim; + struct isl_mat *T; - if (!bmap) + if (!bset) + goto error; + isl_assert(ctx, bset->nparam == 0, goto error); + isl_assert(ctx, bset->n_div == 0, goto error); + bset = isl_basic_set_skew_to_positive_orthant(ctx, bset, &T); + if (!bset) goto error; - dim = bmap->nparam + bmap->n_in + bmap->n_out; - domain = isl_basic_map_to_pip(bmap, 0, 0, 0); + dim = bset->dim; + domain = isl_basic_map_to_pip((struct isl_basic_map *)bset, 0, 0, 0); if (!domain) goto error; options = pip_options_init(); if (!options) goto error; - options->Simplify = 1; - options->Urs_unknowns = -1; sol = pip_solve(domain, NULL, -1, options); if (!sol) goto error; - if (!sol->list) + if (!sol->list) { vec = isl_vec_alloc(ctx, 0); - else { + isl_mat_free(ctx, T); + } else { PipList *l; int i; vec = isl_vec_alloc(ctx, 1 + dim); @@ -39,22 +170,22 @@ struct isl_vec *isl_pip_basic_set_sample(struct isl_ctx *ctx, for (i = 0, l = sol->list; l && i < dim; ++i, l = l->next) { isl_seq_cpy_from_pip(&vec->block.data[1+i], &l->vector->the_vector[0], 1); - if (entier_zero_p(l->vector->the_deno[0])) - isl_int_set_si(vec->block.data[0], 0); + isl_assert(ctx, !entier_zero_p(l->vector->the_deno[0]), + goto error); } - if (i != dim) - goto error; + isl_assert(ctx, i == dim, goto error); + vec = isl_mat_vec_product(ctx, T, vec); } pip_quast_free(sol); pip_options_free(options); pip_matrix_free(domain); - isl_basic_map_free(ctx, bmap); + isl_basic_set_free(ctx, bset); return vec; error: isl_vec_free(ctx, vec); - isl_basic_map_free(ctx, bmap); + isl_basic_set_free(ctx, bset); if (sol) pip_quast_free(sol); if (domain) -- 2.7.4