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 1f2ab1b..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,
@@ -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) {
@@ -4431,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);