2 * Copyright 2006-2007 Universiteit Leiden
3 * Copyright 2008-2009 Katholieke Universiteit Leuven
5 * Use of this software is governed by the MIT license
7 * Written by Sven Verdoolaege, Leiden Institute of Advanced Computer Science,
8 * Universiteit Leiden, Niels Bohrweg 1, 2333 CA Leiden, The Netherlands
9 * and K.U.Leuven, Departement Computerwetenschappen, Celestijnenlaan 200A,
10 * B-3001 Leuven, Belgium
14 #include <isl_ctx_private.h>
15 #include <isl_map_private.h>
16 #include <isl_vec_private.h>
17 #include <isl_options_private.h>
18 #include "isl_basis_reduction.h"
20 static void save_alpha(GBR_LP
*lp
, int first
, int n
, GBR_type
*alpha
)
24 for (i
= 0; i
< n
; ++i
)
25 GBR_lp_get_alpha(lp
, first
+ i
, &alpha
[i
]);
28 /* Compute a reduced basis for the set represented by the tableau "tab".
29 * tab->basis, which must be initialized by the calling function to an affine
30 * unimodular basis, is updated to reflect the reduced basis.
31 * The first tab->n_zero rows of the basis (ignoring the constant row)
32 * are assumed to correspond to equalities and are left untouched.
33 * tab->n_zero is updated to reflect any additional equalities that
34 * have been detected in the first rows of the new basis.
35 * The final tab->n_unbounded rows of the basis are assumed to correspond
36 * to unbounded directions and are also left untouched.
37 * In particular this means that the remaining rows are assumed to
38 * correspond to bounded directions.
40 * This function implements the algorithm described in
41 * "An Implementation of the Generalized Basis Reduction Algorithm
42 * for Integer Programming" of Cook el al. to compute a reduced basis.
43 * We use \epsilon = 1/4.
45 * If ctx->opt->gbr_only_first is set, the user is only interested
46 * in the first direction. In this case we stop the basis reduction when
47 * the width in the first direction becomes smaller than 2.
49 struct isl_tab
*isl_tab_compute_reduced_basis(struct isl_tab
*tab
)
56 GBR_type F_old
, alpha
, F_new
;
59 struct isl_vec
*b_tmp
;
61 GBR_type
*alpha_buffer
[2] = { NULL
, NULL
};
62 GBR_type
*alpha_saved
;
83 gbr_only_first
= ctx
->opt
->gbr_only_first
;
89 n_bounded
= dim
- tab
->n_unbounded
;
90 if (n_bounded
<= tab
->n_zero
+ 1)
106 b_tmp
= isl_vec_alloc(ctx
, dim
);
110 F
= isl_alloc_array(ctx
, GBR_type
, n_bounded
);
111 alpha_buffer
[0] = isl_alloc_array(ctx
, GBR_type
, n_bounded
);
112 alpha_buffer
[1] = isl_alloc_array(ctx
, GBR_type
, n_bounded
);
113 alpha_saved
= alpha_buffer
[0];
115 if (!F
|| !alpha_buffer
[0] || !alpha_buffer
[1])
118 for (i
= 0; i
< n_bounded
; ++i
) {
120 GBR_init(alpha_buffer
[0][i
]);
121 GBR_init(alpha_buffer
[1][i
]);
127 lp
= GBR_lp_init(tab
);
133 GBR_lp_set_obj(lp
, B
->row
[1+i
]+1, dim
);
134 ctx
->stats
->gbr_solved_lps
++;
135 if (GBR_lp_solve(lp
) < 0)
137 GBR_lp_get_obj_val(lp
, &F
[i
]);
139 if (GBR_lt(F
[i
], one
)) {
140 if (!GBR_is_zero(F
[i
])) {
141 empty
= GBR_lp_cut(lp
, B
->row
[1+i
]+1);
150 if (i
+1 == tab
->n_zero
) {
151 GBR_lp_set_obj(lp
, B
->row
[1+i
+1]+1, dim
);
152 ctx
->stats
->gbr_solved_lps
++;
153 if (GBR_lp_solve(lp
) < 0)
155 GBR_lp_get_obj_val(lp
, &F_new
);
156 fixed
= GBR_lp_is_fixed(lp
);
157 GBR_set_ui(alpha
, 0);
158 } else if (use_saved
) {
159 row
= GBR_lp_next_row(lp
);
160 GBR_set(F_new
, F_saved
);
162 GBR_set(alpha
, alpha_saved
[i
]);
164 row
= GBR_lp_add_row(lp
, B
->row
[1+i
]+1, dim
);
165 GBR_lp_set_obj(lp
, B
->row
[1+i
+1]+1, dim
);
166 ctx
->stats
->gbr_solved_lps
++;
167 if (GBR_lp_solve(lp
) < 0)
169 GBR_lp_get_obj_val(lp
, &F_new
);
170 fixed
= GBR_lp_is_fixed(lp
);
172 GBR_lp_get_alpha(lp
, row
, &alpha
);
175 save_alpha(lp
, row
-i
, i
, alpha_saved
);
177 if (GBR_lp_del_row(lp
) < 0)
180 GBR_set(F
[i
+1], F_new
);
182 GBR_floor(mu
[0], alpha
);
183 GBR_ceil(mu
[1], alpha
);
185 if (isl_int_eq(mu
[0], mu
[1]))
186 isl_int_set(tmp
, mu
[0]);
190 for (j
= 0; j
<= 1; ++j
) {
191 isl_int_set(tmp
, mu
[j
]);
192 isl_seq_combine(b_tmp
->el
,
193 ctx
->one
, B
->row
[1+i
+1]+1,
194 tmp
, B
->row
[1+i
]+1, dim
);
195 GBR_lp_set_obj(lp
, b_tmp
->el
, dim
);
196 ctx
->stats
->gbr_solved_lps
++;
197 if (GBR_lp_solve(lp
) < 0)
199 GBR_lp_get_obj_val(lp
, &mu_F
[j
]);
200 mu_fixed
[j
] = GBR_lp_is_fixed(lp
);
202 save_alpha(lp
, row
-i
, i
, alpha_buffer
[j
]);
205 if (GBR_lt(mu_F
[0], mu_F
[1]))
210 isl_int_set(tmp
, mu
[j
]);
211 GBR_set(F_new
, mu_F
[j
]);
213 alpha_saved
= alpha_buffer
[j
];
215 isl_seq_combine(B
->row
[1+i
+1]+1, ctx
->one
, B
->row
[1+i
+1]+1,
216 tmp
, B
->row
[1+i
]+1, dim
);
218 if (i
+1 == tab
->n_zero
&& fixed
) {
219 if (!GBR_is_zero(F
[i
+1])) {
220 empty
= GBR_lp_cut(lp
, B
->row
[1+i
+1]+1);
223 GBR_set_ui(F
[i
+1], 0);
228 GBR_set(F_old
, F
[i
]);
231 /* mu_F[0] = 4 * F_new; mu_F[1] = 3 * F_old */
232 GBR_set_ui(mu_F
[0], 4);
233 GBR_mul(mu_F
[0], mu_F
[0], F_new
);
234 GBR_set_ui(mu_F
[1], 3);
235 GBR_mul(mu_F
[1], mu_F
[1], F_old
);
236 if (GBR_lt(mu_F
[0], mu_F
[1])) {
237 B
= isl_mat_swap_rows(B
, 1 + i
, 1 + i
+ 1);
238 if (i
> tab
->n_zero
) {
240 GBR_set(F_saved
, F_new
);
242 if (GBR_lp_del_row(lp
) < 0)
246 GBR_set(F
[tab
->n_zero
], F_new
);
247 if (gbr_only_first
&& GBR_lt(F
[tab
->n_zero
], two
))
251 if (!GBR_is_zero(F
[tab
->n_zero
])) {
252 empty
= GBR_lp_cut(lp
, B
->row
[1+tab
->n_zero
]+1);
255 GBR_set_ui(F
[tab
->n_zero
], 0);
261 GBR_lp_add_row(lp
, B
->row
[1+i
]+1, dim
);
264 } while (i
< n_bounded
- 1);
278 for (i
= 0; i
< n_bounded
; ++i
) {
280 GBR_clear(alpha_buffer
[0][i
]);
281 GBR_clear(alpha_buffer
[1][i
]);
284 free(alpha_buffer
[0]);
285 free(alpha_buffer
[1]);
299 isl_int_clear(mu
[0]);
300 isl_int_clear(mu
[1]);
307 /* Compute an affine form of a reduced basis of the given basic
308 * non-parametric set, which is assumed to be bounded and not
309 * include any integer divisions.
310 * The first column and the first row correspond to the constant term.
312 * If the input contains any equalities, we first create an initial
313 * basis with the equalities first. Otherwise, we start off with
314 * the identity matrix.
316 __isl_give isl_mat
*isl_basic_set_reduced_basis(__isl_keep isl_basic_set
*bset
)
318 struct isl_mat
*basis
;
321 if (isl_basic_set_check_no_locals(bset
) < 0 ||
322 isl_basic_set_check_no_params(bset
) < 0)
325 tab
= isl_tab_from_basic_set(bset
, 0);
330 tab
->basis
= isl_mat_identity(bset
->ctx
, 1 + tab
->n_var
);
333 isl_size nvar
= isl_basic_set_dim(bset
, isl_dim_all
);
336 eq
= isl_mat_sub_alloc6(bset
->ctx
, bset
->eq
, 0, bset
->n_eq
,
338 eq
= isl_mat_left_hermite(eq
, 0, NULL
, &tab
->basis
);
339 tab
->basis
= isl_mat_lin_to_aff(tab
->basis
);
340 tab
->n_zero
= bset
->n_eq
;
343 tab
= isl_tab_compute_reduced_basis(tab
);
347 basis
= isl_mat_copy(tab
->basis
);