1 #include <isl_constraint.h>
3 #include <isl_polynomial_private.h>
8 struct isl_bound
*bound
;
11 int test_monotonicity
;
14 isl_qpolynomial
*poly
;
15 isl_pw_qpolynomial_fold
*pwf
;
16 isl_pw_qpolynomial_fold
*pwf_tight
;
19 static int propagate_on_domain(__isl_take isl_basic_set
*bset
,
20 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
);
22 /* Check whether the polynomial "poly" has sign "sign" over "bset",
23 * i.e., if sign == 1, check that the lower bound on the polynomial
24 * is non-negative and if sign == -1, check that the upper bound on
25 * the polynomial is non-positive.
27 static int has_sign(__isl_keep isl_basic_set
*bset
,
28 __isl_keep isl_qpolynomial
*poly
, int sign
, int *signs
)
30 struct range_data data_m
;
38 nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
39 nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
41 bset
= isl_basic_set_copy(bset
);
42 poly
= isl_qpolynomial_copy(poly
);
44 bset
= isl_basic_set_move_dims(bset
, isl_dim_set
, 0,
45 isl_dim_param
, 0, nparam
);
46 poly
= isl_qpolynomial_move_dims(poly
, isl_dim_set
, 0,
47 isl_dim_param
, 0, nparam
);
49 dim
= isl_qpolynomial_get_dim(poly
);
50 dim
= isl_dim_drop(dim
, isl_dim_set
, 0, isl_dim_size(dim
, isl_dim_set
));
52 data_m
.test_monotonicity
= 0;
55 type
= data_m
.sign
< 0 ? isl_fold_min
: isl_fold_max
;
56 data_m
.pwf
= isl_pw_qpolynomial_fold_zero(dim
, type
);
58 data_m
.pwf_tight
= NULL
;
60 if (propagate_on_domain(bset
, poly
, &data_m
) < 0)
64 opt
= isl_pw_qpolynomial_fold_min(data_m
.pwf
);
66 opt
= isl_pw_qpolynomial_fold_max(data_m
.pwf
);
70 else if (isl_qpolynomial_is_nan(opt
) ||
71 isl_qpolynomial_is_infty(opt
) ||
72 isl_qpolynomial_is_neginfty(opt
))
75 r
= sign
* isl_qpolynomial_sgn(opt
) >= 0;
77 isl_qpolynomial_free(opt
);
81 isl_pw_qpolynomial_fold_free(data_m
.pwf
);
85 /* Return 1 if poly is monotonically increasing in the last set variable,
86 * -1 if poly is monotonically decreasing in the last set variable,
90 * We simply check the sign of p(x+1)-p(x)
92 static int monotonicity(__isl_keep isl_basic_set
*bset
,
93 __isl_keep isl_qpolynomial
*poly
, struct range_data
*data
)
97 isl_qpolynomial
*sub
= NULL
;
98 isl_qpolynomial
*diff
= NULL
;
103 ctx
= isl_qpolynomial_get_ctx(poly
);
104 dim
= isl_qpolynomial_get_dim(poly
);
106 nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
108 sub
= isl_qpolynomial_var(isl_dim_copy(dim
), isl_dim_set
, nvar
- 1);
109 sub
= isl_qpolynomial_add(sub
,
110 isl_qpolynomial_rat_cst(dim
, ctx
->one
, ctx
->one
));
112 diff
= isl_qpolynomial_substitute(isl_qpolynomial_copy(poly
),
113 isl_dim_set
, nvar
- 1, 1, &sub
);
114 diff
= isl_qpolynomial_sub(diff
, isl_qpolynomial_copy(poly
));
116 s
= has_sign(bset
, diff
, 1, data
->signs
);
122 s
= has_sign(bset
, diff
, -1, data
->signs
);
129 isl_qpolynomial_free(diff
);
130 isl_qpolynomial_free(sub
);
134 isl_qpolynomial_free(diff
);
135 isl_qpolynomial_free(sub
);
139 static __isl_give isl_qpolynomial
*bound2poly(__isl_take isl_constraint
*bound
,
140 __isl_take isl_dim
*dim
, unsigned pos
, int sign
)
144 return isl_qpolynomial_infty(dim
);
146 return isl_qpolynomial_neginfty(dim
);
149 return isl_qpolynomial_from_constraint(bound
, isl_dim_set
, pos
);
152 static int bound_is_integer(__isl_take isl_constraint
*bound
, unsigned pos
)
161 isl_constraint_get_coefficient(bound
, isl_dim_set
, pos
, &c
);
162 is_int
= isl_int_is_one(c
) || isl_int_is_negone(c
);
168 struct isl_fixed_sign_data
{
171 isl_qpolynomial
*poly
;
174 /* Add term "term" to data->poly if it has sign data->sign.
175 * The sign is determined based on the signs of the parameters
176 * and variables in data->signs.
178 static int collect_fixed_sign_terms(__isl_take isl_term
*term
, void *user
)
180 struct isl_fixed_sign_data
*data
= (struct isl_fixed_sign_data
*)user
;
190 nparam
= isl_term_dim(term
, isl_dim_param
);
191 nvar
= isl_term_dim(term
, isl_dim_set
);
193 isl_assert(isl_term_get_ctx(term
), isl_term_dim(term
, isl_dim_div
) == 0,
199 isl_term_get_num(term
, &n
);
200 isl_term_get_den(term
, &d
);
202 sign
= isl_int_sgn(n
);
203 for (i
= 0; i
< nparam
; ++i
) {
204 if (data
->signs
[i
] > 0)
206 if (isl_term_get_exp(term
, isl_dim_param
, i
) % 2)
209 for (i
= 0; i
< nvar
; ++i
) {
210 if (data
->signs
[nparam
+ i
] > 0)
212 if (isl_term_get_exp(term
, isl_dim_set
, i
) % 2)
216 if (sign
== data
->sign
) {
217 isl_qpolynomial
*t
= isl_qpolynomial_from_term(term
);
219 data
->poly
= isl_qpolynomial_add(data
->poly
, t
);
229 /* Construct and return a polynomial that consists of the terms
230 * in "poly" that have sign "sign".
232 static __isl_give isl_qpolynomial
*fixed_sign_terms(
233 __isl_keep isl_qpolynomial
*poly
, int *signs
, int sign
)
235 struct isl_fixed_sign_data data
= { signs
, sign
};
236 data
.poly
= isl_qpolynomial_zero(isl_qpolynomial_get_dim(poly
));
238 if (isl_qpolynomial_foreach_term(poly
, collect_fixed_sign_terms
, &data
) < 0)
243 isl_qpolynomial_free(data
.poly
);
247 /* Helper function to add a guarded polynomial to either pwf_tight or pwf,
248 * depending on whether the result has been determined to be tight.
250 static int add_guarded_poly(__isl_take isl_basic_set
*bset
,
251 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
)
253 enum isl_fold type
= data
->sign
< 0 ? isl_fold_min
: isl_fold_max
;
255 isl_qpolynomial_fold
*fold
;
256 isl_pw_qpolynomial_fold
*pwf
;
258 fold
= isl_qpolynomial_fold_alloc(type
, poly
);
259 set
= isl_set_from_basic_set(bset
);
260 pwf
= isl_pw_qpolynomial_fold_alloc(type
, set
, fold
);
262 data
->pwf_tight
= isl_pw_qpolynomial_fold_fold(
263 data
->pwf_tight
, pwf
);
265 data
->pwf
= isl_pw_qpolynomial_fold_fold(data
->pwf
, pwf
);
270 /* Given a lower and upper bound on the final variable and constraints
271 * on the remaining variables where these bounds are active,
272 * eliminate the variable from data->poly based on these bounds.
273 * If the polynomial has been determined to be monotonic
274 * in the variable, then simply plug in the appropriate bound.
275 * If the current polynomial is tight and if this bound is integer,
276 * then the result is still tight. In all other cases, the results
278 * Otherwise, plug in the largest bound (in absolute value) in
279 * the positive terms (if an upper bound is wanted) or the negative terms
280 * (if a lower bounded is wanted) and the other bound in the other terms.
282 * If all variables have been eliminated, then record the result.
283 * Ohterwise, recurse on the next variable.
285 static int propagate_on_bound_pair(__isl_take isl_constraint
*lower
,
286 __isl_take isl_constraint
*upper
, __isl_take isl_basic_set
*bset
,
289 struct range_data
*data
= (struct range_data
*)user
;
290 int save_tight
= data
->tight
;
291 isl_qpolynomial
*poly
;
295 nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
297 if (data
->monotonicity
) {
298 isl_qpolynomial
*sub
;
299 isl_dim
*dim
= isl_qpolynomial_get_dim(data
->poly
);
300 if (data
->monotonicity
* data
->sign
> 0) {
302 data
->tight
= bound_is_integer(upper
, nvar
);
303 sub
= bound2poly(upper
, dim
, nvar
, 1);
304 isl_constraint_free(lower
);
307 data
->tight
= bound_is_integer(lower
, nvar
);
308 sub
= bound2poly(lower
, dim
, nvar
, -1);
309 isl_constraint_free(upper
);
311 poly
= isl_qpolynomial_copy(data
->poly
);
312 poly
= isl_qpolynomial_substitute(poly
, isl_dim_set
, nvar
, 1, &sub
);
313 poly
= isl_qpolynomial_drop_dims(poly
, isl_dim_set
, nvar
, 1);
315 isl_qpolynomial_free(sub
);
317 isl_qpolynomial
*l
, *u
;
318 isl_qpolynomial
*pos
, *neg
;
319 isl_dim
*dim
= isl_qpolynomial_get_dim(data
->poly
);
320 unsigned nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
321 int sign
= data
->sign
* data
->signs
[nparam
+ nvar
];
325 u
= bound2poly(upper
, isl_dim_copy(dim
), nvar
, 1);
326 l
= bound2poly(lower
, dim
, nvar
, -1);
328 pos
= fixed_sign_terms(data
->poly
, data
->signs
, sign
);
329 neg
= fixed_sign_terms(data
->poly
, data
->signs
, -sign
);
331 pos
= isl_qpolynomial_substitute(pos
, isl_dim_set
, nvar
, 1, &u
);
332 neg
= isl_qpolynomial_substitute(neg
, isl_dim_set
, nvar
, 1, &l
);
334 poly
= isl_qpolynomial_add(pos
, neg
);
335 poly
= isl_qpolynomial_drop_dims(poly
, isl_dim_set
, nvar
, 1);
337 isl_qpolynomial_free(u
);
338 isl_qpolynomial_free(l
);
341 if (isl_basic_set_dim(bset
, isl_dim_set
) == 0)
342 r
= add_guarded_poly(bset
, poly
, data
);
344 r
= propagate_on_domain(bset
, poly
, data
);
346 data
->tight
= save_tight
;
351 /* Recursively perform range propagation on the polynomial "poly"
352 * defined over the basic set "bset" and collect the results in "data".
354 static int propagate_on_domain(__isl_take isl_basic_set
*bset
,
355 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
)
357 isl_qpolynomial
*save_poly
= data
->poly
;
358 int save_monotonicity
= data
->monotonicity
;
364 d
= isl_basic_set_dim(bset
, isl_dim_set
);
365 isl_assert(bset
->ctx
, d
>= 1, goto error
);
367 if (isl_qpolynomial_is_cst(poly
, NULL
, NULL
)) {
368 bset
= isl_basic_set_project_out(bset
, isl_dim_set
, 0, d
);
369 poly
= isl_qpolynomial_drop_dims(poly
, isl_dim_set
, 0, d
);
370 return add_guarded_poly(bset
, poly
, data
);
373 if (data
->test_monotonicity
)
374 data
->monotonicity
= monotonicity(bset
, poly
, data
);
376 data
->monotonicity
= 0;
377 if (data
->monotonicity
< -1)
381 if (isl_basic_set_foreach_bound_pair(bset
, isl_dim_set
, d
- 1,
382 &propagate_on_bound_pair
, data
) < 0)
385 isl_basic_set_free(bset
);
386 isl_qpolynomial_free(poly
);
387 data
->monotonicity
= save_monotonicity
;
388 data
->poly
= save_poly
;
392 isl_basic_set_free(bset
);
393 isl_qpolynomial_free(poly
);
394 data
->monotonicity
= save_monotonicity
;
395 data
->poly
= save_poly
;
399 static int basic_guarded_poly_bound(__isl_take isl_basic_set
*bset
, void *user
)
401 struct range_data
*data
= (struct range_data
*)user
;
402 unsigned nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
403 unsigned dim
= isl_basic_set_dim(bset
, isl_dim_set
);
408 data
->signs
= isl_alloc_array(bset
->ctx
, int,
409 isl_basic_set_dim(bset
, isl_dim_all
));
411 if (isl_basic_set_dims_get_sign(bset
, isl_dim_set
, 0, dim
,
412 data
->signs
+ nparam
) < 0)
414 if (isl_basic_set_dims_get_sign(bset
, isl_dim_param
, 0, nparam
,
418 r
= propagate_on_domain(bset
, isl_qpolynomial_copy(data
->poly
), data
);
425 isl_basic_set_free(bset
);
429 static int qpolynomial_bound_on_domain_range(__isl_take isl_basic_set
*bset
,
430 __isl_take isl_qpolynomial
*poly
, struct range_data
*data
)
432 unsigned nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
433 unsigned nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
440 return add_guarded_poly(bset
, poly
, data
);
442 set
= isl_set_from_basic_set(bset
);
443 set
= isl_set_split_dims(set
, isl_dim_param
, 0, nparam
);
444 set
= isl_set_split_dims(set
, isl_dim_set
, 0, nvar
);
448 data
->test_monotonicity
= 1;
449 if (isl_set_foreach_basic_set(set
, &basic_guarded_poly_bound
, data
) < 0)
453 isl_qpolynomial_free(poly
);
458 isl_qpolynomial_free(poly
);
462 int isl_qpolynomial_bound_on_domain_range(__isl_take isl_basic_set
*bset
,
463 __isl_take isl_qpolynomial
*poly
, struct isl_bound
*bound
)
465 struct range_data data
;
468 data
.pwf
= bound
->pwf
;
469 data
.pwf_tight
= bound
->pwf_tight
;
470 data
.tight
= bound
->check_tight
;
471 if (bound
->type
== isl_fold_min
)
476 r
= qpolynomial_bound_on_domain_range(bset
, poly
, &data
);
478 bound
->pwf
= data
.pwf
;
479 bound
->pwf_tight
= data
.pwf_tight
;