isl_tab.c File Reference

#include "isl_map_private.h"
#include "isl_tab.h"

Go to the source code of this file.

Functions

struct isl_tab * isl_tab_alloc (struct isl_ctx *ctx, unsigned n_row, unsigned n_var)
static int extend_cons (struct isl_ctx *ctx, struct isl_tab *tab, unsigned n_new)
struct isl_tab * isl_tab_extend (struct isl_ctx *ctx, struct isl_tab *tab, unsigned n_new)
static void free_undo (struct isl_ctx *ctx, struct isl_tab *tab)
void isl_tab_free (struct isl_ctx *ctx, struct isl_tab *tab)
static struct isl_tab_var * var_from_index (struct isl_ctx *ctx, struct isl_tab *tab, int i)
static struct isl_tab_var * var_from_row (struct isl_ctx *ctx, struct isl_tab *tab, int i)
static struct isl_tab_var * var_from_col (struct isl_ctx *ctx, struct isl_tab *tab, int i)
static int max_is_manifestly_unbounded (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static int min_is_manifestly_unbounded (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static int pivot_row (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var, int sgn, int c)
static void find_pivot (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var, int sgn, int *row, int *col)
static int is_redundant (struct isl_ctx *ctx, struct isl_tab *tab, int row)
static void swap_rows (struct isl_ctx *ctx, struct isl_tab *tab, int row1, int row2)
static void push (struct isl_ctx *ctx, struct isl_tab *tab, enum isl_tab_undo_type type, struct isl_tab_var *var)
static int mark_redundant (struct isl_ctx *ctx, struct isl_tab *tab, int row)
static void mark_empty (struct isl_ctx *ctx, struct isl_tab *tab)
static void pivot (struct isl_ctx *ctx, struct isl_tab *tab, int row, int col)
static void to_row (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var, int sign)
static void check_table (struct isl_ctx *ctx, struct isl_tab *tab)
static int sign_of_max (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static int restore_row (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static int at_least_zero (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static int sign_of_min (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static int min_at_most_neg_one (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static int at_least_one (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static void swap_cols (struct isl_ctx *ctx, struct isl_tab *tab, int col1, int col2)
static int kill_col (struct isl_ctx *ctx, struct isl_tab *tab, int col)
static void close_row (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static int add_row (struct isl_ctx *ctx, struct isl_tab *tab, isl_int *line)
static int drop_row (struct isl_ctx *ctx, struct isl_tab *tab, int row)
struct isl_tab * isl_tab_add_ineq (struct isl_ctx *ctx, struct isl_tab *tab, isl_int *ineq)
static struct isl_tab * add_eq (struct isl_ctx *ctx, struct isl_tab *tab, isl_int *eq)
struct isl_tab * isl_tab_from_basic_map (struct isl_basic_map *bmap)
struct isl_tab * isl_tab_from_basic_set (struct isl_basic_set *bset)
struct isl_tab * isl_tab_from_recession_cone (struct isl_basic_map *bmap)
int isl_tab_cone_is_bounded (struct isl_ctx *ctx, struct isl_tab *tab)
static int sample_is_integer (struct isl_ctx *ctx, struct isl_tab *tab)
static struct isl_vec * extract_integer_sample (struct isl_ctx *ctx, struct isl_tab *tab)
struct isl_vec * isl_tab_get_sample_value (struct isl_ctx *ctx, struct isl_tab *tab)
struct isl_basic_map * isl_basic_map_update_from_tab (struct isl_basic_map *bmap, struct isl_tab *tab)
struct isl_basic_set * isl_basic_set_update_from_tab (struct isl_basic_set *bset, struct isl_tab *tab)
static struct isl_tab * cut_to_hyperplane (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
struct isl_tab * isl_tab_relax (struct isl_ctx *ctx, struct isl_tab *tab, int con)
struct isl_tab * isl_tab_select_facet (struct isl_ctx *ctx, struct isl_tab *tab, int con)
static int may_be_equality (struct isl_tab *tab, int row)
struct isl_tab * isl_tab_detect_equalities (struct isl_ctx *ctx, struct isl_tab *tab)
struct isl_tab * isl_tab_detect_redundant (struct isl_ctx *ctx, struct isl_tab *tab)
int isl_tab_is_equality (struct isl_ctx *ctx, struct isl_tab *tab, int con)
enum isl_lp_result isl_tab_min (struct isl_ctx *ctx, struct isl_tab *tab, isl_int *f, isl_int denom, isl_int *opt, isl_int *opt_denom)
int isl_tab_is_redundant (struct isl_ctx *ctx, struct isl_tab *tab, int con)
struct isl_tab_undo * isl_tab_snap (struct isl_ctx *ctx, struct isl_tab *tab)
static void unrelax (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_var *var)
static void perform_undo (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_undo *undo)
int isl_tab_rollback (struct isl_ctx *ctx, struct isl_tab *tab, struct isl_tab_undo *snap)
static enum isl_ineq_type separation_type (struct isl_ctx *ctx, struct isl_tab *tab, unsigned row)
enum isl_ineq_type isl_tab_ineq_type (struct isl_ctx *ctx, struct isl_tab *tab, isl_int *ineq)
void isl_tab_dump (struct isl_ctx *ctx, struct isl_tab *tab, FILE *out, int indent)

Function Documentation

struct isl_tab* isl_tab_alloc ( struct isl_ctx *  ctx,
unsigned  n_row,
unsigned  n_var 
) [read]

Definition at line 10 of file isl_tab.c.

00012 {
00013         int i;
00014         struct isl_tab *tab;
00015 
00016         tab = isl_calloc_type(ctx, struct isl_tab);
00017         if (!tab)
00018                 return NULL;
00019         tab->mat = isl_mat_alloc(ctx, n_row, 2 + n_var);
00020         if (!tab->mat)
00021                 goto error;
00022         tab->var = isl_alloc_array(ctx, struct isl_tab_var, n_var);
00023         if (!tab->var)
00024                 goto error;
00025         tab->con = isl_alloc_array(ctx, struct isl_tab_var, n_row);
00026         if (!tab->con)
00027                 goto error;
00028         tab->col_var = isl_alloc_array(ctx, int, n_var);
00029         if (!tab->col_var)
00030                 goto error;
00031         tab->row_var = isl_alloc_array(ctx, int, n_row);
00032         if (!tab->row_var)
00033                 goto error;
00034         for (i = 0; i < n_var; ++i) {
00035                 tab->var[i].index = i;
00036                 tab->var[i].is_row = 0;
00037                 tab->var[i].is_nonneg = 0;
00038                 tab->var[i].is_zero = 0;
00039                 tab->var[i].is_redundant = 0;
00040                 tab->var[i].frozen = 0;
00041                 tab->col_var[i] = i;
00042         }
00043         tab->n_row = 0;
00044         tab->n_con = 0;
00045         tab->n_eq = 0;
00046         tab->max_con = n_row;
00047         tab->n_col = n_var;
00048         tab->n_var = n_var;
00049         tab->n_dead = 0;
00050         tab->n_redundant = 0;
00051         tab->need_undo = 0;
00052         tab->rational = 0;
00053         tab->empty = 0;
00054         tab->bottom.type = isl_tab_undo_bottom;
00055         tab->bottom.next = NULL;
00056         tab->top = &tab->bottom;
00057         return tab;
00058 error:
00059         isl_tab_free(ctx, tab);
00060         return NULL;
00061 }

static int extend_cons ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
unsigned  n_new 
) [static]

Definition at line 63 of file isl_tab.c.

00064 {
00065         if (tab->max_con < tab->n_con + n_new) {
00066                 struct isl_tab_var *con;
00067 
00068                 con = isl_realloc_array(ctx, tab->con,
00069                                     struct isl_tab_var, tab->max_con + n_new);
00070                 if (!con)
00071                         return -1;
00072                 tab->con = con;
00073                 tab->max_con += n_new;
00074         }
00075         if (tab->mat->n_row < tab->n_row + n_new) {
00076                 int *row_var;
00077 
00078                 tab->mat = isl_mat_extend(ctx, tab->mat,
00079                                                 tab->n_row + n_new, tab->n_col);
00080                 if (!tab->mat)
00081                         return -1;
00082                 row_var = isl_realloc_array(ctx, tab->row_var,
00083                                             int, tab->mat->n_row);
00084                 if (!row_var)
00085                         return -1;
00086                 tab->row_var = row_var;
00087         }
00088         return 0;
00089 }

struct isl_tab* isl_tab_extend ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
unsigned  n_new 
) [read]

Definition at line 91 of file isl_tab.c.

00093 {
00094         if (extend_cons(ctx, tab, n_new) >= 0)
00095                 return tab;
00096 
00097         isl_tab_free(ctx, tab);
00098         return NULL;
00099 }

static void free_undo ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
) [static]

Definition at line 101 of file isl_tab.c.

00102 {
00103         struct isl_tab_undo *undo, *next;
00104 
00105         for (undo = tab->top; undo && undo != &tab->bottom; undo = next) {
00106                 next = undo->next;
00107                 free(undo);
00108         }
00109         tab->top = undo;
00110 }

void isl_tab_free ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
)

Definition at line 112 of file isl_tab.c.

00113 {
00114         if (!tab)
00115                 return;
00116         free_undo(ctx, tab);
00117         isl_mat_free(ctx, tab->mat);
00118         free(tab->var);
00119         free(tab->con);
00120         free(tab->row_var);
00121         free(tab->col_var);
00122         free(tab);
00123 }

static struct isl_tab_var* var_from_index ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  i 
) [static, read]

Definition at line 125 of file isl_tab.c.

00127 {
00128         if (i >= 0)
00129                 return &tab->var[i];
00130         else
00131                 return &tab->con[~i];
00132 }

static struct isl_tab_var* var_from_row ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  i 
) [static, read]

Definition at line 134 of file isl_tab.c.

00136 {
00137         return var_from_index(ctx, tab, tab->row_var[i]);
00138 }

static struct isl_tab_var* var_from_col ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  i 
) [static, read]

Definition at line 140 of file isl_tab.c.

00142 {
00143         return var_from_index(ctx, tab, tab->col_var[i]);
00144 }

static int max_is_manifestly_unbounded ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 150 of file isl_tab.c.

00152 {
00153         int i;
00154 
00155         if (var->is_row)
00156                 return 0;
00157         for (i = tab->n_redundant; i < tab->n_row; ++i) {
00158                 if (!isl_int_is_neg(tab->mat->row[i][2 + var->index]))
00159                         continue;
00160                 if (var_from_row(ctx, tab, i)->is_nonneg)
00161                         return 0;
00162         }
00163         return 1;
00164 }

static int min_is_manifestly_unbounded ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 170 of file isl_tab.c.

00172 {
00173         int i;
00174 
00175         if (var->is_row)
00176                 return 0;
00177         for (i = tab->n_redundant; i < tab->n_row; ++i) {
00178                 if (!isl_int_is_pos(tab->mat->row[i][2 + var->index]))
00179                         continue;
00180                 if (var_from_row(ctx, tab, i)->is_nonneg)
00181                         return 0;
00182         }
00183         return 1;
00184 }

static int pivot_row ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var,
int  sgn,
int  c 
) [static]

Definition at line 206 of file isl_tab.c.

00208 {
00209         int j, r, tsgn;
00210         isl_int t;
00211 
00212         isl_int_init(t);
00213         r = -1;
00214         for (j = tab->n_redundant; j < tab->n_row; ++j) {
00215                 if (var && j == var->index)
00216                         continue;
00217                 if (!var_from_row(ctx, tab, j)->is_nonneg)
00218                         continue;
00219                 if (sgn * isl_int_sgn(tab->mat->row[j][2 + c]) >= 0)
00220                         continue;
00221                 if (r < 0) {
00222                         r = j;
00223                         continue;
00224                 }
00225                 isl_int_mul(t, tab->mat->row[r][1], tab->mat->row[j][2 + c]);
00226                 isl_int_submul(t, tab->mat->row[j][1], tab->mat->row[r][2 + c]);
00227                 tsgn = sgn * isl_int_sgn(t);
00228                 if (tsgn < 0 || (tsgn == 0 &&
00229                                             tab->row_var[j] < tab->row_var[r]))
00230                         r = j;
00231         }
00232         isl_int_clear(t);
00233         return r;
00234 }

static void find_pivot ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var,
int  sgn,
int *  row,
int *  col 
) [static]

Definition at line 249 of file isl_tab.c.

00251 {
00252         int j, r, c;
00253         isl_int *tr;
00254 
00255         *row = *col = -1;
00256 
00257         isl_assert(ctx, var->is_row, return);
00258         tr = tab->mat->row[var->index];
00259 
00260         c = -1;
00261         for (j = tab->n_dead; j < tab->n_col; ++j) {
00262                 if (isl_int_is_zero(tr[2 + j]))
00263                         continue;
00264                 if (isl_int_sgn(tr[2 + j]) != sgn &&
00265                     var_from_col(ctx, tab, j)->is_nonneg)
00266                         continue;
00267                 if (c < 0 || tab->col_var[j] < tab->col_var[c])
00268                         c = j;
00269         }
00270         if (c < 0)
00271                 return;
00272 
00273         sgn *= isl_int_sgn(tr[2 + c]);
00274         r = pivot_row(ctx, tab, var, sgn, c);
00275         *row = r < 0 ? var->index : r;
00276         *col = c;
00277 }

static int is_redundant ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  row 
) [static]

