370
372
(struct isl_basic_map *)bset);
375
/* Remove any common factor in numerator and denominator of the div expression,
376
* not taking into account the constant term.
377
* That is, if the div is of the form
379
* floor((a + m f(x))/(m d))
383
* floor((floor(a/m) + f(x))/d)
385
* The difference {a/m}/d in the argument satisfies 0 <= {a/m}/d < 1/d
386
* and can therefore not influence the result of the floor.
388
static void normalize_div_expression(__isl_keep isl_basic_map *bmap, int div)
390
unsigned total = isl_basic_map_total_dim(bmap);
391
isl_ctx *ctx = bmap->ctx;
393
if (isl_int_is_zero(bmap->div[div][0]))
395
isl_seq_gcd(bmap->div[div] + 2, total, &ctx->normalize_gcd);
396
isl_int_gcd(ctx->normalize_gcd, ctx->normalize_gcd, bmap->div[div][0]);
397
if (isl_int_is_one(ctx->normalize_gcd))
399
isl_int_fdiv_q(bmap->div[div][1], bmap->div[div][1],
401
isl_int_divexact(bmap->div[div][0], bmap->div[div][0],
403
isl_seq_scale_down(bmap->div[div] + 2, bmap->div[div] + 2,
404
ctx->normalize_gcd, total);
407
/* Remove any common factor in numerator and denominator of a div expression,
408
* not taking into account the constant term.
409
* That is, look for any div of the form
411
* floor((a + m f(x))/(m d))
415
* floor((floor(a/m) + f(x))/d)
417
* The difference {a/m}/d in the argument satisfies 0 <= {a/m}/d < 1/d
418
* and can therefore not influence the result of the floor.
420
static __isl_give isl_basic_map *normalize_div_expressions(
421
__isl_take isl_basic_map *bmap)
427
if (bmap->n_div == 0)
430
for (i = 0; i < bmap->n_div; ++i)
431
normalize_div_expression(bmap, i);
373
436
/* Assumes divs have been ordered if keep_divs is set.
375
438
static void eliminate_var_using_equality(struct isl_basic_map *bmap,
1154
/* Eliminate knowns divs from constraints where they appear with
1155
* a (positive or negative) unit coefficient.
1159
* floor(e/m) + f >= 0
1167
* -floor(e/m) + f >= 0
1171
* -e + m f + m - 1 >= 0
1173
* The first conversion is valid because floor(e/m) >= -f is equivalent
1174
* to e/m >= -f because -f is an integral expression.
1175
* The second conversion follows from the fact that
1177
* -floor(e/m) = ceil(-e/m) = floor((-e + m - 1)/m)
1180
* We skip integral divs, i.e., those with denominator 1, as we would
1181
* risk eliminating the div from the div constraints. We do not need
1182
* to handle those divs here anyway since the div constraints will turn
1183
* out to form an equality and this equality can then be use to eliminate
1184
* the div from all constraints.
1186
static __isl_give isl_basic_map *eliminate_unit_divs(
1187
__isl_take isl_basic_map *bmap, int *progress)
1196
ctx = isl_basic_map_get_ctx(bmap);
1197
total = 1 + isl_space_dim(bmap->dim, isl_dim_all);
1199
for (i = 0; i < bmap->n_div; ++i) {
1200
if (isl_int_is_zero(bmap->div[i][0]))
1202
if (isl_int_is_one(bmap->div[i][0]))
1204
for (j = 0; j < bmap->n_ineq; ++j) {
1207
if (!isl_int_is_one(bmap->ineq[j][total + i]) &&
1208
!isl_int_is_negone(bmap->ineq[j][total + i]))
1213
s = isl_int_sgn(bmap->ineq[j][total + i]);
1214
isl_int_set_si(bmap->ineq[j][total + i], 0);
1216
isl_seq_combine(bmap->ineq[j],
1217
ctx->negone, bmap->div[i] + 1,
1218
bmap->div[i][0], bmap->ineq[j],
1219
total + bmap->n_div);
1221
isl_seq_combine(bmap->ineq[j],
1222
ctx->one, bmap->div[i] + 1,
1223
bmap->div[i][0], bmap->ineq[j],
1224
total + bmap->n_div);
1226
isl_int_add(bmap->ineq[j][0],
1227
bmap->ineq[j][0], bmap->div[i][0]);
1228
isl_int_sub_ui(bmap->ineq[j][0],
1229
bmap->ineq[j][0], 1);
1087
1237
struct isl_basic_map *isl_basic_map_simplify(struct isl_basic_map *bmap)
1089
1239
int progress = 1;
1372
1535
/* Eliminate the specified n dimensions starting at first from the
1373
* constraints using Fourier-Motzkin. The dimensions themselves
1536
* constraints, without removing the dimensions from the space.
1537
* If the set is rational, the dimensions are eliminated using Fourier-Motzkin.
1538
* Otherwise, they are projected out and the original space is restored.
1376
1540
__isl_give isl_basic_map *isl_basic_map_eliminate(
1377
1541
__isl_take isl_basic_map *bmap,
1378
1542
enum isl_dim_type type, unsigned first, unsigned n)
1385
if (first + n > isl_basic_map_dim(bmap, type))
1551
if (first + n > isl_basic_map_dim(bmap, type) || first + n < first)
1386
1552
isl_die(bmap->ctx, isl_error_invalid,
1387
1553
"index out of bounds", goto error);
1389
first += isl_basic_map_offset(bmap, type) - 1;
1390
bmap = isl_basic_map_eliminate_vars(bmap, first, n);
1391
return isl_basic_map_finalize(bmap);
1555
if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL)) {
1556
first += isl_basic_map_offset(bmap, type) - 1;
1557
bmap = isl_basic_map_eliminate_vars(bmap, first, n);
1558
return isl_basic_map_finalize(bmap);
1561
space = isl_basic_map_get_space(bmap);
1562
bmap = isl_basic_map_project_out(bmap, type, first, n);
1563
bmap = isl_basic_map_insert_dims(bmap, type, first, n);
1564
bmap = isl_basic_map_reset_space(bmap, space);
1393
1567
isl_basic_map_free(bmap);
1571
__isl_give isl_basic_set *isl_basic_set_eliminate(
1572
__isl_take isl_basic_set *bset,
1573
enum isl_dim_type type, unsigned first, unsigned n)
1575
return isl_basic_map_eliminate(bset, type, first, n);
1397
1578
/* Don't assume equalities are in order, because align_divs
1398
1579
* may have changed the order of the divs.
1715
/* Does the (linear part of a) constraint "c" involve any of the "len"
1716
* "relevant" dimensions?
1718
static int is_related(isl_int *c, int len, int *relevant)
1722
for (i = 0; i < len; ++i) {
1725
if (!isl_int_is_zero(c[i]))
1732
/* Drop constraints from "bset" that do not involve any of
1733
* the dimensions marked "relevant".
1735
static __isl_give isl_basic_set *drop_unrelated_constraints(
1736
__isl_take isl_basic_set *bset, int *relevant)
1740
dim = isl_basic_set_dim(bset, isl_dim_set);
1741
for (i = 0; i < dim; ++i)
1747
for (i = bset->n_eq - 1; i >= 0; --i)
1748
if (!is_related(bset->eq[i] + 1, dim, relevant))
1749
isl_basic_set_drop_equality(bset, i);
1751
for (i = bset->n_ineq - 1; i >= 0; --i)
1752
if (!is_related(bset->ineq[i] + 1, dim, relevant))
1753
isl_basic_set_drop_inequality(bset, i);
1758
/* Update the groups in "group" based on the (linear part of a) constraint "c".
1760
* In particular, for any variable involved in the constraint,
1761
* find the actual group id from before and replace the group
1762
* of the corresponding variable by the minimal group of all
1763
* the variables involved in the constraint considered so far
1764
* (if this minimum is smaller) or replace the minimum by this group
1765
* (if the minimum is larger).
1767
* At the end, all the variables in "c" will (indirectly) point
1768
* to the minimal of the groups that they referred to originally.
1770
static void update_groups(int dim, int *group, isl_int *c)
1775
for (j = 0; j < dim; ++j) {
1776
if (isl_int_is_zero(c[j]))
1778
while (group[j] >= 0 && group[group[j]] != group[j])
1779
group[j] = group[group[j]];
1780
if (group[j] == min)
1782
if (group[j] < min) {
1783
if (min >= 0 && min < dim)
1784
group[min] = group[j];
1787
group[group[j]] = min;
1791
/* Drop constraints from "context" that are irrelevant for computing
1792
* the gist of "bset".
1794
* In particular, drop constraints in variables that are not related
1795
* to any of the variables involved in the constraints of "bset"
1796
* in the sense that there is no sequence of constraints that connects them.
1798
* We construct groups of variables that collect variables that
1799
* (indirectly) appear in some common constraint of "context".
1800
* Each group is identified by the first variable in the group,
1801
* except for the special group of variables that appear in "bset"
1802
* (or are related to those variables), which is identified by -1.
1803
* If group[i] is equal to i (or -1), then the group of i is i (or -1),
1804
* otherwise the group of i is the group of group[i].
1806
* We first initialize the -1 group with the variables that appear in "bset".
1807
* Then we initialize groups for the remaining variables.
1808
* Then we iterate over the constraints of "context" and update the
1809
* group of the variables in the constraint by the smallest group.
1810
* Finally, we resolve indirect references to groups by running over
1813
* After computing the groups, we drop constraints that do not involve
1814
* any variables in the -1 group.
1816
static __isl_give isl_basic_set *drop_irrelevant_constraints(
1817
__isl_take isl_basic_set *context, __isl_keep isl_basic_set *bset)
1825
if (!context || !bset)
1826
return isl_basic_set_free(context);
1828
dim = isl_basic_set_dim(bset, isl_dim_set);
1829
ctx = isl_basic_set_get_ctx(bset);
1830
group = isl_calloc_array(ctx, int, dim);
1835
for (i = 0; i < dim; ++i) {
1836
for (j = 0; j < bset->n_eq; ++j)
1837
if (!isl_int_is_zero(bset->eq[j][1 + i]))
1839
if (j < bset->n_eq) {
1843
for (j = 0; j < bset->n_ineq; ++j)
1844
if (!isl_int_is_zero(bset->ineq[j][1 + i]))
1846
if (j < bset->n_ineq)
1851
for (i = 0; i < dim; ++i)
1853
last = group[i] = i;
1859
for (i = 0; i < context->n_eq; ++i)
1860
update_groups(dim, group, context->eq[i] + 1);
1861
for (i = 0; i < context->n_ineq; ++i)
1862
update_groups(dim, group, context->ineq[i] + 1);
1864
for (i = 0; i < dim; ++i)
1866
group[i] = group[group[i]];
1868
for (i = 0; i < dim; ++i)
1869
group[i] = group[i] == -1;
1871
context = drop_unrelated_constraints(context, group);
1877
return isl_basic_set_free(context);
1534
1880
/* Remove all information from bset that is redundant in the context
1535
1881
* of context. Both bset and context are assumed to be full-dimensional.
1537
* We first * remove the inequalities from "bset"
1883
* We first remove the inequalities from "bset"
1538
1884
* that are obviously redundant with respect to some inequality in "context".
1885
* Then we remove those constraints from "context" that have become
1886
* irrelevant for computing the gist of "bset".
1887
* Note that this removal of constraints cannot be replaced by
1888
* a factorization because factors in "bset" may still be connected
1889
* to each other through constraints in "context".
1540
1891
* If there are any inequalities left, we construct a tableau for
1541
1892
* the context and then add the inequalities of "bset".
2208
/* Return a map that has the same intersection with "context" as "map"
2209
* and that as "simple" as possible.
2211
* If "map" is already the universe, then we cannot make it any simpler.
2212
* Similarly, if "context" is the universe, then we cannot exploit it
2214
* If "map" and "context" are identical to each other, then we can
2215
* return the corresponding universe.
2217
* If none of these cases apply, we have to work a bit harder.
1843
2219
static __isl_give isl_map *map_gist(__isl_take isl_map *map,
1844
2220
__isl_take isl_map *context)
2225
is_universe = isl_map_plain_is_universe(map);
2226
if (is_universe >= 0 && !is_universe)
2227
is_universe = isl_map_plain_is_universe(context);
2228
if (is_universe < 0)
2231
isl_map_free(context);
2235
equal = isl_map_plain_is_equal(map, context);
2239
isl_map *res = isl_map_universe(isl_map_get_space(map));
2241
isl_map_free(context);
1846
2245
context = isl_map_compute_divs(context);
1847
2246
return isl_map_gist_basic_map(map, isl_map_simple_hull(context));
2249
isl_map_free(context);
1850
2253
__isl_give isl_map *isl_map_gist(__isl_take isl_map *map,
1990
2393
(struct isl_basic_map *)bset2);
2396
/* Are "map1" and "map2" obviously disjoint?
2398
* If one of them is empty or if they live in different spaces (ignoring
2399
* parameters), then they are clearly disjoint.
2401
* If they have different parameters, then we skip any further tests.
2403
* If they are obviously equal, but not obviously empty, then we will
2404
* not be able to detect if they are disjoint.
2406
* Otherwise we check if each basic map in "map1" is obviously disjoint
2407
* from each basic map in "map2".
1993
2409
int isl_map_plain_is_disjoint(__isl_keep isl_map *map1,
1994
2410
__isl_keep isl_map *map2)
1998
2417
if (!map1 || !map2)
2001
if (isl_map_plain_is_equal(map1, map2))
2420
disjoint = isl_map_plain_is_empty(map1);
2421
if (disjoint < 0 || disjoint)
2424
disjoint = isl_map_plain_is_empty(map2);
2425
if (disjoint < 0 || disjoint)
2428
match = isl_space_tuple_match(map1->dim, isl_dim_in,
2429
map2->dim, isl_dim_in);
2430
if (match < 0 || !match)
2431
return match < 0 ? -1 : 1;
2433
match = isl_space_tuple_match(map1->dim, isl_dim_out,
2434
map2->dim, isl_dim_out);
2435
if (match < 0 || !match)
2436
return match < 0 ? -1 : 1;
2438
match = isl_space_match(map1->dim, isl_dim_param,
2439
map2->dim, isl_dim_param);
2440
if (match < 0 || !match)
2441
return match < 0 ? -1 : 0;
2443
intersect = isl_map_plain_is_equal(map1, map2);
2444
if (intersect < 0 || intersect)
2445
return intersect < 0 ? -1 : 0;
2004
2447
for (i = 0; i < map1->n; ++i) {
2005
2448
for (j = 0; j < map2->n; ++j) {
2458
/* Are "map1" and "map2" disjoint?
2460
* They are disjoint if they are "obviously disjoint" or if one of them
2461
* is empty. Otherwise, they are not disjoint if one of them is universal.
2462
* If none of these cases apply, we compute the intersection and see if
2463
* the result is empty.
2465
int isl_map_is_disjoint(__isl_keep isl_map *map1, __isl_keep isl_map *map2)
2471
disjoint = isl_map_plain_is_disjoint(map1, map2);
2472
if (disjoint < 0 || disjoint)
2475
disjoint = isl_map_is_empty(map1);
2476
if (disjoint < 0 || disjoint)
2479
disjoint = isl_map_is_empty(map2);
2480
if (disjoint < 0 || disjoint)
2483
intersect = isl_map_plain_is_universe(map1);
2484
if (intersect < 0 || intersect)
2485
return intersect < 0 ? -1 : 0;
2487
intersect = isl_map_plain_is_universe(map2);
2488
if (intersect < 0 || intersect)
2489
return intersect < 0 ? -1 : 0;
2491
test = isl_map_intersect(isl_map_copy(map1), isl_map_copy(map2));
2492
disjoint = isl_map_is_empty(test);
2015
2498
int isl_set_plain_is_disjoint(__isl_keep isl_set *set1,
2016
2499
__isl_keep isl_set *set2)
added
removed
isl/isl_map_simplify.c
