* Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
*/
+#include <isl_ctx_private.h>
#include <isl_mat_private.h>
#include "isl_map_private.h"
#include "isl_tab.h"
#include <isl/seq.h>
+#include <isl_config.h>
/*
* The implementation of tableaus in this file was inspired by Section 8
return NULL;
}
+static void free_undo_record(struct isl_tab_undo *undo)
+{
+ switch (undo->type) {
+ case isl_tab_undo_saved_basis:
+ free(undo->u.col_var);
+ break;
+ default:;
+ }
+ free(undo);
+}
+
static void free_undo(struct isl_tab *tab)
{
struct isl_tab_undo *undo, *next;
for (undo = tab->top; undo && undo != &tab->bottom; undo = next) {
next = undo->next;
- free(undo);
+ free_undo_record(undo);
}
tab->top = undo;
}
struct isl_tab_var *var;
unsigned off = 2 + tab->M;
+ if (tab->mat->ctx->abort) {
+ isl_ctx_set_error(tab->mat->ctx, isl_error_abort);
+ return -1;
+ }
+
isl_int_swap(mat->row[row][0], mat->row[row][off + col]);
sgn = isl_int_sgn(mat->row[row][0]);
if (sgn < 0) {
return isl_tab_pivot(tab, r, var->index);
}
+/* Check whether all variables that are marked as non-negative
+ * also have a non-negative sample value. This function is not
+ * called from the current code but is useful during debugging.
+ */
+static void check_table(struct isl_tab *tab) __attribute__ ((unused));
static void check_table(struct isl_tab *tab)
{
int i;
}
}
+static int row_is_manifestly_non_integral(struct isl_tab *tab, int row)
+{
+ unsigned off = 2 + tab->M;
+
+ if (tab->M && !isl_int_eq(tab->mat->row[row][2],
+ tab->mat->row[row][0]))
+ return 0;
+ if (isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
+ tab->n_col - tab->n_dead) != -1)
+ return 0;
+
+ return !isl_int_is_divisible_by(tab->mat->row[row][1],
+ tab->mat->row[row][0]);
+}
+
+/* For integer tableaus, check if any of the coordinates are stuck
+ * at a non-integral value.
+ */
+static int tab_is_manifestly_empty(struct isl_tab *tab)
+{
+ int i;
+
+ if (tab->empty)
+ return 1;
+ if (tab->rational)
+ return 0;
+
+ for (i = 0; i < tab->n_var; ++i) {
+ if (!tab->var[i].is_row)
+ continue;
+ if (row_is_manifestly_non_integral(tab, tab->var[i].index))
+ return 1;
+ }
+
+ return 0;
+}
+
/* Row variable "var" is non-negative and cannot attain any values
* larger than zero. This means that the coefficients of the unrestricted
* column variables are zero and that the coefficients of the non-negative
}
if (isl_tab_mark_redundant(tab, var->index) < 0)
return -1;
+ if (tab_is_manifestly_empty(tab) && isl_tab_mark_empty(tab) < 0)
+ return -1;
return 0;
}
* d_r d_r d_r d_x/g m
*
* with g the gcd of d_r and d_x and m the lcm of d_r and d_x.
+ *
+ * If tab->M is set, then, internally, each variable x is represented
+ * as x' - M. We then also need no subtract k d_r from the coefficient of M.
*/
int isl_tab_add_row(struct isl_tab *tab, isl_int *line)
{
return -1;
}
+/* Check whether the div described by "div" is obviously non-negative.
+ * If we are using a big parameter, then we will encode the div
+ * as div' = M + div, which is always non-negative.
+ * Otherwise, we check whether div is a non-negative affine combination
+ * of non-negative variables.
+ */
+static int div_is_nonneg(struct isl_tab *tab, __isl_keep isl_vec *div)
+{
+ int i;
+
+ if (tab->M)
+ return 1;
+
+ if (isl_int_is_neg(div->el[1]))
+ return 0;
+
+ for (i = 0; i < tab->n_var; ++i) {
+ if (isl_int_is_neg(div->el[2 + i]))
+ return 0;
+ if (isl_int_is_zero(div->el[2 + i]))
+ continue;
+ if (!tab->var[i].is_nonneg)
+ return 0;
+ }
+
+ return 1;
+}
+
/* Add an extra div, prescribed by "div" to the tableau and
* the associated bmap (which is assumed to be non-NULL).
*
int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div,
int (*add_ineq)(void *user, isl_int *), void *user)
{
- int i;
int r;
int k;
int nonneg;
isl_assert(tab->mat->ctx, tab->bmap, return -1);
- for (i = 0; i < tab->n_var; ++i) {
- if (isl_int_is_neg(div->el[2 + i]))
- break;
- if (isl_int_is_zero(div->el[2 + i]))
- continue;
- if (!tab->var[i].is_nonneg)
- break;
- }
- nonneg = i == tab->n_var && !isl_int_is_neg(div->el[1]);
+ nonneg = div_is_nonneg(tab, div);
if (isl_tab_extend_cons(tab, 3) < 0)
return -1;
if (nonneg)
tab->var[r].is_nonneg = 1;
- tab->bmap = isl_basic_map_extend_dim(tab->bmap,
- isl_basic_map_get_dim(tab->bmap), 1, 0, 2);
+ tab->bmap = isl_basic_map_extend_space(tab->bmap,
+ isl_basic_map_get_space(tab->bmap), 1, 0, 2);
k = isl_basic_map_alloc_div(tab->bmap);
if (k < 0)
return -1;
static int may_be_equality(struct isl_tab *tab, int row)
{
- unsigned off = 2 + tab->M;
return tab->rational ? isl_int_is_zero(tab->mat->row[row][1])
: isl_int_lt(tab->mat->row[row][1],
tab->mat->row[row][0]);
off = 2 + tab->M;
return isl_int_is_zero(tab->mat->row[row][1]) &&
- isl_seq_first_non_zero(tab->mat->row[row] + 2 + tab->n_dead,
+ (!tab->M || isl_int_is_zero(tab->mat->row[row][2])) &&
+ isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
tab->n_col - tab->n_dead) == -1;
}
if (r < 0)
return isl_lp_error;
var = &tab->con[r];
- isl_int_mul(tab->mat->row[var->index][0],
- tab->mat->row[var->index][0], denom);
for (;;) {
int row, col;
find_pivot(tab, var, var, -1, &row, &col);
if (isl_tab_pivot(tab, row, col) < 0)
return isl_lp_error;
}
+ isl_int_mul(tab->mat->row[var->index][0],
+ tab->mat->row[var->index][0], denom);
if (ISL_FL_ISSET(flags, ISL_TAB_SAVE_DUAL)) {
int i;
static int perform_undo_var(struct isl_tab *tab, struct isl_tab_undo *undo)
{
struct isl_tab_var *var = var_from_index(tab, undo->u.var_index);
- switch(undo->type) {
+ switch (undo->type) {
case isl_tab_undo_nonneg:
var->is_nonneg = 0;
break;
break;
case isl_tab_undo_relax:
return unrelax(tab, var);
+ default:
+ isl_die(tab->mat->ctx, isl_error_internal,
+ "perform_undo_var called on invalid undo record",
+ return -1);
}
return 0;
}
free(extra);
- free(col_var);
return 0;
error:
free(extra);
- free(col_var);
return -1;
}
tab->in_undo = 0;
return -1;
}
- free(undo);
+ free_undo_record(undo);
}
tab->in_undo = 0;
tab->top = undo;
* In particular, if the row has been reduced to the constant -1,
* then we know the inequality is adjacent (but opposite) to
* an equality in the tableau.
- * If the row has been reduced to r = -1 -r', with r' an inequality
- * of the tableau, then the inequality is adjacent (but opposite)
- * to the inequality r'.
+ * If the row has been reduced to r = c*(-1 -r'), with r' an inequality
+ * of the tableau and c a positive constant, then the inequality
+ * is adjacent (but opposite) to the inequality r'.
*/
static enum isl_ineq_type separation_type(struct isl_tab *tab, unsigned row)
{
if (!isl_int_is_one(tab->mat->row[row][0]))
return isl_ineq_separate;
- if (!isl_int_is_negone(tab->mat->row[row][1]))
- return isl_ineq_separate;
pos = isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
tab->n_col - tab->n_dead);
- if (pos == -1)
- return isl_ineq_adj_eq;
+ if (pos == -1) {
+ if (isl_int_is_negone(tab->mat->row[row][1]))
+ return isl_ineq_adj_eq;
+ else
+ return isl_ineq_separate;
+ }
- if (!isl_int_is_negone(tab->mat->row[row][off + tab->n_dead + pos]))
+ if (!isl_int_eq(tab->mat->row[row][1],
+ tab->mat->row[row][off + tab->n_dead + pos]))
return isl_ineq_separate;
pos = isl_seq_first_non_zero(
int isl_tab_track_bmap(struct isl_tab *tab, __isl_take isl_basic_map *bmap)
{
+ bmap = isl_basic_map_cow(bmap);
if (!tab || !bmap)
goto error;
- isl_assert(tab->mat->ctx, tab->n_eq == bmap->n_eq, return -1);
+ isl_assert(tab->mat->ctx, tab->n_eq == bmap->n_eq, goto error);
isl_assert(tab->mat->ctx,
- tab->n_con == bmap->n_eq + bmap->n_ineq, return -1);
+ tab->n_con == bmap->n_eq + bmap->n_ineq, goto error);
tab->bmap = bmap;
return (isl_basic_set *)tab->bmap;
}
-void isl_tab_dump(struct isl_tab *tab, FILE *out, int indent)
+static void isl_tab_print_internal(__isl_keep struct isl_tab *tab,
+ FILE *out, int indent)
{
unsigned r, c;
int i;
tab->mat->n_row = tab->n_row;
c = tab->mat->n_col;
tab->mat->n_col = 2 + tab->M + tab->n_col;
- isl_mat_dump(tab->mat, out, indent);
+ isl_mat_print_internal(tab->mat, out, indent);
tab->mat->n_row = r;
tab->mat->n_col = c;
if (tab->bmap)
isl_basic_map_print_internal(tab->bmap, out, indent);
}
+
+void isl_tab_dump(__isl_keep struct isl_tab *tab)
+{
+ isl_tab_print_internal(tab, stderr, 0);
+}