| /* |
| * 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) |
| { |
| int i; |
| isl_ctx *ctx; |
| isl_size nvar; |
| size_t prefix_len = strlen(prefix); |
| |
| if (!space) |
| return NULL; |
| |
| ctx = isl_space_get_ctx(space); |
| nvar = isl_space_dim(space, isl_dim_set); |
| if (nvar < 0) |
| return isl_space_free(space); |
| |
| for (i = 0; i < nvar; ++i) { |
| const char *name; |
| char *prefix_name; |
| |
| name = isl_space_get_dim_name(space, isl_dim_set, i); |
| if (!name) |
| continue; |
| |
| prefix_name = isl_alloc_array(ctx, char, |
| prefix_len + strlen(name) + 1); |
| if (!prefix_name) |
| goto error; |
| memcpy(prefix_name, prefix, prefix_len); |
| strcpy(prefix_name + prefix_len, name); |
| |
| space = isl_space_set_dim_name(space, |
| isl_dim_set, i, prefix_name); |
| free(prefix_name); |
| } |
| |
| return space; |
| error: |
| isl_space_free(space); |
| return NULL; |
| } |
| |
| /* 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) |
| { |
| isl_space *space_param; |
| isl_size nvar; |
| isl_size nparam; |
| |
| nvar = isl_space_dim(space, isl_dim_set); |
| nparam = isl_space_dim(space, isl_dim_param); |
| if (nvar < 0 || nparam < 0) |
| return isl_space_free(space); |
| space_param = isl_space_copy(space); |
| space_param = isl_space_drop_dims(space_param, isl_dim_set, 0, nvar); |
| space_param = isl_space_move_dims(space_param, isl_dim_set, 0, |
| isl_dim_param, 0, nparam); |
| space_param = isl_space_prefix(space_param, "c_"); |
| space_param = isl_space_insert_dims(space_param, isl_dim_set, 0, 1); |
| space_param = isl_space_set_dim_name(space_param, |
| isl_dim_set, 0, "c_cst"); |
| space = isl_space_drop_dims(space, isl_dim_param, 0, nparam); |
| space = isl_space_prefix(space, "c_"); |
| space = isl_space_join(isl_space_from_domain(space_param), |
| isl_space_from_range(space)); |
| space = isl_space_wrap(space); |
| space = isl_space_set_tuple_name(space, isl_dim_set, "coefficients"); |
| |
| return 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) |
| { |
| int i; |
| isl_size n; |
| size_t prefix_len = strlen(prefix); |
| |
| n = isl_space_dim(space, type); |
| if (n < 0) |
| return isl_space_free(space); |
| |
| for (i = 0; i < n; ++i) { |
| const char *name; |
| |
| name = isl_space_get_dim_name(space, type, i); |
| if (!name) |
| continue; |
| if (strncmp(name, prefix, prefix_len)) |
| continue; |
| |
| space = isl_space_set_dim_name(space, |
| type, i, name + prefix_len); |
| } |
| |
| return space; |
| } |
| |
| /* 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) |
| { |
| isl_size nparam; |
| |
| space = isl_space_unwrap(space); |
| space = isl_space_drop_dims(space, isl_dim_in, 0, 1); |
| space = isl_space_unprefix(space, isl_dim_in, "c_"); |
| space = isl_space_unprefix(space, isl_dim_out, "c_"); |
| nparam = isl_space_dim(space, isl_dim_in); |
| if (nparam < 0) |
| return isl_space_free(space); |
| space = isl_space_move_dims(space, |
| isl_dim_param, 0, isl_dim_in, 0, nparam); |
| space = isl_space_range(space); |
| |
| return space; |
| } |
| |
| /* Return the rational universe basic set in the given space. |
| */ |
| static __isl_give isl_basic_set *rational_universe(__isl_take isl_space *space) |
| { |
| isl_basic_set *bset; |
| |
| bset = isl_basic_set_universe(space); |
| bset = isl_basic_set_set_rational(bset); |
| |
| return bset; |
| } |
| |
| /* 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) |
| { |
| int i, j, k; |
| isl_ctx *ctx; |
| isl_space *space; |
| isl_basic_set *dual = NULL; |
| isl_size total; |
| |
| total = isl_basic_set_dim(bset, isl_dim_all); |
| if (total < 0) |
| return isl_basic_set_free(bset); |
| |
| ctx = isl_basic_set_get_ctx(bset); |
| space = isl_space_set_alloc(ctx, 0, total + shift); |
| if (isl_basic_set_plain_is_empty(bset)) { |
| isl_basic_set_free(bset); |
| return rational_universe(space); |
| } |
| |
| dual = isl_basic_set_alloc_space(space, bset->n_eq + bset->n_ineq, |
| total, bset->n_ineq + (shift > 0)); |
| dual = isl_basic_set_set_rational(dual); |
| |
| for (i = 0; i < bset->n_eq + bset->n_ineq; ++i) { |
| k = isl_basic_set_alloc_div(dual); |
| if (k < 0) |
| goto error; |
| isl_int_set_si(dual->div[k][0], 0); |
| } |
| |
| for (i = 0; i < total; ++i) { |
| k = isl_basic_set_alloc_equality(dual); |
| if (k < 0) |
| goto error; |
| isl_seq_clr(dual->eq[k], 1 + shift + total); |
| isl_int_set_si(dual->eq[k][1 + shift + i], -1); |
| for (j = 0; j < bset->n_eq; ++j) |
| isl_int_set(dual->eq[k][1 + shift + total + j], |
| bset->eq[j][1 + i]); |
| for (j = 0; j < bset->n_ineq; ++j) |
| isl_int_set(dual->eq[k][1 + shift + total + bset->n_eq + j], |
| bset->ineq[j][1 + i]); |
| } |
| |
| for (i = 0; i < bset->n_ineq; ++i) { |
| k = isl_basic_set_alloc_inequality(dual); |
| if (k < 0) |
| goto error; |
| isl_seq_clr(dual->ineq[k], |
| 1 + shift + total + bset->n_eq + bset->n_ineq); |
| isl_int_set_si(dual->ineq[k][1 + shift + total + bset->n_eq + i], 1); |
| } |
| |
| if (shift > 0) { |
| k = isl_basic_set_alloc_inequality(dual); |
| if (k < 0) |
| goto error; |
| isl_seq_clr(dual->ineq[k], 2 + total); |
| isl_int_set_si(dual->ineq[k][1], 1); |
| for (j = 0; j < bset->n_eq; ++j) |
| isl_int_neg(dual->ineq[k][2 + total + j], |
| bset->eq[j][0]); |
| for (j = 0; j < bset->n_ineq; ++j) |
| isl_int_neg(dual->ineq[k][2 + total + bset->n_eq + j], |
| bset->ineq[j][0]); |
| } |
| |
| dual = isl_basic_set_remove_divs(dual); |
| dual = isl_basic_set_simplify(dual); |
| dual = isl_basic_set_finalize(dual); |
| |
| isl_basic_set_free(bset); |
| return dual; |
| error: |
| isl_basic_set_free(bset); |
| isl_basic_set_free(dual); |
| return NULL; |
| } |
| |
| /* 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 farkas(bset, 1); |
| } |
| |
| /* Return the inverse mapping of "morph". |
| */ |
| static __isl_give isl_mat *peek_inv(__isl_keep isl_morph *morph) |
| { |
| return morph ? morph->inv : NULL; |
| } |
| |
| /* Return a copy of the inverse mapping of "morph". |
| */ |
| static __isl_give isl_mat *get_inv(__isl_keep isl_morph *morph) |
| { |
| return isl_mat_copy(peek_inv(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 { |
| isl_basic_set *coeff; |
| int start; |
| int dim; |
| int n_line; |
| int n_ray; |
| int n_vertex; |
| int pos; |
| }; |
| |
| /* 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 { |
| int n; |
| int pos; |
| int start_next; |
| struct isl_coefficients_factor_data *factors; |
| }; |
| |
| /* 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) |
| { |
| data->n = n; |
| data->pos = 0; |
| data->start_next = 0; |
| data->factors = isl_calloc_array(ctx, |
| struct isl_coefficients_factor_data, n); |
| if (!data->factors) |
| return isl_stat_error; |
| return isl_stat_ok; |
| } |
| |
| /* Free all memory allocated in "data". |
| */ |
| static void isl_coefficients_product_data_clear( |
| struct isl_coefficients_product_data *data) |
| { |
| int i; |
| |
| if (data->factors) { |
| for (i = 0; i < data->n; ++i) { |
| isl_basic_set_free(data->factors[i].coeff); |
| } |
| } |
| free(data->factors); |
| } |
| |
| /* 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) |
| { |
| return isl_int_is_zero(bset->ineq[ineq][1]); |
| } |
| |
| /* 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) |
| { |
| struct isl_coefficients_product_data *data = user; |
| isl_basic_set *coeff; |
| isl_size n_eq, n_ineq, dim; |
| int i, n_ray, n_vertex; |
| |
| coeff = isl_basic_set_coefficients_base(isl_basic_set_copy(bset)); |
| data->factors[data->pos].coeff = coeff; |
| if (!coeff) |
| return isl_bool_error; |
| |
| dim = isl_basic_set_dim(bset, isl_dim_set); |
| n_eq = isl_basic_set_n_equality(coeff); |
| n_ineq = isl_basic_set_n_inequality(coeff); |
| if (dim < 0 || n_eq < 0 || n_ineq < 0) |
| return isl_bool_error; |
| n_ray = n_vertex = 0; |
| for (i = 0; i < n_ineq; ++i) { |
| if (is_ray(coeff, i)) |
| n_ray++; |
| else |
| n_vertex++; |
| } |
| data->factors[data->pos].start = data->start_next; |
| data->factors[data->pos].dim = dim; |
| data->factors[data->pos].n_line = n_eq; |
| data->factors[data->pos].n_ray = n_ray; |
| data->factors[data->pos].n_vertex = n_vertex; |
| data->pos++; |
| data->start_next += dim; |
| |
| return isl_bool_true; |
| } |
| |
| /* 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) |
| { |
| isl_seq_clr(entry, 1 + 1 + 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) |
| { |
| isl_seq_cpy(entry + 1 + 1 + data->start, src + 1 + 1, data->dim); |
| } |
| |
| /* 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) |
| { |
| isl_seq_scale(entry + 1 + 1 + data->start, src + 1 + 1, f, data->dim); |
| } |
| |
| /* 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) |
| { |
| int i; |
| |
| for (i = 0; i < factor->n_line; ++i) { |
| int k; |
| |
| k = isl_basic_set_alloc_equality(bset); |
| if (k < 0) |
| return isl_basic_set_free(bset); |
| clear_entry(bset->eq[k], total); |
| set_factor(bset->eq[k], factor->coeff->eq[i], factor); |
| } |
| |
| return bset; |
| } |
| |
| /* 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) |
| { |
| int i; |
| int n_ineq = data->n_ray + data->n_vertex; |
| |
| for (i = 0; i < n_ineq; ++i) { |
| int k; |
| |
| if (!is_ray(data->coeff, i)) |
| continue; |
| |
| k = isl_basic_set_alloc_inequality(bset); |
| if (k < 0) |
| return isl_basic_set_free(bset); |
| clear_entry(bset->ineq[k], total); |
| set_factor(bset->ineq[k], data->coeff->ineq[i], data); |
| } |
| |
| return bset; |
| } |
| |
| /* 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) |
| { |
| int j; |
| int n = factor->n_ray + factor->n_vertex; |
| |
| for (j = start; j < n; ++j) { |
| if (is_ray(factor->coeff, j)) |
| continue; |
| factor->pos = j; |
| return 1; |
| } |
| |
| return 0; |
| } |
| |
| /* 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) |
| { |
| int i; |
| |
| for (i = first; i < data->n; ++i) |
| factor_first_vertex(&data->factors[i], 0); |
| } |
| |
| /* 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) |
| { |
| int i; |
| |
| for (i = data->n - 1; i >= 0; --i) { |
| struct isl_coefficients_factor_data *factor = &data->factors[i]; |
| |
| if (!factor_first_vertex(factor, factor->pos + 1)) |
| continue; |
| first_vertex(data, i + 1); |
| return 1; |
| } |
| |
| return 0; |
| } |
| |
| /* 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) |
| { |
| int i; |
| int k; |
| isl_int lcm, f; |
| |
| k = isl_basic_set_alloc_inequality(bset); |
| if (k < 0) |
| return isl_basic_set_free(bset); |
| |
| isl_int_init(lcm); |
| isl_int_init(f); |
| isl_int_set_si(lcm, 1); |
| for (i = 0; i < data->n; ++i) { |
| struct isl_coefficients_factor_data *factor = &data->factors[i]; |
| isl_basic_set *coeff = factor->coeff; |
| int pos = factor->pos; |
| isl_int_lcm(lcm, lcm, coeff->ineq[pos][1]); |
| } |
| isl_int_set_si(bset->ineq[k][0], 0); |
| isl_int_set(bset->ineq[k][1], lcm); |
| |
| for (i = 0; i < data->n; ++i) { |
| struct isl_coefficients_factor_data *factor = &data->factors[i]; |
| isl_basic_set *coeff = factor->coeff; |
| int pos = factor->pos; |
| isl_int_divexact(f, lcm, coeff->ineq[pos][1]); |
| scale_factor(bset->ineq[k], coeff->ineq[pos], f, factor); |
| } |
| |
| isl_int_clear(f); |
| isl_int_clear(lcm); |
| |
| return bset; |
| } |
| |
| /* 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) |
| { |
| int i; |
| int n_line, n_ray, n_vertex; |
| int total; |
| isl_space *space; |
| isl_basic_set *product; |
| |
| if (!data->factors) |
| return NULL; |
| |
| total = data->start_next; |
| |
| n_line = 0; |
| n_ray = 0; |
| n_vertex = 1; |
| for (i = 0; i < data->n; ++i) { |
| n_line += data->factors[i].n_line; |
| n_ray += data->factors[i].n_ray; |
| n_vertex *= data->factors[i].n_vertex; |
| } |
| |
| space = isl_space_set_alloc(ctx, 0, 1 + total); |
| if (n_vertex == 0) |
| return rational_universe(space); |
| product = isl_basic_set_alloc_space(space, 0, n_line, n_ray + n_vertex); |
| product = isl_basic_set_set_rational(product); |
| |
| for (i = 0; i < data->n; ++i) |
| product = add_lines(product, &data->factors[i], total); |
| for (i = 0; i < data->n; ++i) |
| product = add_rays(product, &data->factors[i], total); |
| |
| first_vertex(data, 0); |
| do { |
| product = add_vertex(product, data); |
| } while (next_vertex(data)); |
| |
| return product; |
| } |
| |
| /* 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) |
| { |
| struct isl_coefficients_product_data data; |
| isl_ctx *ctx; |
| isl_basic_set *coeff; |
| isl_bool every; |
| |
| ctx = isl_factorizer_get_ctx(f); |
| if (isl_coefficients_product_data_init(ctx, &data, f->n_group) < 0) |
| f = isl_factorizer_free(f); |
| every = isl_factorizer_every_factor_basic_set(f, |
| &isl_basic_set_coefficients_factor, &data); |
| isl_factorizer_free(f); |
| if (every >= 0) |
| coeff = construct_product(ctx, &data); |
| else |
| coeff = NULL; |
| isl_coefficients_product_data_clear(&data); |
| |
| return coeff; |
| } |
| |
| /* 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) |
| { |
| isl_bool is_identity; |
| isl_space *space; |
| isl_mat *inv; |
| isl_multi_aff *ma; |
| isl_basic_set *coeff; |
| |
| if (!f) |
| goto error; |
| is_identity = isl_mat_is_scaled_identity(peek_inv(f->morph)); |
| if (is_identity < 0) |
| goto error; |
| if (is_identity) |
| return isl_basic_set_coefficients_product(f); |
| |
| inv = get_inv(f->morph); |
| inv = isl_mat_transpose(inv); |
| inv = isl_mat_lin_to_aff(inv); |
| |
| coeff = isl_basic_set_coefficients_product(f); |
| space = isl_space_map_from_set(isl_basic_set_get_space(coeff)); |
| ma = isl_multi_aff_from_aff_mat(space, inv); |
| coeff = isl_basic_set_preimage_multi_aff(coeff, ma); |
| |
| return coeff; |
| error: |
| isl_factorizer_free(f); |
| return NULL; |
| } |
| |
| /* 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) |
| { |
| isl_factorizer *f; |
| isl_size nparam; |
| |
| nparam = isl_basic_set_dim(bset, isl_dim_param); |
| if (nparam < 0) |
| return isl_basic_set_free(bset); |
| bset = isl_basic_set_move_dims(bset, isl_dim_set, 0, |
| isl_dim_param, 0, nparam); |
| |
| f = isl_basic_set_factorizer(bset); |
| if (!f) |
| return isl_basic_set_free(bset); |
| if (f->n_group > 0) { |
| isl_basic_set_free(bset); |
| return isl_basic_set_coefficients_morphed_product(f); |
| } |
| isl_factorizer_free(f); |
| return isl_basic_set_coefficients_base(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) |
| { |
| isl_space *space; |
| |
| if (!bset) |
| return NULL; |
| if (bset->n_div) |
| isl_die(bset->ctx, isl_error_invalid, |
| "input set not allowed to have local variables", |
| goto error); |
| |
| space = isl_basic_set_get_space(bset); |
| space = isl_space_coefficients(space); |
| |
| bset = basic_set_coefficients(bset); |
| bset = isl_basic_set_reset_space(bset, space); |
| return bset; |
| error: |
| isl_basic_set_free(bset); |
| return NULL; |
| } |
| |
| /* 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) |
| { |
| isl_space *space; |
| |
| if (!bset) |
| return NULL; |
| if (bset->n_div) |
| isl_die(bset->ctx, isl_error_invalid, |
| "input set not allowed to have local variables", |
| goto error); |
| |
| space = isl_basic_set_get_space(bset); |
| space = isl_space_solutions(space); |
| |
| bset = farkas(bset, -1); |
| bset = isl_basic_set_reset_space(bset, space); |
| return bset; |
| error: |
| isl_basic_set_free(bset); |
| return NULL; |
| } |
| |
| /* 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) |
| { |
| int i; |
| isl_basic_set *coeff; |
| |
| if (!set) |
| return NULL; |
| if (set->n == 0) { |
| isl_space *space = isl_set_get_space(set); |
| space = isl_space_coefficients(space); |
| isl_set_free(set); |
| return rational_universe(space); |
| } |
| |
| coeff = isl_basic_set_coefficients(isl_basic_set_copy(set->p[0])); |
| |
| for (i = 1; i < set->n; ++i) { |
| isl_basic_set *bset, *coeff_i; |
| bset = isl_basic_set_copy(set->p[i]); |
| coeff_i = isl_basic_set_coefficients(bset); |
| coeff = isl_basic_set_intersect(coeff, coeff_i); |
| } |
| |
| isl_set_free(set); |
| return coeff; |
| } |
| |
| /* 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) |
| { |
| return isl_basic_set_coefficients(bset); |
| } |
| |
| /* 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) |
| { |
| return isl_basic_set_list_map(list, &coefficients_wrap, NULL); |
| } |
| |
| /* 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) |
| { |
| int i; |
| isl_basic_set *sol; |
| |
| if (!set) |
| return NULL; |
| if (set->n == 0) { |
| isl_space *space = isl_set_get_space(set); |
| space = isl_space_solutions(space); |
| isl_set_free(set); |
| return rational_universe(space); |
| } |
| |
| sol = isl_basic_set_solutions(isl_basic_set_copy(set->p[0])); |
| |
| for (i = 1; i < set->n; ++i) { |
| isl_basic_set *bset, *sol_i; |
| bset = isl_basic_set_copy(set->p[i]); |
| sol_i = isl_basic_set_solutions(bset); |
| sol = isl_basic_set_intersect(sol, sol_i); |
| } |
| |
| isl_set_free(set); |
| return sol; |
| } |