isl_basic_map_gist: prefer contraints without existentially quantified variables

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

diff --git a/isl_map.c b/isl_map.c
index 5173369..06aa85c 100644 (file)
--- a/isl_map.c
+++ b/isl_map.c
@@ -6735,6 +6735,9 @@ struct constraint {
        isl_int         *c;
 };
 
+/* uset_gist depends on constraints without existentially quantified
+ * variables sorting first.
+ */
 static int qsort_constraint_cmp(const void *p1, const void *p2)
 {
        const struct constraint *c1 = (const struct constraint *)p1;

diff --git a/isl_map_simplify.c b/isl_map_simplify.c
index 302c123..093d1ca 100644 (file)
--- a/isl_map_simplify.c
+++ b/isl_map_simplify.c
@@ -1702,6 +1702,13 @@ error:
  * We first compute the integer affine hull of the intersection,
  * compute the gist inside this affine hull and then add back
  * those equalities that are not implied by the context.
+ *
+ * If two constraints are mutually redundant, then uset_gist_full
+ * will remove the second of those constraints.  We therefore first
+ * sort the constraints so that constraints not involving existentially
+ * quantified variables are given precedence over those that do.
+ * We have to perform this sorting before the variable compression,
+ * because that may effect the order of the variables.
  */
 static __isl_give isl_basic_set *uset_gist(__isl_take isl_basic_set *bset,
        __isl_take isl_basic_set *context)
@@ -1720,6 +1727,7 @@ static __isl_give isl_basic_set *uset_gist(__isl_take isl_basic_set *bset,
                isl_basic_set_free(context);
                return bset;
        }
+       bset = isl_basic_set_sort_constraints(bset);
        aff = isl_basic_set_affine_hull(isl_basic_set_copy(bset));
        if (!aff)
                goto error;

diff --git a/isl_test.c b/isl_test.c
index 56ee9fb..c6f1f26 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -650,7 +650,33 @@ void test_gist_case(struct isl_ctx *ctx, const char *name)
 
 void test_gist(struct isl_ctx *ctx)
 {
+       const char *str;
+       isl_basic_set *bset1, *bset2;
+
        test_gist_case(ctx, "gist1");
+
+       str = "[p0, p2, p3, p5, p6, p10] -> { [] : "
+           "exists (e0 = [(15 + p0 + 15p6 + 15p10)/16], e1 = [(p5)/8], "
+           "e2 = [(p6)/128], e3 = [(8p2 - p5)/128], "
+           "e4 = [(128p3 - p6)/4096]: 8e1 = p5 and 128e2 = p6 and "
+           "128e3 = 8p2 - p5 and 4096e4 = 128p3 - p6 and p2 >= 0 and "
+           "16e0 >= 16 + 16p6 + 15p10 and  p2 <= 15 and p3 >= 0 and "
+           "p3 <= 31 and  p6 >= 128p3 and p5 >= 8p2 and p10 >= 0 and "
+           "16e0 <= 15 + p0 + 15p6 + 15p10 and 16e0 >= p0 + 15p6 + 15p10 and "
+           "p10 <= 15 and p10 <= -1 + p0 - p6) }";
+       bset1 = isl_basic_set_read_from_str(ctx, str, -1);
+       str = "[p0, p2, p3, p5, p6, p10] -> { [] : exists (e0 = [(p5)/8], "
+           "e1 = [(p6)/128], e2 = [(8p2 - p5)/128], "
+           "e3 = [(128p3 - p6)/4096]: 8e0 = p5 and 128e1 = p6 and "
+           "128e2 = 8p2 - p5 and 4096e3 = 128p3 - p6 and p5 >= -7 and "
+           "p2 >= 0 and 8p2 <= -1 + p0 and p2 <= 15 and p3 >= 0 and "
+           "p3 <= 31 and 128p3 <= -1 + p0 and p6 >= -127 and "
+           "p5 <= -1 + p0 and p6 <= -1 + p0 and p6 >= 128p3 and "
+           "p0 >= 1 and p5 >= 8p2 and p10 >= 0 and p10 <= 15 ) }";
+       bset2 = isl_basic_set_read_from_str(ctx, str, -1);
+       bset1 = isl_basic_set_gist(bset1, bset2);
+       assert(bset1 && bset1->n_div == 0);
+       isl_basic_set_free(bset1);
 }
 
 void test_coalesce_set(isl_ctx *ctx, const char *str, int check_one)