Definition at line 285 of file isl_tab.c.

00286 {
00287         int i;
00288 
00289         if (tab->row_var[row] < 0 && !var_from_row(ctx, tab, row)->is_nonneg)
00290                 return 0;
00291 
00292         if (isl_int_is_neg(tab->mat->row[row][1]))
00293                 return 0;
00294 
00295         for (i = tab->n_dead; i < tab->n_col; ++i) {
00296                 if (isl_int_is_zero(tab->mat->row[row][2 + i]))
00297                         continue;
00298                 if (isl_int_is_neg(tab->mat->row[row][2 + i]))
00299                         return 0;
00300                 if (!var_from_col(ctx, tab, i)->is_nonneg)
00301                         return 0;
00302         }
00303         return 1;
00304 }

static void swap_rows ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  row1,
int  row2 
) [static]

Definition at line 306 of file isl_tab.c.

00308 {
00309         int t;
00310         t = tab->row_var[row1];
00311         tab->row_var[row1] = tab->row_var[row2];
00312         tab->row_var[row2] = t;
00313         var_from_row(ctx, tab, row1)->index = row1;
00314         var_from_row(ctx, tab, row2)->index = row2;
00315         tab->mat = isl_mat_swap_rows(ctx, tab->mat, row1, row2);
00316 }

static void push ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
enum isl_tab_undo_type  type,
struct isl_tab_var *  var 
) [static]

Definition at line 318 of file isl_tab.c.

00320 {
00321         struct isl_tab_undo *undo;
00322 
00323         if (!tab->need_undo)
00324                 return;
00325 
00326         undo = isl_alloc_type(ctx, struct isl_tab_undo);
00327         if (!undo) {
00328                 free_undo(ctx, tab);
00329                 tab->top = NULL;
00330                 return;
00331         }
00332         undo->type = type;
00333         undo->var = var;
00334         undo->next = tab->top;
00335         tab->top = undo;
00336 }

static int mark_redundant ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  row 
) [static]

Definition at line 350 of file isl_tab.c.

