2 #include <isl/stream.h>
3 #include <isl_map_private.h>
4 #include <isl/polynomial.h>
7 #include <isl/options.h>
8 #include <isl/deprecated/point_int.h>
9 #include <isl/deprecated/polynomial_int.h>
11 struct bound_options
{
12 struct isl_options
*isl
;
15 int continue_on_error
;
18 ISL_ARGS_START(struct bound_options
, bound_options_args
)
19 ISL_ARG_CHILD(struct bound_options
, isl
, "isl", &isl_options_args
,
21 ISL_ARG_BOOL(struct bound_options
, verify
, 'T', "verify", 0, NULL
)
22 ISL_ARG_BOOL(struct bound_options
, print_all
, 'A', "print-all", 0, NULL
)
23 ISL_ARG_BOOL(struct bound_options
, continue_on_error
, '\0', "continue-on-error", 0, NULL
)
26 ISL_ARG_DEF(bound_options
, struct bound_options
, bound_options_args
)
28 static __isl_give isl_set
*set_bounds(__isl_take isl_set
*set
)
35 nparam
= isl_set_dim(set
, isl_dim_param
);
36 r
= nparam
>= 8 ? 5 : nparam
>= 5 ? 15 : 50;
38 pt
= isl_set_sample_point(isl_set_copy(set
));
39 pt2
= isl_point_copy(pt
);
41 for (i
= 0; i
< nparam
; ++i
) {
42 pt
= isl_point_add_ui(pt
, isl_dim_param
, i
, r
);
43 pt2
= isl_point_sub_ui(pt2
, isl_dim_param
, i
, r
);
46 box
= isl_set_box_from_points(pt
, pt2
);
48 return isl_set_intersect(set
, box
);
51 struct verify_point_bound
{
52 struct bound_options
*options
;
58 isl_pw_qpolynomial_fold
*pwf
;
59 isl_pw_qpolynomial_fold
*bound
;
62 static isl_stat
verify_point(__isl_take isl_point
*pnt
, void *user
)
66 struct verify_point_bound
*vpb
= (struct verify_point_bound
*) user
;
69 isl_pw_qpolynomial_fold
*pwf
;
70 isl_val
*bound
= NULL
;
78 FILE *out
= vpb
->options
->print_all
? stdout
: stderr
;
90 ctx
= isl_point_get_ctx(pnt
);
91 p
= isl_printer_to_file(ctx
, out
);
95 pwf
= isl_pw_qpolynomial_fold_copy(vpb
->pwf
);
97 nparam
= isl_pw_qpolynomial_fold_dim(pwf
, isl_dim_param
);
98 for (i
= 0; i
< nparam
; ++i
) {
99 isl_point_get_coordinate(pnt
, isl_dim_param
, i
, &t
);
100 pwf
= isl_pw_qpolynomial_fold_fix_dim(pwf
, isl_dim_param
, i
, t
);
103 bound
= isl_pw_qpolynomial_fold_eval(
104 isl_pw_qpolynomial_fold_copy(vpb
->bound
),
105 isl_point_copy(pnt
));
107 dom
= isl_pw_qpolynomial_fold_domain(isl_pw_qpolynomial_fold_copy(pwf
));
108 bounded
= isl_set_is_bounded(dom
);
114 opt
= isl_pw_qpolynomial_fold_eval(
115 isl_pw_qpolynomial_fold_copy(pwf
),
116 isl_set_sample_point(isl_set_copy(dom
)));
118 opt
= isl_pw_qpolynomial_fold_max(isl_pw_qpolynomial_fold_copy(pwf
));
120 opt
= isl_pw_qpolynomial_fold_min(isl_pw_qpolynomial_fold_copy(pwf
));
122 if (vpb
->exact
&& bounded
)
123 ok
= isl_val_eq(opt
, bound
);
125 ok
= isl_val_le(opt
, bound
);
127 ok
= isl_val_le(bound
, opt
);
131 if (vpb
->options
->print_all
|| !ok
) {
132 p
= isl_printer_print_str(p
, minmax
);
133 p
= isl_printer_print_str(p
, "(");
134 for (i
= 0; i
< nparam
; ++i
) {
136 p
= isl_printer_print_str(p
, ", ");
137 isl_point_get_coordinate(pnt
, isl_dim_param
, i
, &t
);
138 p
= isl_printer_print_isl_int(p
, t
);
140 p
= isl_printer_print_str(p
, ") = ");
141 p
= isl_printer_print_val(p
, bound
);
142 p
= isl_printer_print_str(p
, ", ");
143 p
= isl_printer_print_str(p
, bounded
? "opt" : "sample");
144 p
= isl_printer_print_str(p
, " = ");
145 p
= isl_printer_print_val(p
, opt
);
147 p
= isl_printer_print_str(p
, ". OK");
149 p
= isl_printer_print_str(p
, ". NOT OK");
150 p
= isl_printer_end_line(p
);
151 } else if ((vpb
->n
% vpb
->stride
) == 0) {
152 p
= isl_printer_print_str(p
, "o");
153 p
= isl_printer_flush(p
);
161 isl_pw_qpolynomial_fold_free(pwf
);
174 if (vpb
->options
->continue_on_error
)
177 return (vpb
->n
>= 1 && ok
) ? isl_stat_ok
: isl_stat_error
;
180 static int check_solution(__isl_take isl_pw_qpolynomial_fold
*pwf
,
181 __isl_take isl_pw_qpolynomial_fold
*bound
, int exact
,
182 struct bound_options
*options
)
184 struct verify_point_bound vpb
;
190 dom
= isl_pw_qpolynomial_fold_domain(isl_pw_qpolynomial_fold_copy(pwf
));
191 context
= isl_set_params(isl_set_copy(dom
));
192 context
= isl_set_remove_divs(context
);
193 context
= set_bounds(context
);
198 isl_int_set_si(max
, 200);
199 r
= isl_set_count_upto(context
, max
, &count
);
201 n
= isl_int_get_si(count
);
204 isl_int_clear(count
);
206 vpb
.options
= options
;
210 vpb
.stride
= n
> 70 ? 1 + (n
+ 1)/70 : 1;
214 if (!options
->print_all
) {
215 for (i
= 0; i
< vpb
.n
; i
+= vpb
.stride
)
221 isl_set_foreach_point(context
, verify_point
, &vpb
);
223 isl_set_free(context
);
225 isl_pw_qpolynomial_fold_free(pwf
);
226 isl_pw_qpolynomial_fold_free(bound
);
228 if (!options
->print_all
)
232 fprintf(stderr
, "Check failed !\n");
239 int main(int argc
, char **argv
)
242 isl_pw_qpolynomial_fold
*copy
;
243 isl_pw_qpolynomial_fold
*pwf
;
246 struct bound_options
*options
;
250 options
= bound_options_new_with_defaults();
252 argc
= bound_options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
254 ctx
= isl_ctx_alloc_with_options(&bound_options_args
, options
);
256 s
= isl_stream_new_file(ctx
, stdin
);
257 obj
= isl_stream_read_obj(s
);
258 if (obj
.type
== isl_obj_pw_qpolynomial
)
259 pwf
= isl_pw_qpolynomial_fold_from_pw_qpolynomial(isl_fold_max
,
261 else if (obj
.type
== isl_obj_pw_qpolynomial_fold
)
264 obj
.type
->free(obj
.v
);
265 isl_die(ctx
, isl_error_invalid
, "invalid input", goto error
);
269 copy
= isl_pw_qpolynomial_fold_copy(pwf
);
271 pwf
= isl_pw_qpolynomial_fold_bound(pwf
, &exact
);
272 pwf
= isl_pw_qpolynomial_fold_coalesce(pwf
);
274 if (options
->verify
) {
275 r
= check_solution(copy
, pwf
, exact
, options
);
278 printf("# NOT exact\n");
279 isl_pw_qpolynomial_fold_print(pwf
, stdout
, 0);
280 fprintf(stdout
, "\n");
281 isl_pw_qpolynomial_fold_free(pwf
);