allow construction of 0D "nonorthogonal" vector
[barvinok.git] / barvinok.cc
blob546f3bf60f4ddd5f3462ec79154438d7994f021f
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 if (dim == 0)
487 return;
489 for (int i = 2; !found && i <= 50*dim; i+=4) {
490 for (int j = 0; j < MAX_TRY; ++j) {
491 for (int k = 0; k < dim; ++k) {
492 int r = random_int(i)+2;
493 int v = (2*(r%2)-1) * (r >> 1);
494 lambda[k] = v;
496 int k = 0;
497 for (; k < rays.NumRows(); ++k)
498 if (lambda * rays[k] == 0)
499 break;
500 if (k == rays.NumRows()) {
501 found = true;
502 break;
506 assert(found);
509 static void add_rays(mat_ZZ& rays, Polyhedron *i, int *r)
511 unsigned dim = i->Dimension;
512 for (int k = 0; k < i->NbRays; ++k) {
513 if (!value_zero_p(i->Ray[k][dim+1]))
514 continue;
515 values2zz(i->Ray[k]+1, rays[(*r)++], dim);
519 void lattice_point(Value* values, Polyhedron *i, vec_ZZ& vertex)
521 unsigned dim = i->Dimension;
522 if(!value_one_p(values[dim])) {
523 Matrix* Rays = rays(i);
524 Matrix *inv = Matrix_Alloc(Rays->NbRows, Rays->NbColumns);
525 int ok = Matrix_Inverse(Rays, inv);
526 assert(ok);
527 Matrix_Free(Rays);
528 Rays = rays(i);
529 Vector *lambda = Vector_Alloc(dim+1);
530 Vector_Matrix_Product(values, inv, lambda->p);
531 Matrix_Free(inv);
532 for (int j = 0; j < dim; ++j)
533 mpz_cdiv_q(lambda->p[j], lambda->p[j], lambda->p[dim]);
534 value_set_si(lambda->p[dim], 1);
535 Vector *A = Vector_Alloc(dim+1);
536 Vector_Matrix_Product(lambda->p, Rays, A->p);
537 Vector_Free(lambda);
538 Matrix_Free(Rays);
539 values2zz(A->p, vertex, dim);
540 Vector_Free(A);
541 } else
542 values2zz(values, vertex, dim);
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 vec_ZZ vertex;
574 ZZ num, l;
575 Vector * values = Vector_Alloc(dim + 1);
576 Vector_Matrix_Product(val->p, T, values->p);
577 value_assign(values->p[dim], lcm);
578 lattice_point(values->p, i, vertex);
579 num = vertex * lambda;
580 value2zz(lcm, l);
581 num *= l;
582 num += offset;
583 value_init(ev->x.n);
584 zz2value(num, ev->x.n);
585 value_assign(ev->d, lcm);
586 Vector_Free(values);
587 return;
590 value_init(tmp);
591 vec_ZZ vertex;
592 values2zz(T->p[p], vertex, dim);
593 nump = vertex * lambda;
594 if (First_Non_Zero(val->p, p) == -1) {
595 value_assign(tmp, lcm);
596 evalue *ET = term(p, nump, &tmp);
597 eadd(ET, E);
598 free_evalue_refs(ET);
599 delete ET;
602 value_assign(tmp, lcm);
603 if (First_Non_Zero(T->p[p], dim) != -1)
604 Vector_Gcd(T->p[p], dim, &tmp);
605 Gcd(tmp, lcm, &tmp);
606 if (value_lt(tmp, lcm)) {
607 ZZ count;
609 value_division(tmp, lcm, tmp);
610 value_set_si(ev->d, 0);
611 ev->x.p = new_enode(periodic, VALUE_TO_INT(tmp), p+1);
612 value2zz(tmp, count);
613 do {
614 value_decrement(tmp, tmp);
615 --count;
616 ZZ new_offset = offset - count * nump;
617 value_assign(val->p[p], tmp);
618 vertex_period(i, lambda, T, lcm, p+1, val, E,
619 &ev->x.p->arr[VALUE_TO_INT(tmp)], new_offset);
620 } while (value_pos_p(tmp));
621 } else
622 vertex_period(i, lambda, T, lcm, p+1, val, E, ev, offset);
623 value_clear(tmp);
626 static void mask_r(Matrix *f, int nr, Vector *lcm, int p, Vector *val, evalue *ev)
628 unsigned nparam = lcm->Size;
630 if (p == nparam) {
631 Vector * prod = Vector_Alloc(f->NbRows);
632 Matrix_Vector_Product(f, val->p, prod->p);
633 int isint = 1;
634 for (int i = 0; i < nr; ++i) {
635 value_modulus(prod->p[i], prod->p[i], f->p[i][nparam+1]);
636 isint &= value_zero_p(prod->p[i]);
638 value_set_si(ev->d, 1);
639 value_init(ev->x.n);
640 value_set_si(ev->x.n, isint);
641 Vector_Free(prod);
642 return;
645 Value tmp;
646 value_init(tmp);
647 if (value_one_p(lcm->p[p]))
648 mask_r(f, nr, lcm, p+1, val, ev);
649 else {
650 value_assign(tmp, lcm->p[p]);
651 value_set_si(ev->d, 0);
652 ev->x.p = new_enode(periodic, VALUE_TO_INT(tmp), p+1);
653 do {
654 value_decrement(tmp, tmp);
655 value_assign(val->p[p], tmp);
656 mask_r(f, nr, lcm, p+1, val, &ev->x.p->arr[VALUE_TO_INT(tmp)]);
657 } while (value_pos_p(tmp));
659 value_clear(tmp);
662 static evalue *multi_monom(vec_ZZ& p)
664 evalue *X = new evalue();
665 value_init(X->d);
666 value_init(X->x.n);
667 unsigned nparam = p.length()-1;
668 zz2value(p[nparam], X->x.n);
669 value_set_si(X->d, 1);
670 for (int i = 0; i < nparam; ++i) {
671 if (p[i] == 0)
672 continue;
673 evalue *T = term(i, p[i]);
674 eadd(T, X);
675 free_evalue_refs(T);
676 delete T;
678 return X;
682 * Check whether mapping polyhedron P on the affine combination
683 * num yields a range that has a fixed quotient on integer
684 * division by d
685 * If zero is true, then we are only interested in the quotient
686 * for the cases where the remainder is zero.
687 * Returns NULL if false and a newly allocated value if true.
689 static Value *fixed_quotient(Polyhedron *P, vec_ZZ& num, Value d, bool zero)
691 Value* ret = NULL;
692 int len = num.length();
693 Matrix *T = Matrix_Alloc(2, len);
694 zz2values(num, T->p[0]);
695 value_set_si(T->p[1][len-1], 1);
696 Polyhedron *I = Polyhedron_Image(P, T, P->NbConstraints);
697 Matrix_Free(T);
699 int i;
700 for (i = 0; i < I->NbRays; ++i)
701 if (value_zero_p(I->Ray[i][2])) {
702 Polyhedron_Free(I);
703 return NULL;
706 Value min, max;
707 value_init(min);
708 value_init(max);
709 int bounded = line_minmax(I, &min, &max);
710 assert(bounded);
712 if (zero)
713 mpz_cdiv_q(min, min, d);
714 else
715 mpz_fdiv_q(min, min, d);
716 mpz_fdiv_q(max, max, d);
718 if (value_eq(min, max)) {
719 ALLOC(Value, ret);
720 value_init(*ret);
721 value_assign(*ret, min);
723 value_clear(min);
724 value_clear(max);
725 return ret;
729 * Normalize linear expression coef modulo m
730 * Removes common factor and reduces coefficients
731 * Returns index of first non-zero coefficient or len
733 static int normal_mod(Value *coef, int len, Value *m)
735 Value gcd;
736 value_init(gcd);
738 Vector_Gcd(coef, len, &gcd);
739 Gcd(gcd, *m, &gcd);
740 Vector_AntiScale(coef, coef, gcd, len);
742 value_division(*m, *m, gcd);
743 value_clear(gcd);
745 if (value_one_p(*m))
746 return len;
748 int j;
749 for (j = 0; j < len; ++j)
750 mpz_fdiv_r(coef[j], coef[j], *m);
751 for (j = 0; j < len; ++j)
752 if (value_notzero_p(coef[j]))
753 break;
755 return j;
758 #ifdef USE_MODULO
759 static void mask(Matrix *f, evalue *factor)
761 int nr = f->NbRows, nc = f->NbColumns;
762 int n;
763 bool found = false;
764 for (n = 0; n < nr && value_notzero_p(f->p[n][nc-1]); ++n)
765 if (value_notone_p(f->p[n][nc-1]) &&
766 value_notmone_p(f->p[n][nc-1]))
767 found = true;
768 if (!found)
769 return;
771 evalue EP;
772 nr = n;
774 Value m;
775 value_init(m);
777 evalue EV;
778 value_init(EV.d);
779 value_init(EV.x.n);
780 value_set_si(EV.x.n, 1);
782 for (n = 0; n < nr; ++n) {
783 value_assign(m, f->p[n][nc-1]);
784 if (value_one_p(m) || value_mone_p(m))
785 continue;
787 int j = normal_mod(f->p[n], nc-1, &m);
788 if (j == nc-1) {
789 free_evalue_refs(factor);
790 value_init(factor->d);
791 evalue_set_si(factor, 0, 1);
792 break;
794 vec_ZZ row;
795 values2zz(f->p[n], row, nc-1);
796 ZZ g;
797 value2zz(m, g);
798 if (j < (nc-1)-1 && row[j] > g/2) {
799 for (int k = j; k < (nc-1); ++k)
800 if (row[k] != 0)
801 row[k] = g - row[k];
804 value_init(EP.d);
805 value_set_si(EP.d, 0);
806 EP.x.p = new_enode(relation, 2, 0);
807 value_clear(EP.x.p->arr[1].d);
808 EP.x.p->arr[1] = *factor;
809 evalue *ev = &EP.x.p->arr[0];
810 value_set_si(ev->d, 0);
811 ev->x.p = new_enode(fractional, 3, -1);
812 evalue_set_si(&ev->x.p->arr[1], 0, 1);
813 evalue_set_si(&ev->x.p->arr[2], 1, 1);
814 evalue *E = multi_monom(row);
815 value_assign(EV.d, m);
816 emul(&EV, E);
817 value_clear(ev->x.p->arr[0].d);
818 ev->x.p->arr[0] = *E;
819 delete E;
820 *factor = EP;
823 value_clear(m);
824 free_evalue_refs(&EV);
826 #else
830 static void mask(Matrix *f, evalue *factor)
832 int nr = f->NbRows, nc = f->NbColumns;
833 int n;
834 bool found = false;
835 for (n = 0; n < nr && value_notzero_p(f->p[n][nc-1]); ++n)
836 if (value_notone_p(f->p[n][nc-1]) &&
837 value_notmone_p(f->p[n][nc-1]))
838 found = true;
839 if (!found)
840 return;
842 Value tmp;
843 value_init(tmp);
844 nr = n;
845 unsigned np = nc - 2;
846 Vector *lcm = Vector_Alloc(np);
847 Vector *val = Vector_Alloc(nc);
848 Vector_Set(val->p, 0, nc);
849 value_set_si(val->p[np], 1);
850 Vector_Set(lcm->p, 1, np);
851 for (n = 0; n < nr; ++n) {
852 if (value_one_p(f->p[n][nc-1]) ||
853 value_mone_p(f->p[n][nc-1]))
854 continue;
855 for (int j = 0; j < np; ++j)
856 if (value_notzero_p(f->p[n][j])) {
857 Gcd(f->p[n][j], f->p[n][nc-1], &tmp);
858 value_division(tmp, f->p[n][nc-1], tmp);
859 value_lcm(tmp, lcm->p[j], &lcm->p[j]);
862 evalue EP;
863 value_init(EP.d);
864 mask_r(f, nr, lcm, 0, val, &EP);
865 value_clear(tmp);
866 Vector_Free(val);
867 Vector_Free(lcm);
868 emul(&EP,factor);
869 free_evalue_refs(&EP);
871 #endif
873 struct term_info {
874 evalue *E;
875 ZZ constant;
876 ZZ coeff;
877 int pos;
880 static bool mod_needed(Polyhedron *PD, vec_ZZ& num, Value d, evalue *E)
882 Value *q = fixed_quotient(PD, num, d, false);
884 if (!q)
885 return true;
887 value_oppose(*q, *q);
888 evalue EV;
889 value_init(EV.d);
890 value_set_si(EV.d, 1);
891 value_init(EV.x.n);
892 value_multiply(EV.x.n, *q, d);
893 eadd(&EV, E);
894 free_evalue_refs(&EV);
895 value_clear(*q);
896 free(q);
897 return false;
900 static void ceil_mod(Value *coef, int len, Value d, ZZ& f, evalue *EP, Polyhedron *PD)
902 Value m;
903 value_init(m);
904 value_set_si(m, -1);
906 Vector_Scale(coef, coef, m, len);
908 value_assign(m, d);
909 int j = normal_mod(coef, len, &m);
911 if (j == len) {
912 value_clear(m);
913 return;
916 vec_ZZ num;
917 values2zz(coef, num, len);
919 ZZ g;
920 value2zz(m, g);
922 evalue tmp;
923 value_init(tmp.d);
924 evalue_set_si(&tmp, 0, 1);
926 int p = j;
927 if (g % 2 == 0)
928 while (j < len-1 && (num[j] == g/2 || num[j] == 0))
929 ++j;
930 if ((j < len-1 && num[j] > g/2) || (j == len-1 && num[j] >= (g+1)/2)) {
931 for (int k = j; k < len-1; ++k)
932 if (num[k] != 0)
933 num[k] = g - num[k];
934 num[len-1] = g - 1 - num[len-1];
935 value_assign(tmp.d, m);
936 ZZ t = f*(g-1);
937 zz2value(t, tmp.x.n);
938 eadd(&tmp, EP);
939 f = -f;
942 if (p >= len-1) {
943 ZZ t = num[len-1] * f;
944 zz2value(t, tmp.x.n);
945 value_assign(tmp.d, m);
946 eadd(&tmp, EP);
947 } else {
948 evalue *E = multi_monom(num);
949 evalue EV;
950 value_init(EV.d);
952 if (PD && !mod_needed(PD, num, m, E)) {
953 value_init(EV.x.n);
954 zz2value(f, EV.x.n);
955 value_assign(EV.d, m);
956 emul(&EV, E);
957 eadd(E, EP);
958 } else {
959 value_init(EV.x.n);
960 value_set_si(EV.x.n, 1);
961 value_assign(EV.d, m);
962 emul(&EV, E);
963 value_clear(EV.x.n);
964 value_set_si(EV.d, 0);
965 EV.x.p = new_enode(fractional, 3, -1);
966 evalue_copy(&EV.x.p->arr[0], E);
967 evalue_set_si(&EV.x.p->arr[1], 0, 1);
968 value_init(EV.x.p->arr[2].x.n);
969 zz2value(f, EV.x.p->arr[2].x.n);
970 value_set_si(EV.x.p->arr[2].d, 1);
972 eadd(&EV, EP);
975 free_evalue_refs(&EV);
976 free_evalue_refs(E);
977 delete E;
980 free_evalue_refs(&tmp);
982 out:
983 value_clear(m);
986 evalue* bv_ceil3(Value *coef, int len, Value d, Polyhedron *P)
988 Vector *val = Vector_Alloc(len);
990 Value t;
991 value_init(t);
992 value_set_si(t, -1);
993 Vector_Scale(coef, val->p, t, len);
994 value_absolute(t, d);
996 vec_ZZ num;
997 values2zz(val->p, num, len);
998 evalue *EP = multi_monom(num);
1000 evalue tmp;
1001 value_init(tmp.d);
1002 value_init(tmp.x.n);
1003 value_set_si(tmp.x.n, 1);
1004 value_assign(tmp.d, t);
1006 emul(&tmp, EP);
1008 ZZ one;
1009 one = 1;
1010 ceil_mod(val->p, len, t, one, EP, P);
1011 value_clear(t);
1013 /* copy EP to malloc'ed evalue */
1014 evalue *E;
1015 ALLOC(evalue, E);
1016 *E = *EP;
1017 delete EP;
1019 free_evalue_refs(&tmp);
1020 Vector_Free(val);
1022 return E;
1025 #ifdef USE_MODULO
1026 evalue* lattice_point(
1027 Polyhedron *i, vec_ZZ& lambda, Matrix *W, Value lcm, Polyhedron *PD)
1029 unsigned nparam = W->NbColumns - 1;
1031 Matrix* Rays = rays2(i);
1032 Matrix *T = Transpose(Rays);
1033 Matrix *T2 = Matrix_Copy(T);
1034 Matrix *inv = Matrix_Alloc(T2->NbRows, T2->NbColumns);
1035 int ok = Matrix_Inverse(T2, inv);
1036 assert(ok);
1037 Matrix_Free(Rays);
1038 Matrix_Free(T2);
1039 mat_ZZ vertex;
1040 matrix2zz(W, vertex, W->NbRows, W->NbColumns);
1042 vec_ZZ num;
1043 num = lambda * vertex;
1045 evalue *EP = multi_monom(num);
1047 evalue tmp;
1048 value_init(tmp.d);
1049 value_init(tmp.x.n);
1050 value_set_si(tmp.x.n, 1);
1051 value_assign(tmp.d, lcm);
1053 emul(&tmp, EP);
1055 Matrix *L = Matrix_Alloc(inv->NbRows, W->NbColumns);
1056 Matrix_Product(inv, W, L);
1058 mat_ZZ RT;
1059 matrix2zz(T, RT, T->NbRows, T->NbColumns);
1060 Matrix_Free(T);
1062 vec_ZZ p = lambda * RT;
1064 for (int i = 0; i < L->NbRows; ++i) {
1065 ceil_mod(L->p[i], nparam+1, lcm, p[i], EP, PD);
1068 Matrix_Free(L);
1070 Matrix_Free(inv);
1071 free_evalue_refs(&tmp);
1072 return EP;
1074 #else
1075 evalue* lattice_point(
1076 Polyhedron *i, vec_ZZ& lambda, Matrix *W, Value lcm, Polyhedron *PD)
1078 Matrix *T = Transpose(W);
1079 unsigned nparam = T->NbRows - 1;
1081 evalue *EP = new evalue();
1082 value_init(EP->d);
1083 evalue_set_si(EP, 0, 1);
1085 evalue ev;
1086 Vector *val = Vector_Alloc(nparam+1);
1087 value_set_si(val->p[nparam], 1);
1088 ZZ offset(INIT_VAL, 0);
1089 value_init(ev.d);
1090 vertex_period(i, lambda, T, lcm, 0, val, EP, &ev, offset);
1091 Vector_Free(val);
1092 eadd(&ev, EP);
1093 free_evalue_refs(&ev);
1095 Matrix_Free(T);
1097 reduce_evalue(EP);
1099 return EP;
1101 #endif
1103 void lattice_point(
1104 Param_Vertices* V, Polyhedron *i, vec_ZZ& lambda, term_info* term,
1105 Polyhedron *PD)
1107 unsigned nparam = V->Vertex->NbColumns - 2;
1108 unsigned dim = i->Dimension;
1109 mat_ZZ vertex;
1110 vertex.SetDims(V->Vertex->NbRows, nparam+1);
1111 Value lcm, tmp;
1112 value_init(lcm);
1113 value_init(tmp);
1114 value_set_si(lcm, 1);
1115 for (int j = 0; j < V->Vertex->NbRows; ++j) {
1116 value_lcm(lcm, V->Vertex->p[j][nparam+1], &lcm);
1118 if (value_notone_p(lcm)) {
1119 Matrix * mv = Matrix_Alloc(dim, nparam+1);
1120 for (int j = 0 ; j < dim; ++j) {
1121 value_division(tmp, lcm, V->Vertex->p[j][nparam+1]);
1122 Vector_Scale(V->Vertex->p[j], mv->p[j], tmp, nparam+1);
1125 term->E = lattice_point(i, lambda, mv, lcm, PD);
1126 term->constant = 0;
1128 Matrix_Free(mv);
1129 value_clear(lcm);
1130 value_clear(tmp);
1131 return;
1133 for (int i = 0; i < V->Vertex->NbRows; ++i) {
1134 assert(value_one_p(V->Vertex->p[i][nparam+1])); // for now
1135 values2zz(V->Vertex->p[i], vertex[i], nparam+1);
1138 vec_ZZ num;
1139 num = lambda * vertex;
1141 int p = -1;
1142 int nn = 0;
1143 for (int j = 0; j < nparam; ++j)
1144 if (num[j] != 0) {
1145 ++nn;
1146 p = j;
1148 if (nn >= 2) {
1149 term->E = multi_monom(num);
1150 term->constant = 0;
1151 } else {
1152 term->E = NULL;
1153 term->constant = num[nparam];
1154 term->pos = p;
1155 if (p != -1)
1156 term->coeff = num[p];
1159 value_clear(lcm);
1160 value_clear(tmp);
1163 void normalize(Polyhedron *i, vec_ZZ& lambda, ZZ& sign, ZZ& num, vec_ZZ& den)
1165 unsigned dim = i->Dimension;
1167 int r = 0;
1168 mat_ZZ rays;
1169 rays.SetDims(dim, dim);
1170 add_rays(rays, i, &r);
1171 den = rays * lambda;
1172 int change = 0;
1174 for (int j = 0; j < den.length(); ++j) {
1175 if (den[j] > 0)
1176 change ^= 1;
1177 else {
1178 den[j] = abs(den[j]);
1179 num += den[j];
1182 if (change)
1183 sign = -sign;
1186 typedef Polyhedron * Polyhedron_p;
1188 void barvinok_count(Polyhedron *P, Value* result, unsigned NbMaxCons)
1190 Polyhedron ** vcone;
1191 vec_ZZ sign;
1192 int ncone = 0;
1193 sign.SetLength(ncone);
1194 unsigned dim;
1195 int allocated = 0;
1196 Value factor;
1197 Polyhedron *Q;
1198 int r = 0;
1200 if (emptyQ(P)) {
1201 value_set_si(*result, 0);
1202 return;
1204 if (P->NbBid == 0)
1205 for (; r < P->NbRays; ++r)
1206 if (value_zero_p(P->Ray[r][P->Dimension+1]))
1207 break;
1208 if (P->NbBid !=0 || r < P->NbRays) {
1209 value_set_si(*result, -1);
1210 return;
1212 if (P->NbEq != 0) {
1213 P = remove_equalities(P);
1214 if (emptyQ(P)) {
1215 Polyhedron_Free(P);
1216 value_set_si(*result, 0);
1217 return;
1219 allocated = 1;
1221 value_init(factor);
1222 value_set_si(factor, 1);
1223 Q = Polyhedron_Reduce(P, &factor);
1224 if (Q) {
1225 if (allocated)
1226 Polyhedron_Free(P);
1227 P = Q;
1228 allocated = 1;
1230 if (P->Dimension == 0) {
1231 value_assign(*result, factor);
1232 if (allocated)
1233 Polyhedron_Free(P);
1234 value_clear(factor);
1235 return;
1238 dim = P->Dimension;
1239 vcone = new Polyhedron_p[P->NbRays];
1241 for (int j = 0; j < P->NbRays; ++j) {
1242 int npos, nneg;
1243 Polyhedron *C = supporting_cone(P, j);
1244 decompose(C, &vcone[j], &npos, &nneg, NbMaxCons);
1245 ncone += npos + nneg;
1246 sign.SetLength(ncone);
1247 for (int k = 0; k < npos; ++k)
1248 sign[ncone-nneg-k-1] = 1;
1249 for (int k = 0; k < nneg; ++k)
1250 sign[ncone-k-1] = -1;
1253 mat_ZZ rays;
1254 rays.SetDims(ncone * dim, dim);
1255 r = 0;
1256 for (int j = 0; j < P->NbRays; ++j) {
1257 for (Polyhedron *i = vcone[j]; i; i = i->next) {
1258 assert(i->NbRays-1 == dim);
1259 add_rays(rays, i, &r);
1262 vec_ZZ lambda;
1263 nonorthog(rays, lambda);
1265 ZZ num;
1266 vec_ZZ den;
1267 den.SetLength(dim);
1269 int f = 0;
1270 vec_ZZ vertex;
1271 mpq_t count;
1272 mpq_init(count);
1273 for (int j = 0; j < P->NbRays; ++j) {
1274 for (Polyhedron *i = vcone[j]; i; i = i->next) {
1275 lattice_point(P->Ray[j]+1, i, vertex);
1276 num = vertex * lambda;
1277 normalize(i, lambda, sign[f], num, den);
1279 dpoly d(dim, num);
1280 dpoly n(dim, den[0], 1);
1281 for (int k = 1; k < dim; ++k) {
1282 dpoly fact(dim, den[k], 1);
1283 n *= fact;
1285 d.div(n, count, sign[f]);
1287 ++f;
1289 Domain_Free(vcone[j]);
1292 assert(value_one_p(&count[0]._mp_den));
1293 value_multiply(*result, &count[0]._mp_num, factor);
1294 mpq_clear(count);
1296 delete [] vcone;
1298 if (allocated)
1299 Polyhedron_Free(P);
1300 value_clear(factor);
1303 static void uni_polynom(int param, Vector *c, evalue *EP)
1305 unsigned dim = c->Size-2;
1306 value_init(EP->d);
1307 value_set_si(EP->d,0);
1308 EP->x.p = new_enode(polynomial, dim+1, param+1);
1309 for (int j = 0; j <= dim; ++j)
1310 evalue_set(&EP->x.p->arr[j], c->p[j], c->p[dim+1]);
1313 static void multi_polynom(Vector *c, evalue* X, evalue *EP)
1315 unsigned dim = c->Size-2;
1316 evalue EC;
1318 value_init(EC.d);
1319 evalue_set(&EC, c->p[dim], c->p[dim+1]);
1321 value_init(EP->d);
1322 evalue_set(EP, c->p[dim], c->p[dim+1]);
1324 for (int i = dim-1; i >= 0; --i) {
1325 emul(X, EP);
1326 value_assign(EC.x.n, c->p[i]);
1327 eadd(&EC, EP);
1329 free_evalue_refs(&EC);
1332 Polyhedron *unfringe (Polyhedron *P, unsigned MaxRays)
1334 int len = P->Dimension+2;
1335 Polyhedron *T, *R = P;
1336 Value g;
1337 value_init(g);
1338 Vector *row = Vector_Alloc(len);
1339 value_set_si(row->p[0], 1);
1341 R = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
1343 Matrix *M = Matrix_Alloc(2, len-1);
1344 value_set_si(M->p[1][len-2], 1);
1345 for (int v = 0; v < P->Dimension; ++v) {
1346 value_set_si(M->p[0][v], 1);
1347 Polyhedron *I = Polyhedron_Image(P, M, 2+1);
1348 value_set_si(M->p[0][v], 0);
1349 for (int r = 0; r < I->NbConstraints; ++r) {
1350 if (value_zero_p(I->Constraint[r][0]))
1351 continue;
1352 if (value_zero_p(I->Constraint[r][1]))
1353 continue;
1354 if (value_one_p(I->Constraint[r][1]))
1355 continue;
1356 if (value_mone_p(I->Constraint[r][1]))
1357 continue;
1358 value_absolute(g, I->Constraint[r][1]);
1359 Vector_Set(row->p+1, 0, len-2);
1360 value_division(row->p[1+v], I->Constraint[r][1], g);
1361 mpz_fdiv_q(row->p[len-1], I->Constraint[r][2], g);
1362 T = R;
1363 R = AddConstraints(row->p, 1, R, MaxRays);
1364 if (T != P)
1365 Polyhedron_Free(T);
1367 Polyhedron_Free(I);
1369 Matrix_Free(M);
1370 Vector_Free(row);
1371 value_clear(g);
1372 return R;
1375 static Polyhedron *reduce_domain(Polyhedron *D, Matrix *CT, Polyhedron *CEq,
1376 Polyhedron **fVD, int nd, unsigned MaxRays)
1378 assert(CEq);
1380 Polyhedron *Dt;
1381 Dt = CT ? DomainPreimage(D, CT, MaxRays) : D;
1382 Polyhedron *rVD = DomainIntersection(Dt, CEq, MaxRays);
1384 /* if rVD is empty or too small in geometric dimension */
1385 if(!rVD || emptyQ(rVD) ||
1386 (rVD->Dimension-rVD->NbEq < Dt->Dimension-Dt->NbEq-CEq->NbEq)) {
1387 if(rVD)
1388 Domain_Free(rVD);
1389 if (CT)
1390 Domain_Free(Dt);
1391 return 0; /* empty validity domain */
1394 if (CT)
1395 Domain_Free(Dt);
1397 fVD[nd] = Domain_Copy(rVD);
1398 for (int i = 0 ; i < nd; ++i) {
1399 Polyhedron *I = DomainIntersection(fVD[nd], fVD[i], MaxRays);
1400 if (emptyQ(I)) {
1401 Domain_Free(I);
1402 continue;
1404 Polyhedron *F = DomainSimplify(I, fVD[nd], MaxRays);
1405 if (F->NbEq == 1) {
1406 Polyhedron *T = rVD;
1407 rVD = DomainDifference(rVD, F, MaxRays);
1408 Domain_Free(T);
1410 Domain_Free(F);
1411 Domain_Free(I);
1414 rVD = DomainConstraintSimplify(rVD, MaxRays);
1415 if (emptyQ(rVD)) {
1416 Domain_Free(fVD[nd]);
1417 Domain_Free(rVD);
1418 return 0;
1421 Value c;
1422 value_init(c);
1423 barvinok_count(rVD, &c, MaxRays);
1424 if (value_zero_p(c)) {
1425 Domain_Free(rVD);
1426 rVD = 0;
1428 value_clear(c);
1430 return rVD;
1433 static bool Polyhedron_is_infinite(Polyhedron *P, unsigned nparam)
1435 int r;
1436 for (r = 0; r < P->NbRays; ++r)
1437 if (value_zero_p(P->Ray[r][0]) ||
1438 value_zero_p(P->Ray[r][P->Dimension+1])) {
1439 int i;
1440 for (i = P->Dimension - nparam; i < P->Dimension; ++i)
1441 if (value_notzero_p(P->Ray[r][i+1]))
1442 break;
1443 if (i >= P->Dimension)
1444 break;
1446 return r < P->NbRays;
1449 evalue* barvinok_enumerate_ev(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1451 //P = unfringe(P, MaxRays);
1452 Polyhedron *CEq = NULL, *rVD, *pVD, *CA;
1453 Matrix *CT = NULL;
1454 Param_Polyhedron *PP = NULL;
1455 Param_Domain *D, *next;
1456 Param_Vertices *V;
1457 int r = 0;
1458 unsigned nparam = C->Dimension;
1459 evalue *eres;
1460 ALLOC(evalue, eres);
1461 value_init(eres->d);
1462 value_set_si(eres->d, 0);
1464 evalue factor;
1465 value_init(factor.d);
1466 evalue_set_si(&factor, 1, 1);
1468 CA = align_context(C, P->Dimension, MaxRays);
1469 P = DomainIntersection(P, CA, MaxRays);
1470 Polyhedron_Free(CA);
1472 if (C->Dimension == 0 || emptyQ(P)) {
1473 constant:
1474 eres->x.p = new_enode(partition, 2, C->Dimension);
1475 EVALUE_SET_DOMAIN(eres->x.p->arr[0],
1476 DomainConstraintSimplify(CEq ? CEq : Polyhedron_Copy(C), MaxRays));
1477 value_set_si(eres->x.p->arr[1].d, 1);
1478 value_init(eres->x.p->arr[1].x.n);
1479 if (emptyQ(P))
1480 value_set_si(eres->x.p->arr[1].x.n, 0);
1481 else
1482 barvinok_count(P, &eres->x.p->arr[1].x.n, MaxRays);
1483 out:
1484 emul(&factor, eres);
1485 reduce_evalue(eres);
1486 free_evalue_refs(&factor);
1487 Polyhedron_Free(P);
1488 if (CT)
1489 Matrix_Free(CT);
1490 if (PP)
1491 Param_Polyhedron_Free(PP);
1493 return eres;
1495 if (Polyhedron_is_infinite(P, nparam))
1496 goto constant;
1498 if (P->NbEq != 0) {
1499 Matrix *f;
1500 P = remove_equalities_p(P, P->Dimension-nparam, &f);
1501 mask(f, &factor);
1502 Matrix_Free(f);
1504 if (P->Dimension == nparam) {
1505 CEq = P;
1506 P = Universe_Polyhedron(0);
1507 goto constant;
1510 Polyhedron *Q = ParamPolyhedron_Reduce(P, P->Dimension-nparam, &factor);
1511 if (Q) {
1512 Polyhedron_Free(P);
1513 if (Q->Dimension == nparam) {
1514 CEq = Q;
1515 P = Universe_Polyhedron(0);
1516 goto constant;
1518 P = Q;
1520 Polyhedron *oldP = P;
1521 PP = Polyhedron2Param_SimplifiedDomain(&P,C,MaxRays,&CEq,&CT);
1522 if (P != oldP)
1523 Polyhedron_Free(oldP);
1525 if (isIdentity(CT)) {
1526 Matrix_Free(CT);
1527 CT = NULL;
1528 } else {
1529 assert(CT->NbRows != CT->NbColumns);
1530 if (CT->NbRows == 1) // no more parameters
1531 goto constant;
1532 nparam = CT->NbRows - 1;
1535 unsigned dim = P->Dimension - nparam;
1536 Polyhedron ** vcone = new Polyhedron_p[PP->nbV];
1537 int * npos = new int[PP->nbV];
1538 int * nneg = new int[PP->nbV];
1539 ZZ sign;
1541 int i;
1542 for (i = 0, V = PP->V; V; ++i, V = V->next) {
1543 Polyhedron *C = supporting_cone_p(P, V);
1544 decompose(C, &vcone[i], &npos[i], &nneg[i], MaxRays);
1547 Vector *c = Vector_Alloc(dim+2);
1549 int nd;
1550 for (nd = 0, D=PP->D; D; ++nd, D=D->next);
1551 struct section { Polyhedron *D; evalue E; };
1552 section *s = new section[nd];
1553 Polyhedron **fVD = new Polyhedron_p[nd];
1555 for(nd = 0, D=PP->D; D; D=next) {
1556 next = D->next;
1558 Polyhedron *rVD = reduce_domain(D->Domain, CT, CEq,
1559 fVD, nd, MaxRays);
1560 if (!rVD)
1561 continue;
1563 pVD = CT ? DomainImage(rVD,CT,MaxRays) : rVD;
1565 int ncone = 0;
1566 FORALL_PVertex_in_ParamPolyhedron(V,D,PP) // _i is internal counter
1567 ncone += npos[_i] + nneg[_i];
1568 END_FORALL_PVertex_in_ParamPolyhedron;
1570 mat_ZZ rays;
1571 rays.SetDims(ncone * dim, dim);
1572 r = 0;
1573 FORALL_PVertex_in_ParamPolyhedron(V,D,PP) // _i is internal counter
1574 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1575 assert(i->NbRays-1 == dim);
1576 add_rays(rays, i, &r);
1578 END_FORALL_PVertex_in_ParamPolyhedron;
1579 vec_ZZ lambda;
1580 nonorthog(rays, lambda);
1582 vec_ZZ den;
1583 den.SetLength(dim);
1584 term_info num;
1586 value_init(s[nd].E.d);
1587 evalue_set_si(&s[nd].E, 0, 1);
1588 mpq_t count;
1589 mpq_init(count);
1590 FORALL_PVertex_in_ParamPolyhedron(V,D,PP)
1591 int f = 0;
1592 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1593 sign = f < npos[_i] ? 1 : -1;
1594 lattice_point(V, i, lambda, &num, pVD);
1595 normalize(i, lambda, sign, num.constant, den);
1597 dpoly n(dim, den[0], 1);
1598 for (int k = 1; k < dim; ++k) {
1599 dpoly fact(dim, den[k], 1);
1600 n *= fact;
1602 if (num.E != NULL) {
1603 ZZ one(INIT_VAL, 1);
1604 dpoly_n d(dim, num.constant, one);
1605 d.div(n, c, sign);
1606 evalue EV;
1607 multi_polynom(c, num.E, &EV);
1608 eadd(&EV , &s[nd].E);
1609 free_evalue_refs(&EV);
1610 free_evalue_refs(num.E);
1611 delete num.E;
1612 } else if (num.pos != -1) {
1613 dpoly_n d(dim, num.constant, num.coeff);
1614 d.div(n, c, sign);
1615 evalue EV;
1616 uni_polynom(num.pos, c, &EV);
1617 eadd(&EV , &s[nd].E);
1618 free_evalue_refs(&EV);
1619 } else {
1620 mpq_set_si(count, 0, 1);
1621 dpoly d(dim, num.constant);
1622 d.div(n, count, sign);
1623 evalue EV;
1624 value_init(EV.d);
1625 evalue_set(&EV, &count[0]._mp_num, &count[0]._mp_den);
1626 eadd(&EV , &s[nd].E);
1627 free_evalue_refs(&EV);
1629 ++f;
1631 END_FORALL_PVertex_in_ParamPolyhedron;
1633 mpq_clear(count);
1635 if (CT)
1636 addeliminatedparams_evalue(&s[nd].E, CT);
1637 s[nd].D = rVD;
1638 ++nd;
1639 if (rVD != pVD)
1640 Domain_Free(pVD);
1643 if (nd == 0)
1644 evalue_set_si(eres, 0, 1);
1645 else {
1646 eres->x.p = new_enode(partition, 2*nd, C->Dimension);
1647 for (int j = 0; j < nd; ++j) {
1648 EVALUE_SET_DOMAIN(eres->x.p->arr[2*j], s[j].D);
1649 value_clear(eres->x.p->arr[2*j+1].d);
1650 eres->x.p->arr[2*j+1] = s[j].E;
1651 Domain_Free(fVD[j]);
1654 delete [] s;
1655 delete [] fVD;
1657 Vector_Free(c);
1659 for (int j = 0; j < PP->nbV; ++j)
1660 Domain_Free(vcone[j]);
1661 delete [] vcone;
1662 delete [] npos;
1663 delete [] nneg;
1665 if (CEq)
1666 Polyhedron_Free(CEq);
1668 goto out;
1671 Enumeration* barvinok_enumerate(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1673 evalue *EP = barvinok_enumerate_ev(P, C, MaxRays);
1675 return partition2enumeration(EP);
1678 static void SwapColumns(Value **V, int n, int i, int j)
1680 for (int r = 0; r < n; ++r)
1681 value_swap(V[r][i], V[r][j]);
1684 static void SwapColumns(Polyhedron *P, int i, int j)
1686 SwapColumns(P->Constraint, P->NbConstraints, i, j);
1687 SwapColumns(P->Ray, P->NbRays, i, j);
1690 static void negative_test_constraint(Value *l, Value *u, Value *c, int pos,
1691 int len, Value *v)
1693 value_oppose(*v, u[pos+1]);
1694 Vector_Combine(l+1, u+1, c+1, *v, l[pos+1], len-1);
1695 value_multiply(*v, *v, l[pos+1]);
1696 value_substract(c[len-1], c[len-1], *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]);
1700 ConstraintSimplify(c, c, len, v);
1703 static void oppose_constraint(Value *c, int len, Value *v)
1705 value_set_si(*v, -1);
1706 Vector_Scale(c+1, c+1, *v, len-1);
1707 value_decrement(c[len-1], c[len-1]);
1710 static bool SplitOnConstraint(Polyhedron *P, int i, int l, int u,
1711 int nvar, int len, int exist, int MaxRays,
1712 Vector *row, Value& f, bool independent,
1713 Polyhedron **pos, Polyhedron **neg)
1715 negative_test_constraint(P->Constraint[l], P->Constraint[u],
1716 row->p, nvar+i, len, &f);
1717 *neg = AddConstraints(row->p, 1, P, MaxRays);
1719 /* We found an independent, but useless constraint
1720 * Maybe we should detect this earlier and not
1721 * mark the variable as INDEPENDENT
1723 if (emptyQ((*neg))) {
1724 Polyhedron_Free(*neg);
1725 return false;
1728 oppose_constraint(row->p, len, &f);
1729 *pos = AddConstraints(row->p, 1, P, MaxRays);
1731 if (emptyQ((*pos))) {
1732 Polyhedron_Free(*neg);
1733 Polyhedron_Free(*pos);
1734 return false;
1737 return true;
1741 * unimodularly transform P such that constraint r is transformed
1742 * into a constraint that involves only a single (the first)
1743 * existential variable
1746 static Polyhedron *rotate_along(Polyhedron *P, int r, int nvar, int exist,
1747 unsigned MaxRays)
1749 Value g;
1750 value_init(g);
1752 Vector *row = Vector_Alloc(exist);
1753 Vector_Copy(P->Constraint[r]+1+nvar, row->p, exist);
1754 Vector_Gcd(row->p, exist, &g);
1755 if (value_notone_p(g))
1756 Vector_AntiScale(row->p, row->p, g, exist);
1757 value_clear(g);
1759 Matrix *M = unimodular_complete(row);
1760 Matrix *M2 = Matrix_Alloc(P->Dimension+1, P->Dimension+1);
1761 for (r = 0; r < nvar; ++r)
1762 value_set_si(M2->p[r][r], 1);
1763 for ( ; r < nvar+exist; ++r)
1764 Vector_Copy(M->p[r-nvar], M2->p[r]+nvar, exist);
1765 for ( ; r < P->Dimension+1; ++r)
1766 value_set_si(M2->p[r][r], 1);
1767 Polyhedron *T = Polyhedron_Image(P, M2, MaxRays);
1769 Matrix_Free(M2);
1770 Matrix_Free(M);
1771 Vector_Free(row);
1773 return T;
1776 static bool SplitOnVar(Polyhedron *P, int i,
1777 int nvar, int len, int exist, int MaxRays,
1778 Vector *row, Value& f, bool independent,
1779 Polyhedron **pos, Polyhedron **neg)
1781 int j;
1783 for (int l = P->NbEq; l < P->NbConstraints; ++l) {
1784 if (value_negz_p(P->Constraint[l][nvar+i+1]))
1785 continue;
1787 if (independent) {
1788 for (j = 0; j < exist; ++j)
1789 if (j != i && value_notzero_p(P->Constraint[l][nvar+j+1]))
1790 break;
1791 if (j < exist)
1792 continue;
1795 for (int u = P->NbEq; u < P->NbConstraints; ++u) {
1796 if (value_posz_p(P->Constraint[u][nvar+i+1]))
1797 continue;
1799 if (independent) {
1800 for (j = 0; j < exist; ++j)
1801 if (j != i && value_notzero_p(P->Constraint[u][nvar+j+1]))
1802 break;
1803 if (j < exist)
1804 continue;
1807 if (SplitOnConstraint(P, i, l, u,
1808 nvar, len, exist, MaxRays,
1809 row, f, independent,
1810 pos, neg)) {
1811 if (independent) {
1812 if (i != 0)
1813 SwapColumns(*neg, nvar+1, nvar+1+i);
1815 return true;
1820 return false;
1823 static bool double_bound_pair(Polyhedron *P, int nvar, int exist,
1824 int i, int l1, int l2,
1825 Polyhedron **pos, Polyhedron **neg)
1827 Value f;
1828 value_init(f);
1829 Vector *row = Vector_Alloc(P->Dimension+2);
1830 value_set_si(row->p[0], 1);
1831 value_oppose(f, P->Constraint[l1][nvar+i+1]);
1832 Vector_Combine(P->Constraint[l1]+1, P->Constraint[l2]+1,
1833 row->p+1,
1834 P->Constraint[l2][nvar+i+1], f,
1835 P->Dimension+1);
1836 ConstraintSimplify(row->p, row->p, P->Dimension+2, &f);
1837 *pos = AddConstraints(row->p, 1, P, 0);
1838 value_set_si(f, -1);
1839 Vector_Scale(row->p+1, row->p+1, f, P->Dimension+1);
1840 value_decrement(row->p[P->Dimension+1], row->p[P->Dimension+1]);
1841 *neg = AddConstraints(row->p, 1, P, 0);
1842 Vector_Free(row);
1843 value_clear(f);
1845 return !emptyQ((*pos)) && !emptyQ((*neg));
1848 static bool double_bound(Polyhedron *P, int nvar, int exist,
1849 Polyhedron **pos, Polyhedron **neg)
1851 for (int i = 0; i < exist; ++i) {
1852 int l1, l2;
1853 for (l1 = P->NbEq; l1 < P->NbConstraints; ++l1) {
1854 if (value_negz_p(P->Constraint[l1][nvar+i+1]))
1855 continue;
1856 for (l2 = l1 + 1; l2 < P->NbConstraints; ++l2) {
1857 if (value_negz_p(P->Constraint[l2][nvar+i+1]))
1858 continue;
1859 if (double_bound_pair(P, nvar, exist, i, l1, l2, pos, neg))
1860 return true;
1863 for (l1 = P->NbEq; l1 < P->NbConstraints; ++l1) {
1864 if (value_posz_p(P->Constraint[l1][nvar+i+1]))
1865 continue;
1866 if (l1 < P->NbConstraints)
1867 for (l2 = l1 + 1; l2 < P->NbConstraints; ++l2) {
1868 if (value_posz_p(P->Constraint[l2][nvar+i+1]))
1869 continue;
1870 if (double_bound_pair(P, nvar, exist, i, l1, l2, pos, neg))
1871 return true;
1874 return false;
1876 return false;
1879 enum constraint {
1880 ALL_POS = 1 << 0,
1881 ONE_NEG = 1 << 1,
1882 INDEPENDENT = 1 << 2
1885 static evalue* enumerate_or(Polyhedron *D,
1886 unsigned exist, unsigned nparam, unsigned MaxRays)
1888 #ifdef DEBUG_ER
1889 fprintf(stderr, "\nER: Or\n");
1890 #endif /* DEBUG_ER */
1892 Polyhedron *N = D->next;
1893 D->next = 0;
1894 evalue *EP =
1895 barvinok_enumerate_e(D, exist, nparam, MaxRays);
1896 Polyhedron_Free(D);
1898 for (D = N; D; D = N) {
1899 N = D->next;
1900 D->next = 0;
1902 evalue *EN =
1903 barvinok_enumerate_e(D, exist, nparam, MaxRays);
1905 eor(EN, EP);
1906 free_evalue_refs(EN);
1907 free(EN);
1908 Polyhedron_Free(D);
1911 reduce_evalue(EP);
1913 return EP;
1916 static evalue* enumerate_sum(Polyhedron *P,
1917 unsigned exist, unsigned nparam, unsigned MaxRays)
1919 int nvar = P->Dimension - exist - nparam;
1920 int toswap = nvar < exist ? nvar : exist;
1921 for (int i = 0; i < toswap; ++i)
1922 SwapColumns(P, 1 + i, nvar+exist - i);
1923 nparam += nvar;
1925 #ifdef DEBUG_ER
1926 fprintf(stderr, "\nER: Sum\n");
1927 #endif /* DEBUG_ER */
1929 evalue *EP = barvinok_enumerate_e(P, exist, nparam, MaxRays);
1931 for (int i = 0; i < /* nvar */ nparam; ++i) {
1932 Matrix *C = Matrix_Alloc(1, 1 + nparam + 1);
1933 value_set_si(C->p[0][0], 1);
1934 evalue split;
1935 value_init(split.d);
1936 value_set_si(split.d, 0);
1937 split.x.p = new_enode(partition, 4, nparam);
1938 value_set_si(C->p[0][1+i], 1);
1939 Matrix *C2 = Matrix_Copy(C);
1940 EVALUE_SET_DOMAIN(split.x.p->arr[0],
1941 Constraints2Polyhedron(C2, MaxRays));
1942 Matrix_Free(C2);
1943 evalue_set_si(&split.x.p->arr[1], 1, 1);
1944 value_set_si(C->p[0][1+i], -1);
1945 value_set_si(C->p[0][1+nparam], -1);
1946 EVALUE_SET_DOMAIN(split.x.p->arr[2],
1947 Constraints2Polyhedron(C, MaxRays));
1948 evalue_set_si(&split.x.p->arr[3], 1, 1);
1949 emul(&split, EP);
1950 free_evalue_refs(&split);
1951 Matrix_Free(C);
1953 reduce_evalue(EP);
1954 evalue_range_reduction(EP);
1956 evalue_frac2floor(EP);
1958 evalue *sum = esum(EP, nvar);
1960 free_evalue_refs(EP);
1961 free(EP);
1962 EP = sum;
1964 evalue_range_reduction(EP);
1966 return EP;
1969 static evalue* split_sure(Polyhedron *P, Polyhedron *S,
1970 unsigned exist, unsigned nparam, unsigned MaxRays)
1972 int nvar = P->Dimension - exist - nparam;
1974 Matrix *M = Matrix_Alloc(exist, S->Dimension+2);
1975 for (int i = 0; i < exist; ++i)
1976 value_set_si(M->p[i][nvar+i+1], 1);
1977 Polyhedron *O = S;
1978 S = DomainAddRays(S, M, MaxRays);
1979 Polyhedron_Free(O);
1980 Polyhedron *F = DomainAddRays(P, M, MaxRays);
1981 Polyhedron *D = DomainDifference(F, S, MaxRays);
1982 O = D;
1983 D = Disjoint_Domain(D, 0, MaxRays);
1984 Polyhedron_Free(F);
1985 Domain_Free(O);
1986 Matrix_Free(M);
1988 M = Matrix_Alloc(P->Dimension+1-exist, P->Dimension+1);
1989 for (int j = 0; j < nvar; ++j)
1990 value_set_si(M->p[j][j], 1);
1991 for (int j = 0; j < nparam+1; ++j)
1992 value_set_si(M->p[nvar+j][nvar+exist+j], 1);
1993 Polyhedron *T = Polyhedron_Image(S, M, MaxRays);
1994 evalue *EP = barvinok_enumerate_e(T, 0, nparam, MaxRays);
1995 Polyhedron_Free(S);
1996 Polyhedron_Free(T);
1997 Matrix_Free(M);
1999 for (Polyhedron *Q = D; Q; Q = Q->next) {
2000 Polyhedron *N = Q->next;
2001 Q->next = 0;
2002 T = DomainIntersection(P, Q, MaxRays);
2003 evalue *E = barvinok_enumerate_e(T, exist, nparam, MaxRays);
2004 eadd(E, EP);
2005 free_evalue_refs(E);
2006 free(E);
2007 Polyhedron_Free(T);
2008 Q->next = N;
2010 Domain_Free(D);
2011 return EP;
2014 static evalue* enumerate_sure(Polyhedron *P,
2015 unsigned exist, unsigned nparam, unsigned MaxRays)
2017 int i;
2018 Polyhedron *S = P;
2019 int nvar = P->Dimension - exist - nparam;
2020 Value lcm;
2021 Value f;
2022 value_init(lcm);
2023 value_init(f);
2025 for (i = 0; i < exist; ++i) {
2026 Matrix *M = Matrix_Alloc(S->NbConstraints, S->Dimension+2);
2027 int c = 0;
2028 value_set_si(lcm, 1);
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_lcm(lcm, S->Constraint[j][1+nvar+i], &lcm);
2037 for (int j = 0; j < S->NbConstraints; ++j) {
2038 if (value_negz_p(S->Constraint[j][1+nvar+i]))
2039 continue;
2040 if (value_one_p(S->Constraint[j][1+nvar+i]))
2041 continue;
2042 value_division(f, lcm, S->Constraint[j][1+nvar+i]);
2043 Vector_Scale(S->Constraint[j], M->p[c], f, S->Dimension+2);
2044 value_substract(M->p[c][S->Dimension+1],
2045 M->p[c][S->Dimension+1],
2046 lcm);
2047 value_increment(M->p[c][S->Dimension+1],
2048 M->p[c][S->Dimension+1]);
2049 ++c;
2051 Polyhedron *O = S;
2052 S = AddConstraints(M->p[0], c, S, MaxRays);
2053 if (O != P)
2054 Polyhedron_Free(O);
2055 Matrix_Free(M);
2056 if (emptyQ(S)) {
2057 Polyhedron_Free(S);
2058 value_clear(lcm);
2059 value_clear(f);
2060 return 0;
2063 value_clear(lcm);
2064 value_clear(f);
2066 #ifdef DEBUG_ER
2067 fprintf(stderr, "\nER: Sure\n");
2068 #endif /* DEBUG_ER */
2070 return split_sure(P, S, exist, nparam, MaxRays);
2073 static evalue* enumerate_sure2(Polyhedron *P,
2074 unsigned exist, unsigned nparam, unsigned MaxRays)
2076 int nvar = P->Dimension - exist - nparam;
2077 int r;
2078 for (r = 0; r < P->NbRays; ++r)
2079 if (value_one_p(P->Ray[r][0]) &&
2080 value_one_p(P->Ray[r][P->Dimension+1]))
2081 break;
2083 if (r >= P->NbRays)
2084 return 0;
2086 Matrix *M = Matrix_Alloc(nvar + 1 + nparam, P->Dimension+2);
2087 for (int i = 0; i < nvar; ++i)
2088 value_set_si(M->p[i][1+i], 1);
2089 for (int i = 0; i < nparam; ++i)
2090 value_set_si(M->p[i+nvar][1+nvar+exist+i], 1);
2091 Vector_Copy(P->Ray[r]+1+nvar, M->p[nvar+nparam]+1+nvar, exist);
2092 value_set_si(M->p[nvar+nparam][0], 1);
2093 value_set_si(M->p[nvar+nparam][P->Dimension+1], 1);
2094 Polyhedron * F = Rays2Polyhedron(M, MaxRays);
2095 Matrix_Free(M);
2097 Polyhedron *I = DomainIntersection(F, P, MaxRays);
2098 Polyhedron_Free(F);
2100 #ifdef DEBUG_ER
2101 fprintf(stderr, "\nER: Sure2\n");
2102 #endif /* DEBUG_ER */
2104 return split_sure(P, I, exist, nparam, MaxRays);
2107 static evalue* enumerate_cyclic(Polyhedron *P,
2108 unsigned exist, unsigned nparam,
2109 evalue * EP, int r, int p, unsigned MaxRays)
2111 int nvar = P->Dimension - exist - nparam;
2113 /* If EP in its fractional maps only contains references
2114 * to the remainder parameter with appropriate coefficients
2115 * then we could in principle avoid adding existentially
2116 * quantified variables to the validity domains.
2117 * We'd have to replace the remainder by m { p/m }
2118 * and multiply with an appropriate factor that is one
2119 * only in the appropriate range.
2120 * This last multiplication can be avoided if EP
2121 * has a single validity domain with no (further)
2122 * constraints on the remainder parameter
2125 Matrix *CT = Matrix_Alloc(nparam+1, nparam+3);
2126 Matrix *M = Matrix_Alloc(1, 1+nparam+3);
2127 for (int j = 0; j < nparam; ++j)
2128 if (j != p)
2129 value_set_si(CT->p[j][j], 1);
2130 value_set_si(CT->p[p][nparam+1], 1);
2131 value_set_si(CT->p[nparam][nparam+2], 1);
2132 value_set_si(M->p[0][1+p], -1);
2133 value_absolute(M->p[0][1+nparam], P->Ray[0][1+nvar+exist+p]);
2134 value_set_si(M->p[0][1+nparam+1], 1);
2135 Polyhedron *CEq = Constraints2Polyhedron(M, 1);
2136 Matrix_Free(M);
2137 addeliminatedparams_enum(EP, CT, CEq, MaxRays, nparam);
2138 Polyhedron_Free(CEq);
2139 Matrix_Free(CT);
2141 return EP;
2144 static void enumerate_vd_add_ray(evalue *EP, Matrix *Rays, unsigned MaxRays)
2146 if (value_notzero_p(EP->d))
2147 return;
2149 assert(EP->x.p->type == partition);
2150 assert(EP->x.p->pos == EVALUE_DOMAIN(EP->x.p->arr[0])->Dimension);
2151 for (int i = 0; i < EP->x.p->size/2; ++i) {
2152 Polyhedron *D = EVALUE_DOMAIN(EP->x.p->arr[2*i]);
2153 Polyhedron *N = DomainAddRays(D, Rays, MaxRays);
2154 EVALUE_SET_DOMAIN(EP->x.p->arr[2*i], N);
2155 Domain_Free(D);
2159 static evalue* enumerate_line(Polyhedron *P,
2160 unsigned exist, unsigned nparam, unsigned MaxRays)
2162 if (P->NbBid == 0)
2163 return 0;
2165 #ifdef DEBUG_ER
2166 fprintf(stderr, "\nER: Line\n");
2167 #endif /* DEBUG_ER */
2169 int nvar = P->Dimension - exist - nparam;
2170 int i, j;
2171 for (i = 0; i < nparam; ++i)
2172 if (value_notzero_p(P->Ray[0][1+nvar+exist+i]))
2173 break;
2174 assert(i < nparam);
2175 for (j = i+1; j < nparam; ++j)
2176 if (value_notzero_p(P->Ray[0][1+nvar+exist+i]))
2177 break;
2178 assert(j >= nparam); // for now
2180 Matrix *M = Matrix_Alloc(2, P->Dimension+2);
2181 value_set_si(M->p[0][0], 1);
2182 value_set_si(M->p[0][1+nvar+exist+i], 1);
2183 value_set_si(M->p[1][0], 1);
2184 value_set_si(M->p[1][1+nvar+exist+i], -1);
2185 value_absolute(M->p[1][1+P->Dimension], P->Ray[0][1+nvar+exist+i]);
2186 value_decrement(M->p[1][1+P->Dimension], M->p[1][1+P->Dimension]);
2187 Polyhedron *S = AddConstraints(M->p[0], 2, P, MaxRays);
2188 evalue *EP = barvinok_enumerate_e(S, exist, nparam, MaxRays);
2189 Polyhedron_Free(S);
2190 Matrix_Free(M);
2192 return enumerate_cyclic(P, exist, nparam, EP, 0, i, MaxRays);
2195 static int single_param_pos(Polyhedron*P, unsigned exist, unsigned nparam,
2196 int r)
2198 int nvar = P->Dimension - exist - nparam;
2199 if (First_Non_Zero(P->Ray[r]+1, nvar) != -1)
2200 return -1;
2201 int i = First_Non_Zero(P->Ray[r]+1+nvar+exist, nparam);
2202 if (i == -1)
2203 return -1;
2204 if (First_Non_Zero(P->Ray[r]+1+nvar+exist+1, nparam-i-1) != -1)
2205 return -1;
2206 return i;
2209 static evalue* enumerate_remove_ray(Polyhedron *P, int r,
2210 unsigned exist, unsigned nparam, unsigned MaxRays)
2212 #ifdef DEBUG_ER
2213 fprintf(stderr, "\nER: RedundantRay\n");
2214 #endif /* DEBUG_ER */
2216 Value one;
2217 value_init(one);
2218 value_set_si(one, 1);
2219 int len = P->NbRays-1;
2220 Matrix *M = Matrix_Alloc(2 * len, P->Dimension+2);
2221 Vector_Copy(P->Ray[0], M->p[0], r * (P->Dimension+2));
2222 Vector_Copy(P->Ray[r+1], M->p[r], (len-r) * (P->Dimension+2));
2223 for (int j = 0; j < P->NbRays; ++j) {
2224 if (j == r)
2225 continue;
2226 Vector_Combine(P->Ray[j], P->Ray[r], M->p[len+j-(j>r)],
2227 one, P->Ray[j][P->Dimension+1], P->Dimension+2);
2230 P = Rays2Polyhedron(M, MaxRays);
2231 Matrix_Free(M);
2232 evalue *EP = barvinok_enumerate_e(P, exist, nparam, MaxRays);
2233 Polyhedron_Free(P);
2234 value_clear(one);
2236 return EP;
2239 static evalue* enumerate_redundant_ray(Polyhedron *P,
2240 unsigned exist, unsigned nparam, unsigned MaxRays)
2242 assert(P->NbBid == 0);
2243 int nvar = P->Dimension - exist - nparam;
2244 Value m;
2245 value_init(m);
2247 for (int r = 0; r < P->NbRays; ++r) {
2248 if (value_notzero_p(P->Ray[r][P->Dimension+1]))
2249 continue;
2250 int i1 = single_param_pos(P, exist, nparam, r);
2251 if (i1 == -1)
2252 continue;
2253 for (int r2 = r+1; r2 < P->NbRays; ++r2) {
2254 if (value_notzero_p(P->Ray[r2][P->Dimension+1]))
2255 continue;
2256 int i2 = single_param_pos(P, exist, nparam, r2);
2257 if (i2 == -1)
2258 continue;
2259 if (i1 != i2)
2260 continue;
2262 value_division(m, P->Ray[r][1+nvar+exist+i1],
2263 P->Ray[r2][1+nvar+exist+i1]);
2264 value_multiply(m, m, P->Ray[r2][1+nvar+exist+i1]);
2265 /* r2 divides r => r redundant */
2266 if (value_eq(m, P->Ray[r][1+nvar+exist+i1])) {
2267 value_clear(m);
2268 return enumerate_remove_ray(P, r, exist, nparam, MaxRays);
2271 value_division(m, P->Ray[r2][1+nvar+exist+i1],
2272 P->Ray[r][1+nvar+exist+i1]);
2273 value_multiply(m, m, P->Ray[r][1+nvar+exist+i1]);
2274 /* r divides r2 => r2 redundant */
2275 if (value_eq(m, P->Ray[r2][1+nvar+exist+i1])) {
2276 value_clear(m);
2277 return enumerate_remove_ray(P, r2, exist, nparam, MaxRays);
2281 value_clear(m);
2282 return 0;
2285 static Polyhedron *upper_bound(Polyhedron *P,
2286 int pos, Value *max, Polyhedron **R)
2288 Value v;
2289 int r;
2290 value_init(v);
2292 *R = 0;
2293 Polyhedron *N;
2294 Polyhedron *B = 0;
2295 for (Polyhedron *Q = P; Q; Q = N) {
2296 N = Q->next;
2297 for (r = 0; r < P->NbRays; ++r) {
2298 if (value_zero_p(P->Ray[r][P->Dimension+1]) &&
2299 value_pos_p(P->Ray[r][1+pos]))
2300 break;
2302 if (r < P->NbRays) {
2303 Q->next = *R;
2304 *R = Q;
2305 continue;
2306 } else {
2307 Q->next = B;
2308 B = Q;
2310 for (r = 0; r < P->NbRays; ++r) {
2311 if (value_zero_p(P->Ray[r][P->Dimension+1]))
2312 continue;
2313 mpz_fdiv_q(v, P->Ray[r][1+pos], P->Ray[r][1+P->Dimension]);
2314 if ((!Q->next && r == 0) || value_gt(v, *max))
2315 value_assign(*max, v);
2318 value_clear(v);
2319 return B;
2322 static evalue* enumerate_ray(Polyhedron *P,
2323 unsigned exist, unsigned nparam, unsigned MaxRays)
2325 assert(P->NbBid == 0);
2326 int nvar = P->Dimension - exist - nparam;
2328 int r;
2329 for (r = 0; r < P->NbRays; ++r)
2330 if (value_zero_p(P->Ray[r][P->Dimension+1]))
2331 break;
2332 if (r >= P->NbRays)
2333 return 0;
2335 int r2;
2336 for (r2 = r+1; r2 < P->NbRays; ++r2)
2337 if (value_zero_p(P->Ray[r2][P->Dimension+1]))
2338 break;
2339 if (r2 < P->NbRays) {
2340 if (nvar > 0)
2341 return enumerate_sum(P, exist, nparam, MaxRays);
2344 #ifdef DEBUG_ER
2345 fprintf(stderr, "\nER: Ray\n");
2346 #endif /* DEBUG_ER */
2348 Value m;
2349 Value one;
2350 value_init(m);
2351 value_init(one);
2352 value_set_si(one, 1);
2353 int i = single_param_pos(P, exist, nparam, r);
2354 assert(i != -1); // for now;
2356 Matrix *M = Matrix_Alloc(P->NbRays, P->Dimension+2);
2357 for (int j = 0; j < P->NbRays; ++j) {
2358 Vector_Combine(P->Ray[j], P->Ray[r], M->p[j],
2359 one, P->Ray[j][P->Dimension+1], P->Dimension+2);
2361 Polyhedron *S = Rays2Polyhedron(M, MaxRays);
2362 Matrix_Free(M);
2363 Polyhedron *D = DomainDifference(P, S, MaxRays);
2364 Polyhedron_Free(S);
2365 // Polyhedron_Print(stderr, P_VALUE_FMT, D);
2366 assert(value_pos_p(P->Ray[r][1+nvar+exist+i])); // for now
2367 Polyhedron *R;
2368 D = upper_bound(D, nvar+exist+i, &m, &R);
2369 assert(D);
2370 Domain_Free(D);
2372 M = Matrix_Alloc(2, P->Dimension+2);
2373 value_set_si(M->p[0][0], 1);
2374 value_set_si(M->p[1][0], 1);
2375 value_set_si(M->p[0][1+nvar+exist+i], -1);
2376 value_set_si(M->p[1][1+nvar+exist+i], 1);
2377 value_assign(M->p[0][1+P->Dimension], m);
2378 value_oppose(M->p[1][1+P->Dimension], m);
2379 value_addto(M->p[1][1+P->Dimension], M->p[1][1+P->Dimension],
2380 P->Ray[r][1+nvar+exist+i]);
2381 value_decrement(M->p[1][1+P->Dimension], M->p[1][1+P->Dimension]);
2382 // Matrix_Print(stderr, P_VALUE_FMT, M);
2383 D = AddConstraints(M->p[0], 2, P, MaxRays);
2384 // Polyhedron_Print(stderr, P_VALUE_FMT, D);
2385 value_substract(M->p[0][1+P->Dimension], M->p[0][1+P->Dimension],
2386 P->Ray[r][1+nvar+exist+i]);
2387 // Matrix_Print(stderr, P_VALUE_FMT, M);
2388 S = AddConstraints(M->p[0], 1, P, MaxRays);
2389 // Polyhedron_Print(stderr, P_VALUE_FMT, S);
2390 Matrix_Free(M);
2392 evalue *EP = barvinok_enumerate_e(D, exist, nparam, MaxRays);
2393 Polyhedron_Free(D);
2394 value_clear(one);
2395 value_clear(m);
2397 if (value_notone_p(P->Ray[r][1+nvar+exist+i]))
2398 EP = enumerate_cyclic(P, exist, nparam, EP, r, i, MaxRays);
2399 else {
2400 M = Matrix_Alloc(1, nparam+2);
2401 value_set_si(M->p[0][0], 1);
2402 value_set_si(M->p[0][1+i], 1);
2403 enumerate_vd_add_ray(EP, M, MaxRays);
2404 Matrix_Free(M);
2407 if (!emptyQ(S)) {
2408 evalue *E = barvinok_enumerate_e(S, exist, nparam, MaxRays);
2409 eadd(E, EP);
2410 free_evalue_refs(E);
2411 free(E);
2413 Polyhedron_Free(S);
2415 if (R) {
2416 assert(nvar == 0);
2417 evalue *ER = enumerate_or(R, exist, nparam, MaxRays);
2418 eor(ER, EP);
2419 free_evalue_refs(ER);
2420 free(ER);
2423 return EP;
2426 static evalue* new_zero_ep()
2428 evalue *EP;
2429 ALLOC(evalue, EP);
2430 value_init(EP->d);
2431 evalue_set_si(EP, 0, 1);
2432 return EP;
2435 static evalue* enumerate_vd(Polyhedron **PA,
2436 unsigned exist, unsigned nparam, unsigned MaxRays)
2438 Polyhedron *P = *PA;
2439 int nvar = P->Dimension - exist - nparam;
2440 Param_Polyhedron *PP = NULL;
2441 Polyhedron *C = Universe_Polyhedron(nparam);
2442 Polyhedron *CEq;
2443 Matrix *CT;
2444 Polyhedron *PR = P;
2445 PP = Polyhedron2Param_SimplifiedDomain(&PR,C,MaxRays,&CEq,&CT);
2446 Polyhedron_Free(C);
2448 int nd;
2449 Param_Domain *D, *last;
2450 Value c;
2451 value_init(c);
2452 for (nd = 0, D=PP->D; D; D=D->next, ++nd)
2455 Polyhedron **VD = new Polyhedron_p[nd];
2456 Polyhedron **fVD = new Polyhedron_p[nd];
2457 for(nd = 0, D=PP->D; D; D=D->next) {
2458 Polyhedron *rVD = reduce_domain(D->Domain, CT, CEq,
2459 fVD, nd, MaxRays);
2460 if (!rVD)
2461 continue;
2463 VD[nd++] = rVD;
2464 last = D;
2467 evalue *EP = 0;
2469 if (nd == 0)
2470 EP = new_zero_ep();
2472 /* This doesn't seem to have any effect */
2473 if (nd == 1) {
2474 Polyhedron *CA = align_context(VD[0], P->Dimension, MaxRays);
2475 Polyhedron *O = P;
2476 P = DomainIntersection(P, CA, MaxRays);
2477 if (O != *PA)
2478 Polyhedron_Free(O);
2479 Polyhedron_Free(CA);
2480 if (emptyQ(P))
2481 EP = new_zero_ep();
2484 if (!EP && CT->NbColumns != CT->NbRows) {
2485 Polyhedron *CEqr = DomainImage(CEq, CT, MaxRays);
2486 Polyhedron *CA = align_context(CEqr, PR->Dimension, MaxRays);
2487 Polyhedron *I = DomainIntersection(PR, CA, MaxRays);
2488 Polyhedron_Free(CEqr);
2489 Polyhedron_Free(CA);
2490 #ifdef DEBUG_ER
2491 fprintf(stderr, "\nER: Eliminate\n");
2492 #endif /* DEBUG_ER */
2493 nparam -= CT->NbColumns - CT->NbRows;
2494 EP = barvinok_enumerate_e(I, exist, nparam, MaxRays);
2495 nparam += CT->NbColumns - CT->NbRows;
2496 addeliminatedparams_enum(EP, CT, CEq, MaxRays, nparam);
2497 Polyhedron_Free(I);
2499 if (PR != *PA)
2500 Polyhedron_Free(PR);
2501 PR = 0;
2503 if (!EP && nd > 1) {
2504 #ifdef DEBUG_ER
2505 fprintf(stderr, "\nER: VD\n");
2506 #endif /* DEBUG_ER */
2507 for (int i = 0; i < nd; ++i) {
2508 Polyhedron *CA = align_context(VD[i], P->Dimension, MaxRays);
2509 Polyhedron *I = DomainIntersection(P, CA, MaxRays);
2511 if (i == 0)
2512 EP = barvinok_enumerate_e(I, exist, nparam, MaxRays);
2513 else {
2514 evalue *E = barvinok_enumerate_e(I, exist, nparam, MaxRays);
2515 eadd(E, EP);
2516 free_evalue_refs(E);
2517 free(E);
2519 Polyhedron_Free(I);
2520 Polyhedron_Free(CA);
2524 for (int i = 0; i < nd; ++i) {
2525 Polyhedron_Free(VD[i]);
2526 Polyhedron_Free(fVD[i]);
2528 delete [] VD;
2529 delete [] fVD;
2530 value_clear(c);
2532 if (!EP && nvar == 0) {
2533 Value f;
2534 value_init(f);
2535 Param_Vertices *V, *V2;
2536 Matrix* M = Matrix_Alloc(1, P->Dimension+2);
2538 FORALL_PVertex_in_ParamPolyhedron(V, last, PP) {
2539 bool found = false;
2540 FORALL_PVertex_in_ParamPolyhedron(V2, last, PP) {
2541 if (V == V2) {
2542 found = true;
2543 continue;
2545 if (!found)
2546 continue;
2547 for (int i = 0; i < exist; ++i) {
2548 value_oppose(f, V->Vertex->p[i][nparam+1]);
2549 Vector_Combine(V->Vertex->p[i],
2550 V2->Vertex->p[i],
2551 M->p[0] + 1 + nvar + exist,
2552 V2->Vertex->p[i][nparam+1],
2554 nparam+1);
2555 int j;
2556 for (j = 0; j < nparam; ++j)
2557 if (value_notzero_p(M->p[0][1+nvar+exist+j]))
2558 break;
2559 if (j >= nparam)
2560 continue;
2561 ConstraintSimplify(M->p[0], M->p[0],
2562 P->Dimension+2, &f);
2563 value_set_si(M->p[0][0], 0);
2564 Polyhedron *para = AddConstraints(M->p[0], 1, P,
2565 MaxRays);
2566 if (emptyQ(para)) {
2567 Polyhedron_Free(para);
2568 continue;
2570 Polyhedron *pos, *neg;
2571 value_set_si(M->p[0][0], 1);
2572 value_decrement(M->p[0][P->Dimension+1],
2573 M->p[0][P->Dimension+1]);
2574 neg = AddConstraints(M->p[0], 1, P, MaxRays);
2575 value_set_si(f, -1);
2576 Vector_Scale(M->p[0]+1, M->p[0]+1, f,
2577 P->Dimension+1);
2578 value_decrement(M->p[0][P->Dimension+1],
2579 M->p[0][P->Dimension+1]);
2580 value_decrement(M->p[0][P->Dimension+1],
2581 M->p[0][P->Dimension+1]);
2582 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2583 if (emptyQ(neg) && emptyQ(pos)) {
2584 Polyhedron_Free(para);
2585 Polyhedron_Free(pos);
2586 Polyhedron_Free(neg);
2587 continue;
2589 #ifdef DEBUG_ER
2590 fprintf(stderr, "\nER: Order\n");
2591 #endif /* DEBUG_ER */
2592 EP = barvinok_enumerate_e(para, exist, nparam, MaxRays);
2593 evalue *E;
2594 if (!emptyQ(pos)) {
2595 E = barvinok_enumerate_e(pos, exist, nparam, MaxRays);
2596 eadd(E, EP);
2597 free_evalue_refs(E);
2598 free(E);
2600 if (!emptyQ(neg)) {
2601 E = barvinok_enumerate_e(neg, exist, nparam, MaxRays);
2602 eadd(E, EP);
2603 free_evalue_refs(E);
2604 free(E);
2606 Polyhedron_Free(para);
2607 Polyhedron_Free(pos);
2608 Polyhedron_Free(neg);
2609 break;
2611 if (EP)
2612 break;
2613 } END_FORALL_PVertex_in_ParamPolyhedron;
2614 if (EP)
2615 break;
2616 } END_FORALL_PVertex_in_ParamPolyhedron;
2618 if (!EP) {
2619 /* Search for vertex coordinate to split on */
2620 /* First look for one independent of the parameters */
2621 FORALL_PVertex_in_ParamPolyhedron(V, last, PP) {
2622 for (int i = 0; i < exist; ++i) {
2623 int j;
2624 for (j = 0; j < nparam; ++j)
2625 if (value_notzero_p(V->Vertex->p[i][j]))
2626 break;
2627 if (j < nparam)
2628 continue;
2629 value_set_si(M->p[0][0], 1);
2630 Vector_Set(M->p[0]+1, 0, nvar+exist);
2631 Vector_Copy(V->Vertex->p[i],
2632 M->p[0] + 1 + nvar + exist, nparam+1);
2633 value_oppose(M->p[0][1+nvar+i],
2634 V->Vertex->p[i][nparam+1]);
2636 Polyhedron *pos, *neg;
2637 value_set_si(M->p[0][0], 1);
2638 value_decrement(M->p[0][P->Dimension+1],
2639 M->p[0][P->Dimension+1]);
2640 neg = AddConstraints(M->p[0], 1, P, MaxRays);
2641 value_set_si(f, -1);
2642 Vector_Scale(M->p[0]+1, M->p[0]+1, f,
2643 P->Dimension+1);
2644 value_decrement(M->p[0][P->Dimension+1],
2645 M->p[0][P->Dimension+1]);
2646 value_decrement(M->p[0][P->Dimension+1],
2647 M->p[0][P->Dimension+1]);
2648 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2649 if (emptyQ(neg) || emptyQ(pos)) {
2650 Polyhedron_Free(pos);
2651 Polyhedron_Free(neg);
2652 continue;
2654 Polyhedron_Free(pos);
2655 value_increment(M->p[0][P->Dimension+1],
2656 M->p[0][P->Dimension+1]);
2657 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2658 #ifdef DEBUG_ER
2659 fprintf(stderr, "\nER: Vertex\n");
2660 #endif /* DEBUG_ER */
2661 pos->next = neg;
2662 EP = enumerate_or(pos, exist, nparam, MaxRays);
2663 break;
2665 if (EP)
2666 break;
2667 } END_FORALL_PVertex_in_ParamPolyhedron;
2670 if (!EP) {
2671 /* Search for vertex coordinate to split on */
2672 /* Now look for one that depends on the parameters */
2673 FORALL_PVertex_in_ParamPolyhedron(V, last, PP) {
2674 for (int i = 0; i < exist; ++i) {
2675 value_set_si(M->p[0][0], 1);
2676 Vector_Set(M->p[0]+1, 0, nvar+exist);
2677 Vector_Copy(V->Vertex->p[i],
2678 M->p[0] + 1 + nvar + exist, nparam+1);
2679 value_oppose(M->p[0][1+nvar+i],
2680 V->Vertex->p[i][nparam+1]);
2682 Polyhedron *pos, *neg;
2683 value_set_si(M->p[0][0], 1);
2684 value_decrement(M->p[0][P->Dimension+1],
2685 M->p[0][P->Dimension+1]);
2686 neg = AddConstraints(M->p[0], 1, P, MaxRays);
2687 value_set_si(f, -1);
2688 Vector_Scale(M->p[0]+1, M->p[0]+1, f,
2689 P->Dimension+1);
2690 value_decrement(M->p[0][P->Dimension+1],
2691 M->p[0][P->Dimension+1]);
2692 value_decrement(M->p[0][P->Dimension+1],
2693 M->p[0][P->Dimension+1]);
2694 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2695 if (emptyQ(neg) || emptyQ(pos)) {
2696 Polyhedron_Free(pos);
2697 Polyhedron_Free(neg);
2698 continue;
2700 Polyhedron_Free(pos);
2701 value_increment(M->p[0][P->Dimension+1],
2702 M->p[0][P->Dimension+1]);
2703 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2704 #ifdef DEBUG_ER
2705 fprintf(stderr, "\nER: ParamVertex\n");
2706 #endif /* DEBUG_ER */
2707 pos->next = neg;
2708 EP = enumerate_or(pos, exist, nparam, MaxRays);
2709 break;
2711 if (EP)
2712 break;
2713 } END_FORALL_PVertex_in_ParamPolyhedron;
2716 Matrix_Free(M);
2717 value_clear(f);
2720 if (CEq)
2721 Polyhedron_Free(CEq);
2722 if (CT)
2723 Matrix_Free(CT);
2724 if (PP)
2725 Param_Polyhedron_Free(PP);
2726 *PA = P;
2728 return EP;
2731 #ifndef HAVE_PIPLIB
2732 evalue *barvinok_enumerate_pip(Polyhedron *P,
2733 unsigned exist, unsigned nparam, unsigned MaxRays)
2735 return 0;
2737 #else
2738 evalue *barvinok_enumerate_pip(Polyhedron *P,
2739 unsigned exist, unsigned nparam, unsigned MaxRays)
2741 int nvar = P->Dimension - exist - nparam;
2742 evalue *EP = new_zero_ep();
2743 Polyhedron *Q, *N, *T = 0;
2744 Value min, tmp;
2745 value_init(min);
2746 value_init(tmp);
2748 #ifdef DEBUG_ER
2749 fprintf(stderr, "\nER: PIP\n");
2750 #endif /* DEBUG_ER */
2752 for (int i = 0; i < P->Dimension; ++i) {
2753 bool pos = false;
2754 bool neg = false;
2755 bool posray = false;
2756 bool negray = false;
2757 value_set_si(min, 0);
2758 for (int j = 0; j < P->NbRays; ++j) {
2759 if (value_pos_p(P->Ray[j][1+i])) {
2760 pos = true;
2761 if (value_zero_p(P->Ray[j][1+P->Dimension]))
2762 posray = true;
2763 } else if (value_neg_p(P->Ray[j][1+i])) {
2764 neg = true;
2765 if (value_zero_p(P->Ray[j][1+P->Dimension]))
2766 negray = true;
2767 else {
2768 mpz_fdiv_q(tmp,
2769 P->Ray[j][1+i], P->Ray[j][1+P->Dimension]);
2770 if (value_lt(tmp, min))
2771 value_assign(min, tmp);
2775 if (pos && neg) {
2776 assert(!(posray && negray));
2777 assert(!negray); // for now
2778 Polyhedron *O = T ? T : P;
2779 /* shift by a safe amount */
2780 Matrix *M = Matrix_Alloc(O->NbRays, O->Dimension+2);
2781 Vector_Copy(O->Ray[0], M->p[0], O->NbRays * (O->Dimension+2));
2782 for (int j = 0; j < P->NbRays; ++j) {
2783 if (value_notzero_p(M->p[j][1+P->Dimension])) {
2784 value_multiply(tmp, min, M->p[j][1+P->Dimension]);
2785 value_substract(M->p[j][1+i], M->p[j][1+i], tmp);
2788 if (T)
2789 Polyhedron_Free(T);
2790 T = Rays2Polyhedron(M, MaxRays);
2791 Matrix_Free(M);
2792 } else if (neg) {
2793 /* negating a parameter requires that we substitute in the
2794 * sign again afterwards.
2795 * Disallow for now.
2797 assert(i < nvar+exist);
2798 if (!T)
2799 T = Polyhedron_Copy(P);
2800 for (int j = 0; j < T->NbRays; ++j)
2801 value_oppose(T->Ray[j][1+i], T->Ray[j][1+i]);
2802 for (int j = 0; j < T->NbConstraints; ++j)
2803 value_oppose(T->Constraint[j][1+i], T->Constraint[j][1+i]);
2806 value_clear(min);
2807 value_clear(tmp);
2809 Polyhedron *D = pip_lexmin(T ? T : P, exist, nparam);
2810 for (Q = D; Q; Q = N) {
2811 N = Q->next;
2812 Q->next = 0;
2813 evalue *E;
2814 exist = Q->Dimension - nvar - nparam;
2815 E = barvinok_enumerate_e(Q, exist, nparam, MaxRays);
2816 Polyhedron_Free(Q);
2817 eadd(E, EP);
2818 free_evalue_refs(E);
2819 free(E);
2822 if (T)
2823 Polyhedron_Free(T);
2825 return EP;
2827 #endif
2830 static bool is_single(Value *row, int pos, int len)
2832 return First_Non_Zero(row, pos) == -1 &&
2833 First_Non_Zero(row+pos+1, len-pos-1) == -1;
2836 static evalue* barvinok_enumerate_e_r(Polyhedron *P,
2837 unsigned exist, unsigned nparam, unsigned MaxRays);
2839 #ifdef DEBUG_ER
2840 static int er_level = 0;
2842 evalue* barvinok_enumerate_e(Polyhedron *P,
2843 unsigned exist, unsigned nparam, unsigned MaxRays)
2845 fprintf(stderr, "\nER: level %i\n", er_level);
2846 int nvar = P->Dimension - exist - nparam;
2847 fprintf(stderr, "%d %d %d\n", nvar, exist, nparam);
2849 Polyhedron_Print(stderr, P_VALUE_FMT, P);
2850 ++er_level;
2851 P = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
2852 evalue *EP = barvinok_enumerate_e_r(P, exist, nparam, MaxRays);
2853 Polyhedron_Free(P);
2854 --er_level;
2855 return EP;
2857 #else
2858 evalue* barvinok_enumerate_e(Polyhedron *P,
2859 unsigned exist, unsigned nparam, unsigned MaxRays)
2861 P = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
2862 evalue *EP = barvinok_enumerate_e_r(P, exist, nparam, MaxRays);
2863 Polyhedron_Free(P);
2864 return EP;
2866 #endif
2868 static evalue* barvinok_enumerate_e_r(Polyhedron *P,
2869 unsigned exist, unsigned nparam, unsigned MaxRays)
2871 if (exist == 0) {
2872 Polyhedron *U = Universe_Polyhedron(nparam);
2873 evalue *EP = barvinok_enumerate_ev(P, U, MaxRays);
2874 //char *param_name[] = {"P", "Q", "R", "S", "T" };
2875 //print_evalue(stdout, EP, param_name);
2876 Polyhedron_Free(U);
2877 return EP;
2880 int nvar = P->Dimension - exist - nparam;
2881 int len = P->Dimension + 2;
2883 if (emptyQ(P))
2884 return new_zero_ep();
2886 if (nvar == 0 && nparam == 0) {
2887 evalue *EP = new_zero_ep();
2888 barvinok_count(P, &EP->x.n, MaxRays);
2889 if (value_pos_p(EP->x.n))
2890 value_set_si(EP->x.n, 1);
2891 return EP;
2894 int r;
2895 for (r = 0; r < P->NbRays; ++r)
2896 if (value_zero_p(P->Ray[r][0]) ||
2897 value_zero_p(P->Ray[r][P->Dimension+1])) {
2898 int i;
2899 for (i = 0; i < nvar; ++i)
2900 if (value_notzero_p(P->Ray[r][i+1]))
2901 break;
2902 if (i >= nvar)
2903 continue;
2904 for (i = nvar + exist; i < nvar + exist + nparam; ++i)
2905 if (value_notzero_p(P->Ray[r][i+1]))
2906 break;
2907 if (i >= nvar + exist + nparam)
2908 break;
2910 if (r < P->NbRays) {
2911 evalue *EP = new_zero_ep();
2912 value_set_si(EP->x.n, -1);
2913 return EP;
2916 int first;
2917 for (r = 0; r < P->NbEq; ++r)
2918 if ((first = First_Non_Zero(P->Constraint[r]+1+nvar, exist)) != -1)
2919 break;
2920 if (r < P->NbEq) {
2921 if (First_Non_Zero(P->Constraint[r]+1+nvar+first+1,
2922 exist-first-1) != -1) {
2923 Polyhedron *T = rotate_along(P, r, nvar, exist, MaxRays);
2924 #ifdef DEBUG_ER
2925 fprintf(stderr, "\nER: Equality\n");
2926 #endif /* DEBUG_ER */
2927 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2928 Polyhedron_Free(T);
2929 return EP;
2930 } else {
2931 #ifdef DEBUG_ER
2932 fprintf(stderr, "\nER: Fixed\n");
2933 #endif /* DEBUG_ER */
2934 if (first == 0)
2935 return barvinok_enumerate_e(P, exist-1, nparam, MaxRays);
2936 else {
2937 Polyhedron *T = Polyhedron_Copy(P);
2938 SwapColumns(T, nvar+1, nvar+1+first);
2939 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2940 Polyhedron_Free(T);
2941 return EP;
2946 Vector *row = Vector_Alloc(len);
2947 value_set_si(row->p[0], 1);
2949 Value f;
2950 value_init(f);
2952 enum constraint* info = new constraint[exist];
2953 for (int i = 0; i < exist; ++i) {
2954 info[i] = ALL_POS;
2955 for (int l = P->NbEq; l < P->NbConstraints; ++l) {
2956 if (value_negz_p(P->Constraint[l][nvar+i+1]))
2957 continue;
2958 bool l_parallel = is_single(P->Constraint[l]+nvar+1, i, exist);
2959 for (int u = P->NbEq; u < P->NbConstraints; ++u) {
2960 if (value_posz_p(P->Constraint[u][nvar+i+1]))
2961 continue;
2962 bool lu_parallel = l_parallel ||
2963 is_single(P->Constraint[u]+nvar+1, i, exist);
2964 value_oppose(f, P->Constraint[u][nvar+i+1]);
2965 Vector_Combine(P->Constraint[l]+1, P->Constraint[u]+1, row->p+1,
2966 f, P->Constraint[l][nvar+i+1], len-1);
2967 if (!(info[i] & INDEPENDENT)) {
2968 int j;
2969 for (j = 0; j < exist; ++j)
2970 if (j != i && value_notzero_p(row->p[nvar+j+1]))
2971 break;
2972 if (j == exist) {
2973 //printf("independent: i: %d, l: %d, u: %d\n", i, l, u);
2974 info[i] = (constraint)(info[i] | INDEPENDENT);
2977 if (info[i] & ALL_POS) {
2978 value_addto(row->p[len-1], row->p[len-1],
2979 P->Constraint[l][nvar+i+1]);
2980 value_addto(row->p[len-1], row->p[len-1], f);
2981 value_multiply(f, f, P->Constraint[l][nvar+i+1]);
2982 value_substract(row->p[len-1], row->p[len-1], f);
2983 value_decrement(row->p[len-1], row->p[len-1]);
2984 ConstraintSimplify(row->p, row->p, len, &f);
2985 value_set_si(f, -1);
2986 Vector_Scale(row->p+1, row->p+1, f, len-1);
2987 value_decrement(row->p[len-1], row->p[len-1]);
2988 Polyhedron *T = AddConstraints(row->p, 1, P, MaxRays);
2989 if (!emptyQ(T)) {
2990 //printf("not all_pos: i: %d, l: %d, u: %d\n", i, l, u);
2991 info[i] = (constraint)(info[i] ^ ALL_POS);
2993 //puts("pos remainder");
2994 //Polyhedron_Print(stdout, P_VALUE_FMT, T);
2995 Polyhedron_Free(T);
2997 if (!(info[i] & ONE_NEG)) {
2998 if (lu_parallel) {
2999 negative_test_constraint(P->Constraint[l],
3000 P->Constraint[u],
3001 row->p, nvar+i, len, &f);
3002 oppose_constraint(row->p, len, &f);
3003 Polyhedron *T = AddConstraints(row->p, 1, P, MaxRays);
3004 if (emptyQ(T)) {
3005 //printf("one_neg i: %d, l: %d, u: %d\n", i, l, u);
3006 info[i] = (constraint)(info[i] | ONE_NEG);
3008 //puts("neg remainder");
3009 //Polyhedron_Print(stdout, P_VALUE_FMT, T);
3010 Polyhedron_Free(T);
3013 if (!(info[i] & ALL_POS) && (info[i] & ONE_NEG))
3014 goto next;
3017 if (info[i] & ALL_POS)
3018 break;
3019 next:
3024 for (int i = 0; i < exist; ++i)
3025 printf("%i: %i\n", i, info[i]);
3027 for (int i = 0; i < exist; ++i)
3028 if (info[i] & ALL_POS) {
3029 #ifdef DEBUG_ER
3030 fprintf(stderr, "\nER: Positive\n");
3031 #endif /* DEBUG_ER */
3032 // Eliminate
3033 // Maybe we should chew off some of the fat here
3034 Matrix *M = Matrix_Alloc(P->Dimension, P->Dimension+1);
3035 for (int j = 0; j < P->Dimension; ++j)
3036 value_set_si(M->p[j][j + (j >= i+nvar)], 1);
3037 Polyhedron *T = Polyhedron_Image(P, M, MaxRays);
3038 Matrix_Free(M);
3039 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
3040 Polyhedron_Free(T);
3041 value_clear(f);
3042 Vector_Free(row);
3043 delete [] info;
3044 return EP;
3046 for (int i = 0; i < exist; ++i)
3047 if (info[i] & ONE_NEG) {
3048 #ifdef DEBUG_ER
3049 fprintf(stderr, "\nER: Negative\n");
3050 #endif /* DEBUG_ER */
3051 Vector_Free(row);
3052 value_clear(f);
3053 delete [] info;
3054 if (i == 0)
3055 return barvinok_enumerate_e(P, exist-1, nparam, MaxRays);
3056 else {
3057 Polyhedron *T = Polyhedron_Copy(P);
3058 SwapColumns(T, nvar+1, nvar+1+i);
3059 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
3060 Polyhedron_Free(T);
3061 return EP;
3064 for (int i = 0; i < exist; ++i)
3065 if (info[i] & INDEPENDENT) {
3066 Polyhedron *pos, *neg;
3068 /* Find constraint again and split off negative part */
3070 if (SplitOnVar(P, i, nvar, len, exist, MaxRays,
3071 row, f, true, &pos, &neg)) {
3072 #ifdef DEBUG_ER
3073 fprintf(stderr, "\nER: Split\n");
3074 #endif /* DEBUG_ER */
3076 evalue *EP =
3077 barvinok_enumerate_e(neg, exist-1, nparam, MaxRays);
3078 evalue *E =
3079 barvinok_enumerate_e(pos, exist, nparam, MaxRays);
3080 eadd(E, EP);
3081 free_evalue_refs(E);
3082 free(E);
3083 Polyhedron_Free(neg);
3084 Polyhedron_Free(pos);
3085 value_clear(f);
3086 Vector_Free(row);
3087 delete [] info;
3088 return EP;
3091 delete [] info;
3093 Polyhedron *O = P;
3094 Polyhedron *F;
3096 evalue *EP;
3098 EP = enumerate_line(P, exist, nparam, MaxRays);
3099 if (EP)
3100 goto out;
3102 EP = barvinok_enumerate_pip(P, exist, nparam, MaxRays);
3103 if (EP)
3104 goto out;
3106 EP = enumerate_redundant_ray(P, exist, nparam, MaxRays);
3107 if (EP)
3108 goto out;
3110 EP = enumerate_sure(P, exist, nparam, MaxRays);
3111 if (EP)
3112 goto out;
3114 EP = enumerate_ray(P, exist, nparam, MaxRays);
3115 if (EP)
3116 goto out;
3118 EP = enumerate_sure2(P, exist, nparam, MaxRays);
3119 if (EP)
3120 goto out;
3122 F = unfringe(P, MaxRays);
3123 if (!PolyhedronIncludes(F, P)) {
3124 #ifdef DEBUG_ER
3125 fprintf(stderr, "\nER: Fringed\n");
3126 #endif /* DEBUG_ER */
3127 EP = barvinok_enumerate_e(F, exist, nparam, MaxRays);
3128 Polyhedron_Free(F);
3129 goto out;
3131 Polyhedron_Free(F);
3133 if (nparam)
3134 EP = enumerate_vd(&P, exist, nparam, MaxRays);
3135 if (EP)
3136 goto out2;
3138 if (nvar != 0) {
3139 EP = enumerate_sum(P, exist, nparam, MaxRays);
3140 goto out2;
3143 assert(nvar == 0);
3145 int i;
3146 Polyhedron *pos, *neg;
3147 for (i = 0; i < exist; ++i)
3148 if (SplitOnVar(P, i, nvar, len, exist, MaxRays,
3149 row, f, false, &pos, &neg))
3150 break;
3152 assert (i < exist);
3154 pos->next = neg;
3155 EP = enumerate_or(pos, exist, nparam, MaxRays);
3157 out2:
3158 if (O != P)
3159 Polyhedron_Free(P);
3161 out:
3162 value_clear(f);
3163 Vector_Free(row);
3164 return EP;