isl_basic_map_gist: allow existentially quantified variables
[isl.git] / isl_box.c
blobc674af0d376234c48e522a6c4302db220aad82b9
1 /*
2 * Copyright 2010-2011 INRIA Saclay
3 * Copyright 2012-2013 Ecole Normale Superieure
5 * Use of this software is governed by the MIT license
7 * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
8 * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
9 * 91893 Orsay, France
10 * and Ecole Normale Superieure, 45 rue d'Ulm, 75230 Paris, France
13 #include <isl/val.h>
14 #include <isl/space.h>
15 #include <isl_map_private.h>
16 #include <isl_aff_private.h>
17 #include <isl/constraint.h>
18 #include <isl/ilp.h>
19 #include <isl/fixed_box.h>
20 #include <isl/stream.h>
22 /* Representation of a box of fixed size containing the elements
23 * [offset, offset + size).
24 * "size" lives in the target space of "offset".
26 * If any of the "offsets" is NaN, then the object represents
27 * the failure of finding a fixed-size box.
29 struct isl_fixed_box {
30 isl_multi_aff *offset;
31 isl_multi_val *size;
34 /* Free "box" and return NULL.
36 __isl_null isl_fixed_box *isl_fixed_box_free(__isl_take isl_fixed_box *box)
38 if (!box)
39 return NULL;
40 isl_multi_aff_free(box->offset);
41 isl_multi_val_free(box->size);
42 free(box);
43 return NULL;
46 /* Construct an isl_fixed_box with the given offset and size.
48 static __isl_give isl_fixed_box *isl_fixed_box_alloc(
49 __isl_take isl_multi_aff *offset, __isl_take isl_multi_val *size)
51 isl_ctx *ctx;
52 isl_fixed_box *box;
54 if (!offset || !size)
55 goto error;
56 ctx = isl_multi_aff_get_ctx(offset);
57 box = isl_alloc_type(ctx, struct isl_fixed_box);
58 if (!box)
59 goto error;
60 box->offset = offset;
61 box->size = size;
63 return box;
64 error:
65 isl_multi_aff_free(offset);
66 isl_multi_val_free(size);
67 return NULL;
70 /* Construct an initial isl_fixed_box with zero offsets
71 * in the given space and zero corresponding sizes.
73 static __isl_give isl_fixed_box *isl_fixed_box_init(
74 __isl_take isl_space *space)
76 isl_multi_aff *offset;
77 isl_multi_val *size;
79 offset = isl_multi_aff_zero(isl_space_copy(space));
80 space = isl_space_drop_all_params(isl_space_range(space));
81 size = isl_multi_val_zero(space);
82 return isl_fixed_box_alloc(offset, size);
85 /* Return a copy of "box".
87 __isl_give isl_fixed_box *isl_fixed_box_copy(__isl_keep isl_fixed_box *box)
89 isl_multi_aff *offset;
90 isl_multi_val *size;
92 offset = isl_fixed_box_get_offset(box);
93 size = isl_fixed_box_get_size(box);
94 return isl_fixed_box_alloc(offset, size);
97 /* Replace the offset and size in direction "pos" by "offset" and "size"
98 * (without checking whether "box" is a valid box).
100 static __isl_give isl_fixed_box *isl_fixed_box_set_extent(
101 __isl_take isl_fixed_box *box, int pos, __isl_keep isl_aff *offset,
102 __isl_keep isl_val *size)
104 if (!box)
105 return NULL;
106 box->offset = isl_multi_aff_set_aff(box->offset, pos,
107 isl_aff_copy(offset));
108 box->size = isl_multi_val_set_val(box->size, pos, isl_val_copy(size));
109 if (!box->offset || !box->size)
110 return isl_fixed_box_free(box);
111 return box;
114 /* Replace the offset and size in direction "pos" by "offset" and "size",
115 * if "box" is a valid box.
117 static __isl_give isl_fixed_box *isl_fixed_box_set_valid_extent(
118 __isl_take isl_fixed_box *box, int pos, __isl_keep isl_aff *offset,
119 __isl_keep isl_val *size)
121 isl_bool valid;
123 valid = isl_fixed_box_is_valid(box);
124 if (valid < 0 || !valid)
125 return box;
126 return isl_fixed_box_set_extent(box, pos, offset, size);
129 /* Replace "box" by an invalid box, by setting all offsets to NaN
130 * (and all sizes to infinity).
132 static __isl_give isl_fixed_box *isl_fixed_box_invalidate(
133 __isl_take isl_fixed_box *box)
135 int i;
136 isl_size n;
137 isl_space *space;
138 isl_val *infty;
139 isl_aff *nan;
141 if (!box)
142 return NULL;
143 n = isl_multi_val_dim(box->size, isl_dim_set);
144 if (n < 0)
145 return isl_fixed_box_free(box);
147 infty = isl_val_infty(isl_fixed_box_get_ctx(box));
148 space = isl_space_domain(isl_fixed_box_get_space(box));
149 nan = isl_aff_nan_on_domain(isl_local_space_from_space(space));
150 for (i = 0; i < n; ++i)
151 box = isl_fixed_box_set_extent(box, i, nan, infty);
152 isl_aff_free(nan);
153 isl_val_free(infty);
155 if (!box->offset || !box->size)
156 return isl_fixed_box_free(box);
157 return box;
160 /* Project the domain of the fixed box onto its parameter space.
161 * In particular, project out the domain of the offset.
163 static __isl_give isl_fixed_box *isl_fixed_box_project_domain_on_params(
164 __isl_take isl_fixed_box *box)
166 isl_bool valid;
168 valid = isl_fixed_box_is_valid(box);
169 if (valid < 0)
170 return isl_fixed_box_free(box);
171 if (!valid)
172 return box;
174 box->offset = isl_multi_aff_project_domain_on_params(box->offset);
175 if (!box->offset)
176 return isl_fixed_box_free(box);
178 return box;
181 /* Return the isl_ctx to which "box" belongs.
183 isl_ctx *isl_fixed_box_get_ctx(__isl_keep isl_fixed_box *box)
185 if (!box)
186 return NULL;
187 return isl_multi_aff_get_ctx(box->offset);
190 /* Return the space in which "box" lives.
192 __isl_give isl_space *isl_fixed_box_get_space(__isl_keep isl_fixed_box *box)
194 if (!box)
195 return NULL;
196 return isl_multi_aff_get_space(box->offset);
199 /* Does "box" contain valid information?
201 isl_bool isl_fixed_box_is_valid(__isl_keep isl_fixed_box *box)
203 if (!box)
204 return isl_bool_error;
205 return isl_bool_not(isl_multi_aff_involves_nan(box->offset));
208 /* Return the offsets of the box "box".
210 __isl_give isl_multi_aff *isl_fixed_box_get_offset(
211 __isl_keep isl_fixed_box *box)
213 if (!box)
214 return NULL;
215 return isl_multi_aff_copy(box->offset);
218 /* Return the sizes of the box "box".
220 __isl_give isl_multi_val *isl_fixed_box_get_size(__isl_keep isl_fixed_box *box)
222 if (!box)
223 return NULL;
224 return isl_multi_val_copy(box->size);
227 /* Data used in set_dim_extent and compute_size_in_direction.
229 * "bset" is a wrapped copy of the basic map that has the selected
230 * output dimension as range.
231 * "pos" is the position of the variable representing the output dimension,
232 * i.e., the variable for which the size should be computed. This variable
233 * is also the last variable in "bset".
234 * "size" is the best size found so far
235 * (infinity if no offset was found so far).
236 * "offset" is the offset corresponding to the best size
237 * (NULL if no offset was found so far).
239 struct isl_size_info {
240 isl_basic_set *bset;
241 isl_size pos;
242 isl_val *size;
243 isl_aff *offset;
246 /* Is "c" a suitable bound on dimension "pos" for use as a lower bound
247 * of a fixed-size range.
248 * In particular, it needs to be a lower bound on "pos".
249 * In order for the final offset not to be too complicated,
250 * the constraint itself should also not involve any integer divisions.
252 static isl_bool is_suitable_bound(__isl_keep isl_constraint *c, unsigned pos)
254 isl_size n_div;
255 isl_bool is_bound, any_divs;
257 is_bound = isl_constraint_is_lower_bound(c, isl_dim_set, pos);
258 if (is_bound < 0 || !is_bound)
259 return is_bound;
261 n_div = isl_constraint_dim(c, isl_dim_div);
262 if (n_div < 0)
263 return isl_bool_error;
264 any_divs = isl_constraint_involves_dims(c, isl_dim_div, 0, n_div);
265 return isl_bool_not(any_divs);
268 /* Given a constraint from the basic set describing the bounds on
269 * an array index, check if it is a lower bound, say m i >= b(x), and,
270 * if so, check whether the expression "i - ceil(b(x)/m) + 1" has a constant
271 * upper bound. If so, and if this bound is smaller than any bound
272 * derived from earlier constraints, set the size to this bound on
273 * the expression and the lower bound to ceil(b(x)/m).
275 static isl_stat compute_size_in_direction(__isl_take isl_constraint *c,
276 void *user)
278 struct isl_size_info *info = user;
279 isl_val *v;
280 isl_aff *aff;
281 isl_aff *lb;
282 isl_bool is_bound, better;
284 is_bound = is_suitable_bound(c, info->pos);
285 if (is_bound < 0 || !is_bound) {
286 isl_constraint_free(c);
287 return is_bound < 0 ? isl_stat_error : isl_stat_ok;
290 aff = isl_constraint_get_bound(c, isl_dim_set, info->pos);
291 aff = isl_aff_ceil(aff);
293 lb = isl_aff_copy(aff);
295 aff = isl_aff_neg(aff);
296 aff = isl_aff_add_coefficient_si(aff, isl_dim_in, info->pos, 1);
298 v = isl_basic_set_max_val(info->bset, aff);
299 isl_aff_free(aff);
301 v = isl_val_add_ui(v, 1);
302 better = isl_val_lt(v, info->size);
303 if (better >= 0 && better) {
304 isl_val_free(info->size);
305 info->size = isl_val_copy(v);
306 lb = isl_aff_domain_factor_domain(lb);
307 isl_aff_free(info->offset);
308 info->offset = isl_aff_copy(lb);
310 isl_val_free(v);
311 isl_aff_free(lb);
313 isl_constraint_free(c);
315 return better < 0 ? isl_stat_error : isl_stat_ok;
318 /* Look for a fixed-size range of values for the output dimension "pos"
319 * of "map", by looking for a lower-bound expression in the parameters
320 * and input dimensions such that the range of the output dimension
321 * is a constant shifted by this expression.
323 * In particular, look through the explicit lower bounds on the output dimension
324 * for candidate expressions and pick the one that results in the smallest size.
325 * Initialize the size with infinity and if no better size is found
326 * then invalidate the box. Otherwise, set the offset and size
327 * in the given direction by those that correspond to the smallest size.
329 * Note that while evaluating the size corresponding to a lower bound,
330 * an affine expression is constructed from the lower bound.
331 * This lower bound may therefore not have any unknown local variables.
332 * Eliminate any unknown local variables up front.
333 * No such restriction needs to be imposed on the set over which
334 * the size is computed.
336 static __isl_give isl_fixed_box *set_dim_extent(__isl_take isl_fixed_box *box,
337 __isl_keep isl_map *map, int pos)
339 struct isl_size_info info;
340 isl_bool valid;
341 isl_ctx *ctx;
342 isl_basic_set *bset;
344 if (!box || !map)
345 return isl_fixed_box_free(box);
347 ctx = isl_map_get_ctx(map);
348 map = isl_map_copy(map);
349 map = isl_map_project_onto(map, isl_dim_out, pos, 1);
350 info.size = isl_val_infty(ctx);
351 info.offset = NULL;
352 info.pos = isl_map_dim(map, isl_dim_in);
353 info.bset = isl_basic_map_wrap(isl_map_simple_hull(map));
354 bset = isl_basic_set_copy(info.bset);
355 bset = isl_basic_set_remove_unknown_divs(bset);
356 if (info.pos < 0)
357 bset = isl_basic_set_free(bset);
358 if (isl_basic_set_foreach_constraint(bset,
359 &compute_size_in_direction, &info) < 0)
360 box = isl_fixed_box_free(box);
361 isl_basic_set_free(bset);
362 valid = isl_val_is_int(info.size);
363 if (valid < 0)
364 box = isl_fixed_box_free(box);
365 else if (valid)
366 box = isl_fixed_box_set_valid_extent(box, pos,
367 info.offset, info.size);
368 else
369 box = isl_fixed_box_invalidate(box);
370 isl_val_free(info.size);
371 isl_aff_free(info.offset);
372 isl_basic_set_free(info.bset);
374 return box;
377 /* Try and construct a fixed-size rectangular box with an offset
378 * in terms of the domain of "map" that contains the range of "map".
379 * If no such box can be constructed, then return an invalidated box,
380 * i.e., one where isl_fixed_box_is_valid returns false.
382 * Iterate over the dimensions in the range
383 * setting the corresponding offset and extent.
385 __isl_give isl_fixed_box *isl_map_get_range_simple_fixed_box_hull(
386 __isl_keep isl_map *map)
388 int i;
389 isl_size n;
390 isl_space *space;
391 isl_fixed_box *box;
393 n = isl_map_dim(map, isl_dim_out);
394 if (n < 0)
395 return NULL;
396 space = isl_map_get_space(map);
397 box = isl_fixed_box_init(space);
399 map = isl_map_detect_equalities(isl_map_copy(map));
400 for (i = 0; i < n; ++i) {
401 isl_bool valid;
403 box = set_dim_extent(box, map, i);
404 valid = isl_fixed_box_is_valid(box);
405 if (valid < 0 || !valid)
406 break;
408 isl_map_free(map);
410 return box;
413 /* Compute a fixed box from "set" using "map_box" by treating it as a map
414 * with a zero-dimensional domain and
415 * project out the domain again from the result.
417 static __isl_give isl_fixed_box *fixed_box_as_map(__isl_keep isl_set *set,
418 __isl_give isl_fixed_box *(*map_box)(__isl_keep isl_map *map))
420 isl_map *map;
421 isl_fixed_box *box;
423 map = isl_map_from_range(isl_set_copy(set));
424 box = map_box(map);
425 isl_map_free(map);
426 box = isl_fixed_box_project_domain_on_params(box);
428 return box;
431 /* Try and construct a fixed-size rectangular box with an offset
432 * in terms of the parameters of "set" that contains "set".
433 * If no such box can be constructed, then return an invalidated box,
434 * i.e., one where isl_fixed_box_is_valid returns false.
436 * Compute the box using isl_map_get_range_simple_fixed_box_hull
437 * by constructing a map from the set and
438 * project out the domain again from the result.
440 __isl_give isl_fixed_box *isl_set_get_simple_fixed_box_hull(
441 __isl_keep isl_set *set)
443 return fixed_box_as_map(set, &isl_map_get_range_simple_fixed_box_hull);
446 /* Check whether the output elements lie on a rectangular lattice,
447 * possibly depending on the parameters and the input dimensions.
448 * Return a tile in this lattice.
449 * If no stride information can be found, then return a tile of size 1
450 * (and offset 0).
452 * Obtain stride information in each output dimension separately and
453 * combine the results.
455 __isl_give isl_fixed_box *isl_map_get_range_lattice_tile(
456 __isl_keep isl_map *map)
458 int i;
459 isl_size n;
460 isl_space *space;
461 isl_fixed_box *box;
463 n = isl_map_dim(map, isl_dim_out);
464 if (n < 0)
465 return NULL;
466 space = isl_map_get_space(map);
467 box = isl_fixed_box_init(space);
469 for (i = 0; i < n; ++i) {
470 isl_val *stride;
471 isl_aff *offset;
472 isl_stride_info *si;
474 si = isl_map_get_range_stride_info(map, i);
475 stride = isl_stride_info_get_stride(si);
476 offset = isl_stride_info_get_offset(si);
477 isl_stride_info_free(si);
479 box = isl_fixed_box_set_valid_extent(box, i, offset, stride);
481 isl_aff_free(offset);
482 isl_val_free(stride);
485 return box;
488 /* Check whether the elements lie on a rectangular lattice,
489 * possibly depending on the parameters.
490 * Return a tile in this lattice.
491 * If no stride information can be found, then return a tile of size 1
492 * (and offset 0).
494 * Consider the set as a map with a zero-dimensional domain and
495 * obtain a lattice tile of that map.
497 __isl_give isl_fixed_box *isl_set_get_lattice_tile(__isl_keep isl_set *set)
499 return fixed_box_as_map(set, &isl_map_get_range_lattice_tile);
502 /* An enumeration of the keys that may appear in a YAML mapping
503 * of an isl_fixed_box object.
505 enum isl_fb_key {
506 isl_fb_key_error = -1,
507 isl_fb_key_offset,
508 isl_fb_key_size,
509 isl_fb_key_end,
512 /* Textual representations of the YAML keys for an isl_fixed_box object.
514 static char *key_str[] = {
515 [isl_fb_key_offset] = "offset",
516 [isl_fb_key_size] = "size",
519 #undef BASE
520 #define BASE multi_val
521 #include "print_yaml_field_templ.c"
523 #undef BASE
524 #define BASE multi_aff
525 #include "print_yaml_field_templ.c"
527 /* Print the information contained in "box" to "p".
528 * The information is printed as a YAML document.
530 __isl_give isl_printer *isl_printer_print_fixed_box(
531 __isl_take isl_printer *p, __isl_keep isl_fixed_box *box)
533 if (!box)
534 return isl_printer_free(p);
536 p = isl_printer_yaml_start_mapping(p);
537 p = print_yaml_field_multi_aff(p, key_str[isl_fb_key_offset],
538 box->offset);
539 p = print_yaml_field_multi_val(p, key_str[isl_fb_key_size], box->size);
540 p = isl_printer_yaml_end_mapping(p);
542 return p;
545 #undef BASE
546 #define BASE fixed_box
547 #include <print_templ_yaml.c>
549 #undef KEY
550 #define KEY enum isl_fb_key
551 #undef KEY_ERROR
552 #define KEY_ERROR isl_fb_key_error
553 #undef KEY_END
554 #define KEY_END isl_fb_key_end
555 #undef KEY_STR
556 #define KEY_STR key_str
557 #undef KEY_EXTRACT
558 #define KEY_EXTRACT extract_key
559 #undef KEY_GET
560 #define KEY_GET get_key
561 #include "extract_key.c"
563 #undef BASE
564 #define BASE multi_val
565 #include "read_in_string_templ.c"
567 #undef BASE
568 #define BASE multi_aff
569 #include "read_in_string_templ.c"
571 /* Read an isl_fixed_box object from "s".
573 * The input needs to contain both an offset and a size.
574 * If either is specified multiple times, then the last specification
575 * overrides all previous ones. This is simpler than checking
576 * that each is only specified once.
578 static __isl_give isl_fixed_box *isl_stream_read_fixed_box(isl_stream *s)
580 isl_bool more;
581 isl_multi_aff *offset = NULL;
582 isl_multi_val *size = NULL;
584 if (isl_stream_yaml_read_start_mapping(s) < 0)
585 return NULL;
587 while ((more = isl_stream_yaml_next(s)) == isl_bool_true) {
588 enum isl_fb_key key;
590 key = get_key(s);
591 if (isl_stream_yaml_next(s) < 0)
592 goto error;
593 switch (key) {
594 case isl_fb_key_end:
595 case isl_fb_key_error:
596 goto error;
597 case isl_fb_key_offset:
598 isl_multi_aff_free(offset);
599 offset = read_multi_aff(s);
600 if (!offset)
601 goto error;
602 break;
603 case isl_fb_key_size:
604 isl_multi_val_free(size);
605 size = read_multi_val(s);
606 if (!size)
607 goto error;
608 break;
611 if (more < 0)
612 goto error;
614 if (isl_stream_yaml_read_end_mapping(s) < 0)
615 goto error;
617 if (!offset) {
618 isl_stream_error(s, NULL, "no offset specified");
619 goto error;
622 if (!size) {
623 isl_stream_error(s, NULL, "no size specified");
624 goto error;
627 return isl_fixed_box_alloc(offset, size);
628 error:
629 isl_multi_aff_free(offset);
630 isl_multi_val_free(size);
631 return NULL;
634 #undef TYPE_BASE
635 #define TYPE_BASE fixed_box
636 #include "isl_read_from_str_templ.c"