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 ISL_ARGS_START(struct options
, options_args
)
13 ISL_ARG_CHILD(struct options
, verify
, NULL
,
14 &verify_options_args
, "verification")
17 ISL_ARG_DEF(options
, struct options
, options_args
)
19 struct verify_point_sum
{
20 struct verify_point_data vpd
;
21 isl_pw_qpolynomial
*pwqp
;
22 isl_pw_qpolynomial
*sum
;
24 isl_pw_qpolynomial
*fixed
;
25 isl_qpolynomial
*manual
;
28 static int manual_sum(__isl_take isl_point
*pnt
, void *user
)
30 struct verify_point_sum
*vps
= (struct verify_point_sum
*) user
;
33 qp
= isl_pw_qpolynomial_eval(isl_pw_qpolynomial_copy(vps
->fixed
), pnt
);
34 vps
->manual
= isl_qpolynomial_add(vps
->manual
, qp
);
39 static int verify_point(__isl_take isl_point
*pnt
, void *user
)
41 struct verify_point_sum
*vps
= (struct verify_point_sum
*) user
;
49 isl_qpolynomial
*eval
;
51 FILE *out
= vps
->vpd
.options
->print_all
? stdout
: stderr
;
55 vps
->fixed
= isl_pw_qpolynomial_copy(vps
->pwqp
);
56 nparam
= isl_pw_qpolynomial_dim(vps
->sum
, isl_dim_param
);
57 for (i
= 0; i
< nparam
; ++i
) {
58 v
= isl_point_get_coordinate_val(pnt
, isl_dim_param
, i
);
59 vps
->fixed
= isl_pw_qpolynomial_fix_val(vps
->fixed
,
63 eval
= isl_pw_qpolynomial_eval(isl_pw_qpolynomial_copy(vps
->sum
),
66 space
= isl_pw_qpolynomial_get_domain_space(vps
->pwqp
);
67 vps
->manual
= isl_qpolynomial_zero_on_domain(space
);
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 v
= isl_point_get_coordinate_val(pnt
, isl_dim_param
, i
);
87 p
= isl_printer_print_val(p
, v
);
91 p
= isl_printer_print_qpolynomial(p
, eval
);
92 fprintf(out
, ", sum(EP) = ");
93 p
= isl_printer_print_qpolynomial(p
, vps
->manual
);
95 fprintf(out
, ". OK\n");
97 fprintf(out
, ". NOT OK\n");
99 } else if ((vps
->vpd
.n
% vps
->vpd
.s
) == 0) {
108 isl_qpolynomial_free(vps
->manual
);
109 isl_pw_qpolynomial_free(vps
->fixed
);
110 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_args
, 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
);