#include "isl_tab.h"
#include <isl/vec.h>
#include <isl_mat_private.h>
-
-/* Maps dst positions to src positions */
-struct isl_dim_map {
- unsigned len;
- int pos[1];
-};
-
-static struct isl_dim_map *isl_dim_map_alloc(struct isl_ctx *ctx, unsigned len)
-{
- int i;
- struct isl_dim_map *dim_map;
- dim_map = isl_alloc(ctx, struct isl_dim_map,
- sizeof(struct isl_dim_map) + len * sizeof(int));
- if (!dim_map)
- return NULL;
- dim_map->len = 1 + len;
- dim_map->pos[0] = 0;
- for (i = 0; i < len; ++i)
- dim_map->pos[1 + i] = -1;
- return dim_map;
-}
+#include <isl_dim_map.h>
static unsigned n(struct isl_dim *dim, enum isl_dim_type type)
{
}
}
-static void isl_dim_map_dim_range(struct isl_dim_map *dim_map,
- struct isl_dim *dim, enum isl_dim_type type,
- unsigned first, unsigned n, unsigned dst_pos)
-{
- int i;
- unsigned src_pos;
-
- if (!dim_map || !dim)
- return;
-
- src_pos = pos(dim, type);
- for (i = 0; i < n; ++i)
- dim_map->pos[1 + dst_pos + i] = src_pos + first + i;
-}
-
-static void isl_dim_map_dim(struct isl_dim_map *dim_map, struct isl_dim *dim,
- enum isl_dim_type type, unsigned dst_pos)
-{
- isl_dim_map_dim_range(dim_map, dim, type, 0, n(dim, type), dst_pos);
-}
-
-static void isl_dim_map_div(struct isl_dim_map *dim_map,
- struct isl_basic_map *bmap, unsigned dst_pos)
-{
- int i;
- unsigned src_pos;
-
- if (!dim_map || !bmap)
- return;
-
- src_pos = 1 + isl_dim_total(bmap->dim);
- for (i = 0; i < bmap->n_div; ++i)
- dim_map->pos[1 + dst_pos + i] = src_pos + i;
-}
-
-static void isl_dim_map_dump(struct isl_dim_map *dim_map)
-{
- int i;
-
- for (i = 0; i < dim_map->len; ++i)
- fprintf(stderr, "%d -> %d; ", i, dim_map->pos[i]);
- fprintf(stderr, "\n");
-}
-
unsigned isl_basic_map_dim(const struct isl_basic_map *bmap,
enum isl_dim_type type)
{
}
}
+unsigned isl_basic_set_offset(struct isl_basic_set *bset,
+ enum isl_dim_type type)
+{
+ return isl_basic_map_offset(bset, type);
+}
+
static unsigned map_offset(struct isl_map *map, enum isl_dim_type type)
{
return pos(map->dim, type);
return NULL;
}
-static void copy_constraint_dim_map(isl_int *dst, isl_int *src,
- struct isl_dim_map *dim_map)
-{
- int i;
-
- for (i = 0; i < dim_map->len; ++i) {
- if (dim_map->pos[i] < 0)
- isl_int_set_si(dst[i], 0);
- else
- isl_int_set(dst[i], src[dim_map->pos[i]]);
- }
-}
-
-static void copy_div_dim_map(isl_int *dst, isl_int *src,
- struct isl_dim_map *dim_map)
-{
- isl_int_set(dst[0], src[0]);
- copy_constraint_dim_map(dst+1, src+1, dim_map);
-}
-
-static struct isl_basic_map *add_constraints_dim_map(struct isl_basic_map *dst,
- struct isl_basic_map *src, struct isl_dim_map *dim_map)
-{
- int i;
-
- if (!src || !dst || !dim_map)
- goto error;
-
- for (i = 0; i < src->n_eq; ++i) {
- int i1 = isl_basic_map_alloc_equality(dst);
- if (i1 < 0)
- goto error;
- copy_constraint_dim_map(dst->eq[i1], src->eq[i], dim_map);
- }
-
- for (i = 0; i < src->n_ineq; ++i) {
- int i1 = isl_basic_map_alloc_inequality(dst);
- if (i1 < 0)
- goto error;
- copy_constraint_dim_map(dst->ineq[i1], src->ineq[i], dim_map);
- }
-
- for (i = 0; i < src->n_div; ++i) {
- int i1 = isl_basic_map_alloc_div(dst);
- if (i1 < 0)
- goto error;
- copy_div_dim_map(dst->div[i1], src->div[i], dim_map);
- }
-
- free(dim_map);
- isl_basic_map_free(src);
-
- return dst;
-error:
- free(dim_map);
- isl_basic_map_free(src);
- isl_basic_map_free(dst);
- return NULL;
-}
-
struct isl_basic_set *isl_basic_set_add_constraints(struct isl_basic_set *bset1,
struct isl_basic_set *bset2, unsigned pos)
{
(struct isl_basic_map *)bset);
}
-struct isl_set *isl_set_remove_divs(struct isl_set *set)
+__isl_give isl_map *isl_map_remove_divs(__isl_take isl_map *map)
{
int i;
- if (!set)
+ if (!map)
return NULL;
- if (set->n == 0)
- return set;
+ if (map->n == 0)
+ return map;
- set = isl_set_cow(set);
- if (!set)
+ map = isl_map_cow(map);
+ if (!map)
return NULL;
- for (i = 0; i < set->n; ++i) {
- set->p[i] = isl_basic_set_remove_divs(set->p[i]);
- if (!set->p[i])
+ for (i = 0; i < map->n; ++i) {
+ map->p[i] = isl_basic_map_remove_divs(map->p[i]);
+ if (!map->p[i])
goto error;
}
- return set;
+ return map;
error:
- isl_set_free(set);
+ isl_map_free(map);
return NULL;
}
+__isl_give isl_set *isl_set_remove_divs(__isl_take isl_set *set)
+{
+ return isl_map_remove_divs(set);
+}
+
struct isl_basic_map *isl_basic_map_remove_dims(struct isl_basic_map *bmap,
enum isl_dim_type type, unsigned first, unsigned n)
{
bmap->n_div, bmap->n_eq, bmap->n_ineq);
if (isl_basic_map_is_rational(bmap))
res = isl_basic_map_set_rational(res);
- res = add_constraints_dim_map(res, bmap, dim_map);
+ res = isl_basic_map_add_constraints_dim_map(res, bmap, dim_map);
return isl_basic_map_finalize(res);
}
res = isl_basic_map_alloc_dim(isl_basic_map_get_dim(bmap),
bmap->n_div, bmap->n_eq, bmap->n_ineq);
- bmap = add_constraints_dim_map(res, bmap, dim_map);
+ bmap = isl_basic_map_add_constraints_dim_map(res, bmap, dim_map);
bmap->dim = isl_dim_move(bmap->dim, dst_type, dst_pos,
src_type, src_pos, n);
res = isl_basic_map_alloc_dim(isl_basic_map_get_dim(bmap),
bmap->n_div, bmap->n_eq, bmap->n_ineq);
- res = add_constraints_dim_map(res, bmap, dim_map);
+ res = isl_basic_map_add_constraints_dim_map(res, bmap, dim_map);
return res;
}
bmap1->n_div + bmap2->n_div + n,
bmap1->n_eq + bmap2->n_eq,
bmap1->n_ineq + bmap2->n_ineq);
- bmap = add_constraints_dim_map(bmap, bmap1, dim_map1);
- bmap = add_constraints_dim_map(bmap, bmap2, dim_map2);
+ bmap = isl_basic_map_add_constraints_dim_map(bmap, bmap1, dim_map1);
+ bmap = isl_basic_map_add_constraints_dim_map(bmap, bmap2, dim_map2);
bmap = add_divs(bmap, n);
bmap = isl_basic_map_simplify(bmap);
bmap = isl_basic_map_drop_redundant_divs(bmap);
isl_int_set_si(bmap->eq[j][1+pos+i], 1);
isl_int_set_si(bmap->eq[j][1+pos-n_out+i], 1);
}
- bmap = add_constraints_dim_map(bmap, bmap1, dim_map1);
- bmap = add_constraints_dim_map(bmap, bmap2, dim_map2);
+ bmap = isl_basic_map_add_constraints_dim_map(bmap, bmap1, dim_map1);
+ bmap = isl_basic_map_add_constraints_dim_map(bmap, bmap2, dim_map2);
bmap = add_divs(bmap, 2 * n_out);
bmap = isl_basic_map_simplify(bmap);
result = isl_basic_map_alloc_dim(isl_dim_copy(bmap->dim),
bmap->n_div + n_out,
bmap->n_eq, bmap->n_ineq + 2 * n_out);
- result = add_constraints_dim_map(result, bmap, dim_map);
+ result = isl_basic_map_add_constraints_dim_map(result, bmap, dim_map);
result = add_divs(result, n_out);
for (i = 0; i < n_out; ++i) {
int j;
if (!map)
goto error;
- if (isl_map_dim(map, isl_dim_in) == 0)
+ if (isl_map_dim(map, isl_dim_in) == 0 &&
+ !isl_dim_is_named_or_nested(map->dim, isl_dim_in))
return (isl_set *)map;
map = isl_map_cow(map);
if (i == bset->n_eq)
return isl_basic_set_lexmin(bset);
- eq = isl_mat_sub_alloc(bset->ctx, bset->eq, i, bset->n_eq - i,
+ eq = isl_mat_sub_alloc6(bset->ctx, bset->eq, i, bset->n_eq - i,
0, 1 + nparam);
eq = isl_mat_cow(eq);
T = isl_mat_variable_compression(isl_mat_copy(eq), &T2);
bmap1->n_div + bmap2->n_div,
bmap1->n_eq + bmap2->n_eq,
bmap1->n_ineq + bmap2->n_ineq);
- bmap = add_constraints_dim_map(bmap, bmap1, dim_map1);
- bmap = add_constraints_dim_map(bmap, bmap2, dim_map2);
+ bmap = isl_basic_map_add_constraints_dim_map(bmap, bmap1, dim_map1);
+ bmap = isl_basic_map_add_constraints_dim_map(bmap, bmap2, dim_map2);
bmap = isl_basic_map_simplify(bmap);
return isl_basic_map_finalize(bmap);
error:
bmap1->n_div + bmap2->n_div,
bmap1->n_eq + bmap2->n_eq,
bmap1->n_ineq + bmap2->n_ineq);
- bmap = add_constraints_dim_map(bmap, bmap1, dim_map1);
- bmap = add_constraints_dim_map(bmap, bmap2, dim_map2);
+ bmap = isl_basic_map_add_constraints_dim_map(bmap, bmap1, dim_map1);
+ bmap = isl_basic_map_add_constraints_dim_map(bmap, bmap2, dim_map2);
bmap = isl_basic_map_simplify(bmap);
return isl_basic_map_finalize(bmap);
error:
return sv;
}
+int isl_map_is_injective(__isl_keep isl_map *map)
+{
+ int in;
+
+ map = isl_map_copy(map);
+ map = isl_map_reverse(map);
+ in = isl_map_is_single_valued(map);
+ isl_map_free(map);
+
+ return in;
+}
+
int isl_map_is_bijective(__isl_keep isl_map *map)
{
int sv;
if (sv < 0 || !sv)
return sv;
- map = isl_map_copy(map);
- map = isl_map_reverse(map);
- sv = isl_map_is_single_valued(map);
- isl_map_free(map);
-
- return sv;
+ return isl_map_is_injective(map);
}
int isl_set_is_singleton(__isl_keep isl_set *set)
return map;
}
-/* Extend the given dim_map with mappings for the divs in bmap.
- */
-static __isl_give struct isl_dim_map *extend_dim_map(
- __isl_keep struct isl_dim_map *dim_map,
- __isl_keep isl_basic_map *bmap)
-{
- int i;
- struct isl_dim_map *res;
- int offset;
-
- offset = isl_basic_map_offset(bmap, isl_dim_div);
-
- res = isl_dim_map_alloc(bmap->ctx, dim_map->len - 1 + bmap->n_div);
- if (!res)
- return NULL;
-
- for (i = 0; i < dim_map->len; ++i)
- res->pos[i] = dim_map->pos[i];
- for (i = 0; i < bmap->n_div; ++i)
- res->pos[dim_map->len + i] = offset + i;
-
- return res;
-}
-
-/* Extract a dim_map from a reordering.
- * We essentially need to reverse the mapping, and add an offset
- * of 1 for the constant term.
- */
-__isl_give struct isl_dim_map *isl_dim_map_from_reordering(
- __isl_keep isl_reordering *exp)
-{
- int i;
- struct isl_dim_map *dim_map;
-
- if (!exp)
- return NULL;
-
- dim_map = isl_dim_map_alloc(exp->dim->ctx, isl_dim_total(exp->dim));
- if (!dim_map)
- return NULL;
-
- for (i = 0; i < exp->len; ++i)
- dim_map->pos[1 + exp->pos[i]] = 1 + i;
-
- return dim_map;
-}
-
/* Reorder the dimensions of "bmap" according to the given dim_map
* and set the dimension specification to "dim".
*/
res = isl_basic_map_alloc_dim(dim,
bmap->n_div, bmap->n_eq, bmap->n_ineq);
- res = add_constraints_dim_map(res, bmap, dim_map);
+ res = isl_basic_map_add_constraints_dim_map(res, bmap, dim_map);
res = isl_basic_map_finalize(res);
return res;
error:
for (i = 0; i < map->n; ++i) {
struct isl_dim_map *dim_map_i;
- dim_map_i = extend_dim_map(dim_map, map->p[i]);
+ dim_map_i = isl_dim_map_extend(dim_map, map->p[i]);
map->p[i] = isl_basic_map_realign(map->p[i],
isl_dim_copy(r->dim), dim_map_i);
* The strategy used for obtaining a feasible solution is different
* from the one used in isl_tab.c. In particular, in isl_tab.c,
* upon finding a constraint that is not yet satisfied, we pivot
- * in a row that increases the constant term of row holding the
+ * in a row that increases the constant term of the row holding the
* constraint, making sure the sample solution remains feasible
* for all the constraints it already satisfied.
* Here, we always pivot in the row holding the constraint,
return -1;
}
+/* Check whether the invariant that all columns are lexico-positive
+ * is satisfied. This function is not called from the current code
+ * but is useful during debugging.
+ */
+static void check_lexpos(struct isl_tab *tab)
+{
+ unsigned off = 2 + tab->M;
+ int col;
+ int var;
+ 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))
+ continue;
+ for (var = tab->n_param; var < tab->n_var - tab->n_div; ++var) {
+ if (!tab->var[var].is_row) {
+ if (tab->var[var].index == col)
+ break;
+ else
+ continue;
+ }
+ row = tab->var[var].index;
+ if (isl_int_is_zero(tab->mat->row[row][off + col]))
+ continue;
+ if (isl_int_is_pos(tab->mat->row[row][off + col]))
+ break;
+ fprintf(stderr, "lexneg column %d (row %d)\n",
+ col, row);
+ }
+ if (var >= tab->n_var - tab->n_div)
+ fprintf(stderr, "zero column %d\n", col);
+ }
+}
+
+/* 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 represents a constraint) and all constraint columns with
+ * non-zero (and therefore negative) coefficient.
+ */
+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
* smallest increment in the sample point. If there is no such column
* then the tableau is infeasible.
*/
-static struct isl_tab *restore_lexmin(struct isl_tab *tab) WARN_UNUSED;
-static struct isl_tab *restore_lexmin(struct isl_tab *tab)
+static int restore_lexmin(struct isl_tab *tab) WARN_UNUSED;
+static int restore_lexmin(struct isl_tab *tab)
{
int row, col;
if (!tab)
- return NULL;
+ return -1;
if (tab->empty)
- return tab;
+ return 0;
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)
- goto error;
- return tab;
+ return -1;
+ return 0;
}
if (col < 0)
- goto error;
+ return -1;
if (isl_tab_pivot(tab, row, col) < 0)
- goto error;
+ return -1;
}
- return tab;
-error:
- isl_tab_free(tab);
- return NULL;
+ return 0;
}
/* Given a row that represents an equality, look for an appropriate
* 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;
}
- tab = restore_lexmin(tab);
- if (!tab || tab->empty)
- return tab;
+ if (restore_lexmin(tab) < 0)
+ return -1;
+ if (tab->empty)
+ 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;
- tab = restore_lexmin(tab);
- if (!tab || tab->empty)
- return tab;
+ if (restore_lexmin(tab) < 0)
+ return -1;
+ if (tab->empty)
+ 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
return tab;
}
- tab = restore_lexmin(tab);
- if (tab && !tab->empty && tab->con[r].is_row &&
+ if (restore_lexmin(tab) < 0)
+ goto error;
+ if (!tab->empty && tab->con[r].is_row &&
isl_tab_row_is_redundant(tab, tab->con[r].index))
if (isl_tab_mark_redundant(tab, tab->con[r].index) < 0)
goto error;
if (row < 0)
goto error;
} while ((var = next_non_integer_var(tab, var, &flags)) != -1);
- tab = restore_lexmin(tab);
- if (!tab || tab->empty)
+ if (restore_lexmin(tab) < 0)
+ goto error;
+ if (tab->empty)
break;
}
return tab;
if (!tab || tab->empty)
return tab;
}
- if (bmap->n_eq)
- tab = restore_lexmin(tab);
+ if (bmap->n_eq && restore_lexmin(tab) < 0)
+ goto error;
for (i = 0; i < bmap->n_ineq; ++i) {
if (max)
isl_seq_neg(bmap->ineq[i] + 1 + tab->n_param,
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)
clex->context.op = &isl_context_lex_op;
clex->tab = context_tab_for_lexmin(isl_basic_set_copy(dom));
- clex->tab = restore_lexmin(clex->tab);
+ if (restore_lexmin(clex->tab) < 0)
+ goto error;
clex->tab = check_integer_feasible(clex->tab);
if (!clex->tab)
goto error;
if (isl_tab_kill_col(tab, j) < 0)
goto error;
- tab = restore_lexmin(tab);
+ if (restore_lexmin(tab) < 0)
+ goto error;
}
isl_vec_free(eq);
static void find_solutions(struct isl_sol *sol, struct isl_tab *tab)
{
struct isl_context *context;
+ int r;
if (!tab || sol->error)
goto error;
if (context->op->is_empty(context))
goto done;
- for (; tab && !tab->empty; tab = restore_lexmin(tab)) {
+ for (r = 0; r >= 0 && tab && !tab->empty; r = restore_lexmin(tab)) {
int flags;
int row;
enum isl_tab_row_sign sgn;
if (row < 0)
goto error;
}
+ if (r < 0)
+ goto error;
done:
sol_add(sol, tab);
isl_tab_free(tab);
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);
if (sol->sol.error || !dom || !M)
goto error;
- dom = isl_basic_set_simplify(dom);
dom = isl_basic_set_finalize(dom);
if (sol->fn(isl_basic_set_copy(dom), isl_mat_copy(M), sol->user) < 0)
{
return isl_basic_map_foreach_lexopt(bmap, 1, fn, 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 need_update = 0;
+ int r;
+ isl_ctx *ctx = isl_basic_set_get_ctx(bset);
+ isl_vec *v = NULL;
+ isl_vec *sol = isl_vec_alloc(ctx, 0);
+ struct isl_tab *tab;
+ struct isl_trivial *triv = NULL;
+ int level, init;
+
+ tab = tab_for_lexmin(isl_basic_map_from_range(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);
+ 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;
+
+ tab = tab_for_lexmin(isl_basic_map_from_range(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;
+}
projects / platform / upstream / isl.git / commitdiff