3 #include <barvinok/evalue.h>
4 #include <barvinok/options.h>
5 #include <barvinok/util.h>
6 #include <barvinok/barvinok.h>
7 #include <barvinok/bernstein.h>
8 #include <bound_common.h>
9 #include "bound_options.h"
10 #include "evalue_convert.h"
11 #include "evalue_read.h"
17 using namespace barvinok
;
19 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
21 struct verify_point_bound
{
22 struct verify_point_data vpd
;
23 isl_pw_qpolynomial
*pwqp
;
24 isl_pw_qpolynomial_fold
*pwf
;
27 static int verify_point(__isl_take isl_point
*pnt
, void *user
)
31 struct verify_point_bound
*vpb
= (struct verify_point_bound
*) user
;
32 isl_int v
, n
, d
, b
, t
;
33 isl_pw_qpolynomial
*pwqp
;
34 isl_qpolynomial
*bound
;
40 FILE *out
= vpb
->vpd
.options
->print_all
? stdout
: stderr
;
44 if (vpb
->vpd
.options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
) {
58 pwqp
= isl_pw_qpolynomial_copy(vpb
->pwqp
);
60 nparam
= isl_pw_qpolynomial_dim(pwqp
, isl_dim_param
);
61 for (i
= 0; i
< nparam
; ++i
) {
62 isl_point_get_coordinate(pnt
, isl_dim_param
, i
, &v
);
63 pwqp
= isl_pw_qpolynomial_fix_dim(pwqp
, isl_dim_param
, i
, v
);
66 bound
= isl_pw_qpolynomial_fold_eval(isl_pw_qpolynomial_fold_copy(vpb
->pwf
),
70 opt
= isl_pw_qpolynomial_max(pwqp
);
72 opt
= isl_pw_qpolynomial_min(pwqp
);
74 cst
= isl_qpolynomial_is_cst(opt
, &n
, &d
);
78 isl_int_fdiv_q(v
, n
, d
);
80 isl_int_cdiv_q(v
, n
, d
);
82 cst
= isl_qpolynomial_is_cst(bound
, &n
, &d
);
86 isl_int_fdiv_q(b
, n
, d
);
88 isl_int_cdiv_q(b
, n
, d
);
95 if (vpb
->vpd
.options
->print_all
|| !ok
) {
96 fprintf(out
, "%s(", minmax
);
97 for (i
= 0; i
< nparam
; ++i
) {
100 isl_point_get_coordinate(pnt
, isl_dim_param
, i
, &t
);
101 isl_int_print(out
, t
, 0);
103 fprintf(out
, ") = ");
104 isl_int_print(out
, n
, 0);
105 if (!isl_int_is_one(d
)) {
107 isl_int_print(out
, d
, 0);
109 isl_int_print(out
, b
, 0);
112 fprintf(out
, ", %s(EP) = ", minmax
);
113 isl_int_print(out
, v
, 0);
115 fprintf(out
, ". OK\n");
117 fprintf(out
, ". NOT OK\n");
118 } else if ((vpb
->vpd
.n
% vpb
->vpd
.s
) == 0) {
128 isl_qpolynomial_free(bound
);
129 isl_qpolynomial_free(opt
);
141 if (vpb
->vpd
.options
->continue_on_error
)
144 return (vpb
->vpd
.n
>= 1 && ok
) ? 0 : -1;
147 static int verify(__isl_keep isl_pw_qpolynomial_fold
*pwf
, evalue
*EP
, unsigned nvar
,
148 struct verify_options
*options
)
150 struct verify_point_bound vpb
= { { options
} };
157 ctx
= isl_pw_qpolynomial_fold_get_ctx(pwf
);
158 nparam
= isl_pw_qpolynomial_fold_dim(pwf
, isl_dim_param
);
160 dim
= isl_dim_set_alloc(ctx
, nvar
+ nparam
, 0);
161 vpb
.pwqp
= isl_pw_qpolynomial_from_evalue(dim
, EP
);
162 vpb
.pwqp
= isl_pw_qpolynomial_move_dims(vpb
.pwqp
, isl_dim_set
, 0,
163 isl_dim_param
, 0, nvar
);
164 context
= isl_pw_qpolynomial_fold_domain(
165 isl_pw_qpolynomial_fold_copy(vpb
.pwf
));
166 context
= verify_context_set_bounds(context
, options
);
168 r
= verify_point_data_init(&vpb
.vpd
, context
);
171 isl_set_foreach_point(context
, verify_point
, &vpb
);
175 isl_set_free(context
);
176 isl_pw_qpolynomial_free(vpb
.pwqp
);
178 verify_point_data_fini(&vpb
.vpd
);
183 static __isl_give isl_pw_qpolynomial_fold
*iterate(
184 __isl_take isl_pw_qpolynomial
*pwqp
, enum isl_fold type
)
186 isl_dim
*dim
= isl_pw_qpolynomial_get_dim(pwqp
);
189 isl_qpolynomial_fold
*fold
;
192 assert(isl_dim_size(dim
, isl_dim_param
) == 0);
193 nvar
= isl_dim_size(dim
, isl_dim_set
);
195 if (type
== isl_fold_min
)
196 qp
= isl_pw_qpolynomial_min(pwqp
);
198 qp
= isl_pw_qpolynomial_max(pwqp
);
200 qp
= isl_qpolynomial_drop_dims(qp
, isl_dim_set
, 0, nvar
);
201 fold
= isl_qpolynomial_fold_alloc(type
, qp
);
202 dim
= isl_dim_drop(dim
, isl_dim_set
, 0, nvar
);
203 set
= isl_set_universe(dim
);
205 return isl_pw_qpolynomial_fold_alloc(set
, fold
);
209 * Split (partition) EP into a partition with (sub)domains containing
210 * size integer points or less and a partition with (sub)domains
211 * containing more integer points.
213 static void split_on_domain_size(evalue
*EP
, evalue
**EP_less
, evalue
**EP_more
,
214 int size
, barvinok_options
*options
)
216 assert(value_zero_p(EP
->d
));
217 assert(EP
->x
.p
->type
== partition
);
218 assert(EP
->x
.p
->size
>= 2);
220 struct evalue_section
*s_less
= new evalue_section
[EP
->x
.p
->size
/2];
221 struct evalue_section
*s_more
= new evalue_section
[EP
->x
.p
->size
/2];
229 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
230 Polyhedron
*D
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
231 Polyhedron
*D_less
= NULL
;
232 Polyhedron
*D_more
= NULL
;
233 Polyhedron
**next_less
= &D_less
;
234 Polyhedron
**next_more
= &D_more
;
236 for (Polyhedron
*P
= D
; P
; P
= P
->next
) {
237 Polyhedron
*next
= P
->next
;
239 barvinok_count_with_options(P
, &c
, options
);
245 if (value_pos_p(c
) && value_cmp_si(c
, size
) <= 0) {
246 *next_less
= Polyhedron_Copy(P
);
247 next_less
= &(*next_less
)->next
;
249 *next_more
= Polyhedron_Copy(P
);
250 next_more
= &(*next_more
)->next
;
255 s_less
[n_less
].D
= D_less
;
256 s_less
[n_less
].E
= evalue_dup(&EP
->x
.p
->arr
[2*i
+1]);
259 s_more
[n_more
].D
= D_more
;
260 s_more
[n_more
].E
= evalue_dup(&EP
->x
.p
->arr
[2*i
+1]);
267 *EP_less
= evalue_from_section_array(s_less
, n_less
);
268 *EP_more
= evalue_from_section_array(s_more
, n_more
);
274 static __isl_give isl_pw_qpolynomial_fold
*optimize(evalue
*EP
, unsigned nvar
,
275 Polyhedron
*C
, __isl_take isl_dim
*dim
,
276 struct options
*options
)
278 isl_pw_qpolynomial_fold
*pwf
;
279 if (options
->iterate
> 0) {
280 evalue
*EP_less
= NULL
;
281 evalue
*EP_more
= NULL
;
282 isl_pw_qpolynomial_fold
*pwf
= NULL
, *pwf_more
= NULL
;
284 split_on_domain_size(EP
, &EP_less
, &EP_more
, options
->iterate
,
285 options
->verify
->barvinok
);
286 if (!EVALUE_IS_ZERO(*EP_less
)) {
287 options
->iterate
= -1;
288 pwf
= optimize(EP_less
, nvar
, C
, isl_dim_copy(dim
), options
);
290 if (!EVALUE_IS_ZERO(*EP_more
)) {
291 options
->iterate
= 0;
292 pwf_more
= optimize(EP_more
, nvar
, C
, isl_dim_copy(dim
), options
);
295 evalue_free(EP_less
);
296 evalue_free(EP_more
);
301 return isl_pw_qpolynomial_fold_add(pwf
, pwf_more
);
303 int method
= options
->verify
->barvinok
->bound
;
305 isl_pw_qpolynomial
*pwqp
;
306 enum isl_fold type
= options
->lower
? isl_fold_min
: isl_fold_max
;
307 dim_EP
= isl_dim_insert(dim
, isl_dim_param
, 0, nvar
);
308 pwqp
= isl_pw_qpolynomial_from_evalue(dim_EP
, EP
);
309 pwqp
= isl_pw_qpolynomial_move_dims(pwqp
, isl_dim_set
, 0, isl_dim_param
, 0, nvar
);
310 if (options
->iterate
)
311 pwf
= iterate(pwqp
, type
);
313 pwf
= isl_pw_qpolynomial_bound(pwqp
, type
, method
);
317 static int optimize(evalue
*EP
, const char **all_vars
,
318 unsigned nvar
, unsigned nparam
, struct options
*options
)
321 U
= Universe_Polyhedron(nparam
);
322 int print_solution
= 1;
324 isl_ctx
*ctx
= isl_ctx_alloc_with_options(options_arg
, options
);
326 isl_pw_qpolynomial_fold
*pwf
;
328 dim
= isl_dim_set_alloc(ctx
, nparam
, 0);
329 for (int i
= 0; i
< nparam
; ++i
)
330 dim
= isl_dim_set_name(dim
, isl_dim_param
, i
, all_vars
[nvar
+ i
]);
332 if (options
->verify
->verify
) {
333 verify_options_set_range(options
->verify
, nvar
+nparam
);
334 if (!options
->verify
->barvinok
->verbose
)
339 options
->verify
->barvinok
->bernstein_optimize
= BV_BERNSTEIN_MIN
;
341 options
->verify
->barvinok
->bernstein_optimize
= BV_BERNSTEIN_MAX
;
342 pwf
= optimize(EP
, nvar
, U
, dim
, options
);
344 if (print_solution
) {
345 isl_printer
*p
= isl_printer_to_file(ctx
, stdout
);
346 p
= isl_printer_print_pw_qpolynomial_fold(p
, pwf
);
347 p
= isl_printer_end_line(p
);
350 if (options
->verify
->verify
) {
351 result
= verify(pwf
, EP
, nvar
, options
->verify
);
353 isl_pw_qpolynomial_fold_free(pwf
);
362 int main(int argc
, char **argv
)
365 const char **all_vars
= NULL
;
368 struct options
*options
= options_new_with_defaults();
371 argc
= options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
373 EP
= evalue_read_from_file(stdin
, options
->var_list
, &all_vars
,
374 &nvar
, &nparam
, options
->verify
->barvinok
->MaxRays
);
378 evalue_split_periods(EP
, options
->split
, options
->verify
->barvinok
->MaxRays
);
380 evalue_convert(EP
, options
->convert
, options
->verify
->barvinok
->verbose
,
381 nvar
+nparam
, all_vars
);
383 if (EVALUE_IS_ZERO(*EP
))
384 print_evalue(stdout
, EP
, all_vars
);
386 result
= optimize(EP
, all_vars
, nvar
, nparam
, options
);
390 Free_ParamNames(all_vars
, nvar
+nparam
);