isl_test.c

   1 #include <assert.h>
   2 #include <stdio.h>
   3 #include <limits.h>
   4 #include <isl_ctx.h>
   5 #include <isl_set.h>
   6 #include <isl_constraint.h>
   7
   8 static char *srcdir;
   9
  10 void test_read(struct isl_ctx *ctx)
  11 {
  12         char filename[PATH_MAX];
  13         FILE *input;
  14         int n;
  15         struct isl_basic_set *bset1, *bset2;
  16         const char *str = "{[y]: Exists ( alpha : 2alpha = y)}";
  17
  18         n = snprintf(filename, sizeof(filename),
  19                         "%s/test_inputs/set.omega", srcdir);
  20         assert(n < sizeof(filename));
  21         input = fopen(filename, "r");
  22         assert(input);
  23
  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);
  26
  27         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
  28
  29         isl_basic_set_free(bset1);
  30         isl_basic_set_free(bset2);
  31
  32         fclose(input);
  33 }
  34
  35 /* Construct the basic set { [i] : 5 <= i <= N } */
  36 void test_construction(struct isl_ctx *ctx)
  37 {
  38         isl_int v;
  39         struct isl_dim *dim;
  40         struct isl_basic_set *bset;
  41         struct isl_constraint *c;
  42
  43         isl_int_init(v);
  44
  45         dim = isl_dim_set_alloc(ctx, 1, 1);
  46         bset = isl_basic_set_universe(dim);
  47
  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);
  51         isl_int_set_si(v, 1);
  52         isl_constraint_set_coefficient(c, isl_dim_param, 0, v);
  53         bset = isl_basic_set_add_constraint(bset, c);
  54
  55         c = isl_inequality_alloc(isl_dim_copy(bset->dim));
  56         isl_int_set_si(v, 1);
  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);
  61
  62         isl_basic_set_free(bset);
  63
  64         isl_int_clear(v);
  65 }
  66
  67 void test_div(struct isl_ctx *ctx)
  68 {
  69         isl_int v;
  70         int pos;
  71         struct isl_dim *dim;
  72         struct isl_div *div;
  73         struct isl_basic_set *bset;
  74         struct isl_constraint *c;
  75
  76         isl_int_init(v);
  77
  78         /* test 1 */
  79         dim = isl_dim_set_alloc(ctx, 0, 1);
  80         bset = isl_basic_set_universe(dim);
  81
  82         c = isl_equality_alloc(isl_dim_copy(bset->dim));
  83         isl_int_set_si(v, -1);
  84         isl_constraint_set_constant(c, v);
  85         isl_int_set_si(v, 1);
  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);
  89         isl_int_set_si(v, 3);
  90         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
  91         bset = isl_basic_set_add_constraint(bset, c);
  92
  93         c = isl_equality_alloc(isl_dim_copy(bset->dim));
  94         isl_int_set_si(v, 1);
  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);
 103
 104         assert(bset->n_div == 1);
 105         isl_basic_set_free(bset);
 106
 107         /* test 2 */
 108         dim = isl_dim_set_alloc(ctx, 0, 1);
 109         bset = isl_basic_set_universe(dim);
 110
 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);
 121
 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);
 132
 133         assert(bset->n_div == 1);
 134         isl_basic_set_free(bset);
 135
 136         /* test 3 */
 137         dim = isl_dim_set_alloc(ctx, 0, 1);
 138         bset = isl_basic_set_universe(dim);
 139
 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);
 150
 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);
 161
 162         assert(bset->n_div == 1);
 163         isl_basic_set_free(bset);
 164
 165         /* test 4 */
 166         dim = isl_dim_set_alloc(ctx, 0, 1);
 167         bset = isl_basic_set_universe(dim);
 168
 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);
 179
 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);
 190
 191         assert(isl_basic_set_is_empty(bset));
 192         isl_basic_set_free(bset);
 193
 194         /* test 5 */
 195         dim = isl_dim_set_alloc(ctx, 0, 2);
 196         bset = isl_basic_set_universe(dim);
 197
 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);
 206
 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);
 213
 214         assert(bset->n_div == 0);
 215         isl_basic_set_free(bset);
 216
 217         /* test 6 */
 218         dim = isl_dim_set_alloc(ctx, 0, 2);
 219         bset = isl_basic_set_universe(dim);
 220
 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);
 229
 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);
 236
 237         assert(bset->n_div == 1);
 238         isl_basic_set_free(bset);
 239
 240         /* test 7 */
 241         /* This test is a bit tricky.  We set up an equality
 242          *              a + 3b + 3c = 6 e0
 243          * Normalization of divs creates _two_ divs
 244          *              a = 3 e0
 245          *              c - b - e0 = 2 e1
 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.
 249          */
 250         dim = isl_dim_set_alloc(ctx, 0, 3);
 251         bset = isl_basic_set_universe(dim);
 252
 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);
 265
 266         assert(bset->n_div == 1);
 267         isl_basic_set_free(bset);
 268
 269         /* test 8 */
 270         dim = isl_dim_set_alloc(ctx, 0, 4);
 271         bset = isl_basic_set_universe(dim);
 272
 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);
 285
 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);
 294
 295         assert(bset->n_div == 1);
 296         isl_basic_set_free(bset);
 297
 298         /* test 9 */
 299         dim = isl_dim_set_alloc(ctx, 0, 2);
 300         bset = isl_basic_set_universe(dim);
 301
 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);
 312
 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);
 323
 324         bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
 325
 326         assert(!isl_basic_set_is_empty(bset));
 327
 328         isl_basic_set_free(bset);
 329
 330         /* test 10 */
 331         dim = isl_dim_set_alloc(ctx, 0, 2);
 332         bset = isl_basic_set_universe(dim);
 333
 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);
 342
 343         bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
 344
 345         isl_basic_set_free(bset);
 346
 347         isl_int_clear(v);
 348 }
 349
 350 void test_application_case(struct isl_ctx *ctx, const char *name)
 351 {
 352         char filename[PATH_MAX];
 353         FILE *input;
 354         int n;
 355         struct isl_basic_set *bset1, *bset2;
 356         struct isl_basic_map *bmap;
 357
 358         n = snprintf(filename, sizeof(filename),
 359                         "%s/test_inputs/%s.omega", srcdir, name);
 360         assert(n < sizeof(filename));
 361         input = fopen(filename, "r");
 362         assert(input);
 363
 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);
 366
 367         bset1 = isl_basic_set_apply(bset1, bmap);
 368
 369         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
 370
 371         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 372
 373         isl_basic_set_free(bset1);
 374         isl_basic_set_free(bset2);
 375
 376         fclose(input);
 377 }
 378
 379 void test_application(struct isl_ctx *ctx)
 380 {
 381         test_application_case(ctx, "application");
 382         test_application_case(ctx, "application2");
 383 }
 384
 385 void test_affine_hull_case(struct isl_ctx *ctx, const char *name)
 386 {
 387         char filename[PATH_MAX];
 388         FILE *input;
 389         int n;
 390         struct isl_basic_set *bset1, *bset2;
 391
 392         n = snprintf(filename, sizeof(filename),
 393                         "%s/test_inputs/%s.polylib", srcdir, name);
 394         assert(n < sizeof(filename));
 395         input = fopen(filename, "r");
 396         assert(input);
 397
 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);
 400
 401         bset1 = isl_basic_set_affine_hull(bset1);
 402
 403         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 404
 405         isl_basic_set_free(bset1);
 406         isl_basic_set_free(bset2);
 407
 408         fclose(input);
 409 }
 410
 411 void test_affine_hull(struct isl_ctx *ctx)
 412 {
 413         test_affine_hull_case(ctx, "affine2");
 414         test_affine_hull_case(ctx, "affine");
 415 }
 416
 417 void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
 418 {
 419         char filename[PATH_MAX];
 420         FILE *input;
 421         int n;
 422         struct isl_basic_set *bset1, *bset2;
 423         struct isl_set *set;
 424
 425         n = snprintf(filename, sizeof(filename),
 426                         "%s/test_inputs/%s.polylib", srcdir, name);
 427         assert(n < sizeof(filename));
 428         input = fopen(filename, "r");
 429         assert(input);
 430
 431         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 432         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 433
 434         set = isl_basic_set_union(bset1, bset2);
 435         bset1 = isl_set_convex_hull(set);
 436
 437         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 438
 439         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 440
 441         isl_basic_set_free(bset1);
 442         isl_basic_set_free(bset2);
 443
 444         fclose(input);
 445 }
 446
 447 void test_convex_hull(struct isl_ctx *ctx)
 448 {
 449         test_convex_hull_case(ctx, "convex0");
 450         test_convex_hull_case(ctx, "convex1");
 451         test_convex_hull_case(ctx, "convex2");
 452         test_convex_hull_case(ctx, "convex3");
 453         test_convex_hull_case(ctx, "convex4");
 454         test_convex_hull_case(ctx, "convex5");
 455         test_convex_hull_case(ctx, "convex6");
 456         test_convex_hull_case(ctx, "convex7");
 457         test_convex_hull_case(ctx, "convex8");
 458         test_convex_hull_case(ctx, "convex9");
 459         test_convex_hull_case(ctx, "convex10");
 460         test_convex_hull_case(ctx, "convex11");
 461 }
 462
 463 void test_gist_case(struct isl_ctx *ctx, const char *name)
 464 {
 465         char filename[PATH_MAX];
 466         FILE *input;
 467         int n;
 468         struct isl_basic_set *bset1, *bset2;
 469         struct isl_set *set;
 470
 471         n = snprintf(filename, sizeof(filename),
 472                         "%s/test_inputs/%s.polylib", srcdir, name);
 473         assert(n < sizeof(filename));
 474         input = fopen(filename, "r");
 475         assert(input);
 476
 477         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 478         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 479
 480         bset1 = isl_basic_set_gist(bset1, bset2);
 481
 482         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 483
 484         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 485
 486         isl_basic_set_free(bset1);
 487         isl_basic_set_free(bset2);
 488
 489         fclose(input);
 490 }
 491
 492 void test_gist(struct isl_ctx *ctx)
 493 {
 494         test_gist_case(ctx, "gist1");
 495 }
 496
 497 int main()
 498 {
 499         struct isl_ctx *ctx;
 500
 501         srcdir = getenv("srcdir");
 502
 503         ctx = isl_ctx_alloc();
 504         test_read(ctx);
 505         test_construction(ctx);
 506         test_div(ctx);
 507         test_application(ctx);
 508         test_affine_hull(ctx);
 509         test_convex_hull(ctx);
 510         test_gist(ctx);
 511         isl_ctx_free(ctx);
 512         return 0;
 513 }