2 #include <isl/stream.h>
3 #include <barvinok/barvinok.h>
4 #include <barvinok/options.h>
5 #include <barvinok/util.h>
9 struct verify_options
*verify
;
12 struct isl_arg options_arg
[] = {
13 ISL_ARG_CHILD(struct options
, verify
, NULL
,
14 verify_options_arg
, "verification")
18 ISL_ARG_DEF(options
, struct options
, options_arg
)
20 struct verify_point_sum
{
21 struct verify_point_data vpd
;
22 isl_pw_qpolynomial
*pwqp
;
23 isl_pw_qpolynomial
*sum
;
25 isl_pw_qpolynomial
*fixed
;
26 isl_qpolynomial
*manual
;
29 static int manual_sum(__isl_take isl_point
*pnt
, void *user
)
31 struct verify_point_sum
*vps
= (struct verify_point_sum
*) user
;
34 qp
= isl_pw_qpolynomial_eval(isl_pw_qpolynomial_copy(vps
->fixed
), pnt
);
35 vps
->manual
= isl_qpolynomial_add(vps
->manual
, qp
);
40 static int verify_point(__isl_take isl_point
*pnt
, void *user
)
42 struct verify_point_sum
*vps
= (struct verify_point_sum
*) user
;
49 isl_qpolynomial
*eval
;
51 FILE *out
= vps
->vpd
.options
->print_all
? stdout
: stderr
;
56 vps
->fixed
= isl_pw_qpolynomial_copy(vps
->pwqp
);
57 nparam
= isl_pw_qpolynomial_dim(vps
->sum
, isl_dim_param
);
58 for (i
= 0; i
< nparam
; ++i
) {
59 isl_point_get_coordinate(pnt
, isl_dim_param
, i
, &v
);
60 vps
->fixed
= isl_pw_qpolynomial_fix_dim(vps
->fixed
,
64 eval
= isl_pw_qpolynomial_eval(isl_pw_qpolynomial_copy(vps
->sum
),
67 vps
->manual
= isl_qpolynomial_zero(isl_pw_qpolynomial_get_space(vps
->pwqp
));
68 dom
= isl_pw_qpolynomial_domain(isl_pw_qpolynomial_copy(vps
->fixed
));
69 r
= isl_set_foreach_point(dom
, &manual_sum
, user
);
74 nvar
= isl_set_dim(dom
, isl_dim_set
);
75 vps
->manual
= isl_qpolynomial_project_domain_on_params(vps
->manual
);
77 ok
= isl_qpolynomial_plain_is_equal(eval
, vps
->manual
);
79 if (vps
->vpd
.options
->print_all
|| !ok
) {
80 isl_ctx
*ctx
= isl_pw_qpolynomial_get_ctx(vps
->pwqp
);
81 isl_printer
*p
= isl_printer_to_file(ctx
, out
);
83 for (i
= 0; i
< nparam
; ++i
) {
86 isl_point_get_coordinate(pnt
, isl_dim_param
, i
, &v
);
87 isl_int_print(out
, v
, 0);
90 p
= isl_printer_print_qpolynomial(p
, eval
);
91 fprintf(out
, ", sum(EP) = ");
92 p
= isl_printer_print_qpolynomial(p
, vps
->manual
);
94 fprintf(out
, ". OK\n");
96 fprintf(out
, ". NOT OK\n");
98 } else if ((vps
->vpd
.n
% vps
->vpd
.s
) == 0) {
107 isl_qpolynomial_free(vps
->manual
);
108 isl_pw_qpolynomial_free(vps
->fixed
);
109 isl_qpolynomial_free(eval
);
116 if (vps
->vpd
.options
->continue_on_error
)
119 return (vps
->vpd
.n
>= 1 && ok
) ? 0 : -1;
122 static int verify(__isl_keep isl_pw_qpolynomial
*pwqp
,
123 __isl_take isl_pw_qpolynomial
*sum
, struct verify_options
*options
)
125 struct verify_point_sum vps
= { { options
} };
132 context
= isl_pw_qpolynomial_domain(isl_pw_qpolynomial_copy(sum
));
133 context
= verify_context_set_bounds(context
, options
);
135 r
= verify_point_data_init(&vps
.vpd
, context
);
138 isl_set_foreach_point(context
, verify_point
, &vps
);
142 isl_set_free(context
);
144 verify_point_data_fini(&vps
.vpd
);
149 int main(int argc
, char **argv
)
155 isl_pw_qpolynomial
*pwqp
;
156 isl_pw_qpolynomial
*sum
;
157 struct isl_stream
*s
;
158 struct options
*options
= options_new_with_defaults();
160 argc
= options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
161 ctx
= isl_ctx_alloc_with_options(options_arg
, options
);
163 s
= isl_stream_new_file(ctx
, stdin
);
164 pwqp
= isl_stream_read_pw_qpolynomial(s
);
166 if (options
->verify
->verify
) {
167 isl_space
*dim
= isl_pw_qpolynomial_get_space(pwqp
);
168 unsigned total
= isl_space_dim(dim
, isl_dim_all
);
170 verify_options_set_range(options
->verify
, total
);
173 sum
= isl_pw_qpolynomial_sum(isl_pw_qpolynomial_copy(pwqp
));
174 if (options
->verify
->verify
)
175 result
= verify(pwqp
, sum
, options
->verify
);
177 isl_printer
*p
= isl_printer_to_file(ctx
, stdout
);
178 p
= isl_printer_print_pw_qpolynomial(p
, sum
);
179 p
= isl_printer_end_line(p
);
182 isl_pw_qpolynomial_free(sum
);
183 isl_pw_qpolynomial_free(pwqp
);