isl_tab_pip.c: correctly detect non-negativity of divs in lexmin contexts

In particular, the variables used to encode the div in the context
tableau is always non-negative, but the actual variable used in the main
tableau may not be non-negative.

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

diff --git a/isl_tab.c b/isl_tab.c
index 1bd1645..ae2eab8 100644 (file)
--- a/isl_tab.c
+++ b/isl_tab.c
@@ -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 f9f700e..421a49f 100644 (file)
--- 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,