Lines Matching refs:tab
37 struct isl_tab *tab;
40 tab = isl_calloc_type(ctx, struct isl_tab);
41 if (!tab)
43 tab->mat = isl_mat_alloc(ctx, n_row, off + n_var);
44 if (!tab->mat)
46 tab->var = isl_alloc_array(ctx, struct isl_tab_var, n_var);
47 if (n_var && !tab->var)
49 tab->con = isl_alloc_array(ctx, struct isl_tab_var, n_row);
50 if (n_row && !tab->con)
52 tab->col_var = isl_alloc_array(ctx, int, n_var);
53 if (n_var && !tab->col_var)
55 tab->row_var = isl_alloc_array(ctx, int, n_row);
56 if (n_row && !tab->row_var)
59 tab->var[i].index = i;
60 tab->var[i].is_row = 0;
61 tab->var[i].is_nonneg = 0;
62 tab->var[i].is_zero = 0;
63 tab->var[i].is_redundant = 0;
64 tab->var[i].frozen = 0;
65 tab->var[i].negated = 0;
66 tab->col_var[i] = i;
68 tab->n_row = 0;
69 tab->n_con = 0;
70 tab->n_eq = 0;
71 tab->max_con = n_row;
72 tab->n_col = n_var;
73 tab->n_var = n_var;
74 tab->max_var = n_var;
75 tab->n_param = 0;
76 tab->n_div = 0;
77 tab->n_dead = 0;
78 tab->n_redundant = 0;
79 tab->strict_redundant = 0;
80 tab->need_undo = 0;
81 tab->rational = 0;
82 tab->empty = 0;
83 tab->in_undo = 0;
84 tab->M = M;
85 tab->cone = 0;
86 tab->bottom.type = isl_tab_undo_bottom;
87 tab->bottom.next = NULL;
88 tab->top = &tab->bottom;
90 tab->n_zero = 0;
91 tab->n_unbounded = 0;
92 tab->basis = NULL;
94 return tab;
96 isl_tab_free(tab);
100 isl_ctx *isl_tab_get_ctx(struct isl_tab *tab)
102 return tab ? isl_mat_get_ctx(tab->mat) : NULL;
105 int isl_tab_extend_cons(struct isl_tab *tab, unsigned n_new)
109 if (!tab)
112 off = 2 + tab->M;
114 if (tab->max_con < tab->n_con + n_new) {
117 con = isl_realloc_array(tab->mat->ctx, tab->con,
118 struct isl_tab_var, tab->max_con + n_new);
121 tab->con = con;
122 tab->max_con += n_new;
124 if (tab->mat->n_row < tab->n_row + n_new) {
127 tab->mat = isl_mat_extend(tab->mat,
128 tab->n_row + n_new, off + tab->n_col);
129 if (!tab->mat)
131 row_var = isl_realloc_array(tab->mat->ctx, tab->row_var,
132 int, tab->mat->n_row);
135 tab->row_var = row_var;
136 if (tab->row_sign) {
138 s = isl_realloc_array(tab->mat->ctx, tab->row_sign,
139 enum isl_tab_row_sign, tab->mat->n_row);
142 tab->row_sign = s;
151 int isl_tab_extend_vars(struct isl_tab *tab, unsigned n_new)
154 unsigned off = 2 + tab->M;
156 if (tab->max_var < tab->n_var + n_new) {
157 var = isl_realloc_array(tab->mat->ctx, tab->var,
158 struct isl_tab_var, tab->n_var + n_new);
161 tab->var = var;
162 tab->max_var = tab->n_var + n_new;
165 if (tab->mat->n_col < off + tab->n_col + n_new) {
168 tab->mat = isl_mat_extend(tab->mat,
169 tab->mat->n_row, off + tab->n_col + n_new);
170 if (!tab->mat)
172 p = isl_realloc_array(tab->mat->ctx, tab->col_var,
173 int, tab->n_col + n_new);
176 tab->col_var = p;
193 static void free_undo(struct isl_tab *tab)
197 for (undo = tab->top; undo && undo != &tab->bottom; undo = next) {
201 tab->top = undo;
204 void isl_tab_free(struct isl_tab *tab)
206 if (!tab)
208 free_undo(tab);
209 isl_mat_free(tab->mat);
210 isl_vec_free(tab->dual);
211 isl_basic_map_free(tab->bmap);
212 free(tab->var);
213 free(tab->con);
214 free(tab->row_var);
215 free(tab->col_var);
216 free(tab->row_sign);
217 isl_mat_free(tab->samples);
218 free(tab->sample_index);
219 isl_mat_free(tab->basis);
220 free(tab);
223 struct isl_tab *isl_tab_dup(struct isl_tab *tab)
229 if (!tab)
232 off = 2 + tab->M;
233 dup = isl_calloc_type(tab->mat->ctx, struct isl_tab);
236 dup->mat = isl_mat_dup(tab->mat);
239 dup->var = isl_alloc_array(tab->mat->ctx, struct isl_tab_var, tab->max_var);
240 if (tab->max_var && !dup->var)
242 for (i = 0; i < tab->n_var; ++i)
243 dup->var[i] = tab->var[i];
244 dup->con = isl_alloc_array(tab->mat->ctx, struct isl_tab_var, tab->max_con);
245 if (tab->max_con && !dup->con)
247 for (i = 0; i < tab->n_con; ++i)
248 dup->con[i] = tab->con[i];
249 dup->col_var = isl_alloc_array(tab->mat->ctx, int, tab->mat->n_col - off);
250 if ((tab->mat->n_col - off) && !dup->col_var)
252 for (i = 0; i < tab->n_col; ++i)
253 dup->col_var[i] = tab->col_var[i];
254 dup->row_var = isl_alloc_array(tab->mat->ctx, int, tab->mat->n_row);
255 if (tab->mat->n_row && !dup->row_var)
257 for (i = 0; i < tab->n_row; ++i)
258 dup->row_var[i] = tab->row_var[i];
259 if (tab->row_sign) {
260 dup->row_sign = isl_alloc_array(tab->mat->ctx, enum isl_tab_row_sign,
261 tab->mat->n_row);
262 if (tab->mat->n_row && !dup->row_sign)
264 for (i = 0; i < tab->n_row; ++i)
265 dup->row_sign[i] = tab->row_sign[i];
267 if (tab->samples) {
268 dup->samples = isl_mat_dup(tab->samples);
271 dup->sample_index = isl_alloc_array(tab->mat->ctx, int,
272 tab->samples->n_row);
273 if (tab->samples->n_row && !dup->sample_index)
275 dup->n_sample = tab->n_sample;
276 dup->n_outside = tab->n_outside;
278 dup->n_row = tab->n_row;
279 dup->n_con = tab->n_con;
280 dup->n_eq = tab->n_eq;
281 dup->max_con = tab->max_con;
282 dup->n_col = tab->n_col;
283 dup->n_var = tab->n_var;
284 dup->max_var = tab->max_var;
285 dup->n_param = tab->n_param;
286 dup->n_div = tab->n_div;
287 dup->n_dead = tab->n_dead;
288 dup->n_redundant = tab->n_redundant;
289 dup->rational = tab->rational;
290 dup->empty = tab->empty;
294 dup->M = tab->M;
295 dup->cone = tab->cone;
300 dup->n_zero = tab->n_zero;
301 dup->n_unbounded = tab->n_unbounded;
302 dup->basis = isl_mat_dup(tab->basis);
563 static struct isl_tab_var *var_from_index(struct isl_tab *tab, int i)
566 return &tab->var[i];
568 return &tab->con[~i];
571 struct isl_tab_var *isl_tab_var_from_row(struct isl_tab *tab, int i)
573 return var_from_index(tab, tab->row_var[i]);
576 static struct isl_tab_var *var_from_col(struct isl_tab *tab, int i)
578 return var_from_index(tab, tab->col_var[i]);
585 static int max_is_manifestly_unbounded(struct isl_tab *tab,
589 unsigned off = 2 + tab->M;
593 for (i = tab->n_redundant; i < tab->n_row; ++i) {
594 if (!isl_int_is_neg(tab->mat->row[i][off + var->index]))
596 if (isl_tab_var_from_row(tab, i)->is_nonneg)
606 static int min_is_manifestly_unbounded(struct isl_tab *tab,
610 unsigned off = 2 + tab->M;
614 for (i = tab->n_redundant; i < tab->n_row; ++i) {
615 if (!isl_int_is_pos(tab->mat->row[i][off + var->index]))
617 if (isl_tab_var_from_row(tab, i)->is_nonneg)
623 static int row_cmp(struct isl_tab *tab, int r1, int r2, int c, isl_int *t)
625 unsigned off = 2 + tab->M;
627 if (tab->M) {
629 isl_int_mul(*t, tab->mat->row[r1][2], tab->mat->row[r2][off+c]);
630 isl_int_submul(*t, tab->mat->row[r2][2], tab->mat->row[r1][off+c]);
635 isl_int_mul(*t, tab->mat->row[r1][1], tab->mat->row[r2][off + c]);
636 isl_int_submul(*t, tab->mat->row[r2][1], tab->mat->row[r1][off + c]);
660 static int pivot_row(struct isl_tab *tab,
665 unsigned off = 2 + tab->M;
669 for (j = tab->n_redundant; j < tab->n_row; ++j) {
672 if (!isl_tab_var_from_row(tab, j)->is_nonneg)
674 if (sgn * isl_int_sgn(tab->mat->row[j][off + c]) >= 0)
680 tsgn = sgn * row_cmp(tab, r, j, c, &t);
682 tab->row_var[j] < tab->row_var[r]))
705 static void find_pivot(struct isl_tab *tab,
714 isl_assert(tab->mat->ctx, var->is_row, return);
715 tr = tab->mat->row[var->index] + 2 + tab->M;
718 for (j = tab->n_dead; j < tab->n_col; ++j) {
722 var_from_col(tab, j)->is_nonneg)
724 if (c < 0 || tab->col_var[j] < tab->col_var[c])
731 r = pivot_row(tab, skip_var, sgn, c);
742 int isl_tab_row_is_redundant(struct isl_tab *tab, int row)
745 unsigned off = 2 + tab->M;
747 if (tab->row_var[row] < 0 && !isl_tab_var_from_row(tab, row)->is_nonneg)
750 if (isl_int_is_neg(tab->mat->row[row][1]))
752 if (tab->strict_redundant && isl_int_is_zero(tab->mat->row[row][1]))
754 if (tab->M && isl_int_is_neg(tab->mat->row[row][2]))
757 for (i = tab->n_dead; i < tab->n_col; ++i) {
758 if (isl_int_is_zero(tab->mat->row[row][off + i]))
760 if (tab->col_var[i] >= 0)
762 if (isl_int_is_neg(tab->mat->row[row][off + i]))
764 if (!var_from_col(tab, i)->is_nonneg)
770 static void swap_rows(struct isl_tab *tab, int row1, int row2)
775 t = tab->row_var[row1];
776 tab->row_var[row1] = tab->row_var[row2];
777 tab->row_var[row2] = t;
778 isl_tab_var_from_row(tab, row1)->index = row1;
779 isl_tab_var_from_row(tab, row2)->index = row2;
780 tab->mat = isl_mat_swap_rows(tab->mat, row1, row2);
782 if (!tab->row_sign)
784 s = tab->row_sign[row1];
785 tab->row_sign[row1] = tab->row_sign[row2];
786 tab->row_sign[row2] = s;
789 static isl_stat push_union(struct isl_tab *tab,
792 /* Push record "u" onto the undo stack of "tab", provided "tab"
799 static isl_stat push_union(struct isl_tab *tab,
804 if (!tab)
806 if (!tab->need_undo)
809 undo = isl_alloc_type(tab->mat->ctx, struct isl_tab_undo);
814 undo->next = tab->top;
815 tab->top = undo;
819 free_undo(tab);
820 tab->top = NULL;
824 isl_stat isl_tab_push_var(struct isl_tab *tab,
829 u.var_index = tab->row_var[var->index];
831 u.var_index = tab->col_var[var->index];
832 return push_union(tab, type, u);
835 isl_stat isl_tab_push(struct isl_tab *tab, enum isl_tab_undo_type type)
838 return push_union(tab, type, u);
844 isl_stat isl_tab_push_basis(struct isl_tab *tab)
849 u.col_var = isl_alloc_array(tab->mat->ctx, int, tab->n_col);
850 if (tab->n_col && !u.col_var)
852 for (i = 0; i < tab->n_col; ++i)
853 u.col_var[i] = tab->col_var[i];
854 return push_union(tab, isl_tab_undo_saved_basis, u);
857 isl_stat isl_tab_push_callback(struct isl_tab *tab,
862 return push_union(tab, isl_tab_undo_callback, u);
865 struct isl_tab *isl_tab_init_samples(struct isl_tab *tab)
867 if (!tab)
870 tab->n_sample = 0;
871 tab->n_outside = 0;
872 tab->samples = isl_mat_alloc(tab->mat->ctx, 1, 1 + tab->n_var);
873 if (!tab->samples)
875 tab->sample_index = isl_alloc_array(tab->mat->ctx, int, 1);
876 if (!tab->sample_index)
878 return tab;
880 isl_tab_free(tab);
884 int isl_tab_add_sample(struct isl_tab *tab, __isl_take isl_vec *sample)
886 if (!tab || !sample)
889 if (tab->n_sample + 1 > tab->samples->n_row) {
890 int *t = isl_realloc_array(tab->mat->ctx,
891 tab->sample_index, int, tab->n_sample + 1);
894 tab->sample_index = t;
897 tab->samples = isl_mat_extend(tab->samples,
898 tab->n_sample + 1, tab->samples->n_col);
899 if (!tab->samples)
902 isl_seq_cpy(tab->samples->row[tab->n_sample], sample->el, sample->size);
904 tab->sample_index[tab->n_sample] = tab->n_sample;
905 tab->n_sample++;
913 struct isl_tab *isl_tab_drop_sample(struct isl_tab *tab, int s)
915 if (s != tab->n_outside) {
916 int t = tab->sample_index[tab->n_outside];
917 tab->sample_index[tab->n_outside] = tab->sample_index[s];
918 tab->sample_index[s] = t;
919 isl_mat_swap_rows(tab->samples, tab->n_outside, s);
921 tab->n_outside++;
922 if (isl_tab_push(tab, isl_tab_undo_drop_sample) < 0) {
923 isl_tab_free(tab);
927 return tab;
933 isl_stat isl_tab_save_samples(struct isl_tab *tab)
937 if (!tab)
940 u.n = tab->n_sample;
941 return push_union(tab, isl_tab_undo_saved_samples, u);
956 int isl_tab_mark_redundant(struct isl_tab *tab, int row)
958 struct isl_tab_var *var = isl_tab_var_from_row(tab, row);
960 isl_assert(tab->mat->ctx, row >= tab->n_redundant, return -1);
961 if (tab->preserve || tab->need_undo || tab->row_var[row] >= 0) {
962 if (tab->row_var[row] >= 0 && !var->is_nonneg) {
964 if (isl_tab_push_var(tab, isl_tab_undo_nonneg, var) < 0)
967 if (row != tab->n_redundant)
968 swap_rows(tab, row, tab->n_redundant);
969 tab->n_redundant++;
970 return isl_tab_push_var(tab, isl_tab_undo_redundant, var);
972 if (row != tab->n_row - 1)
973 swap_rows(tab, row, tab->n_row - 1);
974 isl_tab_var_from_row(tab, tab->n_row - 1)->index = -1;
975 tab->n_row--;
980 /* Mark "tab" as a rational tableau.
985 int isl_tab_mark_rational(struct isl_tab *tab)
987 if (!tab)
989 if (!tab->rational && tab->need_undo)
990 if (isl_tab_push(tab, isl_tab_undo_rational) < 0)
992 tab->rational = 1;
996 isl_stat isl_tab_mark_empty(struct isl_tab *tab)
998 if (!tab)
1000 if (!tab->empty && tab->need_undo)
1001 if (isl_tab_push(tab, isl_tab_undo_empty) < 0)
1003 tab->empty = 1;
1007 int isl_tab_freeze_constraint(struct isl_tab *tab, int con)
1011 if (!tab)
1014 var = &tab->con[con];
1021 if (tab->need_undo)
1022 return isl_tab_push_var(tab, isl_tab_undo_freeze, var);
1044 static void update_row_sign(struct isl_tab *tab, int row, int col, int row_sgn)
1047 struct isl_mat *mat = tab->mat;
1048 unsigned off = 2 + tab->M;
1050 if (!tab->row_sign)
1053 if (tab->row_sign[row] == 0)
1056 isl_assert(mat->ctx, tab->row_sign[row] == isl_tab_row_neg, return);
1057 tab->row_sign[row] = isl_tab_row_pos;
1058 for (i = 0; i < tab->n_row; ++i) {
1065 if (!tab->row_sign[i])
1067 if (s < 0 && tab->row_sign[i] == isl_tab_row_neg)
1069 if (s > 0 && tab->row_sign[i] == isl_tab_row_pos)
1071 tab->row_sign[i] = isl_tab_row_unknown;
1125 int isl_tab_pivot(struct isl_tab *tab, int row, int col)
1131 struct isl_mat *mat = tab->mat;
1133 unsigned off = 2 + tab->M;
1135 ctx = isl_tab_get_ctx(tab);
1145 for (j = 0; j < off - 1 + tab->n_col; ++j) {
1151 isl_seq_normalize(mat->ctx, mat->row[row], off + tab->n_col);
1152 for (i = 0; i < tab->n_row; ++i) {
1158 for (j = 0; j < off - 1 + tab->n_col; ++j) {
1169 isl_seq_normalize(mat->ctx, mat->row[i], off + tab->n_col);
1171 t = tab->row_var[row];
1172 tab->row_var[row] = tab->col_var[col];
1173 tab->col_var[col] = t;
1174 var = isl_tab_var_from_row(tab, row);
1177 var = var_from_col(tab, col);
1180 update_row_sign(tab, row, col, sgn);
1181 if (tab->in_undo)
1183 for (i = tab->n_redundant; i < tab->n_row; ++i) {
1186 if (!isl_tab_var_from_row(tab, i)->frozen &&
1187 isl_tab_row_is_redundant(tab, i)) {
1188 int redo = isl_tab_mark_redundant(tab, i);
1204 static int to_row(struct isl_tab *tab, struct isl_tab_var *var, int sign) WARN_UNUSED;
1205 static int to_row(struct isl_tab *tab, struct isl_tab_var *var, int sign)
1208 unsigned off = 2 + tab->M;
1214 for (r = tab->n_redundant; r < tab->n_row; ++r)
1215 if (!isl_int_is_zero(tab->mat->row[r][off+var->index]))
1217 isl_assert(tab->mat->ctx, r < tab->n_row, return -1);
1219 r = pivot_row(tab, NULL, sign, var->index);
1220 isl_assert(tab->mat->ctx, r >= 0, return -1);
1223 return isl_tab_pivot(tab, r, var->index);
1230 static void check_table(struct isl_tab *tab) __attribute__ ((unused));
1231 static void check_table(struct isl_tab *tab)
1235 if (tab->empty)
1237 for (i = tab->n_redundant; i < tab->n_row; ++i) {
1239 var = isl_tab_var_from_row(tab, i);
1242 if (tab->M) {
1243 isl_assert(tab->mat->ctx,
1244 !isl_int_is_neg(tab->mat->row[i][2]), abort());
1245 if (isl_int_is_pos(tab->mat->row[i][2]))
1248 isl_assert(tab->mat->ctx, !isl_int_is_neg(tab->mat->row[i][1]),
1264 static int sign_of_max(struct isl_tab *tab, struct isl_tab_var *var)
1268 if (max_is_manifestly_unbounded(tab, var))
1270 if (to_row(tab, var, 1) < 0)
1272 while (!isl_int_is_pos(tab->mat->row[var->index][1])) {
1273 find_pivot(tab, var, var, 1, &row, &col);
1275 return isl_int_sgn(tab->mat->row[var->index][1]);
1276 if (isl_tab_pivot(tab, row, col) < 0)
1284 int isl_tab_sign_of_max(struct isl_tab *tab, int con)
1288 if (!tab)
1291 var = &tab->con[con];
1292 isl_assert(tab->mat->ctx, !var->is_redundant, return -2);
1293 isl_assert(tab->mat->ctx, !var->is_zero, return -2);
1295 return sign_of_max(tab, var);
1298 static int row_is_neg(struct isl_tab *tab, int row)
1300 if (!tab->M)
1301 return isl_int_is_neg(tab->mat->row[row][1]);
1302 if (isl_int_is_pos(tab->mat->row[row][2]))
1304 if (isl_int_is_neg(tab->mat->row[row][2]))
1306 return isl_int_is_neg(tab->mat->row[row][1]);
1309 static int row_sgn(struct isl_tab *tab, int row)
1311 if (!tab->M)
1312 return isl_int_sgn(tab->mat->row[row][1]);
1313 if (!isl_int_is_zero(tab->mat->row[row][2]))
1314 return isl_int_sgn(tab->mat->row[row][2]);
1316 return isl_int_sgn(tab->mat->row[row][1]);
1324 static int restore_row(struct isl_tab *tab, struct isl_tab_var *var)
1328 while (row_is_neg(tab, var->index)) {
1329 find_pivot(tab, var, var, 1, &row, &col);
1332 if (isl_tab_pivot(tab, row, col) < 0)
1337 return row_sgn(tab, var->index);
1345 static int at_least_zero(struct isl_tab *tab, struct isl_tab_var *var)
1349 while (isl_int_is_neg(tab->mat->row[var->index][1])) {
1350 find_pivot(tab, var, var, 1, &row, &col);
1355 if (isl_tab_pivot(tab, row, col) < 0)
1358 return !isl_int_is_neg(tab->mat->row[var->index][1]);
1378 static int sign_of_min(struct isl_tab *tab, struct isl_tab_var *var)
1383 if (min_is_manifestly_unbounded(tab, var))
1387 row = pivot_row(tab, NULL, -1, col);
1388 pivot_var = var_from_col(tab, col);
1389 if (isl_tab_pivot(tab, row, col) < 0)
1393 if (isl_int_is_neg(tab->mat->row[var->index][1])) {
1397 if (isl_tab_pivot(tab, row, col) < 0)
1400 if (restore_row(tab, var) < -1)
1408 while (!isl_int_is_neg(tab->mat->row[var->index][1])) {
1409 find_pivot(tab, var, var, -1, &row, &col);
1413 return isl_int_sgn(tab->mat->row[var->index][1]);
1414 pivot_var = var_from_col(tab, col);
1415 if (isl_tab_pivot(tab, row, col) < 0)
1423 if (isl_tab_pivot(tab, row, col) < 0)
1426 if (restore_row(tab, var) < -1)
1432 static int row_at_most_neg_one(struct isl_tab *tab, int row)
1434 if (tab->M) {
1435 if (isl_int_is_pos(tab->mat->row[row][2]))
1437 if (isl_int_is_neg(tab->mat->row[row][2]))
1440 return isl_int_is_neg(tab->mat->row[row][1]) &&
1441 isl_int_abs_ge(tab->mat->row[row][1],
1442 tab->mat->row[row][0]);
1454 int isl_tab_min_at_most_neg_one(struct isl_tab *tab, struct isl_tab_var *var)
1459 if (min_is_manifestly_unbounded(tab, var))
1463 row = pivot_row(tab, NULL, -1, col);
1464 pivot_var = var_from_col(tab, col);
1465 if (isl_tab_pivot(tab, row, col) < 0)
1469 if (row_at_most_neg_one(tab, var->index)) {
1473 if (isl_tab_pivot(tab, row, col) < 0)
1476 if (restore_row(tab, var) < -1)
1485 find_pivot(tab, var, var, -1, &row, &col);
1487 if (var->is_nonneg && restore_row(tab, var) < -1)
1493 pivot_var = var_from_col(tab, col);
1494 if (isl_tab_pivot(tab, row, col) < 0)
1498 } while (!row_at_most_neg_one(tab, var->index));
1502 if (isl_tab_pivot(tab, row, col) < 0)
1504 if (restore_row(tab, var) < -1)
1513 static int at_least_one(struct isl_tab *tab, struct isl_tab_var *var)
1518 if (max_is_manifestly_unbounded(tab, var))
1520 if (to_row(tab, var, 1) < 0)
1522 r = tab->mat->row[var->index];
1524 find_pivot(tab, var, var, 1, &row, &col);
1529 if (isl_tab_pivot(tab, row, col) < 0)
1535 static void swap_cols(struct isl_tab *tab, int col1, int col2)
1538 unsigned off = 2 + tab->M;
1539 t = tab->col_var[col1];
1540 tab->col_var[col1] = tab->col_var[col2];
1541 tab->col_var[col2] = t;
1542 var_from_col(tab, col1)->index = col1;
1543 var_from_col(tab, col2)->index = col2;
1544 tab->mat = isl_mat_swap_cols(tab->mat, off + col1, off + col2);
1559 int isl_tab_kill_col(struct isl_tab *tab, int col)
1561 var_from_col(tab, col)->is_zero = 1;
1562 if (tab->need_undo) {
1563 if (isl_tab_push_var(tab, isl_tab_undo_zero,
1564 var_from_col(tab, col)) < 0)
1566 if (col != tab->n_dead)
1567 swap_cols(tab, col, tab->n_dead);
1568 tab->n_dead++;
1571 if (col != tab->n_col - 1)
1572 swap_cols(tab, col, tab->n_col - 1);
1573 var_from_col(tab, tab->n_col - 1)->index = -1;
1574 tab->n_col--;
1579 static int row_is_manifestly_non_integral(struct isl_tab *tab, int row)
1581 unsigned off = 2 + tab->M;
1583 if (tab->M && !isl_int_eq(tab->mat->row[row][2],
1584 tab->mat->row[row][0]))
1586 if (isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
1587 tab->n_col - tab->n_dead) != -1)
1590 return !isl_int_is_divisible_by(tab->mat->row[row][1],
1591 tab->mat->row[row][0]);
1597 static int tab_is_manifestly_empty(struct isl_tab *tab)
1601 if (tab->empty)
1603 if (tab->rational)
1606 for (i = 0; i < tab->n_var; ++i) {
1607 if (!tab->var[i].is_row)
1609 if (row_is_manifestly_non_integral(tab, tab->var[i].index))
1633 static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var,
1635 static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var,
1639 struct isl_mat *mat = tab->mat;
1640 unsigned off = 2 + tab->M;
1643 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1647 if (!temp_var && tab->need_undo)
1648 if (isl_tab_push_var(tab, isl_tab_undo_zero, var) < 0)
1650 for (j = tab->n_dead; j < tab->n_col; ++j) {
1655 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1658 recheck = isl_tab_kill_col(tab, j);
1664 if (!temp_var && isl_tab_mark_redundant(tab, var->index) < 0)
1666 if (tab_is_manifestly_empty(tab) && isl_tab_mark_empty(tab) < 0)
1677 int isl_tab_allocate_con(struct isl_tab *tab)
1681 isl_assert(tab->mat->ctx, tab->n_row < tab->mat->n_row, return -1);
1682 isl_assert(tab->mat->ctx, tab->n_con < tab->max_con, return -1);
1684 r = tab->n_con;
1685 tab->con[r].index = tab->n_row;
1686 tab->con[r].is_row = 1;
1687 tab->con[r].is_nonneg = 0;
1688 tab->con[r].is_zero = 0;
1689 tab->con[r].is_redundant = 0;
1690 tab->con[r].frozen = 0;
1691 tab->con[r].negated = 0;
1692 tab->row_var[tab->n_row] = ~r;
1694 tab->n_row++;
1695 tab->n_con++;
1696 if (isl_tab_push_var(tab, isl_tab_undo_allocate, &tab->con[r]) < 0)
1702 /* Move the entries in tab->var up one position, starting at "first",
1704 * Since some of the entries of tab->row_var and tab->col_var contain
1707 static int var_insert_entry(struct isl_tab *tab, int first)
1711 if (tab->n_var >= tab->max_var)
1712 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1714 if (first > tab->n_var)
1715 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1718 for (i = tab->n_var - 1; i >= first; --i) {
1719 tab->var[i + 1] = tab->var[i];
1720 if (tab->var[i + 1].is_row)
1721 tab->row_var[tab->var[i + 1].index]++;
1723 tab->col_var[tab->var[i + 1].index]++;
1726 tab->n_var++;
1731 /* Drop the entry at position "first" in tab->var, moving all
1733 * Since some of the entries of tab->row_var and tab->col_var contain
1736 static int var_drop_entry(struct isl_tab *tab, int first)
1740 if (first >= tab->n_var)
1741 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
1744 tab->n_var--;
1746 for (i = first; i < tab->n_var; ++i) {
1747 tab->var[i] = tab->var[i + 1];
1748 if (tab->var[i + 1].is_row)
1749 tab->row_var[tab->var[i].index]--;
1751 tab->col_var[tab->var[i].index]--;
1761 int isl_tab_insert_var(struct isl_tab *tab, int r)
1764 unsigned off = 2 + tab->M;
1766 isl_assert(tab->mat->ctx, tab->n_col < tab->mat->n_col, return -1);
1768 if (var_insert_entry(tab, r) < 0)
1771 tab->var[r].index = tab->n_col;
1772 tab->var[r].is_row = 0;
1773 tab->var[r].is_nonneg = 0;
1774 tab->var[r].is_zero = 0;
1775 tab->var[r].is_redundant = 0;
1776 tab->var[r].frozen = 0;
1777 tab->var[r].negated = 0;
1778 tab->col_var[tab->n_col] = r;
1780 for (i = 0; i < tab->n_row; ++i)
1781 isl_int_set_si(tab->mat->row[i][off + tab->n_col], 0);
1783 tab->n_col++;
1784 if (isl_tab_push_var(tab, isl_tab_undo_allocate, &tab->var[r]) < 0)
1809 * If tab->M is set, then, internally, each variable x is represented
1812 int isl_tab_add_row(struct isl_tab *tab, isl_int *line)
1818 unsigned off = 2 + tab->M;
1820 r = isl_tab_allocate_con(tab);
1826 row = tab->mat->row[tab->con[r].index];
1829 isl_seq_clr(row + 2, tab->M + tab->n_col);
1830 for (i = 0; i < tab->n_var; ++i) {
1831 if (tab->var[i].is_zero)
1833 if (tab->var[i].is_row) {
1835 row[0], tab->mat->row[tab->var[i].index][0]);
1839 row[0], tab->mat->row[tab->var[i].index][0]);
1842 b, tab->mat->row[tab->var[i].index] + 1,
1843 1 + tab->M + tab->n_col);
1845 isl_int_addmul(row[off + tab->var[i].index],
1847 if (tab->M && i >= tab->n_param && i < tab->n_var - tab->n_div)
1850 isl_seq_normalize(tab->mat->ctx, row, off + tab->n_col);
1854 if (tab->row_sign)
1855 tab->row_sign[tab->con[r].index] = isl_tab_row_unknown;
1860 static isl_stat drop_row(struct isl_tab *tab, int row)
1862 isl_assert(tab->mat->ctx, ~tab->row_var[row] == tab->n_con - 1,
1864 if (row != tab->n_row - 1)
1865 swap_rows(tab, row, tab->n_row - 1);
1866 tab->n_row--;
1867 tab->n_con--;
1877 static isl_stat drop_col(struct isl_tab *tab, int col)
1881 var = tab->col_var[col];
1882 if (col != tab->n_col - 1)
1883 swap_cols(tab, col, tab->n_col - 1);
1884 tab->n_col--;
1885 if (var_drop_entry(tab, var) < 0)
1896 isl_stat isl_tab_add_ineq(struct isl_tab *tab, isl_int *ineq)
1902 if (!tab)
1904 if (tab->bmap) {
1905 struct isl_basic_map *bmap = tab->bmap;
1907 isl_assert(tab->mat->ctx, tab->n_eq == bmap->n_eq,
1909 isl_assert(tab->mat->ctx,
1910 tab->n_con == bmap->n_eq + bmap->n_ineq,
1912 tab->bmap = isl_basic_map_add_ineq(tab->bmap, ineq);
1913 if (isl_tab_push(tab, isl_tab_undo_bmap_ineq) < 0)
1915 if (!tab->bmap)
1918 if (tab->cone) {
1923 r = isl_tab_add_row(tab, ineq);
1924 if (tab->cone) {
1930 tab->con[r].is_nonneg = 1;
1931 if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0)
1933 if (isl_tab_row_is_redundant(tab, tab->con[r].index)) {
1934 if (isl_tab_mark_redundant(tab, tab->con[r].index) < 0)
1939 sgn = restore_row(tab, &tab->con[r]);
1943 return isl_tab_mark_empty(tab);
1944 if (tab->con[r].is_row && isl_tab_row_is_redundant(tab, tab->con[r].index))
1945 if (isl_tab_mark_redundant(tab, tab->con[r].index) < 0)
1953 static int to_col(struct isl_tab *tab, struct isl_tab_var *var) WARN_UNUSED;
1954 static int to_col(struct isl_tab *tab, struct isl_tab_var *var)
1958 unsigned off = 2 + tab->M;
1963 while (isl_int_is_pos(tab->mat->row[var->index][1])) {
1964 find_pivot(tab, var, NULL, -1, &row, &col);
1965 isl_assert(tab->mat->ctx, row != -1, return -1);
1966 if (isl_tab_pivot(tab, row, col) < 0)
1972 for (i = tab->n_dead; i < tab->n_col; ++i)
1973 if (!isl_int_is_zero(tab->mat->row[var->index][off + i]))
1976 isl_assert(tab->mat->ctx, i < tab->n_col, return -1);
1977 if (isl_tab_pivot(tab, var->index, i) < 0)
1991 static struct isl_tab *add_eq(struct isl_tab *tab, isl_int *eq)
1996 if (!tab)
1998 r = isl_tab_add_row(tab, eq);
2002 r = tab->con[r].index;
2003 i = isl_seq_first_non_zero(tab->mat->row[r] + 2 + tab->M + tab->n_dead,
2004 tab->n_col - tab->n_dead);
2005 isl_assert(tab->mat->ctx, i >= 0, goto error);
2006 i += tab->n_dead;
2007 if (isl_tab_pivot(tab, r, i) < 0)
2009 if (isl_tab_kill_col(tab, i) < 0)
2011 tab->n_eq++;
2013 return tab;
2015 isl_tab_free(tab);
2019 /* Does the sample value of row "row" of "tab" involve the big parameter,
2022 static int row_is_big(struct isl_tab *tab, int row)
2024 return tab->M && !isl_int_is_zero(tab->mat->row[row][2]);
2027 static int row_is_manifestly_zero(struct isl_tab *tab, int row)
2029 unsigned off = 2 + tab->M;
2031 if (!isl_int_is_zero(tab->mat->row[row][1]))
2033 if (row_is_big(tab, row))
2035 return isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
2036 tab->n_col - tab->n_dead) == -1;
2044 int isl_tab_add_valid_eq(struct isl_tab *tab, isl_int *eq)
2049 if (!tab)
2051 r = isl_tab_add_row(tab, eq);
2055 var = &tab->con[r];
2057 if (row_is_manifestly_zero(tab, r)) {
2059 if (isl_tab_mark_redundant(tab, r) < 0)
2064 if (isl_int_is_neg(tab->mat->row[r][1])) {
2065 isl_seq_neg(tab->mat->row[r] + 1, tab->mat->row[r] + 1,
2066 1 + tab->n_col);
2070 if (to_col(tab, var) < 0)
2073 if (isl_tab_kill_col(tab, var->index) < 0)
2079 /* Add a zero row to "tab" and return the corresponding index
2085 static int add_zero_row(struct isl_tab *tab)
2090 r = isl_tab_allocate_con(tab);
2094 row = tab->mat->row[tab->con[r].index];
2095 isl_seq_clr(row + 1, 1 + tab->M + tab->n_col);
2106 * If tab->bmap is set, then two rows are needed instead of one.
2108 isl_stat isl_tab_add_eq(struct isl_tab *tab, isl_int *eq)
2117 if (!tab)
2119 isl_assert(tab->mat->ctx, !tab->M, return isl_stat_error);
2121 if (tab->need_undo)
2122 snap = isl_tab_snap(tab);
2124 if (tab->cone) {
2129 r = isl_tab_add_row(tab, eq);
2130 if (tab->cone) {
2137 var = &tab->con[r];
2139 if (row_is_manifestly_zero(tab, row)) {
2141 return isl_tab_rollback(tab, snap);
2142 return drop_row(tab, row);
2145 if (tab->bmap) {
2146 tab->bmap = isl_basic_map_add_ineq(tab->bmap, eq);
2147 if (isl_tab_push(tab, isl_tab_undo_bmap_ineq) < 0)
2149 isl_seq_neg(eq, eq, 1 + tab->n_var);
2150 tab->bmap = isl_basic_map_add_ineq(tab->bmap, eq);
2151 isl_seq_neg(eq, eq, 1 + tab->n_var);
2152 if (isl_tab_push(tab, isl_tab_undo_bmap_ineq) < 0)
2154 if (!tab->bmap)
2156 if (add_zero_row(tab) < 0)
2160 sgn = isl_int_sgn(tab->mat->row[row][1]);
2163 isl_seq_neg(tab->mat->row[row] + 1, tab->mat->row[row] + 1,
2164 1 + tab->n_col);
2170 sgn = sign_of_max(tab, var);
2174 if (isl_tab_mark_empty(tab) < 0)
2181 if (to_col(tab, var) < 0)
2184 if (isl_tab_kill_col(tab, var->index) < 0)
2237 static isl_stat add_div_constraints(struct isl_tab *tab, unsigned div,
2244 total = isl_basic_map_dim(tab->bmap, isl_dim_all);
2247 div_pos = 1 + total - tab->bmap->n_div + div;
2249 ineq = ineq_for_div(tab->bmap, div);
2257 if (isl_tab_add_ineq(tab, ineq->el) < 0)
2261 isl_seq_neg(ineq->el, tab->bmap->div[div] + 1, 1 + total);
2262 isl_int_set(ineq->el[div_pos], tab->bmap->div[div][0]);
2270 if (isl_tab_add_ineq(tab, ineq->el) < 0)
2288 static int div_is_nonneg(struct isl_tab *tab, __isl_keep isl_vec *div)
2292 if (tab->M)
2298 for (i = 0; i < tab->n_var; ++i) {
2303 if (!tab->var[i].is_nonneg)
2321 int isl_tab_insert_div(struct isl_tab *tab, int pos, __isl_keep isl_vec *div,
2329 if (!tab || !div)
2332 if (div->size != 1 + 1 + tab->n_var)
2333 isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
2336 n_div = isl_basic_map_dim(tab->bmap, isl_dim_div);
2339 o_div = tab->n_var - n_div;
2340 if (pos < o_div || pos > tab->n_var)
2341 isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
2344 nonneg = div_is_nonneg(tab, div);
2346 if (isl_tab_extend_cons(tab, 3) < 0)
2348 if (isl_tab_extend_vars(tab, 1) < 0)
2350 r = isl_tab_insert_var(tab, pos);
2355 tab->var[r].is_nonneg = 1;
2357 tab->bmap = isl_basic_map_insert_div(tab->bmap, pos - o_div, div);
2358 if (!tab->bmap)
2360 if (isl_tab_push_var(tab, isl_tab_undo_bmap_div, &tab->var[r]) < 0)
2363 if (add_div_constraints(tab, pos - o_div, add_ineq, user) < 0)
2372 int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div)
2374 if (!tab)
2376 return isl_tab_insert_div(tab, tab->n_var, div, NULL, NULL);
2379 /* If "track" is set, then we want to keep track of all constraints in tab
2382 * in the constructed tab.
2388 struct isl_tab *tab;
2394 tab = isl_tab_alloc(bmap->ctx, total + bmap->n_ineq + 1, total, 0);
2395 if (!tab)
2397 tab->preserve = track;
2398 tab->rational = ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL);
2400 if (isl_tab_mark_empty(tab) < 0)
2405 tab = add_eq(tab, bmap->eq[i]);
2406 if (!tab)
2407 return tab;
2410 if (isl_tab_add_ineq(tab, bmap->ineq[i]) < 0)
2412 if (tab->empty)
2416 if (track && isl_tab_track_bmap(tab, isl_basic_map_copy(bmap)) < 0)
2418 return tab;
2420 isl_tab_free(tab);
2437 struct isl_tab *tab;
2446 tab = isl_tab_alloc(bset->ctx, bset->n_eq + bset->n_ineq,
2448 if (!tab)
2450 tab->rational = ISL_F_ISSET(bset, ISL_BASIC_SET_RATIONAL);
2451 tab->cone = 1;
2458 if (isl_tab_add_eq(tab, bset->eq[i] + offset) < 0)
2461 tab = add_eq(tab, bset->eq[i]);
2463 if (!tab)
2469 r = isl_tab_add_row(tab, bset->ineq[i] + offset);
2473 tab->con[r].is_nonneg = 1;
2474 if (isl_tab_push_var(tab, isl_tab_undo_nonneg, &tab->con[r]) < 0)
2479 return tab;
2482 isl_tab_free(tab);
2486 /* Assuming "tab" is the tableau of a cone, check if the cone is
2489 isl_bool isl_tab_cone_is_bounded(struct isl_tab *tab)
2493 if (!tab)
2495 if (tab->empty)
2497 if (tab->n_dead == tab->n_col)
2501 for (i = tab->n_redundant; i < tab->n_row; ++i) {
2504 var = isl_tab_var_from_row(tab, i);
2507 sgn = sign_of_max(tab, var);
2512 if (close_row(tab, var, 0) < 0)
2516 if (tab->n_dead == tab->n_col)
2518 if (i == tab->n_row)
2523 int isl_tab_sample_is_integer(struct isl_tab *tab)
2527 if (!tab)
2530 for (i = 0; i < tab->n_var; ++i) {
2532 if (!tab->var[i].is_row)
2534 row = tab->var[i].index;
2535 if (!isl_int_is_divisible_by(tab->mat->row[row][1],
2536 tab->mat->row[row][0]))
2542 static struct isl_vec *extract_integer_sample(struct isl_tab *tab)
2547 vec = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_var);
2552 for (i = 0; i < tab->n_var; ++i) {
2553 if (!tab->var[i].is_row)
2556 int row = tab->var[i].index;
2558 tab->mat->row[row][1], tab->mat->row[row][0]);
2565 __isl_give isl_vec *isl_tab_get_sample_value(struct isl_tab *tab)
2571 if (!tab)
2574 vec = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_var);
2581 for (i = 0; i < tab->n_var; ++i) {
2583 if (!tab->var[i].is_row) {
2587 row = tab->var[i].index;
2588 isl_int_gcd(m, vec->block.data[0], tab->mat->row[row][0]);
2589 isl_int_divexact(m, tab->mat->row[row][0], m);
2591 isl_int_divexact(m, vec->block.data[0], tab->mat->row[row][0]);
2592 isl_int_mul(vec->block.data[1 + i], m, tab->mat->row[row][1]);
2600 /* Store the sample value of "var" of "tab" rounded up (if sgn > 0)
2603 static void get_rounded_sample_value(struct isl_tab *tab,
2609 isl_int_cdiv_q(*v, tab->mat->row[var->index][1],
2610 tab->mat->row[var->index][0]);
2612 isl_int_fdiv_q(*v, tab->mat->row[var->index][1],
2613 tab->mat->row[var->index][0]);
2616 /* Update "bmap" based on the results of the tableau "tab".
2625 __isl_take isl_basic_map *bmap, struct isl_tab *tab)
2632 if (!tab)
2635 n_eq = tab->n_eq;
2636 if (tab->empty)
2640 if (isl_tab_is_equality(tab, n_eq + i))
2642 else if (isl_tab_is_redundant(tab, n_eq + i))
2647 if (!tab->rational &&
2648 bmap && !bmap->sample && isl_tab_sample_is_integer(tab))
2649 bmap->sample = extract_integer_sample(tab);
2654 __isl_take isl_basic_set *bset, struct isl_tab *tab)
2657 tab));
2660 /* Drop the last constraint added to "tab" in position "r".
2663 static isl_stat drop_last_con_in_row(struct isl_tab *tab, int r)
2665 if (!tab->con[r].is_row)
2666 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
2669 if (r + 1 != tab->n_con)
2670 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
2672 if (drop_row(tab, tab->con[r].index) < 0)
2688 static isl_stat cut_to_hyperplane(struct isl_tab *tab, struct isl_tab_var *var)
2693 unsigned off = 2 + tab->M;
2698 isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
2702 if (isl_tab_extend_cons(tab, 1) < 0)
2705 r = tab->n_con;
2706 tab->con[r].index = tab->n_row;
2707 tab->con[r].is_row = 1;
2708 tab->con[r].is_nonneg = 0;
2709 tab->con[r].is_zero = 0;
2710 tab->con[r].is_redundant = 0;
2711 tab->con[r].frozen = 0;
2712 tab->con[r].negated = 0;
2713 tab->row_var[tab->n_row] = ~r;
2714 row = tab->mat->row[tab->n_row];
2717 isl_int_set(row[0], tab->mat->row[var->index][0]);
2719 tab->mat->row[var->index] + 1, 1 + tab->n_col);
2722 isl_seq_clr(row + 1, 1 + tab->n_col);
2726 tab->n_row++;
2727 tab->n_con++;
2729 sgn = sign_of_max(tab, &tab->con[r]);
2733 if (drop_last_con_in_row(tab, r) < 0)
2735 if (isl_tab_mark_empty(tab) < 0)
2739 tab->con[r].is_nonneg = 1;
2741 if (close_row(tab, &tab->con[r], 1) < 0)
2743 if (drop_last_con_in_row(tab, r) < 0)
2749 /* Check that "con" is a valid constraint position for "tab".
2751 static isl_stat isl_tab_check_con(struct isl_tab *tab, int con)
2753 if (!tab)
2755 if (con < 0 || con >= tab->n_con)
2756 isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
2761 /* Given a tableau "tab" and an inequality constraint "con" of the tableau,
2778 int isl_tab_relax(struct isl_tab *tab, int con)
2782 if (!tab)
2785 var = &tab->con[con];
2787 if (var->is_row && (var->index < 0 || var->index < tab->n_redundant))
2788 isl_die(tab->mat->ctx, isl_error_invalid,
2790 if (!var->is_row && (var->index < 0 || var->index < tab->n_dead))
2791 isl_die(tab->mat->ctx, isl_error_invalid,
2794 if (!var->is_row && !max_is_manifestly_unbounded(tab, var))
2795 if (to_row(tab, var, 1) < 0)
2797 if (!var->is_row && !min_is_manifestly_unbounded(tab, var))
2798 if (to_row(tab, var, -1) < 0)
2802 isl_int_add(tab->mat->row[var->index][1],
2803 tab->mat->row[var->index][1], tab->mat->row[var->index][0]);
2804 if (restore_row(tab, var) < 0)
2808 unsigned off = 2 + tab->M;
2810 for (i = 0; i < tab->n_row; ++i) {
2811 if (isl_int_is_zero(tab->mat->row[i][off + var->index]))
2813 isl_int_sub(tab->mat->row[i][1], tab->mat->row[i][1],
2814 tab->mat->row[i][off + var->index]);
2819 if (isl_tab_push_var(tab, isl_tab_undo_relax, var) < 0)
2825 /* Replace the variable v at position "pos" in the tableau "tab"
2842 int isl_tab_shift_var(struct isl_tab *tab, int pos, isl_int shift)
2846 if (!tab)
2851 var = &tab->var[pos];
2854 if (!max_is_manifestly_unbounded(tab, var))
2855 if (to_row(tab, var, 1) < 0)
2858 if (!min_is_manifestly_unbounded(tab, var))
2859 if (to_row(tab, var, -1) < 0)
2865 isl_int_addmul(tab->mat->row[var->index][1],
2866 shift, tab->mat->row[var->index][0]);
2869 unsigned off = 2 + tab->M;
2871 for (i = 0; i < tab->n_row; ++i) {
2872 if (isl_int_is_zero(tab->mat->row[i][off + var->index]))
2874 isl_int_submul(tab->mat->row[i][1],
2875 shift, tab->mat->row[i][off + var->index]);
2888 int isl_tab_unrestrict(struct isl_tab *tab, int con)
2892 if (!tab)
2895 var = &tab->con[con];
2900 if (isl_tab_push_var(tab, isl_tab_undo_unrestrict, var) < 0)
2906 int isl_tab_select_facet(struct isl_tab *tab, int con)
2908 if (!tab)
2911 return cut_to_hyperplane(tab, &tab->con[con]);
2914 static int may_be_equality(struct isl_tab *tab, int row)
2916 return tab->rational ? isl_int_is_zero(tab->mat->row[row][1])
2917 : isl_int_lt(tab->mat->row[row][1],
2918 tab->mat->row[row][0]);
2929 * an implicit equality, there is no need to return any tab variable that
2932 static struct isl_tab_var *select_marked(struct isl_tab *tab)
2937 for (i = tab->n_con - 1; i >= 0; --i) {
2938 var = &tab->con[i];
2941 if (var->is_row && var->index < tab->n_redundant)
2943 if (!var->is_row && var->index < tab->n_dead)
2969 int isl_tab_detect_implicit_equalities(struct isl_tab *tab)
2974 if (!tab)
2976 if (tab->empty)
2978 if (tab->n_dead == tab->n_col)
2982 for (i = tab->n_redundant; i < tab->n_row; ++i) {
2983 struct isl_tab_var *var = isl_tab_var_from_row(tab, i);
2985 may_be_equality(tab, i);
2989 for (i = tab->n_dead; i < tab->n_col; ++i) {
2990 struct isl_tab_var *var = var_from_col(tab, i);
2998 var = select_marked(tab);
3003 sgn = sign_of_max(tab, var);
3007 if (close_row(tab, var, 0) < 0)
3009 } else if (!tab->rational && !at_least_one(tab, var)) {
3010 if (cut_to_hyperplane(tab, var) < 0)
3012 return isl_tab_detect_implicit_equalities(tab);
3014 for (i = tab->n_redundant; i < tab->n_row; ++i) {
3015 var = isl_tab_var_from_row(tab, i);
3018 if (may_be_equality(tab, i))
3029 * constraint tab->con[i] to a move from position "old" to position "i".
3031 static int update_con_after_move(struct isl_tab *tab, int i, int old)
3036 index = tab->con[i].index;
3039 p = tab->con[i].is_row ? tab->row_var : tab->col_var;
3041 isl_die(tab->mat->ctx, isl_error_internal,
3048 /* Interchange constraints "con1" and "con2" in "tab".
3049 * In particular, interchange the contents of these entries in tab->con.
3050 * Since tab->col_var and tab->row_var point back into this array,
3053 isl_stat isl_tab_swap_constraints(struct isl_tab *tab, int con1, int con2)
3057 if (isl_tab_check_con(tab, con1) < 0 ||
3058 isl_tab_check_con(tab, con2) < 0)
3061 var = tab->con[con1];
3062 tab->con[con1] = tab->con[con2];
3063 if (update_con_after_move(tab, con1, con2) < 0)
3065 tab->con[con2] = var;
3066 if (update_con_after_move(tab, con2, con1) < 0)
3075 static int rotate_constraints(struct isl_tab *tab, int first, int n)
3084 var = tab->con[last];
3086 tab->con[i] = tab->con[i - 1];
3087 if (update_con_after_move(tab, i, i - 1) < 0)
3090 tab->con[first] = var;
3091 if (update_con_after_move(tab, first, last) < 0)
3097 /* Drop the "n" entries starting at position "first" in tab->con, moving all
3099 * Since some of the entries of tab->row_var and tab->col_var contain
3102 static isl_stat con_drop_entries(struct isl_tab *tab,
3107 if (first + n > tab->n_con || first + n < first)
3108 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
3111 tab->n_con -= n;
3113 for (i = first; i < tab->n_con; ++i) {
3114 tab->con[i] = tab->con[i + n];
3115 if (update_con_after_move(tab, i, i + n) < 0)
3124 * in the basic map. Perform the same interchange in "tab".
3128 struct isl_tab *tab = user;
3130 return isl_tab_swap_constraints(tab, a, b);
3138 * Drop the same number of equality constraints from "tab" or
3143 struct isl_tab *tab = user;
3145 if (tab->n_eq == n)
3146 return isl_tab_mark_empty(tab);
3148 tab->n_eq -= n;
3149 return con_drop_entries(tab, tab->n_eq, n);
3153 * isl_basic_map_gauss on it, updating "tab" accordingly.
3156 struct isl_tab *tab)
3165 return isl_basic_map_gauss5(bmap, NULL, &swap_eq, &drop_eq, tab);
3169 * detected in the corresponding "tab" explicit in "bmap" and update
3170 * "tab" to reflect the new order of the constraints.
3191 * If "tab" contains any constraints that are not in "bmap" then they
3201 __isl_give isl_basic_map *isl_tab_make_equalities_explicit(struct isl_tab *tab,
3207 if (!tab || !bmap)
3209 if (tab->empty)
3212 n_eq = tab->n_eq;
3214 if (!isl_tab_is_equality(tab, bmap->n_eq + i))
3217 if (rotate_constraints(tab, 0, tab->n_eq + i + 1) < 0)
3219 if (rotate_constraints(tab, tab->n_eq + i + 1,
3222 tab->n_eq++;
3225 if (n_eq != tab->n_eq)
3226 bmap = gauss_if_shared(bmap, tab);
3231 static int con_is_redundant(struct isl_tab *tab, struct isl_tab_var *var)
3233 if (!tab)
3235 if (tab->rational) {
3236 int sgn = sign_of_min(tab, var);
3241 int irred = isl_tab_min_at_most_neg_one(tab, var);
3261 int isl_tab_detect_redundant(struct isl_tab *tab)
3266 if (!tab)
3268 if (tab->empty)
3270 if (tab->n_redundant == tab->n_row)
3274 for (i = tab->n_redundant; i < tab->n_row; ++i) {
3275 struct isl_tab_var *var = isl_tab_var_from_row(tab, i);
3280 for (i = tab->n_dead; i < tab->n_col; ++i) {
3281 struct isl_tab_var *var = var_from_col(tab, i);
3283 !min_is_manifestly_unbounded(tab, var);
3290 var = select_marked(tab);
3295 red = con_is_redundant(tab, var);
3299 if (isl_tab_mark_redundant(tab, var->index) < 0)
3301 for (i = tab->n_dead; i < tab->n_col; ++i) {
3302 var = var_from_col(tab, i);
3305 if (!min_is_manifestly_unbounded(tab, var))
3315 int isl_tab_is_equality(struct isl_tab *tab, int con)
3320 if (!tab)
3322 if (tab->con[con].is_zero)
3324 if (tab->con[con].is_redundant)
3326 if (!tab->con[con].is_row)
3327 return tab->con[con].index < tab->n_dead;
3329 row = tab->con[con].index;
3331 off = 2 + tab->M;
3332 return isl_int_is_zero(tab->mat->row[row][1]) &&
3333 !row_is_big(tab, row) &&
3334 isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
3335 tab->n_col - tab->n_dead) == -1;
3348 enum isl_lp_result isl_tab_min(struct isl_tab *tab,
3357 if (!tab)
3360 if (tab->empty)
3363 snap = isl_tab_snap(tab);
3364 r = isl_tab_add_row(tab, f);
3367 var = &tab->con[r];
3370 find_pivot(tab, var, var, -1, &row, &col);
3377 if (isl_tab_pivot(tab, row, col) < 0)
3380 isl_int_mul(tab->mat->row[var->index][0],
3381 tab->mat->row[var->index][0], denom);
3385 isl_vec_free(tab->dual);
3386 tab->dual = isl_vec_alloc(tab->mat->ctx, 1 + tab->n_con);
3387 if (!tab->dual)
3389 isl_int_set(tab->dual->el[0], tab->mat->row[var->index][0]);
3390 for (i = 0; i < tab->n_con; ++i) {
3392 if (tab->con[i].is_row) {
3393 isl_int_set_si(tab->dual->el[1 + i], 0);
3396 pos = 2 + tab->M + tab->con[i].index;
3397 if (tab->con[i].negated)
3398 isl_int_neg(tab->dual->el[1 + i],
3399 tab->mat->row[var->index][pos]);
3401 isl_int_set(tab->dual->el[1 + i],
3402 tab->mat->row[var->index][pos]);
3407 isl_int_set(*opt, tab->mat->row[var->index][1]);
3408 isl_int_set(*opt_denom, tab->mat->row[var->index][0]);
3410 get_rounded_sample_value(tab, var, 1, opt);
3412 if (isl_tab_rollback(tab, snap) < 0)
3422 * tab->n_redundant positions (or removes the row, assigning it index -1),
3425 int isl_tab_is_redundant(struct isl_tab *tab, int con)
3427 if (isl_tab_check_con(tab, con) < 0)
3429 if (tab->con[con].is_zero)
3431 if (tab->con[con].is_redundant)
3433 return tab->con[con].is_row && tab->con[con].index < tab->n_redundant;
3436 /* Is variable "var" of "tab" fixed to a constant value by its row
3444 static isl_bool is_constant(struct isl_tab *tab, struct isl_tab_var *var,
3447 unsigned off = 2 + tab->M;
3448 isl_mat *mat = tab->mat;
3456 if (row_is_big(tab, row))
3458 n = tab->n_col - tab->n_dead;
3459 pos = isl_seq_first_non_zero(mat->row[row] + off + tab->n_dead, n);
3467 /* Has the variable "var' of "tab" reached a value that is greater than
3477 static int reached(struct isl_tab *tab, struct isl_tab_var *var, int sgn,
3480 if (row_is_big(tab, var->index))
3482 isl_int_mul(*tmp, tab->mat->row[var->index][0], target);
3484 return isl_int_ge(tab->mat->row[var->index][1], *tmp);
3486 return isl_int_le(tab->mat->row[var->index][1], *tmp);
3489 /* Can variable "var" of "tab" attain the value "target" by
3505 static isl_bool var_reaches(struct isl_tab *tab, struct isl_tab_var *var,
3510 if (sgn < 0 && min_is_manifestly_unbounded(tab, var))
3512 if (sgn > 0 && max_is_manifestly_unbounded(tab, var))
3514 if (to_row(tab, var, sgn) < 0)
3516 while (!reached(tab, var, sgn, target, tmp)) {
3517 find_pivot(tab, var, var, sgn, &row, &col);
3522 if (isl_tab_pivot(tab, row, col) < 0)
3529 /* Check if variable "var" of "tab" can only attain a single (integer)
3548 static isl_bool detect_constant_with_tmp(struct isl_tab *tab,
3556 get_rounded_sample_value(tab, var, -1, target);
3558 reached = var_reaches(tab, var, -1, *target, tmp);
3561 get_rounded_sample_value(tab, var, 1, target);
3563 reached = var_reaches(tab, var, 1, *target, tmp);
3566 get_rounded_sample_value(tab, var, -1, tmp);
3569 if (isl_tab_mark_empty(tab) < 0)
3574 if (isl_tab_extend_cons(tab, 1) < 0)
3576 eq = isl_vec_alloc(isl_tab_get_ctx(tab), 1 + tab->n_var);
3579 pos = var - tab->var;
3580 isl_seq_clr(eq->el + 1, tab->n_var);
3583 r = isl_tab_add_eq(tab, eq->el);
3589 /* Check if variable "var" of "tab" can only attain a single (integer)
3602 static isl_bool get_constant(struct isl_tab *tab, struct isl_tab_var *var,
3608 if (var->is_row && row_is_big(tab, var->index))
3610 is_cst = is_constant(tab, var, value);
3618 is_cst = detect_constant_with_tmp(tab, var,
3628 /* Check if variable "var" of "tab" can only attain a single (integer)
3635 isl_bool isl_tab_is_constant(struct isl_tab *tab, int var, isl_int *value)
3637 if (!tab)
3639 if (var < 0 || var >= tab->n_var)
3640 isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
3642 if (tab->rational)
3645 return get_constant(tab, &tab->var[var], value);
3648 /* Check if any of the variables of "tab" can only attain a single (integer)
3654 isl_stat isl_tab_detect_constants(struct isl_tab *tab)
3658 if (!tab)
3660 if (tab->rational)
3663 for (i = 0; i < tab->n_var; ++i) {
3664 if (get_constant(tab, &tab->var[i], NULL) < 0)
3674 struct isl_tab_undo *isl_tab_snap(struct isl_tab *tab)
3676 if (!tab)
3678 tab->need_undo = 1;
3679 return tab->top;
3682 /* Does "tab" need to keep track of undo information?
3685 isl_bool isl_tab_need_undo(struct isl_tab *tab)
3687 if (!tab)
3690 return isl_bool_ok(tab->need_undo);
3693 /* Remove all tracking of undo information from "tab", invalidating
3698 void isl_tab_clear_undo(struct isl_tab *tab)
3700 if (!tab)
3703 free_undo(tab);
3704 tab->need_undo = 0;
3709 static isl_stat unrelax(struct isl_tab *tab, struct isl_tab_var *var)
3711 static isl_stat unrelax(struct isl_tab *tab, struct isl_tab_var *var)
3713 unsigned off = 2 + tab->M;
3715 if (!var->is_row && !max_is_manifestly_unbounded(tab, var))
3716 if (to_row(tab, var, 1) < 0)
3720 isl_int_sub(tab->mat->row[var->index][1],
3721 tab->mat->row[var->index][1], tab->mat->row[var->index][0]);
3723 int sgn = restore_row(tab, var);
3724 isl_assert(tab->mat->ctx, sgn >= 0,
3730 for (i = 0; i < tab->n_row; ++i) {
3731 if (isl_int_is_zero(tab->mat->row[i][off + var->index]))
3733 isl_int_add(tab->mat->row[i][1], tab->mat->row[i][1],
3734 tab->mat->row[i][off + var->index]);
3747 static isl_stat ununrestrict(struct isl_tab *tab, struct isl_tab_var *var)
3751 if (var->is_row && restore_row(tab, var) < -1)
3757 /* Unmark the last redundant row in "tab" as being redundant.
3764 static isl_stat restore_last_redundant(struct isl_tab *tab)
3768 if (tab->n_redundant < 1)
3769 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
3772 var = isl_tab_var_from_row(tab, tab->n_redundant - 1);
3774 tab->n_redundant--;
3775 restore_row(tab, var);
3780 static isl_stat perform_undo_var(struct isl_tab *tab, struct isl_tab_undo *undo)
3782 static isl_stat perform_undo_var(struct isl_tab *tab, struct isl_tab_undo *undo)
3784 struct isl_tab_var *var = var_from_index(tab, undo->u.var_index);
3790 if (!var->is_row || var->index != tab->n_redundant - 1)
3791 isl_die(isl_tab_get_ctx(tab), isl_error_internal,
3794 return restore_last_redundant(tab);
3801 tab->n_dead--;
3805 isl_assert(tab->mat->ctx, !var->is_row,
3807 return drop_col(tab, var->index);
3810 if (!max_is_manifestly_unbounded(tab, var)) {
3811 if (to_row(tab, var, 1) < 0)
3813 } else if (!min_is_manifestly_unbounded(tab, var)) {
3814 if (to_row(tab, var, -1) < 0)
3817 if (to_row(tab, var, 0) < 0)
3820 return drop_row(tab, var->index);
3822 return unrelax(tab, var);
3824 return ununrestrict(tab, var);
3826 isl_die(tab->mat->ctx, isl_error_internal,
3841 isl_stat isl_tab_restore_redundant(struct isl_tab *tab)
3843 if (!tab)
3846 if (tab->need_undo)
3847 isl_die(isl_tab_get_ctx(tab), isl_error_invalid,
3852 while (tab->n_redundant > 0) {
3853 if (tab->row_var[tab->n_redundant - 1] >= 0) {
3856 var = isl_tab_var_from_row(tab, tab->n_redundant - 1);
3859 restore_last_redundant(tab);
3865 * of "tab" in position "pos".
3867 static isl_stat drop_bmap_div(struct isl_tab *tab, int pos)
3872 n_div = isl_basic_map_dim(tab->bmap, isl_dim_div);
3875 off = tab->n_var - n_div;
3876 tab->bmap = isl_basic_map_drop_div(tab->bmap, pos - off);
3877 if (!tab->bmap)
3879 if (tab->samples) {
3880 tab->samples = isl_mat_drop_cols(tab->samples, 1 + pos, 1);
3881 if (!tab->samples)
3899 static int restore_basis(struct isl_tab *tab, int *col_var)
3904 unsigned off = 2 + tab->M;
3906 extra = isl_alloc_array(tab->mat->ctx, int, tab->n_col);
3907 if (tab->n_col && !extra)
3909 for (i = 0; i < tab->n_col; ++i) {
3910 for (j = 0; j < tab->n_col; ++j)
3911 if (tab->col_var[i] == col_var[j])
3913 if (j < tab->n_col)
3917 for (i = 0; i < tab->n_col && n_extra > 0; ++i) {
3921 for (j = 0; j < tab->n_col; ++j)
3922 if (col_var[i] == tab->col_var[j])
3924 if (j < tab->n_col)
3926 var = var_from_index(tab, col_var[i]);
3929 if (!isl_int_is_zero(tab->mat->row[row][off+extra[j]]))
3931 isl_assert(tab->mat->ctx, j < n_extra, goto error);
3932 if (isl_tab_pivot(tab, row, extra[j]) < 0)
3948 static void drop_samples_since(struct isl_tab *tab, int n)
3952 for (i = tab->n_sample - 1; i >= 0 && tab->n_sample > n; --i) {
3953 if (tab->sample_index[i] < n)
3956 if (i != tab->n_sample - 1) {
3957 int t = tab->sample_index[tab->n_sample-1];
3958 tab->sample_index[tab->n_sample-1] = tab->sample_index[i];
3959 tab->sample_index[i] = t;
3960 isl_mat_swap_rows(tab->samples, tab->n_sample-1, i);
3962 tab->n_sample--;
3966 static isl_stat perform_undo(struct isl_tab *tab, struct isl_tab_undo *undo)
3968 static isl_stat perform_undo(struct isl_tab *tab, struct isl_tab_undo *undo)
3972 tab->rational = 0;
3975 tab->empty = 0;
3984 return perform_undo_var(tab, undo);
3986 tab->bmap = isl_basic_map_free_equality(tab->bmap, 1);
3987 return tab->bmap ? isl_stat_ok : isl_stat_error;
3989 tab->bmap = isl_basic_map_free_inequality(tab->bmap, 1);
3990 return tab->bmap ? isl_stat_ok : isl_stat_error;
3992 return drop_bmap_div(tab, undo->u.var_index);
3994 if (restore_basis(tab, undo->u.col_var) < 0)
3998 tab->n_outside--;
4001 drop_samples_since(tab, undo->u.n);
4006 isl_assert(tab->mat->ctx, 0, return isl_stat_error);
4014 isl_stat isl_tab_rollback(struct isl_tab *tab, struct isl_tab_undo *snap)
4018 if (!tab)
4021 tab->in_undo = 1;
4022 for (undo = tab->top; undo && undo != &tab->bottom; undo = next) {
4026 if (perform_undo(tab, undo) < 0) {
4027 tab->top = undo;
4028 free_undo(tab);
4029 tab->in_undo = 0;
4034 tab->in_undo = 0;
4035 tab->top = undo;
4051 static enum isl_ineq_type separation_type(struct isl_tab *tab, unsigned row)
4054 unsigned off = 2 + tab->M;
4056 if (tab->rational)
4059 if (!isl_int_is_one(tab->mat->row[row][0]))
4062 pos = isl_seq_first_non_zero(tab->mat->row[row] + off + tab->n_dead,
4063 tab->n_col - tab->n_dead);
4065 if (isl_int_is_negone(tab->mat->row[row][1]))
4071 if (!isl_int_eq(tab->mat->row[row][1],
4072 tab->mat->row[row][off + tab->n_dead + pos]))
4076 tab->mat->row[row] + off + tab->n_dead + pos + 1,
4077 tab->n_col - tab->n_dead - pos - 1);
4082 /* Check the effect of inequality "ineq" on the tableau "tab".
4090 enum isl_ineq_type isl_tab_ineq_type(struct isl_tab *tab, isl_int *ineq)
4097 if (!tab)
4100 if (isl_tab_extend_cons(tab, 1) < 0)
4103 snap = isl_tab_snap(tab);
4105 con = isl_tab_add_row(tab, ineq);
4109 row = tab->con[con].index;
4110 if (isl_tab_row_is_redundant(tab, row))
4112 else if (isl_int_is_neg(tab->mat->row[row][1]) &&
4113 (tab->rational ||
4114 isl_int_abs_ge(tab->mat->row[row][1],
4115 tab->mat->row[row][0]))) {
4116 int nonneg = at_least_zero(tab, &tab->con[con]);
4122 type = separation_type(tab, row);
4124 int red = con_is_redundant(tab, &tab->con[con]);
4133 if (isl_tab_rollback(tab, snap))
4140 isl_stat isl_tab_track_bmap(struct isl_tab *tab, __isl_take isl_basic_map *bmap)
4143 if (!tab || !bmap)
4146 if (tab->empty) {
4150 tab->bmap = bmap;
4154 isl_assert(tab->mat->ctx, tab->n_eq == bmap->n_eq, goto error);
4155 isl_assert(tab->mat->ctx,
4156 tab->n_con == bmap->n_eq + bmap->n_ineq, goto error);
4158 tab->bmap = bmap;
4166 isl_stat isl_tab_track_bset(struct isl_tab *tab, __isl_take isl_basic_set *bset)
4168 return isl_tab_track_bmap(tab, bset_to_bmap(bset));
4171 __isl_keep isl_basic_set *isl_tab_peek_bset(struct isl_tab *tab)
4173 if (!tab)
4176 return bset_from_bmap(tab->bmap);
4179 /* Print information about a tab variable representing a variable or
4194 static void isl_tab_print_internal(__isl_keep struct isl_tab *tab,
4200 if (!tab) {
4201 fprintf(out, "%*snull tab\n", indent, "");
4205 tab->n_redundant, tab->n_dead);
4206 if (tab->rational)
4208 if (tab->empty)
4212 for (i = 0; i < tab->n_var; ++i) {
4214 fprintf(out, (i == tab->n_param ||
4215 i == tab->n_var - tab->n_div) ? "; "
4217 print_tab_var(out, &tab->var[i]);
4221 for (i = 0; i < tab->n_con; ++i) {
4224 print_tab_var(out, &tab->con[i]);
4228 for (i = 0; i < tab->n_row; ++i) {
4232 if (tab->row_sign) {
4233 if (tab->row_sign[i] == isl_tab_row_unknown)
4235 else if (tab->row_sign[i] == isl_tab_row_neg)
4237 else if (tab->row_sign[i] == isl_tab_row_pos)
4242 fprintf(out, "r%d: %d%s%s", i, tab->row_var[i],
4243 isl_tab_var_from_row(tab, i)->is_nonneg ? " [>=0]" : "", sign);
4247 for (i = 0; i < tab->n_col; ++i) {
4250 fprintf(out, "c%d: %d%s", i, tab->col_var[i],
4251 var_from_col(tab, i)->is_nonneg ? " [>=0]" : "");
4254 r = tab->mat->n_row;
4255 tab->mat->n_row = tab->n_row;
4256 c = tab->mat->n_col;
4257 tab->mat->n_col = 2 + tab->M + tab->n_col;
4258 isl_mat_print_internal(tab->mat, out, indent);
4259 tab->mat->n_row = r;
4260 tab->mat->n_col = c;
4261 if (tab->bmap)
4262 isl_basic_map_print_internal(tab->bmap, out, indent);
4265 void isl_tab_dump(__isl_keep struct isl_tab *tab)
4267 isl_tab_print_internal(tab, stderr, 0);