6 #include <isl_constraint.h>
10 void test_read(struct isl_ctx *ctx)
12 char filename[PATH_MAX];
15 struct isl_basic_set *bset1, *bset2;
16 const char *str = "{[y]: Exists ( alpha : 2alpha = y)}";
18 n = snprintf(filename, sizeof(filename),
19 "%s/test_inputs/set.omega", srcdir);
20 assert(n < sizeof(filename));
21 input = fopen(filename, "r");
24 bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
25 bset2 = isl_basic_set_read_from_str(ctx, str, 0, ISL_FORMAT_OMEGA);
27 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
29 isl_basic_set_free(bset1);
30 isl_basic_set_free(bset2);
35 /* Construct the basic set { [i] : 5 <= i <= N } */
36 void test_construction(struct isl_ctx *ctx)
40 struct isl_basic_set *bset;
41 struct isl_constraint *c;
45 dim = isl_dim_set_alloc(ctx, 1, 1);
46 bset = isl_basic_set_universe(dim);
48 c = isl_inequality_alloc(isl_dim_copy(bset->dim));
49 isl_int_set_si(v, -1);
50 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
52 isl_constraint_set_coefficient(c, isl_dim_param, 0, v);
53 bset = isl_basic_set_add_constraint(bset, c);
55 c = isl_inequality_alloc(isl_dim_copy(bset->dim));
57 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
58 isl_int_set_si(v, -5);
59 isl_constraint_set_constant(c, v);
60 bset = isl_basic_set_add_constraint(bset, c);
62 isl_basic_set_free(bset);
67 void test_div(struct isl_ctx *ctx)
73 struct isl_basic_set *bset;
74 struct isl_constraint *c;
79 dim = isl_dim_set_alloc(ctx, 0, 1);
80 bset = isl_basic_set_universe(dim);
82 c = isl_equality_alloc(isl_dim_copy(bset->dim));
83 isl_int_set_si(v, -1);
84 isl_constraint_set_constant(c, v);
86 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
87 div = isl_div_alloc(isl_dim_copy(bset->dim));
88 c = isl_constraint_add_div(c, div, &pos);
90 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
91 bset = isl_basic_set_add_constraint(bset, c);
93 c = isl_equality_alloc(isl_dim_copy(bset->dim));
95 isl_constraint_set_constant(c, v);
96 isl_int_set_si(v, -1);
97 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
98 div = isl_div_alloc(isl_dim_copy(bset->dim));
99 c = isl_constraint_add_div(c, div, &pos);
100 isl_int_set_si(v, 3);
101 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
102 bset = isl_basic_set_add_constraint(bset, c);
104 assert(bset->n_div == 1);
105 isl_basic_set_free(bset);
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, -3);
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, 4);
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, 2);
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, -1);
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, 6);
188 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
189 bset = isl_basic_set_add_constraint(bset, c);
191 assert(isl_basic_set_is_empty(bset));
192 isl_basic_set_free(bset);
195 dim = isl_dim_set_alloc(ctx, 0, 2);
196 bset = isl_basic_set_universe(dim);
198 c = isl_equality_alloc(isl_dim_copy(bset->dim));
199 isl_int_set_si(v, -1);
200 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
201 div = isl_div_alloc(isl_dim_copy(bset->dim));
202 c = isl_constraint_add_div(c, div, &pos);
203 isl_int_set_si(v, 3);
204 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
205 bset = isl_basic_set_add_constraint(bset, c);
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 isl_int_set_si(v, -3);
211 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
212 bset = isl_basic_set_add_constraint(bset, c);
214 assert(bset->n_div == 0);
215 isl_basic_set_free(bset);
218 dim = isl_dim_set_alloc(ctx, 0, 2);
219 bset = isl_basic_set_universe(dim);
221 c = isl_equality_alloc(isl_dim_copy(bset->dim));
222 isl_int_set_si(v, -1);
223 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
224 div = isl_div_alloc(isl_dim_copy(bset->dim));
225 c = isl_constraint_add_div(c, div, &pos);
226 isl_int_set_si(v, 6);
227 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
228 bset = isl_basic_set_add_constraint(bset, c);
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 isl_int_set_si(v, -3);
234 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
235 bset = isl_basic_set_add_constraint(bset, c);
237 assert(bset->n_div == 1);
238 isl_basic_set_free(bset);
241 /* This test is a bit tricky. We set up an equality
243 * Normalization of divs creates _two_ divs
246 * Afterwards e0 is removed again because it has coefficient -1
247 * and we end up with the original equality and div again.
248 * Perhaps we can avoid the introduction of this temporary div.
250 dim = isl_dim_set_alloc(ctx, 0, 3);
251 bset = isl_basic_set_universe(dim);
253 c = isl_equality_alloc(isl_dim_copy(bset->dim));
254 isl_int_set_si(v, -1);
255 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
256 isl_int_set_si(v, -3);
257 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
258 isl_int_set_si(v, -3);
259 isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
260 div = isl_div_alloc(isl_dim_copy(bset->dim));
261 c = isl_constraint_add_div(c, div, &pos);
262 isl_int_set_si(v, 6);
263 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
264 bset = isl_basic_set_add_constraint(bset, c);
266 assert(bset->n_div == 1);
267 isl_basic_set_free(bset);
270 dim = isl_dim_set_alloc(ctx, 0, 4);
271 bset = isl_basic_set_universe(dim);
273 c = isl_equality_alloc(isl_dim_copy(bset->dim));
274 isl_int_set_si(v, -1);
275 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
276 isl_int_set_si(v, -3);
277 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
278 isl_int_set_si(v, -3);
279 isl_constraint_set_coefficient(c, isl_dim_set, 3, v);
280 div = isl_div_alloc(isl_dim_copy(bset->dim));
281 c = isl_constraint_add_div(c, div, &pos);
282 isl_int_set_si(v, 6);
283 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
284 bset = isl_basic_set_add_constraint(bset, c);
286 c = isl_equality_alloc(isl_dim_copy(bset->dim));
287 isl_int_set_si(v, -1);
288 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
289 isl_int_set_si(v, 1);
290 isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
291 isl_int_set_si(v, 1);
292 isl_constraint_set_constant(c, 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, 2);
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, -1);
306 isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
307 div = isl_div_alloc(isl_dim_copy(bset->dim));
308 c = isl_constraint_add_div(c, div, &pos);
309 isl_int_set_si(v, -2);
310 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
311 bset = isl_basic_set_add_constraint(bset, c);
313 c = isl_equality_alloc(isl_dim_copy(bset->dim));
314 isl_int_set_si(v, -1);
315 isl_constraint_set_coefficient(c, isl_dim_set, 0, 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, 3);
319 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
320 isl_int_set_si(v, 2);
321 isl_constraint_set_constant(c, v);
322 bset = isl_basic_set_add_constraint(bset, c);
324 bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
326 assert(!isl_basic_set_is_empty(bset));
328 isl_basic_set_free(bset);
331 dim = isl_dim_set_alloc(ctx, 0, 2);
332 bset = isl_basic_set_universe(dim);
334 c = isl_equality_alloc(isl_dim_copy(bset->dim));
335 isl_int_set_si(v, 1);
336 isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
337 div = isl_div_alloc(isl_dim_copy(bset->dim));
338 c = isl_constraint_add_div(c, div, &pos);
339 isl_int_set_si(v, -2);
340 isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
341 bset = isl_basic_set_add_constraint(bset, c);
343 bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
345 isl_basic_set_free(bset);
350 void test_application_case(struct isl_ctx *ctx, const char *name)
352 char filename[PATH_MAX];
355 struct isl_basic_set *bset1, *bset2;
356 struct isl_basic_map *bmap;
358 n = snprintf(filename, sizeof(filename),
359 "%s/test_inputs/%s.omega", srcdir, name);
360 assert(n < sizeof(filename));
361 input = fopen(filename, "r");
364 bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
365 bmap = isl_basic_map_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
367 bset1 = isl_basic_set_apply(bset1, bmap);
369 bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
371 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
373 isl_basic_set_free(bset1);
374 isl_basic_set_free(bset2);
379 void test_application(struct isl_ctx *ctx)
381 test_application_case(ctx, "application");
382 test_application_case(ctx, "application2");
385 void test_affine_hull_case(struct isl_ctx *ctx, const char *name)
387 char filename[PATH_MAX];
390 struct isl_basic_set *bset1, *bset2;
392 n = snprintf(filename, sizeof(filename),
393 "%s/test_inputs/%s.polylib", srcdir, name);
394 assert(n < sizeof(filename));
395 input = fopen(filename, "r");
398 bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
399 bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
401 bset1 = isl_basic_set_affine_hull(bset1);
403 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
405 isl_basic_set_free(bset1);
406 isl_basic_set_free(bset2);
411 void test_affine_hull(struct isl_ctx *ctx)
413 test_affine_hull_case(ctx, "affine2");
414 test_affine_hull_case(ctx, "affine");
415 test_affine_hull_case(ctx, "affine3");
418 void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
420 char filename[PATH_MAX];
423 struct isl_basic_set *bset1, *bset2;
426 n = snprintf(filename, sizeof(filename),
427 "%s/test_inputs/%s.polylib", srcdir, name);
428 assert(n < sizeof(filename));
429 input = fopen(filename, "r");
432 bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
433 bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
435 set = isl_basic_set_union(bset1, bset2);
436 bset1 = isl_set_convex_hull(set);
438 bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
440 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
442 isl_basic_set_free(bset1);
443 isl_basic_set_free(bset2);
448 void test_convex_hull(struct isl_ctx *ctx)
450 test_convex_hull_case(ctx, "convex0");
451 test_convex_hull_case(ctx, "convex1");
452 test_convex_hull_case(ctx, "convex2");
453 test_convex_hull_case(ctx, "convex3");
454 test_convex_hull_case(ctx, "convex4");
455 test_convex_hull_case(ctx, "convex5");
456 test_convex_hull_case(ctx, "convex6");
457 test_convex_hull_case(ctx, "convex7");
458 test_convex_hull_case(ctx, "convex8");
459 test_convex_hull_case(ctx, "convex9");
460 test_convex_hull_case(ctx, "convex10");
461 test_convex_hull_case(ctx, "convex11");
462 test_convex_hull_case(ctx, "convex12");
463 test_convex_hull_case(ctx, "convex13");
464 test_convex_hull_case(ctx, "convex14");
467 void test_gist_case(struct isl_ctx *ctx, const char *name)
469 char filename[PATH_MAX];
472 struct isl_basic_set *bset1, *bset2;
474 n = snprintf(filename, sizeof(filename),
475 "%s/test_inputs/%s.polylib", srcdir, name);
476 assert(n < sizeof(filename));
477 input = fopen(filename, "r");
480 bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
481 bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
483 bset1 = isl_basic_set_gist(bset1, bset2);
485 bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
487 assert(isl_basic_set_is_equal(bset1, bset2) == 1);
489 isl_basic_set_free(bset1);
490 isl_basic_set_free(bset2);
495 void test_gist(struct isl_ctx *ctx)
497 test_gist_case(ctx, "gist1");
500 static struct isl_set *s_union(struct isl_ctx *ctx,
501 const char *s1, const char *s2)
503 struct isl_basic_set *bset1;
504 struct isl_basic_set *bset2;
505 struct isl_set *set1, *set2;
507 bset1 = isl_basic_set_read_from_str(ctx, s1, 0, ISL_FORMAT_OMEGA);
508 bset2 = isl_basic_set_read_from_str(ctx, s2, 0, ISL_FORMAT_OMEGA);
509 set1 = isl_set_from_basic_set(bset1);
510 set2 = isl_set_from_basic_set(bset2);
511 return isl_set_union(set1, set2);
514 void test_coalesce(struct isl_ctx *ctx)
518 set = s_union(ctx, "{[x,y]: x >= 0 & x <= 10 & y >= 0 & y <= 10}",
519 "{[x,y]: y >= x & x >= 2 & 5 >= y}");
520 set = isl_set_coalesce(set);
521 assert(set && set->n == 1);
524 set = s_union(ctx, "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0}",
525 "{[x,y]: x + y >= 10 & y <= x & x + y <= 20 & y >= 0}");
526 set = isl_set_coalesce(set);
527 assert(set && set->n == 1);
530 set = s_union(ctx, "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0}",
531 "{[x,y]: x + y >= 10 & y <= x & x + y <= 19 & y >= 0}");
532 set = isl_set_coalesce(set);
533 assert(set && set->n == 2);
536 set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
537 "{[x,y]: y >= 0 & x >= 6 & x <= 10 & y <= x}");
538 set = isl_set_coalesce(set);
539 assert(set && set->n == 1);
542 set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
543 "{[x,y]: y >= 0 & x >= 7 & x <= 10 & y <= x}");
544 set = isl_set_coalesce(set);
545 assert(set && set->n == 2);
548 set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
549 "{[x,y]: y >= 0 & x >= 6 & x <= 10 & y + 1 <= x}");
550 set = isl_set_coalesce(set);
551 assert(set && set->n == 2);
554 set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
555 "{[x,y]: y >= 0 & x = 6 & y <= 6}");
556 set = isl_set_coalesce(set);
557 assert(set && set->n == 1);
560 set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
561 "{[x,y]: y >= 0 & x = 7 & y <= 6}");
562 set = isl_set_coalesce(set);
563 assert(set && set->n == 2);
566 set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
567 "{[x,y]: y >= 0 & x = 6 & y <= 5}");
568 set = isl_set_coalesce(set);
569 assert(set && set->n == 2);
572 set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
573 "{[x,y]: y >= 0 & x = 6 & y <= 7}");
574 set = isl_set_coalesce(set);
575 assert(set && set->n == 2);
583 srcdir = getenv("srcdir");
586 ctx = isl_ctx_alloc();
588 test_construction(ctx);
590 test_application(ctx);
591 test_affine_hull(ctx);
592 test_convex_hull(ctx);