isl_basic_map_simplify: fix elimination of unit coefficient known divs
authorSven Verdoolaege <skimo@kotnet.org>
Mon, 30 Dec 2013 16:03:11 +0000 (30 17:03 +0100)
committerSven Verdoolaege <skimo@kotnet.org>
Mon, 30 Dec 2013 16:11:28 +0000 (30 17:11 +0100)
If a known div appears with a unit coefficient in a constraint,
then it is eliminated from that constraint in order to simplify
the constraint.
However, one if the div constraints may have been eliminated
as being redundant with respect to the modified constraint and
the elimination of the div from the constraint may therefore
result in a loss of information about the div from the constraints.
To make sure this problem does not occur, we (re)introduce
the div constraint that could potentially have been eliminated
with respect to the modified constraint.

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
isl_map.c
isl_map_private.h
isl_map_simplify.c
isl_test.c

index af99916..4b3b0bf 100644 (file)
--- a/isl_map.c
+++ b/isl_map.c
@@ -4299,19 +4299,14 @@ error:
        return NULL;
 }
 
-/* For a div d = floor(f/m), add the constraints
+/* For a div d = floor(f/m), add the constraint
  *
  *             f - m d >= 0
- *             -(f-(n-1)) + m d >= 0
- *
- * Note that the second constraint is the negation of
- *
- *             f - m d >= n
  */
