X-Git-Url: http://review.tizen.org/git/?a=blobdiff_plain;f=isl_tab_pip.c;h=2592a285c0e179164254439f4b2c0e0d84bd12ed;hb=63fb8a7f484648c3caa25351c8c94ac2395ec563;hp=cf1321d33e182f94faeb42e8a9eb9fed0a737013;hpb=ca5ec125ce6db04ae2339031c1d865a48f3373bf;p=platform%2Fupstream%2Fisl.git

diff --git a/isl_tab_pip.c b/isl_tab_pip.c
index cf1321d..2592a28 100644
--- a/isl_tab_pip.c
+++ b/isl_tab_pip.c
@@ -2,7 +2,7 @@
  * Copyright 2008-2009 Katholieke Universiteit Leuven
  * Copyright 2010      INRIA Saclay
  *
- * Use of this software is governed by the GNU LGPLv2.1 license
+ * Use of this software is governed by the MIT license
  *
  * Written by Sven Verdoolaege, K.U.Leuven, Departement
  * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
@@ -16,6 +16,9 @@
 #include "isl_tab.h"
 #include "isl_sample.h"
 #include <isl_mat_private.h>
+#include <isl_aff_private.h>
+#include <isl_options_private.h>
+#include <isl_config.h>
 
 /*
  * The implementation of parametric integer linear programming in this file
@@ -99,6 +102,8 @@ struct isl_context_op {
 	void *(*save)(struct isl_context *context);
 	/* restore saved context */
 	void (*restore)(struct isl_context *context, void *);
+	/* discard saved context */
+	void (*discard)(void *);
 	/* invalidate context */
 	void (*invalidate)(struct isl_context *context);
 	/* free context */
@@ -114,6 +119,14 @@ struct isl_context_lex {
 	struct isl_tab *tab;
 };
 
+/* A stack (linked list) of solutions of subtrees of the search space.
+ *
+ * "M" describes the solution in terms of the dimensions of "dom".
+ * The number of columns of "M" is one more than the total number
+ * of dimensions of "dom".
+ *
+ * If "M" is NULL, then there is no solution on "dom".
+ */
 struct isl_partial_sol {
 	int level;
 	struct isl_basic_set *dom;
@@ -198,6 +211,7 @@ static void sol_push_sol(struct isl_sol *sol,
 	return;
 error:
 	isl_basic_set_free(dom);
+	isl_mat_free(M);
 	sol->error = 1;
 }
 
@@ -301,13 +315,26 @@ static void sol_pop(struct isl_sol *sol)
 			sol_pop_one(sol);
 		} else {
 			struct isl_basic_set *bset;
+			isl_mat *M;
+			unsigned n;
 
+			n = isl_basic_set_dim(partial->next->dom, isl_dim_div);
+			n -= n_div;
 			bset = sol_domain(sol);
-
 			isl_basic_set_free(partial->next->dom);
 			partial->next->dom = bset;
+			M = partial->next->M;
+			if (M) {
+				M = isl_mat_drop_cols(M, M->n_col - n, n);
+				partial->next->M = M;
+				if (!M)
+					goto error;
+			}
 			partial->next->level = sol->level;
 
+			if (!bset)
+				goto error;
+
 			sol->partial = partial->next;
 			isl_basic_set_free(partial->dom);
 			isl_mat_free(partial->M);
@@ -315,6 +342,9 @@ static void sol_pop(struct isl_sol *sol)
 		}
 	} else
 		sol_pop_one(sol);
+
+	if (0)
+error:		sol->error = 1;
 }
 
 static void sol_dec_level(struct isl_sol *sol)
@@ -420,7 +450,7 @@ static void sol_add(struct isl_sol *sol, struct isl_tab *tab)
 	struct isl_basic_set *bset = NULL;
 	struct isl_mat *mat = NULL;
 	unsigned off;
-	int row, i;
+	int row;
 	isl_int m;
 
 	if (sol->error || !tab)
@@ -428,6 +458,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);
 
@@ -554,18 +586,6 @@ static void sol_map_add_empty_wrap(struct isl_sol *sol,
 	sol_map_add_empty((struct isl_sol_map *)sol, bset);
 }
 
-/* Add bset to sol's empty, but only if we are actually collecting
- * the empty set.
- */
-static void sol_map_add_empty_if_needed(struct isl_sol_map *sol,
-	struct isl_basic_set *bset)
-{
-	if (sol->empty)
-		sol_map_add_empty(sol, bset);
-	else
-		isl_basic_set_free(bset);
-}
-
 /* Given a basic map "dom" that represents the context and an affine
  * matrix "M" that maps the dimensions of the context to the
  * output variables, construct a basic map with the same parameters
@@ -585,7 +605,6 @@ static void sol_map_add(struct isl_sol_map *sol,
 {
 	int i;
 	struct isl_basic_map *bmap = NULL;
-	isl_basic_set *context_bset;
 	unsigned n_eq;
 	unsigned n_ineq;
 	unsigned nparam;
@@ -602,7 +621,7 @@ static void sol_map_add(struct isl_sol_map *sol,
 	n_div = dom->n_div;
 	nparam = isl_basic_set_total_dim(dom) - n_div;
 	total = isl_map_dim(sol->map, isl_dim_all);
-	bmap = isl_basic_map_alloc_dim(isl_map_get_dim(sol->map),
+	bmap = isl_basic_map_alloc_space(isl_map_get_space(sol->map),
 					n_div, n_eq, 2 * n_div + n_ineq);
 	if (!bmap)
 		goto error;
@@ -649,10 +668,10 @@ static void sol_map_add(struct isl_sol_map *sol,
 	bmap = isl_basic_map_finalize(bmap);
 	sol->map = isl_map_grow(sol->map, 1);
 	sol->map = isl_map_add_basic_map(sol->map, bmap);
-	if (!sol->map)
-		goto error;
 	isl_basic_set_free(dom);
 	isl_mat_free(M);
+	if (!sol->map)
+		sol->sol.error = 1;
 	return;
 error:
 	isl_basic_set_free(dom);
@@ -753,6 +772,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
  *
@@ -773,8 +816,8 @@ 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);
 	isl_seq_neg(div->el + 1, div->el + 1, div->size - 1);
+	normalize_div(div);
 	isl_seq_fdiv_r(div->el + 1, div->el + 1, div->el[0], div->size - 1);
 
 	return div;
@@ -801,7 +844,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;
@@ -839,7 +882,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
  *
@@ -870,7 +913,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;
@@ -1117,6 +1161,7 @@ static int first_neg(struct isl_tab *tab)
  * is satisfied.  This function is not called from the current code
  * but is useful during debugging.
  */
+static void check_lexpos(struct isl_tab *tab) __attribute__ ((unused));
 static void check_lexpos(struct isl_tab *tab)
 {
 	unsigned off = 2 + tab->M;
@@ -1149,6 +1194,50 @@ static void check_lexpos(struct isl_tab *tab)
 	}
 }
 
+/* Report to the caller that the given constraint is part of an encountered
+ * conflict.
+ */
+static int report_conflicting_constraint(struct isl_tab *tab, int con)
+{
+	return tab->conflict(con, tab->conflict_user);
+}
+
+/* Given a conflicting row in the tableau, report all constraints
+ * involved in the row to the caller.  That is, the row itself
+ * (if it represents a constraint) and all constraint columns with
+ * non-zero (and therefore negative) coefficients.
+ */
+static int report_conflict(struct isl_tab *tab, int row)
+{
+	int j;
+	isl_int *tr;
+
+	if (!tab->conflict)
+		return 0;
+
+	if (tab->row_var[row] < 0 &&
+	    report_conflicting_constraint(tab, ~tab->row_var[row]) < 0)
+		return -1;
+
+	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))
+			continue;
+
+		if (!isl_int_is_neg(tr[j]))
+			continue;
+
+		if (tab->col_var[j] < 0 &&
+		    report_conflicting_constraint(tab, ~tab->col_var[j]) < 0)
+			return -1;
+	}
+
+	return 0;
+}
+
 /* 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
@@ -1167,6 +1256,8 @@ static int restore_lexmin(struct isl_tab *tab)
 	while ((row = first_neg(tab)) != -1) {
 		col = lexmin_pivot_col(tab, row);
 		if (col >= tab->n_col) {
+			if (report_conflict(tab, row) < 0)
+				return -1;
 			if (isl_tab_mark_empty(tab) < 0)
 				return -1;
 			return 0;
@@ -1287,80 +1378,77 @@ static int is_constant(struct isl_tab *tab, int row)
  * In the end we try to use one of the two constraints to eliminate
  * a column.
  */
-static struct isl_tab *add_lexmin_eq(struct isl_tab *tab, isl_int *eq) WARN_UNUSED;
-static struct isl_tab *add_lexmin_eq(struct isl_tab *tab, isl_int *eq)
+static int add_lexmin_eq(struct isl_tab *tab, isl_int *eq) WARN_UNUSED;
+static int add_lexmin_eq(struct isl_tab *tab, isl_int *eq)
 {
 	int r1, r2;
 	int row;
 	struct isl_tab_undo *snap;
 
 	if (!tab)
-		return NULL;
+		return -1;
 	snap = isl_tab_snap(tab);
 	r1 = isl_tab_add_row(tab, eq);
 	if (r1 < 0)
-		goto error;
+		return -1;
 	tab->con[r1].is_nonneg = 1;
 	if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r1]) < 0)
