5 #include <barvinok/util.h>
6 #include <barvinok/barvinok.h>
12 #include "omega_interface/convert.h"
13 #include "omega_interface/count.h"
15 #include "skewed_genfun.h"
17 #include "verif_ehrhart.h"
18 #include "verify_series.h"
19 #include "evalue_convert.h"
21 /* The input of this example program is a polytope in combined
22 * data and parameter space followed by two lines indicating
23 * the number of existential variables and parameters respectively.
24 * The first lines starts with "E ", followed by a number.
25 * The second lines starts with "P ", followed by a number.
26 * These two lines are (optionally) followed by the names of the parameters.
27 * The polytope is in PolyLib notation.
30 struct argp_option argp_options
[] = {
32 { "omega", 'o', 0, 0 },
33 { "parker", 'P', 0, 0 },
34 { "series", 's', 0, 0 },
35 { "series", 's', 0, 0, "compute rational generating function" },
36 { "explicit", 'e', 0, 0, "convert rgf to psp" },
37 { "scarf", 'S', 0, 0 },
42 struct verify_options verify
;
43 struct convert_options convert
;
52 error_t
parse_opt(int key
, char *arg
, struct argp_state
*state
)
54 struct arguments
*arguments
= (struct arguments
*)(state
->input
);
58 state
->child_inputs
[0] = arguments
->verify
.barvinok
;
59 state
->child_inputs
[1] = &arguments
->verify
;
60 state
->child_inputs
[2] = &arguments
->convert
;
63 arguments
->function
= 1;
66 arguments
->series
= 1;
75 error(0, 0, "--omega option not supported");
80 arguments
->parker
= 1;
82 error(0, 0, "--parker option not supported");
89 return ARGP_ERR_UNKNOWN
;
96 Polyhedron
*Omega_simplify(Polyhedron
*P
,
97 unsigned exist
, unsigned nparam
, const char **parms
,
102 Relation r
= Polyhedron2relation(P
, exist
, nparam
, parms
);
104 return relation2Domain(r
, varv
, paramv
, MaxRays
);
107 Polyhedron
*Omega_simplify(Polyhedron
*P
,
108 unsigned exist
, unsigned nparam
, const char **parms
,
114 evalue
*barvinok_enumerate_parker(Polyhedron
*P
,
115 unsigned exist
, unsigned nparam
,
123 static void verify_results(Polyhedron
*P
, evalue
*EP
, gen_fun
*gf
,
124 int exist
, int nparam
,
127 static char *next_line(FILE *input
, char *line
, unsigned len
)
132 if (!(p
= fgets(line
, len
, input
)))
134 while (isspace(*p
) && *p
!= '\n')
136 } while (*p
== '#' || *p
== '\n');
141 int main(int argc
, char **argv
)
145 const char **param_name
;
146 int exist
, nparam
, nvar
;
150 int print_solution
= 1;
151 struct arguments arguments
;
152 static struct argp_child argp_children
[] = {
153 { &barvinok_argp
, 0, 0, 0 },
154 { &verify_argp
, 0, "verification", BV_GRP_LAST
+1 },
155 { &convert_argp
, 0, "output conversion", BV_GRP_LAST
+2 },
158 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
159 struct barvinok_options
*options
= barvinok_options_new_with_defaults();
161 arguments
.verify
.barvinok
= options
;
164 arguments
.parker
= 0;
166 arguments
.series
= 0;
167 arguments
.function
= 0;
169 set_program_name(argv
[0]);
170 argp_parse(&argp
, argc
, argv
, 0, 0, &arguments
);
173 A
= Constraints2Polyhedron(MA
, options
->MaxRays
);
177 while (next_line(stdin
, s
, sizeof(s
)))
178 if (sscanf(s
, "E %d", &exist
) == 1)
183 while (next_line(stdin
, s
, sizeof(s
)))
184 if (sscanf(s
, "P %d", &nparam
) == 1)
188 /******* Read the options: initialize Min and Max ********/
190 if (arguments
.verify
.verify
) {
191 verify_options_set_range(&arguments
.verify
, A
->Dimension
);
192 if (!options
->verbose
)
196 if (print_solution
&& options
->verbose
) {
197 Polyhedron_Print(stdout
, P_VALUE_FMT
, A
);
198 printf("exist: %d, nparam: %d\n", exist
, nparam
);
200 param_name
= Read_ParamNames(stdin
, nparam
);
201 nvar
= A
->Dimension
- exist
- nparam
;
202 if (arguments
.omega
) {
203 A
= Omega_simplify(A
, exist
, nparam
, param_name
, options
->MaxRays
);
205 exist
= A
->Dimension
- nvar
- nparam
;
207 if (arguments
.series
) {
209 gf
= barvinok_enumerate_scarf_series(A
, exist
, nparam
, options
);
211 gf
= barvinok_enumerate_e_series(A
, exist
, nparam
, options
);
212 if (print_solution
) {
213 gf
->print(std::cout
, nparam
, param_name
);
216 if (arguments
.function
) {
219 print_evalue(stdout
, EP
, param_name
);
222 if (arguments
.parker
)
223 EP
= barvinok_enumerate_parker(A
, A
->Dimension
-nparam
-exist
,
224 nparam
, options
->MaxRays
);
225 else if (arguments
.scarf
)
226 EP
= barvinok_enumerate_scarf(A
, exist
, nparam
, options
);
227 else if (arguments
.isl
&& exist
> 0)
228 EP
= barvinok_enumerate_isl(A
, exist
, nparam
, options
);
230 EP
= barvinok_enumerate_e_with_options(A
, exist
, nparam
, options
);
232 if (evalue_convert(EP
, &arguments
.convert
, options
->verbose
, nparam
,
236 print_evalue(stdout
, EP
, param_name
);
238 if (arguments
.verify
.verify
) {
239 arguments
.verify
.params
= param_name
;
240 verify_results(A
, EP
, gf
, exist
, nparam
, &arguments
);
247 if (options
->print_stats
)
248 barvinok_stats_print(options
->stats
, stdout
);
250 Free_ParamNames(param_name
, nparam
);
252 barvinok_options_free(options
);
256 void verify_results(Polyhedron
*P
, evalue
*EP
, gen_fun
*gf
,
257 int exist
, int nparam
,
265 unsigned MaxRays
= options
->verify
.barvinok
->MaxRays
;
266 Polyhedron
*C
= NULL
;
269 p
= Vector_Alloc(P
->Dimension
+2);
270 value_set_si(p
->p
[P
->Dimension
+1], 1);
272 CS
= check_poly_context_scan(P
, &C
, nparam
, &options
->verify
);
274 C
= Universe_Polyhedron(nparam
);
276 /* S = scanning list of polyhedra */
277 S
= Polyhedron_Scan(P
, C
, MaxRays
& POL_NO_DUAL
? 0 : MaxRays
);
279 check_poly_init(C
, &options
->verify
);
281 /******* CHECK NOW *********/
283 if (!options
->series
|| options
->function
) {
284 if (!check_poly_EP(S
, CS
, EP
, exist
, nparam
, 0, p
->p
,
288 skewed_gen_fun
*sgf
= new skewed_gen_fun(new gen_fun(gf
));
289 if (!check_poly_gf(S
, CS
, sgf
, exist
, nparam
, 0, p
->p
,
296 if (!options
->verify
.print_all
)