allow negative powers
[barvinok.git] / barvinok.cc
blobacd19c59a547627a32e88b43decb382545badfe4
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 vec_ZZ num;
1264 mat_ZZ den;
1265 num.SetLength(ncone);
1266 den.SetDims(ncone,dim);
1268 int f = 0;
1269 for (int j = 0; j < P->NbRays; ++j) {
1270 for (Polyhedron *i = vcone[j]; i; i = i->next) {
1271 lattice_point(P->Ray[j]+1, i, lambda, num[f]);
1272 normalize(i, lambda, sign[f], num[f], den[f]);
1273 ++f;
1276 ZZ min = num[0];
1277 for (int j = 1; j < num.length(); ++j)
1278 if (num[j] < min)
1279 min = num[j];
1280 for (int j = 0; j < num.length(); ++j)
1281 num[j] -= min;
1283 f = 0;
1284 mpq_t count;
1285 mpq_init(count);
1286 for (int j = 0; j < P->NbRays; ++j) {
1287 for (Polyhedron *i = vcone[j]; i; i = i->next) {
1288 dpoly d(dim, num[f]);
1289 dpoly n(dim, den[f][0], 1);
1290 for (int k = 1; k < dim; ++k) {
1291 dpoly fact(dim, den[f][k], 1);
1292 n *= fact;
1294 d.div(n, count, sign[f]);
1295 ++f;
1298 assert(value_one_p(&count[0]._mp_den));
1299 value_multiply(*result, &count[0]._mp_num, factor);
1300 mpq_clear(count);
1302 for (int j = 0; j < P->NbRays; ++j)
1303 Domain_Free(vcone[j]);
1305 delete [] vcone;
1307 if (allocated)
1308 Polyhedron_Free(P);
1309 value_clear(factor);
1312 static void uni_polynom(int param, Vector *c, evalue *EP)
1314 unsigned dim = c->Size-2;
1315 value_init(EP->d);
1316 value_set_si(EP->d,0);
1317 EP->x.p = new_enode(polynomial, dim+1, param+1);
1318 for (int j = 0; j <= dim; ++j)
1319 evalue_set(&EP->x.p->arr[j], c->p[j], c->p[dim+1]);
1322 static void multi_polynom(Vector *c, evalue* X, evalue *EP)
1324 unsigned dim = c->Size-2;
1325 evalue EC;
1327 value_init(EC.d);
1328 evalue_set(&EC, c->p[dim], c->p[dim+1]);
1330 value_init(EP->d);
1331 evalue_set(EP, c->p[dim], c->p[dim+1]);
1333 for (int i = dim-1; i >= 0; --i) {
1334 emul(X, EP);
1335 value_assign(EC.x.n, c->p[i]);
1336 eadd(&EC, EP);
1338 free_evalue_refs(&EC);
1341 Polyhedron *unfringe (Polyhedron *P, unsigned MaxRays)
1343 int len = P->Dimension+2;
1344 Polyhedron *T, *R = P;
1345 Value g;
1346 value_init(g);
1347 Vector *row = Vector_Alloc(len);
1348 value_set_si(row->p[0], 1);
1350 R = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
1352 Matrix *M = Matrix_Alloc(2, len-1);
1353 value_set_si(M->p[1][len-2], 1);
1354 for (int v = 0; v < P->Dimension; ++v) {
1355 value_set_si(M->p[0][v], 1);
1356 Polyhedron *I = Polyhedron_Image(P, M, 2+1);
1357 value_set_si(M->p[0][v], 0);
1358 for (int r = 0; r < I->NbConstraints; ++r) {
1359 if (value_zero_p(I->Constraint[r][0]))
1360 continue;
1361 if (value_zero_p(I->Constraint[r][1]))
1362 continue;
1363 if (value_one_p(I->Constraint[r][1]))
1364 continue;
1365 if (value_mone_p(I->Constraint[r][1]))
1366 continue;
1367 value_absolute(g, I->Constraint[r][1]);
1368 Vector_Set(row->p+1, 0, len-2);
1369 value_division(row->p[1+v], I->Constraint[r][1], g);
1370 mpz_fdiv_q(row->p[len-1], I->Constraint[r][2], g);
1371 T = R;
1372 R = AddConstraints(row->p, 1, R, MaxRays);
1373 if (T != P)
1374 Polyhedron_Free(T);
1376 Polyhedron_Free(I);
1378 Matrix_Free(M);
1379 Vector_Free(row);
1380 value_clear(g);
1381 return R;
1384 static Polyhedron *reduce_domain(Polyhedron *D, Matrix *CT, Polyhedron *CEq,
1385 Polyhedron **fVD, int nd, unsigned MaxRays)
1387 assert(CEq);
1389 Polyhedron *Dt;
1390 Dt = CT ? DomainPreimage(D, CT, MaxRays) : D;
1391 Polyhedron *rVD = DomainIntersection(Dt, CEq, MaxRays);
1393 /* if rVD is empty or too small in geometric dimension */
1394 if(!rVD || emptyQ(rVD) ||
1395 (rVD->Dimension-rVD->NbEq < Dt->Dimension-Dt->NbEq-CEq->NbEq)) {
1396 if(rVD)
1397 Domain_Free(rVD);
1398 if (CT)
1399 Domain_Free(Dt);
1400 return 0; /* empty validity domain */
1403 if (CT)
1404 Domain_Free(Dt);
1406 fVD[nd] = Domain_Copy(rVD);
1407 for (int i = 0 ; i < nd; ++i) {
1408 Polyhedron *I = DomainIntersection(fVD[nd], fVD[i], MaxRays);
1409 if (emptyQ(I)) {
1410 Domain_Free(I);
1411 continue;
1413 Polyhedron *F = DomainSimplify(I, fVD[nd], MaxRays);
1414 if (F->NbEq == 1) {
1415 Polyhedron *T = rVD;
1416 rVD = DomainDifference(rVD, F, MaxRays);
1417 Domain_Free(T);
1419 Domain_Free(F);
1420 Domain_Free(I);
1423 rVD = DomainConstraintSimplify(rVD, MaxRays);
1424 if (emptyQ(rVD)) {
1425 Domain_Free(fVD[nd]);
1426 Domain_Free(rVD);
1427 return 0;
1430 Value c;
1431 value_init(c);
1432 barvinok_count(rVD, &c, MaxRays);
1433 if (value_zero_p(c)) {
1434 Domain_Free(rVD);
1435 rVD = 0;
1437 value_clear(c);
1439 return rVD;
1442 evalue* barvinok_enumerate_ev(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1444 //P = unfringe(P, MaxRays);
1445 Polyhedron *CEq = NULL, *rVD, *pVD, *CA;
1446 Matrix *CT = NULL;
1447 Param_Polyhedron *PP = NULL;
1448 Param_Domain *D, *next;
1449 Param_Vertices *V;
1450 int r = 0;
1451 unsigned nparam = C->Dimension;
1452 evalue *eres;
1453 ALLOC(evalue, eres);
1454 value_init(eres->d);
1455 value_set_si(eres->d, 0);
1457 evalue factor;
1458 value_init(factor.d);
1459 evalue_set_si(&factor, 1, 1);
1461 CA = align_context(C, P->Dimension, MaxRays);
1462 P = DomainIntersection(P, CA, MaxRays);
1463 Polyhedron_Free(CA);
1465 if (C->Dimension == 0 || emptyQ(P)) {
1466 constant:
1467 eres->x.p = new_enode(partition, 2, C->Dimension);
1468 EVALUE_SET_DOMAIN(eres->x.p->arr[0],
1469 DomainConstraintSimplify(CEq ? CEq : Polyhedron_Copy(C), MaxRays));
1470 value_set_si(eres->x.p->arr[1].d, 1);
1471 value_init(eres->x.p->arr[1].x.n);
1472 if (emptyQ(P))
1473 value_set_si(eres->x.p->arr[1].x.n, 0);
1474 else
1475 barvinok_count(P, &eres->x.p->arr[1].x.n, MaxRays);
1476 out:
1477 emul(&factor, eres);
1478 reduce_evalue(eres);
1479 free_evalue_refs(&factor);
1480 Polyhedron_Free(P);
1481 if (CT)
1482 Matrix_Free(CT);
1483 if (PP)
1484 Param_Polyhedron_Free(PP);
1486 return eres;
1488 for (r = 0; r < P->NbRays; ++r)
1489 if (value_zero_p(P->Ray[r][0]) ||
1490 value_zero_p(P->Ray[r][P->Dimension+1])) {
1491 int i;
1492 for (i = P->Dimension - nparam; i < P->Dimension; ++i)
1493 if (value_notzero_p(P->Ray[r][i+1]))
1494 break;
1495 if (i >= P->Dimension)
1496 break;
1498 if (r < P->NbRays)
1499 goto constant;
1501 if (P->NbEq != 0) {
1502 Matrix *f;
1503 P = remove_equalities_p(P, P->Dimension-nparam, &f);
1504 mask(f, &factor);
1505 Matrix_Free(f);
1507 if (P->Dimension == nparam) {
1508 CEq = P;
1509 P = Universe_Polyhedron(0);
1510 goto constant;
1513 Polyhedron *Q = ParamPolyhedron_Reduce(P, P->Dimension-nparam, &factor);
1514 if (Q) {
1515 Polyhedron_Free(P);
1516 if (Q->Dimension == nparam) {
1517 CEq = Q;
1518 P = Universe_Polyhedron(0);
1519 goto constant;
1521 P = Q;
1523 Polyhedron *oldP = P;
1524 PP = Polyhedron2Param_SimplifiedDomain(&P,C,MaxRays,&CEq,&CT);
1525 if (P != oldP)
1526 Polyhedron_Free(oldP);
1528 if (isIdentity(CT)) {
1529 Matrix_Free(CT);
1530 CT = NULL;
1531 } else {
1532 assert(CT->NbRows != CT->NbColumns);
1533 if (CT->NbRows == 1) // no more parameters
1534 goto constant;
1535 nparam = CT->NbRows - 1;
1538 unsigned dim = P->Dimension - nparam;
1539 Polyhedron ** vcone = new Polyhedron_p[PP->nbV];
1540 int * npos = new int[PP->nbV];
1541 int * nneg = new int[PP->nbV];
1542 vec_ZZ sign;
1544 int i;
1545 for (i = 0, V = PP->V; V; ++i, V = V->next) {
1546 Polyhedron *C = supporting_cone_p(P, V);
1547 decompose(C, &vcone[i], &npos[i], &nneg[i], MaxRays);
1550 Vector *c = Vector_Alloc(dim+2);
1552 int nd;
1553 for (nd = 0, D=PP->D; D; ++nd, D=D->next);
1554 struct section { Polyhedron *D; evalue E; };
1555 section *s = new section[nd];
1556 Polyhedron **fVD = new Polyhedron_p[nd];
1558 for(nd = 0, D=PP->D; D; D=next) {
1559 next = D->next;
1561 Polyhedron *rVD = reduce_domain(D->Domain, CT, CEq,
1562 fVD, nd, MaxRays);
1563 if (!rVD)
1564 continue;
1566 pVD = CT ? DomainImage(rVD,CT,MaxRays) : rVD;
1568 int ncone = 0;
1569 sign.SetLength(ncone);
1570 FORALL_PVertex_in_ParamPolyhedron(V,D,PP) // _i is internal counter
1571 ncone += npos[_i] + nneg[_i];
1572 sign.SetLength(ncone);
1573 for (int k = 0; k < npos[_i]; ++k)
1574 sign[ncone-nneg[_i]-k-1] = 1;
1575 for (int k = 0; k < nneg[_i]; ++k)
1576 sign[ncone-k-1] = -1;
1577 END_FORALL_PVertex_in_ParamPolyhedron;
1579 mat_ZZ rays;
1580 rays.SetDims(ncone * dim, dim);
1581 r = 0;
1582 FORALL_PVertex_in_ParamPolyhedron(V,D,PP) // _i is internal counter
1583 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1584 assert(i->NbRays-1 == dim);
1585 add_rays(rays, i, &r);
1587 END_FORALL_PVertex_in_ParamPolyhedron;
1588 vec_ZZ lambda;
1589 nonorthog(rays, lambda);
1591 mat_ZZ den;
1592 den.SetDims(ncone,dim);
1593 term_info *num = new term_info[ncone];
1595 int f = 0;
1596 FORALL_PVertex_in_ParamPolyhedron(V,D,PP)
1597 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1598 lattice_point(V, i, lambda, &num[f], pVD);
1599 normalize(i, lambda, sign[f], num[f].constant, den[f]);
1600 ++f;
1602 END_FORALL_PVertex_in_ParamPolyhedron;
1603 ZZ min = num[0].constant;
1604 for (int j = 1; j < ncone; ++j)
1605 if (num[j].constant < min)
1606 min = num[j].constant;
1607 for (int j = 0; j < ncone; ++j)
1608 num[j].constant -= min;
1609 f = 0;
1610 value_init(s[nd].E.d);
1611 evalue_set_si(&s[nd].E, 0, 1);
1612 mpq_t count;
1613 mpq_init(count);
1614 FORALL_PVertex_in_ParamPolyhedron(V,D,PP)
1615 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1616 dpoly n(dim, den[f][0], 1);
1617 for (int k = 1; k < dim; ++k) {
1618 dpoly fact(dim, den[f][k], 1);
1619 n *= fact;
1621 if (num[f].E != NULL) {
1622 ZZ one(INIT_VAL, 1);
1623 dpoly_n d(dim, num[f].constant, one);
1624 d.div(n, c, sign[f]);
1625 evalue EV;
1626 multi_polynom(c, num[f].E, &EV);
1627 eadd(&EV , &s[nd].E);
1628 free_evalue_refs(&EV);
1629 free_evalue_refs(num[f].E);
1630 delete num[f].E;
1631 } else if (num[f].pos != -1) {
1632 dpoly_n d(dim, num[f].constant, num[f].coeff);
1633 d.div(n, c, sign[f]);
1634 evalue EV;
1635 uni_polynom(num[f].pos, c, &EV);
1636 eadd(&EV , &s[nd].E);
1637 free_evalue_refs(&EV);
1638 } else {
1639 mpq_set_si(count, 0, 1);
1640 dpoly d(dim, num[f].constant);
1641 d.div(n, count, sign[f]);
1642 evalue EV;
1643 value_init(EV.d);
1644 evalue_set(&EV, &count[0]._mp_num, &count[0]._mp_den);
1645 eadd(&EV , &s[nd].E);
1646 free_evalue_refs(&EV);
1648 ++f;
1650 END_FORALL_PVertex_in_ParamPolyhedron;
1652 mpq_clear(count);
1653 delete [] num;
1655 if (CT)
1656 addeliminatedparams_evalue(&s[nd].E, CT);
1657 s[nd].D = rVD;
1658 ++nd;
1659 if (rVD != pVD)
1660 Domain_Free(pVD);
1663 if (nd == 0)
1664 evalue_set_si(eres, 0, 1);
1665 else {
1666 eres->x.p = new_enode(partition, 2*nd, C->Dimension);
1667 for (int j = 0; j < nd; ++j) {
1668 EVALUE_SET_DOMAIN(eres->x.p->arr[2*j], s[j].D);
1669 value_clear(eres->x.p->arr[2*j+1].d);
1670 eres->x.p->arr[2*j+1] = s[j].E;
1671 Domain_Free(fVD[j]);
1674 delete [] s;
1675 delete [] fVD;
1677 Vector_Free(c);
1679 for (int j = 0; j < PP->nbV; ++j)
1680 Domain_Free(vcone[j]);
1681 delete [] vcone;
1682 delete [] npos;
1683 delete [] nneg;
1685 if (CEq)
1686 Polyhedron_Free(CEq);
1688 goto out;
1691 Enumeration* barvinok_enumerate(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1693 evalue *EP = barvinok_enumerate_ev(P, C, MaxRays);
1695 return partition2enumeration(EP);
1698 static void SwapColumns(Value **V, int n, int i, int j)
1700 for (int r = 0; r < n; ++r)
1701 value_swap(V[r][i], V[r][j]);
1704 static void SwapColumns(Polyhedron *P, int i, int j)
1706 SwapColumns(P->Constraint, P->NbConstraints, i, j);
1707 SwapColumns(P->Ray, P->NbRays, i, j);
1710 static void negative_test_constraint(Value *l, Value *u, Value *c, int pos,
1711 int len, Value *v)
1713 value_oppose(*v, u[pos+1]);
1714 Vector_Combine(l+1, u+1, c+1, *v, l[pos+1], len-1);
1715 value_multiply(*v, *v, l[pos+1]);
1716 value_substract(c[len-1], c[len-1], *v);
1717 value_set_si(*v, -1);
1718 Vector_Scale(c+1, c+1, *v, len-1);
1719 value_decrement(c[len-1], c[len-1]);
1720 ConstraintSimplify(c, c, len, v);
1723 static void oppose_constraint(Value *c, int len, Value *v)
1725 value_set_si(*v, -1);
1726 Vector_Scale(c+1, c+1, *v, len-1);
1727 value_decrement(c[len-1], c[len-1]);
1730 static bool SplitOnConstraint(Polyhedron *P, int i, int l, int u,
1731 int nvar, int len, int exist, int MaxRays,
1732 Vector *row, Value& f, bool independent,
1733 Polyhedron **pos, Polyhedron **neg)
1735 negative_test_constraint(P->Constraint[l], P->Constraint[u],
1736 row->p, nvar+i, len, &f);
1737 *neg = AddConstraints(row->p, 1, P, MaxRays);
1739 /* We found an independent, but useless constraint
1740 * Maybe we should detect this earlier and not
1741 * mark the variable as INDEPENDENT
1743 if (emptyQ((*neg))) {
1744 Polyhedron_Free(*neg);
1745 return false;
1748 oppose_constraint(row->p, len, &f);
1749 *pos = AddConstraints(row->p, 1, P, MaxRays);
1751 if (emptyQ((*pos))) {
1752 Polyhedron_Free(*neg);
1753 Polyhedron_Free(*pos);
1754 return false;
1757 return true;
1761 * unimodularly transform P such that constraint r is transformed
1762 * into a constraint that involves only a single (the first)
1763 * existential variable
1766 static Polyhedron *rotate_along(Polyhedron *P, int r, int nvar, int exist,
1767 unsigned MaxRays)
1769 Value g;
1770 value_init(g);
1772 Vector *row = Vector_Alloc(exist);
1773 Vector_Copy(P->Constraint[r]+1+nvar, row->p, exist);
1774 Vector_Gcd(row->p, exist, &g);
1775 if (value_notone_p(g))
1776 Vector_AntiScale(row->p, row->p, g, exist);
1777 value_clear(g);
1779 Matrix *M = unimodular_complete(row);
1780 Matrix *M2 = Matrix_Alloc(P->Dimension+1, P->Dimension+1);
1781 for (r = 0; r < nvar; ++r)
1782 value_set_si(M2->p[r][r], 1);
1783 for ( ; r < nvar+exist; ++r)
1784 Vector_Copy(M->p[r-nvar], M2->p[r]+nvar, exist);
1785 for ( ; r < P->Dimension+1; ++r)
1786 value_set_si(M2->p[r][r], 1);
1787 Polyhedron *T = Polyhedron_Image(P, M2, MaxRays);
1789 Matrix_Free(M2);
1790 Matrix_Free(M);
1791 Vector_Free(row);
1793 return T;
1796 static bool SplitOnVar(Polyhedron *P, int i,
1797 int nvar, int len, int exist, int MaxRays,
1798 Vector *row, Value& f, bool independent,
1799 Polyhedron **pos, Polyhedron **neg)
1801 int j;
1803 for (int l = P->NbEq; l < P->NbConstraints; ++l) {
1804 if (value_negz_p(P->Constraint[l][nvar+i+1]))
1805 continue;
1807 if (independent) {
1808 for (j = 0; j < exist; ++j)
1809 if (j != i && value_notzero_p(P->Constraint[l][nvar+j+1]))
1810 break;
1811 if (j < exist)
1812 continue;
1815 for (int u = P->NbEq; u < P->NbConstraints; ++u) {
1816 if (value_posz_p(P->Constraint[u][nvar+i+1]))
1817 continue;
1819 if (independent) {
1820 for (j = 0; j < exist; ++j)
1821 if (j != i && value_notzero_p(P->Constraint[u][nvar+j+1]))
1822 break;
1823 if (j < exist)
1824 continue;
1827 if (SplitOnConstraint(P, i, l, u,
1828 nvar, len, exist, MaxRays,
1829 row, f, independent,
1830 pos, neg)) {
1831 if (independent) {
1832 if (i != 0)
1833 SwapColumns(*neg, nvar+1, nvar+1+i);
1835 return true;
1840 return false;
1843 static bool double_bound_pair(Polyhedron *P, int nvar, int exist,
1844 int i, int l1, int l2,
1845 Polyhedron **pos, Polyhedron **neg)
1847 Value f;
1848 value_init(f);
1849 Vector *row = Vector_Alloc(P->Dimension+2);
1850 value_set_si(row->p[0], 1);
1851 value_oppose(f, P->Constraint[l1][nvar+i+1]);
1852 Vector_Combine(P->Constraint[l1]+1, P->Constraint[l2]+1,
1853 row->p+1,
1854 P->Constraint[l2][nvar+i+1], f,
1855 P->Dimension+1);
1856 ConstraintSimplify(row->p, row->p, P->Dimension+2, &f);
1857 *pos = AddConstraints(row->p, 1, P, 0);
1858 value_set_si(f, -1);
1859 Vector_Scale(row->p+1, row->p+1, f, P->Dimension+1);
1860 value_decrement(row->p[P->Dimension+1], row->p[P->Dimension+1]);
1861 *neg = AddConstraints(row->p, 1, P, 0);
1862 Vector_Free(row);
1863 value_clear(f);
1865 return !emptyQ((*pos)) && !emptyQ((*neg));
1868 static bool double_bound(Polyhedron *P, int nvar, int exist,
1869 Polyhedron **pos, Polyhedron **neg)
1871 for (int i = 0; i < exist; ++i) {
1872 int l1, l2;
1873 for (l1 = P->NbEq; l1 < P->NbConstraints; ++l1) {
1874 if (value_negz_p(P->Constraint[l1][nvar+i+1]))
1875 continue;
1876 for (l2 = l1 + 1; l2 < P->NbConstraints; ++l2) {
1877 if (value_negz_p(P->Constraint[l2][nvar+i+1]))
1878 continue;
1879 if (double_bound_pair(P, nvar, exist, i, l1, l2, pos, neg))
1880 return true;
1883 for (l1 = P->NbEq; l1 < P->NbConstraints; ++l1) {
1884 if (value_posz_p(P->Constraint[l1][nvar+i+1]))
1885 continue;
1886 if (l1 < P->NbConstraints)
1887 for (l2 = l1 + 1; l2 < P->NbConstraints; ++l2) {
1888 if (value_posz_p(P->Constraint[l2][nvar+i+1]))
1889 continue;
1890 if (double_bound_pair(P, nvar, exist, i, l1, l2, pos, neg))
1891 return true;
1894 return false;
1896 return false;
1899 enum constraint {
1900 ALL_POS = 1 << 0,
1901 ONE_NEG = 1 << 1,
1902 INDEPENDENT = 1 << 2
1905 static evalue* enumerate_or(Polyhedron *D,
1906 unsigned exist, unsigned nparam, unsigned MaxRays)
1908 #ifdef DEBUG_ER
1909 fprintf(stderr, "\nER: Or\n");
1910 #endif /* DEBUG_ER */
1912 Polyhedron *N = D->next;
1913 D->next = 0;
1914 evalue *EP =
1915 barvinok_enumerate_e(D, exist, nparam, MaxRays);
1916 Polyhedron_Free(D);
1918 for (D = N; D; D = N) {
1919 N = D->next;
1920 D->next = 0;
1922 evalue *EN =
1923 barvinok_enumerate_e(D, exist, nparam, MaxRays);
1925 eor(EN, EP);
1926 free_evalue_refs(EN);
1927 free(EN);
1928 Polyhedron_Free(D);
1931 reduce_evalue(EP);
1933 return EP;
1936 static evalue* enumerate_sum(Polyhedron *P,
1937 unsigned exist, unsigned nparam, unsigned MaxRays)
1939 int nvar = P->Dimension - exist - nparam;
1940 int toswap = nvar < exist ? nvar : exist;
1941 for (int i = 0; i < toswap; ++i)
1942 SwapColumns(P, 1 + i, nvar+exist - i);
1943 nparam += nvar;
1945 #ifdef DEBUG_ER
1946 fprintf(stderr, "\nER: Sum\n");
1947 #endif /* DEBUG_ER */
1949 evalue *EP = barvinok_enumerate_e(P, exist, nparam, MaxRays);
1951 for (int i = 0; i < /* nvar */ nparam; ++i) {
1952 Matrix *C = Matrix_Alloc(1, 1 + nparam + 1);
1953 value_set_si(C->p[0][0], 1);
1954 evalue split;
1955 value_init(split.d);
1956 value_set_si(split.d, 0);
1957 split.x.p = new_enode(partition, 4, nparam);
1958 value_set_si(C->p[0][1+i], 1);
1959 Matrix *C2 = Matrix_Copy(C);
1960 EVALUE_SET_DOMAIN(split.x.p->arr[0],
1961 Constraints2Polyhedron(C2, MaxRays));
1962 Matrix_Free(C2);
1963 evalue_set_si(&split.x.p->arr[1], 1, 1);
1964 value_set_si(C->p[0][1+i], -1);
1965 value_set_si(C->p[0][1+nparam], -1);
1966 EVALUE_SET_DOMAIN(split.x.p->arr[2],
1967 Constraints2Polyhedron(C, MaxRays));
1968 evalue_set_si(&split.x.p->arr[3], 1, 1);
1969 emul(&split, EP);
1970 free_evalue_refs(&split);
1971 Matrix_Free(C);
1973 reduce_evalue(EP);
1974 evalue_range_reduction(EP);
1976 evalue_frac2floor(EP);
1978 evalue *sum = esum(EP, nvar);
1980 free_evalue_refs(EP);
1981 free(EP);
1982 EP = sum;
1984 evalue_range_reduction(EP);
1986 return EP;
1989 static evalue* split_sure(Polyhedron *P, Polyhedron *S,
1990 unsigned exist, unsigned nparam, unsigned MaxRays)
1992 int nvar = P->Dimension - exist - nparam;
1994 Matrix *M = Matrix_Alloc(exist, S->Dimension+2);
1995 for (int i = 0; i < exist; ++i)
1996 value_set_si(M->p[i][nvar+i+1], 1);
1997 Polyhedron *O = S;
1998 S = DomainAddRays(S, M, MaxRays);
1999 Polyhedron_Free(O);
2000 Polyhedron *F = DomainAddRays(P, M, MaxRays);
2001 Polyhedron *D = DomainDifference(F, S, MaxRays);
2002 O = D;
2003 D = Disjoint_Domain(D, 0, MaxRays);
2004 Polyhedron_Free(F);
2005 Domain_Free(O);
2006 Matrix_Free(M);
2008 M = Matrix_Alloc(P->Dimension+1-exist, P->Dimension+1);
2009 for (int j = 0; j < nvar; ++j)
2010 value_set_si(M->p[j][j], 1);
2011 for (int j = 0; j < nparam+1; ++j)
2012 value_set_si(M->p[nvar+j][nvar+exist+j], 1);
2013 Polyhedron *T = Polyhedron_Image(S, M, MaxRays);
2014 evalue *EP = barvinok_enumerate_e(T, 0, nparam, MaxRays);
2015 Polyhedron_Free(S);
2016 Polyhedron_Free(T);
2017 Matrix_Free(M);
2019 for (Polyhedron *Q = D; Q; Q = Q->next) {
2020 Polyhedron *N = Q->next;
2021 Q->next = 0;
2022 T = DomainIntersection(P, Q, MaxRays);
2023 evalue *E = barvinok_enumerate_e(T, exist, nparam, MaxRays);
2024 eadd(E, EP);
2025 free_evalue_refs(E);
2026 free(E);
2027 Polyhedron_Free(T);
2028 Q->next = N;
2030 Domain_Free(D);
2031 return EP;
2034 static evalue* enumerate_sure(Polyhedron *P,
2035 unsigned exist, unsigned nparam, unsigned MaxRays)
2037 int i;
2038 Polyhedron *S = P;
2039 int nvar = P->Dimension - exist - nparam;
2040 Value lcm;
2041 Value f;
2042 value_init(lcm);
2043 value_init(f);
2045 for (i = 0; i < exist; ++i) {
2046 Matrix *M = Matrix_Alloc(S->NbConstraints, S->Dimension+2);
2047 int c = 0;
2048 value_set_si(lcm, 1);
2049 for (int j = 0; j < S->NbConstraints; ++j) {
2050 if (value_negz_p(S->Constraint[j][1+nvar+i]))
2051 continue;
2052 if (value_one_p(S->Constraint[j][1+nvar+i]))
2053 continue;
2054 value_lcm(lcm, S->Constraint[j][1+nvar+i], &lcm);
2057 for (int j = 0; j < S->NbConstraints; ++j) {
2058 if (value_negz_p(S->Constraint[j][1+nvar+i]))
2059 continue;
2060 if (value_one_p(S->Constraint[j][1+nvar+i]))
2061 continue;
2062 value_division(f, lcm, S->Constraint[j][1+nvar+i]);
2063 Vector_Scale(S->Constraint[j], M->p[c], f, S->Dimension+2);
2064 value_substract(M->p[c][S->Dimension+1],
2065 M->p[c][S->Dimension+1],
2066 lcm);
2067 value_increment(M->p[c][S->Dimension+1],
2068 M->p[c][S->Dimension+1]);
2069 ++c;
2071 Polyhedron *O = S;
2072 S = AddConstraints(M->p[0], c, S, MaxRays);
2073 if (O != P)
2074 Polyhedron_Free(O);
2075 Matrix_Free(M);
2076 if (emptyQ(S)) {
2077 Polyhedron_Free(S);
2078 value_clear(lcm);
2079 value_clear(f);
2080 return 0;
2083 value_clear(lcm);
2084 value_clear(f);
2086 #ifdef DEBUG_ER
2087 fprintf(stderr, "\nER: Sure\n");
2088 #endif /* DEBUG_ER */
2090 return split_sure(P, S, exist, nparam, MaxRays);
2093 static evalue* enumerate_sure2(Polyhedron *P,
2094 unsigned exist, unsigned nparam, unsigned MaxRays)
2096 int nvar = P->Dimension - exist - nparam;
2097 int r;
2098 for (r = 0; r < P->NbRays; ++r)
2099 if (value_one_p(P->Ray[r][0]) &&
2100 value_one_p(P->Ray[r][P->Dimension+1]))
2101 break;
2103 if (r >= P->NbRays)
2104 return 0;
2106 Matrix *M = Matrix_Alloc(nvar + 1 + nparam, P->Dimension+2);
2107 for (int i = 0; i < nvar; ++i)
2108 value_set_si(M->p[i][1+i], 1);
2109 for (int i = 0; i < nparam; ++i)
2110 value_set_si(M->p[i+nvar][1+nvar+exist+i], 1);
2111 Vector_Copy(P->Ray[r]+1+nvar, M->p[nvar+nparam]+1+nvar, exist);
2112 value_set_si(M->p[nvar+nparam][0], 1);
2113 value_set_si(M->p[nvar+nparam][P->Dimension+1], 1);
2114 Polyhedron * F = Rays2Polyhedron(M, MaxRays);
2115 Matrix_Free(M);
2117 Polyhedron *I = DomainIntersection(F, P, MaxRays);
2118 Polyhedron_Free(F);
2120 #ifdef DEBUG_ER
2121 fprintf(stderr, "\nER: Sure2\n");
2122 #endif /* DEBUG_ER */
2124 return split_sure(P, I, exist, nparam, MaxRays);
2127 static evalue* enumerate_cyclic(Polyhedron *P,
2128 unsigned exist, unsigned nparam,
2129 evalue * EP, int r, int p, unsigned MaxRays)
2131 int nvar = P->Dimension - exist - nparam;
2133 /* If EP in its fractional maps only contains references
2134 * to the remainder parameter with appropriate coefficients
2135 * then we could in principle avoid adding existentially
2136 * quantified variables to the validity domains.
2137 * We'd have to replace the remainder by m { p/m }
2138 * and multiply with an appropriate factor that is one
2139 * only in the appropriate range.
2140 * This last multiplication can be avoided if EP
2141 * has a single validity domain with no (further)
2142 * constraints on the remainder parameter
2145 Matrix *CT = Matrix_Alloc(nparam+1, nparam+3);
2146 Matrix *M = Matrix_Alloc(1, 1+nparam+3);
2147 for (int j = 0; j < nparam; ++j)
2148 if (j != p)
2149 value_set_si(CT->p[j][j], 1);
2150 value_set_si(CT->p[p][nparam+1], 1);
2151 value_set_si(CT->p[nparam][nparam+2], 1);
2152 value_set_si(M->p[0][1+p], -1);
2153 value_absolute(M->p[0][1+nparam], P->Ray[0][1+nvar+exist+p]);
2154 value_set_si(M->p[0][1+nparam+1], 1);
2155 Polyhedron *CEq = Constraints2Polyhedron(M, 1);
2156 Matrix_Free(M);
2157 addeliminatedparams_enum(EP, CT, CEq, MaxRays, nparam);
2158 Polyhedron_Free(CEq);
2159 Matrix_Free(CT);
2161 return EP;
2164 static void enumerate_vd_add_ray(evalue *EP, Matrix *Rays, unsigned MaxRays)
2166 if (value_notzero_p(EP->d))
2167 return;
2169 assert(EP->x.p->type == partition);
2170 assert(EP->x.p->pos == EVALUE_DOMAIN(EP->x.p->arr[0])->Dimension);
2171 for (int i = 0; i < EP->x.p->size/2; ++i) {
2172 Polyhedron *D = EVALUE_DOMAIN(EP->x.p->arr[2*i]);
2173 Polyhedron *N = DomainAddRays(D, Rays, MaxRays);
2174 EVALUE_SET_DOMAIN(EP->x.p->arr[2*i], N);
2175 Domain_Free(D);
2179 static evalue* enumerate_line(Polyhedron *P,
2180 unsigned exist, unsigned nparam, unsigned MaxRays)
2182 if (P->NbBid == 0)
2183 return 0;
2185 #ifdef DEBUG_ER
2186 fprintf(stderr, "\nER: Line\n");
2187 #endif /* DEBUG_ER */
2189 int nvar = P->Dimension - exist - nparam;
2190 int i, j;
2191 for (i = 0; i < nparam; ++i)
2192 if (value_notzero_p(P->Ray[0][1+nvar+exist+i]))
2193 break;
2194 assert(i < nparam);
2195 for (j = i+1; j < nparam; ++j)
2196 if (value_notzero_p(P->Ray[0][1+nvar+exist+i]))
2197 break;
2198 assert(j >= nparam); // for now
2200 Matrix *M = Matrix_Alloc(2, P->Dimension+2);
2201 value_set_si(M->p[0][0], 1);
2202 value_set_si(M->p[0][1+nvar+exist+i], 1);
2203 value_set_si(M->p[1][0], 1);
2204 value_set_si(M->p[1][1+nvar+exist+i], -1);
2205 value_absolute(M->p[1][1+P->Dimension], P->Ray[0][1+nvar+exist+i]);
2206 value_decrement(M->p[1][1+P->Dimension], M->p[1][1+P->Dimension]);
2207 Polyhedron *S = AddConstraints(M->p[0], 2, P, MaxRays);
2208 evalue *EP = barvinok_enumerate_e(S, exist, nparam, MaxRays);
2209 Polyhedron_Free(S);
2210 Matrix_Free(M);
2212 return enumerate_cyclic(P, exist, nparam, EP, 0, i, MaxRays);
2215 static int single_param_pos(Polyhedron*P, unsigned exist, unsigned nparam,
2216 int r)
2218 int nvar = P->Dimension - exist - nparam;
2219 if (First_Non_Zero(P->Ray[r]+1, nvar) != -1)
2220 return -1;
2221 int i = First_Non_Zero(P->Ray[r]+1+nvar+exist, nparam);
2222 if (i == -1)
2223 return -1;
2224 if (First_Non_Zero(P->Ray[r]+1+nvar+exist+1, nparam-i-1) != -1)
2225 return -1;
2226 return i;
2229 static evalue* enumerate_remove_ray(Polyhedron *P, int r,
2230 unsigned exist, unsigned nparam, unsigned MaxRays)
2232 #ifdef DEBUG_ER
2233 fprintf(stderr, "\nER: RedundantRay\n");
2234 #endif /* DEBUG_ER */
2236 Value one;
2237 value_init(one);
2238 value_set_si(one, 1);
2239 int len = P->NbRays-1;
2240 Matrix *M = Matrix_Alloc(2 * len, P->Dimension+2);
2241 Vector_Copy(P->Ray[0], M->p[0], r * (P->Dimension+2));
2242 Vector_Copy(P->Ray[r+1], M->p[r], (len-r) * (P->Dimension+2));
2243 for (int j = 0; j < P->NbRays; ++j) {
2244 if (j == r)
2245 continue;
2246 Vector_Combine(P->Ray[j], P->Ray[r], M->p[len+j-(j>r)],
2247 one, P->Ray[j][P->Dimension+1], P->Dimension+2);
2250 P = Rays2Polyhedron(M, MaxRays);
2251 Matrix_Free(M);
2252 evalue *EP = barvinok_enumerate_e(P, exist, nparam, MaxRays);
2253 Polyhedron_Free(P);
2254 value_clear(one);
2256 return EP;
2259 static evalue* enumerate_redundant_ray(Polyhedron *P,
2260 unsigned exist, unsigned nparam, unsigned MaxRays)
2262 assert(P->NbBid == 0);
2263 int nvar = P->Dimension - exist - nparam;
2264 Value m;
2265 value_init(m);
2267 for (int r = 0; r < P->NbRays; ++r) {
2268 if (value_notzero_p(P->Ray[r][P->Dimension+1]))
2269 continue;
2270 int i1 = single_param_pos(P, exist, nparam, r);
2271 if (i1 == -1)
2272 continue;
2273 for (int r2 = r+1; r2 < P->NbRays; ++r2) {
2274 if (value_notzero_p(P->Ray[r2][P->Dimension+1]))
2275 continue;
2276 int i2 = single_param_pos(P, exist, nparam, r2);
2277 if (i2 == -1)
2278 continue;
2279 if (i1 != i2)
2280 continue;
2282 value_division(m, P->Ray[r][1+nvar+exist+i1],
2283 P->Ray[r2][1+nvar+exist+i1]);
2284 value_multiply(m, m, P->Ray[r2][1+nvar+exist+i1]);
2285 /* r2 divides r => r redundant */
2286 if (value_eq(m, P->Ray[r][1+nvar+exist+i1])) {
2287 value_clear(m);
2288 return enumerate_remove_ray(P, r, exist, nparam, MaxRays);
2291 value_division(m, P->Ray[r2][1+nvar+exist+i1],
2292 P->Ray[r][1+nvar+exist+i1]);
2293 value_multiply(m, m, P->Ray[r][1+nvar+exist+i1]);
2294 /* r divides r2 => r2 redundant */
2295 if (value_eq(m, P->Ray[r2][1+nvar+exist+i1])) {
2296 value_clear(m);
2297 return enumerate_remove_ray(P, r2, exist, nparam, MaxRays);
2301 value_clear(m);
2302 return 0;
2305 static Polyhedron *upper_bound(Polyhedron *P,
2306 int pos, Value *max, Polyhedron **R)
2308 Value v;
2309 int r;
2310 value_init(v);
2312 *R = 0;
2313 Polyhedron *N;
2314 Polyhedron *B = 0;
2315 for (Polyhedron *Q = P; Q; Q = N) {
2316 N = Q->next;
2317 for (r = 0; r < P->NbRays; ++r) {
2318 if (value_zero_p(P->Ray[r][P->Dimension+1]) &&
2319 value_pos_p(P->Ray[r][1+pos]))
2320 break;
2322 if (r < P->NbRays) {
2323 Q->next = *R;
2324 *R = Q;
2325 continue;
2326 } else {
2327 Q->next = B;
2328 B = Q;
2330 for (r = 0; r < P->NbRays; ++r) {
2331 if (value_zero_p(P->Ray[r][P->Dimension+1]))
2332 continue;
2333 mpz_fdiv_q(v, P->Ray[r][1+pos], P->Ray[r][1+P->Dimension]);
2334 if ((!Q->next && r == 0) || value_gt(v, *max))
2335 value_assign(*max, v);
2338 value_clear(v);
2339 return B;
2342 static evalue* enumerate_ray(Polyhedron *P,
2343 unsigned exist, unsigned nparam, unsigned MaxRays)
2345 assert(P->NbBid == 0);
2346 int nvar = P->Dimension - exist - nparam;
2348 int r;
2349 for (r = 0; r < P->NbRays; ++r)
2350 if (value_zero_p(P->Ray[r][P->Dimension+1]))
2351 break;
2352 if (r >= P->NbRays)
2353 return 0;
2355 int r2;
2356 for (r2 = r+1; r2 < P->NbRays; ++r2)
2357 if (value_zero_p(P->Ray[r2][P->Dimension+1]))
2358 break;
2359 if (r2 < P->NbRays) {
2360 if (nvar > 0)
2361 return enumerate_sum(P, exist, nparam, MaxRays);
2364 #ifdef DEBUG_ER
2365 fprintf(stderr, "\nER: Ray\n");
2366 #endif /* DEBUG_ER */
2368 Value m;
2369 Value one;
2370 value_init(m);
2371 value_init(one);
2372 value_set_si(one, 1);
2373 int i = single_param_pos(P, exist, nparam, r);
2374 assert(i != -1); // for now;
2376 Matrix *M = Matrix_Alloc(P->NbRays, P->Dimension+2);
2377 for (int j = 0; j < P->NbRays; ++j) {
2378 Vector_Combine(P->Ray[j], P->Ray[r], M->p[j],
2379 one, P->Ray[j][P->Dimension+1], P->Dimension+2);
2381 Polyhedron *S = Rays2Polyhedron(M, MaxRays);
2382 Matrix_Free(M);
2383 Polyhedron *D = DomainDifference(P, S, MaxRays);
2384 Polyhedron_Free(S);
2385 // Polyhedron_Print(stderr, P_VALUE_FMT, D);
2386 assert(value_pos_p(P->Ray[r][1+nvar+exist+i])); // for now
2387 Polyhedron *R;
2388 D = upper_bound(D, nvar+exist+i, &m, &R);
2389 assert(D);
2390 Domain_Free(D);
2392 M = Matrix_Alloc(2, P->Dimension+2);
2393 value_set_si(M->p[0][0], 1);
2394 value_set_si(M->p[1][0], 1);
2395 value_set_si(M->p[0][1+nvar+exist+i], -1);
2396 value_set_si(M->p[1][1+nvar+exist+i], 1);
2397 value_assign(M->p[0][1+P->Dimension], m);
2398 value_oppose(M->p[1][1+P->Dimension], m);
2399 value_addto(M->p[1][1+P->Dimension], M->p[1][1+P->Dimension],
2400 P->Ray[r][1+nvar+exist+i]);
2401 value_decrement(M->p[1][1+P->Dimension], M->p[1][1+P->Dimension]);
2402 // Matrix_Print(stderr, P_VALUE_FMT, M);
2403 D = AddConstraints(M->p[0], 2, P, MaxRays);
2404 // Polyhedron_Print(stderr, P_VALUE_FMT, D);
2405 value_substract(M->p[0][1+P->Dimension], M->p[0][1+P->Dimension],
2406 P->Ray[r][1+nvar+exist+i]);
2407 // Matrix_Print(stderr, P_VALUE_FMT, M);
2408 S = AddConstraints(M->p[0], 1, P, MaxRays);
2409 // Polyhedron_Print(stderr, P_VALUE_FMT, S);
2410 Matrix_Free(M);
2412 evalue *EP = barvinok_enumerate_e(D, exist, nparam, MaxRays);
2413 Polyhedron_Free(D);
2414 value_clear(one);
2415 value_clear(m);
2417 if (value_notone_p(P->Ray[r][1+nvar+exist+i]))
2418 EP = enumerate_cyclic(P, exist, nparam, EP, r, i, MaxRays);
2419 else {
2420 M = Matrix_Alloc(1, nparam+2);
2421 value_set_si(M->p[0][0], 1);
2422 value_set_si(M->p[0][1+i], 1);
2423 enumerate_vd_add_ray(EP, M, MaxRays);
2424 Matrix_Free(M);
2427 if (!emptyQ(S)) {
2428 evalue *E = barvinok_enumerate_e(S, exist, nparam, MaxRays);
2429 eadd(E, EP);
2430 free_evalue_refs(E);
2431 free(E);
2433 Polyhedron_Free(S);
2435 if (R) {
2436 assert(nvar == 0);
2437 evalue *ER = enumerate_or(R, exist, nparam, MaxRays);
2438 eor(ER, EP);
2439 free_evalue_refs(ER);
2440 free(ER);
2443 return EP;
2446 static evalue* new_zero_ep()
2448 evalue *EP;
2449 ALLOC(evalue, EP);
2450 value_init(EP->d);
2451 evalue_set_si(EP, 0, 1);
2452 return EP;
2455 static evalue* enumerate_vd(Polyhedron **PA,
2456 unsigned exist, unsigned nparam, unsigned MaxRays)
2458 Polyhedron *P = *PA;
2459 int nvar = P->Dimension - exist - nparam;
2460 Param_Polyhedron *PP = NULL;
2461 Polyhedron *C = Universe_Polyhedron(nparam);
2462 Polyhedron *CEq;
2463 Matrix *CT;
2464 Polyhedron *PR = P;
2465 PP = Polyhedron2Param_SimplifiedDomain(&PR,C,MaxRays,&CEq,&CT);
2466 Polyhedron_Free(C);
2468 int nd;
2469 Param_Domain *D, *last;
2470 Value c;
2471 value_init(c);
2472 for (nd = 0, D=PP->D; D; D=D->next, ++nd)
2475 Polyhedron **VD = new Polyhedron_p[nd];
2476 Polyhedron **fVD = new Polyhedron_p[nd];
2477 for(nd = 0, D=PP->D; D; D=D->next) {
2478 Polyhedron *rVD = reduce_domain(D->Domain, CT, CEq,
2479 fVD, nd, MaxRays);
2480 if (!rVD)
2481 continue;
2483 VD[nd++] = rVD;
2484 last = D;
2487 evalue *EP = 0;
2489 if (nd == 0)
2490 EP = new_zero_ep();
2492 /* This doesn't seem to have any effect */
2493 if (nd == 1) {
2494 Polyhedron *CA = align_context(VD[0], P->Dimension, MaxRays);
2495 Polyhedron *O = P;
2496 P = DomainIntersection(P, CA, MaxRays);
2497 if (O != *PA)
2498 Polyhedron_Free(O);
2499 Polyhedron_Free(CA);
2500 if (emptyQ(P))
2501 EP = new_zero_ep();
2504 if (!EP && CT->NbColumns != CT->NbRows) {
2505 Polyhedron *CEqr = DomainImage(CEq, CT, MaxRays);
2506 Polyhedron *CA = align_context(CEqr, PR->Dimension, MaxRays);
2507 Polyhedron *I = DomainIntersection(PR, CA, MaxRays);
2508 Polyhedron_Free(CEqr);
2509 Polyhedron_Free(CA);
2510 #ifdef DEBUG_ER
2511 fprintf(stderr, "\nER: Eliminate\n");
2512 #endif /* DEBUG_ER */
2513 nparam -= CT->NbColumns - CT->NbRows;
2514 EP = barvinok_enumerate_e(I, exist, nparam, MaxRays);
2515 nparam += CT->NbColumns - CT->NbRows;
2516 addeliminatedparams_enum(EP, CT, CEq, MaxRays, nparam);
2517 Polyhedron_Free(I);
2519 if (PR != *PA)
2520 Polyhedron_Free(PR);
2521 PR = 0;
2523 if (!EP && nd > 1) {
2524 #ifdef DEBUG_ER
2525 fprintf(stderr, "\nER: VD\n");
2526 #endif /* DEBUG_ER */
2527 for (int i = 0; i < nd; ++i) {
2528 Polyhedron *CA = align_context(VD[i], P->Dimension, MaxRays);
2529 Polyhedron *I = DomainIntersection(P, CA, MaxRays);
2531 if (i == 0)
2532 EP = barvinok_enumerate_e(I, exist, nparam, MaxRays);
2533 else {
2534 evalue *E = barvinok_enumerate_e(I, exist, nparam, MaxRays);
2535 eadd(E, EP);
2536 free_evalue_refs(E);
2537 free(E);
2539 Polyhedron_Free(I);
2540 Polyhedron_Free(CA);
2544 for (int i = 0; i < nd; ++i) {
2545 Polyhedron_Free(VD[i]);
2546 Polyhedron_Free(fVD[i]);
2548 delete [] VD;
2549 delete [] fVD;
2550 value_clear(c);
2552 if (!EP && nvar == 0) {
2553 Value f;
2554 value_init(f);
2555 Param_Vertices *V, *V2;
2556 Matrix* M = Matrix_Alloc(1, P->Dimension+2);
2558 FORALL_PVertex_in_ParamPolyhedron(V, last, PP) {
2559 bool found = false;
2560 FORALL_PVertex_in_ParamPolyhedron(V2, last, PP) {
2561 if (V == V2) {
2562 found = true;
2563 continue;
2565 if (!found)
2566 continue;
2567 for (int i = 0; i < exist; ++i) {
2568 value_oppose(f, V->Vertex->p[i][nparam+1]);
2569 Vector_Combine(V->Vertex->p[i],
2570 V2->Vertex->p[i],
2571 M->p[0] + 1 + nvar + exist,
2572 V2->Vertex->p[i][nparam+1],
2574 nparam+1);
2575 int j;
2576 for (j = 0; j < nparam; ++j)
2577 if (value_notzero_p(M->p[0][1+nvar+exist+j]))
2578 break;
2579 if (j >= nparam)
2580 continue;
2581 ConstraintSimplify(M->p[0], M->p[0],
2582 P->Dimension+2, &f);
2583 value_set_si(M->p[0][0], 0);
2584 Polyhedron *para = AddConstraints(M->p[0], 1, P,
2585 MaxRays);
2586 if (emptyQ(para)) {
2587 Polyhedron_Free(para);
2588 continue;
2590 Polyhedron *pos, *neg;
2591 value_set_si(M->p[0][0], 1);
2592 value_decrement(M->p[0][P->Dimension+1],
2593 M->p[0][P->Dimension+1]);
2594 neg = AddConstraints(M->p[0], 1, P, MaxRays);
2595 value_set_si(f, -1);
2596 Vector_Scale(M->p[0]+1, M->p[0]+1, f,
2597 P->Dimension+1);
2598 value_decrement(M->p[0][P->Dimension+1],
2599 M->p[0][P->Dimension+1]);
2600 value_decrement(M->p[0][P->Dimension+1],
2601 M->p[0][P->Dimension+1]);
2602 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2603 if (emptyQ(neg) && emptyQ(pos)) {
2604 Polyhedron_Free(para);
2605 Polyhedron_Free(pos);
2606 Polyhedron_Free(neg);
2607 continue;
2609 #ifdef DEBUG_ER
2610 fprintf(stderr, "\nER: Order\n");
2611 #endif /* DEBUG_ER */
2612 EP = barvinok_enumerate_e(para, exist, nparam, MaxRays);
2613 evalue *E;
2614 if (!emptyQ(pos)) {
2615 E = barvinok_enumerate_e(pos, exist, nparam, MaxRays);
2616 eadd(E, EP);
2617 free_evalue_refs(E);
2618 free(E);
2620 if (!emptyQ(neg)) {
2621 E = barvinok_enumerate_e(neg, exist, nparam, MaxRays);
2622 eadd(E, EP);
2623 free_evalue_refs(E);
2624 free(E);
2626 Polyhedron_Free(para);
2627 Polyhedron_Free(pos);
2628 Polyhedron_Free(neg);
2629 break;
2631 if (EP)
2632 break;
2633 } END_FORALL_PVertex_in_ParamPolyhedron;
2634 if (EP)
2635 break;
2636 } END_FORALL_PVertex_in_ParamPolyhedron;
2638 if (!EP) {
2639 /* Search for vertex coordinate to split on */
2640 /* First look for one independent of the parameters */
2641 FORALL_PVertex_in_ParamPolyhedron(V, last, PP) {
2642 for (int i = 0; i < exist; ++i) {
2643 int j;
2644 for (j = 0; j < nparam; ++j)
2645 if (value_notzero_p(V->Vertex->p[i][j]))
2646 break;
2647 if (j < nparam)
2648 continue;
2649 value_set_si(M->p[0][0], 1);
2650 Vector_Set(M->p[0]+1, 0, nvar+exist);
2651 Vector_Copy(V->Vertex->p[i],
2652 M->p[0] + 1 + nvar + exist, nparam+1);
2653 value_oppose(M->p[0][1+nvar+i],
2654 V->Vertex->p[i][nparam+1]);
2656 Polyhedron *pos, *neg;
2657 value_set_si(M->p[0][0], 1);
2658 value_decrement(M->p[0][P->Dimension+1],
2659 M->p[0][P->Dimension+1]);
2660 neg = AddConstraints(M->p[0], 1, P, MaxRays);
2661 value_set_si(f, -1);
2662 Vector_Scale(M->p[0]+1, M->p[0]+1, f,
2663 P->Dimension+1);
2664 value_decrement(M->p[0][P->Dimension+1],
2665 M->p[0][P->Dimension+1]);
2666 value_decrement(M->p[0][P->Dimension+1],
2667 M->p[0][P->Dimension+1]);
2668 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2669 if (emptyQ(neg) || emptyQ(pos)) {
2670 Polyhedron_Free(pos);
2671 Polyhedron_Free(neg);
2672 continue;
2674 Polyhedron_Free(pos);
2675 value_increment(M->p[0][P->Dimension+1],
2676 M->p[0][P->Dimension+1]);
2677 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2678 #ifdef DEBUG_ER
2679 fprintf(stderr, "\nER: Vertex\n");
2680 #endif /* DEBUG_ER */
2681 pos->next = neg;
2682 EP = enumerate_or(pos, exist, nparam, MaxRays);
2683 break;
2685 if (EP)
2686 break;
2687 } END_FORALL_PVertex_in_ParamPolyhedron;
2690 if (!EP) {
2691 /* Search for vertex coordinate to split on */
2692 /* Now look for one that depends on the parameters */
2693 FORALL_PVertex_in_ParamPolyhedron(V, last, PP) {
2694 for (int i = 0; i < exist; ++i) {
2695 value_set_si(M->p[0][0], 1);
2696 Vector_Set(M->p[0]+1, 0, nvar+exist);
2697 Vector_Copy(V->Vertex->p[i],
2698 M->p[0] + 1 + nvar + exist, nparam+1);
2699 value_oppose(M->p[0][1+nvar+i],
2700 V->Vertex->p[i][nparam+1]);
2702 Polyhedron *pos, *neg;
2703 value_set_si(M->p[0][0], 1);
2704 value_decrement(M->p[0][P->Dimension+1],
2705 M->p[0][P->Dimension+1]);
2706 neg = AddConstraints(M->p[0], 1, P, MaxRays);
2707 value_set_si(f, -1);
2708 Vector_Scale(M->p[0]+1, M->p[0]+1, f,
2709 P->Dimension+1);
2710 value_decrement(M->p[0][P->Dimension+1],
2711 M->p[0][P->Dimension+1]);
2712 value_decrement(M->p[0][P->Dimension+1],
2713 M->p[0][P->Dimension+1]);
2714 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2715 if (emptyQ(neg) || emptyQ(pos)) {
2716 Polyhedron_Free(pos);
2717 Polyhedron_Free(neg);
2718 continue;
2720 Polyhedron_Free(pos);
2721 value_increment(M->p[0][P->Dimension+1],
2722 M->p[0][P->Dimension+1]);
2723 pos = AddConstraints(M->p[0], 1, P, MaxRays);
2724 #ifdef DEBUG_ER
2725 fprintf(stderr, "\nER: ParamVertex\n");
2726 #endif /* DEBUG_ER */
2727 pos->next = neg;
2728 EP = enumerate_or(pos, exist, nparam, MaxRays);
2729 break;
2731 if (EP)
2732 break;
2733 } END_FORALL_PVertex_in_ParamPolyhedron;
2736 Matrix_Free(M);
2737 value_clear(f);
2740 if (CEq)
2741 Polyhedron_Free(CEq);
2742 if (CT)
2743 Matrix_Free(CT);
2744 if (PP)
2745 Param_Polyhedron_Free(PP);
2746 *PA = P;
2748 return EP;
2751 #ifndef HAVE_PIPLIB
2752 evalue *barvinok_enumerate_pip(Polyhedron *P,
2753 unsigned exist, unsigned nparam, unsigned MaxRays)
2755 return 0;
2757 #else
2758 evalue *barvinok_enumerate_pip(Polyhedron *P,
2759 unsigned exist, unsigned nparam, unsigned MaxRays)
2761 int nvar = P->Dimension - exist - nparam;
2762 evalue *EP = new_zero_ep();
2763 Polyhedron *Q, *N, *T = 0;
2764 Value min, tmp;
2765 value_init(min);
2766 value_init(tmp);
2768 #ifdef DEBUG_ER
2769 fprintf(stderr, "\nER: PIP\n");
2770 #endif /* DEBUG_ER */
2772 for (int i = 0; i < P->Dimension; ++i) {
2773 bool pos = false;
2774 bool neg = false;
2775 bool posray = false;
2776 bool negray = false;
2777 value_set_si(min, 0);
2778 for (int j = 0; j < P->NbRays; ++j) {
2779 if (value_pos_p(P->Ray[j][1+i])) {
2780 pos = true;
2781 if (value_zero_p(P->Ray[j][1+P->Dimension]))
2782 posray = true;
2783 } else if (value_neg_p(P->Ray[j][1+i])) {
2784 neg = true;
2785 if (value_zero_p(P->Ray[j][1+P->Dimension]))
2786 negray = true;
2787 else {
2788 mpz_fdiv_q(tmp,
2789 P->Ray[j][1+i], P->Ray[j][1+P->Dimension]);
2790 if (value_lt(tmp, min))
2791 value_assign(min, tmp);
2795 if (pos && neg) {
2796 assert(!(posray && negray));
2797 assert(!negray); // for now
2798 Polyhedron *O = T ? T : P;
2799 /* shift by a safe amount */
2800 Matrix *M = Matrix_Alloc(O->NbRays, O->Dimension+2);
2801 Vector_Copy(O->Ray[0], M->p[0], O->NbRays * (O->Dimension+2));
2802 for (int j = 0; j < P->NbRays; ++j) {
2803 if (value_notzero_p(M->p[j][1+P->Dimension])) {
2804 value_multiply(tmp, min, M->p[j][1+P->Dimension]);
2805 value_substract(M->p[j][1+i], M->p[j][1+i], tmp);
2808 if (T)
2809 Polyhedron_Free(T);
2810 T = Rays2Polyhedron(M, MaxRays);
2811 Matrix_Free(M);
2812 } else if (neg) {
2813 /* negating a parameter requires that we substitute in the
2814 * sign again afterwards.
2815 * Disallow for now.
2817 assert(i < nvar+exist);
2818 if (!T)
2819 T = Polyhedron_Copy(P);
2820 for (int j = 0; j < T->NbRays; ++j)
2821 value_oppose(T->Ray[j][1+i], T->Ray[j][1+i]);
2822 for (int j = 0; j < T->NbConstraints; ++j)
2823 value_oppose(T->Constraint[j][1+i], T->Constraint[j][1+i]);
2826 value_clear(min);
2827 value_clear(tmp);
2829 Polyhedron *D = pip_lexmin(T ? T : P, exist, nparam);
2830 for (Q = D; Q; Q = N) {
2831 N = Q->next;
2832 Q->next = 0;
2833 evalue *E;
2834 exist = Q->Dimension - nvar - nparam;
2835 E = barvinok_enumerate_e(Q, exist, nparam, MaxRays);
2836 Polyhedron_Free(Q);
2837 eadd(E, EP);
2838 free_evalue_refs(E);
2839 free(E);
2842 if (T)
2843 Polyhedron_Free(T);
2845 return EP;
2847 #endif
2850 static bool is_single(Value *row, int pos, int len)
2852 return First_Non_Zero(row, pos) == -1 &&
2853 First_Non_Zero(row+pos+1, len-pos-1) == -1;
2856 static evalue* barvinok_enumerate_e_r(Polyhedron *P,
2857 unsigned exist, unsigned nparam, unsigned MaxRays);
2859 #ifdef DEBUG_ER
2860 static int er_level = 0;
2862 evalue* barvinok_enumerate_e(Polyhedron *P,
2863 unsigned exist, unsigned nparam, unsigned MaxRays)
2865 fprintf(stderr, "\nER: level %i\n", er_level);
2866 int nvar = P->Dimension - exist - nparam;
2867 fprintf(stderr, "%d %d %d\n", nvar, exist, nparam);
2869 Polyhedron_Print(stderr, P_VALUE_FMT, P);
2870 ++er_level;
2871 P = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
2872 evalue *EP = barvinok_enumerate_e_r(P, exist, nparam, MaxRays);
2873 Polyhedron_Free(P);
2874 --er_level;
2875 return EP;
2877 #else
2878 evalue* barvinok_enumerate_e(Polyhedron *P,
2879 unsigned exist, unsigned nparam, unsigned MaxRays)
2881 P = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
2882 evalue *EP = barvinok_enumerate_e_r(P, exist, nparam, MaxRays);
2883 Polyhedron_Free(P);
2884 return EP;
2886 #endif
2888 static evalue* barvinok_enumerate_e_r(Polyhedron *P,
2889 unsigned exist, unsigned nparam, unsigned MaxRays)
2891 if (exist == 0) {
2892 Polyhedron *U = Universe_Polyhedron(nparam);
2893 evalue *EP = barvinok_enumerate_ev(P, U, MaxRays);
2894 //char *param_name[] = {"P", "Q", "R", "S", "T" };
2895 //print_evalue(stdout, EP, param_name);
2896 Polyhedron_Free(U);
2897 return EP;
2900 int nvar = P->Dimension - exist - nparam;
2901 int len = P->Dimension + 2;
2903 if (emptyQ(P))
2904 return new_zero_ep();
2906 if (nvar == 0 && nparam == 0) {
2907 evalue *EP = new_zero_ep();
2908 barvinok_count(P, &EP->x.n, MaxRays);
2909 if (value_pos_p(EP->x.n))
2910 value_set_si(EP->x.n, 1);
2911 return EP;
2914 int r;
2915 for (r = 0; r < P->NbRays; ++r)
2916 if (value_zero_p(P->Ray[r][0]) ||
2917 value_zero_p(P->Ray[r][P->Dimension+1])) {
2918 int i;
2919 for (i = 0; i < nvar; ++i)
2920 if (value_notzero_p(P->Ray[r][i+1]))
2921 break;
2922 if (i >= nvar)
2923 continue;
2924 for (i = nvar + exist; i < nvar + exist + nparam; ++i)
2925 if (value_notzero_p(P->Ray[r][i+1]))
2926 break;
2927 if (i >= nvar + exist + nparam)
2928 break;
2930 if (r < P->NbRays) {
2931 evalue *EP = new_zero_ep();
2932 value_set_si(EP->x.n, -1);
2933 return EP;
2936 int first;
2937 for (r = 0; r < P->NbEq; ++r)
2938 if ((first = First_Non_Zero(P->Constraint[r]+1+nvar, exist)) != -1)
2939 break;
2940 if (r < P->NbEq) {
2941 if (First_Non_Zero(P->Constraint[r]+1+nvar+first+1,
2942 exist-first-1) != -1) {
2943 Polyhedron *T = rotate_along(P, r, nvar, exist, MaxRays);
2944 #ifdef DEBUG_ER
2945 fprintf(stderr, "\nER: Equality\n");
2946 #endif /* DEBUG_ER */
2947 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2948 Polyhedron_Free(T);
2949 return EP;
2950 } else {
2951 #ifdef DEBUG_ER
2952 fprintf(stderr, "\nER: Fixed\n");
2953 #endif /* DEBUG_ER */
2954 if (first == 0)
2955 return barvinok_enumerate_e(P, exist-1, nparam, MaxRays);
2956 else {
2957 Polyhedron *T = Polyhedron_Copy(P);
2958 SwapColumns(T, nvar+1, nvar+1+first);
2959 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2960 Polyhedron_Free(T);
2961 return EP;
2966 Vector *row = Vector_Alloc(len);
2967 value_set_si(row->p[0], 1);
2969 Value f;
2970 value_init(f);
2972 enum constraint* info = new constraint[exist];
2973 for (int i = 0; i < exist; ++i) {
2974 info[i] = ALL_POS;
2975 for (int l = P->NbEq; l < P->NbConstraints; ++l) {
2976 if (value_negz_p(P->Constraint[l][nvar+i+1]))
2977 continue;
2978 bool l_parallel = is_single(P->Constraint[l]+nvar+1, i, exist);
2979 for (int u = P->NbEq; u < P->NbConstraints; ++u) {
2980 if (value_posz_p(P->Constraint[u][nvar+i+1]))
2981 continue;
2982 bool lu_parallel = l_parallel ||
2983 is_single(P->Constraint[u]+nvar+1, i, exist);
2984 value_oppose(f, P->Constraint[u][nvar+i+1]);
2985 Vector_Combine(P->Constraint[l]+1, P->Constraint[u]+1, row->p+1,
2986 f, P->Constraint[l][nvar+i+1], len-1);
2987 if (!(info[i] & INDEPENDENT)) {
2988 int j;
2989 for (j = 0; j < exist; ++j)
2990 if (j != i && value_notzero_p(row->p[nvar+j+1]))
2991 break;
2992 if (j == exist) {
2993 //printf("independent: i: %d, l: %d, u: %d\n", i, l, u);
2994 info[i] = (constraint)(info[i] | INDEPENDENT);
2997 if (info[i] & ALL_POS) {
2998 value_addto(row->p[len-1], row->p[len-1],
2999 P->Constraint[l][nvar+i+1]);
3000 value_addto(row->p[len-1], row->p[len-1], f);
3001 value_multiply(f, f, P->Constraint[l][nvar+i+1]);
3002 value_substract(row->p[len-1], row->p[len-1], f);
3003 value_decrement(row->p[len-1], row->p[len-1]);
3004 ConstraintSimplify(row->p, row->p, len, &f);
3005 value_set_si(f, -1);
3006 Vector_Scale(row->p+1, row->p+1, f, len-1);
3007 value_decrement(row->p[len-1], row->p[len-1]);
3008 Polyhedron *T = AddConstraints(row->p, 1, P, MaxRays);
3009 if (!emptyQ(T)) {
3010 //printf("not all_pos: i: %d, l: %d, u: %d\n", i, l, u);
3011 info[i] = (constraint)(info[i] ^ ALL_POS);
3013 //puts("pos remainder");
3014 //Polyhedron_Print(stdout, P_VALUE_FMT, T);
3015 Polyhedron_Free(T);
3017 if (!(info[i] & ONE_NEG)) {
3018 if (lu_parallel) {
3019 negative_test_constraint(P->Constraint[l],
3020 P->Constraint[u],
3021 row->p, nvar+i, len, &f);
3022 oppose_constraint(row->p, len, &f);
3023 Polyhedron *T = AddConstraints(row->p, 1, P, MaxRays);
3024 if (emptyQ(T)) {
3025 //printf("one_neg i: %d, l: %d, u: %d\n", i, l, u);
3026 info[i] = (constraint)(info[i] | ONE_NEG);
3028 //puts("neg remainder");
3029 //Polyhedron_Print(stdout, P_VALUE_FMT, T);
3030 Polyhedron_Free(T);
3033 if (!(info[i] & ALL_POS) && (info[i] & ONE_NEG))
3034 goto next;
3037 if (info[i] & ALL_POS)
3038 break;
3039 next:
3044 for (int i = 0; i < exist; ++i)
3045 printf("%i: %i\n", i, info[i]);
3047 for (int i = 0; i < exist; ++i)
3048 if (info[i] & ALL_POS) {
3049 #ifdef DEBUG_ER
3050 fprintf(stderr, "\nER: Positive\n");
3051 #endif /* DEBUG_ER */
3052 // Eliminate
3053 // Maybe we should chew off some of the fat here
3054 Matrix *M = Matrix_Alloc(P->Dimension, P->Dimension+1);
3055 for (int j = 0; j < P->Dimension; ++j)
3056 value_set_si(M->p[j][j + (j >= i+nvar)], 1);
3057 Polyhedron *T = Polyhedron_Image(P, M, MaxRays);
3058 Matrix_Free(M);
3059 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
3060 Polyhedron_Free(T);
3061 value_clear(f);
3062 Vector_Free(row);
3063 delete [] info;
3064 return EP;
3066 for (int i = 0; i < exist; ++i)
3067 if (info[i] & ONE_NEG) {
3068 #ifdef DEBUG_ER
3069 fprintf(stderr, "\nER: Negative\n");
3070 #endif /* DEBUG_ER */
3071 Vector_Free(row);
3072 value_clear(f);
3073 delete [] info;
3074 if (i == 0)
3075 return barvinok_enumerate_e(P, exist-1, nparam, MaxRays);
3076 else {
3077 Polyhedron *T = Polyhedron_Copy(P);
3078 SwapColumns(T, nvar+1, nvar+1+i);
3079 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
3080 Polyhedron_Free(T);
3081 return EP;
3084 for (int i = 0; i < exist; ++i)
3085 if (info[i] & INDEPENDENT) {
3086 Polyhedron *pos, *neg;
3088 /* Find constraint again and split off negative part */
3090 if (SplitOnVar(P, i, nvar, len, exist, MaxRays,
3091 row, f, true, &pos, &neg)) {
3092 #ifdef DEBUG_ER
3093 fprintf(stderr, "\nER: Split\n");
3094 #endif /* DEBUG_ER */
3096 evalue *EP =
3097 barvinok_enumerate_e(neg, exist-1, nparam, MaxRays);
3098 evalue *E =
3099 barvinok_enumerate_e(pos, exist, nparam, MaxRays);
3100 eadd(E, EP);
3101 free_evalue_refs(E);
3102 free(E);
3103 Polyhedron_Free(neg);
3104 Polyhedron_Free(pos);
3105 value_clear(f);
3106 Vector_Free(row);
3107 delete [] info;
3108 return EP;
3111 delete [] info;
3113 Polyhedron *O = P;
3114 Polyhedron *F;
3116 evalue *EP;
3118 EP = enumerate_line(P, exist, nparam, MaxRays);
3119 if (EP)
3120 goto out;
3122 EP = barvinok_enumerate_pip(P, exist, nparam, MaxRays);
3123 if (EP)
3124 goto out;
3126 EP = enumerate_redundant_ray(P, exist, nparam, MaxRays);
3127 if (EP)
3128 goto out;
3130 EP = enumerate_sure(P, exist, nparam, MaxRays);
3131 if (EP)
3132 goto out;
3134 EP = enumerate_ray(P, exist, nparam, MaxRays);
3135 if (EP)
3136 goto out;
3138 EP = enumerate_sure2(P, exist, nparam, MaxRays);
3139 if (EP)
3140 goto out;
3142 F = unfringe(P, MaxRays);
3143 if (!PolyhedronIncludes(F, P)) {
3144 #ifdef DEBUG_ER
3145 fprintf(stderr, "\nER: Fringed\n");
3146 #endif /* DEBUG_ER */
3147 EP = barvinok_enumerate_e(F, exist, nparam, MaxRays);
3148 Polyhedron_Free(F);
3149 goto out;
3151 Polyhedron_Free(F);
3153 if (nparam)
3154 EP = enumerate_vd(&P, exist, nparam, MaxRays);
3155 if (EP)
3156 goto out2;
3158 if (nvar != 0) {
3159 EP = enumerate_sum(P, exist, nparam, MaxRays);
3160 goto out2;
3163 assert(nvar == 0);
3165 int i;
3166 Polyhedron *pos, *neg;
3167 for (i = 0; i < exist; ++i)
3168 if (SplitOnVar(P, i, nvar, len, exist, MaxRays,
3169 row, f, false, &pos, &neg))
3170 break;
3172 assert (i < exist);
3174 pos->next = neg;
3175 EP = enumerate_or(pos, exist, nparam, MaxRays);
3177 out2:
3178 if (O != P)
3179 Polyhedron_Free(P);
3181 out:
3182 value_clear(f);
3183 Vector_Free(row);
3184 return EP;