isl_map_coalesce: avoid dropping constraints redundant wrt implicit equalities

isl_map_coalesce first detects implicit equalities in the basic maps.
If two basic maps can indeed be coalesced, then fuse() would
only add this constraint to the fused basic map as an inequality.
Other constraints that imply that this constraint is actually an equality
are redundant with respect to the equality and would not get copied
inside fuse() either.  The end result is that we would lose information.

In principle, we could just modify fuse() to add the implicit equalities
to the fused basic map as equalities, but it seems more prudent to
turn them into explicit equalities from the start.

Reported-by: Tobias Grosser <tobias@grosser.es>
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>

diff --git a/isl_coalesce.c b/isl_coalesce.c
index c68ce20..c2c3bb4 100644 (file)
--- a/isl_coalesce.c
+++ b/isl_coalesce.c
@@ -1533,6 +1533,16 @@ error:
 /* For each pair of basic maps in the map, check if the union of the two
  * can be represented by a single basic map.
  * If so, replace the pair by the single basic map and start over.
+ *
+ * Since we are constructing the tableaus of the basic maps anyway,
+ * we exploit them to detect implicit equalities and redundant constraints.
+ * This also helps the coalescing as it can ignore the redundant constraints.
+ * In order to avoid confusion, we make all implicit equalities explicit
+ * in the basic maps.  We don't call isl_basic_map_gauss, though,
+ * as that may affect the number of constraints.
+ * This means that we have to call isl_basic_map_gauss at the end
+ * of the computation to ensure that the basic maps are not left
+ * in an unexpected state.
  */
 struct isl_map *isl_map_coalesce(struct isl_map *map)
 {
@@ -1562,6 +1572,10 @@ struct isl_map *isl_map_coalesce(struct isl_map *map)
                if (!ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_NO_IMPLICIT))
                        if (isl_tab_detect_implicit_equalities(tabs[i]) < 0)
                                goto error;
+               map->p[i] = isl_tab_make_equalities_explicit(tabs[i],
+                                                               map->p[i]);
+               if (!map->p[i])
+                       goto error;
                if (!ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_NO_REDUNDANT))
                        if (isl_tab_detect_redundant(tabs[i]) < 0)
                                goto error;
@@ -1576,6 +1590,7 @@ struct isl_map *isl_map_coalesce(struct isl_map *map)
                for (i = 0; i < map->n; ++i) {
                        map->p[i] = isl_basic_map_update_from_tab(map->p[i],
                                                                    tabs[i]);
+                       map->p[i] = isl_basic_map_gauss(map->p[i], NULL);
                        map->p[i] = isl_basic_map_finalize(map->p[i]);
                        if (!map->p[i])
                                goto error;

diff --git a/isl_map.c b/isl_map.c
index d08f8c4..c7ac138 100644 (file)
--- a/isl_map.c
+++ b/isl_map.c
@@ -1145,6 +1145,13 @@ int isl_basic_set_drop_equality(struct isl_basic_set *bset, unsigned pos)
        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)
 {

diff --git a/isl_tab.c b/isl_tab.c
index 3fc0367..35ff7fc 100644 (file)
--- a/isl_tab.c
+++ b/isl_tab.c
@@ -1,10 +1,12 @@
 /*
  * Copyright 2008-2009 Katholieke Universiteit Leuven
+ * Copyright 2013      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 Ecole Normale Superieure, 45 rue d'Ulm, 75230 Paris, France
  */
 
 #include <isl_ctx_private.h>
@@ -2699,6 +2701,106 @@ int isl_tab_detect_implicit_equalities(struct isl_tab *tab)
        return 0;
 }
 
