isl_map_coalesce: avoid ignoring constraints redundant wrt implicit equalities
[isl.git] / isl_local.c
blobb607c5dc41f06e0d7f8108f7e4cfaa2d02993bbc
1 /*
2 * Copyright 2011 INRIA Saclay
3 * Copyright 2014 Ecole Normale Superieure
4 * Copyright 2015 Sven Verdoolaege
6 * Use of this software is governed by the MIT license
8 * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
9 * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
10 * 91893 Orsay, France
11 * and Ecole Normale Superieure, 45 rue d'Ulm, 75230 Paris, France
14 #include <isl/space.h>
15 #include <isl_vec_private.h>
16 #include <isl_mat_private.h>
17 #include <isl_reordering.h>
18 #include <isl_seq.h>
19 #include <isl_local_private.h>
21 /* Return the isl_ctx to which "local" belongs.
23 isl_ctx *isl_local_get_ctx(__isl_keep isl_local *local)
25 if (!local)
26 return NULL;
28 return isl_mat_get_ctx(local);
31 /* Create an isl_local object from a matrix describing
32 * integer divisions.
34 * An isl_local object is current defined as exactly such a matrix,
35 * so simply return the input.
37 __isl_give isl_local *isl_local_alloc_from_mat(__isl_take isl_mat *mat)
39 return mat;
42 /* Return a new reference to "local".
44 __isl_give isl_local *isl_local_copy(__isl_keep isl_local *local)
46 return isl_local_alloc_from_mat(isl_mat_copy(local));
49 /* Free "local" and return NULL.
51 __isl_null isl_local *isl_local_free(__isl_take isl_local *local)
53 isl_mat_free(local);
54 return NULL;
57 /* Return the number of local variables (isl_dim_div),
58 * the number of other variables (isl_dim_set) or
59 * the total number of variables (isl_dim_all) in "local".
61 * Other types do not have any meaning for an isl_local object.
63 isl_size isl_local_dim(__isl_keep isl_local *local, enum isl_dim_type type)
65 isl_mat *mat = local;
67 if (!local)
68 return isl_size_error;
69 if (type == isl_dim_div)
70 return isl_mat_rows(mat);
71 if (type == isl_dim_all) {
72 isl_size cols = isl_mat_cols(mat);
73 if (cols < 0)
74 return isl_size_error;
75 return cols - 2;
77 if (type == isl_dim_set) {
78 isl_size total, n_div;
80 total = isl_local_dim(local, isl_dim_all);
81 n_div = isl_local_dim(local, isl_dim_div);
82 if (total < 0 || n_div < 0)
83 return isl_size_error;
84 return total - n_div;
86 isl_die(isl_local_get_ctx(local), isl_error_unsupported,
87 "unsupported dimension type", return isl_size_error);
90 #undef TYPE
91 #define TYPE isl_local
92 static
93 #include "check_type_range_templ.c"
95 /* Check that "pos" is a valid position for a variable in "local".
97 static isl_stat isl_local_check_pos(__isl_keep isl_local *local, int pos)
99 return isl_local_check_range(local, isl_dim_div, pos, 1);
102 /* Given local variables "local",
103 * is the variable at position "pos" marked as not having
104 * an explicit representation?
105 * Note that even if this variable is not marked in this way and therefore
106 * does have an explicit representation, this representation may still
107 * depend (indirectly) on other local variables that do not
108 * have an explicit representation.
110 isl_bool isl_local_div_is_marked_unknown(__isl_keep isl_local *local, int pos)
112 isl_mat *mat = local;
114 if (isl_local_check_pos(local, pos) < 0)
115 return isl_bool_error;
116 return isl_bool_ok(isl_int_is_zero(mat->row[pos][0]));
119 /* Given local variables "local",
120 * does the variable at position "pos" have a complete explicit representation?
121 * Having a complete explicit representation requires not only
122 * an explicit representation, but also that all local variables
123 * that appear in this explicit representation in turn have
124 * a complete explicit representation.
126 isl_bool isl_local_div_is_known(__isl_keep isl_local *local, int pos)
128 isl_bool marked;
129 int i, off;
130 isl_size n, cols;
131 isl_mat *mat = local;
133 if (isl_local_check_pos(local, pos) < 0)
134 return isl_bool_error;
136 marked = isl_local_div_is_marked_unknown(local, pos);
137 if (marked < 0 || marked)
138 return isl_bool_not(marked);
140 n = isl_local_dim(local, isl_dim_div);
141 cols = isl_mat_cols(mat);
142 if (n < 0 || cols < 0)
143 return isl_bool_error;
144 off = cols - n;
146 for (i = n - 1; i >= 0; --i) {
147 isl_bool known;
149 if (isl_int_is_zero(mat->row[pos][off + i]))
150 continue;
151 known = isl_local_div_is_known(local, i);
152 if (known < 0 || !known)
153 return known;
156 return isl_bool_true;
159 /* Does "local" have an explicit representation for all local variables?
161 isl_bool isl_local_divs_known(__isl_keep isl_local *local)
163 int i;
164 isl_size n;
166 n = isl_local_dim(local, isl_dim_div);
167 if (n < 0)
168 return isl_bool_error;
170 for (i = 0; i < n; ++i) {
171 isl_bool unknown = isl_local_div_is_marked_unknown(local, i);
172 if (unknown < 0 || unknown)
173 return isl_bool_not(unknown);
176 return isl_bool_true;
179 /* Compare two sets of local variables, defined over
180 * the same space.
182 * Return -1 if "local1" is "smaller" than "local2", 1 if "local1" is "greater"
183 * than "local2" and 0 if they are equal.
185 * The order is fairly arbitrary. We do "prefer" divs that only involve
186 * earlier dimensions in the sense that we consider matrices where
187 * the first differing div involves earlier dimensions to be smaller.
189 int isl_local_cmp(__isl_keep isl_local *local1, __isl_keep isl_local *local2)
191 int i;
192 int cmp;
193 isl_bool unknown1, unknown2;
194 int last1, last2;
195 isl_size n_col;
196 isl_mat *mat1 = local1;
197 isl_mat *mat2 = local2;
199 if (local1 == local2)
200 return 0;
201 if (!local1)
202 return -1;
203 if (!local2)
204 return 1;
206 if (mat1->n_row != mat2->n_row)
207 return mat1->n_row - mat2->n_row;
209 n_col = isl_mat_cols(mat1);
210 if (n_col < 0)
211 return -1;
212 for (i = 0; i < mat1->n_row; ++i) {
213 unknown1 = isl_local_div_is_marked_unknown(local1, i);
214 unknown2 = isl_local_div_is_marked_unknown(local2, i);
215 if (unknown1 && unknown2)
216 continue;
217 if (unknown1)
218 return 1;
219 if (unknown2)
220 return -1;
221 last1 = isl_seq_last_non_zero(mat1->row[i] + 1, n_col - 1);
222 last2 = isl_seq_last_non_zero(mat2->row[i] + 1, n_col - 1);
223 if (last1 != last2)
224 return last1 - last2;
225 cmp = isl_seq_cmp(mat1->row[i], mat2->row[i], n_col);
226 if (cmp != 0)
227 return cmp;
230 return 0;
233 /* Return the position of the variables of the given type
234 * within the sequence of variables of "local".
236 * Only the position of the local variables can be obtained.
237 * It is equal to the total number of variables minus
238 * the number of local variables.
240 isl_size isl_local_var_offset(__isl_keep isl_local *local,
241 enum isl_dim_type type)
243 isl_size n_div, n_all;
245 if (!local)
246 return isl_size_error;
247 if (type != isl_dim_div)
248 isl_die(isl_local_get_ctx(local), isl_error_unsupported,
249 "only the offset of the local variables "
250 "can be obtained", return isl_size_error);
252 n_div = isl_local_dim(local, isl_dim_div);
253 n_all = isl_local_dim(local, isl_dim_all);
254 if (n_div < 0 || n_all < 0)
255 return isl_size_error;
256 return n_all - n_div;
259 /* Reorder the columns of the given local variables according to the
260 * given reordering.
261 * The order of the local variables themselves is assumed not to change.
263 __isl_give isl_local *isl_local_reorder(__isl_take isl_local *local,
264 __isl_take isl_reordering *r)
266 isl_mat *div = local;
267 int i, j;
268 isl_mat *mat;
269 int extra;
271 if (!local || !r)
272 goto error;
274 extra = r->dst_len - r->src_len;
275 mat = isl_mat_alloc(div->ctx, div->n_row, div->n_col + extra);
276 if (!mat)
277 goto error;
279 for (i = 0; i < div->n_row; ++i) {
280 isl_seq_cpy(mat->row[i], div->row[i], 2);
281 isl_seq_clr(mat->row[i] + 2, mat->n_col - 2);
282 for (j = 0; j < r->src_len; ++j)
283 isl_int_set(mat->row[i][2 + r->pos[j]],
284 div->row[i][2 + j]);
287 isl_reordering_free(r);
288 isl_local_free(local);
289 return isl_local_alloc_from_mat(mat);
290 error:
291 isl_reordering_free(r);
292 isl_local_free(local);
293 return NULL;
296 /* Move the "n" variables starting at "src_pos" of "local" to "dst_pos".
298 * Moving local variables is not allowed.
300 __isl_give isl_local *isl_local_move_vars(__isl_take isl_local *local,
301 unsigned dst_pos, unsigned src_pos, unsigned n)
303 isl_mat *mat = local;
304 isl_size v_div;
306 v_div = isl_local_var_offset(local, isl_dim_div);
307 if (v_div < 0)
308 return isl_local_free(local);
309 if (n == 0)
310 return local;
312 if (dst_pos >= v_div || src_pos >= v_div)
313 isl_die(isl_local_get_ctx(local), isl_error_invalid,
314 "cannot move local variables",
315 return isl_local_free(local));
317 mat = isl_mat_move_cols(mat, 2 + dst_pos, 2 + src_pos, n);
319 return isl_local_alloc_from_mat(mat);
322 /* Does "local" depend on the specified variables?
324 * If the specified variables are local variables themselves,
325 * then only later local variables could possibly depend on them.
327 isl_bool isl_local_involves_vars(__isl_keep isl_local *local,
328 unsigned first, unsigned n)
330 isl_mat *mat = local;
331 int i, first_div;
332 isl_size v_div, n_div;
334 v_div = isl_local_var_offset(local, isl_dim_div);
335 n_div = isl_local_dim(local, isl_dim_div);
336 if (v_div < 0 || n_div < 0 ||
337 isl_local_check_range(local, isl_dim_all, first, n) < 0)
338 return isl_bool_error;
340 first_div = (first >= v_div) ? first - v_div + 1 : 0;
341 for (i = first_div; i < n_div; ++i) {
342 isl_bool unknown;
344 unknown = isl_local_div_is_marked_unknown(local, i);
345 if (unknown < 0)
346 return isl_bool_error;
347 if (unknown)
348 continue;
349 if (isl_seq_first_non_zero(mat->row[i] + 1 + 1 + first, n) >= 0)
350 return isl_bool_true;
353 return isl_bool_false;
356 /* Extend a vector "v" representing an integer point
357 * in the domain space of "local"
358 * to one that also includes values for the local variables.
359 * All local variables are required to have an explicit representation.
360 * If there are no local variables, then the point is not required
361 * to be integral.
363 __isl_give isl_vec *isl_local_extend_point_vec(__isl_keep isl_local *local,
364 __isl_take isl_vec *v)
366 isl_size dim, n_div, size;
367 isl_bool known;
368 isl_mat *mat = local;
370 if (!local || !v)
371 return isl_vec_free(v);
372 known = isl_local_divs_known(local);
373 if (known < 0)
374 return isl_vec_free(v);
375 if (!known)
376 isl_die(isl_local_get_ctx(local), isl_error_invalid,
377 "unknown local variables", return isl_vec_free(v));
378 dim = isl_local_dim(local, isl_dim_set);
379 n_div = isl_local_dim(local, isl_dim_div);
380 size = isl_vec_size(v);
381 if (dim < 0 || n_div < 0 || size < 0)
382 return isl_vec_free(v);
383 if (size != 1 + dim)
384 isl_die(isl_local_get_ctx(local), isl_error_invalid,
385 "incorrect size", return isl_vec_free(v));
386 if (n_div == 0)
387 return v;
388 if (!isl_int_is_one(v->el[0]))
389 isl_die(isl_local_get_ctx(local), isl_error_invalid,
390 "expecting integer point", return isl_vec_free(v));
392 int i;
393 v = isl_vec_add_els(v, n_div);
394 if (!v)
395 return NULL;
397 for (i = 0; i < n_div; ++i) {
398 isl_seq_inner_product(mat->row[i] + 1, v->el,
399 1 + dim + i, &v->el[1+dim+i]);
400 isl_int_fdiv_q(v->el[1+dim+i], v->el[1+dim+i],
401 mat->row[i][0]);
405 return v;