diff options
| -rw-r--r-- | isl_tab.c | 39 | ||||
| -rw-r--r-- | isl_tab_pip.c | 16 |
2 files changed, 44 insertions, 11 deletions
@@ -2057,6 +2057,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, prescrived by "div" to the tableau and * the associated bmap (which is assumed to be non-NULL). * @@ -2069,7 +2097,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; @@ -2079,15 +2106,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; diff --git a/isl_tab_pip.c b/isl_tab_pip.c index f9f700e4..421a49f6 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, |