00352 {
00353         struct isl_tab_var *var = var_from_row(ctx, tab, row);
00354         var->is_redundant = 1;
00355         isl_assert(ctx, row >= tab->n_redundant, return);
00356         if (tab->need_undo || tab->row_var[row] >= 0) {
00357                 if (tab->row_var[row] >= 0) {
00358                         var->is_nonneg = 1;
00359                         push(ctx, tab, isl_tab_undo_nonneg, var);
00360                 }
00361                 if (row != tab->n_redundant)
00362                         swap_rows(ctx, tab, row, tab->n_redundant);
00363                 push(ctx, tab, isl_tab_undo_redundant, var);
00364                 tab->n_redundant++;
00365                 return 0;
00366         } else {
00367                 if (row != tab->n_row - 1)
00368                         swap_rows(ctx, tab, row, tab->n_row - 1);
00369                 var_from_row(ctx, tab, tab->n_row - 1)->index = -1;
00370                 tab->n_row--;
00371                 return 1;
00372         }
00373 }

static void mark_empty ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
) [static]

Definition at line 375 of file isl_tab.c.

00376 {
00377         if (!tab->empty && tab->need_undo)
00378                 push(ctx, tab, isl_tab_undo_empty, NULL);
00379         tab->empty = 1;
00380 }

static void pivot ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  row,
int  col 
) [static]

Definition at line 432 of file isl_tab.c.

00434 {
00435         int i, j;
00436         int sgn;
00437         int t;
00438         struct isl_mat *mat = tab->mat;
00439         struct isl_tab_var *var;
00440 
00441         isl_int_swap(mat->row[row][0], mat->row[row][2 + col]);
00442         sgn = isl_int_sgn(mat->row[row][0]);
00443         if (sgn < 0) {
00444                 isl_int_neg(mat->row[row][0], mat->row[row][0]);
00445                 isl_int_neg(mat->row[row][2 + col], mat->row[row][2 + col]);
00446         } else
00447                 for (j = 0; j < 1 + tab->n_col; ++j) {
00448                         if (j == 1 + col)
00449                                 continue;
00450                         isl_int_neg(mat->row[row][1 + j], mat->row[row][1 + j]);
00451                 }
00452         if (!isl_int_is_one(mat->row[row][0]))
00453                 isl_seq_normalize(mat->row[row], 2 + tab->n_col);
00454         for (i = 0; i < tab->n_row; ++i) {
00455                 if (i == row)
00456                         continue;
00457                 if (isl_int_is_zero(mat->row[i][2 + col]))
00458                         continue;
00459                 isl_int_mul(mat->row[i][0], mat->row[i][0], mat->row[row][0]);
00460                 for (j = 0; j < 1 + tab->n_col; ++j) {
00461                         if (j == 1 + col)
00462                                 continue;
00463                         isl_int_mul(mat->row[i][1 + j],
00464                                     mat->row[i][1 + j], mat->row[row][0]);
00465                         isl_int_addmul(mat->row[i][1 + j],
00466                                     mat->row[i][2 + col], mat->row[row][1 + j]);
00467                 }
00468                 isl_int_mul(mat->row[i][2 + col],
00469                             mat->row[i][2 + col], mat->row[row][2 + col]);
00470                 if (!isl_int_is_one(mat->row[row][0]))
00471                         isl_seq_normalize(mat->row[i], 2 + tab->n_col);
00472         }
00473         t = tab->row_var[row];
00474         tab->row_var[row] = tab->col_var[col];
00475         tab->col_var[col] = t;
00476         var = var_from_row(ctx, tab, row);
00477         var->is_row = 1;
00478         var->index = row;
00479         var = var_from_col(ctx, tab, col);
00480         var->is_row = 0;
00481         var->index = col;
00482         for (i = tab->n_redundant; i < tab->n_row; ++i) {
00483                 if (isl_int_is_zero(mat->row[i][2 + col]))
00484                         continue;
00485                 if (!var_from_row(ctx, tab, i)->frozen &&
00486                     is_redundant(ctx, tab, i))
00487                         if (mark_redundant(ctx, tab, i))
00488                                 --i;
00489         }
00490 }

static void to_row ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var,
int  sign 
) [static]

Definition at line 496 of file isl_tab.c.

00498 {
00499         int r;
00500 
00501         if (var->is_row)
00502                 return;
00503 
00504         r = pivot_row(ctx, tab, NULL, sign, var->index);
00505         isl_assert(ctx, r >= 0, return);
00506         pivot(ctx, tab, r, var->index);
00507 }

static void check_table ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
) [static]

Definition at line 509 of file isl_tab.c.

00510 {
00511         int i;
00512 
00513         if (tab->empty)
00514                 return;
00515         for (i = 0; i < tab->n_row; ++i) {
00516                 if (!var_from_row(ctx, tab, i)->is_nonneg)
00517                         continue;
00518                 assert(!isl_int_is_neg(tab->mat->row[i][1]));
00519         }
00520 }

static int sign_of_max ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 533 of file isl_tab.c.

00535 {
00536         int row, col;
00537 
00538         if (max_is_manifestly_unbounded(ctx, tab, var))
00539                 return 1;
00540         to_row(ctx, tab, var, 1);
00541         while (!isl_int_is_pos(tab->mat->row[var->index][1])) {
00542                 find_pivot(ctx, tab, var, 1, &row, &col);
00543                 if (row == -1)
00544                         return isl_int_sgn(tab->mat->row[var->index][1]);
00545                 pivot(ctx, tab, row, col);
00546                 if (!var->is_row) /* manifestly unbounded */
00547                         return 1;
00548         }
00549         return 1;
00550 }

static int restore_row ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 557 of file isl_tab.c.

00559 {
00560         int row, col;
00561 
00562         while (isl_int_is_neg(tab->mat->row[var->index][1])) {
00563                 find_pivot(ctx, tab, var, 1, &row, &col);
00564                 if (row == -1)
00565                         break;
00566                 pivot(ctx, tab, row, col);
00567                 if (!var->is_row) /* manifestly unbounded */
00568                         return 1;
00569         }
00570         return isl_int_sgn(tab->mat->row[var->index][1]);
00571 }

static int at_least_zero ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 578 of file isl_tab.c.

00580 {
00581         int row, col;
00582 
00583         while (isl_int_is_neg(tab->mat->row[var->index][1])) {
00584                 find_pivot(ctx, tab, var, 1, &row, &col);
00585                 if (row == -1)
00586                         break;
00587                 if (row == var->index) /* manifestly unbounded */
00588                         return 1;
00589                 pivot(ctx, tab, row, col);
00590         }
00591         return !isl_int_is_neg(tab->mat->row[var->index][1]);
00592 }

static int sign_of_min ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 611 of file isl_tab.c.

00613 {
00614         int row, col;
00615         struct isl_tab_var *pivot_var;
00616 
00617         if (min_is_manifestly_unbounded(ctx, tab, var))
00618                 return -1;
00619         if (!var->is_row) {
00620                 col = var->index;
00621                 row = pivot_row(ctx, tab, NULL, -1, col);
00622                 pivot_var = var_from_col(ctx, tab, col);
00623                 pivot(ctx, tab, row, col);
00624                 if (var->is_redundant)
00625                         return 0;
00626                 if (isl_int_is_neg(tab->mat->row[var->index][1])) {
00627                         if (var->is_nonneg) {
00628                                 if (!pivot_var->is_redundant &&
00629                                     pivot_var->index == row)
00630                                         pivot(ctx, tab, row, col);
00631                                 else
00632                                         restore_row(ctx, tab, var);
00633                         }
00634                         return -1;
00635                 }
00636         }
00637         if (var->is_redundant)
00638                 return 0;
00639         while (!isl_int_is_neg(tab->mat->row[var->index][1])) {
00640                 find_pivot(ctx, tab, var, -1, &row, &col);
00641                 if (row == var->index)
00642                         return -1;
00643                 if (row == -1)
00644                         return isl_int_sgn(tab->mat->row[var->index][1]);
00645                 pivot_var = var_from_col(ctx, tab, col);
00646                 pivot(ctx, tab, row, col);
00647                 if (var->is_redundant)
00648                         return 0;
00649         }
00650         if (var->is_nonneg) {
00651                 /* pivot back to non-negative value */
00652                 if (!pivot_var->is_redundant && pivot_var->index == row)
00653                         pivot(ctx, tab, row, col);
00654                 else
00655                         restore_row(ctx, tab, var);
00656         }
00657         return -1;
00658 }

