iscc: add lexicographic operators
[barvinok.git] / barvinok_enumerate_e.cc
blobc2f991888ecc40df3f21d553e1fdf665a7f5f54b
1 #include <ctype.h>
2 #include <unistd.h>
3 #include <stdlib.h>
4 #include <assert.h>
5 #include <barvinok/util.h>
6 #include <barvinok/barvinok.h>
7 #include "config.h"
8 #ifdef HAVE_OMEGA
9 #include "omega_interface/convert.h"
10 #include "omega_interface/count.h"
11 #endif
12 #include "skewed_genfun.h"
13 #include "verify.h"
14 #include "verif_ehrhart.h"
15 #include "verify_series.h"
16 #include "evalue_convert.h"
17 #include "barvinok_enumerate_e_options.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 #ifdef HAVE_OMEGA
30 Polyhedron *Omega_simplify(Polyhedron *P,
31 unsigned exist, unsigned nparam, const char **parms,
32 unsigned MaxRays)
34 varvector varv;
35 varvector paramv;
36 Relation r = Polyhedron2relation(P, exist, nparam, parms);
37 Polyhedron_Free(P);
38 return relation2Domain(r, varv, paramv, MaxRays);
40 #else
41 Polyhedron *Omega_simplify(Polyhedron *P,
42 unsigned exist, unsigned nparam, const char **parms,
43 unsigned MaxRays)
45 return P;
48 evalue *barvinok_enumerate_parker(Polyhedron *P,
49 unsigned exist, unsigned nparam,
50 unsigned MaxRays)
52 assert(0);
53 return NULL;
55 #endif
57 static void verify_results(Polyhedron *P, evalue *EP, gen_fun *gf,
58 int exist, int nparam,
59 enumerate_e_options *options);
61 static char *next_line(FILE *input, char *line, unsigned len)
63 char *p;
65 do {
66 if (!(p = fgets(line, len, input)))
67 return NULL;
68 while (isspace(*p) && *p != '\n')
69 ++p;
70 } while (*p == '#' || *p == '\n');
72 return p;
75 int main(int argc, char **argv)
77 Polyhedron *A;
78 Matrix *MA;
79 const char **param_name;
80 int exist, nparam, nvar;
81 char s[128];
82 evalue *EP = NULL;
83 gen_fun *gf = NULL;
84 int print_solution = 1;
85 struct enumerate_e_options *options = enumerate_e_options_new_with_defaults();
87 argc = enumerate_e_options_parse(options, argc, argv, ISL_ARG_ALL);
89 MA = Matrix_Read();
90 A = Constraints2Polyhedron(MA, options->verify->barvinok->MaxRays);
91 Matrix_Free(MA);
93 exist = -1;
94 while (next_line(stdin, s, sizeof(s)))
95 if (sscanf(s, "E %d", &exist) == 1)
96 break;
97 assert(exist >= 0);
99 nparam = -1;
100 while (next_line(stdin, s, sizeof(s)))
101 if (sscanf(s, "P %d", &nparam) == 1)
102 break;
103 assert(nparam >= 0);
105 /******* Read the options: initialize Min and Max ********/
107 if (options->verify->verify) {
108 verify_options_set_range(options->verify, A->Dimension);
109 if (!options->verify->barvinok->verbose)
110 print_solution = 0;
113 if (print_solution && options->verify->barvinok->verbose) {
114 Polyhedron_Print(stdout, P_VALUE_FMT, A);
115 printf("exist: %d, nparam: %d\n", exist, nparam);
117 param_name = Read_ParamNames(stdin, nparam);
118 nvar = A->Dimension - exist - nparam;
119 if (options->omega) {
120 A = Omega_simplify(A, exist, nparam, param_name,
121 options->verify->barvinok->MaxRays);
122 assert(!A->next);
123 exist = A->Dimension - nvar - nparam;
125 if (options->series) {
126 if (options->scarf)
127 gf = barvinok_enumerate_scarf_series(A, exist, nparam,
128 options->verify->barvinok);
129 else
130 gf = barvinok_enumerate_e_series(A, exist, nparam,
131 options->verify->barvinok);
132 if (print_solution) {
133 gf->print(std::cout, nparam, param_name);
134 puts("");
136 if (options->function) {
137 EP = *gf;
138 if (print_solution)
139 print_evalue(stdout, EP, param_name);
141 } else {
142 if (options->parker)
143 EP = barvinok_enumerate_parker(A, A->Dimension-nparam-exist, nparam,
144 options->verify->barvinok->MaxRays);
145 else if (options->scarf)
146 EP = barvinok_enumerate_scarf(A, exist, nparam,
147 options->verify->barvinok);
148 else if (options->isl && exist > 0)
149 EP = barvinok_enumerate_isl(A, exist, nparam,
150 options->verify->barvinok);
151 else
152 EP = barvinok_enumerate_e_with_options(A, exist, nparam,
153 options->verify->barvinok);
154 reduce_evalue(EP);
155 if (evalue_convert(EP, options->convert,
156 options->verify->barvinok->verbose, nparam, param_name))
157 print_solution = 0;
158 if (print_solution)
159 print_evalue(stdout, EP, param_name);
161 if (options->verify->verify) {
162 options->verify->params = param_name;
163 verify_results(A, EP, gf, exist, nparam, options);
165 if (gf)
166 delete gf;
167 if (EP)
168 evalue_free(EP);
170 if (options->verify->barvinok->print_stats)
171 barvinok_stats_print(options->verify->barvinok->stats, stdout);
173 Free_ParamNames(param_name, nparam);
174 Polyhedron_Free(A);
175 enumerate_e_options_free(options);
176 return 0;
179 void verify_results(Polyhedron *P, evalue *EP, gen_fun *gf,
180 int exist, int nparam,
181 enumerate_e_options *options)
183 int i;
184 int res = 0;
185 Vector *p;
186 Value tmp;
187 Polyhedron *S, *CS;
188 unsigned MaxRays = options->verify->barvinok->MaxRays;
189 Polyhedron *C = NULL;
190 value_init(tmp);
192 p = Vector_Alloc(P->Dimension+2);
193 value_set_si(p->p[P->Dimension+1], 1);
195 CS = check_poly_context_scan(P, &C, nparam, options->verify);
196 if (!C)
197 C = Universe_Polyhedron(nparam);
199 /* S = scanning list of polyhedra */
200 S = Polyhedron_Scan(P, C, MaxRays & POL_NO_DUAL ? 0 : MaxRays);
202 check_poly_init(C, options->verify);
204 /******* CHECK NOW *********/
205 if (S) {
206 if (!options->series || options->function) {
207 if (!check_poly_EP(S, CS, EP, exist, nparam, 0, p->p,
208 options->verify))
209 res = -1;
210 } else {
211 skewed_gen_fun *sgf = new skewed_gen_fun(new gen_fun(gf));
212 if (!check_poly_gf(S, CS, sgf, exist, nparam, 0, p->p,
213 options->verify))
214 res = -1;
215 delete sgf;
219 if (!options->verify->print_all)
220 printf( "\n" );
222 Vector_Free(p);
223 value_clear(tmp);
224 Domain_Free(S);
225 Polyhedron_Free(C);
226 if (CS)
227 Domain_Free(CS);