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
16 #include <isl_constraint.h>
20 void test_read(struct isl_ctx
*ctx
)
22 char filename
[PATH_MAX
];
25 struct isl_basic_set
*bset1
, *bset2
;
26 const char *str
= "{[y]: Exists ( alpha : 2alpha = y)}";
28 n
= snprintf(filename
, sizeof(filename
),
29 "%s/test_inputs/set.omega", srcdir
);
30 assert(n
< sizeof(filename
));
31 input
= fopen(filename
, "r");
34 bset1
= isl_basic_set_read_from_file(ctx
, input
, 0);
35 bset2
= isl_basic_set_read_from_str(ctx
, str
, 0);
37 assert(isl_basic_set_is_equal(bset1
, bset2
) == 1);
39 isl_basic_set_free(bset1
);
40 isl_basic_set_free(bset2
);
45 /* Construct the basic set { [i] : 5 <= i <= N } */
46 void test_construction(struct isl_ctx
*ctx
)
50 struct isl_basic_set
*bset
;
51 struct isl_constraint
*c
;
55 dim
= isl_dim_set_alloc(ctx
, 1, 1);
56 bset
= isl_basic_set_universe(dim
);
58 c
= isl_inequality_alloc(isl_dim_copy(bset
->dim
));
59 isl_int_set_si(v
, -1);
60 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
62 isl_constraint_set_coefficient(c
, isl_dim_param
, 0, v
);
63 bset
= isl_basic_set_add_constraint(bset
, c
);
65 c
= isl_inequality_alloc(isl_dim_copy(bset
->dim
));
67 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
68 isl_int_set_si(v
, -5);
69 isl_constraint_set_constant(c
, v
);
70 bset
= isl_basic_set_add_constraint(bset
, c
);
72 isl_basic_set_free(bset
);
77 void test_dim(struct isl_ctx
*ctx
)
81 map1
= isl_map_read_from_str(ctx
,
82 "[n] -> { [i] -> [j] : exists (a = [i/10] : i - 10a <= n ) }", -1);
83 map1
= isl_map_add(map1
, isl_dim_in
, 1);
84 map2
= isl_map_read_from_str(ctx
,
85 "[n] -> { [i,k] -> [j] : exists (a = [i/10] : i - 10a <= n ) }", -1);
86 assert(isl_map_is_equal(map1
, map2
));
89 map1
= isl_map_project_out(map1
, isl_dim_in
, 0, 1);
90 map2
= isl_map_read_from_str(ctx
, "[n] -> { [i] -> [j] : n >= 0 }", -1);
91 assert(isl_map_is_equal(map1
, map2
));
97 void test_div(struct isl_ctx
*ctx
)
103 struct isl_basic_set
*bset
;
104 struct isl_constraint
*c
;
109 dim
= isl_dim_set_alloc(ctx
, 0, 1);
110 bset
= isl_basic_set_universe(dim
);
112 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
113 isl_int_set_si(v
, -1);
114 isl_constraint_set_constant(c
, v
);
115 isl_int_set_si(v
, 1);
116 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
117 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
118 c
= isl_constraint_add_div(c
, div
, &pos
);
119 isl_int_set_si(v
, 3);
120 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
121 bset
= isl_basic_set_add_constraint(bset
, c
);
123 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
124 isl_int_set_si(v
, 1);
125 isl_constraint_set_constant(c
, v
);
126 isl_int_set_si(v
, -1);
127 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
128 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
129 c
= isl_constraint_add_div(c
, div
, &pos
);
130 isl_int_set_si(v
, 3);
131 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
132 bset
= isl_basic_set_add_constraint(bset
, c
);
134 assert(bset
->n_div
== 1);
135 isl_basic_set_free(bset
);
138 dim
= isl_dim_set_alloc(ctx
, 0, 1);
139 bset
= isl_basic_set_universe(dim
);
141 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
142 isl_int_set_si(v
, 1);
143 isl_constraint_set_constant(c
, v
);
144 isl_int_set_si(v
, -1);
145 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
146 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
147 c
= isl_constraint_add_div(c
, div
, &pos
);
148 isl_int_set_si(v
, 3);
149 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
150 bset
= isl_basic_set_add_constraint(bset
, c
);
152 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
153 isl_int_set_si(v
, -1);
154 isl_constraint_set_constant(c
, v
);
155 isl_int_set_si(v
, 1);
156 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
157 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
158 c
= isl_constraint_add_div(c
, div
, &pos
);
159 isl_int_set_si(v
, 3);
160 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
161 bset
= isl_basic_set_add_constraint(bset
, c
);
163 assert(bset
->n_div
== 1);
164 isl_basic_set_free(bset
);
167 dim
= isl_dim_set_alloc(ctx
, 0, 1);
168 bset
= isl_basic_set_universe(dim
);
170 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
171 isl_int_set_si(v
, 1);
172 isl_constraint_set_constant(c
, v
);
173 isl_int_set_si(v
, -1);
174 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
175 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
176 c
= isl_constraint_add_div(c
, div
, &pos
);
177 isl_int_set_si(v
, 3);
178 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
179 bset
= isl_basic_set_add_constraint(bset
, c
);
181 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
182 isl_int_set_si(v
, -3);
183 isl_constraint_set_constant(c
, v
);
184 isl_int_set_si(v
, 1);
185 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
186 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
187 c
= isl_constraint_add_div(c
, div
, &pos
);
188 isl_int_set_si(v
, 4);
189 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
190 bset
= isl_basic_set_add_constraint(bset
, c
);
192 assert(bset
->n_div
== 1);
193 isl_basic_set_free(bset
);
196 dim
= isl_dim_set_alloc(ctx
, 0, 1);
197 bset
= isl_basic_set_universe(dim
);
199 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
200 isl_int_set_si(v
, 2);
201 isl_constraint_set_constant(c
, v
);
202 isl_int_set_si(v
, -1);
203 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
204 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
205 c
= isl_constraint_add_div(c
, div
, &pos
);
206 isl_int_set_si(v
, 3);
207 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
208 bset
= isl_basic_set_add_constraint(bset
, c
);
210 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
211 isl_int_set_si(v
, -1);
212 isl_constraint_set_constant(c
, v
);
213 isl_int_set_si(v
, 1);
214 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
215 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
216 c
= isl_constraint_add_div(c
, div
, &pos
);
217 isl_int_set_si(v
, 6);
218 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
219 bset
= isl_basic_set_add_constraint(bset
, c
);
221 assert(isl_basic_set_is_empty(bset
));
222 isl_basic_set_free(bset
);
225 dim
= isl_dim_set_alloc(ctx
, 0, 2);
226 bset
= isl_basic_set_universe(dim
);
228 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
229 isl_int_set_si(v
, -1);
230 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
231 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
232 c
= isl_constraint_add_div(c
, div
, &pos
);
233 isl_int_set_si(v
, 3);
234 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
235 bset
= isl_basic_set_add_constraint(bset
, c
);
237 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
238 isl_int_set_si(v
, 1);
239 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
240 isl_int_set_si(v
, -3);
241 isl_constraint_set_coefficient(c
, isl_dim_set
, 1, v
);
242 bset
= isl_basic_set_add_constraint(bset
, c
);
244 assert(bset
->n_div
== 0);
245 isl_basic_set_free(bset
);
248 dim
= isl_dim_set_alloc(ctx
, 0, 2);
249 bset
= isl_basic_set_universe(dim
);
251 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
252 isl_int_set_si(v
, -1);
253 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
254 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
255 c
= isl_constraint_add_div(c
, div
, &pos
);
256 isl_int_set_si(v
, 6);
257 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
258 bset
= isl_basic_set_add_constraint(bset
, c
);
260 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
261 isl_int_set_si(v
, 1);
262 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
263 isl_int_set_si(v
, -3);
264 isl_constraint_set_coefficient(c
, isl_dim_set
, 1, v
);
265 bset
= isl_basic_set_add_constraint(bset
, c
);
267 assert(bset
->n_div
== 1);
268 isl_basic_set_free(bset
);
271 /* This test is a bit tricky. We set up an equality
273 * Normalization of divs creates _two_ divs
276 * Afterwards e0 is removed again because it has coefficient -1
277 * and we end up with the original equality and div again.
278 * Perhaps we can avoid the introduction of this temporary div.
280 dim
= isl_dim_set_alloc(ctx
, 0, 3);
281 bset
= isl_basic_set_universe(dim
);
283 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
284 isl_int_set_si(v
, -1);
285 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
286 isl_int_set_si(v
, -3);
287 isl_constraint_set_coefficient(c
, isl_dim_set
, 1, v
);
288 isl_int_set_si(v
, -3);
289 isl_constraint_set_coefficient(c
, isl_dim_set
, 2, v
);
290 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
291 c
= isl_constraint_add_div(c
, div
, &pos
);
292 isl_int_set_si(v
, 6);
293 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
294 bset
= isl_basic_set_add_constraint(bset
, c
);
296 /* Test disabled for now */
298 assert(bset->n_div == 1);
300 isl_basic_set_free(bset
);
303 dim
= isl_dim_set_alloc(ctx
, 0, 4);
304 bset
= isl_basic_set_universe(dim
);
306 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
307 isl_int_set_si(v
, -1);
308 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
309 isl_int_set_si(v
, -3);
310 isl_constraint_set_coefficient(c
, isl_dim_set
, 1, v
);
311 isl_int_set_si(v
, -3);
312 isl_constraint_set_coefficient(c
, isl_dim_set
, 3, v
);
313 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
314 c
= isl_constraint_add_div(c
, div
, &pos
);
315 isl_int_set_si(v
, 6);
316 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
317 bset
= isl_basic_set_add_constraint(bset
, c
);
319 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
320 isl_int_set_si(v
, -1);
321 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
322 isl_int_set_si(v
, 1);
323 isl_constraint_set_coefficient(c
, isl_dim_set
, 2, v
);
324 isl_int_set_si(v
, 1);
325 isl_constraint_set_constant(c
, v
);
326 bset
= isl_basic_set_add_constraint(bset
, c
);
328 /* Test disabled for now */
330 assert(bset->n_div == 1);
332 isl_basic_set_free(bset
);
335 dim
= isl_dim_set_alloc(ctx
, 0, 2);
336 bset
= isl_basic_set_universe(dim
);
338 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
339 isl_int_set_si(v
, 1);
340 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
341 isl_int_set_si(v
, -1);
342 isl_constraint_set_coefficient(c
, isl_dim_set
, 1, v
);
343 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
344 c
= isl_constraint_add_div(c
, div
, &pos
);
345 isl_int_set_si(v
, -2);
346 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
347 bset
= isl_basic_set_add_constraint(bset
, c
);
349 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
350 isl_int_set_si(v
, -1);
351 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
352 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
353 c
= isl_constraint_add_div(c
, div
, &pos
);
354 isl_int_set_si(v
, 3);
355 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
356 isl_int_set_si(v
, 2);
357 isl_constraint_set_constant(c
, v
);
358 bset
= isl_basic_set_add_constraint(bset
, c
);
360 bset
= isl_basic_set_fix_si(bset
, isl_dim_set
, 0, 2);
362 assert(!isl_basic_set_is_empty(bset
));
364 isl_basic_set_free(bset
);
367 dim
= isl_dim_set_alloc(ctx
, 0, 2);
368 bset
= isl_basic_set_universe(dim
);
370 c
= isl_equality_alloc(isl_dim_copy(bset
->dim
));
371 isl_int_set_si(v
, 1);
372 isl_constraint_set_coefficient(c
, isl_dim_set
, 0, v
);
373 div
= isl_div_alloc(isl_dim_copy(bset
->dim
));
374 c
= isl_constraint_add_div(c
, div
, &pos
);
375 isl_int_set_si(v
, -2);
376 isl_constraint_set_coefficient(c
, isl_dim_div
, pos
, v
);
377 bset
= isl_basic_set_add_constraint(bset
, c
);
379 bset
= isl_basic_set_fix_si(bset
, isl_dim_set
, 0, 2);
381 isl_basic_set_free(bset
);
386 void test_application_case(struct isl_ctx
*ctx
, const char *name
)
388 char filename
[PATH_MAX
];
391 struct isl_basic_set
*bset1
, *bset2
;
392 struct isl_basic_map
*bmap
;
394 n
= snprintf(filename
, sizeof(filename
),
395 "%s/test_inputs/%s.omega", srcdir
, name
);
396 assert(n
< sizeof(filename
));
397 input
= fopen(filename
, "r");
400 bset1
= isl_basic_set_read_from_file(ctx
, input
, 0);
401 bmap
= isl_basic_map_read_from_file(ctx
, input
, 0);
403 bset1
= isl_basic_set_apply(bset1
, bmap
);
405 bset2
= isl_basic_set_read_from_file(ctx
, input
, 0);
407 assert(isl_basic_set_is_equal(bset1
, bset2
) == 1);
409 isl_basic_set_free(bset1
);
410 isl_basic_set_free(bset2
);
415 void test_application(struct isl_ctx
*ctx
)
417 test_application_case(ctx
, "application");
418 test_application_case(ctx
, "application2");
421 void test_affine_hull_case(struct isl_ctx
*ctx
, const char *name
)
423 char filename
[PATH_MAX
];
426 struct isl_basic_set
*bset1
, *bset2
;
428 n
= snprintf(filename
, sizeof(filename
),
429 "%s/test_inputs/%s.polylib", srcdir
, name
);
430 assert(n
< sizeof(filename
));
431 input
= fopen(filename
, "r");
434 bset1
= isl_basic_set_read_from_file(ctx
, input
, 0);
435 bset2
= isl_basic_set_read_from_file(ctx
, input
, 0);
437 bset1
= isl_basic_set_affine_hull(bset1
);
439 assert(isl_basic_set_is_equal(bset1
, bset2
) == 1);
441 isl_basic_set_free(bset1
);
442 isl_basic_set_free(bset2
);
447 void test_affine_hull(struct isl_ctx
*ctx
)
449 test_affine_hull_case(ctx
, "affine2");
450 test_affine_hull_case(ctx
, "affine");
451 test_affine_hull_case(ctx
, "affine3");
454 void test_convex_hull_case(struct isl_ctx
*ctx
, const char *name
)
456 char filename
[PATH_MAX
];
459 struct isl_basic_set
*bset1
, *bset2
;
462 n
= snprintf(filename
, sizeof(filename
),
463 "%s/test_inputs/%s.polylib", srcdir
, name
);
464 assert(n
< sizeof(filename
));
465 input
= fopen(filename
, "r");
468 bset1
= isl_basic_set_read_from_file(ctx
, input
, 0);
469 bset2
= isl_basic_set_read_from_file(ctx
, input
, 0);
471 set
= isl_basic_set_union(bset1
, bset2
);
472 bset1
= isl_set_convex_hull(set
);
474 bset2
= isl_basic_set_read_from_file(ctx
, input
, 0);
476 assert(isl_basic_set_is_equal(bset1
, bset2
) == 1);
478 isl_basic_set_free(bset1
);
479 isl_basic_set_free(bset2
);
484 void test_convex_hull(struct isl_ctx
*ctx
)
486 const char *str1
, *str2
;
487 isl_set
*set1
, *set2
;
489 test_convex_hull_case(ctx
, "convex0");
490 test_convex_hull_case(ctx
, "convex1");
491 test_convex_hull_case(ctx
, "convex2");
492 test_convex_hull_case(ctx
, "convex3");
493 test_convex_hull_case(ctx
, "convex4");
494 test_convex_hull_case(ctx
, "convex5");
495 test_convex_hull_case(ctx
, "convex6");
496 test_convex_hull_case(ctx
, "convex7");
497 test_convex_hull_case(ctx
, "convex8");
498 test_convex_hull_case(ctx
, "convex9");
499 test_convex_hull_case(ctx
, "convex10");
500 test_convex_hull_case(ctx
, "convex11");
501 test_convex_hull_case(ctx
, "convex12");
502 test_convex_hull_case(ctx
, "convex13");
503 test_convex_hull_case(ctx
, "convex14");
504 test_convex_hull_case(ctx
, "convex15");
506 str1
= "{ [i0, i1, i2] : (i2 = 1 and i0 = 0 and i1 >= 0) or "
507 "(i0 = 1 and i1 = 0 and i2 = 1) or "
508 "(i0 = 0 and i1 = 0 and i2 = 0) }";
509 str2
= "{ [i0, i1, i2] : i0 >= 0 and i2 >= i0 and i2 <= 1 and i1 >= 0 }";
510 set1
= isl_set_read_from_str(ctx
, str1
, -1);
511 set2
= isl_set_read_from_str(ctx
, str2
, -1);
512 set1
= isl_set_from_basic_set(isl_set_convex_hull(set1
));
513 assert(isl_set_is_equal(set1
, set2
));
518 void test_gist_case(struct isl_ctx
*ctx
, const char *name
)
520 char filename
[PATH_MAX
];
523 struct isl_basic_set
*bset1
, *bset2
;
525 n
= snprintf(filename
, sizeof(filename
),
526 "%s/test_inputs/%s.polylib", srcdir
, name
);
527 assert(n
< sizeof(filename
));
528 input
= fopen(filename
, "r");
531 bset1
= isl_basic_set_read_from_file(ctx
, input
, 0);
532 bset2
= isl_basic_set_read_from_file(ctx
, input
, 0);
534 bset1
= isl_basic_set_gist(bset1
, bset2
);
536 bset2
= isl_basic_set_read_from_file(ctx
, input
, 0);
538 assert(isl_basic_set_is_equal(bset1
, bset2
) == 1);
540 isl_basic_set_free(bset1
);
541 isl_basic_set_free(bset2
);
546 void test_gist(struct isl_ctx
*ctx
)
548 test_gist_case(ctx
, "gist1");
551 void test_coalesce_set(isl_ctx
*ctx
, const char *str
, int check_one
)
555 set
= isl_set_read_from_str(ctx
, str
, -1);
556 set
= isl_set_coalesce(set
);
557 set2
= isl_set_read_from_str(ctx
, str
, -1);
558 assert(isl_set_is_equal(set
, set2
));
560 assert(set
&& set
->n
== 1);
565 void test_coalesce(struct isl_ctx
*ctx
)
568 struct isl_set
*set
, *set2
;
569 struct isl_map
*map
, *map2
;
571 set
= isl_set_read_from_str(ctx
,
572 "{[x,y]: x >= 0 & x <= 10 & y >= 0 & y <= 10 or "
573 "y >= x & x >= 2 & 5 >= y }", -1);
574 set
= isl_set_coalesce(set
);
575 assert(set
&& set
->n
== 1);
578 set
= isl_set_read_from_str(ctx
,
579 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
580 "x + y >= 10 & y <= x & x + y <= 20 & y >= 0}", -1);
581 set
= isl_set_coalesce(set
);
582 assert(set
&& set
->n
== 1);
585 set
= isl_set_read_from_str(ctx
,
586 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
587 "x + y >= 10 & y <= x & x + y <= 19 & y >= 0}", -1);
588 set
= isl_set_coalesce(set
);
589 assert(set
&& set
->n
== 2);
592 set
= isl_set_read_from_str(ctx
,
593 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
594 "y >= 0 & x >= 6 & x <= 10 & y <= x}", -1);
595 set
= isl_set_coalesce(set
);
596 assert(set
&& set
->n
== 1);
599 set
= isl_set_read_from_str(ctx
,
600 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
601 "y >= 0 & x >= 7 & x <= 10 & y <= x}", -1);
602 set
= isl_set_coalesce(set
);
603 assert(set
&& set
->n
== 2);
606 set
= isl_set_read_from_str(ctx
,
607 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
608 "y >= 0 & x >= 6 & x <= 10 & y + 1 <= x}", -1);
609 set
= isl_set_coalesce(set
);
610 assert(set
&& set
->n
== 2);
613 set
= isl_set_read_from_str(ctx
,
614 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
615 "y >= 0 & x = 6 & y <= 6}", -1);
616 set
= isl_set_coalesce(set
);
617 assert(set
&& set
->n
== 1);
620 set
= isl_set_read_from_str(ctx
,
621 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
622 "y >= 0 & x = 7 & y <= 6}", -1);
623 set
= isl_set_coalesce(set
);
624 assert(set
&& set
->n
== 2);
627 set
= isl_set_read_from_str(ctx
,
628 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
629 "y >= 0 & x = 6 & y <= 5}", -1);
630 set
= isl_set_coalesce(set
);
631 assert(set
&& set
->n
== 1);
632 set2
= isl_set_read_from_str(ctx
,
633 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
634 "y >= 0 & x = 6 & y <= 5}", -1);
635 assert(isl_set_is_equal(set
, set2
));
639 set
= isl_set_read_from_str(ctx
,
640 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
641 "y >= 0 & x = 6 & y <= 7}", -1);
642 set
= isl_set_coalesce(set
);
643 assert(set
&& set
->n
== 2);
646 set
= isl_set_read_from_str(ctx
,
647 "[n] -> { [i] : i = 1 and n >= 2 or 2 <= i and i <= n }", -1);
648 set
= isl_set_coalesce(set
);
649 assert(set
&& set
->n
== 1);
650 set2
= isl_set_read_from_str(ctx
,
651 "[n] -> { [i] : i = 1 and n >= 2 or 2 <= i and i <= n }", -1);
652 assert(isl_set_is_equal(set
, set2
));
656 set
= isl_set_read_from_str(ctx
,
657 "{[x,y] : x >= 0 and y >= 0 or 0 <= y and y <= 5 and x = -1}", -1);
658 set
= isl_set_coalesce(set
);
659 set2
= isl_set_read_from_str(ctx
,
660 "{[x,y] : x >= 0 and y >= 0 or 0 <= y and y <= 5 and x = -1}", -1);
661 assert(isl_set_is_equal(set
, set2
));
665 set
= isl_set_read_from_str(ctx
,
666 "[n] -> { [i] : 1 <= i and i <= n - 1 or "
667 "2 <= i and i <= n }", -1);
668 set
= isl_set_coalesce(set
);
669 assert(set
&& set
->n
== 1);
670 set2
= isl_set_read_from_str(ctx
,
671 "[n] -> { [i] : 1 <= i and i <= n - 1 or "
672 "2 <= i and i <= n }", -1);
673 assert(isl_set_is_equal(set
, set2
));
677 map
= isl_map_read_from_str(ctx
,
678 "[n] -> { [i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
679 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
680 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
681 "4e4 = -2 + o0 and i0 >= 8 + 2n and o0 >= 2 + i0 and "
682 "o0 <= 56 + 2n and o0 <= -12 + 4n and i0 <= 57 + 2n and "
683 "i0 <= -11 + 4n and o0 >= 6 + 2n and 4e0 <= i0 and "
684 "4e0 >= -3 + i0 and 4e1 <= o0 and 4e1 >= -3 + o0 and "
685 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0);"
686 "[i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
687 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
688 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
689 "4e4 = -2 + o0 and 2e0 >= 3 + n and e0 <= -4 + n and "
690 "2e0 <= 27 + n and e1 <= -4 + n and 2e1 <= 27 + n and "
691 "2e1 >= 2 + n and e1 >= 1 + e0 and i0 >= 7 + 2n and "
692 "i0 <= -11 + 4n and i0 <= 57 + 2n and 4e0 <= -2 + i0 and "
693 "4e0 >= -3 + i0 and o0 >= 6 + 2n and o0 <= -11 + 4n and "
694 "o0 <= 57 + 2n and 4e1 <= -2 + o0 and 4e1 >= -3 + o0 and "
695 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0 ) }", -1);
696 map
= isl_map_coalesce(map
);
697 map2
= isl_map_read_from_str(ctx
,
698 "[n] -> { [i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
699 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
700 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
701 "4e4 = -2 + o0 and i0 >= 8 + 2n and o0 >= 2 + i0 and "
702 "o0 <= 56 + 2n and o0 <= -12 + 4n and i0 <= 57 + 2n and "
703 "i0 <= -11 + 4n and o0 >= 6 + 2n and 4e0 <= i0 and "
704 "4e0 >= -3 + i0 and 4e1 <= o0 and 4e1 >= -3 + o0 and "
705 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0);"
706 "[i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
707 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
708 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
709 "4e4 = -2 + o0 and 2e0 >= 3 + n and e0 <= -4 + n and "
710 "2e0 <= 27 + n and e1 <= -4 + n and 2e1 <= 27 + n and "
711 "2e1 >= 2 + n and e1 >= 1 + e0 and i0 >= 7 + 2n and "
712 "i0 <= -11 + 4n and i0 <= 57 + 2n and 4e0 <= -2 + i0 and "
713 "4e0 >= -3 + i0 and o0 >= 6 + 2n and o0 <= -11 + 4n and "
714 "o0 <= 57 + 2n and 4e1 <= -2 + o0 and 4e1 >= -3 + o0 and "
715 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0 ) }", -1);
716 assert(isl_map_is_equal(map
, map2
));
720 str
= "[n, m] -> { [] -> [o0, o2, o3] : (o3 = 1 and o0 >= 1 + m and "
721 "o0 <= n + m and o2 <= m and o0 >= 2 + n and o2 >= 3) or "
722 "(o0 >= 2 + n and o0 >= 1 + m and o0 <= n + m and n >= 1 and "
723 "o3 <= -1 + o2 and o3 >= 1 - m + o2 and o3 >= 2 and o3 <= n) }";
724 map
= isl_map_read_from_str(ctx
, str
, -1);
725 map
= isl_map_coalesce(map
);
726 map2
= isl_map_read_from_str(ctx
, str
, -1);
727 assert(isl_map_is_equal(map
, map2
));
731 str
= "[M, N] -> { [i0, i1, i2, i3, i4, i5, i6] -> "
732 "[o0, o1, o2, o3, o4, o5, o6] : "
733 "(o6 <= -4 + 2M - 2N + i0 + i1 - i2 + i6 - o0 - o1 + o2 and "
734 "o3 <= -2 + i3 and o6 >= 2 + i0 + i3 + i6 - o0 - o3 and "
735 "o6 >= 2 - M + N + i3 + i4 + i6 - o3 - o4 and o0 <= -1 + i0 and "
736 "o4 >= 4 - 3M + 3N - i0 - i1 + i2 + 2i3 + i4 + o0 + o1 - o2 - 2o3 "
737 "and o6 <= -3 + 2M - 2N + i3 + i4 - i5 + i6 - o3 - o4 + o5 and "
738 "2o6 <= -5 + 5M - 5N + 2i0 + i1 - i2 - i5 + 2i6 - 2o0 - o1 + o2 + o5 "
739 "and o6 >= 2i0 + i1 + i6 - 2o0 - o1 and "
740 "3o6 <= -5 + 4M - 4N + 2i0 + i1 - i2 + 2i3 + i4 - i5 + 3i6 "
741 "- 2o0 - o1 + o2 - 2o3 - o4 + o5) or "
742 "(N >= 2 and o3 <= -1 + i3 and o0 <= -1 + i0 and "
743 "o6 >= i3 + i6 - o3 and M >= 0 and "
744 "2o6 >= 1 + i0 + i3 + 2i6 - o0 - o3 and "
745 "o6 >= 1 - M + i0 + i6 - o0 and N >= 2M and o6 >= i0 + i6 - o0) }";
746 map
= isl_map_read_from_str(ctx
, str
, -1);
747 map
= isl_map_coalesce(map
);
748 map2
= isl_map_read_from_str(ctx
, str
, -1);
749 assert(isl_map_is_equal(map
, map2
));
753 str
= "[M, N] -> { [] -> [o0] : (o0 = 0 and M >= 1 and N >= 2) or "
754 "(o0 = 0 and M >= 1 and N >= 2M and N >= 2 + M) or "
755 "(o0 = 0 and M >= 2 and N >= 3) or "
756 "(M = 0 and o0 = 0 and N >= 3) }";
757 map
= isl_map_read_from_str(ctx
, str
, -1);
758 map
= isl_map_coalesce(map
);
759 map2
= isl_map_read_from_str(ctx
, str
, -1);
760 assert(isl_map_is_equal(map
, map2
));
764 str
= "{ [i0, i1, i2, i3] : (i1 = 10i0 and i0 >= 1 and 10i0 <= 100 and "
765 "i3 <= 9 + 10 i2 and i3 >= 1 + 10i2 and i3 >= 0) or "
766 "(i1 <= 9 + 10i0 and i1 >= 1 + 10i0 and i2 >= 0 and "
767 "i0 >= 0 and i1 <= 100 and i3 <= 9 + 10i2 and i3 >= 1 + 10i2) }";
768 map
= isl_map_read_from_str(ctx
, str
, -1);
769 map
= isl_map_coalesce(map
);
770 map2
= isl_map_read_from_str(ctx
, str
, -1);
771 assert(isl_map_is_equal(map
, map2
));
775 test_coalesce_set(ctx
,
776 "[M] -> { [i1] : (i1 >= 2 and i1 <= M) or "
777 "(i1 = M and M >= 1) }", 0);
778 test_coalesce_set(ctx
,
779 "{[x,y] : x,y >= 0; [x,y] : 10 <= x <= 20 and y >= -1 }", 0);
780 test_coalesce_set(ctx
,
781 "{ [x, y] : (x >= 1 and y >= 1 and x <= 2 and y <= 2) or "
782 "(y = 3 and x = 1) }", 1);
783 test_coalesce_set(ctx
,
784 "[M] -> { [i0, i1, i2, i3, i4] : (i1 >= 3 and i4 >= 2 + i2 and "
785 "i2 >= 2 and i0 >= 2 and i3 >= 1 + i2 and i0 <= M and "
786 "i1 <= M and i3 <= M and i4 <= M) or "
787 "(i1 >= 2 and i4 >= 1 + i2 and i2 >= 2 and i0 >= 2 and "
788 "i3 >= 1 + i2 and i0 <= M and i1 <= -1 + M and i3 <= M and "
789 "i4 <= -1 + M) }", 1);
790 test_coalesce_set(ctx
,
791 "{ [x, y] : (x >= 0 and y >= 0 and x <= 10 and y <= 10) or "
792 "(x >= 1 and y >= 1 and x <= 11 and y <= 11) }", 1);
793 test_coalesce_set(ctx
,
794 "{[x,y,z] : y + 2 >= 0 and x - y + 1 >= 0 and "
795 "-x - y + 1 >= 0 and -3 <= z <= 3;"
796 "[x,y,z] : -x+z + 20 >= 0 and -x-z + 20 >= 0 and "
797 "x-z + 20 >= 0 and x+z + 20 >= 0 and -10 <= y <= 0}", 1);
798 test_coalesce_set(ctx
,
799 "{[x,y] : 0 <= x,y <= 10; [5,y]: 4 <=y <= 11}", 1);
802 void test_closure(struct isl_ctx
*ctx
)
810 /* COCOA example 1 */
811 map
= isl_map_read_from_str(ctx
,
812 "[n,k] -> { [i,j] -> [i2,j2] : i2 = i + 1 and j2 = j + 1 and "
813 "1 <= i and i < n and 1 <= j and j < n or "
814 "i2 = i + 1 and j2 = j - 1 and "
815 "1 <= i and i < n and 2 <= j and j <= n }", -1);
816 map
= isl_map_power(map
, 1, &exact
);
820 /* COCOA example 1 */
821 map
= isl_map_read_from_str(ctx
,
822 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 1 and j2 = j + 1 and "
823 "1 <= i and i < n and 1 <= j and j < n or "
824 "i2 = i + 1 and j2 = j - 1 and "
825 "1 <= i and i < n and 2 <= j and j <= n }", -1);
826 map
= isl_map_transitive_closure(map
, &exact
);
828 map2
= isl_map_read_from_str(ctx
,
829 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k : "
830 "1 <= i and i < n and 1 <= j and j <= n and "
831 "2 <= i2 and i2 <= n and 1 <= j2 and j2 <= n and "
832 "i2 = i + k1 + k2 and j2 = j + k1 - k2 and "
833 "k1 >= 0 and k2 >= 0 and k1 + k2 = k and k >= 1 )}", -1);
834 assert(isl_map_is_equal(map
, map2
));
838 map
= isl_map_read_from_str(ctx
,
839 "[n] -> { [x] -> [y] : y = x + 1 and 0 <= x and x <= n and "
840 " 0 <= y and y <= n }", -1);
841 map
= isl_map_transitive_closure(map
, &exact
);
842 map2
= isl_map_read_from_str(ctx
,
843 "[n] -> { [x] -> [y] : y > x and 0 <= x and x <= n and "
844 " 0 <= y and y <= n }", -1);
845 assert(isl_map_is_equal(map
, map2
));
849 /* COCOA example 2 */
850 map
= isl_map_read_from_str(ctx
,
851 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 2 and j2 = j + 2 and "
852 "1 <= i and i < n - 1 and 1 <= j and j < n - 1 or "
853 "i2 = i + 2 and j2 = j - 2 and "
854 "1 <= i and i < n - 1 and 3 <= j and j <= n }", -1);
855 map
= isl_map_transitive_closure(map
, &exact
);
857 map2
= isl_map_read_from_str(ctx
,
858 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k : "
859 "1 <= i and i < n - 1 and 1 <= j and j <= n and "
860 "3 <= i2 and i2 <= n and 1 <= j2 and j2 <= n and "
861 "i2 = i + 2 k1 + 2 k2 and j2 = j + 2 k1 - 2 k2 and "
862 "k1 >= 0 and k2 >= 0 and k1 + k2 = k and k >= 1) }", -1);
863 assert(isl_map_is_equal(map
, map2
));
867 /* COCOA Fig.2 left */
868 map
= isl_map_read_from_str(ctx
,
869 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 2 and j2 = j and "
870 "i <= 2 j - 3 and i <= n - 2 and j <= 2 i - 1 and "
872 "i2 = i and j2 = j + 2 and i <= 2 j - 1 and i <= n and "
873 "j <= 2 i - 3 and j <= n - 2 or "
874 "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
875 "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }", -1);
876 map
= isl_map_transitive_closure(map
, &exact
);
880 /* COCOA Fig.2 right */
881 map
= isl_map_read_from_str(ctx
,
882 "[n,k] -> { [i,j] -> [i2,j2] : i2 = i + 3 and j2 = j and "
883 "i <= 2 j - 4 and i <= n - 3 and j <= 2 i - 1 and "
885 "i2 = i and j2 = j + 3 and i <= 2 j - 1 and i <= n and "
886 "j <= 2 i - 4 and j <= n - 3 or "
887 "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
888 "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }", -1);
889 map
= isl_map_power(map
, 1, &exact
);
893 /* COCOA Fig.2 right */
894 map
= isl_map_read_from_str(ctx
,
895 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 3 and j2 = j and "
896 "i <= 2 j - 4 and i <= n - 3 and j <= 2 i - 1 and "
898 "i2 = i and j2 = j + 3 and i <= 2 j - 1 and i <= n and "
899 "j <= 2 i - 4 and j <= n - 3 or "
900 "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
901 "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }", -1);
902 map
= isl_map_transitive_closure(map
, &exact
);
904 map2
= isl_map_read_from_str(ctx
,
905 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k3,k : "
906 "i <= 2 j - 1 and i <= n and j <= 2 i - 1 and "
907 "j <= n and 3 + i + 2 j <= 3 n and "
908 "3 + 2 i + j <= 3n and i2 <= 2 j2 -1 and i2 <= n and "
909 "i2 <= 3 j2 - 4 and j2 <= 2 i2 -1 and j2 <= n and "
910 "13 + 4 j2 <= 11 i2 and i2 = i + 3 k1 + k3 and "
911 "j2 = j + 3 k2 + k3 and k1 >= 0 and k2 >= 0 and "
912 "k3 >= 0 and k1 + k2 + k3 = k and k > 0) }", -1);
913 assert(isl_map_is_equal(map
, map2
));
917 /* COCOA Fig.1 right */
918 dom
= isl_set_read_from_str(ctx
,
919 "{ [x,y] : x >= 0 and -2 x + 3 y >= 0 and x <= 3 and "
920 "2 x - 3 y + 3 >= 0 }", -1);
921 right
= isl_map_read_from_str(ctx
,
922 "{ [x,y] -> [x2,y2] : x2 = x + 1 and y2 = y }", -1);
923 up
= isl_map_read_from_str(ctx
,
924 "{ [x,y] -> [x2,y2] : x2 = x and y2 = y + 1 }", -1);
925 right
= isl_map_intersect_domain(right
, isl_set_copy(dom
));
926 right
= isl_map_intersect_range(right
, isl_set_copy(dom
));
927 up
= isl_map_intersect_domain(up
, isl_set_copy(dom
));
928 up
= isl_map_intersect_range(up
, dom
);
929 map
= isl_map_union(up
, right
);
930 map
= isl_map_transitive_closure(map
, &exact
);
932 map2
= isl_map_read_from_str(ctx
,
933 "{ [0,0] -> [0,1]; [0,0] -> [1,1]; [0,1] -> [1,1]; "
934 " [2,2] -> [3,2]; [2,2] -> [3,3]; [3,2] -> [3,3] }", -1);
935 assert(isl_map_is_equal(map
, map2
));
939 /* COCOA Theorem 1 counter example */
940 map
= isl_map_read_from_str(ctx
,
941 "{ [i,j] -> [i2,j2] : i = 0 and 0 <= j and j <= 1 and "
942 "i2 = 1 and j2 = j or "
943 "i = 0 and j = 0 and i2 = 0 and j2 = 1 }", -1);
944 map
= isl_map_transitive_closure(map
, &exact
);
948 map
= isl_map_read_from_str(ctx
,
949 "[m,n] -> { [i,j] -> [i2,j2] : i2 = i and j2 = j + 2 and "
950 "1 <= i,i2 <= n and 1 <= j,j2 <= m or "
951 "i2 = i + 1 and 3 <= j2 - j <= 4 and "
952 "1 <= i,i2 <= n and 1 <= j,j2 <= m }", -1);
953 map
= isl_map_transitive_closure(map
, &exact
);
957 /* Kelly et al 1996, fig 12 */
958 map
= isl_map_read_from_str(ctx
,
959 "[n] -> { [i,j] -> [i2,j2] : i2 = i and j2 = j + 1 and "
960 "1 <= i,j,j+1 <= n or "
961 "j = n and j2 = 1 and i2 = i + 1 and "
962 "1 <= i,i+1 <= n }", -1);
963 map
= isl_map_transitive_closure(map
, &exact
);
965 map2
= isl_map_read_from_str(ctx
,
966 "[n] -> { [i,j] -> [i2,j2] : 1 <= j < j2 <= n and "
967 "1 <= i <= n and i = i2 or "
968 "1 <= i < i2 <= n and 1 <= j <= n and "
969 "1 <= j2 <= n }", -1);
970 assert(isl_map_is_equal(map
, map2
));
974 /* Omega's closure4 */
975 map
= isl_map_read_from_str(ctx
,
976 "[m,n] -> { [x,y] -> [x2,y2] : x2 = x and y2 = y + 1 and "
978 "x2 = x + 1 and y2 = y and "
979 "1 <= x <= 20 && 5 <= y <= 15 }", -1);
980 map
= isl_map_transitive_closure(map
, &exact
);
984 map
= isl_map_read_from_str(ctx
,
985 "[n] -> { [x] -> [y]: 1 <= n <= y - x <= 10 }", -1);
986 map
= isl_map_transitive_closure(map
, &exact
);
988 map2
= isl_map_read_from_str(ctx
,
989 "[n] -> { [x] -> [y] : 1 <= n <= 10 and y >= n + x }", -1);
990 assert(isl_map_is_equal(map
, map2
));
994 str
= "[n, m] -> { [i0, i1, i2, i3] -> [o0, o1, o2, o3] : "
995 "i3 = 1 and o0 = i0 and o1 = -1 + i1 and o2 = -1 + i2 and "
996 "o3 = -2 + i2 and i1 <= -1 + i0 and i1 >= 1 - m + i0 and "
997 "i1 >= 2 and i1 <= n and i2 >= 3 and i2 <= 1 + n and i2 <= m }";
998 map
= isl_map_read_from_str(ctx
, str
, -1);
999 map
= isl_map_transitive_closure(map
, &exact
);
1001 map2
= isl_map_read_from_str(ctx
, str
, -1);
1002 assert(isl_map_is_equal(map
, map2
));
1006 str
= "{[0] -> [1]; [2] -> [3]}";
1007 map
= isl_map_read_from_str(ctx
, str
, -1);
1008 map
= isl_map_transitive_closure(map
, &exact
);
1010 map2
= isl_map_read_from_str(ctx
, str
, -1);
1011 assert(isl_map_is_equal(map
, map2
));
1016 void test_lexmin(struct isl_ctx
*ctx
)
1021 str
= "[p0, p1] -> { [] -> [] : "
1022 "exists (e0 = [(2p1)/3], e1, e2, e3 = [(3 - p1 + 3e0)/3], "
1023 "e4 = [(p1)/3], e5 = [(p1 + 3e4)/3]: "
1024 "3e0 >= -2 + 2p1 and 3e0 >= p1 and 3e3 >= 1 - p1 + 3e0 and "
1025 "3e0 <= 2p1 and 3e3 >= -2 + p1 and 3e3 <= -1 + p1 and p1 >= 3 and "
1026 "3e5 >= -2 + 2p1 and 3e5 >= p1 and 3e5 <= -1 + p1 + 3e4 and "
1027 "3e4 <= p1 and 3e4 >= -2 + p1 and e3 <= -1 + e0 and "
1028 "3e4 >= 6 - p1 + 3e1 and 3e1 >= p1 and 3e5 >= -2 + p1 + 3e4 and "
1029 "2e4 >= 3 - p1 + 2e1 and e4 <= e1 and 3e3 <= 2 - p1 + 3e0 and "
1030 "e5 >= 1 + e1 and 3e4 >= 6 - 2p1 + 3e1 and "
1031 "p0 >= 2 and p1 >= p0 and 3e2 >= p1 and 3e4 >= 6 - p1 + 3e2 and "
1032 "e2 <= e1 and e3 >= 1 and e4 <= e2) }";
1033 map
= isl_map_read_from_str(ctx
, str
, -1);
1034 map
= isl_map_lexmin(map
);
1043 static int collect_must_may(__isl_take isl_map
*dep
, int must
,
1044 void *dep_user
, void *user
)
1046 struct must_may
*mm
= (struct must_may
*)user
;
1049 mm
->must
= isl_map_union(mm
->must
, dep
);
1051 mm
->may
= isl_map_union(mm
->may
, dep
);
1056 static int common_space(void *first
, void *second
)
1058 int depth
= *(int *)first
;
1062 int map_is_equal(__isl_keep isl_map
*map
, const char *str
)
1067 map2
= isl_map_read_from_str(map
->ctx
, str
, -1);
1068 equal
= isl_map_is_equal(map
, map2
);
1074 void test_dep(struct isl_ctx
*ctx
)
1079 isl_access_info
*ai
;
1086 str
= "{ [2,i,0] -> [i] : 0 <= i <= 10 }";
1087 map
= isl_map_read_from_str(ctx
, str
, -1);
1088 ai
= isl_access_info_alloc(map
, &depth
, &common_space
, 2);
1090 str
= "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1091 map
= isl_map_read_from_str(ctx
, str
, -1);
1092 ai
= isl_access_info_add_source(ai
, map
, 1, &depth
);
1094 str
= "{ [1,i,0] -> [5] : 0 <= i <= 10 }";
1095 map
= isl_map_read_from_str(ctx
, str
, -1);
1096 ai
= isl_access_info_add_source(ai
, map
, 1, &depth
);
1098 flow
= isl_access_info_compute_flow(ai
);
1099 dim
= isl_dim_alloc(ctx
, 0, 3, 3);
1100 mm
.must
= isl_map_empty(isl_dim_copy(dim
));
1101 mm
.may
= isl_map_empty(dim
);
1103 isl_flow_foreach(flow
, collect_must_may
, &mm
);
1105 str
= "{ [0,i,0] -> [2,i,0] : (0 <= i <= 4) or (6 <= i <= 10); "
1106 " [1,10,0] -> [2,5,0] }";
1107 assert(map_is_equal(mm
.must
, str
));
1108 str
= "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1109 assert(map_is_equal(mm
.may
, str
));
1111 isl_map_free(mm
.must
);
1112 isl_map_free(mm
.may
);
1113 isl_flow_free(flow
);
1116 str
= "{ [2,i,0] -> [i] : 0 <= i <= 10 }";
1117 map
= isl_map_read_from_str(ctx
, str
, -1);
1118 ai
= isl_access_info_alloc(map
, &depth
, &common_space
, 2);
1120 str
= "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1121 map
= isl_map_read_from_str(ctx
, str
, -1);
1122 ai
= isl_access_info_add_source(ai
, map
, 1, &depth
);
1124 str
= "{ [1,i,0] -> [5] : 0 <= i <= 10 }";
1125 map
= isl_map_read_from_str(ctx
, str
, -1);
1126 ai
= isl_access_info_add_source(ai
, map
, 0, &depth
);
1128 flow
= isl_access_info_compute_flow(ai
);
1129 dim
= isl_dim_alloc(ctx
, 0, 3, 3);
1130 mm
.must
= isl_map_empty(isl_dim_copy(dim
));
1131 mm
.may
= isl_map_empty(dim
);
1133 isl_flow_foreach(flow
, collect_must_may
, &mm
);
1135 str
= "{ [0,i,0] -> [2,i,0] : (0 <= i <= 4) or (6 <= i <= 10) }";
1136 assert(map_is_equal(mm
.must
, str
));
1137 str
= "{ [0,5,0] -> [2,5,0]; [1,i,0] -> [2,5,0] : 0 <= i <= 10 }";
1138 assert(map_is_equal(mm
.may
, str
));
1140 isl_map_free(mm
.must
);
1141 isl_map_free(mm
.may
);
1142 isl_flow_free(flow
);
1145 str
= "{ [2,i,0] -> [i] : 0 <= i <= 10 }";
1146 map
= isl_map_read_from_str(ctx
, str
, -1);
1147 ai
= isl_access_info_alloc(map
, &depth
, &common_space
, 2);
1149 str
= "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1150 map
= isl_map_read_from_str(ctx
, str
, -1);
1151 ai
= isl_access_info_add_source(ai
, map
, 0, &depth
);
1153 str
= "{ [1,i,0] -> [5] : 0 <= i <= 10 }";
1154 map
= isl_map_read_from_str(ctx
, str
, -1);
1155 ai
= isl_access_info_add_source(ai
, map
, 0, &depth
);
1157 flow
= isl_access_info_compute_flow(ai
);
1158 dim
= isl_dim_alloc(ctx
, 0, 3, 3);
1159 mm
.must
= isl_map_empty(isl_dim_copy(dim
));
1160 mm
.may
= isl_map_empty(dim
);
1162 isl_flow_foreach(flow
, collect_must_may
, &mm
);
1164 str
= "{ [0,i,0] -> [2,i,0] : 0 <= i <= 10; "
1165 " [1,i,0] -> [2,5,0] : 0 <= i <= 10 }";
1166 assert(map_is_equal(mm
.may
, str
));
1167 str
= "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1168 assert(map_is_equal(mm
.must
, str
));
1170 isl_map_free(mm
.must
);
1171 isl_map_free(mm
.may
);
1172 isl_flow_free(flow
);
1175 str
= "{ [0,i,2] -> [i] : 0 <= i <= 10 }";
1176 map
= isl_map_read_from_str(ctx
, str
, -1);
1177 ai
= isl_access_info_alloc(map
, &depth
, &common_space
, 2);
1179 str
= "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1180 map
= isl_map_read_from_str(ctx
, str
, -1);
1181 ai
= isl_access_info_add_source(ai
, map
, 0, &depth
);
1183 str
= "{ [0,i,1] -> [5] : 0 <= i <= 10 }";
1184 map
= isl_map_read_from_str(ctx
, str
, -1);
1185 ai
= isl_access_info_add_source(ai
, map
, 0, &depth
);
1187 flow
= isl_access_info_compute_flow(ai
);
1188 dim
= isl_dim_alloc(ctx
, 0, 3, 3);
1189 mm
.must
= isl_map_empty(isl_dim_copy(dim
));
1190 mm
.may
= isl_map_empty(dim
);
1192 isl_flow_foreach(flow
, collect_must_may
, &mm
);
1194 str
= "{ [0,i,0] -> [0,i,2] : 0 <= i <= 10; "
1195 " [0,i,1] -> [0,5,2] : 0 <= i <= 5 }";
1196 assert(map_is_equal(mm
.may
, str
));
1197 str
= "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1198 assert(map_is_equal(mm
.must
, str
));
1200 isl_map_free(mm
.must
);
1201 isl_map_free(mm
.may
);
1202 isl_flow_free(flow
);
1205 str
= "{ [0,i,1] -> [i] : 0 <= i <= 10 }";
1206 map
= isl_map_read_from_str(ctx
, str
, -1);
1207 ai
= isl_access_info_alloc(map
, &depth
, &common_space
, 2);
1209 str
= "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1210 map
= isl_map_read_from_str(ctx
, str
, -1);
1211 ai
= isl_access_info_add_source(ai
, map
, 0, &depth
);
1213 str
= "{ [0,i,2] -> [5] : 0 <= i <= 10 }";
1214 map
= isl_map_read_from_str(ctx
, str
, -1);
1215 ai
= isl_access_info_add_source(ai
, map
, 0, &depth
);
1217 flow
= isl_access_info_compute_flow(ai
);
1218 dim
= isl_dim_alloc(ctx
, 0, 3, 3);
1219 mm
.must
= isl_map_empty(isl_dim_copy(dim
));
1220 mm
.may
= isl_map_empty(dim
);
1222 isl_flow_foreach(flow
, collect_must_may
, &mm
);
1224 str
= "{ [0,i,0] -> [0,i,1] : 0 <= i <= 10; "
1225 " [0,i,2] -> [0,5,1] : 0 <= i <= 4 }";
1226 assert(map_is_equal(mm
.may
, str
));
1227 str
= "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1228 assert(map_is_equal(mm
.must
, str
));
1230 isl_map_free(mm
.must
);
1231 isl_map_free(mm
.may
);
1232 isl_flow_free(flow
);
1237 str
= "{ [1,i,0,0,0] -> [i,j] : 0 <= i <= 10 and 0 <= j <= 10 }";
1238 map
= isl_map_read_from_str(ctx
, str
, -1);
1239 ai
= isl_access_info_alloc(map
, &depth
, &common_space
, 1);
1241 str
= "{ [0,i,0,j,0] -> [i,j] : 0 <= i <= 10 and 0 <= j <= 10 }";
1242 map
= isl_map_read_from_str(ctx
, str
, -1);
1243 ai
= isl_access_info_add_source(ai
, map
, 1, &depth
);
1245 flow
= isl_access_info_compute_flow(ai
);
1246 dim
= isl_dim_alloc(ctx
, 0, 5, 5);
1247 mm
.must
= isl_map_empty(isl_dim_copy(dim
));
1248 mm
.may
= isl_map_empty(dim
);
1250 isl_flow_foreach(flow
, collect_must_may
, &mm
);
1252 str
= "{ [0,i,0,j,0] -> [1,i,0,0,0] : 0 <= i,j <= 10 }";
1253 assert(map_is_equal(mm
.must
, str
));
1254 str
= "{ [0,0,0,0,0] -> [0,0,0,0,0] : 1 = 0 }";
1255 assert(map_is_equal(mm
.may
, str
));
1257 isl_map_free(mm
.must
);
1258 isl_map_free(mm
.may
);
1259 isl_flow_free(flow
);
1262 void test_sv(struct isl_ctx
*ctx
)
1267 str
= "[N] -> { [i] -> [f] : 0 <= i <= N and 0 <= i - 10 f <= 9 }";
1268 map
= isl_map_read_from_str(ctx
, str
, -1);
1269 assert(isl_map_is_single_valued(map
));
1272 str
= "[N] -> { [i] -> [f] : 0 <= i <= N and 0 <= i - 10 f <= 10 }";
1273 map
= isl_map_read_from_str(ctx
, str
, -1);
1274 assert(!isl_map_is_single_valued(map
));
1280 struct isl_ctx
*ctx
;
1282 srcdir
= getenv("srcdir");
1285 ctx
= isl_ctx_alloc();
1289 test_construction(ctx
);
1292 test_application(ctx
);
1293 test_affine_hull(ctx
);
1294 test_convex_hull(ctx
);