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"
20 /* The input of this program is the same as that of the "example" program
21 * from the PipLib distribution, except that the "big parameter column"
22 * should always be -1.
24 * Context constraints in PolyLib format
26 * Problem constraints in PolyLib format
27 * Optional list of options
30 * Maximize compute maximum instead of minimum
31 * Rational compute rational optimum instead of integer optimum
32 * Urs_parms don't assume parameters are non-negative
33 * Urs_unknowns don't assume unknowns are non-negative
37 struct isl_options *isl;
41 struct isl_arg pip_options_arg[] = {
42 ISL_ARG_CHILD(struct pip_options, isl, "isl", isl_options_arg)
43 ISL_ARG_BOOL(struct pip_options, verify, 'T', "verify", 0)
46 ISL_ARG_DEF(pip_options, struct pip_options, pip_options_arg)
48 static struct isl_basic_set *to_parameter_domain(struct isl_basic_set *context)
50 struct isl_dim *param_dim;
51 struct isl_basic_set *model;
53 param_dim = isl_dim_set_alloc(context->ctx,
54 isl_basic_set_n_dim(context), 0);
55 model = isl_basic_set_empty(param_dim);
56 context = isl_basic_set_from_underlying_set(context, model);
61 static isl_basic_set *construct_cube(isl_basic_set *context)
67 struct isl_basic_set *cube;
68 struct isl_basic_set *interval;
69 struct isl_basic_set_list *list;
71 dim = isl_basic_set_total_dim(context);
74 dims = isl_dim_set_alloc(context->ctx, 0, 0);
75 return isl_basic_set_universe(dims);
88 isl_int_set_si(m, -range);
89 isl_int_set_si(M, range);
91 interval = isl_basic_set_interval(context->ctx, m, M);
92 list = isl_basic_set_list_alloc(context->ctx, dim);
93 for (i = 0; i < dim; ++i)
94 list = isl_basic_set_list_add(list, isl_basic_set_copy(interval));
95 isl_basic_set_free(interval);
96 cube = isl_basic_set_product(list);
104 isl_basic_set *plug_in_parameters(isl_basic_set *bset, struct isl_vec *params)
108 for (i = 0; i < params->size - 1; ++i)
109 bset = isl_basic_set_fix(bset,
110 isl_dim_param, i, params->el[1 + i]);
112 bset = isl_basic_set_remove(bset, isl_dim_param, 0, params->size - 1);
114 isl_vec_free(params);
119 isl_set *set_plug_in_parameters(isl_set *set, struct isl_vec *params)
123 for (i = 0; i < params->size - 1; ++i)
124 set = isl_set_fix(set, isl_dim_param, i, params->el[1 + i]);
126 set = isl_set_remove(set, isl_dim_param, 0, params->size - 1);
128 isl_vec_free(params);
133 /* Compute the lexicographically minimal (or maximal if max is set)
134 * element of bset for the given values of the parameters, by
135 * successively solving an ilp problem in each direction.
137 struct isl_vec *opt_at(struct isl_basic_set *bset,
138 struct isl_vec *params, int max)
145 dim = isl_basic_set_dim(bset, isl_dim_set);
147 bset = plug_in_parameters(bset, params);
149 if (isl_basic_set_fast_is_empty(bset)) {
150 opt = isl_vec_alloc(bset->ctx, 0);
151 isl_basic_set_free(bset);
155 opt = isl_vec_alloc(bset->ctx, 1 + dim);
158 obj = isl_vec_alloc(bset->ctx, 1 + dim);
161 isl_int_set_si(opt->el[0], 1);
162 isl_int_set_si(obj->el[0], 0);
164 for (i = 0; i < dim; ++i) {
165 enum isl_lp_result res;
167 isl_seq_clr(obj->el + 1, dim);
168 isl_int_set_si(obj->el[1 + i], 1);
169 res = isl_basic_set_solve_ilp(bset, max, obj->el,
170 &opt->el[1 + i], NULL);
171 if (res == isl_lp_empty)
173 assert(res == isl_lp_ok);
174 bset = isl_basic_set_fix(bset, isl_dim_set, i, opt->el[1 + i]);
177 isl_basic_set_free(bset);
183 opt = isl_vec_alloc(bset->ctx, 0);
184 isl_basic_set_free(bset);
190 struct isl_scan_pip {
191 struct isl_scan_callback callback;
200 /* Check if the "manually" computed optimum of bset at the "sample"
201 * values of the parameters agrees with the solution of pilp problem
202 * represented by the pair (sol, empty).
203 * In particular, if there is no solution for this value of the parameters,
204 * then it should be an element of the parameter domain "empty".
205 * Otherwise, the optimal solution, should be equal to the result of
206 * plugging in the value of the parameters in "sol".
208 static int scan_one(struct isl_scan_callback *callback,
209 __isl_take isl_vec *sample)
211 struct isl_scan_pip *sp = (struct isl_scan_pip *)callback;
214 opt = opt_at(isl_basic_set_copy(sp->bset), isl_vec_copy(sample), sp->max);
217 if (opt->size == 0) {
219 sample_set = isl_set_from_basic_set(
220 isl_basic_set_from_vec(sample));
221 assert(isl_set_is_subset(sample_set, sp->empty));
222 isl_set_free(sample_set);
227 opt_set = isl_set_from_basic_set(isl_basic_set_from_vec(opt));
228 sol = set_plug_in_parameters(isl_set_copy(sp->sol), sample);
229 assert(isl_set_is_equal(opt_set, sol));
231 isl_set_free(opt_set);
234 if (!(sp->n++ % sp->stride)) {
242 struct isl_scan_count {
243 struct isl_scan_callback callback;
247 static int count_one(struct isl_scan_callback *callback,
248 __isl_take isl_vec *sample)
250 struct isl_scan_count *sc = (struct isl_scan_count *)callback;
251 isl_vec_free(sample);
258 static void check_solution(isl_basic_set *bset, isl_basic_set *context,
259 isl_set *sol, isl_set *empty, int max)
262 struct isl_scan_count sc;
263 struct isl_scan_pip sp;
267 context = isl_basic_set_underlying_set(context);
269 cube = construct_cube(context);
270 context = isl_basic_set_intersect(context, cube);
272 sc.callback.add = count_one;
275 r = isl_basic_set_scan(isl_basic_set_copy(context), &sc.callback);
278 sp.callback.add = scan_one;
283 sp.stride = sc.n > 70 ? 1 + (sc.n + 1)/70 : 1;
286 for (i = 0; i < sc.n; i += sp.stride)
291 r = isl_basic_set_scan(context, &sp.callback);
296 isl_basic_set_free(bset);
299 int main(int argc, char **argv)
302 struct isl_basic_set *context, *bset, *copy, *context_copy;
304 struct isl_set *empty;
308 int urs_unknowns = 0;
312 struct pip_options *options;
314 options = pip_options_new_with_defaults();
316 argc = pip_options_parse(options, argc, argv);
318 ctx = isl_ctx_alloc_with_options(options->isl);
321 context = isl_basic_set_read_from_file(ctx, stdin, 0, ISL_FORMAT_POLYLIB);
323 n = fscanf(stdin, "%d", &neg_one);
325 assert(neg_one == -1);
326 bset = isl_basic_set_read_from_file(ctx, stdin,
327 isl_basic_set_dim(context, isl_dim_set), ISL_FORMAT_POLYLIB);
329 while (fgets(s, sizeof(s), stdin)) {
330 if (strncasecmp(s, "Maximize", 8) == 0)
332 if (strncasecmp(s, "Rational", 8) == 0) {
334 bset = isl_basic_set_set_rational(bset);
336 if (strncasecmp(s, "Urs_parms", 9) == 0)
338 if (strncasecmp(s, "Urs_unknowns", 12) == 0)
342 context = isl_basic_set_intersect(context,
343 isl_basic_set_positive_orthant(isl_basic_set_get_dim(context)));
344 context = to_parameter_domain(context);
346 bset = isl_basic_set_intersect(bset,
347 isl_basic_set_positive_orthant(isl_basic_set_get_dim(bset)));
349 if (options->verify) {
350 copy = isl_basic_set_copy(bset);
351 context_copy = isl_basic_set_copy(context);
355 set = isl_basic_set_partial_lexmax(bset, context, &empty);
357 set = isl_basic_set_partial_lexmin(bset, context, &empty);
359 if (options->verify) {
361 check_solution(copy, context_copy, set, empty, max);
363 isl_set_dump(set, stdout, 0);
364 fprintf(stdout, "no solution:\n");
365 isl_set_dump(empty, stdout, 4);