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);
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);
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) {
*
* 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;
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);
}
}
-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;
}
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);
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);
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;
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);
+#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);
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)