3 #include <barvinok/evalue.h>
4 #include <barvinok/options.h>
5 #include <barvinok/util.h>
6 #include <barvinok/barvinok.h>
7 #include "bound_options.h"
8 #include "evalue_convert.h"
9 #include "evalue_read.h"
16 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
18 struct verify_point_bound
{
19 struct verify_point_data vpd
;
20 isl_pw_qpolynomial
*pwqp
;
21 isl_pw_qpolynomial_fold
*pwf
;
25 static int verify_point(__isl_take isl_point
*pnt
, void *user
)
29 struct verify_point_bound
*vpb
= (struct verify_point_bound
*) user
;
30 isl_int v
, n
, d
, b
, t
;
31 isl_pw_qpolynomial
*pwqp
;
32 isl_qpolynomial
*bound
;
38 FILE *out
= vpb
->vpd
.options
->print_all
? stdout
: stderr
;
42 if (vpb
->type
== isl_fold_max
) {
56 pwqp
= isl_pw_qpolynomial_copy(vpb
->pwqp
);
58 nparam
= isl_pw_qpolynomial_dim(pwqp
, isl_dim_param
);
59 for (i
= 0; i
< nparam
; ++i
) {
60 isl_point_get_coordinate(pnt
, isl_dim_param
, i
, &v
);
61 pwqp
= isl_pw_qpolynomial_fix_dim(pwqp
, isl_dim_param
, i
, v
);
64 bound
= isl_pw_qpolynomial_fold_eval(isl_pw_qpolynomial_fold_copy(vpb
->pwf
),
68 opt
= isl_pw_qpolynomial_max(pwqp
);
70 opt
= isl_pw_qpolynomial_min(pwqp
);
72 cst
= isl_qpolynomial_is_cst(opt
, &n
, &d
);
76 isl_int_fdiv_q(v
, n
, d
);
78 isl_int_cdiv_q(v
, n
, d
);
80 cst
= isl_qpolynomial_is_cst(bound
, &n
, &d
);
84 isl_int_fdiv_q(b
, n
, d
);
86 isl_int_cdiv_q(b
, n
, d
);
93 if (vpb
->vpd
.options
->print_all
|| !ok
) {
94 fprintf(out
, "%s(", minmax
);
95 for (i
= 0; i
< nparam
; ++i
) {
98 isl_point_get_coordinate(pnt
, isl_dim_param
, i
, &t
);
99 isl_int_print(out
, t
, 0);
101 fprintf(out
, ") = ");
102 isl_int_print(out
, n
, 0);
103 if (!isl_int_is_one(d
)) {
105 isl_int_print(out
, d
, 0);
107 isl_int_print(out
, b
, 0);
110 fprintf(out
, ", %s(EP) = ", minmax
);
111 isl_int_print(out
, v
, 0);
113 fprintf(out
, ". OK\n");
115 fprintf(out
, ". NOT OK\n");
116 } else if ((vpb
->vpd
.n
% vpb
->vpd
.s
) == 0) {
126 isl_qpolynomial_free(bound
);
127 isl_qpolynomial_free(opt
);
139 if (vpb
->vpd
.options
->continue_on_error
)
142 return (vpb
->vpd
.n
>= 1 && ok
) ? 0 : -1;
145 static int verify(__isl_keep isl_pw_qpolynomial_fold
*pwf
, evalue
*EP
, unsigned nvar
,
146 enum isl_fold type
, struct verify_options
*options
)
148 struct verify_point_bound vpb
= { { options
} };
155 ctx
= isl_pw_qpolynomial_fold_get_ctx(pwf
);
156 nparam
= isl_pw_qpolynomial_fold_dim(pwf
, isl_dim_param
);
158 dim
= isl_dim_set_alloc(ctx
, nvar
+ nparam
, 0);
160 vpb
.pwqp
= isl_pw_qpolynomial_from_evalue(dim
, EP
);
161 vpb
.pwqp
= isl_pw_qpolynomial_move_dims(vpb
.pwqp
, isl_dim_set
, 0,
162 isl_dim_param
, 0, nvar
);
163 context
= isl_pw_qpolynomial_fold_domain(
164 isl_pw_qpolynomial_fold_copy(vpb
.pwf
));
165 context
= verify_context_set_bounds(context
, options
);
167 r
= verify_point_data_init(&vpb
.vpd
, context
);
170 isl_set_foreach_point(context
, verify_point
, &vpb
);
174 isl_set_free(context
);
175 isl_pw_qpolynomial_free(vpb
.pwqp
);
177 verify_point_data_fini(&vpb
.vpd
);
182 static __isl_give isl_pw_qpolynomial_fold
*iterate(
183 __isl_take isl_pw_qpolynomial
*pwqp
, enum isl_fold type
)
185 isl_dim
*dim
= isl_pw_qpolynomial_get_dim(pwqp
);
188 isl_qpolynomial_fold
*fold
;
191 assert(isl_dim_size(dim
, isl_dim_param
) == 0);
192 nvar
= isl_dim_size(dim
, isl_dim_set
);
194 if (type
== isl_fold_min
)
195 qp
= isl_pw_qpolynomial_min(pwqp
);
197 qp
= isl_pw_qpolynomial_max(pwqp
);
199 qp
= isl_qpolynomial_drop_dims(qp
, isl_dim_set
, 0, nvar
);
200 fold
= isl_qpolynomial_fold_alloc(type
, qp
);
201 dim
= isl_dim_drop(dim
, isl_dim_set
, 0, nvar
);
202 set
= isl_set_universe(dim
);
204 return isl_pw_qpolynomial_fold_alloc(set
, fold
);
208 * Split (partition) EP into a partition with (sub)domains containing
209 * size integer points or less and a partition with (sub)domains
210 * containing more integer points.
212 static void split_on_domain_size(evalue
*EP
, evalue
**EP_less
, evalue
**EP_more
,
213 int size
, barvinok_options
*options
)
215 assert(value_zero_p(EP
->d
));
216 assert(EP
->x
.p
->type
== partition
);
217 assert(EP
->x
.p
->size
>= 2);
219 struct evalue_section
*s_less
= new evalue_section
[EP
->x
.p
->size
/2];
220 struct evalue_section
*s_more
= new evalue_section
[EP
->x
.p
->size
/2];
228 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
229 Polyhedron
*D
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
230 Polyhedron
*D_less
= NULL
;
231 Polyhedron
*D_more
= NULL
;
232 Polyhedron
**next_less
= &D_less
;
233 Polyhedron
**next_more
= &D_more
;
235 for (Polyhedron
*P
= D
; P
; P
= P
->next
) {
236 Polyhedron
*next
= P
->next
;
238 barvinok_count_with_options(P
, &c
, options
);
244 if (value_pos_p(c
) && value_cmp_si(c
, size
) <= 0) {
245 *next_less
= Polyhedron_Copy(P
);
246 next_less
= &(*next_less
)->next
;
248 *next_more
= Polyhedron_Copy(P
);
249 next_more
= &(*next_more
)->next
;
254 s_less
[n_less
].D
= D_less
;
255 s_less
[n_less
].E
= evalue_dup(&EP
->x
.p
->arr
[2*i
+1]);
258 s_more
[n_more
].D
= D_more
;
259 s_more
[n_more
].E
= evalue_dup(&EP
->x
.p
->arr
[2*i
+1]);
266 *EP_less
= evalue_from_section_array(s_less
, n_less
);
267 *EP_more
= evalue_from_section_array(s_more
, n_more
);
273 static __isl_give isl_pw_qpolynomial_fold
*optimize(evalue
*EP
, unsigned nvar
,
274 Polyhedron
*C
, __isl_take isl_dim
*dim
,
275 struct options
*options
)
277 isl_pw_qpolynomial_fold
*pwf
;
278 if (options
->iterate
> 0) {
279 evalue
*EP_less
= NULL
;
280 evalue
*EP_more
= NULL
;
281 isl_pw_qpolynomial_fold
*pwf
= NULL
, *pwf_more
= NULL
;
283 split_on_domain_size(EP
, &EP_less
, &EP_more
, options
->iterate
,
284 options
->verify
->barvinok
);
285 if (!EVALUE_IS_ZERO(*EP_less
)) {
286 options
->iterate
= -1;
287 pwf
= optimize(EP_less
, nvar
, C
, isl_dim_copy(dim
), options
);
289 if (!EVALUE_IS_ZERO(*EP_more
)) {
290 options
->iterate
= 0;
291 pwf_more
= optimize(EP_more
, nvar
, C
, isl_dim_copy(dim
), options
);
294 evalue_free(EP_less
);
295 evalue_free(EP_more
);
300 return isl_pw_qpolynomial_fold_add(pwf
, pwf_more
);
303 isl_pw_qpolynomial
*pwqp
;
304 enum isl_fold type
= options
->lower
? isl_fold_min
: isl_fold_max
;
305 dim_EP
= isl_dim_insert(dim
, isl_dim_param
, 0, nvar
);
306 pwqp
= isl_pw_qpolynomial_from_evalue(dim_EP
, EP
);
307 pwqp
= isl_pw_qpolynomial_move_dims(pwqp
, isl_dim_set
, 0, isl_dim_param
, 0, nvar
);
308 if (options
->iterate
)
309 pwf
= iterate(pwqp
, type
);
311 pwf
= isl_pw_qpolynomial_bound(pwqp
, type
, NULL
);
315 static int optimize(evalue
*EP
, const char **all_vars
,
316 unsigned nvar
, unsigned nparam
, struct options
*options
)
319 U
= Universe_Polyhedron(nparam
);
320 int print_solution
= 1;
322 isl_ctx
*ctx
= isl_ctx_alloc_with_options(options_arg
, options
);
324 isl_pw_qpolynomial_fold
*pwf
;
326 dim
= isl_dim_set_alloc(ctx
, nparam
, 0);
327 for (int i
= 0; i
< nparam
; ++i
)
328 dim
= isl_dim_set_name(dim
, isl_dim_param
, i
, all_vars
[nvar
+ i
]);
330 if (options
->verify
->verify
) {
331 verify_options_set_range(options
->verify
, nvar
+nparam
);
332 if (!options
->verify
->barvinok
->verbose
)
336 pwf
= optimize(EP
, nvar
, U
, dim
, options
);
338 if (print_solution
) {
339 isl_printer
*p
= isl_printer_to_file(ctx
, stdout
);
340 p
= isl_printer_print_pw_qpolynomial_fold(p
, pwf
);
341 p
= isl_printer_end_line(p
);
344 if (options
->verify
->verify
) {
345 enum isl_fold type
= options
->lower
? isl_fold_min
: isl_fold_max
;
346 result
= verify(pwf
, EP
, nvar
, type
, options
->verify
);
348 isl_pw_qpolynomial_fold_free(pwf
);
357 int main(int argc
, char **argv
)
360 const char **all_vars
= NULL
;
363 struct options
*options
= options_new_with_defaults();
366 argc
= options_parse(options
, argc
, argv
, ISL_ARG_ALL
);
368 EP
= evalue_read_from_file(stdin
, options
->var_list
, &all_vars
,
369 &nvar
, &nparam
, options
->verify
->barvinok
->MaxRays
);
373 evalue_split_periods(EP
, options
->split
, options
->verify
->barvinok
->MaxRays
);
375 evalue_convert(EP
, options
->convert
, options
->verify
->barvinok
->verbose
,
376 nvar
+nparam
, all_vars
);
378 if (EVALUE_IS_ZERO(*EP
))
379 print_evalue(stdout
, EP
, all_vars
);
381 result
= optimize(EP
, all_vars
, nvar
, nparam
, options
);
385 Free_ParamNames(all_vars
, nvar
+nparam
);