static int min_at_most_neg_one ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 667 of file isl_tab.c.

00669 {
00670         int row, col;
00671         struct isl_tab_var *pivot_var;
00672 
00673         if (min_is_manifestly_unbounded(ctx, tab, var))
00674                 return 1;
00675         if (!var->is_row) {
00676                 col = var->index;
00677                 row = pivot_row(ctx, tab, NULL, -1, col);
00678                 pivot_var = var_from_col(ctx, tab, col);
00679                 pivot(ctx, tab, row, col);
00680                 if (var->is_redundant)
00681                         return 0;
00682                 if (isl_int_is_neg(tab->mat->row[var->index][1]) &&
00683                     isl_int_abs_ge(tab->mat->row[var->index][1],
00684                                    tab->mat->row[var->index][0])) {
00685                         if (var->is_nonneg) {
00686                                 if (!pivot_var->is_redundant &&
00687                                     pivot_var->index == row)
00688                                         pivot(ctx, tab, row, col);
00689                                 else
00690                                         restore_row(ctx, tab, var);
00691                         }
00692                         return 1;
00693                 }
00694         }
00695         if (var->is_redundant)
00696                 return 0;
00697         do {
00698                 find_pivot(ctx, tab, var, -1, &row, &col);
00699                 if (row == var->index)
00700                         return 1;
00701                 if (row == -1)
00702                         return 0;
00703                 pivot_var = var_from_col(ctx, tab, col);
00704                 pivot(ctx, tab, row, col);
00705                 if (var->is_redundant)
00706                         return 0;
00707         } while (!isl_int_is_neg(tab->mat->row[var->index][1]) ||
00708                  isl_int_abs_lt(tab->mat->row[var->index][1],
00709                                 tab->mat->row[var->index][0]));
00710         if (var->is_nonneg) {
00711                 /* pivot back to non-negative value */
00712                 if (!pivot_var->is_redundant && pivot_var->index == row)
00713                         pivot(ctx, tab, row, col);
00714                 restore_row(ctx, tab, var);
00715         }
00716         return 1;
00717 }

static int at_least_one ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 722 of file isl_tab.c.

00724 {
00725         int row, col;
00726         isl_int *r;
00727 
00728         if (max_is_manifestly_unbounded(ctx, tab, var))
00729                 return 1;
00730         to_row(ctx, tab, var, 1);
00731         r = tab->mat->row[var->index];
00732         while (isl_int_lt(r[1], r[0])) {
00733                 find_pivot(ctx, tab, var, 1, &row, &col);
00734                 if (row == -1)
00735                         return isl_int_ge(r[1], r[0]);
00736                 if (row == var->index) /* manifestly unbounded */
00737                         return 1;
00738                 pivot(ctx, tab, row, col);
00739         }
00740         return 1;
00741 }

static void swap_cols ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  col1,
int  col2 
) [static]

Definition at line 743 of file isl_tab.c.

00745 {
00746         int t;
00747         t = tab->col_var[col1];
00748         tab->col_var[col1] = tab->col_var[col2];
00749         tab->col_var[col2] = t;
00750         var_from_col(ctx, tab, col1)->index = col1;
00751         var_from_col(ctx, tab, col2)->index = col2;
00752         tab->mat = isl_mat_swap_cols(ctx, tab->mat, 2 + col1, 2 + col2);
00753 }

static int kill_col ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  col 
) [static]

Definition at line 767 of file isl_tab.c.

00769 {
00770         var_from_col(ctx, tab, col)->is_zero = 1;
00771         if (tab->need_undo) {
00772                 push(ctx, tab, isl_tab_undo_zero, var_from_col(ctx, tab, col));
00773                 if (col != tab->n_dead)
00774                         swap_cols(ctx, tab, col, tab->n_dead);
00775                 tab->n_dead++;
00776                 return 0;
00777         } else {
00778                 if (col != tab->n_col - 1)
00779                         swap_cols(ctx, tab, col, tab->n_col - 1);
00780                 var_from_col(ctx, tab, tab->n_col - 1)->index = -1;
00781                 tab->n_col--;
00782                 return 1;
00783         }
00784 }

static void close_row ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 794 of file isl_tab.c.

00796 {
00797         int j;
00798         struct isl_mat *mat = tab->mat;
00799 
00800         isl_assert(ctx, var->is_nonneg, return);
00801         var->is_zero = 1;
00802         for (j = tab->n_dead; j < tab->n_col; ++j) {
00803                 if (isl_int_is_zero(mat->row[var->index][2 + j]))
00804                         continue;
00805                 isl_assert(ctx, isl_int_is_neg(mat->row[var->index][2 + j]),
00806                         return);
00807                 if (kill_col(ctx, tab, j))
00808                         --j;
00809         }
00810         mark_redundant(ctx, tab, var->index);
00811 }

static int add_row ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
isl_int *  line 
) [static]

Definition at line 829 of file isl_tab.c.

00830 {
00831         int i;
00832         unsigned r;
00833         isl_int *row;
00834         isl_int a, b;
00835 
00836         isl_assert(ctx, tab->n_row < tab->mat->n_row, return -1);
00837 
00838         isl_int_init(a);
00839         isl_int_init(b);
00840         r = tab->n_con;
00841         tab->con[r].index = tab->n_row;
00842         tab->con[r].is_row = 1;
00843         tab->con[r].is_nonneg = 0;
00844         tab->con[r].is_zero = 0;
00845         tab->con[r].is_redundant = 0;
00846         tab->con[r].frozen = 0;
00847         tab->row_var[tab->n_row] = ~r;
00848         row = tab->mat->row[tab->n_row];
00849         isl_int_set_si(row[0], 1);
00850         isl_int_set(row[1], line[0]);
00851         isl_seq_clr(row + 2, tab->n_col);
00852         for (i = 0; i < tab->n_var; ++i) {
00853                 if (tab->var[i].is_zero)
00854                         continue;
00855                 if (tab->var[i].is_row) {
00856                         isl_int_lcm(a,
00857                                 row[0], tab->mat->row[tab->var[i].index][0]);
00858                         isl_int_swap(a, row[0]);
00859                         isl_int_divexact(a, row[0], a);
00860                         isl_int_divexact(b,
00861                                 row[0], tab->mat->row[tab->var[i].index][0]);
00862                         isl_int_mul(b, b, line[1 + i]);
00863                         isl_seq_combine(row + 1, a, row + 1,
00864                             b, tab->mat->row[tab->var[i].index] + 1,
00865                             1 + tab->n_col);
00866                 } else
00867                         isl_int_addmul(row[2 + tab->var[i].index],
00868                                                         line[1 + i], row[0]);
00869         }
00870         isl_seq_normalize(row, 2 + tab->n_col);
00871         tab->n_row++;
00872         tab->n_con++;
00873         push(ctx, tab, isl_tab_undo_allocate, &tab->con[r]);
00874         isl_int_clear(a);
00875         isl_int_clear(b);
00876 
00877         return r;
00878 }

static int drop_row ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  row 
) [static]

Definition at line 880 of file isl_tab.c.

