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