1 1.1 mrg /* 2 1.1 mrg * Copyright 2006-2007 Universiteit Leiden 3 1.1 mrg * Copyright 2008-2009 Katholieke Universiteit Leuven 4 1.1 mrg * 5 1.1 mrg * Use of this software is governed by the MIT license 6 1.1 mrg * 7 1.1 mrg * Written by Sven Verdoolaege, Leiden Institute of Advanced Computer Science, 8 1.1 mrg * Universiteit Leiden, Niels Bohrweg 1, 2333 CA Leiden, The Netherlands 9 1.1 mrg * and K.U.Leuven, Departement Computerwetenschappen, Celestijnenlaan 200A, 10 1.1 mrg * B-3001 Leuven, Belgium 11 1.1 mrg */ 12 1.1 mrg 13 1.1 mrg #include <stdlib.h> 14 1.1 mrg #include <isl_ctx_private.h> 15 1.1 mrg #include <isl_map_private.h> 16 1.1 mrg #include <isl_vec_private.h> 17 1.1 mrg #include <isl_options_private.h> 18 1.1 mrg #include "isl_basis_reduction.h" 19 1.1 mrg 20 1.1 mrg static void save_alpha(GBR_LP *lp, int first, int n, GBR_type *alpha) 21 1.1 mrg { 22 1.1 mrg int i; 23 1.1 mrg 24 1.1 mrg for (i = 0; i < n; ++i) 25 1.1 mrg GBR_lp_get_alpha(lp, first + i, &alpha[i]); 26 1.1 mrg } 27 1.1 mrg 28 1.1 mrg /* Compute a reduced basis for the set represented by the tableau "tab". 29 1.1 mrg * tab->basis, which must be initialized by the calling function to an affine 30 1.1 mrg * unimodular basis, is updated to reflect the reduced basis. 31 1.1 mrg * The first tab->n_zero rows of the basis (ignoring the constant row) 32 1.1 mrg * are assumed to correspond to equalities and are left untouched. 33 1.1 mrg * tab->n_zero is updated to reflect any additional equalities that 34 1.1 mrg * have been detected in the first rows of the new basis. 35 1.1 mrg * The final tab->n_unbounded rows of the basis are assumed to correspond 36 1.1 mrg * to unbounded directions and are also left untouched. 37 1.1 mrg * In particular this means that the remaining rows are assumed to 38 1.1 mrg * correspond to bounded directions. 39 1.1 mrg * 40 1.1 mrg * This function implements the algorithm described in 41 1.1 mrg * "An Implementation of the Generalized Basis Reduction Algorithm 42 1.1 mrg * for Integer Programming" of Cook el al. to compute a reduced basis. 43 1.1 mrg * We use \epsilon = 1/4. 44 1.1 mrg * 45 1.1 mrg * If ctx->opt->gbr_only_first is set, the user is only interested 46 1.1 mrg * in the first direction. In this case we stop the basis reduction when 47 1.1 mrg * the width in the first direction becomes smaller than 2. 48 1.1 mrg */ 49 1.1 mrg struct isl_tab *isl_tab_compute_reduced_basis(struct isl_tab *tab) 50 1.1 mrg { 51 1.1 mrg unsigned dim; 52 1.1 mrg struct isl_ctx *ctx; 53 1.1 mrg struct isl_mat *B; 54 1.1 mrg int i; 55 1.1 mrg GBR_LP *lp = NULL; 56 1.1 mrg GBR_type F_old, alpha, F_new; 57 1.1 mrg int row; 58 1.1 mrg isl_int tmp; 59 1.1 mrg struct isl_vec *b_tmp; 60 1.1 mrg GBR_type *F = NULL; 61 1.1 mrg GBR_type *alpha_buffer[2] = { NULL, NULL }; 62 1.1 mrg GBR_type *alpha_saved; 63 1.1 mrg GBR_type F_saved; 64 1.1 mrg int use_saved = 0; 65 1.1 mrg isl_int mu[2]; 66 1.1 mrg GBR_type mu_F[2]; 67 1.1 mrg GBR_type two; 68 1.1 mrg GBR_type one; 69 1.1 mrg int empty = 0; 70 1.1 mrg int fixed = 0; 71 1.1 mrg int fixed_saved = 0; 72 1.1 mrg int mu_fixed[2]; 73 1.1 mrg int n_bounded; 74 1.1 mrg int gbr_only_first; 75 1.1 mrg 76 1.1 mrg if (!tab) 77 1.1 mrg return NULL; 78 1.1 mrg 79 1.1 mrg if (tab->empty) 80 1.1 mrg return tab; 81 1.1 mrg 82 1.1 mrg ctx = tab->mat->ctx; 83 1.1 mrg gbr_only_first = ctx->opt->gbr_only_first; 84 1.1 mrg dim = tab->n_var; 85 1.1 mrg B = tab->basis; 86 1.1 mrg if (!B) 87 1.1 mrg return tab; 88 1.1 mrg 89 1.1 mrg n_bounded = dim - tab->n_unbounded; 90 1.1 mrg if (n_bounded <= tab->n_zero + 1) 91 1.1 mrg return tab; 92 1.1 mrg 93 1.1 mrg isl_int_init(tmp); 94 1.1 mrg isl_int_init(mu[0]); 95 1.1 mrg isl_int_init(mu[1]); 96 1.1 mrg 97 1.1 mrg GBR_init(alpha); 98 1.1 mrg GBR_init(F_old); 99 1.1 mrg GBR_init(F_new); 100 1.1 mrg GBR_init(F_saved); 101 1.1 mrg GBR_init(mu_F[0]); 102 1.1 mrg GBR_init(mu_F[1]); 103 1.1 mrg GBR_init(two); 104 1.1 mrg GBR_init(one); 105 1.1 mrg 106 1.1 mrg b_tmp = isl_vec_alloc(ctx, dim); 107 1.1 mrg if (!b_tmp) 108 1.1 mrg goto error; 109 1.1 mrg 110 1.1 mrg F = isl_alloc_array(ctx, GBR_type, n_bounded); 111 1.1 mrg alpha_buffer[0] = isl_alloc_array(ctx, GBR_type, n_bounded); 112 1.1 mrg alpha_buffer[1] = isl_alloc_array(ctx, GBR_type, n_bounded); 113 1.1 mrg alpha_saved = alpha_buffer[0]; 114 1.1 mrg 115 1.1 mrg if (!F || !alpha_buffer[0] || !alpha_buffer[1]) 116 1.1 mrg goto error; 117 1.1 mrg 118 1.1 mrg for (i = 0; i < n_bounded; ++i) { 119 1.1 mrg GBR_init(F[i]); 120 1.1 mrg GBR_init(alpha_buffer[0][i]); 121 1.1 mrg GBR_init(alpha_buffer[1][i]); 122 1.1 mrg } 123 1.1 mrg 124 1.1 mrg GBR_set_ui(two, 2); 125 1.1 mrg GBR_set_ui(one, 1); 126 1.1 mrg 127 1.1 mrg lp = GBR_lp_init(tab); 128 1.1 mrg if (!lp) 129 1.1 mrg goto error; 130 1.1 mrg 131 1.1 mrg i = tab->n_zero; 132 1.1 mrg 133 1.1 mrg GBR_lp_set_obj(lp, B->row[1+i]+1, dim); 134 1.1 mrg ctx->stats->gbr_solved_lps++; 135 1.1 mrg if (GBR_lp_solve(lp) < 0) 136 1.1 mrg goto error; 137 1.1 mrg GBR_lp_get_obj_val(lp, &F[i]); 138 1.1 mrg 139 1.1 mrg if (GBR_lt(F[i], one)) { 140 1.1 mrg if (!GBR_is_zero(F[i])) { 141 1.1 mrg empty = GBR_lp_cut(lp, B->row[1+i]+1); 142 1.1 mrg if (empty) 143 1.1 mrg goto done; 144 1.1 mrg GBR_set_ui(F[i], 0); 145 1.1 mrg } 146 1.1 mrg tab->n_zero++; 147 1.1 mrg } 148 1.1 mrg 149 1.1 mrg do { 150 1.1 mrg if (i+1 == tab->n_zero) { 151 1.1 mrg GBR_lp_set_obj(lp, B->row[1+i+1]+1, dim); 152 1.1 mrg ctx->stats->gbr_solved_lps++; 153 1.1 mrg if (GBR_lp_solve(lp) < 0) 154 1.1 mrg goto error; 155 1.1 mrg GBR_lp_get_obj_val(lp, &F_new); 156 1.1 mrg fixed = GBR_lp_is_fixed(lp); 157 1.1 mrg GBR_set_ui(alpha, 0); 158 1.1 mrg } else if (use_saved) { 159 1.1 mrg row = GBR_lp_next_row(lp); 160 1.1 mrg GBR_set(F_new, F_saved); 161 1.1 mrg fixed = fixed_saved; 162 1.1 mrg GBR_set(alpha, alpha_saved[i]); 163 1.1 mrg } else { 164 1.1 mrg row = GBR_lp_add_row(lp, B->row[1+i]+1, dim); 165 1.1 mrg GBR_lp_set_obj(lp, B->row[1+i+1]+1, dim); 166 1.1 mrg ctx->stats->gbr_solved_lps++; 167 1.1 mrg if (GBR_lp_solve(lp) < 0) 168 1.1 mrg goto error; 169 1.1 mrg GBR_lp_get_obj_val(lp, &F_new); 170 1.1 mrg fixed = GBR_lp_is_fixed(lp); 171 1.1 mrg 172 1.1 mrg GBR_lp_get_alpha(lp, row, &alpha); 173 1.1 mrg 174 1.1 mrg if (i > 0) 175 1.1 mrg save_alpha(lp, row-i, i, alpha_saved); 176 1.1 mrg 177 1.1 mrg if (GBR_lp_del_row(lp) < 0) 178 1.1 mrg goto error; 179 1.1 mrg } 180 1.1 mrg GBR_set(F[i+1], F_new); 181 1.1 mrg 182 1.1 mrg GBR_floor(mu[0], alpha); 183 1.1 mrg GBR_ceil(mu[1], alpha); 184 1.1 mrg 185 1.1 mrg if (isl_int_eq(mu[0], mu[1])) 186 1.1 mrg isl_int_set(tmp, mu[0]); 187 1.1 mrg else { 188 1.1 mrg int j; 189 1.1 mrg 190 1.1 mrg for (j = 0; j <= 1; ++j) { 191 1.1 mrg isl_int_set(tmp, mu[j]); 192 1.1 mrg isl_seq_combine(b_tmp->el, 193 1.1 mrg ctx->one, B->row[1+i+1]+1, 194 1.1 mrg tmp, B->row[1+i]+1, dim); 195 1.1 mrg GBR_lp_set_obj(lp, b_tmp->el, dim); 196 1.1 mrg ctx->stats->gbr_solved_lps++; 197 1.1 mrg if (GBR_lp_solve(lp) < 0) 198 1.1 mrg goto error; 199 1.1 mrg GBR_lp_get_obj_val(lp, &mu_F[j]); 200 1.1 mrg mu_fixed[j] = GBR_lp_is_fixed(lp); 201 1.1 mrg if (i > 0) 202 1.1 mrg save_alpha(lp, row-i, i, alpha_buffer[j]); 203 1.1 mrg } 204 1.1 mrg 205 1.1 mrg if (GBR_lt(mu_F[0], mu_F[1])) 206 1.1 mrg j = 0; 207 1.1 mrg else 208 1.1 mrg j = 1; 209 1.1 mrg 210 1.1 mrg isl_int_set(tmp, mu[j]); 211 1.1 mrg GBR_set(F_new, mu_F[j]); 212 1.1 mrg fixed = mu_fixed[j]; 213 1.1 mrg alpha_saved = alpha_buffer[j]; 214 1.1 mrg } 215 1.1 mrg isl_seq_combine(B->row[1+i+1]+1, ctx->one, B->row[1+i+1]+1, 216 1.1 mrg tmp, B->row[1+i]+1, dim); 217 1.1 mrg 218 1.1 mrg if (i+1 == tab->n_zero && fixed) { 219 1.1 mrg if (!GBR_is_zero(F[i+1])) { 220 1.1 mrg empty = GBR_lp_cut(lp, B->row[1+i+1]+1); 221 1.1 mrg if (empty) 222 1.1 mrg goto done; 223 1.1 mrg GBR_set_ui(F[i+1], 0); 224 1.1 mrg } 225 1.1 mrg tab->n_zero++; 226 1.1 mrg } 227 1.1 mrg 228 1.1 mrg GBR_set(F_old, F[i]); 229 1.1 mrg 230 1.1 mrg use_saved = 0; 231 1.1 mrg /* mu_F[0] = 4 * F_new; mu_F[1] = 3 * F_old */ 232 1.1 mrg GBR_set_ui(mu_F[0], 4); 233 1.1 mrg GBR_mul(mu_F[0], mu_F[0], F_new); 234 1.1 mrg GBR_set_ui(mu_F[1], 3); 235 1.1 mrg GBR_mul(mu_F[1], mu_F[1], F_old); 236 1.1 mrg if (GBR_lt(mu_F[0], mu_F[1])) { 237 1.1 mrg B = isl_mat_swap_rows(B, 1 + i, 1 + i + 1); 238 1.1 mrg if (i > tab->n_zero) { 239 1.1 mrg use_saved = 1; 240 1.1 mrg GBR_set(F_saved, F_new); 241 1.1 mrg fixed_saved = fixed; 242 1.1 mrg if (GBR_lp_del_row(lp) < 0) 243 1.1 mrg goto error; 244 1.1 mrg --i; 245 1.1 mrg } else { 246 1.1 mrg GBR_set(F[tab->n_zero], F_new); 247 1.1 mrg if (gbr_only_first && GBR_lt(F[tab->n_zero], two)) 248 1.1 mrg break; 249 1.1 mrg 250 1.1 mrg if (fixed) { 251 1.1 mrg if (!GBR_is_zero(F[tab->n_zero])) { 252 1.1 mrg empty = GBR_lp_cut(lp, B->row[1+tab->n_zero]+1); 253 1.1 mrg if (empty) 254 1.1 mrg goto done; 255 1.1 mrg GBR_set_ui(F[tab->n_zero], 0); 256 1.1 mrg } 257 1.1 mrg tab->n_zero++; 258 1.1 mrg } 259 1.1 mrg } 260 1.1 mrg } else { 261 1.1 mrg GBR_lp_add_row(lp, B->row[1+i]+1, dim); 262 1.1 mrg ++i; 263 1.1 mrg } 264 1.1 mrg } while (i < n_bounded - 1); 265 1.1 mrg 266 1.1 mrg if (0) { 267 1.1 mrg done: 268 1.1 mrg if (empty < 0) { 269 1.1 mrg error: 270 1.1 mrg isl_mat_free(B); 271 1.1 mrg B = NULL; 272 1.1 mrg } 273 1.1 mrg } 274 1.1 mrg 275 1.1 mrg GBR_lp_delete(lp); 276 1.1 mrg 277 1.1 mrg if (alpha_buffer[1]) 278 1.1 mrg for (i = 0; i < n_bounded; ++i) { 279 1.1 mrg GBR_clear(F[i]); 280 1.1 mrg GBR_clear(alpha_buffer[0][i]); 281 1.1 mrg GBR_clear(alpha_buffer[1][i]); 282 1.1 mrg } 283 1.1 mrg free(F); 284 1.1 mrg free(alpha_buffer[0]); 285 1.1 mrg free(alpha_buffer[1]); 286 1.1 mrg 287 1.1 mrg isl_vec_free(b_tmp); 288 1.1 mrg 289 1.1 mrg GBR_clear(alpha); 290 1.1 mrg GBR_clear(F_old); 291 1.1 mrg GBR_clear(F_new); 292 1.1 mrg GBR_clear(F_saved); 293 1.1 mrg GBR_clear(mu_F[0]); 294 1.1 mrg GBR_clear(mu_F[1]); 295 1.1 mrg GBR_clear(two); 296 1.1 mrg GBR_clear(one); 297 1.1 mrg 298 1.1 mrg isl_int_clear(tmp); 299 1.1 mrg isl_int_clear(mu[0]); 300 1.1 mrg isl_int_clear(mu[1]); 301 1.1 mrg 302 1.1 mrg tab->basis = B; 303 1.1 mrg 304 1.1 mrg return tab; 305 1.1 mrg } 306 1.1 mrg 307 1.1 mrg /* Compute an affine form of a reduced basis of the given basic 308 1.1 mrg * non-parametric set, which is assumed to be bounded and not 309 1.1 mrg * include any integer divisions. 310 1.1 mrg * The first column and the first row correspond to the constant term. 311 1.1 mrg * 312 1.1 mrg * If the input contains any equalities, we first create an initial 313 1.1 mrg * basis with the equalities first. Otherwise, we start off with 314 1.1 mrg * the identity matrix. 315 1.1 mrg */ 316 1.1 mrg __isl_give isl_mat *isl_basic_set_reduced_basis(__isl_keep isl_basic_set *bset) 317 1.1 mrg { 318 1.1 mrg struct isl_mat *basis; 319 1.1 mrg struct isl_tab *tab; 320 1.1 mrg 321 1.1 mrg if (isl_basic_set_check_no_locals(bset) < 0 || 322 1.1 mrg isl_basic_set_check_no_params(bset) < 0) 323 1.1 mrg return NULL; 324 1.1 mrg 325 1.1 mrg tab = isl_tab_from_basic_set(bset, 0); 326 1.1 mrg if (!tab) 327 1.1 mrg return NULL; 328 1.1 mrg 329 1.1 mrg if (bset->n_eq == 0) 330 1.1 mrg tab->basis = isl_mat_identity(bset->ctx, 1 + tab->n_var); 331 1.1 mrg else { 332 1.1 mrg isl_mat *eq; 333 1.1 mrg isl_size nvar = isl_basic_set_dim(bset, isl_dim_all); 334 1.1 mrg if (nvar < 0) 335 1.1 mrg goto error; 336 1.1 mrg eq = isl_mat_sub_alloc6(bset->ctx, bset->eq, 0, bset->n_eq, 337 1.1 mrg 1, nvar); 338 1.1 mrg eq = isl_mat_left_hermite(eq, 0, NULL, &tab->basis); 339 1.1 mrg tab->basis = isl_mat_lin_to_aff(tab->basis); 340 1.1 mrg tab->n_zero = bset->n_eq; 341 1.1 mrg isl_mat_free(eq); 342 1.1 mrg } 343 1.1 mrg tab = isl_tab_compute_reduced_basis(tab); 344 1.1 mrg if (!tab) 345 1.1 mrg return NULL; 346 1.1 mrg 347 1.1 mrg basis = isl_mat_copy(tab->basis); 348 1.1 mrg 349 1.1 mrg isl_tab_free(tab); 350 1.1 mrg 351 1.1 mrg return basis; 352 1.1 mrg error: 353 1.1 mrg isl_tab_free(tab); 354 1.1 mrg return NULL; 355 1.1 mrg } 356