iscc: add "lb" operation
[barvinok.git] / bound.c
blob0f8f184dc9493f42671ab5937f0f6f42c9a931a3
1 #include <assert.h>
2 #include <isl/stream.h>
3 #include <barvinok/options.h>
4 #include <barvinok/util.h>
5 #include <barvinok/barvinok.h>
6 #include "verify.h"
8 struct options {
9 struct verify_options *verify;
10 long split;
11 int lower;
12 long iterate;
15 ISL_ARGS_START(struct options, options_args)
16 ISL_ARG_CHILD(struct options, verify, NULL,
17 &verify_options_args, "verification")
18 ISL_ARG_LONG(struct options, split, 0, "split", 0, NULL)
19 ISL_ARG_OPT_LONG(struct options, iterate, 0, "iterate", 0, -1,
20 "exact result by iterating over domain (of specified maximal size)")
21 ISL_ARG_BOOL(struct options, lower, 0, "lower", 0,
22 "compute lower bound instead of upper bound")
23 ISL_ARGS_END
25 ISL_ARG_DEF(options, struct options, options_args)
27 struct verify_point_bound {
28 struct verify_point_data vpd;
29 isl_pw_qpolynomial *pwqp;
30 isl_pw_qpolynomial_fold *pwf;
31 enum isl_fold type;
34 static isl_stat verify_point(__isl_take isl_point *pnt, void *user)
36 int i;
37 unsigned nparam;
38 struct verify_point_bound *vpb = (struct verify_point_bound *) user;
39 isl_val *v, *b, *q, *t;
40 isl_pw_qpolynomial *pwqp;
41 const char *minmax;
42 int sign;
43 int ok;
44 int cst;
45 FILE *out = vpb->vpd.options->print_all ? stdout : stderr;
47 vpb->vpd.n--;
49 if (vpb->type == isl_fold_max) {
50 minmax = "max";
51 sign = 1;
52 } else {
53 minmax = "min";
54 sign = -1;
57 pwqp = isl_pw_qpolynomial_copy(vpb->pwqp);
59 nparam = isl_pw_qpolynomial_dim(pwqp, isl_dim_param);
60 for (i = 0; i < nparam; ++i) {
61 t = isl_point_get_coordinate_val(pnt, isl_dim_param, i);
62 pwqp = isl_pw_qpolynomial_fix_val(pwqp, isl_dim_param, i, t);
65 b = isl_pw_qpolynomial_fold_eval(isl_pw_qpolynomial_fold_copy(vpb->pwf),
66 isl_point_copy(pnt));
68 if (sign > 0)
69 v = isl_pw_qpolynomial_max(pwqp);
70 else
71 v = isl_pw_qpolynomial_min(pwqp);
73 if (sign > 0)
74 v = isl_val_floor(v);
75 else
76 v = isl_val_ceil(v);
78 q = isl_val_copy(b);
79 if (sign > 0)
80 b = isl_val_floor(b);
81 else
82 b = isl_val_ceil(b);
84 if (sign > 0)
85 ok = isl_val_ge(b, v);
86 else
87 ok = isl_val_le(b, v);
89 if (vpb->vpd.options->print_all || !ok) {
90 isl_ctx *ctx = isl_point_get_ctx(pnt);
91 isl_printer *p;
92 p = isl_printer_to_file(ctx, out);
93 p = isl_printer_print_str(p, minmax);
94 p = isl_printer_print_str(p, "(");
95 for (i = 0; i < nparam; ++i) {
96 if (i)
97 p = isl_printer_print_str(p, ", ");
98 t = isl_point_get_coordinate_val(pnt, isl_dim_param, i);
99 p = isl_printer_print_val(p, t);
100 isl_val_free(t);
102 p = isl_printer_print_str(p, ") = ");
103 p = isl_printer_print_val(p, q);
104 if (!isl_val_is_int(q)) {
105 p = isl_printer_print_str(p, " (");
106 p = isl_printer_print_val(p, b);
107 p = isl_printer_print_str(p, ")");
109 p = isl_printer_print_str(p, ", ");
110 p = isl_printer_print_str(p, minmax);
111 p = isl_printer_print_str(p, "(EP) = ");
112 p = isl_printer_print_val(p, v);
113 if (ok)
114 p = isl_printer_print_str(p, ". OK");
115 else
116 p = isl_printer_print_str(p, ". NOT OK");
117 p = isl_printer_end_line(p);
118 isl_printer_free(p);
119 } else if ((vpb->vpd.n % vpb->vpd.s) == 0) {
120 printf("o");
121 fflush(stdout);
124 if (0) {
125 error:
126 ok = 0;
129 isl_point_free(pnt);
131 isl_val_free(b);
132 isl_val_free(q);
133 isl_val_free(v);
135 if (!ok)
136 vpb->vpd.error = 1;
138 if (vpb->vpd.options->continue_on_error)
139 ok = 1;
141 return (vpb->vpd.n >= 1 && ok) ? isl_stat_ok : isl_stat_error;
144 static int verify(__isl_keep isl_pw_qpolynomial_fold *pwf,
145 __isl_take isl_pw_qpolynomial *pwqp, enum isl_fold type,
146 struct verify_options *options)
148 struct verify_point_bound vpb = { { options } };
149 isl_set *context;
150 int r;
152 vpb.pwf = pwf;
153 vpb.type = type;
154 vpb.pwqp = pwqp;
155 context = isl_pw_qpolynomial_fold_domain(
156 isl_pw_qpolynomial_fold_copy(vpb.pwf));
157 context = verify_context_set_bounds(context, options);
159 r = verify_point_data_init(&vpb.vpd, context);
161 if (r == 0)
162 isl_set_foreach_point(context, verify_point, &vpb);
163 if (vpb.vpd.error)
164 r = -1;
166 isl_set_free(context);
167 isl_pw_qpolynomial_free(pwqp);
169 verify_point_data_fini(&vpb.vpd);
171 return r;
174 static __isl_give isl_pw_qpolynomial_fold *iterate(
175 __isl_take isl_pw_qpolynomial *pwqp, enum isl_fold type)
177 isl_space *dim = isl_pw_qpolynomial_get_space(pwqp);
178 isl_set *set;
179 isl_val *v;
180 isl_qpolynomial *qp;
181 isl_qpolynomial_fold *fold;
182 unsigned nvar;
184 assert(isl_space_dim(dim, isl_dim_param) == 0);
185 nvar = isl_space_dim(dim, isl_dim_set);
187 if (type == isl_fold_min)
188 v = isl_pw_qpolynomial_min(pwqp);
189 else
190 v = isl_pw_qpolynomial_max(pwqp);
192 dim = isl_space_drop_dims(dim, isl_dim_set, 0, nvar);
193 qp = isl_qpolynomial_val_on_domain(isl_space_copy(dim), v);
194 fold = isl_qpolynomial_fold_alloc(type, qp);
195 set = isl_set_universe(dim);
197 return isl_pw_qpolynomial_fold_alloc(type, set, fold);
200 struct bv_split_data {
201 int size;
202 __isl_give isl_pw_qpolynomial *pwqp_less;
203 __isl_give isl_pw_qpolynomial *pwqp_more;
206 static isl_stat split_on_size(__isl_take isl_set *set,
207 __isl_take isl_qpolynomial *qp, void *user)
209 struct bv_split_data *data = (struct bv_split_data *)user;
210 int bounded;
211 isl_set *set_np;
212 isl_pw_qpolynomial *pwqp;
213 int nparam;
215 nparam = isl_set_dim(set, isl_dim_param);
216 set_np = isl_set_move_dims(isl_set_copy(set), isl_dim_set, 0,
217 isl_dim_param, 0, nparam);
218 bounded = isl_set_is_bounded(set_np);
219 assert(bounded >= 0);
220 if (bounded) {
221 isl_pw_qpolynomial *pwqp;
222 isl_val *m;
224 pwqp = isl_set_card(set_np);
225 m = isl_pw_qpolynomial_max(pwqp);
226 bounded = isl_val_cmp_si(m, data->size) <= 0;
227 isl_val_free(m);
228 } else
229 isl_set_free(set_np);
231 pwqp = isl_pw_qpolynomial_alloc(set, qp);
232 if (bounded)
233 data->pwqp_less = isl_pw_qpolynomial_add_disjoint(
234 data->pwqp_less, pwqp);
235 else
236 data->pwqp_more = isl_pw_qpolynomial_add_disjoint(
237 data->pwqp_more, pwqp);
239 return isl_stat_ok;
243 * Split (partition) pwpq into a partition with (sub)domains containing
244 * size integer points or less and a partition with (sub)domains
245 * containing more integer points.
247 static int split_on_domain_size(__isl_take isl_pw_qpolynomial *pwqp,
248 __isl_give isl_pw_qpolynomial **pwqp_less,
249 __isl_give isl_pw_qpolynomial **pwqp_more,
250 int size)
252 isl_space *dim;
253 struct bv_split_data data = { size };
254 int r;
256 dim = isl_pw_qpolynomial_get_space(pwqp);
257 data.pwqp_less = isl_pw_qpolynomial_zero(isl_space_copy(dim));
258 data.pwqp_more = isl_pw_qpolynomial_zero(dim);
259 r = isl_pw_qpolynomial_foreach_piece(pwqp, &split_on_size, &data);
260 *pwqp_less = data.pwqp_less;
261 *pwqp_more = data.pwqp_more;
262 isl_pw_qpolynomial_free(pwqp);
264 return r;
267 static __isl_give isl_pw_qpolynomial_fold *optimize(
268 __isl_take isl_pw_qpolynomial *pwqp, enum isl_fold type,
269 struct options *options)
271 isl_pw_qpolynomial_fold *pwf;
273 if (options->iterate > 0) {
274 isl_pw_qpolynomial *pwqp_less, *pwqp_more;
275 isl_pw_qpolynomial_fold *pwf_less, *pwf_more;
276 split_on_domain_size(pwqp, &pwqp_less, &pwqp_more, options->iterate);
277 pwf_less = iterate(pwqp_less, type);
278 pwf_more = isl_pw_qpolynomial_bound(pwqp_more, type, NULL);
279 pwf = isl_pw_qpolynomial_fold_fold(pwf_less, pwf_more);
280 } else if (options->iterate)
281 pwf = iterate(pwqp, type);
282 else
283 pwf = isl_pw_qpolynomial_bound(pwqp, type, NULL);
284 return pwf;
287 static int optimize_and_print(__isl_take isl_pw_qpolynomial *pwqp,
288 struct options *options)
290 int print_solution = 1;
291 int result = 0;
292 isl_pw_qpolynomial_fold *pwf;
293 enum isl_fold type = options->lower ? isl_fold_min : isl_fold_max;
295 if (options->verify->verify) {
296 isl_space *dim = isl_pw_qpolynomial_get_space(pwqp);
297 unsigned total = isl_space_dim(dim, isl_dim_all);
298 isl_space_free(dim);
299 verify_options_set_range(options->verify, total);
300 if (!options->verify->barvinok->verbose)
301 print_solution = 0;
304 pwf = optimize(isl_pw_qpolynomial_copy(pwqp), type, options);
305 assert(pwf);
306 if (print_solution) {
307 isl_ctx *ctx = isl_pw_qpolynomial_get_ctx(pwqp);
308 isl_printer *p = isl_printer_to_file(ctx, stdout);
309 p = isl_printer_print_pw_qpolynomial_fold(p, pwf);
310 p = isl_printer_end_line(p);
311 isl_printer_free(p);
313 if (options->verify->verify) {
314 enum isl_fold type = options->lower ? isl_fold_min : isl_fold_max;
315 result = verify(pwf, pwqp, type, options->verify);
316 } else
317 isl_pw_qpolynomial_free(pwqp);
318 isl_pw_qpolynomial_fold_free(pwf);
320 return result;
323 int main(int argc, char **argv)
325 struct options *options = options_new_with_defaults();
326 isl_ctx *ctx;
327 isl_pw_qpolynomial *pwqp;
328 struct isl_stream *s;
329 int result = 0;
331 argc = options_parse(options, argc, argv, ISL_ARG_ALL);
332 ctx = isl_ctx_alloc_with_options(&options_args, options);
334 s = isl_stream_new_file(ctx, stdin);
335 pwqp = isl_stream_read_pw_qpolynomial(s);
337 if (options->split)
338 pwqp = isl_pw_qpolynomial_split_periods(pwqp, options->split);
340 result = optimize_and_print(pwqp, options);
342 isl_stream_free(s);
343 isl_ctx_free(ctx);
344 return result;