00881 {
00882         isl_assert(ctx, ~tab->row_var[row] == tab->n_con - 1, return -1);
00883         if (row != tab->n_row - 1)
00884                 swap_rows(ctx, tab, row, tab->n_row - 1);
00885         tab->n_row--;
00886         tab->n_con--;
00887         return 0;
00888 }

struct isl_tab* isl_tab_add_ineq ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
isl_int *  ineq 
) [read]

Definition at line 893 of file isl_tab.c.

00895 {
00896         int r;
00897         int sgn;
00898 
00899         if (!tab)
00900                 return NULL;
00901         r = add_row(ctx, tab, ineq);
00902         if (r < 0)
00903                 goto error;
00904         tab->con[r].is_nonneg = 1;
00905         push(ctx, tab, isl_tab_undo_nonneg, &tab->con[r]);
00906         if (is_redundant(ctx, tab, tab->con[r].index)) {
00907                 mark_redundant(ctx, tab, tab->con[r].index);
00908                 return tab;
00909         }
00910 
00911         sgn = restore_row(ctx, tab, &tab->con[r]);
00912         if (sgn < 0)
00913                 mark_empty(ctx, tab);
00914         else if (tab->con[r].is_row &&
00915                  is_redundant(ctx, tab, tab->con[r].index))
00916                 mark_redundant(ctx, tab, tab->con[r].index);
00917         return tab;
00918 error:
00919         isl_tab_free(ctx, tab);
00920         return NULL;
00921 }

static struct isl_tab* add_eq ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
isl_int *  eq 
) [static, read]

Definition at line 928 of file isl_tab.c.

00930 {
00931         int i;
00932         int r;
00933 
00934         if (!tab)
00935                 return NULL;
00936         r = add_row(ctx, tab, eq);
00937         if (r < 0)
00938                 goto error;
00939 
00940         r = tab->con[r].index;
00941         for (i = tab->n_dead; i < tab->n_col; ++i) {
00942                 if (isl_int_is_zero(tab->mat->row[r][2 + i]))
00943                         continue;
00944                 pivot(ctx, tab, r, i);
00945                 kill_col(ctx, tab, i);
00946                 break;
00947         }
00948         tab->n_eq++;
00949 
00950         return tab;
00951 error:
00952         isl_tab_free(ctx, tab);
00953         return NULL;
00954 }

struct isl_tab* isl_tab_from_basic_map ( struct isl_basic_map *  bmap  )  [read]

Definition at line 956 of file isl_tab.c.

00957 {
00958         int i;
00959         struct isl_tab *tab;
00960 
00961         if (!bmap)
00962                 return NULL;
00963         tab = isl_tab_alloc(bmap->ctx,
00964                             isl_basic_map_total_dim(bmap) + bmap->n_ineq + 1,
00965                             isl_basic_map_total_dim(bmap));
00966         if (!tab)
00967                 return NULL;
00968         tab->rational = ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL);
00969         if (ISL_F_ISSET(bmap, ISL_BASIC_MAP_EMPTY)) {
00970                 mark_empty(bmap->ctx, tab);
00971                 return tab;
00972         }
00973         for (i = 0; i < bmap->n_eq; ++i) {
00974                 tab = add_eq(bmap->ctx, tab, bmap->eq[i]);
00975                 if (!tab)
00976                         return tab;
00977         }
00978         for (i = 0; i < bmap->n_ineq; ++i) {
00979                 tab = isl_tab_add_ineq(bmap->ctx, tab, bmap->ineq[i]);
00980                 if (!tab || tab->empty)
00981                         return tab;
00982         }
00983         return tab;
00984 }

struct isl_tab* isl_tab_from_basic_set ( struct isl_basic_set *  bset  )  [read]

Definition at line 986 of file isl_tab.c.

00987 {
00988         return isl_tab_from_basic_map((struct isl_basic_map *)bset);
00989 }

struct isl_tab* isl_tab_from_recession_cone ( struct isl_basic_map *  bmap  )  [read]

Definition at line 993 of file isl_tab.c.

00994 {
00995         isl_int cst;
00996         int i;
00997         struct isl_tab *tab;
00998 
00999         if (!bmap)
01000                 return NULL;
01001         tab = isl_tab_alloc(bmap->ctx, bmap->n_eq + bmap->n_ineq,
01002                                 isl_basic_map_total_dim(bmap));
01003         if (!tab)
01004                 return NULL;
01005         tab->rational = ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL);
01006 
01007         isl_int_init(cst);
01008         for (i = 0; i < bmap->n_eq; ++i) {
01009                 isl_int_swap(bmap->eq[i][0], cst);
01010                 tab = add_eq(bmap->ctx, tab, bmap->eq[i]);
01011                 isl_int_swap(bmap->eq[i][0], cst);
01012                 if (!tab)
01013                         goto done;
01014         }
01015         for (i = 0; i < bmap->n_ineq; ++i) {
01016                 int r;
01017                 isl_int_swap(bmap->ineq[i][0], cst);
01018                 r = add_row(bmap->ctx, tab, bmap->ineq[i]);
01019                 isl_int_swap(bmap->ineq[i][0], cst);
01020                 if (r < 0)
01021                         goto error;
01022                 tab->con[r].is_nonneg = 1;
01023                 push(bmap->ctx, tab, isl_tab_undo_nonneg, &tab->con[r]);
01024         }
01025 done:
01026         isl_int_clear(cst);
01027         return tab;
01028 error:
01029         isl_int_clear(cst);
01030         isl_tab_free(bmap->ctx, tab);
01031         return NULL;
01032 }

int isl_tab_cone_is_bounded ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
)

Definition at line 1037 of file isl_tab.c.

01038 {
01039         int i;
01040 
01041         if (!tab)
01042                 return -1;
01043         if (tab->empty)
01044                 return 1;
01045         if (tab->n_dead == tab->n_col)
01046                 return 1;
01047 
01048         for (i = tab->n_redundant; i < tab->n_row; ++i) {
01049                 struct isl_tab_var *var;
01050                 var = var_from_row(ctx, tab, i);
01051                 if (!var->is_nonneg)
01052                         continue;
01053                 if (sign_of_max(ctx, tab, var) == 0)
01054                         close_row(ctx, tab, var);
01055                 else
01056                         return 0;
01057                 if (tab->n_dead == tab->n_col)
01058                         return 1;
01059         }
01060         return 0;
01061 }

static int sample_is_integer ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
) [static]

Definition at line 1063 of file isl_tab.c.

01064 {
01065         int i;
01066 
01067         for (i = 0; i < tab->n_var; ++i) {
01068                 int row;
01069                 if (!tab->var[i].is_row)
01070                         continue;
01071                 row = tab->var[i].index;
01072                 if (!isl_int_is_divisible_by(tab->mat->row[row][1],
01073                                                 tab->mat->row[row][0]))
01074                         return 0;
01075         }
01076         return 1;
01077 }

static struct isl_vec* extract_integer_sample ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
) [static, read]

Definition at line 1079 of file isl_tab.c.

01081 {
01082         int i;
01083         struct isl_vec *vec;
01084 
01085         vec = isl_vec_alloc(ctx, 1 + tab->n_var);
01086         if (!vec)
01087                 return NULL;
01088 
01089         isl_int_set_si(vec->block.data[0], 1);
01090         for (i = 0; i < tab->n_var; ++i) {
01091                 if (!tab->var[i].is_row)
01092                         isl_int_set_si(vec->block.data[1 + i], 0);
01093                 else {
01094                         int row = tab->var[i].index;
01095                         isl_int_divexact(vec->block.data[1 + i],
01096                                 tab->mat->row[row][1], tab->mat->row[row][0]);
01097                 }
01098         }
01099 
01100         return vec;
01101 }

