1 #include <isl_constraint.h>
3 #include <isl_polynomial_private.h>
13 isl_qpolynomial
*poly
;
14 isl_pw_qpolynomial_fold
*pwf
;
15 isl_pw_qpolynomial_fold
*pwf_exact
;
18 static int propagate_on_domain(__isl_take isl_basic_set
*bset
,
19 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
);
21 /* Check whether the polynomial "poly" has sign "sign" over "bset",
22 * i.e., if sign == 1, check that the lower bound on the polynomial
23 * is non-negative and if sign == -1, check that the upper bound on
24 * the polynomial is non-positive.
26 static int has_sign(__isl_keep isl_basic_set
*bset
,
27 __isl_keep isl_qpolynomial
*poly
, int sign
, int *signs
)
29 struct range_data data_m
;
36 nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
37 nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
39 bset
= isl_basic_set_copy(bset
);
40 poly
= isl_qpolynomial_copy(poly
);
42 bset
= isl_basic_set_move_dims(bset
, isl_dim_set
, 0,
43 isl_dim_param
, 0, nparam
);
44 poly
= isl_qpolynomial_move_dims(poly
, isl_dim_set
, 0,
45 isl_dim_param
, 0, nparam
);
47 dim
= isl_qpolynomial_get_dim(poly
);
48 dim
= isl_dim_drop(dim
, isl_dim_set
, 0, isl_dim_size(dim
, isl_dim_set
));
50 data_m
.test_monotonicity
= 0;
52 data_m
.pwf
= isl_pw_qpolynomial_fold_zero(dim
);
55 data_m
.pwf_exact
= NULL
;
57 if (propagate_on_domain(bset
, poly
, &data_m
) < 0)
61 opt
= isl_pw_qpolynomial_fold_min(data_m
.pwf
);
63 opt
= isl_pw_qpolynomial_fold_max(data_m
.pwf
);
67 else if (isl_qpolynomial_is_nan(opt
) ||
68 isl_qpolynomial_is_infty(opt
) ||
69 isl_qpolynomial_is_neginfty(opt
))
72 r
= sign
* isl_qpolynomial_sgn(opt
) >= 0;
74 isl_qpolynomial_free(opt
);
78 isl_pw_qpolynomial_fold_free(data_m
.pwf
);
82 /* Return 1 if poly is monotonically increasing in the last set variable,
83 * -1 if poly is monotonically decreasing in the last set variable,
87 * We simply check the sign of p(x+1)-p(x)
89 static int monotonicity(__isl_keep isl_basic_set
*bset
,
90 __isl_keep isl_qpolynomial
*poly
, struct range_data
*data
)
94 isl_qpolynomial
*sub
= NULL
;
95 isl_qpolynomial
*diff
= NULL
;
100 ctx
= isl_qpolynomial_get_ctx(poly
);
101 dim
= isl_qpolynomial_get_dim(poly
);
103 nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
105 sub
= isl_qpolynomial_var(isl_dim_copy(dim
), isl_dim_set
, nvar
- 1);
106 sub
= isl_qpolynomial_add(sub
,
107 isl_qpolynomial_rat_cst(dim
, ctx
->one
, ctx
->one
));
109 diff
= isl_qpolynomial_substitute(isl_qpolynomial_copy(poly
),
110 isl_dim_set
, nvar
- 1, 1, &sub
);
111 diff
= isl_qpolynomial_sub(diff
, isl_qpolynomial_copy(poly
));
113 s
= has_sign(bset
, diff
, 1, data
->signs
);
119 s
= has_sign(bset
, diff
, -1, data
->signs
);
126 isl_qpolynomial_free(diff
);
127 isl_qpolynomial_free(sub
);
131 isl_qpolynomial_free(diff
);
132 isl_qpolynomial_free(sub
);
136 static __isl_give isl_qpolynomial
*bound2poly(__isl_take isl_constraint
*bound
,
137 __isl_take isl_dim
*dim
, unsigned pos
, int sign
)
141 return isl_qpolynomial_infty(dim
);
143 return isl_qpolynomial_neginfty(dim
);
146 return isl_qpolynomial_from_constraint(bound
, isl_dim_set
, pos
);
149 static int bound_is_integer(__isl_take isl_constraint
*bound
, unsigned pos
)
158 isl_constraint_get_coefficient(bound
, isl_dim_set
, pos
, &c
);
159 is_int
= isl_int_is_one(c
) || isl_int_is_negone(c
);
165 struct isl_fixed_sign_data
{
168 isl_qpolynomial
*poly
;
171 /* Add term "term" to data->poly if it has sign data->sign.
172 * The sign is determined based on the signs of the parameters
173 * and variables in data->signs.
175 static int collect_fixed_sign_terms(__isl_take isl_term
*term
, void *user
)
177 struct isl_fixed_sign_data
*data
= (struct isl_fixed_sign_data
*)user
;
187 nparam
= isl_term_dim(term
, isl_dim_param
);
188 nvar
= isl_term_dim(term
, isl_dim_set
);
190 isl_assert(isl_term_get_ctx(term
), isl_term_dim(term
, isl_dim_div
) == 0,
196 isl_term_get_num(term
, &n
);
197 isl_term_get_den(term
, &d
);
199 sign
= isl_int_sgn(n
);
200 for (i
= 0; i
< nparam
; ++i
) {
201 if (data
->signs
[i
] > 0)
203 if (isl_term_get_exp(term
, isl_dim_param
, i
) % 2)
206 for (i
= 0; i
< nvar
; ++i
) {
207 if (data
->signs
[nparam
+ i
] > 0)
209 if (isl_term_get_exp(term
, isl_dim_set
, i
) % 2)
213 if (sign
== data
->sign
) {
214 isl_qpolynomial
*t
= isl_qpolynomial_from_term(term
);
216 data
->poly
= isl_qpolynomial_add(data
->poly
, t
);
226 /* Construct and return a polynomial that consists of the terms
227 * in "poly" that have sign "sign".
229 static __isl_give isl_qpolynomial
*fixed_sign_terms(
230 __isl_keep isl_qpolynomial
*poly
, int *signs
, int sign
)
232 struct isl_fixed_sign_data data
= { signs
, sign
};
233 data
.poly
= isl_qpolynomial_zero(isl_qpolynomial_get_dim(poly
));
235 if (isl_qpolynomial_foreach_term(poly
, collect_fixed_sign_terms
, &data
) < 0)
240 isl_qpolynomial_free(data
.poly
);
244 /* Helper function to add a guarder polynomial to either pwf_exact or pwf,
245 * depending on whether the result has been determined to be exact.
247 static int add_guarded_poly(__isl_take isl_basic_set
*bset
,
248 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
)
250 enum isl_fold type
= data
->sign
< 0 ? isl_fold_min
: isl_fold_max
;
252 isl_qpolynomial_fold
*fold
;
253 isl_pw_qpolynomial_fold
*pwf
;
255 fold
= isl_qpolynomial_fold_alloc(type
, poly
);
256 set
= isl_set_from_basic_set(bset
);
257 pwf
= isl_pw_qpolynomial_fold_alloc(set
, fold
);
259 data
->pwf_exact
= isl_pw_qpolynomial_fold_add(
260 data
->pwf_exact
, pwf
);
262 data
->pwf
= isl_pw_qpolynomial_fold_add(data
->pwf
, pwf
);
267 /* Given a lower and upper bound on the final variable and constraints
268 * on the remaining variables where these bounds are active,
269 * eliminate the variable from data->poly based on these bounds.
270 * If the polynomial has been determined to be monotonic
271 * in the variable, then simply plug in the appropriate bound.
272 * If the current polynomial is exact and if this bound is integer,
273 * then the result is still exact. In all other cases, the results
275 * Otherwise, plug in the largest bound (in absolute value) in
276 * the positive terms (if an upper bound is wanted) or the negative terms
277 * (if a lower bounded is wanted) and the other bound in the other terms.
279 * If all variables have been eliminated, then record the result.
280 * Ohterwise, recurse on the next variable.
282 static int propagate_on_bound_pair(__isl_take isl_constraint
*lower
,
283 __isl_take isl_constraint
*upper
, __isl_take isl_basic_set
*bset
,
286 struct range_data
*data
= (struct range_data
*)user
;
287 int save_exact
= data
->exact
;
288 isl_qpolynomial
*poly
;
292 nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
294 if (data
->monotonicity
) {
295 isl_qpolynomial
*sub
;
296 isl_dim
*dim
= isl_qpolynomial_get_dim(data
->poly
);
297 if (data
->monotonicity
* data
->sign
> 0) {
299 data
->exact
= bound_is_integer(upper
, nvar
);
300 sub
= bound2poly(upper
, dim
, nvar
, 1);
301 isl_constraint_free(lower
);
304 data
->exact
= bound_is_integer(lower
, nvar
);
305 sub
= bound2poly(lower
, dim
, nvar
, -1);
306 isl_constraint_free(upper
);
308 poly
= isl_qpolynomial_copy(data
->poly
);
309 poly
= isl_qpolynomial_substitute(poly
, isl_dim_set
, nvar
, 1, &sub
);
310 poly
= isl_qpolynomial_drop_dims(poly
, isl_dim_set
, nvar
, 1);
312 isl_qpolynomial_free(sub
);
314 isl_qpolynomial
*l
, *u
;
315 isl_qpolynomial
*pos
, *neg
;
316 isl_dim
*dim
= isl_qpolynomial_get_dim(data
->poly
);
317 unsigned nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
318 int sign
= data
->sign
* data
->signs
[nparam
+ nvar
];
322 u
= bound2poly(upper
, isl_dim_copy(dim
), nvar
, 1);
323 l
= bound2poly(lower
, dim
, nvar
, -1);
325 pos
= fixed_sign_terms(data
->poly
, data
->signs
, sign
);
326 neg
= fixed_sign_terms(data
->poly
, data
->signs
, -sign
);
328 pos
= isl_qpolynomial_substitute(pos
, isl_dim_set
, nvar
, 1, &u
);
329 neg
= isl_qpolynomial_substitute(neg
, isl_dim_set
, nvar
, 1, &l
);
331 poly
= isl_qpolynomial_add(pos
, neg
);
332 poly
= isl_qpolynomial_drop_dims(poly
, isl_dim_set
, nvar
, 1);
334 isl_qpolynomial_free(u
);
335 isl_qpolynomial_free(l
);
338 if (isl_basic_set_dim(bset
, isl_dim_set
) == 0)
339 r
= add_guarded_poly(bset
, poly
, data
);
341 r
= propagate_on_domain(bset
, poly
, data
);
343 data
->exact
= save_exact
;
348 /* Recursively perform range propagation on the polynomial "poly"
349 * defined over the basic set "bset" and collect the results in "data".
351 static int propagate_on_domain(__isl_take isl_basic_set
*bset
,
352 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
)
354 isl_qpolynomial
*save_poly
= data
->poly
;
355 int save_monotonicity
= data
->monotonicity
;
361 d
= isl_basic_set_dim(bset
, isl_dim_set
);
362 isl_assert(bset
->ctx
, d
>= 1, goto error
);
364 if (isl_qpolynomial_is_cst(poly
, NULL
, NULL
)) {
365 bset
= isl_basic_set_project_out(bset
, isl_dim_set
, 0, d
);
366 poly
= isl_qpolynomial_drop_dims(poly
, isl_dim_set
, 0, d
);
367 return add_guarded_poly(bset
, poly
, data
);
370 if (data
->test_monotonicity
)
371 data
->monotonicity
= monotonicity(bset
, poly
, data
);
373 data
->monotonicity
= 0;
374 if (data
->monotonicity
< -1)
378 if (isl_basic_set_foreach_bound_pair(bset
, isl_dim_set
, d
- 1,
379 &propagate_on_bound_pair
, data
) < 0)
382 isl_basic_set_free(bset
);
383 isl_qpolynomial_free(poly
);
384 data
->monotonicity
= save_monotonicity
;
385 data
->poly
= save_poly
;
389 isl_basic_set_free(bset
);
390 isl_qpolynomial_free(poly
);
391 data
->monotonicity
= save_monotonicity
;
392 data
->poly
= save_poly
;
396 static int basic_guarded_poly_bound(__isl_take isl_basic_set
*bset
, void *user
)
398 struct range_data
*data
= (struct range_data
*)user
;
399 unsigned nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
400 unsigned dim
= isl_basic_set_dim(bset
, isl_dim_set
);
405 data
->signs
= isl_alloc_array(bset
->ctx
, int,
406 isl_basic_set_dim(bset
, isl_dim_all
));
408 if (isl_basic_set_dims_get_sign(bset
, isl_dim_set
, 0, dim
,
409 data
->signs
+ nparam
) < 0)
411 if (isl_basic_set_dims_get_sign(bset
, isl_dim_param
, 0, nparam
,
415 r
= propagate_on_domain(bset
, isl_qpolynomial_copy(data
->poly
), data
);
422 isl_basic_set_free(bset
);
426 static int compressed_guarded_poly_bound(__isl_take isl_basic_set
*bset
,
427 __isl_take isl_qpolynomial
*poly
, void *user
)
429 struct range_data
*data
= (struct range_data
*)user
;
430 unsigned nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
431 unsigned nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
438 return add_guarded_poly(bset
, poly
, data
);
440 set
= isl_set_from_basic_set(bset
);
441 set
= isl_set_split_dims(set
, isl_dim_param
, 0, nparam
);
442 set
= isl_set_split_dims(set
, isl_dim_set
, 0, nvar
);
446 if (isl_set_foreach_basic_set(set
, &basic_guarded_poly_bound
, data
) < 0)
450 isl_qpolynomial_free(poly
);
455 isl_qpolynomial_free(poly
);
459 static int guarded_poly_bound(__isl_take isl_basic_set
*bset
,
460 __isl_take isl_qpolynomial
*poly
, void *user
)
462 struct range_data
*data
= (struct range_data
*)user
;
463 isl_pw_qpolynomial_fold
*top_pwf
;
464 isl_pw_qpolynomial_fold
*top_pwf_exact
;
466 isl_morph
*morph
, *morph2
;
470 bset
= isl_basic_set_detect_equalities(bset
);
476 return compressed_guarded_poly_bound(bset
, poly
, user
);
478 orig_nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
480 morph
= isl_basic_set_variable_compression(bset
, isl_dim_param
);
481 bset
= isl_morph_basic_set(isl_morph_copy(morph
), bset
);
483 morph2
= isl_basic_set_parameter_compression(bset
);
484 bset
= isl_morph_basic_set(isl_morph_copy(morph2
), bset
);
486 morph
= isl_morph_compose(morph2
, morph
);
488 morph2
= isl_basic_set_variable_compression(bset
, isl_dim_set
);
489 bset
= isl_morph_basic_set(isl_morph_copy(morph2
), bset
);
491 morph2
= isl_morph_compose(morph2
, isl_morph_copy(morph
));
492 poly
= isl_qpolynomial_morph(poly
, morph2
);
494 dim
= isl_morph_get_ran_dim(morph
);
495 dim
= isl_dim_drop(dim
, isl_dim_set
, 0, isl_dim_size(dim
, isl_dim_set
));
498 top_pwf_exact
= data
->pwf_exact
;
500 data
->pwf
= isl_pw_qpolynomial_fold_zero(isl_dim_copy(dim
));
501 data
->pwf_exact
= isl_pw_qpolynomial_fold_zero(dim
);
503 r
= compressed_guarded_poly_bound(bset
, poly
, user
);
505 morph
= isl_morph_drop_dims(morph
, isl_dim_set
, 0, orig_nvar
);
506 morph
= isl_morph_inverse(morph
);
508 data
->pwf
= isl_pw_qpolynomial_fold_morph(data
->pwf
,
509 isl_morph_copy(morph
));
510 data
->pwf_exact
= isl_pw_qpolynomial_fold_morph(data
->pwf_exact
, morph
);
512 data
->pwf
= isl_pw_qpolynomial_fold_add(top_pwf
, data
->pwf
);
513 data
->pwf_exact
= isl_pw_qpolynomial_fold_add(top_pwf_exact
,
518 isl_basic_set_free(bset
);
519 isl_qpolynomial_free(poly
);
523 static int basic_guarded_bound(__isl_take isl_basic_set
*bset
, void *user
)
525 struct range_data
*data
= (struct range_data
*)user
;
528 r
= isl_qpolynomial_as_polynomial_on_domain(data
->qp
, bset
,
529 &guarded_poly_bound
, user
);
530 isl_basic_set_free(bset
);
534 static int guarded_bound(__isl_take isl_set
*set
,
535 __isl_take isl_qpolynomial
*qp
, void *user
)
537 struct range_data
*data
= (struct range_data
*)user
;
542 set
= isl_set_make_disjoint(set
);
546 if (isl_set_foreach_basic_set(set
, &basic_guarded_bound
, data
) < 0)
550 isl_qpolynomial_free(qp
);
555 isl_qpolynomial_free(qp
);
559 /* Compute a lower or upper bound (depending on "type") on the given
560 * piecewise step-polynomial using range propagation.
562 __isl_give isl_pw_qpolynomial_fold
*isl_pw_qpolynomial_bound_range(
563 __isl_take isl_pw_qpolynomial
*pwqp
, enum isl_fold type
, int *exact
)
566 isl_pw_qpolynomial_fold
*pwf
;
569 struct range_data data
;
575 dim
= isl_pw_qpolynomial_get_dim(pwqp
);
576 nvar
= isl_dim_size(dim
, isl_dim_set
);
578 if (isl_pw_qpolynomial_is_zero(pwqp
)) {
579 isl_pw_qpolynomial_free(pwqp
);
580 dim
= isl_dim_drop(dim
, isl_dim_set
, 0, nvar
);
581 return isl_pw_qpolynomial_fold_zero(dim
);
586 return isl_pw_qpolynomial_fold_from_pw_qpolynomial(type
, pwqp
);
589 dim
= isl_dim_drop(dim
, isl_dim_set
, 0, nvar
);
591 nparam
= isl_dim_size(dim
, isl_dim_param
);
592 data
.pwf
= isl_pw_qpolynomial_fold_zero(isl_dim_copy(dim
));
593 data
.pwf_exact
= isl_pw_qpolynomial_fold_zero(isl_dim_copy(dim
));
594 if (type
== isl_fold_min
)
598 data
.test_monotonicity
= 1;
599 data
.exact
= !!exact
;
601 if (isl_pw_qpolynomial_foreach_lifted_piece(pwqp
, guarded_bound
, &data
))
604 covers
= isl_pw_qpolynomial_fold_covers(data
.pwf_exact
, data
.pwf
);
612 isl_pw_qpolynomial_free(pwqp
);
615 isl_pw_qpolynomial_fold_free(data
.pwf
);
616 return data
.pwf_exact
;
619 data
.pwf
= isl_pw_qpolynomial_fold_add(data
.pwf
, data
.pwf_exact
);
623 isl_pw_qpolynomial_fold_free(data
.pwf
);
625 isl_pw_qpolynomial_free(pwqp
);