/* * Copyright 2008-2009 Katholieke Universiteit Leuven * Copyright 2010 INRIA Saclay * Copyright 2012 Ecole Normale Superieure * * 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 <isl_ctx_private.h> #include <isl_map_private.h> #include <isl_seq.h> #include <isl/set.h> #include <isl/lp.h> #include <isl/map.h> #include "isl_equalities.h" #include "isl_sample.h" #include "isl_tab.h" #include <isl_mat_private.h> #include <isl_vec_private.h> #include <bset_to_bmap.c> #include <bset_from_bmap.c> #include <set_to_map.c> #include <set_from_map.c> __isl_give isl_basic_map *isl_basic_map_implicit_equalities( __isl_take isl_basic_map *bmap) { … } __isl_give isl_basic_set *isl_basic_set_implicit_equalities( __isl_take isl_basic_set *bset) { … } /* Make eq[row][col] of both bmaps equal so we can add the row * add the column to the common matrix. * Note that because of the echelon form, the columns of row row * after column col are zero. */ static void set_common_multiple( struct isl_basic_set *bset1, struct isl_basic_set *bset2, unsigned row, unsigned col) { … } /* Delete a given equality, moving all the following equalities one up. */ static void delete_row(__isl_keep isl_basic_set *bset, unsigned row) { … } /* Make first row entries in column col of bset1 identical to * those of bset2, using the fact that entry bset1->eq[row][col]=a * is non-zero. Initially, these elements of bset1 are all zero. * For each row i < row, we set * A[i] = a * A[i] + B[i][col] * A[row] * B[i] = a * B[i] * so that * A[i][col] = B[i][col] = a * old(B[i][col]) */ static isl_stat construct_column( __isl_keep isl_basic_set *bset1, __isl_keep isl_basic_set *bset2, unsigned row, unsigned col) { … } /* Make first row entries in column col of bset1 identical to * those of bset2, using only these entries of the two matrices. * Let t be the last row with different entries. * For each row i < t, we set * A[i] = (A[t][col]-B[t][col]) * A[i] + (B[i][col]-A[i][col) * A[t] * B[i] = (A[t][col]-B[t][col]) * B[i] + (B[i][col]-A[i][col) * B[t] * so that * A[i][col] = B[i][col] = old(A[t][col]*B[i][col]-A[i][col]*B[t][col]) */ static isl_bool transform_column( __isl_keep isl_basic_set *bset1, __isl_keep isl_basic_set *bset2, unsigned row, unsigned col) { … } /* The implementation is based on Section 5.2 of Michael Karr, * "Affine Relationships Among Variables of a Program", * except that the echelon form we use starts from the last column * and that we are dealing with integer coefficients. */ static __isl_give isl_basic_set *affine_hull( __isl_take isl_basic_set *bset1, __isl_take isl_basic_set *bset2) { … } /* Find an integer point in the set represented by "tab" * that lies outside of the equality "eq" e(x) = 0. * If "up" is true, look for a point satisfying e(x) - 1 >= 0. * Otherwise, look for a point satisfying -e(x) - 1 >= 0 (i.e., e(x) <= -1). * The point, if found, is returned. * If no point can be found, a zero-length vector is returned. * * Before solving an ILP problem, we first check if simply * adding the normal of the constraint to one of the known * integer points in the basic set represented by "tab" * yields another point inside the basic set. * * The caller of this function ensures that the tableau is bounded or * that tab->basis and tab->n_unbounded have been set appropriately. */ static __isl_give isl_vec *outside_point(struct isl_tab *tab, isl_int *eq, int up) { … } __isl_give isl_basic_set *isl_basic_set_recession_cone( __isl_take isl_basic_set *bset) { … } /* 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) { … } /* 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) { … } /* 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 * in the current approximation and adding them to that approximation * until no such points can be found any more. * * 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 __isl_give isl_basic_set *extend_affine_hull(struct isl_tab *tab, __isl_take isl_basic_set *hull, __isl_keep isl_basic_set *bset) { … } /* Construct an initial underapproximation 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) { … } /* Look for all equalities satisfied by the integer points in bset, * which is assumed to be bounded. * * The equalities are obtained by successively looking for * a point that is affinely independent of the points found so far. * In particular, for each equality satisfied by the points so far, * we check if there is any point on a hyperplane parallel to the * corresponding hyperplane shifted by at least one (in either direction). */ static __isl_give isl_basic_set *uset_affine_hull_bounded( __isl_take isl_basic_set *bset) { … } /* Given an unbounded tableau and an integer point satisfying the tableau, * construct an initial affine hull containing the recession cone * shifted to the given point. * * The unbounded directions are taken from the last rows of the basis, * which is assumed to have been initialized appropriately. */ static __isl_give isl_basic_set *initial_hull(struct isl_tab *tab, __isl_take isl_vec *vec) { … } /* Given a tableau of a set and a tableau of the corresponding * recession cone, detect and add all equalities to the tableau. * If the tableau is bounded, then we can simply keep the * tableau in its state after the return from extend_affine_hull. * However, if the tableau is unbounded, then * isl_tab_set_initial_basis_with_cone will add some additional * constraints to the tableau that have to be removed again. * In this case, we therefore rollback to the state before * any constraints were added and then add the equalities back in. */ struct isl_tab *isl_tab_detect_equalities(struct isl_tab *tab, struct isl_tab *tab_cone) { … } /* Compute the affine hull of "bset", where "cone" is the recession cone * of "bset". * * We first compute a unimodular transformation that puts the unbounded * directions in the last dimensions. In particular, we take a transformation * that maps all equalities to equalities (in HNF) on the first dimensions. * Let x be the original dimensions and y the transformed, with y_1 bounded * and y_2 unbounded. * * [ y_1 ] [ y_1 ] [ Q_1 ] * x = U [ y_2 ] [ y_2 ] = [ Q_2 ] x * * Let's call the input basic set S. We compute S' = preimage(S, U) * and drop the final dimensions including any constraints involving them. * This results in set S''. * Then we compute the affine hull A'' of S''. * Let F y_1 >= g be the constraint system of A''. In the transformed * space the y_2 are unbounded, so we can add them back without any constraints, * resulting in * * [ y_1 ] * [ F 0 ] [ y_2 ] >= g * or * [ Q_1 ] * [ F 0 ] [ Q_2 ] x >= g * or * F Q_1 x >= g * * The affine hull in the original space is then obtained as * A = preimage(A'', Q_1). */ static __isl_give isl_basic_set *affine_hull_with_cone( __isl_take isl_basic_set *bset, __isl_take isl_basic_set *cone) { … } /* Look for all equalities satisfied by the integer points in bset, * which is assumed not to have any explicit equalities. * * The equalities are obtained by successively looking for * a point that is affinely independent of the points found so far. * In particular, for each equality satisfied by the points so far, * we check if there is any point on a hyperplane parallel to the * corresponding hyperplane shifted by at least one (in either direction). * * Before looking for any outside points, we first compute the recession * cone. The directions of this recession cone will always be part * of the affine hull, so there is no need for looking for any points * in these directions. * In particular, if the recession cone is full-dimensional, then * the affine hull is simply the whole universe. */ static __isl_give isl_basic_set *uset_affine_hull( __isl_take isl_basic_set *bset) { … } /* Look for all equalities satisfied by the integer points in bmap * that are independent of the equalities already explicitly available * in bmap. * * We first remove all equalities already explicitly available, * then look for additional equalities in the reduced space * and then transform the result to the original space. * The original equalities are _not_ added to this set. This is * the responsibility of the calling function. * The resulting basic set has all meaning about the dimensions removed. * In particular, dimensions that correspond to existential variables * in bmap and that are found to be fixed are not removed. */ static __isl_give isl_basic_set *equalities_in_underlying_set( __isl_take isl_basic_map *bmap) { … } /* Detect and make explicit all equalities satisfied by the (integer) * points in bmap. */ __isl_give isl_basic_map *isl_basic_map_detect_equalities( __isl_take isl_basic_map *bmap) { … } __isl_give isl_basic_set *isl_basic_set_detect_equalities( __isl_take isl_basic_set *bset) { … } __isl_give isl_map *isl_map_detect_equalities(__isl_take isl_map *map) { … } __isl_give isl_set *isl_set_detect_equalities(__isl_take isl_set *set) { … } /* Return the superset of "bmap" described by the equalities * satisfied by "bmap" that are already known. */ __isl_give isl_basic_map *isl_basic_map_plain_affine_hull( __isl_take isl_basic_map *bmap) { … } /* Return the superset of "bset" described by the equalities * satisfied by "bset" that are already known. */ __isl_give isl_basic_set *isl_basic_set_plain_affine_hull( __isl_take isl_basic_set *bset) { … } /* After computing the rational affine hull (by detecting the implicit * equalities), we compute the additional equalities satisfied by * the integer points (if any) and add the original equalities back in. */ __isl_give isl_basic_map *isl_basic_map_affine_hull( __isl_take isl_basic_map *bmap) { … } __isl_give isl_basic_set *isl_basic_set_affine_hull( __isl_take isl_basic_set *bset) { … } /* 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) { … } /* 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) { … } /* 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) { … } static __isl_give isl_set *isl_set_local_affine_hull(__isl_take isl_set *set) { … } /* Return an empty basic map living in the same space as "map". */ static __isl_give isl_basic_map *replace_map_by_empty_basic_map( __isl_take isl_map *map) { … } /* 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) { … } __isl_give isl_basic_set *isl_set_affine_hull(__isl_take isl_set *set) { … }
Codebase Browser
llvm