2 #include <isl/stream.h>
3 #include <barvinok/options.h>
4 #include <barvinok/util.h>
5 #include <barvinok/barvinok.h>
9 struct verify_options
*verify
;
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")
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
;
34 static int verify_point(__isl_take isl_point
*pnt
, void *user
)
38 struct verify_point_bound
*vpb
= (struct verify_point_bound
*) user
;
39 isl_val
*v
, *b
, *q
, *t
;
40 isl_pw_qpolynomial
*pwqp
;
41 isl_qpolynomial
*bound
;
47 FILE *out
= vpb
->vpd
.options
->print_all
? stdout
: stderr
;
51 if (vpb
->type
== isl_fold_max
) {
59 pwqp
= isl_pw_qpolynomial_copy(vpb
->pwqp
);
61 nparam
= isl_pw_qpolynomial_dim(pwqp
, isl_dim_param
);
62 for (i
= 0; i
< nparam
; ++i
) {
63 t
= isl_point_get_coordinate_val(pnt
, isl_dim_param
, i
);
64 pwqp
= isl_pw_qpolynomial_fix_val(pwqp
, isl_dim_param
, i
, t
);
67 bound
= isl_pw_qpolynomial_fold_eval(isl_pw_qpolynomial_fold_copy(vpb
->pwf
),
69 b
= isl_qpolynomial_get_constant_val(bound
);
70 isl_qpolynomial_free(bound
);
73 opt
= isl_pw_qpolynomial_max(pwqp
);
75 opt
= isl_pw_qpolynomial_min(pwqp
);
76 v
= isl_qpolynomial_get_constant_val(opt
);
77 isl_qpolynomial_free(opt
);
91 ok
= isl_val_ge(b
, v
);
93 ok
= isl_val_le(b
, v
);
95 if (vpb
->vpd
.options
->print_all
|| !ok
) {
96 isl_ctx
*ctx
= isl_point_get_ctx(pnt
);
98 p
= isl_printer_to_file(ctx
, out
);
99 p
= isl_printer_print_str(p
, minmax
);
100 p
= isl_printer_print_str(p
, "(");
101 for (i
= 0; i
< nparam
; ++i
) {
103 p
= isl_printer_print_str(p
, ", ");
104 t
= isl_point_get_coordinate_val(pnt
, isl_dim_param
, i
);
105 p
= isl_printer_print_val(p
, t
);
108 p
= isl_printer_print_str(p
, ") = ");
109 p
= isl_printer_print_val(p
, q
);
110 if (!isl_val_is_int(q
)) {
111 p
= isl_printer_print_str(p
, " (");
112 p
= isl_printer_print_val(p
, b
);
113 p
= isl_printer_print_str(p
, ")");
115 p
= isl_printer_print_str(p
, ", ");
116 p
= isl_printer_print_str(p
, minmax
);
117 p
= isl_printer_print_str(p
, "(EP) = ");
118 p
= isl_printer_print_val(p
, v
);
120 p
= isl_printer_print_str(p
, ". OK");
122 p
= isl_printer_print_str(p
, ". NOT OK");
123 p
= isl_printer_end_line(p
);
125 } else if ((vpb
->vpd
.n
% vpb
->vpd
.s
) == 0) {
144 if (vpb
->vpd
.options
->continue_on_error
)
147 return (vpb
->vpd
.n
>= 1 && ok
) ? 0 : -1;
150 static int verify(__isl_keep isl_pw_qpolynomial_fold
*pwf
,
151 __isl_take isl_pw_qpolynomial
*pwqp
, enum isl_fold type
,
152 struct verify_options
*options
)
154 struct verify_point_bound vpb
= { { options
} };
161 context
= isl_pw_qpolynomial_fold_domain(
162 isl_pw_qpolynomial_fold_copy(vpb
.pwf
));
163 context
= verify_context_set_bounds(context
, options
);
165 r
= verify_point_data_init(&vpb
.vpd
, context
);
168 isl_set_foreach_point(context
, verify_point
, &vpb
);
172 isl_set_free(context
);
173 isl_pw_qpolynomial_free(pwqp
);
175 verify_point_data_fini(&vpb
.vpd
);
180 static __isl_give isl_pw_qpolynomial_fold
*iterate(
181 __isl_take isl_pw_qpolynomial
*pwqp
, enum isl_fold type
)
183 isl_space
*dim
= isl_pw_qpolynomial_get_space(pwqp
);
186 isl_qpolynomial_fold
*fold
;
189 assert(isl_space_dim(dim
, isl_dim_param
) == 0);
190 nvar
= isl_space_dim(dim
, isl_dim_set
);
192 if (type
== isl_fold_min
)
193 qp
= isl_pw_qpolynomial_min(pwqp
);
195 qp
= isl_pw_qpolynomial_max(pwqp
);
197 qp
= isl_qpolynomial_drop_dims(qp
, isl_dim_set
, 0, nvar
);
198 fold
= isl_qpolynomial_fold_alloc(type
, qp
);
199 dim
= isl_space_drop_dims(dim
, isl_dim_set
, 0, nvar
);
200 set
= isl_set_universe(dim
);
202 return isl_pw_qpolynomial_fold_alloc(type
, set
, fold
);
205 struct bv_split_data
{
207 __isl_give isl_pw_qpolynomial
*pwqp_less
;
208 __isl_give isl_pw_qpolynomial
*pwqp_more
;
211 static int split_on_size(__isl_take isl_set
*set
,
212 __isl_take isl_qpolynomial
*qp
, void *user
)
214 struct bv_split_data
*data
= (struct bv_split_data
*)user
;
217 isl_pw_qpolynomial
*pwqp
;
220 nparam
= isl_set_dim(set
, isl_dim_param
);
221 set_np
= isl_set_move_dims(isl_set_copy(set
), isl_dim_set
, 0,
222 isl_dim_param
, 0, nparam
);
223 bounded
= isl_set_is_bounded(set_np
);
224 assert(bounded
>= 0);
226 isl_pw_qpolynomial
*pwqp
;
227 isl_qpolynomial
*cst
;
231 pwqp
= isl_set_card(set_np
);
232 cst
= isl_pw_qpolynomial_max(pwqp
);
234 is_cst
= isl_qpolynomial_is_cst(cst
, &m
, NULL
);
235 isl_qpolynomial_free(cst
);
237 bounded
= isl_int_cmp_si(m
, data
->size
) <= 0;
240 isl_set_free(set_np
);
242 pwqp
= isl_pw_qpolynomial_alloc(set
, qp
);
244 data
->pwqp_less
= isl_pw_qpolynomial_add_disjoint(
245 data
->pwqp_less
, pwqp
);
247 data
->pwqp_more
= isl_pw_qpolynomial_add_disjoint(
248 data
->pwqp_more
, pwqp
);
254 * Split (partition) pwpq into a partition with (sub)domains containing
255 * size integer points or less and a partition with (sub)domains
256 * containing more integer points.
258 static int split_on_domain_size(__isl_take isl_pw_qpolynomial
*pwqp
,
259 __isl_give isl_pw_qpolynomial
**pwqp_less
,
260 __isl_give isl_pw_qpolynomial
**pwqp_more
,
264 struct bv_split_data data
= { size
};
267 dim
= isl_pw_qpolynomial_get_space(pwqp
);
268 data
.pwqp_less
= isl_pw_qpolynomial_zero(isl_space_copy(dim
));
269 data
.pwqp_more
= isl_pw_qpolynomial_zero(dim
);
270 r
= isl_pw_qpolynomial_foreach_piece(pwqp
, &split_on_size
, &data
);
271 *pwqp_less
= data
.pwqp_less
;
272 *pwqp_more
= data
.pwqp_more
;
273 isl_pw_qpolynomial_free(pwqp
);
278 static __isl_give isl_pw_qpolynomial_fold
*optimize(
279 __isl_take isl_pw_qpolynomial
*pwqp
, enum isl_fold type
,
280 struct options
*options
)
282 isl_pw_qpolynomial_fold
*pwf
;
284 if (options
->iterate
> 0) {
285 isl_pw_qpolynomial
*pwqp_less
, *pwqp_more
;
286 isl_pw_qpolynomial_fold
*pwf_less
, *pwf_more
;
287 split_on_domain_size(pwqp
, &pwqp_less
, &pwqp_more
, options
->iterate
);
288 pwf_less
= iterate(pwqp_less
, type
);
289 pwf_more
= isl_pw_qpolynomial_bound(pwqp_more
, type
, NULL
);
290 pwf
= isl_pw_qpolynomial_fold_fold(pwf_less
, pwf_more
);
291 } else if (options
->iterate
)
292 pwf
= iterate(pwqp
, type
);
294 pwf
= isl_pw_qpolynomial_bound(pwqp
, type
, NULL
);
298 static int optimize_and_print(__isl_take isl_pw_qpolynomial
*pwqp
,
299 struct options
*options
)
301 int print_solution
= 1;
303 isl_pw_qpolynomial_fold
*pwf
;
304 enum isl_fold type
= options
->lower
? isl_fold_min
: isl_fold_max
;
306 if (options
->verify
->verify
) {
307 isl_space
*dim
= isl_pw_qpolynomial_get_space(pwqp
);
308 unsigned total
= isl_space_dim(dim
, isl_dim_all
);
310 verify_options_set_range(options
->verify
, total
);
311 if (!options
->verify
->barvinok
->verbose
)
315 pwf
= optimize(isl_pw_qpolynomial_copy(pwqp
), type
, options
);
317 if (print_solution
) {
318 isl_ctx
*ctx
= isl_pw_qpolynomial_get_ctx(pwqp
);
319 isl_printer
*p
= isl_printer_to_file(ctx
, stdout
);
320 p
= isl_printer_print_pw_qpolynomial_fold(p
, pwf
);
321 p
= isl_printer_end_line(p
);
324 if (options
->verify
->verify
) {
325 enum isl_fold type
= options
->lower
? isl_fold_min
: isl_fold_max
;
326 result
= verify(pwf
, pwqp
, type
, options
->verify
);
328 isl_pw_qpolynomial_free(pwqp
);
329 isl_pw_qpolynomial_fold_free(pwf
);
334 int main(int argc
, char **argv
)
336 struct options
*options
= options_new_with_defaults();
338 isl_pw_qpolynomial
*pwqp
;
339 struct isl_stream
*s
;
342 argc
= options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
343 ctx
= isl_ctx_alloc_with_options(&options_args
, options
);
345 s
= isl_stream_new_file(ctx
, stdin
);
346 pwqp
= isl_stream_read_pw_qpolynomial(s
);
349 pwqp
= isl_pw_qpolynomial_split_periods(pwqp
, options
->split
);
351 result
= optimize_and_print(pwqp
, options
);