1 #include <isl/space.h>
2 #include <isl/set.h>
3 #include <isl/map.h>
4 #include <isl/union_set.h>
5 #include <isl/union_map.h>
6 #include <isl/polynomial.h>
7 #include <isl_set_polylib.h>
8 #include <barvinok/polylib.h>
9 #include <barvinok/options.h>
10 #include <barvinok/util.h>
11 #include "bernoulli.h"
12 #include "euler.h"
13 #include "laurent.h"
14 #include "laurent_old.h"
15 #include "summate.h"
16 #include "section_array.h"
17 #include "remove_equalities.h"
18
19 extern evalue *evalue_outer_floor(evalue *e);
20 extern int evalue_replace_floor(evalue *e, const evalue *floor, int var);
21 extern void evalue_drop_floor(evalue *e, const evalue *floor);
22
23 #define ALLOC(type) (type*)malloc(sizeof(type))
24 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
25
26 /* Apply the variable transformation specified by T and CP on
27 * the polynomial e. T expresses the old variables in terms
28 * of the new variables (and optionally also the new parameters),
29 * while CP expresses the old parameters in terms of the new
30 * parameters.
31 */
transform_polynomial(evalue * E,Matrix * T,Matrix * CP,unsigned nvar,unsigned nparam,unsigned new_nvar,unsigned new_nparam)32 static void transform_polynomial(evalue *E, Matrix *T, Matrix *CP,
33 unsigned nvar, unsigned nparam,
34 unsigned new_nvar, unsigned new_nparam)
35 {
36 int j;
37 evalue **subs;
38
39 subs = ALLOCN(evalue *, nvar+nparam);
40
41 for (j = 0; j < nvar; ++j) {
42 if (T)
43 subs[j] = affine2evalue(T->p[j], T->p[T->NbRows-1][T->NbColumns-1],
44 T->NbColumns-1);
45 else
46 subs[j] = evalue_var(j);
47 }
48 for (j = 0; j < nparam; ++j) {
49 if (CP)
50 subs[nvar+j] = affine2evalue(CP->p[j], CP->p[nparam][new_nparam],
51 new_nparam);
52 else
53 subs[nvar+j] = evalue_var(j);
54 evalue_shift_variables(subs[nvar+j], 0, new_nvar);
55 }
56
57 evalue_substitute(E, subs);
58 reduce_evalue(E);
59
60 for (j = 0; j < nvar+nparam; ++j)
61 evalue_free(subs[j]);
62 free(subs);
63 }
64
65 /* Compute the sum of the quasi-polynomial E
66 * over a 0D (non-empty, but possibly parametric) polytope P.
67 *
68 * Consumes P and E.
69 *
70 * We simply return a partition evalue with P as domain and E as value.
71 */
sum_over_polytope_0D(Polyhedron * P,evalue * E)72 static evalue *sum_over_polytope_0D(Polyhedron *P, evalue *E)
73 {
74 evalue *sum;
75
76 sum = ALLOC(evalue);
77 value_init(sum->d);
78 sum->x.p = new_enode(partition, 2, P->Dimension);
79 EVALUE_SET_DOMAIN(sum->x.p->arr[0], P);
80 value_clear(sum->x.p->arr[1].d);
81 sum->x.p->arr[1] = *E;
82 free(E);
83
84 return sum;
85 }
86
sum_with_equalities(Polyhedron * P,evalue * E,unsigned nvar,struct evalue_section_array * sections,struct barvinok_options * options,evalue * (* base)(Polyhedron * P,evalue * E,unsigned nvar,struct evalue_section_array * sections,struct barvinok_options * options))87 static evalue *sum_with_equalities(Polyhedron *P, evalue *E,
88 unsigned nvar, struct evalue_section_array *sections,
89 struct barvinok_options *options,
90 evalue *(*base)(Polyhedron *P, evalue *E, unsigned nvar,
91 struct evalue_section_array *sections,
92 struct barvinok_options *options))
93 {
94 unsigned dim = P->Dimension;
95 unsigned new_dim, new_nparam;
96 Matrix *T = NULL, *CP = NULL;
97 evalue *sum;
98
99 if (emptyQ(P))
100 return evalue_zero();
101
102 assert(P->NbEq > 0);
103
104 remove_all_equalities(&P, NULL, &CP, &T, dim-nvar, options->MaxRays);
105
106 if (emptyQ(P)) {
107 Polyhedron_Free(P);
108 return evalue_zero();
109 }
110
111 new_nparam = CP ? CP->NbColumns-1 : dim - nvar;
112 new_dim = T ? T->NbColumns-1 : nvar + new_nparam;
113
114 /* We can avoid these substitutions if E is a constant */
115 E = evalue_dup(E);
116 transform_polynomial(E, T, CP, nvar, dim-nvar,
117 new_dim-new_nparam, new_nparam);
118
119 if (new_dim-new_nparam > 0) {
120 sum = base(P, E, new_dim-new_nparam, sections, options);
121 evalue_free(E);
122 Polyhedron_Free(P);
123 } else {
124 sum = sum_over_polytope_0D(P, E);
125 }
126
127 if (CP) {
128 evalue_backsubstitute(sum, CP, options->MaxRays);
129 Matrix_Free(CP);
130 }
131
132 if (T)
133 Matrix_Free(T);
134
135 return sum;
136 }
137
sum_over_polytope_with_equalities(Polyhedron * P,evalue * E,unsigned nvar,struct evalue_section_array * sections,struct barvinok_options * options)138 static evalue *sum_over_polytope_with_equalities(Polyhedron *P, evalue *E,
139 unsigned nvar, struct evalue_section_array *sections,
140 struct barvinok_options *options)
141 {
142 return sum_with_equalities(P, E, nvar, sections, options,
143 &barvinok_sum_over_polytope);
144 }
145
146 static evalue *sum_base(Polyhedron *P, evalue *E, unsigned nvar,
147 struct barvinok_options *options);
148
sum_base_wrap(Polyhedron * P,evalue * E,unsigned nvar,struct evalue_section_array * sections,struct barvinok_options * options)149 static evalue *sum_base_wrap(Polyhedron *P, evalue *E, unsigned nvar,
150 struct evalue_section_array *sections, struct barvinok_options *options)
151 {
152 return sum_base(P, E, nvar, options);
153 }
154
sum_base_with_equalities(Polyhedron * P,evalue * E,unsigned nvar,struct barvinok_options * options)155 static evalue *sum_base_with_equalities(Polyhedron *P, evalue *E,
156 unsigned nvar, struct barvinok_options *options)
157 {
158 return sum_with_equalities(P, E, nvar, NULL, options, &sum_base_wrap);
159 }
160
161 /* The substitutions in sum_step_polynomial may have reintroduced equalities
162 * (in particular, one of the floor expressions may be equal to one of
163 * the variables), so we need to check for them again.
164 */
sum_base(Polyhedron * P,evalue * E,unsigned nvar,struct barvinok_options * options)165 static evalue *sum_base(Polyhedron *P, evalue *E, unsigned nvar,
166 struct barvinok_options *options)
167 {
168 if (P->NbEq)
169 return sum_base_with_equalities(P, E, nvar, options);
170 if (options->summation == BV_SUM_EULER)
171 return euler_summate(P, E, nvar, options);
172 else if (options->summation == BV_SUM_LAURENT)
173 return laurent_summate(P, E, nvar, options);
174 else if (options->summation == BV_SUM_LAURENT_OLD)
175 return laurent_summate_old(P, E, nvar, options);
176 assert(0);
177 }
178
179 /* Count the number of non-zero terms in e when viewed as a polynomial
180 * in only the first nvar variables. "count" is the number counted
181 * so far.
182 */
evalue_count_terms(const evalue * e,unsigned nvar,int count)183 static int evalue_count_terms(const evalue *e, unsigned nvar, int count)
184 {
185 int i;
186
187 if (EVALUE_IS_ZERO(*e))
188 return count;
189
190 if (value_zero_p(e->d))
191 assert(e->x.p->type == polynomial);
192 if (value_notzero_p(e->d) || e->x.p->pos >= nvar+1)
193 return count+1;
194
195 for (i = 0; i < e->x.p->size; ++i)
196 count = evalue_count_terms(&e->x.p->arr[i], nvar, count);
197
198 return count;
199 }
200
201 /* Create placeholder structure for unzipping.
202 * A "polynomial" is created with size terms in variable pos,
203 * with each term having itself as coefficient.
204 */
create_placeholder(int size,int pos)205 static evalue *create_placeholder(int size, int pos)
206 {
207 int i, j;
208 evalue *E = ALLOC(evalue);
209 value_init(E->d);
210 E->x.p = new_enode(polynomial, size, pos+1);
211 for (i = 0; i < size; ++i) {
212 E->x.p->arr[i].x.p = new_enode(polynomial, i+1, pos+1);
213 for (j = 0; j < i; ++j)
214 evalue_set_si(&E->x.p->arr[i].x.p->arr[j], 0, 1);
215 evalue_set_si(&E->x.p->arr[i].x.p->arr[i], 1, 1);
216 }
217 return E;
218 }
219
220 /* Interchange each non-zero term in e (when viewed as a polynomial
221 * in only the first nvar variables) with a placeholder in ph (created
222 * by create_placeholder), resulting in two polynomials in the
223 * placeholder variable such that for each non-zero term in e
224 * there is a power of the placeholder variable such that the factors
225 * in the first nvar variables form the coefficient of that power in
226 * the first polynomial (e) and the factors in the remaining variables
227 * form the coefficient of that power in the second polynomial (ph).
228 */
evalue_unzip_terms(evalue * e,evalue * ph,unsigned nvar,int count)229 static int evalue_unzip_terms(evalue *e, evalue *ph, unsigned nvar, int count)
230 {
231 int i;
232
233 if (EVALUE_IS_ZERO(*e))
234 return count;
235
236 if (value_zero_p(e->d))
237 assert(e->x.p->type == polynomial);
238 if (value_notzero_p(e->d) || e->x.p->pos >= nvar+1) {
239 evalue t = *e;
240 *e = ph->x.p->arr[count];
241 ph->x.p->arr[count] = t;
242 return count+1;
243 }
244
245 for (i = 0; i < e->x.p->size; ++i)
246 count = evalue_unzip_terms(&e->x.p->arr[i], ph, nvar, count);
247
248 return count;
249 }
250
251 /* Remove n variables at pos (0-based) from the polyhedron P.
252 * Each of these variables is assumed to be completely free,
253 * i.e., there is a line in the polyhedron corresponding to
254 * each of these variables.
255 */
Polyhedron_Remove_Columns(Polyhedron * P,unsigned pos,unsigned n)256 static Polyhedron *Polyhedron_Remove_Columns(Polyhedron *P, unsigned pos,
257 unsigned n)
258 {
259 int i, j;
260 unsigned NbConstraints = 0;
261 unsigned NbRays = 0;
262 Polyhedron *Q;
263
264 if (n == 0)
265 return P;
266
267 assert(pos <= P->Dimension);
268
269 if (POL_HAS(P, POL_INEQUALITIES))
270 NbConstraints = P->NbConstraints;
271 if (POL_HAS(P, POL_POINTS))
272 NbRays = P->NbRays - n;
273
274 Q = Polyhedron_Alloc(P->Dimension - n, NbConstraints, NbRays);
275 if (POL_HAS(P, POL_INEQUALITIES)) {
276 Q->NbEq = P->NbEq;
277 for (i = 0; i < P->NbConstraints; ++i) {
278 Vector_Copy(P->Constraint[i], Q->Constraint[i], 1+pos);
279 Vector_Copy(P->Constraint[i]+1+pos+n, Q->Constraint[i]+1+pos,
280 Q->Dimension-pos+1);
281 }
282 }
283 if (POL_HAS(P, POL_POINTS)) {
284 Q->NbBid = P->NbBid - n;
285 for (i = 0; i < n; ++i)
286 value_set_si(Q->Ray[i][1+pos+i], 1);
287 for (i = 0, j = 0; i < P->NbRays; ++i) {
288 int line = First_Non_Zero(P->Ray[i], 1+P->Dimension+1);
289 assert(line != -1);
290 if (line-1 >= pos && line-1 < pos+n) {
291 ++j;
292 assert(j <= n);
293 continue;
294 }
295 assert(i-j < Q->NbRays);
296 Vector_Copy(P->Ray[i], Q->Ray[i-j], 1+pos);
297 Vector_Copy(P->Ray[i]+1+pos+n, Q->Ray[i-j]+1+pos,
298 Q->Dimension-pos+1);
299 }
300 }
301 POL_SET(Q, POL_VALID);
302 if (POL_HAS(P, POL_INEQUALITIES))
303 POL_SET(Q, POL_INEQUALITIES);
304 if (POL_HAS(P, POL_POINTS))
305 POL_SET(Q, POL_POINTS);
306 if (POL_HAS(P, POL_VERTICES))
307 POL_SET(Q, POL_VERTICES);
308 return Q;
309 }
310
311 /* Remove n variables at pos (0-based) from the union of polyhedra P.
312 * Each of these variables is assumed to be completely free,
313 * i.e., there is a line in the polyhedron corresponding to
314 * each of these variables.
315 */
Domain_Remove_Columns(Polyhedron * P,unsigned pos,unsigned n)316 static Polyhedron *Domain_Remove_Columns(Polyhedron *P, unsigned pos,
317 unsigned n)
318 {
319 Polyhedron *R;
320 Polyhedron **next = &R;
321
322 for (; P; P = P->next) {
323 *next = Polyhedron_Remove_Columns(P, pos, n);
324 next = &(*next)->next;
325 }
326 return R;
327 }
328
329 /* Drop n parameters starting at first from partition evalue e */
drop_parameters(evalue * e,int first,int n)330 static void drop_parameters(evalue *e, int first, int n)
331 {
332 int i;
333
334 if (EVALUE_IS_ZERO(*e))
335 return;
336
337 assert(value_zero_p(e->d) && e->x.p->type == partition);
338 for (i = 0; i < e->x.p->size/2; ++i) {
339 Polyhedron *P = EVALUE_DOMAIN(e->x.p->arr[2*i]);
340 Polyhedron *Q = Domain_Remove_Columns(P, first, n);
341 EVALUE_SET_DOMAIN(e->x.p->arr[2*i], Q);
342 Domain_Free(P);
343 evalue_shift_variables(&e->x.p->arr[2*i+1], first, -n);
344 }
345 e->x.p->pos -= n;
346 }
347
extract_term_into(const evalue * src,int var,int exp,evalue * dst)348 static void extract_term_into(const evalue *src, int var, int exp, evalue *dst)
349 {
350 int i;
351
352 if (value_notzero_p(src->d) ||
353 src->x.p->type != polynomial ||
354 src->x.p->pos > var+1) {
355 if (exp == 0)
356 evalue_copy(dst, src);
357 else
358 evalue_set_si(dst, 0, 1);
359 return;
360 }
361
362 if (src->x.p->pos == var+1) {
363 if (src->x.p->size > exp)
364 evalue_copy(dst, &src->x.p->arr[exp]);
365 else
366 evalue_set_si(dst, 0, 1);
367 return;
368 }
369
370 dst->x.p = new_enode(polynomial, src->x.p->size, src->x.p->pos);
371 for (i = 0; i < src->x.p->size; ++i)
372 extract_term_into(&src->x.p->arr[i], var, exp,
373 &dst->x.p->arr[i]);
374 }
375
376 /* Extract the coefficient of var^exp.
377 */
extract_term(const evalue * e,int var,int exp)378 static evalue *extract_term(const evalue *e, int var, int exp)
379 {
380 int i;
381 evalue *res;
382
383 if (EVALUE_IS_ZERO(*e))
384 return evalue_zero();
385
386 assert(value_zero_p(e->d) && e->x.p->type == partition);
387 res = ALLOC(evalue);
388 value_init(res->d);
389 res->x.p = new_enode(partition, e->x.p->size, e->x.p->pos);
390 for (i = 0; i < e->x.p->size/2; ++i) {
391 EVALUE_SET_DOMAIN(res->x.p->arr[2*i],
392 Domain_Copy(EVALUE_DOMAIN(e->x.p->arr[2*i])));
393 extract_term_into(&e->x.p->arr[2*i+1], var, exp,
394 &res->x.p->arr[2*i+1]);
395 reduce_evalue(&res->x.p->arr[2*i+1]);
396 }
397 return res;
398 }
399
400 /* Insert n free variables at pos (0-based) in the polyhedron P.
401 */
Polyhedron_Insert_Columns(Polyhedron * P,unsigned pos,unsigned n)402 static Polyhedron *Polyhedron_Insert_Columns(Polyhedron *P, unsigned pos,
403 unsigned n)
404 {
405 int i;
406 unsigned NbConstraints = 0;
407 unsigned NbRays = 0;
408 Polyhedron *Q;
409
410 if (!P)
411 return P;
412 if (n == 0)
413 return P;
414
415 assert(pos <= P->Dimension);
416
417 if (POL_HAS(P, POL_INEQUALITIES))
418 NbConstraints = P->NbConstraints;
419 if (POL_HAS(P, POL_POINTS))
420 NbRays = P->NbRays + n;
421
422 Q = Polyhedron_Alloc(P->Dimension+n, NbConstraints, NbRays);
423 if (POL_HAS(P, POL_INEQUALITIES)) {
424 Q->NbEq = P->NbEq;
425 for (i = 0; i < P->NbConstraints; ++i) {
426 Vector_Copy(P->Constraint[i], Q->Constraint[i], 1+pos);
427 Vector_Copy(P->Constraint[i]+1+pos, Q->Constraint[i]+1+pos+n,
428 P->Dimension-pos+1);
429 }
430 }
431 if (POL_HAS(P, POL_POINTS)) {
432 Q->NbBid = P->NbBid + n;
433 for (i = 0; i < n; ++i)
434 value_set_si(Q->Ray[i][1+pos+i], 1);
435 for (i = 0; i < P->NbRays; ++i) {
436 Vector_Copy(P->Ray[i], Q->Ray[n+i], 1+pos);
437 Vector_Copy(P->Ray[i]+1+pos, Q->Ray[n+i]+1+pos+n,
438 P->Dimension-pos+1);
439 }
440 }
441 POL_SET(Q, POL_VALID);
442 if (POL_HAS(P, POL_INEQUALITIES))
443 POL_SET(Q, POL_INEQUALITIES);
444 if (POL_HAS(P, POL_POINTS))
445 POL_SET(Q, POL_POINTS);
446 if (POL_HAS(P, POL_VERTICES))
447 POL_SET(Q, POL_VERTICES);
448 return Q;
449 }
450
451 /* Perform summation of e over a list of 1 or more factors F, with context C.
452 * nvar is the total number of variables in the remaining factors.
453 * extra is the number of placeholder parameters introduced in e,
454 * but not (yet) in F or C.
455 *
456 * If there is only one factor left, F is intersected with the
457 * context C, the placeholder variables are added, and then
458 * e is summed over the resulting parametric polytope.
459 *
460 * If there is more than one factor left, we create two polynomials
461 * in a new placeholder variable (which is placed after the regular
462 * parameters, but before any previously introduced placeholder
463 * variables) that has the factors of the variables in the first
464 * factor of F and the factor of the remaining variables of
465 * each term as its coefficients.
466 * These two polynomials are then summed over their domains
467 * and afterwards the results are combined and the placeholder
468 * variable is removed again.
469 */
sum_factors(Polyhedron * F,Polyhedron * C,evalue * e,unsigned nvar,unsigned extra,struct barvinok_options * options)470 static evalue *sum_factors(Polyhedron *F, Polyhedron *C, evalue *e,
471 unsigned nvar, unsigned extra,
472 struct barvinok_options *options)
473 {
474 unsigned nparam = C->Dimension;
475 unsigned F_var = F->Dimension - C->Dimension;
476 int i, n;
477 evalue *s1, *s2, *s;
478 evalue *ph;
479
480 if (!F->next) {
481 Polyhedron *CA = align_context(C, nvar+nparam, options->MaxRays);
482 Polyhedron *P = DomainIntersection(F, CA, options->MaxRays);
483 Polyhedron *Q = Polyhedron_Insert_Columns(P, nvar+nparam, extra);
484 Polyhedron_Free(CA);
485 Polyhedron_Free(F);
486 Polyhedron_Free(P);
487 evalue *sum = sum_base(Q, e, nvar, options);
488 Polyhedron_Free(Q);
489 return sum;
490 }
491
492 n = evalue_count_terms(e, F_var, 0);
493 ph = create_placeholder(n, nvar+nparam);
494 evalue_shift_variables(e, nvar+nparam, 1);
495 evalue_unzip_terms(e, ph, F_var, 0);
496 evalue_shift_variables(e, nvar, -(nvar-F_var));
497 evalue_reorder_terms(ph);
498 evalue_shift_variables(ph, 0, -F_var);
499
500 s2 = sum_factors(F->next, C, ph, nvar-F_var, extra+1, options);
501 evalue_free(ph);
502 F->next = NULL;
503 s1 = sum_factors(F, C, e, F_var, extra+1, options);
504
505 if (n == 1) {
506 /* remove placeholder "polynomial" */
507 reduce_evalue(s1);
508 emul(s1, s2);
509 evalue_free(s1);
510 drop_parameters(s2, nparam, 1);
511 return s2;
512 }
513
514 s = evalue_zero();
515 for (i = 0; i < n; ++i) {
516 evalue *t1, *t2;
517 t1 = extract_term(s1, nparam, i);
518 t2 = extract_term(s2, nparam, i);
519 emul(t1, t2);
520 eadd(t2, s);
521 evalue_free(t1);
522 evalue_free(t2);
523 }
524 evalue_free(s1);
525 evalue_free(s2);
526
527 drop_parameters(s, nparam, 1);
528 return s;
529 }
530
531 /* Perform summation over a product of factors F, obtained using
532 * variable transformation T from the original problem specification.
533 *
534 * We first perform the corresponding transformation on the polynomial E,
535 * compute the common context over all factors and then perform
536 * the actual summation over the factors.
537 */
sum_product(Polyhedron * F,evalue * E,Matrix * T,unsigned nparam,struct barvinok_options * options)538 static evalue *sum_product(Polyhedron *F, evalue *E, Matrix *T, unsigned nparam,
539 struct barvinok_options *options)
540 {
541 int i;
542 Matrix *T2;
543 unsigned nvar = T->NbRows;
544 Polyhedron *C;
545 evalue *sum;
546
547 assert(nvar == T->NbColumns);
548 T2 = Matrix_Alloc(nvar+1, nvar+1);
549 for (i = 0; i < nvar; ++i)
550 Vector_Copy(T->p[i], T2->p[i], nvar);
551 value_set_si(T2->p[nvar][nvar], 1);
552
553 transform_polynomial(E, T2, NULL, nvar, nparam, nvar, nparam);
554
555 C = Factor_Context(F, nparam, options->MaxRays);
556 if (F->Dimension == nparam) {
557 Polyhedron *T = F;
558 F = F->next;
559 T->next = NULL;
560 Polyhedron_Free(T);
561 }
562 sum = sum_factors(F, C, E, nvar, 0, options);
563
564 Polyhedron_Free(C);
565 Matrix_Free(T2);
566 Matrix_Free(T);
567 return sum;
568 }
569
570 /* Add two constraints corresponding to floor = floor(e/d),
571 *
572 * e - d t >= 0
573 * -e + d t + d-1 >= 0
574 *
575 * e is assumed to be an affine expression.
576 */
add_floor_var(Polyhedron * P,unsigned nvar,const evalue * floor,struct barvinok_options * options)577 Polyhedron *add_floor_var(Polyhedron *P, unsigned nvar, const evalue *floor,
578 struct barvinok_options *options)
579 {
580 int i;
581 unsigned dim = P->Dimension+1;
582 Matrix *M = Matrix_Alloc(P->NbConstraints+2, 2+dim);
583 Polyhedron *CP;
584 Value *d = &M->p[0][1+nvar];
585 evalue_extract_affine(floor, M->p[0]+1, M->p[0]+1+dim, d);
586 value_oppose(*d, *d);
587 value_set_si(M->p[0][0], 1);
588 value_set_si(M->p[1][0], 1);
589 Vector_Oppose(M->p[0]+1, M->p[1]+1, M->NbColumns-1);
590 value_subtract(M->p[1][1+dim], M->p[1][1+dim], *d);
591 value_decrement(M->p[1][1+dim], M->p[1][1+dim]);
592
593 for (i = 0; i < P->NbConstraints; ++i) {
594 Vector_Copy(P->Constraint[i], M->p[i+2], 1+nvar);
595 Vector_Copy(P->Constraint[i]+1+nvar, M->p[i+2]+1+nvar+1, dim-nvar-1+1);
596 }
597
598 CP = Constraints2Polyhedron(M, options->MaxRays);
599 Matrix_Free(M);
600 return CP;
601 }
602
evalue_add(evalue * a,evalue * b)603 static evalue *evalue_add(evalue *a, evalue *b)
604 {
605 if (!a)
606 return b;
607 if (!b)
608 return a;
609 eadd(a, b);
610 evalue_free(a);
611 return b;
612 }
613
614 /* Compute sum of a step-polynomial over a polytope by grouping
615 * terms containing the same floor-expressions and introducing
616 * new variables for each such expression.
617 * In particular, while there is any floor-expression left,
618 * the step-polynomial is split into a polynomial containing
619 * the expression, which is then converted to a new variable,
620 * and a polynomial not containing the expression.
621 */
sum_step_polynomial(Polyhedron * P,evalue * E,unsigned nvar,struct barvinok_options * options)622 static evalue *sum_step_polynomial(Polyhedron *P, evalue *E, unsigned nvar,
623 struct barvinok_options *options)
624 {
625 evalue *floor;
626 evalue *cur = E;
627 evalue *sum = NULL;
628 evalue *t;
629
630 while ((floor = evalue_outer_floor(cur))) {
631 Polyhedron *CP;
632 evalue *converted;
633 evalue *converted_floor;
634
635 /* Ignore floors that do not depend on variables. */
636 if (value_notzero_p(floor->d) || floor->x.p->pos >= nvar+1)
637 break;
638
639 converted = evalue_dup(cur);
640 converted_floor = evalue_dup(floor);
641 evalue_shift_variables(converted, nvar, 1);
642 evalue_shift_variables(converted_floor, nvar, 1);
643 evalue_replace_floor(converted, converted_floor, nvar);
644 CP = add_floor_var(P, nvar, converted_floor, options);
645 evalue_free(converted_floor);
646 t = sum_step_polynomial(CP, converted, nvar+1, options);
647 evalue_free(converted);
648 Polyhedron_Free(CP);
649 sum = evalue_add(t, sum);
650
651 if (cur == E)
652 cur = evalue_dup(cur);
653 evalue_drop_floor(cur, floor);
654 evalue_free(floor);
655 }
656 if (floor) {
657 evalue_floor2frac(cur);
658 evalue_free(floor);
659 }
660
661 if (EVALUE_IS_ZERO(*cur))
662 t = NULL;
663 else {
664 Matrix *T;
665 unsigned nparam = P->Dimension - nvar;
666 Polyhedron *F = Polyhedron_Factor(P, nparam, &T, options->MaxRays);
667 if (!F)
668 t = sum_base(P, cur, nvar, options);
669 else {
670 if (cur == E)
671 cur = evalue_dup(cur);
672 t = sum_product(F, cur, T, nparam, options);
673 }
674 }
675
676 if (E != cur)
677 evalue_free(cur);
678
679 return evalue_add(t, sum);
680 }
681
barvinok_sum_over_polytope(Polyhedron * P,evalue * E,unsigned nvar,struct evalue_section_array * sections,struct barvinok_options * options)682 evalue *barvinok_sum_over_polytope(Polyhedron *P, evalue *E, unsigned nvar,
683 struct evalue_section_array *sections,
684 struct barvinok_options *options)
685 {
686 if (P->NbEq)
687 return sum_over_polytope_with_equalities(P, E, nvar, sections, options);
688
689 if (nvar == 0)
690 return sum_over_polytope_0D(Polyhedron_Copy(P), evalue_dup(E));
691
692 if (options->summation == BV_SUM_BERNOULLI)
693 return bernoulli_summate(P, E, nvar, sections, options);
694 else if (options->summation == BV_SUM_BOX)
695 return box_summate(P, E, nvar, options->MaxRays);
696
697 evalue_frac2floor2(E, 0);
698
699 return sum_step_polynomial(P, E, nvar, options);
700 }
701
barvinok_summate(evalue * e,int nvar,struct barvinok_options * options)702 evalue *barvinok_summate(evalue *e, int nvar, struct barvinok_options *options)
703 {
704 int i;
705 struct evalue_section_array sections;
706 evalue *sum;
707
708 assert(nvar >= 0);
709 if (nvar == 0 || EVALUE_IS_ZERO(*e))
710 return evalue_dup(e);
711
712 assert(value_zero_p(e->d));
713 assert(e->x.p->type == partition);
714
715 evalue_section_array_init(§ions);
716 sum = evalue_zero();
717
718 for (i = 0; i < e->x.p->size/2; ++i) {
719 Polyhedron *D;
720 for (D = EVALUE_DOMAIN(e->x.p->arr[2*i]); D; D = D->next) {
721 Polyhedron *next = D->next;
722 evalue *tmp;
723 D->next = NULL;
724
725 tmp = barvinok_sum_over_polytope(D, &e->x.p->arr[2*i+1], nvar,
726 §ions, options);
727 assert(tmp);
728 eadd(tmp, sum);
729 evalue_free(tmp);
730
731 D->next = next;
732 }
733 }
734
735 free(sections.s);
736
737 reduce_evalue(sum);
738 return sum;
739 }
740
add_unbounded_guarded_qp(__isl_take isl_pw_qpolynomial * sum,__isl_take isl_basic_set * bset,__isl_take isl_qpolynomial * qp)741 static __isl_give isl_pw_qpolynomial *add_unbounded_guarded_qp(
742 __isl_take isl_pw_qpolynomial *sum,
743 __isl_take isl_basic_set *bset, __isl_take isl_qpolynomial *qp)
744 {
745 int zero;
746
747 if (!sum || !bset || !qp)
748 goto error;
749
750 zero = isl_qpolynomial_is_zero(qp);
751 if (zero < 0)
752 goto error;
753
754 if (!zero) {
755 isl_space *space;
756 isl_set *set;
757 isl_pw_qpolynomial *pwqp;
758
759 space = isl_pw_qpolynomial_get_domain_space(sum);
760 set = isl_set_from_basic_set(isl_basic_set_copy(bset));
761 set = isl_map_domain(isl_map_from_range(set));
762 set = isl_set_reset_space(set, isl_space_copy(space));
763 pwqp = isl_pw_qpolynomial_alloc(set,
764 isl_qpolynomial_nan_on_domain(space));
765 sum = isl_pw_qpolynomial_add(sum, pwqp);
766 }
767
768 isl_basic_set_free(bset);
769 isl_qpolynomial_free(qp);
770 return sum;
771 error:
772 isl_basic_set_free(bset);
773 isl_qpolynomial_free(qp);
774 isl_pw_qpolynomial_free(sum);
775 return NULL;
776 }
777
778 struct barvinok_summate_data {
779 isl_space *space;
780 isl_qpolynomial *qp;
781 isl_pw_qpolynomial *sum;
782 int n_in;
783 int wrapping;
784 evalue *e;
785 struct evalue_section_array sections;
786 struct barvinok_options *options;
787 };
788
add_basic_guarded_qp(__isl_take isl_basic_set * bset,void * user)789 static isl_stat add_basic_guarded_qp(__isl_take isl_basic_set *bset, void *user)
790 {
791 struct barvinok_summate_data *data = user;
792 Polyhedron *P;
793 evalue *tmp;
794 isl_pw_qpolynomial *pwqp;
795 int bounded;
796 unsigned nvar = isl_basic_set_dim(bset, isl_dim_set);
797 isl_space *space;
798
799 if (!bset)
800 return isl_stat_error;
801
802 bounded = isl_basic_set_is_bounded(bset);
803 if (bounded < 0)
804 goto error;
805
806 if (!bounded) {
807 data->sum = add_unbounded_guarded_qp(data->sum, bset,
808 isl_qpolynomial_copy(data->qp));
809 return isl_stat_ok;
810 }
811
812 space = isl_space_params(isl_basic_set_get_space(bset));
813
814 P = isl_basic_set_to_polylib(bset);
815 tmp = barvinok_sum_over_polytope(P, data->e, nvar,
816 &data->sections, data->options);
817 Polyhedron_Free(P);
818 assert(tmp);
819 pwqp = isl_pw_qpolynomial_from_evalue(space, tmp);
820 evalue_free(tmp);
821 pwqp = isl_pw_qpolynomial_reset_domain_space(pwqp,
822 isl_space_domain(isl_space_copy(data->space)));
823 data->sum = isl_pw_qpolynomial_add(data->sum, pwqp);
824
825 isl_basic_set_free(bset);
826
827 return isl_stat_ok;
828 error:
829 isl_basic_set_free(bset);
830 return isl_stat_error;
831 }
832
add_guarded_qp(__isl_take isl_set * set,__isl_take isl_qpolynomial * qp,void * user)833 static isl_stat add_guarded_qp(__isl_take isl_set *set,
834 __isl_take isl_qpolynomial *qp, void *user)
835 {
836 isl_stat r;
837 struct barvinok_summate_data *data = user;
838
839 if (!set || !qp)
840 goto error;
841
842 data->qp = qp;
843
844 if (data->wrapping) {
845 unsigned nparam = isl_set_dim(set, isl_dim_param);
846 isl_qpolynomial *qp2 = isl_qpolynomial_copy(qp);
847 set = isl_set_move_dims(set, isl_dim_param, nparam,
848 isl_dim_set, 0, data->n_in);
849 qp2 = isl_qpolynomial_move_dims(qp2, isl_dim_param, nparam,
850 isl_dim_in, 0, data->n_in);
851 data->e = isl_qpolynomial_to_evalue(qp2);
852 isl_qpolynomial_free(qp2);
853 } else
854 data->e = isl_qpolynomial_to_evalue(qp);
855 if (!data->e)
856 goto error;
857
858 evalue_section_array_init(&data->sections);
859
860 set = isl_set_make_disjoint(set);
861 set = isl_set_compute_divs(set);
862
863 r = isl_set_foreach_basic_set(set, &add_basic_guarded_qp, data);
864
865 free(data->sections.s);
866
867 evalue_free(data->e);
868
869 isl_set_free(set);
870 isl_qpolynomial_free(qp);
871
872 return r;
873 error:
874 isl_set_free(set);
875 isl_qpolynomial_free(qp);
876 return isl_stat_error;
877 }
878
isl_pw_qpolynomial_sum(__isl_take isl_pw_qpolynomial * pwqp)879 __isl_give isl_pw_qpolynomial *isl_pw_qpolynomial_sum(
880 __isl_take isl_pw_qpolynomial *pwqp)
881 {
882 isl_ctx *ctx;
883 struct barvinok_summate_data data;
884 int options_allocated = 0;
885 int nvar;
886
887 data.space = NULL;
888 data.options = NULL;
889 data.sum = NULL;
890
891 if (!pwqp)
892 return NULL;
893
894 nvar = isl_pw_qpolynomial_dim(pwqp, isl_dim_set);
895
896 data.space = isl_pw_qpolynomial_get_domain_space(pwqp);
897 if (!data.space)
898 goto error;
899 if (isl_space_is_params(data.space))
900 isl_die(isl_pw_qpolynomial_get_ctx(pwqp), isl_error_invalid,
901 "input polynomial has no domain", goto error);
902 data.wrapping = isl_space_is_wrapping(data.space);
903 if (data.wrapping) {
904 data.space = isl_space_unwrap(data.space);
905 data.n_in = isl_space_dim(data.space, isl_dim_in);
906 nvar = isl_space_dim(data.space, isl_dim_out);
907 } else
908 data.n_in = 0;
909
910 data.space = isl_space_domain(data.space);
911 if (nvar == 0)
912 return isl_pw_qpolynomial_reset_domain_space(pwqp, data.space);
913
914 data.space = isl_space_from_domain(data.space);
915 data.space = isl_space_add_dims(data.space, isl_dim_out, 1);
916 data.sum = isl_pw_qpolynomial_zero(isl_space_copy(data.space));
917
918 ctx = isl_pw_qpolynomial_get_ctx(pwqp);
919 data.options = isl_ctx_peek_barvinok_options(ctx);
920 if (!data.options) {
921 data.options = barvinok_options_new_with_defaults();
922 options_allocated = 1;
923 }
924
925 if (isl_pw_qpolynomial_foreach_lifted_piece(pwqp,
926 add_guarded_qp, &data) < 0)
927 goto error;
928
929 if (options_allocated)
930 barvinok_options_free(data.options);
931
932 isl_space_free(data.space);
933
934 isl_pw_qpolynomial_free(pwqp);
935
936 return data.sum;
937 error:
938 if (options_allocated)
939 barvinok_options_free(data.options);
940 isl_pw_qpolynomial_free(pwqp);
941 isl_space_free(data.space);
942 isl_pw_qpolynomial_free(data.sum);
943 return NULL;
944 }
945
pw_qpolynomial_sum(__isl_take isl_pw_qpolynomial * pwqp,void * user)946 static isl_stat pw_qpolynomial_sum(__isl_take isl_pw_qpolynomial *pwqp,
947 void *user)
948 {
949 isl_union_pw_qpolynomial **res = (isl_union_pw_qpolynomial **)user;
950 isl_pw_qpolynomial *sum;
951 isl_union_pw_qpolynomial *upwqp;
952
953 sum = isl_pw_qpolynomial_sum(pwqp);
954 upwqp = isl_union_pw_qpolynomial_from_pw_qpolynomial(sum);
955 *res = isl_union_pw_qpolynomial_add(*res, upwqp);
956
957 return isl_stat_ok;
958 }
959
isl_union_pw_qpolynomial_sum(__isl_take isl_union_pw_qpolynomial * upwqp)960 __isl_give isl_union_pw_qpolynomial *isl_union_pw_qpolynomial_sum(
961 __isl_take isl_union_pw_qpolynomial *upwqp)
962 {
963 isl_space *dim;
964 isl_union_pw_qpolynomial *res;
965
966 dim = isl_union_pw_qpolynomial_get_space(upwqp);
967 res = isl_union_pw_qpolynomial_zero(dim);
968 if (isl_union_pw_qpolynomial_foreach_pw_qpolynomial(upwqp,
969 &pw_qpolynomial_sum, &res) < 0)
970 goto error;
971 isl_union_pw_qpolynomial_free(upwqp);
972
973 return res;
974 error:
975 isl_union_pw_qpolynomial_free(upwqp);
976 isl_union_pw_qpolynomial_free(res);
977 return NULL;
978 }
979
join_compatible(__isl_keep isl_space * space1,__isl_keep isl_space * space2)980 static int join_compatible(__isl_keep isl_space *space1,
981 __isl_keep isl_space *space2)
982 {
983 int m;
984 m = isl_space_has_equal_params(space1, space2);
985 if (m < 0 || !m)
986 return m;
987 return isl_space_tuple_is_equal(space1, isl_dim_out,
988 space2, isl_dim_in);
989 }
990
991 /* Compute the intersection of the range of the map and the domain
992 * of the piecewise quasipolynomial and then sum the associated
993 * quasipolynomial over all elements in this intersection.
994 *
995 * We first introduce some unconstrained dimensions in the
996 * piecewise quasipolynomial, intersect the resulting domain
997 * with the wrapped map and then compute the sum.
998 */
isl_map_apply_pw_qpolynomial(__isl_take isl_map * map,__isl_take isl_pw_qpolynomial * pwqp)999 __isl_give isl_pw_qpolynomial *isl_map_apply_pw_qpolynomial(
1000 __isl_take isl_map *map, __isl_take isl_pw_qpolynomial *pwqp)
1001 {
1002 isl_ctx *ctx;
1003 isl_set *dom;
1004 isl_space *map_dim;
1005 isl_space *pwqp_dim;
1006 unsigned n_in;
1007 int ok;
1008
1009 ctx = isl_map_get_ctx(map);
1010 if (!ctx)
1011 goto error;
1012
1013 map_dim = isl_map_get_space(map);
1014 pwqp_dim = isl_pw_qpolynomial_get_space(pwqp);
1015 ok = join_compatible(map_dim, pwqp_dim);
1016 isl_space_free(map_dim);
1017 isl_space_free(pwqp_dim);
1018 if (!ok)
1019 isl_die(ctx, isl_error_invalid, "incompatible dimensions",
1020 goto error);
1021
1022 n_in = isl_map_dim(map, isl_dim_in);
1023 pwqp = isl_pw_qpolynomial_insert_dims(pwqp, isl_dim_in, 0, n_in);
1024
1025 dom = isl_map_wrap(map);
1026 pwqp = isl_pw_qpolynomial_reset_domain_space(pwqp,
1027 isl_set_get_space(dom));
1028
1029 pwqp = isl_pw_qpolynomial_intersect_domain(pwqp, dom);
1030 pwqp = isl_pw_qpolynomial_sum(pwqp);
1031
1032 return pwqp;
1033 error:
1034 isl_map_free(map);
1035 isl_pw_qpolynomial_free(pwqp);
1036 return NULL;
1037 }
1038
isl_set_apply_pw_qpolynomial(__isl_take isl_set * set,__isl_take isl_pw_qpolynomial * pwqp)1039 __isl_give isl_pw_qpolynomial *isl_set_apply_pw_qpolynomial(
1040 __isl_take isl_set *set, __isl_take isl_pw_qpolynomial *pwqp)
1041 {
1042 isl_map *map;
1043
1044 map = isl_map_from_range(set);
1045 pwqp = isl_map_apply_pw_qpolynomial(map, pwqp);
1046 pwqp = isl_pw_qpolynomial_project_domain_on_params(pwqp);
1047 return pwqp;
1048 }
1049
1050 struct barvinok_apply_data {
1051 isl_union_pw_qpolynomial *upwqp;
1052 isl_union_pw_qpolynomial *res;
1053 isl_map *map;
1054 };
1055
pw_qpolynomial_apply(__isl_take isl_pw_qpolynomial * pwqp,void * user)1056 static isl_stat pw_qpolynomial_apply(__isl_take isl_pw_qpolynomial *pwqp,
1057 void *user)
1058 {
1059 isl_space *map_dim;
1060 isl_space *pwqp_dim;
1061 struct barvinok_apply_data *data = user;
1062 int ok;
1063
1064 map_dim = isl_map_get_space(data->map);
1065 pwqp_dim = isl_pw_qpolynomial_get_space(pwqp);
1066 ok = join_compatible(map_dim, pwqp_dim);
1067 isl_space_free(map_dim);
1068 isl_space_free(pwqp_dim);
1069
1070 if (ok) {
1071 isl_union_pw_qpolynomial *upwqp;
1072
1073 pwqp = isl_map_apply_pw_qpolynomial(isl_map_copy(data->map),
1074 pwqp);
1075 upwqp = isl_union_pw_qpolynomial_from_pw_qpolynomial(pwqp);
1076 data->res = isl_union_pw_qpolynomial_add(data->res, upwqp);
1077 } else
1078 isl_pw_qpolynomial_free(pwqp);
1079
1080 return isl_stat_ok;
1081 }
1082
map_apply(__isl_take isl_map * map,void * user)1083 static isl_stat map_apply(__isl_take isl_map *map, void *user)
1084 {
1085 struct barvinok_apply_data *data = user;
1086 isl_stat r;
1087
1088 data->map = map;
1089 r = isl_union_pw_qpolynomial_foreach_pw_qpolynomial(data->upwqp,
1090 &pw_qpolynomial_apply, data);
1091
1092 isl_map_free(map);
1093 return r;
1094 }
1095
isl_union_map_apply_union_pw_qpolynomial(__isl_take isl_union_map * umap,__isl_take isl_union_pw_qpolynomial * upwqp)1096 __isl_give isl_union_pw_qpolynomial *isl_union_map_apply_union_pw_qpolynomial(
1097 __isl_take isl_union_map *umap,
1098 __isl_take isl_union_pw_qpolynomial *upwqp)
1099 {
1100 isl_space *dim;
1101 struct barvinok_apply_data data;
1102
1103 upwqp = isl_union_pw_qpolynomial_align_params(upwqp,
1104 isl_union_map_get_space(umap));
1105 umap = isl_union_map_align_params(umap,
1106 isl_union_pw_qpolynomial_get_space(upwqp));
1107
1108 data.upwqp = upwqp;
1109 dim = isl_union_pw_qpolynomial_get_space(upwqp);
1110 data.res = isl_union_pw_qpolynomial_zero(dim);
1111 if (isl_union_map_foreach_map(umap, &map_apply, &data) < 0)
1112 goto error;
1113
1114 isl_union_map_free(umap);
1115 isl_union_pw_qpolynomial_free(upwqp);
1116
1117 return data.res;
1118 error:
1119 isl_union_map_free(umap);
1120 isl_union_pw_qpolynomial_free(upwqp);
1121 isl_union_pw_qpolynomial_free(data.res);
1122 return NULL;
1123 }
1124
1125 struct barvinok_apply_set_data {
1126 isl_union_pw_qpolynomial *upwqp;
1127 isl_union_pw_qpolynomial *res;
1128 isl_set *set;
1129 };
1130
pw_qpolynomial_apply_set(__isl_take isl_pw_qpolynomial * pwqp,void * user)1131 static isl_stat pw_qpolynomial_apply_set(__isl_take isl_pw_qpolynomial *pwqp,
1132 void *user)
1133 {
1134 isl_space *set_dim;
1135 isl_space *pwqp_dim;
1136 struct barvinok_apply_set_data *data = user;
1137 int ok;
1138
1139 set_dim = isl_set_get_space(data->set);
1140 pwqp_dim = isl_pw_qpolynomial_get_space(pwqp);
1141 ok = join_compatible(set_dim, pwqp_dim);
1142 isl_space_free(set_dim);
1143 isl_space_free(pwqp_dim);
1144
1145 if (ok) {
1146 isl_union_pw_qpolynomial *upwqp;
1147
1148 pwqp = isl_set_apply_pw_qpolynomial(isl_set_copy(data->set),
1149 pwqp);
1150 upwqp = isl_union_pw_qpolynomial_from_pw_qpolynomial(pwqp);
1151 data->res = isl_union_pw_qpolynomial_add(data->res, upwqp);
1152 } else
1153 isl_pw_qpolynomial_free(pwqp);
1154
1155 return isl_stat_ok;
1156 }
1157
set_apply(__isl_take isl_set * set,void * user)1158 static isl_stat set_apply(__isl_take isl_set *set, void *user)
1159 {
1160 struct barvinok_apply_set_data *data = user;
1161 isl_stat r;
1162
1163 data->set = set;
1164 r = isl_union_pw_qpolynomial_foreach_pw_qpolynomial(data->upwqp,
1165 &pw_qpolynomial_apply_set, data);
1166
1167 isl_set_free(set);
1168 return r;
1169 }
1170
isl_union_set_apply_union_pw_qpolynomial(__isl_take isl_union_set * uset,__isl_take isl_union_pw_qpolynomial * upwqp)1171 __isl_give isl_union_pw_qpolynomial *isl_union_set_apply_union_pw_qpolynomial(
1172 __isl_take isl_union_set *uset,
1173 __isl_take isl_union_pw_qpolynomial *upwqp)
1174 {
1175 isl_space *dim;
1176 struct barvinok_apply_set_data data;
1177
1178 upwqp = isl_union_pw_qpolynomial_align_params(upwqp,
1179 isl_union_set_get_space(uset));
1180 uset = isl_union_set_align_params(uset,
1181 isl_union_pw_qpolynomial_get_space(upwqp));
1182
1183 data.upwqp = upwqp;
1184 dim = isl_union_pw_qpolynomial_get_space(upwqp);
1185 data.res = isl_union_pw_qpolynomial_zero(dim);
1186 if (isl_union_set_foreach_set(uset, &set_apply, &data) < 0)
1187 goto error;
1188
1189 isl_union_set_free(uset);
1190 isl_union_pw_qpolynomial_free(upwqp);
1191
1192 return data.res;
1193 error:
1194 isl_union_set_free(uset);
1195 isl_union_pw_qpolynomial_free(upwqp);
1196 isl_union_pw_qpolynomial_free(data.res);
1197 return NULL;
1198 }
1199
evalue_sum(evalue * E,int nvar,unsigned MaxRays)1200 evalue *evalue_sum(evalue *E, int nvar, unsigned MaxRays)
1201 {
1202 evalue *sum;
1203 struct barvinok_options *options = barvinok_options_new_with_defaults();
1204 options->MaxRays = MaxRays;
1205 sum = barvinok_summate(E, nvar, options);
1206 barvinok_options_free(options);
1207 return sum;
1208 }
1209
esum(evalue * e,int nvar)1210 evalue *esum(evalue *e, int nvar)
1211 {
1212 evalue *sum;
1213 struct barvinok_options *options = barvinok_options_new_with_defaults();
1214 sum = barvinok_summate(e, nvar, options);
1215 barvinok_options_free(options);
1216 return sum;
1217 }
1218
1219 /* Turn unweighted counting problem into "weighted" counting problem
1220 * with weight equal to 1 and call barvinok_summate on this weighted problem.
1221 */
barvinok_summate_unweighted(Polyhedron * P,Polyhedron * C,struct barvinok_options * options)1222 evalue *barvinok_summate_unweighted(Polyhedron *P, Polyhedron *C,
1223 struct barvinok_options *options)
1224 {
1225 Polyhedron *CA, *D;
1226 evalue e;
1227 evalue *sum;
1228
1229 if (emptyQ(P) || emptyQ(C))
1230 return evalue_zero();
1231
1232 CA = align_context(C, P->Dimension, options->MaxRays);
1233 D = DomainIntersection(P, CA, options->MaxRays);
1234 Domain_Free(CA);
1235
1236 if (emptyQ(D)) {
1237 Domain_Free(D);
1238 return evalue_zero();
1239 }
1240
1241 value_init(e.d);
1242 e.x.p = new_enode(partition, 2, P->Dimension);
1243 EVALUE_SET_DOMAIN(e.x.p->arr[0], D);
1244 evalue_set_si(&e.x.p->arr[1], 1, 1);
1245 sum = barvinok_summate(&e, P->Dimension - C->Dimension, options);
1246 free_evalue_refs(&e);
1247 return sum;
1248 }
1249