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