isl_tab_basic_map_partial_lexopt: properly normalize divs

We were only dividing out common divisors that also divide
the constant term, but we should ignore the constant term
while determining the greatest common divisor.

We already properly normalize the constraints and not properly
normalizing the divs could result in div constraints not being
recognized as such.  In particular, inside isl_map_affine_hull,
div constraints are added inside the call to isl_basic_map_overlying_set.
Usually, these constraints are removed again in remove_redundant_divs,
but they would remain if the the divs are not properly normalized.

Now, arguably, we shouldn't be adding div constraints inside
isl_map_affine_hull, but a proper normalization of divs is useful in any case.

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

diff --git a/isl_tab_pip.c b/isl_tab_pip.c
index dd14fb8..4e613f5 100644 (file)
--- a/isl_tab_pip.c
+++ b/isl_tab_pip.c
@@ -745,6 +745,30 @@ static struct isl_vec *get_row_parameter_ineq(struct isl_tab *tab, int row)
        return ineq;
 }
 
+/* Normalize a div expression of the form
+ *
+ *     [(g*f(x) + c)/(g * m)]
+ *
+ * with c the constant term and f(x) the remaining coefficients, to
+ *
+ *     [(f(x) + [c/g])/m]
+ */
+static void normalize_div(__isl_keep isl_vec *div)
+{
+       isl_ctx *ctx = isl_vec_get_ctx(div);
+       int len = div->size - 2;
+
+       isl_seq_gcd(div->el + 2, len, &ctx->normalize_gcd);
+       isl_int_gcd(ctx->normalize_gcd, ctx->normalize_gcd, div->el[0]);
+
+       if (isl_int_is_one(ctx->normalize_gcd))
+               return;
+
+       isl_int_divexact(div->el[0], div->el[0], ctx->normalize_gcd);
+       isl_int_fdiv_q(div->el[1], div->el[1], ctx->normalize_gcd);
+       isl_seq_scale_down(div->el + 2, div->el + 2, ctx->normalize_gcd, len);
+}
+
 /* Return a integer division for use in a parametric cut based on the given row.
  * In particular, let the parametric constant of the row be
  *
@@ -765,7 +789,7 @@ static struct isl_vec *get_row_parameter_div(struct isl_tab *tab, int row)
 
        isl_int_set(div->el[0], tab->mat->row[row][0]);
        get_row_parameter_line(tab, row, div->el + 1);
-       div = isl_vec_normalize(div);
+       normalize_div(div);
        isl_seq_neg(div->el + 1, div->el + 1, div->size - 1);
        isl_seq_fdiv_r(div->el + 1, div->el + 1, div->el[0], div->size - 1);
 
@@ -793,7 +817,7 @@ static struct isl_vec *get_row_split_div(struct isl_tab *tab, int row)
 
        isl_int_set(div->el[0], tab->mat->row[row][0]);
        get_row_parameter_line(tab, row, div->el + 1);
-       div = isl_vec_normalize(div);
+       normalize_div(div);
        isl_seq_fdiv_r(div->el + 1, div->el + 1, div->el[0], div->size - 1);
 
        return div;

diff --git a/isl_test.c b/isl_test.c
index 5f1f9dc..0640d6d 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -637,11 +637,30 @@ void test_affine_hull_case(struct isl_ctx *ctx, const char *name)
        fclose(input);
 }
 
-void test_affine_hull(struct isl_ctx *ctx)
+int test_affine_hull(struct isl_ctx *ctx)
 {
+       const char *str;
+       isl_set *set;
+       isl_basic_set *bset;
+       int n;
+
        test_affine_hull_case(ctx, "affine2");
        test_affine_hull_case(ctx, "affine");
        test_affine_hull_case(ctx, "affine3");
+
+       str = "[m] -> { [i0] : exists (e0, e1: e1 <= 1 + i0 and "
+                       "m >= 3 and 4i0 <= 2 + m and e1 >= i0 and "
+                       "e1 >= 0 and e1 <= 2 and e1 >= 1 + 2e0 and "
+                       "2e1 <= 1 + m + 4e0 and 2e1 >= 2 - m + 4i0 - 4e0) }";
+       set = isl_set_read_from_str(ctx, str);
+       bset = isl_set_affine_hull(set);
+       n = isl_basic_set_dim(bset, isl_dim_div);
+       isl_basic_set_free(bset);
+       if (n != 0)
+               isl_die(ctx, isl_error_unknown, "not expecting any divs",
+                       return -1);
+
+       return 0;
 }
 
 void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
@@ -2712,7 +2731,8 @@ int main()
        test_dim(ctx);
        test_div(ctx);
        test_application(ctx);
-       test_affine_hull(ctx);
+       if (test_affine_hull(ctx) < 0)
+               goto error;
        test_convex_hull(ctx);
        test_gist(ctx);
        test_coalesce(ctx);