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>
15 #include <isl_options_private.h>
16 #include <isl_local_space_private.h>
17 #include <isl_aff_private.h>
18 #include <isl_mat_private.h>
19 #include <isl_val_private.h>
20 #include <isl_vec_private.h>
22 #include <bset_to_bmap.c>
23 #include <set_to_map.c>
25 enum isl_lp_result
isl_tab_solve_lp(__isl_keep isl_basic_map
*bmap
,
26 int maximize
, isl_int
*f
, isl_int denom
, isl_int
*opt
,
27 isl_int
*opt_denom
, __isl_give isl_vec
**sol
)
30 enum isl_lp_result res
;
31 isl_size dim
= isl_basic_map_dim(bmap
, isl_dim_all
);
36 isl_seq_neg(f
, f
, 1 + dim
);
38 bmap
= isl_basic_map_gauss(bmap
, NULL
);
39 tab
= isl_tab_from_basic_map(bmap
, 0);
40 res
= isl_tab_min(tab
, f
, denom
, opt
, opt_denom
, 0);
41 if (res
== isl_lp_ok
&& sol
) {
42 *sol
= isl_tab_get_sample_value(tab
);
49 isl_seq_neg(f
, f
, 1 + dim
);
51 isl_int_neg(*opt
, *opt
);
56 /* Given a basic map "bmap" and an affine combination of the variables "f"
57 * with denominator "denom", set *opt / *opt_denom to the minimal
58 * (or maximal if "maximize" is true) value attained by f/d over "bmap",
59 * assuming the basic map is not empty and the expression cannot attain
60 * arbitrarily small (or large) values.
61 * If opt_denom is NULL, then *opt is rounded up (or down)
62 * to the nearest integer.
63 * The return value reflects the nature of the result (empty, unbounded,
64 * minimal or maximal value returned in *opt).
66 enum isl_lp_result
isl_basic_map_solve_lp(__isl_keep isl_basic_map
*bmap
,
67 int max
, isl_int
*f
, isl_int d
, isl_int
*opt
, isl_int
*opt_denom
,
68 __isl_give isl_vec
**sol
)
76 return isl_tab_solve_lp(bmap
, max
, f
, d
, opt
, opt_denom
, sol
);
79 enum isl_lp_result
isl_basic_set_solve_lp(struct isl_basic_set
*bset
, int max
,
80 isl_int
*f
, isl_int d
, isl_int
*opt
,
84 return isl_basic_map_solve_lp(bset_to_bmap(bset
), max
,
85 f
, d
, opt
, opt_denom
, sol
);
88 enum isl_lp_result
isl_map_solve_lp(__isl_keep isl_map
*map
, int max
,
89 isl_int
*f
, isl_int d
, isl_int
*opt
,
98 enum isl_lp_result res
;
108 for (i
= 0; i
< map
->n
; ++i
)
109 if (map
->p
[i
]->n_div
> max_div
)
110 max_div
= map
->p
[i
]->n_div
;
112 isl_size total
= isl_map_dim(map
, isl_dim_all
);
115 v
= isl_vec_alloc(map
->ctx
, 1 + total
+ max_div
);
118 isl_seq_cpy(v
->el
, f
, 1 + total
);
119 isl_seq_clr(v
->el
+ 1 + total
, max_div
);
123 if (!opt
&& map
->n
> 1 && sol
) {
129 if (map
->n
> 0 && opt_denom
) {
130 isl_int_init(opt_denom_i
);
134 res
= isl_basic_map_solve_lp(map
->p
[0], max
, f
, d
,
135 opt
, opt_denom
, sol
);
136 if (res
== isl_lp_error
|| res
== isl_lp_unbounded
)
142 for (i
= 1; i
< map
->n
; ++i
) {
143 isl_vec
*sol_i
= NULL
;
144 enum isl_lp_result res_i
;
147 res_i
= isl_basic_map_solve_lp(map
->p
[i
], max
, f
, d
,
149 opt_denom
? &opt_denom_i
: NULL
,
150 sol
? &sol_i
: NULL
);
151 if (res_i
== isl_lp_error
|| res_i
== isl_lp_unbounded
) {
155 if (res_i
== isl_lp_empty
)
157 if (res
== isl_lp_empty
) {
159 } else if (!opt_denom
) {
161 better
= isl_int_gt(opt_i
, *opt
);
163 better
= isl_int_lt(opt_i
, *opt
);
165 isl_int_mul(t
, opt_i
, *opt_denom
);
166 isl_int_submul(t
, *opt
, opt_denom_i
);
168 better
= isl_int_is_pos(t
);
170 better
= isl_int_is_neg(t
);
175 isl_int_set(*opt
, opt_i
);
177 isl_int_set(*opt_denom
, opt_denom_i
);
188 if (map
->n
> 0 && opt_denom
) {
189 isl_int_clear(opt_denom_i
);
193 isl_int_clear(opt_i
);
199 enum isl_lp_result
isl_set_solve_lp(__isl_keep isl_set
*set
, int max
,
200 isl_int
*f
, isl_int d
, isl_int
*opt
,
202 struct isl_vec
**sol
)
204 return isl_map_solve_lp(set_to_map(set
), max
,
205 f
, d
, opt
, opt_denom
, sol
);
208 /* Return the optimal (rational) value of "obj" over "bset", assuming
209 * that "obj" and "bset" have aligned parameters and divs.
210 * If "max" is set, then the maximal value is computed.
211 * Otherwise, the minimal value is computed.
213 * Return infinity or negative infinity if the optimal value is unbounded and
214 * NaN if "bset" is empty.
216 * Call isl_basic_set_solve_lp and translate the results.
218 static __isl_give isl_val
*basic_set_opt_lp(
219 __isl_keep isl_basic_set
*bset
, int max
, __isl_keep isl_aff
*obj
)
223 enum isl_lp_result lp_res
;
228 ctx
= isl_aff_get_ctx(obj
);
229 res
= isl_val_alloc(ctx
);
232 lp_res
= isl_basic_set_solve_lp(bset
, max
, obj
->v
->el
+ 1,
233 obj
->v
->el
[0], &res
->n
, &res
->d
, NULL
);
234 if (lp_res
== isl_lp_ok
)
235 return isl_val_normalize(res
);
237 if (lp_res
== isl_lp_error
)
239 if (lp_res
== isl_lp_empty
)
240 return isl_val_nan(ctx
);
242 return isl_val_infty(ctx
);
244 return isl_val_neginfty(ctx
);
247 /* Return the optimal (rational) value of "obj" over "bset", assuming
248 * that "obj" and "bset" have aligned parameters.
249 * If "max" is set, then the maximal value is computed.
250 * Otherwise, the minimal value is computed.
252 * Return infinity or negative infinity if the optimal value is unbounded and
253 * NaN if "bset" is empty.
255 * Align the divs of "bset" and "obj" and call basic_set_opt_lp.
257 static __isl_give isl_val
*isl_basic_set_opt_lp_val_aligned(
258 __isl_keep isl_basic_set
*bset
, int max
, __isl_keep isl_aff
*obj
)
263 isl_mat
*bset_div
= NULL
;
266 isl_size bset_n_div
, obj_n_div
;
271 ctx
= isl_aff_get_ctx(obj
);
272 if (!isl_space_is_equal(bset
->dim
, obj
->ls
->dim
))
273 isl_die(ctx
, isl_error_invalid
,
274 "spaces don't match", return NULL
);
276 bset_n_div
= isl_basic_set_dim(bset
, isl_dim_div
);
277 obj_n_div
= isl_aff_dim(obj
, isl_dim_div
);
278 if (bset_n_div
< 0 || obj_n_div
< 0)
280 if (bset_n_div
== 0 && obj_n_div
== 0)
281 return basic_set_opt_lp(bset
, max
, obj
);
283 bset
= isl_basic_set_copy(bset
);
284 obj
= isl_aff_copy(obj
);
286 bset_div
= isl_basic_set_get_divs(bset
);
287 exp1
= isl_alloc_array(ctx
, int, bset_n_div
);
288 exp2
= isl_alloc_array(ctx
, int, obj_n_div
);
289 if (!bset_div
|| (bset_n_div
&& !exp1
) || (obj_n_div
&& !exp2
))
292 div
= isl_merge_divs(bset_div
, obj
->ls
->div
, exp1
, exp2
);
294 bset
= isl_basic_set_expand_divs(bset
, isl_mat_copy(div
), exp1
);
295 obj
= isl_aff_expand_divs(obj
, isl_mat_copy(div
), exp2
);
297 res
= basic_set_opt_lp(bset
, max
, obj
);
299 isl_mat_free(bset_div
);
303 isl_basic_set_free(bset
);
309 isl_mat_free(bset_div
);
312 isl_basic_set_free(bset
);
317 /* Return the optimal (rational) value of "obj" over "bset".
318 * If "max" is set, then the maximal value is computed.
319 * Otherwise, the minimal value is computed.
321 * Return infinity or negative infinity if the optimal value is unbounded and
322 * NaN if "bset" is empty.
324 static __isl_give isl_val
*isl_basic_set_opt_lp_val(
325 __isl_keep isl_basic_set
*bset
, int max
, __isl_keep isl_aff
*obj
)
333 equal
= isl_basic_set_space_has_equal_params(bset
, obj
->ls
->dim
);
337 return isl_basic_set_opt_lp_val_aligned(bset
, max
, obj
);
339 bset
= isl_basic_set_copy(bset
);
340 obj
= isl_aff_copy(obj
);
341 bset
= isl_basic_set_align_params(bset
, isl_aff_get_domain_space(obj
));
342 obj
= isl_aff_align_params(obj
, isl_basic_set_get_space(bset
));
344 res
= isl_basic_set_opt_lp_val_aligned(bset
, max
, obj
);
346 isl_basic_set_free(bset
);
352 /* Return the minimal (rational) value of "obj" over "bset".
354 * Return negative infinity if the minimal value is unbounded and
355 * NaN if "bset" is empty.
357 __isl_give isl_val
*isl_basic_set_min_lp_val(__isl_keep isl_basic_set
*bset
,
358 __isl_keep isl_aff
*obj
)
360 return isl_basic_set_opt_lp_val(bset
, 0, obj
);
363 /* Return the maximal (rational) value of "obj" over "bset".
365 * Return infinity if the maximal value is unbounded and
366 * NaN if "bset" is empty.
368 __isl_give isl_val
*isl_basic_set_max_lp_val(__isl_keep isl_basic_set
*bset
,
369 __isl_keep isl_aff
*obj
)
371 return isl_basic_set_opt_lp_val(bset
, 1, obj
);