-int isl_basic_map_add_div_constraints_var(__isl_keep isl_basic_map *bmap,
+static int add_upper_div_constraint(__isl_keep isl_basic_map *bmap,
        unsigned pos, isl_int *div)
 {
-       int i, j;
+       int i;
        unsigned total = isl_basic_map_total_dim(bmap);
 
        i = isl_basic_map_alloc_inequality(bmap);
@@ -4320,13 +4315,47 @@ int isl_basic_map_add_div_constraints_var(__isl_keep isl_basic_map *bmap,
        isl_seq_cpy(bmap->ineq[i], div + 1, 1 + total);
        isl_int_neg(bmap->ineq[i][1 + pos], div[0]);
 
-       j = isl_basic_map_alloc_inequality(bmap);
-       if (j < 0)
+       return 0;
+}
+
+/* For a div d = floor(f/m), add the constraint
+ *
+ *             -(f-(n-1)) + m d >= 0
+ */
+static int add_lower_div_constraint(__isl_keep isl_basic_map *bmap,
+       unsigned pos, isl_int *div)
+{
+       int i;
+       unsigned total = isl_basic_map_total_dim(bmap);
+
+       i = isl_basic_map_alloc_inequality(bmap);
+       if (i < 0)
+               return -1;
+       isl_seq_neg(bmap->ineq[i], div + 1, 1 + total);
+       isl_int_set(bmap->ineq[i][1 + pos], div[0]);
+       isl_int_add(bmap->ineq[i][0], bmap->ineq[i][0], bmap->ineq[i][1 + pos]);
+       isl_int_sub_ui(bmap->ineq[i][0], bmap->ineq[i][0], 1);
+
+       return 0;
+}
+
+/* For a div d = floor(f/m), add the constraints
+ *
+ *             f - m d >= 0
+ *             -(f-(n-1)) + m d >= 0
+ *
+ * Note that the second constraint is the negation of
+ *
+ *             f - m d >= n
+ */
+int isl_basic_map_add_div_constraints_var(__isl_keep isl_basic_map *bmap,
+       unsigned pos, isl_int *div)
+{
+       if (add_upper_div_constraint(bmap, pos, div) < 0)
                return -1;
-       isl_seq_neg(bmap->ineq[j], bmap->ineq[i], 1 + total);
-       isl_int_add(bmap->ineq[j][0], bmap->ineq[j][0], bmap->ineq[j][1 + pos]);
-       isl_int_sub_ui(bmap->ineq[j][0], bmap->ineq[j][0], 1);
-       return j;
+       if (add_lower_div_constraint(bmap, pos, div) < 0)
+               return -1;
+       return 0;
 }
 
 int isl_basic_set_add_div_constraints_var(__isl_keep isl_basic_set *bset,
@@ -4345,6 +4374,37 @@ int isl_basic_map_add_div_constraints(struct isl_basic_map *bmap, unsigned div)
                                                        bmap->div[div]);
 }
 
+/* Add the div constraint of sign "sign" for div "div" of "bmap".
+ *
+ * In particular, if this div is of the form d = floor(f/m),
+ * then add the constraint
+ *
+ *             f - m d >= 0
+ *
+ * if sign < 0 or the constraint
+ *
+ *             -(f-(n-1)) + m d >= 0
+ *
+ * if sign > 0.
+ */
+int isl_basic_map_add_div_constraint(__isl_keep isl_basic_map *bmap,
+       unsigned div, int sign)
+{
+       unsigned total;
+       unsigned div_pos;
+
+       if (!bmap)
+               return -1;
+
+       total = isl_basic_map_total_dim(bmap);
+       div_pos = total - bmap->n_div + div;
+
+       if (sign < 0)
+               return add_upper_div_constraint(bmap, div_pos, bmap->div[div]);
+       else
+               return add_lower_div_constraint(bmap, div_pos, bmap->div[div]);
+}
+
 int isl_basic_set_add_div_constraints(struct isl_basic_set *bset, unsigned div)
 {
        return isl_basic_map_add_div_constraints(bset, div);
index 66862d7..db5f96b 100644 (file)
@@ -272,6 +272,8 @@ __isl_give isl_set *isl_set_eliminate(__isl_take isl_set *set,
 int isl_basic_set_constraint_is_redundant(struct isl_basic_set **bset,
        isl_int *c, isl_int *opt_n, isl_int *opt_d);
 
+int isl_basic_map_add_div_constraint(__isl_keep isl_basic_map *bmap,
+       unsigned div, int sign);
 int isl_basic_map_add_div_constraints(struct isl_basic_map *bmap, unsigned div);
 struct isl_basic_map *isl_basic_map_drop_redundant_divs(
        struct isl_basic_map *bmap);
index af24943..a575db0 100644 (file)
@@ -1207,6 +1207,12 @@ static struct isl_basic_map *remove_duplicate_constraints(
  *     -floor(e/m) = ceil(-e/m) = floor((-e + m - 1)/m)
  *
  *
+ * Note that one of the div constraints may have been eliminated
+ * due to being redundant with respect to the constraint that is
+ * being modified by this function.  The modified constraint may
+ * no longer imply this div constraint, so we add it back to make
+ * sure we do not lose any information.
+ *
  * We skip integral divs, i.e., those with denominator 1, as we would
  * risk eliminating the div from the div constraints.  We do not need
  * to handle those divs here anyway since the div constraints will turn
@@ -1258,6 +1264,10 @@ static __isl_give isl_basic_map *eliminate_unit_divs(
                                isl_int_sub_ui(bmap->ineq[j][0],
                                        bmap->ineq[j][0], 1);
                        }
+
+                       bmap = isl_basic_map_extend_constraints(bmap, 0, 1);
+                       if (isl_basic_map_add_div_constraint(bmap, i, s) < 0)
+                               return isl_basic_map_free(bmap);
                }
        }
 
index 94e105e..738af55 100644 (file)
@@ -2300,6 +2300,18 @@ struct {
        { "{ rat: [i] : 0 <= i <= 10 }", "{ [i] : 0 <= i <= 10 }", 0 },
        { "{ rat: [0] }", "{ [i] : 0 <= i <= 10 }", 1 },
        { "{ rat: [(1)/2] }", "{ [i] : 0 <= i <= 10 }", 0 },
+       { "{ [t, i] : (exists (e0 = [(2 + t)/4]: 4e0 <= 2 + t and "
+                       "4e0 >= -1 + t and i >= 57 and i <= 62 and "
+                       "4e0 <= 62 + t - i and 4e0 >= -61 + t + i and "
+                       "t >= 0 and t <= 511 and 4e0 <= -57 + t + i and "
+                       "4e0 >= 58 + t - i and i >= 58 + t and i >= 62 - t)) }",
+         "{ [i0, i1] : (exists (e0 = [(4 + i0)/4]: 4e0 <= 62 + i0 - i1 and "
+                       "4e0 >= 1 + i0 and i0 >= 0 and i0 <= 511 and "
+                       "4e0 <= -57 + i0 + i1)) or "
+               "(exists (e0 = [(2 + i0)/4]: 4e0 <= i0 and "
+                       "4e0 >= 58 + i0 - i1 and i0 >= 2 and i0 <= 511 and "
+                       "4e0 >= -61 + i0 + i1)) or "
+               "(i1 <= 66 - i0 and i0 >= 2 and i1 >= 59 + i0) }", 1 },
 };
 
 static int test_subset(isl_ctx *ctx)