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
14 #include "isl_map_private.h"
15 #include "isl_sample.h"
19 #include <isl_point_private.h>
21 /* The input of this program is the same as that of the "example" program
22 * from the PipLib distribution, except that the "big parameter column"
23 * should always be -1.
25 * Context constraints in PolyLib format
27 * Problem constraints in PolyLib format
28 * Optional list of options
31 * Maximize compute maximum instead of minimum
32 * Rational compute rational optimum instead of integer optimum
33 * Urs_parms don't assume parameters are non-negative
34 * Urs_unknowns don't assume unknowns are non-negative
38 struct isl_options
*isl
;
42 struct isl_arg options_arg
[] = {
43 ISL_ARG_CHILD(struct options
, isl
, "isl", isl_options_arg
, "isl options")
44 ISL_ARG_BOOL(struct options
, verify
, 'T', "verify", 0, NULL
)
48 ISL_ARG_DEF(options
, struct options
, options_arg
)
50 static __isl_give isl_basic_set
*set_bounds(__isl_take isl_basic_set
*bset
)
57 nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
58 r
= nparam
>= 8 ? 4 : nparam
>= 5 ? 6 : 30;
60 pt
= isl_basic_set_sample_point(isl_basic_set_copy(bset
));
61 pt2
= isl_point_copy(pt
);
63 for (i
= 0; i
< nparam
; ++i
) {
64 pt
= isl_point_add_ui(pt
, isl_dim_param
, i
, r
);
65 pt2
= isl_point_sub_ui(pt2
, isl_dim_param
, i
, r
);
68 box
= isl_basic_set_box_from_points(pt
, pt2
);
70 return isl_basic_set_intersect(bset
, box
);
73 static struct isl_basic_set
*to_parameter_domain(struct isl_basic_set
*context
)
75 return isl_basic_set_move_dims(context
, isl_dim_param
, 0, isl_dim_set
, 0,
76 isl_basic_set_dim(context
, isl_dim_set
));
79 isl_basic_set
*plug_in_parameters(isl_basic_set
*bset
, struct isl_vec
*params
)
83 for (i
= 0; i
< params
->size
- 1; ++i
)
84 bset
= isl_basic_set_fix(bset
,
85 isl_dim_param
, i
, params
->el
[1 + i
]);
87 bset
= isl_basic_set_remove_dims(bset
,
88 isl_dim_param
, 0, params
->size
- 1);
95 isl_set
*set_plug_in_parameters(isl_set
*set
, struct isl_vec
*params
)
99 for (i
= 0; i
< params
->size
- 1; ++i
)
100 set
= isl_set_fix(set
, isl_dim_param
, i
, params
->el
[1 + i
]);
102 set
= isl_set_remove_dims(set
, isl_dim_param
, 0, params
->size
- 1);
104 isl_vec_free(params
);
109 /* Compute the lexicographically minimal (or maximal if max is set)
110 * element of bset for the given values of the parameters, by
111 * successively solving an ilp problem in each direction.
113 struct isl_vec
*opt_at(struct isl_basic_set
*bset
,
114 struct isl_vec
*params
, int max
)
121 dim
= isl_basic_set_dim(bset
, isl_dim_set
);
123 bset
= plug_in_parameters(bset
, params
);
125 if (isl_basic_set_fast_is_empty(bset
)) {
126 opt
= isl_vec_alloc(bset
->ctx
, 0);
127 isl_basic_set_free(bset
);
131 opt
= isl_vec_alloc(bset
->ctx
, 1 + dim
);
134 obj
= isl_vec_alloc(bset
->ctx
, 1 + dim
);
137 isl_int_set_si(opt
->el
[0], 1);
138 isl_int_set_si(obj
->el
[0], 0);
140 for (i
= 0; i
< dim
; ++i
) {
141 enum isl_lp_result res
;
143 isl_seq_clr(obj
->el
+ 1, dim
);
144 isl_int_set_si(obj
->el
[1 + i
], 1);
145 res
= isl_basic_set_solve_ilp(bset
, max
, obj
->el
,
146 &opt
->el
[1 + i
], NULL
);
147 if (res
== isl_lp_empty
)
149 assert(res
== isl_lp_ok
);
150 bset
= isl_basic_set_fix(bset
, isl_dim_set
, i
, opt
->el
[1 + i
]);
153 isl_basic_set_free(bset
);
159 opt
= isl_vec_alloc(bset
->ctx
, 0);
160 isl_basic_set_free(bset
);
166 struct isl_scan_pip
{
167 struct isl_scan_callback callback
;
176 /* Check if the "manually" computed optimum of bset at the "sample"
177 * values of the parameters agrees with the solution of pilp problem
178 * represented by the pair (sol, empty).
179 * In particular, if there is no solution for this value of the parameters,
180 * then it should be an element of the parameter domain "empty".
181 * Otherwise, the optimal solution, should be equal to the result of
182 * plugging in the value of the parameters in "sol".
184 static int scan_one(struct isl_scan_callback
*callback
,
185 __isl_take isl_vec
*sample
)
187 struct isl_scan_pip
*sp
= (struct isl_scan_pip
*)callback
;
190 opt
= opt_at(isl_basic_set_copy(sp
->bset
), isl_vec_copy(sample
), sp
->max
);
193 if (opt
->size
== 0) {
194 isl_point
*sample_pnt
;
195 sample_pnt
= isl_point_alloc(isl_set_get_dim(sp
->empty
), sample
);
196 assert(isl_set_contains_point(sp
->empty
, sample_pnt
));
197 isl_point_free(sample_pnt
);
202 opt_set
= isl_set_from_basic_set(isl_basic_set_from_vec(opt
));
203 sol
= set_plug_in_parameters(isl_set_copy(sp
->sol
), sample
);
204 assert(isl_set_is_equal(opt_set
, sol
));
206 isl_set_free(opt_set
);
209 if (!(sp
->n
++ % sp
->stride
)) {
217 struct isl_scan_count
{
218 struct isl_scan_callback callback
;
222 static int count_one(struct isl_scan_callback
*callback
,
223 __isl_take isl_vec
*sample
)
225 struct isl_scan_count
*sc
= (struct isl_scan_count
*)callback
;
226 isl_vec_free(sample
);
233 static void check_solution(isl_basic_set
*bset
, isl_basic_set
*context
,
234 isl_set
*sol
, isl_set
*empty
, int max
)
236 struct isl_scan_count sc
;
237 struct isl_scan_pip sp
;
241 context
= set_bounds(context
);
242 context
= isl_basic_set_underlying_set(context
);
244 sc
.callback
.add
= count_one
;
247 r
= isl_basic_set_scan(isl_basic_set_copy(context
), &sc
.callback
);
250 sp
.callback
.add
= scan_one
;
255 sp
.stride
= sc
.n
> 70 ? 1 + (sc
.n
+ 1)/70 : 1;
258 for (i
= 0; i
< sc
.n
; i
+= sp
.stride
)
263 r
= isl_basic_set_scan(context
, &sp
.callback
);
268 isl_basic_set_free(bset
);
271 int main(int argc
, char **argv
)
274 struct isl_basic_set
*context
, *bset
, *copy
, *context_copy
;
276 struct isl_set
*empty
;
280 int urs_unknowns
= 0;
284 struct options
*options
;
286 options
= options_new_with_defaults();
288 argc
= options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
290 ctx
= isl_ctx_alloc_with_options(options_arg
, options
);
292 context
= isl_basic_set_read_from_file(ctx
, stdin
, 0);
294 n
= fscanf(stdin
, "%d", &neg_one
);
296 assert(neg_one
== -1);
297 bset
= isl_basic_set_read_from_file(ctx
, stdin
,
298 isl_basic_set_dim(context
, isl_dim_set
));
300 while (fgets(s
, sizeof(s
), stdin
)) {
301 if (strncasecmp(s
, "Maximize", 8) == 0)
303 if (strncasecmp(s
, "Rational", 8) == 0) {
305 bset
= isl_basic_set_set_rational(bset
);
307 if (strncasecmp(s
, "Urs_parms", 9) == 0)
309 if (strncasecmp(s
, "Urs_unknowns", 12) == 0)
313 context
= isl_basic_set_intersect(context
,
314 isl_basic_set_positive_orthant(isl_basic_set_get_dim(context
)));
315 context
= to_parameter_domain(context
);
317 bset
= isl_basic_set_intersect(bset
,
318 isl_basic_set_positive_orthant(isl_basic_set_get_dim(bset
)));
320 if (options
->verify
) {
321 copy
= isl_basic_set_copy(bset
);
322 context_copy
= isl_basic_set_copy(context
);
326 set
= isl_basic_set_partial_lexmax(bset
, context
, &empty
);
328 set
= isl_basic_set_partial_lexmin(bset
, context
, &empty
);
330 if (options
->verify
) {
332 check_solution(copy
, context_copy
, set
, empty
, max
);
334 isl_set_print(set
, stdout
, 0, ISL_FORMAT_ISL
);
335 fprintf(stdout
, "\n");
336 fprintf(stdout
, "no solution: ");
337 isl_set_print(empty
, stdout
, 0, ISL_FORMAT_ISL
);
338 fprintf(stdout
, "\n");