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(struct isl_basic_map
*bmap
, int maximize
,
26 isl_int
*f
, isl_int denom
, isl_int
*opt
,
31 enum isl_lp_result res
;
32 unsigned dim
= isl_basic_map_total_dim(bmap
);
35 isl_seq_neg(f
, f
, 1 + dim
);
37 bmap
= isl_basic_map_gauss(bmap
, NULL
);
38 tab
= isl_tab_from_basic_map(bmap
, 0);
39 res
= isl_tab_min(tab
, f
, denom
, opt
, opt_denom
, 0);
40 if (res
== isl_lp_ok
&& sol
) {
41 *sol
= isl_tab_get_sample_value(tab
);
48 isl_seq_neg(f
, f
, 1 + dim
);
50 isl_int_neg(*opt
, *opt
);
55 /* Given a basic map "bmap" and an affine combination of the variables "f"
56 * with denominator "denom", set *opt / *opt_denom to the minimal
57 * (or maximal if "maximize" is true) value attained by f/d over "bmap",
58 * assuming the basic map is not empty and the expression cannot attain
59 * arbitrarily small (or large) values.
60 * If opt_denom is NULL, then *opt is rounded up (or down)
61 * to the nearest integer.
62 * The return value reflects the nature of the result (empty, unbounded,
63 * minimal or maximal value returned in *opt).
65 enum isl_lp_result
isl_basic_map_solve_lp(struct isl_basic_map
*bmap
, int max
,
66 isl_int
*f
, isl_int d
, isl_int
*opt
,
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 unsigned total
= isl_space_dim(map
->dim
, isl_dim_all
);
113 v
= isl_vec_alloc(map
->ctx
, 1 + total
+ max_div
);
116 isl_seq_cpy(v
->el
, f
, 1 + total
);
117 isl_seq_clr(v
->el
+ 1 + total
, max_div
);
121 if (!opt
&& map
->n
> 1 && sol
) {
127 if (map
->n
> 0 && opt_denom
) {
128 isl_int_init(opt_denom_i
);
132 res
= isl_basic_map_solve_lp(map
->p
[0], max
, f
, d
,
133 opt
, opt_denom
, sol
);
134 if (res
== isl_lp_error
|| res
== isl_lp_unbounded
)
140 for (i
= 1; i
< map
->n
; ++i
) {
141 isl_vec
*sol_i
= NULL
;
142 enum isl_lp_result res_i
;
145 res_i
= isl_basic_map_solve_lp(map
->p
[i
], max
, f
, d
,
147 opt_denom
? &opt_denom_i
: NULL
,
148 sol
? &sol_i
: NULL
);
149 if (res_i
== isl_lp_error
|| res_i
== isl_lp_unbounded
) {
153 if (res_i
== isl_lp_empty
)
155 if (res
== isl_lp_empty
) {
157 } else if (!opt_denom
) {
159 better
= isl_int_gt(opt_i
, *opt
);
161 better
= isl_int_lt(opt_i
, *opt
);
163 isl_int_mul(t
, opt_i
, *opt_denom
);
164 isl_int_submul(t
, *opt
, opt_denom_i
);
166 better
= isl_int_is_pos(t
);
168 better
= isl_int_is_neg(t
);
173 isl_int_set(*opt
, opt_i
);
175 isl_int_set(*opt_denom
, opt_denom_i
);
186 if (map
->n
> 0 && opt_denom
) {
187 isl_int_clear(opt_denom_i
);
191 isl_int_clear(opt_i
);
197 enum isl_lp_result
isl_set_solve_lp(__isl_keep isl_set
*set
, int max
,
198 isl_int
*f
, isl_int d
, isl_int
*opt
,
200 struct isl_vec
**sol
)
202 return isl_map_solve_lp(set_to_map(set
), max
,
203 f
, d
, opt
, opt_denom
, sol
);
206 /* Return the optimal (rational) value of "obj" over "bset", assuming
207 * that "obj" and "bset" have aligned parameters and divs.
208 * If "max" is set, then the maximal value is computed.
209 * Otherwise, the minimal value is computed.
211 * Return infinity or negative infinity if the optimal value is unbounded and
212 * NaN if "bset" is empty.
214 * Call isl_basic_set_solve_lp and translate the results.
216 static __isl_give isl_val
*basic_set_opt_lp(
217 __isl_keep isl_basic_set
*bset
, int max
, __isl_keep isl_aff
*obj
)
221 enum isl_lp_result lp_res
;
226 ctx
= isl_aff_get_ctx(obj
);
227 res
= isl_val_alloc(ctx
);
230 lp_res
= isl_basic_set_solve_lp(bset
, max
, obj
->v
->el
+ 1,
231 obj
->v
->el
[0], &res
->n
, &res
->d
, NULL
);
232 if (lp_res
== isl_lp_ok
)
233 return isl_val_normalize(res
);
235 if (lp_res
== isl_lp_error
)
237 if (lp_res
== isl_lp_empty
)
238 return isl_val_nan(ctx
);
240 return isl_val_infty(ctx
);
242 return isl_val_neginfty(ctx
);
245 /* Return the optimal (rational) value of "obj" over "bset", assuming
246 * that "obj" and "bset" have aligned parameters.
247 * If "max" is set, then the maximal value is computed.
248 * Otherwise, the minimal value is computed.
250 * Return infinity or negative infinity if the optimal value is unbounded and
251 * NaN if "bset" is empty.
253 * Align the divs of "bset" and "obj" and call basic_set_opt_lp.
255 static __isl_give isl_val
*isl_basic_set_opt_lp_val_aligned(
256 __isl_keep isl_basic_set
*bset
, int max
, __isl_keep isl_aff
*obj
)
261 isl_mat
*bset_div
= NULL
;
264 int bset_n_div
, obj_n_div
;
269 ctx
= isl_aff_get_ctx(obj
);
270 if (!isl_space_is_equal(bset
->dim
, obj
->ls
->dim
))
271 isl_die(ctx
, isl_error_invalid
,
272 "spaces don't match", return NULL
);
274 bset_n_div
= isl_basic_set_dim(bset
, isl_dim_div
);
275 obj_n_div
= isl_aff_dim(obj
, isl_dim_div
);
276 if (bset_n_div
== 0 && obj_n_div
== 0)
277 return basic_set_opt_lp(bset
, max
, obj
);
279 bset
= isl_basic_set_copy(bset
);
280 obj
= isl_aff_copy(obj
);
282 bset_div
= isl_basic_set_get_divs(bset
);
283 exp1
= isl_alloc_array(ctx
, int, bset_n_div
);
284 exp2
= isl_alloc_array(ctx
, int, obj_n_div
);
285 if (!bset_div
|| (bset_n_div
&& !exp1
) || (obj_n_div
&& !exp2
))
288 div
= isl_merge_divs(bset_div
, obj
->ls
->div
, exp1
, exp2
);
290 bset
= isl_basic_set_expand_divs(bset
, isl_mat_copy(div
), exp1
);
291 obj
= isl_aff_expand_divs(obj
, isl_mat_copy(div
), exp2
);
293 res
= basic_set_opt_lp(bset
, max
, obj
);
295 isl_mat_free(bset_div
);
299 isl_basic_set_free(bset
);
305 isl_mat_free(bset_div
);
308 isl_basic_set_free(bset
);
313 /* Return the optimal (rational) value of "obj" over "bset".
314 * If "max" is set, then the maximal value is computed.
315 * Otherwise, the minimal value is computed.
317 * Return infinity or negative infinity if the optimal value is unbounded and
318 * NaN if "bset" is empty.
320 static __isl_give isl_val
*isl_basic_set_opt_lp_val(
321 __isl_keep isl_basic_set
*bset
, int max
, __isl_keep isl_aff
*obj
)
329 equal
= isl_basic_set_space_has_equal_params(bset
, obj
->ls
->dim
);
333 return isl_basic_set_opt_lp_val_aligned(bset
, max
, obj
);
335 bset
= isl_basic_set_copy(bset
);
336 obj
= isl_aff_copy(obj
);
337 bset
= isl_basic_set_align_params(bset
, isl_aff_get_domain_space(obj
));
338 obj
= isl_aff_align_params(obj
, isl_basic_set_get_space(bset
));
340 res
= isl_basic_set_opt_lp_val_aligned(bset
, max
, obj
);
342 isl_basic_set_free(bset
);
348 /* Return the minimal (rational) value of "obj" over "bset".
350 * Return negative infinity if the minimal value is unbounded and
351 * NaN if "bset" is empty.
353 __isl_give isl_val
*isl_basic_set_min_lp_val(__isl_keep isl_basic_set
*bset
,
354 __isl_keep isl_aff
*obj
)
356 return isl_basic_set_opt_lp_val(bset
, 0, obj
);
359 /* Return the maximal (rational) value of "obj" over "bset".
361 * Return infinity if the maximal value is unbounded and
362 * NaN if "bset" is empty.
364 __isl_give isl_val
*isl_basic_set_max_lp_val(__isl_keep isl_basic_set
*bset
,
365 __isl_keep isl_aff
*obj
)
367 return isl_basic_set_opt_lp_val(bset
, 1, obj
);