Merge branch 'maint'
[platform/upstream/isl.git] / isl_tab_pip.c
index 412e8ee..4e613f5 100644 (file)
@@ -17,6 +17,7 @@
 #include "isl_sample.h"
 #include <isl_mat_private.h>
 #include <isl_aff_private.h>
+#include <isl_options_private.h>
 #include <isl_config.h>
 
 /*
@@ -430,6 +431,8 @@ static void sol_add(struct isl_sol *sol, struct isl_tab *tab)
 
        if (tab->empty && !sol->add_empty)
                return;
+       if (sol->context->op->is_empty(sol->context))
+               return;
 
        bset = sol_domain(sol);
 
@@ -742,6 +745,30 @@ static struct isl_vec *get_row_parameter_ineq(struct isl_tab *tab, int row)
        return ineq;
 }
 
+/* Normalize a div expression of the form
+ *
+ *     [(g*f(x) + c)/(g * m)]
+ *
+ * with c the constant term and f(x) the remaining coefficients, to
+ *
+ *     [(f(x) + [c/g])/m]
+ */
+static void normalize_div(__isl_keep isl_vec *div)
+{
+       isl_ctx *ctx = isl_vec_get_ctx(div);
+       int len = div->size - 2;
+
+       isl_seq_gcd(div->el + 2, len, &ctx->normalize_gcd);
+       isl_int_gcd(ctx->normalize_gcd, ctx->normalize_gcd, div->el[0]);
+
+       if (isl_int_is_one(ctx->normalize_gcd))
+               return;
+
+       isl_int_divexact(div->el[0], div->el[0], ctx->normalize_gcd);
+       isl_int_fdiv_q(div->el[1], div->el[1], ctx->normalize_gcd);
+       isl_seq_scale_down(div->el + 2, div->el + 2, ctx->normalize_gcd, len);
+}
+
 /* Return a integer division for use in a parametric cut based on the given row.
  * In particular, let the parametric constant of the row be
  *
@@ -762,7 +789,7 @@ static struct isl_vec *get_row_parameter_div(struct isl_tab *tab, int row)
 
        isl_int_set(div->el[0], tab->mat->row[row][0]);
        get_row_parameter_line(tab, row, div->el + 1);
-       div = isl_vec_normalize(div);
+       normalize_div(div);
        isl_seq_neg(div->el + 1, div->el + 1, div->size - 1);
        isl_seq_fdiv_r(div->el + 1, div->el + 1, div->el[0], div->size - 1);
 
@@ -790,7 +817,7 @@ static struct isl_vec *get_row_split_div(struct isl_tab *tab, int row)
 
        isl_int_set(div->el[0], tab->mat->row[row][0]);
        get_row_parameter_line(tab, row, div->el + 1);
-       div = isl_vec_normalize(div);
+       normalize_div(div);
        isl_seq_fdiv_r(div->el + 1, div->el + 1, div->el[0], div->size - 1);
 
        return div;
@@ -828,7 +855,7 @@ static struct isl_vec *ineq_for_div(struct isl_basic_set *bset, unsigned div)
 }
 
 /* Given a row in the tableau and a div that was created
- * using get_row_split_div and that been constrained to equality, i.e.,
+ * using get_row_split_div and that has been constrained to equality, i.e.,
  *
  *             d = floor(\sum_i {a_i} y_i) = \sum_i {a_i} y_i
  *
@@ -859,7 +886,8 @@ static struct isl_tab *set_row_cst_to_div(struct isl_tab *tab, int row, int div)
        } else {
                int dcol = tab->var[tab->n_var - tab->n_div + div].index;
 
-               isl_int_set_si(tab->mat->row[row][2 + tab->M + dcol], 1);
+               isl_int_add_ui(tab->mat->row[row][2 + tab->M + dcol],
+                               tab->mat->row[row][2 + tab->M + dcol], 1);
        }
 
        return tab;
@@ -1602,6 +1630,9 @@ static int add_cut(struct isl_tab *tab, int row)
        return tab->con[r].index;
 }
 
+#define CUT_ALL 1
+#define CUT_ONE 0
+
 /* Given a non-parametric tableau, add cuts until an integer
  * sample point is obtained or until the tableau is determined
  * to be integer infeasible.
@@ -1613,8 +1644,12 @@ static int add_cut(struct isl_tab *tab, int row)
  * combination of variables/constraints plus a non-integral constant,
  * then there is no way to obtain an integer point and we return
  * a tableau that is marked empty.
+ * The parameter cutting_strategy controls the strategy used when adding cuts
+ * to remove non-integer points. CUT_ALL adds all possible cuts
+ * before continuing the search. CUT_ONE adds only one cut at a time.
  */
-static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab)
+static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab,
+       int cutting_strategy)
 {
        int var;
        int row;
@@ -1636,6 +1671,8 @@ static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab)
                        row = add_cut(tab, row);
                        if (row < 0)
                                goto error;
+                       if (cutting_strategy == CUT_ONE)
+                               break;
                } while ((var = next_non_integer_var(tab, var, &flags)) != -1);
                if (restore_lexmin(tab) < 0)
                        goto error;
@@ -1726,7 +1763,7 @@ static struct isl_tab *check_integer_feasible(struct isl_tab *tab)
        if (isl_tab_push_basis(tab) < 0)
                goto error;
 