+/* Update the element of row_var or col_var that corresponds to
+ * constraint tab->con[i] to a move from position "old" to position "i".
+ */
+static int update_con_after_move(struct isl_tab *tab, int i, int old)
+{
+       int *p;
+       int index;
+
+       index = tab->con[i].index;
+       if (index == -1)
+               return 0;
+       p = tab->con[i].is_row ? tab->row_var : tab->col_var;
+       if (p[index] != ~old)
+               isl_die(tab->mat->ctx, isl_error_internal,
+                       "broken internal state", return -1);
+       p[index] = ~i;
+
+       return 0;
+}
+
+/* Rotate the "n" constraints starting at "first" to the right,
+ * putting the last constraint in the position of the first constraint.
+ */
+static int rotate_constraints(struct isl_tab *tab, int first, int n)
+{
+       int i, last;
+       struct isl_tab_var var;
+
+       if (n <= 1)
+               return 0;
+
+       last = first + n - 1;
+       var = tab->con[last];
+       for (i = last; i > first; --i) {
+               tab->con[i] = tab->con[i - 1];
+               if (update_con_after_move(tab, i, i - 1) < 0)
+                       return -1;
+       }
+       tab->con[first] = var;
+       if (update_con_after_move(tab, first, last) < 0)
+               return -1;
+
+       return 0;
+}
+
+/* Make the equalities that are implicit in "bmap" but that have been
+ * detected in the corresponding "tab" explicit in "bmap" and update
+ * "tab" to reflect the new order of the constraints.
+ *
+ * In particular, if inequality i is an implicit equality then
+ * isl_basic_map_inequality_to_equality will move the inequality
+ * in front of the other equality and it will move the last inequality
+ * in the position of inequality i.
+ * In the tableau, the inequalities of "bmap" are stored after the equalities
+ * and so the original order
+ *
+ *             E E E E E A A A I B B B B L
+ *
+ * is changed into
+ *
+ *             I E E E E E A A A L B B B B
+ *
+ * where I is the implicit equality, the E are equalities,
+ * the A inequalities before I, the B inequalities after I and
+ * L the last inequality.
+ * We therefore need to rotate to the right two sets of constraints,
+ * those up to and including I and those after I.
+ *
+ * If "tab" contains any constraints that are not in "bmap" then they
+ * appear after those in "bmap" and they should be left untouched.
+ *
+ * Note that this function leaves "bmap" in a temporary state
+ * as it does not call isl_basic_map_gauss.  Calling this function
+ * is the responsibility of the caller.
+ */
+__isl_give isl_basic_map *isl_tab_make_equalities_explicit(struct isl_tab *tab,
+       __isl_take isl_basic_map *bmap)
+{
+       int i;
+
+       if (!tab || !bmap)
+               return isl_basic_map_free(bmap);
+       if (tab->empty)
+               return bmap;
+
+       for (i = bmap->n_ineq - 1; i >= 0; --i) {
+               if (!isl_tab_is_equality(tab, bmap->n_eq + i))
+                       continue;
+               isl_basic_map_inequality_to_equality(bmap, i);
+               if (rotate_constraints(tab, 0, tab->n_eq + i + 1) < 0)
+                       return isl_basic_map_free(bmap);
+               if (rotate_constraints(tab, tab->n_eq + i + 1,
+                                       bmap->n_ineq - i) < 0)
+                       return isl_basic_map_free(bmap);
+               tab->n_eq++;
+       }
+
+       return bmap;
+}
+
 static int con_is_redundant(struct isl_tab *tab, struct isl_tab_var *var)
 {
        if (!tab)

diff --git a/isl_tab.h b/isl_tab.h
index 139bd34..b48db73 100644 (file)
--- a/isl_tab.h
+++ b/isl_tab.h
@@ -193,6 +193,8 @@ struct isl_basic_map *isl_basic_map_update_from_tab(struct isl_basic_map *bmap,
 struct isl_basic_set *isl_basic_set_update_from_tab(struct isl_basic_set *bset,
        struct isl_tab *tab);
 int isl_tab_detect_implicit_equalities(struct isl_tab *tab) WARN_UNUSED;
+__isl_give isl_basic_map *isl_tab_make_equalities_explicit(struct isl_tab *tab,
+       __isl_take isl_basic_map *bmap);
 int isl_tab_detect_redundant(struct isl_tab *tab) WARN_UNUSED;
 #define ISL_TAB_SAVE_DUAL      (1 << 0)
 enum isl_lp_result isl_tab_min(struct isl_tab *tab,

diff --git a/isl_test.c b/isl_test.c
index 7c28f65..4be52e5 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -1185,6 +1185,19 @@ int test_coalesce(struct isl_ctx *ctx)
        if (test_coalesce_set(ctx, "{ [i,j] : exists a,b : i = 2a and j = 3b; "
                                     "[i,j] : exists a : j = 3a }", 1) < 0)
                return -1;
+       if (test_coalesce_set(ctx,
+               "{ [a, b, c] : (c <= 7 - b and b <= 1 and b >= 0 and "
+                       "c >= 3 + b and b <= 3 + 8a and b >= -26 + 8a and "
+                       "a >= 3) or "
+                   "(b <= 1 and c <= 7 and b >= 0 and c >= 4 + b and "
+                       "b <= 3 + 8a and b >= -26 + 8a and a >= 3) }", 1) < 0)
+               return -1;
+       if (test_coalesce_set(ctx,
+               "{ [a, 0, c] : c >= 1 and c <= 29 and c >= -1 + 8a and "
+                               "c <= 6 + 8a and a >= 3; "
+                   "[a, -1, c] : c >= 1 and c <= 30 and c >= 8a and "
+                               "c <= 7 + 8a and a >= 3 and a <= 4 }", 1) < 0)
+               return -1;
        return 0;
 }