1 #include <isl_ctx_private.h>
3 #include <isl_constraint_private.h>
5 #include <isl_polynomial_private.h>
10 struct isl_bound
*bound
;
13 int test_monotonicity
;
16 isl_qpolynomial
*poly
;
17 isl_pw_qpolynomial_fold
*pwf
;
18 isl_pw_qpolynomial_fold
*pwf_tight
;
21 static isl_stat
propagate_on_domain(__isl_take isl_basic_set
*bset
,
22 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
);
24 /* Check whether the polynomial "poly" has sign "sign" over "bset",
25 * i.e., if sign == 1, check that the lower bound on the polynomial
26 * is non-negative and if sign == -1, check that the upper bound on
27 * the polynomial is non-positive.
29 static isl_bool
has_sign(__isl_keep isl_basic_set
*bset
,
30 __isl_keep isl_qpolynomial
*poly
, int sign
, int *signs
)
32 struct range_data data_m
;
39 nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
41 return isl_bool_error
;
43 bset
= isl_basic_set_copy(bset
);
44 poly
= isl_qpolynomial_copy(poly
);
46 bset
= isl_basic_set_move_dims(bset
, isl_dim_set
, 0,
47 isl_dim_param
, 0, nparam
);
48 poly
= isl_qpolynomial_move_dims(poly
, isl_dim_in
, 0,
49 isl_dim_param
, 0, nparam
);
51 space
= isl_qpolynomial_get_space(poly
);
52 space
= isl_space_params(space
);
53 space
= isl_space_from_domain(space
);
54 space
= isl_space_add_dims(space
, isl_dim_out
, 1);
56 data_m
.test_monotonicity
= 0;
59 type
= data_m
.sign
< 0 ? isl_fold_min
: isl_fold_max
;
60 data_m
.pwf
= isl_pw_qpolynomial_fold_zero(space
, type
);
62 data_m
.pwf_tight
= NULL
;
64 if (propagate_on_domain(bset
, poly
, &data_m
) < 0)
68 opt
= isl_pw_qpolynomial_fold_min(data_m
.pwf
);
70 opt
= isl_pw_qpolynomial_fold_max(data_m
.pwf
);
74 else if (isl_val_is_nan(opt
) ||
75 isl_val_is_infty(opt
) ||
76 isl_val_is_neginfty(opt
))
79 r
= sign
* isl_val_sgn(opt
) >= 0;
85 isl_pw_qpolynomial_fold_free(data_m
.pwf
);
86 return isl_bool_error
;
89 /* Return 1 if poly is monotonically increasing in the last set variable,
90 * -1 if poly is monotonically decreasing in the last set variable,
94 * We simply check the sign of p(x+1)-p(x)
96 static int monotonicity(__isl_keep isl_basic_set
*bset
,
97 __isl_keep isl_qpolynomial
*poly
, struct range_data
*data
)
101 isl_qpolynomial
*sub
= NULL
;
102 isl_qpolynomial
*diff
= NULL
;
107 nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
111 ctx
= isl_qpolynomial_get_ctx(poly
);
112 space
= isl_qpolynomial_get_domain_space(poly
);
114 sub
= isl_qpolynomial_var_on_domain(isl_space_copy(space
),
115 isl_dim_set
, nvar
- 1);
116 sub
= isl_qpolynomial_add(sub
,
117 isl_qpolynomial_rat_cst_on_domain(space
, ctx
->one
, ctx
->one
));
119 diff
= isl_qpolynomial_substitute(isl_qpolynomial_copy(poly
),
120 isl_dim_in
, nvar
- 1, 1, &sub
);
121 diff
= isl_qpolynomial_sub(diff
, isl_qpolynomial_copy(poly
));
123 s
= has_sign(bset
, diff
, 1, data
->signs
);
129 s
= has_sign(bset
, diff
, -1, data
->signs
);
136 isl_qpolynomial_free(diff
);
137 isl_qpolynomial_free(sub
);
141 isl_qpolynomial_free(diff
);
142 isl_qpolynomial_free(sub
);
146 /* Return a positive ("sign" > 0) or negative ("sign" < 0) infinite polynomial
147 * with domain space "space".
149 static __isl_give isl_qpolynomial
*signed_infty(__isl_take isl_space
*space
,
153 return isl_qpolynomial_infty_on_domain(space
);
155 return isl_qpolynomial_neginfty_on_domain(space
);
158 static __isl_give isl_qpolynomial
*bound2poly(__isl_take isl_constraint
*bound
,
159 __isl_take isl_space
*space
, unsigned pos
, int sign
)
162 return signed_infty(space
, sign
);
163 isl_space_free(space
);
164 return isl_qpolynomial_from_constraint(bound
, isl_dim_set
, pos
);
167 static int bound_is_integer(__isl_keep isl_constraint
*bound
, unsigned pos
)
176 isl_constraint_get_coefficient(bound
, isl_dim_set
, pos
, &c
);
177 is_int
= isl_int_is_one(c
) || isl_int_is_negone(c
);
183 struct isl_fixed_sign_data
{
186 isl_qpolynomial
*poly
;
189 /* Add term "term" to data->poly if it has sign data->sign.
190 * The sign is determined based on the signs of the parameters
191 * and variables in data->signs. The integer divisions, if
192 * any, are assumed to be non-negative.
194 static isl_stat
collect_fixed_sign_terms(__isl_take isl_term
*term
, void *user
)
196 struct isl_fixed_sign_data
*data
= (struct isl_fixed_sign_data
*)user
;
203 nparam
= isl_term_dim(term
, isl_dim_param
);
204 nvar
= isl_term_dim(term
, isl_dim_set
);
205 if (nparam
< 0 || nvar
< 0)
206 return isl_stat_error
;
209 isl_term_get_num(term
, &n
);
210 sign
= isl_int_sgn(n
);
213 for (i
= 0; i
< nparam
; ++i
) {
214 if (data
->signs
[i
] > 0)
216 if (isl_term_get_exp(term
, isl_dim_param
, i
) % 2)
219 for (i
= 0; i
< nvar
; ++i
) {
220 if (data
->signs
[nparam
+ i
] > 0)
222 if (isl_term_get_exp(term
, isl_dim_set
, i
) % 2)
226 if (sign
== data
->sign
) {
227 isl_qpolynomial
*t
= isl_qpolynomial_from_term(term
);
229 data
->poly
= isl_qpolynomial_add(data
->poly
, t
);
236 /* Construct and return a polynomial that consists of the terms
237 * in "poly" that have sign "sign". The integer divisions, if
238 * any, are assumed to be non-negative.
240 __isl_give isl_qpolynomial
*isl_qpolynomial_terms_of_sign(
241 __isl_keep isl_qpolynomial
*poly
, int *signs
, int sign
)
244 struct isl_fixed_sign_data data
= { signs
, sign
};
246 space
= isl_qpolynomial_get_domain_space(poly
);
247 data
.poly
= isl_qpolynomial_zero_on_domain(space
);
249 if (isl_qpolynomial_foreach_term(poly
, collect_fixed_sign_terms
, &data
) < 0)
254 isl_qpolynomial_free(data
.poly
);
258 /* Helper function to add a guarded polynomial to either pwf_tight or pwf,
259 * depending on whether the result has been determined to be tight.
261 static isl_stat
add_guarded_poly(__isl_take isl_basic_set
*bset
,
262 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
)
264 enum isl_fold type
= data
->sign
< 0 ? isl_fold_min
: isl_fold_max
;
266 isl_qpolynomial_fold
*fold
;
267 isl_pw_qpolynomial_fold
*pwf
;
269 bset
= isl_basic_set_params(bset
);
270 poly
= isl_qpolynomial_project_domain_on_params(poly
);
272 fold
= isl_qpolynomial_fold_alloc(type
, poly
);
273 set
= isl_set_from_basic_set(bset
);
274 pwf
= isl_pw_qpolynomial_fold_alloc(type
, set
, fold
);
276 data
->pwf_tight
= isl_pw_qpolynomial_fold_fold(
277 data
->pwf_tight
, pwf
);
279 data
->pwf
= isl_pw_qpolynomial_fold_fold(data
->pwf
, pwf
);
284 /* Plug in "sub" for the variable at position "pos" in "poly".
286 * If "sub" is an infinite polynomial and if the variable actually
287 * appears in "poly", then calling isl_qpolynomial_substitute
288 * to perform the substitution may result in a NaN result.
289 * In such cases, return positive or negative infinity instead,
290 * depending on whether an upper bound or a lower bound is being computed,
291 * and mark the result as not being tight.
293 static __isl_give isl_qpolynomial
*plug_in_at_pos(
294 __isl_take isl_qpolynomial
*poly
, int pos
,
295 __isl_take isl_qpolynomial
*sub
, struct range_data
*data
)
297 isl_bool involves
, infty
;
299 involves
= isl_qpolynomial_involves_dims(poly
, isl_dim_in
, pos
, 1);
303 isl_qpolynomial_free(sub
);
307 infty
= isl_qpolynomial_is_infty(sub
);
308 if (infty
>= 0 && !infty
)
309 infty
= isl_qpolynomial_is_neginfty(sub
);
313 isl_space
*space
= isl_qpolynomial_get_domain_space(poly
);
315 isl_qpolynomial_free(poly
);
316 isl_qpolynomial_free(sub
);
317 return signed_infty(space
, data
->sign
);
320 poly
= isl_qpolynomial_substitute(poly
, isl_dim_in
, pos
, 1, &sub
);
321 isl_qpolynomial_free(sub
);
325 isl_qpolynomial_free(poly
);
326 isl_qpolynomial_free(sub
);
330 /* Given a lower and upper bound on the final variable and constraints
331 * on the remaining variables where these bounds are active,
332 * eliminate the variable from data->poly based on these bounds.
333 * If the polynomial has been determined to be monotonic
334 * in the variable, then simply plug in the appropriate bound.
335 * If the current polynomial is tight and if this bound is integer,
336 * then the result is still tight. In all other cases, the results
338 * Otherwise, plug in the largest bound (in absolute value) in
339 * the positive terms (if an upper bound is wanted) or the negative terms
340 * (if a lower bounded is wanted) and the other bound in the other terms.
342 * If all variables have been eliminated, then record the result.
343 * Ohterwise, recurse on the next variable.
345 static isl_stat
propagate_on_bound_pair(__isl_take isl_constraint
*lower
,
346 __isl_take isl_constraint
*upper
, __isl_take isl_basic_set
*bset
,
349 struct range_data
*data
= (struct range_data
*)user
;
350 int save_tight
= data
->tight
;
351 isl_qpolynomial
*poly
;
353 isl_size nvar
, nparam
;
355 nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
356 nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
357 if (nvar
< 0 || nparam
< 0)
360 if (data
->monotonicity
) {
361 isl_qpolynomial
*sub
;
362 isl_space
*space
= isl_qpolynomial_get_domain_space(data
->poly
);
363 if (data
->monotonicity
* data
->sign
> 0) {
365 data
->tight
= bound_is_integer(upper
, nvar
);
366 sub
= bound2poly(upper
, space
, nvar
, 1);
367 isl_constraint_free(lower
);
370 data
->tight
= bound_is_integer(lower
, nvar
);
371 sub
= bound2poly(lower
, space
, nvar
, -1);
372 isl_constraint_free(upper
);
374 poly
= isl_qpolynomial_copy(data
->poly
);
375 poly
= plug_in_at_pos(poly
, nvar
, sub
, data
);
376 poly
= isl_qpolynomial_drop_dims(poly
, isl_dim_in
, nvar
, 1);
378 isl_qpolynomial
*l
, *u
;
379 isl_qpolynomial
*pos
, *neg
;
380 isl_space
*space
= isl_qpolynomial_get_domain_space(data
->poly
);
381 int sign
= data
->sign
* data
->signs
[nparam
+ nvar
];
385 u
= bound2poly(upper
, isl_space_copy(space
), nvar
, 1);
386 l
= bound2poly(lower
, space
, nvar
, -1);
388 pos
= isl_qpolynomial_terms_of_sign(data
->poly
, data
->signs
, sign
);
389 neg
= isl_qpolynomial_terms_of_sign(data
->poly
, data
->signs
, -sign
);
391 pos
= plug_in_at_pos(pos
, nvar
, u
, data
);
392 neg
= plug_in_at_pos(neg
, nvar
, l
, data
);
394 poly
= isl_qpolynomial_add(pos
, neg
);
395 poly
= isl_qpolynomial_drop_dims(poly
, isl_dim_in
, nvar
, 1);
399 r
= add_guarded_poly(bset
, poly
, data
);
401 r
= propagate_on_domain(bset
, poly
, data
);
403 data
->tight
= save_tight
;
407 isl_constraint_free(lower
);
408 isl_constraint_free(upper
);
409 isl_basic_set_free(bset
);
410 return isl_stat_error
;
413 /* Recursively perform range propagation on the polynomial "poly"
414 * defined over the basic set "bset" and collect the results in "data".
416 static isl_stat
propagate_on_domain(__isl_take isl_basic_set
*bset
,
417 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
)
421 isl_qpolynomial
*save_poly
= data
->poly
;
422 int save_monotonicity
= data
->monotonicity
;
425 d
= isl_basic_set_dim(bset
, isl_dim_set
);
426 is_cst
= isl_qpolynomial_is_cst(poly
, NULL
, NULL
);
427 if (d
< 0 || is_cst
< 0)
430 ctx
= isl_basic_set_get_ctx(bset
);
431 isl_assert(ctx
, d
>= 1, goto error
);
434 bset
= isl_basic_set_project_out(bset
, isl_dim_set
, 0, d
);
435 poly
= isl_qpolynomial_drop_dims(poly
, isl_dim_in
, 0, d
);
436 return add_guarded_poly(bset
, poly
, data
);
439 if (data
->test_monotonicity
)
440 data
->monotonicity
= monotonicity(bset
, poly
, data
);
442 data
->monotonicity
= 0;
443 if (data
->monotonicity
< -1)
447 if (isl_basic_set_foreach_bound_pair(bset
, isl_dim_set
, d
- 1,
448 &propagate_on_bound_pair
, data
) < 0)
451 isl_basic_set_free(bset
);
452 isl_qpolynomial_free(poly
);
453 data
->monotonicity
= save_monotonicity
;
454 data
->poly
= save_poly
;
458 isl_basic_set_free(bset
);
459 isl_qpolynomial_free(poly
);
460 data
->monotonicity
= save_monotonicity
;
461 data
->poly
= save_poly
;
462 return isl_stat_error
;
465 static isl_stat
basic_guarded_poly_bound(__isl_take isl_basic_set
*bset
,
468 struct range_data
*data
= (struct range_data
*)user
;
470 isl_size nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
471 isl_size dim
= isl_basic_set_dim(bset
, isl_dim_set
);
472 isl_size total
= isl_basic_set_dim(bset
, isl_dim_all
);
477 if (nparam
< 0 || dim
< 0 || total
< 0)
480 ctx
= isl_basic_set_get_ctx(bset
);
481 data
->signs
= isl_alloc_array(ctx
, int, total
);
483 if (isl_basic_set_dims_get_sign(bset
, isl_dim_set
, 0, dim
,
484 data
->signs
+ nparam
) < 0)
486 if (isl_basic_set_dims_get_sign(bset
, isl_dim_param
, 0, nparam
,
490 r
= propagate_on_domain(bset
, isl_qpolynomial_copy(data
->poly
), data
);
497 isl_basic_set_free(bset
);
498 return isl_stat_error
;
501 static isl_stat
qpolynomial_bound_on_domain_range(
502 __isl_take isl_basic_set
*bset
, __isl_take isl_qpolynomial
*poly
,
503 struct range_data
*data
)
505 isl_size nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
506 isl_size nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
509 if (nparam
< 0 || nvar
< 0)
513 return add_guarded_poly(bset
, poly
, data
);
515 set
= isl_set_from_basic_set(bset
);
516 set
= isl_set_split_dims(set
, isl_dim_param
, 0, nparam
);
517 set
= isl_set_split_dims(set
, isl_dim_set
, 0, nvar
);
521 data
->test_monotonicity
= 1;
522 if (isl_set_foreach_basic_set(set
, &basic_guarded_poly_bound
, data
) < 0)
526 isl_qpolynomial_free(poly
);
531 isl_qpolynomial_free(poly
);
532 return isl_stat_error
;
535 isl_stat
isl_qpolynomial_bound_on_domain_range(__isl_take isl_basic_set
*bset
,
536 __isl_take isl_qpolynomial
*poly
, struct isl_bound
*bound
)
538 struct range_data data
;
541 data
.pwf
= bound
->pwf
;
542 data
.pwf_tight
= bound
->pwf_tight
;
543 data
.tight
= bound
->check_tight
;
544 if (bound
->type
== isl_fold_min
)
549 r
= qpolynomial_bound_on_domain_range(bset
, poly
, &data
);
551 bound
->pwf
= data
.pwf
;
552 bound
->pwf_tight
= data
.pwf_tight
;