3 #include <barvinok/barvinok.h>
4 #include <barvinok/options.h>
5 #include <barvinok/util.h>
8 #include "evalue_convert.h"
9 #include "evalue_read.h"
16 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
18 #define OPT_VARS (BV_OPT_LAST+1)
20 struct argp_option argp_options
[] = {
21 { "variables", OPT_VARS
, "list", 0,
22 "comma separated list of variables over which to sum" },
27 struct convert_options convert
;
28 struct verify_options verify
;
32 static error_t
parse_opt(int key
, char *arg
, struct argp_state
*state
)
34 struct options
*options
= (struct options
*) state
->input
;
38 state
->child_inputs
[0] = &options
->convert
;
39 state
->child_inputs
[1] = &options
->verify
;
40 state
->child_inputs
[2] = options
->verify
.barvinok
;
41 options
->var_list
= NULL
;
44 options
->var_list
= strdup(arg
);
47 return ARGP_ERR_UNKNOWN
;
52 static int check_poly_sum(const struct check_poly_data
*data
,
54 const struct verify_options
*options
);
56 struct check_poly_sum_data
: public check_poly_data
{
61 check_poly_sum_data(Value
*z
, evalue
*EP
, evalue
*sum
) :
64 this->check
= check_poly_sum
;
68 static void sum(Polyhedron
*S
, int pos
, const check_poly_sum_data
*data
,
69 evalue
*s
, const struct verify_options
*options
)
72 evalue
*e
= evalue_eval(data
->EP
, data
->z
+1);
80 ok
= !(lower_upper_bounds(1+pos
, S
, data
->z
, &LB
, &UB
));
82 for (; value_le(LB
, UB
); value_increment(LB
, LB
)) {
83 value_assign(data
->z
[1+pos
], LB
);
84 sum(S
->next
, pos
+1, data
, s
, options
);
86 value_set_si(data
->z
[1+pos
], 0);
92 static evalue
*sum(const check_poly_sum_data
*data
,
93 const struct verify_options
*options
)
95 evalue
*s
= evalue_zero();
96 for (int i
= 0; i
< data
->EP
->x
.p
->size
/2; ++i
)
97 if (!emptyQ2(data
->S
[i
]))
98 sum(data
->S
[i
], 0, data
, s
, options
);
102 static int check_poly_sum(const struct check_poly_data
*data
,
103 int nparam
, Value
*z
,
104 const struct verify_options
*options
)
106 const check_poly_sum_data
*sum_data
;
107 sum_data
= static_cast<const check_poly_sum_data
*>(data
);
112 e
= evalue_eval(sum_data
->sum
, z
);
113 s
= sum(sum_data
, options
);
117 check_poly_print(ok
, nparam
, z
, s
->x
.n
, s
->d
, e
->x
.n
, e
->d
,
118 "sum", "sum(EP)", "summation", options
);
126 static int verify(Polyhedron
*P
, evalue
*sum
, evalue
*EP
,
127 unsigned nvar
, unsigned nparam
, Vector
*p
,
128 struct verify_options
*options
)
131 unsigned MaxRays
= options
->barvinok
->MaxRays
;
134 CS
= check_poly_context_scan(NULL
, &P
, P
->Dimension
, options
);
136 check_poly_init(P
, options
);
138 if (!(CS
&& emptyQ2(CS
))) {
139 check_poly_sum_data
data(p
->p
, EP
, sum
);
140 data
.S
= ALLOCN(Polyhedron
*, EP
->x
.p
->size
/2);
141 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
142 Polyhedron
*A
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
143 data
.S
[i
] = Polyhedron_Scan(A
, P
, MaxRays
& POL_NO_DUAL
? 0 : MaxRays
);
145 error
= !check_poly(CS
, &data
, nparam
, 0, p
->p
+1+nvar
, options
);
146 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
)
147 Domain_Free(data
.S
[i
]);
151 if (!options
->print_all
)
163 * Project on final dim dimensions
165 Polyhedron
*DomainProject(Polyhedron
*D
, unsigned dim
, unsigned MaxRays
)
170 R
= Polyhedron_Project(D
, dim
);
171 for (P
= D
->next
; P
; P
= P
->next
) {
172 Polyhedron
*R2
= Polyhedron_Project(P
, dim
);
173 Polyhedron
*R3
= DomainUnion(R
, R2
, MaxRays
);
181 static int verify(evalue
*EP
, evalue
*sum
, unsigned nvar
, unsigned nparam
,
182 struct verify_options
*options
)
186 p
= Vector_Alloc(nvar
+nparam
+2);
187 value_set_si(p
->p
[nvar
+nparam
+1], 1);
189 assert(value_zero_p(EP
->d
));
190 assert(EP
->x
.p
->type
== partition
);
192 Polyhedron
*EP_D
= EVALUE_DOMAIN(EP
->x
.p
->arr
[0]);
193 Polyhedron
*D
= Polyhedron_Project(EP_D
, nparam
);
195 for (int i
= 1; i
< EP
->x
.p
->size
/2; ++i
) {
197 EP_D
= DomainProject(EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]), nparam
,
198 options
->barvinok
->MaxRays
);
199 D
= DomainUnion(EP_D
, D
, options
->barvinok
->MaxRays
);
205 for (Polyhedron
*P
= D
; P
; P
= P
->next
) {
206 error
= verify(P
, sum
, EP
, nvar
, nparam
, p
, options
);
207 if (error
&& !options
->continue_on_error
)
217 int main(int argc
, char **argv
)
220 char **all_vars
= NULL
;
223 struct options options
;
224 struct barvinok_options
*bv_options
= barvinok_options_new_with_defaults();
225 static struct argp_child argp_children
[] = {
226 { &convert_argp
, 0, "input conversion", 1 },
227 { &verify_argp
, 0, "verification", 2 },
228 { &barvinok_argp
, 0, "barvinok options", 3 },
231 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
234 options
.verify
.barvinok
= bv_options
;
235 set_program_name(argv
[0]);
236 argp_parse(&argp
, argc
, argv
, 0, 0, &options
);
238 EP
= evalue_read_from_file(stdin
, options
.var_list
, &all_vars
,
239 &nvar
, &nparam
, bv_options
->MaxRays
);
242 if (options
.verify
.verify
)
243 verify_options_set_range(&options
.verify
, nvar
+nparam
);
245 evalue_convert(EP
, &options
.convert
, bv_options
->verbose
, nparam
, all_vars
);
247 if (EVALUE_IS_ZERO(*EP
))
248 print_evalue(stdout
, EP
, all_vars
);
250 evalue
*sum
= barvinok_summate(EP
, nvar
, bv_options
);
252 if (options
.verify
.verify
)
253 result
= verify(EP
, sum
, nvar
, nparam
, &options
.verify
);
255 print_evalue(stdout
, sum
, all_vars
+nvar
);
261 if (options
.var_list
)
262 free(options
.var_list
);
263 Free_ParamNames(all_vars
, nvar
+nparam
);
264 barvinok_options_free(bv_options
);