isl_tab_from_basic_map: preserve all constraints in input when tracking

If the user wants to keep track of a basic map representation of the tableau,
then we need to make sure that the initial tableau corresponds exactly to
the input.  In particular, we need to make sure that no (redundant) constraints
are removed.

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

diff --git a/basis_reduction_templ.c b/basis_reduction_templ.c
index f4c50ed..46fd911 100644 (file)
--- a/basis_reduction_templ.c
+++ b/basis_reduction_templ.c
@@ -329,7 +329,7 @@ struct isl_mat *isl_basic_set_reduced_basis(struct isl_basic_set *bset)
                isl_die(bset->ctx, isl_error_invalid,
                        "no parameters allowed", return NULL);
 
-       tab = isl_tab_from_basic_set(bset);
+       tab = isl_tab_from_basic_set(bset, 0);
        if (!tab)
                return NULL;
 

diff --git a/isl_affine_hull.c b/isl_affine_hull.c
index 96af313..2b606e9 100644 (file)
--- a/isl_affine_hull.c
+++ b/isl_affine_hull.c
@@ -34,7 +34,7 @@ struct isl_basic_map *isl_basic_map_implicit_equalities(
        if (bmap->n_ineq <= 1)
                return bmap;
 
-       tab = isl_tab_from_basic_map(bmap);
+       tab = isl_tab_from_basic_map(bmap, 0);
        if (isl_tab_detect_implicit_equalities(tab) < 0)
                goto error;
        bmap = isl_basic_map_update_from_tab(bmap, tab);
@@ -480,7 +480,7 @@ static struct isl_basic_set *uset_affine_hull_bounded(struct isl_basic_set *bset
                }
        }
 
