1 #include <barvinok/options.h>
2 #include <barvinok/util.h>
5 #define ALLOC(type) (type*)malloc(sizeof(type))
6 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
8 static struct bernoulli bernoulli
;
10 struct bernoulli
*bernoulli_compute(int n
)
13 Value lcm
, factor
, tmp
;
18 if (n
>= bernoulli
.size
) {
23 b
= Vector_Alloc(size
);
25 Vector_Copy(bernoulli
.b_num
->p
, b
->p
, bernoulli
.n
);
26 Vector_Free(bernoulli
.b_num
);
29 b
= Vector_Alloc(size
);
31 Vector_Copy(bernoulli
.b_den
->p
, b
->p
, bernoulli
.n
);
32 Vector_Free(bernoulli
.b_den
);
35 sum
= ALLOCN(Vector
*, size
);
36 for (i
= 0; i
< bernoulli
.n
; ++i
)
37 sum
[i
] = bernoulli
.sum
[i
];
41 bernoulli
.size
= size
;
47 for (i
= 0; i
< bernoulli
.n
; ++i
)
48 value_lcm(lcm
, bernoulli
.b_den
->p
[i
], &lcm
);
49 for (i
= bernoulli
.n
; i
<= n
; ++i
) {
51 value_set_si(bernoulli
.b_num
->p
[0], 1);
52 value_set_si(bernoulli
.b_den
->p
[0], 1);
55 value_set_si(bernoulli
.b_num
->p
[i
], 0);
56 value_set_si(factor
, -(i
+1));
57 for (j
= i
-1; j
>= 0; --j
) {
58 mpz_mul_ui(factor
, factor
, j
+1);
59 mpz_divexact_ui(factor
, factor
, i
+1-j
);
60 value_division(tmp
, lcm
, bernoulli
.b_den
->p
[j
]);
61 value_multiply(tmp
, tmp
, bernoulli
.b_num
->p
[j
]);
62 value_multiply(tmp
, tmp
, factor
);
63 value_addto(bernoulli
.b_num
->p
[i
], bernoulli
.b_num
->p
[i
], tmp
);
65 mpz_mul_ui(bernoulli
.b_den
->p
[i
], lcm
, i
+1);
66 Gcd(bernoulli
.b_num
->p
[i
], bernoulli
.b_den
->p
[i
], &tmp
);
67 if (value_notone_p(tmp
)) {
68 value_division(bernoulli
.b_num
->p
[i
], bernoulli
.b_num
->p
[i
], tmp
);
69 value_division(bernoulli
.b_den
->p
[i
], bernoulli
.b_den
->p
[i
], tmp
);
71 value_lcm(lcm
, bernoulli
.b_den
->p
[i
], &lcm
);
73 for (i
= bernoulli
.n
; i
<= n
; ++i
) {
74 bernoulli
.sum
[i
] = Vector_Alloc(i
+3);
75 value_assign(bernoulli
.sum
[i
]->p
[i
+1], lcm
);
76 mpz_mul_ui(bernoulli
.sum
[i
]->p
[i
+2], lcm
, i
+1);
77 value_set_si(factor
, 1);
78 for (j
= 1; j
<= i
; ++j
) {
79 mpz_mul_ui(factor
, factor
, i
+2-j
);
80 mpz_divexact_ui(factor
, factor
, j
);
81 value_division(bernoulli
.sum
[i
]->p
[i
+1-j
], lcm
, bernoulli
.b_den
->p
[j
]);
82 value_multiply(bernoulli
.sum
[i
]->p
[i
+1-j
],
83 bernoulli
.sum
[i
]->p
[i
+1-j
], bernoulli
.b_num
->p
[j
]);
84 value_multiply(bernoulli
.sum
[i
]->p
[i
+1-j
],
85 bernoulli
.sum
[i
]->p
[i
+1-j
], factor
);
87 Vector_Normalize(bernoulli
.sum
[i
]->p
, i
+3);
97 /* shift variables in polynomial one down */
98 static void shift(evalue
*e
)
101 if (value_notzero_p(e
->d
))
103 assert(e
->x
.p
->type
== polynomial
);
104 assert(e
->x
.p
->pos
> 1);
106 for (i
= 0; i
< e
->x
.p
->size
; ++i
)
107 shift(&e
->x
.p
->arr
[i
]);
110 static evalue
*shifted_copy(evalue
*src
)
112 evalue
*e
= ALLOC(evalue
);
119 static evalue
*power_sums(struct bernoulli
*bernoulli
, evalue
*poly
,
120 Vector
*arg
, Value denom
, int neg
, int alt_neg
)
123 evalue
*base
= affine2evalue(arg
->p
, denom
, arg
->Size
-1);
124 evalue
*sum
= evalue_zero();
126 for (i
= 1; i
< poly
->x
.p
->size
; ++i
) {
127 evalue
*term
= evalue_polynomial(bernoulli
->sum
[i
], base
);
128 evalue
*factor
= shifted_copy(&poly
->x
.p
->arr
[i
]);
130 if (alt_neg
&& (i
% 2))
133 free_evalue_refs(factor
);
134 free_evalue_refs(term
);
140 free_evalue_refs(base
);
146 struct section
{ Polyhedron
*D
; evalue
*E
; };
148 struct Bernoulli_data
{
156 static void Bernoulli_cb(Matrix
*M
, Value
*lower
, Value
*upper
, void *cb_data
)
158 struct Bernoulli_data
*data
= (struct Bernoulli_data
*)cb_data
;
161 evalue
*factor
= NULL
;
162 evalue
*linear
= NULL
;
165 unsigned dim
= M
->NbColumns
-2;
168 assert(data
->ns
< data
->size
);
171 T
= Constraints2Polyhedron(M2
, data
->MaxRays
);
174 POL_ENSURE_VERTICES(T
);
180 assert(lower
!= upper
);
182 row
= Vector_Alloc(dim
+1);
184 if (value_notzero_p(data
->e
->d
)) {
188 assert(data
->e
->x
.p
->type
== polynomial
);
189 if (data
->e
->x
.p
->pos
> 1) {
190 factor
= shifted_copy(data
->e
);
193 factor
= shifted_copy(&data
->e
->x
.p
->arr
[0]);
195 if (!EVALUE_IS_ZERO(*factor
)) {
196 value_absolute(tmp
, upper
[1]);
198 Vector_Combine(lower
+2, upper
+2, row
->p
, tmp
, lower
[1], dim
+1);
199 value_multiply(tmp
, tmp
, lower
[1]);
200 /* upper - lower + 1 */
201 value_addto(row
->p
[dim
], row
->p
[dim
], tmp
);
203 linear
= affine2evalue(row
->p
, tmp
, dim
);
204 emul(factor
, linear
);
206 linear
= evalue_zero();
209 data
->s
[data
->ns
].E
= linear
;
210 data
->s
[data
->ns
].D
= T
;
213 evalue
*poly_u
= NULL
, *poly_l
= NULL
;
215 struct bernoulli
*bernoulli
;
216 assert(data
->e
->x
.p
->type
== polynomial
);
217 assert(data
->e
->x
.p
->pos
== 1);
218 bernoulli
= bernoulli_compute(data
->e
->x
.p
->size
-1);
219 /* lower is the constraint
220 * b i - l' >= 0 i >= l'/b = l
221 * upper is the constraint
222 * -a i + u' >= 0 i <= u'/a = u
224 M2
= Matrix_Alloc(3, 2+T
->Dimension
);
225 value_set_si(M2
->p
[0][0], 1);
226 value_set_si(M2
->p
[1][0], 1);
227 value_set_si(M2
->p
[2][0], 1);
231 Vector_Oppose(lower
+2, M2
->p
[0]+1, T
->Dimension
+1);
232 value_subtract(M2
->p
[0][1+T
->Dimension
], M2
->p
[0][1+T
->Dimension
],
234 D
= AddConstraints(M2
->p_Init
, 1, T
, data
->MaxRays
);
240 Vector_Copy(upper
+2, row
->p
, dim
+1);
241 value_oppose(tmp
, upper
[1]);
242 value_addto(row
->p
[dim
], row
->p
[dim
], tmp
);
243 poly_u
= power_sums(bernoulli
, data
->e
, row
, tmp
, 0, 0);
245 Vector_Oppose(lower
+2, row
->p
, dim
+1);
246 extra
= power_sums(bernoulli
, data
->e
, row
, lower
[1], 1, 0);
250 data
->s
[data
->ns
].E
= extra
;
251 data
->s
[data
->ns
].D
= D
;
256 * 1 <= -u -u' - a >= 0
258 Vector_Oppose(upper
+2, M2
->p
[0]+1, T
->Dimension
+1);
259 value_addto(M2
->p
[0][1+T
->Dimension
], M2
->p
[0][1+T
->Dimension
],
261 D
= AddConstraints(M2
->p_Init
, 1, T
, data
->MaxRays
);
267 Vector_Copy(lower
+2, row
->p
, dim
+1);
268 value_addto(row
->p
[dim
], row
->p
[dim
], lower
[1]);
269 poly_l
= power_sums(bernoulli
, data
->e
, row
, lower
[1], 0, 1);
271 Vector_Oppose(upper
+2, row
->p
, dim
+1);
272 value_oppose(tmp
, upper
[1]);
273 extra
= power_sums(bernoulli
, data
->e
, row
, tmp
, 1, 1);
277 data
->s
[data
->ns
].E
= extra
;
278 data
->s
[data
->ns
].D
= D
;
286 Vector_Copy(upper
+2, M2
->p
[0]+1, T
->Dimension
+1);
287 Vector_Copy(lower
+2, M2
->p
[1]+1, T
->Dimension
+1);
288 D
= AddConstraints(M2
->p_Init
, 2, T
, data
->MaxRays
);
293 Vector_Copy(lower
+2, row
->p
, dim
+1);
294 value_addto(row
->p
[dim
], row
->p
[dim
], lower
[1]);
295 poly_l
= power_sums(bernoulli
, data
->e
, row
, lower
[1], 0, 1);
298 Vector_Copy(upper
+2, row
->p
, dim
+1);
299 value_oppose(tmp
, upper
[1]);
300 value_addto(row
->p
[dim
], row
->p
[dim
], tmp
);
301 poly_u
= power_sums(bernoulli
, data
->e
, row
, tmp
, 0, 0);
304 data
->s
[data
->ns
].E
= ALLOC(evalue
);
305 value_init(data
->s
[data
->ns
].E
->d
);
306 evalue_copy(data
->s
[data
->ns
].E
, poly_u
);
307 eadd(poly_l
, data
->s
[data
->ns
].E
);
308 eadd(linear
, data
->s
[data
->ns
].E
);
309 data
->s
[data
->ns
].D
= D
;
314 * l < 1 -l' + b - 1 >= 0
317 Vector_Copy(lower
+2, M2
->p
[0]+1, T
->Dimension
+1);
318 value_addto(M2
->p
[0][1+T
->Dimension
], M2
->p
[0][1+T
->Dimension
], lower
[1]);
319 value_decrement(M2
->p
[0][1+T
->Dimension
], M2
->p
[0][1+T
->Dimension
]);
320 Vector_Oppose(lower
+2, M2
->p
[1]+1, T
->Dimension
+1);
321 value_decrement(M2
->p
[1][1+T
->Dimension
], M2
->p
[1][1+T
->Dimension
]);
322 D
= AddConstraints(M2
->p_Init
, 2, T
, data
->MaxRays
);
327 Vector_Copy(upper
+2, row
->p
, dim
+1);
328 value_oppose(tmp
, upper
[1]);
329 value_addto(row
->p
[dim
], row
->p
[dim
], tmp
);
330 poly_u
= power_sums(bernoulli
, data
->e
, row
, tmp
, 0, 0);
333 eadd(linear
, poly_u
);
334 data
->s
[data
->ns
].E
= poly_u
;
336 data
->s
[data
->ns
].D
= D
;
341 * -u < 1 u' + a - 1 >= 0
342 * 0 < -u -u' - 1 >= 0
345 Vector_Copy(upper
+2, M2
->p
[0]+1, T
->Dimension
+1);
346 value_subtract(M2
->p
[0][1+T
->Dimension
], M2
->p
[0][1+T
->Dimension
],
348 value_decrement(M2
->p
[0][1+T
->Dimension
], M2
->p
[0][1+T
->Dimension
]);
349 Vector_Oppose(upper
+2, M2
->p
[1]+1, T
->Dimension
+1);
350 value_decrement(M2
->p
[1][1+T
->Dimension
], M2
->p
[1][1+T
->Dimension
]);
351 Vector_Copy(lower
+2, M2
->p
[2]+1, T
->Dimension
+1);
352 D
= AddConstraints(M2
->p_Init
, 3, T
, data
->MaxRays
);
357 Vector_Copy(lower
+2, row
->p
, dim
+1);
358 value_addto(row
->p
[dim
], row
->p
[dim
], lower
[1]);
359 poly_l
= power_sums(bernoulli
, data
->e
, row
, lower
[1], 0, 1);
362 eadd(linear
, poly_l
);
363 data
->s
[data
->ns
].E
= poly_l
;
365 data
->s
[data
->ns
].D
= D
;
372 free_evalue_refs(poly_l
);
376 free_evalue_refs(poly_u
);
379 free_evalue_refs(linear
);
382 if (factor
!= data
->e
) {
383 free_evalue_refs(factor
);
390 evalue
*Bernoulli_sum_evalue(evalue
*e
, unsigned nvar
,
391 struct barvinok_options
*options
)
393 struct Bernoulli_data data
;
395 evalue
*sum
= evalue_zero();
397 if (EVALUE_IS_ZERO(*e
))
405 assert(value_zero_p(e
->d
));
406 assert(e
->x
.p
->type
== partition
);
408 data
.size
= e
->x
.p
->size
* 2 + 16;
409 data
.s
= ALLOCN(struct section
, data
.size
);
410 data
.MaxRays
= options
->MaxRays
;
412 for (i
= 0; i
< e
->x
.p
->size
/2; ++i
) {
414 for (D
= EVALUE_DOMAIN(e
->x
.p
->arr
[2*i
]); D
; D
= D
->next
) {
415 unsigned dim
= D
->Dimension
- 1;
416 Polyhedron
*next
= D
->next
;
421 value_set_si(tmp
.d
, 0);
423 if (value_zero_p(D
->Constraint
[0][0]) &&
424 value_notzero_p(D
->Constraint
[0][1])) {
425 tmp
.x
.p
= new_enode(partition
, 2, dim
);
426 EVALUE_SET_DOMAIN(tmp
.x
.p
->arr
[0], Polyhedron_Project(D
, dim
));
427 evalue_copy(&tmp
.x
.p
->arr
[1], &e
->x
.p
->arr
[2*i
+1]);
428 reduce_evalue_in_domain(&tmp
.x
.p
->arr
[1], D
);
429 shift(&tmp
.x
.p
->arr
[1]);
432 data
.e
= &e
->x
.p
->arr
[2*i
+1];
434 for_each_lower_upper_bound(D
, Bernoulli_cb
, &data
);
437 evalue_set_si(&tmp
, 0, 1);
439 tmp
.x
.p
= new_enode(partition
, 2*data
.ns
, dim
);
440 for (j
= 0; j
< data
.ns
; ++j
) {
441 EVALUE_SET_DOMAIN(tmp
.x
.p
->arr
[2*j
], data
.s
[j
].D
);
442 value_clear(tmp
.x
.p
->arr
[2*j
+1].d
);
443 tmp
.x
.p
->arr
[2*j
+1] = *data
.s
[j
].E
;
450 evalue
*res
= Bernoulli_sum_evalue(&tmp
, nvar
-1, options
);
452 free_evalue_refs(res
);
457 free_evalue_refs(&tmp
);
468 evalue
*Bernoulli_sum(Polyhedron
*P
, Polyhedron
*C
,
469 struct barvinok_options
*options
)
475 e
.x
.p
= new_enode(partition
, 2, P
->Dimension
);
476 EVALUE_SET_DOMAIN(e
.x
.p
->arr
[0], Polyhedron_Copy(P
));
477 evalue_set_si(&e
.x
.p
->arr
[1], 1, 1);
478 sum
= Bernoulli_sum_evalue(&e
, P
->Dimension
- C
->Dimension
, options
);
479 free_evalue_refs(&e
);