2 #include <bernstein/bernstein.h>
3 #include <barvinok/evalue.h>
4 #include <barvinok/options.h>
5 #include <barvinok/util.h>
6 #include <barvinok/bernstein.h>
9 #include "evalue_convert.h"
15 using namespace GiNaC
;
16 using namespace bernstein
;
17 using namespace barvinok
;
19 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
21 #define OPT_VARS (BV_OPT_LAST+1)
22 #define OPT_SPLIT (BV_OPT_LAST+2)
23 #define OPT_MIN (BV_OPT_LAST+3)
25 struct argp_option argp_options
[] = {
26 { "split", OPT_SPLIT
, "int" },
27 { "variables", OPT_VARS
, "list", 0,
28 "comma separated list of variables over which to maximize" },
29 { "verbose", 'v', 0, 0, },
30 { "minimize", OPT_MIN
, 0, 0, "minimize instead of maximize"},
35 struct convert_options convert
;
36 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
;
55 options
->minimize
= 0;
61 options
->var_list
= strdup(arg
);
64 options
->split
= atoi(arg
);
67 options
->minimize
= 1;
70 return ARGP_ERR_UNKNOWN
;
76 #define ALLOC(type) (type*)malloc(sizeof(type))
77 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
79 enum token_type
{ TOKEN_UNKNOWN
= 256, TOKEN_VALUE
, TOKEN_IDENT
, TOKEN_GE
,
80 TOKEN_NE
, TOKEN_UNION
, TOKEN_VARS
};
94 static struct token
*token_new(int line
, int col
)
96 struct token
*tok
= ALLOC(struct token
);
102 void token_free(struct token
*tok
)
104 if (tok
->type
== TOKEN_VALUE
)
105 value_clear(tok
->u
.v
);
106 else if (tok
->type
== TOKEN_IDENT
)
122 struct token
*tokens
[5];
126 static struct stream
* stream_new(FILE *file
)
129 struct stream
*s
= ALLOC(struct stream
);
132 s
->buffer
= (char*)malloc(s
->size
);
138 for (i
= 0; i
< 5; ++i
)
144 static void stream_free(struct stream
*s
)
147 assert(s
->n_token
== 0);
151 static int stream_getc(struct stream
*s
)
170 static void stream_ungetc(struct stream
*s
, int c
)
176 static void stream_push_char(struct stream
*s
, int c
)
178 if (s
->len
>= s
->size
) {
179 s
->size
= (3*s
->size
)/2;
180 s
->buffer
= (char*)realloc(s
->buffer
, s
->size
);
182 s
->buffer
[s
->len
++] = c
;
185 static struct token
*stream_push_token(struct stream
*s
, struct token
*tok
)
187 assert(s
->n_token
< 5);
188 s
->tokens
[s
->n_token
++] = tok
;
191 static struct token
*stream_next_token(struct stream
*s
)
198 return s
->tokens
[--s
->n_token
];
203 while ((c
= stream_getc(s
)) != -1 && isspace(c
))
225 tok
= token_new(line
, col
);
226 tok
->type
= (token_type
)c
;
229 if (c
== '-' || isdigit(c
)) {
230 tok
= token_new(line
, col
);
231 tok
->type
= TOKEN_VALUE
;
232 value_init(tok
->u
.v
);
233 stream_push_char(s
, c
);
234 while ((c
= stream_getc(s
)) != -1 && isdigit(c
))
235 stream_push_char(s
, c
);
238 if (s
->len
== 1 && s
->buffer
[0] == '-')
239 value_set_si(tok
->u
.v
, -1);
241 stream_push_char(s
, '\0');
242 mpz_set_str(tok
->u
.v
, s
->buffer
, 0);
246 if (c
== '#' || isalpha(c
)) {
247 tok
= token_new(line
, col
);
248 stream_push_char(s
, c
);
249 while ((c
= stream_getc(s
)) != -1 && isalnum(c
))
250 stream_push_char(s
, c
);
253 stream_push_char(s
, '\0');
254 if (!strcmp(s
->buffer
, "#variables")) {
255 tok
->type
= TOKEN_VARS
;
256 } else if (s
->buffer
[0] == '#') {
257 tok
->type
= TOKEN_UNKNOWN
;
258 } else if (!strcmp(s
->buffer
, "UNION")) {
259 tok
->type
= TOKEN_UNION
;
261 tok
->type
= TOKEN_IDENT
;
262 tok
->u
.s
= strdup(s
->buffer
);
267 if ((c
= stream_getc(s
)) == '=') {
268 tok
= token_new(line
, col
);
269 tok
->type
= TOKEN_GE
;
276 if ((c
= stream_getc(s
)) == '=') {
277 tok
= token_new(line
, col
);
278 tok
->type
= TOKEN_NE
;
285 tok
= token_new(line
, col
);
286 tok
->type
= TOKEN_UNKNOWN
;
290 void stream_error(struct stream
*s
, struct token
*tok
, char *msg
)
292 int line
= tok
? tok
->line
: s
->line
;
293 int col
= tok
? tok
->col
: s
->col
;
294 fprintf(stderr
, "syntax error (%d, %d): %s\n", line
, col
, msg
);
297 fprintf(stderr
, "got '%c'\n", tok
->type
);
304 struct parameter
*next
;
307 struct parameter
*parameter_new(char *name
, int pos
, struct parameter
*next
)
309 struct parameter
*p
= ALLOC(struct parameter
);
310 p
->name
= strdup(name
);
316 static int parameter_pos(struct parameter
**p
, char *s
)
318 int pos
= *p
? (*p
)->pos
+1 : 0;
321 for (q
= *p
; q
; q
= q
->next
) {
322 if (strcmp(q
->name
, s
) == 0)
328 *p
= parameter_new(s
, pos
, *p
);
332 static int optional_power(struct stream
*s
)
336 tok
= stream_next_token(s
);
339 if (tok
->type
!= '^') {
340 stream_push_token(s
, tok
);
344 tok
= stream_next_token(s
);
345 if (!tok
|| tok
->type
!= TOKEN_VALUE
) {
346 stream_error(s
, tok
, "expecting exponent");
348 stream_push_token(s
, tok
);
351 pow
= VALUE_TO_INT(tok
->u
.v
);
356 static evalue
*evalue_read_factor(struct stream
*s
, struct parameter
**p
);
357 static evalue
*evalue_read_term(struct stream
*s
, struct parameter
**p
);
359 static evalue
*create_fract_like(struct stream
*s
, evalue
*arg
, enode_type type
,
360 struct parameter
**p
)
364 pow
= optional_power(s
);
368 e
->x
.p
= new_enode(type
, pow
+2, -1);
369 value_clear(e
->x
.p
->arr
[0].d
);
370 e
->x
.p
->arr
[0] = *arg
;
372 evalue_set_si(&e
->x
.p
->arr
[1+pow
], 1, 1);
374 evalue_set_si(&e
->x
.p
->arr
[1+pow
], 0, 1);
379 static evalue
*create_relation(evalue
*arg
, int ne
)
385 e
->x
.p
= new_enode(relation
, 2+ne
, 0);
386 value_clear(e
->x
.p
->arr
[0].d
);
387 e
->x
.p
->arr
[0] = *arg
;
390 evalue_set_si(&e
->x
.p
->arr
[1], 0, 1);
391 evalue_set_si(&e
->x
.p
->arr
[1+ne
], 1, 1);
396 static evalue
*read_fract(struct stream
*s
, struct token
*tok
, struct parameter
**p
)
400 tok
= stream_next_token(s
);
402 assert(tok
->type
== '{');
405 arg
= evalue_read_term(s
, p
);
406 tok
= stream_next_token(s
);
407 if (!tok
|| tok
->type
!= '}') {
408 stream_error(s
, tok
, "expecting \"}\"");
410 stream_push_token(s
, tok
);
414 return create_fract_like(s
, arg
, fractional
, p
);
417 static evalue
*read_periodic(struct stream
*s
, struct parameter
**p
)
425 tok
= stream_next_token(s
);
426 assert(tok
&& tok
->type
== '[');
430 list
= (evalue
**)malloc(len
* sizeof(evalue
*));
434 evalue
*e
= evalue_read_term(s
, p
);
436 stream_error(s
, NULL
, "missing argument or list element");
441 list
= (evalue
**)realloc(list
, len
* sizeof(evalue
*));
445 tok
= stream_next_token(s
);
447 stream_error(s
, NULL
, "unexpected EOF");
450 if (tok
->type
!= ',')
455 if (n
== 1 && (tok
->type
== '=' || tok
->type
== TOKEN_NE
)) {
456 int ne
= tok
->type
== TOKEN_NE
;
458 tok
= stream_next_token(s
);
459 if (!tok
|| tok
->type
!= TOKEN_VALUE
) {
460 stream_error(s
, tok
, "expecting \"0\"");
462 stream_push_token(s
, tok
);
466 tok
= stream_next_token(s
);
467 if (!tok
|| tok
->type
!= ']') {
468 stream_error(s
, tok
, "expecting \"]\"");
470 stream_push_token(s
, tok
);
474 e
= create_relation(list
[0], ne
);
479 if (tok
->type
!= ']') {
480 stream_error(s
, tok
, "expecting \"]\"");
481 stream_push_token(s
, tok
);
487 tok
= stream_next_token(s
);
488 if (tok
->type
== '_') {
491 tok
= stream_next_token(s
);
492 if (!tok
|| tok
->type
!= TOKEN_IDENT
) {
493 stream_error(s
, tok
, "expecting identifier");
495 stream_push_token(s
, tok
);
500 pos
= parameter_pos(p
, tok
->u
.s
);
502 e
->x
.p
= new_enode(periodic
, n
, pos
+1);
504 value_clear(e
->x
.p
->arr
[n
].d
);
505 e
->x
.p
->arr
[n
] = *list
[n
];
509 stream_push_token(s
, tok
);
510 e
= create_fract_like(s
, list
[0], flooring
, p
);
513 stream_error(s
, tok
, "unexpected token");
514 stream_push_token(s
, tok
);
519 free_evalue_refs(list
[n
]);
526 static evalue
*evalue_read_factor(struct stream
*s
, struct parameter
**p
)
531 tok
= stream_next_token(s
);
535 if (tok
->type
== '(') {
537 e
= evalue_read_term(s
, p
);
538 tok
= stream_next_token(s
);
539 if (!tok
|| tok
->type
!= ')') {
540 stream_error(s
, tok
, "expecting \")\"");
542 stream_push_token(s
, tok
);
545 } else if (tok
->type
== TOKEN_VALUE
) {
548 value_set_si(e
->d
, 1);
550 value_assign(e
->x
.n
, tok
->u
.v
);
552 tok
= stream_next_token(s
);
553 if (tok
&& tok
->type
== '/') {
555 tok
= stream_next_token(s
);
556 if (!tok
|| tok
->type
!= TOKEN_VALUE
) {
557 stream_error(s
, tok
, "expecting denominator");
559 stream_push_token(s
, tok
);
562 value_assign(e
->d
, tok
->u
.v
);
565 stream_push_token(s
, tok
);
566 } else if (tok
->type
== TOKEN_IDENT
) {
567 int pos
= parameter_pos(p
, tok
->u
.s
);
568 int pow
= optional_power(s
);
572 e
->x
.p
= new_enode(polynomial
, pow
+1, pos
+1);
573 evalue_set_si(&e
->x
.p
->arr
[pow
], 1, 1);
575 evalue_set_si(&e
->x
.p
->arr
[pow
], 0, 1);
576 } else if (tok
->type
== '[') {
577 stream_push_token(s
, tok
);
578 e
= read_periodic(s
, p
);
579 } else if (tok
->type
== '{') {
580 stream_push_token(s
, tok
);
581 e
= read_fract(s
, tok
, p
);
584 tok
= stream_next_token(s
);
585 if (tok
&& tok
->type
== '*') {
588 e2
= evalue_read_factor(s
, p
);
590 stream_error(s
, NULL
, "unexpected EOF");
594 free_evalue_refs(e2
);
597 stream_push_token(s
, tok
);
602 static evalue
*evalue_read_term(struct stream
*s
, struct parameter
**p
)
607 e
= evalue_read_factor(s
, p
);
611 tok
= stream_next_token(s
);
615 if (tok
->type
== '+') {
618 e2
= evalue_read_term(s
, p
);
620 stream_error(s
, NULL
, "unexpected EOF");
624 free_evalue_refs(e2
);
627 stream_push_token(s
, tok
);
635 struct constraint
*next
;
636 struct constraint
*union_next
;
639 static struct constraint
*constraint_new()
641 struct constraint
*c
= ALLOC(struct constraint
);
643 c
->v
= Vector_Alloc(16);
645 c
->union_next
= NULL
;
649 static void constraint_free(struct constraint
*c
)
652 struct constraint
*next
= c
->next
? c
->next
: c
->union_next
;
659 static void constraint_extend(struct constraint
*c
, int pos
)
662 if (pos
< c
->v
->Size
)
665 v
= Vector_Alloc((3*c
->v
->Size
)/2);
666 Vector_Copy(c
->v
->p
, v
->p
, c
->v
->Size
);
671 static int evalue_read_constraint(struct stream
*s
, struct parameter
**p
,
672 struct constraint
**constraints
,
673 struct constraint
*union_next
)
676 struct constraint
*c
= NULL
;
678 while ((tok
= stream_next_token(s
))) {
681 if (tok
->type
== '+')
683 else if (tok
->type
== TOKEN_IDENT
) {
685 c
= constraint_new();
686 pos
= parameter_pos(p
, tok
->u
.s
);
687 constraint_extend(c
, 1+pos
);
688 value_set_si(c
->v
->p
[1+pos
], 1);
690 } else if (tok
->type
== TOKEN_VALUE
) {
692 c
= constraint_new();
693 tok2
= stream_next_token(s
);
694 if (tok2
&& tok2
->type
== TOKEN_IDENT
) {
695 pos
= parameter_pos(p
, tok2
->u
.s
);
696 constraint_extend(c
, 1+pos
);
697 value_assign(c
->v
->p
[1+pos
], tok
->u
.v
);
702 stream_push_token(s
, tok2
);
703 value_assign(c
->v
->p
[0], tok
->u
.v
);
706 } else if (tok
->type
== TOKEN_GE
|| tok
->type
== '=') {
707 int type
= tok
->type
== TOKEN_GE
;
709 tok
= stream_next_token(s
);
710 if (!tok
|| tok
->type
!= TOKEN_VALUE
|| value_notzero_p(tok
->u
.v
)) {
711 stream_error(s
, tok
, "expecting \"0\"");
713 stream_push_token(s
, tok
);
717 c
->next
= *constraints
;
718 c
->union_next
= union_next
;
725 stream_push_token(s
, tok
);
727 stream_error(s
, tok
, "unexpected token");
736 static struct constraint
*evalue_read_domain(struct stream
*s
, struct parameter
**p
,
739 struct constraint
*constraints
= NULL
;
740 struct constraint
*union_next
= NULL
;
744 tok
= stream_next_token(s
);
747 stream_push_token(s
, tok
);
750 while (evalue_read_constraint(s
, p
, &constraints
, union_next
)) {
751 tok
= stream_next_token(s
);
753 if (tok
->type
== TOKEN_UNION
) {
755 tok
= stream_next_token(s
);
757 stream_error(s
, NULL
, "unexpected EOF");
760 stream_push_token(s
, tok
);
761 union_next
= constraints
;
765 stream_push_token(s
, tok
);
766 /* empty line separates domain from evalue */
767 if (tok
->line
> line
+1)
777 struct constraint
*constraints
;
779 struct section
*next
;
782 static char **extract_parameters(struct parameter
*p
, unsigned *nparam
)
787 *nparam
= p
? p
->pos
+1 : 0;
788 params
= ALLOCN(char *, *nparam
);
789 for (i
= 0; i
< *nparam
; ++i
) {
790 struct parameter
*next
= p
->next
;
791 params
[p
->pos
] = p
->name
;
798 static Polyhedron
*constraints2domain(struct constraint
*constraints
,
799 unsigned nparam
, unsigned MaxRays
)
804 struct constraint
*c
;
805 struct constraint
*union_next
= NULL
;
807 for (n
= 0, c
= constraints
; c
; ++n
, c
= c
->next
)
809 M
= Matrix_Alloc(n
, 1+nparam
+1);
811 struct constraint
*next
= constraints
->next
;
812 union_next
= constraints
->union_next
;
813 Vector_Copy(constraints
->v
->p
+1, M
->p
[n
]+1, nparam
);
814 if (constraints
->type
)
815 value_set_si(M
->p
[n
][0], 1);
816 value_assign(M
->p
[n
][1+nparam
], constraints
->v
->p
[0]);
817 constraints
->next
= NULL
;
818 constraints
->union_next
= NULL
;
819 constraint_free(constraints
);
822 D
= Constraints2Polyhedron(M
, MaxRays
);
826 D
= DomainConcat(D
, constraints2domain(union_next
, nparam
, MaxRays
));
830 static evalue
*evalue_read_partition(struct stream
*s
, struct parameter
*p
,
832 unsigned *nparam
, unsigned MaxRays
)
834 struct section
*part
= NULL
;
835 struct constraint
*constraints
;
839 while ((constraints
= evalue_read_domain(s
, &p
, MaxRays
))) {
840 evalue
*e
= evalue_read_term(s
, &p
);
842 stream_error(s
, NULL
, "missing evalue");
845 struct section
*sect
= ALLOC(struct section
);
846 sect
->constraints
= constraints
;
857 *ppp
= extract_parameters(p
, nparam
);
860 e
->x
.p
= new_enode(partition
, 2*m
, *nparam
);
862 for (j
= 0; j
< m
; ++j
) {
864 struct section
*next
= part
->next
;
865 constraints
= part
->constraints
;
866 D
= constraints2domain(part
->constraints
, *nparam
, MaxRays
);
867 EVALUE_SET_DOMAIN(e
->x
.p
->arr
[2*j
], D
);
868 value_clear(e
->x
.p
->arr
[2*j
+1].d
);
869 e
->x
.p
->arr
[2*j
+1] = *part
->e
;
878 static evalue
*evalue_read(FILE *in
, char *var_list
, char ***ppp
, unsigned *nvar
,
879 unsigned *nparam
, unsigned MaxRays
)
881 struct stream
*s
= stream_new(in
);
884 struct parameter
*p
= NULL
;
889 while ((next
= strchr(var_list
, ','))) {
892 parameter_pos(&p
, var_list
);
896 if (strlen(var_list
) > 0)
897 parameter_pos(&p
, var_list
);
898 nv
= p
? p
->pos
+1 : 0;
902 if (!(tok
= stream_next_token(s
)))
905 if (tok
->type
== TOKEN_VARS
) {
908 tok
= stream_next_token(s
);
909 if (!tok
|| tok
->type
!= TOKEN_IDENT
) {
910 stream_error(s
, tok
, "expecting identifier");
914 parameter_pos(&p
, tok
->u
.s
);
916 tok
= stream_next_token(s
);
917 if (!tok
|| tok
->type
!= ',')
924 nv
= p
? p
->pos
+1 : 0;
927 if (tok
->type
== TOKEN_VALUE
) {
928 struct token
*tok2
= stream_next_token(s
);
930 stream_push_token(s
, tok2
);
931 stream_push_token(s
, tok
);
932 if (tok2
&& (tok2
->type
== TOKEN_IDENT
|| tok2
->type
== TOKEN_GE
))
933 e
= evalue_read_partition(s
, p
, ppp
, nparam
, MaxRays
);
935 e
= evalue_read_term(s
, &p
);
936 *ppp
= extract_parameters(p
, nparam
);
938 } else if (tok
->type
== TOKEN_IDENT
) {
939 stream_push_token(s
, tok
);
940 e
= evalue_read_partition(s
, p
, ppp
, nparam
, MaxRays
);
942 stream_error(s
, tok
, "unexpected token");
943 *nparam
= nv
== -1 ? 0 : nv
;
955 static int check_poly_max(const struct check_poly_data
*data
,
956 int nparam
, Value
*z
,
957 const struct verify_options
*options
);
959 struct check_poly_max_data
: public check_poly_data
{
964 check_poly_max_data(Value
*z
, evalue
*EP
, piecewise_lst
*pl
) :
967 this->check
= check_poly_max
;
971 static void optimum(Polyhedron
*S
, int pos
, const check_poly_max_data
*data
,
972 Value
*opt
, bool& found
,
973 const struct verify_options
*options
)
978 value_set_double(c
, compute_evalue(data
->EP
, data
->z
+1)+.25);
980 value_assign(*opt
, c
);
983 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
) {
984 if (value_gt(c
, *opt
))
985 value_assign(*opt
, c
);
987 if (value_lt(c
, *opt
))
988 value_assign(*opt
, c
);
997 ok
= !(lower_upper_bounds(1+pos
, S
, data
->z
, &LB
, &UB
));
999 for (; value_le(LB
, UB
); value_increment(LB
, LB
)) {
1000 value_assign(data
->z
[1+pos
], LB
);
1001 optimum(S
->next
, pos
+1, data
, opt
, found
, options
);
1003 value_set_si(data
->z
[1+pos
], 0);
1009 static void optimum(const check_poly_max_data
*data
, Value
*opt
,
1010 const struct verify_options
*options
)
1013 for (int i
= 0; i
< data
->EP
->x
.p
->size
/2; ++i
)
1014 if (!emptyQ2(data
->S
[i
]))
1015 optimum(data
->S
[i
], 0, data
, opt
, found
, options
);
1019 static int check_poly_max(const struct check_poly_data
*data
,
1020 int nparam
, Value
*z
,
1021 const struct verify_options
*options
)
1025 const check_poly_max_data
*max_data
;
1026 max_data
= static_cast<const check_poly_max_data
*>(data
);
1033 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
1038 max_data
->pl
->evaluate(nparam
, z
, &n
, &d
);
1039 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
1040 mpz_fdiv_q(m
, n
, d
);
1042 mpz_cdiv_q(m
, n
, d
);
1044 if (options
->print_all
) {
1045 printf("%s(", minmax
);
1046 value_print(stdout
, VALUE_FMT
, z
[0]);
1047 for (k
= 1; k
< nparam
; ++k
) {
1049 value_print(stdout
, VALUE_FMT
, z
[k
]);
1052 value_print(stdout
, VALUE_FMT
, n
);
1053 if (value_notone_p(d
)) {
1055 value_print(stdout
, VALUE_FMT
, d
);
1058 value_print(stdout
, VALUE_FMT
, m
);
1062 optimum(max_data
, &n
, options
);
1064 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
1065 ok
= value_ge(m
, n
);
1067 ok
= value_le(m
, n
);
1069 if (options
->print_all
) {
1070 printf(", %s(EP) = ", minmax
);
1071 value_print(stdout
, VALUE_FMT
, n
);
1078 fprintf(stderr
, "Error !\n");
1079 fprintf(stderr
, "%s(", minmax
);
1080 value_print(stderr
, VALUE_FMT
, z
[0]);
1081 for (k
= 1; k
< nparam
; ++k
) {
1082 fprintf(stderr
,", ");
1083 value_print(stderr
, VALUE_FMT
, z
[k
]);
1085 fprintf(stderr
, ") should be ");
1086 if (options
->barvinok
->bernstein_optimize
== BV_BERNSTEIN_MAX
)
1087 fprintf(stderr
, "greater");
1089 fprintf(stderr
, "smaller");
1090 fprintf(stderr
, " than or equal to ");
1091 value_print(stderr
, VALUE_FMT
, n
);
1092 fprintf(stderr
, ", while pl eval gives ");
1093 value_print(stderr
, VALUE_FMT
, m
);
1094 fprintf(stderr
, ".\n");
1095 cerr
<< *max_data
->pl
<< endl
;
1096 } else if (options
->print_all
)
1106 static int verify(Polyhedron
*D
, piecewise_lst
*pl
, evalue
*EP
,
1107 unsigned nvar
, unsigned nparam
, Vector
*p
,
1108 struct verify_options
*options
)
1111 unsigned MaxRays
= options
->barvinok
->MaxRays
;
1112 assert(value_zero_p(EP
->d
));
1113 assert(EP
->x
.p
->type
== partition
);
1116 CS
= check_poly_context_scan(NULL
, &D
, D
->Dimension
, options
);
1118 check_poly_init(D
, options
);
1120 if (!(CS
&& emptyQ2(CS
))) {
1121 check_poly_max_data
data(p
->p
, EP
, pl
);
1122 data
.S
= ALLOCN(Polyhedron
*, EP
->x
.p
->size
/2);
1123 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
1124 Polyhedron
*A
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
1125 data
.S
[i
] = Polyhedron_Scan(A
, D
, MaxRays
& POL_NO_DUAL
? 0 : MaxRays
);
1127 ok
= check_poly(CS
, &data
, nparam
, 0, p
->p
+1+nvar
, options
);
1128 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
)
1129 Domain_Free(data
.S
[i
]);
1133 if (!options
->print_all
)
1144 static int verify(piecewise_lst
*pl
, evalue
*EP
, unsigned nvar
, unsigned nparam
,
1145 struct verify_options
*options
)
1149 p
= Vector_Alloc(nvar
+nparam
+2);
1150 value_set_si(p
->p
[nvar
+nparam
+1], 1);
1152 for (int i
= 0; i
< pl
->list
.size(); ++i
) {
1153 int ok
= verify(pl
->list
[i
].first
, pl
, EP
, nvar
, nparam
, p
, options
);
1154 if (!ok
&& !options
->continue_on_error
)
1163 static int optimize(evalue
*EP
, char **all_vars
, unsigned nvar
, unsigned nparam
,
1164 struct options
*options
)
1167 piecewise_lst
*pl
= NULL
;
1168 U
= Universe_Polyhedron(nparam
);
1169 int print_solution
= 1;
1173 params
= constructParameterVector(all_vars
+nvar
, nparam
);
1175 if (options
->verify
.verify
) {
1176 verify_options_set_range(&options
->verify
, nvar
+nparam
);
1177 if (!options
->verbose
)
1181 if (options
->minimize
)
1182 options
->verify
.barvinok
->bernstein_optimize
= BV_BERNSTEIN_MIN
;
1184 options
->verify
.barvinok
->bernstein_optimize
= BV_BERNSTEIN_MAX
;
1185 pl
= evalue_bernstein_coefficients(NULL
, EP
, U
, params
,
1186 options
->verify
.barvinok
);
1188 if (options
->minimize
)
1193 cout
<< *pl
<< endl
;
1194 if (options
->verify
.verify
)
1195 result
= verify(pl
, EP
, nvar
, nparam
, &options
->verify
);
1203 int main(int argc
, char **argv
)
1206 char **all_vars
= NULL
;
1209 struct options options
;
1210 struct barvinok_options
*bv_options
= barvinok_options_new_with_defaults();
1211 static struct argp_child argp_children
[] = {
1212 { &convert_argp
, 0, "input conversion", 1 },
1213 { &verify_argp
, 0, "verification", 2 },
1214 { &barvinok_argp
, 0, "barvinok options", 3 },
1217 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
1220 options
.verify
.barvinok
= bv_options
;
1221 set_program_name(argv
[0]);
1222 argp_parse(&argp
, argc
, argv
, 0, 0, &options
);
1224 EP
= evalue_read(stdin
, options
.var_list
, &all_vars
, &nvar
, &nparam
,
1225 bv_options
->MaxRays
);
1229 evalue_split_periods(EP
, options
.split
, bv_options
->MaxRays
);
1231 evalue_convert(EP
, &options
.convert
, options
.verbose
, nparam
, all_vars
);
1233 if (EVALUE_IS_ZERO(*EP
))
1234 print_evalue(stdout
, EP
, all_vars
);
1236 result
= optimize(EP
, all_vars
, nvar
, nparam
, &options
);
1238 free_evalue_refs(EP
);
1241 if (options
.var_list
)
1242 free(options
.var_list
);
1243 Free_ParamNames(all_vars
, nvar
+nparam
);
1244 barvinok_options_free(bv_options
);