-       tab = isl_tab_from_basic_set(bset);
+       tab = isl_tab_from_basic_set(bset, 1);
        if (!tab)
                goto error;
        if (tab->empty) {
@@ -488,8 +488,6 @@ static struct isl_basic_set *uset_affine_hull_bounded(struct isl_basic_set *bset
                isl_vec_free(sample);
                return isl_basic_set_set_to_empty(bset);
        }
-       if (isl_tab_track_bset(tab, isl_basic_set_copy(bset)) < 0)
-               goto error;
 
        if (!sample) {
                struct isl_tab_undo *snap;

diff --git a/isl_coalesce.c b/isl_coalesce.c
index b99c7b5..1a4078e 100644 (file)
--- a/isl_coalesce.c
+++ b/isl_coalesce.c
@@ -223,7 +223,7 @@ static int fuse(struct isl_map *map, int i, int j,
            ISL_F_ISSET(map->p[j], ISL_BASIC_MAP_RATIONAL))
                ISL_F_SET(fused, ISL_BASIC_MAP_RATIONAL);
 
-       fused_tab = isl_tab_from_basic_map(fused);
+       fused_tab = isl_tab_from_basic_map(fused, 0);
        if (isl_tab_detect_redundant(fused_tab) < 0)
                goto error;
 
@@ -1242,7 +1242,7 @@ struct isl_map *isl_map_coalesce(struct isl_map *map)
 
        n = map->n;
        for (i = 0; i < map->n; ++i) {
-               tabs[i] = isl_tab_from_basic_map(map->p[i]);
+               tabs[i] = isl_tab_from_basic_map(map->p[i], 0);
                if (!tabs[i])
                        goto error;
                if (!ISL_F_ISSET(map->p[i], ISL_BASIC_MAP_NO_IMPLICIT))

diff --git a/isl_convex_hull.c b/isl_convex_hull.c
index 52c59d2..6fd95bf 100644 (file)
--- a/isl_convex_hull.c
+++ b/isl_convex_hull.c
@@ -94,7 +94,7 @@ __isl_give isl_basic_map *isl_basic_map_remove_redundancies(
        if (bmap->n_ineq <= 1)
                return bmap;
 
-       tab = isl_tab_from_basic_map(bmap);
+       tab = isl_tab_from_basic_map(bmap, 0);
        if (isl_tab_detect_implicit_equalities(tab) < 0)
                goto error;
        if (isl_tab_detect_redundant(tab) < 0)
@@ -1169,7 +1169,7 @@ static struct isl_vec *valid_direction(
                goto error;
        lp = valid_direction_lp(isl_basic_set_copy(bset1),
                                isl_basic_set_copy(bset2));
-       tab = isl_tab_from_basic_set(lp);
+       tab = isl_tab_from_basic_set(lp, 0);
        sample = isl_tab_get_sample_value(tab);
        isl_tab_free(tab);
        isl_basic_set_free(lp);
@@ -2117,7 +2117,7 @@ static int is_bound(struct sh_data *data, struct isl_set *set, int j,
        isl_int opt;
 
        if (!data->p[j].tab) {
-               data->p[j].tab = isl_tab_from_basic_set(set->p[j]);
+               data->p[j].tab = isl_tab_from_basic_set(set->p[j], 0);
                if (!data->p[j].tab)
                        return -1;
        }

diff --git a/isl_lp.c b/isl_lp.c
index d2e35a5..2438b0c 100644 (file)
--- a/isl_lp.c
+++ b/isl_lp.c
@@ -28,7 +28,7 @@ enum isl_lp_result isl_tab_solve_lp(struct isl_basic_map *bmap, int maximize,
                isl_seq_neg(f, f, 1 + dim);
 
        bmap = isl_basic_map_gauss(bmap, NULL);
-       tab = isl_tab_from_basic_map(bmap);
+       tab = isl_tab_from_basic_map(bmap, 0);
        res = isl_tab_min(tab, f, denom, opt, opt_denom, 0);
        if (res == isl_lp_ok && sol) {
                *sol = isl_tab_get_sample_value(tab);

diff --git a/isl_map.c b/isl_map.c
index b91fc27..41d5d49 100644 (file)
--- a/isl_map.c
+++ b/isl_map.c
@@ -8730,7 +8730,7 @@ int isl_basic_set_vars_get_sign(__isl_keep isl_basic_set *bset,
                return -1;
 
        bound = isl_vec_alloc(bset->ctx, 1 + isl_basic_set_total_dim(bset));
-       tab = isl_tab_from_basic_set(bset);
+       tab = isl_tab_from_basic_set(bset, 0);
        if (!bound || !tab)
                goto error;
 

diff --git a/isl_map_simplify.c b/isl_map_simplify.c
index e568733..29bb39d 100644 (file)
--- a/isl_map_simplify.c
+++ b/isl_map_simplify.c
@@ -1579,7 +1579,7 @@ static __isl_give isl_basic_set *uset_gist_full(__isl_take isl_basic_set *bset,
        context_ineq = context->n_ineq;
        combined = isl_basic_set_cow(isl_basic_set_copy(context));
        combined = isl_basic_set_extend_constraints(combined, 0, bset->n_ineq);
-       tab = isl_tab_from_basic_set(combined);
+       tab = isl_tab_from_basic_set(combined, 0);
        for (i = 0; i < context_ineq; ++i)
                if (isl_tab_freeze_constraint(tab, i) < 0)
                        goto error;
@@ -2207,7 +2207,7 @@ static struct isl_basic_map *drop_more_redundant_divs(
        if (!vec)
                goto error;
 
-       tab = isl_tab_from_basic_map(bmap);
+       tab = isl_tab_from_basic_map(bmap, 0);
 
        while (n > 0) {
                int i, l, u;

diff --git a/isl_map_subtract.c b/isl_map_subtract.c
index 1fd4086..e34a369 100644 (file)
--- a/isl_map_subtract.c
+++ b/isl_map_subtract.c
@@ -312,9 +312,7 @@ static int basic_map_collect_diff(__isl_take isl_basic_map *bmap,
        bmap = isl_basic_map_order_divs(bmap);
        map = isl_map_order_divs(map);
 
-       tab = isl_tab_from_basic_map(bmap);
-       if (isl_tab_track_bmap(tab, isl_basic_map_copy(bmap)) < 0)
-               goto error;
+       tab = isl_tab_from_basic_map(bmap, 1);
 
        modified = 0;
        level = 0;

diff --git a/isl_sample.c b/isl_sample.c
index ec63745..d25a5c9 100644 (file)
--- a/isl_sample.c
+++ b/isl_sample.c
@@ -657,7 +657,7 @@ static struct isl_vec *sample_bounded(struct isl_basic_set *bset)
                
        ctx = bset->ctx;
 
-       tab = isl_tab_from_basic_set(bset);
+       tab = isl_tab_from_basic_set(bset, 1);
        if (tab && tab->empty) {
                isl_tab_free(tab);
                ISL_F_SET(bset, ISL_BASIC_SET_EMPTY);
@@ -666,8 +666,6 @@ static struct isl_vec *sample_bounded(struct isl_basic_set *bset)
                return sample;
        }
 
-       if (isl_tab_track_bset(tab, isl_basic_set_copy(bset)) < 0)
-               goto error;
        if (!ISL_F_ISSET(bset, ISL_BASIC_SET_NO_IMPLICIT))
                if (isl_tab_detect_implicit_equalities(tab) < 0)
                        goto error;
@@ -746,7 +744,7 @@ static struct isl_vec *rational_sample(struct isl_basic_set *bset)
        if (!bset)
                return NULL;
 
-       tab = isl_tab_from_basic_set(bset);
+       tab = isl_tab_from_basic_set(bset, 0);
        sample = isl_tab_get_sample_value(tab);
        isl_tab_free(tab);
 

diff --git a/isl_scan.c b/isl_scan.c
index 64654be..6423592 100644 (file)
--- a/isl_scan.c
+++ b/isl_scan.c
@@ -124,7 +124,7 @@ int isl_basic_set_scan(struct isl_basic_set *bset,
        if (!min || !max || !snap)
                goto error;
 
-       tab = isl_tab_from_basic_set(bset);
+       tab = isl_tab_from_basic_set(bset, 0);
        if (!tab)
                goto error;
        if (isl_tab_extend_cons(tab, dim + 1) < 0)

diff --git a/isl_tab.c b/isl_tab.c
index 273d4b6..097b335 100644 (file)
--- a/isl_tab.c
+++ b/isl_tab.c
@@ -939,7 +939,7 @@ int isl_tab_mark_redundant(struct isl_tab *tab, int row)
        struct isl_tab_var *var = isl_tab_var_from_row(tab, row);
        var->is_redundant = 1;
        isl_assert(tab->mat->ctx, row >= tab->n_redundant, return -1);
-       if (tab->need_undo || tab->row_var[row] >= 0) {
+       if (tab->preserve || tab->need_undo || tab->row_var[row] >= 0) {
                if (tab->row_var[row] >= 0 && !var->is_nonneg) {
                        var->is_nonneg = 1;
                        if (isl_tab_push_var(tab, isl_tab_undo_nonneg, var) < 0)
@@ -2199,7 +2199,13 @@ int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div,
        return r;
 }
 
-struct isl_tab *isl_tab_from_basic_map(struct isl_basic_map *bmap)
+/* If "track" is set, then we want to keep track of all constraints in tab
+ * in its bmap field.  This field is initialized from a copy of "bmap",
+ * so we need to make sure that all constraints in "bmap" also appear
+ * in the constructed tab.
+ */
+__isl_give struct isl_tab *isl_tab_from_basic_map(
+       __isl_keep isl_basic_map *bmap, int track)
 {
        int i;
        struct isl_tab *tab;
@@ -2211,11 +2217,12 @@ struct isl_tab *isl_tab_from_basic_map(struct isl_basic_map *bmap)
                            isl_basic_map_total_dim(bmap), 0);
        if (!tab)
                return NULL;
+       tab->preserve = track;
        tab->rational = ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL);
        if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_EMPTY)) {
                if (isl_tab_mark_empty(tab) < 0)
                        goto error;
-               return tab;
+               goto done;
        }
        for (i = 0; i < bmap->n_eq; ++i) {
                tab = add_eq(tab, bmap->eq[i]);
@@ -2226,17 +2233,21 @@ struct isl_tab *isl_tab_from_basic_map(struct isl_basic_map *bmap)
                if (isl_tab_add_ineq(tab, bmap->ineq[i]) < 0)
                        goto error;
                if (tab->empty)
-                       return tab;
+                       goto done;
        }
+done:
+       if (track && isl_tab_track_bmap(tab, isl_basic_map_copy(bmap)) < 0)
+               goto error;
        return tab;
 error:
        isl_tab_free(tab);
        return NULL;
 }
 
-struct isl_tab *isl_tab_from_basic_set(struct isl_basic_set *bset)
+__isl_give struct isl_tab *isl_tab_from_basic_set(
+       __isl_keep isl_basic_set *bset, int track)
 {
-       return isl_tab_from_basic_map((struct isl_basic_map *)bset);
+       return isl_tab_from_basic_map(bset, track);
 }
 
 /* Construct a tableau corresponding to the recession cone of "bset".

diff --git a/isl_tab.h b/isl_tab.h
index 3f68d85..786e6fd 100644 (file)
--- a/isl_tab.h
+++ b/isl_tab.h
@@ -118,6 +118,9 @@ struct isl_tab_undo {
  * can be reinstated during rollback when the constraint that cut them
  * out is removed.  These samples are only maintained for the context
  * tableau while solving PILP problems.
+ *
+ * If "preserve" is set, then we want to keep all constraints in the
+ * tableau, even if they turn out to be redundant.
  */
 enum isl_tab_row_sign {
        isl_tab_row_unknown = 0,
@@ -166,6 +169,7 @@ struct isl_tab {
 
        unsigned strict_redundant : 1;
        unsigned need_undo : 1;
+       unsigned preserve : 1;
        unsigned rational : 1;
        unsigned empty : 1;
        unsigned in_undo : 1;
@@ -177,8 +181,10 @@ struct isl_tab *isl_tab_alloc(struct isl_ctx *ctx,
        unsigned n_row, unsigned n_var, unsigned M);
 void isl_tab_free(struct isl_tab *tab);
 
-struct isl_tab *isl_tab_from_basic_map(struct isl_basic_map *bmap);
-struct isl_tab *isl_tab_from_basic_set(struct isl_basic_set *bset);
+__isl_give struct isl_tab *isl_tab_from_basic_map(
+       __isl_keep isl_basic_map *bmap, int track);
+__isl_give struct isl_tab *isl_tab_from_basic_set(
+       __isl_keep isl_basic_set *bset, int track);
 struct isl_tab *isl_tab_from_recession_cone(struct isl_basic_set *bset,
        int parametric);
 int isl_tab_cone_is_bounded(struct isl_tab *tab);

diff --git a/isl_tab_pip.c b/isl_tab_pip.c
index c864e03..d94e51f 100644 (file)
--- a/isl_tab_pip.c
+++ b/isl_tab_pip.c
@@ -2608,7 +2608,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]);
@@ -3247,12 +3247,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_copy(dom)) < 0)
-               goto error;
        check_gbr_integer_feasible(cgbr);
 
        return &cgbr->context;

diff --git a/isl_vertices.c b/isl_vertices.c
index 5a4f8e3..3cc4026 100644 (file)
--- a/isl_vertices.c
+++ b/isl_vertices.c
@@ -422,7 +422,7 @@ __isl_give isl_vertices *isl_basic_set_compute_vertices(
        if (!bset)
                return NULL;
 
-       tab = isl_tab_from_basic_set(bset);
+       tab = isl_tab_from_basic_set(bset, 0);
        if (!tab)
                goto error;
        tab->strict_redundant = 1;
@@ -876,12 +876,11 @@ static __isl_give isl_vertices *compute_chambers(__isl_take isl_basic_set *bset,
 
        bset = isl_basic_set_params(bset);
 
-       tab = isl_tab_from_basic_set(bset);
+       tab = isl_tab_from_basic_set(bset, 1);
+       isl_basic_set_free(bset);
        for (i = 0; i < bset->n_ineq; ++i)
                if (isl_tab_freeze_constraint(tab, i) < 0)
                        goto error;
-       if (isl_tab_track_bset(tab, bset) < 0)
-               goto error;
 
        snap = isl_tab_snap(tab);