- /*
- for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
- printf("i:%d\n", i);
- bddxy = getbdd(i*3, bm->t);
- x = bddxy->value.x;
- y = bddxy->value.y;
- if (check_space(x, y, LEFT, 1, bm) == 0){
- sokoban_screen *tmp_scr = get_coord(x, y, screen);
- if (tmp_scr->tile == AGENT){
- //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
- BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
- uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT){
- //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
- BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
- uint8_t rel_enc[6] = {1, 1, 1, 1, 0, 0};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- }
- else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 0){
- sokoban_screen *tmp_scr = get_coord(x, y, screen);
- sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
- xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f);
- int deltai = bddvar->value.var[0];
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
- //(0 1 0 0 1 1 1 0 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
- //(0 1 1 0 1 1 1 0 0 1 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
- //(0 1 0 1 1 0 1 0 1 0 0 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
- //(0 1 1 1 1 0 1 0 1 1 0 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX){
- //(0 0 1 1 0 0 1 1 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX){
- //(1 1 0 0 0 0 1 1 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX){
- //(0 0 1 1 0 0 1 1 1 1 0 0)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX){
- //(1 1 0 0 0 0 1 1 1 1 0 0)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- }
- else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 1){
- sokoban_screen *tmp_scr = get_coord(x, y, screen);
- sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
- sokoban_screen *tmp_scr_g = get_coord(x - 2, y, screen);
- xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f);
- int deltai = bddvar->value.var[0];
- bddvar = getxy(x - 2, y, bm->f);
- int gammai = bddvar->value.var[0];
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
- //(0 1 0 0 1 1 1 0 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
- //(0 1 1 0 1 1 1 0 0 1 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
- //(0 1 0 1 1 0 1 0 1 0 0 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
- //(0 1 1 1 1 0 1 0 1 1 0 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
- uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
- //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
- //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
- //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
- //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
- //free box agent -> box agent free
- //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
- //(free targbox agent -> box targagent free)
- //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
- //(target box agent -> targbox agent free)
- //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
- //(target targbox agent -> targbox targagent free)
- //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
- //(free box targagent -> box agent target)
- //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
- //(free targbox targagent -> box targagent target)
- //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
- //(target box targagent -> targbox agent target)
- //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
- //(target targbox targagent -> targbox targagent target)
- //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
- 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};
- BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
- uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
- t = sylvan_union_cube(t, relvarset, rel_enc);
- }
- }
- }
- */