1 files changed, 349 insertions, 273 deletions

diff --git a/polly/lib/External/isl/isl_tab_pip.c b/polly/lib/External/isl/isl_tab_pip.c
index d4747b4807a..c50103427e9 100644
--- a/polly/lib/External/isl/isl_tab_pip.c
+++ b/polly/lib/External/isl/isl_tab_pip.c
@@ -173,13 +173,11 @@ struct isl_sol_callback {
  *
  * The context tableau is owned by isl_sol and is updated incrementally.
  *
- * There are currently three implementations of this interface,
+ * There are currently two implementations of this interface,
  * isl_sol_map, which simply collects the solutions in an isl_map
  * and (optionally) the parts of the context where there is no solution
- * in an isl_set,
- * isl_sol_pma, which collects an isl_pw_multi_aff instead, and
- * isl_sol_for, which calls a user-defined function for each part of
- * the solution.
+ * in an isl_set, and
+ * isl_sol_pma, which collects an isl_pw_multi_aff instead.
  */
 struct isl_sol {
 	int error;
@@ -1166,7 +1164,7 @@ static int is_obviously_nonneg(struct isl_tab *tab, int row)
  * Pivoting with column c will increment the sample value by a non-negative
  * constant times a_{V,c}/a_{r,c}, with a_{V,c} the elements of column c
  * corresponding to the non-parametric variables.
- * If variable v appears in a column c_v, the a_{v,c} = 1 iff c = c_v,
+ * If variable v appears in a column c_v, then a_{v,c} = 1 iff c = c_v,
  * with all other entries in this virtual row equal to zero.
  * If variable v appears in a row, then a_{v,c} is the element in column c
  * of that row.
@@ -1219,6 +1217,37 @@ static int lexmin_col_pair(struct isl_tab *tab,
 	return -1;
 }
 
+/* Does the index into the tab->var or tab->con array "index"
+ * correspond to a variable in the context tableau?
+ * In particular, it needs to be an index into the tab->var array and
+ * it needs to refer to either one of the first tab->n_param variables or
+ * one of the last tab->n_div variables.
+ */
+static int is_parameter_var(struct isl_tab *tab, int index)
+{
+	if (index < 0)
+		return 0;
+	if (index < tab->n_param)
+		return 1;
+	if (index >= tab->n_var - tab->n_div)
+		return 1;
+	return 0;
+}
+
+/* Does column "col" of "tab" refer to a variable in the context tableau?
+ */
+static int col_is_parameter_var(struct isl_tab *tab, int col)
+{
+	return is_parameter_var(tab, tab->col_var[col]);
+}
+
+/* Does row "row" of "tab" refer to a variable in the context tableau?
+ */
+static int row_is_parameter_var(struct isl_tab *tab, int row)
+{
+	return is_parameter_var(tab, tab->row_var[row]);
+}
+
 /* Given a row in the tableau, find and return the column that would
  * result in the lexicographically smallest, but positive, increment
  * in the sample point.
@@ -1237,9 +1266,7 @@ static int lexmin_pivot_col(struct isl_tab *tab, int row)
 	isl_int_init(tmp);
 
 	for (j = tab->n_dead; j < tab->n_col; ++j) {
-		if (tab->col_var[j] >= 0 &&
-		    (tab->col_var[j] < tab->n_param  ||
-		    tab->col_var[j] >= tab->n_var - tab->n_div))
+		if (col_is_parameter_var(tab, j))
 			continue;
 
 		if (!isl_int_is_pos(tr[j]))
@@ -1309,9 +1336,7 @@ static void check_lexpos(struct isl_tab *tab)
 	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))
+		if (col_is_parameter_var(tab, col))
 			continue;
 		for (var = tab->n_param; var < tab->n_var - tab->n_div; ++var) {
 			if (!tab->var[var].is_row) {
@@ -1361,9 +1386,7 @@ static int report_conflict(struct isl_tab *tab, int row)
 	tr = tab->mat->row[row] + 2 + tab->M;
 
 	for (j = tab->n_dead; j < tab->n_col; ++j) {
-		if (tab->col_var[j] >= 0 &&
-		    (tab->col_var[j] < tab->n_param  ||
-		    tab->col_var[j] >= tab->n_var - tab->n_div))
+		if (col_is_parameter_var(tab, j))
 			continue;
 
 		if (!isl_int_is_neg(tr[j]))
@@ -1511,6 +1534,25 @@ static int is_constant(struct isl_tab *tab, int row)
 					tab->n_col - tab->n_dead) == -1;
 }
 
+/* Is the given row a parametric constant?
+ * That is, does it only involve variables that also appear in the context?
+ */
+static int is_parametric_constant(struct isl_tab *tab, int row)
+{
+	unsigned off = 2 + tab->M;
+	int col;
+
+	for (col = tab->n_dead; col < tab->n_col; ++col) {
+		if (col_is_parameter_var(tab, col))
+			continue;
+		if (isl_int_is_zero(tab->mat->row[row][off + col]))
+			continue;
+		return 0;
+	}
+
+	return 1;
+}
+
 /* Add an equality that may or may not be valid to the tableau.
  * If the resulting row is a pure constant, then it must be zero.
  * Otherwise, the resulting tableau is empty.
@@ -1675,9 +1717,7 @@ static int integer_variable(struct isl_tab *tab, int row)
 	unsigned off = 2 + tab->M;
 
 	for (i = tab->n_dead; i < tab->n_col; ++i) {
-		if (tab->col_var[i] >= 0 &&
-		    (tab->col_var[i] < tab->n_param ||
-		     tab->col_var[i] >= tab->n_var - tab->n_div))
+		if (col_is_parameter_var(tab, i))
 			continue;
 		if (!isl_int_is_divisible_by(tab->mat->row[row][off + i],
 						tab->mat->row[row][0]))
@@ -2107,7 +2147,7 @@ static int get_div(struct isl_tab *tab, struct isl_context *context,
 }
 
 /* Add a parametric cut to cut away the non-integral sample value
- * of the give row.
+ * of the given row.
  * Let a_i be the coefficients of the constant term and the parameters
  * and let b_i be the coefficients of the variables or constraints
  * in basis of the tableau.
@@ -2303,7 +2343,13 @@ error:
 /* Given a main tableau where more than one row requires a split,
  * determine and return the "best" row to split on.
  *
- * Given two rows in the main tableau, if the inequality corresponding
+ * If any of the rows requiring a split only involves
+ * variables that also appear in the context tableau,
+ * then the negative part is guaranteed not to have a solution.
+ * It is therefore best to split on any of these rows first.
+ *
+ * Otherwise,
+ * given two rows in the main tableau, if the inequality corresponding
  * to the first row is redundant with respect to that of the second row
  * in the current tableau, then it is better to split on the second row,
  * since in the positive part, both rows will be positive.
@@ -2347,6 +2393,9 @@ static int best_split(struct isl_tab *tab, struct isl_tab *context_tab)
 		if (tab->row_sign[split] != isl_tab_row_any)
 			continue;
 
+		if (is_parametric_constant(tab, split))
+			return split;
+
 		ineq = get_row_parameter_ineq(tab, split);
 		if (!ineq)
 			return -1;
@@ -3660,9 +3709,7 @@ static int is_critical(struct isl_tab *tab, int row)
 	unsigned off = 2 + tab->M;
 
 	for (j = tab->n_dead; j < tab->n_col; ++j) {
-		if (tab->col_var[j] >= 0 &&
-		    (tab->col_var[j] < tab->n_param  ||
-		    tab->col_var[j] >= tab->n_var - tab->n_div))
+		if (col_is_parameter_var(tab, j))
 			continue;
 
 		if (isl_int_is_pos(tab->mat->row[row][off + j]))
@@ -4170,10 +4217,7 @@ static void find_solutions_main(struct isl_sol *sol, struct isl_tab *tab)
 		int p;
 		struct isl_vec *eq;
 
-		if (tab->row_var[row] < 0)
-			continue;
-		if (tab->row_var[row] >= tab->n_param &&
-		    tab->row_var[row] < tab->n_var - tab->n_div)
+		if (!row_is_parameter_var(tab, row))
 			continue;
 		if (tab->row_var[row] < tab->n_param)
 			p = tab->row_var[row];
@@ -4898,145 +4942,6 @@ static __isl_give isl_basic_set *extract_domain(__isl_keep isl_basic_map *bmap,
 #define SUFFIX
 #include "isl_tab_lexopt_templ.c"
 
-struct isl_sol_for {
-	struct isl_sol	sol;
-	isl_stat	(*fn)(__isl_take isl_basic_set *dom,
-				__isl_take isl_aff_list *list, void *user);
-	void		*user;
-};
-
-static void sol_for_free(struct isl_sol *sol)
-{
-}
-
-/* Add the solution identified by the tableau and the context tableau.
- * In particular, "dom" represents the context and "ma" expresses
- * the solution on that context.
- *
- * See documentation of sol_add for more details.
- *
- * Instead of constructing a basic map, this function calls a user
- * defined function with the current context as a basic set and
- * a list of affine expressions representing the relation between
- * the input and output.  The space over which the affine expressions
- * are defined is the same as that of the domain.  The number of
- * affine expressions in the list is equal to the number of output variables.
- */
-static void sol_for_add(struct isl_sol_for *sol,
-	__isl_take isl_basic_set *dom, __isl_take isl_multi_aff *ma)
-{
-	int i, n;
-	isl_ctx *ctx;
-	isl_aff *aff;
-	isl_aff_list *list;
-
-	if (sol->sol.error || !dom || !ma)
-		goto error;
-
-	ctx = isl_basic_set_get_ctx(dom);
-	n = isl_multi_aff_dim(ma, isl_dim_out);
-	list = isl_aff_list_alloc(ctx, n);
-	for (i = 0; i < n; ++i) {
-		aff = isl_multi_aff_get_aff(ma, i);
-		list = isl_aff_list_add(list, aff);
-	}
-
-	dom = isl_basic_set_finalize(dom);
-
-	if (sol->fn(isl_basic_set_copy(dom), list, sol->user) < 0)
-		goto error;
-
-	isl_basic_set_free(dom);
-	isl_multi_aff_free(ma);
-	return;
-error:
-	isl_basic_set_free(dom);
-	isl_multi_aff_free(ma);
-	sol->sol.error = 1;
-}
-
-static void sol_for_add_wrap(struct isl_sol *sol,
-	__isl_take isl_basic_set *dom, __isl_take isl_multi_aff *ma)
-{
-	sol_for_add((struct isl_sol_for *)sol, dom, ma);
-}
-
-static struct isl_sol_for *sol_for_init(__isl_keep isl_basic_map *bmap, int max,
-	isl_stat (*fn)(__isl_take isl_basic_set *dom,
-		__isl_take isl_aff_list *list, void *user),
-	void *user)
-{
-	struct isl_sol_for *sol_for = NULL;
-	isl_space *dom_dim;
-	struct isl_basic_set *dom = NULL;
-
-	sol_for = isl_calloc_type(bmap->ctx, struct isl_sol_for);
-	if (!sol_for)
-		goto error;
-
-	dom_dim = isl_space_domain(isl_space_copy(bmap->dim));
-	dom = isl_basic_set_universe(dom_dim);
-
-	sol_for->sol.free = &sol_for_free;
-	if (sol_init(&sol_for->sol, bmap, dom, max) < 0)
-		goto error;
-	sol_for->fn = fn;
-	sol_for->user = user;
-	sol_for->sol.add = &sol_for_add_wrap;
-	sol_for->sol.add_empty = NULL;
-
-	isl_basic_set_free(dom);
-	return sol_for;
-error:
-	isl_basic_set_free(dom);
-	sol_free(&sol_for->sol);
-	return NULL;
-}
-
-static void sol_for_find_solutions(struct isl_sol_for *sol_for,
-	struct isl_tab *tab)
-{
-	find_solutions_main(&sol_for->sol, tab);
-}
-
-isl_stat isl_basic_map_foreach_lexopt(__isl_keep isl_basic_map *bmap, int max,
-	isl_stat (*fn)(__isl_take isl_basic_set *dom,
-		__isl_take isl_aff_list *list, void *user),
-	void *user)
-{
-	struct isl_sol_for *sol_for = NULL;
-
-	bmap = isl_basic_map_copy(bmap);
-	bmap = isl_basic_map_detect_equalities(bmap);
-	if (!bmap)
-		return isl_stat_error;
-
-	sol_for = sol_for_init(bmap, max, fn, user);
-	if (!sol_for)
-		goto error;
-
-	if (isl_basic_map_plain_is_empty(bmap))
-		/* nothing */;
-	else {
-		struct isl_tab *tab;
-		struct isl_context *context = sol_for->sol.context;
-		tab = tab_for_lexmin(bmap,
-				context->op->peek_basic_set(context), 1, max);
-		tab = context->op->detect_nonnegative_parameters(context, tab);
-		sol_for_find_solutions(sol_for, tab);
-		if (sol_for->sol.error)
-			goto error;
-	}
-
-	sol_free(&sol_for->sol);
-	isl_basic_map_free(bmap);
-	return isl_stat_ok;
-error:
-	sol_free(&sol_for->sol);
-	isl_basic_map_free(bmap);
-	return isl_stat_error;
-}
-
 /* Extract the subsequence of the sample value of "tab"
  * starting at "pos" and of length "len".
  */
@@ -5058,7 +4963,8 @@ static __isl_give isl_vec *extract_sample_sequence(struct isl_tab *tab,
 			int row;
 
 			row = tab->var[pos + i].index;
-			isl_int_set(v->el[i], tab->mat->row[row][1]);
+			isl_int_divexact(v->el[i], tab->mat->row[row][1],
+					tab->mat->row[row][0]);
 		}
 	}
 
@@ -5093,25 +4999,53 @@ static isl_bool region_is_trivial(struct isl_tab *tab, int pos,
 	return is_trivial;
 }
 
+/* Global internal data for isl_tab_basic_set_non_trivial_lexmin.
+ *
+ * "n_op" is the number of initial coordinates to optimize,
+ * as passed to isl_tab_basic_set_non_trivial_lexmin.
+ * "region" is the "n_region"-sized array of regions passed
+ * to isl_tab_basic_set_non_trivial_lexmin.
+ *
+ * "tab" is the tableau that corresponds to the ILP problem.
+ * "local" is an array of local data structure, one for each
+ * (potential) level of the backtracking procedure of
+ * isl_tab_basic_set_non_trivial_lexmin.
+ * "v" is a pre-allocated vector that can be used for adding
+ * constraints to the tableau.
+ *
+ * "sol" contains the best solution found so far.
+ * It is initialized to a vector of size zero.
+ */
+struct isl_lexmin_data {
+	int n_op;
+	int n_region;
+	struct isl_trivial_region *region;
+
+	struct isl_tab *tab;
+	struct isl_local_region *local;
+	isl_vec *v;
+
+	isl_vec *sol;
+};
+
 /* Return the index of the first trivial region, "n_region" if all regions
  * are non-trivial or -1 in case of error.
  */
-static int first_trivial_region(struct isl_tab *tab,
-	int n_region, struct isl_trivial_region *region)
+static int first_trivial_region(struct isl_lexmin_data *data)
 {
 	int i;
 
-	for (i = 0; i < n_region; ++i) {
+	for (i = 0; i < data->n_region; ++i) {
 		isl_bool trivial;
-		trivial = region_is_trivial(tab, region[i].pos,
-					region[i].trivial);
+		trivial = region_is_trivial(data->tab, data->region[i].pos,
+					data->region[i].trivial);
 		if (trivial < 0)
 			return -1;
 		if (trivial)
 			return i;
 	}
 
-	return n_region;
+	return data->n_region;
 }
 
 /* Check if the solution is optimal, i.e., whether the first
@@ -5181,22 +5115,13 @@ error:
 	return -1;
 }
 
-/* Global internal data for isl_tab_basic_set_non_trivial_lexmin.
- *
- * "v" is a pre-allocated vector that can be used for adding
- * constraints to the tableau.
- */
-struct isl_trivial_global {
-	isl_vec *v;
-};
-
 /* Fix triviality direction "dir" of the given region to zero.
  *
  * This function assumes that at least two more rows and at least
  * two more elements in the constraint array are available in the tableau.
  */
 static isl_stat fix_zero(struct isl_tab *tab, struct isl_trivial_region *region,
-	int dir, struct isl_trivial_global *data)
+	int dir, struct isl_lexmin_data *data)
 {
 	int len;
 
@@ -5222,7 +5147,7 @@ static isl_stat fix_zero(struct isl_tab *tab, struct isl_trivial_region *region,
  */
 static struct isl_tab *pos_neg(struct isl_tab *tab,
 	struct isl_trivial_region *region,
-	int side, struct isl_trivial_global *data)
+	int side, struct isl_lexmin_data *data)
 {
 	int len;
 
@@ -5254,8 +5179,10 @@ error:
  * "region" is the non-triviality region considered at this level.
  * "side" is the index of the current case at this level.
  * "n" is the number of triviality directions.
+ * "snap" is a snapshot of the tableau holding a state that needs
+ * to be satisfied by all subsequent cases.
  */
-struct isl_trivial {
+struct isl_local_region {
 	int update;
 	int n_zero;
 	int region;
@@ -5264,6 +5191,224 @@ struct isl_trivial {
 	struct isl_tab_undo *snap;
 };
 
+/* Initialize the global data structure "data" used while solving
+ * the ILP problem "bset".
+ */
+static isl_stat init_lexmin_data(struct isl_lexmin_data *data,
+	__isl_keep isl_basic_set *bset)
+{
+	isl_ctx *ctx;
+
+	ctx = isl_basic_set_get_ctx(bset);
+
+	data->tab = tab_for_lexmin(bset, NULL, 0, 0);
+	if (!data->tab)
+		return isl_stat_error;
+
+	data->v = isl_vec_alloc(ctx, 1 + data->tab->n_var);
+	if (!data->v)
+		return isl_stat_error;
+	data->local = isl_calloc_array(ctx, struct isl_local_region,
+					data->n_region);
+	if (data->n_region && !data->local)
+		return isl_stat_error;
+
+	data->sol = isl_vec_alloc(ctx, 0);
+
+	return isl_stat_ok;
+}
+
+/* Mark all outer levels as requiring a better solution
+ * in the next cases.
+ */
+static void update_outer_levels(struct isl_lexmin_data *data, int level)
+{
+	int i;
+
+	for (i = 0; i < level; ++i)
+		data->local[i].update = 1;
+}
+
+/* Initialize "local" to refer to region "region" and
+ * to initiate processing at this level.
+ */
+static void init_local_region(struct isl_local_region *local, int region,
+	struct isl_lexmin_data *data)
+{
+	local->n = isl_mat_rows(data->region[region].trivial);
+	local->region = region;
+	local->side = 0;
+	local->update = 0;
+	local->n_zero = 0;
+}
+
+/* What to do next after entering a level of the backtracking procedure.
+ *
+ * error: some error has occurred; abort
+ * done: an optimal solution has been found; stop search
+ * backtrack: backtrack to the previous level
+ * handle: add the constraints for the current level and
+ * 	move to the next level
+ */
+enum isl_next {
+	isl_next_error = -1,
+	isl_next_done,
+	isl_next_backtrack,
+	isl_next_handle,
+};
+
+/* Have all cases of the current region been considered?
+ * If there are n directions, then there are 2n cases.
+ *
+ * The constraints in the current tableau are imposed
+ * in all subsequent cases.  This means that if the current
+ * tableau is empty, then none of those cases should be considered
+ * anymore and all cases have effectively been considered.
+ */
+static int finished_all_cases(struct isl_local_region *local,
+	struct isl_lexmin_data *data)
+{
+	if (data->tab->empty)
+		return 1;
+	return local->side >= 2 * local->n;
+}
+
+/* Enter level "level" of the backtracking search and figure out
+ * what to do next.  "init" is set if the level was entered
+ * from a higher level and needs to be initialized.
+ * Otherwise, the level is entered as a result of backtracking and
+ * the tableau needs to be restored to a position that can
+ * be used for the next case at this level.
+ * The snapshot is assumed to have been saved in the previous case,
+ * before the constraints specific to that case were added.
+ *
+ * In the initialization case, the local region is initialized
+ * to point to the first violated region.
+ * If the constraints of all regions are satisfied by the current
+ * sample of the tableau, then tell the caller to continue looking
+ * for a better solution or to stop searching if an optimal solution
+ * has been found.
+ *
+ * If the tableau is empty or if all cases at the current level
+ * have been considered, then the caller needs to backtrack as well.
+ */
+static enum isl_next enter_level(int level, int init,
+	struct isl_lexmin_data *data)
+{
+	struct isl_local_region *local = &data->local[level];
+
+	if (init) {
+		int r;
+
+		data->tab = cut_to_integer_lexmin(data->tab, CUT_ONE);
+		if (!data->tab)
+			return isl_next_error;
+		if (data->tab->empty)
+			return isl_next_backtrack;
+		r = first_trivial_region(data);
+		if (r < 0)
+			return isl_next_error;
+		if (r == data->n_region) {
+			update_outer_levels(data, level);
+			isl_vec_free(data->sol);
+			data->sol = isl_tab_get_sample_value(data->tab);
+			if (!data->sol)
+				return isl_next_error;
+			if (is_optimal(data->sol, data->n_op))
+				return isl_next_done;
+			return isl_next_backtrack;
+		}
+		if (level >= data->n_region)
+			isl_die(isl_vec_get_ctx(data->v), isl_error_internal,
+				"nesting level too deep",
+				return isl_next_error);
+		init_local_region(local, r, data);
+		if (isl_tab_extend_cons(data->tab,
+				    2 * local->n + 2 * data->n_op) < 0)
+			return isl_next_error;
+	} else {
+		if (isl_tab_rollback(data->tab, local->snap) < 0)
+			return isl_next_error;
+	}
+
+	if (finished_all_cases(local, data))
+		return isl_next_backtrack;
+	return isl_next_handle;
+}
+
+/* If a solution has been found in the previous case at this level
+ * (marked by local->update being set), then add constraints
+ * that enforce a better solution in the present and all following cases.
+ * The constraints only need to be imposed once because they are
+ * included in the snapshot (taken in pick_side) that will be used in
+ * subsequent cases.
+ */
+static isl_stat better_next_side(struct isl_local_region *local,
+	struct isl_lexmin_data *data)
+{
+	if (!local->update)
+		return isl_stat_ok;
+
+	local->n_zero = force_better_solution(data->tab,
+				data->sol, data->n_op, local->n_zero);
+	if (local->n_zero < 0)
+		return isl_stat_error;
+
+	local->update = 0;
+
+	return isl_stat_ok;
+}
+
+/* Add constraints to data->tab that select the current case (local->side)
+ * at the current level.
+ *
+ * If the linear combinations v should not be zero, then the cases are
+ *	v_0 >= 1
+ *	v_0 <= -1
+ *	v_0 = 0 and v_1 >= 1
+ *	v_0 = 0 and v_1 <= -1
+ *	v_0 = 0 and v_1 = 0 and v_2 >= 1
+ *	v_0 = 0 and v_1 = 0 and v_2 <= -1
+ *	...
+ * in this order.
+ *
+ * A snapshot is taken after the equality constraint (if any) has been added
+ * such that the next case can start off from this position.
+ * The rollback to this position is performed in enter_level.
+ */
+static isl_stat pick_side(struct isl_local_region *local,
+	struct isl_lexmin_data *data)
+{
+	struct isl_trivial_region *region;
+	int side, base;
+
+	region = &data->region[local->region];
+	side = local->side;
+	base = 2 * (side/2);
+
+	if (side == base && base >= 2 &&
+	    fix_zero(data->tab, region, base / 2 - 1, data) < 0)
+		return isl_stat_error;
+
+	local->snap = isl_tab_snap(data->tab);
+	if (isl_tab_push_basis(data->tab) < 0)
+		return isl_stat_error;
+
+	data->tab = pos_neg(data->tab, region, side, data);
+	if (!data->tab)
+		return isl_stat_error;
+	return isl_stat_ok;
+}
+
+/* Free the memory associated to "data".
+ */
+static void clear_lexmin_data(struct isl_lexmin_data *data)
+{
+	free(data->local);
+	isl_vec_free(data->v);
+	isl_tab_free(data->tab);
+}
+
 /* Return the lexicographically smallest non-trivial solution of the
  * given ILP problem.
  *
@@ -5305,122 +5450,53 @@ __isl_give isl_vec *isl_tab_basic_set_non_trivial_lexmin(
 	struct isl_trivial_region *region,
 	int (*conflict)(int con, void *user), void *user)
 {
-	struct isl_trivial_global data = { 0 };
-	int i;
-	int r;
-	isl_ctx *ctx;
-	isl_vec *sol = NULL;
-	struct isl_tab *tab;
-	struct isl_trivial *triv = NULL;
+	struct isl_lexmin_data data = { n_op, n_region, region };
 	int level, init;
 
 	if (!bset)
 		return NULL;
 
-	ctx = isl_basic_set_get_ctx(bset);
-	sol = isl_vec_alloc(ctx, 0);
-
-	tab = tab_for_lexmin(bset, NULL, 0, 0);
-	if (!tab)
-		goto error;
-	tab->conflict = conflict;
-	tab->conflict_user = user;
-
-	data.v = isl_vec_alloc(ctx, 1 + tab->n_var);
-	triv = isl_calloc_array(ctx, struct isl_trivial, n_region);
-	if (!data.v || (n_region && !triv))
+	if (init_lexmin_data(&data, bset) < 0)
 		goto error;
+	data.tab->conflict = conflict;
+	data.tab->conflict_user = user;
 
 	level = 0;
 	init = 1;
 
 	while (level >= 0) {
-		int side, base;
+		enum isl_next next;
+		struct isl_local_region *local = &data.local[level];
 
-		if (init) {
-			tab = cut_to_integer_lexmin(tab, CUT_ONE);
-			if (!tab)
-				goto error;
-			if (tab->empty)
-				goto backtrack;
-			r = first_trivial_region(tab, n_region, region);
-			if (r < 0)
-				goto error;
-			if (r == n_region) {
-				for (i = 0; i < level; ++i)
-					triv[i].update = 1;
-				isl_vec_free(sol);
-				sol = isl_tab_get_sample_value(tab);
-				if (!sol)
-					goto error;
-				if (is_optimal(sol, n_op))
-					break;
-				goto backtrack;
-			}
-			if (level >= n_region)
-				isl_die(ctx, isl_error_internal,
-					"nesting level too deep", goto error);
-			triv[level].n = isl_mat_rows(region[r].trivial);
-			if (isl_tab_extend_cons(tab,
-					    2 * triv[level].n + 2 * n_op) < 0)
-				goto error;
-			triv[level].region = r;
-			triv[level].side = 0;
-			triv[level].update = 0;
-			triv[level].n_zero = 0;
-		}
-
-		r = triv[level].region;
-		side = triv[level].side;
-		base = 2 * (side/2);
-
-		if (side >= 2 * triv[level].n) {
-backtrack:
+		next = enter_level(level, init, &data);
+		if (next < 0)
+			goto error;
+		if (next == isl_next_done)
+			break;
+		if (next == isl_next_backtrack) {
 			level--;
 			init = 0;
-			if (level >= 0)
-				if (isl_tab_rollback(tab, triv[level].snap) < 0)
-					goto error;
 			continue;
 		}
 
-		if (triv[level].update) {
-			triv[level].n_zero = force_better_solution(tab, sol,
-						    n_op, triv[level].n_zero);
-			if (triv[level].n_zero < 0)
-				goto error;
-			triv[level].update = 0;
-		}
-
-		if (side == base && base >= 2 &&
-		    fix_zero(tab, &region[r], base / 2 - 1, &data) < 0)
+		if (better_next_side(local, &data) < 0)
 			goto error;
-
-		triv[level].snap = isl_tab_snap(tab);
-		if (isl_tab_push_basis(tab) < 0)
-			goto error;
-
-		tab = pos_neg(tab, &region[r], side, &data);
-		if (!tab)
+		if (pick_side(local, &data) < 0)
 			goto error;
 
-		triv[level].side++;
+		local->side++;
 		level++;
 		init = 1;
 	}
 
-	free(triv);
-	isl_vec_free(data.v);
-	isl_tab_free(tab);
+	clear_lexmin_data(&data);
 	isl_basic_set_free(bset);
 
-	return sol;
+	return data.sol;
 error:
-	free(triv);
-	isl_vec_free(data.v);
-	isl_tab_free(tab);
+	clear_lexmin_data(&data);
 	isl_basic_set_free(bset);
-	isl_vec_free(sol);
+	isl_vec_free(data.sol);
 	return NULL;
 }