struct isl_vec* isl_tab_get_sample_value ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
) [read]

Definition at line 1103 of file isl_tab.c.

01105 {
01106         int i;
01107         struct isl_vec *vec;
01108         isl_int m;
01109 
01110         if (!tab)
01111                 return NULL;
01112 
01113         vec = isl_vec_alloc(ctx, 1 + tab->n_var);
01114         if (!vec)
01115                 return NULL;
01116 
01117         isl_int_init(m);
01118 
01119         isl_int_set_si(vec->block.data[0], 1);
01120         for (i = 0; i < tab->n_var; ++i) {
01121                 int row;
01122                 if (!tab->var[i].is_row) {
01123                         isl_int_set_si(vec->block.data[1 + i], 0);
01124                         continue;
01125                 }
01126                 row = tab->var[i].index;
01127                 isl_int_gcd(m, vec->block.data[0], tab->mat->row[row][0]);
01128                 isl_int_divexact(m, tab->mat->row[row][0], m);
01129                 isl_seq_scale(vec->block.data, vec->block.data, m, 1 + i);
01130                 isl_int_divexact(m, vec->block.data[0], tab->mat->row[row][0]);
01131                 isl_int_mul(vec->block.data[1 + i], m, tab->mat->row[row][1]);
01132         }
01133         isl_seq_normalize(vec->block.data, vec->size);
01134 
01135         isl_int_clear(m);
01136         return vec;
01137 }

struct isl_basic_map* isl_basic_map_update_from_tab ( struct isl_basic_map *  bmap,
struct isl_tab *  tab 
) [read]

Definition at line 1147 of file isl_tab.c.

01149 {
01150         int i;
01151         unsigned n_eq;
01152 
01153         if (!bmap)
01154                 return NULL;
01155         if (!tab)
01156                 return bmap;
01157 
01158         n_eq = tab->n_eq;
01159         if (tab->empty)
01160                 bmap = isl_basic_map_set_to_empty(bmap);
01161         else
01162                 for (i = bmap->n_ineq - 1; i >= 0; --i) {
01163                         if (isl_tab_is_equality(bmap->ctx, tab, n_eq + i))
01164                                 isl_basic_map_inequality_to_equality(bmap, i);
01165                         else if (isl_tab_is_redundant(bmap->ctx, tab, n_eq + i))
01166                                 isl_basic_map_drop_inequality(bmap, i);
01167                 }
01168         if (!tab->rational &&
01169             !bmap->sample && sample_is_integer(bmap->ctx, tab))
01170                 bmap->sample = extract_integer_sample(bmap->ctx, tab);
01171         return bmap;
01172 }

struct isl_basic_set* isl_basic_set_update_from_tab ( struct isl_basic_set *  bset,
struct isl_tab *  tab 
) [read]

Definition at line 1174 of file isl_tab.c.

01176 {
01177         return (struct isl_basic_set *)isl_basic_map_update_from_tab(
01178                 (struct isl_basic_map *)bset, tab);
01179 }

static struct isl_tab* cut_to_hyperplane ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static, read]

Definition at line 1190 of file isl_tab.c.

01192 {
01193         unsigned r;
01194         isl_int *row;
01195         int sgn;
01196 
01197         if (extend_cons(ctx, tab, 1) < 0)
01198                 goto error;
01199 
01200         r = tab->n_con;
01201         tab->con[r].index = tab->n_row;
01202         tab->con[r].is_row = 1;
01203         tab->con[r].is_nonneg = 0;
01204         tab->con[r].is_zero = 0;
01205         tab->con[r].is_redundant = 0;
01206         tab->con[r].frozen = 0;
01207         tab->row_var[tab->n_row] = ~r;
01208         row = tab->mat->row[tab->n_row];
01209 
01210         if (var->is_row) {
01211                 isl_int_set(row[0], tab->mat->row[var->index][0]);
01212                 isl_seq_neg(row + 1,
01213                             tab->mat->row[var->index] + 1, 1 + tab->n_col);
01214         } else {
01215                 isl_int_set_si(row[0], 1);
01216                 isl_seq_clr(row + 1, 1 + tab->n_col);
01217                 isl_int_set_si(row[2 + var->index], -1);
01218         }
01219 
01220         tab->n_row++;
01221         tab->n_con++;
01222         push(ctx, tab, isl_tab_undo_allocate, &tab->con[r]);
01223 
01224         sgn = sign_of_max(ctx, tab, &tab->con[r]);
01225         if (sgn < 0)
01226                 mark_empty(ctx, tab);
01227         else {
01228                 tab->con[r].is_nonneg = 1;
01229                 push(ctx, tab, isl_tab_undo_nonneg, &tab->con[r]);
01230                 /* sgn == 0 */
01231                 close_row(ctx, tab, &tab->con[r]);
01232         }
01233 
01234         return tab;
01235 error:
01236         isl_tab_free(ctx, tab);
01237         return NULL;
01238 }

struct isl_tab* isl_tab_relax ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  con 
) [read]

Definition at line 1249 of file isl_tab.c.

01251 {
01252         struct isl_tab_var *var;
01253         if (!tab)
01254                 return NULL;
01255 
01256         var = &tab->con[con];
01257 
01258         if (!var->is_row && !max_is_manifestly_unbounded(ctx, tab, var))
01259                 to_row(ctx, tab, var, 1);
01260 
01261         if (var->is_row)
01262                 isl_int_add(tab->mat->row[var->index][1],
01263                     tab->mat->row[var->index][1], tab->mat->row[var->index][0]);
01264         else {
01265                 int i;
01266 
01267                 for (i = 0; i < tab->n_row; ++i) {
01268                         if (isl_int_is_zero(tab->mat->row[i][2 + var->index]))
01269                                 continue;
01270                         isl_int_sub(tab->mat->row[i][1], tab->mat->row[i][1],
01271                             tab->mat->row[i][2 + var->index]);
01272                 }
01273 
01274         }
01275 
01276         push(ctx, tab, isl_tab_undo_relax, var);
01277 
01278         return tab;
01279 }

struct isl_tab* isl_tab_select_facet ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  con 
) [read]

Definition at line 1281 of file isl_tab.c.

01283 {
01284         if (!tab)
01285                 return NULL;
01286 
01287         return cut_to_hyperplane(ctx, tab, &tab->con[con]);
01288 }

static int may_be_equality ( struct isl_tab *  tab,
int  row 
) [static]

Definition at line 1290 of file isl_tab.c.

01291 {
01292         return (tab->rational ? isl_int_is_zero(tab->mat->row[row][1])
01293                               : isl_int_lt(tab->mat->row[row][1],
01294                                             tab->mat->row[row][0])) &&
01295                 isl_seq_first_non_zero(tab->mat->row[row] + 2 + tab->n_dead,
01296                                         tab->n_col - tab->n_dead) != -1;
01297 }

struct isl_tab* isl_tab_detect_equalities ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
) [read]

Definition at line 1315 of file isl_tab.c.

