|
Packit |
fb9d21 |
/*
|
|
Packit |
fb9d21 |
* Copyright 2005-2007 Universiteit Leiden
|
|
Packit |
fb9d21 |
* Copyright 2008-2009 Katholieke Universiteit Leuven
|
|
Packit |
fb9d21 |
* Copyright 2010 INRIA Saclay
|
|
Packit |
fb9d21 |
*
|
|
Packit |
fb9d21 |
* Use of this software is governed by the MIT license
|
|
Packit |
fb9d21 |
*
|
|
Packit |
fb9d21 |
* Written by Sven Verdoolaege, Leiden Institute of Advanced Computer Science,
|
|
Packit |
fb9d21 |
* Universiteit Leiden, Niels Bohrweg 1, 2333 CA Leiden, The Netherlands
|
|
Packit |
fb9d21 |
* and K.U.Leuven, Departement Computerwetenschappen, Celestijnenlaan 200A,
|
|
Packit |
fb9d21 |
* B-3001 Leuven, Belgium
|
|
Packit |
fb9d21 |
* and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,
|
|
Packit |
fb9d21 |
* ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France
|
|
Packit |
fb9d21 |
*/
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
#include <isl_map_private.h>
|
|
Packit |
fb9d21 |
#include <isl_factorization.h>
|
|
Packit |
fb9d21 |
#include <isl_space_private.h>
|
|
Packit |
fb9d21 |
#include <isl_mat_private.h>
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
static __isl_give isl_factorizer *isl_factorizer_alloc(
|
|
Packit |
fb9d21 |
__isl_take isl_morph *morph, int n_group)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
isl_factorizer *f = NULL;
|
|
Packit |
fb9d21 |
int *len = NULL;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
if (!morph)
|
|
Packit |
fb9d21 |
return NULL;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
if (n_group > 0) {
|
|
Packit |
fb9d21 |
len = isl_alloc_array(morph->dom->ctx, int, n_group);
|
|
Packit |
fb9d21 |
if (!len)
|
|
Packit |
fb9d21 |
goto error;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
f = isl_alloc_type(morph->dom->ctx, struct isl_factorizer);
|
|
Packit |
fb9d21 |
if (!f)
|
|
Packit |
fb9d21 |
goto error;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
f->morph = morph;
|
|
Packit |
fb9d21 |
f->n_group = n_group;
|
|
Packit |
fb9d21 |
f->len = len;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
return f;
|
|
Packit |
fb9d21 |
error:
|
|
Packit |
fb9d21 |
free(len);
|
|
Packit |
fb9d21 |
isl_morph_free(morph);
|
|
Packit |
fb9d21 |
return NULL;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
void isl_factorizer_free(__isl_take isl_factorizer *f)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
if (!f)
|
|
Packit |
fb9d21 |
return;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
isl_morph_free(f->morph);
|
|
Packit |
fb9d21 |
free(f->len);
|
|
Packit |
fb9d21 |
free(f);
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
void isl_factorizer_dump(__isl_take isl_factorizer *f)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
int i;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
if (!f)
|
|
Packit |
fb9d21 |
return;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
isl_morph_print_internal(f->morph, stderr);
|
|
Packit |
fb9d21 |
fprintf(stderr, "[");
|
|
Packit |
fb9d21 |
for (i = 0; i < f->n_group; ++i) {
|
|
Packit |
fb9d21 |
if (i)
|
|
Packit |
fb9d21 |
fprintf(stderr, ", ");
|
|
Packit |
fb9d21 |
fprintf(stderr, "%d", f->len[i]);
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
fprintf(stderr, "]\n");
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
__isl_give isl_factorizer *isl_factorizer_identity(__isl_keep isl_basic_set *bset)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
return isl_factorizer_alloc(isl_morph_identity(bset), 0);
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
__isl_give isl_factorizer *isl_factorizer_groups(__isl_keep isl_basic_set *bset,
|
|
Packit |
fb9d21 |
__isl_take isl_mat *Q, __isl_take isl_mat *U, int n, int *len)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
int i;
|
|
Packit |
fb9d21 |
unsigned nvar;
|
|
Packit |
fb9d21 |
unsigned ovar;
|
|
Packit |
fb9d21 |
isl_space *dim;
|
|
Packit |
fb9d21 |
isl_basic_set *dom;
|
|
Packit |
fb9d21 |
isl_basic_set *ran;
|
|
Packit |
fb9d21 |
isl_morph *morph;
|
|
Packit |
fb9d21 |
isl_factorizer *f;
|
|
Packit |
fb9d21 |
isl_mat *id;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
if (!bset || !Q || !U)
|
|
Packit |
fb9d21 |
goto error;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
ovar = 1 + isl_space_offset(bset->dim, isl_dim_set);
|
|
Packit |
fb9d21 |
id = isl_mat_identity(bset->ctx, ovar);
|
|
Packit |
fb9d21 |
Q = isl_mat_diagonal(isl_mat_copy(id), Q);
|
|
Packit |
fb9d21 |
U = isl_mat_diagonal(id, U);
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
nvar = isl_basic_set_dim(bset, isl_dim_set);
|
|
Packit |
fb9d21 |
dim = isl_basic_set_get_space(bset);
|
|
Packit |
fb9d21 |
dom = isl_basic_set_universe(isl_space_copy(dim));
|
|
Packit |
fb9d21 |
dim = isl_space_drop_dims(dim, isl_dim_set, 0, nvar);
|
|
Packit |
fb9d21 |
dim = isl_space_add_dims(dim, isl_dim_set, nvar);
|
|
Packit |
fb9d21 |
ran = isl_basic_set_universe(dim);
|
|
Packit |
fb9d21 |
morph = isl_morph_alloc(dom, ran, Q, U);
|
|
Packit |
fb9d21 |
f = isl_factorizer_alloc(morph, n);
|
|
Packit |
fb9d21 |
if (!f)
|
|
Packit |
fb9d21 |
return NULL;
|
|
Packit |
fb9d21 |
for (i = 0; i < n; ++i)
|
|
Packit |
fb9d21 |
f->len[i] = len[i];
|
|
Packit |
fb9d21 |
return f;
|
|
Packit |
fb9d21 |
error:
|
|
Packit |
fb9d21 |
isl_mat_free(Q);
|
|
Packit |
fb9d21 |
isl_mat_free(U);
|
|
Packit |
fb9d21 |
return NULL;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
struct isl_factor_groups {
|
|
Packit |
fb9d21 |
int *pos; /* for each column: row position of pivot */
|
|
Packit |
fb9d21 |
int *group; /* group to which a column belongs */
|
|
Packit |
fb9d21 |
int *cnt; /* number of columns in the group */
|
|
Packit |
fb9d21 |
int *rowgroup; /* group to which a constraint belongs */
|
|
Packit |
fb9d21 |
};
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
/* Initialize isl_factor_groups structure: find pivot row positions,
|
|
Packit |
fb9d21 |
* each column initially belongs to its own group and the groups
|
|
Packit |
fb9d21 |
* of the constraints are still unknown.
|
|
Packit |
fb9d21 |
*/
|
|
Packit |
fb9d21 |
static int init_groups(struct isl_factor_groups *g, __isl_keep isl_mat *H)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
int i, j;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
if (!H)
|
|
Packit |
fb9d21 |
return -1;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
g->pos = isl_alloc_array(H->ctx, int, H->n_col);
|
|
Packit |
fb9d21 |
g->group = isl_alloc_array(H->ctx, int, H->n_col);
|
|
Packit |
fb9d21 |
g->cnt = isl_alloc_array(H->ctx, int, H->n_col);
|
|
Packit |
fb9d21 |
g->rowgroup = isl_alloc_array(H->ctx, int, H->n_row);
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
if (!g->pos || !g->group || !g->cnt || !g->rowgroup)
|
|
Packit |
fb9d21 |
return -1;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
for (i = 0; i < H->n_row; ++i)
|
|
Packit |
fb9d21 |
g->rowgroup[i] = -1;
|
|
Packit |
fb9d21 |
for (i = 0, j = 0; i < H->n_col; ++i) {
|
|
Packit |
fb9d21 |
for ( ; j < H->n_row; ++j)
|
|
Packit |
fb9d21 |
if (!isl_int_is_zero(H->row[j][i]))
|
|
Packit |
fb9d21 |
break;
|
|
Packit |
fb9d21 |
g->pos[i] = j;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
for (i = 0; i < H->n_col; ++i) {
|
|
Packit |
fb9d21 |
g->group[i] = i;
|
|
Packit |
fb9d21 |
g->cnt[i] = 1;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
return 0;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
/* Update group[k] to the group column k belongs to.
|
|
Packit |
fb9d21 |
* When merging two groups, only the group of the current
|
|
Packit |
fb9d21 |
* group leader is changed. Here we change the group of
|
|
Packit |
fb9d21 |
* the other members to also point to the group that the
|
|
Packit |
fb9d21 |
* old group leader now points to.
|
|
Packit |
fb9d21 |
*/
|
|
Packit |
fb9d21 |
static void update_group(struct isl_factor_groups *g, int k)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
int p = g->group[k];
|
|
Packit |
fb9d21 |
while (g->cnt[p] == 0)
|
|
Packit |
fb9d21 |
p = g->group[p];
|
|
Packit |
fb9d21 |
g->group[k] = p;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
/* Merge group i with all groups of the subsequent columns
|
|
Packit |
fb9d21 |
* with non-zero coefficients in row j of H.
|
|
Packit |
fb9d21 |
* (The previous columns are all zero; otherwise we would have handled
|
|
Packit |
fb9d21 |
* the row before.)
|
|
Packit |
fb9d21 |
*/
|
|
Packit |
fb9d21 |
static int update_group_i_with_row_j(struct isl_factor_groups *g, int i, int j,
|
|
Packit |
fb9d21 |
__isl_keep isl_mat *H)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
int k;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
g->rowgroup[j] = g->group[i];
|
|
Packit |
fb9d21 |
for (k = i + 1; k < H->n_col && j >= g->pos[k]; ++k) {
|
|
Packit |
fb9d21 |
update_group(g, k);
|
|
Packit |
fb9d21 |
update_group(g, i);
|
|
Packit |
fb9d21 |
if (g->group[k] != g->group[i] &&
|
|
Packit |
fb9d21 |
!isl_int_is_zero(H->row[j][k])) {
|
|
Packit |
fb9d21 |
isl_assert(H->ctx, g->cnt[g->group[k]] != 0, return -1);
|
|
Packit |
fb9d21 |
isl_assert(H->ctx, g->cnt[g->group[i]] != 0, return -1);
|
|
Packit |
fb9d21 |
if (g->group[i] < g->group[k]) {
|
|
Packit |
fb9d21 |
g->cnt[g->group[i]] += g->cnt[g->group[k]];
|
|
Packit |
fb9d21 |
g->cnt[g->group[k]] = 0;
|
|
Packit |
fb9d21 |
g->group[g->group[k]] = g->group[i];
|
|
Packit |
fb9d21 |
} else {
|
|
Packit |
fb9d21 |
g->cnt[g->group[k]] += g->cnt[g->group[i]];
|
|
Packit |
fb9d21 |
g->cnt[g->group[i]] = 0;
|
|
Packit |
fb9d21 |
g->group[g->group[i]] = g->group[k];
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
return 0;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
/* Update the group information based on the constraint matrix.
|
|
Packit |
fb9d21 |
*/
|
|
Packit |
fb9d21 |
static int update_groups(struct isl_factor_groups *g, __isl_keep isl_mat *H)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
int i, j;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
for (i = 0; i < H->n_col && g->cnt[0] < H->n_col; ++i) {
|
|
Packit |
fb9d21 |
if (g->pos[i] == H->n_row)
|
|
Packit |
fb9d21 |
continue; /* A line direction */
|
|
Packit |
fb9d21 |
if (g->rowgroup[g->pos[i]] == -1)
|
|
Packit |
fb9d21 |
g->rowgroup[g->pos[i]] = i;
|
|
Packit |
fb9d21 |
for (j = g->pos[i] + 1; j < H->n_row; ++j) {
|
|
Packit |
fb9d21 |
if (isl_int_is_zero(H->row[j][i]))
|
|
Packit |
fb9d21 |
continue;
|
|
Packit |
fb9d21 |
if (g->rowgroup[j] != -1)
|
|
Packit |
fb9d21 |
continue;
|
|
Packit |
fb9d21 |
if (update_group_i_with_row_j(g, i, j, H) < 0)
|
|
Packit |
fb9d21 |
return -1;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
for (i = 1; i < H->n_col; ++i)
|
|
Packit |
fb9d21 |
update_group(g, i);
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
return 0;
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
static void clear_groups(struct isl_factor_groups *g)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
if (!g)
|
|
Packit |
fb9d21 |
return;
|
|
Packit |
fb9d21 |
free(g->pos);
|
|
Packit |
fb9d21 |
free(g->group);
|
|
Packit |
fb9d21 |
free(g->cnt);
|
|
Packit |
fb9d21 |
free(g->rowgroup);
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
/* Determine if the set variables of the basic set can be factorized and
|
|
Packit |
fb9d21 |
* return the results in an isl_factorizer.
|
|
Packit |
fb9d21 |
*
|
|
Packit |
fb9d21 |
* The algorithm works by first computing the Hermite normal form
|
|
Packit |
fb9d21 |
* and then grouping columns linked by one or more constraints together,
|
|
Packit |
fb9d21 |
* where a constraints "links" two or more columns if the constraint
|
|
Packit |
fb9d21 |
* has nonzero coefficients in the columns.
|
|
Packit |
fb9d21 |
*/
|
|
Packit |
fb9d21 |
__isl_give isl_factorizer *isl_basic_set_factorizer(
|
|
Packit |
fb9d21 |
__isl_keep isl_basic_set *bset)
|
|
Packit |
fb9d21 |
{
|
|
Packit |
fb9d21 |
int i, j, n, done;
|
|
Packit |
fb9d21 |
isl_mat *H, *U, *Q;
|
|
Packit |
fb9d21 |
unsigned nvar;
|
|
Packit |
fb9d21 |
struct isl_factor_groups g = { 0 };
|
|
Packit |
fb9d21 |
isl_factorizer *f;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
if (!bset)
|
|
Packit |
fb9d21 |
return NULL;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
isl_assert(bset->ctx, isl_basic_set_dim(bset, isl_dim_div) == 0,
|
|
Packit |
fb9d21 |
return NULL);
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
nvar = isl_basic_set_dim(bset, isl_dim_set);
|
|
Packit |
fb9d21 |
if (nvar <= 1)
|
|
Packit |
fb9d21 |
return isl_factorizer_identity(bset);
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
H = isl_mat_alloc(bset->ctx, bset->n_eq + bset->n_ineq, nvar);
|
|
Packit |
fb9d21 |
if (!H)
|
|
Packit |
fb9d21 |
return NULL;
|
|
Packit |
fb9d21 |
isl_mat_sub_copy(bset->ctx, H->row, bset->eq, bset->n_eq,
|
|
Packit |
fb9d21 |
0, 1 + isl_space_offset(bset->dim, isl_dim_set), nvar);
|
|
Packit |
fb9d21 |
isl_mat_sub_copy(bset->ctx, H->row + bset->n_eq, bset->ineq, bset->n_ineq,
|
|
Packit |
fb9d21 |
0, 1 + isl_space_offset(bset->dim, isl_dim_set), nvar);
|
|
Packit |
fb9d21 |
H = isl_mat_left_hermite(H, 0, &U, &Q);
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
if (init_groups(&g, H) < 0)
|
|
Packit |
fb9d21 |
goto error;
|
|
Packit |
fb9d21 |
if (update_groups(&g, H) < 0)
|
|
Packit |
fb9d21 |
goto error;
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
if (g.cnt[0] == nvar) {
|
|
Packit |
fb9d21 |
isl_mat_free(H);
|
|
Packit |
fb9d21 |
isl_mat_free(U);
|
|
Packit |
fb9d21 |
isl_mat_free(Q);
|
|
Packit |
fb9d21 |
clear_groups(&g);
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
return isl_factorizer_identity(bset);
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
done = 0;
|
|
Packit |
fb9d21 |
n = 0;
|
|
Packit |
fb9d21 |
while (done != nvar) {
|
|
Packit |
fb9d21 |
int group = g.group[done];
|
|
Packit |
fb9d21 |
for (i = 1; i < g.cnt[group]; ++i) {
|
|
Packit |
fb9d21 |
if (g.group[done + i] == group)
|
|
Packit |
fb9d21 |
continue;
|
|
Packit |
fb9d21 |
for (j = done + g.cnt[group]; j < nvar; ++j)
|
|
Packit |
fb9d21 |
if (g.group[j] == group)
|
|
Packit |
fb9d21 |
break;
|
|
Packit |
fb9d21 |
if (j == nvar)
|
|
Packit |
fb9d21 |
isl_die(bset->ctx, isl_error_internal,
|
|
Packit |
fb9d21 |
"internal error", goto error);
|
|
Packit |
fb9d21 |
g.group[j] = g.group[done + i];
|
|
Packit |
fb9d21 |
Q = isl_mat_swap_rows(Q, done + i, j);
|
|
Packit |
fb9d21 |
U = isl_mat_swap_cols(U, done + i, j);
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
done += g.cnt[group];
|
|
Packit |
fb9d21 |
g.pos[n++] = g.cnt[group];
|
|
Packit |
fb9d21 |
}
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
f = isl_factorizer_groups(bset, Q, U, n, g.pos);
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
isl_mat_free(H);
|
|
Packit |
fb9d21 |
clear_groups(&g);
|
|
Packit |
fb9d21 |
|
|
Packit |
fb9d21 |
return f;
|
|
Packit |
fb9d21 |
error:
|
|
Packit |
fb9d21 |
isl_mat_free(H);
|
|
Packit |
fb9d21 |
isl_mat_free(U);
|
|
Packit |
fb9d21 |
isl_mat_free(Q);
|
|
Packit |
fb9d21 |
clear_groups(&g);
|
|
Packit |
fb9d21 |
return NULL;
|
|
Packit |
fb9d21 |
}
|