isl_tab_pip.c: find_context_div: extract out is_known_div_not_involving
[isl.git] / isl_bound.c
blobd2829d958e338957917d3f797efd41c931eaa97a
1 /*
2 * Copyright 2010 INRIA Saclay
4 * Use of this software is governed by the MIT license
6 * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
7 * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
8 * 91893 Orsay, France
9 */
11 #include <isl/aff.h>
12 #include <isl/val.h>
13 #include <isl_ctx_private.h>
14 #include <isl_map_private.h>
15 #include <isl_bound.h>
16 #include <isl_bernstein.h>
17 #include <isl_range.h>
18 #include <isl_polynomial_private.h>
19 #include <isl_options_private.h>
21 /* Given a polynomial "poly" that is constant in terms
22 * of the domain variables, construct a polynomial reduction
23 * of type "type" that is equal to "poly" on "bset",
24 * with the domain projected onto the parameters.
26 __isl_give isl_pw_qpolynomial_fold *isl_qpolynomial_cst_bound(
27 __isl_take isl_basic_set *bset, __isl_take isl_qpolynomial *poly,
28 enum isl_fold type, isl_bool *tight)
30 isl_set *dom;
31 isl_qpolynomial_fold *fold;
32 isl_pw_qpolynomial_fold *pwf;
34 fold = isl_qpolynomial_fold_alloc(type, poly);
35 dom = isl_set_from_basic_set(bset);
36 if (tight)
37 *tight = isl_bool_true;
38 pwf = isl_pw_qpolynomial_fold_alloc(type, dom, fold);
39 return isl_pw_qpolynomial_fold_project_domain_on_params(pwf);
42 /* Add the bound "pwf", which is not known to be tight,
43 * to the output of "bound".
45 isl_stat isl_bound_add(struct isl_bound *bound,
46 __isl_take isl_pw_qpolynomial_fold *pwf)
48 bound->pwf = isl_pw_qpolynomial_fold_fold(bound->pwf, pwf);
49 return isl_stat_non_null(bound->pwf);
52 /* Add the bound "pwf", which is known to be tight,
53 * to the output of "bound".
55 isl_stat isl_bound_add_tight(struct isl_bound *bound,
56 __isl_take isl_pw_qpolynomial_fold *pwf)
58 bound->pwf_tight = isl_pw_qpolynomial_fold_fold(bound->pwf_tight, pwf);
59 return isl_stat_non_null(bound->pwf);
62 /* Given a polynomial "poly" that is constant in terms
63 * of the domain variables and the domain "bset",
64 * construct the corresponding polynomial reduction and
65 * add it to the tight bounds of "bound".
67 static isl_stat add_constant_poly(__isl_take isl_basic_set *bset,
68 __isl_take isl_qpolynomial *poly, struct isl_bound *bound)
70 isl_pw_qpolynomial_fold *pwf;
72 pwf = isl_qpolynomial_cst_bound(bset, poly, bound->type, NULL);
73 return isl_bound_add_tight(bound, pwf);
76 /* Compute a bound on the polynomial defined over the parametric polytope
77 * using either range propagation or bernstein expansion and
78 * store the result in bound->pwf and bound->pwf_tight.
79 * Since bernstein expansion requires bounded domains, we apply
80 * range propagation on unbounded domains. Otherwise, we respect the choice
81 * of the user.
83 * If the polynomial does not depend on the set variables
84 * then the bound is equal to the polynomial and
85 * it can be added to "bound" directly.
87 static isl_stat compressed_guarded_poly_bound(__isl_take isl_basic_set *bset,
88 __isl_take isl_qpolynomial *poly, struct isl_bound *bound)
90 isl_ctx *ctx;
91 int bounded;
92 int degree;
94 if (!bset || !poly)
95 goto error;
97 degree = isl_qpolynomial_degree(poly);
98 if (degree < -1)
99 goto error;
100 if (degree <= 0)
101 return add_constant_poly(bset, poly, bound);
103 ctx = isl_basic_set_get_ctx(bset);
104 if (ctx->opt->bound == ISL_BOUND_RANGE)
105 return isl_qpolynomial_bound_on_domain_range(bset, poly, bound);
107 bounded = isl_basic_set_is_bounded(bset);
108 if (bounded < 0)
109 goto error;
110 if (bounded)
111 return isl_qpolynomial_bound_on_domain_bernstein(bset, poly, bound);
112 else
113 return isl_qpolynomial_bound_on_domain_range(bset, poly, bound);
114 error:
115 isl_basic_set_free(bset);
116 isl_qpolynomial_free(poly);
117 return isl_stat_error;
120 static isl_stat unwrapped_guarded_poly_bound(__isl_take isl_basic_set *bset,
121 __isl_take isl_qpolynomial *poly, struct isl_bound *bound)
123 isl_pw_qpolynomial_fold *top_pwf;
124 isl_pw_qpolynomial_fold *top_pwf_tight;
125 isl_space *space;
126 isl_morph *morph;
127 isl_stat r;
129 bset = isl_basic_set_detect_equalities(bset);
131 if (!bset)
132 goto error;
134 if (bset->n_eq == 0)
135 return compressed_guarded_poly_bound(bset, poly, bound);
137 morph = isl_basic_set_full_compression(bset);
139 bset = isl_morph_basic_set(isl_morph_copy(morph), bset);
140 poly = isl_qpolynomial_morph_domain(poly, isl_morph_copy(morph));
142 space = isl_morph_get_ran_space(morph);
143 space = isl_space_params(space);
145 top_pwf = bound->pwf;
146 top_pwf_tight = bound->pwf_tight;
148 space = isl_space_from_domain(space);
149 space = isl_space_add_dims(space, isl_dim_out, 1);
150 bound->pwf = isl_pw_qpolynomial_fold_zero(isl_space_copy(space),
151 bound->type);
152 bound->pwf_tight = isl_pw_qpolynomial_fold_zero(space, bound->type);
154 r = compressed_guarded_poly_bound(bset, poly, bound);
156 morph = isl_morph_dom_params(morph);
157 morph = isl_morph_ran_params(morph);
158 morph = isl_morph_inverse(morph);
160 bound->pwf = isl_pw_qpolynomial_fold_morph_domain(bound->pwf,
161 isl_morph_copy(morph));
162 bound->pwf_tight = isl_pw_qpolynomial_fold_morph_domain(
163 bound->pwf_tight, morph);
165 isl_bound_add(bound, top_pwf);
166 isl_bound_add_tight(bound, top_pwf_tight);
168 return r;
169 error:
170 isl_basic_set_free(bset);
171 isl_qpolynomial_free(poly);
172 return isl_stat_error;
175 /* Update bound->pwf and bound->pwf_tight with a bound
176 * of type bound->type on the (quasi-)polynomial "qp" over the domain "bset",
177 * by calling "unwrapped" on unwrapped versions of "bset and "qp".
178 * If "qp" is a polynomial, then "unwrapped" will also be called
179 * on a polynomial.
181 * If the original problem did not have a wrapped relation in the domain,
182 * then call "unwrapped" directly.
184 * Otherwise, the bound should be computed over the range
185 * of the wrapped relation. Temporarily treat the domain dimensions
186 * of this wrapped relation as parameters, compute a bound using "unwrapped"
187 * in terms of these and the original parameters,
188 * turn the parameters back into set dimensions and
189 * add the results to bound->pwf and bound->pwf_tight.
191 * Note that even though "bset" is known to live in the same space
192 * as the domain of "qp", the names of the set dimensions
193 * may be different (or missing). Make sure the naming is exactly
194 * the same before turning these dimensions into parameters
195 * to ensure that the spaces are still the same after
196 * this operation.
198 static isl_stat unwrap(__isl_take isl_basic_set *bset,
199 __isl_take isl_qpolynomial *qp,
200 isl_stat (*unwrapped)(__isl_take isl_basic_set *bset,
201 __isl_take isl_qpolynomial *qp, struct isl_bound *bound),
202 struct isl_bound *bound)
204 isl_space *space;
205 isl_pw_qpolynomial_fold *top_pwf;
206 isl_pw_qpolynomial_fold *top_pwf_tight;
207 isl_size nparam;
208 isl_size n_in;
209 isl_stat r;
211 if (!bound->wrapping)
212 return unwrapped(bset, qp, bound);
214 nparam = isl_space_dim(bound->dim, isl_dim_param);
215 n_in = isl_space_dim(bound->dim, isl_dim_in);
216 if (nparam < 0 || n_in < 0)
217 goto error;
219 space = isl_qpolynomial_get_domain_space(qp);
220 bset = isl_basic_set_reset_space(bset, space);
222 bset = isl_basic_set_move_dims(bset, isl_dim_param, nparam,
223 isl_dim_set, 0, n_in);
224 qp = isl_qpolynomial_move_dims(qp, isl_dim_param, nparam,
225 isl_dim_in, 0, n_in);
227 space = isl_basic_set_get_space(bset);
228 space = isl_space_params(space);
230 top_pwf = bound->pwf;
231 top_pwf_tight = bound->pwf_tight;
233 space = isl_space_from_domain(space);
234 space = isl_space_add_dims(space, isl_dim_out, 1);
235 bound->pwf = isl_pw_qpolynomial_fold_zero(isl_space_copy(space),
236 bound->type);
237 bound->pwf_tight = isl_pw_qpolynomial_fold_zero(space, bound->type);
239 r = unwrapped(bset, qp, bound);
241 bound->pwf = isl_pw_qpolynomial_fold_reset_space(bound->pwf,
242 isl_space_copy(bound->dim));
243 bound->pwf_tight = isl_pw_qpolynomial_fold_reset_space(bound->pwf_tight,
244 isl_space_copy(bound->dim));
246 isl_bound_add(bound, top_pwf);
247 isl_bound_add_tight(bound, top_pwf_tight);
249 return r;
250 error:
251 isl_basic_set_free(bset);
252 isl_qpolynomial_free(qp);
253 return isl_stat_error;
256 /* Update bound->pwf and bound->pwf_tight with a bound
257 * of type bound->type on the polynomial "poly" over the domain "bset",
258 * handling any wrapping in the domain.
260 static isl_stat guarded_poly_bound(__isl_take isl_basic_set *bset,
261 __isl_take isl_qpolynomial *poly, void *user)
263 struct isl_bound *bound = (struct isl_bound *)user;
265 return unwrap(bset, poly, &unwrapped_guarded_poly_bound, bound);
268 /* Is "bset" bounded and is "qp" a quasi-affine expression?
270 static isl_bool is_bounded_affine(__isl_keep isl_basic_set *bset,
271 __isl_keep isl_qpolynomial *qp)
273 isl_bool affine;
275 affine = isl_qpolynomial_isa_aff(qp);
276 if (affine < 0 || !affine)
277 return affine;
278 return isl_basic_set_is_bounded(bset);
281 /* Update bound->pwf and bound->pwf_tight with a bound
282 * of type bound->type on the quasi-polynomial "qp" over the domain "bset",
283 * for the case where "bset" is bounded and
284 * "qp" is a quasi-affine expression and
285 * they have both been unwrapped already if needed.
287 * Consider the set of possible function values of "qp" over "bset" and
288 * take the minimum or maximum value in this set, depending
289 * on whether a lower or an upper bound is being computed.
290 * Do this by calling isl_set_lexmin_pw_multi_aff or
291 * isl_set_lexmax_pw_multi_aff, which compute a regular minimum or maximum
292 * since the set is one-dimensional.
293 * Since this computation is exact, the bound is always tight.
295 * Note that the minimum or maximum integer value is being computed,
296 * so if "qp" has some non-trivial denominator, then it needs
297 * to be multiplied out first and then taken into account again
298 * after computing the minimum or maximum.
300 static isl_stat unwrapped_affine_qp(__isl_take isl_basic_set *bset,
301 __isl_take isl_qpolynomial *qp, struct isl_bound *bound)
303 isl_val *d;
304 isl_aff *aff;
305 isl_basic_map *bmap;
306 isl_set *range;
307 isl_pw_multi_aff *opt;
308 isl_pw_aff *pa;
309 isl_pw_qpolynomial *pwqp;
310 isl_pw_qpolynomial_fold *pwf;
312 aff = isl_qpolynomial_as_aff(qp);
313 d = isl_aff_get_denominator_val(aff);
314 aff = isl_aff_scale_val(aff, isl_val_copy(d));
315 bmap = isl_basic_map_from_aff(aff);
316 bmap = isl_basic_map_intersect_domain(bmap, bset);
317 range = isl_set_from_basic_set(isl_basic_map_range(bmap));
318 if (bound->type == isl_fold_min)
319 opt = isl_set_lexmin_pw_multi_aff(range);
320 else
321 opt = isl_set_lexmax_pw_multi_aff(range);
322 pa = isl_pw_multi_aff_get_at(opt, 0);
323 isl_pw_multi_aff_free(opt);
324 pa = isl_pw_aff_scale_down_val(pa, d);
325 pwqp = isl_pw_qpolynomial_from_pw_aff(pa);
326 pwf = isl_pw_qpolynomial_fold_from_pw_qpolynomial(bound->type, pwqp);
328 bound->pwf_tight = isl_pw_qpolynomial_fold_fold(bound->pwf_tight, pwf);
330 return isl_stat_non_null(bound->pwf_tight);
333 /* Update bound->pwf and bound->pwf_tight with a bound
334 * of type bound->type on the quasi-polynomial "qp" over the domain bound->bset,
335 * for the case where bound->bset is bounded and
336 * "qp" is a quasi-affine expression,
337 * handling any wrapping in the domain.
339 static isl_stat affine_qp(__isl_take isl_qpolynomial *qp,
340 struct isl_bound *bound)
342 isl_basic_set *bset;
344 bset = isl_basic_set_copy(bound->bset);
345 return unwrap(bset, qp, &unwrapped_affine_qp, bound);
348 /* Update bound->pwf and bound->pwf_tight with a bound
349 * of type bound->type on the quasi-polynomial "qp" over the domain bound->bset.
351 * If bound->bset is bounded and if "qp" is a quasi-affine expression,
352 * then use a specialized version.
354 * Otherwise, treat the integer divisions as extra variables and
355 * compute a bound over the polynomial in terms of the original and
356 * the extra variables.
358 static isl_stat guarded_qp(__isl_take isl_qpolynomial *qp, void *user)
360 struct isl_bound *bound = (struct isl_bound *)user;
361 isl_stat r;
362 isl_bool bounded_affine;
364 bounded_affine = is_bounded_affine(bound->bset, qp);
365 if (bounded_affine < 0)
366 qp = isl_qpolynomial_free(qp);
367 else if (bounded_affine)
368 return affine_qp(qp, bound);
370 r = isl_qpolynomial_as_polynomial_on_domain(qp, bound->bset,
371 &guarded_poly_bound, user);
372 isl_qpolynomial_free(qp);
373 return r;
376 static isl_stat basic_guarded_fold(__isl_take isl_basic_set *bset, void *user)
378 struct isl_bound *bound = (struct isl_bound *)user;
379 isl_stat r;
381 bound->bset = bset;
382 r = isl_qpolynomial_fold_foreach_qpolynomial(bound->fold,
383 &guarded_qp, user);
384 isl_basic_set_free(bset);
385 return r;
388 static isl_stat guarded_fold(__isl_take isl_set *set,
389 __isl_take isl_qpolynomial_fold *fold, void *user)
391 struct isl_bound *bound = (struct isl_bound *)user;
393 if (!set || !fold)
394 goto error;
396 set = isl_set_make_disjoint(set);
398 bound->fold = fold;
399 bound->type = isl_qpolynomial_fold_get_type(fold);
401 if (isl_set_foreach_basic_set(set, &basic_guarded_fold, bound) < 0)
402 goto error;
404 isl_set_free(set);
405 isl_qpolynomial_fold_free(fold);
407 return isl_stat_ok;
408 error:
409 isl_set_free(set);
410 isl_qpolynomial_fold_free(fold);
411 return isl_stat_error;
414 __isl_give isl_pw_qpolynomial_fold *isl_pw_qpolynomial_fold_bound(
415 __isl_take isl_pw_qpolynomial_fold *pwf, isl_bool *tight)
417 isl_size nvar;
418 struct isl_bound bound;
419 isl_bool covers;
421 if (!pwf)
422 return NULL;
424 bound.dim = isl_pw_qpolynomial_fold_get_domain_space(pwf);
426 bound.wrapping = isl_space_is_wrapping(bound.dim);
427 if (bound.wrapping)
428 bound.dim = isl_space_unwrap(bound.dim);
429 nvar = isl_space_dim(bound.dim, isl_dim_out);
430 if (nvar < 0)
431 bound.dim = isl_space_free(bound.dim);
432 bound.dim = isl_space_domain(bound.dim);
433 bound.dim = isl_space_from_domain(bound.dim);
434 bound.dim = isl_space_add_dims(bound.dim, isl_dim_out, 1);
436 if (nvar == 0) {
437 if (tight)
438 *tight = isl_bool_true;
439 return isl_pw_qpolynomial_fold_reset_space(pwf, bound.dim);
442 if (isl_pw_qpolynomial_fold_is_zero(pwf)) {
443 enum isl_fold type = pwf->type;
444 isl_pw_qpolynomial_fold_free(pwf);
445 if (tight)
446 *tight = isl_bool_true;
447 return isl_pw_qpolynomial_fold_zero(bound.dim, type);
450 bound.pwf = isl_pw_qpolynomial_fold_zero(isl_space_copy(bound.dim),
451 pwf->type);
452 bound.pwf_tight = isl_pw_qpolynomial_fold_zero(isl_space_copy(bound.dim),
453 pwf->type);
454 bound.check_tight = !!tight;
456 if (isl_pw_qpolynomial_fold_foreach_lifted_piece(pwf,
457 guarded_fold, &bound) < 0)
458 goto error;
460 covers = isl_pw_qpolynomial_fold_covers(bound.pwf_tight, bound.pwf);
461 if (covers < 0)
462 goto error;
464 if (tight)
465 *tight = covers;
467 isl_space_free(bound.dim);
468 isl_pw_qpolynomial_fold_free(pwf);
470 if (covers) {
471 isl_pw_qpolynomial_fold_free(bound.pwf);
472 return bound.pwf_tight;
475 bound.pwf = isl_pw_qpolynomial_fold_fold(bound.pwf, bound.pwf_tight);
477 return bound.pwf;
478 error:
479 isl_pw_qpolynomial_fold_free(bound.pwf_tight);
480 isl_pw_qpolynomial_fold_free(bound.pwf);
481 isl_pw_qpolynomial_fold_free(pwf);
482 isl_space_free(bound.dim);
483 return NULL;
486 __isl_give isl_pw_qpolynomial_fold *isl_pw_qpolynomial_bound(
487 __isl_take isl_pw_qpolynomial *pwqp, enum isl_fold type,
488 isl_bool *tight)
490 isl_pw_qpolynomial_fold *pwf;
492 pwf = isl_pw_qpolynomial_fold_from_pw_qpolynomial(type, pwqp);
493 return isl_pw_qpolynomial_fold_bound(pwf, tight);
496 struct isl_union_bound_data {
497 enum isl_fold type;
498 isl_bool tight;
499 isl_union_pw_qpolynomial_fold *res;
502 static isl_stat bound_pw(__isl_take isl_pw_qpolynomial *pwqp, void *user)
504 struct isl_union_bound_data *data = user;
505 isl_pw_qpolynomial_fold *pwf;
507 pwf = isl_pw_qpolynomial_bound(pwqp, data->type,
508 data->tight ? &data->tight : NULL);
509 data->res = isl_union_pw_qpolynomial_fold_fold_pw_qpolynomial_fold(
510 data->res, pwf);
512 return isl_stat_ok;
515 __isl_give isl_union_pw_qpolynomial_fold *isl_union_pw_qpolynomial_bound(
516 __isl_take isl_union_pw_qpolynomial *upwqp,
517 enum isl_fold type, isl_bool *tight)
519 isl_space *space;
520 struct isl_union_bound_data data = { type, 1, NULL };
522 if (!upwqp)
523 return NULL;
525 if (!tight)
526 data.tight = isl_bool_false;
528 space = isl_union_pw_qpolynomial_get_space(upwqp);
529 data.res = isl_union_pw_qpolynomial_fold_zero(space, type);
530 if (isl_union_pw_qpolynomial_foreach_pw_qpolynomial(upwqp,
531 &bound_pw, &data) < 0)
532 goto error;
534 isl_union_pw_qpolynomial_free(upwqp);
535 if (tight)
536 *tight = data.tight;
538 return data.res;
539 error:
540 isl_union_pw_qpolynomial_free(upwqp);
541 isl_union_pw_qpolynomial_fold_free(data.res);
542 return NULL;