-		goto error;
+		return -1;
 
 	row = tab->con[r1].index;
 	if (is_constant(tab, row)) {
 		if (!isl_int_is_zero(tab->mat->row[row][1]) ||
 		    (tab->M && !isl_int_is_zero(tab->mat->row[row][2]))) {
 			if (isl_tab_mark_empty(tab) < 0)
-				goto error;
-			return tab;
+				return -1;
+			return 0;
 		}
 		if (isl_tab_rollback(tab, snap) < 0)
-			goto error;
-		return tab;
+			return -1;
+		return 0;
 	}
 
 	if (restore_lexmin(tab) < 0)
-		goto error;
+		return -1;
 	if (tab->empty)
-		return tab;
+		return 0;
 
 	isl_seq_neg(eq, eq, 1 + tab->n_var);
 
 	r2 = isl_tab_add_row(tab, eq);
 	if (r2 < 0)
-		goto error;
+		return -1;
 	tab->con[r2].is_nonneg = 1;
 	if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r2]) < 0)
-		goto error;
+		return -1;
 
 	if (restore_lexmin(tab) < 0)
-		goto error;
+		return -1;
 	if (tab->empty)
-		return tab;
+		return 0;
 
 	if (!tab->con[r1].is_row) {
 		if (isl_tab_kill_col(tab, tab->con[r1].index) < 0)
-			goto error;
+			return -1;
 	} else if (!tab->con[r2].is_row) {
 		if (isl_tab_kill_col(tab, tab->con[r2].index) < 0)
-			goto error;
+			return -1;
 	}
 
 	if (tab->bmap) {
 		tab->bmap = isl_basic_map_add_ineq(tab->bmap, eq);
 		if (isl_tab_push(tab, isl_tab_undo_bmap_ineq) < 0)
-			goto error;
+			return -1;
 		isl_seq_neg(eq, eq, 1 + tab->n_var);
 		tab->bmap = isl_basic_map_add_ineq(tab->bmap, eq);
 		isl_seq_neg(eq, eq, 1 + tab->n_var);
 		if (isl_tab_push(tab, isl_tab_undo_bmap_ineq) < 0)
-			goto error;
+			return -1;
 		if (!tab->bmap)
-			goto error;
+			return -1;
 	}
 
-	return tab;
-error:
-	isl_tab_free(tab);
-	return NULL;
+	return 0;
 }
 
 /* Add an inequality to the tableau, resolving violations using
@@ -1569,6 +1657,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.
@@ -1580,8 +1671,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;
@@ -1603,6 +1698,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;
@@ -1685,7 +1782,6 @@ static int sample_is_finite(struct isl_tab *tab)
 static struct isl_tab *check_integer_feasible(struct isl_tab *tab)
 {
 	struct isl_tab_undo *snap;
-	int feasible;
 
 	if (!tab)
 		return NULL;
@@ -1694,7 +1790,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;
 
@@ -1888,6 +1984,7 @@ static int add_parametric_cut(struct isl_tab *tab, int row,
 
 	n = tab->n_div;
 	d = context->op->get_div(context, tab, div);
+	isl_vec_free(div);
 	if (d < 0)
 		return -1;
 
@@ -1953,8 +2050,6 @@ static int add_parametric_cut(struct isl_tab *tab, int row,
 	if (tab->row_sign)
 		tab->row_sign[tab->con[r].index] = isl_tab_row_neg;
 
-	isl_vec_free(div);
-
 	row = tab->con[r].index;
 
 	if (d >= n && context->op->detect_equalities(context, tab) < 0)
@@ -2139,24 +2234,14 @@ static struct isl_tab *context_lex_peek_tab(struct isl_context *context)
 	return clex->tab;
 }
 
-static void context_lex_extend(struct isl_context *context, int n)
-{
-	struct isl_context_lex *clex = (struct isl_context_lex *)context;
-	if (!clex->tab)
-		return;
-	if (isl_tab_extend_cons(clex->tab, n) >= 0)
-		return;
-	isl_tab_free(clex->tab);
-	clex->tab = NULL;
-}
-
 static void context_lex_add_eq(struct isl_context *context, isl_int *eq,
 		int check, int update)
 {
 	struct isl_context_lex *clex = (struct isl_context_lex *)context;
 	if (isl_tab_extend_cons(clex->tab, 2) < 0)
 		goto error;
-	clex->tab = add_lexmin_eq(clex->tab, eq);
+	if (add_lexmin_eq(clex->tab, eq) < 0)
+		goto error;
 	if (check) {
 		int v = tab_has_valid_sample(clex->tab, eq, 1);
 		if (v < 0)
@@ -2359,6 +2444,10 @@ static void context_lex_restore(struct isl_context *context, void *save)
 	}
 }
 
+static void context_lex_discard(void *save)
+{
+}
+
 static int context_lex_is_ok(struct isl_context *context)
 {
 	struct isl_context_lex *clex = (struct isl_context_lex *)context;
@@ -2478,6 +2567,7 @@ struct isl_context_op isl_context_lex_op = {
 	context_lex_is_ok,
 	context_lex_save,
 	context_lex_restore,
+	context_lex_discard,
 	context_lex_invalidate,
 	context_lex_free,
 };
@@ -2486,7 +2576,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);
@@ -2527,6 +2616,14 @@ error:
 	return NULL;
 }
 
+/* Representation of the context when using generalized basis reduction.
+ *
+ * "shifted" contains the offsets of the unit hypercubes that lie inside the
+ * context.  Any rational point in "shifted" can therefore be rounded
+ * up to an integer point in the context.
+ * If the context is constrained by any equality, then "shifted" is not used
+ * as it would be empty.
+ */
 struct isl_context_gbr {
 	struct isl_context context;
 	struct isl_tab *tab;
@@ -2585,7 +2682,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]);
@@ -2658,7 +2755,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)
@@ -2734,8 +2832,6 @@ error:
 
 static struct isl_tab *add_gbr_eq(struct isl_tab *tab, isl_int *eq)
 {
-	int r;
-
 	if (!tab)
 		return NULL;
 
@@ -2751,6 +2847,15 @@ error:
 	return NULL;
 }
 
