isl_tab_pip.c: add some debugging code

[platform/upstream/isl.git] / isl_tab_pip.c

diff --git a/isl_tab_pip.c b/isl_tab_pip.c
index f9f700e..f6e238a 100644 (file)
--- a/isl_tab_pip.c
+++ b/isl_tab_pip.c
@@ -10,6 +10,7 @@
  * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France 
  */
 
+#include <isl_ctx_private.h>
 #include "isl_map_private.h"
 #include <isl/seq.h>
 #include "isl_tab.h"
@@ -25,7 +26,7 @@
  * The strategy used for obtaining a feasible solution is different
  * from the one used in isl_tab.c.  In particular, in isl_tab.c,
  * upon finding a constraint that is not yet satisfied, we pivot
- * in a row that increases the constant term of row holding the
+ * in a row that increases the constant term of the row holding the
  * constraint, making sure the sample solution remains feasible
  * for all the constraints it already satisfied.
  * Here, we always pivot in the row holding the constraint,
@@ -39,7 +40,7 @@
  * then the initial sample value may be chosen equal to zero.
  * However, we will not make this assumption.  Instead, we apply
  * the "big parameter" trick.  Any variable x is then not directly
- * used in the tableau, but instead it its represented by another
+ * used in the tableau, but instead it is represented by another
  * variable x' = M + x, where M is an arbitrarily large (positive)
  * value.  x' is therefore always non-negative, whatever the value of x.
  * Taking as initial sample value x' = 0 corresponds to x = -M,
@@ -1112,6 +1113,42 @@ static int first_neg(struct isl_tab *tab)
        return -1;
 }
 
+/* Check whether the invariant that all columns are lexico-positive
+ * is satisfied.  This function is not called from the current code
+ * but is useful during debugging.
+ */
+static void check_lexpos(struct isl_tab *tab)
+{
+       unsigned off = 2 + tab->M;
+       int col;
+       int var;
+       int row;
+
+       for (col = tab->n_dead; col < tab->n_col; ++col) {
+               if (tab->col_var[col] >= 0 &&
+                   (tab->col_var[col] < tab->n_param ||
+                    tab->col_var[col] >= tab->n_var - tab->n_div))
+                       continue;
+               for (var = tab->n_param; var < tab->n_var - tab->n_div; ++var) {
+                       if (!tab->var[var].is_row) {
+                               if (tab->var[var].index == col)
+                                       break;
+                               else
+                                       continue;
+                       }
+                       row = tab->var[var].index;
+                       if (isl_int_is_zero(tab->mat->row[row][off + col]))
+                               continue;
+                       if (isl_int_is_pos(tab->mat->row[row][off + col]))
+                               break;
+                       fprintf(stderr, "lexneg column %d (row %d)\n",
+                               col, row);
+               }
+               if (var >= tab->n_var - tab->n_div)
+                       fprintf(stderr, "zero column %d\n", col);
+       }
+}
+
 /* Resolve all known or obviously violated constraints through pivoting.
  * In particular, as long as we can find any violated constraint, we
  * look for a pivoting column that would result in the lexicographically
@@ -1306,18 +1343,6 @@ static struct isl_tab *add_lexmin_eq(struct isl_tab *tab, isl_int *eq)
        } else if (!tab->con[r2].is_row) {
                if (isl_tab_kill_col(tab, tab->con[r2].index) < 0)
                        goto error;
-       } else if (isl_int_is_zero(tab->mat->row[tab->con[r1].index][1])) {
-               unsigned off = 2 + tab->M;
-               int i;
-               int row = tab->con[r1].index;
-               i = isl_seq_first_non_zero(tab->mat->row[row]+off+tab->n_dead,
-                                               tab->n_col - tab->n_dead);
-               if (i != -1) {
-                       if (isl_tab_pivot(tab, row, tab->n_dead + i) < 0)
-                               goto error;
-                       if (isl_tab_kill_col(tab, tab->n_dead + i) < 0)
-                               goto error;
-               }
        }
 
        if (tab->bmap) {
@@ -2257,11 +2282,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,
@@ -4251,7 +4290,7 @@ static __isl_give isl_map *basic_map_partial_lexopt(
  *
  *     a x >= -u >= -b_i(p)
  *
- * Moreover, m = min_i(b_i(p)) satisfied the constraints on u and can
+ * Moreover, m = min_i(b_i(p)) satisfies the constraints on u and can
  * therefore be plugged into the solution.
  */
 static __isl_give isl_map *basic_map_partial_lexopt_symm(
@@ -4417,6 +4456,9 @@ struct isl_map *isl_tab_basic_map_partial_lexopt(
        isl_assert(bmap->ctx,
            isl_basic_map_compatible_domain(bmap, dom), goto error);
 
+       if (isl_basic_set_dim(dom, isl_dim_all) == 0)
+               return basic_map_partial_lexopt(bmap, dom, empty, max);
+
        bmap = isl_basic_map_intersect_domain(bmap, isl_basic_set_copy(dom));
        bmap = isl_basic_map_detect_equalities(bmap);
        bmap = isl_basic_map_remove_redundancies(bmap);