2 * Copyright 2008-2009 Katholieke Universiteit Leuven
4 * Use of this software is governed by the MIT license
6 * Written by Sven Verdoolaege, K.U.Leuven, Departement
7 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
10 #include <isl_ctx_private.h>
11 #include <isl_map_private.h>
13 #include "isl_sample.h"
15 #include "isl_equalities.h"
16 #include <isl_aff_private.h>
17 #include <isl_local_space_private.h>
18 #include <isl_mat_private.h>
19 #include <isl_val_private.h>
20 #include <isl_vec_private.h>
21 #include <isl_lp_private.h>
22 #include <isl_ilp_private.h>
23 #include <isl/deprecated/ilp_int.h>
25 /* Given a basic set "bset", construct a basic set U such that for
26 * each element x in U, the whole unit box positioned at x is inside
27 * the given basic set.
28 * Note that U may not contain all points that satisfy this property.
30 * We simply add the sum of all negative coefficients to the constant
31 * term. This ensures that if x satisfies the resulting constraints,
32 * then x plus any sum of unit vectors satisfies the original constraints.
34 static struct isl_basic_set
*unit_box_base_points(struct isl_basic_set
*bset
)
37 struct isl_basic_set
*unit_box
= NULL
;
43 if (bset
->n_eq
!= 0) {
44 unit_box
= isl_basic_set_empty_like(bset
);
45 isl_basic_set_free(bset
);
49 total
= isl_basic_set_total_dim(bset
);
50 unit_box
= isl_basic_set_alloc_space(isl_basic_set_get_space(bset
),
53 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
54 k
= isl_basic_set_alloc_inequality(unit_box
);
57 isl_seq_cpy(unit_box
->ineq
[k
], bset
->ineq
[i
], 1 + total
);
58 for (j
= 0; j
< total
; ++j
) {
59 if (isl_int_is_nonneg(unit_box
->ineq
[k
][1 + j
]))
61 isl_int_add(unit_box
->ineq
[k
][0],
62 unit_box
->ineq
[k
][0], unit_box
->ineq
[k
][1 + j
]);
66 isl_basic_set_free(bset
);
69 isl_basic_set_free(bset
);
70 isl_basic_set_free(unit_box
);
74 /* Find an integer point in "bset", preferably one that is
75 * close to minimizing "f".
77 * We first check if we can easily put unit boxes inside bset.
78 * If so, we take the best base point of any of the unit boxes we can find
79 * and round it up to the nearest integer.
80 * If not, we simply pick any integer point in "bset".
82 static struct isl_vec
*initial_solution(struct isl_basic_set
*bset
, isl_int
*f
)
84 enum isl_lp_result res
;
85 struct isl_basic_set
*unit_box
;
88 unit_box
= unit_box_base_points(isl_basic_set_copy(bset
));
90 res
= isl_basic_set_solve_lp(unit_box
, 0, f
, bset
->ctx
->one
,
92 if (res
== isl_lp_ok
) {
93 isl_basic_set_free(unit_box
);
94 return isl_vec_ceil(sol
);
97 isl_basic_set_free(unit_box
);
99 return isl_basic_set_sample_vec(isl_basic_set_copy(bset
));
102 /* Restrict "bset" to those points with values for f in the interval [l, u].
104 static struct isl_basic_set
*add_bounds(struct isl_basic_set
*bset
,
105 isl_int
*f
, isl_int l
, isl_int u
)
110 total
= isl_basic_set_total_dim(bset
);
111 bset
= isl_basic_set_extend_constraints(bset
, 0, 2);
113 k
= isl_basic_set_alloc_inequality(bset
);
116 isl_seq_cpy(bset
->ineq
[k
], f
, 1 + total
);
117 isl_int_sub(bset
->ineq
[k
][0], bset
->ineq
[k
][0], l
);
119 k
= isl_basic_set_alloc_inequality(bset
);
122 isl_seq_neg(bset
->ineq
[k
], f
, 1 + total
);
123 isl_int_add(bset
->ineq
[k
][0], bset
->ineq
[k
][0], u
);
127 isl_basic_set_free(bset
);
131 /* Find an integer point in "bset" that minimizes f (in any) such that
132 * the value of f lies inside the interval [l, u].
133 * Return this integer point if it can be found.
134 * Otherwise, return sol.
136 * We perform a number of steps until l > u.
137 * In each step, we look for an integer point with value in either
138 * the whole interval [l, u] or half of the interval [l, l+floor(u-l-1/2)].
139 * The choice depends on whether we have found an integer point in the
140 * previous step. If so, we look for the next point in half of the remaining
142 * If we find a point, the current solution is updated and u is set
143 * to its value minus 1.
144 * If no point can be found, we update l to the upper bound of the interval
145 * we checked (u or l+floor(u-l-1/2)) plus 1.
147 static struct isl_vec
*solve_ilp_search(struct isl_basic_set
*bset
,
148 isl_int
*f
, isl_int
*opt
, struct isl_vec
*sol
, isl_int l
, isl_int u
)
155 while (isl_int_le(l
, u
)) {
156 struct isl_basic_set
*slice
;
157 struct isl_vec
*sample
;
162 isl_int_sub(tmp
, u
, l
);
163 isl_int_fdiv_q_ui(tmp
, tmp
, 2);
164 isl_int_add(tmp
, tmp
, l
);
166 slice
= add_bounds(isl_basic_set_copy(bset
), f
, l
, tmp
);
167 sample
= isl_basic_set_sample_vec(slice
);
173 if (sample
->size
> 0) {
176 isl_seq_inner_product(f
, sol
->el
, sol
->size
, opt
);
177 isl_int_sub_ui(u
, *opt
, 1);
180 isl_vec_free(sample
);
183 isl_int_add_ui(l
, tmp
, 1);
193 /* Find an integer point in "bset" that minimizes f (if any).
194 * If sol_p is not NULL then the integer point is returned in *sol_p.
195 * The optimal value of f is returned in *opt.
197 * The algorithm maintains a currently best solution and an interval [l, u]
198 * of values of f for which integer solutions could potentially still be found.
199 * The initial value of the best solution so far is any solution.
200 * The initial value of l is minimal value of f over the rationals
201 * (rounded up to the nearest integer).
202 * The initial value of u is the value of f at the initial solution minus 1.
204 * We then call solve_ilp_search to perform a binary search on the interval.
206 static enum isl_lp_result
solve_ilp(struct isl_basic_set
*bset
,
207 isl_int
*f
, isl_int
*opt
,
208 struct isl_vec
**sol_p
)
210 enum isl_lp_result res
;
214 res
= isl_basic_set_solve_lp(bset
, 0, f
, bset
->ctx
->one
,
216 if (res
== isl_lp_ok
&& isl_int_is_one(sol
->el
[0])) {
224 if (res
== isl_lp_error
|| res
== isl_lp_empty
)
227 sol
= initial_solution(bset
, f
);
230 if (sol
->size
== 0) {
234 if (res
== isl_lp_unbounded
) {
236 return isl_lp_unbounded
;
242 isl_int_set(l
, *opt
);
244 isl_seq_inner_product(f
, sol
->el
, sol
->size
, opt
);
245 isl_int_sub_ui(u
, *opt
, 1);
247 sol
= solve_ilp_search(bset
, f
, opt
, sol
, l
, u
);
262 static enum isl_lp_result
solve_ilp_with_eq(struct isl_basic_set
*bset
, int max
,
263 isl_int
*f
, isl_int
*opt
,
264 struct isl_vec
**sol_p
)
267 enum isl_lp_result res
;
268 struct isl_mat
*T
= NULL
;
271 bset
= isl_basic_set_copy(bset
);
272 dim
= isl_basic_set_total_dim(bset
);
273 v
= isl_vec_alloc(bset
->ctx
, 1 + dim
);
276 isl_seq_cpy(v
->el
, f
, 1 + dim
);
277 bset
= isl_basic_set_remove_equalities(bset
, &T
, NULL
);
278 v
= isl_vec_mat_product(v
, isl_mat_copy(T
));
281 res
= isl_basic_set_solve_ilp(bset
, max
, v
->el
, opt
, sol_p
);
283 if (res
== isl_lp_ok
&& sol_p
) {
284 *sol_p
= isl_mat_vec_product(T
, *sol_p
);
289 isl_basic_set_free(bset
);
293 isl_basic_set_free(bset
);
297 /* Find an integer point in "bset" that minimizes (or maximizes if max is set)
299 * If sol_p is not NULL then the integer point is returned in *sol_p.
300 * The optimal value of f is returned in *opt.
302 * If there is any equality among the points in "bset", then we first
303 * project it out. Otherwise, we continue with solve_ilp above.
305 enum isl_lp_result
isl_basic_set_solve_ilp(struct isl_basic_set
*bset
, int max
,
306 isl_int
*f
, isl_int
*opt
,
307 struct isl_vec
**sol_p
)
310 enum isl_lp_result res
;
317 isl_assert(bset
->ctx
, isl_basic_set_n_param(bset
) == 0, goto error
);
319 if (isl_basic_set_plain_is_empty(bset
))
323 return solve_ilp_with_eq(bset
, max
, f
, opt
, sol_p
);
325 dim
= isl_basic_set_total_dim(bset
);
328 isl_seq_neg(f
, f
, 1 + dim
);
330 res
= solve_ilp(bset
, f
, opt
, sol_p
);
333 isl_seq_neg(f
, f
, 1 + dim
);
334 isl_int_neg(*opt
, *opt
);
339 isl_basic_set_free(bset
);
343 static enum isl_lp_result
basic_set_opt(__isl_keep isl_basic_set
*bset
, int max
,
344 __isl_keep isl_aff
*obj
, isl_int
*opt
)
346 enum isl_lp_result res
;
350 bset
= isl_basic_set_copy(bset
);
351 bset
= isl_basic_set_underlying_set(bset
);
352 res
= isl_basic_set_solve_ilp(bset
, max
, obj
->v
->el
+ 1, opt
, NULL
);
353 isl_basic_set_free(bset
);
357 static __isl_give isl_mat
*extract_divs(__isl_keep isl_basic_set
*bset
)
360 isl_ctx
*ctx
= isl_basic_set_get_ctx(bset
);
363 div
= isl_mat_alloc(ctx
, bset
->n_div
,
364 1 + 1 + isl_basic_set_total_dim(bset
));
368 for (i
= 0; i
< bset
->n_div
; ++i
)
369 isl_seq_cpy(div
->row
[i
], bset
->div
[i
], div
->n_col
);
374 enum isl_lp_result
isl_basic_set_opt(__isl_keep isl_basic_set
*bset
, int max
,
375 __isl_keep isl_aff
*obj
, isl_int
*opt
)
380 isl_mat
*bset_div
= NULL
;
382 enum isl_lp_result res
;
383 int bset_n_div
, obj_n_div
;
388 ctx
= isl_aff_get_ctx(obj
);
389 if (!isl_space_is_equal(bset
->dim
, obj
->ls
->dim
))
390 isl_die(ctx
, isl_error_invalid
,
391 "spaces don't match", return isl_lp_error
);
392 if (!isl_int_is_one(obj
->v
->el
[0]))
393 isl_die(ctx
, isl_error_unsupported
,
394 "expecting integer affine expression",
395 return isl_lp_error
);
397 bset_n_div
= isl_basic_set_dim(bset
, isl_dim_div
);
398 obj_n_div
= isl_aff_dim(obj
, isl_dim_div
);
399 if (bset_n_div
== 0 && obj_n_div
== 0)
400 return basic_set_opt(bset
, max
, obj
, opt
);
402 bset
= isl_basic_set_copy(bset
);
403 obj
= isl_aff_copy(obj
);
405 bset_div
= extract_divs(bset
);
406 exp1
= isl_alloc_array(ctx
, int, bset_n_div
);
407 exp2
= isl_alloc_array(ctx
, int, obj_n_div
);
408 if (!bset_div
|| (bset_n_div
&& !exp1
) || (obj_n_div
&& !exp2
))
411 div
= isl_merge_divs(bset_div
, obj
->ls
->div
, exp1
, exp2
);
413 bset
= isl_basic_set_expand_divs(bset
, isl_mat_copy(div
), exp1
);
414 obj
= isl_aff_expand_divs(obj
, isl_mat_copy(div
), exp2
);
416 res
= basic_set_opt(bset
, max
, obj
, opt
);
418 isl_mat_free(bset_div
);
422 isl_basic_set_free(bset
);
428 isl_mat_free(bset_div
);
431 isl_basic_set_free(bset
);
436 /* Compute the minimum (maximum if max is set) of the integer affine
437 * expression obj over the points in set and put the result in *opt.
439 * The parameters are assumed to have been aligned.
441 static enum isl_lp_result
isl_set_opt_aligned(__isl_keep isl_set
*set
, int max
,
442 __isl_keep isl_aff
*obj
, isl_int
*opt
)
445 enum isl_lp_result res
;
454 res
= isl_basic_set_opt(set
->p
[0], max
, obj
, opt
);
455 if (res
== isl_lp_error
|| res
== isl_lp_unbounded
)
459 if (res
== isl_lp_ok
)
463 for (i
= 1; i
< set
->n
; ++i
) {
464 res
= isl_basic_set_opt(set
->p
[i
], max
, obj
, &opt_i
);
465 if (res
== isl_lp_error
|| res
== isl_lp_unbounded
) {
466 isl_int_clear(opt_i
);
469 if (res
== isl_lp_ok
)
471 if (max
? isl_int_gt(opt_i
, *opt
) : isl_int_lt(opt_i
, *opt
))
472 isl_int_set(*opt
, opt_i
);
474 isl_int_clear(opt_i
);
476 return empty
? isl_lp_empty
: isl_lp_ok
;
479 /* Compute the minimum (maximum if max is set) of the integer affine
480 * expression obj over the points in set and put the result in *opt.
482 enum isl_lp_result
isl_set_opt(__isl_keep isl_set
*set
, int max
,
483 __isl_keep isl_aff
*obj
, isl_int
*opt
)
485 enum isl_lp_result res
;
490 if (isl_space_match(set
->dim
, isl_dim_param
,
491 obj
->ls
->dim
, isl_dim_param
))
492 return isl_set_opt_aligned(set
, max
, obj
, opt
);
494 set
= isl_set_copy(set
);
495 obj
= isl_aff_copy(obj
);
496 set
= isl_set_align_params(set
, isl_aff_get_domain_space(obj
));
497 obj
= isl_aff_align_params(obj
, isl_set_get_space(set
));
499 res
= isl_set_opt_aligned(set
, max
, obj
, opt
);
507 enum isl_lp_result
isl_basic_set_max(__isl_keep isl_basic_set
*bset
,
508 __isl_keep isl_aff
*obj
, isl_int
*opt
)
510 return isl_basic_set_opt(bset
, 1, obj
, opt
);
513 enum isl_lp_result
isl_set_max(__isl_keep isl_set
*set
,
514 __isl_keep isl_aff
*obj
, isl_int
*opt
)
516 return isl_set_opt(set
, 1, obj
, opt
);
519 enum isl_lp_result
isl_set_min(__isl_keep isl_set
*set
,
520 __isl_keep isl_aff
*obj
, isl_int
*opt
)
522 return isl_set_opt(set
, 0, obj
, opt
);
525 /* Convert the result of a function that returns an isl_lp_result
526 * to an isl_val. The numerator of "v" is set to the optimal value
527 * if lp_res is isl_lp_ok. "max" is set if a maximum was computed.
529 * Return "v" with denominator set to 1 if lp_res is isl_lp_ok.
530 * Return NULL on error.
531 * Return a NaN if lp_res is isl_lp_empty.
532 * Return infinity or negative infinity if lp_res is isl_lp_unbounded,
533 * depending on "max".
535 static __isl_give isl_val
*convert_lp_result(enum isl_lp_result lp_res
,
536 __isl_take isl_val
*v
, int max
)
540 if (lp_res
== isl_lp_ok
) {
541 isl_int_set_si(v
->d
, 1);
542 return isl_val_normalize(v
);
544 ctx
= isl_val_get_ctx(v
);
546 if (lp_res
== isl_lp_error
)
548 if (lp_res
== isl_lp_empty
)
549 return isl_val_nan(ctx
);
551 return isl_val_infty(ctx
);
553 return isl_val_neginfty(ctx
);
556 /* Return the minimum (maximum if max is set) of the integer affine
557 * expression "obj" over the points in "bset".
559 * Return infinity or negative infinity if the optimal value is unbounded and
560 * NaN if "bset" is empty.
562 * Call isl_basic_set_opt and translate the results.
564 __isl_give isl_val
*isl_basic_set_opt_val(__isl_keep isl_basic_set
*bset
,
565 int max
, __isl_keep isl_aff
*obj
)
569 enum isl_lp_result lp_res
;
574 ctx
= isl_aff_get_ctx(obj
);
575 res
= isl_val_alloc(ctx
);
578 lp_res
= isl_basic_set_opt(bset
, max
, obj
, &res
->n
);
579 return convert_lp_result(lp_res
, res
, max
);
582 /* Return the maximum of the integer affine
583 * expression "obj" over the points in "bset".
585 * Return infinity or negative infinity if the optimal value is unbounded and
586 * NaN if "bset" is empty.
588 __isl_give isl_val
*isl_basic_set_max_val(__isl_keep isl_basic_set
*bset
,
589 __isl_keep isl_aff
*obj
)
591 return isl_basic_set_opt_val(bset
, 1, obj
);
594 /* Return the minimum (maximum if max is set) of the integer affine
595 * expression "obj" over the points in "set".
597 * Return infinity or negative infinity if the optimal value is unbounded and
598 * NaN if "bset" is empty.
600 * Call isl_set_opt and translate the results.
602 __isl_give isl_val
*isl_set_opt_val(__isl_keep isl_set
*set
, int max
,
603 __isl_keep isl_aff
*obj
)
607 enum isl_lp_result lp_res
;
612 ctx
= isl_aff_get_ctx(obj
);
613 res
= isl_val_alloc(ctx
);
616 lp_res
= isl_set_opt(set
, max
, obj
, &res
->n
);
617 return convert_lp_result(lp_res
, res
, max
);
620 /* Return the minimum of the integer affine
621 * expression "obj" over the points in "set".
623 * Return infinity or negative infinity if the optimal value is unbounded and
624 * NaN if "bset" is empty.
626 __isl_give isl_val
*isl_set_min_val(__isl_keep isl_set
*set
,
627 __isl_keep isl_aff
*obj
)
629 return isl_set_opt_val(set
, 0, obj
);
632 /* Return the maximum of the integer affine
633 * expression "obj" over the points in "set".
635 * Return infinity or negative infinity if the optimal value is unbounded and
636 * NaN if "bset" is empty.
638 __isl_give isl_val
*isl_set_max_val(__isl_keep isl_set
*set
,
639 __isl_keep isl_aff
*obj
)
641 return isl_set_opt_val(set
, 1, obj
);