isl_output.c

   1 /*
   2  * Copyright 2008-2009 Katholieke Universiteit Leuven
   3  * Copyright 2010      INRIA Saclay
   4  *
   5  * Use of this software is governed by the GNU LGPLv2.1 license
   6  *
   7  * Written by Sven Verdoolaege, K.U.Leuven, Departement
   8  * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
   9  * and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,
  10  * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France
  11  */
  12
  13 #include <string.h>
  14 #include <isl_set.h>
  15 #include <isl_seq.h>
  16
  17 static void print_constraint_polylib(struct isl_basic_map *bmap,
  18         int ineq, int n,
  19         FILE *out, int indent, const char *prefix, const char *suffix)
  20 {
  21         int i;
  22         unsigned n_in = isl_basic_map_dim(bmap, isl_dim_in);
  23         unsigned n_out = isl_basic_map_dim(bmap, isl_dim_out);
  24         unsigned nparam = isl_basic_map_dim(bmap, isl_dim_param);
  25         isl_int *c = ineq ? bmap->ineq[n] : bmap->eq[n];
  26
  27         fprintf(out, "%*s%s", indent, "", prefix ? prefix : "");
  28         fprintf(out, "%d", ineq);
  29         for (i = 0; i < n_out; ++i) {
  30                 fprintf(out, " ");
  31                 isl_int_print(out, c[1+nparam+n_in+i], 5);
  32         }
  33         for (i = 0; i < n_in; ++i) {
  34                 fprintf(out, " ");
  35                 isl_int_print(out, c[1+nparam+i], 5);
  36         }
  37         for (i = 0; i < bmap->n_div; ++i) {
  38                 fprintf(out, " ");
  39                 isl_int_print(out, c[1+nparam+n_in+n_out+i], 5);
  40         }
  41         for (i = 0; i < nparam; ++i) {
  42                 fprintf(out, " ");
  43                 isl_int_print(out, c[1+i], 5);
  44         }
  45         fprintf(out, " ");
  46         isl_int_print(out, c[0], 5);
  47         fprintf(out, "%s\n", suffix ? suffix : "");
  48 }
  49
  50 static void print_constraints_polylib(struct isl_basic_map *bmap,
  51         FILE *out, int indent, const char *prefix, const char *suffix)
  52 {
  53         int i;
  54
  55         for (i = 0; i < bmap->n_eq; ++i)
  56                 print_constraint_polylib(bmap, 0, i, out,
  57                                         indent, prefix, suffix);
  58         for (i = 0; i < bmap->n_ineq; ++i)
  59                 print_constraint_polylib(bmap, 1, i, out,
  60                                         indent, prefix, suffix);
  61 }
  62
  63 static void bset_print_constraints_polylib(struct isl_basic_set *bset,
  64         FILE *out, int indent, const char *prefix, const char *suffix)
  65 {
  66         print_constraints_polylib((struct isl_basic_map *)bset,
  67                                  out, indent, prefix, suffix);
  68 }
  69
  70 static void isl_basic_map_print_polylib(struct isl_basic_map *bmap, FILE *out,
  71         int indent, const char *prefix, const char *suffix)
  72 {
  73         unsigned total = isl_basic_map_total_dim(bmap);
  74         fprintf(out, "%*s%s", indent, "", prefix ? prefix : "");
  75         fprintf(out, "%d %d", bmap->n_eq + bmap->n_ineq, 1 + total + 1);
  76         fprintf(out, "%s\n", suffix ? suffix : "");
  77         print_constraints_polylib(bmap, out, indent, prefix, suffix);
  78 }
  79
  80 static void isl_basic_set_print_polylib(struct isl_basic_set *bset, FILE *out,
  81         int indent, const char *prefix, const char *suffix)
  82 {
  83         isl_basic_map_print_polylib((struct isl_basic_map *)bset, out,
  84                                         indent, prefix, suffix);
  85 }
  86
  87 static void isl_map_print_polylib(struct isl_map *map, FILE *out, int indent)
  88 {
  89         int i;
  90
  91         fprintf(out, "%*s", indent, "");
  92         fprintf(out, "%d\n", map->n);
  93         for (i = 0; i < map->n; ++i) {
  94                 fprintf(out, "\n");
  95                 isl_basic_map_print_polylib(map->p[i], out, indent, NULL, NULL);
  96         }
  97 }
  98
  99 static void isl_set_print_polylib(struct isl_set *set, FILE *out, int indent)
 100 {
 101         isl_map_print_polylib((struct isl_map *)set, out, indent);
 102 }
 103
 104 static int count_same_name(__isl_keep isl_dim *dim,
 105         enum isl_dim_type type, unsigned pos, const char *name)
 106 {
 107         enum isl_dim_type t;
 108         unsigned p, s;
 109         int count = 0;
 110
 111         for (t = isl_dim_param; t <= type && t <= isl_dim_out; ++t) {
 112                 s = t == type ? pos : isl_dim_size(dim, t);
 113                 for (p = 0; p < s; ++p) {
 114                         const char *n = isl_dim_get_name(dim, t, p);
 115                         if (n && !strcmp(n, name))
 116                                 count++;
 117                 }
 118         }
 119         return count;
 120 }
 121
 122 static void print_name(struct isl_dim *dim, FILE *out,
 123         enum isl_dim_type type, unsigned pos, int set)
 124 {
 125         const char *name;
 126         char buffer[20];
 127         int primes;
 128
 129         name = type == isl_dim_div ? NULL : isl_dim_get_name(dim, type, pos);
 130
 131         if (!name) {
 132                 const char *prefix;
 133                 if (type == isl_dim_param)
 134                         prefix = "p";
 135                 else if (type == isl_dim_div)
 136                         prefix = "e";
 137                 else if (set || type == isl_dim_in)
 138                         prefix = "i";
 139                 else
 140                         prefix = "o";
 141                 snprintf(buffer, sizeof(buffer), "%s%d", prefix, pos);
 142                 name = buffer;
 143         }
 144         primes = count_same_name(dim, name == buffer ? isl_dim_div : type,
 145                                  pos, name);
 146         fprintf(out, "%s", name);
 147         while (primes-- > 0)
 148                 fputc('\'', out);
 149 }
 150
 151 static void print_var_list(struct isl_dim *dim, FILE *out,
 152         enum isl_dim_type type, int set)
 153 {
 154         int i;
 155
 156         for (i = 0; i < isl_dim_size(dim, type); ++i) {
 157                 if (i)
 158                         fprintf(out, ", ");
 159                 print_name(dim, out, type, i, set);
 160         }
 161 }
 162
 163 static void print_tuple(__isl_keep isl_dim *dim, FILE *out,
 164         enum isl_dim_type type, int set)
 165 {
 166         fprintf(out, "[");
 167         print_var_list(dim, out, type, set);
 168         fprintf(out, "]");
 169 }
 170
 171 static void print_omega_parameters(struct isl_dim *dim, FILE *out,
 172         int indent, const char *prefix, const char *suffix)
 173 {
 174         if (isl_dim_size(dim, isl_dim_param) == 0)
 175                 return;
 176
 177         fprintf(out, "%*s%ssymbolic ", indent, "", prefix ? prefix : "");
 178         print_var_list(dim, out, isl_dim_param, 0);
 179         fprintf(out, ";%s\n", suffix ? suffix : "");
 180 }
 181
 182 static void print_term(__isl_keep isl_dim *dim,
 183                         isl_int c, int pos, FILE *out, int set)
 184 {
 185         enum isl_dim_type type;
 186         unsigned n_in = isl_dim_size(dim, isl_dim_in);
 187         unsigned n_out = isl_dim_size(dim, isl_dim_out);
 188         unsigned nparam = isl_dim_size(dim, isl_dim_param);
 189
 190         if (pos == 0) {
 191                 isl_int_print(out, c, 0);
 192                 return;
 193         }
 194
 195         if (isl_int_is_one(c))
 196                 ;
 197         else if (isl_int_is_negone(c))
 198                 fprintf(out, "-");
 199         else
 200                 isl_int_print(out, c, 0);
 201         if (pos < 1 + nparam) {
 202                 type = isl_dim_param;
 203                 pos -= 1;
 204         } else if (pos < 1 + nparam + n_in) {
 205                 type = isl_dim_in;
 206                 pos -= 1 + nparam;
 207         } else if (pos < 1 + nparam + n_in + n_out) {
 208                 type = isl_dim_out;
 209                 pos -= 1 + nparam + n_in;
 210         } else {
 211                 type = isl_dim_div;
 212                 pos -= 1 + nparam + n_in + n_out;
 213         }
 214         print_name(dim, out, type, pos, set);
 215 }
 216
 217 static void print_affine(__isl_keep isl_basic_map *bmap,
 218         __isl_keep isl_dim *dim, FILE *out, isl_int *c, int set)
 219 {
 220         int i;
 221         int first;
 222         unsigned len = 1 + isl_basic_map_total_dim(bmap);
 223
 224         for (i = 0, first = 1; i < len; ++i) {
 225                 int flip = 0;
 226                 if (isl_int_is_zero(c[i]))
 227                         continue;
 228                 if (!first) {
 229                         if (isl_int_is_neg(c[i])) {
 230                                 flip = 1;
 231                                 isl_int_neg(c[i], c[i]);
 232                                 fprintf(out, " - ");
 233                         } else
 234                                 fprintf(out, " + ");
 235                 }
 236                 first = 0;
 237                 print_term(dim, c[i], i, out, set);
 238                 if (flip)
 239                         isl_int_neg(c[i], c[i]);
 240         }
 241         if (first)
 242                 fprintf(out, "0");
 243 }
 244
 245 static void print_constraint(struct isl_basic_map *bmap,
 246         __isl_keep isl_dim *dim, FILE *out,
 247         isl_int *c, int last, const char *op, int first_constraint, int set)
 248 {
 249         if (!first_constraint)
 250                 fprintf(out, " and ");
 251
 252         isl_int_abs(c[last], c[last]);
 253
 254         print_term(dim, c[last], last, out, set);
 255
 256         fprintf(out, " %s ", op);
 257
 258         isl_int_set_si(c[last], 0);
 259         print_affine(bmap, dim, out, c, set);
 260 }
 261
 262 static void print_constraints(__isl_keep isl_basic_map *bmap,
 263         __isl_keep isl_dim *dim, FILE *out, int set)
 264 {
 265         int i;
 266         struct isl_vec *c;
 267         unsigned total = isl_basic_map_total_dim(bmap);
 268
 269         c = isl_vec_alloc(bmap->ctx, 1 + total);
 270         if (!c)
 271                 return;
 272
 273         for (i = bmap->n_eq - 1; i >= 0; --i) {
 274                 int l = isl_seq_last_non_zero(bmap->eq[i], 1 + total);
 275                 isl_assert(bmap->ctx, l >= 0, return);
 276                 if (isl_int_is_neg(bmap->eq[i][l]))
 277                         isl_seq_cpy(c->el, bmap->eq[i], 1 + total);
 278                 else
 279                         isl_seq_neg(c->el, bmap->eq[i], 1 + total);
 280                 print_constraint(bmap, dim, out, c->el, l,
 281                                     "=", i == bmap->n_eq - 1, set);
 282         }
 283         for (i = 0; i < bmap->n_ineq; ++i) {
 284                 int l = isl_seq_last_non_zero(bmap->ineq[i], 1 + total);
 285                 int s;
 286                 isl_assert(bmap->ctx, l >= 0, return);
 287                 s = isl_int_sgn(bmap->ineq[i][l]);
 288                 if (s < 0)
 289                         isl_seq_cpy(c->el, bmap->ineq[i], 1 + total);
 290                 else
 291                         isl_seq_neg(c->el, bmap->ineq[i], 1 + total);
 292                 print_constraint(bmap, dim, out, c->el, l,
 293                                     s < 0 ? "<=" : ">=", !bmap->n_eq && !i, set);
 294         }
 295
 296         isl_vec_free(c);
 297 }
 298
 299 static void print_omega_constraints(__isl_keep isl_basic_map *bmap, FILE *out,
 300         int set)
 301 {
 302         if (bmap->n_eq + bmap->n_ineq == 0)
 303                 return;
 304
 305         fprintf(out, ": ");
 306         if (bmap->n_div > 0) {
 307                 int i;
 308                 fprintf(out, "exists (");
 309                 for (i = 0; i < bmap->n_div; ++i) {
 310                         if (i)
 311                                 fprintf(out, ", ");
 312                         print_name(bmap->dim, out, isl_dim_div, i, 0);
 313                 }
 314                 fprintf(out, ": ");
 315         }
 316         print_constraints(bmap, bmap->dim, out, set);
 317         if (bmap->n_div > 0)
 318                 fprintf(out, ")");
 319 }
 320
 321 static void basic_map_print_omega(struct isl_basic_map *bmap, FILE *out)
 322 {
 323         fprintf(out, "{ [");
 324         print_var_list(bmap->dim, out, isl_dim_in, 0);
 325         fprintf(out, "] -> [");
 326         print_var_list(bmap->dim, out, isl_dim_out, 0);
 327         fprintf(out, "] ");
 328         print_omega_constraints(bmap, out, 0);
 329         fprintf(out, " }");
 330 }
 331
 332 static void isl_basic_map_print_omega(struct isl_basic_map *bmap, FILE *out,
 333         int indent, const char *prefix, const char *suffix)
 334 {
 335         print_omega_parameters(bmap->dim, out, indent, prefix, suffix);
 336
 337         fprintf(out, "%*s%s", indent, "", prefix ? prefix : "");
 338         basic_map_print_omega(bmap, out);
 339         fprintf(out, "%s\n", suffix ? suffix : "");
 340 }
 341
 342 static void basic_set_print_omega(struct isl_basic_set *bset, FILE *out)
 343 {
 344         fprintf(out, "{ [");
 345         print_var_list(bset->dim, out, isl_dim_set, 1);
 346         fprintf(out, "] ");
 347         print_omega_constraints((isl_basic_map *)bset, out, 1);
 348         fprintf(out, " }");
 349 }
 350
 351 static void isl_basic_set_print_omega(struct isl_basic_set *bset, FILE *out,
 352         int indent, const char *prefix, const char *suffix)
 353 {
 354         print_omega_parameters(bset->dim, out, indent, prefix, suffix);
 355
 356         fprintf(out, "%*s%s", indent, "", prefix ? prefix : "");
 357         basic_set_print_omega(bset, out);
 358         fprintf(out, "%s\n", suffix ? suffix : "");
 359 }
 360
 361 static void isl_map_print_omega(struct isl_map *map, FILE *out, int indent)
 362 {
 363         int i;
 364
 365         print_omega_parameters(map->dim, out, indent, "", "");
 366
 367         fprintf(out, "%*s", indent, "");
 368         for (i = 0; i < map->n; ++i) {
 369                 if (i)
 370                         fprintf(out, " union ");
 371                 basic_map_print_omega(map->p[i], out);
 372         }
 373         fprintf(out, "\n");
 374 }
 375
 376 static void isl_set_print_omega(struct isl_set *set, FILE *out, int indent)
 377 {
 378         int i;
 379
 380         print_omega_parameters(set->dim, out, indent, "", "");
 381
 382         fprintf(out, "%*s", indent, "");
 383         for (i = 0; i < set->n; ++i) {
 384                 if (i)
 385                         fprintf(out, " union ");
 386                 basic_set_print_omega(set->p[i], out);
 387         }
 388         fprintf(out, "\n");
 389 }
 390
 391 static void print_disjunct(__isl_keep isl_basic_map *bmap,
 392         __isl_keep isl_dim *dim, FILE *out, int set)
 393 {
 394         if (bmap->n_div > 0) {
 395                 int i;
 396                 fprintf(out, "exists (");
 397                 for (i = 0; i < bmap->n_div; ++i) {
 398                         if (i)
 399                                 fprintf(out, ", ");
 400                         print_name(dim, out, isl_dim_div, i, 0);
 401                         if (isl_int_is_zero(bmap->div[i][0]))
 402                                 continue;
 403                         fprintf(out, " = [(");
 404                         print_affine(bmap, dim, out, bmap->div[i] + 1, set);
 405                         fprintf(out, ")/");
 406                         isl_int_print(out, bmap->div[i][0], 0);
 407                         fprintf(out, "]");
 408                 }
 409                 fprintf(out, ": ");
 410         }
 411
 412         print_constraints(bmap, dim, out, set);
 413
 414         if (bmap->n_div > 0)
 415                 fprintf(out, ")");
 416 }
 417
 418 static void isl_basic_map_print_isl(__isl_keep isl_basic_map *bmap, FILE *out,
 419         int indent, const char *prefix, const char *suffix)
 420 {
 421         int i;
 422
 423         fprintf(out, "%*s%s", indent, "", prefix ? prefix : "");
 424         if (isl_basic_map_dim(bmap, isl_dim_param) > 0) {
 425                 print_tuple(bmap->dim, out, isl_dim_param, 0);
 426                 fprintf(out, " -> ");
 427         }
 428         fprintf(out, "{ ");
 429         print_tuple(bmap->dim, out, isl_dim_in, 0);
 430         fprintf(out, " -> ");
 431         print_tuple(bmap->dim, out, isl_dim_out, 0);
 432         fprintf(out, " : ");
 433         print_disjunct(bmap, bmap->dim, out, 0);
 434         fprintf(out, " }%s\n", suffix ? suffix : "");
 435 }
 436
 437 static void isl_basic_set_print_isl(__isl_keep isl_basic_set *bset, FILE *out,
 438         int indent, const char *prefix, const char *suffix)
 439 {
 440         int i;
 441
 442         fprintf(out, "%*s%s", indent, "", prefix ? prefix : "");
 443         if (isl_basic_set_dim(bset, isl_dim_param) > 0) {
 444                 print_tuple(bset->dim, out, isl_dim_param, 0);
 445                 fprintf(out, " -> ");
 446         }
 447         fprintf(out, "{ ");
 448         print_tuple(bset->dim, out, isl_dim_set, 1);
 449         fprintf(out, " : ");
 450         print_disjunct((isl_basic_map *)bset, bset->dim, out, 1);
 451         fprintf(out, " }%s\n", suffix ? suffix : "");
 452 }
 453
 454 static void print_disjuncts(__isl_keep isl_map *map, FILE *out, int set)
 455 {
 456         int i;
 457
 458         if (isl_map_fast_is_universe(map))
 459                 return;
 460
 461         fprintf(out, " : ");
 462         if (map->n == 0)
 463                 fprintf(out, "1 = 0");
 464         for (i = 0; i < map->n; ++i) {
 465                 if (i)
 466                         fprintf(out, " or ");
 467                 if (map->n > 1 && map->p[i]->n_eq + map->p[i]->n_ineq > 1)
 468                         fprintf(out, "(");
 469                 print_disjunct(map->p[i], map->dim, out, set);
 470                 if (map->n > 1 && map->p[i]->n_eq + map->p[i]->n_ineq > 1)
 471                         fprintf(out, ")");
 472         }
 473 }
 474
 475 static void isl_map_print_isl(__isl_keep isl_map *map, FILE *out, int indent)
 476 {
 477         fprintf(out, "%*s", indent, "");
 478         if (isl_map_dim(map, isl_dim_param) > 0) {
 479                 print_tuple(map->dim, out, isl_dim_param, 0);
 480                 fprintf(out, " -> ");
 481         }
 482         fprintf(out, "{ ");
 483         print_tuple(map->dim, out, isl_dim_in, 0);
 484         fprintf(out, " -> ");
 485         print_tuple(map->dim, out, isl_dim_out, 0);
 486         print_disjuncts(map, out, 0);
 487         fprintf(out, " }\n");
 488 }
 489
 490 static void isl_set_print_isl(__isl_keep isl_set *set, FILE *out, int indent)
 491 {
 492         int i;
 493
 494         fprintf(out, "%*s", indent, "");
 495         if (isl_set_dim(set, isl_dim_param) > 0) {
 496                 print_tuple(set->dim, out, isl_dim_param, 0);
 497                 fprintf(out, " -> ");
 498         }
 499         fprintf(out, "{ ");
 500         print_tuple(set->dim, out, isl_dim_set, 1);
 501         print_disjuncts((isl_map *)set, out, 1);
 502         fprintf(out, " }\n");
 503 }
 504
 505 void isl_basic_map_print(__isl_keep isl_basic_map *bmap, FILE *out, int indent,
 506         const char *prefix, const char *suffix, unsigned output_format)
 507 {
 508         if (!bmap)
 509                 return;
 510         if (output_format == ISL_FORMAT_ISL)
 511                 isl_basic_map_print_isl(bmap, out, indent, prefix, suffix);
 512         else if (output_format == ISL_FORMAT_OMEGA)
 513                 isl_basic_map_print_omega(bmap, out, indent, prefix, suffix);
 514         else
 515                 isl_assert(bmap->ctx, 0, return);
 516 }
 517
 518 void isl_basic_set_print(struct isl_basic_set *bset, FILE *out, int indent,
 519         const char *prefix, const char *suffix, unsigned output_format)
 520 {
 521         if (!bset)
 522                 return;
 523         if (output_format == ISL_FORMAT_ISL)
 524                 isl_basic_set_print_isl(bset, out, indent, prefix, suffix);
 525         else if (output_format == ISL_FORMAT_POLYLIB)
 526                 isl_basic_set_print_polylib(bset, out, indent, prefix, suffix);
 527         else if (output_format == ISL_FORMAT_POLYLIB_CONSTRAINTS)
 528                 bset_print_constraints_polylib(bset, out, indent, prefix, suffix);
 529         else if (output_format == ISL_FORMAT_OMEGA)
 530                 isl_basic_set_print_omega(bset, out, indent, prefix, suffix);
 531         else
 532                 isl_assert(bset->ctx, 0, return);
 533 }
 534
 535 void isl_set_print(struct isl_set *set, FILE *out, int indent,
 536         unsigned output_format)
 537 {
 538         if (!set)
 539                 return;
 540         if (output_format == ISL_FORMAT_ISL)
 541                 isl_set_print_isl(set, out, indent);
 542         else if (output_format == ISL_FORMAT_POLYLIB)
 543                 isl_set_print_polylib(set, out, indent);
 544         else if (output_format == ISL_FORMAT_OMEGA)
 545                 isl_set_print_omega(set, out, indent);
 546         else
 547                 isl_assert(set->ctx, 0, return);
 548 }
 549
 550 void isl_map_print(__isl_keep isl_map *map, FILE *out, int indent,
 551         unsigned output_format)
 552 {
 553         if (!map)
 554                 return;
 555         if (output_format == ISL_FORMAT_ISL)
 556                 isl_map_print_isl(map, out, indent);
 557         else if (output_format == ISL_FORMAT_POLYLIB)
 558                 isl_map_print_polylib(map, out, indent);
 559         else if (output_format == ISL_FORMAT_OMEGA)
 560                 isl_map_print_omega(map, out, indent);
 561         else
 562                 isl_assert(map->ctx, 0, return);
 563 }