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");
496 void test_gist_case(struct isl_ctx *ctx, const char *name)
498 char filename[PATH_MAX];
501 struct isl_basic_set *bset1, *bset2;
503 n = snprintf(filename, sizeof(filename),
504 "%s/test_inputs/%s.polylib", srcdir, name);
505 assert(n < sizeof(filename));
506 input = fopen(filename, "r");
509 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
510 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
512 bset1 = isl_basic_set_gist(bset1, bset2);
514 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
516 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
518 isl_basic_set_free(bset1);
519 isl_basic_set_free(bset2);
524 void test_gist(struct isl_ctx *ctx)
526 test_gist_case(ctx, "gist1");
529 void test_coalesce(struct isl_ctx *ctx)
533 set = isl_set_read_from_str(ctx,
534 "{[x,y]: x >= 0 & x <= 10 & y >= 0 & y <= 10 or "
535 "y >= x & x >= 2 & 5 >= y }", -1);
536 set = isl_set_coalesce(set);
537 assert(set && set->n == 1);
540 set = isl_set_read_from_str(ctx,
541 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
542 "x + y >= 10 & y <= x & x + y <= 20 & y >= 0}", -1);
543 set = isl_set_coalesce(set);
544 assert(set && set->n == 1);
547 set = isl_set_read_from_str(ctx,
548 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
549 "x + y >= 10 & y <= x & x + y <= 19 & y >= 0}", -1);
550 set = isl_set_coalesce(set);
551 assert(set && set->n == 2);
554 set = isl_set_read_from_str(ctx,
555 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
556 "y >= 0 & x >= 6 & x <= 10 & y <= x}", -1);
557 set = isl_set_coalesce(set);
558 assert(set && set->n == 1);
561 set = isl_set_read_from_str(ctx,
562 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
563 "y >= 0 & x >= 7 & x <= 10 & y <= x}", -1);
564 set = isl_set_coalesce(set);
565 assert(set && set->n == 2);
568 set = isl_set_read_from_str(ctx,
569 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
570 "y >= 0 & x >= 6 & x <= 10 & y + 1 <= x}", -1);
571 set = isl_set_coalesce(set);
572 assert(set && set->n == 2);
575 set = isl_set_read_from_str(ctx,
576 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
577 "y >= 0 & x = 6 & y <= 6}", -1);
578 set = isl_set_coalesce(set);
579 assert(set && set->n == 1);
582 set = isl_set_read_from_str(ctx,
583 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
584 "y >= 0 & x = 7 & y <= 6}", -1);
585 set = isl_set_coalesce(set);
586 assert(set && set->n == 2);
589 set = isl_set_read_from_str(ctx,
590 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
591 "y >= 0 & x = 6 & y <= 5}", -1);
592 set = isl_set_coalesce(set);
593 assert(set && set->n == 2);
596 set = isl_set_read_from_str(ctx,
597 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
598 "y >= 0 & x = 6 & y <= 7}", -1);
599 set = isl_set_coalesce(set);
600 assert(set && set->n == 2);
608 srcdir = getenv("srcdir");
611 ctx = isl_ctx_alloc();
613 test_construction(ctx);
616 test_application(ctx);
617 test_affine_hull(ctx);
618 test_convex_hull(ctx);