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
12 #include <isl_map_private.h>
15 #include "isl_sample.h"
18 #include <isl_ilp_private.h>
19 #include <isl/printer.h>
20 #include <isl_point_private.h>
21 #include <isl_vec_private.h>
22 #include <isl/options.h>
23 #include <isl_config.h>
25 /* The input of this program is the same as that of the "example" program
26 * from the PipLib distribution, except that the "big parameter column"
27 * should always be -1.
29 * Context constraints in PolyLib format
31 * Problem constraints in PolyLib format
32 * Optional list of options
35 * Maximize compute maximum instead of minimum
36 * Rational compute rational optimum instead of integer optimum
37 * Urs_parms don't assume parameters are non-negative
38 * Urs_unknowns don't assume unknowns are non-negative
42 struct isl_options
*isl
;
50 struct isl_arg_choice pip_format
[] = {
52 {"affine", FORMAT_AFF
},
56 ISL_ARGS_START(struct options
, options_args
)
57 ISL_ARG_CHILD(struct options
, isl
, "isl", &isl_options_args
, "isl options")
58 ISL_ARG_BOOL(struct options
, verify
, 'T', "verify", 0, NULL
)
59 ISL_ARG_CHOICE(struct options
, format
, 0, "format",
60 pip_format
, FORMAT_SET
, "output format")
63 ISL_ARG_DEF(options
, struct options
, options_args
)
65 static __isl_give isl_basic_set
*set_bounds(__isl_take isl_basic_set
*bset
)
72 nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
74 return isl_basic_set_free(bset
);
75 r
= nparam
>= 8 ? 4 : nparam
>= 5 ? 6 : 30;
77 pt
= isl_basic_set_sample_point(isl_basic_set_copy(bset
));
78 pt2
= isl_point_copy(pt
);
80 for (i
= 0; i
< nparam
; ++i
) {
81 pt
= isl_point_add_ui(pt
, isl_dim_param
, i
, r
);
82 pt2
= isl_point_sub_ui(pt2
, isl_dim_param
, i
, r
);
85 box
= isl_basic_set_box_from_points(pt
, pt2
);
87 return isl_basic_set_intersect(bset
, box
);
90 static __isl_give isl_basic_set
*to_parameter_domain(
91 __isl_take isl_basic_set
*context
)
95 dim
= isl_basic_set_dim(context
, isl_dim_set
);
97 return isl_basic_set_free(context
);
98 context
= isl_basic_set_move_dims(context
, isl_dim_param
, 0,
100 context
= isl_basic_set_params(context
);
104 /* If "context" has more parameters than "bset", then reinterpret
105 * the last dimensions of "bset" as parameters.
107 static __isl_give isl_basic_set
*move_parameters(__isl_take isl_basic_set
*bset
,
108 __isl_keep isl_basic_set
*context
)
110 isl_size nparam
, nparam_bset
, dim
;
112 nparam
= isl_basic_set_dim(context
, isl_dim_param
);
113 nparam_bset
= isl_basic_set_dim(bset
, isl_dim_param
);
114 if (nparam
< 0 || nparam_bset
< 0)
115 return isl_basic_set_free(bset
);
116 if (nparam
== nparam_bset
)
118 dim
= isl_basic_set_dim(bset
, isl_dim_set
);
120 return isl_basic_set_free(bset
);
121 bset
= isl_basic_set_move_dims(bset
, isl_dim_param
, 0,
122 isl_dim_set
, dim
- nparam
, nparam
);
126 /* Plug in the initial values of "params" for the parameters in "bset" and
127 * return the result. The remaining entries in "params", if any,
128 * correspond to the existentially quantified variables in the description
129 * of the original context and can be ignored.
131 static __isl_give isl_basic_set
*plug_in_parameters(
132 __isl_take isl_basic_set
*bset
, __isl_take isl_vec
*params
)
137 n
= isl_basic_set_dim(bset
, isl_dim_param
);
139 bset
= isl_basic_set_free(bset
);
140 for (i
= 0; i
< n
; ++i
)
141 bset
= isl_basic_set_fix(bset
,
142 isl_dim_param
, i
, params
->el
[1 + i
]);
144 bset
= isl_basic_set_remove_dims(bset
, isl_dim_param
, 0, n
);
146 isl_vec_free(params
);
151 /* Plug in the initial values of "params" for the parameters in "set" and
152 * return the result. The remaining entries in "params", if any,
153 * correspond to the existentially quantified variables in the description
154 * of the original context and can be ignored.
156 static __isl_give isl_set
*set_plug_in_parameters(__isl_take isl_set
*set
,
157 __isl_take isl_vec
*params
)
162 n
= isl_set_dim(set
, isl_dim_param
);
164 set
= isl_set_free(set
);
165 for (i
= 0; i
< n
; ++i
)
166 set
= isl_set_fix(set
, isl_dim_param
, i
, params
->el
[1 + i
]);
168 set
= isl_set_remove_dims(set
, isl_dim_param
, 0, n
);
170 isl_vec_free(params
);
175 /* Compute the lexicographically minimal (or maximal if max is set)
176 * element of bset for the given values of the parameters, by
177 * successively solving an ilp problem in each direction.
179 static __isl_give isl_vec
*opt_at(__isl_take isl_basic_set
*bset
,
180 __isl_take isl_vec
*params
, int max
)
188 dim
= isl_basic_set_dim(bset
, isl_dim_set
);
192 bset
= plug_in_parameters(bset
, params
);
194 ctx
= isl_basic_set_get_ctx(bset
);
195 if (isl_basic_set_plain_is_empty(bset
)) {
196 opt
= isl_vec_alloc(ctx
, 0);
197 isl_basic_set_free(bset
);
201 opt
= isl_vec_alloc(ctx
, 1 + dim
);
204 obj
= isl_vec_alloc(ctx
, 1 + dim
);
207 isl_int_set_si(opt
->el
[0], 1);
208 isl_int_set_si(obj
->el
[0], 0);
210 for (i
= 0; i
< dim
; ++i
) {
211 enum isl_lp_result res
;
213 isl_seq_clr(obj
->el
+ 1, dim
);
214 isl_int_set_si(obj
->el
[1 + i
], 1);
215 res
= isl_basic_set_solve_ilp(bset
, max
, obj
->el
,
216 &opt
->el
[1 + i
], NULL
);
217 if (res
== isl_lp_empty
)
219 assert(res
== isl_lp_ok
);
220 bset
= isl_basic_set_fix(bset
, isl_dim_set
, i
, opt
->el
[1 + i
]);
223 isl_basic_set_free(bset
);
228 isl_basic_set_free(bset
);
229 isl_vec_free(params
);
233 opt
= isl_vec_alloc(ctx
, 0);
234 isl_basic_set_free(bset
);
240 struct isl_scan_pip
{
241 struct isl_scan_callback callback
;
250 /* Check if the "manually" computed optimum of bset at the "sample"
251 * values of the parameters agrees with the solution of pilp problem
252 * represented by the pair (sol, empty).
253 * In particular, if there is no solution for this value of the parameters,
254 * then it should be an element of the parameter domain "empty".
255 * Otherwise, the optimal solution, should be equal to the result of
256 * plugging in the value of the parameters in "sol".
258 static isl_stat
scan_one(struct isl_scan_callback
*callback
,
259 __isl_take isl_vec
*sample
)
261 struct isl_scan_pip
*sp
= (struct isl_scan_pip
*)callback
;
266 opt
= opt_at(isl_basic_set_copy(sp
->bset
), isl_vec_copy(sample
), sp
->max
);
269 if (opt
->size
== 0) {
270 isl_point
*sample_pnt
;
271 sample_pnt
= isl_point_alloc(isl_set_get_space(sp
->empty
), sample
);
272 assert(isl_set_contains_point(sp
->empty
, sample_pnt
));
273 isl_point_free(sample_pnt
);
278 opt_set
= isl_set_from_basic_set(isl_basic_set_from_vec(opt
));
279 sol
= set_plug_in_parameters(isl_set_copy(sp
->sol
), sample
);
280 assert(isl_set_is_equal(opt_set
, sol
));
282 isl_set_free(opt_set
);
285 if (!(sp
->n
% sp
->stride
)) {
290 return sp
->n
>= 1 ? isl_stat_ok
: isl_stat_error
;
293 static void check_solution(isl_basic_set
*bset
, isl_basic_set
*context
,
294 isl_set
*sol
, isl_set
*empty
, int max
)
296 struct isl_scan_pip sp
;
297 isl_int count
, count_max
;
301 context
= set_bounds(context
);
302 context
= isl_basic_set_underlying_set(context
);
305 isl_int_init(count_max
);
307 isl_int_set_si(count_max
, 2000);
308 r
= isl_basic_set_count_upto(context
, count_max
, &count
);
310 n
= isl_int_get_si(count
);
312 isl_int_clear(count_max
);
313 isl_int_clear(count
);
315 sp
.callback
.add
= scan_one
;
320 sp
.stride
= n
> 70 ? 1 + (n
+ 1)/70 : 1;
323 for (i
= 0; i
< n
; i
+= sp
.stride
)
328 isl_basic_set_scan(context
, &sp
.callback
);
332 isl_basic_set_free(bset
);
335 int main(int argc
, char **argv
)
338 struct isl_basic_set
*context
, *bset
, *copy
, *context_copy
;
339 struct isl_set
*set
= NULL
;
340 struct isl_set
*empty
;
341 isl_pw_multi_aff
*pma
= NULL
;
345 int urs_unknowns
= 0;
349 struct options
*options
;
351 options
= options_new_with_defaults();
353 argc
= options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
355 ctx
= isl_ctx_alloc_with_options(&options_args
, options
);
357 context
= isl_basic_set_read_from_file(ctx
, stdin
);
359 n
= fscanf(stdin
, "%d", &neg_one
);
361 assert(neg_one
== -1);
362 bset
= isl_basic_set_read_from_file(ctx
, stdin
);
364 while (fgets(s
, sizeof(s
), stdin
)) {
365 if (strncasecmp(s
, "Maximize", 8) == 0)
367 if (strncasecmp(s
, "Rational", 8) == 0) {
369 bset
= isl_basic_set_set_rational(bset
);
371 if (strncasecmp(s
, "Urs_parms", 9) == 0)
373 if (strncasecmp(s
, "Urs_unknowns", 12) == 0)
377 context
= isl_basic_set_intersect(context
,
378 isl_basic_set_positive_orthant(isl_basic_set_get_space(context
)));
379 context
= to_parameter_domain(context
);
380 bset
= move_parameters(bset
, context
);
382 bset
= isl_basic_set_intersect(bset
,
383 isl_basic_set_positive_orthant(isl_basic_set_get_space(bset
)));
385 if (options
->verify
) {
386 copy
= isl_basic_set_copy(bset
);
387 context_copy
= isl_basic_set_copy(context
);
390 if (options
->format
== FORMAT_AFF
) {
392 pma
= isl_basic_set_partial_lexmax_pw_multi_aff(bset
,
395 pma
= isl_basic_set_partial_lexmin_pw_multi_aff(bset
,
399 set
= isl_basic_set_partial_lexmax(bset
,
402 set
= isl_basic_set_partial_lexmin(bset
,
406 if (options
->verify
) {
408 if (options
->format
== FORMAT_AFF
)
409 set
= isl_set_from_pw_multi_aff(pma
);
410 check_solution(copy
, context_copy
, set
, empty
, max
);
414 p
= isl_printer_to_file(ctx
, stdout
);
415 if (options
->format
== FORMAT_AFF
)
416 p
= isl_printer_print_pw_multi_aff(p
, pma
);
418 p
= isl_printer_print_set(p
, set
);
419 p
= isl_printer_end_line(p
);
420 p
= isl_printer_print_str(p
, "no solution: ");
421 p
= isl_printer_print_set(p
, empty
);
422 p
= isl_printer_end_line(p
);
425 isl_pw_multi_aff_free(pma
);