152a25237STobias Grosser #include <assert.h>
252a25237STobias Grosser #include <isl/stream.h>
352a25237STobias Grosser #include <isl_map_private.h>
4fa8079d0STobias Grosser #include <isl/polynomial.h>
552a25237STobias Grosser #include <isl_scan.h>
6fa8079d0STobias Grosser #include <isl/val.h>
752a25237STobias Grosser #include <isl/options.h>
852a25237STobias Grosser
952a25237STobias Grosser struct bound_options {
1052a25237STobias Grosser struct isl_options *isl;
1152a25237STobias Grosser unsigned verify;
1252a25237STobias Grosser int print_all;
1352a25237STobias Grosser int continue_on_error;
1452a25237STobias Grosser };
1552a25237STobias Grosser
ISL_ARGS_START(struct bound_options,bound_options_args)1652a25237STobias Grosser ISL_ARGS_START(struct bound_options, bound_options_args)
1752a25237STobias Grosser ISL_ARG_CHILD(struct bound_options, isl, "isl", &isl_options_args,
1852a25237STobias Grosser "isl options")
1952a25237STobias Grosser ISL_ARG_BOOL(struct bound_options, verify, 'T', "verify", 0, NULL)
2052a25237STobias Grosser ISL_ARG_BOOL(struct bound_options, print_all, 'A', "print-all", 0, NULL)
2152a25237STobias Grosser ISL_ARG_BOOL(struct bound_options, continue_on_error, '\0', "continue-on-error", 0, NULL)
2252a25237STobias Grosser ISL_ARGS_END
2352a25237STobias Grosser
2452a25237STobias Grosser ISL_ARG_DEF(bound_options, struct bound_options, bound_options_args)
2552a25237STobias Grosser
2652a25237STobias Grosser static __isl_give isl_set *set_bounds(__isl_take isl_set *set)
2752a25237STobias Grosser {
28*e8227804SMichael Kruse isl_size nparam;
2952a25237STobias Grosser int i, r;
3052a25237STobias Grosser isl_point *pt, *pt2;
3152a25237STobias Grosser isl_set *box;
3252a25237STobias Grosser
3352a25237STobias Grosser nparam = isl_set_dim(set, isl_dim_param);
34*e8227804SMichael Kruse if (nparam < 0)
35*e8227804SMichael Kruse return isl_set_free(set);
3652a25237STobias Grosser r = nparam >= 8 ? 5 : nparam >= 5 ? 15 : 50;
3752a25237STobias Grosser
3852a25237STobias Grosser pt = isl_set_sample_point(isl_set_copy(set));
3952a25237STobias Grosser pt2 = isl_point_copy(pt);
4052a25237STobias Grosser
4152a25237STobias Grosser for (i = 0; i < nparam; ++i) {
4252a25237STobias Grosser pt = isl_point_add_ui(pt, isl_dim_param, i, r);
4352a25237STobias Grosser pt2 = isl_point_sub_ui(pt2, isl_dim_param, i, r);
4452a25237STobias Grosser }
4552a25237STobias Grosser
4652a25237STobias Grosser box = isl_set_box_from_points(pt, pt2);
4752a25237STobias Grosser
4852a25237STobias Grosser return isl_set_intersect(set, box);
4952a25237STobias Grosser }
5052a25237STobias Grosser
5152a25237STobias Grosser struct verify_point_bound {
5252a25237STobias Grosser struct bound_options *options;
5352a25237STobias Grosser int stride;
5452a25237STobias Grosser int n;
5552a25237STobias Grosser int exact;
5652a25237STobias Grosser int error;
5752a25237STobias Grosser
5852a25237STobias Grosser isl_pw_qpolynomial_fold *pwf;
5952a25237STobias Grosser isl_pw_qpolynomial_fold *bound;
6052a25237STobias Grosser };
6152a25237STobias Grosser
verify_point(__isl_take isl_point * pnt,void * user)62b2f39926STobias Grosser static isl_stat verify_point(__isl_take isl_point *pnt, void *user)
6352a25237STobias Grosser {
6452a25237STobias Grosser int i;
65*e8227804SMichael Kruse isl_size nparam;
6652a25237STobias Grosser struct verify_point_bound *vpb = (struct verify_point_bound *) user;
67fa8079d0STobias Grosser isl_val *v;
6852a25237STobias Grosser isl_ctx *ctx;
6952a25237STobias Grosser isl_pw_qpolynomial_fold *pwf;
7052a25237STobias Grosser isl_val *bound = NULL;
7152a25237STobias Grosser isl_val *opt = NULL;
7252a25237STobias Grosser isl_set *dom = NULL;
7352a25237STobias Grosser isl_printer *p;
7452a25237STobias Grosser const char *minmax;
7572745c2eSTobias Grosser isl_bool bounded;
7652a25237STobias Grosser int sign;
7752a25237STobias Grosser int ok;
7852a25237STobias Grosser FILE *out = vpb->options->print_all ? stdout : stderr;
7952a25237STobias Grosser
8052a25237STobias Grosser vpb->n--;
8152a25237STobias Grosser
8252a25237STobias Grosser if (1) {
8352a25237STobias Grosser minmax = "ub";
8452a25237STobias Grosser sign = 1;
8552a25237STobias Grosser } else {
8652a25237STobias Grosser minmax = "lb";
8752a25237STobias Grosser sign = -1;
8852a25237STobias Grosser }
8952a25237STobias Grosser
9052a25237STobias Grosser ctx = isl_point_get_ctx(pnt);
9152a25237STobias Grosser p = isl_printer_to_file(ctx, out);
9252a25237STobias Grosser
9352a25237STobias Grosser pwf = isl_pw_qpolynomial_fold_copy(vpb->pwf);
9452a25237STobias Grosser
9552a25237STobias Grosser nparam = isl_pw_qpolynomial_fold_dim(pwf, isl_dim_param);
96*e8227804SMichael Kruse if (nparam < 0)
97*e8227804SMichael Kruse pwf = isl_pw_qpolynomial_fold_free(pwf);
9852a25237STobias Grosser for (i = 0; i < nparam; ++i) {
99fa8079d0STobias Grosser v = isl_point_get_coordinate_val(pnt, isl_dim_param, i);
100fa8079d0STobias Grosser pwf = isl_pw_qpolynomial_fold_fix_val(pwf, isl_dim_param, i, v);
10152a25237STobias Grosser }
10252a25237STobias Grosser
10352a25237STobias Grosser bound = isl_pw_qpolynomial_fold_eval(
10452a25237STobias Grosser isl_pw_qpolynomial_fold_copy(vpb->bound),
10552a25237STobias Grosser isl_point_copy(pnt));
10652a25237STobias Grosser
10752a25237STobias Grosser dom = isl_pw_qpolynomial_fold_domain(isl_pw_qpolynomial_fold_copy(pwf));
10852a25237STobias Grosser bounded = isl_set_is_bounded(dom);
10952a25237STobias Grosser
11052a25237STobias Grosser if (bounded < 0)
11152a25237STobias Grosser goto error;
11252a25237STobias Grosser
11352a25237STobias Grosser if (!bounded)
11452a25237STobias Grosser opt = isl_pw_qpolynomial_fold_eval(
11552a25237STobias Grosser isl_pw_qpolynomial_fold_copy(pwf),
11652a25237STobias Grosser isl_set_sample_point(isl_set_copy(dom)));
11752a25237STobias Grosser else if (sign > 0)
11852a25237STobias Grosser opt = isl_pw_qpolynomial_fold_max(isl_pw_qpolynomial_fold_copy(pwf));
11952a25237STobias Grosser else
12052a25237STobias Grosser opt = isl_pw_qpolynomial_fold_min(isl_pw_qpolynomial_fold_copy(pwf));
12152a25237STobias Grosser
12252a25237STobias Grosser if (vpb->exact && bounded)
12352a25237STobias Grosser ok = isl_val_eq(opt, bound);
12452a25237STobias Grosser else if (sign > 0)
12552a25237STobias Grosser ok = isl_val_le(opt, bound);
12652a25237STobias Grosser else
12752a25237STobias Grosser ok = isl_val_le(bound, opt);
12852a25237STobias Grosser if (ok < 0)
12952a25237STobias Grosser goto error;
13052a25237STobias Grosser
13152a25237STobias Grosser if (vpb->options->print_all || !ok) {
13252a25237STobias Grosser p = isl_printer_print_str(p, minmax);
13352a25237STobias Grosser p = isl_printer_print_str(p, "(");
13452a25237STobias Grosser for (i = 0; i < nparam; ++i) {
13552a25237STobias Grosser if (i)
13652a25237STobias Grosser p = isl_printer_print_str(p, ", ");
137fa8079d0STobias Grosser v = isl_point_get_coordinate_val(pnt, isl_dim_param, i);
138fa8079d0STobias Grosser p = isl_printer_print_val(p, v);
139fa8079d0STobias Grosser isl_val_free(v);
14052a25237STobias Grosser }
14152a25237STobias Grosser p = isl_printer_print_str(p, ") = ");
14252a25237STobias Grosser p = isl_printer_print_val(p, bound);
14352a25237STobias Grosser p = isl_printer_print_str(p, ", ");
14452a25237STobias Grosser p = isl_printer_print_str(p, bounded ? "opt" : "sample");
14552a25237STobias Grosser p = isl_printer_print_str(p, " = ");
14652a25237STobias Grosser p = isl_printer_print_val(p, opt);
14752a25237STobias Grosser if (ok)
14852a25237STobias Grosser p = isl_printer_print_str(p, ". OK");
14952a25237STobias Grosser else
15052a25237STobias Grosser p = isl_printer_print_str(p, ". NOT OK");
15152a25237STobias Grosser p = isl_printer_end_line(p);
15252a25237STobias Grosser } else if ((vpb->n % vpb->stride) == 0) {
15352a25237STobias Grosser p = isl_printer_print_str(p, "o");
15452a25237STobias Grosser p = isl_printer_flush(p);
15552a25237STobias Grosser }
15652a25237STobias Grosser
15752a25237STobias Grosser if (0) {
15852a25237STobias Grosser error:
15952a25237STobias Grosser ok = 0;
16052a25237STobias Grosser }
16152a25237STobias Grosser
16252a25237STobias Grosser isl_pw_qpolynomial_fold_free(pwf);
16352a25237STobias Grosser isl_val_free(bound);
16452a25237STobias Grosser isl_val_free(opt);
16552a25237STobias Grosser isl_point_free(pnt);
16652a25237STobias Grosser isl_set_free(dom);
16752a25237STobias Grosser
16852a25237STobias Grosser isl_printer_free(p);
16952a25237STobias Grosser
17052a25237STobias Grosser if (!ok)
17152a25237STobias Grosser vpb->error = 1;
17252a25237STobias Grosser
17352a25237STobias Grosser if (vpb->options->continue_on_error)
17452a25237STobias Grosser ok = 1;
17552a25237STobias Grosser
176b2f39926STobias Grosser return (vpb->n >= 1 && ok) ? isl_stat_ok : isl_stat_error;
17752a25237STobias Grosser }
17852a25237STobias Grosser
check_solution(__isl_take isl_pw_qpolynomial_fold * pwf,__isl_take isl_pw_qpolynomial_fold * bound,int exact,struct bound_options * options)17952a25237STobias Grosser static int check_solution(__isl_take isl_pw_qpolynomial_fold *pwf,
18052a25237STobias Grosser __isl_take isl_pw_qpolynomial_fold *bound, int exact,
18152a25237STobias Grosser struct bound_options *options)
18252a25237STobias Grosser {
18352a25237STobias Grosser struct verify_point_bound vpb;
18452a25237STobias Grosser isl_int count, max;
18552a25237STobias Grosser isl_set *dom;
18652a25237STobias Grosser isl_set *context;
18752a25237STobias Grosser int i, r, n;
18852a25237STobias Grosser
18952a25237STobias Grosser dom = isl_pw_qpolynomial_fold_domain(isl_pw_qpolynomial_fold_copy(pwf));
19052a25237STobias Grosser context = isl_set_params(isl_set_copy(dom));
19152a25237STobias Grosser context = isl_set_remove_divs(context);
19252a25237STobias Grosser context = set_bounds(context);
19352a25237STobias Grosser
19452a25237STobias Grosser isl_int_init(count);
19552a25237STobias Grosser isl_int_init(max);
19652a25237STobias Grosser
19752a25237STobias Grosser isl_int_set_si(max, 200);
19852a25237STobias Grosser r = isl_set_count_upto(context, max, &count);
19952a25237STobias Grosser assert(r >= 0);
20052a25237STobias Grosser n = isl_int_get_si(count);
20152a25237STobias Grosser
20252a25237STobias Grosser isl_int_clear(max);
20352a25237STobias Grosser isl_int_clear(count);
20452a25237STobias Grosser
20552a25237STobias Grosser vpb.options = options;
20652a25237STobias Grosser vpb.pwf = pwf;
20752a25237STobias Grosser vpb.bound = bound;
20852a25237STobias Grosser vpb.n = n;
20952a25237STobias Grosser vpb.stride = n > 70 ? 1 + (n + 1)/70 : 1;
21052a25237STobias Grosser vpb.error = 0;
21152a25237STobias Grosser vpb.exact = exact;
21252a25237STobias Grosser
21352a25237STobias Grosser if (!options->print_all) {
21452a25237STobias Grosser for (i = 0; i < vpb.n; i += vpb.stride)
21552a25237STobias Grosser printf(".");
21652a25237STobias Grosser printf("\r");
21752a25237STobias Grosser fflush(stdout);
21852a25237STobias Grosser }
21952a25237STobias Grosser
22052a25237STobias Grosser isl_set_foreach_point(context, verify_point, &vpb);
22152a25237STobias Grosser
22252a25237STobias Grosser isl_set_free(context);
22352a25237STobias Grosser isl_set_free(dom);
22452a25237STobias Grosser isl_pw_qpolynomial_fold_free(pwf);
22552a25237STobias Grosser isl_pw_qpolynomial_fold_free(bound);
22652a25237STobias Grosser
22752a25237STobias Grosser if (!options->print_all)
22852a25237STobias Grosser printf("\n");
22952a25237STobias Grosser
23052a25237STobias Grosser if (vpb.error) {
23152a25237STobias Grosser fprintf(stderr, "Check failed !\n");
23252a25237STobias Grosser return -1;
23352a25237STobias Grosser }
23452a25237STobias Grosser
23552a25237STobias Grosser return 0;
23652a25237STobias Grosser }
23752a25237STobias Grosser
main(int argc,char ** argv)23852a25237STobias Grosser int main(int argc, char **argv)
23952a25237STobias Grosser {
24052a25237STobias Grosser isl_ctx *ctx;
24152a25237STobias Grosser isl_pw_qpolynomial_fold *copy;
24252a25237STobias Grosser isl_pw_qpolynomial_fold *pwf;
2431fa7b972STobias Grosser isl_stream *s;
24452a25237STobias Grosser struct isl_obj obj;
24552a25237STobias Grosser struct bound_options *options;
246*e8227804SMichael Kruse isl_bool exact;
24752a25237STobias Grosser int r = 0;
24852a25237STobias Grosser
24952a25237STobias Grosser options = bound_options_new_with_defaults();
25052a25237STobias Grosser assert(options);
25152a25237STobias Grosser argc = bound_options_parse(options, argc, argv, ISL_ARG_ALL);
25252a25237STobias Grosser
25352a25237STobias Grosser ctx = isl_ctx_alloc_with_options(&bound_options_args, options);
25452a25237STobias Grosser
25552a25237STobias Grosser s = isl_stream_new_file(ctx, stdin);
25652a25237STobias Grosser obj = isl_stream_read_obj(s);
25752a25237STobias Grosser if (obj.type == isl_obj_pw_qpolynomial)
25852a25237STobias Grosser pwf = isl_pw_qpolynomial_fold_from_pw_qpolynomial(isl_fold_max,
25952a25237STobias Grosser obj.v);
26052a25237STobias Grosser else if (obj.type == isl_obj_pw_qpolynomial_fold)
26152a25237STobias Grosser pwf = obj.v;
26252a25237STobias Grosser else {
26352a25237STobias Grosser obj.type->free(obj.v);
26452a25237STobias Grosser isl_die(ctx, isl_error_invalid, "invalid input", goto error);
26552a25237STobias Grosser }
26652a25237STobias Grosser
26752a25237STobias Grosser if (options->verify)
26852a25237STobias Grosser copy = isl_pw_qpolynomial_fold_copy(pwf);
26952a25237STobias Grosser
27052a25237STobias Grosser pwf = isl_pw_qpolynomial_fold_bound(pwf, &exact);
27152a25237STobias Grosser pwf = isl_pw_qpolynomial_fold_coalesce(pwf);
27252a25237STobias Grosser
27352a25237STobias Grosser if (options->verify) {
27452a25237STobias Grosser r = check_solution(copy, pwf, exact, options);
27552a25237STobias Grosser } else {
27652a25237STobias Grosser if (!exact)
27752a25237STobias Grosser printf("# NOT exact\n");
27852a25237STobias Grosser isl_pw_qpolynomial_fold_print(pwf, stdout, 0);
27952a25237STobias Grosser fprintf(stdout, "\n");
28052a25237STobias Grosser isl_pw_qpolynomial_fold_free(pwf);
28152a25237STobias Grosser }
28252a25237STobias Grosser
28352a25237STobias Grosser error:
28452a25237STobias Grosser isl_stream_free(s);
28552a25237STobias Grosser
28652a25237STobias Grosser isl_ctx_free(ctx);
28752a25237STobias Grosser
28852a25237STobias Grosser return r;
28952a25237STobias Grosser }
290