01317 {
01318         int i;
01319         unsigned n_marked;
01320 
01321         if (!tab)
01322                 return NULL;
01323         if (tab->empty)
01324                 return tab;
01325         if (tab->n_dead == tab->n_col)
01326                 return tab;
01327 
01328         n_marked = 0;
01329         for (i = tab->n_redundant; i < tab->n_row; ++i) {
01330                 struct isl_tab_var *var = var_from_row(ctx, tab, i);
01331                 var->marked = !var->frozen && var->is_nonneg &&
01332                         may_be_equality(tab, i);
01333                 if (var->marked)
01334                         n_marked++;
01335         }
01336         for (i = tab->n_dead; i < tab->n_col; ++i) {
01337                 struct isl_tab_var *var = var_from_col(ctx, tab, i);
01338                 var->marked = !var->frozen && var->is_nonneg;
01339                 if (var->marked)
01340                         n_marked++;
01341         }
01342         while (n_marked) {
01343                 struct isl_tab_var *var;
01344                 for (i = tab->n_redundant; i < tab->n_row; ++i) {
01345                         var = var_from_row(ctx, tab, i);
01346                         if (var->marked)
01347                                 break;
01348                 }
01349                 if (i == tab->n_row) {
01350                         for (i = tab->n_dead; i < tab->n_col; ++i) {
01351                                 var = var_from_col(ctx, tab, i);
01352                                 if (var->marked)
01353                                         break;
01354                         }
01355                         if (i == tab->n_col)
01356                                 break;
01357                 }
01358                 var->marked = 0;
01359                 n_marked--;
01360                 if (sign_of_max(ctx, tab, var) == 0)
01361                         close_row(ctx, tab, var);
01362                 else if (!tab->rational && !at_least_one(ctx, tab, var)) {
01363                         tab = cut_to_hyperplane(ctx, tab, var);
01364                         return isl_tab_detect_equalities(ctx, tab);
01365                 }
01366                 for (i = tab->n_redundant; i < tab->n_row; ++i) {
01367                         var = var_from_row(ctx, tab, i);
01368                         if (!var->marked)
01369                                 continue;
01370                         if (may_be_equality(tab, i))
01371                                 continue;
01372                         var->marked = 0;
01373                         n_marked--;
01374                 }
01375         }
01376 
01377         return tab;
01378 }

struct isl_tab* isl_tab_detect_redundant ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
) [read]

Definition at line 1393 of file isl_tab.c.

01395 {
01396         int i;
01397         unsigned n_marked;
01398 
01399         if (!tab)
01400                 return NULL;
01401         if (tab->empty)
01402                 return tab;
01403         if (tab->n_redundant == tab->n_row)
01404                 return tab;
01405 
01406         n_marked = 0;
01407         for (i = tab->n_redundant; i < tab->n_row; ++i) {
01408                 struct isl_tab_var *var = var_from_row(ctx, tab, i);
01409                 var->marked = !var->frozen && var->is_nonneg;
01410                 if (var->marked)
01411                         n_marked++;
01412         }
01413         for (i = tab->n_dead; i < tab->n_col; ++i) {
01414                 struct isl_tab_var *var = var_from_col(ctx, tab, i);
01415                 var->marked = !var->frozen && var->is_nonneg &&
01416                         !min_is_manifestly_unbounded(ctx, tab, var);
01417                 if (var->marked)
01418                         n_marked++;
01419         }
01420         while (n_marked) {
01421                 struct isl_tab_var *var;
01422                 for (i = tab->n_redundant; i < tab->n_row; ++i) {
01423                         var = var_from_row(ctx, tab, i);
01424                         if (var->marked)
01425                                 break;
01426                 }
01427                 if (i == tab->n_row) {
01428                         for (i = tab->n_dead; i < tab->n_col; ++i) {
01429                                 var = var_from_col(ctx, tab, i);
01430                                 if (var->marked)
01431                                         break;
01432                         }
01433                         if (i == tab->n_col)
01434                                 break;
01435                 }
01436                 var->marked = 0;
01437                 n_marked--;
01438                 if ((tab->rational ? (sign_of_min(ctx, tab, var) >= 0)
01439                                    : !min_at_most_neg_one(ctx, tab, var)) &&
01440                     !var->is_redundant)
01441                         mark_redundant(ctx, tab, var->index);
01442                 for (i = tab->n_dead; i < tab->n_col; ++i) {
01443                         var = var_from_col(ctx, tab, i);
01444                         if (!var->marked)
01445                                 continue;
01446                         if (!min_is_manifestly_unbounded(ctx, tab, var))
01447                                 continue;
01448                         var->marked = 0;
01449                         n_marked--;
01450                 }
01451         }
01452 
01453         return tab;
01454 }

int isl_tab_is_equality ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  con 
)

Definition at line 1456 of file isl_tab.c.

01457 {
01458         int row;
01459 
01460         if (!tab)
01461                 return -1;
01462         if (tab->con[con].is_zero)
01463                 return 1;
01464         if (tab->con[con].is_redundant)
01465                 return 0;
01466         if (!tab->con[con].is_row)
01467                 return tab->con[con].index < tab->n_dead;
01468 
01469         row = tab->con[con].index;
01470 
01471         return isl_int_is_zero(tab->mat->row[row][1]) &&
01472                 isl_seq_first_non_zero(tab->mat->row[row] + 2 + tab->n_dead,
01473                                         tab->n_col - tab->n_dead) == -1;
01474 }

enum isl_lp_result isl_tab_min ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
isl_int *  f,
isl_int  denom,
isl_int *  opt,
isl_int *  opt_denom 
)

Definition at line 1483 of file isl_tab.c.

01485 {
01486         int r;
01487         enum isl_lp_result res = isl_lp_ok;
01488         struct isl_tab_var *var;
01489 
01490         if (tab->empty)
01491                 return isl_lp_empty;
01492 
01493         r = add_row(ctx, tab, f);
01494         if (r < 0)
01495                 return isl_lp_error;
01496         var = &tab->con[r];
01497         isl_int_mul(tab->mat->row[var->index][0],
01498                     tab->mat->row[var->index][0], denom);
01499         for (;;) {
01500                 int row, col;
01501                 find_pivot(ctx, tab, var, -1, &row, &col);
01502                 if (row == var->index) {
01503                         res = isl_lp_unbounded;
01504                         break;
01505                 }
01506                 if (row == -1)
01507                         break;
01508                 pivot(ctx, tab, row, col);
01509         }
01510         if (drop_row(ctx, tab, var->index) < 0)
01511                 return isl_lp_error;
01512         if (res == isl_lp_ok) {
01513                 if (opt_denom) {
01514                         isl_int_set(*opt, tab->mat->row[var->index][1]);
01515                         isl_int_set(*opt_denom, tab->mat->row[var->index][0]);
01516                 } else
01517                         isl_int_cdiv_q(*opt, tab->mat->row[var->index][1],
01518                                              tab->mat->row[var->index][0]);
01519         }
01520         return res;
01521 }

int isl_tab_is_redundant ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
int  con 
)

Definition at line 1523 of file isl_tab.c.

01524 {
01525         int row;
01526         unsigned n_col;
01527 
01528         if (!tab)
01529                 return -1;
01530         if (tab->con[con].is_zero)
01531                 return 0;
01532         if (tab->con[con].is_redundant)
01533                 return 1;
01534         return tab->con[con].is_row && tab->con[con].index < tab->n_redundant;
01535 }

struct isl_tab_undo* isl_tab_snap ( struct isl_ctx *  ctx,
struct isl_tab *  tab 
) [read]

Definition at line 1540 of file isl_tab.c.

01541 {
01542         if (!tab)
01543                 return NULL;
01544         tab->need_undo = 1;
01545         return tab->top;
01546 }

static void unrelax ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_var *  var 
) [static]

Definition at line 1550 of file isl_tab.c.

01552 {
01553         if (!var->is_row && !max_is_manifestly_unbounded(ctx, tab, var))
01554                 to_row(ctx, tab, var, 1);
01555 
01556         if (var->is_row)
01557                 isl_int_sub(tab->mat->row[var->index][1],
01558                     tab->mat->row[var->index][1], tab->mat->row[var->index][0]);
01559         else {
01560                 int i;
01561 
01562                 for (i = 0; i < tab->n_row; ++i) {
01563                         if (isl_int_is_zero(tab->mat->row[i][2 + var->index]))
01564                                 continue;
01565                         isl_int_add(tab->mat->row[i][1], tab->mat->row[i][1],
01566                             tab->mat->row[i][2 + var->index]);
01567                 }
01568 
01569         }
01570 }

