5 #include "isl_map_private.h"
6 #include "isl_sample.h"
11 /* The input of this program is the same as that of the "example" program
12 * from the PipLib distribution, except that the "big parameter column"
13 * should always be -1.
15 * Context constraints in PolyLib format
17 * Problem constraints in PolyLib format
18 * Optional list of options
21 * Maximize compute maximum instead of minimum
22 * Rational compute rational optimum instead of integer optimum
23 * Urs_parms don't assume parameters are non-negative
24 * Urs_unknowns don't assume unknowns are non-negative
28 struct isl_options *isl;
32 struct isl_arg pip_options_arg[] = {
33 ISL_ARG_CHILD(struct pip_options, isl, "isl", isl_options_arg)
34 ISL_ARG_BOOL(struct pip_options, verify, 'T', "verify", 0)
37 ISL_ARG_DEF(pip_options, struct pip_options, pip_options_arg)
39 static struct isl_basic_set *to_parameter_domain(struct isl_basic_set *context)
41 struct isl_dim *param_dim;
42 struct isl_basic_set *model;
44 param_dim = isl_dim_set_alloc(context->ctx,
45 isl_basic_set_n_dim(context), 0);
46 model = isl_basic_set_empty(param_dim);
47 context = isl_basic_set_from_underlying_set(context, model);
52 static isl_basic_set *construct_cube(isl_basic_set *context)
58 struct isl_basic_set *cube;
59 struct isl_basic_set *interval;
60 struct isl_basic_set_list *list;
62 dim = isl_basic_set_total_dim(context);
65 dims = isl_dim_set_alloc(context->ctx, 0, 0);
66 return isl_basic_set_universe(dims);
79 isl_int_set_si(m, -range);
80 isl_int_set_si(M, range);
82 interval = isl_basic_set_interval(context->ctx, m, M);
83 list = isl_basic_set_list_alloc(context->ctx, dim);
84 for (i = 0; i < dim; ++i)
85 list = isl_basic_set_list_add(list, isl_basic_set_copy(interval));
86 isl_basic_set_free(interval);
87 cube = isl_basic_set_product(list);
95 isl_basic_set *plug_in_parameters(isl_basic_set *bset, struct isl_vec *params)
99 for (i = 0; i < params->size - 1; ++i)
100 bset = isl_basic_set_fix(bset,
101 isl_dim_param, i, params->el[1 + i]);
103 bset = isl_basic_set_remove(bset, isl_dim_param, 0, params->size - 1);
105 isl_vec_free(params);
110 isl_set *set_plug_in_parameters(isl_set *set, struct isl_vec *params)
114 for (i = 0; i < params->size - 1; ++i)
115 set = isl_set_fix(set, isl_dim_param, i, params->el[1 + i]);
117 set = isl_set_remove(set, isl_dim_param, 0, params->size - 1);
119 isl_vec_free(params);
124 /* Compute the lexicographically minimal (or maximal if max is set)
125 * element of bset for the given values of the parameters, by
126 * successively solving an ilp problem in each direction.
128 struct isl_vec *opt_at(struct isl_basic_set *bset,
129 struct isl_vec *params, int max)
136 dim = isl_basic_set_dim(bset, isl_dim_set);
138 bset = plug_in_parameters(bset, params);
140 if (isl_basic_set_fast_is_empty(bset)) {
141 opt = isl_vec_alloc(bset->ctx, 0);
142 isl_basic_set_free(bset);
146 opt = isl_vec_alloc(bset->ctx, 1 + dim);
149 obj = isl_vec_alloc(bset->ctx, 1 + dim);
152 isl_int_set_si(opt->el[0], 1);
153 isl_int_set_si(obj->el[0], 0);
155 for (i = 0; i < dim; ++i) {
156 enum isl_lp_result res;
158 isl_seq_clr(obj->el + 1, dim);
159 isl_int_set_si(obj->el[1 + i], 1);
160 res = isl_basic_set_solve_ilp(bset, max, obj->el,
161 &opt->el[1 + i], NULL);
162 if (res == isl_lp_empty)
164 assert(res == isl_lp_ok);
165 bset = isl_basic_set_fix(bset, isl_dim_set, i, opt->el[1 + i]);
168 isl_basic_set_free(bset);
174 opt = isl_vec_alloc(bset->ctx, 0);
175 isl_basic_set_free(bset);
181 struct isl_scan_pip {
182 struct isl_scan_callback callback;
191 /* Check if the "manually" computed optimum of bset at the "sample"
192 * values of the parameters agrees with the solution of pilp problem
193 * represented by the pair (sol, empty).
194 * In particular, if there is no solution for this value of the parameters,
195 * then it should be an element of the parameter domain "empty".
196 * Otherwise, the optimal solution, should be equal to the result of
197 * plugging in the value of the parameters in "sol".
199 static int scan_one(struct isl_scan_callback *callback,
200 __isl_take isl_vec *sample)
202 struct isl_scan_pip *sp = (struct isl_scan_pip *)callback;
205 opt = opt_at(isl_basic_set_copy(sp->bset), isl_vec_copy(sample), sp->max);
208 if (opt->size == 0) {
210 sample_set = isl_set_from_basic_set(
211 isl_basic_set_from_vec(sample));
212 assert(isl_set_is_subset(sample_set, sp->empty));
213 isl_set_free(sample_set);
218 opt_set = isl_set_from_basic_set(isl_basic_set_from_vec(opt));
219 sol = set_plug_in_parameters(isl_set_copy(sp->sol), sample);
220 assert(isl_set_is_equal(opt_set, sol));
222 isl_set_free(opt_set);
225 if (!(sp->n++ % sp->stride)) {
233 struct isl_scan_count {
234 struct isl_scan_callback callback;
238 static int count_one(struct isl_scan_callback *callback,
239 __isl_take isl_vec *sample)
241 struct isl_scan_count *sc = (struct isl_scan_count *)callback;
242 isl_vec_free(sample);
249 static void check_solution(isl_basic_set *bset, isl_basic_set *context,
250 isl_set *sol, isl_set *empty, int max)
253 struct isl_scan_count sc;
254 struct isl_scan_pip sp;
258 context = isl_basic_set_underlying_set(context);
260 cube = construct_cube(context);
261 context = isl_basic_set_intersect(context, cube);
263 sc.callback.add = count_one;
266 r = isl_basic_set_scan(isl_basic_set_copy(context), &sc.callback);
269 sp.callback.add = scan_one;
274 sp.stride = sc.n > 70 ? 1 + (sc.n + 1)/70 : 1;
277 for (i = 0; i < sc.n; i += sp.stride)
282 r = isl_basic_set_scan(context, &sp.callback);
287 isl_basic_set_free(bset);
290 int main(int argc, char **argv)
293 struct isl_basic_set *context, *bset, *copy, *context_copy;
295 struct isl_set *empty;
299 int urs_unknowns = 0;
303 struct pip_options *options;
305 options = pip_options_new_with_defaults();
307 argc = pip_options_parse(options, argc, argv);
309 ctx = isl_ctx_alloc_with_options(options->isl);
312 context = isl_basic_set_read_from_file(ctx, stdin, 0, ISL_FORMAT_POLYLIB);
314 n = fscanf(stdin, "%d", &neg_one);
316 assert(neg_one == -1);
317 bset = isl_basic_set_read_from_file(ctx, stdin,
318 isl_basic_set_dim(context, isl_dim_set), ISL_FORMAT_POLYLIB);
320 while (fgets(s, sizeof(s), stdin)) {
321 if (strncasecmp(s, "Maximize", 8) == 0)
323 if (strncasecmp(s, "Rational", 8) == 0) {
325 bset = isl_basic_set_set_rational(bset);
327 if (strncasecmp(s, "Urs_parms", 9) == 0)
329 if (strncasecmp(s, "Urs_unknowns", 12) == 0)
333 context = isl_basic_set_intersect(context,
334 isl_basic_set_positive_orthant(isl_basic_set_get_dim(context)));
335 context = to_parameter_domain(context);
337 bset = isl_basic_set_intersect(bset,
338 isl_basic_set_positive_orthant(isl_basic_set_get_dim(bset)));
340 if (options->verify) {
341 copy = isl_basic_set_copy(bset);
342 context_copy = isl_basic_set_copy(context);
346 set = isl_basic_set_partial_lexmax(bset, context, &empty);
348 set = isl_basic_set_partial_lexmin(bset, context, &empty);
350 if (options->verify) {
352 check_solution(copy, context_copy, set, empty, max);
354 isl_set_dump(set, stdout, 0);
355 fprintf(stdout, "no solution:\n");
356 isl_set_dump(empty, stdout, 4);