barvinok_enumerate_e: support verification of generating functions
[barvinok.git] / barvinok_enumerate_e.cc
blob02ac868da4b24a2309cd948513ae256e7276a411
1 #include <unistd.h>
2 #include <stdlib.h>
3 #include <assert.h>
4 #include <barvinok/util.h>
5 #include <barvinok/barvinok.h>
6 #include "argp.h"
7 #include "progname.h"
8 #include "error.h"
9 #include "config.h"
10 #ifdef HAVE_OMEGA
11 #include "omega/convert.h"
12 #endif
13 #include "skewed_genfun.h"
14 #include "verify.h"
15 #include "verif_ehrhart.h"
16 #include "verify_series.h"
17 #include "evalue_convert.h"
19 /* The input of this example program is a polytope in combined
20 * data and parameter space followed by two lines indicating
21 * the number of existential variables and parameters respectively.
22 * The first lines starts with "E ", followed by a number.
23 * The second lines starts with "P ", followed by a number.
24 * These two lines are (optionally) followed by the names of the parameters.
25 * The polytope is in PolyLib notation.
28 struct argp_option argp_options[] = {
29 { "omega", 'o', 0, 0 },
30 { "pip", 'p', 0, 0 },
31 { "series", 's', 0, 0 },
32 { "series", 's', 0, 0, "compute rational generating function" },
33 { "explicit", 'e', 0, 0, "convert rgf to psp" },
34 { "scarf", 'S', 0, 0 },
35 { "verbose", 'v' },
36 { 0 }
39 struct arguments {
40 struct verify_options verify;
41 struct convert_options convert;
42 int omega;
43 int pip;
44 int scarf;
45 int series;
46 int verbose;
47 int function;
50 error_t parse_opt(int key, char *arg, struct argp_state *state)
52 struct arguments *arguments = (struct arguments *)(state->input);
54 switch (key) {
55 case ARGP_KEY_INIT:
56 state->child_inputs[0] = arguments->verify.barvinok;
57 state->child_inputs[1] = &arguments->verify;
58 state->child_inputs[2] = &arguments->convert;
59 break;
60 case 'e':
61 arguments->function = 1;
62 /* fall through */
63 case 's':
64 arguments->series = 1;
65 break;
66 case 'S':
67 arguments->scarf = 1;
68 break;
69 case 'o':
70 #ifdef HAVE_OMEGA
71 arguments->omega = 1;
72 #else
73 error(0, 0, "--omega option not supported");
74 #endif
75 break;
76 case 'p':
77 arguments->pip = 1;
78 break;
79 case 'v':
80 arguments->verbose = 1;
81 break;
82 default:
83 return ARGP_ERR_UNKNOWN;
85 return 0;
88 #ifdef HAVE_OMEGA
90 Polyhedron *Omega_simplify(Polyhedron *P,
91 unsigned exist, unsigned nparam, char **parms)
93 varvector varv;
94 varvector paramv;
95 Relation r = Polyhedron2relation(P, exist, nparam, parms);
96 Polyhedron_Free(P);
97 return relation2Domain(r, varv, paramv);
99 #else
100 Polyhedron *Omega_simplify(Polyhedron *P,
101 unsigned exist, unsigned nparam, char **parms)
103 return P;
105 #endif
107 static void verify_results(Polyhedron *P, evalue *EP, gen_fun *gf,
108 int exist, int nparam,
109 arguments *options);
111 int main(int argc, char **argv)
113 Polyhedron *A;
114 Matrix *MA;
115 char **param_name;
116 int exist, nparam, nvar;
117 char s[128];
118 evalue *EP = NULL;
119 gen_fun *gf = NULL;
120 int print_solution = 1;
121 struct arguments arguments;
122 static struct argp_child argp_children[] = {
123 { &barvinok_argp, 0, 0, 0 },
124 { &verify_argp, 0, "verification", BV_GRP_LAST+1 },
125 { &convert_argp, 0, "output conversion", BV_GRP_LAST+2 },
126 { 0 }
128 static struct argp argp = { argp_options, parse_opt, 0, 0, argp_children };
129 struct barvinok_options *options = barvinok_options_new_with_defaults();
131 arguments.verify.barvinok = options;
132 arguments.omega = 0;
133 arguments.pip = 0;
134 arguments.scarf = 0;
135 arguments.series = 0;
136 arguments.function = 0;
137 arguments.verbose = 0;
139 set_program_name(argv[0]);
140 argp_parse(&argp, argc, argv, 0, 0, &arguments);
142 if (arguments.series && !arguments.scarf) {
143 fprintf(stderr,
144 "--series currently only available if --scarf is specified\n");
145 exit(1);
148 MA = Matrix_Read();
149 A = Constraints2Polyhedron(MA, options->MaxRays);
150 Matrix_Free(MA);
152 fgets(s, 128, stdin);
153 while ((*s=='#') || (sscanf(s, "E %d", &exist)<1))
154 fgets(s, 128, stdin);
156 fgets(s, 128, stdin);
157 while ((*s=='#') || (sscanf(s, "P %d", &nparam)<1))
158 fgets(s, 128, stdin);
160 /******* Read the options: initialize Min and Max ********/
162 if (arguments.verify.verify) {
163 verify_options_set_range(&arguments.verify, A->Dimension);
164 if (!arguments.verbose)
165 print_solution = 0;
168 if (print_solution && arguments.verbose) {
169 Polyhedron_Print(stdout, P_VALUE_FMT, A);
170 printf("exist: %d, nparam: %d\n", exist, nparam);
172 param_name = Read_ParamNames(stdin, nparam);
173 nvar = A->Dimension - exist - nparam;
174 if (arguments.omega) {
175 A = Omega_simplify(A, exist, nparam, param_name);
176 assert(!A->next);
177 exist = A->Dimension - nvar - nparam;
179 if (arguments.series) {
180 assert(arguments.scarf);
181 gf = barvinok_enumerate_scarf_series(A, exist, nparam, options);
182 if (print_solution) {
183 gf->print(std::cout, nparam, param_name);
184 puts("");
186 if (arguments.function) {
187 EP = *gf;
188 if (print_solution)
189 print_evalue(stdout, EP, param_name);
191 } else {
192 if (arguments.scarf)
193 EP = barvinok_enumerate_scarf(A, exist, nparam, options);
194 else if (arguments.pip && exist > 0)
195 EP = barvinok_enumerate_pip_with_options(A, exist, nparam, options);
196 else
197 EP = barvinok_enumerate_e_with_options(A, exist, nparam, options);
198 reduce_evalue(EP);
199 if (evalue_convert(EP, &arguments.convert, arguments.verbose, nparam,
200 param_name))
201 print_solution = 0;
202 if (print_solution)
203 print_evalue(stdout, EP, param_name);
205 if (arguments.verify.verify) {
206 arguments.verify.params = param_name;
207 verify_results(A, EP, gf, exist, nparam, &arguments);
209 if (gf)
210 delete gf;
211 if (EP)
212 evalue_free(EP);
213 Free_ParamNames(param_name, nparam);
214 Polyhedron_Free(A);
215 barvinok_options_free(options);
216 return 0;
219 void verify_results(Polyhedron *P, evalue *EP, gen_fun *gf,
220 int exist, int nparam,
221 arguments *options)
223 int i;
224 int res = 0;
225 Vector *p;
226 Value tmp;
227 Polyhedron *S, *CS;
228 unsigned MaxRays = options->verify.barvinok->MaxRays;
229 Polyhedron *C = NULL;
230 value_init(tmp);
232 p = Vector_Alloc(P->Dimension+2);
233 value_set_si(p->p[P->Dimension+1], 1);
235 CS = check_poly_context_scan(P, &C, nparam, &options->verify);
237 /* S = scanning list of polyhedra */
238 S = Polyhedron_Scan(P, C, MaxRays & POL_NO_DUAL ? 0 : MaxRays);
240 check_poly_init(C, &options->verify);
242 /******* CHECK NOW *********/
243 if (S) {
244 if (!options->series || options->function) {
245 if (!check_poly_EP(S, CS, EP, exist, nparam, 0, p->p,
246 &options->verify))
247 res = -1;
248 } else {
249 skewed_gen_fun *sgf = new skewed_gen_fun(new gen_fun(gf));
250 if (!check_poly_gf(S, CS, sgf, exist, nparam, 0, p->p,
251 &options->verify))
252 res = -1;
253 delete sgf;
257 if (!options->verify.print_all)
258 printf( "\n" );
260 Vector_Free(p);
261 value_clear(tmp);
262 Domain_Free(S);
263 Polyhedron_Free(C);
264 if (CS)
265 Domain_Free(CS);