2 * Copyright 2008-2009 Katholieke Universiteit Leuven
4 * Use of this software is governed by the GNU LGPLv2.1 license
6 * Written by Sven Verdoolaege, K.U.Leuven, Departement
7 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
13 #include <isl_map_private.h>
16 #include "isl_sample.h"
20 #include <isl_point_private.h>
22 /* The input of this program is the same as that of the "example" program
23 * from the PipLib distribution, except that the "big parameter column"
24 * should always be -1.
26 * Context constraints in PolyLib format
28 * Problem constraints in PolyLib format
29 * Optional list of options
32 * Maximize compute maximum instead of minimum
33 * Rational compute rational optimum instead of integer optimum
34 * Urs_parms don't assume parameters are non-negative
35 * Urs_unknowns don't assume unknowns are non-negative
39 struct isl_options
*isl
;
43 struct isl_arg options_arg
[] = {
44 ISL_ARG_CHILD(struct options
, isl
, "isl", isl_options_arg
, "isl options")
45 ISL_ARG_BOOL(struct options
, verify
, 'T', "verify", 0, NULL
)
49 ISL_ARG_DEF(options
, struct options
, options_arg
)
51 static __isl_give isl_basic_set
*set_bounds(__isl_take isl_basic_set
*bset
)
58 nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
59 r
= nparam
>= 8 ? 4 : nparam
>= 5 ? 6 : 30;
61 pt
= isl_basic_set_sample_point(isl_basic_set_copy(bset
));
62 pt2
= isl_point_copy(pt
);
64 for (i
= 0; i
< nparam
; ++i
) {
65 pt
= isl_point_add_ui(pt
, isl_dim_param
, i
, r
);
66 pt2
= isl_point_sub_ui(pt2
, isl_dim_param
, i
, r
);
69 box
= isl_basic_set_box_from_points(pt
, pt2
);
71 return isl_basic_set_intersect(bset
, box
);
74 static struct isl_basic_set
*to_parameter_domain(struct isl_basic_set
*context
)
76 context
= isl_basic_set_move_dims(context
, isl_dim_param
, 0,
77 isl_dim_set
, 0, isl_basic_set_dim(context
, isl_dim_set
));
78 context
= isl_basic_set_params(context
);
82 isl_basic_set
*plug_in_parameters(isl_basic_set
*bset
, struct isl_vec
*params
)
86 for (i
= 0; i
< params
->size
- 1; ++i
)
87 bset
= isl_basic_set_fix(bset
,
88 isl_dim_param
, i
, params
->el
[1 + i
]);
90 bset
= isl_basic_set_remove_dims(bset
,
91 isl_dim_param
, 0, params
->size
- 1);
98 isl_set
*set_plug_in_parameters(isl_set
*set
, struct isl_vec
*params
)
102 for (i
= 0; i
< params
->size
- 1; ++i
)
103 set
= isl_set_fix(set
, isl_dim_param
, i
, params
->el
[1 + i
]);
105 set
= isl_set_remove_dims(set
, isl_dim_param
, 0, params
->size
- 1);
107 isl_vec_free(params
);
112 /* Compute the lexicographically minimal (or maximal if max is set)
113 * element of bset for the given values of the parameters, by
114 * successively solving an ilp problem in each direction.
116 struct isl_vec
*opt_at(struct isl_basic_set
*bset
,
117 struct isl_vec
*params
, int max
)
124 dim
= isl_basic_set_dim(bset
, isl_dim_set
);
126 bset
= plug_in_parameters(bset
, params
);
128 if (isl_basic_set_plain_is_empty(bset
)) {
129 opt
= isl_vec_alloc(bset
->ctx
, 0);
130 isl_basic_set_free(bset
);
134 opt
= isl_vec_alloc(bset
->ctx
, 1 + dim
);
137 obj
= isl_vec_alloc(bset
->ctx
, 1 + dim
);
140 isl_int_set_si(opt
->el
[0], 1);
141 isl_int_set_si(obj
->el
[0], 0);
143 for (i
= 0; i
< dim
; ++i
) {
144 enum isl_lp_result res
;
146 isl_seq_clr(obj
->el
+ 1, dim
);
147 isl_int_set_si(obj
->el
[1 + i
], 1);
148 res
= isl_basic_set_solve_ilp(bset
, max
, obj
->el
,
149 &opt
->el
[1 + i
], NULL
);
150 if (res
== isl_lp_empty
)
152 assert(res
== isl_lp_ok
);
153 bset
= isl_basic_set_fix(bset
, isl_dim_set
, i
, opt
->el
[1 + i
]);
156 isl_basic_set_free(bset
);
162 opt
= isl_vec_alloc(bset
->ctx
, 0);
163 isl_basic_set_free(bset
);
169 struct isl_scan_pip
{
170 struct isl_scan_callback callback
;
179 /* Check if the "manually" computed optimum of bset at the "sample"
180 * values of the parameters agrees with the solution of pilp problem
181 * represented by the pair (sol, empty).
182 * In particular, if there is no solution for this value of the parameters,
183 * then it should be an element of the parameter domain "empty".
184 * Otherwise, the optimal solution, should be equal to the result of
185 * plugging in the value of the parameters in "sol".
187 static int scan_one(struct isl_scan_callback
*callback
,
188 __isl_take isl_vec
*sample
)
190 struct isl_scan_pip
*sp
= (struct isl_scan_pip
*)callback
;
195 opt
= opt_at(isl_basic_set_copy(sp
->bset
), isl_vec_copy(sample
), sp
->max
);
198 if (opt
->size
== 0) {
199 isl_point
*sample_pnt
;
200 sample_pnt
= isl_point_alloc(isl_set_get_space(sp
->empty
), sample
);
201 assert(isl_set_contains_point(sp
->empty
, sample_pnt
));
202 isl_point_free(sample_pnt
);
207 opt_set
= isl_set_from_basic_set(isl_basic_set_from_vec(opt
));
208 sol
= set_plug_in_parameters(isl_set_copy(sp
->sol
), sample
);
209 assert(isl_set_is_equal(opt_set
, sol
));
211 isl_set_free(opt_set
);
214 if (!(sp
->n
% sp
->stride
)) {
219 return sp
->n
>= 1 ? 0 : -1;
222 static void check_solution(isl_basic_set
*bset
, isl_basic_set
*context
,
223 isl_set
*sol
, isl_set
*empty
, int max
)
225 struct isl_scan_pip sp
;
226 isl_int count
, count_max
;
230 context
= set_bounds(context
);
231 context
= isl_basic_set_underlying_set(context
);
234 isl_int_init(count_max
);
236 isl_int_set_si(count_max
, 2000);
237 r
= isl_basic_set_count_upto(context
, count_max
, &count
);
239 n
= isl_int_get_si(count
);
241 isl_int_clear(count_max
);
242 isl_int_clear(count
);
244 sp
.callback
.add
= scan_one
;
249 sp
.stride
= n
> 70 ? 1 + (n
+ 1)/70 : 1;
252 for (i
= 0; i
< n
; i
+= sp
.stride
)
257 isl_basic_set_scan(context
, &sp
.callback
);
261 isl_basic_set_free(bset
);
264 int main(int argc
, char **argv
)
267 struct isl_basic_set
*context
, *bset
, *copy
, *context_copy
;
269 struct isl_set
*empty
;
273 int urs_unknowns
= 0;
278 struct options
*options
;
280 options
= options_new_with_defaults();
282 argc
= options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
284 ctx
= isl_ctx_alloc_with_options(options_arg
, options
);
286 context
= isl_basic_set_read_from_file(ctx
, stdin
);
288 n
= fscanf(stdin
, "%d", &neg_one
);
290 assert(neg_one
== -1);
291 bset
= isl_basic_set_read_from_file(ctx
, stdin
);
293 while (fgets(s
, sizeof(s
), stdin
)) {
294 if (strncasecmp(s
, "Maximize", 8) == 0)
296 if (strncasecmp(s
, "Rational", 8) == 0) {
298 bset
= isl_basic_set_set_rational(bset
);
300 if (strncasecmp(s
, "Urs_parms", 9) == 0)
302 if (strncasecmp(s
, "Urs_unknowns", 12) == 0)
306 context
= isl_basic_set_intersect(context
,
307 isl_basic_set_positive_orthant(isl_basic_set_get_space(context
)));
308 context
= to_parameter_domain(context
);
309 nparam
= isl_basic_set_dim(context
, isl_dim_param
);
310 if (nparam
!= isl_basic_set_dim(bset
, isl_dim_param
)) {
311 int dim
= isl_basic_set_dim(bset
, isl_dim_set
);
312 bset
= isl_basic_set_move_dims(bset
, isl_dim_param
, 0,
313 isl_dim_set
, dim
- nparam
, nparam
);
316 bset
= isl_basic_set_intersect(bset
,
317 isl_basic_set_positive_orthant(isl_basic_set_get_space(bset
)));
319 if (options
->verify
) {
320 copy
= isl_basic_set_copy(bset
);
321 context_copy
= isl_basic_set_copy(context
);
325 set
= isl_basic_set_partial_lexmax(bset
, context
, &empty
);
327 set
= isl_basic_set_partial_lexmin(bset
, context
, &empty
);
329 if (options
->verify
) {
331 check_solution(copy
, context_copy
, set
, empty
, max
);
333 isl_set_print(set
, stdout
, 0, ISL_FORMAT_ISL
);
334 fprintf(stdout
, "\n");
335 fprintf(stdout
, "no solution: ");
336 isl_set_print(empty
, stdout
, 0, ISL_FORMAT_ISL
);
337 fprintf(stdout
, "\n");