| 1 | /* |
| 2 | * Copyright 2010 INRIA Saclay |
| 3 | * |
| 4 | * Use of this software is governed by the MIT license |
| 5 | * |
| 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 | */ |
| 10 | |
| 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> |
| 18 | |
| 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. |
| 23 | */ |
| 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) |
| 27 | { |
| 28 | isl_set *dom; |
| 29 | isl_qpolynomial_fold *fold; |
| 30 | isl_pw_qpolynomial_fold *pwf; |
| 31 | |
| 32 | fold = isl_qpolynomial_fold_alloc(type, qp: 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, set: dom, fold); |
| 37 | return isl_pw_qpolynomial_fold_project_domain_on_params(pwf); |
| 38 | } |
| 39 | |
| 40 | /* Add the bound "pwf", which is not known to be tight, |
| 41 | * to the output of "bound". |
| 42 | */ |
| 43 | isl_stat isl_bound_add(struct isl_bound *bound, |
| 44 | __isl_take isl_pw_qpolynomial_fold *pwf) |
| 45 | { |
| 46 | bound->pwf = isl_pw_qpolynomial_fold_fold(pwf1: bound->pwf, pwf2: pwf); |
| 47 | return isl_stat_non_null(obj: bound->pwf); |
| 48 | } |
| 49 | |
| 50 | /* Add the bound "pwf", which is known to be tight, |
| 51 | * to the output of "bound". |
| 52 | */ |
| 53 | isl_stat isl_bound_add_tight(struct isl_bound *bound, |
| 54 | __isl_take isl_pw_qpolynomial_fold *pwf) |
| 55 | { |
| 56 | bound->pwf_tight = isl_pw_qpolynomial_fold_fold(pwf1: bound->pwf_tight, pwf2: pwf); |
| 57 | return isl_stat_non_null(obj: bound->pwf); |
| 58 | } |
| 59 | |
| 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". |
| 64 | */ |
| 65 | static isl_stat add_constant_poly(__isl_take isl_basic_set *bset, |
| 66 | __isl_take isl_qpolynomial *poly, struct isl_bound *bound) |
| 67 | { |
| 68 | isl_pw_qpolynomial_fold *pwf; |
| 69 | |
| 70 | pwf = isl_qpolynomial_cst_bound(bset, poly, type: bound->type, NULL); |
| 71 | return isl_bound_add_tight(bound, pwf); |
| 72 | } |
| 73 | |
| 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. |
| 80 | * |
| 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. |
| 84 | */ |
| 85 | static isl_stat compressed_guarded_poly_bound(__isl_take isl_basic_set *bset, |
| 86 | __isl_take isl_qpolynomial *poly, void *user) |
| 87 | { |
| 88 | struct isl_bound *bound = (struct isl_bound *)user; |
| 89 | isl_ctx *ctx; |
| 90 | int bounded; |
| 91 | int degree; |
| 92 | |
| 93 | if (!bset || !poly) |
| 94 | goto error; |
| 95 | |
| 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); |
| 101 | |
| 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); |
| 105 | |
| 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(qp: poly); |
| 116 | return isl_stat_error; |
| 117 | } |
| 118 | |
| 119 | static isl_stat unwrapped_guarded_poly_bound(__isl_take isl_basic_set *bset, |
| 120 | __isl_take isl_qpolynomial *poly, void *user) |
| 121 | { |
| 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; |
| 128 | |
| 129 | bset = isl_basic_set_detect_equalities(bset); |
| 130 | |
| 131 | if (!bset) |
| 132 | goto error; |
| 133 | |
| 134 | if (bset->n_eq == 0) |
| 135 | return compressed_guarded_poly_bound(bset, poly, user); |
| 136 | |
| 137 | morph = isl_basic_set_full_compression(bset); |
| 138 | |
| 139 | bset = isl_morph_basic_set(morph: isl_morph_copy(morph), bset); |
| 140 | poly = isl_qpolynomial_morph_domain(qp: poly, morph: isl_morph_copy(morph)); |
| 141 | |
| 142 | space = isl_morph_get_ran_space(morph); |
| 143 | space = isl_space_params(space); |
| 144 | |
| 145 | top_pwf = bound->pwf; |
| 146 | top_pwf_tight = bound->pwf_tight; |
| 147 | |
| 148 | space = isl_space_from_domain(space); |
| 149 | space = isl_space_add_dims(space, type: isl_dim_out, n: 1); |
| 150 | bound->pwf = isl_pw_qpolynomial_fold_zero(space: isl_space_copy(space), |
| 151 | type: bound->type); |
| 152 | bound->pwf_tight = isl_pw_qpolynomial_fold_zero(space, type: bound->type); |
| 153 | |
| 154 | r = compressed_guarded_poly_bound(bset, poly, user); |
| 155 | |
| 156 | morph = isl_morph_dom_params(morph); |
| 157 | morph = isl_morph_ran_params(morph); |
| 158 | morph = isl_morph_inverse(morph); |
| 159 | |
| 160 | bound->pwf = isl_pw_qpolynomial_fold_morph_domain(pwf: bound->pwf, |
| 161 | morph: isl_morph_copy(morph)); |
| 162 | bound->pwf_tight = isl_pw_qpolynomial_fold_morph_domain( |
| 163 | pwf: bound->pwf_tight, morph); |
| 164 | |
| 165 | isl_bound_add(bound, pwf: top_pwf); |
| 166 | isl_bound_add_tight(bound, pwf: top_pwf_tight); |
| 167 | |
| 168 | return r; |
| 169 | error: |
| 170 | isl_basic_set_free(bset); |
| 171 | isl_qpolynomial_free(qp: poly); |
| 172 | return isl_stat_error; |
| 173 | } |
| 174 | |
| 175 | /* Update bound->pwf and bound->pwf_tight with a bound |
| 176 | * of type bound->type on the polynomial "poly" over the domain "bset". |
| 177 | * |
| 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. |
| 185 | * |
| 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. |
| 192 | */ |
| 193 | static isl_stat guarded_poly_bound(__isl_take isl_basic_set *bset, |
| 194 | __isl_take isl_qpolynomial *poly, void *user) |
| 195 | { |
| 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; |
| 203 | |
| 204 | if (!bound->wrapping) |
| 205 | return unwrapped_guarded_poly_bound(bset, poly, user); |
| 206 | |
| 207 | nparam = isl_space_dim(space: bound->dim, type: isl_dim_param); |
| 208 | n_in = isl_space_dim(space: bound->dim, type: isl_dim_in); |
| 209 | if (nparam < 0 || n_in < 0) |
| 210 | goto error; |
| 211 | |
| 212 | space = isl_qpolynomial_get_domain_space(qp: poly); |
| 213 | bset = isl_basic_set_reset_space(bset, space); |
| 214 | |
| 215 | bset = isl_basic_set_move_dims(bset, dst_type: isl_dim_param, dst_pos: nparam, |
| 216 | src_type: isl_dim_set, src_pos: 0, n: n_in); |
| 217 | poly = isl_qpolynomial_move_dims(qp: poly, dst_type: isl_dim_param, dst_pos: nparam, |
| 218 | src_type: isl_dim_in, src_pos: 0, n: n_in); |
| 219 | |
| 220 | space = isl_basic_set_get_space(bset); |
| 221 | space = isl_space_params(space); |
| 222 | |
| 223 | top_pwf = bound->pwf; |
| 224 | top_pwf_tight = bound->pwf_tight; |
| 225 | |
| 226 | space = isl_space_from_domain(space); |
| 227 | space = isl_space_add_dims(space, type: isl_dim_out, n: 1); |
| 228 | bound->pwf = isl_pw_qpolynomial_fold_zero(space: isl_space_copy(space), |
| 229 | type: bound->type); |
| 230 | bound->pwf_tight = isl_pw_qpolynomial_fold_zero(space, type: bound->type); |
| 231 | |
| 232 | r = unwrapped_guarded_poly_bound(bset, poly, user); |
| 233 | |
| 234 | bound->pwf = isl_pw_qpolynomial_fold_reset_space(pwf: bound->pwf, |
| 235 | space: isl_space_copy(space: bound->dim)); |
| 236 | bound->pwf_tight = isl_pw_qpolynomial_fold_reset_space(pwf: bound->pwf_tight, |
| 237 | space: isl_space_copy(space: bound->dim)); |
| 238 | |
| 239 | isl_bound_add(bound, pwf: top_pwf); |
| 240 | isl_bound_add_tight(bound, pwf: top_pwf_tight); |
| 241 | |
| 242 | return r; |
| 243 | error: |
| 244 | isl_basic_set_free(bset); |
| 245 | isl_qpolynomial_free(qp: poly); |
| 246 | return isl_stat_error; |
| 247 | } |
| 248 | |
| 249 | static isl_stat guarded_qp(__isl_take isl_qpolynomial *qp, void *user) |
| 250 | { |
| 251 | struct isl_bound *bound = (struct isl_bound *)user; |
| 252 | isl_stat r; |
| 253 | |
| 254 | r = isl_qpolynomial_as_polynomial_on_domain(qp, bset: bound->bset, |
| 255 | fn: &guarded_poly_bound, user); |
| 256 | isl_qpolynomial_free(qp); |
| 257 | return r; |
| 258 | } |
| 259 | |
| 260 | static isl_stat basic_guarded_fold(__isl_take isl_basic_set *bset, void *user) |
| 261 | { |
| 262 | struct isl_bound *bound = (struct isl_bound *)user; |
| 263 | isl_stat r; |
| 264 | |
| 265 | bound->bset = bset; |
| 266 | r = isl_qpolynomial_fold_foreach_qpolynomial(fold: bound->fold, |
| 267 | fn: &guarded_qp, user); |
| 268 | isl_basic_set_free(bset); |
| 269 | return r; |
| 270 | } |
| 271 | |
| 272 | static isl_stat guarded_fold(__isl_take isl_set *set, |
| 273 | __isl_take isl_qpolynomial_fold *fold, void *user) |
| 274 | { |
| 275 | struct isl_bound *bound = (struct isl_bound *)user; |
| 276 | |
| 277 | if (!set || !fold) |
| 278 | goto error; |
| 279 | |
| 280 | set = isl_set_make_disjoint(set); |
| 281 | |
| 282 | bound->fold = fold; |
| 283 | bound->type = isl_qpolynomial_fold_get_type(fold); |
| 284 | |
| 285 | if (isl_set_foreach_basic_set(set, fn: &basic_guarded_fold, user: bound) < 0) |
| 286 | goto error; |
| 287 | |
| 288 | isl_set_free(set); |
| 289 | isl_qpolynomial_fold_free(fold); |
| 290 | |
| 291 | return isl_stat_ok; |
| 292 | error: |
| 293 | isl_set_free(set); |
| 294 | isl_qpolynomial_fold_free(fold); |
| 295 | return isl_stat_error; |
| 296 | } |
| 297 | |
| 298 | __isl_give isl_pw_qpolynomial_fold *isl_pw_qpolynomial_fold_bound( |
| 299 | __isl_take isl_pw_qpolynomial_fold *pwf, isl_bool *tight) |
| 300 | { |
| 301 | isl_size nvar; |
| 302 | struct isl_bound bound; |
| 303 | isl_bool covers; |
| 304 | |
| 305 | if (!pwf) |
| 306 | return NULL; |
| 307 | |
| 308 | bound.dim = isl_pw_qpolynomial_fold_get_domain_space(pwf); |
| 309 | |
| 310 | bound.wrapping = isl_space_is_wrapping(space: bound.dim); |
| 311 | if (bound.wrapping) |
| 312 | bound.dim = isl_space_unwrap(space: bound.dim); |
| 313 | nvar = isl_space_dim(space: bound.dim, type: isl_dim_out); |
| 314 | if (nvar < 0) |
| 315 | bound.dim = isl_space_free(space: bound.dim); |
| 316 | bound.dim = isl_space_domain(space: bound.dim); |
| 317 | bound.dim = isl_space_from_domain(space: bound.dim); |
| 318 | bound.dim = isl_space_add_dims(space: bound.dim, type: isl_dim_out, n: 1); |
| 319 | |
| 320 | if (nvar == 0) { |
| 321 | if (tight) |
| 322 | *tight = isl_bool_true; |
| 323 | return isl_pw_qpolynomial_fold_reset_space(pwf, space: bound.dim); |
| 324 | } |
| 325 | |
| 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(space: bound.dim, type); |
| 332 | } |
| 333 | |
| 334 | bound.pwf = isl_pw_qpolynomial_fold_zero(space: isl_space_copy(space: bound.dim), |
| 335 | type: pwf->type); |
| 336 | bound.pwf_tight = isl_pw_qpolynomial_fold_zero(space: isl_space_copy(space: bound.dim), |
| 337 | type: pwf->type); |
| 338 | bound.check_tight = !!tight; |
| 339 | |
| 340 | if (isl_pw_qpolynomial_fold_foreach_lifted_piece(pwf, |
| 341 | fn: guarded_fold, user: &bound) < 0) |
| 342 | goto error; |
| 343 | |
| 344 | covers = isl_pw_qpolynomial_fold_covers(pwf1: bound.pwf_tight, pwf2: bound.pwf); |
| 345 | if (covers < 0) |
| 346 | goto error; |
| 347 | |
| 348 | if (tight) |
| 349 | *tight = covers; |
| 350 | |
| 351 | isl_space_free(space: bound.dim); |
| 352 | isl_pw_qpolynomial_fold_free(pwf); |
| 353 | |
| 354 | if (covers) { |
| 355 | isl_pw_qpolynomial_fold_free(pwf: bound.pwf); |
| 356 | return bound.pwf_tight; |
| 357 | } |
| 358 | |
| 359 | bound.pwf = isl_pw_qpolynomial_fold_fold(pwf1: bound.pwf, pwf2: bound.pwf_tight); |
| 360 | |
| 361 | return bound.pwf; |
| 362 | error: |
| 363 | isl_pw_qpolynomial_fold_free(pwf: bound.pwf_tight); |
| 364 | isl_pw_qpolynomial_fold_free(pwf: bound.pwf); |
| 365 | isl_pw_qpolynomial_fold_free(pwf); |
| 366 | isl_space_free(space: bound.dim); |
| 367 | return NULL; |
| 368 | } |
| 369 | |
| 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) |
| 373 | { |
| 374 | isl_pw_qpolynomial_fold *pwf; |
| 375 | |
| 376 | pwf = isl_pw_qpolynomial_fold_from_pw_qpolynomial(type, pwqp); |
| 377 | return isl_pw_qpolynomial_fold_bound(pwf, tight); |
| 378 | } |
| 379 | |
| 380 | struct isl_union_bound_data { |
| 381 | enum isl_fold type; |
| 382 | isl_bool tight; |
| 383 | isl_union_pw_qpolynomial_fold *res; |
| 384 | }; |
| 385 | |
| 386 | static isl_stat bound_pw(__isl_take isl_pw_qpolynomial *pwqp, void *user) |
| 387 | { |
| 388 | struct isl_union_bound_data *data = user; |
| 389 | isl_pw_qpolynomial_fold *pwf; |
| 390 | |
| 391 | pwf = isl_pw_qpolynomial_bound(pwqp, type: data->type, |
| 392 | tight: data->tight ? &data->tight : NULL); |
| 393 | data->res = isl_union_pw_qpolynomial_fold_fold_pw_qpolynomial_fold( |
| 394 | upwqp: data->res, pwqp: pwf); |
| 395 | |
| 396 | return isl_stat_ok; |
| 397 | } |
| 398 | |
| 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) |
| 402 | { |
| 403 | isl_space *space; |
| 404 | struct isl_union_bound_data data = { type, 1, NULL }; |
| 405 | |
| 406 | if (!upwqp) |
| 407 | return NULL; |
| 408 | |
| 409 | if (!tight) |
| 410 | data.tight = isl_bool_false; |
| 411 | |
| 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 | fn: &bound_pw, user: &data) < 0) |
| 416 | goto error; |
| 417 | |
| 418 | isl_union_pw_qpolynomial_free(upwqp); |
| 419 | if (tight) |
| 420 | *tight = data.tight; |
| 421 | |
| 422 | return data.res; |
| 423 | error: |
| 424 | isl_union_pw_qpolynomial_free(upwqp); |
| 425 | isl_union_pw_qpolynomial_fold_free(upwf: data.res); |
| 426 | return NULL; |
| 427 | } |
| 428 | |