/*
* Copyright 2008-2009 Katholieke Universiteit Leuven
* Copyright 2010 INRIA Saclay
- * Copyright 2012 Ecole Normale Superieure
+ * Copyright 2012-2013 Ecole Normale Superieure
*
* Use of this software is governed by the MIT license
*
#include <isl_local_space_private.h>
#include <isl_aff_private.h>
#include <isl_options_private.h>
+#include <isl_morph.h>
static unsigned n(__isl_keep isl_space *dim, enum isl_dim_type type)
{
return isl_basic_map_drop_equality((struct isl_basic_map *)bset, pos);
}
+/* Turn inequality "pos" of "bmap" into an equality.
+ *
+ * In particular, we move the inequality in front of the equalities
+ * and move the last inequality in the position of the moved inequality.
+ * Note that isl_tab_make_equalities_explicit depends on this particular
+ * change in the ordering of the constraints.
+ */
void isl_basic_map_inequality_to_equality(
struct isl_basic_map *bmap, unsigned pos)
{
isl_basic_map_set_to_empty((struct isl_basic_map *)bset);
}
-void isl_basic_map_swap_div(struct isl_basic_map *bmap, int a, int b)
+/* Swap divs "a" and "b" in "bmap" (without modifying any of the constraints
+ * of "bmap").
+ */
+static void swap_div(__isl_keep isl_basic_map *bmap, int a, int b)
{
- int i;
- unsigned off = isl_space_dim(bmap->dim, isl_dim_all);
isl_int *t = bmap->div[a];
bmap->div[a] = bmap->div[b];
bmap->div[b] = t;
+}
+
+/* Swap divs "a" and "b" in "bmap" and adjust the constraints and
+ * div definitions accordingly.
+ */
+void isl_basic_map_swap_div(struct isl_basic_map *bmap, int a, int b)
+{
+ int i;
+ unsigned off = isl_space_dim(bmap->dim, isl_dim_all);
+
+ swap_div(bmap, a, b);
for (i = 0; i < bmap->n_eq; ++i)
isl_int_swap(bmap->eq[i][1+off+a], bmap->eq[i][1+off+b]);
res = isl_basic_map_set_rational(res);
if (isl_basic_map_plain_is_empty(bmap)) {
isl_basic_map_free(bmap);
+ free(dim_map);
return isl_basic_map_set_to_empty(res);
}
res = isl_basic_map_add_constraints_dim_map(res, bmap, dim_map);
return res;
}
-/* Turn the n dimensions of type type, starting at first
- * into existentially quantified variables.
+/* Insert "n" rows in the divs of "bmap".
+ *
+ * The number of columns is not changed, which means that the last
+ * dimensions of "bmap" are being reintepreted as the new divs.
+ * The space of "bmap" is not adjusted, however, which means
+ * that "bmap" is left in an inconsistent state. Removing "n" dimensions
+ * from the space of "bmap" is the responsibility of the caller.
*/
-__isl_give isl_basic_map *isl_basic_map_project_out(
- __isl_take isl_basic_map *bmap,
- enum isl_dim_type type, unsigned first, unsigned n)
+static __isl_give isl_basic_map *insert_div_rows(__isl_take isl_basic_map *bmap,
+ int n)
{
int i;
size_t row_size;
isl_int **new_div;
isl_int *old;
- if (n == 0)
- return basic_map_space_reset(bmap, type);
-
- if (!bmap)
- return NULL;
-
- if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
- return isl_basic_map_remove_dims(bmap, type, first, n);
-
- isl_assert(bmap->ctx, first + n <= isl_basic_map_dim(bmap, type),
- goto error);
-
- bmap = move_last(bmap, type, first, n);
bmap = isl_basic_map_cow(bmap);
if (!bmap)
return NULL;
bmap->block2 = isl_blk_extend(bmap->ctx, bmap->block2,
(bmap->extra + n) * (1 + row_size));
if (!bmap->block2.data)
- goto error;
+ return isl_basic_map_free(bmap);
new_div = isl_alloc_array(bmap->ctx, isl_int *, bmap->extra + n);
if (!new_div)
- goto error;
+ return isl_basic_map_free(bmap);
for (i = 0; i < n; ++i) {
new_div[i] = bmap->block2.data +
(bmap->extra + i) * (1 + row_size);
bmap->n_div += n;
bmap->extra += n;
+ return bmap;
+}
+
+/* Turn the n dimensions of type type, starting at first
+ * into existentially quantified variables.
+ */
+__isl_give isl_basic_map *isl_basic_map_project_out(
+ __isl_take isl_basic_map *bmap,
+ enum isl_dim_type type, unsigned first, unsigned n)
+{
+ if (n == 0)
+ return basic_map_space_reset(bmap, type);
+
+ if (!bmap)
+ return NULL;
+
+ if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
+ return isl_basic_map_remove_dims(bmap, type, first, n);
+
+ isl_assert(bmap->ctx, first + n <= isl_basic_map_dim(bmap, type),
+ goto error);
+
+ bmap = move_last(bmap, type, first, n);
+ bmap = isl_basic_map_cow(bmap);
+ bmap = insert_div_rows(bmap, n);
+ if (!bmap)
+ return NULL;
+
bmap->dim = isl_space_drop_dims(bmap->dim, type, first, n);
if (!bmap->dim)
goto error;
dom, empty);
}
+/* Compute the lexicographic minimum (or maximum if "max" is set)
+ * of "bmap" over its domain.
+ *
+ * Since we are not interested in the part of the domain space where
+ * there is no solution, we initialize the domain to those constraints
+ * of "bmap" that only involve the parameters and the input dimensions.
+ * This relieves the parametric programming engine from detecting those
+ * inequalities and transferring them to the context. More importantly,
+ * it ensures that those inequalities are transferred first and not
+ * intermixed with inequalities that actually split the domain.
+ */
__isl_give isl_map *isl_basic_map_lexopt(__isl_take isl_basic_map *bmap, int max)
{
- struct isl_basic_set *dom = NULL;
- isl_space *dom_dim;
+ int n_div;
+ int n_out;
+ isl_basic_map *copy;
+ isl_basic_set *dom;
- if (!bmap)
- goto error;
- dom_dim = isl_space_domain(isl_space_copy(bmap->dim));
- dom = isl_basic_set_universe(dom_dim);
+ n_div = isl_basic_map_dim(bmap, isl_dim_div);
+ n_out = isl_basic_map_dim(bmap, isl_dim_out);
+ copy = isl_basic_map_copy(bmap);
+ copy = isl_basic_map_drop_constraints_involving_dims(copy,
+ isl_dim_div, 0, n_div);
+ copy = isl_basic_map_drop_constraints_involving_dims(copy,
+ isl_dim_out, 0, n_out);
+ dom = isl_basic_map_domain(copy);
return isl_basic_map_partial_lexopt(bmap, dom, NULL, max);
-error:
- isl_basic_map_free(bmap);
- return NULL;
}
__isl_give isl_map *isl_basic_map_lexmin(__isl_take isl_basic_map *bmap)
return (isl_set *)isl_basic_map_lexmax((isl_basic_map *)bset);
}
-__isl_give isl_set *isl_set_lexmin(__isl_take isl_set *set)
-{
- return (isl_set *)isl_map_lexmin((isl_map *)set);
-}
-
-__isl_give isl_set *isl_set_lexmax(__isl_take isl_set *set)
-{
- return (isl_set *)isl_map_lexmax((isl_map *)set);
-}
-
/* Extract the first and only affine expression from list
* and then add it to *pwaff with the given dom.
* This domain is known to be disjoint from other domains
return NULL;
}
+/* Given a basic set "bset" that only involves parameters and existentially
+ * quantified variables, return the index of the first equality
+ * that only involves parameters. If there is no such equality then
+ * return bset->n_eq.
+ *
+ * This function assumes that isl_basic_set_gauss has been called on "bset".
+ */
+static int first_parameter_equality(__isl_keep isl_basic_set *bset)
+{
+ int i, j;
+ unsigned nparam, n_div;
+
+ if (!bset)
+ return -1;
+
+ nparam = isl_basic_set_dim(bset, isl_dim_param);
+ n_div = isl_basic_set_dim(bset, isl_dim_div);
+
+ for (i = 0, j = n_div - 1; i < bset->n_eq && j >= 0; --j) {
+ if (!isl_int_is_zero(bset->eq[i][1 + nparam + j]))
+ ++i;
+ }
+
+ return i;
+}
+
+/* Compute an explicit representation for the existentially quantified
+ * variables in "bset" by computing the "minimal value" of the set
+ * variables. Since there are no set variables, the computation of
+ * the minimal value essentially computes an explicit representation
+ * of the non-empty part(s) of "bset".
+ *
+ * The input only involves parameters and existentially quantified variables.
+ * All equalities among parameters have been removed.
+ *
+ * Since the existentially quantified variables in the result are in general
+ * going to be different from those in the input, we first replace
+ * them by the minimal number of variables based on their equalities.
+ * This should simplify the parametric integer programming.
+ */
+static __isl_give isl_set *base_compute_divs(__isl_take isl_basic_set *bset)
+{
+ isl_morph *morph1, *morph2;
+ isl_set *set;
+ unsigned n;
+
+ if (!bset)
+ return NULL;
+ if (bset->n_eq == 0)
+ return isl_basic_set_lexmin(bset);
+
+ morph1 = isl_basic_set_parameter_compression(bset);
+ bset = isl_morph_basic_set(isl_morph_copy(morph1), bset);
+ bset = isl_basic_set_lift(bset);
+ morph2 = isl_basic_set_variable_compression(bset, isl_dim_set);
+ bset = isl_morph_basic_set(morph2, bset);
+ n = isl_basic_set_dim(bset, isl_dim_set);
+ bset = isl_basic_set_project_out(bset, isl_dim_set, 0, n);
+
+ set = isl_basic_set_lexmin(bset);
+
+ set = isl_morph_set(isl_morph_inverse(morph1), set);
+
+ return set;
+}
+
/* Project the given basic set onto its parameter domain, possibly introducing
* new, explicit, existential variables in the constraints.
* The input has parameters and (possibly implicit) existential variables.
* among the parameters by performing a variable compression on
* the parameters. Afterward, an inverse transformation is performed
* and the equalities among the parameters are inserted back in.
+ *
+ * The variable compression on the parameters may uncover additional
+ * equalities that were only implicit before. We therefore check
+ * if there are any new parameter equalities in the result and
+ * if so recurse. The removal of parameter equalities is required
+ * for the parameter compression performed by base_compute_divs.
*/
static struct isl_set *parameter_compute_divs(struct isl_basic_set *bset)
{
- int i, j;
+ int i;
struct isl_mat *eq;
struct isl_mat *T, *T2;
struct isl_set *set;
- unsigned nparam, n_div;
+ unsigned nparam;
bset = isl_basic_set_cow(bset);
if (!bset)
return NULL;
if (bset->n_eq == 0)
- return isl_basic_set_lexmin(bset);
-
- isl_basic_set_gauss(bset, NULL);
+ return base_compute_divs(bset);
- nparam = isl_basic_set_dim(bset, isl_dim_param);
- n_div = isl_basic_set_dim(bset, isl_dim_div);
+ bset = isl_basic_set_gauss(bset, NULL);
+ if (!bset)
+ return NULL;
+ if (isl_basic_set_plain_is_empty(bset))
+ return isl_set_from_basic_set(bset);
- for (i = 0, j = n_div - 1; i < bset->n_eq && j >= 0; --j) {
- if (!isl_int_is_zero(bset->eq[i][1 + nparam + j]))
- ++i;
- }
+ i = first_parameter_equality(bset);
if (i == bset->n_eq)
- return isl_basic_set_lexmin(bset);
+ return base_compute_divs(bset);
+ nparam = isl_basic_set_dim(bset, isl_dim_param);
eq = isl_mat_sub_alloc6(bset->ctx, bset->eq, i, bset->n_eq - i,
0, 1 + nparam);
eq = isl_mat_cow(eq);
}
bset = basic_set_parameter_preimage(bset, T);
- set = isl_basic_set_lexmin(bset);
+ i = first_parameter_equality(bset);
+ if (!bset)
+ set = NULL;
+ else if (i == bset->n_eq)
+ set = base_compute_divs(bset);
+ else
+ set = parameter_compute_divs(bset);
set = set_parameter_preimage(set, T2);
set = set_append_equalities(set, eq);
return set;
}
-/* Compute an explicit representation for all the existentially
- * quantified variables.
- * The input and output dimensions are first turned into parameters.
- * compute_divs then returns a map with the same parameters and
+/* Insert the divs from "ls" before those of "bmap".
+ *
+ * The number of columns is not changed, which means that the last
+ * dimensions of "bmap" are being reintepreted as the divs from "ls".
+ * The caller is responsible for removing the same number of dimensions
+ * from the space of "bmap".
+ */
+static __isl_give isl_basic_map *insert_divs_from_local_space(
+ __isl_take isl_basic_map *bmap, __isl_keep isl_local_space *ls)
+{
+ int i;
+ int n_div;
+ int old_n_div;
+
+ n_div = isl_local_space_dim(ls, isl_dim_div);
+ if (n_div == 0)
+ return bmap;
+
+ old_n_div = bmap->n_div;
+ bmap = insert_div_rows(bmap, n_div);
+ if (!bmap)
+ return NULL;
+
+ for (i = 0; i < n_div; ++i) {
+ isl_seq_cpy(bmap->div[i], ls->div->row[i], ls->div->n_col);
+ isl_seq_clr(bmap->div[i] + ls->div->n_col, old_n_div);
+ }
+
+ return bmap;
+}
+
+/* Replace the space of "bmap" by the space and divs of "ls".
+ *
+ * If "ls" has any divs, then we simplify the result since we may
+ * have discovered some additional equalities that could simplify
+ * the div expressions.
+ */
+static __isl_give isl_basic_map *basic_replace_space_by_local_space(
+ __isl_take isl_basic_map *bmap, __isl_take isl_local_space *ls)
+{
+ int n_div;
+
+ bmap = isl_basic_map_cow(bmap);
+ if (!bmap || !ls)
+ goto error;
+
+ n_div = isl_local_space_dim(ls, isl_dim_div);
+ bmap = insert_divs_from_local_space(bmap, ls);
+ if (!bmap)
+ goto error;
+
+ isl_space_free(bmap->dim);
+ bmap->dim = isl_local_space_get_space(ls);
+ if (!bmap->dim)
+ goto error;
+
+ isl_local_space_free(ls);
+ if (n_div > 0)
+ bmap = isl_basic_map_simplify(bmap);
+ bmap = isl_basic_map_finalize(bmap);
+ return bmap;
+error:
+ isl_basic_map_free(bmap);
+ isl_local_space_free(ls);
+ return NULL;
+}
+
+/* Replace the space of "map" by the space and divs of "ls".
+ */
+static __isl_give isl_map *replace_space_by_local_space(__isl_take isl_map *map,
+ __isl_take isl_local_space *ls)
+{
+ int i;
+
+ map = isl_map_cow(map);
+ if (!map || !ls)
+ goto error;
+
+ for (i = 0; i < map->n; ++i) {
+ map->p[i] = basic_replace_space_by_local_space(map->p[i],
+ isl_local_space_copy(ls));
+ if (!map->p[i])
+ goto error;
+ }
+ isl_space_free(map->dim);
+ map->dim = isl_local_space_get_space(ls);
+ if (!map->dim)
+ goto error;
+
+ isl_local_space_free(ls);
+ return map;
+error:
+ isl_local_space_free(ls);
+ isl_map_free(map);
+ return NULL;
+}
+
+/* Compute an explicit representation for the existentially
+ * quantified variables for which do not know any explicit representation yet.
+ *
+ * We first sort the existentially quantified variables so that the
+ * existentially quantified variables for which we already have an explicit
+ * representation are placed before those for which we do not.
+ * The input dimensions, the output dimensions and the existentially
+ * quantified variables for which we already have an explicit
+ * representation are then turned into parameters.
+ * compute_divs returns a map with the same parameters and
* no input or output dimensions and the dimension specification
- * is reset to that of the input.
+ * is reset to that of the input, including the existentially quantified
+ * variables for which we already had an explicit representation.
*/
static struct isl_map *compute_divs(struct isl_basic_map *bmap)
{
struct isl_basic_set *bset;
struct isl_set *set;
struct isl_map *map;
- isl_space *dim, *orig_dim = NULL;
+ isl_space *dim;
+ isl_local_space *ls;
unsigned nparam;
unsigned n_in;
unsigned n_out;
+ unsigned n_known;
+ int i;
+ bmap = isl_basic_map_sort_divs(bmap);
bmap = isl_basic_map_cow(bmap);
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;
+
nparam = isl_basic_map_dim(bmap, isl_dim_param);
n_in = isl_basic_map_dim(bmap, isl_dim_in);
n_out = isl_basic_map_dim(bmap, isl_dim_out);
- dim = isl_space_set_alloc(bmap->ctx, nparam + n_in + n_out, 0);
+ dim = isl_space_set_alloc(bmap->ctx,
+ nparam + n_in + n_out + n_known, 0);
if (!dim)
goto error;
- orig_dim = bmap->dim;
- bmap->dim = dim;
+ ls = isl_basic_map_get_local_space(bmap);
+ ls = isl_local_space_drop_dims(ls, isl_dim_div,
+ n_known, bmap->n_div - n_known);
+ if (n_known > 0) {
+ for (i = n_known; i < bmap->n_div; ++i)
+ swap_div(bmap, i - n_known, i);
+ bmap->n_div -= n_known;
+ bmap->extra -= n_known;
+ }
+ bmap = isl_basic_map_reset_space(bmap, dim);
bset = (struct isl_basic_set *)bmap;
set = parameter_compute_divs(bset);
map = (struct isl_map *)set;
- map = isl_map_reset_space(map, orig_dim);
+ map = replace_space_by_local_space(map, ls);
return map;
error:
int l1, l2;
unsigned size = isl_min(c1->size, c2->size);
- l1 = isl_seq_last_non_zero(c1->c, size);
- l2 = isl_seq_last_non_zero(c2->c, size);
+ l1 = isl_seq_last_non_zero(c1->c + 1, size);
+ l2 = isl_seq_last_non_zero(c2->c + 1, size);
if (l1 != l2)
return l1 - l2;
- return isl_seq_cmp(c1->c, c2->c, size);
+ return isl_seq_cmp(c1->c + 1, c2->c + 1, size);
}
static struct isl_basic_map *isl_basic_map_sort_constraints(
if (!isl_basic_map_can_curry(bmap))
isl_die(bmap->ctx, isl_error_invalid,
"basic map cannot be curried", goto error);
+ bmap = isl_basic_map_cow(bmap);
+ if (!bmap)
+ return NULL;
bmap->dim = isl_space_curry(bmap->dim);
if (!bmap->dim)
goto error;
isl_die(bmap->ctx, isl_error_invalid,
"basic map cannot be uncurried",
return isl_basic_map_free(bmap));
+ bmap = isl_basic_map_cow(bmap);
+ if (!bmap)
+ return NULL;
bmap->dim = isl_space_uncurry(bmap->dim);
if (!bmap->dim)
return isl_basic_map_free(bmap);
projects / platform / upstream / isl.git / blobdiff