/* * Copyright 2010 INRIA Saclay * * Use of this software is governed by the MIT license * * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France, * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod, * 91893 Orsay, France */ #include <isl_ctx_private.h> #include <isl_map_private.h> #include <isl/map.h> #include <isl_seq.h> #include <isl_space_private.h> #include <isl_lp_private.h> #include <isl/union_map.h> #include <isl_mat_private.h> #include <isl_vec_private.h> #include <isl_options_private.h> #include <isl_tarjan.h> isl_bool isl_map_is_transitively_closed(__isl_keep isl_map *map) { … } isl_bool isl_union_map_is_transitively_closed(__isl_keep isl_union_map *umap) { … } /* Given a map that represents a path with the length of the path * encoded as the difference between the last output coordindate * and the last input coordinate, set this length to either * exactly "length" (if "exactly" is set) or at least "length" * (if "exactly" is not set). */ static __isl_give isl_map *set_path_length(__isl_take isl_map *map, int exactly, int length) { … } /* Check whether the overapproximation of the power of "map" is exactly * the power of "map". Let R be "map" and A_k the overapproximation. * The approximation is exact if * * A_1 = R * A_k = A_{k-1} \circ R k >= 2 * * Since A_k is known to be an overapproximation, we only need to check * * A_1 \subset R * A_k \subset A_{k-1} \circ R k >= 2 * * In practice, "app" has an extra input and output coordinate * to encode the length of the path. So, we first need to add * this coordinate to "map" and set the length of the path to * one. */ static isl_bool check_power_exactness(__isl_take isl_map *map, __isl_take isl_map *app) { … } /* Check whether the overapproximation of the power of "map" is exactly * the power of "map", possibly after projecting out the power (if "project" * is set). * * If "project" is set and if "steps" can only result in acyclic paths, * then we check * * A = R \cup (A \circ R) * * where A is the overapproximation with the power projected out, i.e., * an overapproximation of the transitive closure. * More specifically, since A is known to be an overapproximation, we check * * A \subset R \cup (A \circ R) * * Otherwise, we check if the power is exact. * * Note that "app" has an extra input and output coordinate to encode * the length of the part. If we are only interested in the transitive * closure, then we can simply project out these coordinates first. */ static isl_bool check_exactness(__isl_take isl_map *map, __isl_take isl_map *app, int project) { … } /* * The transitive closure implementation is based on the paper * "Computing the Transitive Closure of a Union of Affine Integer * Tuple Relations" by Anna Beletska, Denis Barthou, Wlodzimierz Bielecki and * Albert Cohen. */ /* Given a set of n offsets v_i (the rows of "steps"), construct a relation * of the given dimension specification (Z^{n+1} -> Z^{n+1}) * that maps an element x to any element that can be reached * by taking a non-negative number of steps along any of * the extended offsets v'_i = [v_i 1]. * That is, construct * * { [x] -> [y] : exists k_i >= 0, y = x + \sum_i k_i v'_i } * * For any element in this relation, the number of steps taken * is equal to the difference in the final coordinates. */ static __isl_give isl_map *path_along_steps(__isl_take isl_space *space, __isl_keep isl_mat *steps) { … } #define IMPURE … #define PURE_PARAM … #define PURE_VAR … #define MIXED … /* Check whether the parametric constant term of constraint c is never * positive in "bset". */ static isl_bool parametric_constant_never_positive( __isl_keep isl_basic_set *bset, isl_int *c, int *div_purity) { … } /* Return PURE_PARAM if only the coefficients of the parameters are non-zero. * Return PURE_VAR if only the coefficients of the set variables are non-zero. * Return MIXED if only the coefficients of the parameters and the set * variables are non-zero and if moreover the parametric constant * can never attain positive values. * Return IMPURE otherwise. */ static int purity(__isl_keep isl_basic_set *bset, isl_int *c, int *div_purity, int eq) { … } /* Return an array of integers indicating the type of each div in bset. * If the div is (recursively) defined in terms of only the parameters, * then the type is PURE_PARAM. * If the div is (recursively) defined in terms of only the set variables, * then the type is PURE_VAR. * Otherwise, the type is IMPURE. */ static __isl_give int *get_div_purity(__isl_keep isl_basic_set *bset) { … } /* Given a path with the as yet unconstrained length at div position "pos", * check if setting the length to zero results in only the identity * mapping. */ static isl_bool empty_path_is_identity(__isl_keep isl_basic_map *path, unsigned pos) { … } /* If any of the constraints is found to be impure then this function * sets *impurity to 1. * * If impurity is NULL then we are dealing with a non-parametric set * and so the constraints are obviously PURE_VAR. */ static __isl_give isl_basic_map *add_delta_constraints( __isl_take isl_basic_map *path, __isl_keep isl_basic_set *delta, unsigned off, unsigned nparam, unsigned d, int *div_purity, int eq, int *impurity) { … } /* Given a set of offsets "delta", construct a relation of the * given dimension specification (Z^{n+1} -> Z^{n+1}) that * is an overapproximation of the relations that * maps an element x to any element that can be reached * by taking a non-negative number of steps along any of * the elements in "delta". * That is, construct an approximation of * * { [x] -> [y] : exists f \in \delta, k \in Z : * y = x + k [f, 1] and k >= 0 } * * For any element in this relation, the number of steps taken * is equal to the difference in the final coordinates. * * In particular, let delta be defined as * * \delta = [p] -> { [x] : A x + a >= 0 and B p + b >= 0 and * C x + C'p + c >= 0 and * D x + D'p + d >= 0 } * * where the constraints C x + C'p + c >= 0 are such that the parametric * constant term of each constraint j, "C_j x + C'_j p + c_j", * can never attain positive values, then the relation is constructed as * * { [x] -> [y] : exists [f, k] \in Z^{n+1} : y = x + f and * A f + k a >= 0 and B p + b >= 0 and * C f + C'p + c >= 0 and k >= 1 } * union { [x] -> [x] } * * If the zero-length paths happen to correspond exactly to the identity * mapping, then we return * * { [x] -> [y] : exists [f, k] \in Z^{n+1} : y = x + f and * A f + k a >= 0 and B p + b >= 0 and * C f + C'p + c >= 0 and k >= 0 } * * instead. * * Existentially quantified variables in \delta are handled by * classifying them as independent of the parameters, purely * parameter dependent and others. Constraints containing * any of the other existentially quantified variables are removed. * This is safe, but leads to an additional overapproximation. * * If there are any impure constraints, then we also eliminate * the parameters from \delta, resulting in a set * * \delta' = { [x] : E x + e >= 0 } * * and add the constraints * * E f + k e >= 0 * * to the constructed relation. */ static __isl_give isl_map *path_along_delta(__isl_take isl_space *space, __isl_take isl_basic_set *delta) { … } /* Given a dimension specification Z^{n+1} -> Z^{n+1} and a parameter "param", * construct a map that equates the parameter to the difference * in the final coordinates and imposes that this difference is positive. * That is, construct * * { [x,x_s] -> [y,y_s] : k = y_s - x_s > 0 } */ static __isl_give isl_map *equate_parameter_to_length( __isl_take isl_space *space, unsigned param) { … } /* Check whether "path" is acyclic, where the last coordinates of domain * and range of path encode the number of steps taken. * That is, check whether * * { d | d = y - x and (x,y) in path } * * does not contain any element with positive last coordinate (positive length) * and zero remaining coordinates (cycle). */ static isl_bool is_acyclic(__isl_take isl_map *path) { … } /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D * and a dimension specification (Z^{n+1} -> Z^{n+1}), * construct a map that is an overapproximation of the map * that takes an element from the space D \times Z to another * element from the same space, such that the first n coordinates of the * difference between them is a sum of differences between images * and pre-images in one of the R_i and such that the last coordinate * is equal to the number of steps taken. * That is, let * * \Delta_i = { y - x | (x, y) in R_i } * * then the constructed map is an overapproximation of * * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : * d = (\sum_i k_i \delta_i, \sum_i k_i) } * * The elements of the singleton \Delta_i's are collected as the * rows of the steps matrix. For all these \Delta_i's together, * a single path is constructed. * For each of the other \Delta_i's, we compute an overapproximation * of the paths along elements of \Delta_i. * Since each of these paths performs an addition, composition is * symmetric and we can simply compose all resulting paths in any order. */ static __isl_give isl_map *construct_extended_path(__isl_take isl_space *space, __isl_keep isl_map *map, int *project) { … } static isl_bool isl_set_overlaps(__isl_keep isl_set *set1, __isl_keep isl_set *set2) { … } /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D * and a dimension specification (Z^{n+1} -> Z^{n+1}), * construct a map that is an overapproximation of the map * that takes an element from the dom R \times Z to an * element from ran R \times Z, such that the first n coordinates of the * difference between them is a sum of differences between images * and pre-images in one of the R_i and such that the last coordinate * is equal to the number of steps taken. * That is, let * * \Delta_i = { y - x | (x, y) in R_i } * * then the constructed map is an overapproximation of * * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : * d = (\sum_i k_i \delta_i, \sum_i k_i) and * x in dom R and x + d in ran R and * \sum_i k_i >= 1 } */ static __isl_give isl_map *construct_component(__isl_take isl_space *space, __isl_keep isl_map *map, isl_bool *exact, int project) { … } /* Call construct_component and, if "project" is set, project out * the final coordinates. */ static __isl_give isl_map *construct_projected_component( __isl_take isl_space *space, __isl_keep isl_map *map, isl_bool *exact, int project) { … } /* Compute an extended version, i.e., with path lengths, of * an overapproximation of the transitive closure of "bmap" * with path lengths greater than or equal to zero and with * domain and range equal to "dom". */ static __isl_give isl_map *q_closure(__isl_take isl_space *space, __isl_take isl_set *dom, __isl_keep isl_basic_map *bmap, isl_bool *exact) { … } /* Check whether qc has any elements of length at least one * with domain and/or range outside of dom and ran. */ static isl_bool has_spurious_elements(__isl_keep isl_map *qc, __isl_keep isl_set *dom, __isl_keep isl_set *ran) { … } #define LEFT … #define RIGHT … /* For each basic map in "map", except i, check whether it combines * with the transitive closure that is reflexive on C combines * to the left and to the right. * * In particular, if * * dom map_j \subseteq C * * then right[j] is set to 1. Otherwise, if * * ran map_i \cap dom map_j = \emptyset * * then right[j] is set to 0. Otherwise, composing to the right * is impossible. * * Similar, for composing to the left, we have if * * ran map_j \subseteq C * * then left[j] is set to 1. Otherwise, if * * dom map_i \cap ran map_j = \emptyset * * then left[j] is set to 0. Otherwise, composing to the left * is impossible. * * The return value is or'd with LEFT if composing to the left * is possible and with RIGHT if composing to the right is possible. */ static int composability(__isl_keep isl_set *C, int i, isl_set **dom, isl_set **ran, int *left, int *right, __isl_keep isl_map *map) { … } static __isl_give isl_map *anonymize(__isl_take isl_map *map) { … } /* Return a map that is a union of the basic maps in "map", except i, * composed to left and right with qc based on the entries of "left" * and "right". */ static __isl_give isl_map *compose(__isl_keep isl_map *map, int i, __isl_take isl_map *qc, int *left, int *right) { … } /* Compute the transitive closure of "map" incrementally by * computing * * map_i^+ \cup qc^+ * * or * * map_i^+ \cup ((id \cup map_i^) \circ qc^+) * * or * * map_i^+ \cup (qc^+ \circ (id \cup map_i^)) * * depending on whether left or right are NULL. */ static __isl_give isl_map *compute_incremental( __isl_take isl_space *space, __isl_keep isl_map *map, int i, __isl_take isl_map *qc, int *left, int *right, isl_bool *exact) { … } /* Given a map "map", try to find a basic map such that * map^+ can be computed as * * map^+ = map_i^+ \cup * \bigcup_j ((map_i^+ \cup Id_C)^+ \circ map_j \circ (map_i^+ \cup Id_C))^+ * * with C the simple hull of the domain and range of the input map. * map_i^ \cup Id_C is computed by allowing the path lengths to be zero * and by intersecting domain and range with C. * Of course, we need to check that this is actually equal to map_i^ \cup Id_C. * Also, we only use the incremental computation if all the transitive * closures are exact and if the number of basic maps in the union, * after computing the integer divisions, is smaller than the number * of basic maps in the input map. */ static isl_bool incremental_on_entire_domain(__isl_keep isl_space *space, __isl_keep isl_map *map, isl_set **dom, isl_set **ran, int *left, int *right, __isl_give isl_map **res) { … } /* Try and compute the transitive closure of "map" as * * map^+ = map_i^+ \cup * \bigcup_j ((map_i^+ \cup Id_C)^+ \circ map_j \circ (map_i^+ \cup Id_C))^+ * * with C either the simple hull of the domain and range of the entire * map or the simple hull of domain and range of map_i. */ static __isl_give isl_map *incremental_closure(__isl_take isl_space *space, __isl_keep isl_map *map, isl_bool *exact, int project) { … } /* Given an array of sets "set", add "dom" at position "pos" * and search for elements at earlier positions that overlap with "dom". * If any can be found, then merge all of them, together with "dom", into * a single set and assign the union to the first in the array, * which becomes the new group leader for all groups involved in the merge. * During the search, we only consider group leaders, i.e., those with * group[i] = i, as the other sets have already been combined * with one of the group leaders. */ static int merge(isl_set **set, int *group, __isl_take isl_set *dom, int pos) { … } /* Construct a map [x] -> [x+1], with parameters prescribed by "space". */ static __isl_give isl_map *increment(__isl_take isl_space *space) { … } /* Replace each entry in the n by n grid of maps by the cross product * with the relation { [i] -> [i + 1] }. */ static isl_stat add_length(__isl_keep isl_map *map, isl_map ***grid, int n) { … } /* The core of the Floyd-Warshall algorithm. * Updates the given n x x matrix of relations in place. * * The algorithm iterates over all vertices. In each step, the whole * matrix is updated to include all paths that go to the current vertex, * possibly stay there a while (including passing through earlier vertices) * and then come back. At the start of each iteration, the diagonal * element corresponding to the current vertex is replaced by its * transitive closure to account for all indirect paths that stay * in the current vertex. */ static void floyd_warshall_iterate(isl_map ***grid, int n, isl_bool *exact) { … } /* Given a partition of the domains and ranges of the basic maps in "map", * apply the Floyd-Warshall algorithm with the elements in the partition * as vertices. * * In particular, there are "n" elements in the partition and "group" is * an array of length 2 * map->n with entries in [0,n-1]. * * We first construct a matrix of relations based on the partition information, * apply Floyd-Warshall on this matrix of relations and then take the * union of all entries in the matrix as the final result. * * If we are actually computing the power instead of the transitive closure, * i.e., when "project" is not set, then the result should have the * path lengths encoded as the difference between an extra pair of * coordinates. We therefore apply the nested transitive closures * to relations that include these lengths. In particular, we replace * the input relation by the cross product with the unit length relation * { [i] -> [i + 1] }. */ static __isl_give isl_map *floyd_warshall_with_groups( __isl_take isl_space *space, __isl_keep isl_map *map, isl_bool *exact, int project, int *group, int n) { … } /* Partition the domains and ranges of the n basic relations in list * into disjoint cells. * * To find the partition, we simply consider all of the domains * and ranges in turn and combine those that overlap. * "set" contains the partition elements and "group" indicates * to which partition element a given domain or range belongs. * The domain of basic map i corresponds to element 2 * i in these arrays, * while the domain corresponds to element 2 * i + 1. * During the construction group[k] is either equal to k, * in which case set[k] contains the union of all the domains and * ranges in the corresponding group, or is equal to some l < k, * with l another domain or range in the same group. */ static int *setup_groups(isl_ctx *ctx, __isl_keep isl_basic_map **list, int n, isl_set ***set, int *n_group) { … } /* Check if the domains and ranges of the basic maps in "map" can * be partitioned, and if so, apply Floyd-Warshall on the elements * of the partition. Note that we also apply this algorithm * if we want to compute the power, i.e., when "project" is not set. * However, the results are unlikely to be exact since the recursive * calls inside the Floyd-Warshall algorithm typically result in * non-linear path lengths quite quickly. */ static __isl_give isl_map *floyd_warshall(__isl_take isl_space *space, __isl_keep isl_map *map, isl_bool *exact, int project) { … } /* Structure for representing the nodes of the graph of which * strongly connected components are being computed. * * list contains the actual nodes * check_closed is set if we may have used the fact that * a pair of basic maps can be interchanged */ struct isl_tc_follows_data { … }; /* Check whether in the computation of the transitive closure * "list[i]" (R_1) should follow (or be part of the same component as) * "list[j]" (R_2). * * That is check whether * * R_1 \circ R_2 * * is a subset of * * R_2 \circ R_1 * * If so, then there is no reason for R_1 to immediately follow R_2 * in any path. * * *check_closed is set if the subset relation holds while * R_1 \circ R_2 is not empty. */ static isl_bool basic_map_follows(int i, int j, void *user) { … } /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D * and a dimension specification (Z^{n+1} -> Z^{n+1}), * construct a map that is an overapproximation of the map * that takes an element from the dom R \times Z to an * element from ran R \times Z, such that the first n coordinates of the * difference between them is a sum of differences between images * and pre-images in one of the R_i and such that the last coordinate * is equal to the number of steps taken. * If "project" is set, then these final coordinates are not included, * i.e., a relation of type Z^n -> Z^n is returned. * That is, let * * \Delta_i = { y - x | (x, y) in R_i } * * then the constructed map is an overapproximation of * * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : * d = (\sum_i k_i \delta_i, \sum_i k_i) and * x in dom R and x + d in ran R } * * or * * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : * d = (\sum_i k_i \delta_i) and * x in dom R and x + d in ran R } * * if "project" is set. * * We first split the map into strongly connected components, perform * the above on each component and then join the results in the correct * order, at each join also taking in the union of both arguments * to allow for paths that do not go through one of the two arguments. */ static __isl_give isl_map *construct_power_components( __isl_take isl_space *space, __isl_keep isl_map *map, isl_bool *exact, int project) { … } /* Given a union of basic maps R = \cup_i R_i \subseteq D \times D, * construct a map that is an overapproximation of the map * that takes an element from the space D to another * element from the same space, such that the difference between * them is a strictly positive sum of differences between images * and pre-images in one of the R_i. * The number of differences in the sum is equated to parameter "param". * That is, let * * \Delta_i = { y - x | (x, y) in R_i } * * then the constructed map is an overapproximation of * * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : * d = \sum_i k_i \delta_i and k = \sum_i k_i > 0 } * or * * { (x) -> (x + d) | \exists k_i >= 0, \delta_i \in \Delta_i : * d = \sum_i k_i \delta_i and \sum_i k_i > 0 } * * if "project" is set. * * If "project" is not set, then * we construct an extended mapping with an extra coordinate * that indicates the number of steps taken. In particular, * the difference in the last coordinate is equal to the number * of steps taken to move from a domain element to the corresponding * image element(s). */ static __isl_give isl_map *construct_power(__isl_keep isl_map *map, isl_bool *exact, int project) { … } /* Compute the positive powers of "map", or an overapproximation. * If the result is exact, then *exact is set to 1. * * If project is set, then we are actually interested in the transitive * closure, so we can use a more relaxed exactness check. * The lengths of the paths are also projected out instead of being * encoded as the difference between an extra pair of final coordinates. */ static __isl_give isl_map *map_power(__isl_take isl_map *map, isl_bool *exact, int project) { … } /* Compute the positive powers of "map", or an overapproximation. * The result maps the exponent to a nested copy of the corresponding power. * If the result is exact, then *exact is set to 1. * map_power constructs an extended relation with the path lengths * encoded as the difference between the final coordinates. * In the final step, this difference is equated to an extra parameter * and made positive. The extra coordinates are subsequently projected out * and the parameter is turned into the domain of the result. */ __isl_give isl_map *isl_map_power(__isl_take isl_map *map, isl_bool *exact) { … } /* Compute a relation that maps each element in the range of the input * relation to the lengths of all paths composed of edges in the input * relation that end up in the given range element. * The result may be an overapproximation, in which case *exact is set to 0. * The resulting relation is very similar to the power relation. * The difference are that the domain has been projected out, the * range has become the domain and the exponent is the range instead * of a parameter. */ __isl_give isl_map *isl_map_reaching_path_lengths(__isl_take isl_map *map, isl_bool *exact) { … } /* Given a map, compute the smallest superset of this map that is of the form * * { i -> j : L <= j - i <= U and exists a_p: j_p - i_p = M_p a_p } * * (where p ranges over the (non-parametric) dimensions), * compute the transitive closure of this map, i.e., * * { i -> j : exists k > 0: * k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p } * * and intersect domain and range of this transitive closure with * the given domain and range. * * If with_id is set, then try to include as much of the identity mapping * as possible, by computing * * { i -> j : exists k >= 0: * k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p } * * instead (i.e., allow k = 0). * * In practice, we compute the difference set * * delta = { j - i | i -> j in map }, * * look for stride constraint on the individual dimensions and compute * (constant) lower and upper bounds for each individual dimension, * adding a constraint for each bound not equal to infinity. */ static __isl_give isl_map *box_closure_on_domain(__isl_take isl_map *map, __isl_take isl_set *dom, __isl_take isl_set *ran, int with_id) { … } /* Given a map, compute the smallest superset of this map that is of the form * * { i -> j : L <= j - i <= U and exists a_p: j_p - i_p = M_p a_p } * * (where p ranges over the (non-parametric) dimensions), * compute the transitive closure of this map, i.e., * * { i -> j : exists k > 0: * k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p } * * and intersect domain and range of this transitive closure with * domain and range of the original map. */ static __isl_give isl_map *box_closure(__isl_take isl_map *map) { … } /* Given a map, compute the smallest superset of this map that is of the form * * { i -> j : L <= j - i <= U and exists a_p: j_p - i_p = M_p a_p } * * (where p ranges over the (non-parametric) dimensions), * compute the transitive and partially reflexive closure of this map, i.e., * * { i -> j : exists k >= 0: * k L <= j - i <= k U and exists a: j_p - i_p = M_p a_p } * * and intersect domain and range of this transitive closure with * the given domain. */ static __isl_give isl_map *box_closure_with_identity(__isl_take isl_map *map, __isl_take isl_set *dom) { … } /* Check whether app is the transitive closure of map. * In particular, check that app is acyclic and, if so, * check that * * app \subset (map \cup (map \circ app)) */ static isl_bool check_exactness_omega(__isl_keep isl_map *map, __isl_keep isl_map *app) { … } /* Check if basic map M_i can be combined with all the other * basic maps such that * * (\cup_j M_j)^+ * * can be computed as * * M_i \cup (\cup_{j \ne i} M_i^* \circ M_j \circ M_i^*)^+ * * In particular, check if we can compute a compact representation * of * * M_i^* \circ M_j \circ M_i^* * * for each j != i. * Let M_i^? be an extension of M_i^+ that allows paths * of length zero, i.e., the result of box_closure(., 1). * The criterion, as proposed by Kelly et al., is that * id = M_i^? - M_i^+ can be represented as a basic map * and that * * id \circ M_j \circ id = M_j * * for each j != i. * * If this function returns 1, then tc and qc are set to * M_i^+ and M_i^?, respectively. */ static int can_be_split_off(__isl_keep isl_map *map, int i, __isl_give isl_map **tc, __isl_give isl_map **qc) { … } static __isl_give isl_map *box_closure_with_check(__isl_take isl_map *map, isl_bool *exact) { … } /* Compute an overapproximation of the transitive closure of "map" * using a variation of the algorithm from * "Transitive Closure of Infinite Graphs and its Applications" * by Kelly et al. * * We first check whether we can can split of any basic map M_i and * compute * * (\cup_j M_j)^+ * * as * * M_i \cup (\cup_{j \ne i} M_i^* \circ M_j \circ M_i^*)^+ * * using a recursive call on the remaining map. * * If not, we simply call box_closure on the whole map. */ static __isl_give isl_map *transitive_closure_omega(__isl_take isl_map *map, isl_bool *exact) { … } /* Compute the transitive closure of "map", or an overapproximation. * If the result is exact, then *exact is set to 1. * Simply use map_power to compute the powers of map, but tell * it to project out the lengths of the paths instead of equating * the length to a parameter. */ __isl_give isl_map *isl_map_transitive_closure(__isl_take isl_map *map, isl_bool *exact) { … } static isl_stat inc_count(__isl_take isl_map *map, void *user) { … } static isl_stat collect_basic_map(__isl_take isl_map *map, void *user) { … } /* Perform Floyd-Warshall on the given list of basic relations. * The basic relations may live in different dimensions, * but basic relations that get assigned to the diagonal of the * grid have domains and ranges of the same dimension and so * the standard algorithm can be used because the nested transitive * closures are only applied to diagonal elements and because all * compositions are performed on relations with compatible domains and ranges. */ static __isl_give isl_union_map *union_floyd_warshall_on_list(isl_ctx *ctx, __isl_keep isl_basic_map **list, int n, isl_bool *exact) { … } /* Perform Floyd-Warshall on the given union relation. * The implementation is very similar to that for non-unions. * The main difference is that it is applied unconditionally. * We first extract a list of basic maps from the union map * and then perform the algorithm on this list. */ static __isl_give isl_union_map *union_floyd_warshall( __isl_take isl_union_map *umap, isl_bool *exact) { … } /* Decompose the give union relation into strongly connected components. * The implementation is essentially the same as that of * construct_power_components with the major difference that all * operations are performed on union maps. */ static __isl_give isl_union_map *union_components( __isl_take isl_union_map *umap, isl_bool *exact) { … } /* Compute the transitive closure of "umap", or an overapproximation. * If the result is exact, then *exact is set to 1. */ __isl_give isl_union_map *isl_union_map_transitive_closure( __isl_take isl_union_map *umap, isl_bool *exact) { … } struct isl_union_power { … }; static isl_stat power(__isl_take isl_map *map, void *user) { … } /* Construct a map [[x]->[y]] -> [y-x], with parameters prescribed by "space". */ static __isl_give isl_union_map *deltas_map(__isl_take isl_space *space) { … } /* Compute the positive powers of "map", or an overapproximation. * The result maps the exponent to a nested copy of the corresponding power. * If the result is exact, then *exact is set to 1. */ __isl_give isl_union_map *isl_union_map_power(__isl_take isl_union_map *umap, isl_bool *exact) { … } #undef TYPE #define TYPE … #include "isl_power_templ.c" #undef TYPE #define TYPE … #include "isl_power_templ.c"
Codebase Browser
llvm