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
13 #include <isl_map_private.h>
17 #include "isl_sample.h"
20 #include <isl_ilp_private.h>
21 #include <isl/printer.h>
22 #include <isl_point_private.h>
23 #include <isl_vec_private.h>
24 #include <isl/options.h>
26 /* The input of this program is the same as that of the "example" program
27 * from the PipLib distribution, except that the "big parameter column"
28 * should always be -1.
30 * Context constraints in PolyLib format
32 * Problem constraints in PolyLib format
33 * Optional list of options
36 * Maximize compute maximum instead of minimum
37 * Rational compute rational optimum instead of integer optimum
38 * Urs_parms don't assume parameters are non-negative
39 * Urs_unknowns don't assume unknowns are non-negative
43 struct isl_options
*isl
;
51 struct isl_arg_choice pip_format
[] = {
53 {"affine", FORMAT_AFF
},
57 ISL_ARGS_START(struct options
, options_args
)
58 ISL_ARG_CHILD(struct options
, isl
, "isl", &isl_options_args
, "isl options")
59 ISL_ARG_BOOL(struct options
, verify
, 'T', "verify", 0, NULL
)
60 ISL_ARG_CHOICE(struct options
, format
, 0, "format",
61 pip_format
, FORMAT_SET
, "output format")
64 ISL_ARG_DEF(options
, struct options
, options_args
)
66 static __isl_give isl_basic_set
*set_bounds(__isl_take isl_basic_set
*bset
)
73 nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
74 r
= nparam
>= 8 ? 4 : nparam
>= 5 ? 6 : 30;
76 pt
= isl_basic_set_sample_point(isl_basic_set_copy(bset
));
77 pt2
= isl_point_copy(pt
);
79 for (i
= 0; i
< nparam
; ++i
) {
80 pt
= isl_point_add_ui(pt
, isl_dim_param
, i
, r
);
81 pt2
= isl_point_sub_ui(pt2
, isl_dim_param
, i
, r
);
84 box
= isl_basic_set_box_from_points(pt
, pt2
);
86 return isl_basic_set_intersect(bset
, box
);
89 static struct isl_basic_set
*to_parameter_domain(struct isl_basic_set
*context
)
91 context
= isl_basic_set_move_dims(context
, isl_dim_param
, 0,
92 isl_dim_set
, 0, isl_basic_set_dim(context
, isl_dim_set
));
93 context
= isl_basic_set_params(context
);
97 isl_basic_set
*plug_in_parameters(isl_basic_set
*bset
, struct isl_vec
*params
)
101 for (i
= 0; i
< params
->size
- 1; ++i
)
102 bset
= isl_basic_set_fix(bset
,
103 isl_dim_param
, i
, params
->el
[1 + i
]);
105 bset
= isl_basic_set_remove_dims(bset
,
106 isl_dim_param
, 0, params
->size
- 1);
108 isl_vec_free(params
);
113 isl_set
*set_plug_in_parameters(isl_set
*set
, struct isl_vec
*params
)
117 for (i
= 0; i
< params
->size
- 1; ++i
)
118 set
= isl_set_fix(set
, isl_dim_param
, i
, params
->el
[1 + i
]);
120 set
= isl_set_remove_dims(set
, isl_dim_param
, 0, params
->size
- 1);
122 isl_vec_free(params
);
127 /* Compute the lexicographically minimal (or maximal if max is set)
128 * element of bset for the given values of the parameters, by
129 * successively solving an ilp problem in each direction.
131 struct isl_vec
*opt_at(struct isl_basic_set
*bset
,
132 struct isl_vec
*params
, int max
)
139 dim
= isl_basic_set_dim(bset
, isl_dim_set
);
141 bset
= plug_in_parameters(bset
, params
);
143 if (isl_basic_set_plain_is_empty(bset
)) {
144 opt
= isl_vec_alloc(bset
->ctx
, 0);
145 isl_basic_set_free(bset
);
149 opt
= isl_vec_alloc(bset
->ctx
, 1 + dim
);
152 obj
= isl_vec_alloc(bset
->ctx
, 1 + dim
);
155 isl_int_set_si(opt
->el
[0], 1);
156 isl_int_set_si(obj
->el
[0], 0);
158 for (i
= 0; i
< dim
; ++i
) {
159 enum isl_lp_result res
;
161 isl_seq_clr(obj
->el
+ 1, dim
);
162 isl_int_set_si(obj
->el
[1 + i
], 1);
163 res
= isl_basic_set_solve_ilp(bset
, max
, obj
->el
,
164 &opt
->el
[1 + i
], NULL
);
165 if (res
== isl_lp_empty
)
167 assert(res
== isl_lp_ok
);
168 bset
= isl_basic_set_fix(bset
, isl_dim_set
, i
, opt
->el
[1 + i
]);
171 isl_basic_set_free(bset
);
177 opt
= isl_vec_alloc(bset
->ctx
, 0);
178 isl_basic_set_free(bset
);
184 struct isl_scan_pip
{
185 struct isl_scan_callback callback
;
194 /* Check if the "manually" computed optimum of bset at the "sample"
195 * values of the parameters agrees with the solution of pilp problem
196 * represented by the pair (sol, empty).
197 * In particular, if there is no solution for this value of the parameters,
198 * then it should be an element of the parameter domain "empty".
199 * Otherwise, the optimal solution, should be equal to the result of
200 * plugging in the value of the parameters in "sol".
202 static int scan_one(struct isl_scan_callback
*callback
,
203 __isl_take isl_vec
*sample
)
205 struct isl_scan_pip
*sp
= (struct isl_scan_pip
*)callback
;
210 opt
= opt_at(isl_basic_set_copy(sp
->bset
), isl_vec_copy(sample
), sp
->max
);
213 if (opt
->size
== 0) {
214 isl_point
*sample_pnt
;
215 sample_pnt
= isl_point_alloc(isl_set_get_space(sp
->empty
), sample
);
216 assert(isl_set_contains_point(sp
->empty
, sample_pnt
));
217 isl_point_free(sample_pnt
);
222 opt_set
= isl_set_from_basic_set(isl_basic_set_from_vec(opt
));
223 sol
= set_plug_in_parameters(isl_set_copy(sp
->sol
), sample
);
224 assert(isl_set_is_equal(opt_set
, sol
));
226 isl_set_free(opt_set
);
229 if (!(sp
->n
% sp
->stride
)) {
234 return sp
->n
>= 1 ? 0 : -1;
237 static void check_solution(isl_basic_set
*bset
, isl_basic_set
*context
,
238 isl_set
*sol
, isl_set
*empty
, int max
)
240 struct isl_scan_pip sp
;
241 isl_int count
, count_max
;
245 context
= set_bounds(context
);
246 context
= isl_basic_set_underlying_set(context
);
249 isl_int_init(count_max
);
251 isl_int_set_si(count_max
, 2000);
252 r
= isl_basic_set_count_upto(context
, count_max
, &count
);
254 n
= isl_int_get_si(count
);
256 isl_int_clear(count_max
);
257 isl_int_clear(count
);
259 sp
.callback
.add
= scan_one
;
264 sp
.stride
= n
> 70 ? 1 + (n
+ 1)/70 : 1;
267 for (i
= 0; i
< n
; i
+= sp
.stride
)
272 isl_basic_set_scan(context
, &sp
.callback
);
276 isl_basic_set_free(bset
);
279 int main(int argc
, char **argv
)
282 struct isl_basic_set
*context
, *bset
, *copy
, *context_copy
;
283 struct isl_set
*set
= NULL
;
284 struct isl_set
*empty
;
285 isl_pw_multi_aff
*pma
= NULL
;
289 int urs_unknowns
= 0;
294 struct options
*options
;
296 options
= options_new_with_defaults();
298 argc
= options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
300 ctx
= isl_ctx_alloc_with_options(&options_args
, options
);
302 context
= isl_basic_set_read_from_file(ctx
, stdin
);
304 n
= fscanf(stdin
, "%d", &neg_one
);
306 assert(neg_one
== -1);
307 bset
= isl_basic_set_read_from_file(ctx
, stdin
);
309 while (fgets(s
, sizeof(s
), stdin
)) {
310 if (strncasecmp(s
, "Maximize", 8) == 0)
312 if (strncasecmp(s
, "Rational", 8) == 0) {
314 bset
= isl_basic_set_set_rational(bset
);
316 if (strncasecmp(s
, "Urs_parms", 9) == 0)
318 if (strncasecmp(s
, "Urs_unknowns", 12) == 0)
322 context
= isl_basic_set_intersect(context
,
323 isl_basic_set_positive_orthant(isl_basic_set_get_space(context
)));
324 context
= to_parameter_domain(context
);
325 nparam
= isl_basic_set_dim(context
, isl_dim_param
);
326 if (nparam
!= isl_basic_set_dim(bset
, isl_dim_param
)) {
327 int dim
= isl_basic_set_dim(bset
, isl_dim_set
);
328 bset
= isl_basic_set_move_dims(bset
, isl_dim_param
, 0,
329 isl_dim_set
, dim
- nparam
, nparam
);
332 bset
= isl_basic_set_intersect(bset
,
333 isl_basic_set_positive_orthant(isl_basic_set_get_space(bset
)));
335 if (options
->verify
) {
336 copy
= isl_basic_set_copy(bset
);
337 context_copy
= isl_basic_set_copy(context
);
340 if (options
->format
== FORMAT_AFF
) {
342 pma
= isl_basic_set_partial_lexmax_pw_multi_aff(bset
,
345 pma
= isl_basic_set_partial_lexmin_pw_multi_aff(bset
,
349 set
= isl_basic_set_partial_lexmax(bset
,
352 set
= isl_basic_set_partial_lexmin(bset
,
356 if (options
->verify
) {
358 if (options
->format
== FORMAT_AFF
)
359 set
= isl_set_from_pw_multi_aff(pma
);
360 check_solution(copy
, context_copy
, set
, empty
, max
);
364 p
= isl_printer_to_file(ctx
, stdout
);
365 if (options
->format
== FORMAT_AFF
)
366 p
= isl_printer_print_pw_multi_aff(p
, pma
);
368 p
= isl_printer_print_set(p
, set
);
369 p
= isl_printer_end_line(p
);
370 p
= isl_printer_print_str(p
, "no solution: ");
371 p
= isl_printer_print_set(p
, empty
);
372 p
= isl_printer_end_line(p
);
375 isl_pw_multi_aff_free(pma
);