split off part that certainly contains lattice points
[barvinok.git] / barvinok.cc
blob65e735d36d8c508a0de79e7637efa6c1b2433ef3
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"
15 #include "config.h"
16 #include <barvinok.h>
18 #ifdef NTL_STD_CXX
19 using namespace NTL;
20 #endif
21 using std::cout;
22 using std::endl;
23 using std::vector;
24 using std::deque;
25 using std::string;
26 using std::ostringstream;
28 #define ALLOC(p) (((long *) (p))[0])
29 #define SIZE(p) (((long *) (p))[1])
30 #define DATA(p) ((mp_limb_t *) (((long *) (p)) + 2))
32 static void value2zz(Value v, ZZ& z)
34 int sa = v[0]._mp_size;
35 int abs_sa = sa < 0 ? -sa : sa;
37 _ntl_gsetlength(&z.rep, abs_sa);
38 mp_limb_t * adata = DATA(z.rep);
39 for (int i = 0; i < abs_sa; ++i)
40 adata[i] = v[0]._mp_d[i];
41 SIZE(z.rep) = sa;
44 static void zz2value(ZZ& z, Value& v)
46 if (!z.rep) {
47 value_set_si(v, 0);
48 return;
51 int sa = SIZE(z.rep);
52 int abs_sa = sa < 0 ? -sa : sa;
54 mp_limb_t * adata = DATA(z.rep);
55 mpz_realloc2(v, __GMP_BITS_PER_MP_LIMB * abs_sa);
56 for (int i = 0; i < abs_sa; ++i)
57 v[0]._mp_d[i] = adata[i];
58 v[0]._mp_size = sa;
61 #undef ALLOC
62 #define ALLOC(p) p = (typeof(p))malloc(sizeof(*p))
65 * We just ignore the last column and row
66 * If the final element is not equal to one
67 * then the result will actually be a multiple of the input
69 static void matrix2zz(Matrix *M, mat_ZZ& m, unsigned nr, unsigned nc)
71 m.SetDims(nr, nc);
73 for (int i = 0; i < nr; ++i) {
74 // assert(value_one_p(M->p[i][M->NbColumns - 1]));
75 for (int j = 0; j < nc; ++j) {
76 value2zz(M->p[i][j], m[i][j]);
81 static void values2zz(Value *p, vec_ZZ& v, int len)
83 v.SetLength(len);
85 for (int i = 0; i < len; ++i) {
86 value2zz(p[i], v[i]);
92 static void zz2values(vec_ZZ& v, Value *p)
94 for (int i = 0; i < v.length(); ++i)
95 zz2value(v[i], p[i]);
98 static void rays(mat_ZZ& r, Polyhedron *C)
100 unsigned dim = C->NbRays - 1; /* don't count zero vertex */
101 assert(C->NbRays - 1 == C->Dimension);
102 r.SetDims(dim, dim);
103 ZZ tmp;
105 int i, c;
106 for (i = 0, c = 0; i < dim; ++i)
107 if (value_zero_p(C->Ray[i][dim+1])) {
108 for (int j = 0; j < dim; ++j) {
109 value2zz(C->Ray[i][j+1], tmp);
110 r[j][c] = tmp;
112 ++c;
116 static Matrix * rays(Polyhedron *C)
118 unsigned dim = C->NbRays - 1; /* don't count zero vertex */
119 assert(C->NbRays - 1 == C->Dimension);
121 Matrix *M = Matrix_Alloc(dim+1, dim+1);
122 assert(M);
124 int i, c;
125 for (i = 0, c = 0; i <= dim && c < dim; ++i)
126 if (value_zero_p(C->Ray[i][dim+1])) {
127 Vector_Copy(C->Ray[i] + 1, M->p[c], dim);
128 value_set_si(M->p[c++][dim], 0);
130 assert(c == dim);
131 value_set_si(M->p[dim][dim], 1);
133 return M;
136 static Matrix * rays2(Polyhedron *C)
138 unsigned dim = C->NbRays - 1; /* don't count zero vertex */
139 assert(C->NbRays - 1 == C->Dimension);
141 Matrix *M = Matrix_Alloc(dim, dim);
142 assert(M);
144 int i, c;
145 for (i = 0, c = 0; i <= dim && c < dim; ++i)
146 if (value_zero_p(C->Ray[i][dim+1]))
147 Vector_Copy(C->Ray[i] + 1, M->p[c++], dim);
148 assert(c == dim);
150 return M;
154 * Returns the largest absolute value in the vector
156 static ZZ max(vec_ZZ& v)
158 ZZ max = abs(v[0]);
159 for (int i = 1; i < v.length(); ++i)
160 if (abs(v[i]) > max)
161 max = abs(v[i]);
162 return max;
165 class cone {
166 public:
167 cone(Matrix *M) {
168 Cone = 0;
169 Rays = Matrix_Copy(M);
170 set_det();
172 cone(Polyhedron *C) {
173 Cone = Polyhedron_Copy(C);
174 Rays = rays(C);
175 set_det();
177 void set_det() {
178 mat_ZZ A;
179 matrix2zz(Rays, A, Rays->NbRows - 1, Rays->NbColumns - 1);
180 det = determinant(A);
181 Value v;
182 value_init(v);
183 zz2value(det, v);
184 value_clear(v);
187 Vector* short_vector(vec_ZZ& lambda) {
188 Matrix *M = Matrix_Copy(Rays);
189 Matrix *inv = Matrix_Alloc(M->NbRows, M->NbColumns);
190 int ok = Matrix_Inverse(M, inv);
191 assert(ok);
192 Matrix_Free(M);
194 ZZ det2;
195 mat_ZZ B;
196 mat_ZZ U;
197 matrix2zz(inv, B, inv->NbRows - 1, inv->NbColumns - 1);
198 long r = LLL(det2, B, U);
200 ZZ min = max(B[0]);
201 int index = 0;
202 for (int i = 1; i < B.NumRows(); ++i) {
203 ZZ tmp = max(B[i]);
204 if (tmp < min) {
205 min = tmp;
206 index = i;
210 Matrix_Free(inv);
212 lambda = B[index];
214 Vector *z = Vector_Alloc(U[index].length()+1);
215 assert(z);
216 zz2values(U[index], z->p);
217 value_set_si(z->p[U[index].length()], 0);
219 Value tmp;
220 value_init(tmp);
221 Polyhedron *C = poly();
222 int i;
223 for (i = 0; i < C->NbConstraints; ++i) {
224 Inner_Product(z->p, C->Constraint[i]+1, z->Size-1, &tmp);
225 if (value_pos_p(tmp))
226 break;
228 if (i == C->NbConstraints) {
229 value_set_si(tmp, -1);
230 Vector_Scale(z->p, z->p, tmp, z->Size-1);
232 value_clear(tmp);
233 return z;
236 ~cone() {
237 Polyhedron_Free(Cone);
238 Matrix_Free(Rays);
241 Polyhedron *poly() {
242 if (!Cone) {
243 Matrix *M = Matrix_Alloc(Rays->NbRows+1, Rays->NbColumns+1);
244 for (int i = 0; i < Rays->NbRows; ++i) {
245 Vector_Copy(Rays->p[i], M->p[i]+1, Rays->NbColumns);
246 value_set_si(M->p[i][0], 1);
248 Vector_Set(M->p[Rays->NbRows]+1, 0, Rays->NbColumns-1);
249 value_set_si(M->p[Rays->NbRows][0], 1);
250 value_set_si(M->p[Rays->NbRows][Rays->NbColumns], 1);
251 Cone = Rays2Polyhedron(M, M->NbRows+1);
252 assert(Cone->NbConstraints == Cone->NbRays);
253 Matrix_Free(M);
255 return Cone;
258 ZZ det;
259 Polyhedron *Cone;
260 Matrix *Rays;
263 class dpoly {
264 public:
265 vec_ZZ coeff;
266 dpoly(int d, ZZ& degree, int offset = 0) {
267 coeff.SetLength(d+1);
269 int min = d + offset;
270 if (degree < ZZ(INIT_VAL, min))
271 min = to_int(degree);
273 ZZ c = ZZ(INIT_VAL, 1);
274 if (!offset)
275 coeff[0] = c;
276 for (int i = 1; i <= min; ++i) {
277 c *= (degree -i + 1);
278 c /= i;
279 coeff[i-offset] = c;
282 void operator *= (dpoly& f) {
283 assert(coeff.length() == f.coeff.length());
284 vec_ZZ old = coeff;
285 coeff = f.coeff[0] * coeff;
286 for (int i = 1; i < coeff.length(); ++i)
287 for (int j = 0; i+j < coeff.length(); ++j)
288 coeff[i+j] += f.coeff[i] * old[j];
290 void div(dpoly& d, mpq_t count, ZZ& sign) {
291 int len = coeff.length();
292 Value tmp;
293 value_init(tmp);
294 mpq_t* c = new mpq_t[coeff.length()];
295 mpq_t qtmp;
296 mpq_init(qtmp);
297 for (int i = 0; i < len; ++i) {
298 mpq_init(c[i]);
299 zz2value(coeff[i], tmp);
300 mpq_set_z(c[i], tmp);
302 for (int j = 1; j <= i; ++j) {
303 zz2value(d.coeff[j], tmp);
304 mpq_set_z(qtmp, tmp);
305 mpq_mul(qtmp, qtmp, c[i-j]);
306 mpq_sub(c[i], c[i], qtmp);
309 zz2value(d.coeff[0], tmp);
310 mpq_set_z(qtmp, tmp);
311 mpq_div(c[i], c[i], qtmp);
313 if (sign == -1)
314 mpq_sub(count, count, c[len-1]);
315 else
316 mpq_add(count, count, c[len-1]);
318 value_clear(tmp);
319 mpq_clear(qtmp);
320 for (int i = 0; i < len; ++i)
321 mpq_clear(c[i]);
322 delete [] c;
326 class dpoly_n {
327 public:
328 Matrix *coeff;
329 ~dpoly_n() {
330 Matrix_Free(coeff);
332 dpoly_n(int d, ZZ& degree_0, ZZ& degree_1, int offset = 0) {
333 Value d0, d1;
334 value_init(d0);
335 value_init(d1);
336 zz2value(degree_0, d0);
337 zz2value(degree_1, d1);
338 coeff = Matrix_Alloc(d+1, d+1+1);
339 value_set_si(coeff->p[0][0], 1);
340 value_set_si(coeff->p[0][d+1], 1);
341 for (int i = 1; i <= d; ++i) {
342 value_multiply(coeff->p[i][0], coeff->p[i-1][0], d0);
343 Vector_Combine(coeff->p[i-1], coeff->p[i-1]+1, coeff->p[i]+1,
344 d1, d0, i);
345 value_set_si(coeff->p[i][d+1], i);
346 value_multiply(coeff->p[i][d+1], coeff->p[i][d+1], coeff->p[i-1][d+1]);
347 value_decrement(d0, d0);
349 value_clear(d0);
350 value_clear(d1);
352 void div(dpoly& d, Vector *count, ZZ& sign) {
353 int len = coeff->NbRows;
354 Matrix * c = Matrix_Alloc(coeff->NbRows, coeff->NbColumns);
355 Value tmp;
356 value_init(tmp);
357 for (int i = 0; i < len; ++i) {
358 Vector_Copy(coeff->p[i], c->p[i], len+1);
359 for (int j = 1; j <= i; ++j) {
360 zz2value(d.coeff[j], tmp);
361 value_multiply(tmp, tmp, c->p[i][len]);
362 value_oppose(tmp, tmp);
363 Vector_Combine(c->p[i], c->p[i-j], c->p[i],
364 c->p[i-j][len], tmp, len);
365 value_multiply(c->p[i][len], c->p[i][len], c->p[i-j][len]);
367 zz2value(d.coeff[0], tmp);
368 value_multiply(c->p[i][len], c->p[i][len], tmp);
370 if (sign == -1) {
371 value_set_si(tmp, -1);
372 Vector_Scale(c->p[len-1], count->p, tmp, len);
373 value_assign(count->p[len], c->p[len-1][len]);
374 } else
375 Vector_Copy(c->p[len-1], count->p, len+1);
376 Vector_Normalize(count->p, len+1);
377 value_clear(tmp);
378 Matrix_Free(c);
383 * Barvinok's Decomposition of a simplicial cone
385 * Returns two lists of polyhedra
387 void barvinok_decompose(Polyhedron *C, Polyhedron **ppos, Polyhedron **pneg)
389 Polyhedron *pos = *ppos, *neg = *pneg;
390 vector<cone *> nonuni;
391 cone * c = new cone(C);
392 ZZ det = c->det;
393 int s = sign(det);
394 assert(det != 0);
395 if (abs(det) > 1) {
396 nonuni.push_back(c);
397 } else {
398 Polyhedron *p = Polyhedron_Copy(c->Cone);
399 p->next = pos;
400 pos = p;
401 delete c;
403 vec_ZZ lambda;
404 while (!nonuni.empty()) {
405 c = nonuni.back();
406 nonuni.pop_back();
407 Vector* v = c->short_vector(lambda);
408 for (int i = 0; i < c->Rays->NbRows - 1; ++i) {
409 if (lambda[i] == 0)
410 continue;
411 Matrix* M = Matrix_Copy(c->Rays);
412 Vector_Copy(v->p, M->p[i], v->Size);
413 cone * pc = new cone(M);
414 assert (pc->det != 0);
415 if (abs(pc->det) > 1) {
416 assert(abs(pc->det) < abs(c->det));
417 nonuni.push_back(pc);
418 } else {
419 Polyhedron *p = pc->poly();
420 pc->Cone = 0;
421 if (sign(pc->det) == s) {
422 p->next = pos;
423 pos = p;
424 } else {
425 p->next = neg;
426 neg = p;
428 delete pc;
430 Matrix_Free(M);
432 Vector_Free(v);
433 delete c;
435 *ppos = pos;
436 *pneg = neg;
440 * Returns a single list of npos "positive" cones followed by nneg
441 * "negative" cones.
442 * The input cone is freed
444 void decompose(Polyhedron *cone, Polyhedron **parts, int *npos, int *nneg, unsigned MaxRays)
446 Polyhedron_Polarize(cone);
447 if (cone->NbRays - 1 != cone->Dimension) {
448 Polyhedron *tmp = cone;
449 cone = triangularize_cone(cone, MaxRays);
450 Polyhedron_Free(tmp);
452 Polyhedron *polpos = NULL, *polneg = NULL;
453 *npos = 0; *nneg = 0;
454 for (Polyhedron *Polar = cone; Polar; Polar = Polar->next)
455 barvinok_decompose(Polar, &polpos, &polneg);
457 Polyhedron *last;
458 for (Polyhedron *i = polpos; i; i = i->next) {
459 Polyhedron_Polarize(i);
460 ++*npos;
461 last = i;
463 for (Polyhedron *i = polneg; i; i = i->next) {
464 Polyhedron_Polarize(i);
465 ++*nneg;
467 if (last) {
468 last->next = polneg;
469 *parts = polpos;
470 } else
471 *parts = polneg;
472 Domain_Free(cone);
475 const int MAX_TRY=10;
477 * Searches for a vector that is not othogonal to any
478 * of the rays in rays.
480 static void nonorthog(mat_ZZ& rays, vec_ZZ& lambda)
482 int dim = rays.NumCols();
483 bool found = false;
484 lambda.SetLength(dim);
485 for (int i = 2; !found && i <= 50*dim; i+=4) {
486 for (int j = 0; j < MAX_TRY; ++j) {
487 for (int k = 0; k < dim; ++k) {
488 int r = random_int(i)+2;
489 int v = (2*(r%2)-1) * (r >> 1);
490 lambda[k] = v;
492 int k = 0;
493 for (; k < rays.NumRows(); ++k)
494 if (lambda * rays[k] == 0)
495 break;
496 if (k == rays.NumRows()) {
497 found = true;
498 break;
502 assert(found);
505 static void add_rays(mat_ZZ& rays, Polyhedron *i, int *r)
507 unsigned dim = i->Dimension;
508 for (int k = 0; k < i->NbRays; ++k) {
509 if (!value_zero_p(i->Ray[k][dim+1]))
510 continue;
511 values2zz(i->Ray[k]+1, rays[(*r)++], dim);
515 void lattice_point(Value* values, Polyhedron *i, vec_ZZ& lambda, ZZ& num)
517 vec_ZZ vertex;
518 unsigned dim = i->Dimension;
519 if(!value_one_p(values[dim])) {
520 Matrix* Rays = rays(i);
521 Matrix *inv = Matrix_Alloc(Rays->NbRows, Rays->NbColumns);
522 int ok = Matrix_Inverse(Rays, inv);
523 assert(ok);
524 Matrix_Free(Rays);
525 Rays = rays(i);
526 Vector *lambda = Vector_Alloc(dim+1);
527 Vector_Matrix_Product(values, inv, lambda->p);
528 Matrix_Free(inv);
529 for (int j = 0; j < dim; ++j)
530 mpz_cdiv_q(lambda->p[j], lambda->p[j], lambda->p[dim]);
531 value_set_si(lambda->p[dim], 1);
532 Vector *A = Vector_Alloc(dim+1);
533 Vector_Matrix_Product(lambda->p, Rays, A->p);
534 Vector_Free(lambda);
535 Matrix_Free(Rays);
536 values2zz(A->p, vertex, dim);
537 Vector_Free(A);
538 } else
539 values2zz(values, vertex, dim);
541 num = vertex * lambda;
544 static evalue *term(int param, ZZ& c, Value *den = NULL)
546 evalue *EP = new evalue();
547 value_init(EP->d);
548 value_set_si(EP->d,0);
549 EP->x.p = new_enode(polynomial, 2, param + 1);
550 evalue_set_si(&EP->x.p->arr[0], 0, 1);
551 value_init(EP->x.p->arr[1].x.n);
552 if (den == NULL)
553 value_set_si(EP->x.p->arr[1].d, 1);
554 else
555 value_assign(EP->x.p->arr[1].d, *den);
556 zz2value(c, EP->x.p->arr[1].x.n);
557 return EP;
560 static void vertex_period(
561 Polyhedron *i, vec_ZZ& lambda, Matrix *T,
562 Value lcm, int p, Vector *val,
563 evalue *E, evalue* ev,
564 ZZ& offset)
566 unsigned nparam = T->NbRows - 1;
567 unsigned dim = i->Dimension;
568 Value tmp;
569 ZZ nump;
571 if (p == nparam) {
572 ZZ num, l;
573 Vector * values = Vector_Alloc(dim + 1);
574 Vector_Matrix_Product(val->p, T, values->p);
575 value_assign(values->p[dim], lcm);
576 lattice_point(values->p, i, lambda, num);
577 value2zz(lcm, l);
578 num *= l;
579 num += offset;
580 value_init(ev->x.n);
581 zz2value(num, ev->x.n);
582 value_assign(ev->d, lcm);
583 Vector_Free(values);
584 return;
587 value_init(tmp);
588 vec_ZZ vertex;
589 values2zz(T->p[p], vertex, dim);
590 nump = vertex * lambda;
591 if (First_Non_Zero(val->p, p) == -1) {
592 value_assign(tmp, lcm);
593 evalue *ET = term(p, nump, &tmp);
594 eadd(ET, E);
595 free_evalue_refs(ET);
596 delete ET;
599 value_assign(tmp, lcm);
600 if (First_Non_Zero(T->p[p], dim) != -1)
601 Vector_Gcd(T->p[p], dim, &tmp);
602 Gcd(tmp, lcm, &tmp);
603 if (value_lt(tmp, lcm)) {
604 ZZ count;
606 value_division(tmp, lcm, tmp);
607 value_set_si(ev->d, 0);
608 ev->x.p = new_enode(periodic, VALUE_TO_INT(tmp), p+1);
609 value2zz(tmp, count);
610 do {
611 value_decrement(tmp, tmp);
612 --count;
613 ZZ new_offset = offset - count * nump;
614 value_assign(val->p[p], tmp);
615 vertex_period(i, lambda, T, lcm, p+1, val, E,
616 &ev->x.p->arr[VALUE_TO_INT(tmp)], new_offset);
617 } while (value_pos_p(tmp));
618 } else
619 vertex_period(i, lambda, T, lcm, p+1, val, E, ev, offset);
620 value_clear(tmp);
623 static void mask_r(Matrix *f, int nr, Vector *lcm, int p, Vector *val, evalue *ev)
625 unsigned nparam = lcm->Size;
627 if (p == nparam) {
628 Vector * prod = Vector_Alloc(f->NbRows);
629 Matrix_Vector_Product(f, val->p, prod->p);
630 int isint = 1;
631 for (int i = 0; i < nr; ++i) {
632 value_modulus(prod->p[i], prod->p[i], f->p[i][nparam+1]);
633 isint &= value_zero_p(prod->p[i]);
635 value_set_si(ev->d, 1);
636 value_init(ev->x.n);
637 value_set_si(ev->x.n, isint);
638 Vector_Free(prod);
639 return;
642 Value tmp;
643 value_init(tmp);
644 if (value_one_p(lcm->p[p]))
645 mask_r(f, nr, lcm, p+1, val, ev);
646 else {
647 value_assign(tmp, lcm->p[p]);
648 value_set_si(ev->d, 0);
649 ev->x.p = new_enode(periodic, VALUE_TO_INT(tmp), p+1);
650 do {
651 value_decrement(tmp, tmp);
652 value_assign(val->p[p], tmp);
653 mask_r(f, nr, lcm, p+1, val, &ev->x.p->arr[VALUE_TO_INT(tmp)]);
654 } while (value_pos_p(tmp));
656 value_clear(tmp);
659 static evalue *multi_monom(vec_ZZ& p)
661 evalue *X = new evalue();
662 value_init(X->d);
663 value_init(X->x.n);
664 unsigned nparam = p.length()-1;
665 zz2value(p[nparam], X->x.n);
666 value_set_si(X->d, 1);
667 for (int i = 0; i < nparam; ++i) {
668 if (p[i] == 0)
669 continue;
670 evalue *T = term(i, p[i]);
671 eadd(T, X);
672 free_evalue_refs(T);
673 delete T;
675 return X;
679 * Check whether mapping polyhedron P on the affine combination
680 * num yields a range that has a fixed quotient on integer
681 * division by d
682 * If zero is true, then we are only interested in the quotient
683 * for the cases where the remainder is zero.
684 * Returns NULL if false and a newly allocated value if true.
686 static Value *fixed_quotient(Polyhedron *P, vec_ZZ& num, Value d, bool zero)
688 Value* ret = NULL;
689 int len = num.length();
690 Matrix *T = Matrix_Alloc(2, len);
691 zz2values(num, T->p[0]);
692 value_set_si(T->p[1][len-1], 1);
693 Polyhedron *I = Polyhedron_Image(P, T, P->NbConstraints);
694 Matrix_Free(T);
696 int i;
697 for (i = 0; i < I->NbRays; ++i)
698 if (value_zero_p(I->Ray[i][2])) {
699 Polyhedron_Free(I);
700 return NULL;
703 Value min, max;
704 value_init(min);
705 value_init(max);
706 line_minmax(I, &min, &max);
708 if (zero)
709 mpz_cdiv_q(min, min, d);
710 else
711 mpz_fdiv_q(min, min, d);
712 mpz_fdiv_q(max, max, d);
714 if (value_eq(min, max)) {
715 ALLOC(ret);
716 value_init(*ret);
717 value_assign(*ret, min);
719 value_clear(min);
720 value_clear(max);
721 return ret;
725 * Normalize linear expression coef modulo m
726 * Removes common factor and reduces coefficients
727 * Returns index of first non-zero coefficient or len
729 static int normal_mod(Value *coef, int len, Value *m)
731 Value gcd;
732 value_init(gcd);
734 Vector_Gcd(coef, len, &gcd);
735 Gcd(gcd, *m, &gcd);
736 Vector_AntiScale(coef, coef, gcd, len);
738 value_division(*m, *m, gcd);
739 value_clear(gcd);
741 if (value_one_p(*m))
742 return len;
744 int j;
745 for (j = 0; j < len; ++j)
746 mpz_fdiv_r(coef[j], coef[j], *m);
747 for (j = 0; j < len; ++j)
748 if (value_notzero_p(coef[j]))
749 break;
751 return j;
754 #ifdef USE_MODULO
755 static void mask(Matrix *f, evalue *factor)
757 int nr = f->NbRows, nc = f->NbColumns;
758 int n;
759 bool found = false;
760 for (n = 0; n < nr && value_notzero_p(f->p[n][nc-1]); ++n)
761 if (value_notone_p(f->p[n][nc-1]) &&
762 value_notmone_p(f->p[n][nc-1]))
763 found = true;
764 if (!found)
765 return;
767 evalue EP;
768 nr = n;
770 Value m;
771 value_init(m);
773 evalue EV;
774 value_init(EV.d);
775 value_init(EV.x.n);
776 value_set_si(EV.x.n, 1);
778 for (n = 0; n < nr; ++n) {
779 value_assign(m, f->p[n][nc-1]);
780 if (value_one_p(m) || value_mone_p(m))
781 continue;
783 int j = normal_mod(f->p[n], nc-1, &m);
784 if (j == nc-1) {
785 free_evalue_refs(factor);
786 value_init(factor->d);
787 evalue_set_si(factor, 0, 1);
788 break;
790 vec_ZZ row;
791 values2zz(f->p[n], row, nc-1);
792 ZZ g;
793 value2zz(m, g);
794 if (j < (nc-1)-1 && row[j] > g/2) {
795 for (int k = j; k < (nc-1); ++k)
796 if (row[k] != 0)
797 row[k] = g - row[k];
800 value_init(EP.d);
801 value_set_si(EP.d, 0);
802 EP.x.p = new_enode(relation, 2, 0);
803 value_clear(EP.x.p->arr[1].d);
804 EP.x.p->arr[1] = *factor;
805 evalue *ev = &EP.x.p->arr[0];
806 value_set_si(ev->d, 0);
807 ev->x.p = new_enode(fractional, 3, -1);
808 evalue_set_si(&ev->x.p->arr[1], 0, 1);
809 evalue_set_si(&ev->x.p->arr[2], 1, 1);
810 evalue *E = multi_monom(row);
811 value_assign(EV.d, m);
812 emul(&EV, E);
813 value_clear(ev->x.p->arr[0].d);
814 ev->x.p->arr[0] = *E;
815 delete E;
816 *factor = EP;
819 value_clear(m);
820 free_evalue_refs(&EV);
822 #else
826 static void mask(Matrix *f, evalue *factor)
828 int nr = f->NbRows, nc = f->NbColumns;
829 int n;
830 bool found = false;
831 for (n = 0; n < nr && value_notzero_p(f->p[n][nc-1]); ++n)
832 if (value_notone_p(f->p[n][nc-1]) &&
833 value_notmone_p(f->p[n][nc-1]))
834 found = true;
835 if (!found)
836 return;
838 Value tmp;
839 value_init(tmp);
840 nr = n;
841 unsigned np = nc - 2;
842 Vector *lcm = Vector_Alloc(np);
843 Vector *val = Vector_Alloc(nc);
844 Vector_Set(val->p, 0, nc);
845 value_set_si(val->p[np], 1);
846 Vector_Set(lcm->p, 1, np);
847 for (n = 0; n < nr; ++n) {
848 if (value_one_p(f->p[n][nc-1]) ||
849 value_mone_p(f->p[n][nc-1]))
850 continue;
851 for (int j = 0; j < np; ++j)
852 if (value_notzero_p(f->p[n][j])) {
853 Gcd(f->p[n][j], f->p[n][nc-1], &tmp);
854 value_division(tmp, f->p[n][nc-1], tmp);
855 value_lcm(tmp, lcm->p[j], &lcm->p[j]);
858 evalue EP;
859 value_init(EP.d);
860 mask_r(f, nr, lcm, 0, val, &EP);
861 value_clear(tmp);
862 Vector_Free(val);
863 Vector_Free(lcm);
864 emul(&EP,factor);
865 free_evalue_refs(&EP);
867 #endif
869 struct term_info {
870 evalue *E;
871 ZZ constant;
872 ZZ coeff;
873 int pos;
876 static bool mod_needed(Polyhedron *PD, vec_ZZ& num, Value d, evalue *E)
878 Value *q = fixed_quotient(PD, num, d, false);
880 if (!q)
881 return true;
883 value_oppose(*q, *q);
884 evalue EV;
885 value_init(EV.d);
886 value_set_si(EV.d, 1);
887 value_init(EV.x.n);
888 value_multiply(EV.x.n, *q, d);
889 eadd(&EV, E);
890 free_evalue_refs(&EV);
891 value_clear(*q);
892 free(q);
893 return false;
896 static void ceil_mod(Value *coef, int len, Value d, ZZ& f, evalue *EP, Polyhedron *PD)
898 Value m;
899 value_init(m);
900 value_set_si(m, -1);
902 Vector_Scale(coef, coef, m, len);
904 value_assign(m, d);
905 int j = normal_mod(coef, len, &m);
907 if (j == len) {
908 value_clear(m);
909 return;
912 vec_ZZ num;
913 values2zz(coef, num, len);
915 ZZ g;
916 value2zz(m, g);
918 evalue tmp;
919 value_init(tmp.d);
920 evalue_set_si(&tmp, 0, 1);
922 int p = j;
923 if (g % 2 == 0)
924 while (j < len-1 && (num[j] == g/2 || num[j] == 0))
925 ++j;
926 if ((j < len-1 && num[j] > g/2) || (j == len-1 && num[j] >= (g+1)/2)) {
927 for (int k = j; k < len-1; ++k)
928 if (num[k] != 0)
929 num[k] = g - num[k];
930 num[len-1] = g - 1 - num[len-1];
931 value_assign(tmp.d, m);
932 ZZ t = f*(g-1);
933 zz2value(t, tmp.x.n);
934 eadd(&tmp, EP);
935 f = -f;
938 if (p >= len-1) {
939 ZZ t = num[len-1] * f;
940 zz2value(t, tmp.x.n);
941 value_assign(tmp.d, m);
942 eadd(&tmp, EP);
943 } else {
944 evalue *E = multi_monom(num);
945 evalue EV;
946 value_init(EV.d);
948 if (PD && !mod_needed(PD, num, m, E)) {
949 value_init(EV.x.n);
950 zz2value(f, EV.x.n);
951 value_assign(EV.d, m);
952 emul(&EV, E);
953 eadd(E, EP);
954 } else {
955 value_init(EV.x.n);
956 value_set_si(EV.x.n, 1);
957 value_assign(EV.d, m);
958 emul(&EV, E);
959 value_clear(EV.x.n);
960 value_set_si(EV.d, 0);
961 EV.x.p = new_enode(fractional, 3, -1);
962 evalue_copy(&EV.x.p->arr[0], E);
963 evalue_set_si(&EV.x.p->arr[1], 0, 1);
964 value_init(EV.x.p->arr[2].x.n);
965 zz2value(f, EV.x.p->arr[2].x.n);
966 value_set_si(EV.x.p->arr[2].d, 1);
968 eadd(&EV, EP);
971 free_evalue_refs(&EV);
972 free_evalue_refs(E);
973 delete E;
976 free_evalue_refs(&tmp);
978 out:
979 value_clear(m);
982 evalue* bv_ceil3(Value *coef, int len, Value d, Polyhedron *P)
984 Vector *val = Vector_Alloc(len);
986 Value t;
987 value_init(t);
988 value_set_si(t, -1);
989 Vector_Scale(coef, val->p, t, len);
990 value_absolute(t, d);
992 vec_ZZ num;
993 values2zz(val->p, num, len);
994 evalue *EP = multi_monom(num);
996 evalue tmp;
997 value_init(tmp.d);
998 value_init(tmp.x.n);
999 value_set_si(tmp.x.n, 1);
1000 value_assign(tmp.d, t);
1002 emul(&tmp, EP);
1004 ZZ one;
1005 one = 1;
1006 ceil_mod(val->p, len, t, one, EP, P);
1007 value_clear(t);
1009 /* copy EP to malloc'ed evalue */
1010 evalue *E;
1011 ALLOC(E);
1012 *E = *EP;
1013 delete EP;
1015 free_evalue_refs(&tmp);
1016 Vector_Free(val);
1018 return E;
1021 #ifdef USE_MODULO
1022 evalue* lattice_point(
1023 Polyhedron *i, vec_ZZ& lambda, Matrix *W, Value lcm, Polyhedron *PD)
1025 unsigned nparam = W->NbColumns - 1;
1027 Matrix* Rays = rays2(i);
1028 Matrix *T = Transpose(Rays);
1029 Matrix *T2 = Matrix_Copy(T);
1030 Matrix *inv = Matrix_Alloc(T2->NbRows, T2->NbColumns);
1031 int ok = Matrix_Inverse(T2, inv);
1032 assert(ok);
1033 Matrix_Free(Rays);
1034 Matrix_Free(T2);
1035 mat_ZZ vertex;
1036 matrix2zz(W, vertex, W->NbRows, W->NbColumns);
1038 vec_ZZ num;
1039 num = lambda * vertex;
1041 evalue *EP = multi_monom(num);
1043 evalue tmp;
1044 value_init(tmp.d);
1045 value_init(tmp.x.n);
1046 value_set_si(tmp.x.n, 1);
1047 value_assign(tmp.d, lcm);
1049 emul(&tmp, EP);
1051 Matrix *L = Matrix_Alloc(inv->NbRows, W->NbColumns);
1052 Matrix_Product(inv, W, L);
1054 mat_ZZ RT;
1055 matrix2zz(T, RT, T->NbRows, T->NbColumns);
1056 Matrix_Free(T);
1058 vec_ZZ p = lambda * RT;
1060 for (int i = 0; i < L->NbRows; ++i) {
1061 ceil_mod(L->p[i], nparam+1, lcm, p[i], EP, PD);
1064 Matrix_Free(L);
1066 Matrix_Free(inv);
1067 free_evalue_refs(&tmp);
1068 return EP;
1070 #else
1071 evalue* lattice_point(
1072 Polyhedron *i, vec_ZZ& lambda, Matrix *W, Value lcm, Polyhedron *PD)
1074 Matrix *T = Transpose(W);
1075 unsigned nparam = T->NbRows - 1;
1077 evalue *EP = new evalue();
1078 value_init(EP->d);
1079 evalue_set_si(EP, 0, 1);
1081 evalue ev;
1082 Vector *val = Vector_Alloc(nparam+1);
1083 value_set_si(val->p[nparam], 1);
1084 ZZ offset(INIT_VAL, 0);
1085 value_init(ev.d);
1086 vertex_period(i, lambda, T, lcm, 0, val, EP, &ev, offset);
1087 Vector_Free(val);
1088 eadd(&ev, EP);
1089 free_evalue_refs(&ev);
1091 Matrix_Free(T);
1093 reduce_evalue(EP);
1095 return EP;
1097 #endif
1099 void lattice_point(
1100 Param_Vertices* V, Polyhedron *i, vec_ZZ& lambda, term_info* term,
1101 Polyhedron *PD)
1103 unsigned nparam = V->Vertex->NbColumns - 2;
1104 unsigned dim = i->Dimension;
1105 mat_ZZ vertex;
1106 vertex.SetDims(V->Vertex->NbRows, nparam+1);
1107 Value lcm, tmp;
1108 value_init(lcm);
1109 value_init(tmp);
1110 value_set_si(lcm, 1);
1111 for (int j = 0; j < V->Vertex->NbRows; ++j) {
1112 value_lcm(lcm, V->Vertex->p[j][nparam+1], &lcm);
1114 if (value_notone_p(lcm)) {
1115 Matrix * mv = Matrix_Alloc(dim, nparam+1);
1116 for (int j = 0 ; j < dim; ++j) {
1117 value_division(tmp, lcm, V->Vertex->p[j][nparam+1]);
1118 Vector_Scale(V->Vertex->p[j], mv->p[j], tmp, nparam+1);
1121 term->E = lattice_point(i, lambda, mv, lcm, PD);
1122 term->constant = 0;
1124 Matrix_Free(mv);
1125 value_clear(lcm);
1126 value_clear(tmp);
1127 return;
1129 for (int i = 0; i < V->Vertex->NbRows; ++i) {
1130 assert(value_one_p(V->Vertex->p[i][nparam+1])); // for now
1131 values2zz(V->Vertex->p[i], vertex[i], nparam+1);
1134 vec_ZZ num;
1135 num = lambda * vertex;
1137 int p = -1;
1138 int nn = 0;
1139 for (int j = 0; j < nparam; ++j)
1140 if (num[j] != 0) {
1141 ++nn;
1142 p = j;
1144 if (nn >= 2) {
1145 term->E = multi_monom(num);
1146 term->constant = 0;
1147 } else {
1148 term->E = NULL;
1149 term->constant = num[nparam];
1150 term->pos = p;
1151 if (p != -1)
1152 term->coeff = num[p];
1155 value_clear(lcm);
1156 value_clear(tmp);
1159 void normalize(Polyhedron *i, vec_ZZ& lambda, ZZ& sign, ZZ& num, vec_ZZ& den)
1161 unsigned dim = i->Dimension;
1163 int r = 0;
1164 mat_ZZ rays;
1165 rays.SetDims(dim, dim);
1166 add_rays(rays, i, &r);
1167 den = rays * lambda;
1168 int change = 0;
1170 for (int j = 0; j < den.length(); ++j) {
1171 if (den[j] > 0)
1172 change ^= 1;
1173 else {
1174 den[j] = abs(den[j]);
1175 num += den[j];
1178 if (change)
1179 sign = -sign;
1182 void barvinok_count(Polyhedron *P, Value* result, unsigned NbMaxCons)
1184 Polyhedron ** vcone;
1185 vec_ZZ sign;
1186 int ncone = 0;
1187 sign.SetLength(ncone);
1188 unsigned dim;
1189 int allocated = 0;
1190 Value factor;
1191 Polyhedron *Q;
1192 int r = 0;
1194 if (emptyQ(P)) {
1195 value_set_si(*result, 0);
1196 return;
1198 if (P->NbBid == 0)
1199 for (; r < P->NbRays; ++r)
1200 if (value_zero_p(P->Ray[r][P->Dimension+1]))
1201 break;
1202 if (P->NbBid !=0 || r < P->NbRays) {
1203 value_set_si(*result, -1);
1204 return;
1206 if (P->NbEq != 0) {
1207 P = remove_equalities(P);
1208 if (emptyQ(P)) {
1209 Polyhedron_Free(P);
1210 value_set_si(*result, 0);
1211 return;
1213 allocated = 1;
1215 value_init(factor);
1216 value_set_si(factor, 1);
1217 Q = Polyhedron_Reduce(P, &factor);
1218 if (Q) {
1219 if (allocated)
1220 Polyhedron_Free(P);
1221 P = Q;
1222 allocated = 1;
1224 if (P->Dimension == 0) {
1225 value_assign(*result, factor);
1226 if (allocated)
1227 Polyhedron_Free(P);
1228 value_clear(factor);
1229 return;
1232 dim = P->Dimension;
1233 vcone = new (Polyhedron *)[P->NbRays];
1235 for (int j = 0; j < P->NbRays; ++j) {
1236 int npos, nneg;
1237 Polyhedron *C = supporting_cone(P, j);
1238 decompose(C, &vcone[j], &npos, &nneg, NbMaxCons);
1239 ncone += npos + nneg;
1240 sign.SetLength(ncone);
1241 for (int k = 0; k < npos; ++k)
1242 sign[ncone-nneg-k-1] = 1;
1243 for (int k = 0; k < nneg; ++k)
1244 sign[ncone-k-1] = -1;
1247 mat_ZZ rays;
1248 rays.SetDims(ncone * dim, dim);
1249 r = 0;
1250 for (int j = 0; j < P->NbRays; ++j) {
1251 for (Polyhedron *i = vcone[j]; i; i = i->next) {
1252 assert(i->NbRays-1 == dim);
1253 add_rays(rays, i, &r);
1256 vec_ZZ lambda;
1257 nonorthog(rays, lambda);
1259 vec_ZZ num;
1260 mat_ZZ den;
1261 num.SetLength(ncone);
1262 den.SetDims(ncone,dim);
1264 int f = 0;
1265 for (int j = 0; j < P->NbRays; ++j) {
1266 for (Polyhedron *i = vcone[j]; i; i = i->next) {
1267 lattice_point(P->Ray[j]+1, i, lambda, num[f]);
1268 normalize(i, lambda, sign[f], num[f], den[f]);
1269 ++f;
1272 ZZ min = num[0];
1273 for (int j = 1; j < num.length(); ++j)
1274 if (num[j] < min)
1275 min = num[j];
1276 for (int j = 0; j < num.length(); ++j)
1277 num[j] -= min;
1279 f = 0;
1280 mpq_t count;
1281 mpq_init(count);
1282 for (int j = 0; j < P->NbRays; ++j) {
1283 for (Polyhedron *i = vcone[j]; i; i = i->next) {
1284 dpoly d(dim, num[f]);
1285 dpoly n(dim, den[f][0], 1);
1286 for (int k = 1; k < dim; ++k) {
1287 dpoly fact(dim, den[f][k], 1);
1288 n *= fact;
1290 d.div(n, count, sign[f]);
1291 ++f;
1294 assert(value_one_p(&count[0]._mp_den));
1295 value_multiply(*result, &count[0]._mp_num, factor);
1296 mpq_clear(count);
1298 for (int j = 0; j < P->NbRays; ++j)
1299 Domain_Free(vcone[j]);
1301 delete [] vcone;
1303 if (allocated)
1304 Polyhedron_Free(P);
1305 value_clear(factor);
1308 static void uni_polynom(int param, Vector *c, evalue *EP)
1310 unsigned dim = c->Size-2;
1311 value_init(EP->d);
1312 value_set_si(EP->d,0);
1313 EP->x.p = new_enode(polynomial, dim+1, param+1);
1314 for (int j = 0; j <= dim; ++j)
1315 evalue_set(&EP->x.p->arr[j], c->p[j], c->p[dim+1]);
1318 static void multi_polynom(Vector *c, evalue* X, evalue *EP)
1320 unsigned dim = c->Size-2;
1321 evalue EC;
1323 value_init(EC.d);
1324 evalue_set(&EC, c->p[dim], c->p[dim+1]);
1326 value_init(EP->d);
1327 evalue_set(EP, c->p[dim], c->p[dim+1]);
1329 for (int i = dim-1; i >= 0; --i) {
1330 emul(X, EP);
1331 value_assign(EC.x.n, c->p[i]);
1332 eadd(&EC, EP);
1334 free_evalue_refs(&EC);
1337 Polyhedron *unfringe (Polyhedron *P, unsigned MaxRays)
1339 int len = P->Dimension+2;
1340 Polyhedron *T, *R = P;
1341 Value g;
1342 value_init(g);
1343 fprintf(stderr, "in");
1344 Polyhedron_Print(stderr, P_VALUE_FMT, P);
1345 Vector *row = Vector_Alloc(len);
1346 value_set_si(row->p[0], 1);
1348 R = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
1350 Matrix *M = Matrix_Alloc(2, len-1);
1351 value_set_si(M->p[1][len-2], 1);
1352 for (int v = 0; v < P->Dimension; ++v) {
1353 value_set_si(M->p[0][v], 1);
1354 Polyhedron *I = Polyhedron_Image(P, M, 2+1);
1355 Polyhedron_Print(stdout, P_VALUE_FMT, I);
1356 value_set_si(M->p[0][v], 0);
1357 for (int r = 0; r < I->NbConstraints; ++r) {
1358 if (value_zero_p(I->Constraint[r][0]))
1359 continue;
1360 if (value_zero_p(I->Constraint[r][1]))
1361 continue;
1362 if (value_one_p(I->Constraint[r][1]))
1363 continue;
1364 if (value_mone_p(I->Constraint[r][1]))
1365 continue;
1366 value_absolute(g, I->Constraint[r][1]);
1367 Vector_Set(row->p+1, 0, len-2);
1368 value_division(row->p[1+v], I->Constraint[r][1], g);
1369 mpz_fdiv_q(row->p[len-1], I->Constraint[r][2], g);
1370 puts("row");
1371 Vector_Print(stdout, P_VALUE_FMT, row);
1372 T = R;
1373 R = AddConstraints(row->p, 1, R, MaxRays);
1374 if (T != P)
1375 Polyhedron_Free(T);
1378 fprintf(stderr, "out");
1379 Polyhedron_Print(stderr, P_VALUE_FMT, R);
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(rVD);
1426 return 0;
1429 Value c;
1430 value_init(c);
1431 barvinok_count(rVD, &c, MaxRays);
1432 if (value_zero_p(c)) {
1433 Domain_Free(rVD);
1434 rVD = 0;
1436 value_clear(c);
1438 return rVD;
1441 evalue* barvinok_enumerate_ev(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1443 //P = unfringe(P, MaxRays);
1444 Polyhedron *CEq = NULL, *rVD, *pVD, *CA;
1445 Matrix *CT = NULL;
1446 Param_Polyhedron *PP = NULL;
1447 Param_Domain *D, *next;
1448 Param_Vertices *V;
1449 int r = 0;
1450 unsigned nparam = C->Dimension;
1451 evalue *eres;
1452 ALLOC(eres);
1453 value_init(eres->d);
1454 value_set_si(eres->d, 0);
1456 evalue factor;
1457 value_init(factor.d);
1458 evalue_set_si(&factor, 1, 1);
1460 CA = align_context(C, P->Dimension, MaxRays);
1461 P = DomainIntersection(P, CA, MaxRays);
1462 Polyhedron_Free(CA);
1464 if (C->Dimension == 0 || emptyQ(P)) {
1465 constant:
1466 eres->x.p = new_enode(partition, 2, -1);
1467 EVALUE_SET_DOMAIN(eres->x.p->arr[0],
1468 DomainConstraintSimplify(CEq ? CEq : Polyhedron_Copy(C), MaxRays));
1469 value_set_si(eres->x.p->arr[1].d, 1);
1470 value_init(eres->x.p->arr[1].x.n);
1471 if (emptyQ(P))
1472 value_set_si(eres->x.p->arr[1].x.n, 0);
1473 else
1474 barvinok_count(P, &eres->x.p->arr[1].x.n, MaxRays);
1475 out:
1476 emul(&factor, eres);
1477 reduce_evalue(eres);
1478 free_evalue_refs(&factor);
1479 Polyhedron_Free(P);
1480 if (CT)
1481 Matrix_Free(CT);
1482 if (PP)
1483 Param_Polyhedron_Free(PP);
1485 return eres;
1487 for (r = 0; r < P->NbRays; ++r)
1488 if (value_zero_p(P->Ray[r][0]) ||
1489 value_zero_p(P->Ray[r][P->Dimension+1])) {
1490 int i;
1491 for (i = P->Dimension - nparam; i < P->Dimension; ++i)
1492 if (value_notzero_p(P->Ray[r][i+1]))
1493 break;
1494 if (i >= P->Dimension)
1495 break;
1497 if (r < P->NbRays)
1498 goto constant;
1500 if (P->NbEq != 0) {
1501 Matrix *f;
1502 P = remove_equalities_p(P, P->Dimension-nparam, &f);
1503 mask(f, &factor);
1504 Matrix_Free(f);
1506 if (P->Dimension == nparam) {
1507 CEq = P;
1508 P = Universe_Polyhedron(0);
1509 goto constant;
1512 Polyhedron *Q = ParamPolyhedron_Reduce(P, P->Dimension-nparam, &factor);
1513 if (Q) {
1514 Polyhedron_Free(P);
1515 if (Q->Dimension == nparam) {
1516 CEq = Q;
1517 P = Universe_Polyhedron(0);
1518 goto constant;
1520 P = Q;
1522 Polyhedron *oldP = P;
1523 PP = Polyhedron2Param_SimplifiedDomain(&P,C,MaxRays,&CEq,&CT);
1524 if (P != oldP)
1525 Polyhedron_Free(oldP);
1527 if (isIdentity(CT)) {
1528 Matrix_Free(CT);
1529 CT = NULL;
1530 } else {
1531 assert(CT->NbRows != CT->NbColumns);
1532 if (CT->NbRows == 1) // no more parameters
1533 goto constant;
1534 nparam = CT->NbRows - 1;
1537 unsigned dim = P->Dimension - nparam;
1538 Polyhedron ** vcone = new (Polyhedron *)[PP->nbV];
1539 int * npos = new int[PP->nbV];
1540 int * nneg = new int[PP->nbV];
1541 vec_ZZ sign;
1543 int i;
1544 for (i = 0, V = PP->V; V; ++i, V = V->next) {
1545 Polyhedron *C = supporting_cone_p(P, V);
1546 decompose(C, &vcone[i], &npos[i], &nneg[i], MaxRays);
1549 Vector *c = Vector_Alloc(dim+2);
1551 int nd;
1552 for (nd = 0, D=PP->D; D; ++nd, D=D->next);
1553 struct section { Polyhedron *D; evalue E; };
1554 section *s = new section[nd];
1555 Polyhedron **fVD = new (Polyhedron*)[nd];
1557 for(nd = 0, D=PP->D; D; D=next) {
1558 next = D->next;
1560 Polyhedron *rVD = reduce_domain(D->Domain, CT, CEq,
1561 fVD, nd, MaxRays);
1562 if (!rVD)
1563 continue;
1565 pVD = CT ? DomainImage(rVD,CT,MaxRays) : rVD;
1567 int ncone = 0;
1568 sign.SetLength(ncone);
1569 FORALL_PVertex_in_ParamPolyhedron(V,D,PP) // _i is internal counter
1570 ncone += npos[_i] + nneg[_i];
1571 sign.SetLength(ncone);
1572 for (int k = 0; k < npos[_i]; ++k)
1573 sign[ncone-nneg[_i]-k-1] = 1;
1574 for (int k = 0; k < nneg[_i]; ++k)
1575 sign[ncone-k-1] = -1;
1576 END_FORALL_PVertex_in_ParamPolyhedron;
1578 mat_ZZ rays;
1579 rays.SetDims(ncone * dim, dim);
1580 r = 0;
1581 FORALL_PVertex_in_ParamPolyhedron(V,D,PP) // _i is internal counter
1582 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1583 assert(i->NbRays-1 == dim);
1584 add_rays(rays, i, &r);
1586 END_FORALL_PVertex_in_ParamPolyhedron;
1587 vec_ZZ lambda;
1588 nonorthog(rays, lambda);
1590 mat_ZZ den;
1591 den.SetDims(ncone,dim);
1592 term_info *num = new term_info[ncone];
1594 int f = 0;
1595 FORALL_PVertex_in_ParamPolyhedron(V,D,PP)
1596 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1597 lattice_point(V, i, lambda, &num[f], pVD);
1598 normalize(i, lambda, sign[f], num[f].constant, den[f]);
1599 ++f;
1601 END_FORALL_PVertex_in_ParamPolyhedron;
1602 ZZ min = num[0].constant;
1603 for (int j = 1; j < ncone; ++j)
1604 if (num[j].constant < min)
1605 min = num[j].constant;
1606 for (int j = 0; j < ncone; ++j)
1607 num[j].constant -= min;
1608 f = 0;
1609 value_init(s[nd].E.d);
1610 evalue_set_si(&s[nd].E, 0, 1);
1611 mpq_t count;
1612 mpq_init(count);
1613 FORALL_PVertex_in_ParamPolyhedron(V,D,PP)
1614 for (Polyhedron *i = vcone[_i]; i; i = i->next) {
1615 dpoly n(dim, den[f][0], 1);
1616 for (int k = 1; k < dim; ++k) {
1617 dpoly fact(dim, den[f][k], 1);
1618 n *= fact;
1620 if (num[f].E != NULL) {
1621 ZZ one(INIT_VAL, 1);
1622 dpoly_n d(dim, num[f].constant, one);
1623 d.div(n, c, sign[f]);
1624 evalue EV;
1625 multi_polynom(c, num[f].E, &EV);
1626 eadd(&EV , &s[nd].E);
1627 free_evalue_refs(&EV);
1628 free_evalue_refs(num[f].E);
1629 delete num[f].E;
1630 } else if (num[f].pos != -1) {
1631 dpoly_n d(dim, num[f].constant, num[f].coeff);
1632 d.div(n, c, sign[f]);
1633 evalue EV;
1634 uni_polynom(num[f].pos, c, &EV);
1635 eadd(&EV , &s[nd].E);
1636 free_evalue_refs(&EV);
1637 } else {
1638 mpq_set_si(count, 0, 1);
1639 dpoly d(dim, num[f].constant);
1640 d.div(n, count, sign[f]);
1641 evalue EV;
1642 value_init(EV.d);
1643 evalue_set(&EV, &count[0]._mp_num, &count[0]._mp_den);
1644 eadd(&EV , &s[nd].E);
1645 free_evalue_refs(&EV);
1647 ++f;
1649 END_FORALL_PVertex_in_ParamPolyhedron;
1651 mpq_clear(count);
1652 delete [] num;
1654 if (CT)
1655 addeliminatedparams_evalue(&s[nd].E, CT);
1656 s[nd].D = rVD;
1657 ++nd;
1658 if (rVD != pVD)
1659 Domain_Free(pVD);
1662 if (nd == 0)
1663 evalue_set_si(eres, 0, 1);
1664 else {
1665 eres->x.p = new_enode(partition, 2*nd, -1);
1666 for (int j = 0; j < nd; ++j) {
1667 EVALUE_SET_DOMAIN(eres->x.p->arr[2*j], s[j].D);
1668 value_clear(eres->x.p->arr[2*j+1].d);
1669 eres->x.p->arr[2*j+1] = s[j].E;
1670 Domain_Free(fVD[j]);
1673 delete [] s;
1674 delete [] fVD;
1676 Vector_Free(c);
1678 for (int j = 0; j < PP->nbV; ++j)
1679 Domain_Free(vcone[j]);
1680 delete [] vcone;
1681 delete [] npos;
1682 delete [] nneg;
1684 if (CEq)
1685 Polyhedron_Free(CEq);
1687 goto out;
1690 Enumeration* barvinok_enumerate(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1692 evalue *EP = barvinok_enumerate_ev(P, C, MaxRays);
1694 return partition2enumeration(EP);
1697 static void SwapColumns(Value **V, int n, int i, int j)
1699 for (int r = 0; r < n; ++r)
1700 value_swap(V[r][i], V[r][j]);
1703 static void SwapColumns(Polyhedron *P, int i, int j)
1705 SwapColumns(P->Constraint, P->NbConstraints, i, j);
1706 SwapColumns(P->Ray, P->NbRays, i, j);
1709 static bool SplitOnConstraint(Polyhedron *P, int i, int l, int u,
1710 int nvar, int len, int exist, int MaxRays,
1711 Vector *row, Value& f, bool independent,
1712 Polyhedron **pos, Polyhedron **neg)
1714 value_oppose(f, P->Constraint[u][nvar+i+1]);
1715 Vector_Combine(P->Constraint[l]+1, P->Constraint[u]+1,
1716 row->p+1,
1717 f, P->Constraint[l][nvar+i+1], len-1);
1719 //printf("l: %d, u: %d\n", l, u);
1720 value_multiply(f, f, P->Constraint[l][nvar+i+1]);
1721 value_substract(row->p[len-1], row->p[len-1], f);
1722 value_set_si(f, -1);
1723 Vector_Scale(row->p+1, row->p+1, f, len-1);
1724 value_decrement(row->p[len-1], row->p[len-1]);
1725 Vector_Gcd(row->p+1, len - 2, &f);
1726 if (value_notone_p(f)) {
1727 Vector_AntiScale(row->p+1, row->p+1, f, len-2);
1728 mpz_fdiv_q(row->p[len-1], row->p[len-1], f);
1730 *neg = AddConstraints(row->p, 1, P, MaxRays);
1732 /* We found an independent, but useless constraint
1733 * Maybe we should detect this earlier and not
1734 * mark the variable as INDEPENDENT
1736 if (emptyQ((*neg))) {
1737 Polyhedron_Free(*neg);
1738 return false;
1741 value_set_si(f, -1);
1742 Vector_Scale(row->p+1, row->p+1, f, len-1);
1743 value_decrement(row->p[len-1], row->p[len-1]);
1744 *pos = AddConstraints(row->p, 1, P, MaxRays);
1746 if (emptyQ((*pos))) {
1747 Polyhedron_Free(*neg);
1748 Polyhedron_Free(*pos);
1749 return false;
1752 return true;
1756 * unimodularly transform P such that constraint r is transformed
1757 * into a constraint that involves only a single (the first)
1758 * existential variable
1761 static Polyhedron *rotate_along(Polyhedron *P, int r, int nvar, int exist,
1762 unsigned MaxRays)
1764 Value g;
1765 value_init(g);
1767 Vector *row = Vector_Alloc(exist);
1768 Vector_Copy(P->Constraint[r]+1+nvar, row->p, exist);
1769 Vector_Gcd(row->p, exist, &g);
1770 if (value_notone_p(g))
1771 Vector_AntiScale(row->p, row->p, g, exist);
1772 value_clear(g);
1774 Matrix *M = unimodular_complete(row);
1775 Matrix *M2 = Matrix_Alloc(P->Dimension+1, P->Dimension+1);
1776 for (r = 0; r < nvar; ++r)
1777 value_set_si(M2->p[r][r], 1);
1778 for ( ; r < nvar+exist; ++r)
1779 Vector_Copy(M->p[r-nvar], M2->p[r]+nvar, exist);
1780 for ( ; r < P->Dimension+1; ++r)
1781 value_set_si(M2->p[r][r], 1);
1782 Polyhedron *T = Polyhedron_Image(P, M2, MaxRays);
1784 Matrix_Free(M2);
1785 Matrix_Free(M);
1786 Vector_Free(row);
1788 return T;
1791 static bool SplitOnVar(Polyhedron *P, int i,
1792 int nvar, int len, int exist, int MaxRays,
1793 Vector *row, Value& f, bool independent,
1794 Polyhedron **pos, Polyhedron **neg)
1796 int j;
1798 for (int l = P->NbEq; l < P->NbConstraints; ++l) {
1799 if (value_negz_p(P->Constraint[l][nvar+i+1]))
1800 continue;
1802 if (independent) {
1803 for (j = 0; j < exist; ++j)
1804 if (j != i && value_notzero_p(P->Constraint[l][nvar+j+1]))
1805 break;
1806 if (j < exist)
1807 continue;
1810 for (int u = P->NbEq; u < P->NbConstraints; ++u) {
1811 if (value_posz_p(P->Constraint[u][nvar+i+1]))
1812 continue;
1814 if (independent) {
1815 for (j = 0; j < exist; ++j)
1816 if (j != i && value_notzero_p(P->Constraint[u][nvar+j+1]))
1817 break;
1818 if (j < exist)
1819 continue;
1822 if (SplitOnConstraint(P, i, l, u,
1823 nvar, len, exist, MaxRays,
1824 row, f, independent,
1825 pos, neg)) {
1826 if (independent) {
1827 if (i != 0)
1828 SwapColumns(*neg, nvar+1, nvar+1+i);
1830 return true;
1835 return false;
1838 static bool double_bound_pair(Polyhedron *P, int nvar, int exist,
1839 int i, int l1, int l2,
1840 Polyhedron **pos, Polyhedron **neg)
1842 Value f;
1843 value_init(f);
1844 Vector *row = Vector_Alloc(P->Dimension+2);
1845 value_set_si(row->p[0], 1);
1846 value_oppose(f, P->Constraint[l1][nvar+i+1]);
1847 Vector_Combine(P->Constraint[l1]+1, P->Constraint[l2]+1,
1848 row->p+1,
1849 P->Constraint[l2][nvar+i+1], f,
1850 P->Dimension+1);
1851 ConstraintSimplify(row->p, row->p, P->Dimension+2, &f);
1852 *pos = AddConstraints(row->p, 1, P, 0);
1853 value_set_si(f, -1);
1854 Vector_Scale(row->p+1, row->p+1, f, P->Dimension+1);
1855 value_decrement(row->p[P->Dimension+1], row->p[P->Dimension+1]);
1856 *neg = AddConstraints(row->p, 1, P, 0);
1857 Vector_Free(row);
1858 value_clear(f);
1860 return !emptyQ((*pos)) && !emptyQ((*neg));
1863 static bool double_bound(Polyhedron *P, int nvar, int exist,
1864 Polyhedron **pos, Polyhedron **neg)
1866 for (int i = 0; i < exist; ++i) {
1867 int l1, l2;
1868 for (l1 = P->NbEq; l1 < P->NbConstraints; ++l1) {
1869 if (value_negz_p(P->Constraint[l1][nvar+i+1]))
1870 continue;
1871 for (l2 = l1 + 1; l2 < P->NbConstraints; ++l2) {
1872 if (value_negz_p(P->Constraint[l2][nvar+i+1]))
1873 continue;
1874 if (double_bound_pair(P, nvar, exist, i, l1, l2, pos, neg))
1875 return true;
1878 for (l1 = P->NbEq; l1 < P->NbConstraints; ++l1) {
1879 if (value_posz_p(P->Constraint[l1][nvar+i+1]))
1880 continue;
1881 if (l1 < P->NbConstraints)
1882 for (l2 = l1 + 1; l2 < P->NbConstraints; ++l2) {
1883 if (value_posz_p(P->Constraint[l2][nvar+i+1]))
1884 continue;
1885 if (double_bound_pair(P, nvar, exist, i, l1, l2, pos, neg))
1886 return true;
1889 return false;
1891 return false;
1894 enum constraint {
1895 ALL_POS = 1 << 0,
1896 ONE_NEG = 1 << 1,
1897 INDEPENDENT = 1 << 2,
1900 static evalue* enumerate_or(Polyhedron *pos, Polyhedron *neg,
1901 unsigned exist, unsigned nparam, unsigned MaxRays)
1903 #ifdef DEBUG_ER
1904 fprintf(stderr, "\nER: Or\n");
1905 #endif /* DEBUG_ER */
1907 evalue *EN =
1908 barvinok_enumerate_e(neg, exist, nparam, MaxRays);
1909 evalue *EP =
1910 barvinok_enumerate_e(pos, exist, nparam, MaxRays);
1911 evalue E;
1912 value_init(E.d);
1913 evalue_copy(&E, EP);
1914 eadd(EN, &E);
1915 emul(EN, EP);
1916 free_evalue_refs(EN);
1917 value_init(EN->d);
1918 evalue_set_si(EN, -1, 1);
1919 emul(EN, EP);
1920 eadd(&E, EP);
1922 free_evalue_refs(EN);
1923 free(EN);
1924 free_evalue_refs(&E);
1925 Polyhedron_Free(neg);
1926 Polyhedron_Free(pos);
1928 reduce_evalue(EP);
1930 return EP;
1933 static evalue* enumerate_sum(Polyhedron *P,
1934 unsigned exist, unsigned nparam, unsigned MaxRays)
1936 int nvar = P->Dimension - exist - nparam;
1937 int toswap = nvar < exist ? nvar : exist;
1938 for (int i = 0; i < toswap; ++i)
1939 SwapColumns(P, 1 + i, nvar+exist - i);
1940 nparam += nvar;
1942 #ifdef DEBUG_ER
1943 fprintf(stderr, "\nER: Sum\n");
1944 #endif /* DEBUG_ER */
1946 evalue *EP = barvinok_enumerate_e(P, exist, nparam, MaxRays);
1948 for (int i = 0; i < /* nvar */ nparam; ++i) {
1949 Matrix *C = Matrix_Alloc(1, 1 + nparam + 1);
1950 value_set_si(C->p[0][0], 1);
1951 evalue split;
1952 value_init(split.d);
1953 value_set_si(split.d, 0);
1954 split.x.p = new_enode(partition, 4, -1);
1955 value_set_si(C->p[0][1+i], 1);
1956 Matrix *C2 = Matrix_Copy(C);
1957 EVALUE_SET_DOMAIN(split.x.p->arr[0],
1958 Constraints2Polyhedron(C2, MaxRays));
1959 Matrix_Free(C2);
1960 evalue_set_si(&split.x.p->arr[1], 1, 1);
1961 value_set_si(C->p[0][1+i], -1);
1962 value_set_si(C->p[0][1+nparam], -1);
1963 EVALUE_SET_DOMAIN(split.x.p->arr[2],
1964 Constraints2Polyhedron(C, MaxRays));
1965 evalue_set_si(&split.x.p->arr[3], 1, 1);
1966 emul(&split, EP);
1967 free_evalue_refs(&split);
1968 Matrix_Free(C);
1970 reduce_evalue(EP);
1971 evalue_range_reduction(EP);
1973 evalue_frac2floor(EP);
1975 evalue *sum = esum(EP, nvar);
1977 free_evalue_refs(EP);
1978 free(EP);
1979 EP = sum;
1981 return EP;
1984 static evalue* enumerate_sure(Polyhedron *P,
1985 unsigned exist, unsigned nparam, unsigned MaxRays)
1987 int i;
1988 Polyhedron *S = P;
1989 int nvar = P->Dimension - exist - nparam;
1991 for (i = 0; i < exist; ++i) {
1992 Matrix *M = Matrix_Alloc(S->NbConstraints, S->Dimension+2);
1993 int c = 0;
1994 for (int j = 0; j < S->NbConstraints; ++j) {
1995 if (value_negz_p(S->Constraint[j][1+nvar+i]))
1996 continue;
1997 if (value_one_p(S->Constraint[j][1+nvar+i]))
1998 continue;
1999 Vector_Copy(S->Constraint[j], M->p[c], S->Dimension+2);
2000 value_substract(M->p[c][S->Dimension+1],
2001 M->p[c][S->Dimension+1],
2002 S->Constraint[j][1+nvar+i]);
2003 value_increment(M->p[c][S->Dimension+1],
2004 M->p[c][S->Dimension+1]);
2005 ++c;
2007 Polyhedron *O = S;
2008 S = AddConstraints(M->p[0], c, S, MaxRays);
2009 if (O != P)
2010 Polyhedron_Free(O);
2011 Matrix_Free(M);
2012 if (emptyQ(S)) {
2013 Polyhedron_Free(S);
2014 return 0;
2018 Matrix *M = Matrix_Alloc(exist, S->Dimension+2);
2019 for (i = 0; i < exist; ++i)
2020 value_set_si(M->p[i][nvar+i+1], 1);
2021 Polyhedron *O = S;
2022 S = DomainAddRays(S, M, MaxRays);
2023 Polyhedron_Free(O);
2024 Polyhedron *F = DomainAddRays(P, M, MaxRays);
2025 Polyhedron *D = DomainDifference(F, S, MaxRays);
2026 O = D;
2027 D = Disjoint_Domain(D, 0, MaxRays);
2028 Polyhedron_Free(F);
2029 Domain_Free(O);
2030 Matrix_Free(M);
2032 #ifdef DEBUG_ER
2033 fprintf(stderr, "\nER: Sure\n");
2034 #endif /* DEBUG_ER */
2036 M = Matrix_Alloc(P->Dimension+1-exist, P->Dimension+1);
2037 for (int j = 0; j < nvar; ++j)
2038 value_set_si(M->p[j][j], 1);
2039 for (int j = 0; j < nparam+1; ++j)
2040 value_set_si(M->p[nvar+j][nvar+exist+j], 1);
2041 Polyhedron *T = Polyhedron_Image(S, M, MaxRays);
2042 evalue *EP = barvinok_enumerate_e(T, 0, nparam, MaxRays);
2043 Polyhedron_Free(S);
2044 Polyhedron_Free(T);
2045 Matrix_Free(M);
2047 for (Polyhedron *Q = D; Q; Q = Q->next) {
2048 Polyhedron *N = Q->next;
2049 Q->next = 0;
2050 T = DomainIntersection(P, Q, MaxRays);
2051 evalue *E = barvinok_enumerate_e(T, exist, nparam, MaxRays);
2052 eadd(E, EP);
2053 free_evalue_refs(E);
2054 free(E);
2055 Polyhedron_Free(T);
2056 Q->next = N;
2058 Domain_Free(D);
2059 return EP;
2062 static evalue* new_zero_ep()
2064 evalue *EP;
2065 ALLOC(EP);
2066 value_init(EP->d);
2067 evalue_set_si(EP, 0, 1);
2068 return EP;
2071 static evalue* barvinok_enumerate_e_r(Polyhedron *P,
2072 unsigned exist, unsigned nparam, unsigned MaxRays);
2074 #ifdef DEBUG_ER
2075 static int er_level = 0;
2077 evalue* barvinok_enumerate_e(Polyhedron *P,
2078 unsigned exist, unsigned nparam, unsigned MaxRays)
2080 fprintf(stderr, "\nER: level %i\n", er_level);
2081 int nvar = P->Dimension - exist - nparam;
2082 fprintf(stderr, "%d %d %d\n", nvar, exist, nparam);
2084 Polyhedron_Print(stderr, P_VALUE_FMT, P);
2085 ++er_level;
2086 P = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
2087 evalue *EP = barvinok_enumerate_e_r(P, exist, nparam, MaxRays);
2088 Polyhedron_Free(P);
2089 --er_level;
2090 return EP;
2092 #else
2093 evalue* barvinok_enumerate_e(Polyhedron *P,
2094 unsigned exist, unsigned nparam, unsigned MaxRays)
2096 P = DomainConstraintSimplify(Polyhedron_Copy(P), MaxRays);
2097 evalue *EP = barvinok_enumerate_e_r(P, exist, nparam, MaxRays);
2098 Polyhedron_Free(P);
2099 return EP;
2101 #endif
2103 static evalue* barvinok_enumerate_e_r(Polyhedron *P,
2104 unsigned exist, unsigned nparam, unsigned MaxRays)
2106 if (exist == 0) {
2107 Polyhedron *U = Universe_Polyhedron(nparam);
2108 evalue *EP = barvinok_enumerate_ev(P, U, MaxRays);
2109 //char *param_name[] = {"P", "Q", "R", "S", "T" };
2110 //print_evalue(stdout, EP, param_name);
2111 Polyhedron_Free(U);
2112 return EP;
2115 int nvar = P->Dimension - exist - nparam;
2116 int len = P->Dimension + 2;
2118 if (emptyQ(P))
2119 return new_zero_ep();
2121 if (nvar == 0 && nparam == 0) {
2122 evalue *EP = new_zero_ep();
2123 barvinok_count(P, &EP->x.n, MaxRays);
2124 if (value_pos_p(EP->x.n))
2125 value_set_si(EP->x.n, 1);
2126 return EP;
2129 int r;
2130 for (r = 0; r < P->NbRays; ++r)
2131 if (value_zero_p(P->Ray[r][0]) ||
2132 value_zero_p(P->Ray[r][P->Dimension+1])) {
2133 int i;
2134 for (i = nvar; i < nvar + exist; ++i)
2135 if (value_notzero_p(P->Ray[r][i+1]))
2136 break;
2137 if (i >= nvar + exist)
2138 break;
2140 if (r < P->NbRays) {
2141 evalue *EP = new_zero_ep();
2142 value_set_si(EP->x.n, -1);
2143 return EP;
2146 int first;
2147 for (r = 0; r < P->NbEq; ++r)
2148 if ((first = First_Non_Zero(P->Constraint[r]+1+nvar, exist)) != -1)
2149 break;
2150 if (r < P->NbEq) {
2151 if (First_Non_Zero(P->Constraint[r]+1+nvar+first+1,
2152 exist-first-1) != -1) {
2153 Polyhedron *T = rotate_along(P, r, nvar, exist, MaxRays);
2154 #ifdef DEBUG_ER
2155 fprintf(stderr, "\nER: Equality\n");
2156 #endif /* DEBUG_ER */
2157 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2158 Polyhedron_Free(T);
2159 return EP;
2160 } else {
2161 #ifdef DEBUG_ER
2162 fprintf(stderr, "\nER: Fixed\n");
2163 #endif /* DEBUG_ER */
2164 if (first == 0)
2165 return barvinok_enumerate_e(P, exist-1, nparam, MaxRays);
2166 else {
2167 Polyhedron *T = Polyhedron_Copy(P);
2168 SwapColumns(T, nvar+1, nvar+1+first);
2169 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2170 Polyhedron_Free(T);
2171 return EP;
2176 Vector *row = Vector_Alloc(len);
2177 value_set_si(row->p[0], 1);
2179 Value f;
2180 value_init(f);
2182 enum constraint info[exist];
2183 for (int i = 0; i < exist; ++i) {
2184 info[i] = ALL_POS;
2185 for (int l = P->NbEq; l < P->NbConstraints; ++l) {
2186 if (value_negz_p(P->Constraint[l][nvar+i+1]))
2187 continue;
2188 for (int u = P->NbEq; u < P->NbConstraints; ++u) {
2189 if (value_posz_p(P->Constraint[u][nvar+i+1]))
2190 continue;
2191 value_oppose(f, P->Constraint[u][nvar+i+1]);
2192 Vector_Combine(P->Constraint[l]+1, P->Constraint[u]+1, row->p+1,
2193 f, P->Constraint[l][nvar+i+1], len-1);
2194 if (!(info[i] & INDEPENDENT)) {
2195 int j;
2196 for (j = 0; j < exist; ++j)
2197 if (j != i && value_notzero_p(row->p[nvar+j+1]))
2198 break;
2199 if (j == exist) {
2200 //printf("independent: i: %d, l: %d, u: %d\n", i, l, u);
2201 info[i] = (constraint)(info[i] | INDEPENDENT);
2204 if (info[i] & ALL_POS) {
2205 value_addto(row->p[len-1], row->p[len-1],
2206 P->Constraint[l][nvar+i+1]);
2207 value_addto(row->p[len-1], row->p[len-1], f);
2208 value_multiply(f, f, P->Constraint[l][nvar+i+1]);
2209 value_substract(row->p[len-1], row->p[len-1], f);
2210 value_decrement(row->p[len-1], row->p[len-1]);
2211 Vector_Gcd(row->p+1, len - 2, &f);
2212 if (value_notone_p(f)) {
2213 Vector_AntiScale(row->p+1, row->p+1, f, len-2);
2214 mpz_fdiv_q(row->p[len-1], row->p[len-1], f);
2216 value_set_si(f, -1);
2217 Vector_Scale(row->p+1, row->p+1, f, len-1);
2218 value_decrement(row->p[len-1], row->p[len-1]);
2219 Polyhedron *T = AddConstraints(row->p, 1, P, MaxRays);
2220 if (!emptyQ(T)) {
2221 //printf("not all_pos: i: %d, l: %d, u: %d\n", i, l, u);
2222 info[i] = (constraint)(info[i] ^ ALL_POS);
2224 //puts("pos remainder");
2225 //Polyhedron_Print(stdout, P_VALUE_FMT, T);
2226 Polyhedron_Free(T);
2228 if (!(info[i] & ONE_NEG)) {
2229 int j;
2230 for (j = 0; j < exist; ++j)
2231 if (j != i &&
2232 value_notzero_p(P->Constraint[l][nvar+j+1]))
2233 break;
2234 if (j != exist)
2235 for (j = 0; j < exist; ++j)
2236 if (j != i &&
2237 value_notzero_p(P->Constraint[u][nvar+j+1]))
2238 break;
2239 if (j == exist) {
2240 /* recalculate constant */
2241 /* We actually recalculate the whole row for
2242 * now, because it may have already been scaled
2244 value_oppose(f, P->Constraint[u][nvar+i+1]);
2245 Vector_Combine(P->Constraint[l]+1, P->Constraint[u]+1,
2246 row->p+1,
2247 f, P->Constraint[l][nvar+i+1], len-1);
2249 Vector_Combine(P->Constraint[l]+len-1,
2250 P->Constraint[u]+len-1, row->p+len-1,
2251 f, P->Constraint[l][nvar+i+1], 1);
2253 value_multiply(f, f, P->Constraint[l][nvar+i+1]);
2254 value_substract(row->p[len-1], row->p[len-1], f);
2255 value_set_si(f, -1);
2256 Vector_Scale(row->p+1, row->p+1, f, len-1);
2257 value_decrement(row->p[len-1], row->p[len-1]);
2258 Vector_Gcd(row->p+1, len - 2, &f);
2259 if (value_notone_p(f)) {
2260 Vector_AntiScale(row->p+1, row->p+1, f, len-2);
2261 mpz_fdiv_q(row->p[len-1], row->p[len-1], f);
2263 value_set_si(f, -1);
2264 Vector_Scale(row->p+1, row->p+1, f, len-1);
2265 value_decrement(row->p[len-1], row->p[len-1]);
2266 //puts("row");
2267 //Vector_Print(stdout, P_VALUE_FMT, row);
2268 Polyhedron *T = AddConstraints(row->p, 1, P, MaxRays);
2269 if (emptyQ(T)) {
2270 //printf("one_neg i: %d, l: %d, u: %d\n", i, l, u);
2271 info[i] = (constraint)(info[i] | ONE_NEG);
2273 //puts("neg remainder");
2274 //Polyhedron_Print(stdout, P_VALUE_FMT, T);
2275 Polyhedron_Free(T);
2278 if (!(info[i] & ALL_POS) && (info[i] & ONE_NEG))
2279 goto next;
2282 if (info[i] & ALL_POS)
2283 break;
2284 next:
2289 for (int i = 0; i < exist; ++i)
2290 printf("%i: %i\n", i, info[i]);
2292 for (int i = 0; i < exist; ++i)
2293 if (info[i] & ALL_POS) {
2294 #ifdef DEBUG_ER
2295 fprintf(stderr, "\nER: Positive\n");
2296 #endif /* DEBUG_ER */
2297 // Eliminate
2298 // Maybe we should chew off some of the fat here
2299 Matrix *M = Matrix_Alloc(P->Dimension, P->Dimension+1);
2300 for (int j = 0; j < P->Dimension; ++j)
2301 value_set_si(M->p[j][j + (j >= i+nvar)], 1);
2302 Polyhedron *T = Polyhedron_Image(P, M, MaxRays);
2303 Matrix_Free(M);
2304 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2305 Polyhedron_Free(T);
2306 value_clear(f);
2307 Vector_Free(row);
2308 return EP;
2310 for (int i = 0; i < exist; ++i)
2311 if (info[i] & ONE_NEG) {
2312 #ifdef DEBUG_ER
2313 fprintf(stderr, "\nER: Negative\n");
2314 #endif /* DEBUG_ER */
2315 Vector_Free(row);
2316 value_clear(f);
2317 if (i == 0)
2318 return barvinok_enumerate_e(P, exist-1, nparam, MaxRays);
2319 else {
2320 Polyhedron *T = Polyhedron_Copy(P);
2321 SwapColumns(T, nvar+1, nvar+1+i);
2322 evalue *EP = barvinok_enumerate_e(T, exist-1, nparam, MaxRays);
2323 Polyhedron_Free(T);
2324 return EP;
2327 for (int i = 0; i < exist; ++i)
2328 if (info[i] & INDEPENDENT) {
2329 Polyhedron *pos, *neg;
2331 /* Find constraint again and split off negative part */
2333 if (SplitOnVar(P, i, nvar, len, exist, MaxRays,
2334 row, f, true, &pos, &neg)) {
2335 #ifdef DEBUG_ER
2336 fprintf(stderr, "\nER: Split\n");
2337 #endif /* DEBUG_ER */
2339 evalue *EP =
2340 barvinok_enumerate_e(neg, exist-1, nparam, MaxRays);
2341 evalue *E =
2342 barvinok_enumerate_e(pos, exist, nparam, MaxRays);
2343 eadd(E, EP);
2344 free_evalue_refs(E);
2345 free(E);
2346 Polyhedron_Free(neg);
2347 Polyhedron_Free(pos);
2348 value_clear(f);
2349 Vector_Free(row);
2350 return EP;
2354 evalue *EP;
2355 EP = enumerate_sure(P, exist, nparam, MaxRays);
2356 if (EP)
2357 return EP;
2359 if (nvar != 0)
2360 return enumerate_sum(P, exist, nparam, MaxRays);
2362 assert(nvar == 0);
2364 int i;
2365 Polyhedron *pos, *neg;
2366 for (i = 0; i < exist; ++i)
2367 if (SplitOnVar(P, i, nvar, len, exist, MaxRays,
2368 row, f, false, &pos, &neg))
2369 break;
2371 assert (i < exist);
2373 EP = enumerate_or(pos, neg, exist, nparam, MaxRays);
2374 value_clear(f);
2375 Vector_Free(row);
2376 return EP;