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
{
80 check_poly_max_data(Value
*z
, evalue
*EP
, piecewise_lst
*pl
) :
83 this->check
= check_poly_max
;
87 static void optimum(Polyhedron
*S
, int pos
, const check_poly_max_data
*data
,
88 Value
*opt
, bool& found
,
89 const struct verify_options
*options
)
94 value_set_double(c
, compute_evalue(data
->EP
, data
->z
+1)+.25);
96 value_assign(*opt
, c
);
99 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
) {
100 if (value_gt(c
, *opt
))
101 value_assign(*opt
, c
);
103 if (value_lt(c
, *opt
))
104 value_assign(*opt
, c
);
113 ok
= !(lower_upper_bounds(1+pos
, S
, data
->z
, &LB
, &UB
));
115 for (; value_le(LB
, UB
); value_increment(LB
, LB
)) {
116 value_assign(data
->z
[1+pos
], LB
);
117 optimum(S
->next
, pos
+1, data
, opt
, found
, options
);
119 value_set_si(data
->z
[1+pos
], 0);
125 static void optimum(const check_poly_max_data
*data
, Value
*opt
,
126 const struct verify_options
*options
)
129 for (int i
= 0; i
< data
->EP
->x
.p
->size
/2; ++i
)
130 if (!emptyQ2(data
->S
[i
]))
131 optimum(data
->S
[i
], 0, data
, opt
, found
, options
);
135 static int check_poly_max(const struct check_poly_data
*data
,
136 int nparam
, Value
*z
,
137 const struct verify_options
*options
)
141 const check_poly_max_data
*max_data
;
142 max_data
= static_cast<const check_poly_max_data
*>(data
);
149 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
154 max_data
->pl
->evaluate(nparam
, z
, &n
, &d
);
155 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
160 if (options
->print_all
) {
161 printf("%s(", minmax
);
162 value_print(stdout
, VALUE_FMT
, z
[0]);
163 for (k
= 1; k
< nparam
; ++k
) {
165 value_print(stdout
, VALUE_FMT
, z
[k
]);
168 value_print(stdout
, VALUE_FMT
, n
);
169 if (value_notone_p(d
)) {
171 value_print(stdout
, VALUE_FMT
, d
);
174 value_print(stdout
, VALUE_FMT
, m
);
178 optimum(max_data
, &n
, options
);
180 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
185 if (options
->print_all
) {
186 printf(", %s(EP) = ", minmax
);
187 value_print(stdout
, VALUE_FMT
, n
);
194 fprintf(stderr
, "Error !\n");
195 fprintf(stderr
, "%s(", minmax
);
196 value_print(stderr
, VALUE_FMT
, z
[0]);
197 for (k
= 1; k
< nparam
; ++k
) {
198 fprintf(stderr
,", ");
199 value_print(stderr
, VALUE_FMT
, z
[k
]);
201 fprintf(stderr
, ") should be ");
202 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
203 fprintf(stderr
, "greater");
205 fprintf(stderr
, "smaller");
206 fprintf(stderr
, " than or equal to ");
207 value_print(stderr
, VALUE_FMT
, n
);
208 fprintf(stderr
, ", while pl eval gives ");
209 value_print(stderr
, VALUE_FMT
, m
);
210 fprintf(stderr
, ".\n");
211 cerr
<< *max_data
->pl
<< endl
;
212 } else if (options
->print_all
)
222 static int verify(Polyhedron
*D
, piecewise_lst
*pl
, evalue
*EP
,
223 unsigned nvar
, unsigned nparam
, Vector
*p
,
224 struct verify_options
*options
)
227 unsigned MaxRays
= options
->barvinok
->MaxRays
;
228 assert(value_zero_p(EP
->d
));
229 assert(EP
->x
.p
->type
== partition
);
232 CS
= check_poly_context_scan(NULL
, &D
, D
->Dimension
, options
);
234 check_poly_init(D
, options
);
236 if (!(CS
&& emptyQ2(CS
))) {
237 check_poly_max_data
data(p
->p
, EP
, pl
);
238 data
.S
= ALLOCN(Polyhedron
*, EP
->x
.p
->size
/2);
239 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
240 Polyhedron
*A
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
241 data
.S
[i
] = Polyhedron_Scan(A
, D
, MaxRays
& POL_NO_DUAL
? 0 : MaxRays
);
243 ok
= check_poly(CS
, &data
, nparam
, 0, p
->p
+1+nvar
, options
);
244 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
)
245 Domain_Free(data
.S
[i
]);
249 if (!options
->print_all
)
260 static int verify(piecewise_lst
*pl
, evalue
*EP
, unsigned nvar
, unsigned nparam
,
261 struct verify_options
*options
)
265 p
= Vector_Alloc(nvar
+nparam
+2);
266 value_set_si(p
->p
[nvar
+nparam
+1], 1);
268 for (int i
= 0; i
< pl
->list
.size(); ++i
) {
269 int ok
= verify(pl
->list
[i
].first
, pl
, EP
, nvar
, nparam
, p
, options
);
270 if (!ok
&& !options
->continue_on_error
)
279 static int optimize(evalue
*EP
, char **all_vars
, unsigned nvar
, unsigned nparam
,
280 struct options
*options
)
283 piecewise_lst
*pl
= NULL
;
284 U
= Universe_Polyhedron(nparam
);
285 int print_solution
= 1;
289 params
= constructParameterVector(all_vars
+nvar
, nparam
);
291 if (options
->verify
.verify
) {
292 verify_options_set_range(&options
->verify
, nvar
+nparam
);
293 if (!options
->verify
.barvinok
->verbose
)
297 if (options
->minimize
)
298 options
->verify
.barvinok
->bernstein_optimize
= BV_BERNSTEIN_MIN
;
300 options
->verify
.barvinok
->bernstein_optimize
= BV_BERNSTEIN_MAX
;
301 pl
= evalue_bernstein_coefficients(NULL
, EP
, U
, params
,
302 options
->verify
.barvinok
);
304 if (options
->minimize
)
310 if (options
->verify
.verify
)
311 result
= verify(pl
, EP
, nvar
, nparam
, &options
->verify
);
319 int main(int argc
, char **argv
)
322 char **all_vars
= NULL
;
325 struct options options
;
326 struct barvinok_options
*bv_options
= barvinok_options_new_with_defaults();
327 static struct argp_child argp_children
[] = {
328 { &convert_argp
, 0, "input conversion", 1 },
329 { &verify_argp
, 0, "verification", 2 },
330 { &barvinok_argp
, 0, "barvinok options", 3 },
333 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
336 options
.verify
.barvinok
= bv_options
;
337 set_program_name(argv
[0]);
338 argp_parse(&argp
, argc
, argv
, 0, 0, &options
);
340 EP
= evalue_read_from_file(stdin
, options
.var_list
, &all_vars
,
341 &nvar
, &nparam
, bv_options
->MaxRays
);
345 evalue_split_periods(EP
, options
.split
, bv_options
->MaxRays
);
347 evalue_convert(EP
, &options
.convert
, bv_options
->verbose
, nparam
, all_vars
);
349 if (EVALUE_IS_ZERO(*EP
))
350 print_evalue(stdout
, EP
, all_vars
);
352 result
= optimize(EP
, all_vars
, nvar
, nparam
, &options
);
356 if (options
.var_list
)
357 free(options
.var_list
);
358 Free_ParamNames(all_vars
, nvar
+nparam
);
359 barvinok_options_free(bv_options
);