isl_tab.c: unrelax: restore row if variable is non-negative

Unrelaxing a constraint means that the constraint is tightened.
The sample value may therefore become negative and then have to
restore the row again.  This is guaranteed to succeed because
the tableau was supposed to be in a valid state before the constraint
was relaxed.

diff --git a/isl_tab.c b/isl_tab.c
index daed8ec..55d9dc2 100644 (file)
--- a/isl_tab.c
+++ b/isl_tab.c
@@ -2771,10 +2771,14 @@ static int unrelax(struct isl_tab *tab, struct isl_tab_var *var)
                if (to_row(tab, var, 1) < 0)
                        return -1;
 
-       if (var->is_row)
+       if (var->is_row) {
                isl_int_sub(tab->mat->row[var->index][1],
                    tab->mat->row[var->index][1], tab->mat->row[var->index][0]);
-       else {
+               if (var->is_nonneg) {
+                       int sgn = restore_row(tab, var);
+                       isl_assert(tab->mat->ctx, sgn >= 0, return -1);
+               }
+       } else {
                int i;
 
                for (i = 0; i < tab->n_row; ++i) {

diff --git a/isl_test.c b/isl_test.c
index 9f8f299..a1fccdd 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -529,6 +529,7 @@ void test_gist(struct isl_ctx *ctx)
 
 void test_coalesce(struct isl_ctx *ctx)
 {
+       const char *str;
        struct isl_set *set, *set2;
        struct isl_map *map, *map2;
 
@@ -680,6 +681,17 @@ void test_coalesce(struct isl_ctx *ctx)
        assert(isl_map_is_equal(map, map2));
        isl_map_free(map);
        isl_map_free(map2);
+
+       str = "[n, m] -> { [] -> [o0, o2, o3] : (o3 = 1 and o0 >= 1 + m and "
+             "o0 <= n + m and o2 <= m and o0 >= 2 + n and o2 >= 3) or "
+             "(o0 >= 2 + n and o0 >= 1 + m and o0 <= n + m and n >= 1 and "
+             "o3 <= -1 + o2 and o3 >= 1 - m + o2 and o3 >= 2 and o3 <= n) }";
+       map = isl_map_read_from_str(ctx, str, -1);
+       map = isl_map_coalesce(map);
+       map2 = isl_map_read_from_str(ctx, str, -1);
+       assert(isl_map_is_equal(map, map2));
+       isl_map_free(map);
+       isl_map_free(map2);
 }
 
 void test_closure(struct isl_ctx *ctx)