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         isl_int_clear(v);
 241 }
 242
 243 void test_application_case(struct isl_ctx *ctx, const char *name)
 244 {
 245         char filename[PATH_MAX];
 246         FILE *input;
 247         int n;
 248         struct isl_basic_set *bset1, *bset2;
 249         struct isl_basic_map *bmap;
 250
 251         n = snprintf(filename, sizeof(filename),
 252                         "%s/test_inputs/%s.omega", srcdir, name);
 253         assert(n < sizeof(filename));
 254         input = fopen(filename, "r");
 255         assert(input);
 256
 257         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
 258         bmap = isl_basic_map_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
 259
 260         bset1 = isl_basic_set_apply(bset1, bmap);
 261
 262         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
 263
 264         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 265
 266         isl_basic_set_free(bset1);
 267         isl_basic_set_free(bset2);
 268
 269         fclose(input);
 270 }
 271
 272 void test_application(struct isl_ctx *ctx)
 273 {
 274         test_application_case(ctx, "application");
 275         test_application_case(ctx, "application2");
 276 }
 277
 278 void test_affine_hull_case(struct isl_ctx *ctx, const char *name)
 279 {
 280         char filename[PATH_MAX];
 281         FILE *input;
 282         int n;
 283         struct isl_basic_set *bset1, *bset2;
 284
 285         n = snprintf(filename, sizeof(filename),
 286                         "%s/test_inputs/%s.polylib", srcdir, name);
 287         assert(n < sizeof(filename));
 288         input = fopen(filename, "r");
 289         assert(input);
 290
 291         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 292         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 293
 294         bset1 = isl_basic_set_affine_hull(bset1);
 295
 296         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 297
 298         isl_basic_set_free(bset1);
 299         isl_basic_set_free(bset2);
 300
 301         fclose(input);
 302 }
 303
 304 void test_affine_hull(struct isl_ctx *ctx)
 305 {
 306         test_affine_hull_case(ctx, "affine2");
 307         test_affine_hull_case(ctx, "affine");
 308 }
 309
 310 void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
 311 {
 312         char filename[PATH_MAX];
 313         FILE *input;
 314         int n;
 315         struct isl_basic_set *bset1, *bset2;
 316         struct isl_set *set;
 317
 318         n = snprintf(filename, sizeof(filename),
 319                         "%s/test_inputs/%s.polylib", srcdir, name);
 320         assert(n < sizeof(filename));
 321         input = fopen(filename, "r");
 322         assert(input);
 323
 324         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 325         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 326
 327         set = isl_basic_set_union(bset1, bset2);
 328         bset1 = isl_set_convex_hull(set);
 329
 330         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 331
 332         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 333
 334         isl_basic_set_free(bset1);
 335         isl_basic_set_free(bset2);
 336
 337         fclose(input);
 338 }
 339
 340 void test_convex_hull(struct isl_ctx *ctx)
 341 {
 342         test_convex_hull_case(ctx, "convex0");
 343         test_convex_hull_case(ctx, "convex1");
 344         test_convex_hull_case(ctx, "convex2");
 345         test_convex_hull_case(ctx, "convex3");
 346         test_convex_hull_case(ctx, "convex4");
 347         test_convex_hull_case(ctx, "convex5");
 348         test_convex_hull_case(ctx, "convex6");
 349         test_convex_hull_case(ctx, "convex7");
 350         test_convex_hull_case(ctx, "convex8");
 351         test_convex_hull_case(ctx, "convex9");
 352         test_convex_hull_case(ctx, "convex10");
 353         test_convex_hull_case(ctx, "convex11");
 354 }
 355
 356 void test_gist_case(struct isl_ctx *ctx, const char *name)
 357 {
 358         char filename[PATH_MAX];
 359         FILE *input;
 360         int n;
 361         struct isl_basic_set *bset1, *bset2;
 362         struct isl_set *set;
 363
 364         n = snprintf(filename, sizeof(filename),
 365                         "%s/test_inputs/%s.polylib", srcdir, name);
 366         assert(n < sizeof(filename));
 367         input = fopen(filename, "r");
 368         assert(input);
 369
 370         bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 371         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 372
 373         bset1 = isl_basic_set_gist(bset1, bset2);
 374
 375         bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
 376
 377         assert(isl_basic_set_is_equal(bset1, bset2) == 1);
 378
 379         isl_basic_set_free(bset1);
 380         isl_basic_set_free(bset2);
 381
 382         fclose(input);
 383 }
 384
 385 void test_gist(struct isl_ctx *ctx)
 386 {
 387         test_gist_case(ctx, "gist1");
 388 }
 389
 390 int main()
 391 {
 392         struct isl_ctx *ctx;
 393
 394         srcdir = getenv("srcdir");
 395
 396         ctx = isl_ctx_alloc();
 397         test_read(ctx);
 398         test_construction(ctx);
 399         test_div(ctx);
 400         test_application(ctx);
 401         test_affine_hull(ctx);
 402         test_convex_hull(ctx);
 403         test_gist(ctx);
 404         isl_ctx_free(ctx);
 405         return 0;
 406 }