isl_basic_map_eliminate_vars: better handling of divs

In particular, if any div depends on one of the variables that is
being eliminated, then they should be eliminated too.
Furthermore, if a div is eliminated, then its definition should
be removed as well.

diff --git a/isl_map.c b/isl_map.c
index 9aeb6d4..c7146f1 100644 (file)
--- a/isl_map.c
+++ b/isl_map.c
@@ -1746,11 +1746,32 @@ static struct isl_basic_map *normalize_constraints(struct isl_basic_map *bmap)
 }
 
 
+/* Remove any div that is defined in terms of the given variable.
+ */
+static struct isl_basic_map *remove_dependent_vars(struct isl_basic_map *bmap,
+                                                                       int pos)
+{
+       int i;
+       unsigned dim = isl_dim_total(bmap->dim);
+
+       for (i = 0; i < bmap->n_div; ++i) {
+               if (isl_int_is_zero(bmap->div[i][0]))
+                       continue;
+               if (isl_int_is_zero(bmap->div[i][1+1+pos]))
+                       continue;
+               bmap = isl_basic_map_eliminate_vars(bmap, dim + i, 1);
+               if (!bmap)
+                       return NULL;
+       }
+       return bmap;
+}
+
+
 /* Eliminate the specified variables from the constraints using
  * Fourier-Motzkin.  The variables themselves are not removed.
  */
 struct isl_basic_map *isl_basic_map_eliminate_vars(
-       struct isl_basic_map *bmap, int pos, unsigned n)
+       struct isl_basic_map *bmap, unsigned pos, unsigned n)
 {
        int d;
        int i, j, k;
@@ -1763,10 +1784,13 @@ struct isl_basic_map *isl_basic_map_eliminate_vars(
        total = isl_basic_map_total_dim(bmap);
 
        bmap = isl_basic_map_cow(bmap);
-       for (d = pos + n - 1; d >= pos; --d) {
+       for (d = pos + n - 1; d >= 0 && d >= pos; --d) {
                int n_lower, n_upper;
+               bmap = remove_dependent_vars(bmap, d);
                if (!bmap)
                        return NULL;
+               if (d >= total - bmap->n_div)
+                       isl_seq_clr(bmap->div[d-(total-bmap->n_div)], 2+total);
                for (i = 0; i < bmap->n_eq; ++i) {
                        if (isl_int_is_zero(bmap->eq[i][1+d]))
                                continue;

diff --git a/isl_map_private.h b/isl_map_private.h
index b9da4d8..55d0a5f 100644 (file)
--- a/isl_map_private.h
+++ b/isl_map_private.h
@@ -71,6 +71,8 @@ struct isl_set *isl_set_remove_empty_parts(struct isl_set *set);
 struct isl_set *isl_set_drop_vars(
                struct isl_set *set, unsigned first, unsigned n);
 
+struct isl_basic_map *isl_basic_map_eliminate_vars(
+       struct isl_basic_map *bmap, unsigned pos, unsigned n);
 struct isl_basic_set *isl_basic_set_eliminate_vars(
        struct isl_basic_set *bset, unsigned pos, unsigned n);