update isl for rename of !isl_set_dim_has_{lower,upper}_bound
[barvinok.git] / genfun.cc
blobf28767766d4fce8b770d2b3cbedad38762d829af
1 #include <iostream>
2 #include <iomanip>
3 #include <vector>
4 #include <assert.h>
5 #include <barvinok/genfun.h>
6 #include <barvinok/barvinok.h>
7 #include "conversion.h"
8 #include "counter.h"
9 #include "genfun_constructor.h"
10 #include "mat_util.h"
11 #include "matrix_read.h"
12 #include "remove_equalities.h"
14 using std::cout;
15 using std::cerr;
16 using std::endl;
17 using std::pair;
18 using std::vector;
20 bool short_rat_lex_smaller_denominator::operator()(const short_rat* r1,
21 const short_rat* r2) const
23 return lex_cmp(r1->d.power, r2->d.power) < 0;
26 static void lex_order_terms(struct short_rat* rat)
28 for (int i = 0; i < rat->n.power.NumRows(); ++i) {
29 int m = i;
30 for (int j = i+1; j < rat->n.power.NumRows(); ++j)
31 if (lex_cmp(rat->n.power[j], rat->n.power[m]) < 0)
32 m = j;
33 if (m != i) {
34 vec_ZZ tmp = rat->n.power[m];
35 rat->n.power[m] = rat->n.power[i];
36 rat->n.power[i] = tmp;
37 QQ tmp_coeff = rat->n.coeff[m];
38 rat->n.coeff[m] = rat->n.coeff[i];
39 rat->n.coeff[i] = tmp_coeff;
44 short_rat::short_rat(const short_rat& r)
46 n.coeff = r.n.coeff;
47 n.power = r.n.power;
48 d.power = r.d.power;
51 short_rat::short_rat(Value c)
53 n.coeff.SetLength(1);
54 value2zz(c, n.coeff[0].n);
55 n.coeff[0].d = 1;
56 n.power.SetDims(1, 0);
57 d.power.SetDims(0, 0);
60 short_rat::short_rat(const QQ& c, const vec_ZZ& num, const mat_ZZ& den)
62 n.coeff.SetLength(1);
63 ZZ g = GCD(c.n, c.d);
64 n.coeff[0].n = c.n/g;
65 n.coeff[0].d = c.d/g;
66 n.power.SetDims(1, num.length());
67 n.power[0] = num;
68 d.power = den;
69 normalize();
72 short_rat::short_rat(const vec_QQ& c, const mat_ZZ& num, const mat_ZZ& den)
74 n.coeff = c;
75 n.power = num;
76 d.power = den;
77 normalize();
80 void short_rat::normalize()
82 /* Make all powers in denominator reverse-lexico-positive */
83 for (int i = 0; i < d.power.NumRows(); ++i) {
84 int j;
85 for (j = d.power.NumCols()-1; j >= 0; --j)
86 if (!IsZero(d.power[i][j]))
87 break;
88 assert(j >= 0);
89 if (sign(d.power[i][j]) < 0) {
90 negate(d.power[i], d.power[i]);
91 for (int k = 0; k < n.coeff.length(); ++k) {
92 negate(n.coeff[k].n, n.coeff[k].n);
93 n.power[k] += d.power[i];
98 /* Order powers in denominator */
99 lex_order_rows(d.power);
102 void short_rat::add(const short_rat *r)
104 for (int i = 0; i < r->n.power.NumRows(); ++i) {
105 int len = n.coeff.length();
106 int j;
107 for (j = 0; j < len; ++j)
108 if (r->n.power[i] == n.power[j])
109 break;
110 if (j < len) {
111 n.coeff[j] += r->n.coeff[i];
112 if (n.coeff[j].n == 0) {
113 if (j < len-1) {
114 n.power[j] = n.power[len-1];
115 n.coeff[j] = n.coeff[len-1];
117 int dim = n.power.NumCols();
118 n.coeff.SetLength(len-1);
119 n.power.SetDims(len-1, dim);
121 } else {
122 int dim = n.power.NumCols();
123 n.coeff.SetLength(len+1);
124 n.power.SetDims(len+1, dim);
125 n.coeff[len] = r->n.coeff[i];
126 n.power[len] = r->n.power[i];
131 QQ short_rat::coefficient(Value* params, barvinok_options *options) const
133 unsigned nvar = d.power.NumRows();
134 unsigned nparam = d.power.NumCols();
135 Matrix *C = Matrix_Alloc(nparam + nvar, 1 + nvar + 1);
136 Value tmp;
137 value_init(tmp);
139 QQ c(0, 1);
141 for (int j = 0; j < n.coeff.length(); ++j) {
142 C->NbRows = nparam+nvar;
143 for (int r = 0; r < nparam; ++r) {
144 value_set_si(C->p[r][0], 0);
145 for (int c = 0; c < nvar; ++c) {
146 zz2value(d.power[c][r], C->p[r][1+c]);
148 zz2value(n.power[j][r], C->p[r][1+nvar]);
149 value_subtract(C->p[r][1+nvar], C->p[r][1+nvar], params[r]);
151 for (int r = 0; r < nvar; ++r) {
152 value_set_si(C->p[nparam+r][0], 1);
153 Vector_Set(&C->p[nparam+r][1], 0, nvar + 1);
154 value_set_si(C->p[nparam+r][1+r], 1);
156 Polyhedron *P = Constraints2Polyhedron(C, options->MaxRays);
157 if (emptyQ2(P)) {
158 Polyhedron_Free(P);
159 continue;
161 barvinok_count_with_options(P, &tmp, options);
162 Polyhedron_Free(P);
163 if (value_zero_p(tmp))
164 continue;
165 QQ c2(0, 1);
166 value2zz(tmp, c2.n);
167 c2 *= n.coeff[j];
168 c += c2;
170 Matrix_Free(C);
171 value_clear(tmp);
172 return c;
175 bool short_rat::reduced()
177 int dim = n.power.NumCols();
178 lex_order_terms(this);
179 if (n.power.NumRows() % 2 == 0) {
180 if (n.coeff[0].n == -n.coeff[1].n &&
181 n.coeff[0].d == n.coeff[1].d) {
182 vec_ZZ step = n.power[1] - n.power[0];
183 int k;
184 for (k = 1; k < n.power.NumRows()/2; ++k) {
185 if (n.coeff[2*k].n != -n.coeff[2*k+1].n ||
186 n.coeff[2*k].d != n.coeff[2*k+1].d)
187 break;
188 if (step != n.power[2*k+1] - n.power[2*k])
189 break;
191 if (k == n.power.NumRows()/2) {
192 for (k = 0; k < d.power.NumRows(); ++k)
193 if (d.power[k] == step)
194 break;
195 if (k < d.power.NumRows()) {
196 for (++k; k < d.power.NumRows(); ++k)
197 d.power[k-1] = d.power[k];
198 d.power.SetDims(k-1, dim);
199 for (k = 1; k < n.power.NumRows()/2; ++k) {
200 n.coeff[k] = n.coeff[2*k];
201 n.power[k] = n.power[2*k];
203 n.coeff.SetLength(k);
204 n.power.SetDims(k, dim);
205 return true;
210 return false;
213 gen_fun::gen_fun(Value c)
215 short_rat *r = new short_rat(c);
216 context = Universe_Polyhedron(0);
217 term.insert(r);
220 void gen_fun::add(const QQ& c, const vec_ZZ& num, const mat_ZZ& den)
222 if (c.n == 0)
223 return;
225 add(new short_rat(c, num, den));
228 void gen_fun::add(short_rat *r)
230 short_rat_list::iterator i = term.find(r);
231 while (i != term.end()) {
232 (*i)->add(r);
233 if ((*i)->n.coeff.length() == 0) {
234 delete *i;
235 term.erase(i);
236 } else if ((*i)->reduced()) {
237 delete r;
238 /* we've modified term[i], so remove it
239 * and add it back again
241 r = *i;
242 term.erase(i);
243 i = term.find(r);
244 continue;
246 delete r;
247 return;
250 term.insert(r);
253 void gen_fun::add(const QQ& c, const gen_fun *gf, barvinok_options *options)
255 Polyhedron *U = DomainUnion(context, gf->context, options->MaxRays);
256 Polyhedron *C = DomainConvex(U, options->MaxRays);
257 Domain_Free(U);
258 Domain_Free(context);
259 context = C;
261 add(c, gf);
264 void gen_fun::add(const QQ& c, const gen_fun *gf)
266 QQ p;
267 for (short_rat_list::iterator i = gf->term.begin(); i != gf->term.end(); ++i) {
268 for (int j = 0; j < (*i)->n.power.NumRows(); ++j) {
269 p = c;
270 p *= (*i)->n.coeff[j];
271 add(p, (*i)->n.power[j], (*i)->d.power);
276 static void split_param_compression(Matrix *CP, mat_ZZ& map, vec_ZZ& offset)
278 Matrix *T = Transpose(CP);
279 matrix2zz(T, map, T->NbRows-1, T->NbColumns-1);
280 values2zz(T->p[T->NbRows-1], offset, T->NbColumns-1);
281 Matrix_Free(T);
285 * Perform the substitution specified by CP
287 * CP is a homogeneous matrix that maps a set of "compressed parameters"
288 * to the original set of parameters.
290 * This function is applied to a gen_fun computed with the compressed parameters
291 * and adapts it to refer to the original parameters.
293 * That is, if y are the compressed parameters and x = A y + b are the original
294 * parameters, then we want the coefficient of the monomial t^y in the original
295 * generating function to be the coefficient of the monomial u^x in the resulting
296 * generating function.
297 * The original generating function has the form
299 * a t^m/(1-t^n) = a t^m + a t^{m+n} + a t^{m+2n} + ...
301 * Since each term t^y should correspond to a term u^x, with x = A y + b, we want
303 * a u^{A m + b} + a u^{A (m+n) + b} + a u^{A (m+2n) +b} + ... =
305 * = a u^{A m + b}/(1-u^{A n})
307 * Therefore, we multiply the powers m and n in both numerator and denominator by A
308 * and add b to the power in the numerator.
309 * Since the above powers are stored as row vectors m^T and n^T,
310 * we compute, say, m'^T = m^T A^T to obtain m' = A m.
312 * The pair (map, offset) contains the same information as CP.
313 * map is the transpose of the linear part of CP, while offset is the constant part.
315 void gen_fun::substitute(Matrix *CP)
317 mat_ZZ map;
318 vec_ZZ offset;
319 split_param_compression(CP, map, offset);
320 Polyhedron *C = Polyhedron_Image(context, CP, 0);
321 Polyhedron_Free(context);
322 context = C;
324 short_rat_list new_term;
325 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i) {
326 short_rat *r = (*i);
327 r->d.power *= map;
328 r->n.power *= map;
329 for (int j = 0; j < r->n.power.NumRows(); ++j)
330 r->n.power[j] += offset;
331 r->normalize();
332 new_term.insert(r);
334 term.swap(new_term);
337 static int Matrix_Equal(Matrix *M1, Matrix *M2)
339 int i, j;
341 if (M1->NbRows != M2->NbRows)
342 return 0;
343 if (M1->NbColumns != M2->NbColumns)
344 return 0;
345 for (i = 0; i < M1->NbRows; ++i)
346 for (j = 0; j < M1->NbColumns; ++j)
347 if (value_ne(M1->p[i][j], M2->p[i][j]))
348 return 0;
350 return 1;
353 struct parallel_cones {
354 int *pos;
355 vector<pair<Vector *, QQ> > vertices;
356 parallel_cones(int *pos) : pos(pos) {}
359 /* This structure helps in computing the generating functions
360 * of polytopes with pairwise parallel hyperplanes more efficiently.
361 * These occur when computing hadamard products of pairs of generating
362 * functions with the same denominators.
363 * If there are many such pairs then the same vertex cone
364 * may appear more than once. We therefore keep a list of all
365 * vertex cones and only compute the corresponding generating function
366 * once.
367 * However, even HPs of generating functions with the same denominators
368 * can result in polytopes of different "shapes", making them incomparable.
369 * In particular, they can have different equalities among the parameters
370 * and the variables. In such cases, only polytopes of the first "shape"
371 * that is encountered are kept in this way. The others are handled
372 * in the usual, non-optimized way.
374 struct parallel_polytopes {
375 gf_base *red;
376 Polyhedron *context;
377 Matrix *Constraints;
378 Matrix *CP, *T;
379 int dim;
380 int nparam;
381 unsigned reduced_nparam;
382 vector<parallel_cones> cones;
383 barvinok_options *options;
385 parallel_polytopes(int n, Polyhedron *context, int nparam,
386 barvinok_options *options) :
387 context(context), dim(-1), nparam(nparam),
388 options(options) {
389 red = NULL;
390 Constraints = NULL;
391 CP = NULL;
392 T = NULL;
394 bool add(const QQ& c, Polyhedron *P) {
395 int i;
397 for (i = 0; i < P->NbEq; ++i)
398 if (First_Non_Zero(P->Constraint[i]+1,
399 P->Dimension-nparam) == -1)
400 break;
401 if (i < P->NbEq)
402 return false;
404 Polyhedron *Q = remove_equalities_p(Polyhedron_Copy(P), P->Dimension-nparam,
405 NULL, options->MaxRays);
406 POL_ENSURE_VERTICES(Q);
407 if (emptyQ(Q)) {
408 Polyhedron_Free(Q);
409 return true;
412 if (Q->Dimension == 0) {
413 Polyhedron_Free(Q);
414 return false;
417 if (Q->NbEq != 0) {
418 Matrix *Q_CP;
419 Polyhedron *R = Q;
421 remove_all_equalities(&Q, NULL, &Q_CP, NULL, nparam,
422 options->MaxRays);
424 POL_ENSURE_VERTICES(Q);
425 if (emptyQ(Q) || Q->NbEq > 0 || Q->Dimension == 0) {
426 if (Q_CP)
427 Matrix_Free(Q_CP);
428 Polyhedron_Free(R);
429 Polyhedron_Free(Q);
430 return emptyQ(Q);
433 if (red) {
434 if ((!CP ^ !Q_CP) || (CP && !Matrix_Equal(CP, Q_CP))) {
435 Matrix_Free(Q_CP);
436 Polyhedron_Free(R);
437 Polyhedron_Free(Q);
438 return false;
440 Matrix_Free(Q_CP);
441 } else {
442 CP = Q_CP;
443 T = align_matrix(CP, R->Dimension+1);
446 reduced_nparam = CP->NbColumns-1;
447 Polyhedron_Free(R);
448 } else {
449 if (red && CP) {
450 Polyhedron_Free(Q);
451 return false;
453 reduced_nparam = nparam;
456 if (First_Non_Zero(Q->Constraint[Q->NbConstraints-1]+1, Q->Dimension) == -1)
457 Q->NbConstraints--;
459 if (!Constraints) {
460 Polyhedron *reduced_context;
461 dim = Q->Dimension;
462 if (CP)
463 reduced_context = Polyhedron_Preimage(context, CP, options->MaxRays);
464 else
465 reduced_context = Polyhedron_Copy(context);
466 red = gf_base::create(reduced_context, dim, reduced_nparam, options);
467 red->base->init(Q, 0);
468 Constraints = Matrix_Alloc(Q->NbConstraints, Q->Dimension);
469 for (int i = 0; i < Q->NbConstraints; ++i) {
470 Vector_Copy(Q->Constraint[i]+1, Constraints->p[i], Q->Dimension);
472 } else {
473 if (Q->Dimension != dim) {
474 Polyhedron_Free(Q);
475 return false;
477 assert(Q->Dimension == dim);
478 for (int i = 0; i < Q->NbConstraints; ++i) {
479 int j;
480 for (j = 0; j < Constraints->NbRows; ++j)
481 if (Vector_Equal(Q->Constraint[i]+1, Constraints->p[j],
482 Q->Dimension))
483 break;
484 if (j >= Constraints->NbRows) {
485 Matrix_Extend(Constraints, Constraints->NbRows+1);
486 Vector_Copy(Q->Constraint[i]+1,
487 Constraints->p[Constraints->NbRows-1],
488 Q->Dimension);
493 for (int i = 0; i < Q->NbRays; ++i) {
494 if (!value_pos_p(Q->Ray[i][dim+1]))
495 continue;
497 Polyhedron *C = supporting_cone(Q, i);
499 if (First_Non_Zero(C->Constraint[C->NbConstraints-1]+1,
500 C->Dimension) == -1)
501 C->NbConstraints--;
503 int *pos = new int[1+C->NbConstraints];
504 int l = 0;
505 for (int k = 0; k < Constraints->NbRows; ++k) {
506 for (int j = 0; j < C->NbConstraints; ++j) {
507 if (Vector_Equal(C->Constraint[j]+1, Constraints->p[k],
508 C->Dimension)) {
509 pos[1+l++] = k;
510 break;
514 pos[0] = l;
516 int j;
517 for (j = 0; j < cones.size(); ++j)
518 if (!memcmp(pos, cones[j].pos, (1+C->NbConstraints)*sizeof(int)))
519 break;
520 if (j == cones.size())
521 cones.push_back(parallel_cones(pos));
522 else
523 delete [] pos;
525 Polyhedron_Free(C);
527 int k;
528 for (k = 0; k < cones[j].vertices.size(); ++k)
529 if (Vector_Equal(Q->Ray[i]+1, cones[j].vertices[k].first->p,
530 Q->Dimension+1))
531 break;
533 if (k == cones[j].vertices.size()) {
534 Vector *vertex = Vector_Alloc(Q->Dimension+1);
535 Vector_Copy(Q->Ray[i]+1, vertex->p, Q->Dimension+1);
536 cones[j].vertices.push_back(pair<Vector*,QQ>(vertex, c));
537 } else {
538 cones[j].vertices[k].second += c;
539 if (cones[j].vertices[k].second.n == 0) {
540 int size = cones[j].vertices.size();
541 Vector_Free(cones[j].vertices[k].first);
542 if (k < size-1)
543 cones[j].vertices[k] = cones[j].vertices[size-1];
544 cones[j].vertices.pop_back();
549 Polyhedron_Free(Q);
550 return true;
552 gen_fun *compute() {
553 if (!red)
554 return NULL;
555 for (int i = 0; i < cones.size(); ++i) {
556 Matrix *M = Matrix_Alloc(cones[i].pos[0], 1+Constraints->NbColumns+1);
557 Polyhedron *Cone;
558 for (int j = 0; j <cones[i].pos[0]; ++j) {
559 value_set_si(M->p[j][0], 1);
560 Vector_Copy(Constraints->p[cones[i].pos[1+j]], M->p[j]+1,
561 Constraints->NbColumns);
563 Cone = Constraints2Polyhedron(M, options->MaxRays);
564 Matrix_Free(M);
565 for (int j = 0; j < cones[i].vertices.size(); ++j) {
566 red->base->do_vertex_cone(cones[i].vertices[j].second,
567 Polyhedron_Copy(Cone),
568 cones[i].vertices[j].first->p, options);
570 Polyhedron_Free(Cone);
572 if (CP)
573 red->gf->substitute(CP);
574 return red->gf;
576 void print(std::ostream& os) const {
577 for (int i = 0; i < cones.size(); ++i) {
578 os << "[";
579 for (int j = 0; j < cones[i].pos[0]; ++j) {
580 if (j)
581 os << ", ";
582 os << cones[i].pos[1+j];
584 os << "]" << endl;
585 for (int j = 0; j < cones[i].vertices.size(); ++j) {
586 Vector_Print(stderr, P_VALUE_FMT, cones[i].vertices[j].first);
587 os << cones[i].vertices[j].second << endl;
591 ~parallel_polytopes() {
592 for (int i = 0; i < cones.size(); ++i) {
593 delete [] cones[i].pos;
594 for (int j = 0; j < cones[i].vertices.size(); ++j)
595 Vector_Free(cones[i].vertices[j].first);
597 if (Constraints)
598 Matrix_Free(Constraints);
599 if (CP)
600 Matrix_Free(CP);
601 if (T)
602 Matrix_Free(T);
603 delete red;
607 gen_fun *gen_fun::Hadamard_product(const gen_fun *gf, barvinok_options *options)
609 QQ one(1, 1);
610 Polyhedron *C = DomainIntersection(context, gf->context, options->MaxRays);
611 gen_fun *sum = new gen_fun(C);
613 int j = 0;
614 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i, j++) {
615 int k = 0;
616 for (short_rat_list::iterator i2 = gf->term.begin();
617 i2 != gf->term.end();
618 ++i2, k++) {
619 int d = (*i)->d.power.NumCols();
620 int k1 = (*i)->d.power.NumRows();
621 int k2 = (*i2)->d.power.NumRows();
622 assert((*i)->d.power.NumCols() == (*i2)->d.power.NumCols());
624 if (options->verbose)
625 fprintf(stderr, "HP: %d/%zd %d/%zd \r",
626 j, term.size(), k, gf->term.size());
628 parallel_polytopes pp((*i)->n.power.NumRows() *
629 (*i2)->n.power.NumRows(),
630 sum->context, d, options);
632 for (int j = 0; j < (*i)->n.power.NumRows(); ++j) {
633 for (int j2 = 0; j2 < (*i2)->n.power.NumRows(); ++j2) {
634 Matrix *M = Matrix_Alloc(k1+k2+d+d, 1+k1+k2+d+1);
635 for (int k = 0; k < k1+k2; ++k) {
636 value_set_si(M->p[k][0], 1);
637 value_set_si(M->p[k][1+k], 1);
639 for (int k = 0; k < d; ++k) {
640 value_set_si(M->p[k1+k2+k][1+k1+k2+k], -1);
641 zz2value((*i)->n.power[j][k], M->p[k1+k2+k][1+k1+k2+d]);
642 for (int l = 0; l < k1; ++l)
643 zz2value((*i)->d.power[l][k], M->p[k1+k2+k][1+l]);
645 for (int k = 0; k < d; ++k) {
646 value_set_si(M->p[k1+k2+d+k][1+k1+k2+k], -1);
647 zz2value((*i2)->n.power[j2][k],
648 M->p[k1+k2+d+k][1+k1+k2+d]);
649 for (int l = 0; l < k2; ++l)
650 zz2value((*i2)->d.power[l][k],
651 M->p[k1+k2+d+k][1+k1+l]);
653 Polyhedron *P = Constraints2Polyhedron(M, options->MaxRays);
654 Matrix_Free(M);
656 QQ c = (*i)->n.coeff[j];
657 c *= (*i2)->n.coeff[j2];
658 if (!pp.add(c, P)) {
659 gen_fun *t = barvinok_enumerate_series(P, C->Dimension, options);
660 sum->add(c, t);
661 delete t;
664 Polyhedron_Free(P);
668 gen_fun *t = pp.compute();
669 if (t) {
670 sum->add(one, t);
671 delete t;
675 return sum;
678 void gen_fun::add_union(gen_fun *gf, barvinok_options *options)
680 QQ one(1, 1), mone(-1, 1);
682 gen_fun *hp = Hadamard_product(gf, options);
683 add(one, gf);
684 add(mone, hp);
685 delete hp;
688 static void Polyhedron_Shift(Polyhedron *P, Vector *offset)
690 Value tmp;
691 value_init(tmp);
692 for (int i = 0; i < P->NbConstraints; ++i) {
693 Inner_Product(P->Constraint[i]+1, offset->p, P->Dimension, &tmp);
694 value_subtract(P->Constraint[i][1+P->Dimension],
695 P->Constraint[i][1+P->Dimension], tmp);
697 for (int i = 0; i < P->NbRays; ++i) {
698 if (value_notone_p(P->Ray[i][0]))
699 continue;
700 if (value_zero_p(P->Ray[i][1+P->Dimension]))
701 continue;
702 Vector_Combine(P->Ray[i]+1, offset->p, P->Ray[i]+1,
703 P->Ray[i][0], P->Ray[i][1+P->Dimension], P->Dimension);
705 value_clear(tmp);
708 void gen_fun::shift(const vec_ZZ& offset)
710 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i)
711 for (int j = 0; j < (*i)->n.power.NumRows(); ++j)
712 (*i)->n.power[j] += offset;
714 Vector *v = Vector_Alloc(offset.length());
715 zz2values(offset, v->p);
716 Polyhedron_Shift(context, v);
717 Vector_Free(v);
720 /* Divide the generating functin by 1/(1-z^power).
721 * The effect on the corresponding explicit function f(x) is
722 * f'(x) = \sum_{i=0}^\infty f(x - i * power)
724 void gen_fun::divide(const vec_ZZ& power)
726 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i) {
727 int r = (*i)->d.power.NumRows();
728 int c = (*i)->d.power.NumCols();
729 (*i)->d.power.SetDims(r+1, c);
730 (*i)->d.power[r] = power;
733 Vector *v = Vector_Alloc(1+power.length()+1);
734 value_set_si(v->p[0], 1);
735 zz2values(power, v->p+1);
736 Polyhedron *C = AddRays(v->p, 1, context, context->NbConstraints+1);
737 Vector_Free(v);
738 Polyhedron_Free(context);
739 context = C;
742 static void print_power(std::ostream& os, const QQ& c, const vec_ZZ& p,
743 unsigned int nparam, const char **param_name)
745 bool first = true;
747 for (int i = 0; i < p.length(); ++i) {
748 if (p[i] == 0)
749 continue;
750 if (first) {
751 if (c.n == -1 && c.d == 1)
752 os << "-";
753 else if (c.n != 1 || c.d != 1) {
754 os << c.n;
755 if (c.d != 1)
756 os << "/" << c.d;
757 os << "*";
759 first = false;
760 } else
761 os << "*";
762 if (i < nparam)
763 os << param_name[i];
764 else
765 os << "x" << i;
766 if (p[i] == 1)
767 continue;
768 if (p[i] < 0)
769 os << "^(" << p[i] << ")";
770 else
771 os << "^" << p[i];
773 if (first) {
774 os << c.n;
775 if (c.d != 1)
776 os << "/" << c.d;
780 void short_rat::print(std::ostream& os, unsigned int nparam,
781 const char **param_name) const
783 QQ mone(-1, 1);
784 os << "(";
785 for (int j = 0; j < n.coeff.length(); ++j) {
786 if (j != 0 && n.coeff[j].n >= 0)
787 os << "+";
788 print_power(os, n.coeff[j], n.power[j], nparam, param_name);
790 os << ")";
791 if (d.power.NumRows() == 0)
792 return;
793 os << "/(";
794 for (int j = 0; j < d.power.NumRows(); ++j) {
795 if (j != 0)
796 os << " * ";
797 os << "(1";
798 print_power(os, mone, d.power[j], nparam, param_name);
799 os << ")";
801 os << ")";
804 void gen_fun::print(std::ostream& os, unsigned int nparam,
805 const char **param_name) const
807 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i) {
808 if (i != term.begin())
809 os << " + ";
810 (*i)->print(os, nparam, param_name);
814 std::ostream & operator<< (std::ostream & os, const short_rat& r)
816 os << r.n.coeff << endl;
817 os << r.n.power << endl;
818 os << r.d.power << endl;
819 return os;
822 extern "C" { typedef void (*gmp_free_t)(void *, size_t); }
824 std::ostream & operator<< (std::ostream & os, const Polyhedron& P)
826 char *str;
827 gmp_free_t gmp_free;
828 mp_get_memory_functions(NULL, NULL, &gmp_free);
829 os << P.NbConstraints << " " << P.Dimension+2 << endl;
830 for (int i = 0; i < P.NbConstraints; ++i) {
831 for (int j = 0; j < P.Dimension+2; ++j) {
832 str = mpz_get_str(0, 10, P.Constraint[i][j]);
833 os << std::setw(4) << str << " ";
834 (*gmp_free)(str, strlen(str)+1);
836 os << endl;
838 return os;
841 std::ostream & operator<< (std::ostream & os, const gen_fun& gf)
843 os << *gf.context << endl;
844 os << endl;
845 os << gf.term.size() << endl;
846 for (short_rat_list::iterator i = gf.term.begin(); i != gf.term.end(); ++i)
847 os << **i;
848 return os;
851 gen_fun *gen_fun::read(std::istream& is, barvinok_options *options)
853 Matrix *M = Matrix_Read(is);
854 Polyhedron *C = Constraints2Polyhedron(M, options->MaxRays);
855 Matrix_Free(M);
857 gen_fun *gf = new gen_fun(C);
859 int n;
860 is >> n;
862 vec_QQ c;
863 mat_ZZ num;
864 mat_ZZ den;
865 for (int i = 0; i < n; ++i) {
866 is >> c >> num >> den;
867 gf->add(new short_rat(c, num, den));
870 return gf;
873 gen_fun::operator evalue *() const
875 evalue *EP = NULL;
876 evalue factor;
877 value_init(factor.d);
878 value_init(factor.x.n);
879 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i) {
880 unsigned nvar = (*i)->d.power.NumRows();
881 unsigned nparam = (*i)->d.power.NumCols();
882 Matrix *C = Matrix_Alloc(nparam + nvar, 1 + nvar + nparam + 1);
883 mat_ZZ& d = (*i)->d.power;
884 Polyhedron *U = context;
886 for (int j = 0; j < (*i)->n.coeff.length(); ++j) {
887 for (int r = 0; r < nparam; ++r) {
888 value_set_si(C->p[r][0], 0);
889 for (int c = 0; c < nvar; ++c) {
890 zz2value(d[c][r], C->p[r][1+c]);
892 Vector_Set(&C->p[r][1+nvar], 0, nparam);
893 value_set_si(C->p[r][1+nvar+r], -1);
894 zz2value((*i)->n.power[j][r], C->p[r][1+nvar+nparam]);
896 for (int r = 0; r < nvar; ++r) {
897 value_set_si(C->p[nparam+r][0], 1);
898 Vector_Set(&C->p[nparam+r][1], 0, nvar + nparam + 1);
899 value_set_si(C->p[nparam+r][1+r], 1);
901 Polyhedron *P = Constraints2Polyhedron(C, 0);
902 evalue *E = barvinok_enumerate_ev(P, U, 0);
903 Polyhedron_Free(P);
904 if (EVALUE_IS_ZERO(*E)) {
905 evalue_free(E);
906 continue;
908 zz2value((*i)->n.coeff[j].n, factor.x.n);
909 zz2value((*i)->n.coeff[j].d, factor.d);
910 emul(&factor, E);
911 if (!EP)
912 EP = E;
913 else {
914 eadd(E, EP);
915 evalue_free(E);
918 Matrix_Free(C);
920 value_clear(factor.d);
921 value_clear(factor.x.n);
922 return EP ? EP : evalue_zero();
925 ZZ gen_fun::coefficient(Value* params, barvinok_options *options) const
927 if (!in_domain(context, params))
928 return ZZ::zero();
930 QQ sum(0, 1);
932 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i)
933 sum += (*i)->coefficient(params, options);
935 assert(sum.d == 1);
936 return sum.n;
939 void gen_fun::coefficient(Value* params, Value* c) const
941 barvinok_options *options = barvinok_options_new_with_defaults();
943 ZZ coeff = coefficient(params, options);
945 zz2value(coeff, *c);
947 barvinok_options_free(options);
950 gen_fun *gen_fun::summate(int nvar, barvinok_options *options) const
952 int dim = context->Dimension;
953 int nparam = dim - nvar;
954 reducer *red;
955 gen_fun *gf;
957 if (nparam == 0) {
958 bool finite;
959 Value c;
960 value_init(c);
961 finite = summate(&c);
962 assert(finite);
963 gf = new gen_fun(c);
964 value_clear(c);
965 return gf;
968 if (options->incremental_specialization == 1) {
969 red = new partial_ireducer(Polyhedron_Project(context, nparam), dim, nparam);
970 } else
971 red = new partial_reducer(Polyhedron_Project(context, nparam), dim, nparam);
972 for (;;) {
973 int n_try = 0;
974 try {
975 red->init(context, n_try);
976 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i)
977 red->reduce((*i)->n.coeff, (*i)->n.power, (*i)->d.power);
978 break;
979 } catch (OrthogonalException &e) {
980 red->reset();
981 n_try++;
984 gf = red->get_gf();
985 delete red;
986 return gf;
989 /* returns true if the set was finite and false otherwise */
990 bool gen_fun::summate(Value *sum) const
992 if (term.size() == 0) {
993 value_set_si(*sum, 0);
994 return true;
997 int maxlen = 0;
998 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i)
999 if ((*i)->d.power.NumRows() > maxlen)
1000 maxlen = (*i)->d.power.NumRows();
1002 infinite_counter cnt((*term.begin())->d.power.NumCols(), maxlen);
1003 cnt.init(context, 0);
1004 for (short_rat_list::iterator i = term.begin(); i != term.end(); ++i)
1005 cnt.reduce((*i)->n.coeff, (*i)->n.power, (*i)->d.power);
1007 for (int i = 1; i <= maxlen; ++i)
1008 if (value_notzero_p(mpq_numref(cnt.count[i]))) {
1009 value_set_si(*sum, -1);
1010 return false;
1013 assert(value_one_p(mpq_denref(cnt.count[0])));
1014 value_assign(*sum, mpq_numref(cnt.count[0]));
1015 return true;
1018 bool gen_fun::is_zero() const
1020 bool empty;
1021 Value c;
1023 value_init(c);
1025 empty = summate(&c) && value_zero_p(c);
1027 value_clear(c);
1029 return empty;