isl_test.c

   1 /*
   2  * Copyright 2008-2009 Katholieke Universiteit Leuven
   3  *
   4  * Use of this software is governed by the GNU LGPLv2.1 license
   5  *
   6  * Written by Sven Verdoolaege, K.U.Leuven, Departement
   7  * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
   8  */
   9
  10 #include <assert.h>
  11 #include <stdio.h>
  12 #include <limits.h>
  13 #include <isl_ctx.h>
  14 #include <isl_set.h>
  15 #include <isl_flow.h>
  16 #include <isl_constraint.h>
  17 #include <isl_polynomial.h>
  18
  19 static char *srcdir;
  20
  21 void test_read(struct isl_ctx *ctx)
  22 {
  23         char filename[PATH_MAX];
  24         FILE *input;
  25         int n;
  26         struct isl_basic_set *bset1, *bset2;
  27         const char *str = "{[y]: Exists ( alpha : 2alpha = y)}";
  28
  29         n = snprintf(filename, sizeof(filename),
  30                         "%s/test_inputs/set.omega", srcdir);
  31         assert(n < sizeof(filename));
  32         input = fopen(filename, "r");
  33         assert(input);
  34
  35         bset1 = isl_basic_set_read_from_file(ctx, input, 0);
  36         bset2 = isl_basic_set_read_from_str(ctx, str, 0);
  37
  38         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
  39
  40         isl_basic_set_free(bset1);
  41         isl_basic_set_free(bset2);
  42
  43         fclose(input);
  44 }
  45
  46 void test_bounded(struct isl_ctx *ctx)
  47 {
  48         isl_set *set;
  49         int bounded;
  50
  51         set = isl_set_read_from_str(ctx, "[n] -> {[i] : 0 <= i <= n }", -1);
  52         bounded = isl_set_is_bounded(set);
  53         assert(bounded);
  54         isl_set_free(set);
  55
  56         set = isl_set_read_from_str(ctx, "{[n, i] : 0 <= i <= n }", -1);
  57         bounded = isl_set_is_bounded(set);
  58         assert(!bounded);
  59         isl_set_free(set);
  60
  61         set = isl_set_read_from_str(ctx, "[n] -> {[i] : i <= n }", -1);
  62         bounded = isl_set_is_bounded(set);
  63         assert(!bounded);
  64         isl_set_free(set);
  65 }
  66
  67 /* Construct the basic set { [i] : 5 <= i <= N } */
  68 void test_construction(struct isl_ctx *ctx)
  69 {
  70         isl_int v;
  71         struct isl_dim *dim;
  72         struct isl_basic_set *bset;
  73         struct isl_constraint *c;
  74
  75         isl_int_init(v);
  76
  77         dim = isl_dim_set_alloc(ctx, 1, 1);
  78         bset = isl_basic_set_universe(dim);
  79
  80         c = isl_inequality_alloc(isl_basic_set_get_dim(bset));
  81         isl_int_set_si(v, -1);
  82         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
  83         isl_int_set_si(v, 1);
  84         isl_constraint_set_coefficient(c, isl_dim_param, 0, v);
  85         bset = isl_basic_set_add_constraint(bset, c);
  86
  87         c = isl_inequality_alloc(isl_basic_set_get_dim(bset));
  88         isl_int_set_si(v, 1);
  89         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
  90         isl_int_set_si(v, -5);
  91         isl_constraint_set_constant(c, v);
  92         bset = isl_basic_set_add_constraint(bset, c);
  93
  94         isl_basic_set_free(bset);
  95
  96         isl_int_clear(v);
  97 }
  98
  99 void test_dim(struct isl_ctx *ctx)
 100 {
 101         const char *str;
 102         isl_map *map1, *map2;
 103
 104         map1 = isl_map_read_from_str(ctx,
 105             "[n] -> { [i] -> [j] : exists (a = [i/10] : i - 10a <= n ) }", -1);
 106         map1 = isl_map_add(map1, isl_dim_in, 1);
 107         map2 = isl_map_read_from_str(ctx,
 108             "[n] -> { [i,k] -> [j] : exists (a = [i/10] : i - 10a <= n ) }", -1);
 109         assert(isl_map_is_equal(map1, map2));
 110         isl_map_free(map2);
 111
 112         map1 = isl_map_project_out(map1, isl_dim_in, 0, 1);
 113         map2 = isl_map_read_from_str(ctx, "[n] -> { [i] -> [j] : n >= 0 }", -1);
 114         assert(isl_map_is_equal(map1, map2));
 115
 116         isl_map_free(map1);
 117         isl_map_free(map2);
 118
 119         str = "[n] -> { [i] -> [] : exists a : 0 <= i <= n and i = 2 a }";
 120         map1 = isl_map_read_from_str(ctx, str, -1);
 121         str = "{ [i] -> [j] : exists a : 0 <= i <= j and i = 2 a }";
 122         map2 = isl_map_read_from_str(ctx, str, -1);
 123         map1 = isl_map_move_dims(map1, isl_dim_out, 0, isl_dim_param, 0, 1);
 124         assert(isl_map_is_equal(map1, map2));
 125
 126         isl_map_free(map1);
 127         isl_map_free(map2);
 128 }
 129
 130 void test_div(struct isl_ctx *ctx)
 131 {
 132         isl_int v;
 133         int pos;
 134         struct isl_dim *dim;
 135         struct isl_div *div;
 136         struct isl_basic_set *bset;
 137         struct isl_constraint *c;
 138
 139         isl_int_init(v);
 140
 141         /* test 1 */
 142         dim = isl_dim_set_alloc(ctx, 0, 1);
 143         bset = isl_basic_set_universe(dim);
 144
 145         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 146         isl_int_set_si(v, -1);
 147         isl_constraint_set_constant(c, v);
 148         isl_int_set_si(v, 1);
 149         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 150         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 151         c = isl_constraint_add_div(c, div, &pos);
 152         isl_int_set_si(v, 3);
 153         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 154         bset = isl_basic_set_add_constraint(bset, c);
 155
 156         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 157         isl_int_set_si(v, 1);
 158         isl_constraint_set_constant(c, v);
 159         isl_int_set_si(v, -1);
 160         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 161         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 162         c = isl_constraint_add_div(c, div, &pos);
 163         isl_int_set_si(v, 3);
 164         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 165         bset = isl_basic_set_add_constraint(bset, c);
 166
 167         assert(bset && bset->n_div == 1);
 168         isl_basic_set_free(bset);
 169
 170         /* test 2 */
 171         dim = isl_dim_set_alloc(ctx, 0, 1);
 172         bset = isl_basic_set_universe(dim);
 173
 174         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 175         isl_int_set_si(v, 1);
 176         isl_constraint_set_constant(c, v);
 177         isl_int_set_si(v, -1);
 178         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 179         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 180         c = isl_constraint_add_div(c, div, &pos);
 181         isl_int_set_si(v, 3);
 182         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 183         bset = isl_basic_set_add_constraint(bset, c);
 184
 185         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 186         isl_int_set_si(v, -1);
 187         isl_constraint_set_constant(c, v);
 188         isl_int_set_si(v, 1);
 189         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 190         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 191         c = isl_constraint_add_div(c, div, &pos);
 192         isl_int_set_si(v, 3);
 193         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 194         bset = isl_basic_set_add_constraint(bset, c);
 195
 196         assert(bset && bset->n_div == 1);
 197         isl_basic_set_free(bset);
 198
 199         /* test 3 */
 200         dim = isl_dim_set_alloc(ctx, 0, 1);
 201         bset = isl_basic_set_universe(dim);
 202
 203         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 204         isl_int_set_si(v, 1);
 205         isl_constraint_set_constant(c, v);
 206         isl_int_set_si(v, -1);
 207         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 208         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 209         c = isl_constraint_add_div(c, div, &pos);
 210         isl_int_set_si(v, 3);
 211         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 212         bset = isl_basic_set_add_constraint(bset, c);
 213
 214         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 215         isl_int_set_si(v, -3);
 216         isl_constraint_set_constant(c, v);
 217         isl_int_set_si(v, 1);
 218         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 219         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 220         c = isl_constraint_add_div(c, div, &pos);
 221         isl_int_set_si(v, 4);
 222         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 223         bset = isl_basic_set_add_constraint(bset, c);
 224
 225         assert(bset && bset->n_div == 1);
 226         isl_basic_set_free(bset);
 227
 228         /* test 4 */
 229         dim = isl_dim_set_alloc(ctx, 0, 1);
 230         bset = isl_basic_set_universe(dim);
 231
 232         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 233         isl_int_set_si(v, 2);
 234         isl_constraint_set_constant(c, v);
 235         isl_int_set_si(v, -1);
 236         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 237         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 238         c = isl_constraint_add_div(c, div, &pos);
 239         isl_int_set_si(v, 3);
 240         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 241         bset = isl_basic_set_add_constraint(bset, c);
 242
 243         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 244         isl_int_set_si(v, -1);
 245         isl_constraint_set_constant(c, v);
 246         isl_int_set_si(v, 1);
 247         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 248         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 249         c = isl_constraint_add_div(c, div, &pos);
 250         isl_int_set_si(v, 6);
 251         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 252         bset = isl_basic_set_add_constraint(bset, c);
 253
 254         assert(isl_basic_set_is_empty(bset));
 255         isl_basic_set_free(bset);
 256
 257         /* test 5 */
 258         dim = isl_dim_set_alloc(ctx, 0, 2);
 259         bset = isl_basic_set_universe(dim);
 260
 261         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 262         isl_int_set_si(v, -1);
 263         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 264         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 265         c = isl_constraint_add_div(c, div, &pos);
 266         isl_int_set_si(v, 3);
 267         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 268         bset = isl_basic_set_add_constraint(bset, c);
 269
 270         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 271         isl_int_set_si(v, 1);
 272         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 273         isl_int_set_si(v, -3);
 274         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 275         bset = isl_basic_set_add_constraint(bset, c);
 276
 277         assert(bset && bset->n_div == 0);
 278         isl_basic_set_free(bset);
 279
 280         /* test 6 */
 281         dim = isl_dim_set_alloc(ctx, 0, 2);
 282         bset = isl_basic_set_universe(dim);
 283
 284         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 285         isl_int_set_si(v, -1);
 286         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 287         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 288         c = isl_constraint_add_div(c, div, &pos);
 289         isl_int_set_si(v, 6);
 290         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 291         bset = isl_basic_set_add_constraint(bset, c);
 292
 293         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 294         isl_int_set_si(v, 1);
 295         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 296         isl_int_set_si(v, -3);
 297         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 298         bset = isl_basic_set_add_constraint(bset, c);
 299
 300         assert(bset && bset->n_div == 1);
 301         isl_basic_set_free(bset);
 302
 303         /* test 7 */
 304         /* This test is a bit tricky.  We set up an equality
 305          *              a + 3b + 3c = 6 e0
 306          * Normalization of divs creates _two_ divs
 307          *              a = 3 e0
 308          *              c - b - e0 = 2 e1
 309          * Afterwards e0 is removed again because it has coefficient -1
 310          * and we end up with the original equality and div again.
 311          * Perhaps we can avoid the introduction of this temporary div.
 312          */
 313         dim = isl_dim_set_alloc(ctx, 0, 3);
 314         bset = isl_basic_set_universe(dim);
 315
 316         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 317         isl_int_set_si(v, -1);
 318         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 319         isl_int_set_si(v, -3);
 320         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 321         isl_int_set_si(v, -3);
 322         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 323         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 324         c = isl_constraint_add_div(c, div, &pos);
 325         isl_int_set_si(v, 6);
 326         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 327         bset = isl_basic_set_add_constraint(bset, c);
 328
 329         /* Test disabled for now */
 330         /*
 331         assert(bset && bset->n_div == 1);
 332         */
 333         isl_basic_set_free(bset);
 334
 335         /* test 8 */
 336         dim = isl_dim_set_alloc(ctx, 0, 4);
 337         bset = isl_basic_set_universe(dim);
 338
 339         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 340         isl_int_set_si(v, -1);
 341         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 342         isl_int_set_si(v, -3);
 343         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 344         isl_int_set_si(v, -3);
 345         isl_constraint_set_coefficient(c, isl_dim_set, 3, v);
 346         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 347         c = isl_constraint_add_div(c, div, &pos);
 348         isl_int_set_si(v, 6);
 349         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 350         bset = isl_basic_set_add_constraint(bset, c);
 351
 352         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 353         isl_int_set_si(v, -1);
 354         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 355         isl_int_set_si(v, 1);
 356         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 357         isl_int_set_si(v, 1);
 358         isl_constraint_set_constant(c, v);
 359         bset = isl_basic_set_add_constraint(bset, c);
 360
 361         /* Test disabled for now */
 362         /*
 363         assert(bset && bset->n_div == 1);
 364         */
 365         isl_basic_set_free(bset);
 366
 367         /* test 9 */
 368         dim = isl_dim_set_alloc(ctx, 0, 2);
 369         bset = isl_basic_set_universe(dim);
 370
 371         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 372         isl_int_set_si(v, 1);
 373         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 374         isl_int_set_si(v, -1);
 375         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 376         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 377         c = isl_constraint_add_div(c, div, &pos);
 378         isl_int_set_si(v, -2);
 379         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 380         bset = isl_basic_set_add_constraint(bset, c);
 381
 382         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 383         isl_int_set_si(v, -1);
 384         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 385         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 386         c = isl_constraint_add_div(c, div, &pos);
 387         isl_int_set_si(v, 3);
 388         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 389         isl_int_set_si(v, 2);
 390         isl_constraint_set_constant(c, v);
 391         bset = isl_basic_set_add_constraint(bset, c);
 392
 393         bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
 394
 395         assert(!isl_basic_set_is_empty(bset));
 396
 397         isl_basic_set_free(bset);
 398
 399         /* test 10 */
 400         dim = isl_dim_set_alloc(ctx, 0, 2);
 401         bset = isl_basic_set_universe(dim);
 402
 403         c = isl_equality_alloc(isl_basic_set_get_dim(bset));
 404         isl_int_set_si(v, 1);
 405         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 406         div = isl_div_alloc(isl_basic_set_get_dim(bset));
 407         c = isl_constraint_add_div(c, div, &pos);
 408         isl_int_set_si(v, -2);
 409         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 410         bset = isl_basic_set_add_constraint(bset, c);
 411
 412         bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
 413
 414         isl_basic_set_free(bset);
 415
 416         isl_int_clear(v);
 417 }
 418
 419 void test_application_case(struct isl_ctx *ctx, const char *name)
 420 {
 421         char filename[PATH_MAX];
 422         FILE *input;
 423         int n;
 424         struct isl_basic_set *bset1, *bset2;
 425         struct isl_basic_map *bmap;
 426
 427         n = snprintf(filename, sizeof(filename),
 428                         "%s/test_inputs/%s.omega", srcdir, name);
 429         assert(n < sizeof(filename));
 430         input = fopen(filename, "r");
 431         assert(input);
 432
 433         bset1 = isl_basic_set_read_from_file(ctx, input, 0);
 434         bmap = isl_basic_map_read_from_file(ctx, input, 0);
 435
 436         bset1 = isl_basic_set_apply(bset1, bmap);
 437
 438         bset2 = isl_basic_set_read_from_file(ctx, input, 0);
 439
 440         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 441
 442         isl_basic_set_free(bset1);
 443         isl_basic_set_free(bset2);
 444
 445         fclose(input);
 446 }
 447
 448 void test_application(struct isl_ctx *ctx)
 449 {
 450         test_application_case(ctx, "application");
 451         test_application_case(ctx, "application2");
 452 }
 453
 454 void test_affine_hull_case(struct isl_ctx *ctx, const char *name)
 455 {
 456         char filename[PATH_MAX];
 457         FILE *input;
 458         int n;
 459         struct isl_basic_set *bset1, *bset2;
 460
 461         n = snprintf(filename, sizeof(filename),
 462                         "%s/test_inputs/%s.polylib", srcdir, name);
 463         assert(n < sizeof(filename));
 464         input = fopen(filename, "r");
 465         assert(input);
 466
 467         bset1 = isl_basic_set_read_from_file(ctx, input, 0);
 468         bset2 = isl_basic_set_read_from_file(ctx, input, 0);
 469
 470         bset1 = isl_basic_set_affine_hull(bset1);
 471
 472         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 473
 474         isl_basic_set_free(bset1);
 475         isl_basic_set_free(bset2);
 476
 477         fclose(input);
 478 }
 479
 480 void test_affine_hull(struct isl_ctx *ctx)
 481 {
 482         test_affine_hull_case(ctx, "affine2");
 483         test_affine_hull_case(ctx, "affine");
 484         test_affine_hull_case(ctx, "affine3");
 485 }
 486
 487 void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
 488 {
 489         char filename[PATH_MAX];
 490         FILE *input;
 491         int n;
 492         struct isl_basic_set *bset1, *bset2;
 493         struct isl_set *set;
 494
 495         n = snprintf(filename, sizeof(filename),
 496                         "%s/test_inputs/%s.polylib", srcdir, name);
 497         assert(n < sizeof(filename));
 498         input = fopen(filename, "r");
 499         assert(input);
 500
 501         bset1 = isl_basic_set_read_from_file(ctx, input, 0);
 502         bset2 = isl_basic_set_read_from_file(ctx, input, 0);
 503
 504         set = isl_basic_set_union(bset1, bset2);
 505         bset1 = isl_set_convex_hull(set);
 506
 507         bset2 = isl_basic_set_read_from_file(ctx, input, 0);
 508
 509         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 510
 511         isl_basic_set_free(bset1);
 512         isl_basic_set_free(bset2);
 513
 514         fclose(input);
 515 }
 516
 517 void test_convex_hull(struct isl_ctx *ctx)
 518 {
 519         const char *str1, *str2;
 520         isl_set *set1, *set2;
 521
 522         test_convex_hull_case(ctx, "convex0");
 523         test_convex_hull_case(ctx, "convex1");
 524         test_convex_hull_case(ctx, "convex2");
 525         test_convex_hull_case(ctx, "convex3");
 526         test_convex_hull_case(ctx, "convex4");
 527         test_convex_hull_case(ctx, "convex5");
 528         test_convex_hull_case(ctx, "convex6");
 529         test_convex_hull_case(ctx, "convex7");
 530         test_convex_hull_case(ctx, "convex8");
 531         test_convex_hull_case(ctx, "convex9");
 532         test_convex_hull_case(ctx, "convex10");
 533         test_convex_hull_case(ctx, "convex11");
 534         test_convex_hull_case(ctx, "convex12");
 535         test_convex_hull_case(ctx, "convex13");
 536         test_convex_hull_case(ctx, "convex14");
 537         test_convex_hull_case(ctx, "convex15");
 538
 539         str1 = "{ [i0, i1, i2] : (i2 = 1 and i0 = 0 and i1 >= 0) or "
 540                "(i0 = 1 and i1 = 0 and i2 = 1) or "
 541                "(i0 = 0 and i1 = 0 and i2 = 0) }";
 542         str2 = "{ [i0, i1, i2] : i0 >= 0 and i2 >= i0 and i2 <= 1 and i1 >= 0 }";
 543         set1 = isl_set_read_from_str(ctx, str1, -1);
 544         set2 = isl_set_read_from_str(ctx, str2, -1);
 545         set1 = isl_set_from_basic_set(isl_set_convex_hull(set1));
 546         assert(isl_set_is_equal(set1, set2));
 547         isl_set_free(set1);
 548         isl_set_free(set2);
 549 }
 550
 551 void test_gist_case(struct isl_ctx *ctx, const char *name)
 552 {
 553         char filename[PATH_MAX];
 554         FILE *input;
 555         int n;
 556         struct isl_basic_set *bset1, *bset2;
 557
 558         n = snprintf(filename, sizeof(filename),
 559                         "%s/test_inputs/%s.polylib", srcdir, name);
 560         assert(n < sizeof(filename));
 561         input = fopen(filename, "r");
 562         assert(input);
 563
 564         bset1 = isl_basic_set_read_from_file(ctx, input, 0);
 565         bset2 = isl_basic_set_read_from_file(ctx, input, 0);
 566
 567         bset1 = isl_basic_set_gist(bset1, bset2);
 568
 569         bset2 = isl_basic_set_read_from_file(ctx, input, 0);
 570
 571         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 572
 573         isl_basic_set_free(bset1);
 574         isl_basic_set_free(bset2);
 575
 576         fclose(input);
 577 }
 578
 579 void test_gist(struct isl_ctx *ctx)
 580 {
 581         test_gist_case(ctx, "gist1");
 582 }
 583
 584 void test_coalesce_set(isl_ctx *ctx, const char *str, int check_one)
 585 {
 586         isl_set *set, *set2;
 587
 588         set = isl_set_read_from_str(ctx, str, -1);
 589         set = isl_set_coalesce(set);
 590         set2 = isl_set_read_from_str(ctx, str, -1);
 591         assert(isl_set_is_equal(set, set2));
 592         if (check_one)
 593                 assert(set && set->n == 1);
 594         isl_set_free(set);
 595         isl_set_free(set2);
 596 }
 597
 598 void test_coalesce(struct isl_ctx *ctx)
 599 {
 600         const char *str;
 601         struct isl_set *set, *set2;
 602         struct isl_map *map, *map2;
 603
 604         set = isl_set_read_from_str(ctx,
 605                 "{[x,y]: x >= 0 & x <= 10 & y >= 0 & y <= 10 or "
 606                        "y >= x & x >= 2 & 5 >= y }", -1);
 607         set = isl_set_coalesce(set);
 608         assert(set && set->n == 1);
 609         isl_set_free(set);
 610
 611         set = isl_set_read_from_str(ctx,
 612                 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
 613                        "x + y >= 10 & y <= x & x + y <= 20 & y >= 0}", -1);
 614         set = isl_set_coalesce(set);
 615         assert(set && set->n == 1);
 616         isl_set_free(set);
 617
 618         set = isl_set_read_from_str(ctx,
 619                 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
 620                        "x + y >= 10 & y <= x & x + y <= 19 & y >= 0}", -1);
 621         set = isl_set_coalesce(set);
 622         assert(set && set->n == 2);
 623         isl_set_free(set);
 624
 625         set = isl_set_read_from_str(ctx,
 626                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 627                        "y >= 0 & x >= 6 & x <= 10 & y <= x}", -1);
 628         set = isl_set_coalesce(set);
 629         assert(set && set->n == 1);
 630         isl_set_free(set);
 631
 632         set = isl_set_read_from_str(ctx,
 633                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 634                        "y >= 0 & x >= 7 & x <= 10 & y <= x}", -1);
 635         set = isl_set_coalesce(set);
 636         assert(set && set->n == 2);
 637         isl_set_free(set);
 638
 639         set = isl_set_read_from_str(ctx,
 640                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 641                        "y >= 0 & x >= 6 & x <= 10 & y + 1 <= x}", -1);
 642         set = isl_set_coalesce(set);
 643         assert(set && set->n == 2);
 644         isl_set_free(set);
 645
 646         set = isl_set_read_from_str(ctx,
 647                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 648                        "y >= 0 & x = 6 & y <= 6}", -1);
 649         set = isl_set_coalesce(set);
 650         assert(set && set->n == 1);
 651         isl_set_free(set);
 652
 653         set = isl_set_read_from_str(ctx,
 654                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 655                        "y >= 0 & x = 7 & y <= 6}", -1);
 656         set = isl_set_coalesce(set);
 657         assert(set && set->n == 2);
 658         isl_set_free(set);
 659
 660         set = isl_set_read_from_str(ctx,
 661                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 662                        "y >= 0 & x = 6 & y <= 5}", -1);
 663         set = isl_set_coalesce(set);
 664         assert(set && set->n == 1);
 665         set2 = isl_set_read_from_str(ctx,
 666                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 667                        "y >= 0 & x = 6 & y <= 5}", -1);
 668         assert(isl_set_is_equal(set, set2));
 669         isl_set_free(set);
 670         isl_set_free(set2);
 671
 672         set = isl_set_read_from_str(ctx,
 673                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 674                        "y >= 0 & x = 6 & y <= 7}", -1);
 675         set = isl_set_coalesce(set);
 676         assert(set && set->n == 2);
 677         isl_set_free(set);
 678
 679         set = isl_set_read_from_str(ctx,
 680                 "[n] -> { [i] : i = 1 and n >= 2 or 2 <= i and i <= n }", -1);
 681         set = isl_set_coalesce(set);
 682         assert(set && set->n == 1);
 683         set2 = isl_set_read_from_str(ctx,
 684                 "[n] -> { [i] : i = 1 and n >= 2 or 2 <= i and i <= n }", -1);
 685         assert(isl_set_is_equal(set, set2));
 686         isl_set_free(set);
 687         isl_set_free(set2);
 688
 689         set = isl_set_read_from_str(ctx,
 690                 "{[x,y] : x >= 0 and y >= 0 or 0 <= y and y <= 5 and x = -1}", -1);
 691         set = isl_set_coalesce(set);
 692         set2 = isl_set_read_from_str(ctx,
 693                 "{[x,y] : x >= 0 and y >= 0 or 0 <= y and y <= 5 and x = -1}", -1);
 694         assert(isl_set_is_equal(set, set2));
 695         isl_set_free(set);
 696         isl_set_free(set2);
 697
 698         set = isl_set_read_from_str(ctx,
 699                 "[n] -> { [i] : 1 <= i and i <= n - 1 or "
 700                                 "2 <= i and i <= n }", -1);
 701         set = isl_set_coalesce(set);
 702         assert(set && set->n == 1);
 703         set2 = isl_set_read_from_str(ctx,
 704                 "[n] -> { [i] : 1 <= i and i <= n - 1 or "
 705                                 "2 <= i and i <= n }", -1);
 706         assert(isl_set_is_equal(set, set2));
 707         isl_set_free(set);
 708         isl_set_free(set2);
 709
 710         map = isl_map_read_from_str(ctx,
 711                 "[n] -> { [i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
 712                 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
 713                 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
 714                 "4e4 = -2 + o0 and i0 >= 8 + 2n and o0 >= 2 + i0 and "
 715                 "o0 <= 56 + 2n and o0 <= -12 + 4n and i0 <= 57 + 2n and "
 716                 "i0 <= -11 + 4n and o0 >= 6 + 2n and 4e0 <= i0 and "
 717                 "4e0 >= -3 + i0 and 4e1 <= o0 and 4e1 >= -3 + o0 and "
 718                 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0);"
 719                 "[i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
 720                 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
 721                 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
 722                 "4e4 = -2 + o0 and 2e0 >= 3 + n and e0 <= -4 + n and "
 723                 "2e0 <= 27 + n and e1 <= -4 + n and 2e1 <= 27 + n and "
 724                 "2e1 >= 2 + n and e1 >= 1 + e0 and i0 >= 7 + 2n and "
 725                 "i0 <= -11 + 4n and i0 <= 57 + 2n and 4e0 <= -2 + i0 and "
 726                 "4e0 >= -3 + i0 and o0 >= 6 + 2n and o0 <= -11 + 4n and "
 727                 "o0 <= 57 + 2n and 4e1 <= -2 + o0 and 4e1 >= -3 + o0 and "
 728                 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0 ) }", -1);
 729         map = isl_map_coalesce(map);
 730         map2 = isl_map_read_from_str(ctx,
 731                 "[n] -> { [i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
 732                 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
 733                 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
 734                 "4e4 = -2 + o0 and i0 >= 8 + 2n and o0 >= 2 + i0 and "
 735                 "o0 <= 56 + 2n and o0 <= -12 + 4n and i0 <= 57 + 2n and "
 736                 "i0 <= -11 + 4n and o0 >= 6 + 2n and 4e0 <= i0 and "
 737                 "4e0 >= -3 + i0 and 4e1 <= o0 and 4e1 >= -3 + o0 and "
 738                 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0);"
 739                 "[i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
 740                 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
 741                 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
 742                 "4e4 = -2 + o0 and 2e0 >= 3 + n and e0 <= -4 + n and "
 743                 "2e0 <= 27 + n and e1 <= -4 + n and 2e1 <= 27 + n and "
 744                 "2e1 >= 2 + n and e1 >= 1 + e0 and i0 >= 7 + 2n and "
 745                 "i0 <= -11 + 4n and i0 <= 57 + 2n and 4e0 <= -2 + i0 and "
 746                 "4e0 >= -3 + i0 and o0 >= 6 + 2n and o0 <= -11 + 4n and "
 747                 "o0 <= 57 + 2n and 4e1 <= -2 + o0 and 4e1 >= -3 + o0 and "
 748                 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0 ) }", -1);
 749         assert(isl_map_is_equal(map, map2));
 750         isl_map_free(map);
 751         isl_map_free(map2);
 752
 753         str = "[n, m] -> { [] -> [o0, o2, o3] : (o3 = 1 and o0 >= 1 + m and "
 754               "o0 <= n + m and o2 <= m and o0 >= 2 + n and o2 >= 3) or "
 755               "(o0 >= 2 + n and o0 >= 1 + m and o0 <= n + m and n >= 1 and "
 756               "o3 <= -1 + o2 and o3 >= 1 - m + o2 and o3 >= 2 and o3 <= n) }";
 757         map = isl_map_read_from_str(ctx, str, -1);
 758         map = isl_map_coalesce(map);
 759         map2 = isl_map_read_from_str(ctx, str, -1);
 760         assert(isl_map_is_equal(map, map2));
 761         isl_map_free(map);
 762         isl_map_free(map2);
 763
 764         str = "[M, N] -> { [i0, i1, i2, i3, i4, i5, i6] -> "
 765           "[o0, o1, o2, o3, o4, o5, o6] : "
 766           "(o6 <= -4 + 2M - 2N + i0 + i1 - i2 + i6 - o0 - o1 + o2 and "
 767           "o3 <= -2 + i3 and o6 >= 2 + i0 + i3 + i6 - o0 - o3 and "
 768           "o6 >= 2 - M + N + i3 + i4 + i6 - o3 - o4 and o0 <= -1 + i0 and "
 769           "o4 >= 4 - 3M + 3N - i0 - i1 + i2 + 2i3 + i4 + o0 + o1 - o2 - 2o3 "
 770           "and o6 <= -3 + 2M - 2N + i3 + i4 - i5 + i6 - o3 - o4 + o5 and "
 771           "2o6 <= -5 + 5M - 5N + 2i0 + i1 - i2 - i5 + 2i6 - 2o0 - o1 + o2 + o5 "
 772           "and o6 >= 2i0 + i1 + i6 - 2o0 - o1 and "
 773           "3o6 <= -5 + 4M - 4N + 2i0 + i1 - i2 + 2i3 + i4 - i5 + 3i6 "
 774           "- 2o0 - o1 + o2 - 2o3 - o4 + o5) or "
 775           "(N >= 2 and o3 <= -1 + i3 and o0 <= -1 + i0 and "
 776           "o6 >= i3 + i6 - o3 and M >= 0 and "
 777           "2o6 >= 1 + i0 + i3 + 2i6 - o0 - o3 and "
 778           "o6 >= 1 - M + i0 + i6 - o0 and N >= 2M and o6 >= i0 + i6 - o0) }";
 779         map = isl_map_read_from_str(ctx, str, -1);
 780         map = isl_map_coalesce(map);
 781         map2 = isl_map_read_from_str(ctx, str, -1);
 782         assert(isl_map_is_equal(map, map2));
 783         isl_map_free(map);
 784         isl_map_free(map2);
 785
 786         str = "[M, N] -> { [] -> [o0] : (o0 = 0 and M >= 1 and N >= 2) or "
 787                 "(o0 = 0 and M >= 1 and N >= 2M and N >= 2 + M) or "
 788                 "(o0 = 0 and M >= 2 and N >= 3) or "
 789                 "(M = 0 and o0 = 0 and N >= 3) }";
 790         map = isl_map_read_from_str(ctx, str, -1);
 791         map = isl_map_coalesce(map);
 792         map2 = isl_map_read_from_str(ctx, str, -1);
 793         assert(isl_map_is_equal(map, map2));
 794         isl_map_free(map);
 795         isl_map_free(map2);
 796
 797         str = "{ [i0, i1, i2, i3] : (i1 = 10i0 and i0 >= 1 and 10i0 <= 100 and "
 798                 "i3 <= 9 + 10 i2 and i3 >= 1 + 10i2 and i3 >= 0) or "
 799                 "(i1 <= 9 + 10i0 and i1 >= 1 + 10i0 and i2 >= 0 and "
 800                 "i0 >= 0 and i1 <= 100 and i3 <= 9 + 10i2 and i3 >= 1 + 10i2) }";
 801         map = isl_map_read_from_str(ctx, str, -1);
 802         map = isl_map_coalesce(map);
 803         map2 = isl_map_read_from_str(ctx, str, -1);
 804         assert(isl_map_is_equal(map, map2));
 805         isl_map_free(map);
 806         isl_map_free(map2);
 807
 808         test_coalesce_set(ctx,
 809                 "[M] -> { [i1] : (i1 >= 2 and i1 <= M) or "
 810                                 "(i1 = M and M >= 1) }", 0);
 811         test_coalesce_set(ctx,
 812                 "{[x,y] : x,y >= 0; [x,y] : 10 <= x <= 20 and y >= -1 }", 0);
 813         test_coalesce_set(ctx,
 814                 "{ [x, y] : (x >= 1 and y >= 1 and x <= 2 and y <= 2) or "
 815                 "(y = 3 and x = 1) }", 1);
 816         test_coalesce_set(ctx,
 817                 "[M] -> { [i0, i1, i2, i3, i4] : (i1 >= 3 and i4 >= 2 + i2 and "
 818                 "i2 >= 2 and i0 >= 2 and i3 >= 1 + i2 and i0 <= M and "
 819                 "i1 <= M and i3 <= M and i4 <= M) or "
 820                 "(i1 >= 2 and i4 >= 1 + i2 and i2 >= 2 and i0 >= 2 and "
 821                 "i3 >= 1 + i2 and i0 <= M and i1 <= -1 + M and i3 <= M and "
 822                 "i4 <= -1 + M) }", 1);
 823         test_coalesce_set(ctx,
 824                 "{ [x, y] : (x >= 0 and y >= 0 and x <= 10 and y <= 10) or "
 825                 "(x >= 1 and y >= 1 and x <= 11 and y <= 11) }", 1);
 826         test_coalesce_set(ctx,
 827                 "{[x,y,z] : y + 2 >= 0 and x - y + 1 >= 0 and "
 828                         "-x - y + 1 >= 0 and -3 <= z <= 3;"
 829                 "[x,y,z] : -x+z + 20 >= 0 and -x-z + 20 >= 0 and "
 830                         "x-z + 20 >= 0 and x+z + 20 >= 0 and -10 <= y <= 0}", 1);
 831         test_coalesce_set(ctx,
 832                 "{[x,y] : 0 <= x,y <= 10; [5,y]: 4 <=y <= 11}", 1);
 833 }
 834
 835 void test_closure(struct isl_ctx *ctx)
 836 {
 837         const char *str;
 838         isl_set *dom;
 839         isl_map *up, *right;
 840         isl_map *map, *map2;
 841         int exact;
 842
 843         /* COCOA example 1 */
 844         map = isl_map_read_from_str(ctx,
 845                 "[n,k] -> { [i,j] -> [i2,j2] : i2 = i + 1 and j2 = j + 1 and "
 846                         "1 <= i and i < n and 1 <= j and j < n or "
 847                         "i2 = i + 1 and j2 = j - 1 and "
 848                         "1 <= i and i < n and 2 <= j and j <= n }", -1);
 849         map = isl_map_power(map, 1, &exact);
 850         assert(exact);
 851         isl_map_free(map);
 852
 853         /* COCOA example 1 */
 854         map = isl_map_read_from_str(ctx,
 855                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 1 and j2 = j + 1 and "
 856                         "1 <= i and i < n and 1 <= j and j < n or "
 857                         "i2 = i + 1 and j2 = j - 1 and "
 858                         "1 <= i and i < n and 2 <= j and j <= n }", -1);
 859         map = isl_map_transitive_closure(map, &exact);
 860         assert(exact);
 861         map2 = isl_map_read_from_str(ctx,
 862                 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k : "
 863                         "1 <= i and i < n and 1 <= j and j <= n and "
 864                         "2 <= i2 and i2 <= n and 1 <= j2 and j2 <= n and "
 865                         "i2 = i + k1 + k2 and j2 = j + k1 - k2 and "
 866                         "k1 >= 0 and k2 >= 0 and k1 + k2 = k and k >= 1 )}", -1);
 867         assert(isl_map_is_equal(map, map2));
 868         isl_map_free(map2);
 869         isl_map_free(map);
 870
 871         map = isl_map_read_from_str(ctx,
 872                 "[n] -> { [x] -> [y] : y = x + 1 and 0 <= x and x <= n and "
 873                                      " 0 <= y and y <= n }", -1);
 874         map = isl_map_transitive_closure(map, &exact);
 875         map2 = isl_map_read_from_str(ctx,
 876                 "[n] -> { [x] -> [y] : y > x and 0 <= x and x <= n and "
 877                                      " 0 <= y and y <= n }", -1);
 878         assert(isl_map_is_equal(map, map2));
 879         isl_map_free(map2);
 880         isl_map_free(map);
 881
 882         /* COCOA example 2 */
 883         map = isl_map_read_from_str(ctx,
 884                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 2 and j2 = j + 2 and "
 885                         "1 <= i and i < n - 1 and 1 <= j and j < n - 1 or "
 886                         "i2 = i + 2 and j2 = j - 2 and "
 887                         "1 <= i and i < n - 1 and 3 <= j and j <= n }", -1);
 888         map = isl_map_transitive_closure(map, &exact);
 889         assert(exact);
 890         map2 = isl_map_read_from_str(ctx,
 891                 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k : "
 892                         "1 <= i and i < n - 1 and 1 <= j and j <= n and "
 893                         "3 <= i2 and i2 <= n and 1 <= j2 and j2 <= n and "
 894                         "i2 = i + 2 k1 + 2 k2 and j2 = j + 2 k1 - 2 k2 and "
 895                         "k1 >= 0 and k2 >= 0 and k1 + k2 = k and k >= 1) }", -1);
 896         assert(isl_map_is_equal(map, map2));
 897         isl_map_free(map);
 898         isl_map_free(map2);
 899
 900         /* COCOA Fig.2 left */
 901         map = isl_map_read_from_str(ctx,
 902                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 2 and j2 = j and "
 903                         "i <= 2 j - 3 and i <= n - 2 and j <= 2 i - 1 and "
 904                         "j <= n or "
 905                         "i2 = i and j2 = j + 2 and i <= 2 j - 1 and i <= n and "
 906                         "j <= 2 i - 3 and j <= n - 2 or "
 907                         "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
 908                         "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }", -1);
 909         map = isl_map_transitive_closure(map, &exact);
 910         assert(exact);
 911         isl_map_free(map);
 912
 913         /* COCOA Fig.2 right */
 914         map = isl_map_read_from_str(ctx,
 915                 "[n,k] -> { [i,j] -> [i2,j2] : i2 = i + 3 and j2 = j and "
 916                         "i <= 2 j - 4 and i <= n - 3 and j <= 2 i - 1 and "
 917                         "j <= n or "
 918                         "i2 = i and j2 = j + 3 and i <= 2 j - 1 and i <= n and "
 919                         "j <= 2 i - 4 and j <= n - 3 or "
 920                         "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
 921                         "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }", -1);
 922         map = isl_map_power(map, 1, &exact);
 923         assert(exact);
 924         isl_map_free(map);
 925
 926         /* COCOA Fig.2 right */
 927         map = isl_map_read_from_str(ctx,
 928                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 3 and j2 = j and "
 929                         "i <= 2 j - 4 and i <= n - 3 and j <= 2 i - 1 and "
 930                         "j <= n or "
 931                         "i2 = i and j2 = j + 3 and i <= 2 j - 1 and i <= n and "
 932                         "j <= 2 i - 4 and j <= n - 3 or "
 933                         "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
 934                         "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }", -1);
 935         map = isl_map_transitive_closure(map, &exact);
 936         assert(exact);
 937         map2 = isl_map_read_from_str(ctx,
 938                 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k3,k : "
 939                         "i <= 2 j - 1 and i <= n and j <= 2 i - 1 and "
 940                         "j <= n and 3 + i + 2 j <= 3 n and "
 941                         "3 + 2 i + j <= 3n and i2 <= 2 j2 -1 and i2 <= n and "
 942                         "i2 <= 3 j2 - 4 and j2 <= 2 i2 -1 and j2 <= n and "
 943                         "13 + 4 j2 <= 11 i2 and i2 = i + 3 k1 + k3 and "
 944                         "j2 = j + 3 k2 + k3 and k1 >= 0 and k2 >= 0 and "
 945                         "k3 >= 0 and k1 + k2 + k3 = k and k > 0) }", -1);
 946         assert(isl_map_is_equal(map, map2));
 947         isl_map_free(map2);
 948         isl_map_free(map);
 949
 950         /* COCOA Fig.1 right */
 951         dom = isl_set_read_from_str(ctx,
 952                 "{ [x,y] : x >= 0 and -2 x + 3 y >= 0 and x <= 3 and "
 953                         "2 x - 3 y + 3 >= 0 }", -1);
 954         right = isl_map_read_from_str(ctx,
 955                 "{ [x,y] -> [x2,y2] : x2 = x + 1 and y2 = y }", -1);
 956         up = isl_map_read_from_str(ctx,
 957                 "{ [x,y] -> [x2,y2] : x2 = x and y2 = y + 1 }", -1);
 958         right = isl_map_intersect_domain(right, isl_set_copy(dom));
 959         right = isl_map_intersect_range(right, isl_set_copy(dom));
 960         up = isl_map_intersect_domain(up, isl_set_copy(dom));
 961         up = isl_map_intersect_range(up, dom);
 962         map = isl_map_union(up, right);
 963         map = isl_map_transitive_closure(map, &exact);
 964         assert(exact);
 965         map2 = isl_map_read_from_str(ctx,
 966                 "{ [0,0] -> [0,1]; [0,0] -> [1,1]; [0,1] -> [1,1]; "
 967                 "  [2,2] -> [3,2]; [2,2] -> [3,3]; [3,2] -> [3,3] }", -1);
 968         assert(isl_map_is_equal(map, map2));
 969         isl_map_free(map2);
 970         isl_map_free(map);
 971
 972         /* COCOA Theorem 1 counter example */
 973         map = isl_map_read_from_str(ctx,
 974                 "{ [i,j] -> [i2,j2] : i = 0 and 0 <= j and j <= 1 and "
 975                         "i2 = 1 and j2 = j or "
 976                         "i = 0 and j = 0 and i2 = 0 and j2 = 1 }", -1);
 977         map = isl_map_transitive_closure(map, &exact);
 978         assert(exact);
 979         isl_map_free(map);
 980
 981         map = isl_map_read_from_str(ctx,
 982                 "[m,n] -> { [i,j] -> [i2,j2] : i2 = i and j2 = j + 2 and "
 983                         "1 <= i,i2 <= n and 1 <= j,j2 <= m or "
 984                         "i2 = i + 1 and 3 <= j2 - j <= 4 and "
 985                         "1 <= i,i2 <= n and 1 <= j,j2 <= m }", -1);
 986         map = isl_map_transitive_closure(map, &exact);
 987         assert(exact);
 988         isl_map_free(map);
 989
 990         /* Kelly et al 1996, fig 12 */
 991         map = isl_map_read_from_str(ctx,
 992                 "[n] -> { [i,j] -> [i2,j2] : i2 = i and j2 = j + 1 and "
 993                         "1 <= i,j,j+1 <= n or "
 994                         "j = n and j2 = 1 and i2 = i + 1 and "
 995                         "1 <= i,i+1 <= n }", -1);
 996         map = isl_map_transitive_closure(map, &exact);
 997         assert(exact);
 998         map2 = isl_map_read_from_str(ctx,
 999                 "[n] -> { [i,j] -> [i2,j2] : 1 <= j < j2 <= n and "
1000                         "1 <= i <= n and i = i2 or "
1001                         "1 <= i < i2 <= n and 1 <= j <= n and "
1002                         "1 <= j2 <= n }", -1);
1003         assert(isl_map_is_equal(map, map2));
1004         isl_map_free(map2);
1005         isl_map_free(map);
1006
1007         /* Omega's closure4 */
1008         map = isl_map_read_from_str(ctx,
1009                 "[m,n] -> { [x,y] -> [x2,y2] : x2 = x and y2 = y + 1 and "
1010                         "1 <= x,y <= 10 or "
1011                         "x2 = x + 1 and y2 = y and "
1012                         "1 <= x <= 20 && 5 <= y <= 15 }", -1);
1013         map = isl_map_transitive_closure(map, &exact);
1014         assert(exact);
1015         isl_map_free(map);
1016
1017         map = isl_map_read_from_str(ctx,
1018                 "[n] -> { [x] -> [y]: 1 <= n <= y - x <= 10 }", -1);
1019         map = isl_map_transitive_closure(map, &exact);
1020         assert(!exact);
1021         map2 = isl_map_read_from_str(ctx,
1022                 "[n] -> { [x] -> [y] : 1 <= n <= 10 and y >= n + x }", -1);
1023         assert(isl_map_is_equal(map, map2));
1024         isl_map_free(map);
1025         isl_map_free(map2);
1026
1027         str = "[n, m] -> { [i0, i1, i2, i3] -> [o0, o1, o2, o3] : "
1028             "i3 = 1 and o0 = i0 and o1 = -1 + i1 and o2 = -1 + i2 and "
1029             "o3 = -2 + i2 and i1 <= -1 + i0 and i1 >= 1 - m + i0 and "
1030             "i1 >= 2 and i1 <= n and i2 >= 3 and i2 <= 1 + n and i2 <= m }";
1031         map = isl_map_read_from_str(ctx, str, -1);
1032         map = isl_map_transitive_closure(map, &exact);
1033         assert(exact);
1034         map2 = isl_map_read_from_str(ctx, str, -1);
1035         assert(isl_map_is_equal(map, map2));
1036         isl_map_free(map);
1037         isl_map_free(map2);
1038
1039         str = "{[0] -> [1]; [2] -> [3]}";
1040         map = isl_map_read_from_str(ctx, str, -1);
1041         map = isl_map_transitive_closure(map, &exact);
1042         assert(exact);
1043         map2 = isl_map_read_from_str(ctx, str, -1);
1044         assert(isl_map_is_equal(map, map2));
1045         isl_map_free(map);
1046         isl_map_free(map2);
1047 }
1048
1049 void test_lex(struct isl_ctx *ctx)
1050 {
1051         isl_dim *dim;
1052         isl_map *map;
1053
1054         dim = isl_dim_alloc(ctx, 0, 0, 0);
1055         map = isl_map_lex_le(dim);
1056         assert(!isl_map_is_empty(map));
1057         isl_map_free(map);
1058 }
1059
1060 void test_lexmin(struct isl_ctx *ctx)
1061 {
1062         const char *str;
1063         isl_map *map;
1064         isl_set *set;
1065         isl_set *set2;
1066
1067         str = "[p0, p1] -> { [] -> [] : "
1068             "exists (e0 = [(2p1)/3], e1, e2, e3 = [(3 - p1 + 3e0)/3], "
1069             "e4 = [(p1)/3], e5 = [(p1 + 3e4)/3]: "
1070             "3e0 >= -2 + 2p1 and 3e0 >= p1 and 3e3 >= 1 - p1 + 3e0 and "
1071             "3e0 <= 2p1 and 3e3 >= -2 + p1 and 3e3 <= -1 + p1 and p1 >= 3 and "
1072             "3e5 >= -2 + 2p1 and 3e5 >= p1 and 3e5 <= -1 + p1 + 3e4 and "
1073             "3e4 <= p1 and 3e4 >= -2 + p1 and e3 <= -1 + e0 and "
1074             "3e4 >= 6 - p1 + 3e1 and 3e1 >= p1 and 3e5 >= -2 + p1 + 3e4 and "
1075             "2e4 >= 3 - p1 + 2e1 and e4 <= e1 and 3e3 <= 2 - p1 + 3e0 and "
1076             "e5 >= 1 + e1 and 3e4 >= 6 - 2p1 + 3e1 and "
1077             "p0 >= 2 and p1 >= p0 and 3e2 >= p1 and 3e4 >= 6 - p1 + 3e2 and "
1078             "e2 <= e1 and e3 >= 1 and e4 <= e2) }";
1079         map = isl_map_read_from_str(ctx, str, -1);
1080         map = isl_map_lexmin(map);
1081         isl_map_free(map);
1082
1083         str = "[C] -> { [obj,a,b,c] : obj <= 38 a + 7 b + 10 c and "
1084             "a + b <= 1 and c <= 10 b and c <= C and a,b,c,C >= 0 }";
1085         set = isl_set_read_from_str(ctx, str, -1);
1086         set = isl_set_lexmax(set);
1087         str = "[C] -> { [obj,a,b,c] : C = 8 }";
1088         set2 = isl_set_read_from_str(ctx, str, -1);
1089         set = isl_set_intersect(set, set2);
1090         assert(!isl_set_is_empty(set));
1091         isl_set_free(set);
1092 }
1093
1094 struct must_may {
1095         isl_map *must;
1096         isl_map *may;
1097 };
1098
1099 static int collect_must_may(__isl_take isl_map *dep, int must,
1100         void *dep_user, void *user)
1101 {
1102         struct must_may *mm = (struct must_may *)user;
1103
1104         if (must)
1105                 mm->must = isl_map_union(mm->must, dep);
1106         else
1107                 mm->may = isl_map_union(mm->may, dep);
1108
1109         return 0;
1110 }
1111
1112 static int common_space(void *first, void *second)
1113 {
1114         int depth = *(int *)first;
1115         return 2 * depth;
1116 }
1117
1118 static int map_is_equal(__isl_keep isl_map *map, const char *str)
1119 {
1120         isl_map *map2;
1121         int equal;
1122
1123         if (!map)
1124                 return -1;
1125
1126         map2 = isl_map_read_from_str(map->ctx, str, -1);
1127         equal = isl_map_is_equal(map, map2);
1128         isl_map_free(map2);
1129
1130         return equal;
1131 }
1132
1133 void test_dep(struct isl_ctx *ctx)
1134 {
1135         const char *str;
1136         isl_dim *dim;
1137         isl_map *map;
1138         isl_access_info *ai;
1139         isl_flow *flow;
1140         int depth;
1141         struct must_may mm;
1142
1143         depth = 3;
1144
1145         str = "{ [2,i,0] -> [i] : 0 <= i <= 10 }";
1146         map = isl_map_read_from_str(ctx, str, -1);
1147         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1148
1149         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1150         map = isl_map_read_from_str(ctx, str, -1);
1151         ai = isl_access_info_add_source(ai, map, 1, &depth);
1152
1153         str = "{ [1,i,0] -> [5] : 0 <= i <= 10 }";
1154         map = isl_map_read_from_str(ctx, str, -1);
1155         ai = isl_access_info_add_source(ai, map, 1, &depth);
1156
1157         flow = isl_access_info_compute_flow(ai);
1158         dim = isl_dim_alloc(ctx, 0, 3, 3);
1159         mm.must = isl_map_empty(isl_dim_copy(dim));
1160         mm.may = isl_map_empty(dim);
1161
1162         isl_flow_foreach(flow, collect_must_may, &mm);
1163
1164         str = "{ [0,i,0] -> [2,i,0] : (0 <= i <= 4) or (6 <= i <= 10); "
1165               "  [1,10,0] -> [2,5,0] }";
1166         assert(map_is_equal(mm.must, str));
1167         str = "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1168         assert(map_is_equal(mm.may, str));
1169
1170         isl_map_free(mm.must);
1171         isl_map_free(mm.may);
1172         isl_flow_free(flow);
1173
1174
1175         str = "{ [2,i,0] -> [i] : 0 <= i <= 10 }";
1176         map = isl_map_read_from_str(ctx, str, -1);
1177         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1178
1179         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1180         map = isl_map_read_from_str(ctx, str, -1);
1181         ai = isl_access_info_add_source(ai, map, 1, &depth);
1182
1183         str = "{ [1,i,0] -> [5] : 0 <= i <= 10 }";
1184         map = isl_map_read_from_str(ctx, str, -1);
1185         ai = isl_access_info_add_source(ai, map, 0, &depth);
1186
1187         flow = isl_access_info_compute_flow(ai);
1188         dim = isl_dim_alloc(ctx, 0, 3, 3);
1189         mm.must = isl_map_empty(isl_dim_copy(dim));
1190         mm.may = isl_map_empty(dim);
1191
1192         isl_flow_foreach(flow, collect_must_may, &mm);
1193
1194         str = "{ [0,i,0] -> [2,i,0] : (0 <= i <= 4) or (6 <= i <= 10) }";
1195         assert(map_is_equal(mm.must, str));
1196         str = "{ [0,5,0] -> [2,5,0]; [1,i,0] -> [2,5,0] : 0 <= i <= 10 }";
1197         assert(map_is_equal(mm.may, str));
1198
1199         isl_map_free(mm.must);
1200         isl_map_free(mm.may);
1201         isl_flow_free(flow);
1202
1203
1204         str = "{ [2,i,0] -> [i] : 0 <= i <= 10 }";
1205         map = isl_map_read_from_str(ctx, str, -1);
1206         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1207
1208         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1209         map = isl_map_read_from_str(ctx, str, -1);
1210         ai = isl_access_info_add_source(ai, map, 0, &depth);
1211
1212         str = "{ [1,i,0] -> [5] : 0 <= i <= 10 }";
1213         map = isl_map_read_from_str(ctx, str, -1);
1214         ai = isl_access_info_add_source(ai, map, 0, &depth);
1215
1216         flow = isl_access_info_compute_flow(ai);
1217         dim = isl_dim_alloc(ctx, 0, 3, 3);
1218         mm.must = isl_map_empty(isl_dim_copy(dim));
1219         mm.may = isl_map_empty(dim);
1220
1221         isl_flow_foreach(flow, collect_must_may, &mm);
1222
1223         str = "{ [0,i,0] -> [2,i,0] : 0 <= i <= 10; "
1224               "  [1,i,0] -> [2,5,0] : 0 <= i <= 10 }";
1225         assert(map_is_equal(mm.may, str));
1226         str = "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1227         assert(map_is_equal(mm.must, str));
1228
1229         isl_map_free(mm.must);
1230         isl_map_free(mm.may);
1231         isl_flow_free(flow);
1232
1233
1234         str = "{ [0,i,2] -> [i] : 0 <= i <= 10 }";
1235         map = isl_map_read_from_str(ctx, str, -1);
1236         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1237
1238         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1239         map = isl_map_read_from_str(ctx, str, -1);
1240         ai = isl_access_info_add_source(ai, map, 0, &depth);
1241
1242         str = "{ [0,i,1] -> [5] : 0 <= i <= 10 }";
1243         map = isl_map_read_from_str(ctx, str, -1);
1244         ai = isl_access_info_add_source(ai, map, 0, &depth);
1245
1246         flow = isl_access_info_compute_flow(ai);
1247         dim = isl_dim_alloc(ctx, 0, 3, 3);
1248         mm.must = isl_map_empty(isl_dim_copy(dim));
1249         mm.may = isl_map_empty(dim);
1250
1251         isl_flow_foreach(flow, collect_must_may, &mm);
1252
1253         str = "{ [0,i,0] -> [0,i,2] : 0 <= i <= 10; "
1254               "  [0,i,1] -> [0,5,2] : 0 <= i <= 5 }";
1255         assert(map_is_equal(mm.may, str));
1256         str = "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1257         assert(map_is_equal(mm.must, str));
1258
1259         isl_map_free(mm.must);
1260         isl_map_free(mm.may);
1261         isl_flow_free(flow);
1262
1263
1264         str = "{ [0,i,1] -> [i] : 0 <= i <= 10 }";
1265         map = isl_map_read_from_str(ctx, str, -1);
1266         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1267
1268         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1269         map = isl_map_read_from_str(ctx, str, -1);
1270         ai = isl_access_info_add_source(ai, map, 0, &depth);
1271
1272         str = "{ [0,i,2] -> [5] : 0 <= i <= 10 }";
1273         map = isl_map_read_from_str(ctx, str, -1);
1274         ai = isl_access_info_add_source(ai, map, 0, &depth);
1275
1276         flow = isl_access_info_compute_flow(ai);
1277         dim = isl_dim_alloc(ctx, 0, 3, 3);
1278         mm.must = isl_map_empty(isl_dim_copy(dim));
1279         mm.may = isl_map_empty(dim);
1280
1281         isl_flow_foreach(flow, collect_must_may, &mm);
1282
1283         str = "{ [0,i,0] -> [0,i,1] : 0 <= i <= 10; "
1284               "  [0,i,2] -> [0,5,1] : 0 <= i <= 4 }";
1285         assert(map_is_equal(mm.may, str));
1286         str = "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1287         assert(map_is_equal(mm.must, str));
1288
1289         isl_map_free(mm.must);
1290         isl_map_free(mm.may);
1291         isl_flow_free(flow);
1292
1293
1294         depth = 5;
1295
1296         str = "{ [1,i,0,0,0] -> [i,j] : 0 <= i <= 10 and 0 <= j <= 10 }";
1297         map = isl_map_read_from_str(ctx, str, -1);
1298         ai = isl_access_info_alloc(map, &depth, &common_space, 1);
1299
1300         str = "{ [0,i,0,j,0] -> [i,j] : 0 <= i <= 10 and 0 <= j <= 10 }";
1301         map = isl_map_read_from_str(ctx, str, -1);
1302         ai = isl_access_info_add_source(ai, map, 1, &depth);
1303
1304         flow = isl_access_info_compute_flow(ai);
1305         dim = isl_dim_alloc(ctx, 0, 5, 5);
1306         mm.must = isl_map_empty(isl_dim_copy(dim));
1307         mm.may = isl_map_empty(dim);
1308
1309         isl_flow_foreach(flow, collect_must_may, &mm);
1310
1311         str = "{ [0,i,0,j,0] -> [1,i,0,0,0] : 0 <= i,j <= 10 }";
1312         assert(map_is_equal(mm.must, str));
1313         str = "{ [0,0,0,0,0] -> [0,0,0,0,0] : 1 = 0 }";
1314         assert(map_is_equal(mm.may, str));
1315
1316         isl_map_free(mm.must);
1317         isl_map_free(mm.may);
1318         isl_flow_free(flow);
1319 }
1320
1321 void test_sv(struct isl_ctx *ctx)
1322 {
1323         const char *str;
1324         isl_map *map;
1325
1326         str = "[N] -> { [i] -> [f] : 0 <= i <= N and 0 <= i - 10 f <= 9 }";
1327         map = isl_map_read_from_str(ctx, str, -1);
1328         assert(isl_map_is_single_valued(map));
1329         isl_map_free(map);
1330
1331         str = "[N] -> { [i] -> [f] : 0 <= i <= N and 0 <= i - 10 f <= 10 }";
1332         map = isl_map_read_from_str(ctx, str, -1);
1333         assert(!isl_map_is_single_valued(map));
1334         isl_map_free(map);
1335 }
1336
1337 void test_bijective_case(struct isl_ctx *ctx, const char *str, int bijective)
1338 {
1339         isl_map *map;
1340
1341         map = isl_map_read_from_str(ctx, str, -1);
1342         if (bijective)
1343                 assert(isl_map_is_bijective(map));
1344         else
1345                 assert(!isl_map_is_bijective(map));
1346         isl_map_free(map);
1347 }
1348
1349 void test_bijective(struct isl_ctx *ctx)
1350 {
1351         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i]}", 0);
1352         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i] : j=i}", 1);
1353         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i] : j=0}", 1);
1354         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i] : j=N}", 1);
1355         test_bijective_case(ctx, "[N,M]->{[i,j] -> [j,i]}", 1);
1356         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i+j]}", 0);
1357         test_bijective_case(ctx, "[N,M]->{[i,j] -> []}", 0);
1358         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i,j,N]}", 1);
1359         test_bijective_case(ctx, "[N,M]->{[i,j] -> [2i]}", 0);
1360         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i,i]}", 0);
1361         test_bijective_case(ctx, "[N,M]->{[i,j] -> [2i,i]}", 0);
1362         test_bijective_case(ctx, "[N,M]->{[i,j] -> [2i,j]}", 1);
1363         test_bijective_case(ctx, "[N,M]->{[i,j] -> [x,y] : 2x=i & y =j}", 1);
1364 }
1365
1366 void test_pwqp(struct isl_ctx *ctx)
1367 {
1368         const char *str;
1369         isl_pw_qpolynomial *pwqp1, *pwqp2;
1370
1371         str = "{ [i,j,k] -> 1 + 9 * [i/5] + 7 * [j/11] + 4 * [k/13] }";
1372         pwqp1 = isl_pw_qpolynomial_read_from_str(ctx, str);
1373
1374         pwqp1 = isl_pw_qpolynomial_move_dims(pwqp1, isl_dim_param, 0,
1375                                                 isl_dim_set, 1, 1);
1376
1377         str = "[j] -> { [i,k] -> 1 + 9 * [i/5] + 7 * [j/11] + 4 * [k/13] }";
1378         pwqp2 = isl_pw_qpolynomial_read_from_str(ctx, str);
1379
1380         pwqp1 = isl_pw_qpolynomial_sub(pwqp1, pwqp2);
1381
1382         assert(isl_pw_qpolynomial_is_zero(pwqp1));
1383
1384         isl_pw_qpolynomial_free(pwqp1);
1385 }
1386
1387 int main()
1388 {
1389         struct isl_ctx *ctx;
1390
1391         srcdir = getenv("srcdir");
1392         assert(srcdir);
1393
1394         ctx = isl_ctx_alloc();
1395         test_pwqp(ctx);
1396         test_lex(ctx);
1397         test_sv(ctx);
1398         test_bijective(ctx);
1399         test_dep(ctx);
1400         test_read(ctx);
1401         test_bounded(ctx);
1402         test_construction(ctx);
1403         test_dim(ctx);
1404         test_div(ctx);
1405         test_application(ctx);
1406         test_affine_hull(ctx);
1407         test_convex_hull(ctx);
1408         test_gist(ctx);
1409         test_coalesce(ctx);
1410         test_closure(ctx);
1411         test_lexmin(ctx);
1412         isl_ctx_free(ctx);
1413         return 0;
1414 }