3 #include <bernstein/bernstein.h>
4 #include <barvinok/evalue.h>
5 #include <barvinok/options.h>
6 #include <barvinok/util.h>
7 #include <barvinok/bernstein.h>
10 #include "evalue_convert.h"
11 #include "evalue_read.h"
17 using namespace GiNaC
;
18 using namespace bernstein
;
19 using namespace barvinok
;
21 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
23 #define OPT_VARS (BV_OPT_LAST+1)
24 #define OPT_SPLIT (BV_OPT_LAST+2)
25 #define OPT_MIN (BV_OPT_LAST+3)
27 struct argp_option argp_options
[] = {
28 { "split", OPT_SPLIT
, "int" },
29 { "variables", OPT_VARS
, "list", 0,
30 "comma separated list of variables over which to maximize" },
31 { "minimize", OPT_MIN
, 0, 0, "minimize instead of maximize"},
36 struct convert_options convert
;
37 struct verify_options verify
;
43 static error_t
parse_opt(int key
, char *arg
, struct argp_state
*state
)
45 struct options
*options
= (struct options
*) state
->input
;
49 state
->child_inputs
[0] = &options
->convert
;
50 state
->child_inputs
[1] = &options
->verify
;
51 state
->child_inputs
[2] = options
->verify
.barvinok
;
52 options
->var_list
= NULL
;
54 options
->minimize
= 0;
57 options
->var_list
= strdup(arg
);
60 options
->split
= atoi(arg
);
63 options
->minimize
= 1;
66 return ARGP_ERR_UNKNOWN
;
71 static int check_poly_max(const struct check_poly_data
*data
,
73 const struct verify_options
*options
);
75 struct check_poly_max_data
: public check_poly_data
{
81 check_poly_max_data(Value
*z
, evalue
*EP
, piecewise_lst
*pl
) :
84 this->check
= check_poly_max
;
88 static void optimum(Polyhedron
*S
, int pos
, const check_poly_max_data
*data
,
89 Value
*opt
, bool& found
,
90 const struct verify_options
*options
)
95 value_set_double(c
, compute_evalue(data
->EP
, data
->z
+1)+.25);
97 value_assign(*opt
, c
);
100 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
) {
101 if (value_gt(c
, *opt
))
102 value_assign(*opt
, c
);
104 if (value_lt(c
, *opt
))
105 value_assign(*opt
, c
);
114 ok
= !(lower_upper_bounds(1+pos
, S
, data
->z
, &LB
, &UB
));
116 for (; value_le(LB
, UB
); value_increment(LB
, LB
)) {
117 value_assign(data
->z
[1+pos
], LB
);
118 optimum(S
->next
, pos
+1, data
, opt
, found
, options
);
120 value_set_si(data
->z
[1+pos
], 0);
126 static void optimum(const check_poly_max_data
*data
, Value
*opt
,
127 const struct verify_options
*options
)
130 for (int i
= 0; i
< data
->n_S
; ++i
)
131 if (!emptyQ2(data
->S
[i
]))
132 optimum(data
->S
[i
], 0, data
, opt
, found
, options
);
136 static int check_poly_max(const struct check_poly_data
*data
,
137 int nparam
, Value
*z
,
138 const struct verify_options
*options
)
142 const check_poly_max_data
*max_data
;
143 max_data
= static_cast<const check_poly_max_data
*>(data
);
150 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
155 max_data
->pl
->evaluate(nparam
, z
, &n
, &d
);
156 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
161 if (options
->print_all
) {
162 printf("%s(", minmax
);
163 value_print(stdout
, VALUE_FMT
, z
[0]);
164 for (k
= 1; k
< nparam
; ++k
) {
166 value_print(stdout
, VALUE_FMT
, z
[k
]);
169 value_print(stdout
, VALUE_FMT
, n
);
170 if (value_notone_p(d
)) {
172 value_print(stdout
, VALUE_FMT
, d
);
175 value_print(stdout
, VALUE_FMT
, m
);
179 optimum(max_data
, &n
, options
);
181 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
186 if (options
->print_all
) {
187 printf(", %s(EP) = ", minmax
);
188 value_print(stdout
, VALUE_FMT
, n
);
195 fprintf(stderr
, "Error !\n");
196 fprintf(stderr
, "%s(", minmax
);
197 value_print(stderr
, VALUE_FMT
, z
[0]);
198 for (k
= 1; k
< nparam
; ++k
) {
199 fprintf(stderr
,", ");
200 value_print(stderr
, VALUE_FMT
, z
[k
]);
202 fprintf(stderr
, ") should be ");
203 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
204 fprintf(stderr
, "greater");
206 fprintf(stderr
, "smaller");
207 fprintf(stderr
, " than or equal to ");
208 value_print(stderr
, VALUE_FMT
, n
);
209 fprintf(stderr
, ", while pl eval gives ");
210 value_print(stderr
, VALUE_FMT
, m
);
211 fprintf(stderr
, ".\n");
212 cerr
<< *max_data
->pl
<< endl
;
213 } else if (options
->print_all
)
223 static int verify(Polyhedron
*D
, piecewise_lst
*pl
, evalue
*EP
,
224 unsigned nvar
, unsigned nparam
, Vector
*p
,
225 struct verify_options
*options
)
228 unsigned MaxRays
= options
->barvinok
->MaxRays
;
229 assert(value_zero_p(EP
->d
));
230 assert(EP
->x
.p
->type
== partition
);
233 CS
= check_poly_context_scan(NULL
, &D
, D
->Dimension
, options
);
235 check_poly_init(D
, options
);
237 if (!(CS
&& emptyQ2(CS
))) {
240 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
241 Polyhedron
*A
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
242 for (; A
; A
= A
->next
)
246 check_poly_max_data
data(p
->p
, EP
, pl
);
248 data
.S
= ALLOCN(Polyhedron
*, n_S
);
250 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
251 Polyhedron
*A
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
252 for (; A
; A
= A
->next
) {
253 Polyhedron
*next
= A
->next
;
255 data
.S
[n_S
++] = Polyhedron_Scan(A
, D
,
256 MaxRays
& POL_NO_DUAL
? 0 : MaxRays
);
260 ok
= check_poly(CS
, &data
, nparam
, 0, p
->p
+1+nvar
, options
);
261 for (int i
= 0; i
< data
.n_S
; ++i
)
262 Domain_Free(data
.S
[i
]);
266 if (!options
->print_all
)
277 static int verify(piecewise_lst
*pl
, evalue
*EP
, unsigned nvar
, unsigned nparam
,
278 struct verify_options
*options
)
282 p
= Vector_Alloc(nvar
+nparam
+2);
283 value_set_si(p
->p
[nvar
+nparam
+1], 1);
285 for (int i
= 0; i
< pl
->list
.size(); ++i
) {
286 int ok
= verify(pl
->list
[i
].first
, pl
, EP
, nvar
, nparam
, p
, options
);
287 if (!ok
&& !options
->continue_on_error
)
296 static int optimize(evalue
*EP
, char **all_vars
, unsigned nvar
, unsigned nparam
,
297 struct options
*options
)
300 piecewise_lst
*pl
= NULL
;
301 U
= Universe_Polyhedron(nparam
);
302 int print_solution
= 1;
306 params
= constructParameterVector(all_vars
+nvar
, nparam
);
308 if (options
->verify
.verify
) {
309 verify_options_set_range(&options
->verify
, nvar
+nparam
);
310 if (!options
->verify
.barvinok
->verbose
)
314 if (options
->minimize
)
315 options
->verify
.barvinok
->bernstein_optimize
= BV_BERNSTEIN_MIN
;
317 options
->verify
.barvinok
->bernstein_optimize
= BV_BERNSTEIN_MAX
;
318 pl
= evalue_bernstein_coefficients(NULL
, EP
, U
, params
,
319 options
->verify
.barvinok
);
321 if (options
->minimize
)
327 if (options
->verify
.verify
)
328 result
= verify(pl
, EP
, nvar
, nparam
, &options
->verify
);
336 int main(int argc
, char **argv
)
339 char **all_vars
= NULL
;
342 struct options options
;
343 struct barvinok_options
*bv_options
= barvinok_options_new_with_defaults();
344 static struct argp_child argp_children
[] = {
345 { &convert_argp
, 0, "input conversion", 1 },
346 { &verify_argp
, 0, "verification", 2 },
347 { &barvinok_argp
, 0, "barvinok options", 3 },
350 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
353 options
.verify
.barvinok
= bv_options
;
354 set_program_name(argv
[0]);
355 argp_parse(&argp
, argc
, argv
, 0, 0, &options
);
357 EP
= evalue_read_from_file(stdin
, options
.var_list
, &all_vars
,
358 &nvar
, &nparam
, bv_options
->MaxRays
);
362 evalue_split_periods(EP
, options
.split
, bv_options
->MaxRays
);
364 evalue_convert(EP
, &options
.convert
, bv_options
->verbose
, nparam
, all_vars
);
366 if (EVALUE_IS_ZERO(*EP
))
367 print_evalue(stdout
, EP
, all_vars
);
369 result
= optimize(EP
, all_vars
, nvar
, nparam
, &options
);
373 if (options
.var_list
)
374 free(options
.var_list
);
375 Free_ParamNames(all_vars
, nvar
+nparam
);
376 barvinok_options_free(bv_options
);