isl_map_coalesce: extend the handling of a pair adjacent inequalities
authorSven Verdoolaege <skimo@kotnet.org>
Sat, 23 Mar 2013 14:55:02 +0000 (23 15:55 +0100)
committerSven Verdoolaege <skimo@kotnet.org>
Thu, 28 Mar 2013 18:11:32 +0000 (28 19:11 +0100)
In particular, one of the adjacent inequalities may imply an equality
on the integer points in the corresponding set and this equality will
not be valid for the other set.
For example, the set

{ [x,y] : 0 <= x <= 2 and y >= 0 and x + 2y <= 4;
  [x,y] : 3 <= x <= 4 and y >= 0 and x + 2y <= 4 }

may be simplified to

{ [x,y] : 0 <= x <= 2 and y >= 0 and x + 2y <= 4;
  [x,0] : 3 <= x <= 4 }

and the equality y = 0 is not valid for the other component.
However, we may still be able to fuse in such cases if all the constraints
of the other component are valid for the component with the equality and if
we can show that replacing the adjacent inequality x <= 2 by its opposite
(x >= 3) and adding the valid constraints (x <= 4) of the component with
the equality results in a subset of this component.  Since it is also
a superset of this component (all its constraints are valid for the component),
we can fuse the two components by combining their valid constraints.

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
isl_coalesce.c
isl_test.c

