isl_test.c

   1 #include <assert.h>
   2 #include <stdio.h>
   3 #include <limits.h>
   4 #include <isl_ctx.h>
   5 #include <isl_set.h>
   6 #include <isl_constraint.h>
   7
   8 static char *srcdir;
   9
  10 void test_read(struct isl_ctx *ctx)
  11 {
  12         char filename[PATH_MAX];
  13         FILE *input;
  14         int n;
  15         struct isl_basic_set *bset1, *bset2;
  16         const char *str = "{[y]: Exists ( alpha : 2alpha = y)}";
  17
  18         n = snprintf(filename, sizeof(filename),
  19                         "%s/test_inputs/set.omega", srcdir);
  20         assert(n < sizeof(filename));
  21         input = fopen(filename, "r");
  22         assert(input);
  23
  24         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
  25         bset2 = isl_basic_set_read_from_str(ctx, str, 0, ISL_FORMAT_OMEGA);
  26
  27         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
  28
  29         isl_basic_set_free(bset1);
  30         isl_basic_set_free(bset2);
  31
  32         fclose(input);
  33 }
  34
  35 /* Construct the basic set { [i] : 5 <= i <= N } */
  36 void test_construction(struct isl_ctx *ctx)
  37 {
  38         isl_int v;
  39         struct isl_dim *dim;
  40         struct isl_basic_set *bset;
  41         struct isl_constraint *c;
  42
  43         isl_int_init(v);
  44
  45         dim = isl_dim_set_alloc(ctx, 1, 1);
  46         bset = isl_basic_set_universe(dim);
  47
  48         c = isl_inequality_alloc(isl_dim_copy(bset->dim));
  49         isl_int_set_si(v, -1);
  50         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
  51         isl_int_set_si(v, 1);
  52         isl_constraint_set_coefficient(c, isl_dim_param, 0, v);
  53         bset = isl_basic_set_add_constraint(bset, c);
  54
  55         c = isl_inequality_alloc(isl_dim_copy(bset->dim));
  56         isl_int_set_si(v, 1);
  57         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
  58         isl_int_set_si(v, -5);
  59         isl_constraint_set_constant(c, v);
  60         bset = isl_basic_set_add_constraint(bset, c);
  61
  62         isl_basic_set_free(bset);
  63
  64         isl_int_clear(v);
  65 }
  66
  67 void test_div(struct isl_ctx *ctx)
  68 {
  69         isl_int v;
  70         int pos;
  71         struct isl_dim *dim;
  72         struct isl_div *div;
  73         struct isl_basic_set *bset;
  74         struct isl_constraint *c;
  75
  76         isl_int_init(v);
  77
  78         /* test 1 */
  79         dim = isl_dim_set_alloc(ctx, 0, 1);
  80         bset = isl_basic_set_universe(dim);
  81
  82         c = isl_equality_alloc(isl_dim_copy(bset->dim));
  83         isl_int_set_si(v, -1);
  84         isl_constraint_set_constant(c, v);
  85         isl_int_set_si(v, 1);
  86         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
  87         div = isl_div_alloc(isl_dim_copy(bset->dim));
  88         c = isl_constraint_add_div(c, div, &pos);
  89         isl_int_set_si(v, 3);
  90         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
  91         bset = isl_basic_set_add_constraint(bset, c);
  92
  93         c = isl_equality_alloc(isl_dim_copy(bset->dim));
  94         isl_int_set_si(v, 1);
  95         isl_constraint_set_constant(c, v);
  96         isl_int_set_si(v, -1);
  97         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
  98         div = isl_div_alloc(isl_dim_copy(bset->dim));
  99         c = isl_constraint_add_div(c, div, &pos);
 100         isl_int_set_si(v, 3);
 101         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 102         bset = isl_basic_set_add_constraint(bset, c);
 103
 104         assert(bset->n_div == 1);
 105         isl_basic_set_free(bset);
 106
 107         /* test 2 */
 108         dim = isl_dim_set_alloc(ctx, 0, 1);
 109         bset = isl_basic_set_universe(dim);
 110
 111         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 112         isl_int_set_si(v, 1);
 113         isl_constraint_set_constant(c, v);
 114         isl_int_set_si(v, -1);
 115         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 116         div = isl_div_alloc(isl_dim_copy(bset->dim));
 117         c = isl_constraint_add_div(c, div, &pos);
 118         isl_int_set_si(v, 3);
 119         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 120         bset = isl_basic_set_add_constraint(bset, c);
 121
 122         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 123         isl_int_set_si(v, -1);
 124         isl_constraint_set_constant(c, v);
 125         isl_int_set_si(v, 1);
 126         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 127         div = isl_div_alloc(isl_dim_copy(bset->dim));
 128         c = isl_constraint_add_div(c, div, &pos);
 129         isl_int_set_si(v, 3);
 130         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 131         bset = isl_basic_set_add_constraint(bset, c);
 132
 133         assert(bset->n_div == 1);
 134         isl_basic_set_free(bset);
 135
 136         /* test 3 */
 137         dim = isl_dim_set_alloc(ctx, 0, 1);
 138         bset = isl_basic_set_universe(dim);
 139
 140         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 141         isl_int_set_si(v, 1);
 142         isl_constraint_set_constant(c, v);
 143         isl_int_set_si(v, -1);
 144         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 145         div = isl_div_alloc(isl_dim_copy(bset->dim));
 146         c = isl_constraint_add_div(c, div, &pos);
 147         isl_int_set_si(v, 3);
 148         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 149         bset = isl_basic_set_add_constraint(bset, c);
 150
 151         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 152         isl_int_set_si(v, -3);
 153         isl_constraint_set_constant(c, v);
 154         isl_int_set_si(v, 1);
 155         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 156         div = isl_div_alloc(isl_dim_copy(bset->dim));
 157         c = isl_constraint_add_div(c, div, &pos);
 158         isl_int_set_si(v, 4);
 159         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 160         bset = isl_basic_set_add_constraint(bset, c);
 161
 162         assert(bset->n_div == 1);
 163         isl_basic_set_free(bset);
 164
 165         /* test 4 */
 166         dim = isl_dim_set_alloc(ctx, 0, 1);
 167         bset = isl_basic_set_universe(dim);
 168
 169         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 170         isl_int_set_si(v, 2);
 171         isl_constraint_set_constant(c, v);
 172         isl_int_set_si(v, -1);
 173         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 174         div = isl_div_alloc(isl_dim_copy(bset->dim));
 175         c = isl_constraint_add_div(c, div, &pos);
 176         isl_int_set_si(v, 3);
 177         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 178         bset = isl_basic_set_add_constraint(bset, c);
 179
 180         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 181         isl_int_set_si(v, -1);
 182         isl_constraint_set_constant(c, v);
 183         isl_int_set_si(v, 1);
 184         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 185         div = isl_div_alloc(isl_dim_copy(bset->dim));
 186         c = isl_constraint_add_div(c, div, &pos);
 187         isl_int_set_si(v, 6);
 188         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 189         bset = isl_basic_set_add_constraint(bset, c);
 190
 191         assert(isl_basic_set_is_empty(bset));
 192         isl_basic_set_free(bset);
 193
 194         /* test 5 */
 195         dim = isl_dim_set_alloc(ctx, 0, 2);
 196         bset = isl_basic_set_universe(dim);
 197
 198         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 199         isl_int_set_si(v, -1);
 200         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 201         div = isl_div_alloc(isl_dim_copy(bset->dim));
 202         c = isl_constraint_add_div(c, div, &pos);
 203         isl_int_set_si(v, 3);
 204         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 205         bset = isl_basic_set_add_constraint(bset, c);
 206
 207         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 208         isl_int_set_si(v, 1);
 209         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 210         isl_int_set_si(v, -3);
 211         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 212         bset = isl_basic_set_add_constraint(bset, c);
 213
 214         assert(bset->n_div == 0);
 215         isl_basic_set_free(bset);
 216
 217         /* test 6 */
 218         dim = isl_dim_set_alloc(ctx, 0, 2);
 219         bset = isl_basic_set_universe(dim);
 220
 221         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 222         isl_int_set_si(v, -1);
 223         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 224         div = isl_div_alloc(isl_dim_copy(bset->dim));
 225         c = isl_constraint_add_div(c, div, &pos);
 226         isl_int_set_si(v, 6);
 227         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 228         bset = isl_basic_set_add_constraint(bset, c);
 229
 230         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 231         isl_int_set_si(v, 1);
 232         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 233         isl_int_set_si(v, -3);
 234         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 235         bset = isl_basic_set_add_constraint(bset, c);
 236
 237         assert(bset->n_div == 1);
 238         isl_basic_set_free(bset);
 239
 240         /* test 7 */
 241         /* This test is a bit tricky.  We set up an equality
 242          *              a + 3b + 3c = 6 e0
 243          * Normalization of divs creates _two_ divs
 244          *              a = 3 e0
 245          *              c - b - e0 = 2 e1
 246          * Afterwards e0 is removed again because it has coefficient -1
 247          * and we end up with the original equality and div again.
 248          * Perhaps we can avoid the introduction of this temporary div.
 249          */
 250         dim = isl_dim_set_alloc(ctx, 0, 3);
 251         bset = isl_basic_set_universe(dim);
 252
 253         c = isl_equality_alloc(isl_dim_copy(bset->dim));
 254         isl_int_set_si(v, -1);
 255         isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
 256         isl_int_set_si(v, -3);
 257         isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
 258         isl_int_set_si(v, -3);
 259         isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
 260         div = isl_div_alloc(isl_dim_copy(bset->dim));
 261         c = isl_constraint_add_div(c, div, &pos);
 262         isl_int_set_si(v, 6);
 263         isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
 264         bset = isl_basic_set_add_constraint(bset, c);
 265
 266         assert(bset->n_div == 1);
 267         isl_basic_set_free(bset);
 268
 269         isl_int_clear(v);
 270 }
 271
 272 void test_application_case(struct isl_ctx *ctx, const char *name)
 273 {
 274         char filename[PATH_MAX];
 275         FILE *input;
 276         int n;
 277         struct isl_basic_set *bset1, *bset2;
 278         struct isl_basic_map *bmap;
 279
 280         n = snprintf(filename, sizeof(filename),
 281                         "%s/test_inputs/%s.omega", srcdir, name);
 282         assert(n < sizeof(filename));
 283         input = fopen(filename, "r");
 284         assert(input);
 285
 286         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
 287         bmap = isl_basic_map_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
 288
 289         bset1 = isl_basic_set_apply(bset1, bmap);
 290
 291         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
 292
 293         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 294
 295         isl_basic_set_free(bset1);
 296         isl_basic_set_free(bset2);
 297
 298         fclose(input);
 299 }
 300
 301 void test_application(struct isl_ctx *ctx)
 302 {
 303         test_application_case(ctx, "application");
 304         test_application_case(ctx, "application2");
 305 }
 306
 307 void test_affine_hull_case(struct isl_ctx *ctx, const char *name)
 308 {
 309         char filename[PATH_MAX];
 310         FILE *input;
 311         int n;
 312         struct isl_basic_set *bset1, *bset2;
 313
 314         n = snprintf(filename, sizeof(filename),
 315                         "%s/test_inputs/%s.polylib", srcdir, name);
 316         assert(n < sizeof(filename));
 317         input = fopen(filename, "r");
 318         assert(input);
 319
 320         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 321         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 322
 323         bset1 = isl_basic_set_affine_hull(bset1);
 324
 325         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 326
 327         isl_basic_set_free(bset1);
 328         isl_basic_set_free(bset2);
 329
 330         fclose(input);
 331 }
 332
 333 void test_affine_hull(struct isl_ctx *ctx)
 334 {
 335         test_affine_hull_case(ctx, "affine2");
 336         test_affine_hull_case(ctx, "affine");
 337 }
 338
 339 void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
 340 {
 341         char filename[PATH_MAX];
 342         FILE *input;
 343         int n;
 344         struct isl_basic_set *bset1, *bset2;
 345         struct isl_set *set;
 346
 347         n = snprintf(filename, sizeof(filename),
 348                         "%s/test_inputs/%s.polylib", srcdir, name);
 349         assert(n < sizeof(filename));
 350         input = fopen(filename, "r");
 351         assert(input);
 352
 353         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 354         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 355
 356         set = isl_basic_set_union(bset1, bset2);
 357         bset1 = isl_set_convex_hull(set);
 358
 359         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 360
 361         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 362
 363         isl_basic_set_free(bset1);
 364         isl_basic_set_free(bset2);
 365
 366         fclose(input);
 367 }
 368
 369 void test_convex_hull(struct isl_ctx *ctx)
 370 {
 371         test_convex_hull_case(ctx, "convex0");
 372         test_convex_hull_case(ctx, "convex1");
 373         test_convex_hull_case(ctx, "convex2");
 374         test_convex_hull_case(ctx, "convex3");
 375         test_convex_hull_case(ctx, "convex4");
 376         test_convex_hull_case(ctx, "convex5");
 377         test_convex_hull_case(ctx, "convex6");
 378         test_convex_hull_case(ctx, "convex7");
 379         test_convex_hull_case(ctx, "convex8");
 380         test_convex_hull_case(ctx, "convex9");
 381         test_convex_hull_case(ctx, "convex10");
 382         test_convex_hull_case(ctx, "convex11");
 383 }
 384
 385 void test_gist_case(struct isl_ctx *ctx, const char *name)
 386 {
 387         char filename[PATH_MAX];
 388         FILE *input;
 389         int n;
 390         struct isl_basic_set *bset1, *bset2;
 391         struct isl_set *set;
 392
 393         n = snprintf(filename, sizeof(filename),
 394                         "%s/test_inputs/%s.polylib", srcdir, name);
 395         assert(n < sizeof(filename));
 396         input = fopen(filename, "r");
 397         assert(input);
 398
 399         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 400         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 401
 402         bset1 = isl_basic_set_gist(bset1, bset2);
 403
 404         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 405
 406         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 407
 408         isl_basic_set_free(bset1);
 409         isl_basic_set_free(bset2);
 410
 411         fclose(input);
 412 }
 413
 414 void test_gist(struct isl_ctx *ctx)
 415 {
 416         test_gist_case(ctx, "gist1");
 417 }
 418
 419 int main()
 420 {
 421         struct isl_ctx *ctx;
 422
 423         srcdir = getenv("srcdir");
 424
 425         ctx = isl_ctx_alloc();
 426         test_read(ctx);
 427         test_construction(ctx);
 428         test_div(ctx);
 429         test_application(ctx);
 430         test_affine_hull(ctx);
 431         test_convex_hull(ctx);
 432         test_gist(ctx);
 433         isl_ctx_free(ctx);
 434         return 0;
 435 }