isl_pw_qpolynomial_sum: handle existentials in wrapped domains
[barvinok.git] / evalue_isl.c
blob85f3b7dfe33242809afb2bb60e4435e64265967d
1 #include <isl_set_polylib.h>
2 #include <isl_constraint.h>
3 #include <barvinok/evalue.h>
5 static __isl_give isl_qpolynomial *extract_base(__isl_take isl_dim *dim,
6 const evalue *e)
8 int i;
9 isl_ctx *ctx;
10 isl_vec *v;
11 isl_div *div;
12 isl_qpolynomial *base, *c;
13 unsigned nparam;
15 if (!dim)
16 return NULL;
18 if (e->x.p->type == polynomial)
19 return isl_qpolynomial_var(dim, isl_dim_param, e->x.p->pos - 1);
21 ctx = isl_dim_get_ctx(dim);
22 nparam = isl_dim_size(dim, isl_dim_param);
23 v = isl_vec_alloc(ctx, 2 + nparam);
24 if (!v)
25 goto error;
27 isl_seq_clr(v->el + 2, nparam);
28 evalue_extract_affine(&e->x.p->arr[0], v->el + 2, &v->el[1], &v->el[0]);
30 div = isl_div_alloc(isl_dim_copy(dim));
31 isl_div_set_constant(div, v->el[1]);
32 isl_div_set_denominator(div, v->el[0]);
34 for (i = 0; i < nparam; ++i)
35 isl_div_set_coefficient(div, isl_dim_param, i, v->el[2 + i]);
37 base = isl_qpolynomial_div(div);
39 if (e->x.p->type == fractional) {
40 base = isl_qpolynomial_neg(base);
42 c = isl_qpolynomial_rat_cst(isl_dim_copy(dim), v->el[1], v->el[0]);
43 base = isl_qpolynomial_add(base, c);
45 for (i = 0; i < nparam; ++i) {
46 isl_qpolynomial *t;
47 c = isl_qpolynomial_rat_cst(isl_dim_copy(dim),
48 v->el[2 + i], v->el[0]);
49 t = isl_qpolynomial_var(isl_dim_copy(dim),
50 isl_dim_param, i);
51 t = isl_qpolynomial_mul(c, t);
52 base = isl_qpolynomial_add(base, t);
56 isl_vec_free(v);
57 isl_dim_free(dim);
59 return base;
60 error:
61 isl_dim_free(dim);
62 return NULL;
65 static int type_offset(enode *p)
67 return p->type == fractional ? 1 :
68 p->type == flooring ? 1 : 0;
71 __isl_give isl_qpolynomial *isl_qpolynomial_from_evalue(__isl_take isl_dim *dim,
72 const evalue *e)
74 int i;
75 isl_qpolynomial *qp;
76 isl_qpolynomial *base;
77 int offset;
79 if (EVALUE_IS_NAN(*e))
80 return isl_qpolynomial_infty(dim);
81 if (value_notzero_p(e->d))
82 return isl_qpolynomial_rat_cst(dim, e->x.n, e->d);
84 offset = type_offset(e->x.p);
86 assert(e->x.p->type == polynomial ||
87 e->x.p->type == flooring ||
88 e->x.p->type == fractional);
89 assert(e->x.p->size >= 1 + offset);
91 base = extract_base(isl_dim_copy(dim), e);
92 qp = isl_qpolynomial_from_evalue(isl_dim_copy(dim),
93 &e->x.p->arr[e->x.p->size - 1]);
95 for (i = e->x.p->size - 2; i >= offset; --i) {
96 qp = isl_qpolynomial_mul(qp, isl_qpolynomial_copy(base));
97 qp = isl_qpolynomial_add(qp,
98 isl_qpolynomial_from_evalue(isl_dim_copy(dim),
99 &e->x.p->arr[i]));
102 isl_qpolynomial_free(base);
103 isl_dim_free(dim);
105 return qp;
108 static __isl_give isl_pw_qpolynomial *guarded_evalue2pwqp(__isl_take isl_set *set,
109 const evalue *e);
111 static __isl_give isl_pw_qpolynomial *relation2pwqp(__isl_take isl_set *set,
112 const evalue *e)
114 int i;
115 isl_vec *vec;
116 isl_dim *dim;
117 unsigned nparam;
118 isl_pw_qpolynomial *pwqp;
119 struct isl_constraint *c;
120 struct isl_basic_set *bset;
121 struct isl_set *guard;
122 const evalue *fract;
124 if (!set || !e)
125 goto error;
127 if (e->x.p->size == 1) {
128 dim = isl_set_get_dim(set);
129 isl_set_free(set);
130 return isl_pw_qpolynomial_zero(dim);
133 isl_assert(set->ctx, e->x.p->size > 0, goto error);
134 isl_assert(set->ctx, e->x.p->size <= 3, goto error);
135 isl_assert(set->ctx, value_zero_p(e->x.p->arr[0].d), goto error);
136 isl_assert(set->ctx, e->x.p->arr[0].x.p->type == fractional, goto error);
137 fract = &e->x.p->arr[0];
139 nparam = isl_set_dim(set, isl_dim_param);
140 vec = isl_vec_alloc(set->ctx, 2 + nparam + 1);
141 if (!vec)
142 goto error;
144 isl_seq_clr(vec->el + 2, nparam);
145 evalue_extract_affine(&fract->x.p->arr[0],
146 vec->el + 2, &vec->el[1], &vec->el[0]);
148 dim = isl_set_get_dim(set);
149 dim = isl_dim_add(dim, isl_dim_set, 1);
151 bset = isl_basic_set_universe(dim);
152 c = isl_equality_alloc(isl_dim_copy(dim));
153 isl_int_neg(vec->el[0], vec->el[0]);
154 isl_constraint_set_coefficient(c, isl_dim_set, 0, vec->el[0]);
155 isl_constraint_set_constant(c, vec->el[1]);
156 for (i = 0; i < nparam; ++i)
157 isl_constraint_set_coefficient(c, isl_dim_param, i, vec->el[2+i]);
158 bset = isl_basic_set_add_constraint(bset, c);
159 bset = isl_basic_set_project_out(bset, isl_dim_set, 0, 1);
160 guard = isl_set_from_basic_set(bset);
161 isl_vec_free(vec);
163 pwqp = guarded_evalue2pwqp(isl_set_intersect(isl_set_copy(set),
164 isl_set_copy(guard)),
165 &e->x.p->arr[1]);
167 if (e->x.p->size == 3) {
168 isl_pw_qpolynomial *pwqpc;
169 guard = isl_set_complement(guard);
170 pwqpc = guarded_evalue2pwqp(isl_set_intersect(isl_set_copy(set),
171 isl_set_copy(guard)),
172 &e->x.p->arr[2]);
173 pwqp = isl_pw_qpolynomial_add_disjoint(pwqp, pwqpc);
176 isl_set_free(set);
177 isl_set_free(guard);
179 return pwqp;
180 error:
181 isl_set_free(set);
182 return NULL;
185 static __isl_give isl_pw_qpolynomial *guarded_evalue2pwqp(__isl_take isl_set *set,
186 const evalue *e)
188 isl_qpolynomial *qp;
190 if (value_zero_p(e->d) && e->x.p->type == relation)
191 return relation2pwqp(set, e);
193 qp = isl_qpolynomial_from_evalue(isl_set_get_dim(set), e);
195 return isl_pw_qpolynomial_alloc(set, qp);
198 __isl_give isl_pw_qpolynomial *isl_pw_qpolynomial_from_evalue(__isl_take isl_dim *dim, const evalue *e)
200 int i;
201 isl_pw_qpolynomial *pwqp;
203 if (!dim || !e)
204 goto error;
205 if (EVALUE_IS_ZERO(*e))
206 return isl_pw_qpolynomial_zero(dim);
208 if (value_notzero_p(e->d)) {
209 isl_set *set = isl_set_universe(isl_dim_copy(dim));
210 isl_qpolynomial *qp = isl_qpolynomial_rat_cst(dim, e->x.n, e->d);
211 return isl_pw_qpolynomial_alloc(set, qp);
214 assert(!EVALUE_IS_NAN(*e));
216 assert(e->x.p->type == partition);
218 pwqp = isl_pw_qpolynomial_zero(isl_dim_copy(dim));
220 for (i = 0; i < e->x.p->size/2; ++i) {
221 Polyhedron *D = EVALUE_DOMAIN(e->x.p->arr[2 * i]);
222 isl_set *set = isl_set_new_from_polylib(D, isl_dim_copy(dim));
223 isl_pw_qpolynomial *pwqp_i;
225 pwqp_i = guarded_evalue2pwqp(set, &e->x.p->arr[2 * i + 1]);
227 pwqp = isl_pw_qpolynomial_add_disjoint(pwqp, pwqp_i);
230 isl_dim_free(dim);
232 return pwqp;
233 error:
234 isl_dim_free(dim);
235 return NULL;
238 static evalue *evalue_pow(evalue *e, int exp)
240 evalue *pow;
242 if (exp == 1)
243 return e;
245 pow = evalue_dup(e);
246 while (--exp > 0)
247 emul(e, pow);
249 evalue_free(e);
251 return pow;
254 static evalue *div2evalue(__isl_take isl_div *div)
256 int i;
257 isl_vec *vec;
258 unsigned dim;
259 unsigned nparam;
260 evalue *e;
261 evalue *aff;
263 if (!div)
264 return NULL;
266 dim = isl_div_dim(div, isl_dim_set);
267 nparam = isl_div_dim(div, isl_dim_param);
269 vec = isl_vec_alloc(div->ctx, 1 + dim + nparam + 1);
270 if (!vec)
271 goto error;
272 for (i = 0; i < dim; ++i)
273 isl_div_get_coefficient(div, isl_dim_set, i, &vec->el[1 + i]);
274 for (i = 0; i < nparam; ++i)
275 isl_div_get_coefficient(div, isl_dim_param, i,
276 &vec->el[1 + dim + i]);
277 isl_div_get_denominator(div, &vec->el[0]);
278 isl_div_get_constant(div, &vec->el[1 + dim + nparam]);
280 e = isl_alloc_type(div->ctx, evalue);
281 if (!e)
282 goto error;
283 value_init(e->d);
284 value_set_si(e->d, 0);
285 e->x.p = new_enode(flooring, 3, -1);
286 evalue_set_si(&e->x.p->arr[1], 0, 1);
287 evalue_set_si(&e->x.p->arr[2], 1, 1);
288 value_clear(e->x.p->arr[0].d);
289 aff = affine2evalue(vec->el + 1, vec->el[0], dim + nparam);
290 e->x.p->arr[0] = *aff;
291 free(aff);
292 isl_vec_free(vec);
293 isl_div_free(div);
294 return e;
295 error:
296 isl_vec_free(vec);
297 isl_div_free(div);
298 return NULL;
301 static int add_term(__isl_take isl_term *term, void *user)
303 int i;
304 evalue *sum = (evalue *)user;
305 unsigned nparam;
306 unsigned dim;
307 unsigned n_div;
308 isl_ctx *ctx;
309 isl_int n, d;
310 evalue *e;
312 if (!term)
313 return -1;
315 nparam = isl_term_dim(term, isl_dim_param);
316 dim = isl_term_dim(term, isl_dim_set);
317 n_div = isl_term_dim(term, isl_dim_div);
319 ctx = isl_term_get_ctx(term);
320 e = isl_alloc_type(ctx, evalue);
321 if (!e)
322 goto error;
324 isl_int_init(n);
325 isl_int_init(d);
327 isl_term_get_num(term, &n);
328 isl_term_get_den(term, &d);
329 value_init(e->d);
330 evalue_set(e, n, d);
332 for (i = 0; i < dim; ++i) {
333 evalue *pow;
334 int exp = isl_term_get_exp(term, isl_dim_set, i);
336 if (!exp)
337 continue;
339 pow = evalue_pow(evalue_var(i), exp);
340 emul(pow, e);
341 evalue_free(pow);
344 for (i = 0; i < nparam; ++i) {
345 evalue *pow;
346 int exp = isl_term_get_exp(term, isl_dim_param, i);
348 if (!exp)
349 continue;
351 pow = evalue_pow(evalue_var(dim + i), exp);
352 emul(pow, e);
353 evalue_free(pow);
356 for (i = 0; i < n_div; ++i) {
357 evalue *pow;
358 evalue *floor;
359 isl_div *div;
360 int exp = isl_term_get_exp(term, isl_dim_div, i);
362 if (!exp)
363 continue;
365 div = isl_term_get_div(term, i);
366 floor = div2evalue(div);
367 pow = evalue_pow(floor, exp);
368 emul(pow, e);
369 evalue_free(pow);
372 eadd(e, sum);
373 evalue_free(e);
375 isl_int_clear(n);
376 isl_int_clear(d);
378 isl_term_free(term);
380 return 0;
381 error:
382 isl_term_free(term);
383 return -1;
386 evalue *isl_qpolynomial_to_evalue(__isl_keep isl_qpolynomial *qp)
388 evalue *e;
390 e = evalue_zero();
391 if (!e)
392 return NULL;
394 if (isl_qpolynomial_foreach_term(qp, add_term, e) < 0)
395 goto error;
397 return e;
398 error:
399 evalue_free(e);
400 return NULL;
403 static int add_guarded_qp(__isl_take isl_set *set, __isl_take isl_qpolynomial *qp,
404 void *user)
406 Polyhedron *D;
407 evalue *e = NULL;
408 evalue *f;
409 evalue *sum = (evalue *)user;
410 unsigned dim;
412 e = isl_alloc_type(set->ctx, evalue);
413 if (!e)
414 goto error;
416 D = isl_set_to_polylib(set);
417 if (!D)
418 goto error;
420 f = isl_qpolynomial_to_evalue(qp);
421 if (!e) {
422 Domain_Free(D);
423 goto error;
426 dim = isl_set_dim(set, isl_dim_param) + isl_set_dim(set, isl_dim_set);
427 value_init(e->d);
428 e->x.p = new_enode(partition, 2, D->Dimension);
429 EVALUE_SET_DOMAIN(e->x.p->arr[0], D);
431 value_clear(e->x.p->arr[1].d);
432 e->x.p->arr[1] = *f;
433 free(f);
435 eadd(e, sum);
436 evalue_free(e);
438 isl_set_free(set);
439 isl_qpolynomial_free(qp);
441 return 0;
442 error:
443 free(e);
444 isl_set_free(set);
445 isl_qpolynomial_free(qp);
446 return -1;
449 evalue *isl_pw_qpolynomial_to_evalue(__isl_keep isl_pw_qpolynomial *pwqp)
451 evalue *e;
453 if (!pwqp)
454 return NULL;
455 e = evalue_zero();
457 if (isl_pw_qpolynomial_foreach_piece(pwqp, add_guarded_qp, e))
458 goto error;
460 return e;
461 error:
462 evalue_free(e);
463 return NULL;