diff options
| -rw-r--r-- | isl_tab.c | 42 | ||||
| -rw-r--r-- | isl_tab_pip.c | 16 | ||||
| -rwxr-xr-x | pip_test.sh | 4 | ||||
| -rw-r--r-- | test_inputs/seghir-vd.pip | 17 |
4 files changed, 66 insertions, 13 deletions
@@ -2060,6 +2060,34 @@ error: return -1; } +/* Check whether the div described by "div" is obviously non-negative. + * If we are using a big parameter, then we will encode the div + * as div' = M + div, which is always non-negative. + * Otherwise, we check whether div is a non-negative affine combination + * of non-negative variables. + */ +static int div_is_nonneg(struct isl_tab *tab, __isl_keep isl_vec *div) +{ + int i; + + if (tab->M) + return 1; + + if (isl_int_is_neg(div->el[1])) + return 0; + + for (i = 0; i < tab->n_var; ++i) { + if (isl_int_is_neg(div->el[2 + i])) + return 0; + if (isl_int_is_zero(div->el[2 + i])) + continue; + if (!tab->var[i].is_nonneg) + return 0; + } + + return 1; +} + /* Add an extra div, prescribed by "div" to the tableau and * the associated bmap (which is assumed to be non-NULL). * @@ -2072,7 +2100,6 @@ error: int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div, int (*add_ineq)(void *user, isl_int *), void *user) { - int i; int r; int k; int nonneg; @@ -2082,15 +2109,7 @@ int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div, isl_assert(tab->mat->ctx, tab->bmap, return -1); - for (i = 0; i < tab->n_var; ++i) { - if (isl_int_is_neg(div->el[2 + i])) - break; - if (isl_int_is_zero(div->el[2 + i])) - continue; - if (!tab->var[i].is_nonneg) - break; - } - nonneg = i == tab->n_var && !isl_int_is_neg(div->el[1]); + nonneg = div_is_nonneg(tab, div); if (isl_tab_extend_cons(tab, 3) < 0) return -1; @@ -2712,7 +2731,8 @@ int isl_tab_is_equality(struct isl_tab *tab, int con) off = 2 + tab->M; return isl_int_is_zero(tab->mat->row[row][1]) && - isl_seq_first_non_zero(tab->mat->row[row] + 2 + tab->n_dead, + (!tab->M || isl_int_is_zero(tab->mat->row[row][2])) && + isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead, tab->n_col - tab->n_dead) == -1; } diff --git a/isl_tab_pip.c b/isl_tab_pip.c index 401d475f..d09330fa 100644 --- a/isl_tab_pip.c +++ b/isl_tab_pip.c @@ -2257,11 +2257,25 @@ static int context_lex_get_div(struct isl_context *context, struct isl_tab *tab, return get_div(tab, context, div); } +/* Add a div specified by "div" to the context tableau and return + * 1 if the div is obviously non-negative. + * context_tab_add_div will always return 1, because all variables + * in a isl_context_lex tableau are non-negative. + * However, if we are using a big parameter in the context, then this only + * reflects the non-negativity of the variable used to _encode_ the + * div, i.e., div' = M + div, so we can't draw any conclusions. + */ static int context_lex_add_div(struct isl_context *context, struct isl_vec *div) { struct isl_context_lex *clex = (struct isl_context_lex *)context; - return context_tab_add_div(clex->tab, div, + int nonneg; + nonneg = context_tab_add_div(clex->tab, div, context_lex_add_ineq_wrap, context); + if (nonneg < 0) + return -1; + if (clex->tab->M) + return 0; + return nonneg; } static int context_lex_detect_equalities(struct isl_context *context, diff --git a/pip_test.sh b/pip_test.sh index caba3ef0..1d8d57a2 100755 --- a/pip_test.sh +++ b/pip_test.sh @@ -10,6 +10,7 @@ PIP_TESTS="\ fimmel.pip \ max.pip \ negative.pip \ + seghir-vd.pip \ small.pip \ sor1d.pip \ square.pip \ @@ -18,5 +19,6 @@ PIP_TESTS="\ for i in $PIP_TESTS; do echo $i; - ./isl_pip$EXEEXT -T < $srcdir/test_inputs/$i || exit + ./isl_pip$EXEEXT --context=gbr -T < $srcdir/test_inputs/$i || exit + ./isl_pip$EXEEXT --context=lexmin -T < $srcdir/test_inputs/$i || exit done diff --git a/test_inputs/seghir-vd.pip b/test_inputs/seghir-vd.pip new file mode 100644 index 00000000..b5395fbd --- /dev/null +++ b/test_inputs/seghir-vd.pip @@ -0,0 +1,17 @@ +0 6 + +-1 + +9 8 + 0 0 0 1 1 0 0 2 + 1 2 1 0 0 1 0 0 + 1 0 1 0 -1 0 0 -1 + 1 -2 -1 0 0 0 0 -1 + 1 7 3 0 0 0 0 -1 + 1 -6 -4 0 1 0 3 1 + 1 -7 -3 0 0 1 6 4 + 1 0 0 0 0 0 1 0 + 1 0 0 0 0 0 0 1 + +Urs_parms +Urs_unknowns |