isl_test.c

   1 /*
   2  * Copyright 2008-2009 Katholieke Universiteit Leuven
   3  *
   4  * Use of this software is governed by the MIT 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_private.h>
  14 #include <isl_map_private.h>
  15 #include <isl_aff_private.h>
  16 #include <isl/set.h>
  17 #include <isl/flow.h>
  18 #include <isl/constraint.h>
  19 #include <isl/polynomial.h>
  20 #include <isl/union_map.h>
  21 #include <isl_factorization.h>
  22 #include <isl/schedule.h>
  23 #include <isl_options_private.h>
  24 #include <isl/vertices.h>
  25
  26 #define ARRAY_SIZE(array) (sizeof(array)/sizeof(*array))
  27
  28 static char *srcdir;
  29
  30 static char *get_filename(isl_ctx *ctx, const char *name, const char *suffix) {
  31         char *filename;
  32         int length;
  33         char *pattern = "%s/test_inputs/%s.%s";
  34
  35         length = strlen(pattern) - 6 + strlen(srcdir) + strlen(name)
  36                 + strlen(suffix) + 1;
  37         filename = isl_alloc_array(ctx, char, length);
  38
  39         if (!filename)
  40                 return NULL;
  41
  42         sprintf(filename, pattern, srcdir, name, suffix);
  43
  44         return filename;
  45 }
  46
  47 void test_parse_map(isl_ctx *ctx, const char *str)
  48 {
  49         isl_map *map;
  50
  51         map = isl_map_read_from_str(ctx, str);
  52         assert(map);
  53         isl_map_free(map);
  54 }
  55
  56 int test_parse_map_equal(isl_ctx *ctx, const char *str, const char *str2)
  57 {
  58         isl_map *map, *map2;
  59         int equal;
  60
  61         map = isl_map_read_from_str(ctx, str);
  62         map2 = isl_map_read_from_str(ctx, str2);
  63         equal = isl_map_is_equal(map, map2);
  64         isl_map_free(map);
  65         isl_map_free(map2);
  66
  67         if (equal < 0)
  68                 return -1;
  69         if (!equal)
  70                 isl_die(ctx, isl_error_unknown, "maps not equal",
  71                         return -1);
  72
  73         return 0;
  74 }
  75
  76 void test_parse_pwqp(isl_ctx *ctx, const char *str)
  77 {
  78         isl_pw_qpolynomial *pwqp;
  79
  80         pwqp = isl_pw_qpolynomial_read_from_str(ctx, str);
  81         assert(pwqp);
  82         isl_pw_qpolynomial_free(pwqp);
  83 }
  84
  85 static void test_parse_pwaff(isl_ctx *ctx, const char *str)
  86 {
  87         isl_pw_aff *pwaff;
  88
  89         pwaff = isl_pw_aff_read_from_str(ctx, str);
  90         assert(pwaff);
  91         isl_pw_aff_free(pwaff);
  92 }
  93
  94 int test_parse(struct isl_ctx *ctx)
  95 {
  96         isl_map *map, *map2;
  97         const char *str, *str2;
  98
  99         str = "{ [i] -> [-i] }";
 100         map = isl_map_read_from_str(ctx, str);
 101         assert(map);
 102         isl_map_free(map);
 103
 104         str = "{ A[i] -> L[([i/3])] }";
 105         map = isl_map_read_from_str(ctx, str);
 106         assert(map);
 107         isl_map_free(map);
 108
 109         test_parse_map(ctx, "{[[s] -> A[i]] -> [[s+1] -> A[i]]}");
 110         test_parse_map(ctx, "{ [p1, y1, y2] -> [2, y1, y2] : "
 111                                 "p1 = 1 && (y1 <= y2 || y2 = 0) }");
 112
 113         str = "{ [x,y]  : [([x/2]+y)/3] >= 1 }";
 114         str2 = "{ [x, y] : 2y >= 6 - x }";
 115         if (test_parse_map_equal(ctx, str, str2) < 0)
 116                 return -1;
 117
 118         if (test_parse_map_equal(ctx, "{ [x,y] : x <= min(y, 2*y+3) }",
 119                                       "{ [x,y] : x <= y, 2*y + 3 }") < 0)
 120                 return -1;
 121         str = "{ [x, y] : (y <= x and y >= -3) or (2y <= -3 + x and y <= -4) }";
 122         if (test_parse_map_equal(ctx, "{ [x,y] : x >= min(y, 2*y+3) }",
 123                                         str) < 0)
 124                 return -1;
 125
 126         str = "{[new,old] -> [new+1-2*[(new+1)/2],old+1-2*[(old+1)/2]]}";
 127         map = isl_map_read_from_str(ctx, str);
 128         str = "{ [new, old] -> [o0, o1] : "
 129                "exists (e0 = [(-1 - new + o0)/2], e1 = [(-1 - old + o1)/2]: "
 130                "2e0 = -1 - new + o0 and 2e1 = -1 - old + o1 and o0 >= 0 and "
 131                "o0 <= 1 and o1 >= 0 and o1 <= 1) }";
 132         map2 = isl_map_read_from_str(ctx, str);
 133         assert(isl_map_is_equal(map, map2));
 134         isl_map_free(map);
 135         isl_map_free(map2);
 136
 137         str = "{[new,old] -> [new+1-2*[(new+1)/2],old+1-2*[(old+1)/2]]}";
 138         map = isl_map_read_from_str(ctx, str);
 139         str = "{[new,old] -> [(new+1)%2,(old+1)%2]}";
 140         map2 = isl_map_read_from_str(ctx, str);
 141         assert(isl_map_is_equal(map, map2));
 142         isl_map_free(map);
 143         isl_map_free(map2);
 144
 145         str = "[n] -> { [c1] : c1>=0 and c1<=floord(n-4,3) }";
 146         str2 = "[n] -> { [c1] : c1 >= 0 and 3c1 <= -4 + n }";
 147         if (test_parse_map_equal(ctx, str, str2) < 0)
 148                 return -1;
 149
 150         str = "{ [i,j] -> [i] : i < j; [i,j] -> [j] : j <= i }";
 151         str2 = "{ [i,j] -> [min(i,j)] }";
 152         if (test_parse_map_equal(ctx, str, str2) < 0)
 153                 return -1;
 154
 155         str = "{ [i,j] : i != j }";
 156         str2 = "{ [i,j] : i < j or i > j }";
 157         if (test_parse_map_equal(ctx, str, str2) < 0)
 158                 return -1;
 159
 160         str = "{ [i,j] : (i+1)*2 >= j }";
 161         str2 = "{ [i, j] : j <= 2 + 2i }";
 162         if (test_parse_map_equal(ctx, str, str2) < 0)
 163                 return -1;
 164
 165         str = "{ [i] -> [i > 0 ? 4 : 5] }";
 166         str2 = "{ [i] -> [5] : i <= 0; [i] -> [4] : i >= 1 }";
 167         if (test_parse_map_equal(ctx, str, str2) < 0)
 168                 return -1;
 169
 170         str = "[N=2,M] -> { [i=[(M+N)/4]] }";
 171         str2 = "[N, M] -> { [i] : N = 2 and 4i <= 2 + M and 4i >= -1 + M }";
 172         if (test_parse_map_equal(ctx, str, str2) < 0)
 173                 return -1;
 174
 175         str = "{ [x] : x >= 0 }";
 176         str2 = "{ [x] : x-0 >= 0 }";
 177         if (test_parse_map_equal(ctx, str, str2) < 0)
 178                 return -1;
 179
 180         str = "{ [i] : ((i > 10)) }";
 181         str2 = "{ [i] : i >= 11 }";
 182         if (test_parse_map_equal(ctx, str, str2) < 0)
 183                 return -1;
 184
 185         str = "{ [i] -> [0] }";
 186         str2 = "{ [i] -> [0 * i] }";
 187         if (test_parse_map_equal(ctx, str, str2) < 0)
 188                 return -1;
 189
 190         test_parse_pwqp(ctx, "{ [i] -> i + [ (i + [i/3])/2 ] }");
 191         test_parse_map(ctx, "{ S1[i] -> [([i/10]),i%10] : 0 <= i <= 45 }");
 192         test_parse_pwaff(ctx, "{ [i] -> [i + 1] : i > 0; [a] -> [a] : a < 0 }");
 193         test_parse_pwqp(ctx, "{ [x] -> ([(x)/2] * [(x)/3]) }");
 194
 195         if (test_parse_map_equal(ctx, "{ [a] -> [b] : (not false) }",
 196                                       "{ [a] -> [b] : true }") < 0)
 197                 return -1;
 198
 199         if (test_parse_map_equal(ctx, "{ [i] : i/2 <= 5 }",
 200                                       "{ [i] : i <= 10 }") < 0)
 201                 return -1;
 202
 203         if (test_parse_map_equal(ctx, "{Sym=[n] [i] : i <= n }",
 204                                       "[n] -> { [i] : i <= n }") < 0)
 205                 return -1;
 206
 207         return 0;
 208 }
 209
 210 void test_read(struct isl_ctx *ctx)
 211 {
 212         char *filename;
 213         FILE *input;
 214         struct isl_basic_set *bset1, *bset2;
 215         const char *str = "{[y]: Exists ( alpha : 2alpha = y)}";
 216
 217         filename = get_filename(ctx, "set", "omega");
 218         assert(filename);
 219         input = fopen(filename, "r");
 220         assert(input);
 221
 222         bset1 = isl_basic_set_read_from_file(ctx, input);
 223         bset2 = isl_basic_set_read_from_str(ctx, str);
 224
 225         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 226
 227         isl_basic_set_free(bset1);
 228         isl_basic_set_free(bset2);
 229         free(filename);
 230
 231         fclose(input);
 232 }
 233
 234 void test_bounded(struct isl_ctx *ctx)
 235 {
 236         isl_set *set;
 237         int bounded;
 238
 239         set = isl_set_read_from_str(ctx, "[n] -> {[i] : 0 <= i <= n }");
 240         bounded = isl_set_is_bounded(set);
 241         assert(bounded);
 242         isl_set_free(set);
 243
 244         set = isl_set_read_from_str(ctx, "{[n, i] : 0 <= i <= n }");
 245         bounded = isl_set_is_bounded(set);
 246         assert(!bounded);
 247         isl_set_free(set);
 248
 249         set = isl_set_read_from_str(ctx, "[n] -> {[i] : i <= n }");
 250         bounded = isl_set_is_bounded(set);
 251         assert(!bounded);
 252         isl_set_free(set);
 253 }
 254
 255 /* Construct the basic set { [i] : 5 <= i <= N } */
 256 void test_construction(struct isl_ctx *ctx)
 257 {
 258         isl_int v;
 259         isl_space *dim;
 260         isl_local_space *ls;
 261         struct isl_basic_set *bset;
 262         struct isl_constraint *c;
 263
 264         isl_int_init(v);
 265
 266         dim = isl_space_set_alloc(ctx, 1, 1);
 267         bset = isl_basic_set_universe(isl_space_copy(dim));
 268         ls = isl_local_space_from_space(dim);
 269
 270         c = isl_inequality_alloc(isl_local_space_copy(ls));
 271         isl_int_set_si(v, -1);
 272         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 273         isl_int_set_si(v, 1);
 274         isl_constraint_set_coefficient(c, isl_dim_param, 0, v);
 275         bset = isl_basic_set_add_constraint(bset, c);
 276
 277         c = isl_inequality_alloc(isl_local_space_copy(ls));
 278         isl_int_set_si(v, 1);
 279         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 280         isl_int_set_si(v, -5);
 281         isl_constraint_set_constant(c, v);
 282         bset = isl_basic_set_add_constraint(bset, c);
 283
 284         isl_local_space_free(ls);
 285         isl_basic_set_free(bset);
 286
 287         isl_int_clear(v);
 288 }
 289
 290 void test_dim(struct isl_ctx *ctx)
 291 {
 292         const char *str;
 293         isl_map *map1, *map2;
 294
 295         map1 = isl_map_read_from_str(ctx,
 296             "[n] -> { [i] -> [j] : exists (a = [i/10] : i - 10a <= n ) }");
 297         map1 = isl_map_add_dims(map1, isl_dim_in, 1);
 298         map2 = isl_map_read_from_str(ctx,
 299             "[n] -> { [i,k] -> [j] : exists (a = [i/10] : i - 10a <= n ) }");
 300         assert(isl_map_is_equal(map1, map2));
 301         isl_map_free(map2);
 302
 303         map1 = isl_map_project_out(map1, isl_dim_in, 0, 1);
 304         map2 = isl_map_read_from_str(ctx, "[n] -> { [i] -> [j] : n >= 0 }");
 305         assert(isl_map_is_equal(map1, map2));
 306
 307         isl_map_free(map1);
 308         isl_map_free(map2);
 309
 310         str = "[n] -> { [i] -> [] : exists a : 0 <= i <= n and i = 2 a }";
 311         map1 = isl_map_read_from_str(ctx, str);
 312         str = "{ [i] -> [j] : exists a : 0 <= i <= j and i = 2 a }";
 313         map2 = isl_map_read_from_str(ctx, str);
 314         map1 = isl_map_move_dims(map1, isl_dim_out, 0, isl_dim_param, 0, 1);
 315         assert(isl_map_is_equal(map1, map2));
 316
 317         isl_map_free(map1);
 318         isl_map_free(map2);
 319 }
 320
 321 static int test_div(isl_ctx *ctx)
 322 {
 323         unsigned n;
 324         const char *str;
 325         int empty;
 326         isl_int v;
 327         isl_space *dim;
 328         isl_set *set;
 329         isl_local_space *ls;
 330         struct isl_basic_set *bset;
 331         struct isl_constraint *c;
 332
 333         isl_int_init(v);
 334
 335         /* test 1 */
 336         dim = isl_space_set_alloc(ctx, 0, 3);
 337         bset = isl_basic_set_universe(isl_space_copy(dim));
 338         ls = isl_local_space_from_space(dim);
 339
 340         c = isl_equality_alloc(isl_local_space_copy(ls));
 341         isl_int_set_si(v, -1);
 342         isl_constraint_set_constant(c, v);
 343         isl_int_set_si(v, 1);
 344         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 345         isl_int_set_si(v, 3);
 346         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 347         bset = isl_basic_set_add_constraint(bset, c);
 348
 349         c = isl_equality_alloc(isl_local_space_copy(ls));
 350         isl_int_set_si(v, 1);
 351         isl_constraint_set_constant(c, v);
 352         isl_int_set_si(v, -1);
 353         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 354         isl_int_set_si(v, 3);
 355         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 356         bset = isl_basic_set_add_constraint(bset, c);
 357
 358         bset = isl_basic_set_project_out(bset, isl_dim_set, 1, 2);
 359
 360         assert(bset && bset->n_div == 1);
 361         isl_local_space_free(ls);
 362         isl_basic_set_free(bset);
 363
 364         /* test 2 */
 365         dim = isl_space_set_alloc(ctx, 0, 3);
 366         bset = isl_basic_set_universe(isl_space_copy(dim));
 367         ls = isl_local_space_from_space(dim);
 368
 369         c = isl_equality_alloc(isl_local_space_copy(ls));
 370         isl_int_set_si(v, 1);
 371         isl_constraint_set_constant(c, v);
 372         isl_int_set_si(v, -1);
 373         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 374         isl_int_set_si(v, 3);
 375         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 376         bset = isl_basic_set_add_constraint(bset, c);
 377
 378         c = isl_equality_alloc(isl_local_space_copy(ls));
 379         isl_int_set_si(v, -1);
 380         isl_constraint_set_constant(c, v);
 381         isl_int_set_si(v, 1);
 382         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 383         isl_int_set_si(v, 3);
 384         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 385         bset = isl_basic_set_add_constraint(bset, c);
 386
 387         bset = isl_basic_set_project_out(bset, isl_dim_set, 1, 2);
 388
 389         assert(bset && bset->n_div == 1);
 390         isl_local_space_free(ls);
 391         isl_basic_set_free(bset);
 392
 393         /* test 3 */
 394         dim = isl_space_set_alloc(ctx, 0, 3);
 395         bset = isl_basic_set_universe(isl_space_copy(dim));
 396         ls = isl_local_space_from_space(dim);
 397
 398         c = isl_equality_alloc(isl_local_space_copy(ls));
 399         isl_int_set_si(v, 1);
 400         isl_constraint_set_constant(c, v);
 401         isl_int_set_si(v, -1);
 402         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 403         isl_int_set_si(v, 3);
 404         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 405         bset = isl_basic_set_add_constraint(bset, c);
 406
 407         c = isl_equality_alloc(isl_local_space_copy(ls));
 408         isl_int_set_si(v, -3);
 409         isl_constraint_set_constant(c, v);
 410         isl_int_set_si(v, 1);
 411         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 412         isl_int_set_si(v, 4);
 413         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 414         bset = isl_basic_set_add_constraint(bset, c);
 415
 416         bset = isl_basic_set_project_out(bset, isl_dim_set, 1, 2);
 417
 418         assert(bset && bset->n_div == 1);
 419         isl_local_space_free(ls);
 420         isl_basic_set_free(bset);
 421
 422         /* test 4 */
 423         dim = isl_space_set_alloc(ctx, 0, 3);
 424         bset = isl_basic_set_universe(isl_space_copy(dim));
 425         ls = isl_local_space_from_space(dim);
 426
 427         c = isl_equality_alloc(isl_local_space_copy(ls));
 428         isl_int_set_si(v, 2);
 429         isl_constraint_set_constant(c, v);
 430         isl_int_set_si(v, -1);
 431         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 432         isl_int_set_si(v, 3);
 433         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 434         bset = isl_basic_set_add_constraint(bset, c);
 435
 436         c = isl_equality_alloc(isl_local_space_copy(ls));
 437         isl_int_set_si(v, -1);
 438         isl_constraint_set_constant(c, v);
 439         isl_int_set_si(v, 1);
 440         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 441         isl_int_set_si(v, 6);
 442         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 443         bset = isl_basic_set_add_constraint(bset, c);
 444
 445         bset = isl_basic_set_project_out(bset, isl_dim_set, 1, 2);
 446
 447         assert(isl_basic_set_is_empty(bset));
 448         isl_local_space_free(ls);
 449         isl_basic_set_free(bset);
 450
 451         /* test 5 */
 452         dim = isl_space_set_alloc(ctx, 0, 3);
 453         bset = isl_basic_set_universe(isl_space_copy(dim));
 454         ls = isl_local_space_from_space(dim);
 455
 456         c = isl_equality_alloc(isl_local_space_copy(ls));
 457         isl_int_set_si(v, -1);
 458         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 459         isl_int_set_si(v, 3);
 460         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 461         bset = isl_basic_set_add_constraint(bset, c);
 462
 463         c = isl_equality_alloc(isl_local_space_copy(ls));
 464         isl_int_set_si(v, 1);
 465         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 466         isl_int_set_si(v, -3);
 467         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 468         bset = isl_basic_set_add_constraint(bset, c);
 469
 470         bset = isl_basic_set_project_out(bset, isl_dim_set, 2, 1);
 471
 472         assert(bset && bset->n_div == 0);
 473         isl_basic_set_free(bset);
 474         isl_local_space_free(ls);
 475
 476         /* test 6 */
 477         dim = isl_space_set_alloc(ctx, 0, 3);
 478         bset = isl_basic_set_universe(isl_space_copy(dim));
 479         ls = isl_local_space_from_space(dim);
 480
 481         c = isl_equality_alloc(isl_local_space_copy(ls));
 482         isl_int_set_si(v, -1);
 483         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 484         isl_int_set_si(v, 6);
 485         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 486         bset = isl_basic_set_add_constraint(bset, c);
 487
 488         c = isl_equality_alloc(isl_local_space_copy(ls));
 489         isl_int_set_si(v, 1);
 490         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 491         isl_int_set_si(v, -3);
 492         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 493         bset = isl_basic_set_add_constraint(bset, c);
 494
 495         bset = isl_basic_set_project_out(bset, isl_dim_set, 2, 1);
 496
 497         assert(bset && bset->n_div == 1);
 498         isl_basic_set_free(bset);
 499         isl_local_space_free(ls);
 500
 501         /* test 7 */
 502         /* This test is a bit tricky.  We set up an equality
 503          *              a + 3b + 3c = 6 e0
 504          * Normalization of divs creates _two_ divs
 505          *              a = 3 e0
 506          *              c - b - e0 = 2 e1
 507          * Afterwards e0 is removed again because it has coefficient -1
 508          * and we end up with the original equality and div again.
 509          * Perhaps we can avoid the introduction of this temporary div.
 510          */
 511         dim = isl_space_set_alloc(ctx, 0, 4);
 512         bset = isl_basic_set_universe(isl_space_copy(dim));
 513         ls = isl_local_space_from_space(dim);
 514
 515         c = isl_equality_alloc(isl_local_space_copy(ls));
 516         isl_int_set_si(v, -1);
 517         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 518         isl_int_set_si(v, -3);
 519         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 520         isl_int_set_si(v, -3);
 521         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 522         isl_int_set_si(v, 6);
 523         isl_constraint_set_coefficient(c, isl_dim_set, 3, v);
 524         bset = isl_basic_set_add_constraint(bset, c);
 525
 526         bset = isl_basic_set_project_out(bset, isl_dim_set, 3, 1);
 527
 528         /* Test disabled for now */
 529         /*
 530         assert(bset && bset->n_div == 1);
 531         */
 532         isl_local_space_free(ls);
 533         isl_basic_set_free(bset);
 534
 535         /* test 8 */
 536         dim = isl_space_set_alloc(ctx, 0, 5);
 537         bset = isl_basic_set_universe(isl_space_copy(dim));
 538         ls = isl_local_space_from_space(dim);
 539
 540         c = isl_equality_alloc(isl_local_space_copy(ls));
 541         isl_int_set_si(v, -1);
 542         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 543         isl_int_set_si(v, -3);
 544         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 545         isl_int_set_si(v, -3);
 546         isl_constraint_set_coefficient(c, isl_dim_set, 3, v);
 547         isl_int_set_si(v, 6);
 548         isl_constraint_set_coefficient(c, isl_dim_set, 4, v);
 549         bset = isl_basic_set_add_constraint(bset, c);
 550
 551         c = isl_equality_alloc(isl_local_space_copy(ls));
 552         isl_int_set_si(v, -1);
 553         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 554         isl_int_set_si(v, 1);
 555         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 556         isl_int_set_si(v, 1);
 557         isl_constraint_set_constant(c, v);
 558         bset = isl_basic_set_add_constraint(bset, c);
 559
 560         bset = isl_basic_set_project_out(bset, isl_dim_set, 4, 1);
 561
 562         /* Test disabled for now */
 563         /*
 564         assert(bset && bset->n_div == 1);
 565         */
 566         isl_local_space_free(ls);
 567         isl_basic_set_free(bset);
 568
 569         /* test 9 */
 570         dim = isl_space_set_alloc(ctx, 0, 4);
 571         bset = isl_basic_set_universe(isl_space_copy(dim));
 572         ls = isl_local_space_from_space(dim);
 573
 574         c = isl_equality_alloc(isl_local_space_copy(ls));
 575         isl_int_set_si(v, 1);
 576         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 577         isl_int_set_si(v, -1);
 578         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 579         isl_int_set_si(v, -2);
 580         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 581         bset = isl_basic_set_add_constraint(bset, c);
 582
 583         c = isl_equality_alloc(isl_local_space_copy(ls));
 584         isl_int_set_si(v, -1);
 585         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 586         isl_int_set_si(v, 3);
 587         isl_constraint_set_coefficient(c, isl_dim_set, 3, v);
 588         isl_int_set_si(v, 2);
 589         isl_constraint_set_constant(c, v);
 590         bset = isl_basic_set_add_constraint(bset, c);
 591
 592         bset = isl_basic_set_project_out(bset, isl_dim_set, 2, 2);
 593
 594         bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
 595
 596         assert(!isl_basic_set_is_empty(bset));
 597
 598         isl_local_space_free(ls);
 599         isl_basic_set_free(bset);
 600
 601         /* test 10 */
 602         dim = isl_space_set_alloc(ctx, 0, 3);
 603         bset = isl_basic_set_universe(isl_space_copy(dim));
 604         ls = isl_local_space_from_space(dim);
 605
 606         c = isl_equality_alloc(isl_local_space_copy(ls));
 607         isl_int_set_si(v, 1);
 608         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 609         isl_int_set_si(v, -2);
 610         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 611         bset = isl_basic_set_add_constraint(bset, c);
 612
 613         bset = isl_basic_set_project_out(bset, isl_dim_set, 2, 1);
 614
 615         bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
 616
 617         isl_local_space_free(ls);
 618         isl_basic_set_free(bset);
 619
 620         isl_int_clear(v);
 621
 622         str = "{ [i] : exists (e0, e1: 3e1 >= 1 + 2e0 and "
 623             "8e1 <= -1 + 5i - 5e0 and 2e1 >= 1 + 2i - 5e0) }";
 624         set = isl_set_read_from_str(ctx, str);
 625         set = isl_set_compute_divs(set);
 626         isl_set_free(set);
 627         if (!set)
 628                 return -1;
 629
 630         str = "{ [i,j] : 2*[i/2] + 3 * [j/4] <= 10 and 2 i = j }";
 631         bset = isl_basic_set_read_from_str(ctx, str);
 632         n = isl_basic_set_dim(bset, isl_dim_div);
 633         isl_basic_set_free(bset);
 634         if (!bset)
 635                 return -1;
 636         if (n != 0)
 637                 isl_die(ctx, isl_error_unknown,
 638                         "expecting no existentials", return -1);
 639
 640         str = "{ [i,j,k] : 3 + i + 2j >= 0 and 2 * [(i+2j)/4] <= k }";
 641         set = isl_set_read_from_str(ctx, str);
 642         set = isl_set_remove_divs_involving_dims(set, isl_dim_set, 0, 2);
 643         set = isl_set_fix_si(set, isl_dim_set, 2, -3);
 644         empty = isl_set_is_empty(set);
 645         isl_set_free(set);
 646         if (empty < 0)
 647                 return -1;
 648         if (!empty)
 649                 isl_die(ctx, isl_error_unknown,
 650                         "result not as accurate as expected", return -1);
 651
 652         return 0;
 653 }
 654
 655 void test_application_case(struct isl_ctx *ctx, const char *name)
 656 {
 657         char *filename;
 658         FILE *input;
 659         struct isl_basic_set *bset1, *bset2;
 660         struct isl_basic_map *bmap;
 661
 662         filename = get_filename(ctx, name, "omega");
 663         assert(filename);
 664         input = fopen(filename, "r");
 665         assert(input);
 666
 667         bset1 = isl_basic_set_read_from_file(ctx, input);
 668         bmap = isl_basic_map_read_from_file(ctx, input);
 669
 670         bset1 = isl_basic_set_apply(bset1, bmap);
 671
 672         bset2 = isl_basic_set_read_from_file(ctx, input);
 673
 674         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 675
 676         isl_basic_set_free(bset1);
 677         isl_basic_set_free(bset2);
 678         free(filename);
 679
 680         fclose(input);
 681 }
 682
 683 void test_application(struct isl_ctx *ctx)
 684 {
 685         test_application_case(ctx, "application");
 686         test_application_case(ctx, "application2");
 687 }
 688
 689 void test_affine_hull_case(struct isl_ctx *ctx, const char *name)
 690 {
 691         char *filename;
 692         FILE *input;
 693         struct isl_basic_set *bset1, *bset2;
 694
 695         filename = get_filename(ctx, name, "polylib");
 696         assert(filename);
 697         input = fopen(filename, "r");
 698         assert(input);
 699
 700         bset1 = isl_basic_set_read_from_file(ctx, input);
 701         bset2 = isl_basic_set_read_from_file(ctx, input);
 702
 703         bset1 = isl_basic_set_affine_hull(bset1);
 704
 705         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 706
 707         isl_basic_set_free(bset1);
 708         isl_basic_set_free(bset2);
 709         free(filename);
 710
 711         fclose(input);
 712 }
 713
 714 int test_affine_hull(struct isl_ctx *ctx)
 715 {
 716         const char *str;
 717         isl_set *set;
 718         isl_basic_set *bset;
 719         int n;
 720
 721         test_affine_hull_case(ctx, "affine2");
 722         test_affine_hull_case(ctx, "affine");
 723         test_affine_hull_case(ctx, "affine3");
 724
 725         str = "[m] -> { [i0] : exists (e0, e1: e1 <= 1 + i0 and "
 726                         "m >= 3 and 4i0 <= 2 + m and e1 >= i0 and "
 727                         "e1 >= 0 and e1 <= 2 and e1 >= 1 + 2e0 and "
 728                         "2e1 <= 1 + m + 4e0 and 2e1 >= 2 - m + 4i0 - 4e0) }";
 729         set = isl_set_read_from_str(ctx, str);
 730         bset = isl_set_affine_hull(set);
 731         n = isl_basic_set_dim(bset, isl_dim_div);
 732         isl_basic_set_free(bset);
 733         if (n != 0)
 734                 isl_die(ctx, isl_error_unknown, "not expecting any divs",
 735                         return -1);
 736
 737         return 0;
 738 }
 739
 740 void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
 741 {
 742         char *filename;
 743         FILE *input;
 744         struct isl_basic_set *bset1, *bset2;
 745         struct isl_set *set;
 746
 747         filename = get_filename(ctx, name, "polylib");
 748         assert(filename);
 749         input = fopen(filename, "r");
 750         assert(input);
 751
 752         bset1 = isl_basic_set_read_from_file(ctx, input);
 753         bset2 = isl_basic_set_read_from_file(ctx, input);
 754
 755         set = isl_basic_set_union(bset1, bset2);
 756         bset1 = isl_set_convex_hull(set);
 757
 758         bset2 = isl_basic_set_read_from_file(ctx, input);
 759
 760         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 761
 762         isl_basic_set_free(bset1);
 763         isl_basic_set_free(bset2);
 764         free(filename);
 765
 766         fclose(input);
 767 }
 768
 769 void test_convex_hull_algo(struct isl_ctx *ctx, int convex)
 770 {
 771         const char *str1, *str2;
 772         isl_set *set1, *set2;
 773         int orig_convex = ctx->opt->convex;
 774         ctx->opt->convex = convex;
 775
 776         test_convex_hull_case(ctx, "convex0");
 777         test_convex_hull_case(ctx, "convex1");
 778         test_convex_hull_case(ctx, "convex2");
 779         test_convex_hull_case(ctx, "convex3");
 780         test_convex_hull_case(ctx, "convex4");
 781         test_convex_hull_case(ctx, "convex5");
 782         test_convex_hull_case(ctx, "convex6");
 783         test_convex_hull_case(ctx, "convex7");
 784         test_convex_hull_case(ctx, "convex8");
 785         test_convex_hull_case(ctx, "convex9");
 786         test_convex_hull_case(ctx, "convex10");
 787         test_convex_hull_case(ctx, "convex11");
 788         test_convex_hull_case(ctx, "convex12");
 789         test_convex_hull_case(ctx, "convex13");
 790         test_convex_hull_case(ctx, "convex14");
 791         test_convex_hull_case(ctx, "convex15");
 792
 793         str1 = "{ [i0, i1, i2] : (i2 = 1 and i0 = 0 and i1 >= 0) or "
 794                "(i0 = 1 and i1 = 0 and i2 = 1) or "
 795                "(i0 = 0 and i1 = 0 and i2 = 0) }";
 796         str2 = "{ [i0, i1, i2] : i0 >= 0 and i2 >= i0 and i2 <= 1 and i1 >= 0 }";
 797         set1 = isl_set_read_from_str(ctx, str1);
 798         set2 = isl_set_read_from_str(ctx, str2);
 799         set1 = isl_set_from_basic_set(isl_set_convex_hull(set1));
 800         assert(isl_set_is_equal(set1, set2));
 801         isl_set_free(set1);
 802         isl_set_free(set2);
 803
 804         ctx->opt->convex = orig_convex;
 805 }
 806
 807 void test_convex_hull(struct isl_ctx *ctx)
 808 {
 809         test_convex_hull_algo(ctx, ISL_CONVEX_HULL_FM);
 810         test_convex_hull_algo(ctx, ISL_CONVEX_HULL_WRAP);
 811 }
 812
 813 void test_gist_case(struct isl_ctx *ctx, const char *name)
 814 {
 815         char *filename;
 816         FILE *input;
 817         struct isl_basic_set *bset1, *bset2;
 818
 819         filename = get_filename(ctx, name, "polylib");
 820         assert(filename);
 821         input = fopen(filename, "r");
 822         assert(input);
 823
 824         bset1 = isl_basic_set_read_from_file(ctx, input);
 825         bset2 = isl_basic_set_read_from_file(ctx, input);
 826
 827         bset1 = isl_basic_set_gist(bset1, bset2);
 828
 829         bset2 = isl_basic_set_read_from_file(ctx, input);
 830
 831         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 832
 833         isl_basic_set_free(bset1);
 834         isl_basic_set_free(bset2);
 835         free(filename);
 836
 837         fclose(input);
 838 }
 839
 840 void test_gist(struct isl_ctx *ctx)
 841 {
 842         const char *str;
 843         isl_basic_set *bset1, *bset2;
 844
 845         test_gist_case(ctx, "gist1");
 846
 847         str = "[p0, p2, p3, p5, p6, p10] -> { [] : "
 848             "exists (e0 = [(15 + p0 + 15p6 + 15p10)/16], e1 = [(p5)/8], "
 849             "e2 = [(p6)/128], e3 = [(8p2 - p5)/128], "
 850             "e4 = [(128p3 - p6)/4096]: 8e1 = p5 and 128e2 = p6 and "
 851             "128e3 = 8p2 - p5 and 4096e4 = 128p3 - p6 and p2 >= 0 and "
 852             "16e0 >= 16 + 16p6 + 15p10 and  p2 <= 15 and p3 >= 0 and "
 853             "p3 <= 31 and  p6 >= 128p3 and p5 >= 8p2 and p10 >= 0 and "
 854             "16e0 <= 15 + p0 + 15p6 + 15p10 and 16e0 >= p0 + 15p6 + 15p10 and "
 855             "p10 <= 15 and p10 <= -1 + p0 - p6) }";
 856         bset1 = isl_basic_set_read_from_str(ctx, str);
 857         str = "[p0, p2, p3, p5, p6, p10] -> { [] : exists (e0 = [(p5)/8], "
 858             "e1 = [(p6)/128], e2 = [(8p2 - p5)/128], "
 859             "e3 = [(128p3 - p6)/4096]: 8e0 = p5 and 128e1 = p6 and "
 860             "128e2 = 8p2 - p5 and 4096e3 = 128p3 - p6 and p5 >= -7 and "
 861             "p2 >= 0 and 8p2 <= -1 + p0 and p2 <= 15 and p3 >= 0 and "
 862             "p3 <= 31 and 128p3 <= -1 + p0 and p6 >= -127 and "
 863             "p5 <= -1 + p0 and p6 <= -1 + p0 and p6 >= 128p3 and "
 864             "p0 >= 1 and p5 >= 8p2 and p10 >= 0 and p10 <= 15 ) }";
 865         bset2 = isl_basic_set_read_from_str(ctx, str);
 866         bset1 = isl_basic_set_gist(bset1, bset2);
 867         assert(bset1 && bset1->n_div == 0);
 868         isl_basic_set_free(bset1);
 869 }
 870
 871 int test_coalesce_set(isl_ctx *ctx, const char *str, int check_one)
 872 {
 873         isl_set *set, *set2;
 874         int equal;
 875         int one;
 876
 877         set = isl_set_read_from_str(ctx, str);
 878         set = isl_set_coalesce(set);
 879         set2 = isl_set_read_from_str(ctx, str);
 880         equal = isl_set_is_equal(set, set2);
 881         one = set && set->n == 1;
 882         isl_set_free(set);
 883         isl_set_free(set2);
 884
 885         if (equal < 0)
 886                 return -1;
 887         if (!equal)
 888                 isl_die(ctx, isl_error_unknown,
 889                         "coalesced set not equal to input", return -1);
 890         if (check_one && !one)
 891                 isl_die(ctx, isl_error_unknown,
 892                         "coalesced set should not be a union", return -1);
 893
 894         return 0;
 895 }
 896
 897 int test_coalesce_unbounded_wrapping(isl_ctx *ctx)
 898 {
 899         int r = 0;
 900         int bounded;
 901
 902         bounded = isl_options_get_coalesce_bounded_wrapping(ctx);
 903         isl_options_set_coalesce_bounded_wrapping(ctx, 0);
 904
 905         if (test_coalesce_set(ctx,
 906                 "{[x,y,z] : y + 2 >= 0 and x - y + 1 >= 0 and "
 907                         "-x - y + 1 >= 0 and -3 <= z <= 3;"
 908                 "[x,y,z] : -x+z + 20 >= 0 and -x-z + 20 >= 0 and "
 909                         "x-z + 20 >= 0 and x+z + 20 >= 0 and "
 910                         "-10 <= y <= 0}", 1) < 0)
 911                 goto error;
 912         if (test_coalesce_set(ctx,
 913                 "{[x,y] : 0 <= x,y <= 10; [5,y]: 4 <=y <= 11}", 1) < 0)
 914                 goto error;
 915         if (test_coalesce_set(ctx,
 916                 "{[x,0,0] : -5 <= x <= 5; [0,y,1] : -5 <= y <= 5 }", 1) < 0)
 917                 goto error;
 918
 919         if (0) {
 920 error:
 921                 r = -1;
 922         }
 923
 924         isl_options_set_coalesce_bounded_wrapping(ctx, bounded);
 925
 926         return r;
 927 }
 928
 929 int test_coalesce(struct isl_ctx *ctx)
 930 {
 931         const char *str;
 932         struct isl_set *set, *set2;
 933         struct isl_map *map, *map2;
 934
 935         set = isl_set_read_from_str(ctx,
 936                 "{[x,y]: x >= 0 & x <= 10 & y >= 0 & y <= 10 or "
 937                        "y >= x & x >= 2 & 5 >= y }");
 938         set = isl_set_coalesce(set);
 939         assert(set && set->n == 1);
 940         isl_set_free(set);
 941
 942         set = isl_set_read_from_str(ctx,
 943                 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
 944                        "x + y >= 10 & y <= x & x + y <= 20 & y >= 0}");
 945         set = isl_set_coalesce(set);
 946         assert(set && set->n == 1);
 947         isl_set_free(set);
 948
 949         set = isl_set_read_from_str(ctx,
 950                 "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0 or "
 951                        "x + y >= 10 & y <= x & x + y <= 19 & y >= 0}");
 952         set = isl_set_coalesce(set);
 953         assert(set && set->n == 2);
 954         isl_set_free(set);
 955
 956         set = isl_set_read_from_str(ctx,
 957                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 958                        "y >= 0 & x >= 6 & x <= 10 & y <= x}");
 959         set = isl_set_coalesce(set);
 960         assert(set && set->n == 1);
 961         isl_set_free(set);
 962
 963         set = isl_set_read_from_str(ctx,
 964                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 965                        "y >= 0 & x >= 7 & x <= 10 & y <= x}");
 966         set = isl_set_coalesce(set);
 967         assert(set && set->n == 2);
 968         isl_set_free(set);
 969
 970         set = isl_set_read_from_str(ctx,
 971                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 972                        "y >= 0 & x >= 6 & x <= 10 & y + 1 <= x}");
 973         set = isl_set_coalesce(set);
 974         assert(set && set->n == 2);
 975         isl_set_free(set);
 976
 977         set = isl_set_read_from_str(ctx,
 978                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 979                        "y >= 0 & x = 6 & y <= 6}");
 980         set = isl_set_coalesce(set);
 981         assert(set && set->n == 1);
 982         isl_set_free(set);
 983
 984         set = isl_set_read_from_str(ctx,
 985                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 986                        "y >= 0 & x = 7 & y <= 6}");
 987         set = isl_set_coalesce(set);
 988         assert(set && set->n == 2);
 989         isl_set_free(set);
 990
 991         set = isl_set_read_from_str(ctx,
 992                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 993                        "y >= 0 & x = 6 & y <= 5}");
 994         set = isl_set_coalesce(set);
 995         assert(set && set->n == 1);
 996         set2 = isl_set_read_from_str(ctx,
 997                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
 998                        "y >= 0 & x = 6 & y <= 5}");
 999         assert(isl_set_is_equal(set, set2));
1000         isl_set_free(set);
1001         isl_set_free(set2);
1002
1003         set = isl_set_read_from_str(ctx,
1004                 "{[x,y]: y >= 0 & x <= 5 & y <= x or "
1005                        "y >= 0 & x = 6 & y <= 7}");
1006         set = isl_set_coalesce(set);
1007         assert(set && set->n == 2);
1008         isl_set_free(set);
1009
1010         set = isl_set_read_from_str(ctx,
1011                 "[n] -> { [i] : i = 1 and n >= 2 or 2 <= i and i <= n }");
1012         set = isl_set_coalesce(set);
1013         assert(set && set->n == 1);
1014         set2 = isl_set_read_from_str(ctx,
1015                 "[n] -> { [i] : i = 1 and n >= 2 or 2 <= i and i <= n }");
1016         assert(isl_set_is_equal(set, set2));
1017         isl_set_free(set);
1018         isl_set_free(set2);
1019
1020         set = isl_set_read_from_str(ctx,
1021                 "{[x,y] : x >= 0 and y >= 0 or 0 <= y and y <= 5 and x = -1}");
1022         set = isl_set_coalesce(set);
1023         set2 = isl_set_read_from_str(ctx,
1024                 "{[x,y] : x >= 0 and y >= 0 or 0 <= y and y <= 5 and x = -1}");
1025         assert(isl_set_is_equal(set, set2));
1026         isl_set_free(set);
1027         isl_set_free(set2);
1028
1029         set = isl_set_read_from_str(ctx,
1030                 "[n] -> { [i] : 1 <= i and i <= n - 1 or "
1031                                 "2 <= i and i <= n }");
1032         set = isl_set_coalesce(set);
1033         assert(set && set->n == 1);
1034         set2 = isl_set_read_from_str(ctx,
1035                 "[n] -> { [i] : 1 <= i and i <= n - 1 or "
1036                                 "2 <= i and i <= n }");
1037         assert(isl_set_is_equal(set, set2));
1038         isl_set_free(set);
1039         isl_set_free(set2);
1040
1041         map = isl_map_read_from_str(ctx,
1042                 "[n] -> { [i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
1043                 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
1044                 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
1045                 "4e4 = -2 + o0 and i0 >= 8 + 2n and o0 >= 2 + i0 and "
1046                 "o0 <= 56 + 2n and o0 <= -12 + 4n and i0 <= 57 + 2n and "
1047                 "i0 <= -11 + 4n and o0 >= 6 + 2n and 4e0 <= i0 and "
1048                 "4e0 >= -3 + i0 and 4e1 <= o0 and 4e1 >= -3 + o0 and "
1049                 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0);"
1050                 "[i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
1051                 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
1052                 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
1053                 "4e4 = -2 + o0 and 2e0 >= 3 + n and e0 <= -4 + n and "
1054                 "2e0 <= 27 + n and e1 <= -4 + n and 2e1 <= 27 + n and "
1055                 "2e1 >= 2 + n and e1 >= 1 + e0 and i0 >= 7 + 2n and "
1056                 "i0 <= -11 + 4n and i0 <= 57 + 2n and 4e0 <= -2 + i0 and "
1057                 "4e0 >= -3 + i0 and o0 >= 6 + 2n and o0 <= -11 + 4n and "
1058                 "o0 <= 57 + 2n and 4e1 <= -2 + o0 and 4e1 >= -3 + o0 and "
1059                 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0 ) }");
1060         map = isl_map_coalesce(map);
1061         map2 = isl_map_read_from_str(ctx,
1062                 "[n] -> { [i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
1063                 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
1064                 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
1065                 "4e4 = -2 + o0 and i0 >= 8 + 2n and o0 >= 2 + i0 and "
1066                 "o0 <= 56 + 2n and o0 <= -12 + 4n and i0 <= 57 + 2n and "
1067                 "i0 <= -11 + 4n and o0 >= 6 + 2n and 4e0 <= i0 and "
1068                 "4e0 >= -3 + i0 and 4e1 <= o0 and 4e1 >= -3 + o0 and "
1069                 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0);"
1070                 "[i0] -> [o0] : exists (e0 = [(i0)/4], e1 = [(o0)/4], "
1071                 "e2 = [(n)/2], e3 = [(-2 + i0)/4], e4 = [(-2 + o0)/4], "
1072                 "e5 = [(-2n + i0)/4]: 2e2 = n and 4e3 = -2 + i0 and "
1073                 "4e4 = -2 + o0 and 2e0 >= 3 + n and e0 <= -4 + n and "
1074                 "2e0 <= 27 + n and e1 <= -4 + n and 2e1 <= 27 + n and "
1075                 "2e1 >= 2 + n and e1 >= 1 + e0 and i0 >= 7 + 2n and "
1076                 "i0 <= -11 + 4n and i0 <= 57 + 2n and 4e0 <= -2 + i0 and "
1077                 "4e0 >= -3 + i0 and o0 >= 6 + 2n and o0 <= -11 + 4n and "
1078                 "o0 <= 57 + 2n and 4e1 <= -2 + o0 and 4e1 >= -3 + o0 and "
1079                 "4e5 <= -2n + i0 and 4e5 >= -3 - 2n + i0 ) }");
1080         assert(isl_map_is_equal(map, map2));
1081         isl_map_free(map);
1082         isl_map_free(map2);
1083
1084         str = "[n, m] -> { [] -> [o0, o2, o3] : (o3 = 1 and o0 >= 1 + m and "
1085               "o0 <= n + m and o2 <= m and o0 >= 2 + n and o2 >= 3) or "
1086               "(o0 >= 2 + n and o0 >= 1 + m and o0 <= n + m and n >= 1 and "
1087               "o3 <= -1 + o2 and o3 >= 1 - m + o2 and o3 >= 2 and o3 <= n) }";
1088         map = isl_map_read_from_str(ctx, str);
1089         map = isl_map_coalesce(map);
1090         map2 = isl_map_read_from_str(ctx, str);
1091         assert(isl_map_is_equal(map, map2));
1092         isl_map_free(map);
1093         isl_map_free(map2);
1094
1095         str = "[M, N] -> { [i0, i1, i2, i3, i4, i5, i6] -> "
1096           "[o0, o1, o2, o3, o4, o5, o6] : "
1097           "(o6 <= -4 + 2M - 2N + i0 + i1 - i2 + i6 - o0 - o1 + o2 and "
1098           "o3 <= -2 + i3 and o6 >= 2 + i0 + i3 + i6 - o0 - o3 and "
1099           "o6 >= 2 - M + N + i3 + i4 + i6 - o3 - o4 and o0 <= -1 + i0 and "
1100           "o4 >= 4 - 3M + 3N - i0 - i1 + i2 + 2i3 + i4 + o0 + o1 - o2 - 2o3 "
1101           "and o6 <= -3 + 2M - 2N + i3 + i4 - i5 + i6 - o3 - o4 + o5 and "
1102           "2o6 <= -5 + 5M - 5N + 2i0 + i1 - i2 - i5 + 2i6 - 2o0 - o1 + o2 + o5 "
1103           "and o6 >= 2i0 + i1 + i6 - 2o0 - o1 and "
1104           "3o6 <= -5 + 4M - 4N + 2i0 + i1 - i2 + 2i3 + i4 - i5 + 3i6 "
1105           "- 2o0 - o1 + o2 - 2o3 - o4 + o5) or "
1106           "(N >= 2 and o3 <= -1 + i3 and o0 <= -1 + i0 and "
1107           "o6 >= i3 + i6 - o3 and M >= 0 and "
1108           "2o6 >= 1 + i0 + i3 + 2i6 - o0 - o3 and "
1109           "o6 >= 1 - M + i0 + i6 - o0 and N >= 2M and o6 >= i0 + i6 - o0) }";
1110         map = isl_map_read_from_str(ctx, str);
1111         map = isl_map_coalesce(map);
1112         map2 = isl_map_read_from_str(ctx, str);
1113         assert(isl_map_is_equal(map, map2));
1114         isl_map_free(map);
1115         isl_map_free(map2);
1116
1117         str = "[M, N] -> { [] -> [o0] : (o0 = 0 and M >= 1 and N >= 2) or "
1118                 "(o0 = 0 and M >= 1 and N >= 2M and N >= 2 + M) or "
1119                 "(o0 = 0 and M >= 2 and N >= 3) or "
1120                 "(M = 0 and o0 = 0 and N >= 3) }";
1121         map = isl_map_read_from_str(ctx, str);
1122         map = isl_map_coalesce(map);
1123         map2 = isl_map_read_from_str(ctx, str);
1124         assert(isl_map_is_equal(map, map2));
1125         isl_map_free(map);
1126         isl_map_free(map2);
1127
1128         str = "{ [i0, i1, i2, i3] : (i1 = 10i0 and i0 >= 1 and 10i0 <= 100 and "
1129                 "i3 <= 9 + 10 i2 and i3 >= 1 + 10i2 and i3 >= 0) or "
1130                 "(i1 <= 9 + 10i0 and i1 >= 1 + 10i0 and i2 >= 0 and "
1131                 "i0 >= 0 and i1 <= 100 and i3 <= 9 + 10i2 and i3 >= 1 + 10i2) }";
1132         map = isl_map_read_from_str(ctx, str);
1133         map = isl_map_coalesce(map);
1134         map2 = isl_map_read_from_str(ctx, str);
1135         assert(isl_map_is_equal(map, map2));
1136         isl_map_free(map);
1137         isl_map_free(map2);
1138
1139         test_coalesce_set(ctx,
1140                 "[M] -> { [i1] : (i1 >= 2 and i1 <= M) or "
1141                                 "(i1 = M and M >= 1) }", 0);
1142         test_coalesce_set(ctx,
1143                 "{[x,y] : x,y >= 0; [x,y] : 10 <= x <= 20 and y >= -1 }", 0);
1144         test_coalesce_set(ctx,
1145                 "{ [x, y] : (x >= 1 and y >= 1 and x <= 2 and y <= 2) or "
1146                 "(y = 3 and x = 1) }", 1);
1147         test_coalesce_set(ctx,
1148                 "[M] -> { [i0, i1, i2, i3, i4] : (i1 >= 3 and i4 >= 2 + i2 and "
1149                 "i2 >= 2 and i0 >= 2 and i3 >= 1 + i2 and i0 <= M and "
1150                 "i1 <= M and i3 <= M and i4 <= M) or "
1151                 "(i1 >= 2 and i4 >= 1 + i2 and i2 >= 2 and i0 >= 2 and "
1152                 "i3 >= 1 + i2 and i0 <= M and i1 <= -1 + M and i3 <= M and "
1153                 "i4 <= -1 + M) }", 1);
1154         test_coalesce_set(ctx,
1155                 "{ [x, y] : (x >= 0 and y >= 0 and x <= 10 and y <= 10) or "
1156                 "(x >= 1 and y >= 1 and x <= 11 and y <= 11) }", 1);
1157         if (test_coalesce_unbounded_wrapping(ctx) < 0)
1158                 return -1;
1159         if (test_coalesce_set(ctx, "{[x,0] : x >= 0; [x,1] : x <= 20}", 0) < 0)
1160                 return -1;
1161         if (test_coalesce_set(ctx, "{ [x, 1 - x] : 0 <= x <= 1; [0,0] }", 1) < 0)
1162                 return -1;
1163         if (test_coalesce_set(ctx, "{ [0,0]; [i,i] : 1 <= i <= 10 }", 1) < 0)
1164                 return -1;
1165         if (test_coalesce_set(ctx, "{ [0,0]; [i,j] : 1 <= i,j <= 10 }", 0) < 0)
1166                 return -1;
1167         if (test_coalesce_set(ctx, "{ [0,0]; [i,2i] : 1 <= i <= 10 }", 1) < 0)
1168                 return -1;
1169         if (test_coalesce_set(ctx, "{ [0,0]; [i,2i] : 2 <= i <= 10 }", 0) < 0)
1170                 return -1;
1171         if (test_coalesce_set(ctx, "{ [1,0]; [i,2i] : 1 <= i <= 10 }", 0) < 0)
1172                 return -1;
1173         if (test_coalesce_set(ctx, "{ [0,1]; [i,2i] : 1 <= i <= 10 }", 0) < 0)
1174                 return -1;
1175         if (test_coalesce_set(ctx, "{ [a, b] : exists e : 2e = a and "
1176                     "a >= 0 and (a <= 3 or (b <= 0 and b >= -4 + a)) }", 0) < 0)
1177                 return -1;
1178         if (test_coalesce_set(ctx,
1179                 "{ [i, j, i', j'] : i <= 2 and j <= 2 and "
1180                         "j' >= -1 + 2i + j - 2i' and i' <= -1 + i and "
1181                         "j >= 1 and j' <= i + j - i' and i >= 1; "
1182                 "[1, 1, 1, 1] }", 0) < 0)
1183                 return -1;
1184         if (test_coalesce_set(ctx, "{ [i,j] : exists a,b : i = 2a and j = 3b; "
1185                                      "[i,j] : exists a : j = 3a }", 1) < 0)
1186                 return -1;
1187         return 0;
1188 }
1189
1190 void test_closure(struct isl_ctx *ctx)
1191 {
1192         const char *str;
1193         isl_set *dom;
1194         isl_map *up, *right;
1195         isl_map *map, *map2;
1196         int exact;
1197
1198         /* COCOA example 1 */
1199         map = isl_map_read_from_str(ctx,
1200                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 1 and j2 = j + 1 and "
1201                         "1 <= i and i < n and 1 <= j and j < n or "
1202                         "i2 = i + 1 and j2 = j - 1 and "
1203                         "1 <= i and i < n and 2 <= j and j <= n }");
1204         map = isl_map_power(map, &exact);
1205         assert(exact);
1206         isl_map_free(map);
1207
1208         /* COCOA example 1 */
1209         map = isl_map_read_from_str(ctx,
1210                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 1 and j2 = j + 1 and "
1211                         "1 <= i and i < n and 1 <= j and j < n or "
1212                         "i2 = i + 1 and j2 = j - 1 and "
1213                         "1 <= i and i < n and 2 <= j and j <= n }");
1214         map = isl_map_transitive_closure(map, &exact);
1215         assert(exact);
1216         map2 = isl_map_read_from_str(ctx,
1217                 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k : "
1218                         "1 <= i and i < n and 1 <= j and j <= n and "
1219                         "2 <= i2 and i2 <= n and 1 <= j2 and j2 <= n and "
1220                         "i2 = i + k1 + k2 and j2 = j + k1 - k2 and "
1221                         "k1 >= 0 and k2 >= 0 and k1 + k2 = k and k >= 1 )}");
1222         assert(isl_map_is_equal(map, map2));
1223         isl_map_free(map2);
1224         isl_map_free(map);
1225
1226         map = isl_map_read_from_str(ctx,
1227                 "[n] -> { [x] -> [y] : y = x + 1 and 0 <= x and x <= n and "
1228                                      " 0 <= y and y <= n }");
1229         map = isl_map_transitive_closure(map, &exact);
1230         map2 = isl_map_read_from_str(ctx,
1231                 "[n] -> { [x] -> [y] : y > x and 0 <= x and x <= n and "
1232                                      " 0 <= y and y <= n }");
1233         assert(isl_map_is_equal(map, map2));
1234         isl_map_free(map2);
1235         isl_map_free(map);
1236
1237         /* COCOA example 2 */
1238         map = isl_map_read_from_str(ctx,
1239                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 2 and j2 = j + 2 and "
1240                         "1 <= i and i < n - 1 and 1 <= j and j < n - 1 or "
1241                         "i2 = i + 2 and j2 = j - 2 and "
1242                         "1 <= i and i < n - 1 and 3 <= j and j <= n }");
1243         map = isl_map_transitive_closure(map, &exact);
1244         assert(exact);
1245         map2 = isl_map_read_from_str(ctx,
1246                 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k : "
1247                         "1 <= i and i < n - 1 and 1 <= j and j <= n and "
1248                         "3 <= i2 and i2 <= n and 1 <= j2 and j2 <= n and "
1249                         "i2 = i + 2 k1 + 2 k2 and j2 = j + 2 k1 - 2 k2 and "
1250                         "k1 >= 0 and k2 >= 0 and k1 + k2 = k and k >= 1) }");
1251         assert(isl_map_is_equal(map, map2));
1252         isl_map_free(map);
1253         isl_map_free(map2);
1254
1255         /* COCOA Fig.2 left */
1256         map = isl_map_read_from_str(ctx,
1257                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 2 and j2 = j and "
1258                         "i <= 2 j - 3 and i <= n - 2 and j <= 2 i - 1 and "
1259                         "j <= n or "
1260                         "i2 = i and j2 = j + 2 and i <= 2 j - 1 and i <= n and "
1261                         "j <= 2 i - 3 and j <= n - 2 or "
1262                         "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
1263                         "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }");
1264         map = isl_map_transitive_closure(map, &exact);
1265         assert(exact);
1266         isl_map_free(map);
1267
1268         /* COCOA Fig.2 right */
1269         map = isl_map_read_from_str(ctx,
1270                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 3 and j2 = j and "
1271                         "i <= 2 j - 4 and i <= n - 3 and j <= 2 i - 1 and "
1272                         "j <= n or "
1273                         "i2 = i and j2 = j + 3 and i <= 2 j - 1 and i <= n and "
1274                         "j <= 2 i - 4 and j <= n - 3 or "
1275                         "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
1276                         "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }");
1277         map = isl_map_power(map, &exact);
1278         assert(exact);
1279         isl_map_free(map);
1280
1281         /* COCOA Fig.2 right */
1282         map = isl_map_read_from_str(ctx,
1283                 "[n] -> { [i,j] -> [i2,j2] : i2 = i + 3 and j2 = j and "
1284                         "i <= 2 j - 4 and i <= n - 3 and j <= 2 i - 1 and "
1285                         "j <= n or "
1286                         "i2 = i and j2 = j + 3 and i <= 2 j - 1 and i <= n and "
1287                         "j <= 2 i - 4 and j <= n - 3 or "
1288                         "i2 = i + 1 and j2 = j + 1 and i <= 2 j - 1 and "
1289                         "i <= n - 1 and j <= 2 i - 1 and j <= n - 1 }");
1290         map = isl_map_transitive_closure(map, &exact);
1291         assert(exact);
1292         map2 = isl_map_read_from_str(ctx,
1293                 "[n] -> { [i,j] -> [i2,j2] : exists (k1,k2,k3,k : "
1294                         "i <= 2 j - 1 and i <= n and j <= 2 i - 1 and "
1295                         "j <= n and 3 + i + 2 j <= 3 n and "
1296                         "3 + 2 i + j <= 3n and i2 <= 2 j2 -1 and i2 <= n and "
1297                         "i2 <= 3 j2 - 4 and j2 <= 2 i2 -1 and j2 <= n and "
1298                         "13 + 4 j2 <= 11 i2 and i2 = i + 3 k1 + k3 and "
1299                         "j2 = j + 3 k2 + k3 and k1 >= 0 and k2 >= 0 and "
1300                         "k3 >= 0 and k1 + k2 + k3 = k and k > 0) }");
1301         assert(isl_map_is_equal(map, map2));
1302         isl_map_free(map2);
1303         isl_map_free(map);
1304
1305         /* COCOA Fig.1 right */
1306         dom = isl_set_read_from_str(ctx,
1307                 "{ [x,y] : x >= 0 and -2 x + 3 y >= 0 and x <= 3 and "
1308                         "2 x - 3 y + 3 >= 0 }");
1309         right = isl_map_read_from_str(ctx,
1310                 "{ [x,y] -> [x2,y2] : x2 = x + 1 and y2 = y }");
1311         up = isl_map_read_from_str(ctx,
1312                 "{ [x,y] -> [x2,y2] : x2 = x and y2 = y + 1 }");
1313         right = isl_map_intersect_domain(right, isl_set_copy(dom));
1314         right = isl_map_intersect_range(right, isl_set_copy(dom));
1315         up = isl_map_intersect_domain(up, isl_set_copy(dom));
1316         up = isl_map_intersect_range(up, dom);
1317         map = isl_map_union(up, right);
1318         map = isl_map_transitive_closure(map, &exact);
1319         assert(exact);
1320         map2 = isl_map_read_from_str(ctx,
1321                 "{ [0,0] -> [0,1]; [0,0] -> [1,1]; [0,1] -> [1,1]; "
1322                 "  [2,2] -> [3,2]; [2,2] -> [3,3]; [3,2] -> [3,3] }");
1323         assert(isl_map_is_equal(map, map2));
1324         isl_map_free(map2);
1325         isl_map_free(map);
1326
1327         /* COCOA Theorem 1 counter example */
1328         map = isl_map_read_from_str(ctx,
1329                 "{ [i,j] -> [i2,j2] : i = 0 and 0 <= j and j <= 1 and "
1330                         "i2 = 1 and j2 = j or "
1331                         "i = 0 and j = 0 and i2 = 0 and j2 = 1 }");
1332         map = isl_map_transitive_closure(map, &exact);
1333         assert(exact);
1334         isl_map_free(map);
1335
1336         map = isl_map_read_from_str(ctx,
1337                 "[m,n] -> { [i,j] -> [i2,j2] : i2 = i and j2 = j + 2 and "
1338                         "1 <= i,i2 <= n and 1 <= j,j2 <= m or "
1339                         "i2 = i + 1 and 3 <= j2 - j <= 4 and "
1340                         "1 <= i,i2 <= n and 1 <= j,j2 <= m }");
1341         map = isl_map_transitive_closure(map, &exact);
1342         assert(exact);
1343         isl_map_free(map);
1344
1345         /* Kelly et al 1996, fig 12 */
1346         map = isl_map_read_from_str(ctx,
1347                 "[n] -> { [i,j] -> [i2,j2] : i2 = i and j2 = j + 1 and "
1348                         "1 <= i,j,j+1 <= n or "
1349                         "j = n and j2 = 1 and i2 = i + 1 and "
1350                         "1 <= i,i+1 <= n }");
1351         map = isl_map_transitive_closure(map, &exact);
1352         assert(exact);
1353         map2 = isl_map_read_from_str(ctx,
1354                 "[n] -> { [i,j] -> [i2,j2] : 1 <= j < j2 <= n and "
1355                         "1 <= i <= n and i = i2 or "
1356                         "1 <= i < i2 <= n and 1 <= j <= n and "
1357                         "1 <= j2 <= n }");
1358         assert(isl_map_is_equal(map, map2));
1359         isl_map_free(map2);
1360         isl_map_free(map);
1361
1362         /* Omega's closure4 */
1363         map = isl_map_read_from_str(ctx,
1364                 "[m,n] -> { [x,y] -> [x2,y2] : x2 = x and y2 = y + 1 and "
1365                         "1 <= x,y <= 10 or "
1366                         "x2 = x + 1 and y2 = y and "
1367                         "1 <= x <= 20 && 5 <= y <= 15 }");
1368         map = isl_map_transitive_closure(map, &exact);
1369         assert(exact);
1370         isl_map_free(map);
1371
1372         map = isl_map_read_from_str(ctx,
1373                 "[n] -> { [x] -> [y]: 1 <= n <= y - x <= 10 }");
1374         map = isl_map_transitive_closure(map, &exact);
1375         assert(!exact);
1376         map2 = isl_map_read_from_str(ctx,
1377                 "[n] -> { [x] -> [y] : 1 <= n <= 10 and y >= n + x }");
1378         assert(isl_map_is_equal(map, map2));
1379         isl_map_free(map);
1380         isl_map_free(map2);
1381
1382         str = "[n, m] -> { [i0, i1, i2, i3] -> [o0, o1, o2, o3] : "
1383             "i3 = 1 and o0 = i0 and o1 = -1 + i1 and o2 = -1 + i2 and "
1384             "o3 = -2 + i2 and i1 <= -1 + i0 and i1 >= 1 - m + i0 and "
1385             "i1 >= 2 and i1 <= n and i2 >= 3 and i2 <= 1 + n and i2 <= m }";
1386         map = isl_map_read_from_str(ctx, str);
1387         map = isl_map_transitive_closure(map, &exact);
1388         assert(exact);
1389         map2 = isl_map_read_from_str(ctx, str);
1390         assert(isl_map_is_equal(map, map2));
1391         isl_map_free(map);
1392         isl_map_free(map2);
1393
1394         str = "{[0] -> [1]; [2] -> [3]}";
1395         map = isl_map_read_from_str(ctx, str);
1396         map = isl_map_transitive_closure(map, &exact);
1397         assert(exact);
1398         map2 = isl_map_read_from_str(ctx, str);
1399         assert(isl_map_is_equal(map, map2));
1400         isl_map_free(map);
1401         isl_map_free(map2);
1402
1403         str = "[n] -> { [[i0, i1, 1, 0, i0] -> [i5, 1]] -> "
1404             "[[i0, -1 + i1, 2, 0, i0] -> [-1 + i5, 2]] : "
1405             "exists (e0 = [(3 - n)/3]: i5 >= 2 and i1 >= 2 and "
1406             "3i0 <= -1 + n and i1 <= -1 + n and i5 <= -1 + n and "
1407             "3e0 >= 1 - n and 3e0 <= 2 - n and 3i0 >= -2 + n); "
1408             "[[i0, i1, 2, 0, i0] -> [i5, 1]] -> "
1409             "[[i0, i1, 1, 0, i0] -> [-1 + i5, 2]] : "
1410             "exists (e0 = [(3 - n)/3]: i5 >= 2 and i1 >= 1 and "
1411             "3i0 <= -1 + n and i1 <= -1 + n and i5 <= -1 + n and "
1412             "3e0 >= 1 - n and 3e0 <= 2 - n and 3i0 >= -2 + n); "
1413             "[[i0, i1, 1, 0, i0] -> [i5, 2]] -> "
1414             "[[i0, -1 + i1, 2, 0, i0] -> [i5, 1]] : "
1415             "exists (e0 = [(3 - n)/3]: i1 >= 2 and i5 >= 1 and "
1416             "3i0 <= -1 + n and i1 <= -1 + n and i5 <= -1 + n and "
1417             "3e0 >= 1 - n and 3e0 <= 2 - n and 3i0 >= -2 + n); "
1418             "[[i0, i1, 2, 0, i0] -> [i5, 2]] -> "
1419             "[[i0, i1, 1, 0, i0] -> [i5, 1]] : "
1420             "exists (e0 = [(3 - n)/3]: i5 >= 1 and i1 >= 1 and "
1421             "3i0 <= -1 + n and i1 <= -1 + n and i5 <= -1 + n and "
1422             "3e0 >= 1 - n and 3e0 <= 2 - n and 3i0 >= -2 + n) }";
1423         map = isl_map_read_from_str(ctx, str);
1424         map = isl_map_transitive_closure(map, NULL);
1425         assert(map);
1426         isl_map_free(map);
1427 }
1428
1429 void test_lex(struct isl_ctx *ctx)
1430 {
1431         isl_space *dim;
1432         isl_map *map;
1433
1434         dim = isl_space_set_alloc(ctx, 0, 0);
1435         map = isl_map_lex_le(dim);
1436         assert(!isl_map_is_empty(map));
1437         isl_map_free(map);
1438 }
1439
1440 void test_lexmin(struct isl_ctx *ctx)
1441 {
1442         const char *str;
1443         isl_basic_map *bmap;
1444         isl_map *map, *map2;
1445         isl_set *set;
1446         isl_set *set2;
1447         isl_pw_multi_aff *pma;
1448
1449         str = "[p0, p1] -> { [] -> [] : "
1450             "exists (e0 = [(2p1)/3], e1, e2, e3 = [(3 - p1 + 3e0)/3], "
1451             "e4 = [(p1)/3], e5 = [(p1 + 3e4)/3]: "
1452             "3e0 >= -2 + 2p1 and 3e0 >= p1 and 3e3 >= 1 - p1 + 3e0 and "
1453             "3e0 <= 2p1 and 3e3 >= -2 + p1 and 3e3 <= -1 + p1 and p1 >= 3 and "
1454             "3e5 >= -2 + 2p1 and 3e5 >= p1 and 3e5 <= -1 + p1 + 3e4 and "
1455             "3e4 <= p1 and 3e4 >= -2 + p1 and e3 <= -1 + e0 and "
1456             "3e4 >= 6 - p1 + 3e1 and 3e1 >= p1 and 3e5 >= -2 + p1 + 3e4 and "
1457             "2e4 >= 3 - p1 + 2e1 and e4 <= e1 and 3e3 <= 2 - p1 + 3e0 and "
1458             "e5 >= 1 + e1 and 3e4 >= 6 - 2p1 + 3e1 and "
1459             "p0 >= 2 and p1 >= p0 and 3e2 >= p1 and 3e4 >= 6 - p1 + 3e2 and "
1460             "e2 <= e1 and e3 >= 1 and e4 <= e2) }";
1461         map = isl_map_read_from_str(ctx, str);
1462         map = isl_map_lexmin(map);
1463         isl_map_free(map);
1464
1465         str = "[C] -> { [obj,a,b,c] : obj <= 38 a + 7 b + 10 c and "
1466             "a + b <= 1 and c <= 10 b and c <= C and a,b,c,C >= 0 }";
1467         set = isl_set_read_from_str(ctx, str);
1468         set = isl_set_lexmax(set);
1469         str = "[C] -> { [obj,a,b,c] : C = 8 }";
1470         set2 = isl_set_read_from_str(ctx, str);
1471         set = isl_set_intersect(set, set2);
1472         assert(!isl_set_is_empty(set));
1473         isl_set_free(set);
1474
1475         str = "{ [x] -> [y] : x <= y <= 10; [x] -> [5] : -8 <= x <= 8 }";
1476         map = isl_map_read_from_str(ctx, str);
1477         map = isl_map_lexmin(map);
1478         str = "{ [x] -> [5] : 6 <= x <= 8; "
1479                 "[x] -> [x] : x <= 5 or (9 <= x <= 10) }";
1480         map2 = isl_map_read_from_str(ctx, str);
1481         assert(isl_map_is_equal(map, map2));
1482         isl_map_free(map);
1483         isl_map_free(map2);
1484
1485         str = "{ [x] -> [y] : 4y = x or 4y = -1 + x or 4y = -2 + x }";
1486         map = isl_map_read_from_str(ctx, str);
1487         map2 = isl_map_copy(map);
1488         map = isl_map_lexmin(map);
1489         assert(isl_map_is_equal(map, map2));
1490         isl_map_free(map);
1491         isl_map_free(map2);
1492
1493         str = "{ [x] -> [y] : x = 4y; [x] -> [y] : x = 2y }";
1494         map = isl_map_read_from_str(ctx, str);
1495         map = isl_map_lexmin(map);
1496         str = "{ [x] -> [y] : (4y = x and x >= 0) or "
1497                 "(exists (e0 = [(x)/4], e1 = [(-2 + x)/4]: 2y = x and "
1498                 "4e1 = -2 + x and 4e0 <= -1 + x and 4e0 >= -3 + x)) or "
1499                 "(exists (e0 = [(x)/4]: 2y = x and 4e0 = x and x <= -4)) }";
1500         map2 = isl_map_read_from_str(ctx, str);
1501         assert(isl_map_is_equal(map, map2));
1502         isl_map_free(map);
1503         isl_map_free(map2);
1504
1505         str = "{ [i] -> [i', j] : j = i - 8i' and i' >= 0 and i' <= 7 and "
1506                                 " 8i' <= i and 8i' >= -7 + i }";
1507         bmap = isl_basic_map_read_from_str(ctx, str);
1508         pma = isl_basic_map_lexmin_pw_multi_aff(isl_basic_map_copy(bmap));
1509         map2 = isl_map_from_pw_multi_aff(pma);
1510         map = isl_map_from_basic_map(bmap);
1511         assert(isl_map_is_equal(map, map2));
1512         isl_map_free(map);
1513         isl_map_free(map2);
1514
1515         str = "{ T[a] -> S[b, c] : a = 4b-2c and c >= b }";
1516         map = isl_map_read_from_str(ctx, str);
1517         map = isl_map_lexmin(map);
1518         str = "{ T[a] -> S[b, c] : 2b = a and 2c = a }";
1519         map2 = isl_map_read_from_str(ctx, str);
1520         assert(isl_map_is_equal(map, map2));
1521         isl_map_free(map);
1522         isl_map_free(map2);
1523 }
1524
1525 struct must_may {
1526         isl_map *must;
1527         isl_map *may;
1528 };
1529
1530 static int collect_must_may(__isl_take isl_map *dep, int must,
1531         void *dep_user, void *user)
1532 {
1533         struct must_may *mm = (struct must_may *)user;
1534
1535         if (must)
1536                 mm->must = isl_map_union(mm->must, dep);
1537         else
1538                 mm->may = isl_map_union(mm->may, dep);
1539
1540         return 0;
1541 }
1542
1543 static int common_space(void *first, void *second)
1544 {
1545         int depth = *(int *)first;
1546         return 2 * depth;
1547 }
1548
1549 static int map_is_equal(__isl_keep isl_map *map, const char *str)
1550 {
1551         isl_map *map2;
1552         int equal;
1553
1554         if (!map)
1555                 return -1;
1556
1557         map2 = isl_map_read_from_str(map->ctx, str);
1558         equal = isl_map_is_equal(map, map2);
1559         isl_map_free(map2);
1560
1561         return equal;
1562 }
1563
1564 static int map_check_equal(__isl_keep isl_map *map, const char *str)
1565 {
1566         int equal;
1567
1568         equal = map_is_equal(map, str);
1569         if (equal < 0)
1570                 return -1;
1571         if (!equal)
1572                 isl_die(isl_map_get_ctx(map), isl_error_unknown,
1573                         "result not as expected", return -1);
1574         return 0;
1575 }
1576
1577 void test_dep(struct isl_ctx *ctx)
1578 {
1579         const char *str;
1580         isl_space *dim;
1581         isl_map *map;
1582         isl_access_info *ai;
1583         isl_flow *flow;
1584         int depth;
1585         struct must_may mm;
1586
1587         depth = 3;
1588
1589         str = "{ [2,i,0] -> [i] : 0 <= i <= 10 }";
1590         map = isl_map_read_from_str(ctx, str);
1591         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1592
1593         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1594         map = isl_map_read_from_str(ctx, str);
1595         ai = isl_access_info_add_source(ai, map, 1, &depth);
1596
1597         str = "{ [1,i,0] -> [5] : 0 <= i <= 10 }";
1598         map = isl_map_read_from_str(ctx, str);
1599         ai = isl_access_info_add_source(ai, map, 1, &depth);
1600
1601         flow = isl_access_info_compute_flow(ai);
1602         dim = isl_space_alloc(ctx, 0, 3, 3);
1603         mm.must = isl_map_empty(isl_space_copy(dim));
1604         mm.may = isl_map_empty(dim);
1605
1606         isl_flow_foreach(flow, collect_must_may, &mm);
1607
1608         str = "{ [0,i,0] -> [2,i,0] : (0 <= i <= 4) or (6 <= i <= 10); "
1609               "  [1,10,0] -> [2,5,0] }";
1610         assert(map_is_equal(mm.must, str));
1611         str = "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1612         assert(map_is_equal(mm.may, str));
1613
1614         isl_map_free(mm.must);
1615         isl_map_free(mm.may);
1616         isl_flow_free(flow);
1617
1618
1619         str = "{ [2,i,0] -> [i] : 0 <= i <= 10 }";
1620         map = isl_map_read_from_str(ctx, str);
1621         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1622
1623         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1624         map = isl_map_read_from_str(ctx, str);
1625         ai = isl_access_info_add_source(ai, map, 1, &depth);
1626
1627         str = "{ [1,i,0] -> [5] : 0 <= i <= 10 }";
1628         map = isl_map_read_from_str(ctx, str);
1629         ai = isl_access_info_add_source(ai, map, 0, &depth);
1630
1631         flow = isl_access_info_compute_flow(ai);
1632         dim = isl_space_alloc(ctx, 0, 3, 3);
1633         mm.must = isl_map_empty(isl_space_copy(dim));
1634         mm.may = isl_map_empty(dim);
1635
1636         isl_flow_foreach(flow, collect_must_may, &mm);
1637
1638         str = "{ [0,i,0] -> [2,i,0] : (0 <= i <= 4) or (6 <= i <= 10) }";
1639         assert(map_is_equal(mm.must, str));
1640         str = "{ [0,5,0] -> [2,5,0]; [1,i,0] -> [2,5,0] : 0 <= i <= 10 }";
1641         assert(map_is_equal(mm.may, str));
1642
1643         isl_map_free(mm.must);
1644         isl_map_free(mm.may);
1645         isl_flow_free(flow);
1646
1647
1648         str = "{ [2,i,0] -> [i] : 0 <= i <= 10 }";
1649         map = isl_map_read_from_str(ctx, str);
1650         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1651
1652         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1653         map = isl_map_read_from_str(ctx, str);
1654         ai = isl_access_info_add_source(ai, map, 0, &depth);
1655
1656         str = "{ [1,i,0] -> [5] : 0 <= i <= 10 }";
1657         map = isl_map_read_from_str(ctx, str);
1658         ai = isl_access_info_add_source(ai, map, 0, &depth);
1659
1660         flow = isl_access_info_compute_flow(ai);
1661         dim = isl_space_alloc(ctx, 0, 3, 3);
1662         mm.must = isl_map_empty(isl_space_copy(dim));
1663         mm.may = isl_map_empty(dim);
1664
1665         isl_flow_foreach(flow, collect_must_may, &mm);
1666
1667         str = "{ [0,i,0] -> [2,i,0] : 0 <= i <= 10; "
1668               "  [1,i,0] -> [2,5,0] : 0 <= i <= 10 }";
1669         assert(map_is_equal(mm.may, str));
1670         str = "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1671         assert(map_is_equal(mm.must, str));
1672
1673         isl_map_free(mm.must);
1674         isl_map_free(mm.may);
1675         isl_flow_free(flow);
1676
1677
1678         str = "{ [0,i,2] -> [i] : 0 <= i <= 10 }";
1679         map = isl_map_read_from_str(ctx, str);
1680         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1681
1682         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1683         map = isl_map_read_from_str(ctx, str);
1684         ai = isl_access_info_add_source(ai, map, 0, &depth);
1685
1686         str = "{ [0,i,1] -> [5] : 0 <= i <= 10 }";
1687         map = isl_map_read_from_str(ctx, str);
1688         ai = isl_access_info_add_source(ai, map, 0, &depth);
1689
1690         flow = isl_access_info_compute_flow(ai);
1691         dim = isl_space_alloc(ctx, 0, 3, 3);
1692         mm.must = isl_map_empty(isl_space_copy(dim));
1693         mm.may = isl_map_empty(dim);
1694
1695         isl_flow_foreach(flow, collect_must_may, &mm);
1696
1697         str = "{ [0,i,0] -> [0,i,2] : 0 <= i <= 10; "
1698               "  [0,i,1] -> [0,5,2] : 0 <= i <= 5 }";
1699         assert(map_is_equal(mm.may, str));
1700         str = "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1701         assert(map_is_equal(mm.must, str));
1702
1703         isl_map_free(mm.must);
1704         isl_map_free(mm.may);
1705         isl_flow_free(flow);
1706
1707
1708         str = "{ [0,i,1] -> [i] : 0 <= i <= 10 }";
1709         map = isl_map_read_from_str(ctx, str);
1710         ai = isl_access_info_alloc(map, &depth, &common_space, 2);
1711
1712         str = "{ [0,i,0] -> [i] : 0 <= i <= 10 }";
1713         map = isl_map_read_from_str(ctx, str);
1714         ai = isl_access_info_add_source(ai, map, 0, &depth);
1715
1716         str = "{ [0,i,2] -> [5] : 0 <= i <= 10 }";
1717         map = isl_map_read_from_str(ctx, str);
1718         ai = isl_access_info_add_source(ai, map, 0, &depth);
1719
1720         flow = isl_access_info_compute_flow(ai);
1721         dim = isl_space_alloc(ctx, 0, 3, 3);
1722         mm.must = isl_map_empty(isl_space_copy(dim));
1723         mm.may = isl_map_empty(dim);
1724
1725         isl_flow_foreach(flow, collect_must_may, &mm);
1726
1727         str = "{ [0,i,0] -> [0,i,1] : 0 <= i <= 10; "
1728               "  [0,i,2] -> [0,5,1] : 0 <= i <= 4 }";
1729         assert(map_is_equal(mm.may, str));
1730         str = "{ [i,j,k] -> [l,m,n] : 1 = 0 }";
1731         assert(map_is_equal(mm.must, str));
1732
1733         isl_map_free(mm.must);
1734         isl_map_free(mm.may);
1735         isl_flow_free(flow);
1736
1737
1738         depth = 5;
1739
1740         str = "{ [1,i,0,0,0] -> [i,j] : 0 <= i <= 10 and 0 <= j <= 10 }";
1741         map = isl_map_read_from_str(ctx, str);
1742         ai = isl_access_info_alloc(map, &depth, &common_space, 1);
1743
1744         str = "{ [0,i,0,j,0] -> [i,j] : 0 <= i <= 10 and 0 <= j <= 10 }";
1745         map = isl_map_read_from_str(ctx, str);
1746         ai = isl_access_info_add_source(ai, map, 1, &depth);
1747
1748         flow = isl_access_info_compute_flow(ai);
1749         dim = isl_space_alloc(ctx, 0, 5, 5);
1750         mm.must = isl_map_empty(isl_space_copy(dim));
1751         mm.may = isl_map_empty(dim);
1752
1753         isl_flow_foreach(flow, collect_must_may, &mm);
1754
1755         str = "{ [0,i,0,j,0] -> [1,i,0,0,0] : 0 <= i,j <= 10 }";
1756         assert(map_is_equal(mm.must, str));
1757         str = "{ [0,0,0,0,0] -> [0,0,0,0,0] : 1 = 0 }";
1758         assert(map_is_equal(mm.may, str));
1759
1760         isl_map_free(mm.must);
1761         isl_map_free(mm.may);
1762         isl_flow_free(flow);
1763 }
1764
1765 int test_sv(isl_ctx *ctx)
1766 {
1767         const char *str;
1768         isl_map *map;
1769         isl_union_map *umap;
1770         int sv;
1771
1772         str = "[N] -> { [i] -> [f] : 0 <= i <= N and 0 <= i - 10 f <= 9 }";
1773         map = isl_map_read_from_str(ctx, str);
1774         sv = isl_map_is_single_valued(map);
1775         isl_map_free(map);
1776         if (sv < 0)
1777                 return -1;
1778         if (!sv)
1779                 isl_die(ctx, isl_error_internal,
1780                         "map not detected as single valued", return -1);
1781
1782         str = "[N] -> { [i] -> [f] : 0 <= i <= N and 0 <= i - 10 f <= 10 }";
1783         map = isl_map_read_from_str(ctx, str);
1784         sv = isl_map_is_single_valued(map);
1785         isl_map_free(map);
1786         if (sv < 0)
1787                 return -1;
1788         if (sv)
1789                 isl_die(ctx, isl_error_internal,
1790                         "map detected as single valued", return -1);
1791
1792         str = "{ S1[i] -> [i] : 0 <= i <= 9; S2[i] -> [i] : 0 <= i <= 9 }";
1793         umap = isl_union_map_read_from_str(ctx, str);
1794         sv = isl_union_map_is_single_valued(umap);
1795         isl_union_map_free(umap);
1796         if (sv < 0)
1797                 return -1;
1798         if (!sv)
1799                 isl_die(ctx, isl_error_internal,
1800                         "map not detected as single valued", return -1);
1801
1802         str = "{ [i] -> S1[i] : 0 <= i <= 9; [i] -> S2[i] : 0 <= i <= 9 }";
1803         umap = isl_union_map_read_from_str(ctx, str);
1804         sv = isl_union_map_is_single_valued(umap);
1805         isl_union_map_free(umap);
1806         if (sv < 0)
1807                 return -1;
1808         if (sv)
1809                 isl_die(ctx, isl_error_internal,
1810                         "map detected as single valued", return -1);
1811
1812         return 0;
1813 }
1814
1815 void test_bijective_case(struct isl_ctx *ctx, const char *str, int bijective)
1816 {
1817         isl_map *map;
1818
1819         map = isl_map_read_from_str(ctx, str);
1820         if (bijective)
1821                 assert(isl_map_is_bijective(map));
1822         else
1823                 assert(!isl_map_is_bijective(map));
1824         isl_map_free(map);
1825 }
1826
1827 void test_bijective(struct isl_ctx *ctx)
1828 {
1829         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i]}", 0);
1830         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i] : j=i}", 1);
1831         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i] : j=0}", 1);
1832         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i] : j=N}", 1);
1833         test_bijective_case(ctx, "[N,M]->{[i,j] -> [j,i]}", 1);
1834         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i+j]}", 0);
1835         test_bijective_case(ctx, "[N,M]->{[i,j] -> []}", 0);
1836         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i,j,N]}", 1);
1837         test_bijective_case(ctx, "[N,M]->{[i,j] -> [2i]}", 0);
1838         test_bijective_case(ctx, "[N,M]->{[i,j] -> [i,i]}", 0);
1839         test_bijective_case(ctx, "[N,M]->{[i,j] -> [2i,i]}", 0);
1840         test_bijective_case(ctx, "[N,M]->{[i,j] -> [2i,j]}", 1);
1841         test_bijective_case(ctx, "[N,M]->{[i,j] -> [x,y] : 2x=i & y =j}", 1);
1842 }
1843
1844 void test_pwqp(struct isl_ctx *ctx)
1845 {
1846         const char *str;
1847         isl_set *set;
1848         isl_pw_qpolynomial *pwqp1, *pwqp2;
1849
1850         str = "{ [i,j,k] -> 1 + 9 * [i/5] + 7 * [j/11] + 4 * [k/13] }";
1851         pwqp1 = isl_pw_qpolynomial_read_from_str(ctx, str);
1852
1853         pwqp1 = isl_pw_qpolynomial_move_dims(pwqp1, isl_dim_param, 0,
1854                                                 isl_dim_in, 1, 1);
1855
1856         str = "[j] -> { [i,k] -> 1 + 9 * [i/5] + 7 * [j/11] + 4 * [k/13] }";
1857         pwqp2 = isl_pw_qpolynomial_read_from_str(ctx, str);
1858
1859         pwqp1 = isl_pw_qpolynomial_sub(pwqp1, pwqp2);
1860
1861         assert(isl_pw_qpolynomial_is_zero(pwqp1));
1862
1863         isl_pw_qpolynomial_free(pwqp1);
1864
1865         str = "{ [i] -> i }";
1866         pwqp1 = isl_pw_qpolynomial_read_from_str(ctx, str);
1867         str = "{ [k] : exists a : k = 2a }";
1868         set = isl_set_read_from_str(ctx, str);
1869         pwqp1 = isl_pw_qpolynomial_gist(pwqp1, set);
1870         str = "{ [i] -> i }";
1871         pwqp2 = isl_pw_qpolynomial_read_from_str(ctx, str);
1872
1873         pwqp1 = isl_pw_qpolynomial_sub(pwqp1, pwqp2);
1874
1875         assert(isl_pw_qpolynomial_is_zero(pwqp1));
1876
1877         isl_pw_qpolynomial_free(pwqp1);
1878
1879         str = "{ [i] -> i + [ (i + [i/3])/2 ] }";
1880         pwqp1 = isl_pw_qpolynomial_read_from_str(ctx, str);
1881         str = "{ [10] }";
1882         set = isl_set_read_from_str(ctx, str);
1883         pwqp1 = isl_pw_qpolynomial_gist(pwqp1, set);
1884         str = "{ [i] -> 16 }";
1885         pwqp2 = isl_pw_qpolynomial_read_from_str(ctx, str);
1886
1887         pwqp1 = isl_pw_qpolynomial_sub(pwqp1, pwqp2);
1888
1889         assert(isl_pw_qpolynomial_is_zero(pwqp1));
1890
1891         isl_pw_qpolynomial_free(pwqp1);
1892
1893         str = "{ [i] -> ([(i)/2]) }";
1894         pwqp1 = isl_pw_qpolynomial_read_from_str(ctx, str);
1895         str = "{ [k] : exists a : k = 2a+1 }";
1896         set = isl_set_read_from_str(ctx, str);
1897         pwqp1 = isl_pw_qpolynomial_gist(pwqp1, set);
1898         str = "{ [i] -> -1/2 + 1/2 * i }";
1899         pwqp2 = isl_pw_qpolynomial_read_from_str(ctx, str);
1900
1901         pwqp1 = isl_pw_qpolynomial_sub(pwqp1, pwqp2);
1902
1903         assert(isl_pw_qpolynomial_is_zero(pwqp1));
1904
1905         isl_pw_qpolynomial_free(pwqp1);
1906
1907         str = "{ [i] -> ([([i/2] + [i/2])/5]) }";
1908         pwqp1 = isl_pw_qpolynomial_read_from_str(ctx, str);
1909         str = "{ [i] -> ([(2 * [i/2])/5]) }";
1910         pwqp2 = isl_pw_qpolynomial_read_from_str(ctx, str);
1911
1912         pwqp1 = isl_pw_qpolynomial_sub(pwqp1, pwqp2);
1913
1914         assert(isl_pw_qpolynomial_is_zero(pwqp1));
1915
1916         isl_pw_qpolynomial_free(pwqp1);
1917
1918         str = "{ [x] -> ([x/2] + [(x+1)/2]) }";
1919         pwqp1 = isl_pw_qpolynomial_read_from_str(ctx, str);
1920         str = "{ [x] -> x }";
1921         pwqp2 = isl_pw_qpolynomial_read_from_str(ctx, str);
1922
1923         pwqp1 = isl_pw_qpolynomial_sub(pwqp1, pwqp2);
1924
1925         assert(isl_pw_qpolynomial_is_zero(pwqp1));
1926
1927         isl_pw_qpolynomial_free(pwqp1);
1928
1929         str = "{ [i] -> ([i/2]) : i >= 0; [i] -> ([i/3]) : i < 0 }";
1930         pwqp1 = isl_pw_qpolynomial_read_from_str(ctx, str);
1931         pwqp2 = isl_pw_qpolynomial_read_from_str(ctx, str);
1932         pwqp1 = isl_pw_qpolynomial_coalesce(pwqp1);
1933         pwqp1 = isl_pw_qpolynomial_sub(pwqp1, pwqp2);
1934         assert(isl_pw_qpolynomial_is_zero(pwqp1));
1935         isl_pw_qpolynomial_free(pwqp1);
1936 }
1937
1938 void test_split_periods(isl_ctx *ctx)
1939 {
1940         const char *str;
1941         isl_pw_qpolynomial *pwqp;
1942
1943         str = "{ [U,V] -> 1/3 * U + 2/3 * V - [(U + 2V)/3] + [U/2] : "
1944                 "U + 2V + 3 >= 0 and - U -2V  >= 0 and - U + 10 >= 0 and "
1945                 "U  >= 0; [U,V] -> U^2 : U >= 100 }";
1946         pwqp = isl_pw_qpolynomial_read_from_str(ctx, str);
1947
1948         pwqp = isl_pw_qpolynomial_split_periods(pwqp, 2);
1949         assert(pwqp);
1950
1951         isl_pw_qpolynomial_free(pwqp);
1952 }
1953
1954 void test_union(isl_ctx *ctx)
1955 {
1956         const char *str;
1957         isl_union_set *uset1, *uset2;
1958         isl_union_map *umap1, *umap2;
1959
1960         str = "{ [i] : 0 <= i <= 1 }";
1961         uset1 = isl_union_set_read_from_str(ctx, str);
1962         str = "{ [1] -> [0] }";
1963         umap1 = isl_union_map_read_from_str(ctx, str);
1964
1965         umap2 = isl_union_set_lex_gt_union_set(isl_union_set_copy(uset1), uset1);
1966         assert(isl_union_map_is_equal(umap1, umap2));
1967
1968         isl_union_map_free(umap1);
1969         isl_union_map_free(umap2);
1970
1971         str = "{ A[i] -> B[i]; B[i] -> C[i]; A[0] -> C[1] }";
1972         umap1 = isl_union_map_read_from_str(ctx, str);
1973         str = "{ A[i]; B[i] }";
1974         uset1 = isl_union_set_read_from_str(ctx, str);
1975
1976         uset2 = isl_union_map_domain(umap1);
1977
1978         assert(isl_union_set_is_equal(uset1, uset2));
1979
1980         isl_union_set_free(uset1);
1981         isl_union_set_free(uset2);
1982 }
1983
1984 void test_bound(isl_ctx *ctx)
1985 {
1986         const char *str;
1987         isl_pw_qpolynomial *pwqp;
1988         isl_pw_qpolynomial_fold *pwf;
1989
1990         str = "{ [[a, b, c, d] -> [e]] -> 0 }";
1991         pwqp = isl_pw_qpolynomial_read_from_str(ctx, str);
1992         pwf = isl_pw_qpolynomial_bound(pwqp, isl_fold_max, NULL);
1993         assert(isl_pw_qpolynomial_fold_dim(pwf, isl_dim_in) == 4);
1994         isl_pw_qpolynomial_fold_free(pwf);
1995
1996         str = "{ [[x]->[x]] -> 1 : exists a : x = 2 a }";
1997         pwqp = isl_pw_qpolynomial_read_from_str(ctx, str);
1998         pwf = isl_pw_qpolynomial_bound(pwqp, isl_fold_max, NULL);
1999         assert(isl_pw_qpolynomial_fold_dim(pwf, isl_dim_in) == 1);
2000         isl_pw_qpolynomial_fold_free(pwf);
2001 }
2002
2003 void test_lift(isl_ctx *ctx)
2004 {
2005         const char *str;
2006         isl_basic_map *bmap;
2007         isl_basic_set *bset;
2008
2009         str = "{ [i0] : exists e0 : i0 = 4e0 }";
2010         bset = isl_basic_set_read_from_str(ctx, str);
2011         bset = isl_basic_set_lift(bset);
2012         bmap = isl_basic_map_from_range(bset);
2013         bset = isl_basic_map_domain(bmap);
2014         isl_basic_set_free(bset);
2015 }
2016
2017 struct {
2018         const char *set1;
2019         const char *set2;
2020         int subset;
2021 } subset_tests[] = {
2022         { "{ [112, 0] }",
2023           "{ [i0, i1] : exists (e0 = [(i0 - i1)/16], e1: "
2024                 "16e0 <= i0 - i1 and 16e0 >= -15 + i0 - i1 and "
2025                 "16e1 <= i1 and 16e0 >= -i1 and 16e1 >= -i0 + i1) }", 1 },
2026         { "{ [65] }",
2027           "{ [i] : exists (e0 = [(255i)/256], e1 = [(127i + 65e0)/191], "
2028                 "e2 = [(3i + 61e1)/65], e3 = [(52i + 12e2)/61], "
2029                 "e4 = [(2i + e3)/3], e5 = [(4i + e3)/4], e6 = [(8i + e3)/12]: "
2030                     "3e4 = 2i + e3 and 4e5 = 4i + e3 and 12e6 = 8i + e3 and "
2031                     "i <= 255 and 64e3 >= -45 + 67i and i >= 0 and "
2032                     "256e0 <= 255i and 256e0 >= -255 + 255i and "
2033                     "191e1 <= 127i + 65e0 and 191e1 >= -190 + 127i + 65e0 and "
2034                     "65e2 <= 3i + 61e1 and 65e2 >= -64 + 3i + 61e1 and "
2035                     "61e3 <= 52i + 12e2 and 61e3 >= -60 + 52i + 12e2) }", 1 },
2036         { "{ [i] : 0 <= i <= 10 }", "{ rat: [i] : 0 <= i <= 10 }", 1 },
2037         { "{ rat: [i] : 0 <= i <= 10 }", "{ [i] : 0 <= i <= 10 }", 0 },
2038         { "{ rat: [0] }", "{ [i] : 0 <= i <= 10 }", 1 },
2039         { "{ rat: [(1)/2] }", "{ [i] : 0 <= i <= 10 }", 0 },
2040 };
2041
2042 static int test_subset(isl_ctx *ctx)
2043 {
2044         int i;
2045         isl_set *set1, *set2;
2046         int subset;
2047
2048         for (i = 0; i < ARRAY_SIZE(subset_tests); ++i) {
2049                 set1 = isl_set_read_from_str(ctx, subset_tests[i].set1);
2050                 set2 = isl_set_read_from_str(ctx, subset_tests[i].set2);
2051                 subset = isl_set_is_subset(set1, set2);
2052                 isl_set_free(set1);
2053                 isl_set_free(set2);
2054                 if (subset < 0)
2055                         return -1;
2056                 if (subset != subset_tests[i].subset)
2057                         isl_die(ctx, isl_error_unknown,
2058                                 "incorrect subset result", return -1);
2059         }
2060
2061         return 0;
2062 }
2063
2064 struct {
2065         const char *minuend;
2066         const char *subtrahend;
2067         const char *difference;
2068 } subtract_domain_tests[] = {
2069         { "{ A[i] -> B[i] }", "{ A[i] }", "{ }" },
2070         { "{ A[i] -> B[i] }", "{ B[i] }", "{ A[i] -> B[i] }" },
2071         { "{ A[i] -> B[i] }", "{ A[i] : i > 0 }", "{ A[i] -> B[i] : i <= 0 }" },
2072 };
2073
2074 static int test_subtract(isl_ctx *ctx)
2075 {
2076         int i;
2077         isl_union_map *umap1, *umap2;
2078         isl_union_set *uset;
2079         int equal;
2080
2081         for (i = 0; i < ARRAY_SIZE(subtract_domain_tests); ++i) {
2082                 umap1 = isl_union_map_read_from_str(ctx,
2083                                 subtract_domain_tests[i].minuend);
2084                 uset = isl_union_set_read_from_str(ctx,
2085                                 subtract_domain_tests[i].subtrahend);
2086                 umap2 = isl_union_map_read_from_str(ctx,
2087                                 subtract_domain_tests[i].difference);
2088                 umap1 = isl_union_map_subtract_domain(umap1, uset);
2089                 equal = isl_union_map_is_equal(umap1, umap2);
2090                 isl_union_map_free(umap1);
2091                 isl_union_map_free(umap2);
2092                 if (equal < 0)
2093                         return -1;
2094                 if (!equal)
2095                         isl_die(ctx, isl_error_unknown,
2096                                 "incorrect subtract domain result", return -1);
2097         }
2098
2099         return 0;
2100 }
2101
2102 int test_factorize(isl_ctx *ctx)
2103 {
2104         const char *str;
2105         isl_basic_set *bset;
2106         isl_factorizer *f;
2107
2108         str = "{ [i0, i1, i2, i3, i4, i5, i6, i7] : 3i5 <= 2 - 2i0 and "
2109             "i0 >= -2 and i6 >= 1 + i3 and i7 >= 0 and 3i5 >= -2i0 and "
2110             "2i4 <= i2 and i6 >= 1 + 2i0 + 3i1 and i4 <= -1 and "
2111             "i6 >= 1 + 2i0 + 3i5 and i6 <= 2 + 2i0 + 3i5 and "
2112             "3i5 <= 2 - 2i0 - i2 + 3i4 and i6 <= 2 + 2i0 + 3i1 and "
2113             "i0 <= -1 and i7 <= i2 + i3 - 3i4 - i6 and "
2114             "3i5 >= -2i0 - i2 + 3i4 }";
2115         bset = isl_basic_set_read_from_str(ctx, str);
2116         f = isl_basic_set_factorizer(bset);
2117         isl_basic_set_free(bset);
2118         isl_factorizer_free(f);
2119         if (!f)
2120                 isl_die(ctx, isl_error_unknown,
2121                         "failed to construct factorizer", return -1);
2122
2123         str = "{ [i0, i1, i2, i3, i4, i5, i6, i7, i8, i9, i10, i11, i12] : "
2124             "i12 <= 2 + i0 - i11 and 2i8 >= -i4 and i11 >= i1 and "
2125             "3i5 <= -i2 and 2i11 >= -i4 - 2i7 and i11 <= 3 + i0 + 3i9 and "
2126             "i11 <= -i4 - 2i7 and i12 >= -i10 and i2 >= -2 and "
2127             "i11 >= i1 + 3i10 and i11 >= 1 + i0 + 3i9 and "
2128             "i11 <= 1 - i4 - 2i8 and 6i6 <= 6 - i2 and 3i6 >= 1 - i2 and "
2129             "i11 <= 2 + i1 and i12 <= i4 + i11 and i12 >= i0 - i11 and "
2130             "3i5 >= -2 - i2 and i12 >= -1 + i4 + i11 and 3i3 <= 3 - i2 and "
2131             "9i6 <= 11 - i2 + 6i5 and 3i3 >= 1 - i2 and "
2132             "9i6 <= 5 - i2 + 6i3 and i12 <= -1 and i2 <= 0 }";
2133         bset = isl_basic_set_read_from_str(ctx, str);
2134         f = isl_basic_set_factorizer(bset);
2135         isl_basic_set_free(bset);
2136         isl_factorizer_free(f);
2137         if (!f)
2138                 isl_die(ctx, isl_error_unknown,
2139                         "failed to construct factorizer", return -1);
2140
2141         return 0;
2142 }
2143
2144 static int check_injective(__isl_take isl_map *map, void *user)
2145 {
2146         int *injective = user;
2147
2148         *injective = isl_map_is_injective(map);
2149         isl_map_free(map);
2150
2151         if (*injective < 0 || !*injective)
2152                 return -1;
2153
2154         return 0;
2155 }
2156
2157 int test_one_schedule(isl_ctx *ctx, const char *d, const char *w,
2158         const char *r, const char *s, int tilable, int parallel)
2159 {
2160         int i;
2161         isl_union_set *D;
2162         isl_union_map *W, *R, *S;
2163         isl_union_map *empty;
2164         isl_union_map *dep_raw, *dep_war, *dep_waw, *dep;
2165         isl_union_map *validity, *proximity;
2166         isl_union_map *schedule;
2167         isl_union_map *test;
2168         isl_union_set *delta;
2169         isl_union_set *domain;
2170         isl_set *delta_set;
2171         isl_set *slice;
2172         isl_set *origin;
2173         isl_schedule *sched;
2174         int is_nonneg, is_parallel, is_tilable, is_injection, is_complete;
2175
2176         D = isl_union_set_read_from_str(ctx, d);
2177         W = isl_union_map_read_from_str(ctx, w);
2178         R = isl_union_map_read_from_str(ctx, r);
2179         S = isl_union_map_read_from_str(ctx, s);
2180
2181         W = isl_union_map_intersect_domain(W, isl_union_set_copy(D));
2182         R = isl_union_map_intersect_domain(R, isl_union_set_copy(D));
2183
2184         empty = isl_union_map_empty(isl_union_map_get_space(S));
2185         isl_union_map_compute_flow(isl_union_map_copy(R),
2186                                    isl_union_map_copy(W), empty,
2187                                    isl_union_map_copy(S),
2188                                    &dep_raw, NULL, NULL, NULL);
2189         isl_union_map_compute_flow(isl_union_map_copy(W),
2190                                    isl_union_map_copy(W),
2191                                    isl_union_map_copy(R),
2192                                    isl_union_map_copy(S),
2193                                    &dep_waw, &dep_war, NULL, NULL);
2194
2195         dep = isl_union_map_union(dep_waw, dep_war);
2196         dep = isl_union_map_union(dep, dep_raw);
2197         validity = isl_union_map_copy(dep);
2198         proximity = isl_union_map_copy(dep);
2199
2200         sched = isl_union_set_compute_schedule(isl_union_set_copy(D),
2201                                                validity, proximity);
2202         schedule = isl_schedule_get_map(sched);
2203         isl_schedule_free(sched);
2204         isl_union_map_free(W);
2205         isl_union_map_free(R);
2206         isl_union_map_free(S);
2207
2208         is_injection = 1;
2209         isl_union_map_foreach_map(schedule, &check_injective, &is_injection);
2210
2211         domain = isl_union_map_domain(isl_union_map_copy(schedule));
2212         is_complete = isl_union_set_is_subset(D, domain);
2213         isl_union_set_free(D);
2214         isl_union_set_free(domain);
2215
2216         test = isl_union_map_reverse(isl_union_map_copy(schedule));
2217         test = isl_union_map_apply_range(test, dep);
2218         test = isl_union_map_apply_range(test, schedule);
2219
2220         delta = isl_union_map_deltas(test);
2221         if (isl_union_set_n_set(delta) == 0) {
2222                 is_tilable = 1;
2223                 is_parallel = 1;
2224                 is_nonneg = 1;
2225                 isl_union_set_free(delta);
2226         } else {
2227                 delta_set = isl_set_from_union_set(delta);
2228
2229                 slice = isl_set_universe(isl_set_get_space(delta_set));
2230                 for (i = 0; i < tilable; ++i)
2231                         slice = isl_set_lower_bound_si(slice, isl_dim_set, i, 0);
2232                 is_tilable = isl_set_is_subset(delta_set, slice);
2233                 isl_set_free(slice);
2234
2235                 slice = isl_set_universe(isl_set_get_space(delta_set));
2236                 for (i = 0; i < parallel; ++i)
2237                         slice = isl_set_fix_si(slice, isl_dim_set, i, 0);
2238                 is_parallel = isl_set_is_subset(delta_set, slice);
2239                 isl_set_free(slice);
2240
2241                 origin = isl_set_universe(isl_set_get_space(delta_set));
2242                 for (i = 0; i < isl_set_dim(origin, isl_dim_set); ++i)
2243                         origin = isl_set_fix_si(origin, isl_dim_set, i, 0);
2244
2245                 delta_set = isl_set_union(delta_set, isl_set_copy(origin));
2246                 delta_set = isl_set_lexmin(delta_set);
2247
2248                 is_nonneg = isl_set_is_equal(delta_set, origin);
2249
2250                 isl_set_free(origin);
2251                 isl_set_free(delta_set);
2252         }
2253
2254         if (is_nonneg < 0 || is_parallel < 0 || is_tilable < 0 ||
2255             is_injection < 0 || is_complete < 0)
2256                 return -1;
2257         if (!is_complete)
2258                 isl_die(ctx, isl_error_unknown,
2259                         "generated schedule incomplete", return -1);
2260         if (!is_injection)
2261                 isl_die(ctx, isl_error_unknown,
2262                         "generated schedule not injective on each statement",
2263                         return -1);
2264         if (!is_nonneg)
2265                 isl_die(ctx, isl_error_unknown,
2266                         "negative dependences in generated schedule",
2267                         return -1);
2268         if (!is_tilable)
2269                 isl_die(ctx, isl_error_unknown,
2270                         "generated schedule not as tilable as expected",
2271                         return -1);
2272         if (!is_parallel)
2273                 isl_die(ctx, isl_error_unknown,
2274                         "generated schedule not as parallel as expected",
2275                         return -1);
2276
2277         return 0;
2278 }
2279
2280 int test_special_schedule(isl_ctx *ctx, const char *domain,
2281         const char *validity, const char *proximity, const char *expected_sched)
2282 {
2283         isl_union_set *dom;
2284         isl_union_map *dep;
2285         isl_union_map *prox;
2286         isl_union_map *sched1, *sched2;
2287         isl_schedule *schedule;
2288         int equal;
2289
2290         dom = isl_union_set_read_from_str(ctx, domain);
2291         dep = isl_union_map_read_from_str(ctx, validity);
2292         prox = isl_union_map_read_from_str(ctx, proximity);
2293         schedule = isl_union_set_compute_schedule(dom, dep, prox);
2294         sched1 = isl_schedule_get_map(schedule);
2295         isl_schedule_free(schedule);
2296
2297         sched2 = isl_union_map_read_from_str(ctx, expected_sched);
2298
2299         equal = isl_union_map_is_equal(sched1, sched2);
2300         isl_union_map_free(sched1);
2301         isl_union_map_free(sched2);
2302
2303         if (equal < 0)
2304                 return -1;
2305         if (!equal)
2306                 isl_die(ctx, isl_error_unknown, "unexpected schedule",
2307                         return -1);
2308
2309         return 0;
2310 }
2311
2312 int test_schedule(isl_ctx *ctx)
2313 {
2314         const char *D, *W, *R, *V, *P, *S;
2315
2316         /* Jacobi */
2317         D = "[T,N] -> { S1[t,i] : 1 <= t <= T and 2 <= i <= N - 1 }";
2318         W = "{ S1[t,i] -> a[t,i] }";
2319         R = "{ S1[t,i] -> a[t-1,i]; S1[t,i] -> a[t-1,i-1]; "
2320                 "S1[t,i] -> a[t-1,i+1] }";
2321         S = "{ S1[t,i] -> [t,i] }";
2322         if (test_one_schedule(ctx, D, W, R, S, 2, 0) < 0)
2323                 return -1;
2324
2325         /* Fig. 5 of CC2008 */
2326         D = "[N] -> { S_0[i, j] : i >= 0 and i <= -1 + N and j >= 2 and "
2327                                 "j <= -1 + N }";
2328         W = "[N] -> { S_0[i, j] -> a[i, j] : i >= 0 and i <= -1 + N and "
2329                                 "j >= 2 and j <= -1 + N }";
2330         R = "[N] -> { S_0[i, j] -> a[j, i] : i >= 0 and i <= -1 + N and "
2331                                 "j >= 2 and j <= -1 + N; "
2332                     "S_0[i, j] -> a[i, -1 + j] : i >= 0 and i <= -1 + N and "
2333                                 "j >= 2 and j <= -1 + N }";
2334         S = "[N] -> { S_0[i, j] -> [0, i, 0, j, 0] }";
2335         if (test_one_schedule(ctx, D, W, R, S, 2, 0) < 0)
2336                 return -1;
2337
2338         D = "{ S1[i] : 0 <= i <= 10; S2[i] : 0 <= i <= 9 }";
2339         W = "{ S1[i] -> a[i] }";
2340         R = "{ S2[i] -> a[i+1] }";
2341         S = "{ S1[i] -> [0,i]; S2[i] -> [1,i] }";
2342         if (test_one_schedule(ctx, D, W, R, S, 1, 1) < 0)
2343                 return -1;
2344
2345         D = "{ S1[i] : 0 <= i < 10; S2[i] : 0 <= i < 10 }";
2346         W = "{ S1[i] -> a[i] }";
2347         R = "{ S2[i] -> a[9-i] }";
2348         S = "{ S1[i] -> [0,i]; S2[i] -> [1,i] }";
2349         if (test_one_schedule(ctx, D, W, R, S, 1, 1) < 0)
2350                 return -1;
2351
2352         D = "[N] -> { S1[i] : 0 <= i < N; S2[i] : 0 <= i < N }";
2353         W = "{ S1[i] -> a[i] }";
2354         R = "[N] -> { S2[i] -> a[N-1-i] }";
2355         S = "{ S1[i] -> [0,i]; S2[i] -> [1,i] }";
2356         if (test_one_schedule(ctx, D, W, R, S, 1, 1) < 0)
2357                 return -1;
2358
2359         D = "{ S1[i] : 0 < i < 10; S2[i] : 0 <= i < 10 }";
2360         W = "{ S1[i] -> a[i]; S2[i] -> b[i] }";
2361         R = "{ S2[i] -> a[i]; S1[i] -> b[i-1] }";
2362         S = "{ S1[i] -> [i,0]; S2[i] -> [i,1] }";
2363         if (test_one_schedule(ctx, D, W, R, S, 0, 0) < 0)
2364                 return -1;
2365
2366         D = "[N] -> { S1[i] : 1 <= i <= N; S2[i,j] : 1 <= i,j <= N }";
2367         W = "{ S1[i] -> a[0,i]; S2[i,j] -> a[i,j] }";
2368         R = "{ S2[i,j] -> a[i-1,j] }";
2369         S = "{ S1[i] -> [0,i,0]; S2[i,j] -> [1,i,j] }";
2370         if (test_one_schedule(ctx, D, W, R, S, 2, 1) < 0)
2371                 return -1;
2372
2373         D = "[N] -> { S1[i] : 1 <= i <= N; S2[i,j] : 1 <= i,j <= N }";
2374         W = "{ S1[i] -> a[i,0]; S2[i,j] -> a[i,j] }";
2375         R = "{ S2[i,j] -> a[i,j-1] }";
2376         S = "{ S1[i] -> [0,i,0]; S2[i,j] -> [1,i,j] }";
2377         if (test_one_schedule(ctx, D, W, R, S, 2, 1) < 0)
2378                 return -1;
2379
2380         D = "[N] -> { S_0[]; S_1[i] : i >= 0 and i <= -1 + N; S_2[] }";
2381         W = "[N] -> { S_0[] -> a[0]; S_2[] -> b[0]; "
2382                     "S_1[i] -> a[1 + i] : i >= 0 and i <= -1 + N }";
2383         R = "[N] -> { S_2[] -> a[N]; S_1[i] -> a[i] : i >= 0 and i <= -1 + N }";
2384         S = "[N] -> { S_1[i] -> [1, i, 0]; S_2[] -> [2, 0, 1]; "
2385                     "S_0[] -> [0, 0, 0] }";
2386         if (test_one_schedule(ctx, D, W, R, S, 1, 0) < 0)
2387                 return -1;
2388         ctx->opt->schedule_parametric = 0;
2389         if (test_one_schedule(ctx, D, W, R, S, 0, 0) < 0)
2390                 return -1;
2391         ctx->opt->schedule_parametric = 1;
2392
2393         D = "[N] -> { S1[i] : 1 <= i <= N; S2[i] : 1 <= i <= N; "
2394                     "S3[i,j] : 1 <= i,j <= N; S4[i] : 1 <= i <= N }";
2395         W = "{ S1[i] -> a[i,0]; S2[i] -> a[0,i]; S3[i,j] -> a[i,j] }";
2396         R = "[N] -> { S3[i,j] -> a[i-1,j]; S3[i,j] -> a[i,j-1]; "
2397                     "S4[i] -> a[i,N] }";
2398         S = "{ S1[i] -> [0,i,0]; S2[i] -> [1,i,0]; S3[i,j] -> [2,i,j]; "
2399                 "S4[i] -> [4,i,0] }";
2400         if (test_one_schedule(ctx, D, W, R, S, 2, 0) < 0)
2401                 return -1;
2402
2403         D = "[N] -> { S_0[i, j] : i >= 1 and i <= N and j >= 1 and j <= N }";
2404         W = "[N] -> { S_0[i, j] -> s[0] : i >= 1 and i <= N and j >= 1 and "
2405                                         "j <= N }";
2406         R = "[N] -> { S_0[i, j] -> s[0] : i >= 1 and i <= N and j >= 1 and "
2407                                         "j <= N; "
2408                     "S_0[i, j] -> a[i, j] : i >= 1 and i <= N and j >= 1 and "
2409                                         "j <= N }";
2410         S = "[N] -> { S_0[i, j] -> [0, i, 0, j, 0] }";
2411         if (test_one_schedule(ctx, D, W, R, S, 0, 0) < 0)
2412                 return -1;
2413
2414         D = "[N] -> { S_0[t] : t >= 0 and t <= -1 + N; "
2415                     " S_2[t] : t >= 0 and t <= -1 + N; "
2416                     " S_1[t, i] : t >= 0 and t <= -1 + N and i >= 0 and "
2417                                 "i <= -1 + N }";
2418         W = "[N] -> { S_0[t] -> a[t, 0] : t >= 0 and t <= -1 + N; "
2419                     " S_2[t] -> b[t] : t >= 0 and t <= -1 + N; "
2420                     " S_1[t, i] -> a[t, 1 + i] : t >= 0 and t <= -1 + N and "
2421                                                 "i >= 0 and i <= -1 + N }";
2422         R = "[N] -> { S_1[t, i] -> a[t, i] : t >= 0 and t <= -1 + N and "
2423                                             "i >= 0 and i <= -1 + N; "
2424                     " S_2[t] -> a[t, N] : t >= 0 and t <= -1 + N }";
2425         S = "[N] -> { S_2[t] -> [0, t, 2]; S_1[t, i] -> [0, t, 1, i, 0]; "
2426                     " S_0[t] -> [0, t, 0] }";
2427
2428         if (test_one_schedule(ctx, D, W, R, S, 2, 1) < 0)
2429                 return -1;
2430         ctx->opt->schedule_parametric = 0;
2431         if (test_one_schedule(ctx, D, W, R, S, 0, 0) < 0)
2432                 return -1;
2433         ctx->opt->schedule_parametric = 1;
2434
2435         D = "[N] -> { S1[i,j] : 0 <= i,j < N; S2[i,j] : 0 <= i,j < N }";
2436         S = "{ S1[i,j] -> [0,i,j]; S2[i,j] -> [1,i,j] }";
2437         if (test_one_schedule(ctx, D, "{}", "{}", S, 2, 2) < 0)
2438                 return -1;
2439
2440         D = "[M, N] -> { S_1[i] : i >= 0 and i <= -1 + M; "
2441             "S_0[i, j] : i >= 0 and i <= -1 + M and j >= 0 and j <= -1 + N }";
2442         W = "[M, N] -> { S_0[i, j] -> a[j] : i >= 0 and i <= -1 + M and "
2443                                             "j >= 0 and j <= -1 + N; "
2444                         "S_1[i] -> b[0] : i >= 0 and i <= -1 + M }";
2445         R = "[M, N] -> { S_0[i, j] -> a[0] : i >= 0 and i <= -1 + M and "
2446                                             "j >= 0 and j <= -1 + N; "
2447                         "S_1[i] -> b[0] : i >= 0 and i <= -1 + M }";
2448         S = "[M, N] -> { S_1[i] -> [1, i, 0]; S_0[i, j] -> [0, i, 0, j, 0] }";
2449         if (test_one_schedule(ctx, D, W, R, S, 0, 0) < 0)
2450                 return -1;
2451
2452         D = "{ S_0[i] : i >= 0 }";
2453         W = "{ S_0[i] -> a[i] : i >= 0 }";
2454         R = "{ S_0[i] -> a[0] : i >= 0 }";
2455         S = "{ S_0[i] -> [0, i, 0] }";
2456         if (test_one_schedule(ctx, D, W, R, S, 0, 0) < 0)
2457                 return -1;
2458
2459         D = "{ S_0[i] : i >= 0; S_1[i] : i >= 0 }";
2460         W = "{ S_0[i] -> a[i] : i >= 0; S_1[i] -> b[i] : i >= 0 }";
2461         R = "{ S_0[i] -> b[0] : i >= 0; S_1[i] -> a[i] : i >= 0 }";
2462         S = "{ S_1[i] -> [0, i, 1]; S_0[i] -> [0, i, 0] }";
2463         if (test_one_schedule(ctx, D, W, R, S, 0, 0) < 0)
2464                 return -1;
2465
2466         D = "[n] -> { S_0[j, k] : j <= -1 + n and j >= 0 and "
2467                                 "k <= -1 + n and k >= 0 }";
2468         W = "[n] -> { S_0[j, k] -> B[j] : j <= -1 + n and j >= 0 and "                                                  "k <= -1 + n and k >= 0 }";
2469         R = "[n] -> { S_0[j, k] -> B[j] : j <= -1 + n and j >= 0 and "
2470                                         "k <= -1 + n and k >= 0; "
2471                     "S_0[j, k] -> B[k] : j <= -1 + n and j >= 0 and "
2472                                         "k <= -1 + n and k >= 0; "
2473                     "S_0[j, k] -> A[k] : j <= -1 + n and j >= 0 and "
2474                                         "k <= -1 + n and k >= 0 }";
2475         S = "[n] -> { S_0[j, k] -> [2, j, k] }";
2476         ctx->opt->schedule_outer_zero_distance = 1;
2477         if (test_one_schedule(ctx, D, W, R, S, 0, 0) < 0)
2478                 return -1;
2479         ctx->opt->schedule_outer_zero_distance = 0;
2480
2481         D = "{Stmt_for_body24[i0, i1, i2, i3]:"
2482                 "i0 >= 0 and i0 <= 1 and i1 >= 0 and i1 <= 6 and i2 >= 2 and "
2483                 "i2 <= 6 - i1 and i3 >= 0 and i3 <= -1 + i2;"
2484              "Stmt_for_body24[i0, i1, 1, 0]:"
2485                 "i0 >= 0 and i0 <= 1 and i1 >= 0 and i1 <= 5;"
2486              "Stmt_for_body7[i0, i1, i2]:"
2487                 "i0 >= 0 and i0 <= 1 and i1 >= 0 and i1 <= 7 and i2 >= 0 and "
2488                 "i2 <= 7 }";
2489
2490         V = "{Stmt_for_body24[0, i1, i2, i3] -> "
2491                 "Stmt_for_body24[1, i1, i2, i3]:"
2492                 "i3 >= 0 and i3 <= -1 + i2 and i1 >= 0 and i2 <= 6 - i1 and "
2493                 "i2 >= 1;"
2494              "Stmt_for_body24[0, i1, i2, i3] -> "
2495                 "Stmt_for_body7[1, 1 + i1 + i3, 1 + i1 + i2]:"
2496                 "i3 <= -1 + i2 and i2 <= 6 - i1 and i2 >= 1 and i1 >= 0 and "
2497                 "i3 >= 0;"
2498               "Stmt_for_body24[0, i1, i2, i3] ->"
2499                 "Stmt_for_body7[1, i1, 1 + i1 + i3]:"
2500                 "i3 >= 0 and i2 <= 6 - i1 and i1 >= 0 and i3 <= -1 + i2;"
2501               "Stmt_for_body7[0, i1, i2] -> Stmt_for_body7[1, i1, i2]:"
2502                 "(i2 >= 1 + i1 and i2 <= 6 and i1 >= 0 and i1 <= 4) or "
2503                 "(i2 >= 3 and i2 <= 7 and i1 >= 1 and i2 >= 1 + i1) or "
2504                 "(i2 >= 0 and i2 <= i1 and i2 >= -7 + i1 and i1 <= 7);"
2505               "Stmt_for_body7[0, i1, 1 + i1] -> Stmt_for_body7[1, i1, 1 + i1]:"
2506                 "i1 <= 6 and i1 >= 0;"
2507               "Stmt_for_body7[0, 0, 7] -> Stmt_for_body7[1, 0, 7];"
2508               "Stmt_for_body7[i0, i1, i2] -> "
2509                 "Stmt_for_body24[i0, o1, -1 + i2 - o1, -1 + i1 - o1]:"
2510                 "i0 >= 0 and i0 <= 1 and o1 >= 0 and i2 >= 1 + i1 and "
2511                 "o1 <= -2 + i2 and i2 <= 7 and o1 <= -1 + i1;"
2512               "Stmt_for_body7[i0, i1, i2] -> "
2513                 "Stmt_for_body24[i0, i1, o2, -1 - i1 + i2]:"
2514                 "i0 >= 0 and i0 <= 1 and i1 >= 0 and o2 >= -i1 + i2 and "
2515                 "o2 >= 1 and o2 <= 6 - i1 and i2 >= 1 + i1 }";
2516         P = V;
2517         S = "{ Stmt_for_body24[i0, i1, i2, i3] -> "
2518                 "[i0, 5i0 + i1, 6i0 + i1 + i2, 1 + 6i0 + i1 + i2 + i3, 1];"
2519             "Stmt_for_body7[i0, i1, i2] -> [0, 5i0, 6i0 + i1, 6i0 + i2, 0] }";
2520
2521         if (test_special_schedule(ctx, D, V, P, S) < 0)
2522                 return -1;
2523
2524         D = "{ S_0[i, j] : i >= 1 and i <= 10 and j >= 1 and j <= 8 }";
2525         V = "{ S_0[i, j] -> S_0[i, 1 + j] : i >= 1 and i <= 10 and "
2526                                            "j >= 1 and j <= 7;"
2527                 "S_0[i, j] -> S_0[1 + i, j] : i >= 1 and i <= 9 and "
2528                                              "j >= 1 and j <= 8 }";
2529         P = "{ }";
2530         S = "{ S_0[i, j] -> [i + j, j] }";
2531         ctx->opt->schedule_algorithm = ISL_SCHEDULE_ALGORITHM_FEAUTRIER;
2532         if (test_special_schedule(ctx, D, V, P, S) < 0)
2533                 return -1;
2534         ctx->opt->schedule_algorithm = ISL_SCHEDULE_ALGORITHM_ISL;
2535
2536         /* Fig. 1 from Feautrier's "Some Efficient Solutions..." pt. 2, 1992 */
2537         D = "[N] -> { S_0[i, j] : i >= 0 and i <= -1 + N and "
2538                                  "j >= 0 and j <= -1 + i }";
2539         V = "[N] -> { S_0[i, j] -> S_0[i, 1 + j] : j <= -2 + i and "
2540                                         "i <= -1 + N and j >= 0;"
2541                      "S_0[i, -1 + i] -> S_0[1 + i, 0] : i >= 1 and "
2542                                         "i <= -2 + N }";
2543         P = "{ }";
2544         S = "{ S_0[i, j] -> [i, j] }";
2545         ctx->opt->schedule_algorithm = ISL_SCHEDULE_ALGORITHM_FEAUTRIER;
2546         if (test_special_schedule(ctx, D, V, P, S) < 0)
2547                 return -1;
2548         ctx->opt->schedule_algorithm = ISL_SCHEDULE_ALGORITHM_ISL;
2549
2550         /* Test both algorithms on a case with only proximity dependences. */
2551         D = "{ S[i,j] : 0 <= i <= 10 }";
2552         V = "{ }";
2553         P = "{ S[i,j] -> S[i+1,j] : 0 <= i,j <= 10 }";
2554         S = "{ S[i, j] -> [j, i] }";
2555         ctx->opt->schedule_algorithm = ISL_SCHEDULE_ALGORITHM_FEAUTRIER;
2556         if (test_special_schedule(ctx, D, V, P, S) < 0)
2557                 return -1;
2558         ctx->opt->schedule_algorithm = ISL_SCHEDULE_ALGORITHM_ISL;
2559         return test_special_schedule(ctx, D, V, P, S);
2560 }
2561
2562 int test_plain_injective(isl_ctx *ctx, const char *str, int injective)
2563 {
2564         isl_union_map *umap;
2565         int test;
2566
2567         umap = isl_union_map_read_from_str(ctx, str);
2568         test = isl_union_map_plain_is_injective(umap);
2569         isl_union_map_free(umap);
2570         if (test < 0)
2571                 return -1;
2572         if (test == injective)
2573                 return 0;
2574         if (injective)
2575                 isl_die(ctx, isl_error_unknown,
2576                         "map not detected as injective", return -1);
2577         else
2578                 isl_die(ctx, isl_error_unknown,
2579                         "map detected as injective", return -1);
2580 }
2581
2582 int test_injective(isl_ctx *ctx)
2583 {
2584         const char *str;
2585
2586         if (test_plain_injective(ctx, "{S[i,j] -> A[0]; T[i,j] -> B[1]}", 0))
2587                 return -1;
2588         if (test_plain_injective(ctx, "{S[] -> A[0]; T[] -> B[0]}", 1))
2589                 return -1;
2590         if (test_plain_injective(ctx, "{S[] -> A[0]; T[] -> A[1]}", 1))
2591                 return -1;
2592         if (test_plain_injective(ctx, "{S[] -> A[0]; T[] -> A[0]}", 0))
2593                 return -1;
2594         if (test_plain_injective(ctx, "{S[i] -> A[i,0]; T[i] -> A[i,1]}", 1))
2595                 return -1;
2596         if (test_plain_injective(ctx, "{S[i] -> A[i]; T[i] -> A[i]}", 0))
2597                 return -1;
2598         if (test_plain_injective(ctx, "{S[] -> A[0,0]; T[] -> A[0,1]}", 1))
2599                 return -1;
2600         if (test_plain_injective(ctx, "{S[] -> A[0,0]; T[] -> A[1,0]}", 1))
2601                 return -1;
2602
2603         str = "{S[] -> A[0,0]; T[] -> A[0,1]; U[] -> A[1,0]}";
2604         if (test_plain_injective(ctx, str, 1))
2605                 return -1;
2606         str = "{S[] -> A[0,0]; T[] -> A[0,1]; U[] -> A[0,0]}";
2607         if (test_plain_injective(ctx, str, 0))
2608                 return -1;
2609
2610         return 0;
2611 }
2612
2613 static int aff_plain_is_equal(__isl_keep isl_aff *aff, const char *str)
2614 {
2615         isl_aff *aff2;
2616         int equal;
2617
2618         if (!aff)
2619                 return -1;
2620
2621         aff2 = isl_aff_read_from_str(isl_aff_get_ctx(aff), str);
2622         equal = isl_aff_plain_is_equal(aff, aff2);
2623         isl_aff_free(aff2);
2624
2625         return equal;
2626 }
2627
2628 static int aff_check_plain_equal(__isl_keep isl_aff *aff, const char *str)
2629 {
2630         int equal;
2631
2632         equal = aff_plain_is_equal(aff, str);
2633         if (equal < 0)
2634                 return -1;
2635         if (!equal)
2636                 isl_die(isl_aff_get_ctx(aff), isl_error_unknown,
2637                         "result not as expected", return -1);
2638         return 0;
2639 }
2640
2641 int test_aff(isl_ctx *ctx)
2642 {
2643         const char *str;
2644         isl_set *set;
2645         isl_space *space;
2646         isl_local_space *ls;
2647         isl_aff *aff;
2648         int zero, equal;
2649
2650         space = isl_space_set_alloc(ctx, 0, 1);
2651         ls = isl_local_space_from_space(space);
2652         aff = isl_aff_zero_on_domain(ls);
2653
2654         aff = isl_aff_add_coefficient_si(aff, isl_dim_in, 0, 1);
2655         aff = isl_aff_scale_down_ui(aff, 3);
2656         aff = isl_aff_floor(aff);
2657         aff = isl_aff_add_coefficient_si(aff, isl_dim_in, 0, 1);
2658         aff = isl_aff_scale_down_ui(aff, 2);
2659         aff = isl_aff_floor(aff);
2660         aff = isl_aff_add_coefficient_si(aff, isl_dim_in, 0, 1);
2661
2662         str = "{ [10] }";
2663         set = isl_set_read_from_str(ctx, str);
2664         aff = isl_aff_gist(aff, set);
2665
2666         aff = isl_aff_add_constant_si(aff, -16);
2667         zero = isl_aff_plain_is_zero(aff);
2668         isl_aff_free(aff);
2669
2670         if (zero < 0)
2671                 return -1;
2672         if (!zero)
2673                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2674
2675         aff = isl_aff_read_from_str(ctx, "{ [-1] }");
2676         aff = isl_aff_scale_down_ui(aff, 64);
2677         aff = isl_aff_floor(aff);
2678         equal = aff_check_plain_equal(aff, "{ [-1] }");
2679         isl_aff_free(aff);
2680         if (equal < 0)
2681                 return -1;
2682
2683         return 0;
2684 }
2685
2686 int test_dim_max(isl_ctx *ctx)
2687 {
2688         int equal;
2689         const char *str;
2690         isl_set *set1, *set2;
2691         isl_set *set;
2692         isl_map *map;
2693         isl_pw_aff *pwaff;
2694
2695         str = "[N] -> { [i] : 0 <= i <= min(N,10) }";
2696         set = isl_set_read_from_str(ctx, str);
2697         pwaff = isl_set_dim_max(set, 0);
2698         set1 = isl_set_from_pw_aff(pwaff);
2699         str = "[N] -> { [10] : N >= 10; [N] : N <= 9 and N >= 0 }";
2700         set2 = isl_set_read_from_str(ctx, str);
2701         equal = isl_set_is_equal(set1, set2);
2702         isl_set_free(set1);
2703         isl_set_free(set2);
2704         if (equal < 0)
2705                 return -1;
2706         if (!equal)
2707                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2708
2709         str = "[N] -> { [i] : 0 <= i <= max(2N,N+6) }";
2710         set = isl_set_read_from_str(ctx, str);
2711         pwaff = isl_set_dim_max(set, 0);
2712         set1 = isl_set_from_pw_aff(pwaff);
2713         str = "[N] -> { [6 + N] : -6 <= N <= 5; [2N] : N >= 6 }";
2714         set2 = isl_set_read_from_str(ctx, str);
2715         equal = isl_set_is_equal(set1, set2);
2716         isl_set_free(set1);
2717         isl_set_free(set2);
2718         if (equal < 0)
2719                 return -1;
2720         if (!equal)
2721                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2722
2723         str = "[N] -> { [i] : 0 <= i <= 2N or 0 <= i <= N+6 }";
2724         set = isl_set_read_from_str(ctx, str);
2725         pwaff = isl_set_dim_max(set, 0);
2726         set1 = isl_set_from_pw_aff(pwaff);
2727         str = "[N] -> { [6 + N] : -6 <= N <= 5; [2N] : N >= 6 }";
2728         set2 = isl_set_read_from_str(ctx, str);
2729         equal = isl_set_is_equal(set1, set2);
2730         isl_set_free(set1);
2731         isl_set_free(set2);
2732         if (equal < 0)
2733                 return -1;
2734         if (!equal)
2735                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2736
2737         str = "[N,M] -> { [i,j] -> [([i/16]), i%16, ([j/16]), j%16] : "
2738                         "0 <= i < N and 0 <= j < M }";
2739         map = isl_map_read_from_str(ctx, str);
2740         set = isl_map_range(map);
2741
2742         pwaff = isl_set_dim_max(isl_set_copy(set), 0);
2743         set1 = isl_set_from_pw_aff(pwaff);
2744         str = "[N,M] -> { [([(N-1)/16])] : M,N > 0 }";
2745         set2 = isl_set_read_from_str(ctx, str);
2746         equal = isl_set_is_equal(set1, set2);
2747         isl_set_free(set1);
2748         isl_set_free(set2);
2749
2750         pwaff = isl_set_dim_max(isl_set_copy(set), 3);
2751         set1 = isl_set_from_pw_aff(pwaff);
2752         str = "[N,M] -> { [t] : t = min(M-1,15) and M,N > 0 }";
2753         set2 = isl_set_read_from_str(ctx, str);
2754         if (equal >= 0 && equal)
2755                 equal = isl_set_is_equal(set1, set2);
2756         isl_set_free(set1);
2757         isl_set_free(set2);
2758
2759         isl_set_free(set);
2760
2761         if (equal < 0)
2762                 return -1;
2763         if (!equal)
2764                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2765
2766         return 0;
2767 }
2768
2769 int test_product(isl_ctx *ctx)
2770 {
2771         const char *str;
2772         isl_set *set;
2773         isl_union_set *uset1, *uset2;
2774         int ok;
2775
2776         str = "{ A[i] }";
2777         set = isl_set_read_from_str(ctx, str);
2778         set = isl_set_product(set, isl_set_copy(set));
2779         ok = isl_set_is_wrapping(set);
2780         isl_set_free(set);
2781         if (ok < 0)
2782                 return -1;
2783         if (!ok)
2784                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2785
2786         str = "{ [] }";
2787         uset1 = isl_union_set_read_from_str(ctx, str);
2788         uset1 = isl_union_set_product(uset1, isl_union_set_copy(uset1));
2789         str = "{ [[] -> []] }";
2790         uset2 = isl_union_set_read_from_str(ctx, str);
2791         ok = isl_union_set_is_equal(uset1, uset2);
2792         isl_union_set_free(uset1);
2793         isl_union_set_free(uset2);
2794         if (ok < 0)
2795                 return -1;
2796         if (!ok)
2797                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2798
2799         return 0;
2800 }
2801
2802 int test_equal(isl_ctx *ctx)
2803 {
2804         const char *str;
2805         isl_set *set, *set2;
2806         int equal;
2807
2808         str = "{ S_6[i] }";
2809         set = isl_set_read_from_str(ctx, str);
2810         str = "{ S_7[i] }";
2811         set2 = isl_set_read_from_str(ctx, str);
2812         equal = isl_set_is_equal(set, set2);
2813         isl_set_free(set);
2814         isl_set_free(set2);
2815         if (equal < 0)
2816                 return -1;
2817         if (equal)
2818                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2819
2820         return 0;
2821 }
2822
2823 static int test_plain_fixed(isl_ctx *ctx, __isl_take isl_map *map,
2824         enum isl_dim_type type, unsigned pos, int fixed)
2825 {
2826         int test;
2827
2828         test = isl_map_plain_is_fixed(map, type, pos, NULL);
2829         isl_map_free(map);
2830         if (test < 0)
2831                 return -1;
2832         if (test == fixed)
2833                 return 0;
2834         if (fixed)
2835                 isl_die(ctx, isl_error_unknown,
2836                         "map not detected as fixed", return -1);
2837         else
2838                 isl_die(ctx, isl_error_unknown,
2839                         "map detected as fixed", return -1);
2840 }
2841
2842 int test_fixed(isl_ctx *ctx)
2843 {
2844         const char *str;
2845         isl_map *map;
2846
2847         str = "{ [i] -> [i] }";
2848         map = isl_map_read_from_str(ctx, str);
2849         if (test_plain_fixed(ctx, map, isl_dim_out, 0, 0))
2850                 return -1;
2851         str = "{ [i] -> [1] }";
2852         map = isl_map_read_from_str(ctx, str);
2853         if (test_plain_fixed(ctx, map, isl_dim_out, 0, 1))
2854                 return -1;
2855         str = "{ S_1[p1] -> [o0] : o0 = -2 and p1 >= 1 and p1 <= 7 }";
2856         map = isl_map_read_from_str(ctx, str);
2857         if (test_plain_fixed(ctx, map, isl_dim_out, 0, 1))
2858                 return -1;
2859         map = isl_map_read_from_str(ctx, str);
2860         map = isl_map_neg(map);
2861         if (test_plain_fixed(ctx, map, isl_dim_out, 0, 1))
2862                 return -1;
2863
2864         return 0;
2865 }
2866
2867 int test_vertices(isl_ctx *ctx)
2868 {
2869         const char *str;
2870         isl_basic_set *bset;
2871         isl_vertices *vertices;
2872
2873         str = "{ A[t, i] : t = 12 and i >= 4 and i <= 12 }";
2874         bset = isl_basic_set_read_from_str(ctx, str);
2875         vertices = isl_basic_set_compute_vertices(bset);
2876         isl_basic_set_free(bset);
2877         isl_vertices_free(vertices);
2878         if (!vertices)
2879                 return -1;
2880
2881         str = "{ A[t, i] : t = 14 and i = 1 }";
2882         bset = isl_basic_set_read_from_str(ctx, str);
2883         vertices = isl_basic_set_compute_vertices(bset);
2884         isl_basic_set_free(bset);
2885         isl_vertices_free(vertices);
2886         if (!vertices)
2887                 return -1;
2888
2889         return 0;
2890 }
2891
2892 int test_union_pw(isl_ctx *ctx)
2893 {
2894         int equal;
2895         const char *str;
2896         isl_union_set *uset;
2897         isl_union_pw_qpolynomial *upwqp1, *upwqp2;
2898
2899         str = "{ [x] -> x^2 }";
2900         upwqp1 = isl_union_pw_qpolynomial_read_from_str(ctx, str);
2901         upwqp2 = isl_union_pw_qpolynomial_copy(upwqp1);
2902         uset = isl_union_pw_qpolynomial_domain(upwqp1);
2903         upwqp1 = isl_union_pw_qpolynomial_copy(upwqp2);
2904         upwqp1 = isl_union_pw_qpolynomial_intersect_domain(upwqp1, uset);
2905         equal = isl_union_pw_qpolynomial_plain_is_equal(upwqp1, upwqp2);
2906         isl_union_pw_qpolynomial_free(upwqp1);
2907         isl_union_pw_qpolynomial_free(upwqp2);
2908         if (equal < 0)
2909                 return -1;
2910         if (!equal)
2911                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2912
2913         return 0;
2914 }
2915
2916 int test_output(isl_ctx *ctx)
2917 {
2918         char *s;
2919         const char *str;
2920         isl_pw_aff *pa;
2921         isl_printer *p;
2922         int equal;
2923
2924         str = "[x] -> { [1] : x % 4 <= 2; [2] : x = 3 }";
2925         pa = isl_pw_aff_read_from_str(ctx, str);
2926
2927         p = isl_printer_to_str(ctx);
2928         p = isl_printer_set_output_format(p, ISL_FORMAT_C);
2929         p = isl_printer_print_pw_aff(p, pa);
2930         s = isl_printer_get_str(p);
2931         isl_printer_free(p);
2932         isl_pw_aff_free(pa);
2933         equal = !strcmp(s, "(2 - x + 4*floord(x, 4) >= 0) ? (1) : 2");
2934         free(s);
2935         if (equal < 0)
2936                 return -1;
2937         if (!equal)
2938                 isl_die(ctx, isl_error_unknown, "unexpected result", return -1);
2939
2940         return 0;
2941 }
2942
2943 int test_sample(isl_ctx *ctx)
2944 {
2945         const char *str;
2946         isl_basic_set *bset1, *bset2;
2947         int empty, subset;
2948
2949         str = "{ [a, b, c, d, e, f, g, h, i, j, k] : "
2950             "3i >= 1073741823b - c - 1073741823e + f and c >= 0 and "
2951             "3i >= -1 + 3221225466b + c + d - 3221225466e - f and "
2952             "2e >= a - b and 3e <= 2a and 3k <= -a and f <= -1 + a and "
2953             "3i <= 4 - a + 4b + 2c - e - 2f and 3k <= -a + c - f and "
2954             "3h >= -2 + a and 3g >= -3 - a and 3k >= -2 - a and "
2955             "3i >= -2 - a - 2c + 3e + 2f and 3h <= a + c - f and "
2956             "3h >= a + 2147483646b + 2c - 2147483646e - 2f and "
2957             "3g <= -1 - a and 3i <= 1 + c + d - f and a <= 1073741823 and "
2958             "f >= 1 - a + 1073741822b + c + d - 1073741822e and "
2959             "3i >= 1 + 2b - 2c + e + 2f + 3g and "
2960             "1073741822f <= 1073741822 - a + 1073741821b + 1073741822c +"
2961                 "d - 1073741821e and "
2962             "3j <= 3 - a + 3b and 3g <= -2 - 2b + c + d - e - f and "
2963             "3j >= 1 - a + b + 2e and "
2964             "3f >= -3 + a + 3221225462b + 3c + d - 3221225465e and "
2965             "3i <= 4 - a + 4b - e and "
2966             "f <= 1073741822 + 1073741822b - 1073741822e and 3h <= a and "
2967             "f >= 0 and 2e <= 4 - a + 5b - d and 2e <= a - b + d and "
2968             "c <= -1 + a and 3i >= -2 - a + 3e and "
2969             "1073741822e <= 1073741823 - a + 1073741822b + c and "
2970             "3g >= -4 + 3221225464b + 3c + d - 3221225467e - 3f and "
2971             "3i >= -1 + 3221225466b + 3c + d - 3221225466e - 3f and "
2972             "1073741823e >= 1 + 1073741823b - d and "
2973             "3i >= 1073741823b + c - 1073741823e - f and "
2974             "3i >= 1 + 2b + e + 3g }";
2975         bset1 = isl_basic_set_read_from_str(ctx, str);
2976         bset2 = isl_basic_set_sample(isl_basic_set_copy(bset1));
2977         empty = isl_basic_set_is_empty(bset2);
2978         subset = isl_basic_set_is_subset(bset2, bset1);
2979         isl_basic_set_free(bset1);
2980         isl_basic_set_free(bset2);
2981         if (empty)
2982                 isl_die(ctx, isl_error_unknown, "point not found", return -1);
2983         if (!subset)
2984                 isl_die(ctx, isl_error_unknown, "bad point found", return -1);
2985
2986         return 0;
2987 }
2988
2989 int test_fixed_power(isl_ctx *ctx)
2990 {
2991         const char *str;
2992         isl_map *map;
2993         isl_int exp;
2994         int equal;
2995
2996         isl_int_init(exp);
2997         str = "{ [i] -> [i + 1] }";
2998         map = isl_map_read_from_str(ctx, str);
2999         isl_int_set_si(exp, 23);
3000         map = isl_map_fixed_power(map, exp);
3001         equal = map_check_equal(map, "{ [i] -> [i + 23] }");
3002         isl_int_clear(exp);
3003         isl_map_free(map);
3004         if (equal < 0)
3005                 return -1;
3006
3007         return 0;
3008 }
3009
3010 int test_slice(isl_ctx *ctx)
3011 {
3012         const char *str;
3013         isl_map *map;
3014         int equal;
3015
3016         str = "{ [i] -> [j] }";
3017         map = isl_map_read_from_str(ctx, str);
3018         map = isl_map_equate(map, isl_dim_in, 0, isl_dim_out, 0);
3019         equal = map_check_equal(map, "{ [i] -> [i] }");
3020         isl_map_free(map);
3021         if (equal < 0)
3022                 return -1;
3023
3024         str = "{ [i] -> [j] }";
3025         map = isl_map_read_from_str(ctx, str);
3026         map = isl_map_equate(map, isl_dim_in, 0, isl_dim_in, 0);
3027         equal = map_check_equal(map, "{ [i] -> [j] }");
3028         isl_map_free(map);
3029         if (equal < 0)
3030                 return -1;
3031
3032         str = "{ [i] -> [j] }";
3033         map = isl_map_read_from_str(ctx, str);
3034         map = isl_map_oppose(map, isl_dim_in, 0, isl_dim_out, 0);
3035         equal = map_check_equal(map, "{ [i] -> [-i] }");
3036         isl_map_free(map);
3037         if (equal < 0)
3038                 return -1;
3039
3040         str = "{ [i] -> [j] }";
3041         map = isl_map_read_from_str(ctx, str);
3042         map = isl_map_oppose(map, isl_dim_in, 0, isl_dim_in, 0);
3043         equal = map_check_equal(map, "{ [0] -> [j] }");
3044         isl_map_free(map);
3045         if (equal < 0)
3046                 return -1;
3047
3048         str = "{ [i] -> [j] }";
3049         map = isl_map_read_from_str(ctx, str);
3050         map = isl_map_order_gt(map, isl_dim_in, 0, isl_dim_out, 0);
3051         equal = map_check_equal(map, "{ [i] -> [j] : i > j }");
3052         isl_map_free(map);
3053         if (equal < 0)
3054                 return -1;
3055
3056         str = "{ [i] -> [j] }";
3057         map = isl_map_read_from_str(ctx, str);
3058         map = isl_map_order_gt(map, isl_dim_in, 0, isl_dim_in, 0);
3059         equal = map_check_equal(map, "{ [i] -> [j] : false }");
3060         isl_map_free(map);
3061         if (equal < 0)
3062                 return -1;
3063
3064         return 0;
3065 }
3066
3067 int test_eliminate(isl_ctx *ctx)
3068 {
3069         const char *str;
3070         isl_map *map;
3071         int equal;
3072
3073         str = "{ [i] -> [j] : i = 2j }";
3074         map = isl_map_read_from_str(ctx, str);
3075         map = isl_map_eliminate(map, isl_dim_out, 0, 1);
3076         equal = map_check_equal(map, "{ [i] -> [j] : exists a : i = 2a }");
3077         isl_map_free(map);
3078         if (equal < 0)
3079                 return -1;
3080
3081         return 0;
3082 }
3083
3084 /* Check that isl_set_dim_residue_class detects that the values of j
3085  * in the set below are all odd and that it does not detect any spurious
3086  * strides.
3087  */
3088 static int test_residue_class(isl_ctx *ctx)
3089 {
3090         const char *str;
3091         isl_set *set;
3092         isl_int m, r;
3093         int res;
3094
3095         str = "{ [i,j] : j = 4 i + 1 and 0 <= i <= 100; "
3096                 "[i,j] : j = 4 i + 3 and 500 <= i <= 600 }";
3097         set = isl_set_read_from_str(ctx, str);
3098         isl_int_init(m);
3099         isl_int_init(r);
3100         res = isl_set_dim_residue_class(set, 1, &m, &r);
3101         if (res >= 0 &&
3102             (isl_int_cmp_si(m, 2) != 0 || isl_int_cmp_si(r, 1) != 0))
3103                 isl_die(ctx, isl_error_unknown, "incorrect residue class",
3104                         res = -1);
3105         isl_int_clear(r);
3106         isl_int_clear(m);
3107         isl_set_free(set);
3108
3109         return res;
3110 }
3111
3112 int test_align_parameters(isl_ctx *ctx)
3113 {
3114         const char *str;
3115         isl_space *space;
3116         isl_multi_aff *ma1, *ma2;
3117         int equal;
3118
3119         str = "{ A[B[] -> C[]] -> D[E[] -> F[]] }";
3120         ma1 = isl_multi_aff_read_from_str(ctx, str);
3121
3122         space = isl_space_params_alloc(ctx, 1);
3123         space = isl_space_set_dim_name(space, isl_dim_param, 0, "N");
3124         ma1 = isl_multi_aff_align_params(ma1, space);
3125
3126         str = "[N] -> { A[B[] -> C[]] -> D[E[] -> F[]] }";
3127         ma2 = isl_multi_aff_read_from_str(ctx, str);
3128
3129         equal = isl_multi_aff_plain_is_equal(ma1, ma2);
3130
3131         isl_multi_aff_free(ma1);
3132         isl_multi_aff_free(ma2);
3133
3134         if (equal < 0)
3135                 return -1;
3136         if (!equal)
3137                 isl_die(ctx, isl_error_unknown,
3138                         "result not as expected", return -1);
3139
3140         return 0;
3141 }
3142
3143 static int test_list(isl_ctx *ctx)
3144 {
3145         isl_id *a, *b, *c, *d, *id;
3146         isl_id_list *list;
3147         int ok;
3148
3149         a = isl_id_alloc(ctx, "a", NULL);
3150         b = isl_id_alloc(ctx, "b", NULL);
3151         c = isl_id_alloc(ctx, "c", NULL);
3152         d = isl_id_alloc(ctx, "d", NULL);
3153
3154         list = isl_id_list_alloc(ctx, 4);
3155         list = isl_id_list_add(list, a);
3156         list = isl_id_list_add(list, b);
3157         list = isl_id_list_add(list, c);
3158         list = isl_id_list_add(list, d);
3159         list = isl_id_list_drop(list, 1, 1);
3160
3161         if (isl_id_list_n_id(list) != 3) {
3162                 isl_id_list_free(list);
3163                 isl_die(ctx, isl_error_unknown,
3164                         "unexpected number of elements in list", return -1);
3165         }
3166
3167         id = isl_id_list_get_id(list, 0);
3168         ok = id == a;
3169         isl_id_free(id);
3170         id = isl_id_list_get_id(list, 1);
3171         ok = ok && id == c;
3172         isl_id_free(id);
3173         id = isl_id_list_get_id(list, 2);
3174         ok = ok && id == d;
3175         isl_id_free(id);
3176
3177         isl_id_list_free(list);
3178
3179         if (!ok)
3180                 isl_die(ctx, isl_error_unknown,
3181                         "unexpected elements in list", return -1);
3182
3183         return 0;
3184 }
3185
3186 struct {
3187         const char *set;
3188         const char *ma;
3189         const char *res;
3190 } preimage_tests[] = {
3191         { "{ B[i,j] : 0 <= i < 10 and 0 <= j < 100 }",
3192           "{ A[j,i] -> B[i,j] }",
3193           "{ A[j,i] : 0 <= i < 10 and 0 <= j < 100 }" },
3194         { "{ rat: B[i,j] : 0 <= i, j and 3 i + 5 j <= 100 }",
3195           "{ A[a,b] -> B[a/2,b/6] }",
3196           "{ rat: A[a,b] : 0 <= a, b and 9 a + 5 b <= 600 }" },
3197         { "{ B[i,j] : 0 <= i, j and 3 i + 5 j <= 100 }",
3198           "{ A[a,b] -> B[a/2,b/6] }",
3199           "{ A[a,b] : 0 <= a, b and 9 a + 5 b <= 600 and "
3200                     "exists i,j : a = 2 i and b = 6 j }" },
3201         { "[n] -> { S[i] : 0 <= i <= 100 }", "[n] -> { S[n] }",
3202           "[n] -> { : 0 <= n <= 100 }" },
3203         { "{ B[i] : 0 <= i < 100 and exists a : i = 4 a }",
3204           "{ A[a] -> B[2a] }",
3205           "{ A[a] : 0 <= a < 50 and exists b : a = 2 b }" },
3206         { "{ B[i] : 0 <= i < 100 and exists a : i = 4 a }",
3207           "{ A[a] -> B[([a/2])] }",
3208           "{ A[a] : 0 <= a < 200 and exists b : [a/2] = 4 b }" },
3209         { "{ B[i,j,k] : 0 <= i,j,k <= 100 }",
3210           "{ A[a] -> B[a,a,a/3] }",
3211           "{ A[a] : 0 <= a <= 100 and exists b : a = 3 b }" },
3212         { "{ B[i,j] : j = [(i)/2] } ", "{ A[i,j] -> B[i/3,j] }",
3213           "{ A[i,j] : j = [(i)/6] and exists a : i = 3 a }" },
3214 };
3215
3216 int test_preimage(isl_ctx *ctx)
3217 {
3218         int i;
3219         isl_basic_set *bset1, *bset2;
3220         isl_multi_aff *ma;
3221         int equal;
3222
3223         for (i = 0; i < ARRAY_SIZE(preimage_tests); ++i) {
3224                 bset1 = isl_basic_set_read_from_str(ctx, preimage_tests[i].set);
3225                 ma = isl_multi_aff_read_from_str(ctx, preimage_tests[i].ma);
3226                 bset2 = isl_basic_set_read_from_str(ctx, preimage_tests[i].res);
3227                 bset1 = isl_basic_set_preimage_multi_aff(bset1, ma);
3228                 equal = isl_basic_set_is_equal(bset1, bset2);
3229                 isl_basic_set_free(bset1);
3230                 isl_basic_set_free(bset2);
3231                 if (equal < 0)
3232                         return -1;
3233                 if (!equal)
3234                         isl_die(ctx, isl_error_unknown, "bad preimage",
3235                                 return -1);
3236         }
3237
3238         return 0;
3239 }
3240
3241 struct {
3242         const char *name;
3243         int (*fn)(isl_ctx *ctx);
3244 } tests [] = {
3245         { "list", &test_list },
3246         { "align parameters", &test_align_parameters },
3247         { "preimage", &test_preimage },
3248         { "eliminate", &test_eliminate },
3249         { "reisdue class", &test_residue_class },
3250         { "div", &test_div },
3251         { "slice", &test_slice },
3252         { "fixed power", &test_fixed_power },
3253         { "sample", &test_sample },
3254         { "output", &test_output },
3255         { "vertices", &test_vertices },
3256         { "fixed", &test_fixed },
3257         { "equal", &test_equal },
3258         { "product", &test_product },
3259         { "dim_max", &test_dim_max },
3260         { "affine", &test_aff },
3261         { "injective", &test_injective },
3262         { "schedule", &test_schedule },
3263         { "union_pw", &test_union_pw },
3264         { "parse", &test_parse },
3265         { "single-valued", &test_sv },
3266         { "affine hull", &test_affine_hull },
3267         { "coalesce", &test_coalesce },
3268         { "factorize", &test_factorize },
3269         { "subset", &test_subset },
3270         { "subtract", &test_subtract },
3271 };
3272
3273 int main()
3274 {
3275         int i;
3276         struct isl_ctx *ctx;
3277
3278         srcdir = getenv("srcdir");
3279         assert(srcdir);
3280
3281         ctx = isl_ctx_alloc();
3282         for (i = 0; i < ARRAY_SIZE(tests); ++i) {
3283                 printf("%s\n", tests[i].name);
3284                 if (tests[i].fn(ctx) < 0)
3285                         goto error;
3286         }
3287         test_lift(ctx);
3288         test_bound(ctx);
3289         test_union(ctx);
3290         test_split_periods(ctx);
3291         test_pwqp(ctx);
3292         test_lex(ctx);
3293         test_bijective(ctx);
3294         test_dep(ctx);
3295         test_read(ctx);
3296         test_bounded(ctx);
3297         test_construction(ctx);
3298         test_dim(ctx);
3299         test_application(ctx);
3300         test_convex_hull(ctx);
3301         test_gist(ctx);
3302         test_closure(ctx);
3303         test_lexmin(ctx);
3304         isl_ctx_free(ctx);
3305         return 0;
3306 error:
3307         isl_ctx_free(ctx);
3308         return -1;
3309 }