4 #include <barvinok/util.h>
5 #include <barvinok/barvinok.h>
10 #include "omega/convert.h"
13 #include "verif_ehrhart.h"
15 /* The input of this example program is a polytope in combined
16 * data and parameter space followed by two lines indicating
17 * the number of existential variables and parameters respectively.
18 * The first lines starts with "E ", followed by a number.
19 * The second lines starts with "P ", followed by a number.
20 * These two lines are (optionally) followed by the names of the parameters.
21 * The polytope is in PolyLib notation.
24 struct argp_option argp_options
[] = {
25 { "omega", 'o', 0, 0 },
27 { "series", 's', 0, 0 },
28 { "scarf", 'S', 0, 0 },
29 { "convert", 'c', 0, 0 },
30 { "floor", 'f', 0, 0 },
31 { "range-reduction", 'R', 0, 0 },
37 struct verify_options verify
;
48 error_t
parse_opt(int key
, char *arg
, struct argp_state
*state
)
50 struct arguments
*arguments
= (struct arguments
*)(state
->input
);
54 state
->child_inputs
[0] = arguments
->verify
.barvinok
;
55 state
->child_inputs
[1] = &arguments
->verify
;
58 arguments
->series
= 1;
67 error(0, 0, "--omega option not supported");
74 error(0, 0, "--pip option not supported");
81 arguments
->convert
= 1;
87 arguments
->verbose
= 1;
90 return ARGP_ERR_UNKNOWN
;
97 Polyhedron
*Omega_simplify(Polyhedron
*P
,
98 unsigned exist
, unsigned nparam
, char **parms
)
102 Relation r
= Polyhedron2relation(P
, exist
, nparam
, parms
);
104 return relation2Domain(r
, varv
, paramv
);
107 Polyhedron
*Omega_simplify(Polyhedron
*P
,
108 unsigned exist
, unsigned nparam
, char **parms
)
114 static void verify_results(Polyhedron
*P
, evalue
*EP
, int exist
, int nparam
,
115 verify_options
*options
);
117 int main(int argc
, char **argv
)
122 int exist
, nparam
, nvar
;
125 int print_solution
= 1;
126 struct arguments arguments
;
127 static struct argp_child argp_children
[] = {
128 { &barvinok_argp
, 0, 0, 0 },
129 { &verify_argp
, 0, "verification", 1 },
132 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
133 struct barvinok_options
*options
= barvinok_options_new_with_defaults();
135 arguments
.verify
.barvinok
= options
;
137 arguments
.convert
= 0;
141 arguments
.series
= 0;
143 arguments
.verbose
= 0;
145 argp_parse(&argp
, argc
, argv
, 0, 0, &arguments
);
147 if (arguments
.series
&& !arguments
.scarf
) {
149 "--series currently only available if --scarf is specified\n");
154 A
= Constraints2Polyhedron(MA
, options
->MaxRays
);
157 fgets(s
, 128, stdin
);
158 while ((*s
=='#') || (sscanf(s
, "E %d", &exist
)<1))
159 fgets(s
, 128, stdin
);
161 fgets(s
, 128, stdin
);
162 while ((*s
=='#') || (sscanf(s
, "P %d", &nparam
)<1))
163 fgets(s
, 128, stdin
);
165 /******* Read the options: initialize Min and Max ********/
167 if (arguments
.verify
.verify
) {
168 verify_options_set_range(&arguments
.verify
, A
);
169 if (!arguments
.verbose
)
173 if (print_solution
) {
174 Polyhedron_Print(stdout
, P_VALUE_FMT
, A
);
175 printf("exist: %d, nparam: %d\n", exist
, nparam
);
177 param_name
= Read_ParamNames(stdin
, nparam
);
178 nvar
= A
->Dimension
- exist
- nparam
;
179 if (arguments
.omega
) {
180 A
= Omega_simplify(A
, exist
, nparam
, param_name
);
182 exist
= A
->Dimension
- nvar
- nparam
;
184 if (arguments
.series
) {
186 barvinok_options
*options
= barvinok_options_new_with_defaults();
187 assert(arguments
.scarf
);
188 gf
= barvinok_enumerate_scarf_series(A
, exist
, nparam
, options
);
189 if (print_solution
) {
190 gf
->print(std::cout
, nparam
, param_name
);
194 barvinok_options_free(options
);
196 if (arguments
.scarf
) {
197 barvinok_options
*options
= barvinok_options_new_with_defaults();
198 EP
= barvinok_enumerate_scarf(A
, exist
, nparam
, options
);
199 barvinok_options_free(options
);
200 } else if (arguments
.pip
&& exist
> 0)
201 EP
= barvinok_enumerate_pip_with_options(A
, exist
, nparam
, options
);
203 EP
= barvinok_enumerate_e_with_options(A
, exist
, nparam
, options
);
207 evalue_range_reduction(EP
);
209 print_evalue(stdout
, EP
, param_name
);
210 if (arguments
.floor
) {
211 fprintf(stderr
, "WARNING: floor conversion not supported\n");
212 evalue_frac2floor2(EP
, 0);
214 print_evalue(stdout
, EP
, param_name
);
215 } else if (arguments
.convert
) {
216 evalue_mod2table(EP
, nparam
);
218 print_evalue(stdout
, EP
, param_name
);
220 if (arguments
.verify
.verify
) {
221 arguments
.verify
.params
= param_name
;
222 verify_results(A
, EP
, exist
, nparam
, &arguments
.verify
);
224 free_evalue_refs(EP
);
227 Free_ParamNames(param_name
, nparam
);
232 void verify_results(Polyhedron
*P
, evalue
*EP
, int exist
, int nparam
,
233 verify_options
*options
)
239 unsigned MaxRays
= options
->barvinok
->MaxRays
;
240 Polyhedron
*C
= Polyhedron_Project(P
, nparam
);
243 p
= (Value
*)malloc(sizeof(Value
) * (P
->Dimension
+2));
244 for(i
=0;i
<=P
->Dimension
;i
++) {
246 value_set_si(p
[i
],0);
249 value_set_si(p
[i
],1);
251 /* S = scanning list of polyhedra */
252 S
= Polyhedron_Scan(P
, C
, MaxRays
& POL_NO_DUAL
? 0 : MaxRays
);
254 CS
= check_poly_context_scan(C
, options
);
256 check_poly_init(C
, options
);
258 /******* CHECK NOW *********/
260 if (S
&& !check_poly(S
, CS
, EP
, exist
, nparam
, 0, p
, options
)) {
261 fprintf(stderr
,"Check failed !\n");
265 if (!options
->print_all
)
268 for(i
=0;i
<=(P
->Dimension
+1);i
++)