/* * 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_map_private.h> #include <isl/set.h> #include <isl_space_private.h> #include <isl_seq.h> #include <isl_aff_private.h> #include <isl_mat_private.h> #include <isl_factorization.h> /* * Let C be a cone and define * * C' := { y | forall x in C : y x >= 0 } * * C' contains the coefficients of all linear constraints * that are valid for C. * Furthermore, C'' = C. * * If C is defined as { x | A x >= 0 } * then any element in C' must be a non-negative combination * of the rows of A, i.e., y = t A with t >= 0. That is, * * C' = { y | exists t >= 0 : y = t A } * * If any of the rows in A actually represents an equality, then * also negative combinations of this row are allowed and so the * non-negativity constraint on the corresponding element of t * can be dropped. * * A polyhedron P = { x | b + A x >= 0 } can be represented * in homogeneous coordinates by the cone * C = { [z,x] | b z + A x >= and z >= 0 } * The valid linear constraints on C correspond to the valid affine * constraints on P. * This is essentially Farkas' lemma. * * Since * [ 1 0 ] * [ w y ] = [t_0 t] [ b A ] * * we have * * C' = { w, y | exists t_0, t >= 0 : y = t A and w = t_0 + t b } * or * * C' = { w, y | exists t >= 0 : y = t A and w - t b >= 0 } * * In practice, we introduce an extra variable (w), shifting all * other variables to the right, and an extra inequality * (w - t b >= 0) corresponding to the positivity constraint on * the homogeneous coordinate. * * When going back from coefficients to solutions, we immediately * plug in 1 for z, which corresponds to shifting all variables * to the left, with the leftmost ending up in the constant position. */ /* Add the given prefix to all named isl_dim_set dimensions in "space". */ static __isl_give isl_space *isl_space_prefix(__isl_take isl_space *space, const char *prefix) { … } /* Given a dimension specification of the solutions space, construct * a dimension specification for the space of coefficients. * * In particular transform * * [params] -> { S } * * to * * { coefficients[[cst, params] -> S] } * * and prefix each dimension name with "c_". */ static __isl_give isl_space *isl_space_coefficients(__isl_take isl_space *space) { … } /* Drop the given prefix from all named dimensions of type "type" in "space". */ static __isl_give isl_space *isl_space_unprefix(__isl_take isl_space *space, enum isl_dim_type type, const char *prefix) { … } /* Given a dimension specification of the space of coefficients, construct * a dimension specification for the space of solutions. * * In particular transform * * { coefficients[[cst, params] -> S] } * * to * * [params] -> { S } * * and drop the "c_" prefix from the dimension names. */ static __isl_give isl_space *isl_space_solutions(__isl_take isl_space *space) { … } /* Return the rational universe basic set in the given space. */ static __isl_give isl_basic_set *rational_universe(__isl_take isl_space *space) { … } /* Compute the dual of "bset" by applying Farkas' lemma. * As explained above, we add an extra dimension to represent * the coefficient of the constant term when going from solutions * to coefficients (shift == 1) and we drop the extra dimension when going * in the opposite direction (shift == -1). * The dual can be created in an arbitrary space. * The caller is responsible for putting the result in the appropriate space. * * If "bset" is (obviously) empty, then the way this emptiness * is represented by the constraints does not allow for the application * of the standard farkas algorithm. We therefore handle this case * specifically and return the universe basic set. */ static __isl_give isl_basic_set *farkas(__isl_take isl_basic_set *bset, int shift) { … } /* Construct a basic set containing the tuples of coefficients of all * valid affine constraints on the given basic set, ignoring * the space of input and output and without any further decomposition. */ static __isl_give isl_basic_set *isl_basic_set_coefficients_base( __isl_take isl_basic_set *bset) { … } /* Return the inverse mapping of "morph". */ static __isl_give isl_mat *peek_inv(__isl_keep isl_morph *morph) { … } /* Return a copy of the inverse mapping of "morph". */ static __isl_give isl_mat *get_inv(__isl_keep isl_morph *morph) { … } /* Information about a single factor within isl_basic_set_coefficients_product. * * "start" is the position of the first coefficient (beyond * the one corresponding to the constant term) in this factor. * "dim" is the number of coefficients (other than * the one corresponding to the constant term) in this factor. * "n_line" is the number of lines in "coeff". * "n_ray" is the number of rays (other than lines) in "coeff". * "n_vertex" is the number of vertices in "coeff". * * While iterating over the vertices, * "pos" represents the inequality constraint corresponding * to the current vertex. */ struct isl_coefficients_factor_data { … }; /* Internal data structure for isl_basic_set_coefficients_product. * "n" is the number of factors in the factorization. * "pos" is the next factor that will be considered. * "start_next" is the position of the first coefficient (beyond * the one corresponding to the constant term) in the next factor. * "factors" contains information about the individual "n" factors. */ struct isl_coefficients_product_data { … }; /* Initialize the internal data structure for * isl_basic_set_coefficients_product. */ static isl_stat isl_coefficients_product_data_init(isl_ctx *ctx, struct isl_coefficients_product_data *data, int n) { … } /* Free all memory allocated in "data". */ static void isl_coefficients_product_data_clear( struct isl_coefficients_product_data *data) { … } /* Does inequality "ineq" in the (dual) basic set "bset" represent a ray? * In particular, does it have a zero denominator * (i.e., a zero coefficient for the constant term)? */ static int is_ray(__isl_keep isl_basic_set *bset, int ineq) { … } /* isl_factorizer_every_factor_basic_set callback that * constructs a basic set containing the tuples of coefficients of all * valid affine constraints on the factor "bset" and * extracts further information that will be used * when combining the results over the different factors. */ static isl_bool isl_basic_set_coefficients_factor( __isl_keep isl_basic_set *bset, void *user) { … } /* Clear an entry in the product, given that there is a "total" number * of coefficients (other than that of the constant term). */ static void clear_entry(isl_int *entry, int total) { … } /* Set the part of the entry corresponding to factor "data", * from the factor coefficients in "src". */ static void set_factor(isl_int *entry, isl_int *src, struct isl_coefficients_factor_data *data) { … } /* Set the part of the entry corresponding to factor "data", * from the factor coefficients in "src" multiplied by "f". */ static void scale_factor(isl_int *entry, isl_int *src, isl_int f, struct isl_coefficients_factor_data *data) { … } /* Add all lines from the given factor to "bset", * given that there is a "total" number of coefficients * (other than that of the constant term). */ static __isl_give isl_basic_set *add_lines(__isl_take isl_basic_set *bset, struct isl_coefficients_factor_data *factor, int total) { … } /* Add all rays (other than lines) from the given factor to "bset", * given that there is a "total" number of coefficients * (other than that of the constant term). */ static __isl_give isl_basic_set *add_rays(__isl_take isl_basic_set *bset, struct isl_coefficients_factor_data *data, int total) { … } /* Move to the first vertex of the given factor starting * at inequality constraint "start", setting factor->pos and * returning 1 if a vertex is found. */ static int factor_first_vertex(struct isl_coefficients_factor_data *factor, int start) { … } /* Move to the first constraint in each factor starting at "first" * that represents a vertex. * In particular, skip the initial constraints that correspond to rays. */ static void first_vertex(struct isl_coefficients_product_data *data, int first) { … } /* Move to the next vertex in the product. * In particular, move to the next vertex of the last factor. * If all vertices of this last factor have already been considered, * then move to the next vertex of the previous factor(s) * until a factor is found that still has a next vertex. * Once such a next vertex has been found, the subsequent * factors are reset to the first vertex. * Return 1 if any next vertex was found. */ static int next_vertex(struct isl_coefficients_product_data *data) { … } /* Add a vertex to the product "bset" combining the currently selected * vertices of the factors. * * In the dual representation, the constant term is always zero. * The vertex itself is the sum of the contributions of the factors * with a shared denominator in position 1. * * First compute the shared denominator (lcm) and * then scale the numerators to this shared denominator. */ static __isl_give isl_basic_set *add_vertex(__isl_take isl_basic_set *bset, struct isl_coefficients_product_data *data) { … } /* Combine the duals of the factors in the factorization of a basic set * to form the dual of the entire basic set. * The dual share the coefficient of the constant term. * All other coefficients are specific to a factor. * Any constraint not involving the coefficient of the constant term * can therefor simply be copied into the appropriate position. * This includes all equality constraints since the coefficient * of the constant term can always be increased and therefore * never appears in an equality constraint. * The inequality constraints involving the coefficient of * the constant term need to be combined across factors. * In particular, if this coefficient needs to be greater than or equal * to some linear combination of the other coefficients in each factor, * then it needs to be greater than or equal to the sum of * these linear combinations across the factors. * * Alternatively, the constraints of the dual can be seen * as the vertices, rays and lines of the original basic set. * Clearly, rays and lines can simply be copied, * while vertices needs to be combined across factors. * This means that the number of rays and lines in the product * is equal to the sum of the numbers in the factors, * while the number of vertices is the product * of the number of vertices in the factors. Note that each * factor has at least one vertex. * The only exception is when the factor is the dual of an obviously empty set, * in which case a universe dual is created. * In this case, return a universe dual for the product as well. * * While constructing the vertices, look for the first combination * of inequality constraints that represent a vertex, * construct the corresponding vertex and then move on * to the next combination of inequality constraints until * all combinations have been considered. */ static __isl_give isl_basic_set *construct_product(isl_ctx *ctx, struct isl_coefficients_product_data *data) { … } /* Given a factorization "f" of a basic set, * construct a basic set containing the tuples of coefficients of all * valid affine constraints on the product of the factors, ignoring * the space of input and output. * Note that this product may not be equal to the original basic set, * if a non-trivial transformation is involved. * This is handled by the caller. * * Compute the tuples of coefficients for each factor separately and * then combine the results. */ static __isl_give isl_basic_set *isl_basic_set_coefficients_product( __isl_take isl_factorizer *f) { … } /* Given a factorization "f" of a basic set, * construct a basic set containing the tuples of coefficients of all * valid affine constraints on the basic set, ignoring * the space of input and output. * * The factorization may involve a linear transformation of the basic set. * In particular, the transformed basic set is formulated * in terms of x' = U x, i.e., x = V x', with V = U^{-1}. * The dual is then computed in terms of y' with y'^t [z; x'] >= 0. * Plugging in y' = [1 0; 0 V^t] y yields * y^t [1 0; 0 V] [z; x'] >= 0, i.e., y^t [z; x] >= 0, which is * the desired set of coefficients y. * Note that this transformation to y' only needs to be applied * if U is not the identity matrix. */ static __isl_give isl_basic_set *isl_basic_set_coefficients_morphed_product( __isl_take isl_factorizer *f) { … } /* Construct a basic set containing the tuples of coefficients of all * valid affine constraints on the given basic set, ignoring * the space of input and output. * * The caller has already checked that "bset" does not involve * any local variables. It may have parameters, though. * Treat them as regular variables internally. * This is especially important for the factorization, * since the (original) parameters should be taken into account * explicitly in this factorization. * * Check if the basic set can be factorized. * If so, compute constraints on the coefficients of the factors * separately and combine the results. * Otherwise, compute the results for the input basic set as a whole. */ static __isl_give isl_basic_set *basic_set_coefficients( __isl_take isl_basic_set *bset) { … } /* Construct a basic set containing the tuples of coefficients of all * valid affine constraints on the given basic set. */ __isl_give isl_basic_set *isl_basic_set_coefficients( __isl_take isl_basic_set *bset) { … } /* Construct a basic set containing the elements that satisfy all * affine constraints whose coefficient tuples are * contained in the given basic set. */ __isl_give isl_basic_set *isl_basic_set_solutions( __isl_take isl_basic_set *bset) { … } /* Construct a basic set containing the tuples of coefficients of all * valid affine constraints on the given set. */ __isl_give isl_basic_set *isl_set_coefficients(__isl_take isl_set *set) { … } /* Wrapper around isl_basic_set_coefficients for use * as a isl_basic_set_list_map callback. */ static __isl_give isl_basic_set *coefficients_wrap( __isl_take isl_basic_set *bset, void *user) { … } /* Replace the elements of "list" by the result of applying * isl_basic_set_coefficients to them. */ __isl_give isl_basic_set_list *isl_basic_set_list_coefficients( __isl_take isl_basic_set_list *list) { … } /* Construct a basic set containing the elements that satisfy all * affine constraints whose coefficient tuples are * contained in the given set. */ __isl_give isl_basic_set *isl_set_solutions(__isl_take isl_set *set) { … }
Codebase Browser
llvm