index bdd2cec..ed80560 100644 (file)
@@ -1,7 +1,7 @@
 /*
  * 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
  *
@@ -298,6 +298,124 @@ static int check_facets(struct isl_map *map, int i, int j,
        return fuse(map, i, j, tabs, NULL, ineq_i, NULL, ineq_j, NULL);
 }
 
+/* Check if basic map "i" contains the basic map represented
+ * by the tableau "tab".
+ */
+static int contains(struct isl_map *map, int i, int *ineq_i,
+       struct isl_tab *tab)
+{
+       int k, l;
+       unsigned dim;
+
+       dim = isl_basic_map_total_dim(map->p[i]);
+       for (k = 0; k < map->p[i]->n_eq; ++k) {
+               for (l = 0; l < 2; ++l) {
+                       int stat;
+                       isl_seq_neg(map->p[i]->eq[k], map->p[i]->eq[k], 1+dim);
+                       stat = status_in(map->p[i]->eq[k], tab);
+                       if (stat != STATUS_VALID)
+                               return 0;
+               }
+       }
+
+       for (k = 0; k < map->p[i]->n_ineq; ++k) {
+               int stat;
+               if (ineq_i[k] == STATUS_REDUNDANT)
+                       continue;
+               stat = status_in(map->p[i]->ineq[k], tab);
+               if (stat != STATUS_VALID)
+                       return 0;
+       }
+       return 1;
+}
+
+/* Basic map "i" has an inequality (say "k") that is adjacent
+ * to some inequality of basic map "j".  All the other inequalities
+ * are valid for "j".
+ * Check if basic map "j" forms an extension of basic map "i".
+ *
+ * Note that this function is only called if some of the equalities or
+ * inequalities of basic map "j" do cut basic map "i".  The function is
+ * correct even if there are no such cut constraints, but in that case
+ * the additional checks performed by this function are overkill.
+ *
+ * In particular, we replace constraint k, say f >= 0, by constraint
+ * f <= -1, add the inequalities of "j" that are valid for "i"
+ * and check if the result is a subset of basic map "j".
+ * If so, then we know that this result is exactly equal to basic map "j"
+ * since all its constraints are valid for basic map "j".
+ * By combining the valid constraints of "i" (all equalities and all
+ * inequalities except "k") and the valid constraints of "j" we therefore
+ * obtain a basic map that is equal to their union.
+ * In this case, there is no need to perform a rollback of the tableau
+ * since it is going to be destroyed in fuse().
+ *
+ *
+ *     |\__                    |\__
+ *     |   \__                 |   \__
+ *     |      \_       =>      |      \__
+ *     |_______| _             |_________\
+ *
+ *
+ *     |\                      |\
+ *     | \                     | \
+ *     |  \                    |  \
+ *     |  |                    |   \
+ *     |  ||\          =>      |    \
+ *     |  || \                 |     \
+ *     |  ||  |                |      |
+ *     |__||_/                 |_____/
+ */
+static int is_adj_ineq_extension(__isl_keep isl_map *map, int i, int j,
+       struct isl_tab **tabs, int *eq_i, int *ineq_i, int *eq_j, int *ineq_j)
+{
+       int k;
+       struct isl_tab_undo *snap;
+       unsigned n_eq = map->p[i]->n_eq;
+       unsigned total = isl_basic_map_total_dim(map->p[i]);
+       int r;
+
+       if (isl_tab_extend_cons(tabs[i], 1 + map->p[j]->n_ineq) < 0)
+               return -1;
+
+       for (k = 0; k < map->p[i]->n_ineq; ++k)
+               if (ineq_i[k] == STATUS_ADJ_INEQ)
+                       break;
+       if (k >= map->p[i]->n_ineq)
+               isl_die(isl_map_get_ctx(map), isl_error_internal,
+                       "ineq_i should have exactly one STATUS_ADJ_INEQ",
+                       return -1);
+
+       snap = isl_tab_snap(tabs[i]);
+
+       if (isl_tab_unrestrict(tabs[i], n_eq + k) < 0)
+               return -1;
+
+       isl_seq_neg(map->p[i]->ineq[k], map->p[i]->ineq[k], 1 + total);
+       isl_int_sub_ui(map->p[i]->ineq[k][0], map->p[i]->ineq[k][0], 1);
+       r = isl_tab_add_ineq(tabs[i], map->p[i]->ineq[k]);
+       isl_seq_neg(map->p[i]->ineq[k], map->p[i]->ineq[k], 1 + total);
+       isl_int_sub_ui(map->p[i]->ineq[k][0], map->p[i]->ineq[k][0], 1);
+       if (r < 0)
+               return -1;
+
+       for (k = 0; k < map->p[j]->n_ineq; ++k) {
+               if (ineq_j[k] != STATUS_VALID)
+                       continue;
+               if (isl_tab_add_ineq(tabs[i], map->p[j]->ineq[k]) < 0)
+                       return -1;
+       }
+
+       if (contains(map, j, ineq_j, tabs[i]))
+               return fuse(map, i, j, tabs, eq_i, ineq_i, eq_j, ineq_j, NULL);
+
+       if (isl_tab_rollback(tabs[i], snap) < 0)
+               return -1;
+
+       return 0;
+}
+
+
 /* Both basic maps have at least one inequality with and adjacent
  * (but opposite) inequality in the other basic map.
  * Check that there are no cut constraints and that there is only
@@ -324,53 +442,40 @@ static int check_facets(struct isl_map *map, int i, int j,
  *         |   |
  *         |   |
  *         |___|
+ *
+ * If there are some cut constraints on one side, then we may
+ * still be able to fuse the two basic maps, but we need to perform
+ * some additional checks in is_adj_ineq_extension.
  */
 static int check_adj_ineq(struct isl_map *map, int i, int j,
-       struct isl_tab **tabs, int *ineq_i, int *ineq_j)
+       struct isl_tab **tabs, int *eq_i, int *ineq_i, int *eq_j, int *ineq_j)
 {
-       int changed = 0;
+       int count_i, count_j;
+       int cut_i, cut_j;
 
-       if (any(ineq_i, map->p[i]->n_ineq, STATUS_CUT) ||
-           any(ineq_j, map->p[j]->n_ineq, STATUS_CUT))
-               /* ADJ INEQ CUT */
-               ;
-       else if (count(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) == 1 &&
-                count(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ) == 1)
-               changed = fuse(map, i, j, tabs, NULL, ineq_i, NULL, ineq_j, NULL);
-       /* else ADJ INEQ TOO MANY */
+       count_i = count(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ);
+       count_j = count(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ);
 
-       return changed;
-}
+       if (count_i != 1 && count_j != 1)
+               return 0;
 