-       tab = cut_to_integer_lexmin(tab);
+       tab = cut_to_integer_lexmin(tab, CUT_ALL);
        if (!tab)
                goto error;
 
@@ -2508,7 +2545,6 @@ static struct isl_tab *context_tab_for_lexmin(struct isl_basic_set *bset)
 {
        struct isl_tab *tab;
 
-       bset = isl_basic_set_cow(bset);
        if (!bset)
                return NULL;
        tab = tab_for_lexmin((struct isl_basic_map *)bset, NULL, 1, 0);
@@ -2607,7 +2643,7 @@ static void gbr_init_shifted(struct isl_context_gbr *cgbr)
                }
        }
 
-       cgbr->shifted = isl_tab_from_basic_set(bset);
+       cgbr->shifted = isl_tab_from_basic_set(bset, 0);
 
        for (i = 0; i < bset->n_ineq; ++i)
                isl_int_set(bset->ineq[i][0], cst->el[i]);
@@ -2680,7 +2716,8 @@ static struct isl_vec *gbr_get_sample(struct isl_context_gbr *cgbr)
                cgbr->cone = isl_tab_from_recession_cone(bset, 0);
                if (!cgbr->cone)
                        return NULL;
-               if (isl_tab_track_bset(cgbr->cone, isl_basic_set_dup(bset)) < 0)
+               if (isl_tab_track_bset(cgbr->cone,
+                                       isl_basic_set_copy(bset)) < 0)
                        return NULL;
        }
        if (isl_tab_detect_implicit_equalities(cgbr->cone) < 0)
@@ -3042,7 +3079,8 @@ static int context_gbr_detect_equalities(struct isl_context *context,
                cgbr->cone = isl_tab_from_recession_cone(bset, 0);
                if (!cgbr->cone)
                        goto error;
-               if (isl_tab_track_bset(cgbr->cone, isl_basic_set_dup(bset)) < 0)
+               if (isl_tab_track_bset(cgbr->cone,
+                                       isl_basic_set_copy(bset)) < 0)
                        goto error;
        }
        if (isl_tab_detect_implicit_equalities(cgbr->cone) < 0)
@@ -3244,13 +3282,10 @@ static struct isl_context *isl_context_gbr_alloc(struct isl_basic_set *dom)
 
        cgbr->shifted = NULL;
        cgbr->cone = NULL;
-       cgbr->tab = isl_tab_from_basic_set(dom);
+       cgbr->tab = isl_tab_from_basic_set(dom, 1);
        cgbr->tab = isl_tab_init_samples(cgbr->tab);
        if (!cgbr->tab)
                goto error;
-       if (isl_tab_track_bset(cgbr->tab,
-                               isl_basic_set_cow(isl_basic_set_copy(dom))) < 0)
-               goto error;
        check_gbr_integer_feasible(cgbr);
 
        return &cgbr->context;
@@ -4650,6 +4685,7 @@ static void sol_for_add(struct isl_sol_for *sol,
                        isl_int_set(aff->v->el[0], M->row[0][0]);
                        isl_seq_cpy(aff->v->el + 1, M->row[i], M->n_col);
                }
+               aff = isl_aff_normalize(aff);
                list = isl_aff_list_add(list, aff);
        }
        isl_local_space_free(ls);
@@ -4763,30 +4799,6 @@ int isl_basic_set_foreach_lexopt(__isl_keep isl_basic_set *bset, int max,
        return isl_basic_map_foreach_lexopt(bset, max, fn, user);
 }
 
-int isl_basic_map_foreach_lexmin(__isl_keep isl_basic_map *bmap,
-       int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_aff_list *list,
-                 void *user),
-       void *user)
-{
-       return isl_basic_map_foreach_lexopt(bmap, 0, fn, user);
-}
-
-int isl_basic_map_foreach_lexmax(__isl_keep isl_basic_map *bmap,
-       int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_aff_list *list,
-                 void *user),
-       void *user)
-{
-       return isl_basic_map_foreach_lexopt(bmap, 1, fn, user);
-}
-
-int isl_basic_set_foreach_lexmax(__isl_keep isl_basic_set *bset,
-       int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_aff_list *list,
-                 void *user),
-       void *user)
-{
-       return isl_basic_map_foreach_lexmax(bset, fn, user);
-}
-
 /* Check if the given sequence of len variables starting at pos
  * represents a trivial (i.e., zero) solution.
  * The variables are assumed to be non-negative and to come in pairs,
@@ -4979,7 +4991,7 @@ __isl_give isl_vec *isl_tab_basic_set_non_trivial_lexmin(
                int side, base;
 
                if (init) {
-                       tab = cut_to_integer_lexmin(tab);
+                       tab = cut_to_integer_lexmin(tab, CUT_ONE);
                        if (!tab)
                                goto error;
                        if (tab->empty)
@@ -5160,6 +5172,7 @@ static void sol_pma_add(struct isl_sol_pma *sol,
        isl_local_space_free(ls);
        isl_mat_free(M);
        dom = isl_basic_set_simplify(dom);
+       dom = isl_basic_set_finalize(dom);
        pma = isl_pw_multi_aff_alloc(isl_set_from_basic_set(dom), maff);
        sol->pma = isl_pw_multi_aff_add_disjoint(sol->pma, pma);
        if (!sol->pma)