isl_map_coalesce: avoid ignoring constraints redundant wrt implicit equalities
[isl.git] / isl_bound.c
blob64247aca052bc65d3b3a44b0d28cec138d6a71f7
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_ctx_private.h>
12 #include <isl_map_private.h>
13 #include <isl_bound.h>
14 #include <isl_bernstein.h>
15 #include <isl_range.h>
16 #include <isl_polynomial_private.h>
17 #include <isl_options_private.h>
19 /* Given a polynomial "poly" that is constant in terms
20 * of the domain variables, construct a polynomial reduction
21 * of type "type" that is equal to "poly" on "bset",
22 * with the domain projected onto the parameters.
24 __isl_give isl_pw_qpolynomial_fold *isl_qpolynomial_cst_bound(
25 __isl_take isl_basic_set *bset, __isl_take isl_qpolynomial *poly,
26 enum isl_fold type, isl_bool *tight)
28 isl_set *dom;
29 isl_qpolynomial_fold *fold;
30 isl_pw_qpolynomial_fold *pwf;
32 fold = isl_qpolynomial_fold_alloc(type, poly);
33 dom = isl_set_from_basic_set(bset);
34 if (tight)
35 *tight = isl_bool_true;
36 pwf = isl_pw_qpolynomial_fold_alloc(type, dom, fold);
37 return isl_pw_qpolynomial_fold_project_domain_on_params(pwf);
40 /* Add the bound "pwf", which is not known to be tight,
41 * to the output of "bound".
43 isl_stat isl_bound_add(struct isl_bound *bound,
44 __isl_take isl_pw_qpolynomial_fold *pwf)
46 bound->pwf = isl_pw_qpolynomial_fold_fold(bound->pwf, pwf);
47 return isl_stat_non_null(bound->pwf);
50 /* Add the bound "pwf", which is known to be tight,
51 * to the output of "bound".
53 isl_stat isl_bound_add_tight(struct isl_bound *bound,
54 __isl_take isl_pw_qpolynomial_fold *pwf)
56 bound->pwf_tight = isl_pw_qpolynomial_fold_fold(bound->pwf_tight, pwf);
57 return isl_stat_non_null(bound->pwf);
60 /* Given a polynomial "poly" that is constant in terms
61 * of the domain variables and the domain "bset",
62 * construct the corresponding polynomial reduction and
63 * add it to the tight bounds of "bound".
65 static isl_stat add_constant_poly(__isl_take isl_basic_set *bset,
66 __isl_take isl_qpolynomial *poly, struct isl_bound *bound)
68 isl_pw_qpolynomial_fold *pwf;
70 pwf = isl_qpolynomial_cst_bound(bset, poly, bound->type, NULL);
71 return isl_bound_add_tight(bound, pwf);
74 /* Compute a bound on the polynomial defined over the parametric polytope
75 * using either range propagation or bernstein expansion and
76 * store the result in bound->pwf and bound->pwf_tight.
77 * Since bernstein expansion requires bounded domains, we apply
78 * range propagation on unbounded domains. Otherwise, we respect the choice
79 * of the user.
81 * If the polynomial does not depend on the set variables
82 * then the bound is equal to the polynomial and
83 * it can be added to "bound" directly.
85 static isl_stat compressed_guarded_poly_bound(__isl_take isl_basic_set *bset,
86 __isl_take isl_qpolynomial *poly, void *user)
88 struct isl_bound *bound = (struct isl_bound *)user;
89 isl_ctx *ctx;
90 int bounded;
91 int degree;
93 if (!bset || !poly)
94 goto error;
96 degree = isl_qpolynomial_degree(poly);
97 if (degree < -1)
98 goto error;
99 if (degree <= 0)
100 return add_constant_poly(bset, poly, bound);
102 ctx = isl_basic_set_get_ctx(bset);
103 if (ctx->opt->bound == ISL_BOUND_RANGE)
104 return isl_qpolynomial_bound_on_domain_range(bset, poly, bound);
106 bounded = isl_basic_set_is_bounded(bset);
107 if (bounded < 0)
108 goto error;
109 if (bounded)
110 return isl_qpolynomial_bound_on_domain_bernstein(bset, poly, bound);
111 else
112 return isl_qpolynomial_bound_on_domain_range(bset, poly, bound);
113 error:
114 isl_basic_set_free(bset);
115 isl_qpolynomial_free(poly);
116 return isl_stat_error;
119 static isl_stat unwrapped_guarded_poly_bound(__isl_take isl_basic_set *bset,
120 __isl_take isl_qpolynomial *poly, void *user)
122 struct isl_bound *bound = (struct isl_bound *)user;
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, user);
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, user);
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 polynomial "poly" over the domain "bset".
178 * If the original problem had a wrapped relation in the domain,
179 * meaning that the bound should be computed over the range
180 * of this relation, then temporarily treat the domain dimensions
181 * of this wrapped relation as parameters, compute a bound
182 * in terms of these and the original parameters,
183 * turn the parameters back into set dimensions and
184 * add the results to bound->pwf and bound->pwf_tight.
186 * Note that even though "bset" is known to live in the same space
187 * as the domain of "poly", the names of the set dimensions
188 * may be different (or missing). Make sure the naming is exactly
189 * the same before turning these dimensions into parameters
190 * to ensure that the spaces are still the same after
191 * this operation.
193 static isl_stat guarded_poly_bound(__isl_take isl_basic_set *bset,
194 __isl_take isl_qpolynomial *poly, void *user)
196 struct isl_bound *bound = (struct isl_bound *)user;
197 isl_space *space;
198 isl_pw_qpolynomial_fold *top_pwf;
199 isl_pw_qpolynomial_fold *top_pwf_tight;
200 isl_size nparam;
201 isl_size n_in;
202 isl_stat r;
204 if (!bound->wrapping)
205 return unwrapped_guarded_poly_bound(bset, poly, user);
207 nparam = isl_space_dim(bound->dim, isl_dim_param);
208 n_in = isl_space_dim(bound->dim, isl_dim_in);
209 if (nparam < 0 || n_in < 0)
210 goto error;
212 space = isl_qpolynomial_get_domain_space(poly);
213 bset = isl_basic_set_reset_space(bset, space);
215 bset = isl_basic_set_move_dims(bset, isl_dim_param, nparam,
216 isl_dim_set, 0, n_in);
217 poly = isl_qpolynomial_move_dims(poly, isl_dim_param, nparam,
218 isl_dim_in, 0, n_in);
220 space = isl_basic_set_get_space(bset);
221 space = isl_space_params(space);
223 top_pwf = bound->pwf;
224 top_pwf_tight = bound->pwf_tight;
226 space = isl_space_from_domain(space);
227 space = isl_space_add_dims(space, isl_dim_out, 1);
228 bound->pwf = isl_pw_qpolynomial_fold_zero(isl_space_copy(space),
229 bound->type);
230 bound->pwf_tight = isl_pw_qpolynomial_fold_zero(space, bound->type);
232 r = unwrapped_guarded_poly_bound(bset, poly, user);
234 bound->pwf = isl_pw_qpolynomial_fold_reset_space(bound->pwf,
235 isl_space_copy(bound->dim));
236 bound->pwf_tight = isl_pw_qpolynomial_fold_reset_space(bound->pwf_tight,
237 isl_space_copy(bound->dim));
239 isl_bound_add(bound, top_pwf);
240 isl_bound_add_tight(bound, top_pwf_tight);
242 return r;
243 error:
244 isl_basic_set_free(bset);
245 isl_qpolynomial_free(poly);
246 return isl_stat_error;
249 static isl_stat guarded_qp(__isl_take isl_qpolynomial *qp, void *user)
251 struct isl_bound *bound = (struct isl_bound *)user;
252 isl_stat r;
254 r = isl_qpolynomial_as_polynomial_on_domain(qp, bound->bset,
255 &guarded_poly_bound, user);
256 isl_qpolynomial_free(qp);
257 return r;
260 static isl_stat basic_guarded_fold(__isl_take isl_basic_set *bset, void *user)
262 struct isl_bound *bound = (struct isl_bound *)user;
263 isl_stat r;
265 bound->bset = bset;
266 r = isl_qpolynomial_fold_foreach_qpolynomial(bound->fold,
267 &guarded_qp, user);
268 isl_basic_set_free(bset);
269 return r;
272 static isl_stat guarded_fold(__isl_take isl_set *set,
273 __isl_take isl_qpolynomial_fold *fold, void *user)
275 struct isl_bound *bound = (struct isl_bound *)user;
277 if (!set || !fold)
278 goto error;
280 set = isl_set_make_disjoint(set);
282 bound->fold = fold;
283 bound->type = isl_qpolynomial_fold_get_type(fold);
285 if (isl_set_foreach_basic_set(set, &basic_guarded_fold, bound) < 0)
286 goto error;
288 isl_set_free(set);
289 isl_qpolynomial_fold_free(fold);
291 return isl_stat_ok;
292 error:
293 isl_set_free(set);
294 isl_qpolynomial_fold_free(fold);
295 return isl_stat_error;
298 __isl_give isl_pw_qpolynomial_fold *isl_pw_qpolynomial_fold_bound(
299 __isl_take isl_pw_qpolynomial_fold *pwf, isl_bool *tight)
301 isl_size nvar;
302 struct isl_bound bound;
303 isl_bool covers;
305 if (!pwf)
306 return NULL;
308 bound.dim = isl_pw_qpolynomial_fold_get_domain_space(pwf);
310 bound.wrapping = isl_space_is_wrapping(bound.dim);
311 if (bound.wrapping)
312 bound.dim = isl_space_unwrap(bound.dim);
313 nvar = isl_space_dim(bound.dim, isl_dim_out);
314 if (nvar < 0)
315 bound.dim = isl_space_free(bound.dim);
316 bound.dim = isl_space_domain(bound.dim);
317 bound.dim = isl_space_from_domain(bound.dim);
318 bound.dim = isl_space_add_dims(bound.dim, isl_dim_out, 1);
320 if (nvar == 0) {
321 if (tight)
322 *tight = isl_bool_true;
323 return isl_pw_qpolynomial_fold_reset_space(pwf, bound.dim);
326 if (isl_pw_qpolynomial_fold_is_zero(pwf)) {
327 enum isl_fold type = pwf->type;
328 isl_pw_qpolynomial_fold_free(pwf);
329 if (tight)
330 *tight = isl_bool_true;
331 return isl_pw_qpolynomial_fold_zero(bound.dim, type);
334 bound.pwf = isl_pw_qpolynomial_fold_zero(isl_space_copy(bound.dim),
335 pwf->type);
336 bound.pwf_tight = isl_pw_qpolynomial_fold_zero(isl_space_copy(bound.dim),
337 pwf->type);
338 bound.check_tight = !!tight;
340 if (isl_pw_qpolynomial_fold_foreach_lifted_piece(pwf,
341 guarded_fold, &bound) < 0)
342 goto error;
344 covers = isl_pw_qpolynomial_fold_covers(bound.pwf_tight, bound.pwf);
345 if (covers < 0)
346 goto error;
348 if (tight)
349 *tight = covers;
351 isl_space_free(bound.dim);
352 isl_pw_qpolynomial_fold_free(pwf);
354 if (covers) {
355 isl_pw_qpolynomial_fold_free(bound.pwf);
356 return bound.pwf_tight;
359 bound.pwf = isl_pw_qpolynomial_fold_fold(bound.pwf, bound.pwf_tight);
361 return bound.pwf;
362 error:
363 isl_pw_qpolynomial_fold_free(bound.pwf_tight);
364 isl_pw_qpolynomial_fold_free(bound.pwf);
365 isl_pw_qpolynomial_fold_free(pwf);
366 isl_space_free(bound.dim);
367 return NULL;
370 __isl_give isl_pw_qpolynomial_fold *isl_pw_qpolynomial_bound(
371 __isl_take isl_pw_qpolynomial *pwqp, enum isl_fold type,
372 isl_bool *tight)
374 isl_pw_qpolynomial_fold *pwf;
376 pwf = isl_pw_qpolynomial_fold_from_pw_qpolynomial(type, pwqp);
377 return isl_pw_qpolynomial_fold_bound(pwf, tight);
380 struct isl_union_bound_data {
381 enum isl_fold type;
382 isl_bool tight;
383 isl_union_pw_qpolynomial_fold *res;
386 static isl_stat bound_pw(__isl_take isl_pw_qpolynomial *pwqp, void *user)
388 struct isl_union_bound_data *data = user;
389 isl_pw_qpolynomial_fold *pwf;
391 pwf = isl_pw_qpolynomial_bound(pwqp, data->type,
392 data->tight ? &data->tight : NULL);
393 data->res = isl_union_pw_qpolynomial_fold_fold_pw_qpolynomial_fold(
394 data->res, pwf);
396 return isl_stat_ok;
399 __isl_give isl_union_pw_qpolynomial_fold *isl_union_pw_qpolynomial_bound(
400 __isl_take isl_union_pw_qpolynomial *upwqp,
401 enum isl_fold type, isl_bool *tight)
403 isl_space *space;
404 struct isl_union_bound_data data = { type, 1, NULL };
406 if (!upwqp)
407 return NULL;
409 if (!tight)
410 data.tight = isl_bool_false;
412 space = isl_union_pw_qpolynomial_get_space(upwqp);
413 data.res = isl_union_pw_qpolynomial_fold_zero(space, type);
414 if (isl_union_pw_qpolynomial_foreach_pw_qpolynomial(upwqp,
415 &bound_pw, &data) < 0)
416 goto error;
418 isl_union_pw_qpolynomial_free(upwqp);
419 if (tight)
420 *tight = data.tight;
422 return data.res;
423 error:
424 isl_union_pw_qpolynomial_free(upwqp);
425 isl_union_pw_qpolynomial_fold_free(data.res);
426 return NULL;