From f6767d73e1bc38d4760f81abd165c236a502d896 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Thu, 14 Jul 2016 14:54:53 +0200 Subject: [PATCH] isl_tab_detect_implicit_equalities: do not add extra constraints isl_tab_detect_implicit_equalities calls cut_to_hyperplane to mark the implicit equality constraints it finds as equality constraints. This function in turn introduces an extra constraint such that it can call close_row on it. However, after closing the row (which marks the original variable as zero, possibly along with other variables), the extra constraint is no longer required. Remove it again after it has served its purpose. Not introducing extra constraints is important for the use of isl_tab_detect_implicit_equalities inside isl_map_coalesce. In particular, if isl_tab_detect_implicit_equalities adds extra constraints, then the number of the constraints in the basic map and tableau representations is no longer the same. This was not originally a problem, as long as the initial constraints in the tableau still match all constraints of the basic map. However, since a130b58 (isl_map_coalesce: allow general coalescing with expanded divs, Fri May 27 13:12:48 2016 +0200), the tableau may get adjusted to additional constraints that were added to the basic map and for these additional constraints to have the same positions in both representations, the two should have the same number of constraints to start with. The extra constraints that could get added by isl_tab_detect_implicit_equalities break this assumption and caused a bug reported by Tobias Grosser. Note that implicit equality constraints get detected internally at various points inside isl. It is therefore fairly unlikely to end up in a situation where additional implicit equalities get detected from within isl_map_coalesce. The new test case circumvents the detection of implicit equality constraints during parsing by explicitly calling isl_basic_set_union, which currently happens to not perform this detection, whereas the parsing of a combined input would end up calling isl_set_union, which does perform the detection. Reported-by: Tobias Grosser Signed-off-by: Sven Verdoolaege --- isl_tab.c | 59 ++++++++++++++++++++++++++++++++++++++++++++--------------- isl_test.c | 28 ++++++++++++++++++++++++++++ 2 files changed, 72 insertions(+), 15 deletions(-) diff --git a/isl_tab.c b/isl_tab.c index 899a5b1b..d077401f 100644 --- a/isl_tab.c +++ b/isl_tab.c @@ -1603,10 +1603,20 @@ static int tab_is_manifestly_empty(struct isl_tab *tab) * Each of the non-negative variables with a negative coefficient can * then also be written as the negative sum of non-negative variables * and must therefore also be zero. + * + * If "temp_var" is set, then "var" is a temporary variable that + * will be removed after this function returns and for which + * no information is recorded on the undo stack. + * Do not add any undo records involving this variable in this case + * since the variable will have been removed before any future undo + * operations. Also avoid marking the variable as redundant, + * since that either adds an undo record or needlessly removes the row + * (the caller will take care of removing the row). */ -static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var) - WARN_UNUSED; -static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var) +static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var, + int temp_var) WARN_UNUSED; +static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var, + int temp_var) { int j; struct isl_mat *mat = tab->mat; @@ -1617,7 +1627,7 @@ static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var) "expecting non-negative variable", return isl_stat_error); var->is_zero = 1; - if (tab->need_undo) + if (!temp_var && tab->need_undo) if (isl_tab_push_var(tab, isl_tab_undo_zero, var) < 0) return isl_stat_error; for (j = tab->n_dead; j < tab->n_col; ++j) { @@ -1634,7 +1644,7 @@ static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var) if (recheck) --j; } - if (isl_tab_mark_redundant(tab, var->index) < 0) + if (!temp_var && isl_tab_mark_redundant(tab, var->index) < 0) return isl_stat_error; if (tab_is_manifestly_empty(tab) && isl_tab_mark_empty(tab) < 0) return isl_stat_error; @@ -2457,7 +2467,7 @@ int isl_tab_cone_is_bounded(struct isl_tab *tab) return -1; if (sgn != 0) return 0; - if (close_row(tab, var) < 0) + if (close_row(tab, var, 0) < 0) return -1; break; } @@ -2589,9 +2599,28 @@ struct isl_basic_set *isl_basic_set_update_from_tab(struct isl_basic_set *bset, (struct isl_basic_map *)bset, tab); } -/* Given a non-negative variable "var", add a new non-negative variable - * that is the opposite of "var", ensuring that var can only attain the - * value zero. +/* Drop the last constraint added to "tab" in position "r". + * The constraint is expected to have remained in a row. + */ +static isl_stat drop_last_con_in_row(struct isl_tab *tab, int r) +{ + if (!tab->con[r].is_row) + isl_die(isl_tab_get_ctx(tab), isl_error_internal, + "row unexpectedly moved to column", + return isl_stat_error); + if (r + 1 != tab->n_con) + isl_die(isl_tab_get_ctx(tab), isl_error_internal, + "additional constraints added", return isl_stat_error); + if (drop_row(tab, tab->con[r].index) < 0) + return isl_stat_error; + + return isl_stat_ok; +} + +/* Given a non-negative variable "var", temporarily add a new non-negative + * variable that is the opposite of "var", ensuring that "var" can only attain + * the value zero. The new variable is removed again before this function + * returns. However, the effect of forcing "var" to be zero remains. * If var = n/d is a row variable, then the new variable = -n/d. * If var is a column variables, then the new variable = -var. * If the new variable cannot attain non-negative values, then @@ -2638,22 +2667,22 @@ static isl_stat cut_to_hyperplane(struct isl_tab *tab, struct isl_tab_var *var) tab->n_row++; tab->n_con++; - if (isl_tab_push_var(tab, isl_tab_undo_allocate, &tab->con[r]) < 0) - return isl_stat_error; sgn = sign_of_max(tab, &tab->con[r]); if (sgn < -1) return isl_stat_error; if (sgn < 0) { + if (drop_last_con_in_row(tab, r) < 0) + return isl_stat_error; if (isl_tab_mark_empty(tab) < 0) return isl_stat_error; return isl_stat_ok; } tab->con[r].is_nonneg = 1; - if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0) - return isl_stat_error; /* sgn == 0 */ - if (close_row(tab, &tab->con[r]) < 0) + if (close_row(tab, &tab->con[r], 1) < 0) + return isl_stat_error; + if (drop_last_con_in_row(tab, r) < 0) return isl_stat_error; return isl_stat_ok; @@ -2884,7 +2913,7 @@ int isl_tab_detect_implicit_equalities(struct isl_tab *tab) if (sgn < 0) return -1; if (sgn == 0) { - if (close_row(tab, var) < 0) + if (close_row(tab, var, 0) < 0) return -1; } else if (!tab->rational && !at_least_one(tab, var)) { if (cut_to_hyperplane(tab, var) < 0) diff --git a/isl_test.c b/isl_test.c index 479f7e20..42964d8f 100644 --- a/isl_test.c +++ b/isl_test.c @@ -1905,6 +1905,32 @@ static int test_coalesce_special(struct isl_ctx *ctx) return 0; } +/* A specialized coalescing test case that would result in an assertion + * in an earlier version of isl. + * The explicit call to isl_basic_set_union prevents the implicit + * equality constraints in the first basic map from being detected prior + * to the call to isl_set_coalesce, at least at the point + * where this test case was introduced. + */ +static int test_coalesce_special2(struct isl_ctx *ctx) +{ + const char *str; + isl_basic_set *bset1, *bset2; + isl_set *set; + + str = "{ [x, y] : x, y >= 0 and x + 2y <= 1 and 2x + y <= 1 }"; + bset1 = isl_basic_set_read_from_str(ctx, str); + str = "{ [x,0] : -1 <= x <= 1 and x mod 2 = 1 }" ; + bset2 = isl_basic_set_read_from_str(ctx, str); + set = isl_basic_set_union(bset1, bset2); + set = isl_set_coalesce(set); + isl_set_free(set); + + if (!set) + return -1; + return 0; +} + /* Test the functionality of isl_set_coalesce. * That is, check that the output is always equal to the input * and in some cases that the result consists of a single disjunct. @@ -1924,6 +1950,8 @@ static int test_coalesce(struct isl_ctx *ctx) return -1; if (test_coalesce_special(ctx) < 0) return -1; + if (test_coalesce_special2(ctx) < 0) + return -1; return 0; } -- 2.11.4.GIT