X-Git-Url: http://review.tizen.org/git/?p=platform%2Fupstream%2Fisl.git;a=blobdiff_plain;f=isl_affine_hull.c;h=0d66081eaec3ab462eab1b79e7a4157acb78aaf8;hp=adf66cd7050ed9cfc91eb12de5b6c4258d8ec6db;hb=63fb8a7f484648c3caa25351c8c94ac2395ec563;hpb=88e08a163e4032c1a673ac770223fd98f2cd05da diff --git a/isl_affine_hull.c b/isl_affine_hull.c index adf66cd..0d66081 100644 --- a/isl_affine_hull.c +++ b/isl_affine_hull.c @@ -1,14 +1,19 @@ /* * Copyright 2008-2009 Katholieke Universiteit Leuven + * Copyright 2010 INRIA Saclay + * Copyright 2012 Ecole Normale Superieure * - * Use of this software is governed by the GNU LGPLv2.1 license + * Use of this software is governed by the MIT license * * Written by Sven Verdoolaege, K.U.Leuven, Departement * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium + * and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite, + * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France + * and Ecole Normale Superieure, 45 rue d'Ulm, 75230 Paris, France */ +#include #include -#include #include #include #include @@ -34,7 +39,7 @@ struct isl_basic_map *isl_basic_map_implicit_equalities( if (bmap->n_ineq <= 1) return bmap; - tab = isl_tab_from_basic_map(bmap); + tab = isl_tab_from_basic_map(bmap, 0); if (isl_tab_detect_implicit_equalities(tab) < 0) goto error; bmap = isl_basic_map_update_from_tab(bmap, tab); @@ -353,6 +358,72 @@ error: return NULL; } +/* Move "sample" to a point that is one up (or down) from the original + * point in dimension "pos". + */ +static void adjacent_point(__isl_keep isl_vec *sample, int pos, int up) +{ + if (up) + isl_int_add_ui(sample->el[1 + pos], sample->el[1 + pos], 1); + else + isl_int_sub_ui(sample->el[1 + pos], sample->el[1 + pos], 1); +} + +/* Check if any points that are adjacent to "sample" also belong to "bset". + * If so, add them to "hull" and return the updated hull. + * + * Before checking whether and adjacent point belongs to "bset", we first + * check whether it already belongs to "hull" as this test is typically + * much cheaper. + */ +static __isl_give isl_basic_set *add_adjacent_points( + __isl_take isl_basic_set *hull, __isl_take isl_vec *sample, + __isl_keep isl_basic_set *bset) +{ + int i, up; + int dim; + + if (!sample) + goto error; + + dim = isl_basic_set_dim(hull, isl_dim_set); + + for (i = 0; i < dim; ++i) { + for (up = 0; up <= 1; ++up) { + int contains; + isl_basic_set *point; + + adjacent_point(sample, i, up); + contains = isl_basic_set_contains(hull, sample); + if (contains < 0) + goto error; + if (contains) { + adjacent_point(sample, i, !up); + continue; + } + contains = isl_basic_set_contains(bset, sample); + if (contains < 0) + goto error; + if (contains) { + point = isl_basic_set_from_vec( + isl_vec_copy(sample)); + hull = affine_hull(hull, point); + } + adjacent_point(sample, i, !up); + if (contains) + break; + } + } + + isl_vec_free(sample); + + return hull; +error: + isl_vec_free(sample); + isl_basic_set_free(hull); + return NULL; +} + /* Extend an initial (under-)approximation of the affine hull of basic * set represented by the tableau "tab" * by looking for points that do not satisfy one of the equalities @@ -361,9 +432,13 @@ error: * * The caller of this function ensures that "tab" is bounded or * that tab->basis and tab->n_unbounded have been set appropriately. + * + * "bset" may be either NULL or the basic set represented by "tab". + * If "bset" is not NULL, we check for any point we find if any + * of its adjacent points also belong to "bset". */ -static struct isl_basic_set *extend_affine_hull(struct isl_tab *tab, - struct isl_basic_set *hull) +static __isl_give isl_basic_set *extend_affine_hull(struct isl_tab *tab, + __isl_take isl_basic_set *hull, __isl_keep isl_basic_set *bset) { int i, j; unsigned dim; @@ -402,6 +477,9 @@ static struct isl_basic_set *extend_affine_hull(struct isl_tab *tab, tab = isl_tab_add_sample(tab, isl_vec_copy(sample)); if (!tab) goto error; + if (bset) + hull = add_adjacent_points(hull, isl_vec_copy(sample), + bset); point = isl_basic_set_from_vec(sample); hull = affine_hull(hull, point); if (!hull) @@ -414,35 +492,186 @@ error: return NULL; } +/* Drop all constraints in bmap that involve any of the dimensions + * first to first+n-1. + */ +static __isl_give isl_basic_map *isl_basic_map_drop_constraints_involving( + __isl_take isl_basic_map *bmap, unsigned first, unsigned n) +{ + int i; + + if (n == 0) + return bmap; + + bmap = isl_basic_map_cow(bmap); + + if (!bmap) + return NULL; + + for (i = bmap->n_eq - 1; i >= 0; --i) { + if (isl_seq_first_non_zero(bmap->eq[i] + 1 + first, n) == -1) + continue; + isl_basic_map_drop_equality(bmap, i); + } + + for (i = bmap->n_ineq - 1; i >= 0; --i) { + if (isl_seq_first_non_zero(bmap->ineq[i] + 1 + first, n) == -1) + continue; + isl_basic_map_drop_inequality(bmap, i); + } + + return bmap; +} + /* Drop all constraints in bset that involve any of the dimensions * first to first+n-1. */ __isl_give isl_basic_set *isl_basic_set_drop_constraints_involving( __isl_take isl_basic_set *bset, unsigned first, unsigned n) { + return isl_basic_map_drop_constraints_involving(bset, first, n); +} + +/* Drop all constraints in bmap that do not involve any of the dimensions + * first to first + n - 1 of the given type. + */ +__isl_give isl_basic_map *isl_basic_map_drop_constraints_not_involving_dims( + __isl_take isl_basic_map *bmap, + enum isl_dim_type type, unsigned first, unsigned n) +{ int i; + unsigned dim; if (n == 0) - return bset; + return isl_basic_map_set_to_empty(bmap); + bmap = isl_basic_map_cow(bmap); + if (!bmap) + return NULL; - bset = isl_basic_set_cow(bset); + dim = isl_basic_map_dim(bmap, type); + if (first + n > dim || first + n < first) + isl_die(isl_basic_map_get_ctx(bmap), isl_error_invalid, + "index out of bounds", return isl_basic_map_free(bmap)); - if (!bset) - return NULL; + first += isl_basic_map_offset(bmap, type) - 1; - for (i = bset->n_eq - 1; i >= 0; --i) { - if (isl_seq_first_non_zero(bset->eq[i] + 1 + first, n) == -1) + for (i = bmap->n_eq - 1; i >= 0; --i) { + if (isl_seq_first_non_zero(bmap->eq[i] + 1 + first, n) != -1) continue; - isl_basic_set_drop_equality(bset, i); + isl_basic_map_drop_equality(bmap, i); } - for (i = bset->n_ineq - 1; i >= 0; --i) { - if (isl_seq_first_non_zero(bset->ineq[i] + 1 + first, n) == -1) + for (i = bmap->n_ineq - 1; i >= 0; --i) { + if (isl_seq_first_non_zero(bmap->ineq[i] + 1 + first, n) != -1) continue; - isl_basic_set_drop_inequality(bset, i); + isl_basic_map_drop_inequality(bmap, i); } - return bset; + return bmap; +} + +/* Drop all constraints in bset that do not involve any of the dimensions + * first to first + n - 1 of the given type. + */ +__isl_give isl_basic_set *isl_basic_set_drop_constraints_not_involving_dims( + __isl_take isl_basic_set *bset, + enum isl_dim_type type, unsigned first, unsigned n) +{ + return isl_basic_map_drop_constraints_not_involving_dims(bset, + type, first, n); +} + +/* Drop all constraints in bmap that involve any of the dimensions + * first to first + n - 1 of the given type. + */ +__isl_give isl_basic_map *isl_basic_map_drop_constraints_involving_dims( + __isl_take isl_basic_map *bmap, + enum isl_dim_type type, unsigned first, unsigned n) +{ + unsigned dim; + + if (!bmap) + return NULL; + if (n == 0) + return bmap; + + dim = isl_basic_map_dim(bmap, type); + if (first + n > dim || first + n < first) + isl_die(isl_basic_map_get_ctx(bmap), isl_error_invalid, + "index out of bounds", return isl_basic_map_free(bmap)); + + bmap = isl_basic_map_remove_divs_involving_dims(bmap, type, first, n); + first += isl_basic_map_offset(bmap, type) - 1; + return isl_basic_map_drop_constraints_involving(bmap, first, n); +} + +/* Drop all constraints in bset that involve any of the dimensions + * first to first + n - 1 of the given type. + */ +__isl_give isl_basic_set *isl_basic_set_drop_constraints_involving_dims( + __isl_take isl_basic_set *bset, + enum isl_dim_type type, unsigned first, unsigned n) +{ + return isl_basic_map_drop_constraints_involving_dims(bset, + type, first, n); +} + +/* Drop all constraints in map that involve any of the dimensions + * first to first + n - 1 of the given type. + */ +__isl_give isl_map *isl_map_drop_constraints_involving_dims( + __isl_take isl_map *map, + enum isl_dim_type type, unsigned first, unsigned n) +{ + int i; + unsigned dim; + + if (!map) + return NULL; + if (n == 0) + return map; + + dim = isl_map_dim(map, type); + if (first + n > dim || first + n < first) + isl_die(isl_map_get_ctx(map), isl_error_invalid, + "index out of bounds", return isl_map_free(map)); + + map = isl_map_cow(map); + if (!map) + return NULL; + + for (i = 0; i < map->n; ++i) { + map->p[i] = isl_basic_map_drop_constraints_involving_dims( + map->p[i], type, first, n); + if (!map->p[i]) + return isl_map_free(map); + } + + return map; +} + +/* Drop all constraints in set that involve any of the dimensions + * first to first + n - 1 of the given type. + */ +__isl_give isl_set *isl_set_drop_constraints_involving_dims( + __isl_take isl_set *set, + enum isl_dim_type type, unsigned first, unsigned n) +{ + return isl_map_drop_constraints_involving_dims(set, type, first, n); +} + +/* Construct an initial underapproximatino of the hull of "bset" + * from "sample" and any of its adjacent points that also belong to "bset". + */ +static __isl_give isl_basic_set *initialize_hull(__isl_keep isl_basic_set *bset, + __isl_take isl_vec *sample) +{ + isl_basic_set *hull; + + hull = isl_basic_set_from_vec(isl_vec_copy(sample)); + hull = add_adjacent_points(hull, sample, bset); + + return hull; } /* Look for all equalities satisfied by the integer points in bset, @@ -461,7 +690,7 @@ static struct isl_basic_set *uset_affine_hull_bounded(struct isl_basic_set *bset struct isl_tab *tab = NULL; unsigned dim; - if (isl_basic_set_fast_is_empty(bset)) + if (isl_basic_set_plain_is_empty(bset)) return bset; dim = isl_basic_set_n_dim(bset); @@ -480,7 +709,7 @@ static struct isl_basic_set *uset_affine_hull_bounded(struct isl_basic_set *bset } } - tab = isl_tab_from_basic_set(bset); + tab = isl_tab_from_basic_set(bset, 1); if (!tab) goto error; if (tab->empty) { @@ -488,8 +717,6 @@ static struct isl_basic_set *uset_affine_hull_bounded(struct isl_basic_set *bset isl_vec_free(sample); return isl_basic_set_set_to_empty(bset); } - if (isl_tab_track_bset(tab, isl_basic_set_copy(bset)) < 0) - goto error; if (!sample) { struct isl_tab_undo *snap; @@ -509,10 +736,10 @@ static struct isl_basic_set *uset_affine_hull_bounded(struct isl_basic_set *bset return isl_basic_set_set_to_empty(bset); } - hull = isl_basic_set_from_vec(sample); + hull = initialize_hull(bset, sample); + hull = extend_affine_hull(tab, hull, bset); isl_basic_set_free(bset); - hull = extend_affine_hull(tab, hull); isl_tab_free(tab); return hull; @@ -583,7 +810,7 @@ struct isl_tab *isl_tab_detect_equalities(struct isl_tab *tab, { int j; struct isl_vec *sample; - struct isl_basic_set *hull; + struct isl_basic_set *hull = NULL; struct isl_tab_undo *snap; if (!tab || !tab_cone) @@ -624,7 +851,7 @@ struct isl_tab *isl_tab_detect_equalities(struct isl_tab *tab, isl_vec_free(sample); - hull = extend_affine_hull(tab, hull); + hull = extend_affine_hull(tab, hull, NULL); if (!hull) goto error; @@ -648,6 +875,7 @@ struct isl_tab *isl_tab_detect_equalities(struct isl_tab *tab, return tab; error: + isl_basic_set_free(hull); isl_tab_free(tab); return NULL; } @@ -697,7 +925,7 @@ static struct isl_basic_set *affine_hull_with_cone(struct isl_basic_set *bset, total = isl_basic_set_total_dim(cone); cone_dim = total - cone->n_eq; - M = isl_mat_sub_alloc(bset->ctx, cone->eq, 0, cone->n_eq, 1, total); + M = isl_mat_sub_alloc6(bset->ctx, cone->eq, 0, cone->n_eq, 1, total); M = isl_mat_left_hermite(M, 0, &U, &Q); if (!M) goto error; @@ -718,9 +946,10 @@ static struct isl_basic_set *affine_hull_with_cone(struct isl_basic_set *bset, hull = uset_affine_hull_bounded(bset); - if (!hull) + if (!hull) { + isl_mat_free(Q); isl_mat_free(U); - else { + } else { struct isl_vec *sample = isl_vec_copy(hull->sample); U = isl_mat_drop_cols(U, 1 + total - cone_dim, cone_dim); if (sample && sample->size > 0) @@ -764,7 +993,7 @@ static struct isl_basic_set *uset_affine_hull(struct isl_basic_set *bset) { struct isl_basic_set *cone; - if (isl_basic_set_fast_is_empty(bset)) + if (isl_basic_set_plain_is_empty(bset)) return bset; cone = isl_basic_set_recession_cone(isl_basic_set_copy(bset)); @@ -840,6 +1069,7 @@ static struct isl_basic_set *equalities_in_underlying_set( return hull; error: + isl_mat_free(T1); isl_mat_free(T2); isl_basic_set_free(bset); isl_basic_set_free(hull); @@ -873,7 +1103,7 @@ struct isl_basic_map *isl_basic_map_detect_equalities( isl_basic_set_free(hull); return isl_basic_map_set_to_empty(bmap); } - bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim), 0, + bmap = isl_basic_map_extend_space(bmap, isl_space_copy(bmap->dim), 0, hull->n_eq, 0); for (i = 0; i < hull->n_eq; ++i) { j = isl_basic_map_alloc_equality(bmap); @@ -901,27 +1131,10 @@ __isl_give isl_basic_set *isl_basic_set_detect_equalities( isl_basic_map_detect_equalities((isl_basic_map *)bset); } -struct isl_map *isl_map_detect_equalities(struct isl_map *map) +__isl_give isl_map *isl_map_detect_equalities(__isl_take isl_map *map) { - struct isl_basic_map *bmap; - int i; - - if (!map) - return NULL; - - for (i = 0; i < map->n; ++i) { - bmap = isl_basic_map_copy(map->p[i]); - bmap = isl_basic_map_detect_equalities(bmap); - if (!bmap) - goto error; - isl_basic_map_free(map->p[i]); - map->p[i] = bmap; - } - - return map; -error: - isl_map_free(map); - return NULL; + return isl_map_inline_foreach_basic_map(map, + &isl_basic_map_detect_equalities); } __isl_give isl_set *isl_set_detect_equalities(__isl_take isl_set *set) @@ -939,6 +1152,7 @@ struct isl_basic_map *isl_basic_map_affine_hull(struct isl_basic_map *bmap) bmap = isl_basic_map_cow(bmap); if (bmap) isl_basic_map_free_inequality(bmap, bmap->n_ineq); + bmap = isl_basic_map_finalize(bmap); return bmap; } @@ -948,14 +1162,205 @@ struct isl_basic_set *isl_basic_set_affine_hull(struct isl_basic_set *bset) isl_basic_map_affine_hull((struct isl_basic_map *)bset); } -struct isl_basic_map *isl_map_affine_hull(struct isl_map *map) +/* Given a rational affine matrix "M", add stride constraints to "bmap" + * that ensure that + * + * M(x) + * + * is an integer vector. The variables x include all the variables + * of "bmap" except the unknown divs. + * + * If d is the common denominator of M, then we need to impose that + * + * d M(x) = 0 mod d + * + * or + * + * exists alpha : d M(x) = d alpha + * + * This function is similar to add_strides in isl_morph.c + */ +static __isl_give isl_basic_map *add_strides(__isl_take isl_basic_map *bmap, + __isl_keep isl_mat *M, int n_known) +{ + int i, div, k; + isl_int gcd; + + if (isl_int_is_one(M->row[0][0])) + return bmap; + + bmap = isl_basic_map_extend_space(bmap, isl_space_copy(bmap->dim), + M->n_row - 1, M->n_row - 1, 0); + + isl_int_init(gcd); + for (i = 1; i < M->n_row; ++i) { + isl_seq_gcd(M->row[i], M->n_col, &gcd); + if (isl_int_is_divisible_by(gcd, M->row[0][0])) + continue; + div = isl_basic_map_alloc_div(bmap); + if (div < 0) + goto error; + isl_int_set_si(bmap->div[div][0], 0); + k = isl_basic_map_alloc_equality(bmap); + if (k < 0) + goto error; + isl_seq_cpy(bmap->eq[k], M->row[i], M->n_col); + isl_seq_clr(bmap->eq[k] + M->n_col, bmap->n_div - n_known); + isl_int_set(bmap->eq[k][M->n_col - n_known + div], + M->row[0][0]); + } + isl_int_clear(gcd); + + return bmap; +error: + isl_int_clear(gcd); + isl_basic_map_free(bmap); + return NULL; +} + +/* If there are any equalities that involve (multiple) unknown divs, + * then extract the stride information encoded by those equalities + * and make it explicitly available in "bmap". + * + * We first sort the divs so that the unknown divs appear last and + * then we count how many equalities involve these divs. + * + * Let these equalities be of the form + * + * A(x) + B y = 0 + * + * where y represents the unknown divs and x the remaining variables. + * Let [H 0] be the Hermite Normal Form of B, i.e., + * + * B = [H 0] Q + * + * Then x is a solution of the equalities iff + * + * H^-1 A(x) (= - [I 0] Q y) + * + * is an integer vector. Let d be the common denominator of H^-1. + * We impose + * + * d H^-1 A(x) = d alpha + * + * in add_strides, with alpha fresh existentially quantified variables. + */ +static __isl_give isl_basic_map *isl_basic_map_make_strides_explicit( + __isl_take isl_basic_map *bmap) +{ + int known; + int n_known; + int n, n_col; + int total; + isl_ctx *ctx; + isl_mat *A, *B, *M; + + known = isl_basic_map_divs_known(bmap); + if (known < 0) + return isl_basic_map_free(bmap); + if (known) + return bmap; + bmap = isl_basic_map_sort_divs(bmap); + bmap = isl_basic_map_gauss(bmap, NULL); + if (!bmap) + return NULL; + + for (n_known = 0; n_known < bmap->n_div; ++n_known) + if (isl_int_is_zero(bmap->div[n_known][0])) + break; + ctx = isl_basic_map_get_ctx(bmap); + total = isl_space_dim(bmap->dim, isl_dim_all); + for (n = 0; n < bmap->n_eq; ++n) + if (isl_seq_first_non_zero(bmap->eq[n] + 1 + total + n_known, + bmap->n_div - n_known) == -1) + break; + if (n == 0) + return bmap; + B = isl_mat_sub_alloc6(ctx, bmap->eq, 0, n, 0, 1 + total + n_known); + n_col = bmap->n_div - n_known; + A = isl_mat_sub_alloc6(ctx, bmap->eq, 0, n, 1 + total + n_known, n_col); + A = isl_mat_left_hermite(A, 0, NULL, NULL); + A = isl_mat_drop_cols(A, n, n_col - n); + A = isl_mat_lin_to_aff(A); + A = isl_mat_right_inverse(A); + B = isl_mat_insert_zero_rows(B, 0, 1); + B = isl_mat_set_element_si(B, 0, 0, 1); + M = isl_mat_product(A, B); + if (!M) + return isl_basic_map_free(bmap); + bmap = add_strides(bmap, M, n_known); + bmap = isl_basic_map_gauss(bmap, NULL); + isl_mat_free(M); + + return bmap; +} + +/* Compute the affine hull of each basic map in "map" separately + * and make all stride information explicit so that we can remove + * all unknown divs without losing this information. + * The result is also guaranteed to be gaussed. + * + * In simple cases where a div is determined by an equality, + * calling isl_basic_map_gauss is enough to make the stride information + * explicit, as it will derive an explicit representation for the div + * from the equality. If, however, the stride information + * is encoded through multiple unknown divs then we need to make + * some extra effort in isl_basic_map_make_strides_explicit. + */ +static __isl_give isl_map *isl_map_local_affine_hull(__isl_take isl_map *map) { int i; + + map = isl_map_cow(map); + if (!map) + return NULL; + + for (i = 0; i < map->n; ++i) { + map->p[i] = isl_basic_map_affine_hull(map->p[i]); + map->p[i] = isl_basic_map_gauss(map->p[i], NULL); + map->p[i] = isl_basic_map_make_strides_explicit(map->p[i]); + if (!map->p[i]) + return isl_map_free(map); + } + + return map; +} + +static __isl_give isl_set *isl_set_local_affine_hull(__isl_take isl_set *set) +{ + return isl_map_local_affine_hull(set); +} + +/* Compute the affine hull of "map". + * + * We first compute the affine hull of each basic map separately. + * Then we align the divs and recompute the affine hulls of the basic + * maps since some of them may now have extra divs. + * In order to avoid performing parametric integer programming to + * compute explicit expressions for the divs, possible leading to + * an explosion in the number of basic maps, we first drop all unknown + * divs before aligning the divs. Note that isl_map_local_affine_hull tries + * to make sure that all stride information is explicitly available + * in terms of known divs. This involves calling isl_basic_set_gauss, + * which is also needed because affine_hull assumes its input has been gaussed, + * while isl_map_affine_hull may be called on input that has not been gaussed, + * in particular from initial_facet_constraint. + * Similarly, align_divs may reorder some divs so that we need to + * gauss the result again. + * Finally, we combine the individual affine hulls into a single + * affine hull. + */ +__isl_give isl_basic_map *isl_map_affine_hull(__isl_take isl_map *map) +{ struct isl_basic_map *model = NULL; struct isl_basic_map *hull = NULL; struct isl_set *set; + isl_basic_set *bset; map = isl_map_detect_equalities(map); + map = isl_map_local_affine_hull(map); + map = isl_map_remove_empty_parts(map); + map = isl_map_remove_unknown_divs(map); map = isl_map_align_divs(map); if (!map) @@ -970,30 +1375,15 @@ struct isl_basic_map *isl_map_affine_hull(struct isl_map *map) model = isl_basic_map_copy(map->p[0]); set = isl_map_underlying_set(map); set = isl_set_cow(set); + set = isl_set_local_affine_hull(set); if (!set) goto error; - for (i = 0; i < set->n; ++i) { - set->p[i] = isl_basic_set_cow(set->p[i]); - set->p[i] = isl_basic_set_affine_hull(set->p[i]); - set->p[i] = isl_basic_set_gauss(set->p[i], NULL); - if (!set->p[i]) - goto error; - } - set = isl_set_remove_empty_parts(set); - if (set->n == 0) { - hull = isl_basic_map_empty_like(model); - isl_basic_map_free(model); - } else { - struct isl_basic_set *bset; - while (set->n > 1) { - set->p[0] = affine_hull(set->p[0], set->p[--set->n]); - if (!set->p[0]) - goto error; - } - bset = isl_basic_set_copy(set->p[0]); - hull = isl_basic_map_overlying_set(bset, model); - } + while (set->n > 1) + set->p[0] = affine_hull(set->p[0], set->p[--set->n]); + + bset = isl_basic_set_copy(set->p[0]); + hull = isl_basic_map_overlying_set(bset, model); isl_set_free(set); hull = isl_basic_map_simplify(hull); return isl_basic_map_finalize(hull);