+/* 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);
+ return result;
+}
+
+/* Structure used during detection of parallel constraints.
+ * n_in: number of "input" variables: isl_dim_param + isl_dim_in
+ * n_out: number of "output" variables: isl_dim_out + isl_dim_div
+ * val: the coefficients of the output variables
+ */
+struct isl_constraint_equal_info {
+ isl_basic_map *bmap;
+ unsigned n_in;
+ unsigned n_out;
+ isl_int *val;
+};
+
+/* Check whether the coefficients of the output variables
+ * of the constraint in "entry" are equal to info->val.
+ */
+static int constraint_equal(const void *entry, const void *val)
+{
+ isl_int **row = (isl_int **)entry;
+ const struct isl_constraint_equal_info *info = val;
+
+ return isl_seq_eq((*row) + 1 + info->n_in, info->val, info->n_out);
+}
+
+/* Check whether "bmap" has a pair of constraints that have
+ * the same coefficients for the output variables.
+ * Note that the coefficients of the existentially quantified
+ * variables need to be zero since the existentially quantified
+ * of the result are usually not the same as those of the input.
+ * the isl_dim_out and isl_dim_div dimensions.
+ * If so, return 1 and return the row indices of the two constraints
+ * in *first and *second.
+ */
+static int parallel_constraints(__isl_keep isl_basic_map *bmap,
+ int *first, int *second)
+{
+ int i;
+ isl_ctx *ctx = isl_basic_map_get_ctx(bmap);
+ struct isl_hash_table *table = NULL;
+ struct isl_hash_table_entry *entry;
+ struct isl_constraint_equal_info info;
+ unsigned n_out;
+ unsigned n_div;
+
+ ctx = isl_basic_map_get_ctx(bmap);
+ table = isl_hash_table_alloc(ctx, bmap->n_ineq);
+ if (!table)
+ goto error;
+
+ info.n_in = isl_basic_map_dim(bmap, isl_dim_param) +
+ isl_basic_map_dim(bmap, isl_dim_in);
+ info.bmap = bmap;
+ n_out = isl_basic_map_dim(bmap, isl_dim_out);
+ n_div = isl_basic_map_dim(bmap, isl_dim_div);
+ info.n_out = n_out + n_div;
+ for (i = 0; i < bmap->n_ineq; ++i) {
+ uint32_t hash;
+
+ info.val = bmap->ineq[i] + 1 + info.n_in;
+ if (isl_seq_first_non_zero(info.val, n_out) < 0)
+ continue;
+ if (isl_seq_first_non_zero(info.val + n_out, n_div) >= 0)
+ continue;
+ hash = isl_seq_get_hash(info.val, info.n_out);
+ entry = isl_hash_table_find(ctx, table, hash,
+ constraint_equal, &info, 1);
+ if (!entry)
+ goto error;
+ if (entry->data)
+ break;
+ entry->data = &bmap->ineq[i];
+ }
+
+ if (i < bmap->n_ineq) {
+ *first = ((isl_int **)entry->data) - bmap->ineq;
+ *second = i;
+ }
+
+ isl_hash_table_free(ctx, table);
+
+ return i < bmap->n_ineq;
+error:
+ isl_hash_table_free(ctx, table);
+ 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
+ * of the upper bounds is smaller than all the others and assign
+ * this upper bound to m.
+ *
+ * In particular, if there are n bounds b_i, then the result
+ * consists of n basic sets, each one of the form
+ *
+ * m = b_i
+ * b_i <= b_j for j > i
+ * b_i < b_j for j < i
+ */
+static __isl_give isl_set *set_minimum(__isl_take isl_space *dim,
+ __isl_take isl_mat *var)
+{
+ int i, k;
+ isl_basic_set *bset = NULL;
+ isl_ctx *ctx;
+ isl_set *set = NULL;
+
+ if (!dim || !var)
+ goto error;
+
+ 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_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);
+ bset = select_minimum(bset, var, i);
+ set = isl_set_add_basic_set(set, bset);
+ }
+
+ isl_space_free(dim);
+ isl_mat_free(var);
+ return set;
+error:
+ isl_basic_set_free(bset);
+ isl_set_free(set);
+ isl_space_free(dim);
+ isl_mat_free(var);
+ return NULL;
+}
+
+/* Given that the last input variable of "bmap" represents the minimum
+ * of the bounds in "cst", check whether we need to split the domain
+ * based on which bound attains the minimum.
+ *
+ * A split is needed when the minimum appears in an integer division
+ * or in an equality. Otherwise, it is only needed if it appears in
+ * an upper bound that is different from the upper bounds on which it
+ * is defined.
+ */
+static int need_split_basic_map(__isl_keep isl_basic_map *bmap,
+ __isl_keep isl_mat *cst)
+{
+ int i, j;
+ unsigned total;
+ unsigned pos;
+
+ pos = cst->n_col - 1;
+ total = isl_basic_map_dim(bmap, isl_dim_all);
+
+ for (i = 0; i < bmap->n_div; ++i)
+ if (!isl_int_is_zero(bmap->div[i][2 + pos]))
+ return 1;
+
+ for (i = 0; i < bmap->n_eq; ++i)
+ if (!isl_int_is_zero(bmap->eq[i][1 + pos]))
+ return 1;
+
+ for (i = 0; i < bmap->n_ineq; ++i) {
+ if (isl_int_is_nonneg(bmap->ineq[i][1 + pos]))
+ continue;
+ if (!isl_int_is_negone(bmap->ineq[i][1 + pos]))
+ return 1;
+ if (isl_seq_first_non_zero(bmap->ineq[i] + 1 + pos + 1,
+ total - pos - 1) >= 0)
+ return 1;
+
+ for (j = 0; j < cst->n_row; ++j)
+ if (isl_seq_eq(bmap->ineq[i], cst->row[j], cst->n_col))
+ break;
+ if (j >= cst->n_row)
+ return 1;
+ }
+
+ return 0;
+}
+
+/* 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_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
+ * of the bounds in "cst", split each basic set in the set
+ * in pieces where one of the bounds is (strictly) smaller than the others.
+ * This subdivision is given in "min_expr".
+ * The variable is subsequently projected out.
+ *
+ * We only do the split when it is needed.
+ * For example if the last input variable m = min(a,b) and the only
+ * constraints in the given basic set are lower bounds on m,
+ * i.e., l <= m = min(a,b), then we can simply project out m
+ * to obtain l <= a and l <= b, without having to split on whether
+ * m is equal to a or b.
+ */
+static __isl_give isl_set *split(__isl_take isl_set *empty,
+ __isl_take isl_set *min_expr, __isl_take isl_mat *cst)
+{
+ int n_in;
+ int i;
+ 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_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_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);
+
+ res = isl_set_union_disjoint(res, set);
+ }
+
+ isl_set_free(empty);
+ isl_set_free(min_expr);
+ isl_mat_free(cst);
+ return res;
+error:
+ isl_set_free(empty);
+ isl_set_free(min_expr);
+ isl_mat_free(cst);
+ return NULL;
+}
+
+/* Given a map of which the last input variable is the minimum
+ * of the bounds in "cst", split each basic set in the set
+ * in pieces where one of the bounds is (strictly) smaller than the others.
+ * This subdivision is given in "min_expr".
+ * The variable is subsequently projected out.
+ *
+ * The implementation is essentially the same as that of "split".
+ */
+static __isl_give isl_map *split_domain(__isl_take isl_map *opt,
+ __isl_take isl_set *min_expr, __isl_take isl_mat *cst)
+{
+ int n_in;
+ int i;
+ 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_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_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);
+
+ res = isl_map_union_disjoint(res, map);
+ }
+
+ isl_map_free(opt);
+ isl_set_free(min_expr);
+ isl_mat_free(cst);
+ return res;
+error:
+ isl_map_free(opt);
+ isl_set_free(min_expr);
+ isl_mat_free(cst);
+ return NULL;
+}
+
+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);
+
+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
+ *
+ * a x >= -u >= -b_i(p)
+ *
+ * Moreover, m = min_i(b_i(p)) satisfies the constraints on u and can
+ * therefore be plugged into the solution.
+ */
+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 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;
+ unsigned n_in, n_out, n_div;
+ isl_ctx *ctx;
+ isl_vec *var = NULL;
+ isl_mat *cst = NULL;
+ isl_space *map_space, *set_space;
+ union isl_lex_res res;
+
+ 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);
+ n_out = isl_basic_map_dim(bmap, isl_dim_all) - n_in;
+
+ ctx = isl_basic_map_get_ctx(bmap);
+ list = isl_alloc_array(ctx, int, bmap->n_ineq);
+ var = isl_vec_alloc(ctx, n_out);
+ if (!list || !var)
+ goto error;
+
+ list[0] = first;
+ list[1] = second;
+ isl_seq_cpy(var->el, bmap->ineq[first] + 1 + n_in, n_out);
+ for (i = second + 1, n = 2; i < bmap->n_ineq; ++i) {
+ if (isl_seq_eq(var->el, bmap->ineq[i] + 1 + n_in, n_out))
+ list[n++] = i;
+ }
+
+ cst = isl_mat_alloc(ctx, n, 1 + n_in);
+ if (!cst)
+ goto error;
+
+ for (i = 0; i < n; ++i)
+ isl_seq_cpy(cst->row[i], bmap->ineq[list[i]], 1 + n_in);
+
+ bmap = isl_basic_map_cow(bmap);
+ if (!bmap)
+ goto error;
+ for (i = n - 1; i >= 0; --i)
+ if (isl_basic_map_drop_inequality(bmap, list[i]) < 0)
+ goto error;
+
+ bmap = isl_basic_map_add(bmap, isl_dim_in, 1);
+ bmap = isl_basic_map_extend_constraints(bmap, 0, 1);
+ k = isl_basic_map_alloc_inequality(bmap);
+ if (k < 0)
+ goto error;
+ isl_seq_clr(bmap->ineq[k], 1 + n_in);
+ isl_int_set_si(bmap->ineq[k][1 + n_in], 1);
+ isl_seq_cpy(bmap->ineq[k] + 1 + n_in + 1, var->el, n_out);
+ bmap = isl_basic_map_finalize(bmap);
+
+ n_div = isl_basic_set_dim(dom, isl_dim_div);
+ 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);
+ if (k < 0)
+ goto error;
+ isl_seq_cpy(dom->ineq[k], cst->row[i], 1 + n_in);
+ isl_int_set_si(dom->ineq[k][1 + n_in], -1);
+ isl_seq_clr(dom->ineq[k] + 1 + n_in + 1, n_div);
+ }
+
+ isl_vec_free(var);
+ free(list);
+
+ return core(bmap, dom, empty, max, cst, map_space, set_space);
+error:
+ 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);
+ 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
+ * 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 and then call
+ * this function recursively to look for more parallel constraints.
+ */
+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)
+{
+ 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_map(bmap, dom, empty, max);
+
+ return basic_map_partial_lexopt_symm_map(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 map.
+ * 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.
+ */
+struct isl_map *isl_tab_basic_map_partial_lexopt(
+ struct isl_basic_map *bmap, struct isl_basic_set *dom,
+ struct 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(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(bmap, dom, empty, max);
+error:
+ isl_basic_set_free(dom);
+ isl_basic_map_free(bmap);
+ return NULL;
+}
+
+struct isl_sol_for {
+ struct isl_sol sol;
+ int (*fn)(__isl_take isl_basic_set *dom,
+ __isl_take isl_aff_list *list, void *user);
+ void *user;
+};
+