isl_basic_map_foreach_lexopt: properly merge partial solutions

If we detect two identical solutions in adjacent parts of the search space,
then we merge them into a single solution.  The combined domain may however
have fewer existentially quantified variables and so we also need to adjust
the matrix representing the solution on that domain to no longer refer
to the extra existentially quantified variables.  Otherwise, the code
in sol_for_add could end up accessing elements of aff->v outside its bounds.
Note that it is safe to remove the columns that refer to the extra
existentially quantified variables since their coefficients need to be zero
for the two partial solutions to be considered identical.

Reported-by: Andreas Kloeckner <lists@informa.tiker.net>
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>

diff --git a/isl_tab_pip.c b/isl_tab_pip.c
index 8d16d5c..4124f4b 100644 (file)
--- a/isl_tab_pip.c
+++ b/isl_tab_pip.c
@@ -119,6 +119,12 @@ struct isl_context_lex {
        struct isl_tab *tab;
 };
 
+/* A stack (linked list) of solutions of subtrees of the search space.
+ *
+ * "M" describes the solution in terms of the dimensions of "dom".
+ * The number of columns of "M" is one more than the total number
+ * of dimensions of "dom".
+ */
 struct isl_partial_sol {
        int level;
        struct isl_basic_set *dom;
@@ -307,15 +313,22 @@ static void sol_pop(struct isl_sol *sol)
                        sol_pop_one(sol);
                } else {
                        struct isl_basic_set *bset;
+                       isl_mat *M;
+                       unsigned n;
 
+                       n = isl_basic_set_dim(partial->next->dom, isl_dim_div);
+                       n -= n_div;
                        bset = sol_domain(sol);
-                       if (!bset)
-                               goto error;
-
                        isl_basic_set_free(partial->next->dom);
                        partial->next->dom = bset;
+                       M = partial->next->M;
+                       M = isl_mat_drop_cols(M, M->n_col - n, n);
+                       partial->next->M = M;
                        partial->next->level = sol->level;
 
+                       if (!bset || !M)
+                               goto error;
+
                        sol->partial = partial->next;
                        isl_basic_set_free(partial->dom);
                        isl_mat_free(partial->M);

diff --git a/isl_test.c b/isl_test.c
index 4be52e5..745c4ed 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -2815,6 +2815,24 @@ int test_dim_max(isl_ctx *ctx)
        if (!equal)
                isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
 
+       /* Check that solutions are properly merged. */
+       str = "[n] -> { [a, b, c] : c >= -4a - 2b and "
+                               "c <= -1 + n - 4a - 2b and c >= -2b and "
+                               "4a >= -4 + n and c >= 0 }";
+       set = isl_set_read_from_str(ctx, str);
+       pwaff = isl_set_dim_min(set, 2);
+       set1 = isl_set_from_pw_aff(pwaff);
+       str = "[n] -> { [(0)] : n >= 1 }";
+       set2 = isl_set_read_from_str(ctx, str);
+       equal = isl_set_is_equal(set1, set2);
+       isl_set_free(set1);
+       isl_set_free(set2);
+
+       if (equal < 0)
+               return -1;
+       if (!equal)
+               isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
+
        return 0;
 }