isl_tab_ineq_type: classify more constraints as being adjacent to an inequality

In particular, if one constraint b is equal to a c * (-1 - a), with c
a positive constant and A some other constraints, then b can also
be considered to be adjacent to a as relaxing a by one will result
in an overlap with b.  Note that if c is larger than one, then a
will not be considered to be adjacent to b, so this change will not
affect pairs of inequalities.

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

diff --git a/isl_tab.c b/isl_tab.c
index 06b30fb..47cc4d9 100644 (file)
--- a/isl_tab.c
+++ b/isl_tab.c
@@ -3073,9 +3073,9 @@ int isl_tab_rollback(struct isl_tab *tab, struct isl_tab_undo *snap)
  * In particular, if the row has been reduced to the constant -1,
  * then we know the inequality is adjacent (but opposite) to
  * an equality in the tableau.
- * If the row has been reduced to r = -1 -r', with r' an inequality
- * of the tableau, then the inequality is adjacent (but opposite)
- * to the inequality r'.
+ * If the row has been reduced to r = c*(-1 -r'), with r' an inequality
+ * of the tableau and c a positive constant, then the inequality
+ * is adjacent (but opposite) to the inequality r'.
  */
 static enum isl_ineq_type separation_type(struct isl_tab *tab, unsigned row)
 {
@@ -3087,15 +3087,18 @@ static enum isl_ineq_type separation_type(struct isl_tab *tab, unsigned row)
 
        if (!isl_int_is_one(tab->mat->row[row][0]))
                return isl_ineq_separate;
-       if (!isl_int_is_negone(tab->mat->row[row][1]))
-               return isl_ineq_separate;
 
        pos = isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
                                        tab->n_col - tab->n_dead);
-       if (pos == -1)
-               return isl_ineq_adj_eq;
+       if (pos == -1) {
+               if (isl_int_is_negone(tab->mat->row[row][1]))
+                       return isl_ineq_adj_eq;
+               else
+                       return isl_ineq_separate;
+       }
 
-       if (!isl_int_is_negone(tab->mat->row[row][off + tab->n_dead + pos]))
+       if (!isl_int_eq(tab->mat->row[row][1],
+                       tab->mat->row[row][off + tab->n_dead + pos]))
                return isl_ineq_separate;
 
        pos = isl_seq_first_non_zero(

diff --git a/isl_test.c b/isl_test.c
index 6116e3a..56ee9fb 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -908,6 +908,10 @@ void test_coalesce(struct isl_ctx *ctx)
        test_coalesce_set(ctx, "{ [x, 1 - x] : 0 <= x <= 1; [0,0] }", 1);
        test_coalesce_set(ctx, "{ [0,0]; [i,i] : 1 <= i <= 10 }", 1);
        test_coalesce_set(ctx, "{ [0,0]; [i,j] : 1 <= i,j <= 10 }", 0);
+       test_coalesce_set(ctx, "{ [0,0]; [i,2i] : 1 <= i <= 10 }", 1);
+       test_coalesce_set(ctx, "{ [0,0]; [i,2i] : 2 <= i <= 10 }", 0);
+       test_coalesce_set(ctx, "{ [1,0]; [i,2i] : 1 <= i <= 10 }", 0);
+       test_coalesce_set(ctx, "{ [0,1]; [i,2i] : 1 <= i <= 10 }", 0);
 }
 
 void test_closure(struct isl_ctx *ctx)