nexmon – Blame information for rev 1
?pathlinks?
Rev | Author | Line No. | Line |
---|---|---|---|
1 | office | 1 | /* |
2 | * Copyright 2008-2009 Katholieke Universiteit Leuven |
||
3 | * |
||
4 | * Use of this software is governed by the GNU LGPLv2.1 license |
||
5 | * |
||
6 | * Written by Sven Verdoolaege, K.U.Leuven, Departement |
||
7 | * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium |
||
8 | */ |
||
9 | |||
10 | #include <isl_map_private.h> |
||
11 | #include <isl/seq.h> |
||
12 | #include <isl/set.h> |
||
13 | #include <isl/map.h> |
||
14 | #include "isl_tab.h" |
||
15 | #include <isl_point_private.h> |
||
16 | |||
17 | static void expand_constraint(isl_vec *v, unsigned dim, |
||
18 | isl_int *c, int *div_map, unsigned n_div) |
||
19 | { |
||
20 | int i; |
||
21 | |||
22 | isl_seq_cpy(v->el, c, 1 + dim); |
||
23 | isl_seq_clr(v->el + 1 + dim, v->size - (1 + dim)); |
||
24 | |||
25 | for (i = 0; i < n_div; ++i) |
||
26 | isl_int_set(v->el[1 + dim + div_map[i]], c[1 + dim + i]); |
||
27 | } |
||
28 | |||
29 | /* Add all constraints of bmap to tab. The equalities of bmap |
||
30 | * are added as a pair of inequalities. |
||
31 | */ |
||
32 | static int tab_add_constraints(struct isl_tab *tab, |
||
33 | __isl_keep isl_basic_map *bmap, int *div_map) |
||
34 | { |
||
35 | int i; |
||
36 | unsigned dim; |
||
37 | unsigned tab_total; |
||
38 | unsigned bmap_total; |
||
39 | isl_vec *v; |
||
40 | |||
41 | if (!tab || !bmap) |
||
42 | return -1; |
||
43 | |||
44 | tab_total = isl_basic_map_total_dim(tab->bmap); |
||
45 | bmap_total = isl_basic_map_total_dim(bmap); |
||
46 | dim = isl_space_dim(tab->bmap->dim, isl_dim_all); |
||
47 | |||
48 | if (isl_tab_extend_cons(tab, 2 * bmap->n_eq + bmap->n_ineq) < 0) |
||
49 | return -1; |
||
50 | |||
51 | v = isl_vec_alloc(bmap->ctx, 1 + tab_total); |
||
52 | if (!v) |
||
53 | return -1; |
||
54 | |||
55 | for (i = 0; i < bmap->n_eq; ++i) { |
||
56 | expand_constraint(v, dim, bmap->eq[i], div_map, bmap->n_div); |
||
57 | if (isl_tab_add_ineq(tab, v->el) < 0) |
||
58 | goto error; |
||
59 | isl_seq_neg(bmap->eq[i], bmap->eq[i], 1 + bmap_total); |
||
60 | expand_constraint(v, dim, bmap->eq[i], div_map, bmap->n_div); |
||
61 | if (isl_tab_add_ineq(tab, v->el) < 0) |
||
62 | goto error; |
||
63 | isl_seq_neg(bmap->eq[i], bmap->eq[i], 1 + bmap_total); |
||
64 | if (tab->empty) |
||
65 | break; |
||
66 | } |
||
67 | |||
68 | for (i = 0; i < bmap->n_ineq; ++i) { |
||
69 | expand_constraint(v, dim, bmap->ineq[i], div_map, bmap->n_div); |
||
70 | if (isl_tab_add_ineq(tab, v->el) < 0) |
||
71 | goto error; |
||
72 | if (tab->empty) |
||
73 | break; |
||
74 | } |
||
75 | |||
76 | isl_vec_free(v); |
||
77 | return 0; |
||
78 | error: |
||
79 | isl_vec_free(v); |
||
80 | return -1; |
||
81 | } |
||
82 | |||
83 | /* Add a specific constraint of bmap (or its opposite) to tab. |
||
84 | * The position of the constraint is specified by "c", where |
||
85 | * the equalities of bmap are counted twice, once for the inequality |
||
86 | * that is equal to the equality, and once for its negation. |
||
87 | */ |
||
88 | static int tab_add_constraint(struct isl_tab *tab, |
||
89 | __isl_keep isl_basic_map *bmap, int *div_map, int c, int oppose) |
||
90 | { |
||
91 | unsigned dim; |
||
92 | unsigned tab_total; |
||
93 | unsigned bmap_total; |
||
94 | isl_vec *v; |
||
95 | int r; |
||
96 | |||
97 | if (!tab || !bmap) |
||
98 | return -1; |
||
99 | |||
100 | tab_total = isl_basic_map_total_dim(tab->bmap); |
||
101 | bmap_total = isl_basic_map_total_dim(bmap); |
||
102 | dim = isl_space_dim(tab->bmap->dim, isl_dim_all); |
||
103 | |||
104 | v = isl_vec_alloc(bmap->ctx, 1 + tab_total); |
||
105 | if (!v) |
||
106 | return -1; |
||
107 | |||
108 | if (c < 2 * bmap->n_eq) { |
||
109 | if ((c % 2) != oppose) |
||
110 | isl_seq_neg(bmap->eq[c/2], bmap->eq[c/2], |
||
111 | 1 + bmap_total); |
||
112 | if (oppose) |
||
113 | isl_int_sub_ui(bmap->eq[c/2][0], bmap->eq[c/2][0], 1); |
||
114 | expand_constraint(v, dim, bmap->eq[c/2], div_map, bmap->n_div); |
||
115 | r = isl_tab_add_ineq(tab, v->el); |
||
116 | if (oppose) |
||
117 | isl_int_add_ui(bmap->eq[c/2][0], bmap->eq[c/2][0], 1); |
||
118 | if ((c % 2) != oppose) |
||
119 | isl_seq_neg(bmap->eq[c/2], bmap->eq[c/2], |
||
120 | 1 + bmap_total); |
||
121 | } else { |
||
122 | c -= 2 * bmap->n_eq; |
||
123 | if (oppose) { |
||
124 | isl_seq_neg(bmap->ineq[c], bmap->ineq[c], |
||
125 | 1 + bmap_total); |
||
126 | isl_int_sub_ui(bmap->ineq[c][0], bmap->ineq[c][0], 1); |
||
127 | } |
||
128 | expand_constraint(v, dim, bmap->ineq[c], div_map, bmap->n_div); |
||
129 | r = isl_tab_add_ineq(tab, v->el); |
||
130 | if (oppose) { |
||
131 | isl_int_add_ui(bmap->ineq[c][0], bmap->ineq[c][0], 1); |
||
132 | isl_seq_neg(bmap->ineq[c], bmap->ineq[c], |
||
133 | 1 + bmap_total); |
||
134 | } |
||
135 | } |
||
136 | |||
137 | isl_vec_free(v); |
||
138 | return r; |
||
139 | } |
||
140 | |||
141 | static int tab_add_divs(struct isl_tab *tab, __isl_keep isl_basic_map *bmap, |
||
142 | int **div_map) |
||
143 | { |
||
144 | int i, j; |
||
145 | struct isl_vec *vec; |
||
146 | unsigned total; |
||
147 | unsigned dim; |
||
148 | |||
149 | if (!bmap) |
||
150 | return -1; |
||
151 | if (!bmap->n_div) |
||
152 | return 0; |
||
153 | |||
154 | if (!*div_map) |
||
155 | *div_map = isl_alloc_array(bmap->ctx, int, bmap->n_div); |
||
156 | if (!*div_map) |
||
157 | return -1; |
||
158 | |||
159 | total = isl_basic_map_total_dim(tab->bmap); |
||
160 | dim = total - tab->bmap->n_div; |
||
161 | vec = isl_vec_alloc(bmap->ctx, 2 + total + bmap->n_div); |
||
162 | if (!vec) |
||
163 | return -1; |
||
164 | |||
165 | for (i = 0; i < bmap->n_div; ++i) { |
||
166 | isl_seq_cpy(vec->el, bmap->div[i], 2 + dim); |
||
167 | isl_seq_clr(vec->el + 2 + dim, tab->bmap->n_div); |
||
168 | for (j = 0; j < i; ++j) |
||
169 | isl_int_set(vec->el[2 + dim + (*div_map)[j]], |
||
170 | bmap->div[i][2 + dim + j]); |
||
171 | for (j = 0; j < tab->bmap->n_div; ++j) |
||
172 | if (isl_seq_eq(tab->bmap->div[j], |
||
173 | vec->el, 2 + dim + tab->bmap->n_div)) |
||
174 | break; |
||
175 | (*div_map)[i] = j; |
||
176 | if (j == tab->bmap->n_div) { |
||
177 | vec->size = 2 + dim + tab->bmap->n_div; |
||
178 | if (isl_tab_add_div(tab, vec, NULL, NULL) < 0) |
||
179 | goto error; |
||
180 | } |
||
181 | } |
||
182 | |||
183 | isl_vec_free(vec); |
||
184 | |||
185 | return 0; |
||
186 | error: |
||
187 | isl_vec_free(vec); |
||
188 | |||
189 | return -1; |
||
190 | } |
||
191 | |||
192 | /* Freeze all constraints of tableau tab. |
||
193 | */ |
||
194 | static int tab_freeze_constraints(struct isl_tab *tab) |
||
195 | { |
||
196 | int i; |
||
197 | |||
198 | for (i = 0; i < tab->n_con; ++i) |
||
199 | if (isl_tab_freeze_constraint(tab, i) < 0) |
||
200 | return -1; |
||
201 | |||
202 | return 0; |
||
203 | } |
||
204 | |||
205 | /* Check for redundant constraints starting at offset. |
||
206 | * Put the indices of the redundant constraints in index |
||
207 | * and return the number of redundant constraints. |
||
208 | */ |
||
209 | static int n_non_redundant(isl_ctx *ctx, struct isl_tab *tab, |
||
210 | int offset, int **index) |
||
211 | { |
||
212 | int i, n; |
||
213 | int n_test = tab->n_con - offset; |
||
214 | |||
215 | if (isl_tab_detect_redundant(tab) < 0) |
||
216 | return -1; |
||
217 | |||
218 | if (!*index) |
||
219 | *index = isl_alloc_array(ctx, int, n_test); |
||
220 | if (!*index) |
||
221 | return -1; |
||
222 | |||
223 | for (n = 0, i = 0; i < n_test; ++i) { |
||
224 | int r; |
||
225 | r = isl_tab_is_redundant(tab, offset + i); |
||
226 | if (r < 0) |
||
227 | return -1; |
||
228 | if (r) |
||
229 | continue; |
||
230 | (*index)[n++] = i; |
||
231 | } |
||
232 | |||
233 | return n; |
||
234 | } |
||
235 | |||
236 | /* basic_map_collect_diff calls add on each of the pieces of |
||
237 | * the set difference between bmap and map until the add method |
||
238 | * return a negative value. |
||
239 | */ |
||
240 | struct isl_diff_collector { |
||
241 | int (*add)(struct isl_diff_collector *dc, |
||
242 | __isl_take isl_basic_map *bmap); |
||
243 | }; |
||
244 | |||
245 | /* Compute the set difference between bmap and map and call |
||
246 | * dc->add on each of the piece until this function returns |
||
247 | * a negative value. |
||
248 | * Return 0 on success and -1 on error. dc->add returning |
||
249 | * a negative value is treated as an error, but the calling |
||
250 | * function can interpret the results based on the state of dc. |
||
251 | * |
||
252 | * Assumes that map has known divs. |
||
253 | * |
||
254 | * The difference is computed by a backtracking algorithm. |
||
255 | * Each level corresponds to a basic map in "map". |
||
256 | * When a node in entered for the first time, we check |
||
257 | * if the corresonding basic map intersects the current piece |
||
258 | * of "bmap". If not, we move to the next level. |
||
259 | * Otherwise, we split the current piece into as many |
||
260 | * pieces as there are non-redundant constraints of the current |
||
261 | * basic map in the intersection. Each of these pieces is |
||
262 | * handled by a child of the current node. |
||
263 | * In particular, if there are n non-redundant constraints, |
||
264 | * then for each 0 <= i < n, a piece is cut off by adding |
||
265 | * constraints 0 <= j < i and adding the opposite of constraint i. |
||
266 | * If there are no non-redundant constraints, meaning that the current |
||
267 | * piece is a subset of the current basic map, then we simply backtrack. |
||
268 | * |
||
269 | * In the leaves, we check if the remaining piece has any integer points |
||
270 | * and if so, pass it along to dc->add. As a special case, if nothing |
||
271 | * has been removed when we end up in a leaf, we simply pass along |
||
272 | * the original basic map. |
||
273 | */ |
||
274 | static int basic_map_collect_diff(__isl_take isl_basic_map *bmap, |
||
275 | __isl_take isl_map *map, struct isl_diff_collector *dc) |
||
276 | { |
||
277 | int i; |
||
278 | int modified; |
||
279 | int level; |
||
280 | int init; |
||
281 | int empty; |
||
282 | isl_ctx *ctx; |
||
283 | struct isl_tab *tab = NULL; |
||
284 | struct isl_tab_undo **snap = NULL; |
||
285 | int *k = NULL; |
||
286 | int *n = NULL; |
||
287 | int **index = NULL; |
||
288 | int **div_map = NULL; |
||
289 | |||
290 | empty = isl_basic_map_is_empty(bmap); |
||
291 | if (empty) { |
||
292 | isl_basic_map_free(bmap); |
||
293 | isl_map_free(map); |
||
294 | return empty < 0 ? -1 : 0; |
||
295 | } |
||
296 | |||
297 | bmap = isl_basic_map_cow(bmap); |
||
298 | map = isl_map_cow(map); |
||
299 | |||
300 | if (!bmap || !map) |
||
301 | goto error; |
||
302 | |||
303 | ctx = map->ctx; |
||
304 | snap = isl_alloc_array(map->ctx, struct isl_tab_undo *, map->n); |
||
305 | k = isl_alloc_array(map->ctx, int, map->n); |
||
306 | n = isl_alloc_array(map->ctx, int, map->n); |
||
307 | index = isl_calloc_array(map->ctx, int *, map->n); |
||
308 | div_map = isl_calloc_array(map->ctx, int *, map->n); |
||
309 | if (!snap || !k || !n || !index || !div_map) |
||
310 | goto error; |
||
311 | |||
312 | bmap = isl_basic_map_order_divs(bmap); |
||
313 | map = isl_map_order_divs(map); |
||
314 | |||
315 | tab = isl_tab_from_basic_map(bmap, 1); |
||
316 | |||
317 | modified = 0; |
||
318 | level = 0; |
||
319 | init = 1; |
||
320 | |||
321 | while (level >= 0) { |
||
322 | if (level >= map->n) { |
||
323 | int empty; |
||
324 | struct isl_basic_map *bm; |
||
325 | if (!modified) { |
||
326 | if (dc->add(dc, isl_basic_map_copy(bmap)) < 0) |
||
327 | goto error; |
||
328 | break; |
||
329 | } |
||
330 | bm = isl_basic_map_copy(tab->bmap); |
||
331 | bm = isl_basic_map_cow(bm); |
||
332 | bm = isl_basic_map_update_from_tab(bm, tab); |
||
333 | bm = isl_basic_map_simplify(bm); |
||
334 | bm = isl_basic_map_finalize(bm); |
||
335 | empty = isl_basic_map_is_empty(bm); |
||
336 | if (empty) |
||
337 | isl_basic_map_free(bm); |
||
338 | else if (dc->add(dc, bm) < 0) |
||
339 | goto error; |
||
340 | if (empty < 0) |
||
341 | goto error; |
||
342 | level--; |
||
343 | init = 0; |
||
344 | continue; |
||
345 | } |
||
346 | if (init) { |
||
347 | int offset; |
||
348 | struct isl_tab_undo *snap2; |
||
349 | snap2 = isl_tab_snap(tab); |
||
350 | if (tab_add_divs(tab, map->p[level], |
||
351 | &div_map[level]) < 0) |
||
352 | goto error; |
||
353 | offset = tab->n_con; |
||
354 | snap[level] = isl_tab_snap(tab); |
||
355 | if (tab_freeze_constraints(tab) < 0) |
||
356 | goto error; |
||
357 | if (tab_add_constraints(tab, map->p[level], |
||
358 | div_map[level]) < 0) |
||
359 | goto error; |
||
360 | k[level] = 0; |
||
361 | n[level] = 0; |
||
362 | if (tab->empty) { |
||
363 | if (isl_tab_rollback(tab, snap2) < 0) |
||
364 | goto error; |
||
365 | level++; |
||
366 | continue; |
||
367 | } |
||
368 | modified = 1; |
||
369 | n[level] = n_non_redundant(ctx, tab, offset, |
||
370 | &index[level]); |
||
371 | if (n[level] < 0) |
||
372 | goto error; |
||
373 | if (n[level] == 0) { |
||
374 | level--; |
||
375 | init = 0; |
||
376 | continue; |
||
377 | } |
||
378 | if (isl_tab_rollback(tab, snap[level]) < 0) |
||
379 | goto error; |
||
380 | if (tab_add_constraint(tab, map->p[level], |
||
381 | div_map[level], index[level][0], 1) < 0) |
||
382 | goto error; |
||
383 | level++; |
||
384 | continue; |
||
385 | } else { |
||
386 | if (k[level] + 1 >= n[level]) { |
||
387 | level--; |
||
388 | continue; |
||
389 | } |
||
390 | if (isl_tab_rollback(tab, snap[level]) < 0) |
||
391 | goto error; |
||
392 | if (tab_add_constraint(tab, map->p[level], |
||
393 | div_map[level], |
||
394 | index[level][k[level]], 0) < 0) |
||
395 | goto error; |
||
396 | snap[level] = isl_tab_snap(tab); |
||
397 | k[level]++; |
||
398 | if (tab_add_constraint(tab, map->p[level], |
||
399 | div_map[level], |
||
400 | index[level][k[level]], 1) < 0) |
||
401 | goto error; |
||
402 | level++; |
||
403 | init = 1; |
||
404 | continue; |
||
405 | } |
||
406 | } |
||
407 | |||
408 | isl_tab_free(tab); |
||
409 | free(snap); |
||
410 | free(n); |
||
411 | free(k); |
||
412 | for (i = 0; index && i < map->n; ++i) |
||
413 | free(index[i]); |
||
414 | free(index); |
||
415 | for (i = 0; div_map && i < map->n; ++i) |
||
416 | free(div_map[i]); |
||
417 | free(div_map); |
||
418 | |||
419 | isl_basic_map_free(bmap); |
||
420 | isl_map_free(map); |
||
421 | |||
422 | return 0; |
||
423 | error: |
||
424 | isl_tab_free(tab); |
||
425 | free(snap); |
||
426 | free(n); |
||
427 | free(k); |
||
428 | for (i = 0; index && i < map->n; ++i) |
||
429 | free(index[i]); |
||
430 | free(index); |
||
431 | for (i = 0; div_map && i < map->n; ++i) |
||
432 | free(div_map[i]); |
||
433 | free(div_map); |
||
434 | isl_basic_map_free(bmap); |
||
435 | isl_map_free(map); |
||
436 | return -1; |
||
437 | } |
||
438 | |||
439 | /* A diff collector that actually collects all parts of the |
||
440 | * set difference in the field diff. |
||
441 | */ |
||
442 | struct isl_subtract_diff_collector { |
||
443 | struct isl_diff_collector dc; |
||
444 | struct isl_map *diff; |
||
445 | }; |
||
446 | |||
447 | /* isl_subtract_diff_collector callback. |
||
448 | */ |
||
449 | static int basic_map_subtract_add(struct isl_diff_collector *dc, |
||
450 | __isl_take isl_basic_map *bmap) |
||
451 | { |
||
452 | struct isl_subtract_diff_collector *sdc; |
||
453 | sdc = (struct isl_subtract_diff_collector *)dc; |
||
454 | |||
455 | sdc->diff = isl_map_union_disjoint(sdc->diff, |
||
456 | isl_map_from_basic_map(bmap)); |
||
457 | |||
458 | return sdc->diff ? 0 : -1; |
||
459 | } |
||
460 | |||
461 | /* Return the set difference between bmap and map. |
||
462 | */ |
||
463 | static __isl_give isl_map *basic_map_subtract(__isl_take isl_basic_map *bmap, |
||
464 | __isl_take isl_map *map) |
||
465 | { |
||
466 | struct isl_subtract_diff_collector sdc; |
||
467 | sdc.dc.add = &basic_map_subtract_add; |
||
468 | sdc.diff = isl_map_empty_like_basic_map(bmap); |
||
469 | if (basic_map_collect_diff(bmap, map, &sdc.dc) < 0) { |
||
470 | isl_map_free(sdc.diff); |
||
471 | sdc.diff = NULL; |
||
472 | } |
||
473 | return sdc.diff; |
||
474 | } |
||
475 | |||
476 | /* Return the set difference between map1 and map2. |
||
477 | * (U_i A_i) \ (U_j B_j) is computed as U_i (A_i \ (U_j B_j)) |
||
478 | */ |
||
479 | static __isl_give isl_map *map_subtract( __isl_take isl_map *map1, |
||
480 | __isl_take isl_map *map2) |
||
481 | { |
||
482 | int i; |
||
483 | struct isl_map *diff; |
||
484 | |||
485 | if (!map1 || !map2) |
||
486 | goto error; |
||
487 | |||
488 | isl_assert(map1->ctx, isl_space_is_equal(map1->dim, map2->dim), goto error); |
||
489 | |||
490 | if (isl_map_is_empty(map2)) { |
||
491 | isl_map_free(map2); |
||
492 | return map1; |
||
493 | } |
||
494 | |||
495 | map1 = isl_map_compute_divs(map1); |
||
496 | map2 = isl_map_compute_divs(map2); |
||
497 | if (!map1 || !map2) |
||
498 | goto error; |
||
499 | |||
500 | map1 = isl_map_remove_empty_parts(map1); |
||
501 | map2 = isl_map_remove_empty_parts(map2); |
||
502 | |||
503 | diff = isl_map_empty_like(map1); |
||
504 | for (i = 0; i < map1->n; ++i) { |
||
505 | struct isl_map *d; |
||
506 | d = basic_map_subtract(isl_basic_map_copy(map1->p[i]), |
||
507 | isl_map_copy(map2)); |
||
508 | if (ISL_F_ISSET(map1, ISL_MAP_DISJOINT)) |
||
509 | diff = isl_map_union_disjoint(diff, d); |
||
510 | else |
||
511 | diff = isl_map_union(diff, d); |
||
512 | } |
||
513 | |||
514 | isl_map_free(map1); |
||
515 | isl_map_free(map2); |
||
516 | |||
517 | return diff; |
||
518 | error: |
||
519 | isl_map_free(map1); |
||
520 | isl_map_free(map2); |
||
521 | return NULL; |
||
522 | } |
||
523 | |||
524 | __isl_give isl_map *isl_map_subtract( __isl_take isl_map *map1, |
||
525 | __isl_take isl_map *map2) |
||
526 | { |
||
527 | return isl_map_align_params_map_map_and(map1, map2, &map_subtract); |
||
528 | } |
||
529 | |||
530 | struct isl_set *isl_set_subtract(struct isl_set *set1, struct isl_set *set2) |
||
531 | { |
||
532 | return (struct isl_set *) |
||
533 | isl_map_subtract( |
||
534 | (struct isl_map *)set1, (struct isl_map *)set2); |
||
535 | } |
||
536 | |||
537 | /* Remove the elements of "dom" from the domain of "map". |
||
538 | */ |
||
539 | static __isl_give isl_map *map_subtract_domain(__isl_take isl_map *map, |
||
540 | __isl_take isl_set *dom) |
||
541 | { |
||
542 | isl_map *ext_dom; |
||
543 | |||
544 | if (!isl_map_compatible_domain(map, dom)) |
||
545 | isl_die(isl_set_get_ctx(dom), isl_error_invalid, |
||
546 | "incompatible spaces", goto error); |
||
547 | |||
548 | ext_dom = isl_map_universe(isl_map_get_space(map)); |
||
549 | ext_dom = isl_map_intersect_domain(ext_dom, dom); |
||
550 | return isl_map_subtract(map, ext_dom); |
||
551 | error: |
||
552 | isl_map_free(map); |
||
553 | isl_set_free(dom); |
||
554 | return NULL; |
||
555 | } |
||
556 | |||
557 | __isl_give isl_map *isl_map_subtract_domain(__isl_take isl_map *map, |
||
558 | __isl_take isl_set *dom) |
||
559 | { |
||
560 | return isl_map_align_params_map_map_and(map, dom, &map_subtract_domain); |
||
561 | } |
||
562 | |||
563 | /* Remove the elements of "dom" from the range of "map". |
||
564 | */ |
||
565 | static __isl_give isl_map *map_subtract_range(__isl_take isl_map *map, |
||
566 | __isl_take isl_set *dom) |
||
567 | { |
||
568 | isl_map *ext_dom; |
||
569 | |||
570 | if (!isl_map_compatible_range(map, dom)) |
||
571 | isl_die(isl_set_get_ctx(dom), isl_error_invalid, |
||
572 | "incompatible spaces", goto error); |
||
573 | |||
574 | ext_dom = isl_map_universe(isl_map_get_space(map)); |
||
575 | ext_dom = isl_map_intersect_range(ext_dom, dom); |
||
576 | return isl_map_subtract(map, ext_dom); |
||
577 | error: |
||
578 | isl_map_free(map); |
||
579 | isl_set_free(dom); |
||
580 | return NULL; |
||
581 | } |
||
582 | |||
583 | __isl_give isl_map *isl_map_subtract_range(__isl_take isl_map *map, |
||
584 | __isl_take isl_set *dom) |
||
585 | { |
||
586 | return isl_map_align_params_map_map_and(map, dom, &map_subtract_range); |
||
587 | } |
||
588 | |||
589 | /* A diff collector that aborts as soon as its add function is called, |
||
590 | * setting empty to 0. |
||
591 | */ |
||
592 | struct isl_is_empty_diff_collector { |
||
593 | struct isl_diff_collector dc; |
||
594 | int empty; |
||
595 | }; |
||
596 | |||
597 | /* isl_is_empty_diff_collector callback. |
||
598 | */ |
||
599 | static int basic_map_is_empty_add(struct isl_diff_collector *dc, |
||
600 | __isl_take isl_basic_map *bmap) |
||
601 | { |
||
602 | struct isl_is_empty_diff_collector *edc; |
||
603 | edc = (struct isl_is_empty_diff_collector *)dc; |
||
604 | |||
605 | edc->empty = 0; |
||
606 | |||
607 | isl_basic_map_free(bmap); |
||
608 | return -1; |
||
609 | } |
||
610 | |||
611 | /* Check if bmap \ map is empty by computing this set difference |
||
612 | * and breaking off as soon as the difference is known to be non-empty. |
||
613 | */ |
||
614 | static int basic_map_diff_is_empty(__isl_keep isl_basic_map *bmap, |
||
615 | __isl_keep isl_map *map) |
||
616 | { |
||
617 | int r; |
||
618 | struct isl_is_empty_diff_collector edc; |
||
619 | |||
620 | r = isl_basic_map_plain_is_empty(bmap); |
||
621 | if (r) |
||
622 | return r; |
||
623 | |||
624 | edc.dc.add = &basic_map_is_empty_add; |
||
625 | edc.empty = 1; |
||
626 | r = basic_map_collect_diff(isl_basic_map_copy(bmap), |
||
627 | isl_map_copy(map), &edc.dc); |
||
628 | if (!edc.empty) |
||
629 | return 0; |
||
630 | |||
631 | return r < 0 ? -1 : 1; |
||
632 | } |
||
633 | |||
634 | /* Check if map1 \ map2 is empty by checking if the set difference is empty |
||
635 | * for each of the basic maps in map1. |
||
636 | */ |
||
637 | static int map_diff_is_empty(__isl_keep isl_map *map1, __isl_keep isl_map *map2) |
||
638 | { |
||
639 | int i; |
||
640 | int is_empty = 1; |
||
641 | |||
642 | if (!map1 || !map2) |
||
643 | return -1; |
||
644 | |||
645 | for (i = 0; i < map1->n; ++i) { |
||
646 | is_empty = basic_map_diff_is_empty(map1->p[i], map2); |
||
647 | if (is_empty < 0 || !is_empty) |
||
648 | break; |
||
649 | } |
||
650 | |||
651 | return is_empty; |
||
652 | } |
||
653 | |||
654 | /* Return 1 if "bmap" contains a single element. |
||
655 | */ |
||
656 | int isl_basic_map_plain_is_singleton(__isl_keep isl_basic_map *bmap) |
||
657 | { |
||
658 | if (!bmap) |
||
659 | return -1; |
||
660 | if (bmap->n_div) |
||
661 | return 0; |
||
662 | if (bmap->n_ineq) |
||
663 | return 0; |
||
664 | return bmap->n_eq == isl_basic_map_total_dim(bmap); |
||
665 | } |
||
666 | |||
667 | /* Return 1 if "map" contains a single element. |
||
668 | */ |
||
669 | int isl_map_plain_is_singleton(__isl_keep isl_map *map) |
||
670 | { |
||
671 | if (!map) |
||
672 | return -1; |
||
673 | if (map->n != 1) |
||
674 | return 0; |
||
675 | |||
676 | return isl_basic_map_plain_is_singleton(map->p[0]); |
||
677 | } |
||
678 | |||
679 | /* Given a singleton basic map, extract the single element |
||
680 | * as an isl_point. |
||
681 | */ |
||
682 | static __isl_give isl_point *singleton_extract_point( |
||
683 | __isl_keep isl_basic_map *bmap) |
||
684 | { |
||
685 | int j; |
||
686 | unsigned dim; |
||
687 | struct isl_vec *point; |
||
688 | isl_int m; |
||
689 | |||
690 | if (!bmap) |
||
691 | return NULL; |
||
692 | |||
693 | dim = isl_basic_map_total_dim(bmap); |
||
694 | isl_assert(bmap->ctx, bmap->n_eq == dim, return NULL); |
||
695 | point = isl_vec_alloc(bmap->ctx, 1 + dim); |
||
696 | if (!point) |
||
697 | return NULL; |
||
698 | |||
699 | isl_int_init(m); |
||
700 | |||
701 | isl_int_set_si(point->el[0], 1); |
||
702 | for (j = 0; j < bmap->n_eq; ++j) { |
||
703 | int i = dim - 1 - j; |
||
704 | isl_assert(bmap->ctx, |
||
705 | isl_seq_first_non_zero(bmap->eq[j] + 1, i) == -1, |
||
706 | goto error); |
||
707 | isl_assert(bmap->ctx, |
||
708 | isl_int_is_one(bmap->eq[j][1 + i]) || |
||
709 | isl_int_is_negone(bmap->eq[j][1 + i]), |
||
710 | goto error); |
||
711 | isl_assert(bmap->ctx, |
||
712 | isl_seq_first_non_zero(bmap->eq[j]+1+i+1, dim-i-1) == -1, |
||
713 | goto error); |
||
714 | |||
715 | isl_int_gcd(m, point->el[0], bmap->eq[j][1 + i]); |
||
716 | isl_int_divexact(m, bmap->eq[j][1 + i], m); |
||
717 | isl_int_abs(m, m); |
||
718 | isl_seq_scale(point->el, point->el, m, 1 + i); |
||
719 | isl_int_divexact(m, point->el[0], bmap->eq[j][1 + i]); |
||
720 | isl_int_neg(m, m); |
||
721 | isl_int_mul(point->el[1 + i], m, bmap->eq[j][0]); |
||
722 | } |
||
723 | |||
724 | isl_int_clear(m); |
||
725 | return isl_point_alloc(isl_basic_map_get_space(bmap), point); |
||
726 | error: |
||
727 | isl_int_clear(m); |
||
728 | isl_vec_free(point); |
||
729 | return NULL; |
||
730 | } |
||
731 | |||
732 | /* Return 1 is the singleton map "map1" is a subset of "map2", |
||
733 | * i.e., if the single element of "map1" is also an element of "map2". |
||
734 | * Assumes "map2" has known divs. |
||
735 | */ |
||
736 | static int map_is_singleton_subset(__isl_keep isl_map *map1, |
||
737 | __isl_keep isl_map *map2) |
||
738 | { |
||
739 | int i; |
||
740 | int is_subset = 0; |
||
741 | struct isl_point *point; |
||
742 | |||
743 | if (!map1 || !map2) |
||
744 | return -1; |
||
745 | if (map1->n != 1) |
||
746 | return -1; |
||
747 | |||
748 | point = singleton_extract_point(map1->p[0]); |
||
749 | if (!point) |
||
750 | return -1; |
||
751 | |||
752 | for (i = 0; i < map2->n; ++i) { |
||
753 | is_subset = isl_basic_map_contains_point(map2->p[i], point); |
||
754 | if (is_subset) |
||
755 | break; |
||
756 | } |
||
757 | |||
758 | isl_point_free(point); |
||
759 | return is_subset; |
||
760 | } |
||
761 | |||
762 | static int map_is_subset(__isl_keep isl_map *map1, __isl_keep isl_map *map2) |
||
763 | { |
||
764 | int is_subset = 0; |
||
765 | |||
766 | if (!map1 || !map2) |
||
767 | return -1; |
||
768 | |||
769 | if (!isl_map_has_equal_space(map1, map2)) |
||
770 | return 0; |
||
771 | |||
772 | if (isl_map_is_empty(map1)) |
||
773 | return 1; |
||
774 | |||
775 | if (isl_map_is_empty(map2)) |
||
776 | return 0; |
||
777 | |||
778 | if (isl_map_plain_is_universe(map2)) |
||
779 | return 1; |
||
780 | |||
781 | map2 = isl_map_compute_divs(isl_map_copy(map2)); |
||
782 | if (isl_map_plain_is_singleton(map1)) { |
||
783 | is_subset = map_is_singleton_subset(map1, map2); |
||
784 | isl_map_free(map2); |
||
785 | return is_subset; |
||
786 | } |
||
787 | is_subset = map_diff_is_empty(map1, map2); |
||
788 | isl_map_free(map2); |
||
789 | |||
790 | return is_subset; |
||
791 | } |
||
792 | |||
793 | int isl_map_is_subset(__isl_keep isl_map *map1, __isl_keep isl_map *map2) |
||
794 | { |
||
795 | return isl_map_align_params_map_map_and_test(map1, map2, |
||
796 | &map_is_subset); |
||
797 | } |
||
798 | |||
799 | int isl_set_is_subset(struct isl_set *set1, struct isl_set *set2) |
||
800 | { |
||
801 | return isl_map_is_subset( |
||
802 | (struct isl_map *)set1, (struct isl_map *)set2); |
||
803 | } |
||
804 | |||
805 | __isl_give isl_map *isl_map_make_disjoint(__isl_take isl_map *map) |
||
806 | { |
||
807 | int i; |
||
808 | struct isl_subtract_diff_collector sdc; |
||
809 | sdc.dc.add = &basic_map_subtract_add; |
||
810 | |||
811 | if (!map) |
||
812 | return NULL; |
||
813 | if (ISL_F_ISSET(map, ISL_MAP_DISJOINT)) |
||
814 | return map; |
||
815 | if (map->n <= 1) |
||
816 | return map; |
||
817 | |||
818 | map = isl_map_compute_divs(map); |
||
819 | map = isl_map_remove_empty_parts(map); |
||
820 | |||
821 | if (!map || map->n <= 1) |
||
822 | return map; |
||
823 | |||
824 | sdc.diff = isl_map_from_basic_map(isl_basic_map_copy(map->p[0])); |
||
825 | |||
826 | for (i = 1; i < map->n; ++i) { |
||
827 | struct isl_basic_map *bmap = isl_basic_map_copy(map->p[i]); |
||
828 | struct isl_map *copy = isl_map_copy(sdc.diff); |
||
829 | if (basic_map_collect_diff(bmap, copy, &sdc.dc) < 0) { |
||
830 | isl_map_free(sdc.diff); |
||
831 | sdc.diff = NULL; |
||
832 | break; |
||
833 | } |
||
834 | } |
||
835 | |||
836 | isl_map_free(map); |
||
837 | |||
838 | return sdc.diff; |
||
839 | } |
||
840 | |||
841 | __isl_give isl_set *isl_set_make_disjoint(__isl_take isl_set *set) |
||
842 | { |
||
843 | return (struct isl_set *)isl_map_make_disjoint((struct isl_map *)set); |
||
844 | } |
||
845 | |||
846 | __isl_give isl_map *isl_map_complement(__isl_take isl_map *map) |
||
847 | { |
||
848 | isl_map *universe; |
||
849 | |||
850 | if (!map) |
||
851 | return NULL; |
||
852 | |||
853 | universe = isl_map_universe(isl_map_get_space(map)); |
||
854 | |||
855 | return isl_map_subtract(universe, map); |
||
856 | } |
||
857 | |||
858 | __isl_give isl_set *isl_set_complement(__isl_take isl_set *set) |
||
859 | { |
||
860 | return isl_map_complement(set); |
||
861 | } |