summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--basis_reduction_templ.c2
-rw-r--r--isl_affine_hull.c6
-rw-r--r--isl_coalesce.c4
-rw-r--r--isl_convex_hull.c6
-rw-r--r--isl_lp.c2
-rw-r--r--isl_map.c2
-rw-r--r--isl_map_simplify.c4
-rw-r--r--isl_map_subtract.c4
-rw-r--r--isl_sample.c6
-rw-r--r--isl_scan.c2
-rw-r--r--isl_tab.c23
-rw-r--r--isl_tab.h10
-rw-r--r--isl_tab_pip.c6
-rw-r--r--isl_vertices.c7
14 files changed, 46 insertions, 38 deletions
diff --git a/basis_reduction_templ.c b/basis_reduction_templ.c
index f4c50edd..46fd9112 100644
--- 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 96af3134..2b606e9b 100644
--- 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 b99c7b53..1a4078e4 100644
--- 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 52c59d21..6fd95bf6 100644
--- 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 d2e35a5b..2438b0c7 100644
--- 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 b91fc274..41d5d49b 100644
--- 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 e5687333..29bb39de 100644
--- 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 1fd40868..e34a3697 100644
--- 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 ec63745e..d25a5c9c 100644
--- 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 64654be4..64235926 100644
--- 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 273d4b63..097b335c 100644
--- 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 3f68d851..786e6fde 100644
--- 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 c864e03d..d94e51f5 100644
--- 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 5a4f8e3f..3cc40264 100644
--- 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);
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-19 16:19:20 +0000