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 typedef struct {
  22         int x;
  23         int y;
  24 } xy;
  25
  26 typedef struct {
  27         int var[3];
  28 } bddvar;
  29
  30 typedef struct {
  31         xy key;
  32         bddvar value;
  33         UT_hash_handle hh;
  34 } xy_bddvar_map;
  35
  36 typedef struct {
  37         int key;
  38         xy value;
  39         UT_hash_handle hh;
  40 } bddvar_xy_map;
  41
  42 typedef struct {
  43         xy_bddvar_map *f;
  44         bddvar_xy_map *t;
  45 } bimap;
  46
  47 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
  48 {
  49         xy_bddvar_map k, *r = NULL;
  50         memset(&k, 0, sizeof(xy_bddvar_map));
  51         k.key.x = x;
  52         k.key.y = y;
  53         HASH_FIND(hh, map, &k.key, sizeof(xy), r);
  54         return r;
  55 }
  56
  57 bddvar_xy_map *getbdd(int key, bddvar_xy_map *map)
  58 {
  59         bddvar_xy_map k, *r = NULL;
  60         memset(&k, 0, sizeof(bddvar_xy_map));
  61         k.key = key;
  62         HASH_FIND(hh, map, &k.key, sizeof(int), r);
  63         return r;
  64 }
  65
  66
  67 bimap *create_bimap_helper(sokoban_screen *screen)
  68 {
  69         int varcount = 0;
  70         sokoban_screen *r;
  71         xy_bddvar_map *xybdd = NULL;
  72         bddvar_xy_map *bddxy = NULL;
  73         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
  74                 xy_bddvar_map *f = NULL;
  75                 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
  76                 memset(f, 0, sizeof(xy_bddvar_map));
  77                 f->key.x = r->coord.x;
  78                 f->key.y = r->coord.y;
  79                 f->value.var[0] = varcount;
  80                 f->value.var[1] = varcount + 1;
  81                 f->value.var[2] = varcount + 2;
  82                 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
  83
  84                 for (int i = 0; i <3; i++){
  85                         bddvar_xy_map *t = NULL;
  86                         t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
  87                         memset(t, 0, sizeof(bddvar_xy_map));
  88                         t->key = varcount + i;
  89                         t->value.x = r->coord.x;
  90                         t->value.y = r->coord.y;
  91                         HASH_ADD(hh, bddxy, key, sizeof(int), t);
  92                 }
  93                 varcount = varcount + 3;
  94         }
  95         bimap *bm = NULL;
  96         bm = (bimap *)malloc(sizeof(bimap));
  97         bm->f = xybdd;
  98         bm->t = bddxy;
  99         return bm;
 100 }
 101
 102 int check_xy_exists(int x, int y, bimap *bm)
 103 {
 104         int res = 0;
 105         if (getxy(x, y, bm->f) != NULL) res = 1;
 106         return res;
 107 }
 108
 109 int check_space(int x, int y, direction d, int delta, bimap *bm)
 110 {
 111         switch(d){
 112         case LEFT: x = x - delta; break;
 113         case UP: y = y - delta; break;
 114         case RIGHT: x = x + delta; break;
 115         case DOWN: y = y + delta; break;
 116         }
 117         return check_xy_exists(x, y, bm);
 118 }
 119
 120 /*
 121  * Each coordinate has three related boolean variables. The combination of those boolean variables
 122  * defines tiles:
 123  * 000: Wall
 124  * 001: Free
 125  * 010: Box
 126  * 100: Box on target
 127  * 011: Target
 128  * 101: Agent
 129  * 110: Agent on target
 130  * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
 131  * tiles in the shrinked screen.
 132  * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
 133  * directly in transition relations.
 134  */
 135
 136 state *encode_screen(sokoban_screen *screen)
 137 {
 138         LACE_ME;
 139
 140         BDDVAR vars[HASH_COUNT(screen) * 3];
 141         for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
 142                 vars[i] = i * 2;
 143         }
 144
 145         uint8_t st_enc[HASH_COUNT(screen) * 3];
 146
 147         BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
 148         BDD s;
 149         state *fullState = NULL;
 150         fullState = (state *)malloc(sizeof(state));
 151         fullState->vars.varset = varset;
 152         fullState->vars.size = HASH_COUNT(screen) * 3;
 153         int tile_index = 0;
 154         sokoban_screen *r;
 155         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 156                 switch(r->tile){
 157                 case FREE: //001
 158                         st_enc[tile_index] = 0;
 159                         tile_index++;
 160                         st_enc[tile_index] = 0;
 161                         tile_index++;
 162                         st_enc[tile_index] = 1;
 163                         tile_index++;
 164                         break;
 165                 case WALL: //000
 166                         st_enc[tile_index] = 0;
 167                         tile_index++;
 168                         st_enc[tile_index] = 0;
 169                         tile_index++;
 170                         st_enc[tile_index] = 0;
 171                         tile_index++;
 172                         break;
 173                 case BOX: //010
 174                         st_enc[tile_index] = 0;
 175                         tile_index++;
 176                         st_enc[tile_index] = 1;
 177                         tile_index++;
 178                         st_enc[tile_index] = 0;
 179                         tile_index++;
 180                         break;
 181                 case TARGET: //011
 182                         st_enc[tile_index] = 0;
 183                         tile_index++;
 184                         st_enc[tile_index] = 1;
 185                         tile_index++;
 186                         st_enc[tile_index] = 1;
 187                         tile_index++;
 188                         break;
 189                 case AGENT: //101
 190                         st_enc[tile_index] = 1;
 191                         tile_index++;
 192                         st_enc[tile_index] = 0;
 193                         tile_index++;
 194                         st_enc[tile_index] = 1;
 195                         tile_index++;
 196                         break;
 197                 case TARGAGENT: //110
 198                         st_enc[tile_index] = 1;
 199                         tile_index++;
 200                         st_enc[tile_index] = 1;
 201                         tile_index++;
 202                         st_enc[tile_index] = 0;
 203                         tile_index++;
 204                         break;
 205                 case TARGBOX: //100
 206                         st_enc[tile_index] = 1;
 207                         tile_index++;
 208                         st_enc[tile_index] = 0;
 209                         tile_index++;
 210                         st_enc[tile_index] = 0;
 211                         tile_index++;
 212                         break;
 213                 }
 214         }
 215         s = sylvan_cube(varset, st_enc);
 216         fullState->bdd = s;
 217         printf("Initial state encoded\n");
 218         return fullState;
 219 }
 220
 221 BDD create_single_rel(sokoban_screen *screen, direction dir)
 222 {
 223         LACE_ME;
 224         BDD t = sylvan_false;
 225         bimap *bm = create_bimap_helper(screen);
 226         int x = 0;
 227         int y = 0;
 228         bddvar_xy_map *bddxy = NULL;
 229         int xdelta = 0;
 230         int ydelta = 0;
 231         int xgamma = 0;
 232         int ygamma = 0;
 233         switch(dir){
 234         case LEFT:
 235                 xdelta = -1;
 236                 ydelta = 0;
 237                 xgamma = -2;
 238                 ygamma = 0;
 239                 break;
 240         case UP:
 241                 xdelta = 0;
 242                 ydelta = -1;
 243                 xgamma = 0;
 244                 ygamma = -2;
 245                 break;
 246         case RIGHT:
 247                 xdelta = 1;
 248                 ydelta = 0;
 249                 xgamma = 2;
 250                 ygamma = 0;
 251                 break;
 252         case DOWN:
 253                 xdelta = 0;
 254                 ydelta = 1;
 255                 xgamma = 0;
 256                 ygamma = 2;
 257                 break;
 258         }
 259
 260         for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
 261                 bddxy = getbdd(i*3, bm->t);
 262                 x = bddxy->value.x;
 263                 y = bddxy->value.y;
 264                 if (check_space(x, y, dir, 1, bm) == 0){
 265                         sokoban_screen *tmp_scr = get_coord(x, y, screen);
 266                         if (tmp_scr->tile == AGENT){
 267                                 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
 268                                 BDDVAR relvars[6]  = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
 269                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
 270                                 uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
 271                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 272                         }
 273                         if (tmp_scr->tile == TARGAGENT){
 274                                 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
 275                                 BDDVAR relvars[6]  = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
 276                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
 277                                 uint8_t rel_enc[6] = {1, 1, 1, 1, 0, 0};
 278                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 279                         }
 280                 }
 281                 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
 282                         sokoban_screen *tmp_scr = get_coord(x, y, screen);
 283                         sokoban_screen *tmp_scr_d = get_coord(x + xdelta, y + ydelta, screen);
 284                         xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
 285                         int deltai = bddvar->value.var[0];
 286                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
 287                                 //(0 1 0 0 1 1 1 0 0 0 1 1)
 288                                 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};
 289                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 290                                 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 291                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 292                         }
 293                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
 294                                 //(0 1 1 0 1 1 1 0 0 1 1 1)
 295                                 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};
 296                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 297                                 uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
 298                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 299                         }
 300                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
 301                                 //(0 1 0 1 1 0 1 0 1 0 0 1)
 302                                 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};
 303                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 304                                 uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
 305                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 306                         }
 307                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
 308                                 //(0 1 1 1 1 0 1 0 1 1 0 1)
 309                                 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};
 310                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 311                                 uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 312                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 313                         }
 314                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX){
 315                                 //(0 0 1 1 0 0 1 1 0 0 1 1)
 316                                 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};
 317                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 318                                 uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 319                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 320                         }
 321                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX){
 322                                 //(1 1 0 0 0 0 1 1 0 0 1 1)
 323                                 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};
 324                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 325                                 uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
 326                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 327                         }
 328                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX){
 329                                 //(0 0 1 1 0 0 1 1 1 1 0 0)
 330                                 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};
 331                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 332                                 uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 333                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 334                         }
 335                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX){
 336                                 //(1 1 0 0 0 0 1 1 1 1 0 0)
 337                                 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};
 338                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 339                                 uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
 340                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 341                         }
 342                 }
 343                 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
 344                         sokoban_screen *tmp_scr = get_coord(x, y, screen);
 345                         sokoban_screen *tmp_scr_d = get_coord(x + xdelta, y + ydelta, screen);
 346                         sokoban_screen *tmp_scr_g = get_coord(x + xgamma, y + ygamma, screen);
 347                         xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
 348                         int deltai = bddvar->value.var[0];
 349                         bddvar = getxy(x + xgamma, y + ygamma, bm->f);
 350                         int gammai = bddvar->value.var[0];
 351                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
 352                                 //(0 1 0 0 1 1 1 0 0 0 1 1)
 353                                 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};
 354                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 355                                 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 356                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 357                         }
 358                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
 359                                 //(0 1 1 0 1 1 1 0 0 1 1 1)
 360                                 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};
 361                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 362                                 uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
 363                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 364                         }
 365                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
 366                                 //(0 1 0 1 1 0 1 0 1 0 0 1)
 367                                 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};
 368                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 369                                 uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
 370                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 371                         }
 372                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
 373                                 //(0 1 1 1 1 0 1 0 1 1 0 1)
 374                                 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};
 375                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 376                                 uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 377                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 378                         }
 379                         if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
 380                                 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
 381                                 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};
 382                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 383                                 uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 384                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 385                         }
 386                         if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
 387                                 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
 388                                 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};
 389                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 390                                 uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 391                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 392                         }
 393                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
 394                                 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 395                                 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};
 396                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 397                                 uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 398                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 399                         }
 400                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
 401                                 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 402                                 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};
 403                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 404                                 uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 405                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 406                         }
 407                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
 408                                 //free box agent -> box agent free
 409                                 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 410                                 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};
 411                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 412                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
 413                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 414                         }
 415                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
 416                                 //(free targbox agent -> box targagent free)
 417                                 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 418                                 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};
 419                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 420                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
 421                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 422                         }
 423                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
 424                                 //(target box agent -> targbox agent free)
 425                                 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 426                                 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};
 427                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 428                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
 429                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 430                         }
 431                         if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
 432                                 //(target targbox agent -> targbox targagent free)
 433                                 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 434                                 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};
 435                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 436                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
 437                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 438                         }
 439                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
 440                                 //(free box targagent -> box agent target)
 441                                 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
 442                                 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};
 443                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 444                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
 445                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 446                         }
 447                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
 448                                 //(free targbox targagent -> box targagent target)
 449                                 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
 450                                 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};
 451                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 452                                 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
 453                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 454                         }
 455                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
 456                                 //(target box targagent -> targbox agent target)
 457                                 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
 458                                 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};
 459                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 460                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
 461                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 462                         }
 463                         if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
 464                                 //(target targbox targagent -> targbox targagent target)
 465                                 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
 466                                 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};
 467                                 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
 468                                 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
 469                                 t = sylvan_union_cube(t, relvarset, rel_enc);
 470                         }
 471                 }
 472         }
 473         return t;
 474 }
 475
 476 rels *encode_rel(sokoban_screen *screen)
 477 {
 478         LACE_ME;
 479
 480         BDD tl = sylvan_false;
 481
 482         //left relation
 483         tl = create_single_rel(screen, LEFT);
 484
 485         //up relation
 486         BDD tu = create_single_rel(screen, UP);
 487
 488         //right relation
 489         BDD tr = create_single_rel(screen, RIGHT);
 490
 491         //down relation
 492         BDD td = create_single_rel(screen, DOWN);
 493
 494         rels *rls = NULL;
 495         rls = (rels *)malloc(sizeof(rels));
 496         rls->rell = &tl;
 497         rls->relu = &tu;
 498         rls->relr = &tr;
 499         rls->reld = &td;
 500
 501         return rls;
 502 }