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 { "verbose", 'v', 0, 0, },
32 { "minimize", OPT_MIN
, 0, 0, "minimize instead of maximize"},
37 struct convert_options convert
;
38 struct verify_options verify
;
45 static error_t
parse_opt(int key
, char *arg
, struct argp_state
*state
)
47 struct options
*options
= (struct options
*) state
->input
;
51 state
->child_inputs
[0] = &options
->convert
;
52 state
->child_inputs
[1] = &options
->verify
;
53 state
->child_inputs
[2] = options
->verify
.barvinok
;
54 options
->var_list
= NULL
;
57 options
->minimize
= 0;
63 options
->var_list
= strdup(arg
);
66 options
->split
= atoi(arg
);
69 options
->minimize
= 1;
72 return ARGP_ERR_UNKNOWN
;
77 static int check_poly_max(const struct check_poly_data
*data
,
79 const struct verify_options
*options
);
81 struct check_poly_max_data
: public check_poly_data
{
86 check_poly_max_data(Value
*z
, evalue
*EP
, piecewise_lst
*pl
) :
89 this->check
= check_poly_max
;
93 static void optimum(Polyhedron
*S
, int pos
, const check_poly_max_data
*data
,
94 Value
*opt
, bool& found
,
95 const struct verify_options
*options
)
100 value_set_double(c
, compute_evalue(data
->EP
, data
->z
+1)+.25);
102 value_assign(*opt
, c
);
105 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
) {
106 if (value_gt(c
, *opt
))
107 value_assign(*opt
, c
);
109 if (value_lt(c
, *opt
))
110 value_assign(*opt
, c
);
119 ok
= !(lower_upper_bounds(1+pos
, S
, data
->z
, &LB
, &UB
));
121 for (; value_le(LB
, UB
); value_increment(LB
, LB
)) {
122 value_assign(data
->z
[1+pos
], LB
);
123 optimum(S
->next
, pos
+1, data
, opt
, found
, options
);
125 value_set_si(data
->z
[1+pos
], 0);
131 static void optimum(const check_poly_max_data
*data
, Value
*opt
,
132 const struct verify_options
*options
)
135 for (int i
= 0; i
< data
->EP
->x
.p
->size
/2; ++i
)
136 if (!emptyQ2(data
->S
[i
]))
137 optimum(data
->S
[i
], 0, data
, opt
, found
, options
);
141 static int check_poly_max(const struct check_poly_data
*data
,
142 int nparam
, Value
*z
,
143 const struct verify_options
*options
)
147 const check_poly_max_data
*max_data
;
148 max_data
= static_cast<const check_poly_max_data
*>(data
);
155 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
160 max_data
->pl
->evaluate(nparam
, z
, &n
, &d
);
161 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
166 if (options
->print_all
) {
167 printf("%s(", minmax
);
168 value_print(stdout
, VALUE_FMT
, z
[0]);
169 for (k
= 1; k
< nparam
; ++k
) {
171 value_print(stdout
, VALUE_FMT
, z
[k
]);
174 value_print(stdout
, VALUE_FMT
, n
);
175 if (value_notone_p(d
)) {
177 value_print(stdout
, VALUE_FMT
, d
);
180 value_print(stdout
, VALUE_FMT
, m
);
184 optimum(max_data
, &n
, options
);
186 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
191 if (options
->print_all
) {
192 printf(", %s(EP) = ", minmax
);
193 value_print(stdout
, VALUE_FMT
, n
);
200 fprintf(stderr
, "Error !\n");
201 fprintf(stderr
, "%s(", minmax
);
202 value_print(stderr
, VALUE_FMT
, z
[0]);
203 for (k
= 1; k
< nparam
; ++k
) {
204 fprintf(stderr
,", ");
205 value_print(stderr
, VALUE_FMT
, z
[k
]);
207 fprintf(stderr
, ") should be ");
208 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
209 fprintf(stderr
, "greater");
211 fprintf(stderr
, "smaller");
212 fprintf(stderr
, " than or equal to ");
213 value_print(stderr
, VALUE_FMT
, n
);
214 fprintf(stderr
, ", while pl eval gives ");
215 value_print(stderr
, VALUE_FMT
, m
);
216 fprintf(stderr
, ".\n");
217 cerr
<< *max_data
->pl
<< endl
;
218 } else if (options
->print_all
)
228 static int verify(Polyhedron
*D
, piecewise_lst
*pl
, evalue
*EP
,
229 unsigned nvar
, unsigned nparam
, Vector
*p
,
230 struct verify_options
*options
)
233 unsigned MaxRays
= options
->barvinok
->MaxRays
;
234 assert(value_zero_p(EP
->d
));
235 assert(EP
->x
.p
->type
== partition
);
238 CS
= check_poly_context_scan(NULL
, &D
, D
->Dimension
, options
);
240 check_poly_init(D
, options
);
242 if (!(CS
&& emptyQ2(CS
))) {
243 check_poly_max_data
data(p
->p
, EP
, pl
);
244 data
.S
= ALLOCN(Polyhedron
*, EP
->x
.p
->size
/2);
245 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
246 Polyhedron
*A
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
247 data
.S
[i
] = Polyhedron_Scan(A
, D
, MaxRays
& POL_NO_DUAL
? 0 : MaxRays
);
249 ok
= check_poly(CS
, &data
, nparam
, 0, p
->p
+1+nvar
, options
);
250 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
)
251 Domain_Free(data
.S
[i
]);
255 if (!options
->print_all
)
266 static int verify(piecewise_lst
*pl
, evalue
*EP
, unsigned nvar
, unsigned nparam
,
267 struct verify_options
*options
)
271 p
= Vector_Alloc(nvar
+nparam
+2);
272 value_set_si(p
->p
[nvar
+nparam
+1], 1);
274 for (int i
= 0; i
< pl
->list
.size(); ++i
) {
275 int ok
= verify(pl
->list
[i
].first
, pl
, EP
, nvar
, nparam
, p
, options
);
276 if (!ok
&& !options
->continue_on_error
)
285 static int optimize(evalue
*EP
, char **all_vars
, unsigned nvar
, unsigned nparam
,
286 struct options
*options
)
289 piecewise_lst
*pl
= NULL
;
290 U
= Universe_Polyhedron(nparam
);
291 int print_solution
= 1;
295 params
= constructParameterVector(all_vars
+nvar
, nparam
);
297 if (options
->verify
.verify
) {
298 verify_options_set_range(&options
->verify
, nvar
+nparam
);
299 if (!options
->verbose
)
303 if (options
->minimize
)
304 options
->verify
.barvinok
->bernstein_optimize
= BV_BERNSTEIN_MIN
;
306 options
->verify
.barvinok
->bernstein_optimize
= BV_BERNSTEIN_MAX
;
307 pl
= evalue_bernstein_coefficients(NULL
, EP
, U
, params
,
308 options
->verify
.barvinok
);
310 if (options
->minimize
)
316 if (options
->verify
.verify
)
317 result
= verify(pl
, EP
, nvar
, nparam
, &options
->verify
);
325 int main(int argc
, char **argv
)
328 char **all_vars
= NULL
;
331 struct options options
;
332 struct barvinok_options
*bv_options
= barvinok_options_new_with_defaults();
333 static struct argp_child argp_children
[] = {
334 { &convert_argp
, 0, "input conversion", 1 },
335 { &verify_argp
, 0, "verification", 2 },
336 { &barvinok_argp
, 0, "barvinok options", 3 },
339 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
342 options
.verify
.barvinok
= bv_options
;
343 set_program_name(argv
[0]);
344 argp_parse(&argp
, argc
, argv
, 0, 0, &options
);
346 EP
= evalue_read_from_file(stdin
, options
.var_list
, &all_vars
,
347 &nvar
, &nparam
, bv_options
->MaxRays
);
351 evalue_split_periods(EP
, options
.split
, bv_options
->MaxRays
);
353 evalue_convert(EP
, &options
.convert
, options
.verbose
, nparam
, all_vars
);
355 if (EVALUE_IS_ZERO(*EP
))
356 print_evalue(stdout
, EP
, all_vars
);
358 result
= optimize(EP
, all_vars
, nvar
, nparam
, &options
);
360 free_evalue_refs(EP
);
363 if (options
.var_list
)
364 free(options
.var_list
);
365 Free_ParamNames(all_vars
, nvar
+nparam
);
366 barvinok_options_free(bv_options
);