-/* Check if basic map "i" contains the basic map represented
- * by the tableau "tab".
- */
-static int contains(struct isl_map *map, int i, int *ineq_i,
-       struct isl_tab *tab)
-{
-       int k, l;
-       unsigned dim;
+       cut_i = any(eq_i, 2 * map->p[i]->n_eq, STATUS_CUT) ||
+               any(ineq_i, map->p[i]->n_ineq, STATUS_CUT);
+       cut_j = any(eq_j, 2 * map->p[j]->n_eq, STATUS_CUT) ||
+               any(ineq_j, map->p[j]->n_ineq, STATUS_CUT);
 
-       dim = isl_basic_map_total_dim(map->p[i]);
-       for (k = 0; k < map->p[i]->n_eq; ++k) {
-               for (l = 0; l < 2; ++l) {
-                       int stat;
-                       isl_seq_neg(map->p[i]->eq[k], map->p[i]->eq[k], 1+dim);
-                       stat = status_in(map->p[i]->eq[k], tab);
-                       if (stat != STATUS_VALID)
-                               return 0;
-               }
-       }
+       if (!cut_i && !cut_j && count_i == 1 && count_j == 1)
+               return fuse(map, i, j, tabs, NULL, ineq_i, NULL, ineq_j, NULL);
 
-       for (k = 0; k < map->p[i]->n_ineq; ++k) {
-               int stat;
-               if (ineq_i[k] == STATUS_REDUNDANT)
-                       continue;
-               stat = status_in(map->p[i]->ineq[k], tab);
-               if (stat != STATUS_VALID)
-                       return 0;
-       }
-       return 1;
+       if (count_i == 1 && !cut_i)
+               return is_adj_ineq_extension(map, i, j, tabs,
+                                               eq_i, ineq_i, eq_j, ineq_j);
+
+       if (count_j == 1 && !cut_j)
+               return is_adj_ineq_extension(map, j, i, tabs,
+                                               eq_j, ineq_j, eq_i, ineq_i);
+
+       return 0;
 }
 
 /* Basic map "i" has an inequality "k" that is adjacent to some equality
@@ -391,7 +496,7 @@ static int contains(struct isl_map *map, int i, int *ineq_i,
  *       \    ||                \     |
  *        \___||                 \____|
  */
