* 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;
}
-/* Add an extra div, prescrived by "div" to the tableau and
+/* Add an extra div, prescribed by "div" to the tableau and
* the associated bmap (which is assumed to be non-NULL).
*
* If add_ineq is not NULL, then this function is used instead
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]);
tab->n_col - tab->n_dead) == -1;
}
-/* Return the minimial value of the affine expression "f" with denominator
+/* Return the minimal value of the affine expression "f" with denominator
* "denom" in *opt, *opt_denom, assuming the tableau is not empty and
* the expression cannot attain arbitrarily small values.
* If opt_denom is NULL, then *opt is rounded up to the nearest integer.
* The return value reflects the nature of the result (empty, unbounded,
- * minmimal value returned in *opt).
+ * minimal value returned in *opt).
*/
enum isl_lp_result isl_tab_min(struct isl_tab *tab,
isl_int *f, isl_int denom, isl_int *opt, isl_int *opt_denom,
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(
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_dump(tab->bmap, out, indent);
+ 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);
}
projects / platform / upstream / isl.git / blobdiff