modelchecker/coord.c

   1 #include <argp.h>
   2 #include <inttypes.h>
   3 #include <locale.h>
   4 #include <stdio.h>
   5 #include <stdlib.h>
   6 #include <string.h>
   7 #include <sys/time.h>
   8
   9 #ifdef HAVE_PROFILER
  10 #include <gperftools/profiler.h>
  11 #endif
  12
  13 #include <sylvan.h>
  14 #include <llmsset.h>
  15 #include <lace.h>
  16
  17 #include "coord.h"
  18 #include "sokoban.h"
  19
  20 /*
  21  * Global TODOs for now:
  22  * - update the helper maps so it is a single bimap
  23  * - make a data structure for relations
  24  * - encode relations as a set of four relations for each move
  25  */
  26
  27 typedef struct {
  28         int x;
  29         int y;
  30 } xy;
  31
  32 typedef struct {
  33         int var[3];
  34 } bddvar;
  35
  36 typedef struct {
  37         xy key;
  38         bddvar value;
  39         UT_hash_handle hh;
  40 } xy_bddvar_map;
  41
  42 typedef struct {
  43         int key;
  44         xy value;
  45         UT_hash_handle hh;
  46 } bddvar_xy_map;
  47
  48 typedef struct {
  49         xy_bddvar_map *f;
  50         bddvar_xy_map *t;
  51 } bimap;
  52
  53 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
  54 {
  55         xy_bddvar_map k, *r = NULL;
  56         memset(&k, 0, sizeof(xy_bddvar_map));
  57         k.key.x = x;
  58         k.key.y = y;
  59         HASH_FIND(hh, map, &k.key, sizeof(xy), r);
  60         return r;
  61 }
  62
  63 bddvar_xy_map *getbdd(int key, bddvar_xy_map *map)
  64 {
  65         bddvar_xy_map k, *r = NULL;
  66         memset(&k, 0, sizeof(bddvar_xy_map));
  67         k.key = key;
  68         HASH_FIND(hh, map, &k.key, sizeof(int), r);
  69         return r;
  70 }
  71
  72 /*
  73 xy_bddvar_map *create_xy_bddvar_map(sokoban_screen *screen)
  74 {
  75         int varcount = 0;
  76         sokoban_screen *r;
  77         xy_bddvar_map *xybdd = NULL;
  78         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
  79                 xy_bddvar_map *f = NULL;
  80                 //bddvar_xy_map *t = NULL;
  81
  82                 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
  83                 memset(f, 0, sizeof(xy_bddvar_map));
  84                 f->key.x = r->coord.x;
  85                 f->key.y = r->coord.y;
  86                 f->value.var[0] = varcount;
  87                 f->value.var[1] = varcount + 1;
  88                 f->value.var[2] = varcount + 2;
  89                 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
  90                 varcount = varcount + 3;
  91         }
  92         return xybdd;
  93 }
  94
  95 bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen)
  96 {
  97         int varcount = 0;
  98         sokoban_screen *r;
  99         bddvar_xy_map *bddxy = NULL;
 100         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 101                 for (int i = 0; i <3; i++){
 102                         bddvar_xy_map *f = NULL;
 103                         //bddvar_xy_map *t = NULL;
 104
 105                         f = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
 106                         memset(f, 0, sizeof(bddvar_xy_map));
 107                         f->key = varcount + i;
 108                         f->value.x = r->coord.x;
 109                         f->value.y = r->coord.y;
 110                         HASH_ADD(hh, bddxy, key, sizeof(int), f);
 111                 }
 112                 varcount = varcount + 3;
 113         }
 114         return bddxy;
 115 }
 116 */
 117
 118 bimap *create_bimap_helper(sokoban_screen *screen)
 119 {
 120         int varcount = 0;
 121         sokoban_screen *r;
 122         xy_bddvar_map *xybdd = NULL;
 123         bddvar_xy_map *bddxy = NULL;
 124         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 125                 xy_bddvar_map *f = NULL;
 126                 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
 127                 memset(f, 0, sizeof(xy_bddvar_map));
 128                 f->key.x = r->coord.x;
 129                 f->key.y = r->coord.y;
 130                 f->value.var[0] = varcount;
 131                 f->value.var[1] = varcount + 1;
 132                 f->value.var[2] = varcount + 2;
 133                 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
 134
 135                 for (int i = 0; i <3; i++){
 136                         bddvar_xy_map *t = NULL;
 137                         t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
 138                         memset(t, 0, sizeof(bddvar_xy_map));
 139                         t->key = varcount + i;
 140                         t->value.x = r->coord.x;
 141                         t->value.y = r->coord.y;
 142                         HASH_ADD(hh, bddxy, key, sizeof(int), t);
 143                 }
 144                 varcount = varcount + 3;
 145         }
 146         bimap *bm = NULL;
 147         bm = (bimap *)malloc(sizeof(bimap));
 148         bm->f = xybdd;
 149         bm->t = bddxy;
 150         return bm;
 151 }
 152
 153 int check_xy_exists(int x, int y, bimap *bm)
 154 {
 155         int res = 0;
 156         if (getxy(x, y, bm->f) != NULL) res = 1;
 157         return res;
 158 }
 159
 160 int check_space(int x, int y, direction d, int delta, bimap *bm)
 161 {
 162         switch(d){
 163         case LEFT: x = x - delta; break;
 164         case UP: y = y - delta; break;
 165         case RIGHT: x = x + delta; break;
 166         case DOWN: y = y + delta; break;
 167         }
 168         return check_xy_exists(x, y, bm);
 169 }
 170
 171 /*
 172  * Each coordinate has three related boolean variables. The combination of those boolean variables
 173  * defines tiles:
 174  * 000: Wall
 175  * 001: Free
 176  * 010: Box
 177  * 100: Box on target
 178  * 011: Target
 179  * 101: Agent
 180  * 110: Agent on target
 181  * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
 182  * tiles in the shrinked screen.
 183  * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
 184  * directly in transition relations.
 185  */
 186
 187 state *encode_screen(sokoban_screen *screen)
 188 {
 189         LACE_ME;
 190
 191         BDDVAR vars[HASH_COUNT(screen) * 3];
 192         for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
 193                 vars[i] = i * 2;
 194         }
 195
 196         uint8_t st_enc[HASH_COUNT(screen) * 3];
 197
 198         BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
 199         BDD s;
 200         state *fullState = NULL;
 201         fullState = (state *)malloc(sizeof(state));
 202         fullState->vars.varset = varset;
 203         fullState->vars.size = HASH_COUNT(screen) * 3;
 204         int tile_index = 0;
 205         sokoban_screen *r;
 206         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 207                 switch(r->tile){
 208                 case FREE: //001
 209                         st_enc[tile_index] = 0;
 210                         tile_index++;
 211                         st_enc[tile_index] = 0;
 212                         tile_index++;
 213                         st_enc[tile_index] = 1;
 214                         tile_index++;
 215                         break;
 216                 case WALL: //000
 217                         st_enc[tile_index] = 0;
 218                         tile_index++;
 219                         st_enc[tile_index] = 0;
 220                         tile_index++;
 221                         st_enc[tile_index] = 0;
 222                         tile_index++;
 223                         break;
 224                 case BOX: //010
 225                         st_enc[tile_index] = 0;
 226                         tile_index++;
 227                         st_enc[tile_index] = 1;
 228                         tile_index++;
 229                         st_enc[tile_index] = 0;
 230                         tile_index++;
 231                         break;
 232                 case TARGET: //011
 233                         st_enc[tile_index] = 0;
 234                         tile_index++;
 235                         st_enc[tile_index] = 1;
 236                         tile_index++;
 237                         st_enc[tile_index] = 1;
 238                         tile_index++;
 239                         break;
 240                 case AGENT: //101
 241                         st_enc[tile_index] = 1;
 242                         tile_index++;
 243                         st_enc[tile_index] = 0;
 244                         tile_index++;
 245                         st_enc[tile_index] = 1;
 246                         tile_index++;
 247                         break;
 248                 case TARGAGENT: //110
 249                         st_enc[tile_index] = 1;
 250                         tile_index++;
 251                         st_enc[tile_index] = 1;
 252                         tile_index++;
 253                         st_enc[tile_index] = 0;
 254                         tile_index++;
 255                         break;
 256                 case TARGBOX: //100
 257                         st_enc[tile_index] = 1;
 258                         tile_index++;
 259                         st_enc[tile_index] = 0;
 260                         tile_index++;
 261                         st_enc[tile_index] = 0;
 262                         tile_index++;
 263                         break;
 264                 }
 265         }
 266         s = sylvan_cube(varset, st_enc);
 267         fullState->bdd = s;
 268         printf("Initial state encoded\n");
 269         return fullState;
 270 }
 271
 272 int
 273 test_relprod()
 274 {
 275     LACE_ME;
 276
 277     BDDVAR vars[] = {0,2,4};
 278     BDDVAR all_vars[] = {4,5};
 279
 280     BDDSET vars_set = sylvan_set_fromarray(vars, 3);
 281     BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 2);
 282
 283     BDD s, t, next, prev;
 284     BDD zeroes, ones;
 285
 286     // transition relation: 000 --> 111 and !000 --> 000
 287     t = sylvan_false;
 288     //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1,0,1,0,1}));
 289     //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0}));
 290     //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){2,0,1,0,2,0}));
 291     t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0}));
 292
 293     s = sylvan_cube(vars_set, (uint8_t[]){0,0,1});
 294     zeroes = sylvan_cube(vars_set, (uint8_t[]){0,0,0});
 295     ones = sylvan_cube(vars_set, (uint8_t[]){0,0,1});
 296
 297     next = sylvan_relnext(s, t, all_vars_set);
 298     prev = sylvan_relprev(t, next, all_vars_set);
 299     if (next == zeroes) printf("Pass 1\n");
 300     if (prev == ones || prev == zeroes) printf("Pass 2\n");
 301
 302     return 0;
 303 }
 304
 305 BDD create_single_rel(sokoban_screen *screen, direction dir)
 306 {
 307         LACE_ME;
 308         BDD t = sylvan_false;
 309         bimap *bm = create_bimap_helper(screen);
 310         int x = 0;
 311         int y = 0;
 312         bddvar_xy_map *bddxy = NULL;
 313         int xdelta = 0;
 314         int ydelta = 0;
 315         int xgamma = 0;
 316         int ygamma = 0;
 317         switch(dir){
 318         case LEFT:
 319                 xdelta = -1;
 320                 ydelta = 0;
 321                 xgamma = -2;
 322                 ygamma = 0;
 323                 break;
 324         case UP:
 325                 xdelta = 0;
 326                 ydelta = -1;
 327                 xgamma = 0;
 328                 ygamma = -2;
 329                 break;
 330         case RIGHT:
 331                 xdelta = 1;
 332                 ydelta = 0;
 333                 xgamma = 2;
 334                 ygamma = 0;
 335                 break;
 336         case DOWN:
 337                 xdelta = 0;
 338                 ydelta = 1;
 339                 xgamma = 0;
 340                 ygamma = 2;
 341                 break;
 342         }
 343
 344         for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
 345                 bddxy = getbdd(i*3, bm->t);
 346                 x = bddxy->value.x;
 347                 y = bddxy->value.y;
 348                 if (check_space(x, y, dir, 1, bm) == 0){
 349                         sokoban_screen *tmp_scr = get_coord(x, y, screen);
 350                         if (tmp_scr->tile == AGENT){
 351                                 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
 352                                 BDDVAR relvars[6]  = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
 353                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
 354                                 uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
 355                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 356                         }
 357                         if (tmp_scr->tile == TARGAGENT){
 358                                 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
 359                                 BDDVAR relvars[6]  = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
 360                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
 361                                 uint8_t rel_enc[6] = {1, 1, 1, 1, 0, 0};
 362                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 363                         }
 364                 }
 365                 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
 366                         sokoban_screen *tmp_scr = get_coord(x, y, screen);
 367                         sokoban_screen *tmp_scr_d = get_coord(x + xdelta, y + ydelta, screen);
 368                         xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
 369                         int deltai = bddvar->value.var[0];
 370                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
 371                                 //(0 1 0 0 1 1 1 0 0 0 1 1)
 372                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 373                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 374                                 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 375                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 376                         }
 377                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
 378                                 //(0 1 1 0 1 1 1 0 0 1 1 1)
 379                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 380                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 381                                 uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
 382                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 383                         }
 384                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
 385                                 //(0 1 0 1 1 0 1 0 1 0 0 1)
 386                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 387                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 388                                 uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
 389                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 390                         }
 391                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
 392                                 //(0 1 1 1 1 0 1 0 1 1 0 1)
 393                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 394                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 395                                 uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 396                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 397                         }
 398                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX){
 399                                 //(0 0 1 1 0 0 1 1 0 0 1 1)
 400                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 401                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 402                                 uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 403                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 404                         }
 405                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX){
 406                                 //(1 1 0 0 0 0 1 1 0 0 1 1)
 407                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 408                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 409                                 uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
 410                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 411                         }
 412                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX){
 413                                 //(0 0 1 1 0 0 1 1 1 1 0 0)
 414                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 415                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 416                                 uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 417                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 418                         }
 419                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX){
 420                                 //(1 1 0 0 0 0 1 1 1 1 0 0)
 421                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 422                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 423                                 uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
 424                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 425                         }
 426                 }
 427                 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
 428                         sokoban_screen *tmp_scr = get_coord(x, y, screen);
 429                         sokoban_screen *tmp_scr_d = get_coord(x + xdelta, y + ydelta, screen);
 430                         sokoban_screen *tmp_scr_g = get_coord(x + xgamma, y + ygamma, screen);
 431                         xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
 432                         int deltai = bddvar->value.var[0];
 433                         bddvar = getxy(x + xgamma, y + ygamma, bm->f);
 434                         int gammai = bddvar->value.var[0];
 435                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
 436                                 //(0 1 0 0 1 1 1 0 0 0 1 1)
 437                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 438                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 439                                 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 440                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 441                         }
 442                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
 443                                 //(0 1 1 0 1 1 1 0 0 1 1 1)
 444                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 445                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 446                                 uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
 447                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 448                         }
 449                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
 450                                 //(0 1 0 1 1 0 1 0 1 0 0 1)
 451                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 452                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 453                                 uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
 454                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 455                         }
 456                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
 457                                 //(0 1 1 1 1 0 1 0 1 1 0 1)
 458                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 459                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 460                                 uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 461                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 462                         }
 463                         if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
 464                                 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
 465                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 466                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 467                                 uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 468                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 469                         }
 470                         if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
 471                                 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
 472                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 473                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 474                                 uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 475                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 476                         }
 477                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
 478                                 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 479                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 480                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 481                                 uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 482                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 483                         }
 484                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
 485                                 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 486                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 487                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 488                                 uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 489                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 490                         }
 491                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
 492                                 //free box agent -> box agent free
 493                                 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 494                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 495                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 496                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
 497                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 498                         }
 499                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
 500                                 //(free targbox agent -> box targagent free)
 501                                 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 502                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 503                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 504                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
 505                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 506                         }
 507                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
 508                                 //(target box agent -> targbox agent free)
 509                                 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 510                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 511                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 512                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
 513                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 514                         }
 515                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
 516                                 //(target targbox agent -> targbox targagent free)
 517                                 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 518                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 519                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 520                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
 521                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 522                         }
 523                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
 524                                 //(free box targagent -> box agent target)
 525                                 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
 526                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 527                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 528                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
 529                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 530                         }
 531                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
 532                                 //(free targbox targagent -> box targagent target)
 533                                 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
 534                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 535                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 536                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
 537                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 538                         }
 539                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
 540                                 //(target box targagent -> targbox agent target)
 541                                 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
 542                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 543                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 544                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
 545                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 546                         }
 547                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
 548                                 //(target targbox targagent -> targbox targagent target)
 549                                 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
 550                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 551                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 552                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
 553                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 554                         }
 555                 }
 556         }
 557         return t;
 558 }
 559
 560 rels *encode_rel(sokoban_screen *screen)
 561 {
 562         LACE_ME;
 563
 564         BDD tl = sylvan_false;
 565
 566         //left relation
 567         tl = create_single_rel(screen, LEFT);
 568         /*
 569         for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
 570                 printf("i:%d\n", i);
 571                 bddxy = getbdd(i*3, bm->t);
 572                 x = bddxy->value.x;
 573                 y = bddxy->value.y;
 574                 if (check_space(x, y, LEFT, 1, bm) == 0){
 575                         sokoban_screen *tmp_scr = get_coord(x, y, screen);
 576                         if (tmp_scr->tile == AGENT){
 577                                 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
 578                                 BDDVAR relvars[6]  = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
 579                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
 580                                 uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
 581                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 582                         }
 583                         if (tmp_scr->tile == TARGAGENT){
 584                                 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
 585                                 BDDVAR relvars[6]  = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
 586                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
 587                                 uint8_t rel_enc[6] = {1, 1, 1, 1, 0, 0};
 588                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 589                         }
 590                 }
 591                 else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 0){
 592                         sokoban_screen *tmp_scr = get_coord(x, y, screen);
 593                         sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
 594                         xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f);
 595                         int deltai = bddvar->value.var[0];
 596                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
 597                                 //(0 1 0 0 1 1 1 0 0 0 1 1)
 598                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 599                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 600                                 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 601                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 602                         }
 603                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
 604                                 //(0 1 1 0 1 1 1 0 0 1 1 1)
 605                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 606                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 607                                 uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
 608                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 609                         }
 610                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
 611                                 //(0 1 0 1 1 0 1 0 1 0 0 1)
 612                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 613                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 614                                 uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
 615                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 616                         }
 617                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
 618                                 //(0 1 1 1 1 0 1 0 1 1 0 1)
 619                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 620                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 621                                 uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 622                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 623                         }
 624                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX){
 625                                 //(0 0 1 1 0 0 1 1 0 0 1 1)
 626                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 627                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 628                                 uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 629                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 630                         }
 631                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX){
 632                                 //(1 1 0 0 0 0 1 1 0 0 1 1)
 633                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 634                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 635                                 uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
 636                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 637                         }
 638                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX){
 639                                 //(0 0 1 1 0 0 1 1 1 1 0 0)
 640                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 641                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 642                                 uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 643                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 644                         }
 645                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX){
 646                                 //(1 1 0 0 0 0 1 1 1 1 0 0)
 647                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 648                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 649                                 uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
 650                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 651                         }
 652                 }
 653                 else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 1){
 654                         sokoban_screen *tmp_scr = get_coord(x, y, screen);
 655                         sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
 656                         sokoban_screen *tmp_scr_g = get_coord(x - 2, y, screen);
 657                         xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f);
 658                         int deltai = bddvar->value.var[0];
 659                         bddvar = getxy(x - 2, y, bm->f);
 660                         int gammai = bddvar->value.var[0];
 661                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
 662                                 //(0 1 0 0 1 1 1 0 0 0 1 1)
 663                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 664                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 665                                 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 666                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 667                         }
 668                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
 669                                 //(0 1 1 0 1 1 1 0 0 1 1 1)
 670                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 671                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 672                                 uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
 673                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 674                         }
 675                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
 676                                 //(0 1 0 1 1 0 1 0 1 0 0 1)
 677                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 678                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 679                                 uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
 680                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 681                         }
 682                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
 683                                 //(0 1 1 1 1 0 1 0 1 1 0 1)
 684                                 BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 685                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 686                                 uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 687                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 688                         }
 689                         if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
 690                                 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
 691                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 692                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 693                                 uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 694                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 695                         }
 696                         if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
 697                                 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
 698                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 699                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 700                                 uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 701                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 702                         }
 703                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
 704                                 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 705                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 706                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 707                                 uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 708                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 709                         }
 710                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
 711                                 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 712                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 713                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 714                                 uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 715                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 716                         }
 717                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
 718                                 //free box agent -> box agent free
 719                                 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 720                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 721                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 722                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
 723                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 724                         }
 725                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
 726                                 //(free targbox agent -> box targagent free)
 727                                 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 728                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 729                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 730                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
 731                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 732                         }
 733                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
 734                                 //(target box agent -> targbox agent free)
 735                                 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 736                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 737                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 738                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
 739                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 740                         }
 741                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
 742                                 //(target targbox agent -> targbox targagent free)
 743                                 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 744                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 745                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 746                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
 747                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 748                         }
 749                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
 750                                 //(free box targagent -> box agent target)
 751                                 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
 752                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 753                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 754                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
 755                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 756                         }
 757                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
 758                                 //(free targbox targagent -> box targagent target)
 759                                 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
 760                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 761                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 762                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
 763                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 764                         }
 765                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
 766                                 //(target box targagent -> targbox agent target)
 767                                 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
 768                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 769                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 770                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
 771                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 772                         }
 773                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
 774                                 //(target targbox targagent -> targbox targagent target)
 775                                 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
 776                                 BDDVAR relvars[18]  = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
 777                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 778                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
 779                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 780                         }
 781                 }
 782         }
 783         */
 784
 785         //up relation
 786         BDD tu = create_single_rel(screen, UP);
 787
 788         //right relation
 789         BDD tr = create_single_rel(screen, RIGHT);
 790
 791         //down relation
 792         BDD td = create_single_rel(screen, DOWN);
 793
 794         rels *rls = NULL;
 795         rls = (rels *)malloc(sizeof(rels));
 796         rls->rell = &tl;
 797         rls->relu = &tu;
 798         rls->relr = &tr;
 799         rls->reld = &td;
 800
 801         return rls;
 802 }