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
;
475 n
= snprintf(filename
, sizeof(filename
),
476 "%s/test_inputs/%s.polylib", srcdir
, name
);
477 assert(n
< sizeof(filename
));
478 input
= fopen(filename
, "r");
481 bset1
= isl_basic_set_read_from_file(ctx
, input
, 0, ISL_FORMAT_POLYLIB
);
482 bset2
= isl_basic_set_read_from_file(ctx
, input
, 0, ISL_FORMAT_POLYLIB
);
484 bset1
= isl_basic_set_gist(bset1
, bset2
);
486 bset2
= isl_basic_set_read_from_file(ctx
, input
, 0, ISL_FORMAT_POLYLIB
);
488 assert(isl_basic_set_is_equal(bset1
, bset2
) == 1);
490 isl_basic_set_free(bset1
);
491 isl_basic_set_free(bset2
);
496 void test_gist(struct isl_ctx
*ctx
)
498 test_gist_case(ctx
, "gist1");
501 static struct isl_set
*s_union(struct isl_ctx
*ctx
,
502 const char *s1
, const char *s2
)
504 struct isl_basic_set
*bset1
;
505 struct isl_basic_set
*bset2
;
506 struct isl_set
*set1
, *set2
;
508 bset1
= isl_basic_set_read_from_str(ctx
, s1
, 0, ISL_FORMAT_OMEGA
);
509 bset2
= isl_basic_set_read_from_str(ctx
, s2
, 0, ISL_FORMAT_OMEGA
);
510 set1
= isl_set_from_basic_set(bset1
);
511 set2
= isl_set_from_basic_set(bset2
);
512 return isl_set_union(set1
, set2
);
515 void test_coalesce(struct isl_ctx
*ctx
)
519 set
= s_union(ctx
, "{[x,y]: x >= 0 & x <= 10 & y >= 0 & y <= 10}",
520 "{[x,y]: y >= x & x >= 2 & 5 >= y}");
521 set
= isl_set_coalesce(set
);
525 set
= s_union(ctx
, "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0}",
526 "{[x,y]: x + y >= 10 & y <= x & x + y <= 20 & y >= 0}");
527 set
= isl_set_coalesce(set
);
531 set
= s_union(ctx
, "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0}",
532 "{[x,y]: x + y >= 10 & y <= x & x + y <= 19 & y >= 0}");
533 set
= isl_set_coalesce(set
);
537 set
= s_union(ctx
, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
538 "{[x,y]: y >= 0 & x >= 6 & x <= 10 & y <= x}");
539 set
= isl_set_coalesce(set
);
543 set
= s_union(ctx
, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
544 "{[x,y]: y >= 0 & x >= 7 & x <= 10 & y <= x}");
545 set
= isl_set_coalesce(set
);
549 set
= s_union(ctx
, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
550 "{[x,y]: y >= 0 & x >= 6 & x <= 10 & y + 1 <= x}");
551 set
= isl_set_coalesce(set
);
555 set
= s_union(ctx
, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
556 "{[x,y]: y >= 0 & x = 6 & y <= 6}");
557 set
= isl_set_coalesce(set
);
561 set
= s_union(ctx
, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
562 "{[x,y]: y >= 0 & x = 7 & y <= 6}");
563 set
= isl_set_coalesce(set
);
567 set
= s_union(ctx
, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
568 "{[x,y]: y >= 0 & x = 6 & y <= 5}");
569 set
= isl_set_coalesce(set
);
573 set
= s_union(ctx
, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
574 "{[x,y]: y >= 0 & x = 6 & y <= 7}");
575 set
= isl_set_coalesce(set
);
584 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
);