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_div(struct isl_ctx *ctx)
82 struct isl_basic_set *bset;
83 struct isl_constraint *c;
88 dim = isl_dim_set_alloc(ctx, 0, 1);
89 bset = isl_basic_set_universe(dim);
91 c = isl_equality_alloc(isl_dim_copy(bset->dim));
92 isl_int_set_si(v, -1);
93 isl_constraint_set_constant(c, v);
95 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
96 div = isl_div_alloc(isl_dim_copy(bset->dim));
97 c = isl_constraint_add_div(c, div, &pos);
99 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
100 bset = isl_basic_set_add_constraint(bset, c);
102 c = isl_equality_alloc(isl_dim_copy(bset->dim));
103 isl_int_set_si(v, 1);
104 isl_constraint_set_constant(c, v);
105 isl_int_set_si(v, -1);
106 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
107 div = isl_div_alloc(isl_dim_copy(bset->dim));
108 c = isl_constraint_add_div(c, div, &pos);
109 isl_int_set_si(v, 3);
110 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
111 bset = isl_basic_set_add_constraint(bset, c);
113 assert(bset->n_div == 1);
114 isl_basic_set_free(bset);
117 dim = isl_dim_set_alloc(ctx, 0, 1);
118 bset = isl_basic_set_universe(dim);
120 c = isl_equality_alloc(isl_dim_copy(bset->dim));
121 isl_int_set_si(v, 1);
122 isl_constraint_set_constant(c, v);
123 isl_int_set_si(v, -1);
124 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
125 div = isl_div_alloc(isl_dim_copy(bset->dim));
126 c = isl_constraint_add_div(c, div, &pos);
127 isl_int_set_si(v, 3);
128 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
129 bset = isl_basic_set_add_constraint(bset, c);
131 c = isl_equality_alloc(isl_dim_copy(bset->dim));
132 isl_int_set_si(v, -1);
133 isl_constraint_set_constant(c, v);
134 isl_int_set_si(v, 1);
135 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
136 div = isl_div_alloc(isl_dim_copy(bset->dim));
137 c = isl_constraint_add_div(c, div, &pos);
138 isl_int_set_si(v, 3);
139 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
140 bset = isl_basic_set_add_constraint(bset, c);
142 assert(bset->n_div == 1);
143 isl_basic_set_free(bset);
146 dim = isl_dim_set_alloc(ctx, 0, 1);
147 bset = isl_basic_set_universe(dim);
149 c = isl_equality_alloc(isl_dim_copy(bset->dim));
150 isl_int_set_si(v, 1);
151 isl_constraint_set_constant(c, v);
152 isl_int_set_si(v, -1);
153 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
154 div = isl_div_alloc(isl_dim_copy(bset->dim));
155 c = isl_constraint_add_div(c, div, &pos);
156 isl_int_set_si(v, 3);
157 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
158 bset = isl_basic_set_add_constraint(bset, c);
160 c = isl_equality_alloc(isl_dim_copy(bset->dim));
161 isl_int_set_si(v, -3);
162 isl_constraint_set_constant(c, v);
163 isl_int_set_si(v, 1);
164 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
165 div = isl_div_alloc(isl_dim_copy(bset->dim));
166 c = isl_constraint_add_div(c, div, &pos);
167 isl_int_set_si(v, 4);
168 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
169 bset = isl_basic_set_add_constraint(bset, c);
171 assert(bset->n_div == 1);
172 isl_basic_set_free(bset);
175 dim = isl_dim_set_alloc(ctx, 0, 1);
176 bset = isl_basic_set_universe(dim);
178 c = isl_equality_alloc(isl_dim_copy(bset->dim));
179 isl_int_set_si(v, 2);
180 isl_constraint_set_constant(c, v);
181 isl_int_set_si(v, -1);
182 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
183 div = isl_div_alloc(isl_dim_copy(bset->dim));
184 c = isl_constraint_add_div(c, div, &pos);
185 isl_int_set_si(v, 3);
186 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
187 bset = isl_basic_set_add_constraint(bset, c);
189 c = isl_equality_alloc(isl_dim_copy(bset->dim));
190 isl_int_set_si(v, -1);
191 isl_constraint_set_constant(c, v);
192 isl_int_set_si(v, 1);
193 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
194 div = isl_div_alloc(isl_dim_copy(bset->dim));
195 c = isl_constraint_add_div(c, div, &pos);
196 isl_int_set_si(v, 6);
197 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
198 bset = isl_basic_set_add_constraint(bset, c);
200 assert(isl_basic_set_is_empty(bset));
201 isl_basic_set_free(bset);
204 dim = isl_dim_set_alloc(ctx, 0, 2);
205 bset = isl_basic_set_universe(dim);
207 c = isl_equality_alloc(isl_dim_copy(bset->dim));
208 isl_int_set_si(v, -1);
209 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
210 div = isl_div_alloc(isl_dim_copy(bset->dim));
211 c = isl_constraint_add_div(c, div, &pos);
212 isl_int_set_si(v, 3);
213 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
214 bset = isl_basic_set_add_constraint(bset, c);
216 c = isl_equality_alloc(isl_dim_copy(bset->dim));
217 isl_int_set_si(v, 1);
218 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
219 isl_int_set_si(v, -3);
220 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
221 bset = isl_basic_set_add_constraint(bset, c);
223 assert(bset->n_div == 0);
224 isl_basic_set_free(bset);
227 dim = isl_dim_set_alloc(ctx, 0, 2);
228 bset = isl_basic_set_universe(dim);
230 c = isl_equality_alloc(isl_dim_copy(bset->dim));
231 isl_int_set_si(v, -1);
232 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
233 div = isl_div_alloc(isl_dim_copy(bset->dim));
234 c = isl_constraint_add_div(c, div, &pos);
235 isl_int_set_si(v, 6);
236 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
237 bset = isl_basic_set_add_constraint(bset, c);
239 c = isl_equality_alloc(isl_dim_copy(bset->dim));
240 isl_int_set_si(v, 1);
241 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
242 isl_int_set_si(v, -3);
243 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
244 bset = isl_basic_set_add_constraint(bset, c);
246 assert(bset->n_div == 1);
247 isl_basic_set_free(bset);
250 /* This test is a bit tricky. We set up an equality
252 * Normalization of divs creates _two_ divs
255 * Afterwards e0 is removed again because it has coefficient -1
256 * and we end up with the original equality and div again.
257 * Perhaps we can avoid the introduction of this temporary div.
259 dim = isl_dim_set_alloc(ctx, 0, 3);
260 bset = isl_basic_set_universe(dim);
262 c = isl_equality_alloc(isl_dim_copy(bset->dim));
263 isl_int_set_si(v, -1);
264 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
265 isl_int_set_si(v, -3);
266 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
267 isl_int_set_si(v, -3);
268 isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
269 div = isl_div_alloc(isl_dim_copy(bset->dim));
270 c = isl_constraint_add_div(c, div, &pos);
271 isl_int_set_si(v, 6);
272 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
273 bset = isl_basic_set_add_constraint(bset, c);
275 assert(bset->n_div == 1);
276 isl_basic_set_free(bset);
279 dim = isl_dim_set_alloc(ctx, 0, 4);
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, 3, 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 c = isl_equality_alloc(isl_dim_copy(bset->dim));
296 isl_int_set_si(v, -1);
297 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
298 isl_int_set_si(v, 1);
299 isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
300 isl_int_set_si(v, 1);
301 isl_constraint_set_constant(c, v);
302 bset = isl_basic_set_add_constraint(bset, c);
304 assert(bset->n_div == 1);
305 isl_basic_set_free(bset);
308 dim = isl_dim_set_alloc(ctx, 0, 2);
309 bset = isl_basic_set_universe(dim);
311 c = isl_equality_alloc(isl_dim_copy(bset->dim));
312 isl_int_set_si(v, 1);
313 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
314 isl_int_set_si(v, -1);
315 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
316 div = isl_div_alloc(isl_dim_copy(bset->dim));
317 c = isl_constraint_add_div(c, div, &pos);
318 isl_int_set_si(v, -2);
319 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
320 bset = isl_basic_set_add_constraint(bset, c);
322 c = isl_equality_alloc(isl_dim_copy(bset->dim));
323 isl_int_set_si(v, -1);
324 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
325 div = isl_div_alloc(isl_dim_copy(bset->dim));
326 c = isl_constraint_add_div(c, div, &pos);
327 isl_int_set_si(v, 3);
328 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
329 isl_int_set_si(v, 2);
330 isl_constraint_set_constant(c, v);
331 bset = isl_basic_set_add_constraint(bset, c);
333 bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
335 assert(!isl_basic_set_is_empty(bset));
337 isl_basic_set_free(bset);
340 dim = isl_dim_set_alloc(ctx, 0, 2);
341 bset = isl_basic_set_universe(dim);
343 c = isl_equality_alloc(isl_dim_copy(bset->dim));
344 isl_int_set_si(v, 1);
345 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
346 div = isl_div_alloc(isl_dim_copy(bset->dim));
347 c = isl_constraint_add_div(c, div, &pos);
348 isl_int_set_si(v, -2);
349 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
350 bset = isl_basic_set_add_constraint(bset, c);
352 bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
354 isl_basic_set_free(bset);
359 void test_application_case(struct isl_ctx *ctx, const char *name)
361 char filename[PATH_MAX];
364 struct isl_basic_set *bset1, *bset2;
365 struct isl_basic_map *bmap;
367 n = snprintf(filename, sizeof(filename),
368 "%s/test_inputs/%s.omega", srcdir, name);
369 assert(n < sizeof(filename));
370 input = fopen(filename, "r");
373 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
374 bmap = isl_basic_map_read_from_file(ctx, input, 0);
376 bset1 = isl_basic_set_apply(bset1, bmap);
378 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
380 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
382 isl_basic_set_free(bset1);
383 isl_basic_set_free(bset2);
388 void test_application(struct isl_ctx *ctx)
390 test_application_case(ctx, "application");
391 test_application_case(ctx, "application2");
394 void test_affine_hull_case(struct isl_ctx *ctx, const char *name)
396 char filename[PATH_MAX];
399 struct isl_basic_set *bset1, *bset2;
401 n = snprintf(filename, sizeof(filename),
402 "%s/test_inputs/%s.polylib", srcdir, name);
403 assert(n < sizeof(filename));
404 input = fopen(filename, "r");
407 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
408 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
410 bset1 = isl_basic_set_affine_hull(bset1);
412 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
414 isl_basic_set_free(bset1);
415 isl_basic_set_free(bset2);
420 void test_affine_hull(struct isl_ctx *ctx)
422 test_affine_hull_case(ctx, "affine2");
423 test_affine_hull_case(ctx, "affine");
424 test_affine_hull_case(ctx, "affine3");
427 void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
429 char filename[PATH_MAX];
432 struct isl_basic_set *bset1, *bset2;
435 n = snprintf(filename, sizeof(filename),
436 "%s/test_inputs/%s.polylib", srcdir, name);
437 assert(n < sizeof(filename));
438 input = fopen(filename, "r");
441 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
442 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
444 set = isl_basic_set_union(bset1, bset2);
445 bset1 = isl_set_convex_hull(set);
447 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
449 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
451 isl_basic_set_free(bset1);
452 isl_basic_set_free(bset2);
457 void test_convex_hull(struct isl_ctx *ctx)
459 test_convex_hull_case(ctx, "convex0");
460 test_convex_hull_case(ctx, "convex1");
461 test_convex_hull_case(ctx, "convex2");
462 test_convex_hull_case(ctx, "convex3");
463 test_convex_hull_case(ctx, "convex4");
464 test_convex_hull_case(ctx, "convex5");
465 test_convex_hull_case(ctx, "convex6");
466 test_convex_hull_case(ctx, "convex7");
467 test_convex_hull_case(ctx, "convex8");
468 test_convex_hull_case(ctx, "convex9");
469 test_convex_hull_case(ctx, "convex10");
470 test_convex_hull_case(ctx, "convex11");
471 test_convex_hull_case(ctx, "convex12");
472 test_convex_hull_case(ctx, "convex13");
473 test_convex_hull_case(ctx, "convex14");
476 void test_gist_case(struct isl_ctx *ctx, const char *name)
478 char filename[PATH_MAX];
481 struct isl_basic_set *bset1, *bset2;
483 n = snprintf(filename, sizeof(filename),
484 "%s/test_inputs/%s.polylib", srcdir, name);
485 assert(n < sizeof(filename));
486 input = fopen(filename, "r");
489 bset1 = isl_basic_set_read_from_file(ctx, input, 0);
490 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
492 bset1 = isl_basic_set_gist(bset1, bset2);
494 bset2 = isl_basic_set_read_from_file(ctx, input, 0);
496 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
498 isl_basic_set_free(bset1);
499 isl_basic_set_free(bset2);
504 void test_gist(struct isl_ctx *ctx)
506 test_gist_case(ctx, "gist1");
509 void test_coalesce(struct isl_ctx *ctx)
513 set = isl_set_read_from_str(ctx,
514 "{[x,y]: x >= 0 & x <= 10 & y >= 0 & y <= 10 or "
515 "y >= x & x >= 2 & 5 >= y }", -1);
516 set = isl_set_coalesce(set);
517 assert(set && set->n == 1);
520 set = isl_set_read_from_str(ctx,
521 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
522 "x + y >= 10 & y <= x & x + y <= 20 & y >= 0}", -1);
523 set = isl_set_coalesce(set);
524 assert(set && set->n == 1);
527 set = isl_set_read_from_str(ctx,
528 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
529 "x + y >= 10 & y <= x & x + y <= 19 & y >= 0}", -1);
530 set = isl_set_coalesce(set);
531 assert(set && set->n == 2);
534 set = isl_set_read_from_str(ctx,
535 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
536 "y >= 0 & x >= 6 & x <= 10 & y <= x}", -1);
537 set = isl_set_coalesce(set);
538 assert(set && set->n == 1);
541 set = isl_set_read_from_str(ctx,
542 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
543 "y >= 0 & x >= 7 & x <= 10 & y <= x}", -1);
544 set = isl_set_coalesce(set);
545 assert(set && set->n == 2);
548 set = isl_set_read_from_str(ctx,
549 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
550 "y >= 0 & x >= 6 & x <= 10 & y + 1 <= x}", -1);
551 set = isl_set_coalesce(set);
552 assert(set && set->n == 2);
555 set = isl_set_read_from_str(ctx,
556 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
557 "y >= 0 & x = 6 & y <= 6}", -1);
558 set = isl_set_coalesce(set);
559 assert(set && set->n == 1);
562 set = isl_set_read_from_str(ctx,
563 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
564 "y >= 0 & x = 7 & y <= 6}", -1);
565 set = isl_set_coalesce(set);
566 assert(set && set->n == 2);
569 set = isl_set_read_from_str(ctx,
570 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
571 "y >= 0 & x = 6 & y <= 5}", -1);
572 set = isl_set_coalesce(set);
573 assert(set && set->n == 2);
576 set = isl_set_read_from_str(ctx,
577 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
578 "y >= 0 & x = 6 & y <= 7}", -1);
579 set = isl_set_coalesce(set);
580 assert(set && set->n == 2);
588 srcdir = getenv("srcdir");
591 ctx = isl_ctx_alloc();
593 test_construction(ctx);
595 test_application(ctx);
596 test_affine_hull(ctx);
597 test_convex_hull(ctx);