+/* Add the equality described by "eq" to the context.
+ * If "check" is set, then we check if the context is empty after
+ * adding the equality.
+ * If "update" is set, then we check if the samples are still valid.
+ *
+ * We do not explicitly add shifted copies of the equality to
+ * cgbr->shifted since they would conflict with each other.
+ * Instead, we directly mark cgbr->shifted empty.
+ */
 static void context_gbr_add_eq(struct isl_context *context, isl_int *eq,
 		int check, int update)
 {
@@ -2758,6 +2863,11 @@ static void context_gbr_add_eq(struct isl_context *context, isl_int *eq,
 
 	cgbr->tab = add_gbr_eq(cgbr->tab, eq);
 
+	if (cgbr->shifted && !cgbr->shifted->empty && use_shifted(cgbr)) {
+		if (isl_tab_mark_empty(cgbr->shifted) < 0)
+			goto error;
+	}
+
 	if (cgbr->cone && cgbr->cone->n_col != cgbr->cone->n_dead) {
 		if (isl_tab_extend_cons(cgbr->cone, 2) < 0)
 			goto error;
@@ -2922,7 +3032,6 @@ static int last_non_zero_var_col(struct isl_tab *tab, isl_int *p)
 {
 	int i;
 	int col;
-	unsigned dim = tab->n_var - tab->n_param - tab->n_div;
 
 	if (tab->n_var == 0)
 		return -1;
@@ -3014,8 +3123,6 @@ static int context_gbr_detect_equalities(struct isl_context *context,
 {
 	struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
 	struct isl_ctx *ctx;
-	int i;
-	enum isl_lp_result res;
 	unsigned n_ineq;
 
 	ctx = cgbr->tab->mat->ctx;
@@ -3025,7 +3132,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)
@@ -3033,7 +3141,9 @@ static int context_gbr_detect_equalities(struct isl_context *context,
 
 	n_ineq = cgbr->tab->bmap->n_ineq;
 	cgbr->tab = isl_tab_detect_equalities(cgbr->tab, cgbr->cone);
-	if (cgbr->tab && cgbr->tab->bmap->n_ineq > n_ineq)
+	if (!cgbr->tab)
+		return -1;
+	if (cgbr->tab->bmap->n_ineq > n_ineq)
 		propagate_equalities(cgbr, tab, n_ineq);
 
 	return 0;
@@ -3062,8 +3172,8 @@ static int context_gbr_add_div(struct isl_context *context, struct isl_vec *div)
 		if (isl_tab_allocate_var(cgbr->cone) <0)
 			return -1;
 
-		cgbr->cone->bmap = isl_basic_map_extend_dim(cgbr->cone->bmap,
-			isl_basic_map_get_dim(cgbr->cone->bmap), 1, 0, 2);
+		cgbr->cone->bmap = isl_basic_map_extend_space(cgbr->cone->bmap,
+			isl_basic_map_get_space(cgbr->cone->bmap), 1, 0, 2);
 		k = isl_basic_map_alloc_div(cgbr->cone->bmap);
 		if (k < 0)
 			return -1;
@@ -3170,6 +3280,12 @@ error:
 	cgbr->tab = NULL;
 }
 
+static void context_gbr_discard(void *save)
+{
+	struct isl_gbr_tab_undo *snap = (struct isl_gbr_tab_undo *)save;
+	free(snap);
+}
+
 static int context_gbr_is_ok(struct isl_context *context)
 {
 	struct isl_context_gbr *cgbr = (struct isl_context_gbr *)context;
@@ -3208,6 +3324,7 @@ struct isl_context_op isl_context_gbr_op = {
 	context_gbr_is_ok,
 	context_gbr_save,
 	context_gbr_restore,
+	context_gbr_discard,
 	context_gbr_invalidate,
 	context_gbr_free,
 };
@@ -3227,13 +3344,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;
@@ -3260,7 +3374,7 @@ static struct isl_context *isl_context_alloc(struct isl_basic_set *dom)
  * a minimization problem, which means that the variables in the
  * tableau have value "M - x" rather than "M + x".
  */
-static struct isl_sol_map *sol_map_init(struct isl_basic_map *bmap,
+static struct isl_sol *sol_map_init(struct isl_basic_map *bmap,
 	struct isl_basic_set *dom, int track_empty, int max)
 {
 	struct isl_sol_map *sol_map = NULL;
@@ -3280,7 +3394,7 @@ static struct isl_sol_map *sol_map_init(struct isl_basic_map *bmap,
 	sol_map->sol.add = &sol_map_add_wrap;
 	sol_map->sol.add_empty = track_empty ? &sol_map_add_empty_wrap : NULL;
 	sol_map->sol.free = &sol_map_free_wrap;
-	sol_map->map = isl_map_alloc_dim(isl_basic_map_get_dim(bmap), 1,
+	sol_map->map = isl_map_alloc_space(isl_basic_map_get_space(bmap), 1,
 					    ISL_MAP_DISJOINT);
 	if (!sol_map->map)
 		goto error;
@@ -3290,14 +3404,14 @@ static struct isl_sol_map *sol_map_init(struct isl_basic_map *bmap,
 		goto error;
 
 	if (track_empty) {
-		sol_map->empty = isl_set_alloc_dim(isl_basic_set_get_dim(dom),
+		sol_map->empty = isl_set_alloc_space(isl_basic_set_get_space(dom),
 							1, ISL_SET_DISJOINT);
 		if (!sol_map->empty)
 			goto error;
 	}
 
 	isl_basic_set_free(dom);
-	return sol_map;
+	return &sol_map->sol;
 error:
 	isl_basic_set_free(dom);
 	sol_map_free(sol_map);
@@ -3509,6 +3623,8 @@ static void find_in_pos(struct isl_sol *sol, struct isl_tab *tab, isl_int *ineq)
 
 	if (!sol->error)
 		sol->context->op->restore(sol->context, saved);
+	else
+		sol->context->op->discard(saved);
 	return;
 error:
 	sol->error = 1;
@@ -3760,6 +3876,24 @@ error:
 	sol->error = 1;
 }
 
+/* Does "sol" contain a pair of partial solutions that could potentially
+ * be merged?
+ *
+ * We currently only check that "sol" is not in an error state
+ * and that there are at least two partial solutions of which the final two
+ * are defined at the same level.
+ */
+static int sol_has_mergeable_solutions(struct isl_sol *sol)
+{
+	if (sol->error)
+		return 0;
+	if (!sol->partial)
+		return 0;
+	if (!sol->partial->next)
+		return 0;
+	return sol->partial->level == sol->partial->next->level;
+}
+
 /* Compute the lexicographic minimum of the set represented by the main
  * tableau "tab" within the context "sol->context_tab".
  *
@@ -3770,10 +3904,20 @@ error:
  * corresponding rows may not be marked as being non-negative.
  * In parts of the context where the added equality does not hold,
  * the main tableau is marked as being empty.
+ *
+ * Before we embark on the actual computation, we save a copy
+ * of the context.  When we return, we check if there are any
+ * partial solutions that can potentially be merged.  If so,
+ * we perform a rollback to the initial state of the context.
+ * The merging of partial solutions happens inside calls to
+ * sol_dec_level that are pushed onto the undo stack of the context.
+ * If there are no partial solutions that can potentially be merged
+ * then the rollback is skipped as it would just be wasted effort.
  */
 static void find_solutions_main(struct isl_sol *sol, struct isl_tab *tab)
 {
 	int row;
+	void *saved;
 
 	if (!tab)
 		goto error;
@@ -3823,8 +3967,15 @@ static void find_solutions_main(struct isl_sol *sol, struct isl_tab *tab)
 		row = tab->n_redundant - 1;
 	}
 
+	saved = sol->context->op->save(sol->context);
+
 	find_solutions(sol, tab);
 
+	if (sol_has_mergeable_solutions(sol))
+		sol->context->op->restore(sol->context, saved);
+	else
+		sol->context->op->discard(saved);
+
 	sol->level = 0;
 	sol_pop(sol);
 
@@ -3834,12 +3985,6 @@ error:
 	sol->error = 1;
 }
 
-static void sol_map_find_solutions(struct isl_sol_map *sol_map,
-	struct isl_tab *tab)
-{
-	find_solutions_main(&sol_map->sol, tab);
-}
-
 /* Check if integer division "div" of "dom" also occurs in "bmap".
  * If so, return its position within the divs.
  * If not, return -1.
@@ -3848,8 +3993,8 @@ static int find_context_div(struct isl_basic_map *bmap,
 	struct isl_basic_set *dom, unsigned div)
 {
 	int i;
-	unsigned b_dim = isl_dim_total(bmap->dim);
-	unsigned d_dim = isl_dim_total(dom->dim);
+	unsigned b_dim = isl_space_dim(bmap->dim, isl_dim_all);
+	unsigned d_dim = isl_space_dim(dom->dim, isl_dim_all);
 
 	if (isl_int_is_zero(dom->div[div][0]))
 		return -1;
@@ -3894,7 +4039,7 @@ static struct isl_basic_map *align_context_divs(struct isl_basic_map *bmap,
 			common++;
 	other = bmap->n_div - common;
 	if (dom->n_div - common > 0) {
-		bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim),
+		bmap = isl_basic_map_extend_space(bmap, isl_space_copy(bmap->dim),
 				dom->n_div - common, 0, 0);
 		if (!bmap)
 			return NULL;
@@ -3923,48 +4068,72 @@ error:
  * because they will be added one by one in the given order
  * during the construction of the solution map.
  */
-static __isl_give isl_map *basic_map_partial_lexopt_base(
+static struct isl_sol *basic_map_partial_lexopt_base(
 	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
-	__isl_give isl_set **empty, int max)
+	__isl_give isl_set **empty, int max,
+	struct isl_sol *(*init)(__isl_keep isl_basic_map *bmap,
+		    __isl_take isl_basic_set *dom, int track_empty, int max))
 {
-	isl_map *result = NULL;
 	struct isl_tab *tab;
-	struct isl_sol_map *sol_map = NULL;
+	struct isl_sol *sol = NULL;
 	struct isl_context *context;
 
 	if (dom->n_div) {
 		dom = isl_basic_set_order_divs(dom);
 		bmap = align_context_divs(bmap, dom);
 	}
-	sol_map = sol_map_init(bmap, dom, !!empty, max);
-	if (!sol_map)
+	sol = init(bmap, dom, !!empty, max);
+	if (!sol)
 		goto error;
 
-	context = sol_map->sol.context;
-	if (isl_basic_set_fast_is_empty(context->op->peek_basic_set(context)))
+	context = sol->context;
+	if (isl_basic_set_plain_is_empty(context->op->peek_basic_set(context)))
 		/* nothing */;
-	else if (isl_basic_map_fast_is_empty(bmap))
-		sol_map_add_empty_if_needed(sol_map,
+	else if (isl_basic_map_plain_is_empty(bmap)) {
+		if (sol->add_empty)
+			sol->add_empty(sol,
 		    isl_basic_set_copy(context->op->peek_basic_set(context)));
-	else {
+	} else {
 		tab = tab_for_lexmin(bmap,
 				    context->op->peek_basic_set(context), 1, max);
 		tab = context->op->detect_nonnegative_parameters(context, tab);
-		sol_map_find_solutions(sol_map, tab);
+		find_solutions_main(sol, tab);
 	}
-	if (sol_map->sol.error)
+	if (sol->error)
 		goto error;
 
+	isl_basic_map_free(bmap);
+	return sol;
+error:
+	sol_free(sol);
+	isl_basic_map_free(bmap);
+	return NULL;
+}
+
+/* Base case of isl_tab_basic_map_partial_lexopt, after removing
+ * some obvious symmetries.
+ *
+ * We call basic_map_partial_lexopt_base and extract the results.
+ */
+static __isl_give isl_map *basic_map_partial_lexopt_base_map(
+	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
+	__isl_give isl_set **empty, int max)
+{
+	isl_map *result = NULL;
+	struct isl_sol *sol;
+	struct isl_sol_map *sol_map;
+
+	sol = basic_map_partial_lexopt_base(bmap, dom, empty, max,
+					    &sol_map_init);
+	if (!sol)
+		return NULL;
+	sol_map = (struct isl_sol_map *) sol;
+
 	result = isl_map_copy(sol_map->map);
 	if (empty)
 		*empty = isl_set_copy(sol_map->empty);
 	sol_free(&sol_map->sol);
-	isl_basic_map_free(bmap);
 	return result;
-error:
-	sol_free(&sol_map->sol);
-	isl_basic_map_free(bmap);
-	return NULL;
 }
 
 /* Structure used during detection of parallel constraints.
@@ -4052,6 +4221,43 @@ error:
 	return -1;
 }
 
+/* Given a set of upper bounds in "var", add constraints to "bset"
+ * that make the i-th bound smallest.
+ *
+ * In particular, if there are n bounds b_i, then add the constraints
+ *
+ *	b_i <= b_j	for j > i
+ *	b_i <  b_j	for j < i
+ */
+static __isl_give isl_basic_set *select_minimum(__isl_take isl_basic_set *bset,
+	__isl_keep isl_mat *var, int i)
+{
+	isl_ctx *ctx;
+	int j, k;
+
+	ctx = isl_mat_get_ctx(var);
+
+	for (j = 0; j < var->n_row; ++j) {
+		if (j == i)
+			continue;
+		k = isl_basic_set_alloc_inequality(bset);
+		if (k < 0)
+			goto error;
+		isl_seq_combine(bset->ineq[k], ctx->one, var->row[j],
+				ctx->negone, var->row[i], var->n_col);
+		isl_int_set_si(bset->ineq[k][var->n_col], 0);
+		if (j < i)
+			isl_int_sub_ui(bset->ineq[k][0], bset->ineq[k][0], 1);
+	}
+
+	bset = isl_basic_set_finalize(bset);
+
+	return bset;
+error:
+	isl_basic_set_free(bset);
+	return NULL;
+}
+
 /* Given a set of upper bounds on the last "input" variable m,
  * construct a set that assigns the minimal upper bound to m, i.e.,
  * construct a set that divides the space into cells where one
@@ -4065,10 +4271,10 @@ error:
  *	b_i <= b_j	for j > i
  *	b_i <  b_j	for j < i
  */
-static __isl_give isl_set *set_minimum(__isl_take isl_dim *dim,
+static __isl_give isl_set *set_minimum(__isl_take isl_space *dim,
 	__isl_take isl_mat *var)
 {
-	int i, j, k;
+	int i, k;
 	isl_basic_set *bset = NULL;
 	isl_ctx *ctx;
 	isl_set *set = NULL;
@@ -4076,43 +4282,29 @@ static __isl_give isl_set *set_minimum(__isl_take isl_dim *dim,
 	if (!dim || !var)
 		goto error;
 
-	ctx = isl_dim_get_ctx(dim);
-	set = isl_set_alloc_dim(isl_dim_copy(dim),
+	ctx = isl_space_get_ctx(dim);
+	set = isl_set_alloc_space(isl_space_copy(dim),
 				var->n_row, ISL_SET_DISJOINT);
 
 	for (i = 0; i < var->n_row; ++i) {
-		bset = isl_basic_set_alloc_dim(isl_dim_copy(dim), 0,
+		bset = isl_basic_set_alloc_space(isl_space_copy(dim), 0,
 					       1, var->n_row - 1);
 		k = isl_basic_set_alloc_equality(bset);
 		if (k < 0)
 			goto error;
 		isl_seq_cpy(bset->eq[k], var->row[i], var->n_col);
 		isl_int_set_si(bset->eq[k][var->n_col], -1);
-		for (j = 0; j < var->n_row; ++j) {
-			if (j == i)
-				continue;
-			k = isl_basic_set_alloc_inequality(bset);
-			if (k < 0)
-				goto error;
-			isl_seq_combine(bset->ineq[k], ctx->one, var->row[j],
-					ctx->negone, var->row[i],
-					var->n_col);
-			isl_int_set_si(bset->ineq[k][var->n_col], 0);
-			if (j < i)
-				isl_int_sub_ui(bset->ineq[k][0],
-					       bset->ineq[k][0], 1);
-		}
-		bset = isl_basic_set_finalize(bset);
+		bset = select_minimum(bset, var, i);
 		set = isl_set_add_basic_set(set, bset);
 	}
 
-	isl_dim_free(dim);
+	isl_space_free(dim);
 	isl_mat_free(var);
 	return set;
 error:
 	isl_basic_set_free(bset);
 	isl_set_free(set);
-	isl_dim_free(dim);
+	isl_space_free(dim);
 	isl_mat_free(var);
 	return NULL;
 }
@@ -4126,7 +4318,7 @@ error:
  * an upper bound that is different from the upper bounds on which it
  * is defined.
  */
-static int need_split_map(__isl_keep isl_basic_map *bmap,
+static int need_split_basic_map(__isl_keep isl_basic_map *bmap,
 	__isl_keep isl_mat *cst)
 {
 	int i, j;
@@ -4163,10 +4355,33 @@ static int need_split_map(__isl_keep isl_basic_map *bmap,
 	return 0;
 }
 
-static int need_split_set(__isl_keep isl_basic_set *bset,
+/* Given that the last set variable of "bset" represents the minimum
+ * of the bounds in "cst", check whether we need to split the domain
+ * based on which bound attains the minimum.
+ *
+ * We simply call need_split_basic_map here.  This is safe because
+ * the position of the minimum is computed from "cst" and not
+ * from "bmap".
+ */
+static int need_split_basic_set(__isl_keep isl_basic_set *bset,
 	__isl_keep isl_mat *cst)
 {
-	return need_split_map((isl_basic_map *)bset, cst);
+	return need_split_basic_map((isl_basic_map *)bset, cst);
+}
+
+/* Given that the last set variable of "set" represents the minimum
+ * of the bounds in "cst", check whether we need to split the domain
+ * based on which bound attains the minimum.
+ */
+static int need_split_set(__isl_keep isl_set *set, __isl_keep isl_mat *cst)
+{
+	int i;
+
+	for (i = 0; i < set->n; ++i)
+		if (need_split_basic_set(set->p[i], cst))
+			return 1;
+
+	return 0;
 }
 
 /* Given a set of which the last set variable is the minimum
@@ -4187,22 +4402,22 @@ static __isl_give isl_set *split(__isl_take isl_set *empty,
 {
 	int n_in;
 	int i;
-	isl_dim *dim;
+	isl_space *dim;
 	isl_set *res;
 
 	if (!empty || !min_expr || !cst)
 		goto error;
 
 	n_in = isl_set_dim(empty, isl_dim_set);
-	dim = isl_set_get_dim(empty);
-	dim = isl_dim_drop(dim, isl_dim_set, n_in - 1, 1);
+	dim = isl_set_get_space(empty);
+	dim = isl_space_drop_dims(dim, isl_dim_set, n_in - 1, 1);
 	res = isl_set_empty(dim);
 
 	for (i = 0; i < empty->n; ++i) {
 		isl_set *set;
 
 		set = isl_set_from_basic_set(isl_basic_set_copy(empty->p[i]));
-		if (need_split_set(empty->p[i], cst))
+		if (need_split_basic_set(empty->p[i], cst))
 			set = isl_set_intersect(set, isl_set_copy(min_expr));
 		set = isl_set_remove_dims(set, isl_dim_set, n_in - 1, 1);
 
@@ -4233,22 +4448,22 @@ static __isl_give isl_map *split_domain(__isl_take isl_map *opt,
 {
 	int n_in;
 	int i;
-	isl_dim *dim;
+	isl_space *dim;
 	isl_map *res;
 
 	if (!opt || !min_expr || !cst)
 		goto error;
 
 	n_in = isl_map_dim(opt, isl_dim_in);
-	dim = isl_map_get_dim(opt);
-	dim = isl_dim_drop(dim, isl_dim_in, n_in - 1, 1);
+	dim = isl_map_get_space(opt);
+	dim = isl_space_drop_dims(dim, isl_dim_in, n_in - 1, 1);
 	res = isl_map_empty(dim);
 
 	for (i = 0; i < opt->n; ++i) {
 		isl_map *map;
 
 		map = isl_map_from_basic_map(isl_basic_map_copy(opt->p[i]));
-		if (need_split_map(opt->p[i], cst))
+		if (need_split_basic_map(opt->p[i], cst))
 			map = isl_map_intersect_domain(map,
 						       isl_set_copy(min_expr));
 		map = isl_map_remove_dims(map, isl_dim_in, n_in - 1, 1);
@@ -4271,25 +4486,66 @@ static __isl_give isl_map *basic_map_partial_lexopt(
 	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
 	__isl_give isl_set **empty, int max);
 
-/* Given a basic map with at least two parallel constraints (as found
- * by the function parallel_constraints), first look for more constraints
- * parallel to the two constraint and replace the found list of parallel
- * constraints by a single constraint with as "input" part the minimum
- * of the input parts of the list of constraints.  Then, recursively call
- * basic_map_partial_lexopt (possibly finding more parallel constraints)
- * and plug in the definition of the minimum in the result.
- *
- * More specifically, given a set of constraints
- *
- *	a x + b_i(p) >= 0
- *
- * Replace this set by a single constraint
- *
- *	a x + u >= 0
- *
- * with u a new parameter with constraints
- *
- *	u <= b_i(p)
+union isl_lex_res {
+	void *p;
+	isl_map *map;
+	isl_pw_multi_aff *pma;
+};
+
+/* This function is called from basic_map_partial_lexopt_symm.
+ * The last variable of "bmap" and "dom" corresponds to the minimum
+ * of the bounds in "cst".  "map_space" is the space of the original
+ * input relation (of basic_map_partial_lexopt_symm) and "set_space"
+ * is the space of the original domain.
+ *
+ * We recursively call basic_map_partial_lexopt and then plug in
+ * the definition of the minimum in the result.
+ */
+static __isl_give union isl_lex_res basic_map_partial_lexopt_symm_map_core(
+	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
+	__isl_give isl_set **empty, int max, __isl_take isl_mat *cst,
+	__isl_take isl_space *map_space, __isl_take isl_space *set_space)
+{
+	isl_map *opt;
+	isl_set *min_expr;
+	union isl_lex_res res;
+
+	min_expr = set_minimum(isl_basic_set_get_space(dom), isl_mat_copy(cst));
+
+	opt = basic_map_partial_lexopt(bmap, dom, empty, max);
+
+	if (empty) {
+		*empty = split(*empty,
+			       isl_set_copy(min_expr), isl_mat_copy(cst));
+		*empty = isl_set_reset_space(*empty, set_space);
+	}
+
+	opt = split_domain(opt, min_expr, cst);
+	opt = isl_map_reset_space(opt, map_space);
+
+	res.map = opt;
+	return res;
+}
+
+/* Given a basic map with at least two parallel constraints (as found
+ * by the function parallel_constraints), first look for more constraints
+ * parallel to the two constraint and replace the found list of parallel
+ * constraints by a single constraint with as "input" part the minimum
+ * of the input parts of the list of constraints.  Then, recursively call
+ * basic_map_partial_lexopt (possibly finding more parallel constraints)
+ * and plug in the definition of the minimum in the result.
+ *
+ * More specifically, given a set of constraints
+ *
+ *	a x + b_i(p) >= 0
+ *
+ * Replace this set by a single constraint
+ *
+ *	a x + u >= 0
+ *
+ * with u a new parameter with constraints
+ *
+ *	u <= b_i(p)
  *
  * Any solution to the new system is also a solution for the original system
  * since
@@ -4299,9 +4555,15 @@ static __isl_give isl_map *basic_map_partial_lexopt(
  * Moreover, m = min_i(b_i(p)) satisfies the constraints on u and can
  * therefore be plugged into the solution.
  */
-static __isl_give isl_map *basic_map_partial_lexopt_symm(
+static union isl_lex_res basic_map_partial_lexopt_symm(
 	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
-	__isl_give isl_set **empty, int max, int first, int second)
+	__isl_give isl_set **empty, int max, int first, int second,
+	__isl_give union isl_lex_res (*core)(__isl_take isl_basic_map *bmap,
+					    __isl_take isl_basic_set *dom,
+					    __isl_give isl_set **empty,
+					    int max, __isl_take isl_mat *cst,
+					    __isl_take isl_space *map_space,
+					    __isl_take isl_space *set_space))
 {
 	int i, n, k;
 	int *list = NULL;
@@ -4309,12 +4571,11 @@ static __isl_give isl_map *basic_map_partial_lexopt_symm(
 	isl_ctx *ctx;
 	isl_vec *var = NULL;
 	isl_mat *cst = NULL;
-	isl_map *opt;
-	isl_set *min_expr;
-	isl_dim *map_dim, *set_dim;
+	isl_space *map_space, *set_space;
+	union isl_lex_res res;
 
-	map_dim = isl_basic_map_get_dim(bmap);
-	set_dim = empty ? isl_basic_set_get_dim(dom) : NULL;
+	map_space = isl_basic_map_get_space(bmap);
+	set_space = empty ? isl_basic_set_get_space(dom) : NULL;
 
 	n_in = isl_basic_map_dim(bmap, isl_dim_param) +
 	       isl_basic_map_dim(bmap, isl_dim_in);
@@ -4359,7 +4620,7 @@ static __isl_give isl_map *basic_map_partial_lexopt_symm(
 	bmap = isl_basic_map_finalize(bmap);
 
 	n_div = isl_basic_set_dim(dom, isl_dim_div);
-	dom = isl_basic_set_add(dom, isl_dim_set, 1);
+	dom = isl_basic_set_add_dims(dom, isl_dim_set, 1);
 	dom = isl_basic_set_extend_constraints(dom, 0, n);
 	for (i = 0; i < n; ++i) {
 		k = isl_basic_set_alloc_inequality(dom);
@@ -4370,32 +4631,28 @@ static __isl_give isl_map *basic_map_partial_lexopt_symm(
 		isl_seq_clr(dom->ineq[k] + 1 + n_in + 1, n_div);
 	}
 
-	min_expr = set_minimum(isl_basic_set_get_dim(dom), isl_mat_copy(cst));
-
 	isl_vec_free(var);
 	free(list);
 
-	opt = basic_map_partial_lexopt(bmap, dom, empty, max);
-
-	if (empty) {
-		*empty = split(*empty,
-			       isl_set_copy(min_expr), isl_mat_copy(cst));
-		*empty = isl_set_reset_dim(*empty, set_dim);
-	}
-
-	opt = split_domain(opt, min_expr, cst);
-	opt = isl_map_reset_dim(opt, map_dim);
-
-	return opt;
+	return core(bmap, dom, empty, max, cst, map_space, set_space);
 error:
-	isl_dim_free(map_dim);
-	isl_dim_free(set_dim);
+	isl_space_free(map_space);
+	isl_space_free(set_space);
 	isl_mat_free(cst);
 	isl_vec_free(var);
 	free(list);
 	isl_basic_set_free(dom);
 	isl_basic_map_free(bmap);
-	return NULL;
+	res.p = NULL;
+	return res;
+}
+
+static __isl_give isl_map *basic_map_partial_lexopt_symm_map(
+	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
+	__isl_give isl_set **empty, int max, int first, int second)
+{
+	return basic_map_partial_lexopt_symm(bmap, dom, empty, max,
+		    first, second, &basic_map_partial_lexopt_symm_map_core).map;
 }
 
 /* Recursive part of isl_tab_basic_map_partial_lexopt, after detecting
@@ -4422,10 +4679,10 @@ static __isl_give isl_map *basic_map_partial_lexopt(
 	if (par < 0)
 		goto error;
 	if (!par)
-		return basic_map_partial_lexopt_base(bmap, dom, empty, max);
+		return basic_map_partial_lexopt_base_map(bmap, dom, empty, max);
 	
-	return basic_map_partial_lexopt_symm(bmap, dom, empty, max,
-					     first, second);
+	return basic_map_partial_lexopt_symm_map(bmap, dom, empty, max,
+						 first, second);
 error:
 	isl_basic_set_free(dom);
 	isl_basic_map_free(bmap);
@@ -4479,7 +4736,7 @@ error:
 struct isl_sol_for {
 	struct isl_sol	sol;
 	int		(*fn)(__isl_take isl_basic_set *dom,
-				__isl_take isl_mat *map, void *user);
+				__isl_take isl_aff_list *list, void *user);
 	void		*user;
 };
 
@@ -4501,24 +4758,40 @@ static void sol_for_free_wrap(struct isl_sol *sol)
  *
  * Instead of constructing a basic map, this function calls a user
  * defined function with the current context as a basic set and
- * an affine matrix representing the relation between the input and output.
- * The number of rows in this matrix is equal to one plus the number
- * of output variables.  The number of columns is equal to one plus
- * the total dimension of the context, i.e., the number of parameters,
- * input variables and divs.  Since some of the columns in the matrix
- * may refer to the divs, the basic set is not simplified.
- * (Simplification may reorder or remove divs.)
+ * 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,
 	struct isl_basic_set *dom, struct isl_mat *M)
 {
+	int i;
+	isl_ctx *ctx;
+	isl_local_space *ls;
+	isl_aff *aff;
+	isl_aff_list *list;
+
 	if (sol->sol.error || !dom || !M)
 		goto error;
 
-	dom = isl_basic_set_simplify(dom);
+	ctx = isl_basic_set_get_ctx(dom);
+	ls = isl_basic_set_get_local_space(dom);
+	list = isl_aff_list_alloc(ctx, M->n_row - 1);
+	for (i = 1; i < M->n_row; ++i) {
+		aff = isl_aff_alloc(isl_local_space_copy(ls));
+		if (aff) {
+			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);
+
 	dom = isl_basic_set_finalize(dom);
 
-	if (sol->fn(isl_basic_set_copy(dom), isl_mat_copy(M), sol->user) < 0)
+	if (sol->fn(isl_basic_set_copy(dom), list, sol->user) < 0)
 		goto error;
 
 	isl_basic_set_free(dom);
@@ -4537,19 +4810,19 @@ static void sol_for_add_wrap(struct isl_sol *sol,
 }
 
 static struct isl_sol_for *sol_for_init(struct isl_basic_map *bmap, int max,
-	int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_mat *map,
+	int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_aff_list *list,
 		  void *user),
 	void *user)
 {
 	struct isl_sol_for *sol_for = NULL;
-	struct isl_dim *dom_dim;
+	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_dim_domain(isl_dim_copy(bmap->dim));
+	dom_dim = isl_space_domain(isl_space_copy(bmap->dim));
 	dom = isl_basic_set_universe(dom_dim);
 
 	sol_for->sol.rational = ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL);
@@ -4582,20 +4855,22 @@ static void sol_for_find_solutions(struct isl_sol_for *sol_for,
 }
 
 int isl_basic_map_foreach_lexopt(__isl_keep isl_basic_map *bmap, int max,
-	int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_mat *map,
+	int (*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 -1;
 
-	bmap = isl_basic_map_detect_equalities(bmap);
 	sol_for = sol_for_init(bmap, max, fn, user);
+	if (!sol_for)
+		goto error;
 
-	if (isl_basic_map_fast_is_empty(bmap))
+	if (isl_basic_map_plain_is_empty(bmap))
 		/* nothing */;
 	else {
 		struct isl_tab *tab;
@@ -4617,18 +4892,769 @@ error:
 	return -1;
 }
 
-int isl_basic_map_foreach_lexmin(__isl_keep isl_basic_map *bmap,
-	int (*fn)(__isl_take isl_basic_set *dom, __isl_take isl_mat *map,
+int isl_basic_set_foreach_lexopt(__isl_keep isl_basic_set *bset, int max,
+	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);
+	return isl_basic_map_foreach_lexopt(bset, max, 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_mat *map,
-		  void *user),
-	void *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,
+ * with each pair representing a variable of unrestricted sign.
+ * The solution is trivial if each such pair in the sequence consists
+ * of two identical values, meaning that the variable being represented
+ * has value zero.
+ */
+static int region_is_trivial(struct isl_tab *tab, int pos, int len)
+{
+	int i;
+
+	if (len == 0)
+		return 0;
+
+	for (i = 0; i < len; i +=  2) {
+		int neg_row;
+		int pos_row;
+
+		neg_row = tab->var[pos + i].is_row ?
+				tab->var[pos + i].index : -1;
+		pos_row = tab->var[pos + i + 1].is_row ?
+				tab->var[pos + i + 1].index : -1;
+
+		if ((neg_row < 0 ||
+		     isl_int_is_zero(tab->mat->row[neg_row][1])) &&
+		    (pos_row < 0 ||
+		     isl_int_is_zero(tab->mat->row[pos_row][1])))
+			continue;
+
+		if (neg_row < 0 || pos_row < 0)
+			return 0;
+		if (isl_int_ne(tab->mat->row[neg_row][1],
+			       tab->mat->row[pos_row][1]))
+			return 0;
+	}
+
+	return 1;
+}
+
+/* Return the index of the first trivial region or -1 if all regions
+ * are non-trivial.
+ */
+static int first_trivial_region(struct isl_tab *tab,
+	int n_region, struct isl_region *region)
+{
+	int i;
+
+	for (i = 0; i < n_region; ++i) {
+		if (region_is_trivial(tab, region[i].pos, region[i].len))
+			return i;
+	}
+
+	return -1;
+}
+
+/* Check if the solution is optimal, i.e., whether the first
+ * n_op entries are zero.
+ */
+static int is_optimal(__isl_keep isl_vec *sol, int n_op)
+{
+	int i;
+
+	for (i = 0; i < n_op; ++i)
+		if (!isl_int_is_zero(sol->el[1 + i]))
+			return 0;
+	return 1;
+}
+
+/* Add constraints to "tab" that ensure that any solution is significantly
+ * better that that represented by "sol".  That is, find the first
+ * relevant (within first n_op) non-zero coefficient and force it (along
+ * with all previous coefficients) to be zero.
+ * If the solution is already optimal (all relevant coefficients are zero),
+ * then just mark the table as empty.
+ */
+static int force_better_solution(struct isl_tab *tab,
+	__isl_keep isl_vec *sol, int n_op)
+{
+	int i;
+	isl_ctx *ctx;
+	isl_vec *v = NULL;
+
+	if (!sol)
+		return -1;
+
+	for (i = 0; i < n_op; ++i)
+		if (!isl_int_is_zero(sol->el[1 + i]))
+			break;
+
+	if (i == n_op) {
+		if (isl_tab_mark_empty(tab) < 0)
+			return -1;
+		return 0;
+	}
+
+	ctx = isl_vec_get_ctx(sol);
+	v = isl_vec_alloc(ctx, 1 + tab->n_var);
+	if (!v)
+		return -1;
+
+	for (; i >= 0; --i) {
+		v = isl_vec_clr(v);
+		isl_int_set_si(v->el[1 + i], -1);
+		if (add_lexmin_eq(tab, v->el) < 0)
+			goto error;
+	}
+
+	isl_vec_free(v);
+	return 0;
+error:
+	isl_vec_free(v);
+	return -1;
+}
+
+struct isl_trivial {
+	int update;
+	int region;
+	int side;
+	struct isl_tab_undo *snap;
+};
+
+/* Return the lexicographically smallest non-trivial solution of the
+ * given ILP problem.
+ *
+ * All variables are assumed to be non-negative.
+ *
+ * n_op is the number of initial coordinates to optimize.
+ * That is, once a solution has been found, we will only continue looking
+ * for solution that result in significantly better values for those
+ * initial coordinates.  That is, we only continue looking for solutions
+ * that increase the number of initial zeros in this sequence.
+ *
+ * A solution is non-trivial, if it is non-trivial on each of the
+ * specified regions.  Each region represents a sequence of pairs
+ * of variables.  A solution is non-trivial on such a region if
+ * at least one of these pairs consists of different values, i.e.,
+ * such that the non-negative variable represented by the pair is non-zero.
+ *
+ * Whenever a conflict is encountered, all constraints involved are
+ * reported to the caller through a call to "conflict".
+ *
+ * We perform a simple branch-and-bound backtracking search.
+ * Each level in the search represents initially trivial region that is forced
+ * to be non-trivial.
+ * At each level we consider n cases, where n is the length of the region.
+ * In terms of the n/2 variables of unrestricted signs being encoded by
+ * the region, we consider the cases
+ *	x_0 >= 1
+ *	x_0 <= -1
+ *	x_0 = 0 and x_1 >= 1
+ *	x_0 = 0 and x_1 <= -1
+ *	x_0 = 0 and x_1 = 0 and x_2 >= 1
+ *	x_0 = 0 and x_1 = 0 and x_2 <= -1
+ *	...
+ * The cases are considered in this order, assuming that each pair
+ * x_i_a x_i_b represents the value x_i_b - x_i_a.
+ * That is, x_0 >= 1 is enforced by adding the constraint
+ *	x_0_b - x_0_a >= 1
+ */
+__isl_give isl_vec *isl_tab_basic_set_non_trivial_lexmin(
+	__isl_take isl_basic_set *bset, int n_op, int n_region,
+	struct isl_region *region,
+	int (*conflict)(int con, void *user), void *user)
+{
+	int i, j;
+	int r;
+	isl_ctx *ctx;
+	isl_vec *v = NULL;
+	isl_vec *sol = NULL;
+	struct isl_tab *tab;
+	struct isl_trivial *triv = NULL;
+	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;
+
+	v = isl_vec_alloc(ctx, 1 + tab->n_var);
+	triv = isl_calloc_array(ctx, struct isl_trivial, n_region);
+	if (!v || !triv)
+		goto error;
+
+	level = 0;
+	init = 1;
+
+	while (level >= 0) {
+		int side, base;
+
+		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) {
+				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);
+			if (isl_tab_extend_cons(tab,
+					    2 * region[r].len + 2 * n_op) < 0)
+				goto error;
+			triv[level].region = r;
+			triv[level].side = 0;
+		}
+
+		r = triv[level].region;
+		side = triv[level].side;
+		base = 2 * (side/2);
+
+		if (side >= region[r].len) {
+backtrack:
+			level--;
+			init = 0;
+			if (level >= 0)
+				if (isl_tab_rollback(tab, triv[level].snap) < 0)
+					goto error;
+			continue;
+		}
+
+		if (triv[level].update) {
+			if (force_better_solution(tab, sol, n_op) < 0)
+				goto error;
+			triv[level].update = 0;
+		}
+
+		if (side == base && base >= 2) {
+			for (j = base - 2; j < base; ++j) {
+				v = isl_vec_clr(v);
+				isl_int_set_si(v->el[1 + region[r].pos + j], 1);
+				if (add_lexmin_eq(tab, v->el) < 0)
+					goto error;
+			}
+		}
+
+		triv[level].snap = isl_tab_snap(tab);
+		if (isl_tab_push_basis(tab) < 0)
+			goto error;
+
+		v = isl_vec_clr(v);
+		isl_int_set_si(v->el[0], -1);
+		isl_int_set_si(v->el[1 + region[r].pos + side], -1);
+		isl_int_set_si(v->el[1 + region[r].pos + (side ^ 1)], 1);
+		tab = add_lexmin_ineq(tab, v->el);
+
+		triv[level].side++;
+		level++;
+		init = 1;
+	}
+
+	free(triv);
+	isl_vec_free(v);
+	isl_tab_free(tab);
+	isl_basic_set_free(bset);
+
+	return sol;
+error:
+	free(triv);
+	isl_vec_free(v);
+	isl_tab_free(tab);
+	isl_basic_set_free(bset);
+	isl_vec_free(sol);
+	return NULL;
+}
+
+/* Return the lexicographically smallest rational point in "bset",
+ * assuming that all variables are non-negative.
+ * If "bset" is empty, then return a zero-length vector.
+ */
+__isl_give isl_vec *isl_tab_basic_set_non_neg_lexmin(
+	__isl_take isl_basic_set *bset)
+{
+	struct isl_tab *tab;
+	isl_ctx *ctx = isl_basic_set_get_ctx(bset);
+	isl_vec *sol;
+
+	if (!bset)
+		return NULL;
+
+	tab = tab_for_lexmin(bset, NULL, 0, 0);
+	if (!tab)
+		goto error;
+	if (tab->empty)
+		sol = isl_vec_alloc(ctx, 0);
+	else
+		sol = isl_tab_get_sample_value(tab);
+	isl_tab_free(tab);
+	isl_basic_set_free(bset);
+	return sol;
+error:
+	isl_tab_free(tab);
+	isl_basic_set_free(bset);
+	return NULL;
+}
+
+struct isl_sol_pma {
+	struct isl_sol	sol;
+	isl_pw_multi_aff *pma;
+	isl_set *empty;
+};
+
+static void sol_pma_free(struct isl_sol_pma *sol_pma)
+{
+	if (!sol_pma)
+		return;
+	if (sol_pma->sol.context)
+		sol_pma->sol.context->op->free(sol_pma->sol.context);
+	isl_pw_multi_aff_free(sol_pma->pma);
+	isl_set_free(sol_pma->empty);
+	free(sol_pma);
+}
+
+/* This function is called for parts of the context where there is
+ * no solution, with "bset" corresponding to the context tableau.
+ * Simply add the basic set to the set "empty".
+ */
+static void sol_pma_add_empty(struct isl_sol_pma *sol,
+	__isl_take isl_basic_set *bset)
+{
+	if (!bset)
+		goto error;
+	isl_assert(bset->ctx, sol->empty, goto error);
+
+	sol->empty = isl_set_grow(sol->empty, 1);
+	bset = isl_basic_set_simplify(bset);
+	bset = isl_basic_set_finalize(bset);
+	sol->empty = isl_set_add_basic_set(sol->empty, bset);
+	if (!sol->empty)
+		sol->sol.error = 1;
+	return;
+error:
+	isl_basic_set_free(bset);
+	sol->sol.error = 1;
+}
+
+/* Given a basic map "dom" that represents the context and an affine
+ * matrix "M" that maps the dimensions of the context to the
+ * output variables, construct an isl_pw_multi_aff with a single
+ * cell corresponding to "dom" and affine expressions copied from "M".
+ */
+static void sol_pma_add(struct isl_sol_pma *sol,
+	__isl_take isl_basic_set *dom, __isl_take isl_mat *M)
+{
+	int i;
+	isl_local_space *ls;
+	isl_aff *aff;
+	isl_multi_aff *maff;
+	isl_pw_multi_aff *pma;
+
+	maff = isl_multi_aff_alloc(isl_pw_multi_aff_get_space(sol->pma));
+	ls = isl_basic_set_get_local_space(dom);
+	for (i = 1; i < M->n_row; ++i) {
+		aff = isl_aff_alloc(isl_local_space_copy(ls));
+		if (aff) {
+			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);
+		maff = isl_multi_aff_set_aff(maff, i - 1, aff);
+	}
+	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)
+		sol->sol.error = 1;
+}
+
+static void sol_pma_free_wrap(struct isl_sol *sol)
+{
+	sol_pma_free((struct isl_sol_pma *)sol);
+}
+
+static void sol_pma_add_empty_wrap(struct isl_sol *sol,
+	__isl_take isl_basic_set *bset)
+{
+	sol_pma_add_empty((struct isl_sol_pma *)sol, bset);
+}
+
+static void sol_pma_add_wrap(struct isl_sol *sol,
+	__isl_take isl_basic_set *dom, __isl_take isl_mat *M)
+{
+	sol_pma_add((struct isl_sol_pma *)sol, dom, M);
+}
+
+/* Construct an isl_sol_pma structure for accumulating the solution.
+ * If track_empty is set, then we also keep track of the parts
+ * of the context where there is no solution.
+ * If max is set, then we are solving a maximization, rather than
+ * a minimization problem, which means that the variables in the
+ * tableau have value "M - x" rather than "M + x".
+ */
+static struct isl_sol *sol_pma_init(__isl_keep isl_basic_map *bmap,
+	__isl_take isl_basic_set *dom, int track_empty, int max)
+{
+	struct isl_sol_pma *sol_pma = NULL;
+
+	if (!bmap)
+		goto error;
+
+	sol_pma = isl_calloc_type(bmap->ctx, struct isl_sol_pma);
+	if (!sol_pma)
+		goto error;
+
+	sol_pma->sol.rational = ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL);
+	sol_pma->sol.dec_level.callback.run = &sol_dec_level_wrap;
+	sol_pma->sol.dec_level.sol = &sol_pma->sol;
+	sol_pma->sol.max = max;
+	sol_pma->sol.n_out = isl_basic_map_dim(bmap, isl_dim_out);
+	sol_pma->sol.add = &sol_pma_add_wrap;
+	sol_pma->sol.add_empty = track_empty ? &sol_pma_add_empty_wrap : NULL;
+	sol_pma->sol.free = &sol_pma_free_wrap;
+	sol_pma->pma = isl_pw_multi_aff_empty(isl_basic_map_get_space(bmap));
+	if (!sol_pma->pma)
+		goto error;
+
+	sol_pma->sol.context = isl_context_alloc(dom);
+	if (!sol_pma->sol.context)
+		goto error;
+
+	if (track_empty) {
+		sol_pma->empty = isl_set_alloc_space(isl_basic_set_get_space(dom),
+							1, ISL_SET_DISJOINT);
+		if (!sol_pma->empty)
+			goto error;
+	}
+
+	isl_basic_set_free(dom);
+	return &sol_pma->sol;
+error:
+	isl_basic_set_free(dom);
+	sol_pma_free(sol_pma);
+	return NULL;
+}
+
+/* Base case of isl_tab_basic_map_partial_lexopt, after removing
+ * some obvious symmetries.
+ *
+ * We call basic_map_partial_lexopt_base and extract the results.
+ */
+static __isl_give isl_pw_multi_aff *basic_map_partial_lexopt_base_pma(
+	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
+	__isl_give isl_set **empty, int max)
+{
+	isl_pw_multi_aff *result = NULL;
+	struct isl_sol *sol;
+	struct isl_sol_pma *sol_pma;
+
+	sol = basic_map_partial_lexopt_base(bmap, dom, empty, max,
+					    &sol_pma_init);
+	if (!sol)
+		return NULL;
+	sol_pma = (struct isl_sol_pma *) sol;
+
+	result = isl_pw_multi_aff_copy(sol_pma->pma);
+	if (empty)
+		*empty = isl_set_copy(sol_pma->empty);
+	sol_free(&sol_pma->sol);
+	return result;
+}
+
+/* Given that the last input variable of "maff" represents the minimum
+ * of some bounds, check whether we need to plug in the expression
+ * of the minimum.
+ *
+ * In particular, check if the last input variable appears in any
+ * of the expressions in "maff".
+ */
+static int need_substitution(__isl_keep isl_multi_aff *maff)
+{
+	int i;
+	unsigned pos;
+
+	pos = isl_multi_aff_dim(maff, isl_dim_in) - 1;
+
+	for (i = 0; i < maff->n; ++i)
+		if (isl_aff_involves_dims(maff->p[i], isl_dim_in, pos, 1))
+			return 1;
+
+	return 0;
+}
+
+/* Given a set of upper bounds on the last "input" variable m,
+ * construct a piecewise affine expression that selects
+ * the minimal upper bound to m, i.e.,
+ * divide the space into cells where one
+ * of the upper bounds is smaller than all the others and select
+ * this upper bound on that cell.
+ *
+ * In particular, if there are n bounds b_i, then the result
+ * consists of n cell, each one of the form
+ *
+ *	b_i <= b_j	for j > i
+ *	b_i <  b_j	for j < i
+ *
+ * The affine expression on this cell is
+ *
+ *	b_i
+ */
+static __isl_give isl_pw_aff *set_minimum_pa(__isl_take isl_space *space,
+	__isl_take isl_mat *var)
 {
-	return isl_basic_map_foreach_lexopt(bmap, 1, fn, user);
+	int i;
+	isl_aff *aff = NULL;
+	isl_basic_set *bset = NULL;
+	isl_ctx *ctx;
+	isl_pw_aff *paff = NULL;
+	isl_space *pw_space;
+	isl_local_space *ls = NULL;
+
+	if (!space || !var)
+		goto error;
+
+	ctx = isl_space_get_ctx(space);
+	ls = isl_local_space_from_space(isl_space_copy(space));
+	pw_space = isl_space_copy(space);
+	pw_space = isl_space_from_domain(pw_space);
+	pw_space = isl_space_add_dims(pw_space, isl_dim_out, 1);
+	paff = isl_pw_aff_alloc_size(pw_space, var->n_row);
+
+	for (i = 0; i < var->n_row; ++i) {
+		isl_pw_aff *paff_i;
+
+		aff = isl_aff_alloc(isl_local_space_copy(ls));
+		bset = isl_basic_set_alloc_space(isl_space_copy(space), 0,
+					       0, var->n_row - 1);
+		if (!aff || !bset)
+			goto error;
+		isl_int_set_si(aff->v->el[0], 1);
+		isl_seq_cpy(aff->v->el + 1, var->row[i], var->n_col);
+		isl_int_set_si(aff->v->el[1 + var->n_col], 0);
+		bset = select_minimum(bset, var, i);
+		paff_i = isl_pw_aff_alloc(isl_set_from_basic_set(bset), aff);
+		paff = isl_pw_aff_add_disjoint(paff, paff_i);
+	}
+
+	isl_local_space_free(ls);
+	isl_space_free(space);
+	isl_mat_free(var);
+	return paff;
+error:
+	isl_aff_free(aff);
+	isl_basic_set_free(bset);
+	isl_pw_aff_free(paff);
+	isl_local_space_free(ls);
+	isl_space_free(space);
+	isl_mat_free(var);
+	return NULL;
+}
+
+/* Given a piecewise multi-affine expression of which the last input variable
+ * is the minimum of the bounds in "cst", plug in the value of the minimum.
+ * This minimum expression is given in "min_expr_pa".
+ * The set "min_expr" contains the same information, but in the form of a set.
+ * The variable is subsequently projected out.
+ *
+ * The implementation is similar to those of "split" and "split_domain".
+ * If the variable appears in a given expression, then minimum expression
+ * is plugged in.  Otherwise, if the variable appears in the constraints
+ * and a split is required, then the domain is split.  Otherwise, no split
+ * is performed.
+ */
+static __isl_give isl_pw_multi_aff *split_domain_pma(
+	__isl_take isl_pw_multi_aff *opt, __isl_take isl_pw_aff *min_expr_pa,
+	__isl_take isl_set *min_expr, __isl_take isl_mat *cst)
+{
+	int n_in;
+	int i;
+	isl_space *space;
+	isl_pw_multi_aff *res;
+
+	if (!opt || !min_expr || !cst)
+		goto error;
+
+	n_in = isl_pw_multi_aff_dim(opt, isl_dim_in);
+	space = isl_pw_multi_aff_get_space(opt);
+	space = isl_space_drop_dims(space, isl_dim_in, n_in - 1, 1);
+	res = isl_pw_multi_aff_empty(space);
+
+	for (i = 0; i < opt->n; ++i) {
+		isl_pw_multi_aff *pma;
+
+		pma = isl_pw_multi_aff_alloc(isl_set_copy(opt->p[i].set),
+					 isl_multi_aff_copy(opt->p[i].maff));
+		if (need_substitution(opt->p[i].maff))
+			pma = isl_pw_multi_aff_substitute(pma,
+					isl_dim_in, n_in - 1, min_expr_pa);
+		else if (need_split_set(opt->p[i].set, cst))
+			pma = isl_pw_multi_aff_intersect_domain(pma,
+						       isl_set_copy(min_expr));
+		pma = isl_pw_multi_aff_project_out(pma,
+						    isl_dim_in, n_in - 1, 1);
+
+		res = isl_pw_multi_aff_add_disjoint(res, pma);
+	}
+
+	isl_pw_multi_aff_free(opt);
+	isl_pw_aff_free(min_expr_pa);
+	isl_set_free(min_expr);
+	isl_mat_free(cst);
+	return res;
+error:
+	isl_pw_multi_aff_free(opt);
+	isl_pw_aff_free(min_expr_pa);
+	isl_set_free(min_expr);
+	isl_mat_free(cst);
+	return NULL;
+}
+
+static __isl_give isl_pw_multi_aff *basic_map_partial_lexopt_pma(
+	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
+	__isl_give isl_set **empty, int max);
+
+/* This function is called from basic_map_partial_lexopt_symm.
+ * The last variable of "bmap" and "dom" corresponds to the minimum
+ * of the bounds in "cst".  "map_space" is the space of the original
+ * input relation (of basic_map_partial_lexopt_symm) and "set_space"
+ * is the space of the original domain.
+ *
+ * We recursively call basic_map_partial_lexopt and then plug in
+ * the definition of the minimum in the result.
+ */
+static __isl_give union isl_lex_res basic_map_partial_lexopt_symm_pma_core(
+	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
+	__isl_give isl_set **empty, int max, __isl_take isl_mat *cst,
+	__isl_take isl_space *map_space, __isl_take isl_space *set_space)
+{
+	isl_pw_multi_aff *opt;
+	isl_pw_aff *min_expr_pa;
+	isl_set *min_expr;
+	union isl_lex_res res;
+
+	min_expr = set_minimum(isl_basic_set_get_space(dom), isl_mat_copy(cst));
+	min_expr_pa = set_minimum_pa(isl_basic_set_get_space(dom),
+					isl_mat_copy(cst));
+
+	opt = basic_map_partial_lexopt_pma(bmap, dom, empty, max);
+
+	if (empty) {
+		*empty = split(*empty,
+			       isl_set_copy(min_expr), isl_mat_copy(cst));
+		*empty = isl_set_reset_space(*empty, set_space);
+	}
+
+	opt = split_domain_pma(opt, min_expr_pa, min_expr, cst);
+	opt = isl_pw_multi_aff_reset_space(opt, map_space);
+
+	res.pma = opt;
+	return res;
+}
+
+static __isl_give isl_pw_multi_aff *basic_map_partial_lexopt_symm_pma(
+	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
+	__isl_give isl_set **empty, int max, int first, int second)
+{
+	return basic_map_partial_lexopt_symm(bmap, dom, empty, max,
+		    first, second, &basic_map_partial_lexopt_symm_pma_core).pma;
+}
+
+/* Recursive part of isl_basic_map_partial_lexopt_pw_multi_aff, after detecting
+ * equalities and removing redundant constraints.
+ *
+ * We first check if there are any parallel constraints (left).
+ * If not, we are in the base case.
+ * If there are parallel constraints, we replace them by a single
+ * constraint in basic_map_partial_lexopt_symm_pma and then call
+ * this function recursively to look for more parallel constraints.
+ */
+static __isl_give isl_pw_multi_aff *basic_map_partial_lexopt_pma(
+	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
+	__isl_give isl_set **empty, int max)
+{
+	int par = 0;
+	int first, second;
+
+	if (!bmap)
+		goto error;
+
+	if (bmap->ctx->opt->pip_symmetry)
+		par = parallel_constraints(bmap, &first, &second);
+	if (par < 0)
+		goto error;
+	if (!par)
+		return basic_map_partial_lexopt_base_pma(bmap, dom, empty, max);
+	
+	return basic_map_partial_lexopt_symm_pma(bmap, dom, empty, max,
+						 first, second);
+error:
+	isl_basic_set_free(dom);
+	isl_basic_map_free(bmap);
+	return NULL;
+}
+
+/* Compute the lexicographic minimum (or maximum if "max" is set)
+ * of "bmap" over the domain "dom" and return the result as a piecewise
+ * multi-affine expression.
+ * If "empty" is not NULL, then *empty is assigned a set that
+ * contains those parts of the domain where there is no solution.
+ * If "bmap" is marked as rational (ISL_BASIC_MAP_RATIONAL),
+ * then we compute the rational optimum.  Otherwise, we compute
+ * the integral optimum.
+ *
+ * We perform some preprocessing.  As the PILP solver does not
+ * handle implicit equalities very well, we first make sure all
+ * the equalities are explicitly available.
+ *
+ * We also add context constraints to the basic map and remove
+ * redundant constraints.  This is only needed because of the
+ * way we handle simple symmetries.  In particular, we currently look
+ * for symmetries on the constraints, before we set up the main tableau.
+ * It is then no good to look for symmetries on possibly redundant constraints.
+ */
+__isl_give isl_pw_multi_aff *isl_basic_map_partial_lexopt_pw_multi_aff(
+	__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
+	__isl_give isl_set **empty, int max)
+{
+	if (empty)
+		*empty = NULL;
+	if (!bmap || !dom)
+		goto error;
+
+	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_pma(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);
+
+	return basic_map_partial_lexopt_pma(bmap, dom, empty, max);
+error:
+	isl_basic_set_free(dom);
+	isl_basic_map_free(bmap);
+	return NULL;
 }