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/union_set.h>
14 #include "isl_sample.h"
16 #include "isl_equalities.h"
17 #include <isl_aff_private.h>
18 #include <isl_local_space_private.h>
19 #include <isl_mat_private.h>
20 #include <isl_val_private.h>
21 #include <isl_vec_private.h>
22 #include <isl_lp_private.h>
23 #include <isl_ilp_private.h>
24 #include <isl/deprecated/ilp_int.h>
26 /* Given a basic set "bset", construct a basic set U such that for
27 * each element x in U, the whole unit box positioned at x is inside
28 * the given basic set.
29 * Note that U may not contain all points that satisfy this property.
31 * We simply add the sum of all negative coefficients to the constant
32 * term. This ensures that if x satisfies the resulting constraints,
33 * then x plus any sum of unit vectors satisfies the original constraints.
35 static __isl_give isl_basic_set
*unit_box_base_points(
36 __isl_take isl_basic_set
*bset
)
39 struct isl_basic_set
*unit_box
= NULL
;
45 if (bset
->n_eq
!= 0) {
46 isl_space
*space
= isl_basic_set_get_space(bset
);
47 isl_basic_set_free(bset
);
48 return isl_basic_set_empty(space
);
51 total
= isl_basic_set_total_dim(bset
);
52 unit_box
= isl_basic_set_alloc_space(isl_basic_set_get_space(bset
),
55 for (i
= 0; i
< bset
->n_ineq
; ++i
) {
56 k
= isl_basic_set_alloc_inequality(unit_box
);
59 isl_seq_cpy(unit_box
->ineq
[k
], bset
->ineq
[i
], 1 + total
);
60 for (j
= 0; j
< total
; ++j
) {
61 if (isl_int_is_nonneg(unit_box
->ineq
[k
][1 + j
]))
63 isl_int_add(unit_box
->ineq
[k
][0],
64 unit_box
->ineq
[k
][0], unit_box
->ineq
[k
][1 + j
]);
68 isl_basic_set_free(bset
);
71 isl_basic_set_free(bset
);
72 isl_basic_set_free(unit_box
);
76 /* Find an integer point in "bset", preferably one that is
77 * close to minimizing "f".
79 * We first check if we can easily put unit boxes inside bset.
80 * If so, we take the best base point of any of the unit boxes we can find
81 * and round it up to the nearest integer.
82 * If not, we simply pick any integer point in "bset".
84 static __isl_give isl_vec
*initial_solution(__isl_keep isl_basic_set
*bset
,
87 enum isl_lp_result res
;
88 struct isl_basic_set
*unit_box
;
91 unit_box
= unit_box_base_points(isl_basic_set_copy(bset
));
93 res
= isl_basic_set_solve_lp(unit_box
, 0, f
, bset
->ctx
->one
,
95 if (res
== isl_lp_ok
) {
96 isl_basic_set_free(unit_box
);
97 return isl_vec_ceil(sol
);
100 isl_basic_set_free(unit_box
);
102 return isl_basic_set_sample_vec(isl_basic_set_copy(bset
));
105 /* Restrict "bset" to those points with values for f in the interval [l, u].
107 static __isl_give isl_basic_set
*add_bounds(__isl_take isl_basic_set
*bset
,
108 isl_int
*f
, isl_int l
, isl_int u
)
113 total
= isl_basic_set_total_dim(bset
);
114 bset
= isl_basic_set_extend_constraints(bset
, 0, 2);
116 k
= isl_basic_set_alloc_inequality(bset
);
119 isl_seq_cpy(bset
->ineq
[k
], f
, 1 + total
);
120 isl_int_sub(bset
->ineq
[k
][0], bset
->ineq
[k
][0], l
);
122 k
= isl_basic_set_alloc_inequality(bset
);
125 isl_seq_neg(bset
->ineq
[k
], f
, 1 + total
);
126 isl_int_add(bset
->ineq
[k
][0], bset
->ineq
[k
][0], u
);
130 isl_basic_set_free(bset
);
134 /* Find an integer point in "bset" that minimizes f (in any) such that
135 * the value of f lies inside the interval [l, u].
136 * Return this integer point if it can be found.
137 * Otherwise, return sol.
139 * We perform a number of steps until l > u.
140 * In each step, we look for an integer point with value in either
141 * the whole interval [l, u] or half of the interval [l, l+floor(u-l-1/2)].
142 * The choice depends on whether we have found an integer point in the
143 * previous step. If so, we look for the next point in half of the remaining
145 * If we find a point, the current solution is updated and u is set
146 * to its value minus 1.
147 * If no point can be found, we update l to the upper bound of the interval
148 * we checked (u or l+floor(u-l-1/2)) plus 1.
150 static __isl_give isl_vec
*solve_ilp_search(__isl_keep isl_basic_set
*bset
,
151 isl_int
*f
, isl_int
*opt
, __isl_take isl_vec
*sol
, isl_int l
, isl_int u
)
158 while (isl_int_le(l
, u
)) {
159 struct isl_basic_set
*slice
;
160 struct isl_vec
*sample
;
165 isl_int_sub(tmp
, u
, l
);
166 isl_int_fdiv_q_ui(tmp
, tmp
, 2);
167 isl_int_add(tmp
, tmp
, l
);
169 slice
= add_bounds(isl_basic_set_copy(bset
), f
, l
, tmp
);
170 sample
= isl_basic_set_sample_vec(slice
);
176 if (sample
->size
> 0) {
179 isl_seq_inner_product(f
, sol
->el
, sol
->size
, opt
);
180 isl_int_sub_ui(u
, *opt
, 1);
183 isl_vec_free(sample
);
186 isl_int_add_ui(l
, tmp
, 1);
196 /* Find an integer point in "bset" that minimizes f (if any).
197 * If sol_p is not NULL then the integer point is returned in *sol_p.
198 * The optimal value of f is returned in *opt.
200 * The algorithm maintains a currently best solution and an interval [l, u]
201 * of values of f for which integer solutions could potentially still be found.
202 * The initial value of the best solution so far is any solution.
203 * The initial value of l is minimal value of f over the rationals
204 * (rounded up to the nearest integer).
205 * The initial value of u is the value of f at the initial solution minus 1.
207 * We then call solve_ilp_search to perform a binary search on the interval.
209 static enum isl_lp_result
solve_ilp(__isl_keep isl_basic_set
*bset
,
210 isl_int
*f
, isl_int
*opt
, __isl_give isl_vec
**sol_p
)
212 enum isl_lp_result res
;
216 res
= isl_basic_set_solve_lp(bset
, 0, f
, bset
->ctx
->one
,
218 if (res
== isl_lp_ok
&& isl_int_is_one(sol
->el
[0])) {
226 if (res
== isl_lp_error
|| res
== isl_lp_empty
)
229 sol
= initial_solution(bset
, f
);
232 if (sol
->size
== 0) {
236 if (res
== isl_lp_unbounded
) {
238 return isl_lp_unbounded
;
244 isl_int_set(l
, *opt
);
246 isl_seq_inner_product(f
, sol
->el
, sol
->size
, opt
);
247 isl_int_sub_ui(u
, *opt
, 1);
249 sol
= solve_ilp_search(bset
, f
, opt
, sol
, l
, u
);
264 static enum isl_lp_result
solve_ilp_with_eq(__isl_keep isl_basic_set
*bset
,
265 int max
, isl_int
*f
, isl_int
*opt
, __isl_give isl_vec
**sol_p
)
268 enum isl_lp_result res
;
269 struct isl_mat
*T
= NULL
;
272 bset
= isl_basic_set_copy(bset
);
273 dim
= isl_basic_set_total_dim(bset
);
274 v
= isl_vec_alloc(bset
->ctx
, 1 + dim
);
277 isl_seq_cpy(v
->el
, f
, 1 + dim
);
278 bset
= isl_basic_set_remove_equalities(bset
, &T
, NULL
);
279 v
= isl_vec_mat_product(v
, isl_mat_copy(T
));
282 res
= isl_basic_set_solve_ilp(bset
, max
, v
->el
, opt
, sol_p
);
284 if (res
== isl_lp_ok
&& sol_p
) {
285 *sol_p
= isl_mat_vec_product(T
, *sol_p
);
290 isl_basic_set_free(bset
);
294 isl_basic_set_free(bset
);
298 /* Find an integer point in "bset" that minimizes (or maximizes if max is set)
300 * If sol_p is not NULL then the integer point is returned in *sol_p.
301 * The optimal value of f is returned in *opt.
303 * If there is any equality among the points in "bset", then we first
304 * project it out. Otherwise, we continue with solve_ilp above.
306 enum isl_lp_result
isl_basic_set_solve_ilp(struct isl_basic_set
*bset
, int max
,
307 isl_int
*f
, isl_int
*opt
,
308 struct isl_vec
**sol_p
)
311 enum isl_lp_result res
;
318 isl_assert(bset
->ctx
, isl_basic_set_n_param(bset
) == 0,
319 return isl_lp_error
);
321 if (isl_basic_set_plain_is_empty(bset
))
325 return solve_ilp_with_eq(bset
, max
, f
, opt
, sol_p
);
327 dim
= isl_basic_set_total_dim(bset
);
330 isl_seq_neg(f
, f
, 1 + dim
);
332 res
= solve_ilp(bset
, f
, opt
, sol_p
);
335 isl_seq_neg(f
, f
, 1 + dim
);
336 isl_int_neg(*opt
, *opt
);
342 static enum isl_lp_result
basic_set_opt(__isl_keep isl_basic_set
*bset
, int max
,
343 __isl_keep isl_aff
*obj
, isl_int
*opt
)
345 enum isl_lp_result res
;
349 bset
= isl_basic_set_copy(bset
);
350 bset
= isl_basic_set_underlying_set(bset
);
351 res
= isl_basic_set_solve_ilp(bset
, max
, obj
->v
->el
+ 1, opt
, NULL
);
352 isl_basic_set_free(bset
);
356 static __isl_give isl_mat
*extract_divs(__isl_keep isl_basic_set
*bset
)
359 isl_ctx
*ctx
= isl_basic_set_get_ctx(bset
);
362 div
= isl_mat_alloc(ctx
, bset
->n_div
,
363 1 + 1 + isl_basic_set_total_dim(bset
));
367 for (i
= 0; i
< bset
->n_div
; ++i
)
368 isl_seq_cpy(div
->row
[i
], bset
->div
[i
], div
->n_col
);
373 enum isl_lp_result
isl_basic_set_opt(__isl_keep isl_basic_set
*bset
, int max
,
374 __isl_keep isl_aff
*obj
, isl_int
*opt
)
379 isl_mat
*bset_div
= NULL
;
381 enum isl_lp_result res
;
382 int bset_n_div
, obj_n_div
;
387 ctx
= isl_aff_get_ctx(obj
);
388 if (!isl_space_is_equal(bset
->dim
, obj
->ls
->dim
))
389 isl_die(ctx
, isl_error_invalid
,
390 "spaces don't match", return isl_lp_error
);
391 if (!isl_int_is_one(obj
->v
->el
[0]))
392 isl_die(ctx
, isl_error_unsupported
,
393 "expecting integer affine expression",
394 return isl_lp_error
);
396 bset_n_div
= isl_basic_set_dim(bset
, isl_dim_div
);
397 obj_n_div
= isl_aff_dim(obj
, isl_dim_div
);
398 if (bset_n_div
== 0 && obj_n_div
== 0)
399 return basic_set_opt(bset
, max
, obj
, opt
);
401 bset
= isl_basic_set_copy(bset
);
402 obj
= isl_aff_copy(obj
);
404 bset_div
= extract_divs(bset
);
405 exp1
= isl_alloc_array(ctx
, int, bset_n_div
);
406 exp2
= isl_alloc_array(ctx
, int, obj_n_div
);
407 if (!bset_div
|| (bset_n_div
&& !exp1
) || (obj_n_div
&& !exp2
))
410 div
= isl_merge_divs(bset_div
, obj
->ls
->div
, exp1
, exp2
);
412 bset
= isl_basic_set_expand_divs(bset
, isl_mat_copy(div
), exp1
);
413 obj
= isl_aff_expand_divs(obj
, isl_mat_copy(div
), exp2
);
415 res
= basic_set_opt(bset
, max
, obj
, opt
);
417 isl_mat_free(bset_div
);
421 isl_basic_set_free(bset
);
427 isl_mat_free(bset_div
);
430 isl_basic_set_free(bset
);
435 /* Compute the minimum (maximum if max is set) of the integer affine
436 * expression obj over the points in set and put the result in *opt.
438 * The parameters are assumed to have been aligned.
440 static enum isl_lp_result
isl_set_opt_aligned(__isl_keep isl_set
*set
, int max
,
441 __isl_keep isl_aff
*obj
, isl_int
*opt
)
444 enum isl_lp_result res
;
453 res
= isl_basic_set_opt(set
->p
[0], max
, obj
, opt
);
454 if (res
== isl_lp_error
|| res
== isl_lp_unbounded
)
458 if (res
== isl_lp_ok
)
462 for (i
= 1; i
< set
->n
; ++i
) {
463 res
= isl_basic_set_opt(set
->p
[i
], max
, obj
, &opt_i
);
464 if (res
== isl_lp_error
|| res
== isl_lp_unbounded
) {
465 isl_int_clear(opt_i
);
468 if (res
== isl_lp_empty
)
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
;
491 aligned
= isl_set_space_has_equal_params(set
, obj
->ls
->dim
);
495 return isl_set_opt_aligned(set
, max
, obj
, opt
);
497 set
= isl_set_copy(set
);
498 obj
= isl_aff_copy(obj
);
499 set
= isl_set_align_params(set
, isl_aff_get_domain_space(obj
));
500 obj
= isl_aff_align_params(obj
, isl_set_get_space(set
));
502 res
= isl_set_opt_aligned(set
, max
, obj
, opt
);
510 enum isl_lp_result
isl_basic_set_max(__isl_keep isl_basic_set
*bset
,
511 __isl_keep isl_aff
*obj
, isl_int
*opt
)
513 return isl_basic_set_opt(bset
, 1, obj
, opt
);
516 enum isl_lp_result
isl_set_max(__isl_keep isl_set
*set
,
517 __isl_keep isl_aff
*obj
, isl_int
*opt
)
519 return isl_set_opt(set
, 1, obj
, opt
);
522 enum isl_lp_result
isl_set_min(__isl_keep isl_set
*set
,
523 __isl_keep isl_aff
*obj
, isl_int
*opt
)
525 return isl_set_opt(set
, 0, obj
, opt
);
528 /* Convert the result of a function that returns an isl_lp_result
529 * to an isl_val. The numerator of "v" is set to the optimal value
530 * if lp_res is isl_lp_ok. "max" is set if a maximum was computed.
532 * Return "v" with denominator set to 1 if lp_res is isl_lp_ok.
533 * Return NULL on error.
534 * Return a NaN if lp_res is isl_lp_empty.
535 * Return infinity or negative infinity if lp_res is isl_lp_unbounded,
536 * depending on "max".
538 static __isl_give isl_val
*convert_lp_result(enum isl_lp_result lp_res
,
539 __isl_take isl_val
*v
, int max
)
543 if (lp_res
== isl_lp_ok
) {
544 isl_int_set_si(v
->d
, 1);
545 return isl_val_normalize(v
);
547 ctx
= isl_val_get_ctx(v
);
549 if (lp_res
== isl_lp_error
)
551 if (lp_res
== isl_lp_empty
)
552 return isl_val_nan(ctx
);
554 return isl_val_infty(ctx
);
556 return isl_val_neginfty(ctx
);
559 /* Return the minimum (maximum if max is set) of the integer affine
560 * expression "obj" over the points in "bset".
562 * Return infinity or negative infinity if the optimal value is unbounded and
563 * NaN if "bset" is empty.
565 * Call isl_basic_set_opt and translate the results.
567 __isl_give isl_val
*isl_basic_set_opt_val(__isl_keep isl_basic_set
*bset
,
568 int max
, __isl_keep isl_aff
*obj
)
572 enum isl_lp_result lp_res
;
577 ctx
= isl_aff_get_ctx(obj
);
578 res
= isl_val_alloc(ctx
);
581 lp_res
= isl_basic_set_opt(bset
, max
, obj
, &res
->n
);
582 return convert_lp_result(lp_res
, res
, max
);
585 /* Return the maximum of the integer affine
586 * expression "obj" over the points in "bset".
588 * Return infinity or negative infinity if the optimal value is unbounded and
589 * NaN if "bset" is empty.
591 __isl_give isl_val
*isl_basic_set_max_val(__isl_keep isl_basic_set
*bset
,
592 __isl_keep isl_aff
*obj
)
594 return isl_basic_set_opt_val(bset
, 1, obj
);
597 /* Return the minimum (maximum if max is set) of the integer affine
598 * expression "obj" over the points in "set".
600 * Return infinity or negative infinity if the optimal value is unbounded and
601 * NaN if "set" is empty.
603 * Call isl_set_opt and translate the results.
605 __isl_give isl_val
*isl_set_opt_val(__isl_keep isl_set
*set
, int max
,
606 __isl_keep isl_aff
*obj
)
610 enum isl_lp_result lp_res
;
615 ctx
= isl_aff_get_ctx(obj
);
616 res
= isl_val_alloc(ctx
);
619 lp_res
= isl_set_opt(set
, max
, obj
, &res
->n
);
620 return convert_lp_result(lp_res
, res
, max
);
623 /* Return the minimum of the integer affine
624 * expression "obj" over the points in "set".
626 * Return infinity or negative infinity if the optimal value is unbounded and
627 * NaN if "set" is empty.
629 __isl_give isl_val
*isl_set_min_val(__isl_keep isl_set
*set
,
630 __isl_keep isl_aff
*obj
)
632 return isl_set_opt_val(set
, 0, obj
);
635 /* Return the maximum of the integer affine
636 * expression "obj" over the points in "set".
638 * Return infinity or negative infinity if the optimal value is unbounded and
639 * NaN if "set" is empty.
641 __isl_give isl_val
*isl_set_max_val(__isl_keep isl_set
*set
,
642 __isl_keep isl_aff
*obj
)
644 return isl_set_opt_val(set
, 1, obj
);
647 /* Return the optimum (min or max depending on "max") of "v1" and "v2",
648 * where either may be NaN, signifying an uninitialized value.
649 * That is, if either is NaN, then return the other one.
651 static __isl_give isl_val
*val_opt(__isl_take isl_val
*v1
,
652 __isl_take isl_val
*v2
, int max
)
656 if (isl_val_is_nan(v1
)) {
660 if (isl_val_is_nan(v2
)) {
665 return isl_val_max(v1
, v2
);
667 return isl_val_min(v1
, v2
);
674 /* Internal data structure for isl_set_opt_pw_aff.
676 * "max" is set if the maximum should be computed.
677 * "set" is the set over which the optimum should be computed.
678 * "res" contains the current optimum and is initialized to NaN.
680 struct isl_set_opt_data
{
687 /* Update the optimum in data->res with respect to the affine function
688 * "aff" defined over "set".
690 static isl_stat
piece_opt(__isl_take isl_set
*set
, __isl_take isl_aff
*aff
,
693 struct isl_set_opt_data
*data
= user
;
696 set
= isl_set_intersect(set
, isl_set_copy(data
->set
));
697 opt
= isl_set_opt_val(set
, data
->max
, aff
);
701 data
->res
= val_opt(data
->res
, opt
, data
->max
);
703 return isl_stat_error
;
708 /* Return the minimum (maximum if "max" is set) of the integer piecewise affine
709 * expression "obj" over the points in "set".
711 * Return infinity or negative infinity if the optimal value is unbounded and
712 * NaN if the intersection of "set" with the domain of "obj" is empty.
714 * Initialize the result to NaN and then update it for each of the pieces
717 static __isl_give isl_val
*isl_set_opt_pw_aff(__isl_keep isl_set
*set
, int max
,
718 __isl_keep isl_pw_aff
*obj
)
720 struct isl_set_opt_data data
= { max
, set
};
722 data
.res
= isl_val_nan(isl_set_get_ctx(set
));
723 if (isl_pw_aff_foreach_piece(obj
, &piece_opt
, &data
) < 0)
724 return isl_val_free(data
.res
);
729 /* Internal data structure for isl_union_set_opt_union_pw_aff.
731 * "max" is set if the maximum should be computed.
732 * "obj" is the objective function that needs to be optimized.
733 * "res" contains the current optimum and is initialized to NaN.
735 struct isl_union_set_opt_data
{
737 isl_union_pw_aff
*obj
;
742 /* Update the optimum in data->res with the optimum over "set".
743 * Do so by first extracting the matching objective function
746 static isl_stat
set_opt(__isl_take isl_set
*set
, void *user
)
748 struct isl_union_set_opt_data
*data
= user
;
753 space
= isl_set_get_space(set
);
754 space
= isl_space_from_domain(space
);
755 space
= isl_space_add_dims(space
, isl_dim_out
, 1);
756 pa
= isl_union_pw_aff_extract_pw_aff(data
->obj
, space
);
757 opt
= isl_set_opt_pw_aff(set
, data
->max
, pa
);
761 data
->res
= val_opt(data
->res
, opt
, data
->max
);
763 return isl_stat_error
;
768 /* Return the minimum (maximum if "max" is set) of the integer piecewise affine
769 * expression "obj" over the points in "uset".
771 * Return infinity or negative infinity if the optimal value is unbounded and
772 * NaN if the intersection of "uset" with the domain of "obj" is empty.
774 * Initialize the result to NaN and then update it for each of the sets
777 static __isl_give isl_val
*isl_union_set_opt_union_pw_aff(
778 __isl_keep isl_union_set
*uset
, int max
,
779 __isl_keep isl_union_pw_aff
*obj
)
781 struct isl_union_set_opt_data data
= { max
, obj
};
783 data
.res
= isl_val_nan(isl_union_set_get_ctx(uset
));
784 if (isl_union_set_foreach_set(uset
, &set_opt
, &data
) < 0)
785 return isl_val_free(data
.res
);
790 /* Return a list of minima (maxima if "max" is set) over the points in "uset"
791 * for each of the expressions in "obj".
793 * An element in the list is infinity or negative infinity if the optimal
794 * value of the corresponding expression is unbounded and
795 * NaN if the intersection of "uset" with the domain of the expression
798 * Iterate over all the expressions in "obj" and collect the results.
800 static __isl_give isl_multi_val
*isl_union_set_opt_multi_union_pw_aff(
801 __isl_keep isl_union_set
*uset
, int max
,
802 __isl_keep isl_multi_union_pw_aff
*obj
)
810 n
= isl_multi_union_pw_aff_dim(obj
, isl_dim_set
);
811 mv
= isl_multi_val_zero(isl_multi_union_pw_aff_get_space(obj
));
813 for (i
= 0; i
< n
; ++i
) {
815 isl_union_pw_aff
*upa
;
817 upa
= isl_multi_union_pw_aff_get_union_pw_aff(obj
, i
);
818 v
= isl_union_set_opt_union_pw_aff(uset
, max
, upa
);
819 isl_union_pw_aff_free(upa
);
820 mv
= isl_multi_val_set_val(mv
, i
, v
);
826 /* Return a list of minima over the points in "uset"
827 * for each of the expressions in "obj".
829 * An element in the list is infinity or negative infinity if the optimal
830 * value of the corresponding expression is unbounded and
831 * NaN if the intersection of "uset" with the domain of the expression
834 __isl_give isl_multi_val
*isl_union_set_min_multi_union_pw_aff(
835 __isl_keep isl_union_set
*uset
, __isl_keep isl_multi_union_pw_aff
*obj
)
837 return isl_union_set_opt_multi_union_pw_aff(uset
, 0, obj
);