isl_tab_pip.c: propagate some equalities from gbr context to main tableau
[isl.git] / isl_ilp.c
blob3aa10bd8ddf1914dfafb5390b9c2dbae5a16378f
1 #include "isl_ilp.h"
2 #include "isl_map_private.h"
3 #include "isl_sample.h"
4 #include "isl_seq.h"
5 #include "isl_equalities.h"
7 /* Given a basic set "bset", construct a basic set U such that for
8 * each element x in U, the whole unit box positioned at x is inside
9 * the given basic set.
10 * Note that U may not contain all points that satisfy this property.
12 * We simply add the sum of all negative coefficients to the constant
13 * term. This ensures that if x satisfies the resulting constraints,
14 * then x plus any sum of unit vectors satisfies the original constraints.
16 static struct isl_basic_set *unit_box_base_points(struct isl_basic_set *bset)
18 int i, j, k;
19 struct isl_basic_set *unit_box = NULL;
20 unsigned total;
22 if (!bset)
23 goto error;
25 if (bset->n_eq != 0) {
26 unit_box = isl_basic_set_empty_like(bset);
27 isl_basic_set_free(bset);
28 return unit_box;
31 total = isl_basic_set_total_dim(bset);
32 unit_box = isl_basic_set_alloc_dim(isl_basic_set_get_dim(bset),
33 0, 0, bset->n_ineq);
35 for (i = 0; i < bset->n_ineq; ++i) {
36 k = isl_basic_set_alloc_inequality(unit_box);
37 if (k < 0)
38 goto error;
39 isl_seq_cpy(unit_box->ineq[k], bset->ineq[i], 1 + total);
40 for (j = 0; j < total; ++j) {
41 if (isl_int_is_nonneg(unit_box->ineq[k][1 + j]))
42 continue;
43 isl_int_add(unit_box->ineq[k][0],
44 unit_box->ineq[k][0], unit_box->ineq[k][1 + j]);
48 isl_basic_set_free(bset);
49 return unit_box;
50 error:
51 isl_basic_set_free(bset);
52 isl_basic_set_free(unit_box);
53 return NULL;
56 /* Find an integer point in "bset", preferably one that is
57 * close to minimizing "f".
59 * We first check if we can easily put unit boxes inside bset.
60 * If so, we take the best base point of any of the unit boxes we can find
61 * and round it up to the nearest integer.
62 * If not, we simply pick any integer point in "bset".
64 static struct isl_vec *initial_solution(struct isl_basic_set *bset, isl_int *f)
66 enum isl_lp_result res;
67 struct isl_basic_set *unit_box;
68 struct isl_vec *sol;
70 unit_box = unit_box_base_points(isl_basic_set_copy(bset));
72 res = isl_basic_set_solve_lp(unit_box, 0, f, bset->ctx->one,
73 NULL, NULL, &sol);
74 if (res == isl_lp_ok) {
75 isl_basic_set_free(unit_box);
76 return isl_vec_ceil(sol);
79 isl_basic_set_free(unit_box);
81 return isl_basic_set_sample_vec(isl_basic_set_copy(bset));
84 /* Restrict "bset" to those points with values for f in the interval [l, u].
86 static struct isl_basic_set *add_bounds(struct isl_basic_set *bset,
87 isl_int *f, isl_int l, isl_int u)
89 int k;
90 unsigned total;
92 total = isl_basic_set_total_dim(bset);
93 bset = isl_basic_set_extend_constraints(bset, 0, 2);
95 k = isl_basic_set_alloc_inequality(bset);
96 if (k < 0)
97 goto error;
98 isl_seq_cpy(bset->ineq[k], f, 1 + total);
99 isl_int_sub(bset->ineq[k][0], bset->ineq[k][0], l);
101 k = isl_basic_set_alloc_inequality(bset);
102 if (k < 0)
103 goto error;
104 isl_seq_neg(bset->ineq[k], f, 1 + total);
105 isl_int_add(bset->ineq[k][0], bset->ineq[k][0], u);
107 return bset;
108 error:
109 isl_basic_set_free(bset);
110 return NULL;
113 /* Find an integer point in "bset" that minimizes f (in any) such that
114 * the value of f lies inside the interval [l, u].
115 * Return this integer point if it can be found.
116 * Otherwise, return sol.
118 * We perform a number of steps until l > u.
119 * In each step, we look for an integer point with value in either
120 * the whole interval [l, u] or half of the interval [l, l+floor(u-l-1/2)].
121 * The choice depends on whether we have found an integer point in the
122 * previous step. If so, we look for the next point in half of the remaining
123 * interval.
124 * If we find a point, the current solution is updated and u is set
125 * to its value minus 1.
126 * If no point can be found, we update l to the upper bound of the interval
127 * we checked (u or l+floor(u-l-1/2)) plus 1.
129 static struct isl_vec *solve_ilp_search(struct isl_basic_set *bset,
130 isl_int *f, isl_int *opt, struct isl_vec *sol, isl_int l, isl_int u)
132 isl_int tmp;
133 int divide = 1;
135 isl_int_init(tmp);
137 while (isl_int_le(l, u)) {
138 struct isl_basic_set *slice;
139 struct isl_vec *sample;
141 if (!divide)
142 isl_int_set(tmp, u);
143 else {
144 isl_int_sub(tmp, u, l);
145 isl_int_fdiv_q_ui(tmp, tmp, 2);
146 isl_int_add(tmp, tmp, l);
148 slice = add_bounds(isl_basic_set_copy(bset), f, l, tmp);
149 sample = isl_basic_set_sample_vec(slice);
150 if (!sample) {
151 isl_vec_free(sol);
152 sol = NULL;
153 break;
155 if (sample->size > 0) {
156 isl_vec_free(sol);
157 sol = sample;
158 isl_seq_inner_product(f, sol->el, sol->size, opt);
159 isl_int_sub_ui(u, *opt, 1);
160 divide = 1;
161 } else {
162 isl_vec_free(sample);
163 if (!divide)
164 break;
165 isl_int_add_ui(l, tmp, 1);
166 divide = 0;
170 isl_int_clear(tmp);
172 return sol;
175 /* Find an integer point in "bset" that minimizes f (if any).
176 * If sol_p is not NULL then the integer point is returned in *sol_p.
177 * The optimal value of f is returned in *opt.
179 * The algorithm maintains a currently best solution and an interval [l, u]
180 * of values of f for which integer solutions could potentially still be found.
181 * The initial value of the best solution so far is any solution.
182 * The initial value of l is minimal value of f over the rationals
183 * (rounded up to the nearest integer).
184 * The initial value of u is the value of f at the initial solution minus 1.
186 * We then call solve_ilp_search to perform a binary search on the interval.
188 static enum isl_lp_result solve_ilp(struct isl_basic_set *bset,
189 isl_int *f, isl_int *opt,
190 struct isl_vec **sol_p)
192 enum isl_lp_result res;
193 isl_int l, u;
194 struct isl_vec *sol;
196 res = isl_basic_set_solve_lp(bset, 0, f, bset->ctx->one,
197 opt, NULL, &sol);
198 if (res == isl_lp_ok && isl_int_is_one(sol->el[0])) {
199 if (sol_p)
200 *sol_p = sol;
201 else
202 isl_vec_free(sol);
203 return isl_lp_ok;
205 isl_vec_free(sol);
206 if (res == isl_lp_error || res == isl_lp_empty)
207 return res;
209 sol = initial_solution(bset, f);
210 if (!sol)
211 return isl_lp_error;
212 if (sol->size == 0) {
213 isl_vec_free(sol);
214 return isl_lp_empty;
216 if (res == isl_lp_unbounded) {
217 isl_vec_free(sol);
218 return isl_lp_unbounded;
221 isl_int_init(l);
222 isl_int_init(u);
224 isl_int_set(l, *opt);
226 isl_seq_inner_product(f, sol->el, sol->size, opt);
227 isl_int_sub_ui(u, *opt, 1);
229 sol = solve_ilp_search(bset, f, opt, sol, l, u);
230 if (!sol)
231 res = isl_lp_error;
233 isl_int_clear(l);
234 isl_int_clear(u);
236 if (sol_p)
237 *sol_p = sol;
238 else
239 isl_vec_free(sol);
241 return res;
244 static enum isl_lp_result solve_ilp_with_eq(struct isl_basic_set *bset, int max,
245 isl_int *f, isl_int *opt,
246 struct isl_vec **sol_p)
248 unsigned dim;
249 enum isl_lp_result res;
250 struct isl_mat *T = NULL;
251 struct isl_vec *v;
253 dim = isl_basic_set_total_dim(bset);
254 v = isl_vec_alloc(bset->ctx, 1 + dim);
255 if (!v)
256 goto error;
257 isl_seq_cpy(v->el, f, 1 + dim);
258 bset = isl_basic_set_remove_equalities(bset, &T, NULL);
259 v = isl_vec_mat_product(v, isl_mat_copy(T));
260 if (!v)
261 goto error;
262 res = isl_basic_set_solve_ilp(bset, max, v->el, opt, sol_p);
263 isl_vec_free(v);
264 if (res == isl_lp_ok && *sol_p) {
265 *sol_p = isl_mat_vec_product(T, *sol_p);
266 if (!*sol_p)
267 res = isl_lp_error;
268 } else
269 isl_mat_free(T);
270 return res;
271 error:
272 isl_mat_free(T);
273 isl_basic_set_free(bset);
274 return isl_lp_error;
277 /* Find an integer point in "bset" that minimizes (or maximizes if max is set)
278 * f (if any).
279 * If sol_p is not NULL then the integer point is returned in *sol_p.
280 * The optimal value of f is returned in *opt.
282 * If there is any equality among the points in "bset", then we first
283 * project it out. Otherwise, we continue with solve_ilp above.
285 enum isl_lp_result isl_basic_set_solve_ilp(struct isl_basic_set *bset, int max,
286 isl_int *f, isl_int *opt,
287 struct isl_vec **sol_p)
289 unsigned dim;
290 enum isl_lp_result res;
292 if (!bset)
293 return isl_lp_error;
294 if (sol_p)
295 *sol_p = NULL;
297 isl_assert(bset->ctx, isl_basic_set_n_param(bset) == 0, goto error);
299 if (bset->n_eq)
300 return solve_ilp_with_eq(bset, max, f, opt, sol_p);
302 dim = isl_basic_set_total_dim(bset);
304 if (max)
305 isl_seq_neg(f, f, 1 + dim);
307 res = solve_ilp(bset, f, opt, sol_p);
309 if (max) {
310 isl_seq_neg(f, f, 1 + dim);
311 isl_int_neg(*opt, *opt);
314 return res;
315 error:
316 isl_basic_set_free(bset);
317 return isl_lp_error;