barvinok_enumerate_e_series: handle all equalities involving existentials
[barvinok.git] / series.cc
blob1eec2740e7209aac00b4ac8b0f6250d0e51eacd2
1 #include <assert.h>
2 #include <barvinok/barvinok.h>
3 #include <barvinok/util.h>
4 #include "genfun_constructor.h"
5 #include "lattice_width.h"
6 #include "remove_equalities.h"
8 using std::cerr;
9 using std::endl;
11 /* Check whether all rays point in the positive directions
12 * for the parameters
14 static bool Polyhedron_has_positive_rays(Polyhedron *P, unsigned nparam)
16 int r;
17 for (r = 0; r < P->NbRays; ++r)
18 if (value_zero_p(P->Ray[r][P->Dimension+1])) {
19 int i;
20 for (i = P->Dimension - nparam; i < P->Dimension; ++i)
21 if (value_neg_p(P->Ray[r][i+1]))
22 return false;
24 return true;
27 gen_fun *barvinok_enumerate_series(Polyhedron *P, unsigned nparam,
28 barvinok_options *options)
30 Matrix *CP = NULL;
31 gen_fun *gf;
32 Polyhedron *P_orig = P;
34 if (emptyQ2(P))
35 return new gen_fun(Empty_Polyhedron(nparam));
37 assert(!Polyhedron_is_unbounded(P, nparam, options->MaxRays));
38 assert(P->NbBid == 0);
39 assert(Polyhedron_has_revlex_positive_rays(P, nparam));
40 if (P->NbEq != 0)
41 remove_all_equalities(&P, NULL, &CP, NULL, nparam, options->MaxRays);
42 assert(emptyQ2(P) || P->NbEq == 0);
43 if (CP)
44 nparam = CP->NbColumns-1;
46 if (nparam == 0) {
47 Value c;
48 value_init(c);
49 barvinok_count_with_options(P, &c, options);
50 gf = new gen_fun(c);
51 value_clear(c);
52 } else {
53 POL_ENSURE_VERTICES(P);
54 if (P->NbEq)
55 gf = barvinok_enumerate_series(P, nparam, options);
56 else {
57 gf_base *red;
58 red = gf_base::create(Polyhedron_Project(P, nparam),
59 P->Dimension, nparam, options);
60 red->start_gf(P, options);
61 gf = red->gf;
62 delete red;
65 if (CP) {
66 gf->substitute(CP);
67 Matrix_Free(CP);
69 if (P != P_orig)
70 Polyhedron_Free(P);
71 return gf;
74 gen_fun * barvinok_series_with_options(Polyhedron *P, Polyhedron* C,
75 barvinok_options *options)
77 Polyhedron *CA;
78 unsigned nparam = C->Dimension;
79 gen_fun *gf;
81 CA = align_context(C, P->Dimension, options->MaxRays);
82 P = DomainIntersection(P, CA, options->MaxRays);
83 Polyhedron_Free(CA);
85 gf = barvinok_enumerate_series(P, nparam, options);
86 Polyhedron_Free(P);
88 return gf;
91 gen_fun * barvinok_series(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
93 gen_fun *gf;
94 barvinok_options *options = barvinok_options_new_with_defaults();
95 options->MaxRays = MaxRays;
96 gf = barvinok_series_with_options(P, C, options);
97 barvinok_options_free(options);
98 return gf;
101 static Polyhedron *skew_into_positive_orthant(Polyhedron *D, unsigned nparam,
102 unsigned MaxRays)
104 Matrix *M = NULL;
105 Value tmp;
106 value_init(tmp);
107 for (Polyhedron *P = D; P; P = P->next) {
108 POL_ENSURE_VERTICES(P);
109 assert(!Polyhedron_is_unbounded(P, nparam, MaxRays));
110 assert(P->NbBid == 0);
111 assert(Polyhedron_has_positive_rays(P, nparam));
113 for (int r = 0; r < P->NbRays; ++r) {
114 if (value_notzero_p(P->Ray[r][P->Dimension+1]))
115 continue;
116 for (int i = 0; i < nparam; ++i) {
117 int j;
118 if (value_posz_p(P->Ray[r][i+1]))
119 continue;
120 if (!M) {
121 M = Matrix_Alloc(D->Dimension+1, D->Dimension+1);
122 for (int i = 0; i < D->Dimension+1; ++i)
123 value_set_si(M->p[i][i], 1);
124 } else {
125 Inner_Product(P->Ray[r]+1, M->p[i], D->Dimension+1, &tmp);
126 if (value_posz_p(tmp))
127 continue;
129 for (j = P->Dimension - nparam; j < P->Dimension; ++j)
130 if (value_pos_p(P->Ray[r][j+1]))
131 break;
132 assert(j < P->Dimension);
133 value_pdivision(tmp, P->Ray[r][j+1], P->Ray[r][i+1]);
134 value_subtract(M->p[i][j], M->p[i][j], tmp);
138 value_clear(tmp);
139 if (M) {
140 D = DomainImage(D, M, MaxRays);
141 Matrix_Free(M);
143 return D;
146 gen_fun* barvinok_enumerate_union_series_with_options(Polyhedron *D, Polyhedron* C,
147 barvinok_options *options)
149 Polyhedron *conv, *D2;
150 Polyhedron *CA;
151 gen_fun *gf = NULL, *gf2;
152 unsigned nparam = C->Dimension;
153 ZZ one, mone;
154 one = 1;
155 mone = -1;
157 CA = align_context(C, D->Dimension, options->MaxRays);
158 D = DomainIntersection(D, CA, options->MaxRays);
159 Polyhedron_Free(CA);
161 D2 = skew_into_positive_orthant(D, nparam, options->MaxRays);
162 for (Polyhedron *P = D2; P; P = P->next) {
163 assert(P->Dimension == D2->Dimension);
164 gen_fun *P_gf;
166 P_gf = barvinok_enumerate_series(P, P->Dimension, options);
167 if (!gf)
168 gf = P_gf;
169 else {
170 gf->add_union(P_gf, options);
171 delete P_gf;
174 /* we actually only need the convex union of the parameter space
175 * but the reducer classes currently expect a polyhedron in
176 * the combined space
178 Polyhedron_Free(gf->context);
179 gf->context = DomainConvex(D2, options->MaxRays);
181 gf2 = gf->summate(D2->Dimension - nparam, options);
183 delete gf;
184 if (D != D2)
185 Domain_Free(D2);
186 Domain_Free(D);
187 return gf2;
190 gen_fun* barvinok_enumerate_union_series(Polyhedron *D, Polyhedron* C,
191 unsigned MaxRays)
193 gen_fun *gf;
194 barvinok_options *options = barvinok_options_new_with_defaults();
195 options->MaxRays = MaxRays;
196 gf = barvinok_enumerate_union_series_with_options(D, C, options);
197 barvinok_options_free(options);
198 return gf;
201 /* Unimodularly transform the polyhedron P, such that
202 * the direction specified by dir corresponds to the last
203 * variable in the transformed polyhedron.
204 * The number of variables is given by the length of dir.
206 static Polyhedron *put_direction_last(Polyhedron *P, Vector *dir,
207 unsigned MaxRays)
209 Polyhedron *R;
210 Matrix *T;
211 int n = dir->Size;
213 T = Matrix_Alloc(P->Dimension+1, P->Dimension+1);
214 T->NbColumns = T->NbRows = n;
215 Vector_Copy(dir->p, T->p[0], n);
216 unimodular_complete(T, 1);
217 Vector_Exchange(T->p[0], T->p[n-1], n);
218 T->NbColumns = T->NbRows = P->Dimension+1;
219 for (int j = n; j < P->Dimension+1; ++j)
220 value_set_si(T->p[j][j], 1);
222 R = Polyhedron_Image(P, T, MaxRays);
223 Matrix_Free(T);
225 return R;
228 /* Do we need to continue shifting and subtracting?
229 * i is the number of times we shifted so far
230 * n is the number of coordinates projected out
232 static bool more_shifts_needed(int j, int n,
233 gen_fun *S, gen_fun *S_divide, const vec_ZZ& up,
234 barvinok_options *options)
236 bool empty;
237 gen_fun *hp;
238 Value c;
240 /* For the 2-dimensional case, we need to subtract at most once */
241 if (n == 2 && j > 0)
242 return false;
244 S_divide->shift(up);
246 /* Assume that we have to subtract at least once */
247 if (j == 0)
248 return true;
250 hp = S->Hadamard_product(S_divide, options);
252 value_init(c);
254 empty = hp->summate(&c) && value_zero_p(c);
255 delete hp;
257 value_clear(c);
259 return !empty;
262 /* Return gf of P projected on last dim(P)-n coordinates, i.e.,
263 * project out the first n coordinates.
265 gen_fun *project(Polyhedron *P, unsigned n, barvinok_options *options)
267 QQ one(1, 1);
268 QQ mone(-1, 1);
269 vec_ZZ up;
270 gen_fun *gf = NULL;
271 struct width_direction_array *dirs;
272 Polyhedron *U;
274 up.SetLength(P->Dimension - (n-1));
275 up[0] = 1;
276 for (int i = 1; i < P->Dimension - (n-1); ++i)
277 up[i] = 0;
279 if (n == 1) {
280 gen_fun *S, *S_shift, *hp;
282 S = barvinok_enumerate_series(P, P->Dimension, options);
283 S_shift = new gen_fun(S);
284 S_shift->shift(up);
285 hp = S->Hadamard_product(S_shift, options);
286 S->add(mone, hp, options);
287 delete S_shift;
288 delete hp;
290 gf = S->summate(1, options);
291 delete S;
293 return gf;
296 U = Universe_Polyhedron(P->Dimension - n);
297 dirs = Polyhedron_Lattice_Width_Directions(P, U, options);
298 Polyhedron_Free(U);
300 for (int i = 0; i < dirs->n; ++i) {
301 Polyhedron *Pi, *R;
302 Polyhedron *CA;
303 gen_fun *S, *S_shift, *S_divide, *sum;
305 CA = align_context(dirs->wd[i].domain, P->Dimension, options->MaxRays);
306 R = DomainIntersection(P, CA, options->MaxRays);
307 Polyhedron_Free(CA);
308 assert(dirs->wd[i].dir->Size == n);
309 Pi = put_direction_last(R, dirs->wd[i].dir, options->MaxRays);
310 Polyhedron_Free(R);
312 S = project(Pi, n-1, options);
313 Polyhedron_Free(Pi);
315 S_shift = new gen_fun(S);
316 S_divide = new gen_fun(S);
317 S_divide->divide(up);
319 for (int j = 0; more_shifts_needed(j, n, S, S_divide, up, options); ++j) {
320 gen_fun *hp;
322 S_shift->shift(up);
323 hp = S->Hadamard_product(S_shift, options);
324 S->add(mone, hp, options);
326 delete hp;
329 sum = S->summate(1, options);
331 delete S_shift;
332 delete S_divide;
333 delete S;
335 if (!gf)
336 gf = sum;
337 else {
338 gf->add(one, sum, options);
339 delete sum;
342 free_width_direction_array(dirs);
344 return gf;
347 gen_fun *barvinok_enumerate_e_series(Polyhedron *P,
348 unsigned exist, unsigned nparam, barvinok_options *options)
350 Matrix *CP = NULL;
351 Polyhedron *P_orig = P;
352 gen_fun *gf, *proj;
353 unsigned nvar = P->Dimension - exist - nparam;
355 if (exist == 0)
356 return barvinok_enumerate_series(P, nparam, options);
358 if (emptyQ(P))
359 return new gen_fun(Empty_Polyhedron(nparam));
361 assert(!Polyhedron_is_unbounded(P, nparam, options->MaxRays));
362 assert(P->NbBid == 0);
363 assert(Polyhedron_has_revlex_positive_rays(P, nparam));
365 /* Move existentially quantified variables to the front.*/
366 if (nvar) {
367 Matrix *T;
368 T = Matrix_Alloc(exist+nvar+nparam+1, nvar+exist+nparam+1);
369 for (int i = 0; i < exist; ++i)
370 value_set_si(T->p[i][nvar+i], 1);
371 for (int i = 0; i < nvar; ++i)
372 value_set_si(T->p[exist+i][i], 1);
373 for (int i = 0; i < nparam+1; ++i)
374 value_set_si(T->p[exist+nvar+i][nvar+exist+i], 1);
375 P = Polyhedron_Image(P, T, options->MaxRays);
376 Matrix_Free(T);
378 if (P->NbEq != 0) {
379 Polyhedron *Q = P;
380 remove_all_equalities(&P, NULL, &CP, NULL, nvar+nparam,
381 options->MaxRays);
382 if (CP)
383 exist = P->Dimension - (CP->NbColumns-1);
384 else
385 exist = P->Dimension - (nvar + nparam);
386 if (Q != P_orig)
387 Polyhedron_Free(Q);
390 proj = project(P, exist, options);
391 if (CP) {
392 proj->substitute(CP);
393 Matrix_Free(CP);
396 if (P != P_orig)
397 Polyhedron_Free(P);
399 if (!nvar)
400 gf = proj;
401 else {
402 gf = proj->summate(nvar, options);
403 delete proj;
405 return gf;