+ BDD state = sylvan_false;
+ int tile_index = 0;
+ sokoban_screen *r;
+ LACE_ME;
+ for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
+ switch(r->tile){
+ case FREE:
+ if (state == sylvan_false){
+ state = sylvan_not(sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ }
+ else {
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ }
+ break;
+ case WALL:
+ if (state == sylvan_false){
+ state = sylvan_not(sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ }
+ else {
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ }
+ break;
+ case BOX:
+ if (state == sylvan_false){
+ state = sylvan_not(sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ }
+ else {
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ }
+ break;
+ case TARGET:
+ if (state == sylvan_false){
+ state = sylvan_not(sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ }
+ else {
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ }
+ break;
+ case AGENT:
+ if (state == sylvan_false){
+ state = sylvan_ithvar(tile_index);
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ }
+ else {
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ }
+ break;
+ case TARGAGENT:
+ if (state == sylvan_false){
+ state = sylvan_ithvar(tile_index);
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ }
+ else {
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ }
+ break;
+ case TARGBOX:
+ if (state == sylvan_false){
+ state = sylvan_ithvar(tile_index);
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ }
+ else {
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ }
+ break;
+ }
+ }
+ /*
+ xy_bddvar_map *map = NULL;
+ map = create_xy_bddvar_map(screen);
+ xy_bddvar_map *m = getxy(1, 1, map);
+ bddvar_xy_map *map2 = NULL;
+ map2 = create_bddvar_xy_map(screen);
+ bddvar_xy_map *m2 = getbdd(2, map2);
+ printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]);
+ printf("Test2: %d %d\n", m2->value.x, m2->value.y);
+ */
+ /*
+ bimap *bm = NULL;
+ bm = create_bimap_helper(screen);
+ xy_bddvar_map *m = getxy(1, 1, bm->f);
+ bddvar_xy_map *m2 = getbdd(2, bm->t);
+ printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]);
+ printf("Test2: %d %d\n", m2->value.x, m2->value.y);
+ printf("%d tiles were encoded\n", tile_index);
+ if (bm != NULL) printf ("WORKS!\n");
+ */
+ return state;