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" },
23 { "verbose", 'v', 0, 0, },
28 struct convert_options convert
;
29 struct verify_options verify
;
34 static error_t
parse_opt(int key
, char *arg
, struct argp_state
*state
)
36 struct options
*options
= (struct options
*) state
->input
;
40 state
->child_inputs
[0] = &options
->convert
;
41 state
->child_inputs
[1] = &options
->verify
;
42 state
->child_inputs
[2] = options
->verify
.barvinok
;
43 options
->var_list
= NULL
;
50 options
->var_list
= strdup(arg
);
53 return ARGP_ERR_UNKNOWN
;
58 static int check_poly_sum(const struct check_poly_data
*data
,
60 const struct verify_options
*options
);
62 struct check_poly_sum_data
: public check_poly_data
{
67 check_poly_sum_data(Value
*z
, evalue
*EP
, evalue
*sum
) :
70 this->check
= check_poly_sum
;
74 static void sum(Polyhedron
*S
, int pos
, const check_poly_sum_data
*data
,
75 evalue
*s
, const struct verify_options
*options
)
78 evalue
*e
= evalue_eval(data
->EP
, data
->z
+1);
86 ok
= !(lower_upper_bounds(1+pos
, S
, data
->z
, &LB
, &UB
));
88 for (; value_le(LB
, UB
); value_increment(LB
, LB
)) {
89 value_assign(data
->z
[1+pos
], LB
);
90 sum(S
->next
, pos
+1, data
, s
, options
);
92 value_set_si(data
->z
[1+pos
], 0);
98 static evalue
*sum(const check_poly_sum_data
*data
,
99 const struct verify_options
*options
)
101 evalue
*s
= evalue_zero();
102 for (int i
= 0; i
< data
->EP
->x
.p
->size
/2; ++i
)
103 if (!emptyQ2(data
->S
[i
]))
104 sum(data
->S
[i
], 0, data
, s
, options
);
108 static int check_poly_sum(const struct check_poly_data
*data
,
109 int nparam
, Value
*z
,
110 const struct verify_options
*options
)
112 const check_poly_sum_data
*sum_data
;
113 sum_data
= static_cast<const check_poly_sum_data
*>(data
);
118 e
= evalue_eval(sum_data
->sum
, z
);
119 s
= sum(sum_data
, options
);
123 check_poly_print(ok
, nparam
, z
, s
->x
.n
, s
->d
, e
->x
.n
, e
->d
,
124 "sum", "sum(EP)", "summation", options
);
132 static int verify(Polyhedron
*P
, evalue
*sum
, evalue
*EP
,
133 unsigned nvar
, unsigned nparam
, Vector
*p
,
134 struct verify_options
*options
)
137 unsigned MaxRays
= options
->barvinok
->MaxRays
;
140 CS
= check_poly_context_scan(NULL
, &P
, P
->Dimension
, options
);
142 check_poly_init(P
, options
);
144 if (!(CS
&& emptyQ2(CS
))) {
145 check_poly_sum_data
data(p
->p
, EP
, sum
);
146 data
.S
= ALLOCN(Polyhedron
*, EP
->x
.p
->size
/2);
147 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
) {
148 Polyhedron
*A
= EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]);
149 data
.S
[i
] = Polyhedron_Scan(A
, P
, MaxRays
& POL_NO_DUAL
? 0 : MaxRays
);
151 error
= !check_poly(CS
, &data
, nparam
, 0, p
->p
+1+nvar
, options
);
152 for (int i
= 0; i
< EP
->x
.p
->size
/2; ++i
)
153 Domain_Free(data
.S
[i
]);
157 if (!options
->print_all
)
169 * Project on final dim dimensions
171 Polyhedron
*DomainProject(Polyhedron
*D
, unsigned dim
, unsigned MaxRays
)
176 R
= Polyhedron_Project(D
, dim
);
177 for (P
= D
->next
; P
; P
= P
->next
) {
178 Polyhedron
*R2
= Polyhedron_Project(P
, dim
);
179 Polyhedron
*R3
= DomainUnion(R
, R2
, MaxRays
);
187 static int verify(evalue
*EP
, evalue
*sum
, unsigned nvar
, unsigned nparam
,
188 struct verify_options
*options
)
192 p
= Vector_Alloc(nvar
+nparam
+2);
193 value_set_si(p
->p
[nvar
+nparam
+1], 1);
195 assert(value_zero_p(EP
->d
));
196 assert(EP
->x
.p
->type
== partition
);
198 Polyhedron
*EP_D
= EVALUE_DOMAIN(EP
->x
.p
->arr
[0]);
199 Polyhedron
*D
= Polyhedron_Project(EP_D
, nparam
);
201 for (int i
= 1; i
< EP
->x
.p
->size
/2; ++i
) {
203 EP_D
= DomainProject(EVALUE_DOMAIN(EP
->x
.p
->arr
[2*i
]), nparam
,
204 options
->barvinok
->MaxRays
);
205 D
= DomainUnion(EP_D
, D
, options
->barvinok
->MaxRays
);
211 for (Polyhedron
*P
= D
; P
; P
= P
->next
) {
212 error
= verify(P
, sum
, EP
, nvar
, nparam
, p
, options
);
213 if (error
&& !options
->continue_on_error
)
223 int main(int argc
, char **argv
)
226 char **all_vars
= NULL
;
229 struct options options
;
230 struct barvinok_options
*bv_options
= barvinok_options_new_with_defaults();
231 static struct argp_child argp_children
[] = {
232 { &convert_argp
, 0, "input conversion", 1 },
233 { &verify_argp
, 0, "verification", 2 },
234 { &barvinok_argp
, 0, "barvinok options", 3 },
237 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
240 options
.verify
.barvinok
= bv_options
;
241 set_program_name(argv
[0]);
242 argp_parse(&argp
, argc
, argv
, 0, 0, &options
);
244 EP
= evalue_read_from_file(stdin
, options
.var_list
, &all_vars
,
245 &nvar
, &nparam
, bv_options
->MaxRays
);
248 if (options
.verify
.verify
)
249 verify_options_set_range(&options
.verify
, nvar
+nparam
);
251 evalue_convert(EP
, &options
.convert
, options
.verbose
, nparam
, all_vars
);
253 if (EVALUE_IS_ZERO(*EP
))
254 print_evalue(stdout
, EP
, all_vars
);
256 evalue
*sum
= barvinok_summate(EP
, nvar
, bv_options
);
258 if (options
.verify
.verify
)
259 result
= verify(EP
, sum
, nvar
, nparam
, &options
.verify
);
261 print_evalue(stdout
, sum
, all_vars
+nvar
);
267 if (options
.var_list
)
268 free(options
.var_list
);
269 Free_ParamNames(all_vars
, nvar
+nparam
);
270 barvinok_options_free(bv_options
);