don't make numerator power positive + merge loops
[barvinok.git] / barvinok.cc
blob248e6f9460b9847cb4a750ac6681bdeb0a1ce01b
1 #include <assert.h>
2 #include <iostream>
3 #include <vector>
4 #include <deque>
5 #include <string>
6 #include <sstream>
7 #include <gmp.h>
8 #include <NTL/mat_ZZ.h>
9 #include <NTL/LLL.h>
10 #include <util.h>
11 extern "C" {
12 #include <polylib/polylibgmp.h>
13 #include "ev_operations.h"
14 #include "piputil.h"
16 #include "config.h"
17 #include <barvinok.h>
19 #ifdef NTL_STD_CXX
20 using namespace NTL;
21 #endif
22 using std::cout;
23 using std::endl;
24 using std::vector;
25 using std::deque;
26 using std::string;
27 using std::ostringstream;
29 #define ALLOC(p) (((long *) (p))[0])
30 #define SIZE(p) (((long *) (p))[1])
31 #define DATA(p) ((mp_limb_t *) (((long *) (p)) + 2))
33 static void value2zz(Value v, ZZ& z)
35 int sa = v[0]._mp_size;
36 int abs_sa = sa < 0 ? -sa : sa;
38 _ntl_gsetlength(&z.rep, abs_sa);
39 mp_limb_t * adata = DATA(z.rep);
40 for (int i = 0; i < abs_sa; ++i)
41 adata[i] = v[0]._mp_d[i];
42 SIZE(z.rep) = sa;
45 static void zz2value(ZZ& z, Value& v)
47 if (!z.rep) {
48 value_set_si(v, 0);
49 return;
52 int sa = SIZE(z.rep);
53 int abs_sa = sa < 0 ? -sa : sa;
55 mp_limb_t * adata = DATA(z.rep);
56 _mpz_realloc(v, abs_sa);
57 for (int i = 0; i < abs_sa; ++i)
58 v[0]._mp_d[i] = adata[i];
59 v[0]._mp_size = sa;
62 #undef ALLOC
63 #define ALLOC(t,p) p = (t*)malloc(sizeof(*p))
66 * We just ignore the last column and row
67 * If the final element is not equal to one
68 * then the result will actually be a multiple of the input
70 static void matrix2zz(Matrix *M, mat_ZZ& m, unsigned nr, unsigned nc)
72 m.SetDims(nr, nc);
74 for (int i = 0; i < nr; ++i) {
75 // assert(value_one_p(M->p[i][M->NbColumns - 1]));
76 for (int j = 0; j < nc; ++j) {
77 value2zz(M->p[i][j], m[i][j]);
82 static void values2zz(Value *p, vec_ZZ& v, int len)
84 v.SetLength(len);
86 for (int i = 0; i < len; ++i) {
87 value2zz(p[i], v[i]);
93 static void zz2values(vec_ZZ& v, Value *p)
95 for (int i = 0; i < v.length(); ++i)
96 zz2value(v[i], p[i]);
99 static void rays(mat_ZZ& r, Polyhedron *C)
101 unsigned dim = C->NbRays - 1; /* don't count zero vertex */
102 assert(C->NbRays - 1 == C->Dimension);
103 r.SetDims(dim, dim);
104 ZZ tmp;
106 int i, c;
107 for (i = 0, c = 0; i < dim; ++i)
108 if (value_zero_p(C->Ray[i][dim+1])) {
109 for (int j = 0; j < dim; ++j) {
110 value2zz(C->Ray[i][j+1], tmp);
111 r[j][c] = tmp;
113 ++c;
117 static Matrix * rays(Polyhedron *C)
119 unsigned dim = C->NbRays - 1; /* don't count zero vertex */
120 assert(C->NbRays - 1 == C->Dimension);
122 Matrix *M = Matrix_Alloc(dim+1, dim+1);
123 assert(M);
125 int i, c;
126 for (i = 0, c = 0; i <= dim && c < dim; ++i)
127 if (value_zero_p(C->Ray[i][dim+1])) {
128 Vector_Copy(C->Ray[i] + 1, M->p[c], dim);
129 value_set_si(M->p[c++][dim], 0);
131 assert(c == dim);
132 value_set_si(M->p[dim][dim], 1);
134 return M;
137 static Matrix * rays2(Polyhedron *C)
139 unsigned dim = C->NbRays - 1; /* don't count zero vertex */
140 assert(C->NbRays - 1 == C->Dimension);
142 Matrix *M = Matrix_Alloc(dim, dim);
143 assert(M);
145 int i, c;
146 for (i = 0, c = 0; i <= dim && c < dim; ++i)
147 if (value_zero_p(C->Ray[i][dim+1]))
148 Vector_Copy(C->Ray[i] + 1, M->p[c++], dim);
149 assert(c == dim);
151 return M;
155 * Returns the largest absolute value in the vector
157 static ZZ max(vec_ZZ& v)
159 ZZ max = abs(v[0]);
160 for (int i = 1; i < v.length(); ++i)
161 if (abs(v[i]) > max)
162 max = abs(v[i]);
163 return max;
166 class cone {
167 public:
168 cone(Matrix *M) {
169 Cone = 0;
170 Rays = Matrix_Copy(M);
171 set_det();
173 cone(Polyhedron *C) {
174 Cone = Polyhedron_Copy(C);
175 Rays = rays(C);
176 set_det();
178 void set_det() {
179 mat_ZZ A;
180 matrix2zz(Rays, A, Rays->NbRows - 1, Rays->NbColumns - 1);
181 det = determinant(A);
182 Value v;
183 value_init(v);
184 zz2value(det, v);
185 value_clear(v);
188 Vector* short_vector(vec_ZZ& lambda) {
189 Matrix *M = Matrix_Copy(Rays);
190 Matrix *inv = Matrix_Alloc(M->NbRows, M->NbColumns);
191 int ok = Matrix_Inverse(M, inv);
192 assert(ok);
193 Matrix_Free(M);
195 ZZ det2;
196 mat_ZZ B;
197 mat_ZZ U;
198 matrix2zz(inv, B, inv->NbRows - 1, inv->NbColumns - 1);
199 long r = LLL(det2, B, U);
201 ZZ min = max(B[0]);
202 int index = 0;
203 for (int i = 1; i < B.NumRows(); ++i) {
204 ZZ tmp = max(B[i]);
205 if (tmp < min) {
206 min = tmp;
207 index = i;
211 Matrix_Free(inv);
213 lambda = B[index];
215 Vector *z = Vector_Alloc(U[index].length()+1);
216 assert(z);
217 zz2values(U[index], z->p);
218 value_set_si(z->p[U[index].length()], 0);
220 Value tmp;
221 value_init(tmp);
222 Polyhedron *C = poly();
223 int i;
224 for (i = 0; i < C->NbConstraints; ++i) {
225 Inner_Product(z->p, C->Constraint[i]+1, z->Size-1, &tmp);
226 if (value_pos_p(tmp))
227 break;
229 if (i == C->NbConstraints) {
230 value_set_si(tmp, -1);
231 Vector_Scale(z->p, z->p, tmp, z->Size-1);
233 value_clear(tmp);
234 return z;
237 ~cone() {
238 Polyhedron_Free(Cone);
239 Matrix_Free(Rays);
242 Polyhedron *poly() {
243 if (!Cone) {
244 Matrix *M = Matrix_Alloc(Rays->NbRows+1, Rays->NbColumns+1);
245 for (int i = 0; i < Rays->NbRows; ++i) {
246 Vector_Copy(Rays->p[i], M->p[i]+1, Rays->NbColumns);
247 value_set_si(M->p[i][0], 1);
249 Vector_Set(M->p[Rays->NbRows]+1, 0, Rays->NbColumns-1);
250 value_set_si(M->p[Rays->NbRows][0], 1);
251 value_set_si(M->p[Rays->NbRows][Rays->NbColumns], 1);
252 Cone = Rays2Polyhedron(M, M->NbRows+1);
253 assert(Cone->NbConstraints == Cone->NbRays);
254 Matrix_Free(M);
256 return Cone;
259 ZZ det;
260 Polyhedron *Cone;
261 Matrix *Rays;
264 class dpoly {
265 public:
266 vec_ZZ coeff;
267 dpoly(int d, ZZ& degree, int offset = 0) {
268 coeff.SetLength(d+1);
270 int min = d + offset;
271 if (degree >= 0 && degree < ZZ(INIT_VAL, min))
272 min = to_int(degree);
274 ZZ c = ZZ(INIT_VAL, 1);
275 if (!offset)
276 coeff[0] = c;
277 for (int i = 1; i <= min; ++i) {
278 c *= (degree -i + 1);
279 c /= i;
280 coeff[i-offset] = c;
283 void operator *= (dpoly& f) {
284 assert(coeff.length() == f.coeff.length());
285 vec_ZZ old = coeff;
286 coeff = f.coeff[0] * coeff;
287 for (int i = 1; i < coeff.length(); ++i)
288 for (int j = 0; i+j < coeff.length(); ++j)
289 coeff[i+j] += f.coeff[i] * old[j];
291 void div(dpoly& d, mpq_t count, ZZ& sign) {
292 int len = coeff.length();
293 Value tmp;
294 value_init(tmp);
295 mpq_t* c = new mpq_t[coeff.length()];
296 mpq_t qtmp;
297 mpq_init(qtmp);
298 for (int i = 0; i < len; ++i) {
299 mpq_init(c[i]);
300 zz2value(coeff[i], tmp);
301 mpq_set_z(c[i], tmp);
303 for (int j = 1; j <= i; ++j) {
304 zz2value(d.coeff[j], tmp);
305 mpq_set_z(qtmp, tmp);
306 mpq_mul(qtmp, qtmp, c[i-j]);
307 mpq_sub(c[i], c[i], qtmp);
310 zz2value(d.coeff[0], tmp);
311 mpq_set_z(qtmp, tmp);
312 mpq_div(c[i], c[i], qtmp);
314 if (sign == -1)
315 mpq_sub(count, count, c[len-1]);
316 else
317 mpq_add(count, count, c[len-1]);
319 value_clear(tmp);
320 mpq_clear(qtmp);
321 for (int i = 0; i < len; ++i)
322 mpq_clear(c[i]);
323 delete [] c;
327 class dpoly_n {
328 public:
329 Matrix *coeff;
330 ~dpoly_n() {
331 Matrix_Free(coeff);
333 dpoly_n(int d, ZZ& degree_0, ZZ& degree_1, int offset = 0) {
334 Value d0, d1;
335 value_init(d0);
336 value_init(d1);
337 zz2value(degree_0, d0);
338 zz2value(degree_1, d1);
339 coeff = Matrix_Alloc(d+1, d+1+1);
340 value_set_si(coeff->p[0][0], 1);
341 value_set_si(coeff->p[0][d+1], 1);
342 for (int i = 1; i <= d; ++i) {
343 value_multiply(coeff->p[i][0], coeff->p[i-1][0], d0);
344 Vector_Combine(coeff->p[i-1], coeff->p[i-1]+1, coeff->p[i]+1,
345 d1, d0, i);
346 value_set_si(coeff->p[i][d+1], i);
347 value_multiply(coeff->p[i][d+1], coeff->p[i][d+1], coeff->p[i-1][d+1]);
348 value_decrement(d0, d0);
350 value_clear(d0);
351 value_clear(d1);
353 void div(dpoly& d, Vector *count, ZZ& sign) {
354 int len = coeff->NbRows;
355 Matrix * c = Matrix_Alloc(coeff->NbRows, coeff->NbColumns);
356 Value tmp;
357 value_init(tmp);
358 for (int i = 0; i < len; ++i) {
359 Vector_Copy(coeff->p[i], c->p[i], len+1);
360 for (int j = 1; j <= i; ++j) {
361 zz2value(d.coeff[j], tmp);
362 value_multiply(tmp, tmp, c->p[i][len]);
363 value_oppose(tmp, tmp);
364 Vector_Combine(c->p[i], c->p[i-j], c->p[i],
365 c->p[i-j][len], tmp, len);
366 value_multiply(c->p[i][len], c->p[i][len], c->p[i-j][len]);
368 zz2value(d.coeff[0], tmp);
369 value_multiply(c->p[i][len], c->p[i][len], tmp);
371 if (sign == -1) {
372 value_set_si(tmp, -1);
373 Vector_Scale(c->p[len-1], count->p, tmp, len);
374 value_assign(count->p[len], c->p[len-1][len]);
375 } else
376 Vector_Copy(c->p[len-1], count->p, len+1);
377 Vector_Normalize(count->p, len+1);
378 value_clear(tmp);
379 Matrix_Free(c);
384 * Barvinok's Decomposition of a simplicial cone
386 * Returns two lists of polyhedra
388 void barvinok_decompose(Polyhedron *C, Polyhedron **ppos, Polyhedron **pneg)
390 Polyhedron *pos = *ppos, *neg = *pneg;
391 vector<cone *> nonuni;
392 cone * c = new cone(C);
393 ZZ det = c->det;
394 int s = sign(det);
395 assert(det != 0);
396 if (abs(det) > 1) {
397 nonuni.push_back(c);
398 } else {
399 Polyhedron *p = Polyhedron_Copy(c->Cone);
400 p->next = pos;
401 pos = p;
402 delete c;
404 vec_ZZ lambda;
405 while (!nonuni.empty()) {
406 c = nonuni.back();
407 nonuni.pop_back();
408 Vector* v = c->short_vector(lambda);
409 for (int i = 0; i < c->Rays->NbRows - 1; ++i) {
410 if (lambda[i] == 0)
411 continue;
412 Matrix* M = Matrix_Copy(c->Rays);
413 Vector_Copy(v->p, M->p[i], v->Size);
414 cone * pc = new cone(M);
415 assert (pc->det != 0);
416 if (abs(pc->det) > 1) {
417 assert(abs(pc->det) < abs(c->det));
418 nonuni.push_back(pc);
419 } else {
420 Polyhedron *p = pc->poly();
421 pc->Cone = 0;
422 if (sign(pc->det) == s) {
423 p->next = pos;
424 pos = p;
425 } else {
426 p->next = neg;
427 neg = p;
429 delete pc;
431 Matrix_Free(M);
433 Vector_Free(v);
434 delete c;
436 *ppos = pos;
437 *pneg = neg;
441 * Returns a single list of npos "positive" cones followed by nneg
442 * "negative" cones.
443 * The input cone is freed
445 void decompose(Polyhedron *cone, Polyhedron **parts, int *npos, int *nneg, unsigned MaxRays)
447 Polyhedron_Polarize(cone);
448 if (cone->NbRays - 1 != cone->Dimension) {
449 Polyhedron *tmp = cone;
450 cone = triangularize_cone(cone, MaxRays);
451 Polyhedron_Free(tmp);
453 Polyhedron *polpos = NULL, *polneg = NULL;
454 *npos = 0; *nneg = 0;
455 for (Polyhedron *Polar = cone; Polar; Polar = Polar->next)
456 barvinok_decompose(Polar, &polpos, &polneg);
458 Polyhedron *last;
459 for (Polyhedron *i = polpos; i; i = i->next) {
460 Polyhedron_Polarize(i);
461 ++*npos;
462 last = i;
464 for (Polyhedron *i = polneg; i; i = i->next) {
465 Polyhedron_Polarize(i);
466 ++*nneg;
468 if (last) {
469 last->next = polneg;
470 *parts = polpos;
471 } else
472 *parts = polneg;
473 Domain_Free(cone);
476 const int MAX_TRY=10;
478 * Searches for a vector that is not othogonal to any
479 * of the rays in rays.
481 static void nonorthog(mat_ZZ& rays, vec_ZZ& lambda)
483 int dim = rays.NumCols();
484 bool found = false;
485 lambda.SetLength(dim);
486 for (int i = 2; !found && i <= 50*dim; i+=4) {
487 for (int j = 0; j < MAX_TRY; ++j) {
488 for (int k = 0; k < dim; ++k) {
489 int r = random_int(i)+2;
490 int v = (2*(r%2)-1) * (r >> 1);
491 lambda[k] = v;
493 int k = 0;
494 for (; k < rays.NumRows(); ++k)
495 if (lambda * rays[k] == 0)
496 break;
497 if (k == rays.NumRows()) {
498 found = true;
499 break;
503 assert(found);
506 static void add_rays(mat_ZZ& rays, Polyhedron *i, int *r)
508 unsigned dim = i->Dimension;
509 for (int k = 0; k < i->NbRays; ++k) {
510 if (!value_zero_p(i->Ray[k][dim+1]))
511 continue;
512 values2zz(i->Ray[k]+1, rays[(*r)++], dim);
516 void lattice_point(Value* values, Polyhedron *i, vec_ZZ& lambda, ZZ& num)
518 vec_ZZ vertex;
519 unsigned dim = i->Dimension;
520 if(!value_one_p(values[dim])) {
521 Matrix* Rays = rays(i);
522 Matrix *inv = Matrix_Alloc(Rays->NbRows, Rays->NbColumns);
523 int ok = Matrix_Inverse(Rays, inv);
524 assert(ok);
525 Matrix_Free(Rays);
526 Rays = rays(i);
527 Vector *lambda = Vector_Alloc(dim+1);
528 Vector_Matrix_Product(values, inv, lambda->p);
529 Matrix_Free(inv);
530 for (int j = 0; j < dim; ++j)
531 mpz_cdiv_q(lambda->p[j], lambda->p[j], lambda->p[dim]);
532 value_set_si(lambda->p[dim], 1);
533 Vector *A = Vector_Alloc(dim+1);
534 Vector_Matrix_Product(lambda->p, Rays, A->p);
535 Vector_Free(lambda);
536 Matrix_Free(Rays);
537 values2zz(A->p, vertex, dim);
538 Vector_Free(A);
539 } else
540 values2zz(values, vertex, dim);
542 num = vertex * lambda;
545 static evalue *term(int param, ZZ& c, Value *den = NULL)
547 evalue *EP = new evalue();
548 value_init(EP->d);
549 value_set_si(EP->d,0);
550 EP->x.p = new_enode(polynomial, 2, param + 1);
551 evalue_set_si(&EP->x.p->arr[0], 0, 1);
552 value_init(EP->x.p->arr[1].x.n);
553 if (den == NULL)
554 value_set_si(EP->x.p->arr[1].d, 1);
555 else
556 value_assign(EP->x.p->arr[1].d, *den);
557 zz2value(c, EP->x.p->arr[1].x.n);
558 return EP;
561 static void vertex_period(
562 Polyhedron *i, vec_ZZ& lambda, Matrix *T,
563 Value lcm, int p, Vector *val,
564 evalue *E, evalue* ev,
565 ZZ& offset)
567 unsigned nparam = T->NbRows - 1;
568 unsigned dim = i->Dimension;
569 Value tmp;
570 ZZ nump;
572 if (p == nparam) {
573 ZZ num, l;
574 Vector * values = Vector_Alloc(dim + 1);
575 Vector_Matrix_Product(val->p, T, values->p);
576 value_assign(values->p[dim], lcm);
577 lattice_point(values->p, i, lambda, num);
578 value2zz(lcm, l);
579 num *= l;
580 num += offset;
581 value_init(ev->x.n);
582 zz2value(num, ev->x.n);
583 value_assign(ev->d, lcm);
584 Vector_Free(values);
585 return;
588 value_init(tmp);
589 vec_ZZ vertex;
590 values2zz(T->p[p], vertex, dim);
591 nump = vertex * lambda;
592 if (First_Non_Zero(val->p, p) == -1) {
593 value_assign(tmp, lcm);
594 evalue *ET = term(p, nump, &tmp);
595 eadd(ET, E);
596 free_evalue_refs(ET);
597 delete ET;
600 value_assign(tmp, lcm);
601 if (First_Non_Zero(T->p[p], dim) != -1)
602 Vector_Gcd(T->p[p], dim, &tmp);
603 Gcd(tmp, lcm, &tmp);
604 if (value_lt(tmp, lcm)) {
605 ZZ count;
607 value_division(tmp, lcm, tmp);
608 value_set_si(ev->d, 0);
609 ev->x.p = new_enode(periodic, VALUE_TO_INT(tmp), p+1);
610 value2zz(tmp, count);
611 do {
612 value_decrement(tmp, tmp);
613 --count;
614 ZZ new_offset = offset - count * nump;
615 value_assign(val->p[p], tmp);
616 vertex_period(i, lambda, T, lcm, p+1, val, E,
617 &ev->x.p->arr[VALUE_TO_INT(tmp)], new_offset);
618 } while (value_pos_p(tmp));
619 } else
620 vertex_period(i, lambda, T, lcm, p+1, val, E, ev, offset);
621 value_clear(tmp);
624 static void mask_r(Matrix *f, int nr, Vector *lcm, int p, Vector *val, evalue *ev)
626 unsigned nparam = lcm->Size;
628 if (p == nparam) {
629 Vector * prod = Vector_Alloc(f->NbRows);
630 Matrix_Vector_Product(f, val->p, prod->p);
631 int isint = 1;
632 for (int i = 0; i < nr; ++i) {
633 value_modulus(prod->p[i], prod->p[i], f->p[i][nparam+1]);
634 isint &= value_zero_p(prod->p[i]);
636 value_set_si(ev->d, 1);
637 value_init(ev->x.n);
638 value_set_si(ev->x.n, isint);
639 Vector_Free(prod);
640 return;
643 Value tmp;
644 value_init(tmp);
645 if (value_one_p(lcm->p[p]))
646 mask_r(f, nr, lcm, p+1, val, ev);
647 else {
648 value_assign(tmp, lcm->p[p]);
649 value_set_si(ev->d, 0);
650 ev->x.p = new_enode(periodic, VALUE_TO_INT(tmp), p+1);
651 do {
652 value_decrement(tmp, tmp);
653 value_assign(val->p[p], tmp);
654 mask_r(f, nr, lcm, p+1, val, &ev->x.p->arr[VALUE_TO_INT(tmp)]);
655 } while (value_pos_p(tmp));
657 value_clear(tmp);
660 static evalue *multi_monom(vec_ZZ& p)
662 evalue *X = new evalue();
663 value_init(X->d);
664 value_init(X->x.n);
665 unsigned nparam = p.length()-1;
666 zz2value(p[nparam], X->x.n);
667 value_set_si(X->d, 1);
668 for (int i = 0; i < nparam; ++i) {
669 if (p[i] == 0)
670 continue;
671 evalue *T = term(i, p[i]);
672 eadd(T, X);
673 free_evalue_refs(T);
674 delete T;
676 return X;
680 * Check whether mapping polyhedron P on the affine combination
681 * num yields a range that has a fixed quotient on integer
682 * division by d
683 * If zero is true, then we are only interested in the quotient
684 * for the cases where the remainder is zero.
685 * Returns NULL if false and a newly allocated value if true.
687 static Value *fixed_quotient(Polyhedron *P, vec_ZZ& num, Value d, bool zero)
689 Value* ret = NULL;
690 int len = num.length();
691 Matrix *T = Matrix_Alloc(2, len);
692 zz2values(num, T->p[0]);
693 value_set_si(T->p[1][len-1], 1);
694 Polyhedron *I = Polyhedron_Image(P, T, P->NbConstraints);
695 Matrix_Free(T);
697 int i;
698 for (i = 0; i < I->NbRays; ++i)
699 if (value_zero_p(I->Ray[i][2])) {
700 Polyhedron_Free(I);
701 return NULL;
704 Value min, max;
705 value_init(min);
706 value_init(max);
707 int bounded = line_minmax(I, &min, &max);
708 assert(bounded);
710 if (zero)
711 mpz_cdiv_q(min, min, d);
712 else
713 mpz_fdiv_q(min, min, d);
714 mpz_fdiv_q(max, max, d);
716 if (value_eq(min, max)) {
717 ALLOC(Value, ret);
718 value_init(*ret);
719 value_assign(*ret, min);
721 value_clear(min);
722 value_clear(max);
723 return ret;
727 * Normalize linear expression coef modulo m
728 * Removes common factor and reduces coefficients
729 * Returns index of first non-zero coefficient or len
731 static int normal_mod(Value *coef, int len, Value *m)
733 Value gcd;
734 value_init(gcd);
736 Vector_Gcd(coef, len, &gcd);
737 Gcd(gcd, *m, &gcd);
738 Vector_AntiScale(coef, coef, gcd, len);
740 value_division(*m, *m, gcd);
741 value_clear(gcd);
743 if (value_one_p(*m))
744 return len;
746 int j;
747 for (j = 0; j < len; ++j)
748 mpz_fdiv_r(coef[j], coef[j], *m);
749 for (j = 0; j < len; ++j)
750 if (value_notzero_p(coef[j]))
751 break;
753 return j;
756 #ifdef USE_MODULO
757 static void mask(Matrix *f, evalue *factor)
759 int nr = f->NbRows, nc = f->NbColumns;
760 int n;
761 bool found = false;
762 for (n = 0; n < nr && value_notzero_p(f->p[n][nc-1]); ++n)
763 if (value_notone_p(f->p[n][nc-1]) &&
764 value_notmone_p(f->p[n][nc-1]))
765 found = true;
766 if (!found)
767 return;
769 evalue EP;
770 nr = n;
772 Value m;
773 value_init(m);
775 evalue EV;
776 value_init(EV.d);
777 value_init(EV.x.n);
778 value_set_si(EV.x.n, 1);
780 for (n = 0; n < nr; ++n) {
781 value_assign(m, f->p[n][nc-1]);
782 if (value_one_p(m) || value_mone_p(m))
783 continue;
785 int j = normal_mod(f->p[n], nc-1, &m);
786 if (j == nc-1) {
787 free_evalue_refs(factor);
788 value_init(factor->d);
789 evalue_set_si(factor, 0, 1);
790 break;
792 vec_ZZ row;
793 values2zz(f->p[n], row, nc-1);
794 ZZ g;
795 value2zz(m, g);
796 if (j < (nc-1)-1 && row[j] > g/2) {
797 for (int k = j; k < (nc-1); ++k)
798 if (row[k] != 0)
799 row[k] = g - row[k];
802 value_init(EP.d);
803 value_set_si(EP.d, 0);
804 EP.x.p = new_enode(relation, 2, 0);
805 value_clear(EP.x.p->arr[1].d);
806 EP.x.p->arr[1] = *factor;
807 evalue *ev = &EP.x.p->arr[0];
808 value_set_si(ev->d, 0);
809 ev->x.p = new_enode(fractional, 3, -1);
810 evalue_set_si(&ev->x.p->arr[1], 0, 1);
811 evalue_set_si(&ev->x.p->arr[2], 1, 1);
812 evalue *E = multi_monom(row);
813 value_assign(EV.d, m);
814 emul(&EV, E);
815 value_clear(ev->x.p->arr[0].d);
816 ev->x.p->arr[0] = *E;
817 delete E;
818 *factor = EP;
821 value_clear(m);
822 free_evalue_refs(&EV);
824 #else
828 static void mask(Matrix *f, evalue *factor)
830 int nr = f->NbRows, nc = f->NbColumns;
831 int n;
832 bool found = false;
833 for (n = 0; n < nr && value_notzero_p(f->p[n][nc-1]); ++n)
834 if (value_notone_p(f->p[n][nc-1]) &&
835 value_notmone_p(f->p[n][nc-1]))
836 found = true;
837 if (!found)
838 return;
840 Value tmp;
841 value_init(tmp);
842 nr = n;
843 unsigned np = nc - 2;
844 Vector *lcm = Vector_Alloc(np);
845 Vector *val = Vector_Alloc(nc);
846 Vector_Set(val->p, 0, nc);
847 value_set_si(val->p[np], 1);
848 Vector_Set(lcm->p, 1, np);
849 for (n = 0; n < nr; ++n) {
850 if (value_one_p(f->p[n][nc-1]) ||
851 value_mone_p(f->p[n][nc-1]))
852 continue;
853 for (int j = 0; j < np; ++j)
854 if (value_notzero_p(f->p[n][j])) {
855 Gcd(f->p[n][j], f->p[n][nc-1], &tmp);
856 value_division(tmp, f->p[n][nc-1], tmp);
857 value_lcm(tmp, lcm->p[j], &lcm->p[j]);
860 evalue EP;
861 value_init(EP.d);
862 mask_r(f, nr, lcm, 0, val, &EP);
863 value_clear(tmp);
864 Vector_Free(val);
865 Vector_Free(lcm);
866 emul(&EP,factor);
867 free_evalue_refs(&EP);
869 #endif
871 struct term_info {
872 evalue *E;
873 ZZ constant;
874 ZZ coeff;
875 int pos;
878 static bool mod_needed(Polyhedron *PD, vec_ZZ& num, Value d, evalue *E)
880 Value *q = fixed_quotient(PD, num, d, false);
882 if (!q)
883 return true;
885 value_oppose(*q, *q);
886 evalue EV;
887 value_init(EV.d);
888 value_set_si(EV.d, 1);
889 value_init(EV.x.n);
890 value_multiply(EV.x.n, *q, d);
891 eadd(&EV, E);
892 free_evalue_refs(&EV);
893 value_clear(*q);
894 free(q);
895 return false;
898 static void ceil_mod(Value *coef, int len, Value d, ZZ& f, evalue *EP, Polyhedron *PD)
900 Value m;
901 value_init(m);
902 value_set_si(m, -1);
904 Vector_Scale(coef, coef, m, len);
906 value_assign(m, d);
907 int j = normal_mod(coef, len, &m);
909 if (j == len) {
910 value_clear(m);
911 return;
914 vec_ZZ num;
915 values2zz(coef, num, len);
917 ZZ g;
918 value2zz(m, g);
920 evalue tmp;
921 value_init(tmp.d);
922 evalue_set_si(&tmp, 0, 1);
924 int p = j;
925 if (g % 2 == 0)
926 while (j < len-1 && (num[j] == g/2 || num[j] == 0))
927 ++j;
928 if ((j < len-1 && num[j] > g/2) || (j == len-1 && num[j] >= (g+1)/2)) {
929 for (int k = j; k < len-1; ++k)
930 if (num[k] != 0)
931 num[k] = g - num[k];
932 num[len-1] = g - 1 - num[len-1];
933 value_assign(tmp.d, m);
934 ZZ t = f*(g-1);
935 zz2value(t, tmp.x.n);
936 eadd(&tmp, EP);
937 f = -f;
940 if (p >= len-1) {
941 ZZ t = num[len-1] * f;
942 zz2value(t, tmp.x.n);
943 value_assign(tmp.d, m);
944 eadd(&tmp, EP);
945 } else {
946 evalue *E = multi_monom(num);
947 evalue EV;
948 value_init(EV.d);
950 if (PD && !mod_needed(PD, num, m, E)) {
951 value_init(EV.x.n);
952 zz2value(f, EV.x.n);
953 value_assign(EV.d, m);
954 emul(&EV, E);
955 eadd(E, EP);
956 } else {
957 value_init(EV.x.n);
958 value_set_si(EV.x.n, 1);
959 value_assign(EV.d, m);
960 emul(&EV, E);
961 value_clear(EV.x.n);
962 value_set_si(EV.d, 0);
963 EV.x.p = new_enode(fractional, 3, -1);
964 evalue_copy(&EV.x.p->arr[0], E);
965 evalue_set_si(&EV.x.p->arr[1], 0, 1);
966 value_init(EV.x.p->arr[2].x.n);
967 zz2value(f, EV.x.p->arr[2].x.n);
968 value_set_si(EV.x.p->arr[2].d, 1);
970 eadd(&EV, EP);
973 free_evalue_refs(&EV);
974 free_evalue_refs(E);
975 delete E;
978 free_evalue_refs(&tmp);
980 out:
981 value_clear(m);
984 evalue* bv_ceil3(Value *coef, int len, Value d, Polyhedron *P)
986 Vector *val = Vector_Alloc(len);
988 Value t;
989 value_init(t);
990 value_set_si(t, -1);
991 Vector_Scale(coef, val->p, t, len);
992 value_absolute(t, d);
994 vec_ZZ num;
995 values2zz(val->p, num, len);
996 evalue *EP = multi_monom(num);
998 evalue tmp;
999 value_init(tmp.d);
1000 value_init(tmp.x.n);
1001 value_set_si(tmp.x.n, 1);
1002 value_assign(tmp.d, t);
1004 emul(&tmp, EP);
1006 ZZ one;
1007 one = 1;
1008 ceil_mod(val->p, len, t, one, EP, P);
1009 value_clear(t);
1011 /* copy EP to malloc'ed evalue */
1012 evalue *E;
1013 ALLOC(evalue, E);
1014 *E = *EP;
1015 delete EP;
1017 free_evalue_refs(&tmp);
1018 Vector_Free(val);
1020 return E;
1023 #ifdef USE_MODULO
1024 evalue* lattice_point(
1025 Polyhedron *i, vec_ZZ& lambda, Matrix *W, Value lcm, Polyhedron *PD)
1027 unsigned nparam = W->NbColumns - 1;
1029 Matrix* Rays = rays2(i);
1030 Matrix *T = Transpose(Rays);
1031 Matrix *T2 = Matrix_Copy(T);
1032 Matrix *inv = Matrix_Alloc(T2->NbRows, T2->NbColumns);
1033 int ok = Matrix_Inverse(T2, inv);
1034 assert(ok);
1035 Matrix_Free(Rays);
1036 Matrix_Free(T2);
1037 mat_ZZ vertex;
1038 matrix2zz(W, vertex, W->NbRows, W->NbColumns);
1040 vec_ZZ num;
1041 num = lambda * vertex;
1043 evalue *EP = multi_monom(num);
1045 evalue tmp;
1046 value_init(tmp.d);
1047 value_init(tmp.x.n);
1048 value_set_si(tmp.x.n, 1);
1049 value_assign(tmp.d, lcm);
1051 emul(&tmp, EP);
1053 Matrix *L = Matrix_Alloc(inv->NbRows, W->NbColumns);
1054 Matrix_Product(inv, W, L);
1056 mat_ZZ RT;
1057 matrix2zz(T, RT, T->NbRows, T->NbColumns);
1058 Matrix_Free(T);
1060 vec_ZZ p = lambda * RT;
1062 for (int i = 0; i < L->NbRows; ++i) {
1063 ceil_mod(L->p[i], nparam+1, lcm, p[i], EP, PD);
1066 Matrix_Free(L);
1068 Matrix_Free(inv);
1069 free_evalue_refs(&tmp);
1070 return EP;
1072 #else
1073 evalue* lattice_point(
1074 Polyhedron *i, vec_ZZ& lambda, Matrix *W, Value lcm, Polyhedron *PD)
1076 Matrix *T = Transpose(W);
1077 unsigned nparam = T->NbRows - 1;
1079 evalue *EP = new evalue();
1080 value_init(EP->d);
1081 evalue_set_si(EP, 0, 1);
1083 evalue ev;
1084 Vector *val = Vector_Alloc(nparam+1);
1085 value_set_si(val->p[nparam], 1);
1086 ZZ offset(INIT_VAL, 0);
1087 value_init(ev.d);
1088 vertex_period(i, lambda, T, lcm, 0, val, EP, &ev, offset);
1089 Vector_Free(val);
1090 eadd(&ev, EP);
1091 free_evalue_refs(&ev);
1093 Matrix_Free(T);
1095 reduce_evalue(EP);
1097 return EP;
1099 #endif
1101 void lattice_point(
1102 Param_Vertices* V, Polyhedron *i, vec_ZZ& lambda, term_info* term,
1103 Polyhedron *PD)
1105 unsigned nparam = V->Vertex->NbColumns - 2;
1106 unsigned dim = i->Dimension;
1107 mat_ZZ vertex;
1108 vertex.SetDims(V->Vertex->NbRows, nparam+1);
1109 Value lcm, tmp;
1110 value_init(lcm);
1111 value_init(tmp);
1112 value_set_si(lcm, 1);
1113 for (int j = 0; j < V->Vertex->NbRows; ++j) {
1114 value_lcm(lcm, V->Vertex->p[j][nparam+1], &lcm);
1116 if (value_notone_p(lcm)) {
1117 Matrix * mv = Matrix_Alloc(dim, nparam+1);
1118 for (int j = 0 ; j < dim; ++j) {
1119 value_division(tmp, lcm, V->Vertex->p[j][nparam+1]);
1120 Vector_Scale(V->Vertex->p[j], mv->p[j], tmp, nparam+1);
1123 term->E = lattice_point(i, lambda, mv, lcm, PD);
1124 term->constant = 0;
1126 Matrix_Free(mv);
1127 value_clear(lcm);
1128 value_clear(tmp);
1129 return;
1131 for (int i = 0; i < V->Vertex->NbRows; ++i) {
1132 assert(value_one_p(V->Vertex->p[i][nparam+1])); // for now
1133 values2zz(V->Vertex->p[i], vertex[i], nparam+1);
1136 vec_ZZ num;
1137 num = lambda * vertex;
1139 int p = -1;
1140 int nn = 0;
1141 for (int j = 0; j < nparam; ++j)
1142 if (num[j] != 0) {
1143 ++nn;
1144 p = j;
1146 if (nn >= 2) {
1147 term->E = multi_monom(num);
1148 term->constant = 0;
1149 } else {
1150 term->E = NULL;
1151 term->constant = num[nparam];
1152 term->pos = p;
1153 if (p != -1)
1154 term->coeff = num[p];
1157 value_clear(lcm);
1158 value_clear(tmp);
1161 void normalize(Polyhedron *i, vec_ZZ& lambda, ZZ& sign, ZZ& num, vec_ZZ& den)
1163 unsigned dim = i->Dimension;
1165 int r = 0;
1166 mat_ZZ rays;
1167 rays.SetDims(dim, dim);
1168 add_rays(rays, i, &r);
1169 den = rays * lambda;
1170 int change = 0;
1172 for (int j = 0; j < den.length(); ++j) {
1173 if (den[j] > 0)
1174 change ^= 1;
1175 else {
1176 den[j] = abs(den[j]);
1177 num += den[j];
1180 if (change)
1181 sign = -sign;
1184 typedef Polyhedron * Polyhedron_p;
1186 void barvinok_count(Polyhedron *P, Value* result, unsigned NbMaxCons)
1188 Polyhedron ** vcone;
1189 vec_ZZ sign;
1190 int ncone = 0;
1191 sign.SetLength(ncone);
1192 unsigned dim;
1193 int allocated = 0;
1194 Value factor;
1195 Polyhedron *Q;
1196 int r = 0;
1198 if (emptyQ(P)) {
1199 value_set_si(*result, 0);
1200 return;
1202 if (P->NbBid == 0)
1203 for (; r < P->NbRays; ++r)
1204 if (value_zero_p(P->Ray[r][P->Dimension+1]))
1205 break;
1206 if (P->NbBid !=0 || r < P->NbRays) {
1207 value_set_si(*result, -1);
1208 return;
1210 if (P->NbEq != 0) {
1211 P = remove_equalities(P);
1212 if (emptyQ(P)) {
1213 Polyhedron_Free(P);
1214 value_set_si(*result, 0);
1215 return;
1217 allocated = 1;
1219 value_init(factor);
1220 value_set_si(factor, 1);
1221 Q = Polyhedron_Reduce(P, &factor);
1222 if (Q) {
1223 if (allocated)
1224 Polyhedron_Free(P);
1225 P = Q;
1226 allocated = 1;
1228 if (P->Dimension == 0) {
1229 value_assign(*result, factor);
1230 if (allocated)
1231 Polyhedron_Free(P);
1232 value_clear(factor);
1233 return;
1236 dim = P->Dimension;
1237 vcone = new Polyhedron_p[P->NbRays];
1239 for (int j = 0; j < P->NbRays; ++j) {
1240 int npos, nneg;
1241 Polyhedron *C = supporting_cone(P, j);
1242 decompose(C, &vcone[j], &npos, &nneg, NbMaxCons);
1243 ncone += npos + nneg;
1244 sign.SetLength(ncone);
1245 for (int k = 0; k < npos; ++k)
1246 sign[ncone-nneg-k-1] = 1;
1247 for (int k = 0; k < nneg; ++k)
1248 sign[ncone-k-1] = -1;
1251 mat_ZZ rays;
1252 rays.SetDims(ncone * dim, dim);
1253 r = 0;
1254 for (int j = 0; j < P->NbRays; ++j) {
1255 for (Polyhedron *i = vcone[j]; i; i = i->next) {
1256 assert(i->NbRays-1 == dim);
1257 add_rays(rays, i, &r);
1260 vec_ZZ lambda;
1261 nonorthog(rays, lambda);
1263 ZZ num;
1264 vec_ZZ den;
1265 den.SetLength(dim);
1267 int f = 0;
1268 vec_ZZ vertex;
1269 mpq_t count;
1270 mpq_init(count);
1271 for (int j = 0; j < P->NbRays; ++j) {
1272 for (Polyhedron *i = vcone[j]; i; i = i->next) {
1273 lattice_point(P->Ray[j]+1, i, vertex);
1274 num = vertex * lambda;
1275 normalize(i, lambda, sign[f], num, den);
1277 dpoly d(dim, num);
1278 dpoly n(dim, den[0], 1);
1279 for (int k = 1; k < dim; ++k) {
1280 dpoly fact(dim, den[k], 1);
1281 n *= fact;
1283 d.div(n, count, sign[f]);
1285 ++f;
1287 Domain_Free(vcone[j]);
1290 assert(value_one_p(&count[0]._mp_den));
1291 value_multiply(*result, &count[0]._mp_num, factor);
1292 mpq_clear(count);
1294 delete [] vcone;
1296 if (allocated)
1297 Polyhedron_Free(P);
1298 value_clear(factor);
1301 static void uni_polynom(int param, Vector *c, evalue *EP)
1303 unsigned dim = c->Size-2;
1304 value_init(EP->d);
1305 value_set_si(EP->d,0);
1306 EP->x.p = new_enode(polynomial, dim+1, param+1);
1307 for (int j = 0; j <= dim; ++j)
1308 evalue_set(&EP->x.p->arr[j], c->p[j], c->p[dim+1]);
1311 static void multi_polynom(Vector *c, evalue* X, evalue *EP)
1313 unsigned dim = c->Size-2;
1314 evalue EC;
1316 value_init(EC.d);
1317 evalue_set(&EC, c->p[dim], c->p[dim+1]);
1319 value_init(EP->d);
1320 evalue_set(EP, c->p[dim], c->p[dim+1]);
1322 for (int i = dim-1; i >= 0; --i) {
1323 emul(X, EP);
1324 value_assign(EC.x.n, c->p[i]);
1325 eadd(&EC, EP);
1327 free_evalue_refs(&EC);
1330 Polyhedron *unfringe (Polyhedron *P, unsigned MaxRays)
1332 int len = P->Dimension+2;
1333 Polyhedron *T, *R = P;
1334 Value g;
1335 value_init(g);
1336 Vector *row = Vector_Alloc(len);
1337 value_set_si(row->p[0], 1);
1339 R = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
1341 Matrix *M = Matrix_Alloc(2, len-1);
1342 value_set_si(M->p[1][len-2], 1);
1343 for (int v = 0; v < P->Dimension; ++v) {
1344 value_set_si(M->p[0][v], 1);
1345 Polyhedron *I = Polyhedron_Image(P, M, 2+1);
1346 value_set_si(M->p[0][v], 0);
1347 for (int r = 0; r < I->NbConstraints; ++r) {
1348 if (value_zero_p(I->Constraint[r][0]))
1349 continue;
1350 if (value_zero_p(I->Constraint[r][1]))
1351 continue;
1352 if (value_one_p(I->Constraint[r][1]))
1353 continue;
1354 if (value_mone_p(I->Constraint[r][1]))
1355 continue;
1356 value_absolute(g, I->Constraint[r][1]);
1357 Vector_Set(row->p+1, 0, len-2);
1358 value_division(row->p[1+v], I->Constraint[r][1], g);
1359 mpz_fdiv_q(row->p[len-1], I->Constraint[r][2], g);
1360 T = R;
1361 R = AddConstraints(row->p, 1, R, MaxRays);
1362 if (T != P)
1363 Polyhedron_Free(T);
1365 Polyhedron_Free(I);
1367 Matrix_Free(M);
1368 Vector_Free(row);
1369 value_clear(g);
1370 return R;
1373 static Polyhedron *reduce_domain(Polyhedron *D, Matrix *CT, Polyhedron *CEq,
1374 Polyhedron **fVD, int nd, unsigned MaxRays)
1376 assert(CEq);
1378 Polyhedron *Dt;
1379 Dt = CT ? DomainPreimage(D, CT, MaxRays) : D;
1380 Polyhedron *rVD = DomainIntersection(Dt, CEq, MaxRays);
1382 /* if rVD is empty or too small in geometric dimension */
1383 if(!rVD || emptyQ(rVD) ||
1384 (rVD->Dimension-rVD->NbEq < Dt->Dimension-Dt->NbEq-CEq->NbEq)) {
1385 if(rVD)
1386 Domain_Free(rVD);
1387 if (CT)
1388 Domain_Free(Dt);
1389 return 0; /* empty validity domain */
1392 if (CT)
1393 Domain_Free(Dt);
1395 fVD[nd] = Domain_Copy(rVD);
1396 for (int i = 0 ; i < nd; ++i) {
1397 Polyhedron *I = DomainIntersection(fVD[nd], fVD[i], MaxRays);
1398 if (emptyQ(I)) {
1399 Domain_Free(I);
1400 continue;
1402 Polyhedron *F = DomainSimplify(I, fVD[nd], MaxRays);
1403 if (F->NbEq == 1) {
1404 Polyhedron *T = rVD;
1405 rVD = DomainDifference(rVD, F, MaxRays);
1406 Domain_Free(T);
1408 Domain_Free(F);
1409 Domain_Free(I);
1412 rVD = DomainConstraintSimplify(rVD, MaxRays);
1413 if (emptyQ(rVD)) {
1414 Domain_Free(fVD[nd]);
1415 Domain_Free(rVD);
1416 return 0;
1419 Value c;
1420 value_init(c);
1421 barvinok_count(rVD, &c, MaxRays);
1422 if (value_zero_p(c)) {
1423 Domain_Free(rVD);
1424 rVD = 0;
1426 value_clear(c);
1428 return rVD;
1431 evalue* barvinok_enumerate_ev(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1433 //P = unfringe(P, MaxRays);
1434 Polyhedron *CEq = NULL, *rVD, *pVD, *CA;
1435 Matrix *CT = NULL;
1436 Param_Polyhedron *PP = NULL;
1437 Param_Domain *D, *next;
1438 Param_Vertices *V;
1439 int r = 0;
1440 unsigned nparam = C->Dimension;
1441 evalue *eres;
1442 ALLOC(evalue, eres);
1443 value_init(eres->d);
1444 value_set_si(eres->d, 0);
1446 evalue factor;
1447 value_init(factor.d);
1448 evalue_set_si(&factor, 1, 1);
1450 CA = align_context(C, P->Dimension, MaxRays);
1451 P = DomainIntersection(P, CA, MaxRays);
1452 Polyhedron_Free(CA);
1454 if (C->Dimension == 0 || emptyQ(P)) {
1455 constant:
1456 eres->x.p = new_enode(partition, 2, C->Dimension);
1457 EVALUE_SET_DOMAIN(eres->x.p->arr[0],
1458 DomainConstraintSimplify(CEq ? CEq : Polyhedron_Copy(C), MaxRays));
1459 value_set_si(eres->x.p->arr[1].d, 1);
1460 value_init(eres->x.p->arr[1].x.n);
1461 if (emptyQ(P))
1462 value_set_si(eres->x.p->arr[1].x.n, 0);
1463 else
1464 barvinok_count(P, &eres->x.p->arr[1].x.n, MaxRays);
1465 out:
1466 emul(&factor, eres);
1467 reduce_evalue(eres);
1468 free_evalue_refs(&factor);
1469 Polyhedron_Free(P);
1470 if (CT)
1471 Matrix_Free(CT);
1472 if (PP)
1473 Param_Polyhedron_Free(PP);
1475 return eres;
1477 for (r = 0; r < P->NbRays; ++r)
1478 if (value_zero_p(P->Ray[r][0]) ||
1479 value_zero_p(P->Ray[r][P->Dimension+1])) {
1480 int i;
1481 for (i = P->Dimension - nparam; i < P->Dimension; ++i)
1482 if (value_notzero_p(P->Ray[r][i+1]))
1483 break;
1484 if (i >= P->Dimension)
1485 break;
1487 if (r < P->NbRays)
1488 goto constant;
1490 if (P->NbEq != 0) {
1491 Matrix *f;
1492 P = remove_equalities_p(P, P->Dimension-nparam, &f);
1493 mask(f, &factor);
1494 Matrix_Free(f);
1496 if (P->Dimension == nparam) {
1497 CEq = P;
1498 P = Universe_Polyhedron(0);
1499 goto constant;
1502 Polyhedron *Q = ParamPolyhedron_Reduce(P, P->Dimension-nparam, &factor);
1503 if (Q) {
1504 Polyhedron_Free(P);
1505 if (Q->Dimension == nparam) {
1506 CEq = Q;
1507 P = Universe_Polyhedron(0);
1508 goto constant;
1510 P = Q;
1512 Polyhedron *oldP = P;
1513 PP = Polyhedron2Param_SimplifiedDomain(&P,C,MaxRays,&CEq,&CT);
1514 if (P != oldP)
1515 Polyhedron_Free(oldP);
1517 if (isIdentity(CT)) {
1518 Matrix_Free(CT);
1519 CT = NULL;
1520 } else {
1521 assert(CT->NbRows != CT->NbColumns);
1522 if (CT->NbRows == 1) // no more parameters
1523 goto constant;
1524 nparam = CT->NbRows - 1;
1527 unsigned dim = P->Dimension - nparam;
1528 Polyhedron ** vcone = new Polyhedron_p[PP->nbV];
1529 int * npos = new int[PP->nbV];
1530 int * nneg = new int[PP->nbV];
1531 ZZ sign;
1533 int i;
1534 for (i = 0, V = PP->V; V; ++i, V = V->next) {
1535 Polyhedron *C = supporting_cone_p(P, V);
1536 decompose(C, &vcone[i], &npos[i], &nneg[i], MaxRays);
1539 Vector *c = Vector_Alloc(dim+2);
1541 int nd;
1542 for (nd = 0, D=PP->D; D; ++nd, D=D->next);
1543 struct section { Polyhedron *D; evalue E; };
1544 section *s = new section[nd];
1545 Polyhedron **fVD = new Polyhedron_p[nd];
1547 for(nd = 0, D=PP->D; D; D=next) {
1548 next = D->next;
1550 Polyhedron *rVD = reduce_domain(D->Domain, CT, CEq,
1551 fVD, nd, MaxRays);
1552 if (!rVD)
1553 continue;
1555 pVD = CT ? DomainImage(rVD,CT,MaxRays) : rVD;
1557 int ncone = 0;
1558 FORALL_PVertex_in_ParamPolyhedron(V,D,PP) // _i is internal counter
1559 ncone += npos[_i] + nneg[_i];
1560 END_FORALL_PVertex_in_ParamPolyhedron;
1562 mat_ZZ rays;
1563 rays.SetDims(ncone * dim, dim);
1564 r = 0;
1565 FORALL_PVertex_in_ParamPolyhedron(V,D,PP) // _i is internal counter
1566 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1567 assert(i->NbRays-1 == dim);
1568 add_rays(rays, i, &r);
1570 END_FORALL_PVertex_in_ParamPolyhedron;
1571 vec_ZZ lambda;
1572 nonorthog(rays, lambda);
1574 vec_ZZ den;
1575 den.SetLength(dim);
1576 term_info num;
1578 value_init(s[nd].E.d);
1579 evalue_set_si(&s[nd].E, 0, 1);
1580 mpq_t count;
1581 mpq_init(count);
1582 FORALL_PVertex_in_ParamPolyhedron(V,D,PP)
1583 int f = 0;
1584 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1585 sign = f < npos[_i] ? 1 : -1;
1586 lattice_point(V, i, lambda, &num, pVD);
1587 normalize(i, lambda, sign, num.constant, den);
1589 dpoly n(dim, den[0], 1);
1590 for (int k = 1; k < dim; ++k) {
1591 dpoly fact(dim, den[k], 1);
1592 n *= fact;
1594 if (num.E != NULL) {
1595 ZZ one(INIT_VAL, 1);
1596 dpoly_n d(dim, num.constant, one);
1597 d.div(n, c, sign);
1598 evalue EV;
1599 multi_polynom(c, num.E, &EV);
1600 eadd(&EV , &s[nd].E);
1601 free_evalue_refs(&EV);
1602 free_evalue_refs(num.E);
1603 delete num.E;
1604 } else if (num.pos != -1) {
1605 dpoly_n d(dim, num.constant, num.coeff);
1606 d.div(n, c, sign);
1607 evalue EV;
1608 uni_polynom(num.pos, c, &EV);
1609 eadd(&EV , &s[nd].E);
1610 free_evalue_refs(&EV);
1611 } else {
1612 mpq_set_si(count, 0, 1);
1613 dpoly d(dim, num.constant);
1614 d.div(n, count, sign);
1615 evalue EV;
1616 value_init(EV.d);
1617 evalue_set(&EV, &count[0]._mp_num, &count[0]._mp_den);
1618 eadd(&EV , &s[nd].E);
1619 free_evalue_refs(&EV);
1621 ++f;
1623 END_FORALL_PVertex_in_ParamPolyhedron;
1625 mpq_clear(count);
1627 if (CT)
1628 addeliminatedparams_evalue(&s[nd].E, CT);
1629 s[nd].D = rVD;
1630 ++nd;
1631 if (rVD != pVD)
1632 Domain_Free(pVD);
1635 if (nd == 0)
1636 evalue_set_si(eres, 0, 1);
1637 else {
1638 eres->x.p = new_enode(partition, 2*nd, C->Dimension);
1639 for (int j = 0; j < nd; ++j) {
1640 EVALUE_SET_DOMAIN(eres->x.p->arr[2*j], s[j].D);
1641 value_clear(eres->x.p->arr[2*j+1].d);
1642 eres->x.p->arr[2*j+1] = s[j].E;
1643 Domain_Free(fVD[j]);
1646 delete [] s;
1647 delete [] fVD;
1649 Vector_Free(c);
1651 for (int j = 0; j < PP->nbV; ++j)
1652 Domain_Free(vcone[j]);
1653 delete [] vcone;
1654 delete [] npos;
1655 delete [] nneg;
1657 if (CEq)
1658 Polyhedron_Free(CEq);
1660 goto out;
1663 Enumeration* barvinok_enumerate(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1665 evalue *EP = barvinok_enumerate_ev(P, C, MaxRays);
1667 return partition2enumeration(EP);
1670 static void SwapColumns(Value **V, int n, int i, int j)
1672 for (int r = 0; r < n; ++r)
1673 value_swap(V[r][i], V[r][j]);
1676 static void SwapColumns(Polyhedron *P, int i, int j)
1678 SwapColumns(P->Constraint, P->NbConstraints, i, j);
1679 SwapColumns(P->Ray, P->NbRays, i, j);
1682 static void negative_test_constraint(Value *l, Value *u, Value *c, int pos,
1683 int len, Value *v)
1685 value_oppose(*v, u[pos+1]);
1686 Vector_Combine(l+1, u+1, c+1, *v, l[pos+1], len-1);
1687 value_multiply(*v, *v, l[pos+1]);
1688 value_substract(c[len-1], c[len-1], *v);
1689 value_set_si(*v, -1);
1690 Vector_Scale(c+1, c+1, *v, len-1);
1691 value_decrement(c[len-1], c[len-1]);
1692 ConstraintSimplify(c, c, len, v);
1695 static void oppose_constraint(Value *c, int len, Value *v)
1697 value_set_si(*v, -1);
1698 Vector_Scale(c+1, c+1, *v, len-1);
1699 value_decrement(c[len-1], c[len-1]);
1702 static bool SplitOnConstraint(Polyhedron *P, int i, int l, int u,
1703 int nvar, int len, int exist, int MaxRays,
1704 Vector *row, Value& f, bool independent,
1705 Polyhedron **pos, Polyhedron **neg)
1707 negative_test_constraint(P->Constraint[l], P->Constraint[u],
1708 row->p, nvar+i, len, &f);
1709 *neg = AddConstraints(row->p, 1, P, MaxRays);
1711 /* We found an independent, but useless constraint
1712 * Maybe we should detect this earlier and not
1713 * mark the variable as INDEPENDENT
1715 if (emptyQ((*neg))) {
1716 Polyhedron_Free(*neg);
1717 return false;
1720 oppose_constraint(row->p, len, &f);
1721 *pos = AddConstraints(row->p, 1, P, MaxRays);
1723 if (emptyQ((*pos))) {
1724 Polyhedron_Free(*neg);
1725 Polyhedron_Free(*pos);
1726 return false;
1729 return true;
1733 * unimodularly transform P such that constraint r is transformed
1734 * into a constraint that involves only a single (the first)
1735 * existential variable
1738 static Polyhedron *rotate_along(Polyhedron *P, int r, int nvar, int exist,
1739 unsigned MaxRays)
1741 Value g;
1742 value_init(g);
1744 Vector *row = Vector_Alloc(exist);
1745 Vector_Copy(P->Constraint[r]+1+nvar, row->p, exist);
1746 Vector_Gcd(row->p, exist, &g);
1747 if (value_notone_p(g))
1748 Vector_AntiScale(row->p, row->p, g, exist);
1749 value_clear(g);
1751 Matrix *M = unimodular_complete(row);
1752 Matrix *M2 = Matrix_Alloc(P->Dimension+1, P->Dimension+1);
1753 for (r = 0; r < nvar; ++r)
1754 value_set_si(M2->p[r][r], 1);
1755 for ( ; r < nvar+exist; ++r)
1756 Vector_Copy(M->p[r-nvar], M2->p[r]+nvar, exist);
1757 for ( ; r < P->Dimension+1; ++r)
1758 value_set_si(M2->p[r][r], 1);
1759 Polyhedron *T = Polyhedron_Image(P, M2, MaxRays);
1761 Matrix_Free(M2);
1762 Matrix_Free(M);
1763 Vector_Free(row);
1765 return T;
1768 static bool SplitOnVar(Polyhedron *P, int i,
1769 int nvar, int len, int exist, int MaxRays,
1770 Vector *row, Value& f, bool independent,
1771 Polyhedron **pos, Polyhedron **neg)
1773 int j;
1775 for (int l = P->NbEq; l < P->NbConstraints; ++l) {
1776 if (value_negz_p(P->Constraint[l][nvar+i+1]))
1777 continue;
1779 if (independent) {
1780 for (j = 0; j < exist; ++j)
1781 if (j != i && value_notzero_p(P->Constraint[l][nvar+j+1]))
1782 break;
1783 if (j < exist)
1784 continue;
1787 for (int u = P->NbEq; u < P->NbConstraints; ++u) {
1788 if (value_posz_p(P->Constraint[u][nvar+i+1]))
1789 continue;
1791 if (independent) {
1792 for (j = 0; j < exist; ++j)
1793 if (j != i && value_notzero_p(P->Constraint[u][nvar+j+1]))
1794 break;
1795 if (j < exist)
1796 continue;
1799 if (SplitOnConstraint(P, i, l, u,
1800 nvar, len, exist, MaxRays,
1801 row, f, independent,
1802 pos, neg)) {
1803 if (independent) {
1804 if (i != 0)
1805 SwapColumns(*neg, nvar+1, nvar+1+i);
1807 return true;
1812 return false;
1815 static bool double_bound_pair(Polyhedron *P, int nvar, int exist,
1816 int i, int l1, int l2,
1817 Polyhedron **pos, Polyhedron **neg)
1819 Value f;
1820 value_init(f);
1821 Vector *row = Vector_Alloc(P->Dimension+2);
1822 value_set_si(row->p[0], 1);
1823 value_oppose(f, P->Constraint[l1][nvar+i+1]);
1824 Vector_Combine(P->Constraint[l1]+1, P->Constraint[l2]+1,
1825 row->p+1,
1826 P->Constraint[l2][nvar+i+1], f,
1827 P->Dimension+1);
1828 ConstraintSimplify(row->p, row->p, P->Dimension+2, &f);
1829 *pos = AddConstraints(row->p, 1, P, 0);
1830 value_set_si(f, -1);
1831 Vector_Scale(row->p+1, row->p+1, f, P->Dimension+1);
1832 value_decrement(row->p[P->Dimension+1], row->p[P->Dimension+1]);
1833 *neg = AddConstraints(row->p, 1, P, 0);
1834 Vector_Free(row);
1835 value_clear(f);
1837 return !emptyQ((*pos)) && !emptyQ((*neg));
1840 static bool double_bound(Polyhedron *P, int nvar, int exist,
1841 Polyhedron **pos, Polyhedron **neg)
1843 for (int i = 0; i < exist; ++i) {
1844 int l1, l2;
1845 for (l1 = P->NbEq; l1 < P->NbConstraints; ++l1) {
1846 if (value_negz_p(P->Constraint[l1][nvar+i+1]))
1847 continue;
1848 for (l2 = l1 + 1; l2 < P->NbConstraints; ++l2) {
1849 if (value_negz_p(P->Constraint[l2][nvar+i+1]))
1850 continue;
1851 if (double_bound_pair(P, nvar, exist, i, l1, l2, pos, neg))
1852 return true;
1855 for (l1 = P->NbEq; l1 < P->NbConstraints; ++l1) {
1856 if (value_posz_p(P->Constraint[l1][nvar+i+1]))
1857 continue;
1858 if (l1 < P->NbConstraints)
1859 for (l2 = l1 + 1; l2 < P->NbConstraints; ++l2) {
1860 if (value_posz_p(P->Constraint[l2][nvar+i+1]))
1861 continue;
1862 if (double_bound_pair(P, nvar, exist, i, l1, l2, pos, neg))
1863 return true;
1866 return false;
1868 return false;
1871 enum constraint {
1872 ALL_POS = 1 << 0,
1873 ONE_NEG = 1 << 1,
1874 INDEPENDENT = 1 << 2
1877 static evalue* enumerate_or(Polyhedron *D,
1878 unsigned exist, unsigned nparam, unsigned MaxRays)
1880 #ifdef DEBUG_ER
1881 fprintf(stderr, "\nER: Or\n");
1882 #endif /* DEBUG_ER */
1884 Polyhedron *N = D->next;
1885 D->next = 0;
1886 evalue *EP =
1887 barvinok_enumerate_e(D, exist, nparam, MaxRays);
1888 Polyhedron_Free(D);
1890 for (D = N; D; D = N) {
1891 N = D->next;
1892 D->next = 0;
1894 evalue *EN =
1895 barvinok_enumerate_e(D, exist, nparam, MaxRays);
1897 eor(EN, EP);
1898 free_evalue_refs(EN);
1899 free(EN);
1900 Polyhedron_Free(D);
1903 reduce_evalue(EP);
1905 return EP;
1908 static evalue* enumerate_sum(Polyhedron *P,
1909 unsigned exist, unsigned nparam, unsigned MaxRays)
1911 int nvar = P->Dimension - exist - nparam;
1912 int toswap = nvar < exist ? nvar : exist;
1913 for (int i = 0; i < toswap; ++i)
1914 SwapColumns(P, 1 + i, nvar+exist - i);
1915 nparam += nvar;
1917 #ifdef DEBUG_ER
1918 fprintf(stderr, "\nER: Sum\n");
1919 #endif /* DEBUG_ER */
1921 evalue *EP = barvinok_enumerate_e(P, exist, nparam, MaxRays);
1923 for (int i = 0; i < /* nvar */ nparam; ++i) {
1924 Matrix *C = Matrix_Alloc(1, 1 + nparam + 1);
1925 value_set_si(C->p[0][0], 1);
1926 evalue split;
1927 value_init(split.d);
1928 value_set_si(split.d, 0);
1929 split.x.p = new_enode(partition, 4, nparam);
1930 value_set_si(C->p[0][1+i], 1);
1931 Matrix *C2 = Matrix_Copy(C);
1932 EVALUE_SET_DOMAIN(split.x.p->arr[0],
1933 Constraints2Polyhedron(C2, MaxRays));
1934 Matrix_Free(C2);
1935 evalue_set_si(&split.x.p->arr[1], 1, 1);
1936 value_set_si(C->p[0][1+i], -1);
1937 value_set_si(C->p[0][1+nparam], -1);
1938 EVALUE_SET_DOMAIN(split.x.p->arr[2],
1939 Constraints2Polyhedron(C, MaxRays));
1940 evalue_set_si(&split.x.p->arr[3], 1, 1);
1941 emul(&split, EP);
1942 free_evalue_refs(&split);
1943 Matrix_Free(C);
1945 reduce_evalue(EP);
1946 evalue_range_reduction(EP);
1948 evalue_frac2floor(EP);
1950 evalue *sum = esum(EP, nvar);
1952 free_evalue_refs(EP);
1953 free(EP);
1954 EP = sum;
1956 evalue_range_reduction(EP);
1958 return EP;
1961 static evalue* split_sure(Polyhedron *P, Polyhedron *S,
1962 unsigned exist, unsigned nparam, unsigned MaxRays)
1964 int nvar = P->Dimension - exist - nparam;
1966 Matrix *M = Matrix_Alloc(exist, S->Dimension+2);
1967 for (int i = 0; i < exist; ++i)
1968 value_set_si(M->p[i][nvar+i+1], 1);
1969 Polyhedron *O = S;
1970 S = DomainAddRays(S, M, MaxRays);
1971 Polyhedron_Free(O);
1972 Polyhedron *F = DomainAddRays(P, M, MaxRays);
1973 Polyhedron *D = DomainDifference(F, S, MaxRays);
1974 O = D;
1975 D = Disjoint_Domain(D, 0, MaxRays);
1976 Polyhedron_Free(F);
1977 Domain_Free(O);
1978 Matrix_Free(M);
1980 M = Matrix_Alloc(P->Dimension+1-exist, P->Dimension+1);
1981 for (int j = 0; j < nvar; ++j)
1982 value_set_si(M->p[j][j], 1);
1983 for (int j = 0; j < nparam+1; ++j)
1984 value_set_si(M->p[nvar+j][nvar+exist+j], 1);
1985 Polyhedron *T = Polyhedron_Image(S, M, MaxRays);
1986 evalue *EP = barvinok_enumerate_e(T, 0, nparam, MaxRays);
1987 Polyhedron_Free(S);
1988 Polyhedron_Free(T);
1989 Matrix_Free(M);
1991 for (Polyhedron *Q = D; Q; Q = Q->next) {
1992 Polyhedron *N = Q->next;
1993 Q->next = 0;
1994 T = DomainIntersection(P, Q, MaxRays);
1995 evalue *E = barvinok_enumerate_e(T, exist, nparam, MaxRays);
1996 eadd(E, EP);
1997 free_evalue_refs(E);
1998 free(E);
1999 Polyhedron_Free(T);
2000 Q->next = N;
2002 Domain_Free(D);
2003 return EP;
2006 static evalue* enumerate_sure(Polyhedron *P,
2007 unsigned exist, unsigned nparam, unsigned MaxRays)
2009 int i;
2010 Polyhedron *S = P;
2011 int nvar = P->Dimension - exist - nparam;
2012 Value lcm;
2013 Value f;
2014 value_init(lcm);
2015 value_init(f);
2017 for (i = 0; i < exist; ++i) {
2018 Matrix *M = Matrix_Alloc(S->NbConstraints, S->Dimension+2);
2019 int c = 0;
2020 value_set_si(lcm, 1);
2021 for (int j = 0; j < S->NbConstraints; ++j) {
2022 if (value_negz_p(S->Constraint[j][1+nvar+i]))
2023 continue;
2024 if (value_one_p(S->Constraint[j][1+nvar+i]))
2025 continue;
2026 value_lcm(lcm, S->Constraint[j][1+nvar+i], &lcm);
2029 for (int j = 0; j < S->NbConstraints; ++j) {
2030 if (value_negz_p(S->Constraint[j][1+nvar+i]))
2031 continue;
2032 if (value_one_p(S->Constraint[j][1+nvar+i]))
2033 continue;
2034 value_division(f, lcm, S->Constraint[j][1+nvar+i]);
2035 Vector_Scale(S->Constraint[j], M->p[c], f, S->Dimension+2);
2036 value_substract(M->p[c][S->Dimension+1],
2037 M->p[c][S->Dimension+1],
2038 lcm);
2039 value_increment(M->p[c][S->Dimension+1],
2040 M->p[c][S->Dimension+1]);
2041 ++c;
2043 Polyhedron *O = S;
2044 S = AddConstraints(M->p[0], c, S, MaxRays);
2045 if (O != P)
2046 Polyhedron_Free(O);
2047 Matrix_Free(M);
2048 if (emptyQ(S)) {
2049 Polyhedron_Free(S);
2050 value_clear(lcm);
2051 value_clear(f);
2052 return 0;
2055 value_clear(lcm);
2056 value_clear(f);
2058 #ifdef DEBUG_ER
2059 fprintf(stderr, "\nER: Sure\n");
2060 #endif /* DEBUG_ER */
2062 return split_sure(P, S, exist, nparam, MaxRays);
2065 static evalue* enumerate_sure2(Polyhedron *P,
2066 unsigned exist, unsigned nparam, unsigned MaxRays)
2068 int nvar = P->Dimension - exist - nparam;
2069 int r;
2070 for (r = 0; r < P->NbRays; ++r)
2071 if (value_one_p(P->Ray[r][0]) &&
2072 value_one_p(P->Ray[r][P->Dimension+1]))
2073 break;
2075 if (r >= P->NbRays)
2076 return 0;
2078 Matrix *M = Matrix_Alloc(nvar + 1 + nparam, P->Dimension+2);
2079 for (int i = 0; i < nvar; ++i)
2080 value_set_si(M->p[i][1+i], 1);
2081 for (int i = 0; i < nparam; ++i)
2082 value_set_si(M->p[i+nvar][1+nvar+exist+i], 1);
2083 Vector_Copy(P->Ray[r]+1+nvar, M->p[nvar+nparam]+1+nvar, exist);
2084 value_set_si(M->p[nvar+nparam][0], 1);
2085 value_set_si(M->p[nvar+nparam][P->Dimension+1], 1);
2086 Polyhedron * F = Rays2Polyhedron(M, MaxRays);
2087 Matrix_Free(M);
2089 Polyhedron *I = DomainIntersection(F, P, MaxRays);
2090 Polyhedron_Free(F);
2092 #ifdef DEBUG_ER
2093 fprintf(stderr, "\nER: Sure2\n");
2094 #endif /* DEBUG_ER */
2096 return split_sure(P, I, exist, nparam, MaxRays);
2099 static evalue* enumerate_cyclic(Polyhedron *P,
2100 unsigned exist, unsigned nparam,
2101 evalue * EP, int r, int p, unsigned MaxRays)
2103 int nvar = P->Dimension - exist - nparam;
2105 /* If EP in its fractional maps only contains references
2106 * to the remainder parameter with appropriate coefficients
2107 * then we could in principle avoid adding existentially
2108 * quantified variables to the validity domains.
2109 * We'd have to replace the remainder by m { p/m }
2110 * and multiply with an appropriate factor that is one
2111 * only in the appropriate range.
2112 * This last multiplication can be avoided if EP
2113 * has a single validity domain with no (further)
2114 * constraints on the remainder parameter
2117 Matrix *CT = Matrix_Alloc(nparam+1, nparam+3);
2118 Matrix *M = Matrix_Alloc(1, 1+nparam+3);
2119 for (int j = 0; j < nparam; ++j)
2120 if (j != p)
2121 value_set_si(CT->p[j][j], 1);
2122 value_set_si(CT->p[p][nparam+1], 1);
2123 value_set_si(CT->p[nparam][nparam+2], 1);
2124 value_set_si(M->p[0][1+p], -1);
2125 value_absolute(M->p[0][1+nparam], P->Ray[0][1+nvar+exist+p]);
2126 value_set_si(M->p[0][1+nparam+1], 1);
2127 Polyhedron *CEq = Constraints2Polyhedron(M, 1);
2128 Matrix_Free(M);
2129 addeliminatedparams_enum(EP, CT, CEq, MaxRays, nparam);
2130 Polyhedron_Free(CEq);
2131 Matrix_Free(CT);
2133 return EP;
2136 static void enumerate_vd_add_ray(evalue *EP, Matrix *Rays, unsigned MaxRays)
2138 if (value_notzero_p(EP->d))
2139 return;
2141 assert(EP->x.p->type == partition);
2142 assert(EP->x.p->pos == EVALUE_DOMAIN(EP->x.p->arr[0])->Dimension);
2143 for (int i = 0; i < EP->x.p->size/2; ++i) {
2144 Polyhedron *D = EVALUE_DOMAIN(EP->x.p->arr[2*i]);
2145 Polyhedron *N = DomainAddRays(D, Rays, MaxRays);
2146 EVALUE_SET_DOMAIN(EP->x.p->arr[2*i], N);
2147 Domain_Free(D);
2151 static evalue* enumerate_line(Polyhedron *P,
2152 unsigned exist, unsigned nparam, unsigned MaxRays)
2154 if (P->NbBid == 0)
2155 return 0;
2157 #ifdef DEBUG_ER
2158 fprintf(stderr, "\nER: Line\n");
2159 #endif /* DEBUG_ER */
2161 int nvar = P->Dimension - exist - nparam;
2162 int i, j;
2163 for (i = 0; i < nparam; ++i)
2164 if (value_notzero_p(P->Ray[0][1+nvar+exist+i]))
2165 break;
2166 assert(i < nparam);
2167 for (j = i+1; j < nparam; ++j)
2168 if (value_notzero_p(P->Ray[0][1+nvar+exist+i]))
2169 break;
2170 assert(j >= nparam); // for now
2172 Matrix *M = Matrix_Alloc(2, P->Dimension+2);
2173 value_set_si(M->p[0][0], 1);
2174 value_set_si(M->p[0][1+nvar+exist+i], 1);
2175 value_set_si(M->p[1][0], 1);
2176 value_set_si(M->p[1][1+nvar+exist+i], -1);
2177 value_absolute(M->p[1][1+P->Dimension], P->Ray[0][1+nvar+exist+i]);
2178 value_decrement(M->p[1][1+P->Dimension], M->p[1][1+P->Dimension]);
2179 Polyhedron *S = AddConstraints(M->p[0], 2, P, MaxRays);
2180 evalue *EP = barvinok_enumerate_e(S, exist, nparam, MaxRays);
2181 Polyhedron_Free(S);
2182 Matrix_Free(M);
2184 return enumerate_cyclic(P, exist, nparam, EP, 0, i, MaxRays);
2187 static int single_param_pos(Polyhedron*P, unsigned exist, unsigned nparam,
2188 int r)
2190 int nvar = P->Dimension - exist - nparam;
2191 if (First_Non_Zero(P->Ray[r]+1, nvar) != -1)
2192 return -1;
2193 int i = First_Non_Zero(P->Ray[r]+1+nvar+exist, nparam);
2194 if (i == -1)
2195 return -1;
2196 if (First_Non_Zero(P->Ray[r]+1+nvar+exist+1, nparam-i-1) != -1)
2197 return -1;
2198 return i;
2201 static evalue* enumerate_remove_ray(Polyhedron *P, int r,
2202 unsigned exist, unsigned nparam, unsigned MaxRays)
2204 #ifdef DEBUG_ER
2205 fprintf(stderr, "\nER: RedundantRay\n");
2206 #endif /* DEBUG_ER */
2208 Value one;
2209 value_init(one);
2210 value_set_si(one, 1);
2211 int len = P->NbRays-1;
2212 Matrix *M = Matrix_Alloc(2 * len, P->Dimension+2);
2213 Vector_Copy(P->Ray[0], M->p[0], r * (P->Dimension+2));
2214 Vector_Copy(P->Ray[r+1], M->p[r], (len-r) * (P->Dimension+2));
2215 for (int j = 0; j < P->NbRays; ++j) {
2216 if (j == r)
2217 continue;
2218 Vector_Combine(P->Ray[j], P->Ray[r], M->p[len+j-(j>r)],
2219 one, P->Ray[j][P->Dimension+1], P->Dimension+2);
2222 P = Rays2Polyhedron(M, MaxRays);
2223 Matrix_Free(M);
2224 evalue *EP = barvinok_enumerate_e(P, exist, nparam, MaxRays);
2225 Polyhedron_Free(P);
2226 value_clear(one);
2228 return EP;
2231 static evalue* enumerate_redundant_ray(Polyhedron *P,
2232 unsigned exist, unsigned nparam, unsigned MaxRays)
2234 assert(P->NbBid == 0);
2235 int nvar = P->Dimension - exist - nparam;
2236 Value m;
2237 value_init(m);
2239 for (int r = 0; r < P->NbRays; ++r) {
2240 if (value_notzero_p(P->Ray[r][P->Dimension+1]))
2241 continue;
2242 int i1 = single_param_pos(P, exist, nparam, r);
2243 if (i1 == -1)
2244 continue;
2245 for (int r2 = r+1; r2 < P->NbRays; ++r2) {
2246 if (value_notzero_p(P->Ray[r2][P->Dimension+1]))
2247 continue;
2248 int i2 = single_param_pos(P, exist, nparam, r2);
2249 if (i2 == -1)
2250 continue;
2251 if (i1 != i2)
2252 continue;
2254 value_division(m, P->Ray[r][1+nvar+exist+i1],
2255 P->Ray[r2][1+nvar+exist+i1]);
2256 value_multiply(m, m, P->Ray[r2][1+nvar+exist+i1]);
2257 /* r2 divides r => r redundant */
2258 if (value_eq(m, P->Ray[r][1+nvar+exist+i1])) {
2259 value_clear(m);
2260 return enumerate_remove_ray(P, r, exist, nparam, MaxRays);
2263 value_division(m, P->Ray[r2][1+nvar+exist+i1],
2264 P->Ray[r][1+nvar+exist+i1]);
2265 value_multiply(m, m, P->Ray[r][1+nvar+exist+i1]);
2266 /* r divides r2 => r2 redundant */
2267 if (value_eq(m, P->Ray[r2][1+nvar+exist+i1])) {
2268 value_clear(m);
2269 return enumerate_remove_ray(P, r2, exist, nparam, MaxRays);
2273 value_clear(m);
2274 return 0;
2277 static Polyhedron *upper_bound(Polyhedron *P,
2278 int pos, Value *max, Polyhedron **R)
2280 Value v;
2281 int r;
2282 value_init(v);
2284 *R = 0;
2285 Polyhedron *N;
2286 Polyhedron *B = 0;
2287 for (Polyhedron *Q = P; Q; Q = N) {
2288 N = Q->next;
2289 for (r = 0; r < P->NbRays; ++r) {
2290 if (value_zero_p(P->Ray[r][P->Dimension+1]) &&
2291 value_pos_p(P->Ray[r][1+pos]))
2292 break;
2294 if (r < P->NbRays) {
2295 Q->next = *R;
2296 *R = Q;
2297 continue;
2298 } else {
2299 Q->next = B;
2300 B = Q;
2302 for (r = 0; r < P->NbRays; ++r) {
2303 if (value_zero_p(P->Ray[r][P->Dimension+1]))
2304 continue;
2305 mpz_fdiv_q(v, P->Ray[r][1+pos], P->Ray[r][1+P->Dimension]);
2306 if ((!Q->next && r == 0) || value_gt(v, *max))
2307 value_assign(*max, v);
2310 value_clear(v);
2311 return B;
2314 static evalue* enumerate_ray(Polyhedron *P,
2315 unsigned exist, unsigned nparam, unsigned MaxRays)
2317 assert(P->NbBid == 0);
2318 int nvar = P->Dimension - exist - nparam;
2320 int r;
2321 for (r = 0; r < P->NbRays; ++r)
2322 if (value_zero_p(P->Ray[r][P->Dimension+1]))
2323 break;
2324 if (r >= P->NbRays)
2325 return 0;
2327 int r2;
2328 for (r2 = r+1; r2 < P->NbRays; ++r2)
2329 if (value_zero_p(P->Ray[r2][P->Dimension+1]))
2330 break;
2331 if (r2 < P->NbRays) {
2332 if (nvar > 0)
2333 return enumerate_sum(P, exist, nparam, MaxRays);
2336 #ifdef DEBUG_ER
2337 fprintf(stderr, "\nER: Ray\n");
2338 #endif /* DEBUG_ER */
2340 Value m;
2341 Value one;
2342 value_init(m);
2343 value_init(one);
2344 value_set_si(one, 1);
2345 int i = single_param_pos(P, exist, nparam, r);
2346 assert(i != -1); // for now;
2348 Matrix *M = Matrix_Alloc(P->NbRays, P->Dimension+2);
2349 for (int j = 0; j < P->NbRays; ++j) {
2350 Vector_Combine(P->Ray[j], P->Ray[r], M->p[j],
2351 one, P->Ray[j][P->Dimension+1], P->Dimension+2);
2353 Polyhedron *S = Rays2Polyhedron(M, MaxRays);
2354 Matrix_Free(M);
2355 Polyhedron *D = DomainDifference(P, S, MaxRays);
2356 Polyhedron_Free(S);
2357 // Polyhedron_Print(stderr, P_VALUE_FMT, D);
2358 assert(value_pos_p(P->Ray[r][1+nvar+exist+i])); // for now
2359 Polyhedron *R;
2360 D = upper_bound(D, nvar+exist+i, &m, &R);
2361 assert(D);
2362 Domain_Free(D);
2364 M = Matrix_Alloc(2, P->Dimension+2);
2365 value_set_si(M->p[0][0], 1);
2366 value_set_si(M->p[1][0], 1);
2367 value_set_si(M->p[0][1+nvar+exist+i], -1);
2368 value_set_si(M->p[1][1+nvar+exist+i], 1);
2369 value_assign(M->p[0][1+P->Dimension], m);
2370 value_oppose(M->p[1][1+P->Dimension], m);
2371 value_addto(M->p[1][1+P->Dimension], M->p[1][1+P->Dimension],
2372 P->Ray[r][1+nvar+exist+i]);
2373 value_decrement(M->p[1][1+P->Dimension], M->p[1][1+P->Dimension]);
2374 // Matrix_Print(stderr, P_VALUE_FMT, M);
2375 D = AddConstraints(M->p[0], 2, P, MaxRays);
2376 // Polyhedron_Print(stderr, P_VALUE_FMT, D);
2377 value_substract(M->p[0][1+P->Dimension], M->p[0][1+P->Dimension],
2378 P->Ray[r][1+nvar+exist+i]);
2379 // Matrix_Print(stderr, P_VALUE_FMT, M);
2380 S = AddConstraints(M->p[0], 1, P, MaxRays);
2381 // Polyhedron_Print(stderr, P_VALUE_FMT, S);
2382 Matrix_Free(M);
2384 evalue *EP = barvinok_enumerate_e(D, exist, nparam, MaxRays);
2385 Polyhedron_Free(D);
2386 value_clear(one);
2387 value_clear(m);
2389 if (value_notone_p(P->Ray[r][1+nvar+exist+i]))
2390 EP = enumerate_cyclic(P, exist, nparam, EP, r, i, MaxRays);
2391 else {
2392 M = Matrix_Alloc(1, nparam+2);
2393 value_set_si(M->p[0][0], 1);
2394 value_set_si(M->p[0][1+i], 1);
2395 enumerate_vd_add_ray(EP, M, MaxRays);
2396 Matrix_Free(M);
2399 if (!emptyQ(S)) {
2400 evalue *E = barvinok_enumerate_e(S, exist, nparam, MaxRays);
2401 eadd(E, EP);
2402 free_evalue_refs(E);
2403 free(E);
2405 Polyhedron_Free(S);
2407 if (R) {
2408 assert(nvar == 0);
2409 evalue *ER = enumerate_or(R, exist, nparam, MaxRays);
2410 eor(ER, EP);
2411 free_evalue_refs(ER);
2412 free(ER);
2415 return EP;
2418 static evalue* new_zero_ep()
2420 evalue *EP;
2421 ALLOC(evalue, EP);
2422 value_init(EP->d);
2423 evalue_set_si(EP, 0, 1);
2424 return EP;
2427 static evalue* enumerate_vd(Polyhedron **PA,
2428 unsigned exist, unsigned nparam, unsigned MaxRays)
2430 Polyhedron *P = *PA;
2431 int nvar = P->Dimension - exist - nparam;
2432 Param_Polyhedron *PP = NULL;
2433 Polyhedron *C = Universe_Polyhedron(nparam);
2434 Polyhedron *CEq;
2435 Matrix *CT;
2436 Polyhedron *PR = P;
2437 PP = Polyhedron2Param_SimplifiedDomain(&PR,C,MaxRays,&CEq,&CT);
2438 Polyhedron_Free(C);
2440 int nd;
2441 Param_Domain *D, *last;
2442 Value c;
2443 value_init(c);
2444 for (nd = 0, D=PP->D; D; D=D->next, ++nd)
2447 Polyhedron **VD = new Polyhedron_p[nd];
2448 Polyhedron **fVD = new Polyhedron_p[nd];
2449 for(nd = 0, D=PP->D; D; D=D->next) {
2450 Polyhedron *rVD = reduce_domain(D->Domain, CT, CEq,
2451 fVD, nd, MaxRays);
2452 if (!rVD)
2453 continue;
2455 VD[nd++] = rVD;
2456 last = D;
2459 evalue *EP = 0;
2461 if (nd == 0)
2462 EP = new_zero_ep();
2464 /* This doesn't seem to have any effect */
2465 if (nd == 1) {
2466 Polyhedron *CA = align_context(VD[0], P->Dimension, MaxRays);
2467 Polyhedron *O = P;
2468 P = DomainIntersection(P, CA, MaxRays);
2469 if (O != *PA)
2470 Polyhedron_Free(O);
2471 Polyhedron_Free(CA);
2472 if (emptyQ(P))
2473 EP = new_zero_ep();
2476 if (!EP && CT->NbColumns != CT->NbRows) {
2477 Polyhedron *CEqr = DomainImage(CEq, CT, MaxRays);
2478 Polyhedron *CA = align_context(CEqr, PR->Dimension, MaxRays);
2479 Polyhedron *I = DomainIntersection(PR, CA, MaxRays);
2480 Polyhedron_Free(CEqr);
2481 Polyhedron_Free(CA);
2482 #ifdef DEBUG_ER
2483 fprintf(stderr, "\nER: Eliminate\n");
2484 #endif /* DEBUG_ER */
2485 nparam -= CT->NbColumns - CT->NbRows;
2486 EP = barvinok_enumerate_e(I, exist, nparam, MaxRays);
2487 nparam += CT->NbColumns - CT->NbRows;
2488 addeliminatedparams_enum(EP, CT, CEq, MaxRays, nparam);
2489 Polyhedron_Free(I);
2491 if (PR != *PA)
2492 Polyhedron_Free(PR);
2493 PR = 0;
2495 if (!EP && nd > 1) {
2496 #ifdef DEBUG_ER
2497 fprintf(stderr, "\nER: VD\n");
2498 #endif /* DEBUG_ER */
2499 for (int i = 0; i < nd; ++i) {
2500 Polyhedron *CA = align_context(VD[i], P->Dimension, MaxRays);
2501 Polyhedron *I = DomainIntersection(P, CA, MaxRays);
2503 if (i == 0)
2504 EP = barvinok_enumerate_e(I, exist, nparam, MaxRays);
2505 else {
2506 evalue *E = barvinok_enumerate_e(I, exist, nparam, MaxRays);
2507 eadd(E, EP);
2508 free_evalue_refs(E);
2509 free(E);
2511 Polyhedron_Free(I);
2512 Polyhedron_Free(CA);
2516 for (int i = 0; i < nd; ++i) {
2517 Polyhedron_Free(VD[i]);
2518 Polyhedron_Free(fVD[i]);
2520 delete [] VD;
2521 delete [] fVD;
2522 value_clear(c);
2524 if (!EP && nvar == 0) {
2525 Value f;
2526 value_init(f);
2527 Param_Vertices *V, *V2;
2528 Matrix* M = Matrix_Alloc(1, P->Dimension+2);
2530 FORALL_PVertex_in_ParamPolyhedron(V, last, PP) {
2531 bool found = false;
2532 FORALL_PVertex_in_ParamPolyhedron(V2, last, PP) {
2533 if (V == V2) {
2534 found = true;
2535 continue;
2537 if (!found)
2538 continue;
2539 for (int i = 0; i < exist; ++i) {
2540 value_oppose(f, V->Vertex->p[i][nparam+1]);
2541 Vector_Combine(V->Vertex->p[i],
2542 V2->Vertex->p[i],
2543 M->p[0] + 1 + nvar + exist,
2544 V2->Vertex->p[i][nparam+1],
2546 nparam+1);
2547 int j;
2548 for (j = 0; j < nparam; ++j)
2549 if (value_notzero_p(M->p[0][1+nvar+exist+j]))
2550 break;
2551 if (j >= nparam)
2552 continue;
2553 ConstraintSimplify(M->p[0], M->p[0],
2554 P->Dimension+2, &f);
2555 value_set_si(M->p[0][0], 0);
2556 Polyhedron *para = AddConstraints(M->p[0], 1, P,
2557 MaxRays);
2558 if (emptyQ(para)) {
2559 Polyhedron_Free(para);
2560 continue;
2562 Polyhedron *pos, *neg;
2563 value_set_si(M->p[0][0], 1);
2564 value_decrement(M->p[0][P->Dimension+1],
2565 M->p[0][P->Dimension+1]);
2566 neg = AddConstraints(M->p[0], 1, P, MaxRays);
2567 value_set_si(f, -1);
2568 Vector_Scale(M->p[0]+1, M->p[0]+1, f,
2569 P->Dimension+1);
2570 value_decrement(M->p[0][P->Dimension+1],
2571 M->p[0][P->Dimension+1]);
2572 value_decrement(M->p[0][P->Dimension+1],
2573 M->p[0][P->Dimension+1]);
2574 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2575 if (emptyQ(neg) && emptyQ(pos)) {
2576 Polyhedron_Free(para);
2577 Polyhedron_Free(pos);
2578 Polyhedron_Free(neg);
2579 continue;
2581 #ifdef DEBUG_ER
2582 fprintf(stderr, "\nER: Order\n");
2583 #endif /* DEBUG_ER */
2584 EP = barvinok_enumerate_e(para, exist, nparam, MaxRays);
2585 evalue *E;
2586 if (!emptyQ(pos)) {
2587 E = barvinok_enumerate_e(pos, exist, nparam, MaxRays);
2588 eadd(E, EP);
2589 free_evalue_refs(E);
2590 free(E);
2592 if (!emptyQ(neg)) {
2593 E = barvinok_enumerate_e(neg, exist, nparam, MaxRays);
2594 eadd(E, EP);
2595 free_evalue_refs(E);
2596 free(E);
2598 Polyhedron_Free(para);
2599 Polyhedron_Free(pos);
2600 Polyhedron_Free(neg);
2601 break;
2603 if (EP)
2604 break;
2605 } END_FORALL_PVertex_in_ParamPolyhedron;
2606 if (EP)
2607 break;
2608 } END_FORALL_PVertex_in_ParamPolyhedron;
2610 if (!EP) {
2611 /* Search for vertex coordinate to split on */
2612 /* First look for one independent of the parameters */
2613 FORALL_PVertex_in_ParamPolyhedron(V, last, PP) {
2614 for (int i = 0; i < exist; ++i) {
2615 int j;
2616 for (j = 0; j < nparam; ++j)
2617 if (value_notzero_p(V->Vertex->p[i][j]))
2618 break;
2619 if (j < nparam)
2620 continue;
2621 value_set_si(M->p[0][0], 1);
2622 Vector_Set(M->p[0]+1, 0, nvar+exist);
2623 Vector_Copy(V->Vertex->p[i],
2624 M->p[0] + 1 + nvar + exist, nparam+1);
2625 value_oppose(M->p[0][1+nvar+i],
2626 V->Vertex->p[i][nparam+1]);
2628 Polyhedron *pos, *neg;
2629 value_set_si(M->p[0][0], 1);
2630 value_decrement(M->p[0][P->Dimension+1],
2631 M->p[0][P->Dimension+1]);
2632 neg = AddConstraints(M->p[0], 1, P, MaxRays);
2633 value_set_si(f, -1);
2634 Vector_Scale(M->p[0]+1, M->p[0]+1, f,
2635 P->Dimension+1);
2636 value_decrement(M->p[0][P->Dimension+1],
2637 M->p[0][P->Dimension+1]);
2638 value_decrement(M->p[0][P->Dimension+1],
2639 M->p[0][P->Dimension+1]);
2640 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2641 if (emptyQ(neg) || emptyQ(pos)) {
2642 Polyhedron_Free(pos);
2643 Polyhedron_Free(neg);
2644 continue;
2646 Polyhedron_Free(pos);
2647 value_increment(M->p[0][P->Dimension+1],
2648 M->p[0][P->Dimension+1]);
2649 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2650 #ifdef DEBUG_ER
2651 fprintf(stderr, "\nER: Vertex\n");
2652 #endif /* DEBUG_ER */
2653 pos->next = neg;
2654 EP = enumerate_or(pos, exist, nparam, MaxRays);
2655 break;
2657 if (EP)
2658 break;
2659 } END_FORALL_PVertex_in_ParamPolyhedron;
2662 if (!EP) {
2663 /* Search for vertex coordinate to split on */
2664 /* Now look for one that depends on the parameters */
2665 FORALL_PVertex_in_ParamPolyhedron(V, last, PP) {
2666 for (int i = 0; i < exist; ++i) {
2667 value_set_si(M->p[0][0], 1);
2668 Vector_Set(M->p[0]+1, 0, nvar+exist);
2669 Vector_Copy(V->Vertex->p[i],
2670 M->p[0] + 1 + nvar + exist, nparam+1);
2671 value_oppose(M->p[0][1+nvar+i],
2672 V->Vertex->p[i][nparam+1]);
2674 Polyhedron *pos, *neg;
2675 value_set_si(M->p[0][0], 1);
2676 value_decrement(M->p[0][P->Dimension+1],
2677 M->p[0][P->Dimension+1]);
2678 neg = AddConstraints(M->p[0], 1, P, MaxRays);
2679 value_set_si(f, -1);
2680 Vector_Scale(M->p[0]+1, M->p[0]+1, f,
2681 P->Dimension+1);
2682 value_decrement(M->p[0][P->Dimension+1],
2683 M->p[0][P->Dimension+1]);
2684 value_decrement(M->p[0][P->Dimension+1],
2685 M->p[0][P->Dimension+1]);
2686 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2687 if (emptyQ(neg) || emptyQ(pos)) {
2688 Polyhedron_Free(pos);
2689 Polyhedron_Free(neg);
2690 continue;
2692 Polyhedron_Free(pos);
2693 value_increment(M->p[0][P->Dimension+1],
2694 M->p[0][P->Dimension+1]);
2695 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2696 #ifdef DEBUG_ER
2697 fprintf(stderr, "\nER: ParamVertex\n");
2698 #endif /* DEBUG_ER */
2699 pos->next = neg;
2700 EP = enumerate_or(pos, exist, nparam, MaxRays);
2701 break;
2703 if (EP)
2704 break;
2705 } END_FORALL_PVertex_in_ParamPolyhedron;
2708 Matrix_Free(M);
2709 value_clear(f);
2712 if (CEq)
2713 Polyhedron_Free(CEq);
2714 if (CT)
2715 Matrix_Free(CT);
2716 if (PP)
2717 Param_Polyhedron_Free(PP);
2718 *PA = P;
2720 return EP;
2723 #ifndef HAVE_PIPLIB
2724 evalue *barvinok_enumerate_pip(Polyhedron *P,
2725 unsigned exist, unsigned nparam, unsigned MaxRays)
2727 return 0;
2729 #else
2730 evalue *barvinok_enumerate_pip(Polyhedron *P,
2731 unsigned exist, unsigned nparam, unsigned MaxRays)
2733 int nvar = P->Dimension - exist - nparam;
2734 evalue *EP = new_zero_ep();
2735 Polyhedron *Q, *N, *T = 0;
2736 Value min, tmp;
2737 value_init(min);
2738 value_init(tmp);
2740 #ifdef DEBUG_ER
2741 fprintf(stderr, "\nER: PIP\n");
2742 #endif /* DEBUG_ER */
2744 for (int i = 0; i < P->Dimension; ++i) {
2745 bool pos = false;
2746 bool neg = false;
2747 bool posray = false;
2748 bool negray = false;
2749 value_set_si(min, 0);
2750 for (int j = 0; j < P->NbRays; ++j) {
2751 if (value_pos_p(P->Ray[j][1+i])) {
2752 pos = true;
2753 if (value_zero_p(P->Ray[j][1+P->Dimension]))
2754 posray = true;
2755 } else if (value_neg_p(P->Ray[j][1+i])) {
2756 neg = true;
2757 if (value_zero_p(P->Ray[j][1+P->Dimension]))
2758 negray = true;
2759 else {
2760 mpz_fdiv_q(tmp,
2761 P->Ray[j][1+i], P->Ray[j][1+P->Dimension]);
2762 if (value_lt(tmp, min))
2763 value_assign(min, tmp);
2767 if (pos && neg) {
2768 assert(!(posray && negray));
2769 assert(!negray); // for now
2770 Polyhedron *O = T ? T : P;
2771 /* shift by a safe amount */
2772 Matrix *M = Matrix_Alloc(O->NbRays, O->Dimension+2);
2773 Vector_Copy(O->Ray[0], M->p[0], O->NbRays * (O->Dimension+2));
2774 for (int j = 0; j < P->NbRays; ++j) {
2775 if (value_notzero_p(M->p[j][1+P->Dimension])) {
2776 value_multiply(tmp, min, M->p[j][1+P->Dimension]);
2777 value_substract(M->p[j][1+i], M->p[j][1+i], tmp);
2780 if (T)
2781 Polyhedron_Free(T);
2782 T = Rays2Polyhedron(M, MaxRays);
2783 Matrix_Free(M);
2784 } else if (neg) {
2785 /* negating a parameter requires that we substitute in the
2786 * sign again afterwards.
2787 * Disallow for now.
2789 assert(i < nvar+exist);
2790 if (!T)
2791 T = Polyhedron_Copy(P);
2792 for (int j = 0; j < T->NbRays; ++j)
2793 value_oppose(T->Ray[j][1+i], T->Ray[j][1+i]);
2794 for (int j = 0; j < T->NbConstraints; ++j)
2795 value_oppose(T->Constraint[j][1+i], T->Constraint[j][1+i]);
2798 value_clear(min);
2799 value_clear(tmp);
2801 Polyhedron *D = pip_lexmin(T ? T : P, exist, nparam);
2802 for (Q = D; Q; Q = N) {
2803 N = Q->next;
2804 Q->next = 0;
2805 evalue *E;
2806 exist = Q->Dimension - nvar - nparam;
2807 E = barvinok_enumerate_e(Q, exist, nparam, MaxRays);
2808 Polyhedron_Free(Q);
2809 eadd(E, EP);
2810 free_evalue_refs(E);
2811 free(E);
2814 if (T)
2815 Polyhedron_Free(T);
2817 return EP;
2819 #endif
2822 static bool is_single(Value *row, int pos, int len)
2824 return First_Non_Zero(row, pos) == -1 &&
2825 First_Non_Zero(row+pos+1, len-pos-1) == -1;
2828 static evalue* barvinok_enumerate_e_r(Polyhedron *P,
2829 unsigned exist, unsigned nparam, unsigned MaxRays);
2831 #ifdef DEBUG_ER
2832 static int er_level = 0;
2834 evalue* barvinok_enumerate_e(Polyhedron *P,
2835 unsigned exist, unsigned nparam, unsigned MaxRays)
2837 fprintf(stderr, "\nER: level %i\n", er_level);
2838 int nvar = P->Dimension - exist - nparam;
2839 fprintf(stderr, "%d %d %d\n", nvar, exist, nparam);
2841 Polyhedron_Print(stderr, P_VALUE_FMT, P);
2842 ++er_level;
2843 P = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
2844 evalue *EP = barvinok_enumerate_e_r(P, exist, nparam, MaxRays);
2845 Polyhedron_Free(P);
2846 --er_level;
2847 return EP;
2849 #else
2850 evalue* barvinok_enumerate_e(Polyhedron *P,
2851 unsigned exist, unsigned nparam, unsigned MaxRays)
2853 P = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
2854 evalue *EP = barvinok_enumerate_e_r(P, exist, nparam, MaxRays);
2855 Polyhedron_Free(P);
2856 return EP;
2858 #endif
2860 static evalue* barvinok_enumerate_e_r(Polyhedron *P,
2861 unsigned exist, unsigned nparam, unsigned MaxRays)
2863 if (exist == 0) {
2864 Polyhedron *U = Universe_Polyhedron(nparam);
2865 evalue *EP = barvinok_enumerate_ev(P, U, MaxRays);
2866 //char *param_name[] = {"P", "Q", "R", "S", "T" };
2867 //print_evalue(stdout, EP, param_name);
2868 Polyhedron_Free(U);
2869 return EP;
2872 int nvar = P->Dimension - exist - nparam;
2873 int len = P->Dimension + 2;
2875 if (emptyQ(P))
2876 return new_zero_ep();
2878 if (nvar == 0 && nparam == 0) {
2879 evalue *EP = new_zero_ep();
2880 barvinok_count(P, &EP->x.n, MaxRays);
2881 if (value_pos_p(EP->x.n))
2882 value_set_si(EP->x.n, 1);
2883 return EP;
2886 int r;
2887 for (r = 0; r < P->NbRays; ++r)
2888 if (value_zero_p(P->Ray[r][0]) ||
2889 value_zero_p(P->Ray[r][P->Dimension+1])) {
2890 int i;
2891 for (i = 0; i < nvar; ++i)
2892 if (value_notzero_p(P->Ray[r][i+1]))
2893 break;
2894 if (i >= nvar)
2895 continue;
2896 for (i = nvar + exist; i < nvar + exist + nparam; ++i)
2897 if (value_notzero_p(P->Ray[r][i+1]))
2898 break;
2899 if (i >= nvar + exist + nparam)
2900 break;
2902 if (r < P->NbRays) {
2903 evalue *EP = new_zero_ep();
2904 value_set_si(EP->x.n, -1);
2905 return EP;
2908 int first;
2909 for (r = 0; r < P->NbEq; ++r)
2910 if ((first = First_Non_Zero(P->Constraint[r]+1+nvar, exist)) != -1)
2911 break;
2912 if (r < P->NbEq) {
2913 if (First_Non_Zero(P->Constraint[r]+1+nvar+first+1,
2914 exist-first-1) != -1) {
2915 Polyhedron *T = rotate_along(P, r, nvar, exist, MaxRays);
2916 #ifdef DEBUG_ER
2917 fprintf(stderr, "\nER: Equality\n");
2918 #endif /* DEBUG_ER */
2919 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2920 Polyhedron_Free(T);
2921 return EP;
2922 } else {
2923 #ifdef DEBUG_ER
2924 fprintf(stderr, "\nER: Fixed\n");
2925 #endif /* DEBUG_ER */
2926 if (first == 0)
2927 return barvinok_enumerate_e(P, exist-1, nparam, MaxRays);
2928 else {
2929 Polyhedron *T = Polyhedron_Copy(P);
2930 SwapColumns(T, nvar+1, nvar+1+first);
2931 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2932 Polyhedron_Free(T);
2933 return EP;
2938 Vector *row = Vector_Alloc(len);
2939 value_set_si(row->p[0], 1);
2941 Value f;
2942 value_init(f);
2944 enum constraint* info = new constraint[exist];
2945 for (int i = 0; i < exist; ++i) {
2946 info[i] = ALL_POS;
2947 for (int l = P->NbEq; l < P->NbConstraints; ++l) {
2948 if (value_negz_p(P->Constraint[l][nvar+i+1]))
2949 continue;
2950 bool l_parallel = is_single(P->Constraint[l]+nvar+1, i, exist);
2951 for (int u = P->NbEq; u < P->NbConstraints; ++u) {
2952 if (value_posz_p(P->Constraint[u][nvar+i+1]))
2953 continue;
2954 bool lu_parallel = l_parallel ||
2955 is_single(P->Constraint[u]+nvar+1, i, exist);
2956 value_oppose(f, P->Constraint[u][nvar+i+1]);
2957 Vector_Combine(P->Constraint[l]+1, P->Constraint[u]+1, row->p+1,
2958 f, P->Constraint[l][nvar+i+1], len-1);
2959 if (!(info[i] & INDEPENDENT)) {
2960 int j;
2961 for (j = 0; j < exist; ++j)
2962 if (j != i && value_notzero_p(row->p[nvar+j+1]))
2963 break;
2964 if (j == exist) {
2965 //printf("independent: i: %d, l: %d, u: %d\n", i, l, u);
2966 info[i] = (constraint)(info[i] | INDEPENDENT);
2969 if (info[i] & ALL_POS) {
2970 value_addto(row->p[len-1], row->p[len-1],
2971 P->Constraint[l][nvar+i+1]);
2972 value_addto(row->p[len-1], row->p[len-1], f);
2973 value_multiply(f, f, P->Constraint[l][nvar+i+1]);
2974 value_substract(row->p[len-1], row->p[len-1], f);
2975 value_decrement(row->p[len-1], row->p[len-1]);
2976 ConstraintSimplify(row->p, row->p, len, &f);
2977 value_set_si(f, -1);
2978 Vector_Scale(row->p+1, row->p+1, f, len-1);
2979 value_decrement(row->p[len-1], row->p[len-1]);
2980 Polyhedron *T = AddConstraints(row->p, 1, P, MaxRays);
2981 if (!emptyQ(T)) {
2982 //printf("not all_pos: i: %d, l: %d, u: %d\n", i, l, u);
2983 info[i] = (constraint)(info[i] ^ ALL_POS);
2985 //puts("pos remainder");
2986 //Polyhedron_Print(stdout, P_VALUE_FMT, T);
2987 Polyhedron_Free(T);
2989 if (!(info[i] & ONE_NEG)) {
2990 if (lu_parallel) {
2991 negative_test_constraint(P->Constraint[l],
2992 P->Constraint[u],
2993 row->p, nvar+i, len, &f);
2994 oppose_constraint(row->p, len, &f);
2995 Polyhedron *T = AddConstraints(row->p, 1, P, MaxRays);
2996 if (emptyQ(T)) {
2997 //printf("one_neg i: %d, l: %d, u: %d\n", i, l, u);
2998 info[i] = (constraint)(info[i] | ONE_NEG);
3000 //puts("neg remainder");
3001 //Polyhedron_Print(stdout, P_VALUE_FMT, T);
3002 Polyhedron_Free(T);
3005 if (!(info[i] & ALL_POS) && (info[i] & ONE_NEG))
3006 goto next;
3009 if (info[i] & ALL_POS)
3010 break;
3011 next:
3016 for (int i = 0; i < exist; ++i)
3017 printf("%i: %i\n", i, info[i]);
3019 for (int i = 0; i < exist; ++i)
3020 if (info[i] & ALL_POS) {
3021 #ifdef DEBUG_ER
3022 fprintf(stderr, "\nER: Positive\n");
3023 #endif /* DEBUG_ER */
3024 // Eliminate
3025 // Maybe we should chew off some of the fat here
3026 Matrix *M = Matrix_Alloc(P->Dimension, P->Dimension+1);
3027 for (int j = 0; j < P->Dimension; ++j)
3028 value_set_si(M->p[j][j + (j >= i+nvar)], 1);
3029 Polyhedron *T = Polyhedron_Image(P, M, MaxRays);
3030 Matrix_Free(M);
3031 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
3032 Polyhedron_Free(T);
3033 value_clear(f);
3034 Vector_Free(row);
3035 delete [] info;
3036 return EP;
3038 for (int i = 0; i < exist; ++i)
3039 if (info[i] & ONE_NEG) {
3040 #ifdef DEBUG_ER
3041 fprintf(stderr, "\nER: Negative\n");
3042 #endif /* DEBUG_ER */
3043 Vector_Free(row);
3044 value_clear(f);
3045 delete [] info;
3046 if (i == 0)
3047 return barvinok_enumerate_e(P, exist-1, nparam, MaxRays);
3048 else {
3049 Polyhedron *T = Polyhedron_Copy(P);
3050 SwapColumns(T, nvar+1, nvar+1+i);
3051 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
3052 Polyhedron_Free(T);
3053 return EP;
3056 for (int i = 0; i < exist; ++i)
3057 if (info[i] & INDEPENDENT) {
3058 Polyhedron *pos, *neg;
3060 /* Find constraint again and split off negative part */
3062 if (SplitOnVar(P, i, nvar, len, exist, MaxRays,
3063 row, f, true, &pos, &neg)) {
3064 #ifdef DEBUG_ER
3065 fprintf(stderr, "\nER: Split\n");
3066 #endif /* DEBUG_ER */
3068 evalue *EP =
3069 barvinok_enumerate_e(neg, exist-1, nparam, MaxRays);
3070 evalue *E =
3071 barvinok_enumerate_e(pos, exist, nparam, MaxRays);
3072 eadd(E, EP);
3073 free_evalue_refs(E);
3074 free(E);
3075 Polyhedron_Free(neg);
3076 Polyhedron_Free(pos);
3077 value_clear(f);
3078 Vector_Free(row);
3079 delete [] info;
3080 return EP;
3083 delete [] info;
3085 Polyhedron *O = P;
3086 Polyhedron *F;
3088 evalue *EP;
3090 EP = enumerate_line(P, exist, nparam, MaxRays);
3091 if (EP)
3092 goto out;
3094 EP = barvinok_enumerate_pip(P, exist, nparam, MaxRays);
3095 if (EP)
3096 goto out;
3098 EP = enumerate_redundant_ray(P, exist, nparam, MaxRays);
3099 if (EP)
3100 goto out;
3102 EP = enumerate_sure(P, exist, nparam, MaxRays);
3103 if (EP)
3104 goto out;
3106 EP = enumerate_ray(P, exist, nparam, MaxRays);
3107 if (EP)
3108 goto out;
3110 EP = enumerate_sure2(P, exist, nparam, MaxRays);
3111 if (EP)
3112 goto out;
3114 F = unfringe(P, MaxRays);
3115 if (!PolyhedronIncludes(F, P)) {
3116 #ifdef DEBUG_ER
3117 fprintf(stderr, "\nER: Fringed\n");
3118 #endif /* DEBUG_ER */
3119 EP = barvinok_enumerate_e(F, exist, nparam, MaxRays);
3120 Polyhedron_Free(F);
3121 goto out;
3123 Polyhedron_Free(F);
3125 if (nparam)
3126 EP = enumerate_vd(&P, exist, nparam, MaxRays);
3127 if (EP)
3128 goto out2;
3130 if (nvar != 0) {
3131 EP = enumerate_sum(P, exist, nparam, MaxRays);
3132 goto out2;
3135 assert(nvar == 0);
3137 int i;
3138 Polyhedron *pos, *neg;
3139 for (i = 0; i < exist; ++i)
3140 if (SplitOnVar(P, i, nvar, len, exist, MaxRays,
3141 row, f, false, &pos, &neg))
3142 break;
3144 assert (i < exist);
3146 pos->next = neg;
3147 EP = enumerate_or(pos, exist, nparam, MaxRays);
3149 out2:
3150 if (O != P)
3151 Polyhedron_Free(P);
3153 out:
3154 value_clear(f);
3155 Vector_Free(row);
3156 return EP;