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_lp_piplib.h"
16 #include <isl_options_private.h>
17 #include <isl_local_space_private.h>
18 #include <isl_aff_private.h>
19 #include <isl_mat_private.h>
20 #include <isl_val_private.h>
22 enum isl_lp_result
isl_tab_solve_lp(struct isl_basic_map
*bmap
, int maximize
,
23 isl_int
*f
, isl_int denom
, isl_int
*opt
,
28 enum isl_lp_result res
;
29 unsigned dim
= isl_basic_map_total_dim(bmap
);
32 isl_seq_neg(f
, f
, 1 + dim
);
34 bmap
= isl_basic_map_gauss(bmap
, NULL
);
35 tab
= isl_tab_from_basic_map(bmap
, 0);
36 res
= isl_tab_min(tab
, f
, denom
, opt
, opt_denom
, 0);
37 if (res
== isl_lp_ok
&& sol
) {
38 *sol
= isl_tab_get_sample_value(tab
);
45 isl_seq_neg(f
, f
, 1 + dim
);
47 isl_int_neg(*opt
, *opt
);
52 /* Given a basic map "bmap" and an affine combination of the variables "f"
53 * with denominator "denom", set *opt / *opt_denom to the minimal
54 * (or maximal if "maximize" is true) value attained by f/d over "bmap",
55 * assuming the basic map is not empty and the expression cannot attain
56 * arbitrarily small (or large) values.
57 * If opt_denom is NULL, then *opt is rounded up (or down)
58 * to the nearest integer.
59 * The return value reflects the nature of the result (empty, unbounded,
60 * minmimal or maximal value returned in *opt).
62 enum isl_lp_result
isl_basic_map_solve_lp(struct isl_basic_map
*bmap
, int max
,
63 isl_int
*f
, isl_int d
, isl_int
*opt
,
73 switch (bmap
->ctx
->opt
->lp_solver
) {
75 return isl_pip_solve_lp(bmap
, max
, f
, d
, opt
, opt_denom
, sol
);
77 return isl_tab_solve_lp(bmap
, max
, f
, d
, opt
, opt_denom
, sol
);
83 enum isl_lp_result
isl_basic_set_solve_lp(struct isl_basic_set
*bset
, int max
,
84 isl_int
*f
, isl_int d
, isl_int
*opt
,
88 return isl_basic_map_solve_lp((struct isl_basic_map
*)bset
, max
,
89 f
, d
, opt
, opt_denom
, sol
);
92 enum isl_lp_result
isl_map_solve_lp(__isl_keep isl_map
*map
, int max
,
93 isl_int
*f
, isl_int d
, isl_int
*opt
,
102 enum isl_lp_result res
;
112 for (i
= 0; i
< map
->n
; ++i
)
113 if (map
->p
[i
]->n_div
> max_div
)
114 max_div
= map
->p
[i
]->n_div
;
116 unsigned total
= isl_space_dim(map
->dim
, isl_dim_all
);
117 v
= isl_vec_alloc(map
->ctx
, 1 + total
+ max_div
);
120 isl_seq_cpy(v
->el
, f
, 1 + total
);
121 isl_seq_clr(v
->el
+ 1 + total
, max_div
);
125 if (!opt
&& map
->n
> 1 && sol
) {
131 if (map
->n
> 0 && opt_denom
) {
132 isl_int_init(opt_denom_i
);
136 res
= isl_basic_map_solve_lp(map
->p
[0], max
, f
, d
,
137 opt
, opt_denom
, sol
);
138 if (res
== isl_lp_error
|| res
== isl_lp_unbounded
)
144 for (i
= 1; i
< map
->n
; ++i
) {
145 isl_vec
*sol_i
= NULL
;
146 enum isl_lp_result res_i
;
149 res_i
= isl_basic_map_solve_lp(map
->p
[i
], max
, f
, d
,
151 opt_denom
? &opt_denom_i
: NULL
,
152 sol
? &sol_i
: NULL
);
153 if (res_i
== isl_lp_error
|| res_i
== isl_lp_unbounded
) {
157 if (res_i
== isl_lp_empty
)
159 if (res
== isl_lp_empty
) {
161 } else if (!opt_denom
) {
163 better
= isl_int_gt(opt_i
, *opt
);
165 better
= isl_int_lt(opt_i
, *opt
);
167 isl_int_mul(t
, opt_i
, *opt_denom
);
168 isl_int_submul(t
, *opt
, opt_denom_i
);
170 better
= isl_int_is_pos(t
);
172 better
= isl_int_is_neg(t
);
177 isl_int_set(*opt
, opt_i
);
179 isl_int_set(*opt_denom
, opt_denom_i
);
190 if (map
->n
> 0 && opt_denom
) {
191 isl_int_clear(opt_denom_i
);
195 isl_int_clear(opt_i
);
201 enum isl_lp_result
isl_set_solve_lp(__isl_keep isl_set
*set
, int max
,
202 isl_int
*f
, isl_int d
, isl_int
*opt
,
204 struct isl_vec
**sol
)
206 return isl_map_solve_lp((struct isl_map
*)set
, max
,
207 f
, d
, opt
, opt_denom
, sol
);
210 /* Return the optimal (rational) value of "obj" over "bset", assuming
211 * that "obj" and "bset" have aligned parameters and divs.
212 * If "max" is set, then the maximal value is computed.
213 * Otherwise, the minimal value is computed.
215 * Return infinity or negative infinity if the optimal value is unbounded and
216 * NaN if "bset" is empty.
218 * Call isl_basic_set_solve_lp and translate the results.
220 static __isl_give isl_val
*basic_set_opt_lp(
221 __isl_keep isl_basic_set
*bset
, int max
, __isl_keep isl_aff
*obj
)
225 enum isl_lp_result lp_res
;
230 ctx
= isl_aff_get_ctx(obj
);
231 res
= isl_val_alloc(ctx
);
234 lp_res
= isl_basic_set_solve_lp(bset
, max
, obj
->v
->el
+ 1,
235 obj
->v
->el
[0], &res
->n
, &res
->d
, NULL
);
236 if (lp_res
== isl_lp_ok
)
237 return isl_val_normalize(res
);
239 if (lp_res
== isl_lp_error
)
241 if (lp_res
== isl_lp_empty
)
242 return isl_val_nan(ctx
);
244 return isl_val_infty(ctx
);
246 return isl_val_neginfty(ctx
);
249 /* Return the optimal (rational) value of "obj" over "bset", assuming
250 * that "obj" and "bset" have aligned parameters.
251 * If "max" is set, then the maximal value is computed.
252 * Otherwise, the minimal value is computed.
254 * Return infinity or negative infinity if the optimal value is unbounded and
255 * NaN if "bset" is empty.
257 * Align the divs of "bset" and "obj" and call basic_set_opt_lp.
259 static __isl_give isl_val
*isl_basic_set_opt_lp_val_aligned(
260 __isl_keep isl_basic_set
*bset
, int max
, __isl_keep isl_aff
*obj
)
265 isl_mat
*bset_div
= NULL
;
268 int bset_n_div
, obj_n_div
;
273 ctx
= isl_aff_get_ctx(obj
);
274 if (!isl_space_is_equal(bset
->dim
, obj
->ls
->dim
))
275 isl_die(ctx
, isl_error_invalid
,
276 "spaces don't match", return NULL
);
278 bset_n_div
= isl_basic_set_dim(bset
, isl_dim_div
);
279 obj_n_div
= isl_aff_dim(obj
, isl_dim_div
);
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
)
332 if (isl_space_match(bset
->dim
, isl_dim_param
,
333 obj
->ls
->dim
, isl_dim_param
))
334 return isl_basic_set_opt_lp_val_aligned(bset
, max
, obj
);
336 bset
= isl_basic_set_copy(bset
);
337 obj
= isl_aff_copy(obj
);
338 bset
= isl_basic_set_align_params(bset
, isl_aff_get_domain_space(obj
));
339 obj
= isl_aff_align_params(obj
, isl_basic_set_get_space(bset
));
341 res
= isl_basic_set_opt_lp_val_aligned(bset
, max
, obj
);
343 isl_basic_set_free(bset
);
349 /* Return the minimal (rational) value of "obj" over "bset".
351 * Return negative infinity if the minimal value is unbounded and
352 * NaN if "bset" is empty.
354 __isl_give isl_val
*isl_basic_set_min_lp_val(__isl_keep isl_basic_set
*bset
,
355 __isl_keep isl_aff
*obj
)
357 return isl_basic_set_opt_lp_val(bset
, 0, obj
);
360 /* Return the maximal (rational) value of "obj" over "bset".
362 * Return infinity if the maximal value is unbounded and
363 * NaN if "bset" is empty.
365 __isl_give isl_val
*isl_basic_set_max_lp_val(__isl_keep isl_basic_set
*bset
,
366 __isl_keep isl_aff
*obj
)
368 return isl_basic_set_opt_lp_val(bset
, 1, obj
);