update pet for rename of pet_scop_collect_* to pet_scop_get_*
[barvinok.git] / barvinok.cc
blob95265d635313d41893b7848dbd6feafa162e2859
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 <isl/map.h>
11 #include <isl_set_polylib.h>
12 #include <barvinok/util.h>
13 #include <barvinok/evalue.h>
14 #include "config.h"
15 #include <barvinok/barvinok.h>
16 #include <barvinok/genfun.h>
17 #include <barvinok/options.h>
18 #include <barvinok/sample.h>
19 #include "bfcounter.h"
20 #include "conversion.h"
21 #include "counter.h"
22 #include "decomposer.h"
23 #include "euler.h"
24 #include "lattice_point.h"
25 #include "laurent.h"
26 #include "reduce_domain.h"
27 #include "remove_equalities.h"
28 #include "scale.h"
29 #include "volume.h"
30 #include "bernoulli.h"
31 #include "param_util.h"
32 #include "summate.h"
34 using namespace NTL;
35 using std::cerr;
36 using std::cout;
37 using std::endl;
38 using std::vector;
39 using std::deque;
40 using std::string;
41 using std::ostringstream;
43 #define ALLOC(t,p) p = (t*)malloc(sizeof(*p))
45 class dpoly_n {
46 public:
47 Matrix *coeff;
48 ~dpoly_n() {
49 Matrix_Free(coeff);
51 dpoly_n(int d) {
52 Value d0, one;
53 value_init(d0);
54 value_init(one);
55 value_set_si(one, 1);
56 coeff = Matrix_Alloc(d+1, d+1+1);
57 value_set_si(coeff->p[0][0], 1);
58 value_set_si(coeff->p[0][d+1], 1);
59 for (int i = 1; i <= d; ++i) {
60 value_multiply(coeff->p[i][0], coeff->p[i-1][0], d0);
61 Vector_Combine(coeff->p[i-1], coeff->p[i-1]+1, coeff->p[i]+1,
62 one, d0, i);
63 value_set_si(coeff->p[i][d+1], i);
64 value_multiply(coeff->p[i][d+1], coeff->p[i][d+1], coeff->p[i-1][d+1]);
65 value_decrement(d0, d0);
67 value_clear(d0);
68 value_clear(one);
70 void div(dpoly& d, Vector *count, int sign) {
71 int len = coeff->NbRows;
72 Matrix * c = Matrix_Alloc(coeff->NbRows, coeff->NbColumns);
73 Value tmp;
74 value_init(tmp);
75 for (int i = 0; i < len; ++i) {
76 Vector_Copy(coeff->p[i], c->p[i], len+1);
77 for (int j = 1; j <= i; ++j) {
78 value_multiply(tmp, d.coeff->p[j], c->p[i][len]);
79 value_oppose(tmp, tmp);
80 Vector_Combine(c->p[i], c->p[i-j], c->p[i],
81 c->p[i-j][len], tmp, len);
82 value_multiply(c->p[i][len], c->p[i][len], c->p[i-j][len]);
84 value_multiply(c->p[i][len], c->p[i][len], d.coeff->p[0]);
86 if (sign == -1) {
87 value_set_si(tmp, -1);
88 Vector_Scale(c->p[len-1], count->p, tmp, len);
89 value_assign(count->p[len], c->p[len-1][len]);
90 } else
91 Vector_Copy(c->p[len-1], count->p, len+1);
92 Vector_Normalize(count->p, len+1);
93 value_clear(tmp);
94 Matrix_Free(c);
98 static void add_rays(mat_ZZ& rays, Polyhedron *i, int *r, int nvar = -1,
99 bool all = false)
101 unsigned dim = i->Dimension;
102 if (nvar == -1)
103 nvar = dim;
104 for (int k = 0; k < i->NbRays; ++k) {
105 if (!value_zero_p(i->Ray[k][dim+1]))
106 continue;
107 if (!all && nvar != dim && First_Non_Zero(i->Ray[k]+1, nvar) == -1)
108 continue;
109 values2zz(i->Ray[k]+1, rays[(*r)++], nvar);
113 struct bfe_term : public bfc_term_base {
114 vector<evalue *> factors;
116 bfe_term(int len) : bfc_term_base(len) {
119 ~bfe_term() {
120 for (int i = 0; i < factors.size(); ++i) {
121 if (!factors[i])
122 continue;
123 free_evalue_refs(factors[i]);
124 delete factors[i];
129 static void print_int_vector(int *v, int len, const char *name)
131 cerr << name << endl;
132 for (int j = 0; j < len; ++j) {
133 cerr << v[j] << " ";
135 cerr << endl;
138 static void print_bfc_terms(mat_ZZ& factors, bfc_vec& v)
140 cerr << endl;
141 cerr << "factors" << endl;
142 cerr << factors << endl;
143 for (int i = 0; i < v.size(); ++i) {
144 cerr << "term: " << i << endl;
145 print_int_vector(v[i]->powers, factors.NumRows(), "powers");
146 cerr << "terms" << endl;
147 cerr << v[i]->terms << endl;
148 bfc_term* bfct = static_cast<bfc_term *>(v[i]);
149 cerr << bfct->c << endl;
153 static void print_bfe_terms(mat_ZZ& factors, bfc_vec& v)
155 cerr << endl;
156 cerr << "factors" << endl;
157 cerr << factors << endl;
158 for (int i = 0; i < v.size(); ++i) {
159 cerr << "term: " << i << endl;
160 print_int_vector(v[i]->powers, factors.NumRows(), "powers");
161 cerr << "terms" << endl;
162 cerr << v[i]->terms << endl;
163 bfe_term* bfet = static_cast<bfe_term *>(v[i]);
164 for (int j = 0; j < v[i]->terms.NumRows(); ++j) {
165 const char * test[] = {"a", "b"};
166 print_evalue(stderr, bfet->factors[j], test);
167 fprintf(stderr, "\n");
172 struct bfcounter : public bfcounter_base {
173 mpq_t count;
174 Value tz;
176 bfcounter(unsigned dim) : bfcounter_base(dim) {
177 mpq_init(count);
178 lower = 1;
179 value_init(tz);
181 ~bfcounter() {
182 mpq_clear(count);
183 value_clear(tz);
185 virtual void base(mat_ZZ& factors, bfc_vec& v);
186 virtual void get_count(Value *result) {
187 assert(value_one_p(&count[0]._mp_den));
188 value_assign(*result, &count[0]._mp_num);
192 void bfcounter::base(mat_ZZ& factors, bfc_vec& v)
194 unsigned nf = factors.NumRows();
196 for (int i = 0; i < v.size(); ++i) {
197 bfc_term* bfct = static_cast<bfc_term *>(v[i]);
198 int total_power = 0;
199 // factor is always positive, so we always
200 // change signs
201 for (int k = 0; k < nf; ++k)
202 total_power += v[i]->powers[k];
204 int j;
205 for (j = 0; j < nf; ++j)
206 if (v[i]->powers[j] > 0)
207 break;
209 zz2value(factors[j][0], tz);
210 dpoly D(total_power, tz, 1);
211 for (int k = 1; k < v[i]->powers[j]; ++k) {
212 zz2value(factors[j][0], tz);
213 dpoly fact(total_power, tz, 1);
214 D *= fact;
216 for ( ; ++j < nf; )
217 for (int k = 0; k < v[i]->powers[j]; ++k) {
218 zz2value(factors[j][0], tz);
219 dpoly fact(total_power, tz, 1);
220 D *= fact;
223 for (int k = 0; k < v[i]->terms.NumRows(); ++k) {
224 zz2value(v[i]->terms[k][0], tz);
225 dpoly n(total_power, tz);
226 mpq_set_si(tcount, 0, 1);
227 n.div(D, tcount, 1);
228 if (total_power % 2)
229 bfct->c[k].n = -bfct->c[k].n;
230 zz2value(bfct->c[k].n, tn);
231 zz2value(bfct->c[k].d, td);
233 mpz_mul(mpq_numref(tcount), mpq_numref(tcount), tn);
234 mpz_mul(mpq_denref(tcount), mpq_denref(tcount), td);
235 mpq_canonicalize(tcount);
236 mpq_add(count, count, tcount);
238 delete v[i];
243 /* Check whether the polyhedron is unbounded and if so,
244 * check whether it has any (and therefore an infinite number of)
245 * integer points.
246 * If one of the vertices is integer, then we are done.
247 * Otherwise, transform the polyhedron such that one of the rays
248 * is the first unit vector and cut it off at a height that ensures
249 * that if the whole polyhedron has any points, then the remaining part
250 * has integer points. In particular we add the largest coefficient
251 * of a ray to the highest vertex (rounded up).
253 static bool Polyhedron_is_infinite(Polyhedron *P, Value* result,
254 barvinok_options *options)
256 int r = 0;
257 Matrix *M, *M2;
258 Value c, tmp;
259 Value g;
260 bool first;
261 Vector *v;
262 Value offset, size;
263 Polyhedron *R;
265 if (P->NbBid == 0)
266 for (; r < P->NbRays; ++r)
267 if (value_zero_p(P->Ray[r][P->Dimension+1]))
268 break;
269 if (P->NbBid == 0 && r == P->NbRays)
270 return false;
272 if (options->count_sample_infinite) {
273 Vector *sample;
275 sample = Polyhedron_Sample(P, options);
276 if (!sample)
277 value_set_si(*result, 0);
278 else {
279 value_set_si(*result, -1);
280 Vector_Free(sample);
282 return true;
285 for (int i = 0; i < P->NbRays; ++i)
286 if (value_one_p(P->Ray[i][1+P->Dimension])) {
287 value_set_si(*result, -1);
288 return true;
291 value_init(g);
292 M = Matrix_Alloc(P->Dimension+1, P->Dimension+1);
293 Vector_Gcd(P->Ray[r]+1, P->Dimension, &g);
294 Vector_AntiScale(P->Ray[r]+1, M->p[0], g, P->Dimension+1);
295 int ok = unimodular_complete(M, 1);
296 assert(ok);
297 value_set_si(M->p[P->Dimension][P->Dimension], 1);
298 M2 = Transpose(M);
299 Matrix_Free(M);
300 P = Polyhedron_Preimage(P, M2, 0);
301 Matrix_Free(M2);
302 value_clear(g);
304 first = true;
305 value_init(offset);
306 value_init(size);
307 value_init(tmp);
308 value_set_si(size, 0);
310 for (int i = 0; i < P->NbBid; ++i) {
311 value_absolute(tmp, P->Ray[i][1]);
312 if (value_gt(tmp, size))
313 value_assign(size, tmp);
315 for (int i = P->NbBid; i < P->NbRays; ++i) {
316 if (value_zero_p(P->Ray[i][P->Dimension+1])) {
317 if (value_gt(P->Ray[i][1], size))
318 value_assign(size, P->Ray[i][1]);
319 continue;
321 mpz_cdiv_q(tmp, P->Ray[i][1], P->Ray[i][P->Dimension+1]);
322 if (first || value_gt(tmp, offset)) {
323 value_assign(offset, tmp);
324 first = false;
327 value_addto(offset, offset, size);
328 value_clear(size);
329 value_clear(tmp);
331 v = Vector_Alloc(P->Dimension+2);
332 value_set_si(v->p[0], 1);
333 value_set_si(v->p[1], -1);
334 value_assign(v->p[1+P->Dimension], offset);
335 R = AddConstraints(v->p, 1, P, options->MaxRays);
336 Polyhedron_Free(P);
337 P = R;
339 value_clear(offset);
340 Vector_Free(v);
342 value_init(c);
343 barvinok_count_with_options(P, &c, options);
344 Polyhedron_Free(P);
345 if (value_zero_p(c))
346 value_set_si(*result, 0);
347 else
348 value_set_si(*result, -1);
349 value_clear(c);
351 return true;
354 static void evalue2value(evalue *e, Value *v)
356 if (EVALUE_IS_ZERO(*e)) {
357 value_set_si(*v, 0);
358 return;
361 if (value_notzero_p(e->d)) {
362 assert(value_one_p(e->d));
363 value_assign(*v, e->x.n);
364 return;
367 assert(e->x.p->type == partition);
368 assert(e->x.p->size == 2);
369 assert(EVALUE_DOMAIN(e->x.p->arr[0])->Dimension == 0);
370 evalue2value(&e->x.p->arr[1], v);
373 static void barvinok_count_f(Polyhedron *P, Value* result,
374 barvinok_options *options);
376 void barvinok_count_with_options(Polyhedron *P, Value* result,
377 struct barvinok_options *options)
379 unsigned dim;
380 int allocated = 0;
381 Polyhedron *Q;
382 bool infinite = false;
384 if (P->next)
385 fprintf(stderr,
386 "barvinok_count: input is a union; only first polyhedron is counted\n");
388 if (emptyQ2(P)) {
389 value_set_si(*result, 0);
390 return;
392 if (P->NbEq != 0) {
393 Q = NULL;
394 do {
395 P = remove_equalities(P, options->MaxRays);
396 if (P)
397 P = DomainConstraintSimplify(P, options->MaxRays);
398 if (Q)
399 Polyhedron_Free(Q);
400 Q = P;
401 } while (P && !emptyQ(P) && P->NbEq != 0);
402 if (!P || emptyQ(P)) {
403 Polyhedron_Free(P);
404 value_set_si(*result, 0);
405 return;
407 allocated = 1;
409 if (Polyhedron_is_infinite(P, result, options)) {
410 if (allocated)
411 Polyhedron_Free(P);
412 return;
414 if (P->Dimension == 0) {
415 /* Test whether the constraints are satisfied */
416 POL_ENSURE_VERTICES(P);
417 value_set_si(*result, !emptyQ(P));
418 if (allocated)
419 Polyhedron_Free(P);
420 return;
422 if (options->summation == BV_SUM_BERNOULLI) {
423 Polyhedron *C = Universe_Polyhedron(0);
424 evalue *sum = barvinok_summate_unweighted(P, C, options);
425 Polyhedron_Free(C);
426 evalue2value(sum, result);
427 evalue_free(sum);
428 return;
430 Q = Polyhedron_Factor(P, 0, NULL, options->MaxRays);
431 if (Q) {
432 if (allocated)
433 Polyhedron_Free(P);
434 P = Q;
435 allocated = 1;
438 barvinok_count_f(P, result, options);
439 if (value_neg_p(*result))
440 infinite = true;
441 if (Q && P->next && value_notzero_p(*result)) {
442 Value factor;
443 value_init(factor);
445 for (Q = P->next; Q; Q = Q->next) {
446 barvinok_count_f(Q, &factor, options);
447 if (value_neg_p(factor)) {
448 infinite = true;
449 continue;
450 } else if (Q->next && value_zero_p(factor)) {
451 value_set_si(*result, 0);
452 break;
454 value_multiply(*result, *result, factor);
457 value_clear(factor);
460 if (allocated)
461 Domain_Free(P);
462 if (infinite)
463 value_set_si(*result, -1);
466 void barvinok_count(Polyhedron *P, Value* result, unsigned NbMaxCons)
468 barvinok_options *options = barvinok_options_new_with_defaults();
469 options->MaxRays = NbMaxCons;
470 barvinok_count_with_options(P, result, options);
471 barvinok_options_free(options);
474 static void barvinok_count_f(Polyhedron *P, Value* result,
475 barvinok_options *options)
477 if (emptyQ2(P)) {
478 value_set_si(*result, 0);
479 return;
482 if (P->Dimension == 1)
483 return Line_Length(P, result);
485 int c = P->NbConstraints;
486 POL_ENSURE_FACETS(P);
487 if (c != P->NbConstraints || P->NbEq != 0) {
488 Polyhedron *next = P->next;
489 P->next = NULL;
490 barvinok_count_with_options(P, result, options);
491 P->next = next;
492 return;
495 POL_ENSURE_VERTICES(P);
497 if (Polyhedron_is_infinite(P, result, options))
498 return;
500 np_base *cnt;
501 if (options->incremental_specialization == BV_SPECIALIZATION_BF)
502 cnt = new bfcounter(P->Dimension);
503 else if (options->incremental_specialization == BV_SPECIALIZATION_DF)
504 cnt = new icounter(P->Dimension);
505 else if (options->incremental_specialization == BV_SPECIALIZATION_TODD)
506 cnt = new tcounter(P->Dimension, options->max_index);
507 else
508 cnt = new counter(P->Dimension, options->max_index);
509 cnt->start(P, options);
511 cnt->get_count(result);
512 delete cnt;
515 static void uni_polynom(int param, Vector *c, evalue *EP)
517 unsigned dim = c->Size-2;
518 value_init(EP->d);
519 value_set_si(EP->d,0);
520 EP->x.p = new_enode(polynomial, dim+1, param+1);
521 for (int j = 0; j <= dim; ++j)
522 evalue_set(&EP->x.p->arr[j], c->p[j], c->p[dim+1]);
525 typedef evalue * evalue_p;
527 struct enumerator_base {
528 unsigned dim;
529 evalue ** vE;
530 evalue mone;
531 vertex_decomposer *vpd;
533 enumerator_base(unsigned dim, vertex_decomposer *vpd)
535 this->dim = dim;
536 this->vpd = vpd;
538 vE = new evalue_p[vpd->PP->nbV];
539 for (int j = 0; j < vpd->PP->nbV; ++j)
540 vE[j] = 0;
542 value_init(mone.d);
543 evalue_set_si(&mone, -1, 1);
546 void decompose_at(Param_Vertices *V, int _i, barvinok_options *options) {
547 //this->pVD = pVD;
549 vE[_i] = new evalue;
550 value_init(vE[_i]->d);
551 evalue_set_si(vE[_i], 0, 1);
553 vpd->decompose_at_vertex(V, _i, options);
556 virtual ~enumerator_base() {
557 for (int j = 0; j < vpd->PP->nbV; ++j)
558 if (vE[j]) {
559 free_evalue_refs(vE[j]);
560 delete vE[j];
562 delete [] vE;
564 free_evalue_refs(&mone);
567 static enumerator_base *create(Polyhedron *P, unsigned dim,
568 Param_Polyhedron *PP,
569 barvinok_options *options);
572 struct enumerator : public signed_cone_consumer, public vertex_decomposer,
573 public enumerator_base {
574 vec_ZZ lambda;
575 vec_ZZ den;
576 term_info num;
577 Vector *c;
578 mpq_t count;
579 Value tz;
581 enumerator(Polyhedron *P, unsigned dim, Param_Polyhedron *PP) :
582 vertex_decomposer(PP, *this), enumerator_base(dim, this) {
583 randomvector(P, lambda, dim, 0);
584 den.SetLength(dim);
585 c = Vector_Alloc(dim+2);
587 mpq_init(count);
588 value_init(tz);
591 ~enumerator() {
592 mpq_clear(count);
593 Vector_Free(c);
594 value_clear(tz);
597 virtual void handle(const signed_cone& sc, barvinok_options *options);
600 void enumerator::handle(const signed_cone& sc, barvinok_options *options)
602 int sign = sc.sign;
603 int r = 0;
604 assert(sc.rays.NumRows() == dim);
605 for (int k = 0; k < dim; ++k) {
606 if (lambda * sc.rays[k] == 0)
607 throw Orthogonal;
610 lattice_point(V, sc.rays, lambda, &num, sc.det, options);
611 den = sc.rays * lambda;
613 if (dim % 2)
614 sign = -sign;
616 zz2value(den[0], tz);
617 dpoly n(dim, tz, 1);
618 for (int k = 1; k < dim; ++k) {
619 zz2value(den[k], tz);
620 dpoly fact(dim, tz, 1);
621 n *= fact;
623 if (num.E != NULL) {
624 dpoly_n d(dim);
625 d.div(n, c, sign);
626 for (unsigned long i = 0; i < sc.det; ++i) {
627 evalue *EV = evalue_polynomial(c, num.E[i]);
628 eadd(EV, vE[vert]);
629 evalue_free(EV);
630 evalue_free(num.E[i]);
632 delete [] num.E;
633 } else {
634 mpq_set_si(count, 0, 1);
635 if (num.constant.length() == 1) {
636 zz2value(num.constant[0], tz);
637 dpoly d(dim, tz);
638 d.div(n, count, sign);
639 } else {
640 dpoly_n d(dim);
641 d.div(n, c, sign);
642 Value x, sum, acc;
643 value_init(x);
644 value_init(acc);
645 for (unsigned long i = 0; i < sc.det; ++i) {
646 value_assign(acc, c->p[dim]);
647 zz2value(num.constant[i], x);
648 for (int j = dim-1; j >= 0; --j) {
649 value_multiply(acc, acc, x);
650 value_addto(acc, acc, c->p[j]);
652 value_addto(mpq_numref(count), mpq_numref(count), acc);
654 mpz_set(mpq_denref(count), c->p[dim+1]);
655 value_clear(acc);
656 value_clear(x);
658 evalue EV;
659 value_init(EV.d);
660 evalue_set(&EV, &count[0]._mp_num, &count[0]._mp_den);
661 eadd(&EV, vE[vert]);
662 free_evalue_refs(&EV);
666 struct ienumerator_base : enumerator_base {
667 evalue ** E_vertex;
669 ienumerator_base(unsigned dim, vertex_decomposer *vpd) :
670 enumerator_base(dim,vpd) {
671 E_vertex = new evalue_p[dim];
674 virtual ~ienumerator_base() {
675 delete [] E_vertex;
678 evalue *E_num(int i, int d) {
679 return E_vertex[i + (dim-d)];
683 struct cumulator {
684 evalue *factor;
685 evalue *v;
686 dpoly_r *r;
688 cumulator(evalue *factor, evalue *v, dpoly_r *r) :
689 factor(factor), v(v), r(r) {}
691 void cumulate(barvinok_options *options);
693 virtual void add_term(const vector<int>& powers, evalue *f2) = 0;
694 virtual ~cumulator() {}
697 void cumulator::cumulate(barvinok_options *options)
699 evalue cum; // factor * 1 * E_num[0]/1 * (E_num[0]-1)/2 *...
700 evalue f;
701 evalue t; // E_num[0] - (m-1)
702 evalue *cst;
703 evalue mone;
705 if (options->lookup_table) {
706 value_init(mone.d);
707 evalue_set_si(&mone, -1, 1);
710 value_init(cum.d);
711 evalue_copy(&cum, factor);
712 value_init(f.d);
713 value_init(f.x.n);
714 value_set_si(f.d, 1);
715 value_set_si(f.x.n, 1);
716 value_init(t.d);
717 evalue_copy(&t, v);
719 if (!options->lookup_table) {
720 for (cst = &t; value_zero_p(cst->d); ) {
721 if (cst->x.p->type == fractional)
722 cst = &cst->x.p->arr[1];
723 else
724 cst = &cst->x.p->arr[0];
728 for (int m = 0; m < r->len; ++m) {
729 if (m > 0) {
730 if (m > 1) {
731 value_set_si(f.d, m);
732 emul(&f, &cum);
733 if (!options->lookup_table)
734 value_subtract(cst->x.n, cst->x.n, cst->d);
735 else
736 eadd(&mone, &t);
738 emul(&t, &cum);
740 dpoly_r_term_list& current = r->c[r->len-1-m];
741 dpoly_r_term_list::iterator j;
742 for (j = current.begin(); j != current.end(); ++j) {
743 if ((*j)->coeff == 0)
744 continue;
745 evalue *f2 = new evalue;
746 value_init(f2->d);
747 value_init(f2->x.n);
748 zz2value((*j)->coeff, f2->x.n);
749 zz2value(r->denom, f2->d);
750 emul(&cum, f2);
752 add_term((*j)->powers, f2);
755 free_evalue_refs(&f);
756 free_evalue_refs(&t);
757 free_evalue_refs(&cum);
758 if (options->lookup_table)
759 free_evalue_refs(&mone);
762 struct E_poly_term {
763 vector<int> powers;
764 evalue *E;
767 struct ie_cum : public cumulator {
768 vector<E_poly_term *> terms;
770 ie_cum(evalue *factor, evalue *v, dpoly_r *r) : cumulator(factor, v, r) {}
772 virtual void add_term(const vector<int>& powers, evalue *f2);
775 void ie_cum::add_term(const vector<int>& powers, evalue *f2)
777 int k;
778 for (k = 0; k < terms.size(); ++k) {
779 if (terms[k]->powers == powers) {
780 eadd(f2, terms[k]->E);
781 free_evalue_refs(f2);
782 delete f2;
783 break;
786 if (k >= terms.size()) {
787 E_poly_term *ET = new E_poly_term;
788 ET->powers = powers;
789 ET->E = f2;
790 terms.push_back(ET);
794 struct ienumerator : public signed_cone_consumer, public vertex_decomposer,
795 public ienumerator_base {
796 //Polyhedron *pVD;
797 mat_ZZ den;
798 mat_ZZ vertex;
799 mpq_t tcount;
800 Value tz;
802 ienumerator(Polyhedron *P, unsigned dim, Param_Polyhedron *PP) :
803 vertex_decomposer(PP, *this), ienumerator_base(dim, this) {
804 vertex.SetDims(1, dim);
806 den.SetDims(dim, dim);
807 mpq_init(tcount);
808 value_init(tz);
811 ~ienumerator() {
812 mpq_clear(tcount);
813 value_clear(tz);
816 virtual void handle(const signed_cone& sc, barvinok_options *options);
817 void reduce(evalue *factor, const mat_ZZ& num, const mat_ZZ& den_f,
818 barvinok_options *options);
821 void ienumerator::reduce(evalue *factor, const mat_ZZ& num, const mat_ZZ& den_f,
822 barvinok_options *options)
824 unsigned len = den_f.NumRows(); // number of factors in den
825 unsigned dim = num.NumCols();
826 assert(num.NumRows() == 1);
828 if (dim == 0) {
829 eadd(factor, vE[vert]);
830 return;
833 vec_ZZ den_s;
834 mat_ZZ den_r;
835 vec_ZZ num_s;
836 mat_ZZ num_p;
838 split_one(num, num_s, num_p, den_f, den_s, den_r);
840 vec_ZZ den_p;
841 den_p.SetLength(len);
843 ZZ one;
844 one = 1;
845 normalize(one, num_s, num_p, den_s, den_p, den_r);
846 if (one != 1)
847 emul(&mone, factor);
849 int only_param = 0;
850 int no_param = 0;
851 for (int k = 0; k < len; ++k) {
852 if (den_p[k] == 0)
853 ++no_param;
854 else if (den_s[k] == 0)
855 ++only_param;
857 if (no_param == 0) {
858 reduce(factor, num_p, den_r, options);
859 } else {
860 int k, l;
861 mat_ZZ pden;
862 pden.SetDims(only_param, dim-1);
864 for (k = 0, l = 0; k < len; ++k)
865 if (den_s[k] == 0)
866 pden[l++] = den_r[k];
868 for (k = 0; k < len; ++k)
869 if (den_p[k] == 0)
870 break;
872 zz2value(num_s[0], tz);
873 dpoly n(no_param, tz);
874 zz2value(den_s[k], tz);
875 dpoly D(no_param, tz, 1);
876 for ( ; ++k < len; )
877 if (den_p[k] == 0) {
878 zz2value(den_s[k], tz);
879 dpoly fact(no_param, tz, 1);
880 D *= fact;
883 dpoly_r * r = 0;
884 // if no_param + only_param == len then all powers
885 // below will be all zero
886 if (no_param + only_param == len) {
887 if (E_num(0, dim) != 0)
888 r = new dpoly_r(n, len);
889 else {
890 mpq_set_si(tcount, 0, 1);
891 one = 1;
892 n.div(D, tcount, 1);
894 if (value_notzero_p(mpq_numref(tcount))) {
895 evalue f;
896 value_init(f.d);
897 value_init(f.x.n);
898 value_assign(f.x.n, mpq_numref(tcount));
899 value_assign(f.d, mpq_denref(tcount));
900 emul(&f, factor);
901 reduce(factor, num_p, pden, options);
902 free_evalue_refs(&f);
904 return;
906 } else {
907 for (k = 0; k < len; ++k) {
908 if (den_s[k] == 0 || den_p[k] == 0)
909 continue;
911 zz2value(den_s[k], tz);
912 dpoly pd(no_param-1, tz, 1);
914 int l;
915 for (l = 0; l < k; ++l)
916 if (den_r[l] == den_r[k])
917 break;
919 if (r == 0)
920 r = new dpoly_r(n, pd, l, len);
921 else {
922 dpoly_r *nr = new dpoly_r(r, pd, l, len);
923 delete r;
924 r = nr;
928 dpoly_r *rc = r->div(D);
929 delete r;
930 r = rc;
931 if (E_num(0, dim) == 0) {
932 int common = pden.NumRows();
933 dpoly_r_term_list& final = r->c[r->len-1];
934 int rows;
935 evalue t;
936 evalue f;
937 value_init(f.d);
938 value_init(f.x.n);
939 zz2value(r->denom, f.d);
940 dpoly_r_term_list::iterator j;
941 for (j = final.begin(); j != final.end(); ++j) {
942 if ((*j)->coeff == 0)
943 continue;
944 rows = common;
945 for (int k = 0; k < r->dim; ++k) {
946 int n = (*j)->powers[k];
947 if (n == 0)
948 continue;
949 pden.SetDims(rows+n, pden.NumCols());
950 for (int l = 0; l < n; ++l)
951 pden[rows+l] = den_r[k];
952 rows += n;
954 value_init(t.d);
955 evalue_copy(&t, factor);
956 zz2value((*j)->coeff, f.x.n);
957 emul(&f, &t);
958 reduce(&t, num_p, pden, options);
959 free_evalue_refs(&t);
961 free_evalue_refs(&f);
962 } else {
963 ie_cum cum(factor, E_num(0, dim), r);
964 cum.cumulate(options);
966 int common = pden.NumRows();
967 int rows;
968 for (int j = 0; j < cum.terms.size(); ++j) {
969 rows = common;
970 pden.SetDims(rows, pden.NumCols());
971 for (int k = 0; k < r->dim; ++k) {
972 int n = cum.terms[j]->powers[k];
973 if (n == 0)
974 continue;
975 pden.SetDims(rows+n, pden.NumCols());
976 for (int l = 0; l < n; ++l)
977 pden[rows+l] = den_r[k];
978 rows += n;
980 reduce(cum.terms[j]->E, num_p, pden, options);
981 free_evalue_refs(cum.terms[j]->E);
982 delete cum.terms[j]->E;
983 delete cum.terms[j];
986 delete r;
990 static int type_offset(enode *p)
992 return p->type == fractional ? 1 :
993 p->type == flooring ? 1 : 0;
996 static int edegree(evalue *e)
998 int d = 0;
999 enode *p;
1001 if (value_notzero_p(e->d))
1002 return 0;
1004 p = e->x.p;
1005 int i = type_offset(p);
1006 if (p->size-i-1 > d)
1007 d = p->size - i - 1;
1008 for (; i < p->size; i++) {
1009 int d2 = edegree(&p->arr[i]);
1010 if (d2 > d)
1011 d = d2;
1013 return d;
1016 void ienumerator::handle(const signed_cone& sc, barvinok_options *options)
1018 assert(sc.det == 1);
1019 assert(sc.rays.NumRows() == dim);
1021 lattice_point(V, sc.rays, vertex[0], E_vertex, options);
1023 den = sc.rays;
1025 evalue one;
1026 value_init(one.d);
1027 evalue_set_si(&one, sc.sign, 1);
1028 reduce(&one, vertex, den, options);
1029 free_evalue_refs(&one);
1031 for (int i = 0; i < dim; ++i)
1032 if (E_vertex[i])
1033 evalue_free(E_vertex[i]);
1036 struct bfenumerator : public vertex_decomposer, public bf_base,
1037 public ienumerator_base {
1038 evalue *factor;
1040 bfenumerator(Polyhedron *P, unsigned dim, Param_Polyhedron *PP) :
1041 vertex_decomposer(PP, *this),
1042 bf_base(dim), ienumerator_base(dim, this) {
1043 lower = 0;
1044 factor = NULL;
1047 ~bfenumerator() {
1050 virtual void handle(const signed_cone& sc, barvinok_options *options);
1051 virtual void base(mat_ZZ& factors, bfc_vec& v);
1053 bfc_term_base* new_bf_term(int len) {
1054 bfe_term* t = new bfe_term(len);
1055 return t;
1058 virtual void set_factor(bfc_term_base *t, int k, int change) {
1059 bfe_term* bfet = static_cast<bfe_term *>(t);
1060 factor = bfet->factors[k];
1061 assert(factor != NULL);
1062 bfet->factors[k] = NULL;
1063 if (change)
1064 emul(&mone, factor);
1067 virtual void set_factor(bfc_term_base *t, int k, mpq_t &q, int change) {
1068 bfe_term* bfet = static_cast<bfe_term *>(t);
1069 factor = bfet->factors[k];
1070 assert(factor != NULL);
1071 bfet->factors[k] = NULL;
1073 evalue f;
1074 value_init(f.d);
1075 value_init(f.x.n);
1076 if (change)
1077 value_oppose(f.x.n, mpq_numref(q));
1078 else
1079 value_assign(f.x.n, mpq_numref(q));
1080 value_assign(f.d, mpq_denref(q));
1081 emul(&f, factor);
1082 free_evalue_refs(&f);
1085 virtual void set_factor(bfc_term_base *t, int k, const QQ& c, int change) {
1086 bfe_term* bfet = static_cast<bfe_term *>(t);
1088 factor = new evalue;
1090 evalue f;
1091 value_init(f.d);
1092 value_init(f.x.n);
1093 zz2value(c.n, f.x.n);
1094 if (change)
1095 value_oppose(f.x.n, f.x.n);
1096 zz2value(c.d, f.d);
1098 value_init(factor->d);
1099 evalue_copy(factor, bfet->factors[k]);
1100 emul(&f, factor);
1101 free_evalue_refs(&f);
1104 void set_factor(evalue *f, int change) {
1105 if (change)
1106 emul(&mone, f);
1107 factor = f;
1110 virtual void insert_term(bfc_term_base *t, int i) {
1111 bfe_term* bfet = static_cast<bfe_term *>(t);
1112 int len = t->terms.NumRows()-1; // already increased by one
1114 bfet->factors.resize(len+1);
1115 for (int j = len; j > i; --j) {
1116 bfet->factors[j] = bfet->factors[j-1];
1117 t->terms[j] = t->terms[j-1];
1119 bfet->factors[i] = factor;
1120 factor = NULL;
1123 virtual void update_term(bfc_term_base *t, int i) {
1124 bfe_term* bfet = static_cast<bfe_term *>(t);
1126 eadd(factor, bfet->factors[i]);
1127 free_evalue_refs(factor);
1128 delete factor;
1131 virtual bool constant_vertex(int dim) { return E_num(0, dim) == 0; }
1133 virtual void cum(bf_reducer *bfr, bfc_term_base *t, int k, dpoly_r *r,
1134 barvinok_options *options);
1137 enumerator_base *enumerator_base::create(Polyhedron *P, unsigned dim,
1138 Param_Polyhedron *PP,
1139 barvinok_options *options)
1141 enumerator_base *eb;
1143 if (options->incremental_specialization == BV_SPECIALIZATION_BF)
1144 eb = new bfenumerator(P, dim, PP);
1145 else if (options->incremental_specialization == BV_SPECIALIZATION_DF)
1146 eb = new ienumerator(P, dim, PP);
1147 else
1148 eb = new enumerator(P, dim, PP);
1150 return eb;
1153 struct bfe_cum : public cumulator {
1154 bfenumerator *bfe;
1155 bfc_term_base *told;
1156 int k;
1157 bf_reducer *bfr;
1159 bfe_cum(evalue *factor, evalue *v, dpoly_r *r, bf_reducer *bfr,
1160 bfc_term_base *t, int k, bfenumerator *e) :
1161 cumulator(factor, v, r), told(t), k(k),
1162 bfr(bfr), bfe(e) {
1165 virtual void add_term(const vector<int>& powers, evalue *f2);
1168 void bfe_cum::add_term(const vector<int>& powers, evalue *f2)
1170 bfr->update_powers(powers);
1172 bfc_term_base * t = bfe->find_bfc_term(bfr->vn, bfr->npowers, bfr->nnf);
1173 bfe->set_factor(f2, bfr->l_changes % 2);
1174 bfe->add_term(t, told->terms[k], bfr->l_extra_num);
1177 void bfenumerator::cum(bf_reducer *bfr, bfc_term_base *t, int k,
1178 dpoly_r *r, barvinok_options *options)
1180 bfe_term* bfet = static_cast<bfe_term *>(t);
1181 bfe_cum cum(bfet->factors[k], E_num(0, bfr->d), r, bfr, t, k, this);
1182 cum.cumulate(options);
1185 void bfenumerator::base(mat_ZZ& factors, bfc_vec& v)
1187 for (int i = 0; i < v.size(); ++i) {
1188 assert(v[i]->terms.NumRows() == 1);
1189 evalue *factor = static_cast<bfe_term *>(v[i])->factors[0];
1190 eadd(factor, vE[vert]);
1191 delete v[i];
1195 void bfenumerator::handle(const signed_cone& sc, barvinok_options *options)
1197 assert(sc.det == 1);
1198 assert(sc.rays.NumRows() == enumerator_base::dim);
1200 bfe_term* t = new bfe_term(enumerator_base::dim);
1201 vector< bfc_term_base * > v;
1202 v.push_back(t);
1204 t->factors.resize(1);
1206 t->terms.SetDims(1, enumerator_base::dim);
1207 lattice_point(V, sc.rays, t->terms[0], E_vertex, options);
1209 // the elements of factors are always lexpositive
1210 mat_ZZ factors;
1211 int s = setup_factors(sc.rays, factors, t, sc.sign);
1213 t->factors[0] = new evalue;
1214 value_init(t->factors[0]->d);
1215 evalue_set_si(t->factors[0], s, 1);
1216 reduce(factors, v, options);
1218 for (int i = 0; i < enumerator_base::dim; ++i)
1219 if (E_vertex[i])
1220 evalue_free(E_vertex[i]);
1223 static evalue* barvinok_enumerate_ev_f(Polyhedron *P, Polyhedron* C,
1224 barvinok_options *options);
1226 /* Destroys C */
1227 static evalue* barvinok_enumerate_cst(Polyhedron *P, Polyhedron* C,
1228 struct barvinok_options *options)
1230 evalue *eres;
1232 if (emptyQ2(C)) {
1233 Polyhedron_Free(C);
1234 return evalue_zero();
1237 ALLOC(evalue, eres);
1238 value_init(eres->d);
1239 value_set_si(eres->d, 0);
1240 eres->x.p = new_enode(partition, 2, C->Dimension);
1241 EVALUE_SET_DOMAIN(eres->x.p->arr[0],
1242 DomainConstraintSimplify(C, options->MaxRays));
1243 value_set_si(eres->x.p->arr[1].d, 1);
1244 value_init(eres->x.p->arr[1].x.n);
1245 if (emptyQ2(P))
1246 value_set_si(eres->x.p->arr[1].x.n, 0);
1247 else
1248 barvinok_count_with_options(P, &eres->x.p->arr[1].x.n, options);
1249 if (value_mone_p(eres->x.p->arr[1].x.n)) {
1250 value_clear(eres->x.p->arr[1].x.n);
1251 value_set_si(eres->x.p->arr[1].d, -2); /* NaN */
1254 return eres;
1257 static evalue* enumerate(Polyhedron *P, Polyhedron* C,
1258 struct barvinok_options *options)
1260 Polyhedron *next;
1261 Polyhedron *Porig = P;
1262 Polyhedron *Corig = C;
1263 Polyhedron *CEq = NULL, *rVD;
1264 int r = 0;
1265 unsigned nparam = C->Dimension;
1266 evalue *eres;
1267 Matrix *CP = NULL;
1269 evalue factor;
1270 value_init(factor.d);
1271 evalue_set_si(&factor, 1, 1);
1273 /* for now */
1274 POL_ENSURE_FACETS(P);
1275 POL_ENSURE_VERTICES(P);
1276 POL_ENSURE_FACETS(C);
1277 POL_ENSURE_VERTICES(C);
1279 if (C->Dimension == 0 || emptyQ(P) || emptyQ(C)) {
1280 constant:
1281 if (CEq == Porig)
1282 CEq = Polyhedron_Copy(CEq);
1283 eres = barvinok_enumerate_cst(P, CEq ? CEq : Polyhedron_Copy(C), options);
1284 out:
1285 if (CP) {
1286 evalue_backsubstitute(eres, CP, options->MaxRays);
1287 Matrix_Free(CP);
1290 emul(&factor, eres);
1291 if (options->approx->method == BV_APPROX_DROP) {
1292 if (options->approx->approximation == BV_APPROX_SIGN_UPPER)
1293 evalue_frac2polynomial(eres, 1, options->MaxRays);
1294 if (options->approx->approximation == BV_APPROX_SIGN_LOWER)
1295 evalue_frac2polynomial(eres, -1, options->MaxRays);
1296 if (options->approx->approximation == BV_APPROX_SIGN_APPROX)
1297 evalue_frac2polynomial(eres, 0, options->MaxRays);
1299 reduce_evalue(eres);
1300 free_evalue_refs(&factor);
1301 if (P != Porig)
1302 Domain_Free(P);
1303 if (C != Corig)
1304 Polyhedron_Free(C);
1306 return eres;
1308 if (Polyhedron_is_unbounded(P, nparam, options->MaxRays))
1309 goto constant;
1311 if (P->Dimension == nparam) {
1312 CEq = DomainIntersection(P, C, options->MaxRays);
1313 P = Universe_Polyhedron(0);
1314 goto constant;
1316 if (P->NbEq != 0 || C->NbEq != 0) {
1317 Polyhedron *Q = P;
1318 Polyhedron *D = C;
1319 remove_all_equalities(&P, &C, &CP, NULL, nparam, options->MaxRays);
1320 if (C != D && D != Corig)
1321 Polyhedron_Free(D);
1322 if (P != Q && Q != Porig)
1323 Domain_Free(Q);
1324 eres = enumerate(P, C, options);
1325 goto out;
1328 Polyhedron *T = Polyhedron_Factor(P, nparam, NULL, options->MaxRays);
1329 if (T || (P->Dimension == nparam+1)) {
1330 Polyhedron *C2 = C;
1331 Polyhedron *FC = Factor_Context(T ? T : P, nparam, options->MaxRays);
1332 C = DomainIntersection(C, FC, options->MaxRays);
1333 if (C2 != Corig)
1334 Polyhedron_Free(C2);
1335 Polyhedron_Free(FC);
1337 if (T) {
1338 if (P != Porig)
1339 Polyhedron_Free(P);
1340 P = T;
1341 if (T->Dimension == C->Dimension) {
1342 P = T->next;
1343 T->next = NULL;
1344 Polyhedron_Free(T);
1348 next = P->next;
1349 P->next = NULL;
1350 eres = barvinok_enumerate_ev_f(P, C, options);
1351 P->next = next;
1353 if (P->next) {
1354 Polyhedron *Q;
1355 evalue *f;
1357 for (Q = P->next; Q; Q = Q->next) {
1358 Polyhedron *next = Q->next;
1359 Q->next = NULL;
1361 f = barvinok_enumerate_ev_f(Q, C, options);
1362 emul(f, eres);
1363 evalue_free(f);
1365 Q->next = next;
1369 goto out;
1372 evalue* barvinok_enumerate_with_options(Polyhedron *P, Polyhedron* C,
1373 struct barvinok_options *options)
1375 Polyhedron *next, *Cnext, *C1;
1376 Polyhedron *Corig = C;
1377 evalue *eres;
1379 if (P->next)
1380 fprintf(stderr,
1381 "barvinok_enumerate: input is a union; only first polyhedron is enumerated\n");
1383 if (C->next)
1384 fprintf(stderr,
1385 "barvinok_enumerate: context is a union; only first polyhedron is considered\n");
1387 Cnext = C->next;
1388 C->next = NULL;
1389 C1 = Polyhedron_Project(P, C->Dimension);
1390 C = DomainIntersection(C, C1, options->MaxRays);
1391 Polyhedron_Free(C1);
1392 next = P->next;
1393 P->next = NULL;
1395 if (options->approx->method == BV_APPROX_BERNOULLI ||
1396 options->summation == BV_SUM_BERNOULLI) {
1397 int summation = options->summation;
1398 options->summation = BV_SUM_BERNOULLI;
1399 eres = barvinok_summate_unweighted(P, C, options);
1400 options->summation = summation;
1401 } else
1402 eres = enumerate(P, C, options);
1403 Domain_Free(C);
1405 P->next= next;
1406 Corig->next = Cnext;
1408 return eres;
1411 evalue* barvinok_enumerate_ev(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1413 evalue *E;
1414 barvinok_options *options = barvinok_options_new_with_defaults();
1415 options->MaxRays = MaxRays;
1416 E = barvinok_enumerate_with_options(P, C, options);
1417 barvinok_options_free(options);
1418 return E;
1421 evalue *Param_Polyhedron_Enumerate(Param_Polyhedron *PP, Polyhedron *P,
1422 Polyhedron *C,
1423 struct barvinok_options *options)
1425 evalue *eres;
1426 Param_Domain *D;
1427 unsigned nparam = C->Dimension;
1428 unsigned dim = P->Dimension - nparam;
1430 int nd;
1431 for (nd = 0, D=PP->D; D; ++nd, D=D->next);
1432 evalue_section *s = new evalue_section[nd];
1434 enumerator_base *et = NULL;
1435 try_again:
1436 if (et)
1437 delete et;
1439 et = enumerator_base::create(P, dim, PP, options);
1441 Polyhedron *TC = true_context(P, C, options->MaxRays);
1442 FORALL_REDUCED_DOMAIN(PP, TC, nd, options, i, D, rVD)
1443 Param_Vertices *V;
1445 s[i].E = evalue_zero();
1446 s[i].D = rVD;
1448 FORALL_PVertex_in_ParamPolyhedron(V,D,PP) // _i is internal counter
1449 if (!et->vE[_i])
1450 try {
1451 et->decompose_at(V, _i, options);
1452 } catch (OrthogonalException &e) {
1453 FORALL_REDUCED_DOMAIN_RESET;
1454 for (; i >= 0; --i) {
1455 evalue_free(s[i].E);
1456 Domain_Free(s[i].D);
1458 goto try_again;
1460 eadd(et->vE[_i] , s[i].E);
1461 END_FORALL_PVertex_in_ParamPolyhedron;
1462 evalue_range_reduction_in_domain(s[i].E, rVD);
1463 END_FORALL_REDUCED_DOMAIN
1464 Polyhedron_Free(TC);
1466 delete et;
1467 eres = evalue_from_section_array(s, nd);
1468 delete [] s;
1470 return eres;
1473 static evalue* barvinok_enumerate_ev_f(Polyhedron *P, Polyhedron* C,
1474 barvinok_options *options)
1476 unsigned nparam = C->Dimension;
1477 bool do_scale = options->approx->method == BV_APPROX_SCALE;
1479 if (options->summation == BV_SUM_EULER)
1480 return barvinok_summate_unweighted(P, C, options);
1482 if (options->approx->method == BV_APPROX_VOLUME)
1483 return Param_Polyhedron_Volume(P, C, options);
1485 if (P->Dimension - nparam == 1 && !do_scale)
1486 return ParamLine_Length(P, C, options);
1488 Param_Polyhedron *PP = NULL;
1489 evalue *eres;
1491 if (do_scale) {
1492 eres = scale_bound(P, C, options);
1493 if (eres)
1494 return eres;
1497 PP = Polyhedron2Param_Polyhedron(P, C, options);
1499 if (do_scale)
1500 eres = scale(PP, P, C, options);
1501 else
1502 eres = Param_Polyhedron_Enumerate(PP, P, C, options);
1504 if (PP)
1505 Param_Polyhedron_Free(PP);
1507 return eres;
1510 Enumeration* barvinok_enumerate(Polyhedron *P, Polyhedron* C, unsigned MaxRays)
1512 evalue *EP = barvinok_enumerate_ev(P, C, MaxRays);
1514 return partition2enumeration(EP);
1517 evalue* barvinok_enumerate_union(Polyhedron *D, Polyhedron* C, unsigned MaxRays)
1519 evalue *EP;
1520 gen_fun *gf = barvinok_enumerate_union_series(D, C, MaxRays);
1521 EP = *gf;
1522 delete gf;
1523 return EP;
1526 static __isl_give isl_pw_qpolynomial *basic_set_card(
1527 __isl_take isl_basic_set *bset)
1529 isl_ctx *ctx;
1530 isl_space *dim;
1531 isl_pw_qpolynomial *pwqp;
1532 unsigned nparam = isl_basic_set_dim(bset, isl_dim_param);
1533 Polyhedron *U = Universe_Polyhedron(nparam);
1534 Polyhedron *P;
1535 evalue *E;
1536 barvinok_options *options;
1537 int options_allocated = 0;
1539 ctx = isl_basic_set_get_ctx(bset);
1540 options = isl_ctx_peek_barvinok_options(ctx);
1541 if (!options) {
1542 options = barvinok_options_new_with_defaults();
1543 options_allocated = 1;
1546 dim = isl_basic_set_get_space(bset);
1547 dim = isl_space_domain(dim);
1549 P = isl_basic_set_to_polylib(bset);
1550 E = enumerate(P, U, options);
1552 pwqp = isl_pw_qpolynomial_from_evalue(dim, E);
1553 isl_basic_set_free(bset);
1555 evalue_free(E);
1556 Polyhedron_Free(P);
1557 Polyhedron_Free(U);
1558 if (options_allocated)
1559 barvinok_options_free(options);
1561 return pwqp;
1564 static isl_stat basic_map_card(__isl_take isl_basic_map *bmap, void *user)
1566 isl_pw_qpolynomial **sum = (isl_pw_qpolynomial **)user;
1567 isl_pw_qpolynomial *pwqp;
1568 unsigned nparam = isl_basic_map_dim(bmap, isl_dim_param);
1569 unsigned n_in = isl_basic_map_dim(bmap, isl_dim_in);
1570 isl_space *target_dim;
1571 isl_basic_set *bset;
1573 target_dim = isl_basic_map_get_space(bmap);
1574 target_dim = isl_space_domain(target_dim);
1576 bmap = isl_basic_map_move_dims(bmap, isl_dim_param, nparam,
1577 isl_dim_in, 0, n_in);
1579 bset = isl_basic_map_range(bmap);
1580 bset = isl_basic_set_lift(bset);
1581 pwqp = isl_basic_set_multiplicative_call(bset, &basic_set_card);
1583 pwqp = isl_pw_qpolynomial_move_dims(pwqp, isl_dim_in, 0,
1584 isl_dim_param, nparam, n_in);
1585 pwqp = isl_pw_qpolynomial_reset_domain_space(pwqp, target_dim);
1586 *sum = isl_pw_qpolynomial_add(*sum, pwqp);
1588 return isl_stat_ok;
1591 static __isl_give isl_pw_qpolynomial *card_as_sum(__isl_take isl_map *map,
1592 barvinok_options *options)
1594 isl_ctx *ctx;
1595 isl_val *one;
1596 isl_space *dim;
1597 isl_set *set;
1598 isl_qpolynomial *qp;
1599 isl_pw_qpolynomial *pwqp;
1600 int summation = options->summation;
1602 if (!map)
1603 return NULL;
1605 options->summation = BV_SUM_BERNOULLI;
1607 set = isl_map_wrap(map);
1608 dim = isl_set_get_space(set);
1609 ctx = isl_map_get_ctx(map);
1610 one = isl_val_one(ctx);
1611 qp = isl_qpolynomial_val_on_domain(dim, one);
1613 pwqp = isl_pw_qpolynomial_alloc(set, qp);
1614 pwqp = isl_pw_qpolynomial_sum(pwqp);
1616 options->summation = summation;
1618 return pwqp;
1621 __isl_give isl_pw_qpolynomial *isl_map_card(__isl_take isl_map *map)
1623 isl_ctx *ctx;
1624 isl_space *dim;
1625 isl_pw_qpolynomial *sum;
1626 barvinok_options *options;
1628 ctx = isl_map_get_ctx(map);
1629 options = isl_ctx_peek_barvinok_options(ctx);
1630 if (options &&
1631 (options->approx->method == BV_APPROX_BERNOULLI ||
1632 options->summation == BV_SUM_BERNOULLI))
1633 return card_as_sum(map, options);
1635 dim = isl_map_get_space(map);
1636 dim = isl_space_domain(dim);
1637 dim = isl_space_from_domain(dim);
1638 dim = isl_space_add_dims(dim, isl_dim_out, 1);
1639 sum = isl_pw_qpolynomial_zero(dim);
1641 map = isl_map_make_disjoint(map);
1642 map = isl_map_compute_divs(map);
1644 if (isl_map_foreach_basic_map(map, &basic_map_card, &sum) < 0)
1645 goto error;
1647 isl_map_free(map);
1649 return sum;
1650 error:
1651 isl_map_free(map);
1652 isl_pw_qpolynomial_free(sum);
1653 return NULL;
1656 __isl_give isl_pw_qpolynomial *isl_set_card(__isl_take isl_set *set)
1658 isl_pw_qpolynomial *pwqp;
1659 pwqp = isl_map_card(isl_map_from_range(set));
1660 pwqp = isl_pw_qpolynomial_project_domain_on_params(pwqp);
1661 return pwqp;
1664 __isl_give isl_pw_qpolynomial *isl_basic_map_card(__isl_take isl_basic_map *bmap)
1666 return isl_map_card(isl_map_from_basic_map(bmap));
1669 __isl_give isl_pw_qpolynomial *isl_basic_set_card(__isl_take isl_basic_set *bset)
1671 isl_pw_qpolynomial *pwqp;
1672 pwqp = isl_basic_map_card(isl_basic_map_from_range(bset));
1673 pwqp = isl_pw_qpolynomial_project_domain_on_params(pwqp);
1674 return pwqp;
1677 static isl_stat set_card(__isl_take isl_set *set, void *user)
1679 isl_union_pw_qpolynomial **res = (isl_union_pw_qpolynomial **)user;
1680 isl_pw_qpolynomial *pwqp;
1681 isl_union_pw_qpolynomial *upwqp;
1683 pwqp = isl_set_card(set);
1684 upwqp = isl_union_pw_qpolynomial_from_pw_qpolynomial(pwqp);
1685 *res = isl_union_pw_qpolynomial_add(*res, upwqp);
1687 return isl_stat_ok;
1690 __isl_give isl_union_pw_qpolynomial *isl_union_set_card(
1691 __isl_take isl_union_set *uset)
1693 isl_space *dim;
1694 isl_union_pw_qpolynomial *res;
1696 dim = isl_union_set_get_space(uset);
1697 res = isl_union_pw_qpolynomial_zero(dim);
1698 if (isl_union_set_foreach_set(uset, &set_card, &res) < 0)
1699 goto error;
1700 isl_union_set_free(uset);
1702 return res;
1703 error:
1704 isl_union_set_free(uset);
1705 isl_union_pw_qpolynomial_free(res);
1706 return NULL;
1709 static isl_stat map_card(__isl_take isl_map *map, void *user)
1711 isl_union_pw_qpolynomial **res = (isl_union_pw_qpolynomial **)user;
1712 isl_pw_qpolynomial *pwqp;
1713 isl_union_pw_qpolynomial *upwqp;
1715 pwqp = isl_map_card(map);
1716 upwqp = isl_union_pw_qpolynomial_from_pw_qpolynomial(pwqp);
1717 *res = isl_union_pw_qpolynomial_add(*res, upwqp);
1719 return isl_stat_ok;
1722 __isl_give isl_union_pw_qpolynomial *isl_union_map_card(
1723 __isl_take isl_union_map *umap)
1725 isl_space *dim;
1726 isl_union_pw_qpolynomial *res;
1728 dim = isl_union_map_get_space(umap);
1729 res = isl_union_pw_qpolynomial_zero(dim);
1730 if (isl_union_map_foreach_map(umap, &map_card, &res) < 0)
1731 goto error;
1732 isl_union_map_free(umap);
1734 return res;
1735 error:
1736 isl_union_map_free(umap);
1737 isl_union_pw_qpolynomial_free(res);
1738 return NULL;