2 * Copyright 2008-2009 Katholieke Universiteit Leuven
4 * Use of this software is governed by the GNU LGPLv2.1 license
6 * Written by Sven Verdoolaege, K.U.Leuven, Departement
7 * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
15 #include <isl_constraint.h>
19 void test_read(struct isl_ctx *ctx)
21 char filename[PATH_MAX];
24 struct isl_basic_set *bset1, *bset2;
25 const char *str = "{[y]: Exists ( alpha : 2alpha = y)}";
27 n = snprintf(filename, sizeof(filename),
28 "%s/test_inputs/set.omega", srcdir);
29 assert(n < sizeof(filename));
30 input = fopen(filename, "r");
33 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
34 bset2 = isl_basic_set_read_from_str(ctx, str, 0);
36 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
38 isl_basic_set_free(bset1);
39 isl_basic_set_free(bset2);
44 /* Construct the basic set { [i] : 5 <= i <= N } */
45 void test_construction(struct isl_ctx *ctx)
49 struct isl_basic_set *bset;
50 struct isl_constraint *c;
54 dim = isl_dim_set_alloc(ctx, 1, 1);
55 bset = isl_basic_set_universe(dim);
57 c = isl_inequality_alloc(isl_dim_copy(bset->dim));
58 isl_int_set_si(v, -1);
59 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
61 isl_constraint_set_coefficient(c, isl_dim_param, 0, v);
62 bset = isl_basic_set_add_constraint(bset, c);
64 c = isl_inequality_alloc(isl_dim_copy(bset->dim));
66 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
67 isl_int_set_si(v, -5);
68 isl_constraint_set_constant(c, v);
69 bset = isl_basic_set_add_constraint(bset, c);
71 isl_basic_set_free(bset);
76 void test_dim(struct isl_ctx *ctx)
80 map1 = isl_map_read_from_str(ctx,
81 "[n] -> { [i] -> [j] : exists (a = [i/10] : i - 10a <= n ) }", -1);
82 map1 = isl_map_add(map1, isl_dim_in, 1);
83 map2 = isl_map_read_from_str(ctx,
84 "[n] -> { [i,k] -> [j] : exists (a = [i/10] : i - 10a <= n ) }", -1);
85 assert(isl_map_is_equal(map1, map2));
88 map1 = isl_map_project_out(map1, isl_dim_in, 0, 1);
89 map2 = isl_map_read_from_str(ctx, "[n] -> { [i] -> [j] : n >= 0 }", -1);
90 assert(isl_map_is_equal(map1, map2));
96 void test_div(struct isl_ctx *ctx)
102 struct isl_basic_set *bset;
103 struct isl_constraint *c;
108 dim = isl_dim_set_alloc(ctx, 0, 1);
109 bset = isl_basic_set_universe(dim);
111 c = isl_equality_alloc(isl_dim_copy(bset->dim));
112 isl_int_set_si(v, -1);
113 isl_constraint_set_constant(c, v);
114 isl_int_set_si(v, 1);
115 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
116 div = isl_div_alloc(isl_dim_copy(bset->dim));
117 c = isl_constraint_add_div(c, div, &pos);
118 isl_int_set_si(v, 3);
119 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
120 bset = isl_basic_set_add_constraint(bset, c);
122 c = isl_equality_alloc(isl_dim_copy(bset->dim));
123 isl_int_set_si(v, 1);
124 isl_constraint_set_constant(c, v);
125 isl_int_set_si(v, -1);
126 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
127 div = isl_div_alloc(isl_dim_copy(bset->dim));
128 c = isl_constraint_add_div(c, div, &pos);
129 isl_int_set_si(v, 3);
130 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
131 bset = isl_basic_set_add_constraint(bset, c);
133 assert(bset->n_div == 1);
134 isl_basic_set_free(bset);
137 dim = isl_dim_set_alloc(ctx, 0, 1);
138 bset = isl_basic_set_universe(dim);
140 c = isl_equality_alloc(isl_dim_copy(bset->dim));
141 isl_int_set_si(v, 1);
142 isl_constraint_set_constant(c, v);
143 isl_int_set_si(v, -1);
144 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
145 div = isl_div_alloc(isl_dim_copy(bset->dim));
146 c = isl_constraint_add_div(c, div, &pos);
147 isl_int_set_si(v, 3);
148 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
149 bset = isl_basic_set_add_constraint(bset, c);
151 c = isl_equality_alloc(isl_dim_copy(bset->dim));
152 isl_int_set_si(v, -1);
153 isl_constraint_set_constant(c, v);
154 isl_int_set_si(v, 1);
155 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
156 div = isl_div_alloc(isl_dim_copy(bset->dim));
157 c = isl_constraint_add_div(c, div, &pos);
158 isl_int_set_si(v, 3);
159 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
160 bset = isl_basic_set_add_constraint(bset, c);
162 assert(bset->n_div == 1);
163 isl_basic_set_free(bset);
166 dim = isl_dim_set_alloc(ctx, 0, 1);
167 bset = isl_basic_set_universe(dim);
169 c = isl_equality_alloc(isl_dim_copy(bset->dim));
170 isl_int_set_si(v, 1);
171 isl_constraint_set_constant(c, v);
172 isl_int_set_si(v, -1);
173 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
174 div = isl_div_alloc(isl_dim_copy(bset->dim));
175 c = isl_constraint_add_div(c, div, &pos);
176 isl_int_set_si(v, 3);
177 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
178 bset = isl_basic_set_add_constraint(bset, c);
180 c = isl_equality_alloc(isl_dim_copy(bset->dim));
181 isl_int_set_si(v, -3);
182 isl_constraint_set_constant(c, v);
183 isl_int_set_si(v, 1);
184 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
185 div = isl_div_alloc(isl_dim_copy(bset->dim));
186 c = isl_constraint_add_div(c, div, &pos);
187 isl_int_set_si(v, 4);
188 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
189 bset = isl_basic_set_add_constraint(bset, c);
191 assert(bset->n_div == 1);
192 isl_basic_set_free(bset);
195 dim = isl_dim_set_alloc(ctx, 0, 1);
196 bset = isl_basic_set_universe(dim);
198 c = isl_equality_alloc(isl_dim_copy(bset->dim));
199 isl_int_set_si(v, 2);
200 isl_constraint_set_constant(c, v);
201 isl_int_set_si(v, -1);
202 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
203 div = isl_div_alloc(isl_dim_copy(bset->dim));
204 c = isl_constraint_add_div(c, div, &pos);
205 isl_int_set_si(v, 3);
206 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
207 bset = isl_basic_set_add_constraint(bset, c);
209 c = isl_equality_alloc(isl_dim_copy(bset->dim));
210 isl_int_set_si(v, -1);
211 isl_constraint_set_constant(c, v);
212 isl_int_set_si(v, 1);
213 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
214 div = isl_div_alloc(isl_dim_copy(bset->dim));
215 c = isl_constraint_add_div(c, div, &pos);
216 isl_int_set_si(v, 6);
217 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
218 bset = isl_basic_set_add_constraint(bset, c);
220 assert(isl_basic_set_is_empty(bset));
221 isl_basic_set_free(bset);
224 dim = isl_dim_set_alloc(ctx, 0, 2);
225 bset = isl_basic_set_universe(dim);
227 c = isl_equality_alloc(isl_dim_copy(bset->dim));
228 isl_int_set_si(v, -1);
229 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
230 div = isl_div_alloc(isl_dim_copy(bset->dim));
231 c = isl_constraint_add_div(c, div, &pos);
232 isl_int_set_si(v, 3);
233 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
234 bset = isl_basic_set_add_constraint(bset, c);
236 c = isl_equality_alloc(isl_dim_copy(bset->dim));
237 isl_int_set_si(v, 1);
238 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
239 isl_int_set_si(v, -3);
240 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
241 bset = isl_basic_set_add_constraint(bset, c);
243 assert(bset->n_div == 0);
244 isl_basic_set_free(bset);
247 dim = isl_dim_set_alloc(ctx, 0, 2);
248 bset = isl_basic_set_universe(dim);
250 c = isl_equality_alloc(isl_dim_copy(bset->dim));
251 isl_int_set_si(v, -1);
252 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
253 div = isl_div_alloc(isl_dim_copy(bset->dim));
254 c = isl_constraint_add_div(c, div, &pos);
255 isl_int_set_si(v, 6);
256 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
257 bset = isl_basic_set_add_constraint(bset, c);
259 c = isl_equality_alloc(isl_dim_copy(bset->dim));
260 isl_int_set_si(v, 1);
261 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
262 isl_int_set_si(v, -3);
263 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
264 bset = isl_basic_set_add_constraint(bset, c);
266 assert(bset->n_div == 1);
267 isl_basic_set_free(bset);
270 /* This test is a bit tricky. We set up an equality
272 * Normalization of divs creates _two_ divs
275 * Afterwards e0 is removed again because it has coefficient -1
276 * and we end up with the original equality and div again.
277 * Perhaps we can avoid the introduction of this temporary div.
279 dim = isl_dim_set_alloc(ctx, 0, 3);
280 bset = isl_basic_set_universe(dim);
282 c = isl_equality_alloc(isl_dim_copy(bset->dim));
283 isl_int_set_si(v, -1);
284 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
285 isl_int_set_si(v, -3);
286 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
287 isl_int_set_si(v, -3);
288 isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
289 div = isl_div_alloc(isl_dim_copy(bset->dim));
290 c = isl_constraint_add_div(c, div, &pos);
291 isl_int_set_si(v, 6);
292 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
293 bset = isl_basic_set_add_constraint(bset, c);
295 assert(bset->n_div == 1);
296 isl_basic_set_free(bset);
299 dim = isl_dim_set_alloc(ctx, 0, 4);
300 bset = isl_basic_set_universe(dim);
302 c = isl_equality_alloc(isl_dim_copy(bset->dim));
303 isl_int_set_si(v, -1);
304 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
305 isl_int_set_si(v, -3);
306 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
307 isl_int_set_si(v, -3);
308 isl_constraint_set_coefficient(c, isl_dim_set, 3, v);
309 div = isl_div_alloc(isl_dim_copy(bset->dim));
310 c = isl_constraint_add_div(c, div, &pos);
311 isl_int_set_si(v, 6);
312 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
313 bset = isl_basic_set_add_constraint(bset, c);
315 c = isl_equality_alloc(isl_dim_copy(bset->dim));
316 isl_int_set_si(v, -1);
317 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
318 isl_int_set_si(v, 1);
319 isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
320 isl_int_set_si(v, 1);
321 isl_constraint_set_constant(c, v);
322 bset = isl_basic_set_add_constraint(bset, c);
324 assert(bset->n_div == 1);
325 isl_basic_set_free(bset);
328 dim = isl_dim_set_alloc(ctx, 0, 2);
329 bset = isl_basic_set_universe(dim);
331 c = isl_equality_alloc(isl_dim_copy(bset->dim));
332 isl_int_set_si(v, 1);
333 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
334 isl_int_set_si(v, -1);
335 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
336 div = isl_div_alloc(isl_dim_copy(bset->dim));
337 c = isl_constraint_add_div(c, div, &pos);
338 isl_int_set_si(v, -2);
339 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
340 bset = isl_basic_set_add_constraint(bset, c);
342 c = isl_equality_alloc(isl_dim_copy(bset->dim));
343 isl_int_set_si(v, -1);
344 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
345 div = isl_div_alloc(isl_dim_copy(bset->dim));
346 c = isl_constraint_add_div(c, div, &pos);
347 isl_int_set_si(v, 3);
348 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
349 isl_int_set_si(v, 2);
350 isl_constraint_set_constant(c, v);
351 bset = isl_basic_set_add_constraint(bset, c);
353 bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
355 assert(!isl_basic_set_is_empty(bset));
357 isl_basic_set_free(bset);
360 dim = isl_dim_set_alloc(ctx, 0, 2);
361 bset = isl_basic_set_universe(dim);
363 c = isl_equality_alloc(isl_dim_copy(bset->dim));
364 isl_int_set_si(v, 1);
365 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
366 div = isl_div_alloc(isl_dim_copy(bset->dim));
367 c = isl_constraint_add_div(c, div, &pos);
368 isl_int_set_si(v, -2);
369 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
370 bset = isl_basic_set_add_constraint(bset, c);
372 bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
374 isl_basic_set_free(bset);
379 void test_application_case(struct isl_ctx *ctx, const char *name)
381 char filename[PATH_MAX];
384 struct isl_basic_set *bset1, *bset2;
385 struct isl_basic_map *bmap;
387 n = snprintf(filename, sizeof(filename),
388 "%s/test_inputs/%s.omega", srcdir, name);
389 assert(n < sizeof(filename));
390 input = fopen(filename, "r");
393 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
394 bmap = isl_basic_map_read_from_file(ctx, input, 0);
396 bset1 = isl_basic_set_apply(bset1, bmap);
398 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
400 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
402 isl_basic_set_free(bset1);
403 isl_basic_set_free(bset2);
408 void test_application(struct isl_ctx *ctx)
410 test_application_case(ctx, "application");
411 test_application_case(ctx, "application2");
414 void test_affine_hull_case(struct isl_ctx *ctx, const char *name)
416 char filename[PATH_MAX];
419 struct isl_basic_set *bset1, *bset2;
421 n = snprintf(filename, sizeof(filename),
422 "%s/test_inputs/%s.polylib", srcdir, name);
423 assert(n < sizeof(filename));
424 input = fopen(filename, "r");
427 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
428 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
430 bset1 = isl_basic_set_affine_hull(bset1);
432 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
434 isl_basic_set_free(bset1);
435 isl_basic_set_free(bset2);
440 void test_affine_hull(struct isl_ctx *ctx)
442 test_affine_hull_case(ctx, "affine2");
443 test_affine_hull_case(ctx, "affine");
444 test_affine_hull_case(ctx, "affine3");
447 void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
449 char filename[PATH_MAX];
452 struct isl_basic_set *bset1, *bset2;
455 n = snprintf(filename, sizeof(filename),
456 "%s/test_inputs/%s.polylib", srcdir, name);
457 assert(n < sizeof(filename));
458 input = fopen(filename, "r");
461 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
462 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
464 set = isl_basic_set_union(bset1, bset2);
465 bset1 = isl_set_convex_hull(set);
467 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
469 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
471 isl_basic_set_free(bset1);
472 isl_basic_set_free(bset2);
477 void test_convex_hull(struct isl_ctx *ctx)
479 test_convex_hull_case(ctx, "convex0");
480 test_convex_hull_case(ctx, "convex1");
481 test_convex_hull_case(ctx, "convex2");
482 test_convex_hull_case(ctx, "convex3");
483 test_convex_hull_case(ctx, "convex4");
484 test_convex_hull_case(ctx, "convex5");
485 test_convex_hull_case(ctx, "convex6");
486 test_convex_hull_case(ctx, "convex7");
487 test_convex_hull_case(ctx, "convex8");
488 test_convex_hull_case(ctx, "convex9");
489 test_convex_hull_case(ctx, "convex10");
490 test_convex_hull_case(ctx, "convex11");
491 test_convex_hull_case(ctx, "convex12");
492 test_convex_hull_case(ctx, "convex13");
493 test_convex_hull_case(ctx, "convex14");
494 test_convex_hull_case(ctx, "convex15");
497 void test_gist_case(struct isl_ctx *ctx, const char *name)
499 char filename[PATH_MAX];
502 struct isl_basic_set *bset1, *bset2;
504 n = snprintf(filename, sizeof(filename),
505 "%s/test_inputs/%s.polylib", srcdir, name);
506 assert(n < sizeof(filename));
507 input = fopen(filename, "r");
510 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
511 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
513 bset1 = isl_basic_set_gist(bset1, bset2);
515 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
517 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
519 isl_basic_set_free(bset1);
520 isl_basic_set_free(bset2);
525 void test_gist(struct isl_ctx *ctx)
527 test_gist_case(ctx, "gist1");
530 void test_coalesce(struct isl_ctx *ctx)
532 struct isl_set *set, *set2;
533 struct isl_map *map, *map2;
535 set = isl_set_read_from_str(ctx,
536 "{[x,y]: x >= 0 & x <= 10 & y >= 0 & y <= 10 or "
537 "y >= x & x >= 2 & 5 >= y }", -1);
538 set = isl_set_coalesce(set);
539 assert(set && set->n == 1);
542 set = isl_set_read_from_str(ctx,
543 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
544 "x + y >= 10 & y <= x & x + y <= 20 & y >= 0}", -1);
545 set = isl_set_coalesce(set);
546 assert(set && set->n == 1);
549 set = isl_set_read_from_str(ctx,
550 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
551 "x + y >= 10 & y <= x & x + y <= 19 & y >= 0}", -1);
552 set = isl_set_coalesce(set);
553 assert(set && set->n == 2);
556 set = isl_set_read_from_str(ctx,
557 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
558 "y >= 0 & x >= 6 & x <= 10 & y <= x}", -1);
559 set = isl_set_coalesce(set);
560 assert(set && set->n == 1);
563 set = isl_set_read_from_str(ctx,
564 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
565 "y >= 0 & x >= 7 & x <= 10 & y <= x}", -1);
566 set = isl_set_coalesce(set);
567 assert(set && set->n == 2);
570 set = isl_set_read_from_str(ctx,
571 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
572 "y >= 0 & x >= 6 & x <= 10 & y + 1 <= x}", -1);
573 set = isl_set_coalesce(set);
574 assert(set && set->n == 2);
577 set = isl_set_read_from_str(ctx,
578 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
579 "y >= 0 & x = 6 & y <= 6}", -1);
580 set = isl_set_coalesce(set);
581 assert(set && set->n == 1);
584 set = isl_set_read_from_str(ctx,
585 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
586 "y >= 0 & x = 7 & y <= 6}", -1);
587 set = isl_set_coalesce(set);
588 assert(set && set->n == 2);
591 set = isl_set_read_from_str(ctx,
592 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
593 "y >= 0 & x = 6 & y <= 5}", -1);
594 set = isl_set_coalesce(set);
595 assert(set && set->n == 1);
596 set2 = isl_set_read_from_str(ctx,
597 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
598 "y >= 0 & x = 6 & y <= 5}", -1);
599 assert(isl_set_is_equal(set, set2));
603 set = isl_set_read_from_str(ctx,
604 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
605 "y >= 0 & x = 6 & y <= 7}", -1);
606 set = isl_set_coalesce(set);
607 assert(set && set->n == 2);
610 set = isl_set_read_from_str(ctx,
611 "[n] -> { [i] : i = 1 and n >= 2 or 2 <= i and i <= n }", -1);
612 set = isl_set_coalesce(set);
613 assert(set && set->n == 1);
614 set2 = isl_set_read_from_str(ctx,
615 "[n] -> { [i] : i = 1 and n >= 2 or 2 <= i and i <= n }", -1);
616 assert(isl_set_is_equal(set, set2));
620 set = isl_set_read_from_str(ctx,
621 "{[x,y] : x >= 0 and y >= 0 or 0 <= y and y <= 5 and x = -1}", -1);
622 set = isl_set_coalesce(set);
623 set2 = isl_set_read_from_str(ctx,
624 "{[x,y] : x >= 0 and y >= 0 or 0 <= y and y <= 5 and x = -1}", -1);
625 assert(isl_set_is_equal(set, set2));
629 set = isl_set_read_from_str(ctx,
630 "[n] -> { [i] : 1 <= i and i <= n - 1 or "
631 "2 <= i and i <= n }", -1);
632 set = isl_set_coalesce(set);
633 assert(set && set->n == 1);
634 set2 = isl_set_read_from_str(ctx,
635 "[n] -> { [i] : 1 <= i and i <= n - 1 or "
636 "2 <= i and i <= n }", -1);
637 assert(isl_set_is_equal(set, set2));
641 map = isl_map_read_from_str(ctx,
642 "[n] -> { [i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
643 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
644 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
645 "4e4 = -2 + o0 and i0 >= 8 + 2n and o0 >= 2 + i0 and "
646 "o0 <= 56 + 2n and o0 <= -12 + 4n and i0 <= 57 + 2n and "
647 "i0 <= -11 + 4n and o0 >= 6 + 2n and 4e0 <= i0 and "
648 "4e0 >= -3 + i0 and 4e1 <= o0 and 4e1 >= -3 + o0 and "
649 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0);"
650 "[i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
651 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
652 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
653 "4e4 = -2 + o0 and 2e0 >= 3 + n and e0 <= -4 + n and "
654 "2e0 <= 27 + n and e1 <= -4 + n and 2e1 <= 27 + n and "
655 "2e1 >= 2 + n and e1 >= 1 + e0 and i0 >= 7 + 2n and "
656 "i0 <= -11 + 4n and i0 <= 57 + 2n and 4e0 <= -2 + i0 and "
657 "4e0 >= -3 + i0 and o0 >= 6 + 2n and o0 <= -11 + 4n and "
658 "o0 <= 57 + 2n and 4e1 <= -2 + o0 and 4e1 >= -3 + o0 and "
659 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0 ) }", -1);
660 map = isl_map_coalesce(map);
661 map2 = isl_map_read_from_str(ctx,
662 "[n] -> { [i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
663 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
664 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
665 "4e4 = -2 + o0 and i0 >= 8 + 2n and o0 >= 2 + i0 and "
666 "o0 <= 56 + 2n and o0 <= -12 + 4n and i0 <= 57 + 2n and "
667 "i0 <= -11 + 4n and o0 >= 6 + 2n and 4e0 <= i0 and "
668 "4e0 >= -3 + i0 and 4e1 <= o0 and 4e1 >= -3 + o0 and "
669 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0);"
670 "[i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
671 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
672 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
673 "4e4 = -2 + o0 and 2e0 >= 3 + n and e0 <= -4 + n and "
674 "2e0 <= 27 + n and e1 <= -4 + n and 2e1 <= 27 + n and "
675 "2e1 >= 2 + n and e1 >= 1 + e0 and i0 >= 7 + 2n and "
676 "i0 <= -11 + 4n and i0 <= 57 + 2n and 4e0 <= -2 + i0 and "
677 "4e0 >= -3 + i0 and o0 >= 6 + 2n and o0 <= -11 + 4n and "
678 "o0 <= 57 + 2n and 4e1 <= -2 + o0 and 4e1 >= -3 + o0 and "
679 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0 ) }", -1);
680 assert(isl_map_is_equal(map, map2));
685 void test_closure(struct isl_ctx *ctx)
692 /* COCOA example 1 */
693 map = isl_map_read_from_str(ctx,
694 "[n,k] -> { [i,j] -> [i2,j2] : i2 = i + 1 and j2 = j + 1 and "
695 "1 <= i and i < n and 1 <= j and j < n or "
696 "i2 = i + 1 and j2 = j - 1 and "
697 "1 <= i and i < n and 2 <= j and j <= n }", -1);
698 map = isl_map_power(map, 1, &exact);
702 /* COCOA example 1 */
703 map = isl_map_read_from_str(ctx,
704 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 1 and j2 = j + 1 and "
705 "1 <= i and i < n and 1 <= j and j < n or "
706 "i2 = i + 1 and j2 = j - 1 and "
707 "1 <= i and i < n and 2 <= j and j <= n }", -1);
708 map = isl_map_transitive_closure(map, &exact);
710 map2 = isl_map_read_from_str(ctx,
711 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k : "
712 "1 <= i and i < n and 1 <= j and j <= n and "
713 "2 <= i2 and i2 <= n and 1 <= j2 and j2 <= n and "
714 "i2 = i + k1 + k2 and j2 = j + k1 - k2 and "
715 "k1 >= 0 and k2 >= 0 and k1 + k2 = k and k >= 1 )}", -1);
716 assert(isl_map_is_equal(map, map2));
720 map = isl_map_read_from_str(ctx,
721 "[n] -> { [x] -> [y] : y = x + 1 and 0 <= x and x <= n and "
722 " 0 <= y and y <= n }", -1);
723 map = isl_map_transitive_closure(map, &exact);
724 map2 = isl_map_read_from_str(ctx,
725 "[n] -> { [x] -> [y] : y > x and 0 <= x and x <= n and "
726 " 0 <= y and y <= n }", -1);
727 assert(isl_map_is_equal(map, map2));
731 /* COCOA example 2 */
732 map = isl_map_read_from_str(ctx,
733 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 2 and j2 = j + 2 and "
734 "1 <= i and i < n - 1 and 1 <= j and j < n - 1 or "
735 "i2 = i + 2 and j2 = j - 2 and "
736 "1 <= i and i < n - 1 and 3 <= j and j <= n }", -1);
737 map = isl_map_transitive_closure(map, &exact);
739 map2 = isl_map_read_from_str(ctx,
740 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k : "
741 "1 <= i and i < n - 1 and 1 <= j and j <= n and "
742 "3 <= i2 and i2 <= n and 1 <= j2 and j2 <= n and "
743 "i2 = i + 2 k1 + 2 k2 and j2 = j + 2 k1 - 2 k2 and "
744 "k1 >= 0 and k2 >= 0 and k1 + k2 = k and k >= 1) }", -1);
745 assert(isl_map_is_equal(map, map2));
749 /* COCOA Fig.2 left */
750 map = isl_map_read_from_str(ctx,
751 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 2 and j2 = j and "
752 "i <= 2 j - 3 and i <= n - 2 and j <= 2 i - 1 and "
754 "i2 = i and j2 = j + 2 and i <= 2 j - 1 and i <= n and "
755 "j <= 2 i - 3 and j <= n - 2 or "
756 "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
757 "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }", -1);
758 map = isl_map_transitive_closure(map, &exact);
762 /* COCOA Fig.2 right */
763 map = isl_map_read_from_str(ctx,
764 "[n,k] -> { [i,j] -> [i2,j2] : i2 = i + 3 and j2 = j and "
765 "i <= 2 j - 4 and i <= n - 3 and j <= 2 i - 1 and "
767 "i2 = i and j2 = j + 3 and i <= 2 j - 1 and i <= n and "
768 "j <= 2 i - 4 and j <= n - 3 or "
769 "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
770 "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }", -1);
771 map = isl_map_power(map, 1, &exact);
775 /* COCOA Fig.2 right */
776 map = isl_map_read_from_str(ctx,
777 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 3 and j2 = j and "
778 "i <= 2 j - 4 and i <= n - 3 and j <= 2 i - 1 and "
780 "i2 = i and j2 = j + 3 and i <= 2 j - 1 and i <= n and "
781 "j <= 2 i - 4 and j <= n - 3 or "
782 "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
783 "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }", -1);
784 map = isl_map_transitive_closure(map, &exact);
786 map2 = isl_map_read_from_str(ctx,
787 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k3,k : "
788 "i <= 2 j - 1 and i <= n and j <= 2 i - 1 and "
789 "j <= n and 3 + i + 2 j <= 3 n and "
790 "3 + 2 i + j <= 3n and i2 <= 2 j2 -1 and i2 <= n and "
791 "i2 <= 3 j2 - 4 and j2 <= 2 i2 -1 and j2 <= n and "
792 "13 + 4 j2 <= 11 i2 and i2 = i + 3 k1 + k3 and "
793 "j2 = j + 3 k2 + k3 and k1 >= 0 and k2 >= 0 and "
794 "k3 >= 0 and k1 + k2 + k3 = k and k > 0) }", -1);
795 assert(isl_map_is_equal(map, map2));
799 /* COCOA Fig.1 right */
800 dom = isl_set_read_from_str(ctx,
801 "{ [x,y] : x >= 0 and -2 x + 3 y >= 0 and x <= 3 and "
802 "2 x - 3 y + 3 >= 0 }", -1);
803 right = isl_map_read_from_str(ctx,
804 "{ [x,y] -> [x2,y2] : x2 = x + 1 and y2 = y }", -1);
805 up = isl_map_read_from_str(ctx,
806 "{ [x,y] -> [x2,y2] : x2 = x and y2 = y + 1 }", -1);
807 right = isl_map_intersect_domain(right, isl_set_copy(dom));
808 right = isl_map_intersect_range(right, isl_set_copy(dom));
809 up = isl_map_intersect_domain(up, isl_set_copy(dom));
810 up = isl_map_intersect_range(up, dom);
811 map = isl_map_union(up, right);
812 map = isl_map_transitive_closure(map, &exact);
816 /* COCOA Theorem 1 counter example */
817 map = isl_map_read_from_str(ctx,
818 "{ [i,j] -> [i2,j2] : i = 0 and 0 <= j and j <= 1 and "
819 "i2 = 1 and j2 = j or "
820 "i = 0 and j = 0 and i2 = 0 and j2 = 1 }", -1);
821 map = isl_map_transitive_closure(map, &exact);
825 map = isl_map_read_from_str(ctx,
826 "[m,n] -> { [i,j] -> [i2,j2] : i2 = i and j2 = j + 2 and "
827 "1 <= i,i2 <= n and 1 <= j,j2 <= m or "
828 "i2 = i + 1 and 3 <= j2 - j <= 4 and "
829 "1 <= i,i2 <= n and 1 <= j,j2 <= m }", -1);
830 map = isl_map_transitive_closure(map, &exact);
834 /* Kelly et al 1996, fig 12 */
835 map = isl_map_read_from_str(ctx,
836 "[n] -> { [i,j] -> [i2,j2] : i2 = i and j2 = j + 1 and "
837 "1 <= i,j,j+1 <= n or "
838 "j = n and j2 = 1 and i2 = i + 1 and "
839 "1 <= i,i+1 <= n }", -1);
840 map = isl_map_transitive_closure(map, &exact);
842 map2 = isl_map_read_from_str(ctx,
843 "[n] -> { [i,j] -> [i2,j2] : 1 <= j < j2 <= n and "
844 "1 <= i <= n and i = i2 or "
845 "1 <= i < i2 <= n and 1 <= j <= n and "
846 "1 <= j2 <= n }", -1);
847 assert(isl_map_is_equal(map, map2));
851 /* Omega's closure4 */
852 map = isl_map_read_from_str(ctx,
853 "[m,n] -> { [x,y] -> [x2,y2] : x2 = x and y2 = y + 1 and "
855 "x2 = x + 1 and y2 = y and "
856 "1 <= x <= 20 && 5 <= y <= 15 }", -1);
857 map = isl_map_transitive_closure(map, &exact);
861 map = isl_map_read_from_str(ctx,
862 "[n] -> { [x] -> [y]: 1 <= n <= y - x <= 10 }", -1);
863 map = isl_map_transitive_closure(map, &exact);
865 map2 = isl_map_read_from_str(ctx,
866 "[n] -> { [x] -> [y] : 1 <= n <= 10 and y >= n + x }", -1);
867 assert(isl_map_is_equal(map, map2));
876 srcdir = getenv("srcdir");
879 ctx = isl_ctx_alloc();
881 test_construction(ctx);
884 test_application(ctx);
885 test_affine_hull(ctx);
886 test_convex_hull(ctx);