eqv2.cc

   1 #include <stdio.h>
   2 #include <stdlib.h>
   3 #include <string.h>
   4 #include <algorithm>
   5 #include <map>
   6 #include <set>
   7 #include <string>
   8 #include <sstream>
   9 #include <vaucanson/int_boolean_automaton.hh>
  10
  11 #include <isa/yaml.h>
  12 #include <isa/pdg.h>
  13 #include "dependence_graph.h"
  14 #include "eqv2_options.h"
  15 #include "msa.h"
  16
  17 #include "config.h"
  18
  19 #include <isl/ctx.h>
  20 #include <isl/val.h>
  21 #include <isl/local_space.h>
  22 #include <isl/set.h>
  23 #include <isl/map.h>
  24 #include <isl/constraint.h>
  25
  26 #ifdef HAVE_OMEGA_PLUS
  27 #include <omega.h>
  28
  29 using namespace omega;
  30
  31 typedef std::vector<Variable_ID> varvector;
  32 typedef std::vector<Global_Var_Decl *> globalvector;
  33
  34 static void create_globals(globalvector &globals, __isl_keep isl_space *dim)
  35 {
  36         unsigned nparam = isl_space_dim(dim, isl_dim_param);
  37         for (int i = 0; i < nparam; ++i) {
  38                 const char *name;
  39                 name = isl_space_get_dim_name(dim, isl_dim_param, i);
  40                 globals.push_back(new Global_Var_Decl(name));
  41         }
  42 }
  43
  44 struct map2rel_data {
  45         varvector in;
  46         varvector out;
  47         varvector params;
  48         varvector exists;
  49
  50         F_And *base;
  51 };
  52
  53 static isl_stat add_constraint(__isl_take isl_constraint *c, void *user)
  54 {
  55         struct map2rel_data *data = (struct map2rel_data *) user;
  56         Constraint_Handle h;
  57         isl_val *v;
  58
  59         if (isl_constraint_is_equality(c))
  60                 h = data->base->add_EQ();
  61         else
  62                 h = data->base->add_GEQ();
  63
  64         for (int i = 0; i < data->in.size(); ++i) {
  65                 v = isl_constraint_get_coefficient_val(c, isl_dim_in, i);
  66                 h.update_coef(data->in[i], isl_val_get_num_si(v));
  67                 isl_val_free(v);
  68         }
  69         for (int i = 0; i < data->out.size(); ++i) {
  70                 v = isl_constraint_get_coefficient_val(c, isl_dim_out, i);
  71                 h.update_coef(data->out[i], isl_val_get_num_si(v));
  72                 isl_val_free(v);
  73         }
  74         for (int i = 0; i < data->params.size(); ++i) {
  75                 v = isl_constraint_get_coefficient_val(c, isl_dim_param, i);
  76                 h.update_coef(data->params[i], isl_val_get_num_si(v));
  77                 isl_val_free(v);
  78         }
  79         for (int i = 0; i < data->exists.size(); ++i) {
  80                 v = isl_constraint_get_coefficient_val(c, isl_dim_div, i);
  81                 h.update_coef(data->exists[i], isl_val_get_num_si(v));
  82                 isl_val_free(v);
  83         }
  84         v = isl_constraint_get_constant_val(c);
  85         h.update_const(isl_val_get_num_si(v));
  86         isl_val_free(v);
  87
  88         isl_constraint_free(c);
  89
  90         return isl_stat_ok;
  91 }
  92
  93 static Relation basic_map2relation(isl_basic_map *bmap,
  94         const Variable_ID_Tuple *globals)
  95 {
  96         struct map2rel_data data;
  97
  98         Relation r(isl_basic_map_dim(bmap, isl_dim_in),
  99                    isl_basic_map_dim(bmap, isl_dim_out));
 100         F_Exists *e = r.add_exists();
 101         data.base = e->add_and();
 102
 103         for (int j = 1; j <= r.n_inp(); ++j)
 104                 data.in.push_back(r.input_var(j));
 105         for (int j = 1; j <= r.n_out(); ++j)
 106                 data.out.push_back(r.output_var(j));
 107         for (int i = 0; i < isl_basic_map_dim(bmap, isl_dim_div); ++i)
 108                 data.exists.push_back(e->declare());
 109         for (int i = 0; i < globals->size(); ++i)
 110                 data.params.push_back(r.get_local((*globals)[i+1]));
 111
 112         isl_basic_map_foreach_constraint(bmap, &add_constraint, &data);
 113
 114         r.finalize();
 115         return r;
 116 }
 117
 118 static isl_stat bm2r(__isl_take isl_basic_map *bmap, void *user)
 119 {
 120         Relation *r = (Relation *)user;
 121
 122         *r = Union(*r, basic_map2relation(bmap, r->global_decls()));
 123
 124         isl_basic_map_free(bmap);
 125
 126         return isl_stat_ok;
 127 }
 128
 129 static Relation map2relation(__isl_keep isl_map *map,
 130         const globalvector &globals)
 131 {
 132         Relation r(isl_map_dim(map, isl_dim_in), isl_map_dim(map, isl_dim_out));
 133         for (int i = 0; i < globals.size(); ++i)
 134                 r.get_local(globals[i]);
 135         r.add_or();
 136         r.finalize();
 137
 138         isl_map_foreach_basic_map(map, &bm2r, &r);
 139
 140         return r;
 141 }
 142
 143 static void max_index(Constraint_Handle c, varvector& vv, varvector& params)
 144 {
 145         for (Constr_Vars_Iter cvi(c); cvi; ++cvi) {
 146                 Variable_ID var = (*cvi).var;
 147                 if (find(vv.begin(), vv.end(), var) == vv.end() &&
 148                     find(params.begin(), params.end(), var) == params.end())
 149                         vv.push_back(var);
 150         }
 151 }
 152
 153 static __isl_give isl_constraint *set_constraint(__isl_take isl_constraint *c,
 154         Constraint_Handle h, varvector &vv, varvector &params)
 155 {
 156         int v;
 157
 158         for (int i = 0; i < vv.size(); ++i) {
 159                 v = h.get_coef(vv[i]);
 160                 c = isl_constraint_set_coefficient_si(c, isl_dim_set, i, v);
 161         }
 162         for (int i = 0; i < params.size(); ++i) {
 163                 v = h.get_coef(params[i]);
 164                 c = isl_constraint_set_coefficient_si(c, isl_dim_param, i, v);
 165         }
 166         v = h.get_const();
 167         c = isl_constraint_set_constant_si(c, v);
 168
 169         return c;
 170 }
 171
 172 static isl_basic_set *disjunct2basic_set(DNF_Iterator &di, isl_space *dim,
 173                                             varvector &vv, varvector &params)
 174 {
 175         int d = vv.size();
 176         isl_constraint *c;
 177         isl_basic_set *bset;
 178         isl_local_space *ls;
 179
 180         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
 181                 max_index((*ei), vv, params);
 182         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
 183                 max_index((*gi), vv, params);
 184
 185         dim = isl_space_add_dims(dim, isl_dim_set, vv.size() - d);
 186         bset = isl_basic_set_universe(isl_space_copy(dim));
 187         ls = isl_local_space_from_space(dim);
 188
 189         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei) {
 190                 c = isl_constraint_alloc_equality(isl_local_space_copy(ls));
 191                 c = set_constraint(c, (*ei), vv, params);
 192                 bset = isl_basic_set_add_constraint(bset, c);
 193         }
 194         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi) {
 195                 c = isl_constraint_alloc_inequality(isl_local_space_copy(ls));
 196                 c = set_constraint(c, (*gi), vv, params);
 197                 bset = isl_basic_set_add_constraint(bset, c);
 198         }
 199
 200         isl_local_space_free(ls);
 201
 202         bset = isl_basic_set_project_out(bset, isl_dim_set, d, vv.size() - d);
 203         vv.resize(d);
 204
 205         return bset;
 206 }
 207
 208 static __isl_give isl_map *relation2map(__isl_take isl_space *dim, Relation &r)
 209 {
 210         varvector vv;
 211         varvector params;
 212         isl_ctx *ctx;
 213         isl_space *dim_set;
 214         isl_map *map;
 215
 216         for (int j = 1; j <= r.n_inp(); ++j)
 217                 vv.push_back(r.input_var(j));
 218         for (int j = 1; j <= r.n_out(); ++j)
 219                 vv.push_back(r.output_var(j));
 220
 221         const Variable_ID_Tuple *globals = r.global_decls();
 222         for (int i = 0; i < globals->size(); ++i)
 223                 params.push_back(r.get_local((*globals)[i+1]));
 224
 225         ctx = isl_space_get_ctx(dim);
 226         dim_set = isl_space_set_alloc(ctx, params.size(), vv.size());
 227         map = isl_map_empty(isl_space_copy(dim));
 228
 229         for (DNF_Iterator di(r.query_DNF()); di; ++di) {
 230                 isl_basic_set *bset;
 231                 isl_basic_map *bmap;
 232
 233                 bset = disjunct2basic_set(di, isl_space_copy(dim_set), vv, params);
 234                 bmap = isl_basic_map_from_basic_set(bset, isl_space_copy(dim));
 235                 map = isl_map_union(map, isl_map_from_basic_map(bmap));
 236         }
 237
 238         isl_space_free(dim_set);
 239         isl_space_free(dim);
 240
 241         return map;
 242 }
 243
 244 /* Compute transitive closure using Omega+.
 245  * Note that the result computed by Omega also contains the identity
 246  * mapping on the intersection of domain and range, but we will include
 247  * the entire identity mapping later, so this shouldn't be a problem.
 248  */
 249 static __isl_give isl_map *omega_closure(__isl_take isl_map *map)
 250 {
 251         isl_ctx *ctx = isl_map_get_ctx(map);
 252         struct options *options = isl_ctx_peek_eqv2_options(ctx);
 253         isl_space *dim;
 254         globalvector globals;
 255
 256         dim = isl_map_get_space(map);
 257         create_globals(globals, dim);
 258
 259         Relation R = map2relation(map, globals);
 260         isl_map_free(map);
 261
 262         Relation TC;
 263         if (options->try_lower) {
 264                 int exact;
 265                 TC = TransitiveClosure(copy(R));
 266                 Relation test = Composition(copy(TC), copy(R));
 267
 268                 exact = TC.is_exact() &&
 269                         Must_Be_Subset(copy(R), copy(TC)) &&
 270                         Must_Be_Subset(test, copy(TC));
 271                 if (!exact)
 272                         TC = Upper_Bound(ApproxClosure(R));
 273         } else
 274                 TC = Upper_Bound(ApproxClosure(R));
 275
 276         map = relation2map(dim, TC);
 277
 278         return map;
 279 }
 280 #endif
 281
 282 /* Compute transitive closure */
 283 static __isl_give isl_map *closure(__isl_take isl_map *map)
 284 {
 285         isl_ctx *ctx = isl_map_get_ctx(map);
 286         struct options *options = isl_ctx_peek_eqv2_options(ctx);
 287
 288 #ifdef HAVE_OMEGA_PLUS
 289         if (options->omega)
 290                 return omega_closure(map);
 291 #endif
 292
 293         return isl_map_transitive_closure(map, NULL);
 294 }
 295
 296 using namespace vcsn::int_boolean_automaton;
 297 using namespace vcsn;
 298
 299 template <class Exp_, class Dispatch_>
 300 class acc_visitor : public algebra::KRatExpMatcher<
 301       acc_visitor<Exp_, Dispatch_>, Exp_, isl_map *, Dispatch_ >
 302 {
 303 public:
 304         typedef typename Exp_::monoid_elt_value_t       monoid_elt_value_t;
 305         typedef acc_visitor<Exp_, Dispatch_>            this_class;
 306         typedef isl_map *                               return_type;
 307
 308 private:
 309         const MSA &msa;
 310
 311 public:
 312         acc_visitor(const MSA &msa) : msa(msa) {}
 313
 314         INHERIT_CONSTRUCTORS(this_class, Exp_, isl_map *, Dispatch_);
 315
 316         MATCH__(Product, lhs, rhs) {
 317                 return isl_map_apply_range(this->match(lhs), this->match(rhs));
 318         } END
 319
 320         MATCH__(Sum, lhs, rhs) {
 321                 return isl_map_union(this->match(lhs), this->match(rhs));
 322         } END
 323
 324         MATCH_(Star, node) {
 325                 isl_space *dim;
 326                 isl_map *map;
 327                 map = closure(this->match(node));
 328                 dim = isl_map_get_space(map);
 329                 return isl_map_union(map, isl_map_identity(dim));
 330         } END
 331
 332         MATCH__(LeftWeight, w, node) {
 333                 assert(0);
 334                 return 0;
 335         } END
 336
 337         MATCH__(RightWeight, node, w) {
 338                 assert(0);
 339                 return 0;
 340         } END
 341
 342         MATCH_(Constant, m) {
 343                 isl_map *map;
 344                 typename monoid_elt_value_t::const_iterator i = m.begin();
 345                 assert(i != m.end());
 346                 map = isl_map_copy(msa.firing[*i]);
 347                 ++i;
 348                 assert(i == m.end());
 349
 350                 return map;
 351         } END
 352
 353         /* By construction, there should always be a path */
 354         MATCH(Zero) {
 355                 assert(0);
 356                 return 0;
 357         } END
 358
 359         /* There can be no zero-length path */
 360         MATCH(One) {
 361                 assert(0);
 362                 return 0;
 363         } END
 364 };
 365
 366 template<typename Exp>
 367 isl_map *accessibility(const MSA &msa, const Exp &kexp)
 368 {
 369         acc_visitor<Exp, algebra::DispatchFunction<Exp> > m(msa);
 370         return m.match(kexp);
 371 }
 372
 373 static unsigned update_out_dim(pdg::PDG *pdg, unsigned out_dim)
 374 {
 375         for (int i = 0; i < pdg->arrays.size(); ++i) {
 376                 pdg::array *array = pdg->arrays[i];
 377                 if (array->type != pdg::array::output)
 378                         continue;
 379                 if (array->dims.size() + 1 > out_dim)
 380                         out_dim = array->dims.size() + 1;
 381         }
 382
 383         return out_dim;
 384 }
 385
 386 /* The input arrays of the two programs are supposed to be the same,
 387  * so they should at least have the same dimension.  Make sure
 388  * this is true, because we depend on it later on.
 389  */
 390 static int check_input_arrays(dependence_graph *dg1, dependence_graph *dg2)
 391 {
 392         for (int i = 0; i < dg1->input_computations.size(); ++i)
 393                 for (int j = 0; j < dg2->input_computations.size(); ++j) {
 394                         if (strcmp(dg1->input_computations[i]->operation,
 395                                    dg2->input_computations[j]->operation))
 396                                 continue;
 397                         if (dg1->input_computations[i]->dim ==
 398                             dg2->input_computations[j]->dim)
 399                                 continue;
 400                         fprintf(stderr,
 401                             "input arrays \"%s\" do not have the same dimension\n",
 402                             dg1->input_computations[i]->operation);
 403                         return -1;
 404                 }
 405
 406         return 0;
 407 }
 408
 409 /* Compute a map between the domains of the output nodes of
 410  * the dependence graphs that expresses that array1 in dg1
 411  * and array2 in dg2 are equal.
 412  * This map is then returned as a set.
 413  */
 414 static __isl_give isl_set *compute_equal_array(
 415         dependence_graph *dg1, dependence_graph *dg2, int array1, int array2)
 416 {
 417         unsigned n_in;
 418         const char *array_name = dg1->output_arrays[array1];
 419         isl_set *out1 = isl_set_copy(dg1->out->domain);
 420         isl_set *out2 = isl_set_copy(dg2->out->domain);
 421         unsigned dim1 = isl_set_n_dim(out1);
 422         unsigned dim2 = isl_set_n_dim(out2);
 423
 424         out1 = isl_set_fix_dim_si(out1, dim1 - 1, array1);
 425         out2 = isl_set_fix_dim_si(out2, dim2 - 1, array2);
 426         out1 = isl_set_remove_dims(out1, isl_dim_set, dim1 - 1, 1);
 427         out2 = isl_set_remove_dims(out2, isl_dim_set, dim2 - 1, 1);
 428         int equal = isl_set_is_equal(out1, out2);
 429         isl_set_free(out1);
 430         isl_set_free(out2);
 431         assert(equal >= 0);
 432         if (!equal) {
 433                 fprintf(stderr, "different output domains for array %s\n",
 434                                 array_name);
 435                 return NULL;
 436         }
 437
 438         out1 = isl_set_copy(dg1->out->domain);
 439         out2 = isl_set_copy(dg2->out->domain);
 440         out1 = isl_set_fix_dim_si(out1, dim1 - 1, array1);
 441         out2 = isl_set_fix_dim_si(out2, dim2 - 1, array2);
 442         out1 = isl_set_coalesce(out1);
 443         out2 = isl_set_coalesce(out2);
 444         isl_space *dim = isl_space_map_from_set(isl_set_get_space(out2));
 445         isl_map *id = isl_map_identity(dim);
 446         n_in = isl_map_dim(id, isl_dim_in);
 447         id = isl_map_remove_dims(id, isl_dim_in, n_in - 1, 1);
 448         id = isl_map_apply_domain(id, isl_map_copy(id));
 449         id = isl_map_intersect_domain(id, out1);
 450         id = isl_map_intersect_range(id, out2);
 451
 452         return isl_map_wrap(id);
 453 }
 454
 455 /* Compute a map between the domains of the output nodes of
 456  * the dependence graphs that expresses that arrays with
 457  * the same names in both graphs are equal.
 458  * The map is returned as a set.
 459  */
 460 static __isl_give isl_set *compute_equal_output(
 461         dependence_graph *dg1, dependence_graph *dg2)
 462 {
 463         int i1 = 0, i2 = 0;
 464         isl_space *dim;
 465         isl_map *map;
 466         isl_set *equal_output;
 467         unsigned d;
 468
 469         dim = isl_set_get_space(dg1->out->domain);
 470         d = isl_space_dim(dim, isl_dim_set);
 471         map = isl_map_empty(isl_space_map_from_set(dim));
 472         equal_output = isl_map_wrap(map);
 473
 474         while (i1 < dg1->output_arrays.size() || i2 < dg2->output_arrays.size()) {
 475                 int cmp;
 476                 cmp = i1 == dg1->output_arrays.size() ? 1 :
 477                       i2 == dg2->output_arrays.size() ? -1 :
 478                       strcmp(dg1->output_arrays[i1], dg2->output_arrays[i2]);
 479                 if (cmp < 0) {
 480                         fprintf(stdout,
 481                                 "Array \"%s\" only in program 1; not checked\n",
 482                                 dg1->output_arrays[i1]);
 483                         ++i1;
 484                 } else if (cmp > 0) {
 485                         fprintf(stdout,
 486                                 "Array \"%s\" only in program 2; not checked\n",
 487                                 dg2->output_arrays[i2]);
 488                         ++i2;
 489                 } else {
 490                         isl_set *eq_array;
 491                         eq_array = compute_equal_array(dg1, dg2, i1, i2);
 492                         equal_output = isl_set_union(equal_output, eq_array);
 493                         ++i1;
 494                         ++i2;
 495                 }
 496         }
 497
 498         equal_output = isl_set_set_tuple_name(equal_output, "s0");
 499
 500         return equal_output;
 501 }
 502
 503 static int check_equivalence(isl_ctx *ctx,
 504         dependence_graph *dg1, dependence_graph *dg2)
 505 {
 506         int root;
 507         MSA msa;
 508         isl_printer *p;
 509         unsigned d;
 510         int ok = 1;
 511
 512         if (check_input_arrays(dg1, dg2))
 513                 return -1;
 514
 515         p = isl_printer_to_file(ctx, stdout);
 516
 517         root = msa.add(dg1->out, dg2->out);
 518
 519         alphabet_t alpha;
 520         for (int i = 0; i < msa.firing.size(); ++i)
 521                 alpha.insert(i);
 522
 523         automaton_t a = make_automaton(alpha);
 524         std::vector<hstate_t> state;
 525         for (int i = 0; i < msa.state.size(); ++i)
 526                 state.push_back(a.add_state());
 527
 528         for (int i = 0; i < msa.transition.size(); ++i) {
 529                 int s1 = msa.transition[i].first.first;
 530                 int s2 = msa.transition[i].first.second;
 531                 int f = msa.transition[i].second;
 532                 a.add_letter_transition(state[s1], state[s2], f);
 533         }
 534
 535         a.set_initial(state[root]);
 536
 537         isl_set *equal_output;
 538         equal_output = compute_equal_output(dg1, dg2);
 539
 540         for (int i = 0; i < msa.input_state.size(); ++i) {
 541                 isl_map *acc;
 542                 isl_set *set;
 543                 isl_map *map;
 544                 isl_map *id;
 545
 546                 a.set_final(state[msa.input_state[i]]);
 547                 rat_exp_t ratexp = aut_to_exp(a);
 548                 a.clear_final();
 549
 550                 acc = accessibility(msa, ratexp.value());
 551                 set = isl_set_apply(isl_set_copy(equal_output),
 552                                         isl_map_copy(acc));
 553                 map = isl_set_unwrap(set);
 554
 555                 id = isl_map_identity(isl_map_get_space(map));
 556                 map = isl_map_subtract(map, id);
 557
 558                 set = isl_map_wrap(map);
 559                 set = isl_set_set_tuple_name(set,
 560                                     isl_map_get_tuple_name(acc, isl_dim_out));
 561                 set = isl_set_apply(set, isl_map_reverse(acc));
 562                 d = isl_set_dim(set, isl_dim_set) / 2;
 563                 set = isl_set_remove_dims(set, isl_dim_set, d, d);
 564                 if (!isl_set_is_empty(set)) {
 565                         ok = 0;
 566                         isl_printer_print_str(p, "NOT equivalent");
 567                         isl_printer_end_line(p);
 568                         set = isl_set_coalesce(set);
 569                         isl_printer_print_set(p, set);
 570                         isl_printer_end_line(p);
 571                 }
 572
 573                 isl_set_free(set);
 574         }
 575
 576         /* Consider each fail state in turn as the corresponding
 577          * domains may have different dimensions.
 578          */
 579         for (int i = 0; i < msa.fail_state.size(); ++i) {
 580                 isl_map *acc;
 581                 isl_set *set;
 582
 583                 a.set_final(state[msa.fail_state[i]]);
 584                 rat_exp_t ratexp = aut_to_exp(a);
 585                 a.clear_final();
 586
 587                 acc = accessibility(msa, ratexp.value());
 588                 acc = isl_map_intersect_domain(acc, isl_set_copy(equal_output));
 589
 590                 set = isl_map_domain(acc);
 591                 d = isl_set_dim(set, isl_dim_set) / 2;
 592                 set = isl_set_remove_dims(set, isl_dim_set, d, d);
 593                 if (!isl_set_is_empty(set)) {
 594                         ok = 0;
 595                         isl_printer_print_str(p, "NOT equivalent");
 596                         isl_printer_end_line(p);
 597                         set = isl_set_coalesce(set);
 598                         isl_printer_print_set(p, set);
 599                         isl_printer_end_line(p);
 600                 }
 601
 602                 isl_set_free(set);
 603         }
 604
 605         isl_set_free(equal_output);
 606
 607         if (!ok)
 608                 isl_printer_print_str(p, "NOT ");
 609         isl_printer_print_str(p, "OK");
 610         isl_printer_end_line(p);
 611
 612         isl_printer_free(p);
 613
 614         return 0;
 615 }
 616
 617 int main(int argc, char *argv[])
 618 {
 619         struct isl_ctx *ctx;
 620         struct options *options = eqv2_options_new_with_defaults();
 621         isl_set *context = NULL;
 622         dependence_graph *dg[2];
 623
 624         argc = eqv2_options_parse(options, argc, argv, ISL_ARG_ALL);
 625
 626         ctx = isl_ctx_alloc_with_options(&options_args, options);
 627         if (!ctx) {
 628                 fprintf(stderr, "Unable to allocate ctx\n");
 629                 return -1;
 630         }
 631
 632         if (options->context)
 633                 context = isl_set_read_from_str(ctx, options->context);
 634
 635         pdg::PDG *pdg[2];
 636         unsigned out_dim = 0;
 637         for (int i = 0; i < 2; ++i) {
 638                 FILE *in;
 639                 in = fopen(options->program[i], "r");
 640                 if (!in) {
 641                         fprintf(stderr, "Unable to open %s\n", options->program[i]);
 642                         return -1;
 643                 }
 644                 pdg[i] = yaml::Load<pdg::PDG>(in, ctx);
 645                 fclose(in);
 646                 if (!pdg[i]) {
 647                         fprintf(stderr, "Unable to read %s\n", options->program[i]);
 648                         return -1;
 649                 }
 650                 out_dim = update_out_dim(pdg[i], out_dim);
 651
 652                 if (context &&
 653                     pdg[i]->params.size() != isl_set_dim(context, isl_dim_param)) {
 654                         fprintf(stdout,
 655                             "Parameter dimension mismatch; context ignored\n");
 656                         isl_set_free(context);
 657                         context = NULL;
 658                 }
 659         }
 660
 661         for (int i = 0; i < 2; ++i) {
 662                 dg[i] = pdg_to_dg(pdg[i], out_dim, isl_set_copy(context));
 663                 pdg[i]->free();
 664                 delete pdg[i];
 665         }
 666
 667         int res = check_equivalence(ctx, dg[0], dg[1]);
 668
 669         for (int i = 0; i < 2; ++i)
 670                 delete dg[i];
 671         isl_set_free(context);
 672         isl_ctx_free(ctx);
 673
 674         return res;
 675 }