1*5971e316Smrg /*
2*5971e316Smrg * Copyright 2005-2007 Universiteit Leiden
3*5971e316Smrg * Copyright 2008-2009 Katholieke Universiteit Leuven
4*5971e316Smrg * Copyright 2010 INRIA Saclay
5*5971e316Smrg *
6*5971e316Smrg * Use of this software is governed by the MIT license
7*5971e316Smrg *
8*5971e316Smrg * Written by Sven Verdoolaege, Leiden Institute of Advanced Computer Science,
9*5971e316Smrg * Universiteit Leiden, Niels Bohrweg 1, 2333 CA Leiden, The Netherlands
10*5971e316Smrg * and K.U.Leuven, Departement Computerwetenschappen, Celestijnenlaan 200A,
11*5971e316Smrg * B-3001 Leuven, Belgium
12*5971e316Smrg * and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,
13*5971e316Smrg * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France
14*5971e316Smrg */
15*5971e316Smrg
16*5971e316Smrg #include <isl_map_private.h>
17*5971e316Smrg #include <isl_factorization.h>
18*5971e316Smrg #include <isl_space_private.h>
19*5971e316Smrg #include <isl_mat_private.h>
20*5971e316Smrg
21*5971e316Smrg /* Return the isl_ctx to which "f" belongs.
22*5971e316Smrg */
isl_factorizer_get_ctx(__isl_keep isl_factorizer * f)23*5971e316Smrg isl_ctx *isl_factorizer_get_ctx(__isl_keep isl_factorizer *f)
24*5971e316Smrg {
25*5971e316Smrg if (!f)
26*5971e316Smrg return NULL;
27*5971e316Smrg return isl_basic_set_get_ctx(f->bset);
28*5971e316Smrg }
29*5971e316Smrg
isl_factorizer_alloc(__isl_keep isl_basic_set * bset,__isl_take isl_morph * morph,int n_group)30*5971e316Smrg static __isl_give isl_factorizer *isl_factorizer_alloc(
31*5971e316Smrg __isl_keep isl_basic_set *bset, __isl_take isl_morph *morph,
32*5971e316Smrg int n_group)
33*5971e316Smrg {
34*5971e316Smrg isl_factorizer *f = NULL;
35*5971e316Smrg int *len = NULL;
36*5971e316Smrg
37*5971e316Smrg if (!morph)
38*5971e316Smrg return NULL;
39*5971e316Smrg
40*5971e316Smrg if (n_group > 0) {
41*5971e316Smrg len = isl_alloc_array(morph->dom->ctx, int, n_group);
42*5971e316Smrg if (!len)
43*5971e316Smrg goto error;
44*5971e316Smrg }
45*5971e316Smrg
46*5971e316Smrg f = isl_alloc_type(morph->dom->ctx, struct isl_factorizer);
47*5971e316Smrg if (!f)
48*5971e316Smrg goto error;
49*5971e316Smrg
50*5971e316Smrg f->bset = isl_basic_set_copy(bset);
51*5971e316Smrg f->morph = morph;
52*5971e316Smrg f->n_group = n_group;
53*5971e316Smrg f->len = len;
54*5971e316Smrg
55*5971e316Smrg return f;
56*5971e316Smrg error:
57*5971e316Smrg free(len);
58*5971e316Smrg isl_morph_free(morph);
59*5971e316Smrg return NULL;
60*5971e316Smrg }
61*5971e316Smrg
isl_factorizer_free(__isl_take isl_factorizer * f)62*5971e316Smrg __isl_null isl_factorizer *isl_factorizer_free(__isl_take isl_factorizer *f)
63*5971e316Smrg {
64*5971e316Smrg if (!f)
65*5971e316Smrg return NULL;
66*5971e316Smrg
67*5971e316Smrg isl_basic_set_free(f->bset);
68*5971e316Smrg isl_morph_free(f->morph);
69*5971e316Smrg free(f->len);
70*5971e316Smrg free(f);
71*5971e316Smrg return NULL;
72*5971e316Smrg }
73*5971e316Smrg
isl_factorizer_dump(__isl_take isl_factorizer * f)74*5971e316Smrg void isl_factorizer_dump(__isl_take isl_factorizer *f)
75*5971e316Smrg {
76*5971e316Smrg int i;
77*5971e316Smrg
78*5971e316Smrg if (!f)
79*5971e316Smrg return;
80*5971e316Smrg
81*5971e316Smrg isl_morph_print_internal(f->morph, stderr);
82*5971e316Smrg fprintf(stderr, "[");
83*5971e316Smrg for (i = 0; i < f->n_group; ++i) {
84*5971e316Smrg if (i)
85*5971e316Smrg fprintf(stderr, ", ");
86*5971e316Smrg fprintf(stderr, "%d", f->len[i]);
87*5971e316Smrg }
88*5971e316Smrg fprintf(stderr, "]\n");
89*5971e316Smrg }
90*5971e316Smrg
isl_factorizer_identity(__isl_keep isl_basic_set * bset)91*5971e316Smrg __isl_give isl_factorizer *isl_factorizer_identity(__isl_keep isl_basic_set *bset)
92*5971e316Smrg {
93*5971e316Smrg return isl_factorizer_alloc(bset, isl_morph_identity(bset), 0);
94*5971e316Smrg }
95*5971e316Smrg
isl_factorizer_groups(__isl_keep isl_basic_set * bset,__isl_take isl_mat * Q,__isl_take isl_mat * U,int n,int * len)96*5971e316Smrg __isl_give isl_factorizer *isl_factorizer_groups(__isl_keep isl_basic_set *bset,
97*5971e316Smrg __isl_take isl_mat *Q, __isl_take isl_mat *U, int n, int *len)
98*5971e316Smrg {
99*5971e316Smrg int i;
100*5971e316Smrg isl_size nvar, off;
101*5971e316Smrg isl_space *space;
102*5971e316Smrg isl_basic_set *dom;
103*5971e316Smrg isl_basic_set *ran;
104*5971e316Smrg isl_morph *morph;
105*5971e316Smrg isl_factorizer *f;
106*5971e316Smrg isl_mat *id;
107*5971e316Smrg
108*5971e316Smrg nvar = isl_basic_set_dim(bset, isl_dim_set);
109*5971e316Smrg off = isl_basic_set_var_offset(bset, isl_dim_set);
110*5971e316Smrg if (nvar < 0 || off < 0 || !Q || !U)
111*5971e316Smrg goto error;
112*5971e316Smrg
113*5971e316Smrg id = isl_mat_identity(bset->ctx, 1 + off);
114*5971e316Smrg Q = isl_mat_diagonal(isl_mat_copy(id), Q);
115*5971e316Smrg U = isl_mat_diagonal(id, U);
116*5971e316Smrg
117*5971e316Smrg space = isl_basic_set_get_space(bset);
118*5971e316Smrg dom = isl_basic_set_universe(isl_space_copy(space));
119*5971e316Smrg space = isl_space_drop_dims(space, isl_dim_set, 0, nvar);
120*5971e316Smrg space = isl_space_add_dims(space, isl_dim_set, nvar);
121*5971e316Smrg ran = isl_basic_set_universe(space);
122*5971e316Smrg morph = isl_morph_alloc(dom, ran, Q, U);
123*5971e316Smrg f = isl_factorizer_alloc(bset, morph, n);
124*5971e316Smrg if (!f)
125*5971e316Smrg return NULL;
126*5971e316Smrg for (i = 0; i < n; ++i)
127*5971e316Smrg f->len[i] = len[i];
128*5971e316Smrg return f;
129*5971e316Smrg error:
130*5971e316Smrg isl_mat_free(Q);
131*5971e316Smrg isl_mat_free(U);
132*5971e316Smrg return NULL;
133*5971e316Smrg }
134*5971e316Smrg
135*5971e316Smrg struct isl_factor_groups {
136*5971e316Smrg int *pos; /* for each column: row position of pivot */
137*5971e316Smrg int *group; /* group to which a column belongs */
138*5971e316Smrg int *cnt; /* number of columns in the group */
139*5971e316Smrg int *rowgroup; /* group to which a constraint belongs */
140*5971e316Smrg };
141*5971e316Smrg
142*5971e316Smrg /* Initialize isl_factor_groups structure: find pivot row positions,
143*5971e316Smrg * each column initially belongs to its own group and the groups
144*5971e316Smrg * of the constraints are still unknown.
145*5971e316Smrg */
init_groups(struct isl_factor_groups * g,__isl_keep isl_mat * H)146*5971e316Smrg static int init_groups(struct isl_factor_groups *g, __isl_keep isl_mat *H)
147*5971e316Smrg {
148*5971e316Smrg int i, j;
149*5971e316Smrg
150*5971e316Smrg if (!H)
151*5971e316Smrg return -1;
152*5971e316Smrg
153*5971e316Smrg g->pos = isl_alloc_array(H->ctx, int, H->n_col);
154*5971e316Smrg g->group = isl_alloc_array(H->ctx, int, H->n_col);
155*5971e316Smrg g->cnt = isl_alloc_array(H->ctx, int, H->n_col);
156*5971e316Smrg g->rowgroup = isl_alloc_array(H->ctx, int, H->n_row);
157*5971e316Smrg
158*5971e316Smrg if (!g->pos || !g->group || !g->cnt || !g->rowgroup)
159*5971e316Smrg return -1;
160*5971e316Smrg
161*5971e316Smrg for (i = 0; i < H->n_row; ++i)
162*5971e316Smrg g->rowgroup[i] = -1;
163*5971e316Smrg for (i = 0, j = 0; i < H->n_col; ++i) {
164*5971e316Smrg for ( ; j < H->n_row; ++j)
165*5971e316Smrg if (!isl_int_is_zero(H->row[j][i]))
166*5971e316Smrg break;
167*5971e316Smrg g->pos[i] = j;
168*5971e316Smrg }
169*5971e316Smrg for (i = 0; i < H->n_col; ++i) {
170*5971e316Smrg g->group[i] = i;
171*5971e316Smrg g->cnt[i] = 1;
172*5971e316Smrg }
173*5971e316Smrg
174*5971e316Smrg return 0;
175*5971e316Smrg }
176*5971e316Smrg
177*5971e316Smrg /* Update group[k] to the group column k belongs to.
178*5971e316Smrg * When merging two groups, only the group of the current
179*5971e316Smrg * group leader is changed. Here we change the group of
180*5971e316Smrg * the other members to also point to the group that the
181*5971e316Smrg * old group leader now points to.
182*5971e316Smrg */
update_group(struct isl_factor_groups * g,int k)183*5971e316Smrg static void update_group(struct isl_factor_groups *g, int k)
184*5971e316Smrg {
185*5971e316Smrg int p = g->group[k];
186*5971e316Smrg while (g->cnt[p] == 0)
187*5971e316Smrg p = g->group[p];
188*5971e316Smrg g->group[k] = p;
189*5971e316Smrg }
190*5971e316Smrg
191*5971e316Smrg /* Merge group i with all groups of the subsequent columns
192*5971e316Smrg * with non-zero coefficients in row j of H.
193*5971e316Smrg * (The previous columns are all zero; otherwise we would have handled
194*5971e316Smrg * the row before.)
195*5971e316Smrg */
update_group_i_with_row_j(struct isl_factor_groups * g,int i,int j,__isl_keep isl_mat * H)196*5971e316Smrg static int update_group_i_with_row_j(struct isl_factor_groups *g, int i, int j,
197*5971e316Smrg __isl_keep isl_mat *H)
198*5971e316Smrg {
199*5971e316Smrg int k;
200*5971e316Smrg
201*5971e316Smrg g->rowgroup[j] = g->group[i];
202*5971e316Smrg for (k = i + 1; k < H->n_col && j >= g->pos[k]; ++k) {
203*5971e316Smrg update_group(g, k);
204*5971e316Smrg update_group(g, i);
205*5971e316Smrg if (g->group[k] != g->group[i] &&
206*5971e316Smrg !isl_int_is_zero(H->row[j][k])) {
207*5971e316Smrg isl_assert(H->ctx, g->cnt[g->group[k]] != 0, return -1);
208*5971e316Smrg isl_assert(H->ctx, g->cnt[g->group[i]] != 0, return -1);
209*5971e316Smrg if (g->group[i] < g->group[k]) {
210*5971e316Smrg g->cnt[g->group[i]] += g->cnt[g->group[k]];
211*5971e316Smrg g->cnt[g->group[k]] = 0;
212*5971e316Smrg g->group[g->group[k]] = g->group[i];
213*5971e316Smrg } else {
214*5971e316Smrg g->cnt[g->group[k]] += g->cnt[g->group[i]];
215*5971e316Smrg g->cnt[g->group[i]] = 0;
216*5971e316Smrg g->group[g->group[i]] = g->group[k];
217*5971e316Smrg }
218*5971e316Smrg }
219*5971e316Smrg }
220*5971e316Smrg
221*5971e316Smrg return 0;
222*5971e316Smrg }
223*5971e316Smrg
224*5971e316Smrg /* Update the group information based on the constraint matrix.
225*5971e316Smrg */
update_groups(struct isl_factor_groups * g,__isl_keep isl_mat * H)226*5971e316Smrg static int update_groups(struct isl_factor_groups *g, __isl_keep isl_mat *H)
227*5971e316Smrg {
228*5971e316Smrg int i, j;
229*5971e316Smrg
230*5971e316Smrg for (i = 0; i < H->n_col && g->cnt[0] < H->n_col; ++i) {
231*5971e316Smrg if (g->pos[i] == H->n_row)
232*5971e316Smrg continue; /* A line direction */
233*5971e316Smrg if (g->rowgroup[g->pos[i]] == -1)
234*5971e316Smrg g->rowgroup[g->pos[i]] = i;
235*5971e316Smrg for (j = g->pos[i] + 1; j < H->n_row; ++j) {
236*5971e316Smrg if (isl_int_is_zero(H->row[j][i]))
237*5971e316Smrg continue;
238*5971e316Smrg if (g->rowgroup[j] != -1)
239*5971e316Smrg continue;
240*5971e316Smrg if (update_group_i_with_row_j(g, i, j, H) < 0)
241*5971e316Smrg return -1;
242*5971e316Smrg }
243*5971e316Smrg }
244*5971e316Smrg for (i = 1; i < H->n_col; ++i)
245*5971e316Smrg update_group(g, i);
246*5971e316Smrg
247*5971e316Smrg return 0;
248*5971e316Smrg }
249*5971e316Smrg
clear_groups(struct isl_factor_groups * g)250*5971e316Smrg static void clear_groups(struct isl_factor_groups *g)
251*5971e316Smrg {
252*5971e316Smrg if (!g)
253*5971e316Smrg return;
254*5971e316Smrg free(g->pos);
255*5971e316Smrg free(g->group);
256*5971e316Smrg free(g->cnt);
257*5971e316Smrg free(g->rowgroup);
258*5971e316Smrg }
259*5971e316Smrg
260*5971e316Smrg /* Determine if the set variables of the basic set can be factorized and
261*5971e316Smrg * return the results in an isl_factorizer.
262*5971e316Smrg *
263*5971e316Smrg * The algorithm works by first computing the Hermite normal form
264*5971e316Smrg * and then grouping columns linked by one or more constraints together,
265*5971e316Smrg * where a constraints "links" two or more columns if the constraint
266*5971e316Smrg * has nonzero coefficients in the columns.
267*5971e316Smrg */
isl_basic_set_factorizer(__isl_keep isl_basic_set * bset)268*5971e316Smrg __isl_give isl_factorizer *isl_basic_set_factorizer(
269*5971e316Smrg __isl_keep isl_basic_set *bset)
270*5971e316Smrg {
271*5971e316Smrg int i, j, n, done;
272*5971e316Smrg isl_mat *H, *U, *Q;
273*5971e316Smrg isl_size nvar, first;
274*5971e316Smrg struct isl_factor_groups g = { 0 };
275*5971e316Smrg isl_factorizer *f;
276*5971e316Smrg
277*5971e316Smrg nvar = isl_basic_set_dim(bset, isl_dim_set);
278*5971e316Smrg first = isl_basic_set_var_offset(bset, isl_dim_set);
279*5971e316Smrg if (nvar < 0 || first < 0 || isl_basic_set_check_no_locals(bset) < 0)
280*5971e316Smrg return NULL;
281*5971e316Smrg
282*5971e316Smrg if (nvar <= 1)
283*5971e316Smrg return isl_factorizer_identity(bset);
284*5971e316Smrg
285*5971e316Smrg H = isl_mat_alloc(bset->ctx, bset->n_eq + bset->n_ineq, nvar);
286*5971e316Smrg if (!H)
287*5971e316Smrg return NULL;
288*5971e316Smrg isl_mat_sub_copy(bset->ctx, H->row, bset->eq, bset->n_eq,
289*5971e316Smrg 0, 1 + first, nvar);
290*5971e316Smrg isl_mat_sub_copy(bset->ctx, H->row + bset->n_eq, bset->ineq, bset->n_ineq,
291*5971e316Smrg 0, 1 + first, nvar);
292*5971e316Smrg H = isl_mat_left_hermite(H, 0, &U, &Q);
293*5971e316Smrg
294*5971e316Smrg if (init_groups(&g, H) < 0)
295*5971e316Smrg goto error;
296*5971e316Smrg if (update_groups(&g, H) < 0)
297*5971e316Smrg goto error;
298*5971e316Smrg
299*5971e316Smrg if (g.cnt[0] == nvar) {
300*5971e316Smrg isl_mat_free(H);
301*5971e316Smrg isl_mat_free(U);
302*5971e316Smrg isl_mat_free(Q);
303*5971e316Smrg clear_groups(&g);
304*5971e316Smrg
305*5971e316Smrg return isl_factorizer_identity(bset);
306*5971e316Smrg }
307*5971e316Smrg
308*5971e316Smrg done = 0;
309*5971e316Smrg n = 0;
310*5971e316Smrg while (done != nvar) {
311*5971e316Smrg int group = g.group[done];
312*5971e316Smrg for (i = 1; i < g.cnt[group]; ++i) {
313*5971e316Smrg if (g.group[done + i] == group)
314*5971e316Smrg continue;
315*5971e316Smrg for (j = done + g.cnt[group]; j < nvar; ++j)
316*5971e316Smrg if (g.group[j] == group)
317*5971e316Smrg break;
318*5971e316Smrg if (j == nvar)
319*5971e316Smrg isl_die(bset->ctx, isl_error_internal,
320*5971e316Smrg "internal error", goto error);
321*5971e316Smrg g.group[j] = g.group[done + i];
322*5971e316Smrg Q = isl_mat_swap_rows(Q, done + i, j);
323*5971e316Smrg U = isl_mat_swap_cols(U, done + i, j);
324*5971e316Smrg }
325*5971e316Smrg done += g.cnt[group];
326*5971e316Smrg g.pos[n++] = g.cnt[group];
327*5971e316Smrg }
328*5971e316Smrg
329*5971e316Smrg f = isl_factorizer_groups(bset, Q, U, n, g.pos);
330*5971e316Smrg
331*5971e316Smrg isl_mat_free(H);
332*5971e316Smrg clear_groups(&g);
333*5971e316Smrg
334*5971e316Smrg return f;
335*5971e316Smrg error:
336*5971e316Smrg isl_mat_free(H);
337*5971e316Smrg isl_mat_free(U);
338*5971e316Smrg isl_mat_free(Q);
339*5971e316Smrg clear_groups(&g);
340*5971e316Smrg return NULL;
341*5971e316Smrg }
342*5971e316Smrg
343*5971e316Smrg /* Given the factorizer "f" of a basic set,
344*5971e316Smrg * call "test" on each resulting factor as long as each call succeeds.
345*5971e316Smrg */
isl_factorizer_every_factor_basic_set(__isl_keep isl_factorizer * f,isl_bool (* test)(__isl_keep isl_basic_set * bset,void * user),void * user)346*5971e316Smrg __isl_give isl_bool isl_factorizer_every_factor_basic_set(
347*5971e316Smrg __isl_keep isl_factorizer *f,
348*5971e316Smrg isl_bool (*test)(__isl_keep isl_basic_set *bset, void *user),
349*5971e316Smrg void *user)
350*5971e316Smrg {
351*5971e316Smrg int i, n;
352*5971e316Smrg isl_bool every = isl_bool_true;
353*5971e316Smrg isl_size nparam, nvar;
354*5971e316Smrg isl_basic_set *bset;
355*5971e316Smrg
356*5971e316Smrg if (!f)
357*5971e316Smrg return isl_bool_error;
358*5971e316Smrg nparam = isl_basic_set_dim(f->bset, isl_dim_param);
359*5971e316Smrg nvar = isl_basic_set_dim(f->bset, isl_dim_set);
360*5971e316Smrg if (nparam < 0 || nvar < 0)
361*5971e316Smrg return isl_bool_error;
362*5971e316Smrg
363*5971e316Smrg bset = isl_basic_set_copy(f->bset);
364*5971e316Smrg bset = isl_morph_basic_set(isl_morph_copy(f->morph), bset);
365*5971e316Smrg
366*5971e316Smrg for (i = 0, n = 0; i < f->n_group; ++i) {
367*5971e316Smrg isl_basic_set *factor;
368*5971e316Smrg
369*5971e316Smrg factor = isl_basic_set_copy(bset);
370*5971e316Smrg factor = isl_basic_set_drop_constraints_involving(factor,
371*5971e316Smrg nparam + n + f->len[i], nvar - n - f->len[i]);
372*5971e316Smrg factor = isl_basic_set_drop_constraints_involving(factor,
373*5971e316Smrg nparam, n);
374*5971e316Smrg factor = isl_basic_set_drop(factor, isl_dim_set,
375*5971e316Smrg n + f->len[i], nvar - n - f->len[i]);
376*5971e316Smrg factor = isl_basic_set_drop(factor, isl_dim_set, 0, n);
377*5971e316Smrg every = test(factor, user);
378*5971e316Smrg isl_basic_set_free(factor);
379*5971e316Smrg
380*5971e316Smrg if (every < 0 || !every)
381*5971e316Smrg break;
382*5971e316Smrg
383*5971e316Smrg n += f->len[i];
384*5971e316Smrg }
385*5971e316Smrg
386*5971e316Smrg isl_basic_set_free(bset);
387*5971e316Smrg
388*5971e316Smrg return every;
389*5971e316Smrg }
390