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