static void perform_undo ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_undo *  undo 
) [static]

Definition at line 1572 of file isl_tab.c.

01574 {
01575         switch(undo->type) {
01576         case isl_tab_undo_empty:
01577                 tab->empty = 0;
01578                 break;
01579         case isl_tab_undo_nonneg:
01580                 undo->var->is_nonneg = 0;
01581                 break;
01582         case isl_tab_undo_redundant:
01583                 undo->var->is_redundant = 0;
01584                 tab->n_redundant--;
01585                 break;
01586         case isl_tab_undo_zero:
01587                 undo->var->is_zero = 0;
01588                 tab->n_dead--;
01589                 break;
01590         case isl_tab_undo_allocate:
01591                 if (!undo->var->is_row) {
01592                         if (max_is_manifestly_unbounded(ctx, tab, undo->var))
01593                                 to_row(ctx, tab, undo->var, -1);
01594                         else
01595                                 to_row(ctx, tab, undo->var, 1);
01596                 }
01597                 drop_row(ctx, tab, undo->var->index);
01598                 break;
01599         case isl_tab_undo_relax:
01600                 unrelax(ctx, tab, undo->var);
01601                 break;
01602         }
01603 }

int isl_tab_rollback ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
struct isl_tab_undo *  snap 
)

Definition at line 1608 of file isl_tab.c.

01610 {
01611         struct isl_tab_undo *undo, *next;
01612 
01613         if (!tab)
01614                 return -1;
01615 
01616         for (undo = tab->top; undo && undo != &tab->bottom; undo = next) {
01617                 next = undo->next;
01618                 if (undo == snap)
01619                         break;
01620                 perform_undo(ctx, tab, undo);
01621                 free(undo);
01622         }
01623         tab->top = undo;
01624         if (!undo)
01625                 return -1;
01626         return 0;
01627 }

static enum isl_ineq_type separation_type ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
unsigned  row 
) [static]

Definition at line 1639 of file isl_tab.c.

01641 {
01642         int pos;
01643 
01644         if (tab->rational)
01645                 return isl_ineq_separate;
01646 
01647         if (!isl_int_is_one(tab->mat->row[row][0]))
01648                 return isl_ineq_separate;
01649         if (!isl_int_is_negone(tab->mat->row[row][1]))
01650                 return isl_ineq_separate;
01651 
01652         pos = isl_seq_first_non_zero(tab->mat->row[row] + 2 + tab->n_dead,
01653                                         tab->n_col - tab->n_dead);
01654         if (pos == -1)
01655                 return isl_ineq_adj_eq;
01656 
01657         if (!isl_int_is_negone(tab->mat->row[row][2 + tab->n_dead + pos]))
01658                 return isl_ineq_separate;
01659 
01660         pos = isl_seq_first_non_zero(
01661                         tab->mat->row[row] + 2 + tab->n_dead + pos + 1,
01662                         tab->n_col - tab->n_dead - pos - 1);
01663 
01664         return pos == -1 ? isl_ineq_adj_ineq : isl_ineq_separate;
01665 }

enum isl_ineq_type isl_tab_ineq_type ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
isl_int *  ineq 
)

Definition at line 1675 of file isl_tab.c.

01677 {
01678         enum isl_ineq_type type = isl_ineq_error;
01679         struct isl_tab_undo *snap = NULL;
01680         int con;
01681         int row;
01682 
01683         if (!tab)
01684                 return isl_ineq_error;
01685 
01686         if (extend_cons(ctx, tab, 1) < 0)
01687                 return isl_ineq_error;
01688 
01689         snap = isl_tab_snap(ctx, tab);
01690 
01691         con = add_row(ctx, tab, ineq);
01692         if (con < 0)
01693                 goto error;
01694 
01695         row = tab->con[con].index;
01696         if (is_redundant(ctx, tab, row))
01697                 type = isl_ineq_redundant;
01698         else if (isl_int_is_neg(tab->mat->row[row][1]) &&
01699                  (tab->rational ||
01700                     isl_int_abs_ge(tab->mat->row[row][1],
01701                                    tab->mat->row[row][0]))) {
01702                 if (at_least_zero(ctx, tab, &tab->con[con]))
01703                         type = isl_ineq_cut;
01704                 else
01705                         type = separation_type(ctx, tab, row);
01706         } else if (tab->rational ? (sign_of_min(ctx, tab, &tab->con[con]) < 0)
01707                              : min_at_most_neg_one(ctx, tab, &tab->con[con]))
01708                 type = isl_ineq_cut;
01709         else
01710                 type = isl_ineq_redundant;
01711 
01712         if (isl_tab_rollback(ctx, tab, snap))
01713                 return isl_ineq_error;
01714         return type;
01715 error:
01716         isl_tab_rollback(ctx, tab, snap);
01717         return isl_ineq_error;
01718 }

void isl_tab_dump ( struct isl_ctx *  ctx,
struct isl_tab *  tab,
FILE *  out,
int  indent 
)

Definition at line 1720 of file isl_tab.c.

01722 {
01723         unsigned r, c;
01724         int i;
01725 
01726         if (!tab) {
01727                 fprintf(out, "%*snull tab\n", indent, "");
01728                 return;
01729         }
01730         fprintf(out, "%*sn_redundant: %d, n_dead: %d", indent, "",
01731                 tab->n_redundant, tab->n_dead);
01732         if (tab->rational)
01733                 fprintf(out, ", rational");
01734         if (tab->empty)
01735                 fprintf(out, ", empty");
01736         fprintf(out, "\n");
01737         fprintf(out, "%*s[", indent, "");
01738         for (i = 0; i < tab->n_var; ++i) {
01739                 if (i)
01740                         fprintf(out, ", ");
01741                 fprintf(out, "%c%d%s", tab->var[i].is_row ? 'r' : 'c',
01742                                         tab->var[i].index,
01743                                         tab->var[i].is_zero ? " [=0]" :
01744                                         tab->var[i].is_redundant ? " [R]" : "");
01745         }
01746         fprintf(out, "]\n");
01747         fprintf(out, "%*s[", indent, "");
01748         for (i = 0; i < tab->n_con; ++i) {
01749                 if (i)
01750                         fprintf(out, ", ");
01751                 fprintf(out, "%c%d%s", tab->con[i].is_row ? 'r' : 'c',
01752                                         tab->con[i].index,
01753                                         tab->con[i].is_zero ? " [=0]" :
01754                                         tab->con[i].is_redundant ? " [R]" : "");
01755         }
01756         fprintf(out, "]\n");
01757         fprintf(out, "%*s[", indent, "");
01758         for (i = 0; i < tab->n_row; ++i) {
01759                 if (i)
01760                         fprintf(out, ", ");
01761                 fprintf(out, "r%d: %d%s", i, tab->row_var[i],
01762                     var_from_row(ctx, tab, i)->is_nonneg ? " [>=0]" : "");
01763         }
01764         fprintf(out, "]\n");
01765         fprintf(out, "%*s[", indent, "");
01766         for (i = 0; i < tab->n_col; ++i) {
01767                 if (i)
01768                         fprintf(out, ", ");
01769                 fprintf(out, "c%d: %d%s", i, tab->col_var[i],
01770                     var_from_col(ctx, tab, i)->is_nonneg ? " [>=0]" : "");
01771         }
01772         fprintf(out, "]\n");
01773         r = tab->mat->n_row;
01774         tab->mat->n_row = tab->n_row;
01775         c = tab->mat->n_col;
01776         tab->mat->n_col = 2 + tab->n_col;
01777         isl_mat_dump(ctx, tab->mat, out, indent);
01778         tab->mat->n_row = r;
01779         tab->mat->n_col = c;
01780 }

Generated on Fri Jul 17 16:32:58 2009 for CLooG / ISL by  doxygen 1.5.9