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
12 #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_plain_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
;
192 opt
= opt_at(isl_basic_set_copy(sp
->bset
), isl_vec_copy(sample
), sp
->max
);
195 if (opt
->size
== 0) {
196 isl_point
*sample_pnt
;
197 sample_pnt
= isl_point_alloc(isl_set_get_dim(sp
->empty
), sample
);
198 assert(isl_set_contains_point(sp
->empty
, sample_pnt
));
199 isl_point_free(sample_pnt
);
204 opt_set
= isl_set_from_basic_set(isl_basic_set_from_vec(opt
));
205 sol
= set_plug_in_parameters(isl_set_copy(sp
->sol
), sample
);
206 assert(isl_set_is_equal(opt_set
, sol
));
208 isl_set_free(opt_set
);
211 if (!(sp
->n
% sp
->stride
)) {
216 return sp
->n
>= 1 ? 0 : -1;
219 static void check_solution(isl_basic_set
*bset
, isl_basic_set
*context
,
220 isl_set
*sol
, isl_set
*empty
, int max
)
222 struct isl_scan_pip sp
;
223 isl_int count
, count_max
;
227 context
= set_bounds(context
);
228 context
= isl_basic_set_underlying_set(context
);
231 isl_int_init(count_max
);
233 isl_int_set_si(count_max
, 2000);
234 r
= isl_basic_set_count_upto(context
, count_max
, &count
);
236 n
= isl_int_get_si(count
);
238 isl_int_clear(count_max
);
239 isl_int_clear(count
);
241 sp
.callback
.add
= scan_one
;
246 sp
.stride
= n
> 70 ? 1 + (n
+ 1)/70 : 1;
249 for (i
= 0; i
< n
; i
+= sp
.stride
)
254 isl_basic_set_scan(context
, &sp
.callback
);
258 isl_basic_set_free(bset
);
261 int main(int argc
, char **argv
)
264 struct isl_basic_set
*context
, *bset
, *copy
, *context_copy
;
266 struct isl_set
*empty
;
270 int urs_unknowns
= 0;
274 struct options
*options
;
276 options
= options_new_with_defaults();
278 argc
= options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
280 ctx
= isl_ctx_alloc_with_options(options_arg
, options
);
282 context
= isl_basic_set_read_from_file(ctx
, stdin
, 0);
284 n
= fscanf(stdin
, "%d", &neg_one
);
286 assert(neg_one
== -1);
287 bset
= isl_basic_set_read_from_file(ctx
, stdin
,
288 isl_basic_set_dim(context
, isl_dim_set
));
290 while (fgets(s
, sizeof(s
), stdin
)) {
291 if (strncasecmp(s
, "Maximize", 8) == 0)
293 if (strncasecmp(s
, "Rational", 8) == 0) {
295 bset
= isl_basic_set_set_rational(bset
);
297 if (strncasecmp(s
, "Urs_parms", 9) == 0)
299 if (strncasecmp(s
, "Urs_unknowns", 12) == 0)
303 context
= isl_basic_set_intersect(context
,
304 isl_basic_set_positive_orthant(isl_basic_set_get_dim(context
)));
305 context
= to_parameter_domain(context
);
307 bset
= isl_basic_set_intersect(bset
,
308 isl_basic_set_positive_orthant(isl_basic_set_get_dim(bset
)));
310 if (options
->verify
) {
311 copy
= isl_basic_set_copy(bset
);
312 context_copy
= isl_basic_set_copy(context
);
316 set
= isl_basic_set_partial_lexmax(bset
, context
, &empty
);
318 set
= isl_basic_set_partial_lexmin(bset
, context
, &empty
);
320 if (options
->verify
) {
322 check_solution(copy
, context_copy
, set
, empty
, max
);
324 isl_set_print(set
, stdout
, 0, ISL_FORMAT_ISL
);
325 fprintf(stdout
, "\n");
326 fprintf(stdout
, "no solution: ");
327 isl_set_print(empty
, stdout
, 0, ISL_FORMAT_ISL
);
328 fprintf(stdout
, "\n");