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