-static int is_extension(struct isl_map *map, int i, int j, int k,
+static int is_adj_eq_extension(struct isl_map *map, int i, int j, int k,
        struct isl_tab **tabs, int *eq_i, int *ineq_i, int *eq_j, int *ineq_j)
 {
        int changed = 0;
@@ -1048,11 +1153,12 @@ static int check_adj_eq(struct isl_map *map, int i, int j,
                /* ADJ EQ TOO MANY */
                return 0;
 
-       for (k = 0; k < map->p[i]->n_ineq ; ++k)
+       for (k = 0; k < map->p[i]->n_ineq; ++k)
                if (ineq_i[k] == STATUS_ADJ_EQ)
                        break;
 
-       changed = is_extension(map, i, j, k, tabs, eq_i, ineq_i, eq_j, ineq_j);
+       changed = is_adj_eq_extension(map, i, j, k, tabs,
+                                       eq_i, ineq_i, eq_j, ineq_j);
        if (changed)
                return changed;
 
@@ -1200,7 +1306,15 @@ unbounded:
  *             => the pair can be replaced by a basic map consisting
  *                of the valid constraints in both basic maps
  *
- *     4. there is a single adjacent pair of an inequality and an equality,
+ *     4. one basic map has a single adjacent inequality, while the other
+ *        constraints are "valid".  The other basic map has some
+ *        "cut" constraints, but replacing the adjacent inequality by
+ *        its opposite and adding the valid constraints of the other
+ *        basic map results in a subset of the other basic map
+ *             => the pair can be replaced by a basic map consisting
+ *                of the valid constraints in both basic maps
+ *
+ *     5. there is a single adjacent pair of an inequality and an equality,
  *        the other constraints of the basic map containing the inequality are
  *        "valid".  Moreover, if the inequality the basic map is relaxed
  *        and then turned into an equality, then resulting facet lies
@@ -1208,7 +1322,7 @@ unbounded:
  *             => the pair can be replaced by the basic map containing
  *                the inequality, with the inequality relaxed.
  *
- *     5. there is a single adjacent pair of an inequality and an equality,
+ *     6. there is a single adjacent pair of an inequality and an equality,
  *        the other constraints of the basic map containing the inequality are
  *        "valid".  Moreover, the facets corresponding to both
  *        the inequality and the equality can be wrapped around their
@@ -1217,7 +1331,7 @@ unbounded:
  *                of the valid constraints in both basic maps together
  *                with all wrapping constraints
  *
- *     6. one of the basic maps extends beyond the other by at most one.
+ *     7. one of the basic maps extends beyond the other by at most one.
  *        Moreover, the facets corresponding to the cut constraints and
  *        the pieces of the other basic map at offset one from these cut
  *        constraints can be wrapped around their ridges to include
@@ -1226,7 +1340,7 @@ unbounded:
  *                of the valid constraints in both basic maps together
  *                with all wrapping constraints
  *
- *     7. the two basic maps live in adjacent hyperplanes.  In principle
+ *     8. the two basic maps live in adjacent hyperplanes.  In principle
  *        such sets can always be combined through wrapping, but we impose
  *        that there is only one such pair, to avoid overeager coalescing.
  *
@@ -1299,10 +1413,8 @@ static int coalesce_local_pair(__isl_keep isl_map *map, int i, int j,
                /* BAD ADJ INEQ */
        } else if (any(ineq_i, map->p[i]->n_ineq, STATUS_ADJ_INEQ) ||
                   any(ineq_j, map->p[j]->n_ineq, STATUS_ADJ_INEQ)) {
-               if (!any(eq_i, 2 * map->p[i]->n_eq, STATUS_CUT) &&
-                   !any(eq_j, 2 * map->p[j]->n_eq, STATUS_CUT))
-                       changed = check_adj_ineq(map, i, j, tabs,
-                                                ineq_i, ineq_j);
+               changed = check_adj_ineq(map, i, j, tabs,
+                                       eq_i, ineq_i, eq_j, ineq_j);
        } else {
                if (!any(eq_i, 2 * map->p[i]->n_eq, STATUS_CUT) &&
                    !any(eq_j, 2 * map->p[j]->n_eq, STATUS_CUT))
index d7d5ca7..3fbb8f5 100644 (file)
@@ -1040,6 +1040,17 @@ struct {
                                "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, "{ [x,y] : 0 <= x <= 2 and y >= 0 and x + 2y <= 4; "
+               "[x,0] : 3 <= x <= 4 }" },
+       { 1, "{ [x,y] : 0 <= x <= 3 and y >= 0 and x + 3y <= 6; "
+               "[x,0] : 4 <= x <= 5 }" },
+       { 0, "{ [x,y] : 0 <= x <= 2 and y >= 0 and x + 2y <= 4; "
+               "[x,0] : 3 <= x <= 5 }" },
+       { 0, "{ [x,y] : 0 <= x <= 2 and y >= 0 and x + y <= 4; "
+               "[x,0] : 3 <= x <= 4 }" },
+       { 1 , "{ [i0, i1] : i0 <= 122 and i0 >= 1 and 128i1 >= -249 + i0 and "
+                       "i1 <= 0; "
+               "[i0, 0] : i0 >= 123 and i0 <= 124 }" },
 };
 
 /* Test the functionality of isl_set_coalesce.