+ 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++;
+ }
+ printf("x = %d y = %d FREE\n", r->coord.x, r->coord.y);
+ 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++;
+ }
+ printf("x = %d y = %d WALL\n", r->coord.x, r->coord.y);
+ 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++;
+ }
+ printf("x = %d y = %d BOX\n", r->coord.x, r->coord.y);
+ 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++;
+ }
+ printf("x = %d y = %d TARGET\n", r->coord.x, r->coord.y);
+ 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++;
+ }
+ printf("x = %d y = %d AGENT\n", r->coord.x, r->coord.y);
+ 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++;
+ }
+ printf("x = %d y = %d TARGAGENT\n", r->coord.x, r->coord.y);
+ 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++;
+ }
+ printf("x = %d y = %d TARGBOX\n", r->coord.x, r->coord.y);
+ break;
+ }
+ }
+ return state;