Home | History | Annotate | Line # | Download | only in dist
basis_reduction_templ.c revision 1.1
      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