add isl_printer
[isl.git] / pip.c
blobaf290c7580cacfb505eb1c0e222d005de169b216
1 /*
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
8 */
10 #include <assert.h>
11 #include <string.h>
12 #include "isl_set.h"
13 #include "isl_tab.h"
14 #include "isl_map_private.h"
15 #include "isl_sample.h"
16 #include "isl_scan.h"
17 #include "isl_seq.h"
18 #include "isl_ilp.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
26 * -1
27 * Problem constraints in PolyLib format
28 * Optional list of options
30 * The options are
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
37 struct pip_options {
38 struct isl_options *isl;
39 unsigned verify;
42 struct isl_arg pip_options_arg[] = {
43 ISL_ARG_CHILD(struct pip_options, isl, "isl", isl_options_arg)
44 ISL_ARG_BOOL(struct pip_options, verify, 'T', "verify", 0)
47 ISL_ARG_DEF(pip_options, struct pip_options, pip_options_arg)
49 static struct isl_basic_set *to_parameter_domain(struct isl_basic_set *context)
51 struct isl_dim *param_dim;
52 struct isl_basic_set *model;
54 param_dim = isl_dim_set_alloc(context->ctx,
55 isl_basic_set_n_dim(context), 0);
56 model = isl_basic_set_empty(param_dim);
57 context = isl_basic_set_from_underlying_set(context, model);
59 return context;
62 static isl_basic_set *construct_cube(isl_basic_set *context)
64 int i;
65 unsigned dim;
66 int range;
67 isl_int m, M;
68 struct isl_basic_set *cube;
69 struct isl_basic_set *interval;
70 struct isl_basic_set_list *list;
72 dim = isl_basic_set_total_dim(context);
73 if (dim == 0) {
74 struct isl_dim *dims;
75 dims = isl_dim_set_alloc(context->ctx, 0, 0);
76 return isl_basic_set_universe(dims);
79 if (dim >= 8)
80 range = 4;
81 else if (dim >= 5)
82 range = 6;
83 else
84 range = 30;
86 isl_int_init(m);
87 isl_int_init(M);
89 isl_int_set_si(m, -range);
90 isl_int_set_si(M, range);
92 interval = isl_basic_set_interval(context->ctx, m, M);
93 list = isl_basic_set_list_alloc(context->ctx, dim);
94 for (i = 0; i < dim; ++i)
95 list = isl_basic_set_list_add(list, isl_basic_set_copy(interval));
96 isl_basic_set_free(interval);
97 cube = isl_basic_set_product(list);
99 isl_int_clear(m);
100 isl_int_clear(M);
102 return cube;
105 isl_basic_set *plug_in_parameters(isl_basic_set *bset, struct isl_vec *params)
107 int i;
109 for (i = 0; i < params->size - 1; ++i)
110 bset = isl_basic_set_fix(bset,
111 isl_dim_param, i, params->el[1 + i]);
113 bset = isl_basic_set_remove(bset, isl_dim_param, 0, params->size - 1);
115 isl_vec_free(params);
117 return bset;
120 isl_set *set_plug_in_parameters(isl_set *set, struct isl_vec *params)
122 int i;
124 for (i = 0; i < params->size - 1; ++i)
125 set = isl_set_fix(set, isl_dim_param, i, params->el[1 + i]);
127 set = isl_set_remove(set, isl_dim_param, 0, params->size - 1);
129 isl_vec_free(params);
131 return set;
134 /* Compute the lexicographically minimal (or maximal if max is set)
135 * element of bset for the given values of the parameters, by
136 * successively solving an ilp problem in each direction.
138 struct isl_vec *opt_at(struct isl_basic_set *bset,
139 struct isl_vec *params, int max)
141 unsigned dim;
142 struct isl_vec *opt;
143 struct isl_vec *obj;
144 int i;
146 dim = isl_basic_set_dim(bset, isl_dim_set);
148 bset = plug_in_parameters(bset, params);
150 if (isl_basic_set_fast_is_empty(bset)) {
151 opt = isl_vec_alloc(bset->ctx, 0);
152 isl_basic_set_free(bset);
153 return opt;
156 opt = isl_vec_alloc(bset->ctx, 1 + dim);
157 assert(opt);
159 obj = isl_vec_alloc(bset->ctx, 1 + dim);
160 assert(obj);
162 isl_int_set_si(opt->el[0], 1);
163 isl_int_set_si(obj->el[0], 0);
165 for (i = 0; i < dim; ++i) {
166 enum isl_lp_result res;
168 isl_seq_clr(obj->el + 1, dim);
169 isl_int_set_si(obj->el[1 + i], 1);
170 res = isl_basic_set_solve_ilp(bset, max, obj->el,
171 &opt->el[1 + i], NULL);
172 if (res == isl_lp_empty)
173 goto empty;
174 assert(res == isl_lp_ok);
175 bset = isl_basic_set_fix(bset, isl_dim_set, i, opt->el[1 + i]);
178 isl_basic_set_free(bset);
179 isl_vec_free(obj);
181 return opt;
182 empty:
183 isl_vec_free(opt);
184 opt = isl_vec_alloc(bset->ctx, 0);
185 isl_basic_set_free(bset);
186 isl_vec_free(obj);
188 return opt;
191 struct isl_scan_pip {
192 struct isl_scan_callback callback;
193 isl_basic_set *bset;
194 isl_set *sol;
195 isl_set *empty;
196 int stride;
197 int n;
198 int max;
201 /* Check if the "manually" computed optimum of bset at the "sample"
202 * values of the parameters agrees with the solution of pilp problem
203 * represented by the pair (sol, empty).
204 * In particular, if there is no solution for this value of the parameters,
205 * then it should be an element of the parameter domain "empty".
206 * Otherwise, the optimal solution, should be equal to the result of
207 * plugging in the value of the parameters in "sol".
209 static int scan_one(struct isl_scan_callback *callback,
210 __isl_take isl_vec *sample)
212 struct isl_scan_pip *sp = (struct isl_scan_pip *)callback;
213 struct isl_vec *opt;
215 opt = opt_at(isl_basic_set_copy(sp->bset), isl_vec_copy(sample), sp->max);
216 assert(opt);
218 if (opt->size == 0) {
219 isl_point *sample_pnt;
220 sample_pnt = isl_point_alloc(isl_set_get_dim(sp->empty), sample);
221 assert(isl_set_contains_point(sp->empty, sample_pnt));
222 isl_point_free(sample_pnt);
223 isl_vec_free(opt);
224 } else {
225 isl_set *sol;
226 isl_set *opt_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));
230 isl_set_free(sol);
231 isl_set_free(opt_set);
234 if (!(sp->n++ % sp->stride)) {
235 printf("o");
236 fflush(stdout);
239 return 0;
242 struct isl_scan_count {
243 struct isl_scan_callback callback;
244 int n;
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);
253 sc->n++;
255 return 0;
258 static void check_solution(isl_basic_set *bset, isl_basic_set *context,
259 isl_set *sol, isl_set *empty, int max)
261 isl_basic_set *cube;
262 struct isl_scan_count sc;
263 struct isl_scan_pip sp;
264 int i;
265 int r;
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;
273 sc.n = 0;
275 r = isl_basic_set_scan(isl_basic_set_copy(context), &sc.callback);
276 assert (r == 0);
278 sp.callback.add = scan_one;
279 sp.bset = bset;
280 sp.sol = sol;
281 sp.empty = empty;
282 sp.n = 0;
283 sp.stride = sc.n > 70 ? 1 + (sc.n + 1)/70 : 1;
284 sp.max = max;
286 for (i = 0; i < sc.n; i += sp.stride)
287 printf(".");
288 printf("\r");
289 fflush(stdout);
291 r = isl_basic_set_scan(context, &sp.callback);
292 assert(r == 0);
294 printf("\n");
296 isl_basic_set_free(bset);
299 int main(int argc, char **argv)
301 struct isl_ctx *ctx;
302 struct isl_basic_set *context, *bset, *copy, *context_copy;
303 struct isl_set *set;
304 struct isl_set *empty;
305 int neg_one;
306 char s[1024];
307 int urs_parms = 0;
308 int urs_unknowns = 0;
309 int max = 0;
310 int rational = 0;
311 int n;
312 struct pip_options *options;
314 options = pip_options_new_with_defaults();
315 assert(options);
316 argc = pip_options_parse(options, argc, argv);
318 ctx = isl_ctx_alloc_with_options(options->isl);
319 options->isl = NULL;
321 context = isl_basic_set_read_from_file(ctx, stdin, 0);
322 assert(context);
323 n = fscanf(stdin, "%d", &neg_one);
324 assert(n == 1);
325 assert(neg_one == -1);
326 bset = isl_basic_set_read_from_file(ctx, stdin,
327 isl_basic_set_dim(context, isl_dim_set));
329 while (fgets(s, sizeof(s), stdin)) {
330 if (strncasecmp(s, "Maximize", 8) == 0)
331 max = 1;
332 if (strncasecmp(s, "Rational", 8) == 0) {
333 rational = 1;
334 bset = isl_basic_set_set_rational(bset);
336 if (strncasecmp(s, "Urs_parms", 9) == 0)
337 urs_parms = 1;
338 if (strncasecmp(s, "Urs_unknowns", 12) == 0)
339 urs_unknowns = 1;
341 if (!urs_parms)
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);
345 if (!urs_unknowns)
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);
354 if (max)
355 set = isl_basic_set_partial_lexmax(bset, context, &empty);
356 else
357 set = isl_basic_set_partial_lexmin(bset, context, &empty);
359 if (options->verify) {
360 assert(!rational);
361 check_solution(copy, context_copy, set, empty, max);
362 } else {
363 isl_set_print(set, stdout, 0, ISL_FORMAT_ISL);
364 fprintf(stdout, "\n");
365 fprintf(stdout, "no solution: ");
366 isl_set_print(empty, stdout, 0, ISL_FORMAT_ISL);
367 fprintf(stdout, "\n");
370 isl_set_free(set);
371 isl_set_free(empty);
372 isl_ctx_free(ctx);
373 free(options);
375 return 0;