X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=42ad6cee7c9e787d2b7c2ee5a5f7349e90a69f47;hb=313c58c1cd85852f33ff7ca7c638ccb3066d5069;hp=e54fe568c428c2f6818ec9a16abd94fd50f3c0fb;hpb=6a8c26fdf4e143d9009c3288659ed00bc7d88043;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index e54fe56..42ad6ce 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -1,17 +1,7 @@ #include -#include -#include #include #include -#include -#include - -#ifdef HAVE_PROFILER -#include -#endif - #include -#include #include #include "coord.h" @@ -76,16 +66,16 @@ bimap *create_bimap_helper(sokoban_screen *screen) memset(f, 0, sizeof(xy_bddvar_map)); f->key.x = r->coord.x; f->key.y = r->coord.y; - f->value.var[0] = varcount; - f->value.var[1] = varcount + 1; - f->value.var[2] = varcount + 2; + f->value.var[0] = varcount * 2; + f->value.var[1] = (varcount + 1) * 2; + f->value.var[2] = (varcount + 2) * 2; HASH_ADD(hh, xybdd, key, sizeof(xy), f); for (int i = 0; i <3; i++){ bddvar_xy_map *t = NULL; t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map)); memset(t, 0, sizeof(bddvar_xy_map)); - t->key = varcount + i; + t->key = (varcount + i) * 2; t->value.x = r->coord.x; t->value.y = r->coord.y; HASH_ADD(hh, bddxy, key, sizeof(int), t); @@ -132,7 +122,6 @@ int check_space(int x, int y, direction d, int delta, bimap *bm) * It seems that the move variable is not necessary since non-deterministic moves can be emvedded * directly in transition relations. */ - state *encode_screen(sokoban_screen *screen) { LACE_ME; @@ -151,70 +140,108 @@ state *encode_screen(sokoban_screen *screen) fullState->vars.varset = varset; fullState->vars.size = HASH_COUNT(screen) * 3; int tile_index = 0; - sokoban_screen *r; - for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ + for(sokoban_screen *r=screen; r != NULL; r = r->hh.next){ switch(r->tile){ case FREE: //001 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; break; case WALL: //000 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; case BOX: //010 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; break; case TARGET: //011 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 1; break; case AGENT: //101 - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; break; case TARGAGENT: //110 - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; break; case TARGBOX: //100 - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + } + } + s = sylvan_cube(varset, st_enc); + fullState->bdd = s; + return fullState; +} + +state *encode_goal(sokoban_screen *screen){ + LACE_ME; + + BDDVAR vars[HASH_COUNT(screen) * 3]; + for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){ + vars[i] = i * 2; + } + + uint8_t st_enc[HASH_COUNT(screen) * 3]; + + BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3); + BDD s; + state *fullState = NULL; + fullState = (state *)malloc(sizeof(state)); + fullState->vars.varset = varset; + fullState->vars.size = HASH_COUNT(screen) * 3; + int tile_index = 0; + for(sokoban_screen *r=screen; r != NULL; r=r->hh.next){ + switch(r->tile){ + case FREE: //001 -> any + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + break; + case WALL: //000 -> stays the same + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + case BOX: //010 -> any + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + break; + case TARGET: //011 -> targbox + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + case AGENT: //101 -> any + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + break; + case TARGAGENT: //110 -> targbox + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + case TARGBOX: //100 -> stays the same + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; } } s = sylvan_cube(varset, st_enc); fullState->bdd = s; - printf("Initial state encoded\n"); return fullState; } @@ -259,16 +286,15 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) } for (unsigned int i = 0; i < HASH_COUNT(screen); i++){ - bddxy = getbdd(i*3, bm->t); + bddxy = getbdd(i*6, bm->t); x = bddxy->value.x; y = bddxy->value.y; if (check_space(x, y, dir, 1, bm) == 0){ - + //Agent -> 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}; + BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5}; BDDSET relvarset = sylvan_set_fromarray(relvars, 6); uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1}; - trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -276,20 +302,11 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; + //Targagent -> Targagent //1 1 1 1 0 0 (1 1 0 -> 1 1 0) - relvars[0] = i * 3; - relvars[1] = i * 3 + 1; - relvars[2] = i * 3 + 2; - relvars[3] = i * 3 + 3; - relvars[4] = i * 3 + 4; - relvars[5] = i * 3 + 5; relvarset = sylvan_set_fromarray(relvars, 6); - rel_enc[0] = 1; - rel_enc[1] = 1; - rel_enc[2] = 1; - rel_enc[3] = 1; - rel_enc[4] = 0; - rel_enc[5] = 0; + uint8_t rel_enc1[6] = {1, 1, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc1, 6*sizeof(uint8_t)); trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); @@ -298,16 +315,24 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - } - else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){ - + } else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){ xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); - int deltai = bddvar->value.var[0]; - - //(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}; + unsigned int deltai = bddvar->value.var[0]; + //Agent Free -> Free Agent + //(1 0 0 0 1 1 0 1 0 0 1 1) + //or + //(0 1 0 0 1 1 1 0 0 0 1 1) + BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+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}; + uint8_t rel_enc[12]; + if (i*6 < deltai){ + uint8_t rel_enc0[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc0[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -315,32 +340,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 1 1 0 1 1 1 0 0 1 1 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Agent Target -> Free Targagent + //(1 0 0 0 1 1 0 1 1 1 1 0) + //or + //(0 1 1 1 1 0 1 0 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 1; - rel_enc[3] = 0; - rel_enc[4] = 1; - rel_enc[5] = 1; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 0; - rel_enc[9] = 1; - rel_enc[10] = 1; - rel_enc[11] = 1; + if (i*6 < deltai){ + uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0}; + memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -348,32 +360,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 1 0 1 1 0 1 0 1 0 0 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Free -> Target Agent + //(1 0 1 1 0 1 0 1 0 0 1 1) + //or + //(0 1 0 0 1 1 1 0 1 1 0 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 0; - rel_enc[3] = 1; - rel_enc[4] = 1; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 1; - rel_enc[9] = 0; - rel_enc[10] = 0; - rel_enc[11] = 1; + if (i*6 < deltai){ + uint8_t rel_enc3[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc3[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -381,32 +380,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 1 1 1 1 0 1 0 1 1 0 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Target -> Target Targagent + //(1 0 1 1 0 1 0 1 1 1 1 0) + //or + //(0 1 1 1 1 0 1 0 1 1 0 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 1; - rel_enc[3] = 1; - rel_enc[4] = 1; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 1; - rel_enc[9] = 1; - rel_enc[10] = 0; - rel_enc[11] = 1; + if (i*6 < deltai){ + uint8_t rel_enc4[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0}; + memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc4[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -414,32 +400,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 0 1 1 0 0 1 1 0 0 1 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Agent Box -> Agent Box + //(1 1 0 0 1 1 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 0; - rel_enc[2] = 1; - rel_enc[3] = 1; - rel_enc[4] = 0; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 1; - rel_enc[8] = 0; - rel_enc[9] = 0; - rel_enc[10] = 1; - rel_enc[11] = 1; + if (i*6 < deltai){ + uint8_t rel_enc5[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc5[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -447,32 +420,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(1 1 0 0 0 0 1 1 0 0 1 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Agent Targbox -> Agent Targbox + //(1 1 0 0 1 1 1 1 0 0 0 0) + // + //(1 1 0 0 0 0 1 1 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 1; - rel_enc[1] = 1; - rel_enc[2] = 0; - rel_enc[3] = 0; - rel_enc[4] = 0; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 1; - rel_enc[8] = 0; - rel_enc[9] = 0; - rel_enc[10] = 1; - rel_enc[11] = 1; + if (i*6 < deltai){ + uint8_t rel_enc6[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc6[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -480,32 +440,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 0 1 1 0 0 1 1 1 1 0 0) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Box -> Targagent Box + //(1 1 1 1 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 1 1 0 0) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 0; - rel_enc[2] = 1; - rel_enc[3] = 1; - rel_enc[4] = 0; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 1; - rel_enc[8] = 1; - rel_enc[9] = 1; - rel_enc[10] = 0; - rel_enc[11] = 0; + if (i*6 < deltai){ + uint8_t rel_enc7[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc7[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -513,51 +460,45 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(1 1 0 0 0 0 1 1 1 1 0 0) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Targbox -> Targagent Targbox + //(1 1 1 1 0 0 1 1 0 0 0 0) + //or + //(1 1 0 0 0 0 1 1 1 1 0 0) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 1; - rel_enc[1] = 1; - rel_enc[2] = 0; - rel_enc[3] = 0; - rel_enc[4] = 0; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 1; - rel_enc[8] = 1; - rel_enc[9] = 1; - rel_enc[10] = 0; - rel_enc[11] = 0; + if (i*6 < deltai){ + uint8_t rel_enc8[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc8[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; trs_current->varset.size = 12; trs_current->next_rel = trs; trs = trs_current; - - } - else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){ - + } else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){ xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); - int deltai = bddvar->value.var[0]; + unsigned int deltai = bddvar->value.var[0]; bddvar = getxy(x + xgamma, y + ygamma, bm->f); - int gammai = bddvar->value.var[0]; - - //(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}; + unsigned int gammai = bddvar->value.var[0]; + //Agent Free -> Free Agent + //(1 0 0 0 1 1 0 1 0 0 1 1) + //or + //(0 1 0 0 1 1 1 0 0 0 1 1) + BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+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}; + uint8_t rel_enc[12]; + if (i*6 < deltai){ + uint8_t rel_enc_[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc_[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -565,32 +506,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 1 1 0 1 1 1 0 0 1 1 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Agent Target -> Free Targagent + //(1 0 0 0 1 1 0 1 1 1 1 0) + //or + //(0 1 1 1 1 0 1 0 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 1; - rel_enc[3] = 0; - rel_enc[4] = 1; - rel_enc[5] = 1; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 0; - rel_enc[9] = 1; - rel_enc[10] = 1; - rel_enc[11] = 1; + if (i*6 < deltai){ + uint8_t rel_enc9[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0}; + memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc9[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -598,32 +526,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 1 0 1 1 0 1 0 1 0 0 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Free -> Target Agent (LEFT || UP) + //(1 0 1 1 0 1 0 1 0 0 1 1) + //or + //(0 1 0 0 1 1 1 0 1 1 0 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 0; - rel_enc[3] = 1; - rel_enc[4] = 1; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 1; - rel_enc[9] = 0; - rel_enc[10] = 0; - rel_enc[11] = 1; + if (i*6 < deltai){ + uint8_t rel_enc10[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc10[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -631,32 +546,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 1 1 1 1 0 1 0 1 1 0 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Target -> Target Targagent (LEFT || UP) + //(1 0 1 1 0 1 0 1 1 1 1 0) + //or + //(0 1 1 1 1 0 1 0 1 1 0 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 1; - rel_enc[3] = 1; - rel_enc[4] = 1; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 1; - rel_enc[9] = 1; - rel_enc[10] = 0; - rel_enc[11] = 1; + if (i*6 < deltai){ + uint8_t rel_enc11[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0}; + memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc11[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -664,46 +566,46 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars1[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}; - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Box Box -> Agent Box Box + //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma) + //or + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i) + //or + //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta) + //or + //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta) + //or + //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma) + //or + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i) + BDDVAR relvars1[18] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5, gammai, gammai+1, gammai+2, gammai+3, gammai+4, gammai+5}; BDD relvarset1 = sylvan_set_fromarray(relvars1, 18); uint8_t rel_enc1[18]; - rel_enc1[0] = 0; - rel_enc1[1] = 0; - rel_enc1[2] = 1; - rel_enc1[3] = 1; - rel_enc1[4] = 0; - rel_enc1[5] = 0; - rel_enc1[6] = 0; - rel_enc1[7] = 0; - rel_enc1[8] = 1; - rel_enc1[9] = 1; - rel_enc1[10] = 0; - rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 1; - rel_enc1[14] = 0; - rel_enc1[15] = 0; - rel_enc1[16] = 1; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -711,44 +613,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Box Targbox -> Agent Box Targbox (LEFT || UP) + //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma) + //or + //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i) + //or + //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta) + //or + //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta) + //or + //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma) + //or + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i) relvarset1 = sylvan_set_fromarray(relvars1, 18); - rel_enc1[0] = 1; - rel_enc1[1] = 1; - rel_enc1[2] = 0; - rel_enc1[3] = 0; - rel_enc1[4] = 0; - rel_enc1[5] = 0; - rel_enc1[6] = 0; - rel_enc1[7] = 0; - rel_enc1[8] = 1; - rel_enc1[9] = 1; - rel_enc1[10] = 0; - rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 1; - rel_enc1[14] = 0; - rel_enc1[15] = 0; - rel_enc1[16] = 1; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -756,45 +657,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Box Box -> Targagent Box Box + //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0) + //or + //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - rel_enc1[0] = 0; - rel_enc1[1] = 0; - rel_enc1[2] = 1; - rel_enc1[3] = 1; - rel_enc1[4] = 0; - rel_enc1[5] = 0; - rel_enc1[6] = 0; - rel_enc1[7] = 0; - rel_enc1[8] = 1; - rel_enc1[9] = 1; - rel_enc1[10] = 0; - rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 1; - rel_enc1[14] = 1; - rel_enc1[15] = 1; - rel_enc1[16] = 0; - rel_enc1[17] = 0; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -802,45 +701,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP) + //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0) + //or + //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0) + //or + //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0) + //or + //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0) + //or + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - rel_enc1[0] = 1; - rel_enc1[1] = 1; - rel_enc1[2] = 0; - rel_enc1[3] = 0; - rel_enc1[4] = 0; - rel_enc1[5] = 0; - rel_enc1[6] = 0; - rel_enc1[7] = 0; - rel_enc1[8] = 1; - rel_enc1[9] = 1; - rel_enc1[10] = 0; - rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 1; - rel_enc1[14] = 1; - rel_enc1[15] = 1; - rel_enc1[16] = 0; - rel_enc1[17] = 0; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -848,93 +745,92 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //free box agent -> box agent free - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Box Free -> Free Agent Box + //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0) + //or + //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1) + //or + //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1) + //or + //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1) + //or + //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0) + //or + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - rel_enc1[0] = 0; - rel_enc1[1] = 0; - rel_enc1[2] = 0; - rel_enc1[3] = 1; - rel_enc1[4] = 1; - rel_enc1[5] = 0; - rel_enc1[6] = 0; - rel_enc1[7] = 1; - rel_enc1[8] = 1; - rel_enc1[9] = 0; - rel_enc1[10] = 0; - rel_enc1[11] = 1; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 0; - rel_enc1[15] = 0; - rel_enc1[16] = 1; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; trs_current->varset.size = 18; trs_current->next_rel = trs; trs = trs_current; - //(free targbox agent -> box targagent free) - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Targbox Free -> Free Targagent Box + //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0) + //or + //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1) + //or + //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0) + //or + //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0) + //or + //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0) + //or + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - rel_enc1[0] = 0; - rel_enc1[1] = 0; - rel_enc1[2] = 0; - rel_enc1[3] = 1; - rel_enc1[4] = 1; - rel_enc1[5] = 0; - rel_enc1[6] = 1; - rel_enc1[7] = 1; - rel_enc1[8] = 0; - rel_enc1[9] = 1; - rel_enc1[10] = 0; - rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 0; - rel_enc1[15] = 0; - rel_enc1[16] = 1; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -942,46 +838,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(target box agent -> targbox agent free) - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Box Target -> Free Agent Targbox + //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0) + //or + //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1) + //or + //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1) + //or + //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1) + //or + //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0) + //or + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - rel_enc1[0] = 0; - rel_enc1[1] = 1; - rel_enc1[2] = 1; - rel_enc1[3] = 0; - rel_enc1[4] = 1; - rel_enc1[5] = 0; - rel_enc1[6] = 0; - rel_enc1[7] = 1; - rel_enc1[8] = 1; - rel_enc1[9] = 0; - rel_enc1[10] = 0; - rel_enc1[11] = 1; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 0; - rel_enc1[15] = 0; - rel_enc1[16] = 1; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -989,46 +882,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(target targbox agent -> targbox targagent free) - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Targbox Target -> Free Targagent Targbox + //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0) + //or + //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1) + //or + //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0) + //or + //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0) + //or + //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0) + //or + //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - rel_enc1[0] = 0; - rel_enc1[1] = 1; - rel_enc1[2] = 1; - rel_enc1[3] = 0; - rel_enc1[4] = 1; - rel_enc1[5] = 0; - rel_enc1[6] = 1; - rel_enc1[7] = 1; - rel_enc1[8] = 0; - rel_enc1[9] = 1; - rel_enc1[10] = 0; - rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 0; - rel_enc1[15] = 0; - rel_enc1[16] = 1; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -1036,46 +926,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(free box targagent -> box agent target) - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Box Free -> Target Agent Box + //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0) + //or + //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1) + //or + //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1) + //or + //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1) + //or + //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0) + //or + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - rel_enc1[0] = 0; - rel_enc1[1] = 0; - rel_enc1[2] = 0; - rel_enc1[3] = 1; - rel_enc1[4] = 1; - rel_enc1[5] = 0; - rel_enc1[6] = 0; - rel_enc1[7] = 1; - rel_enc1[8] = 1; - rel_enc1[9] = 0; - rel_enc1[10] = 0; - rel_enc1[11] = 1; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 1; - rel_enc1[15] = 1; - rel_enc1[16] = 0; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -1083,46 +970,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(free targbox targagent -> box targagent target) - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Targbox Free -> Target Targagent Box + //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0) + //or + //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1) + //or + //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0) + //or + //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0) + //or + //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0) + //or + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - rel_enc1[0] = 0; - rel_enc1[1] = 0; - rel_enc1[2] = 0; - rel_enc1[3] = 1; - rel_enc1[4] = 1; - rel_enc1[5] = 0; - rel_enc1[6] = 1; - rel_enc1[7] = 1; - rel_enc1[8] = 0; - rel_enc1[9] = 1; - rel_enc1[10] = 0; - rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 1; - rel_enc1[15] = 1; - rel_enc1[16] = 0; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -1130,46 +1014,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(target box targagent -> targbox agent target) - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Box Target -> Target Agent Targbox + //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0) + //or + //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1) + //or + //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1) + //or + //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1) + //or + //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0) + //or + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - rel_enc1[0] = 0; - rel_enc1[1] = 1; - rel_enc1[2] = 1; - rel_enc1[3] = 0; - rel_enc1[4] = 1; - rel_enc1[5] = 0; - rel_enc1[6] = 0; - rel_enc1[7] = 1; - rel_enc1[8] = 1; - rel_enc1[9] = 0; - rel_enc1[10] = 0; - rel_enc1[11] = 1; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 1; - rel_enc1[15] = 1; - rel_enc1[16] = 0; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -1177,46 +1058,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //(target targbox targagent -> targbox targagent target) - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Targbox Target -> Target Targagent Targbox + //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0) + //or + //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1) + //or + //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0) + //or + //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0) + //or + //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0) + //or + //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - rel_enc1[0] = 0; - rel_enc1[1] = 1; - rel_enc1[2] = 1; - rel_enc1[3] = 0; - rel_enc1[4] = 1; - rel_enc1[5] = 0; - rel_enc1[6] = 1; - rel_enc1[7] = 1; - rel_enc1[8] = 0; - rel_enc1[9] = 1; - rel_enc1[10] = 0; - rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 1; - rel_enc1[15] = 1; - rel_enc1[16] = 0; - rel_enc1[17] = 1; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -1224,6 +1102,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; } + } trs_current = trs; return trs; @@ -1237,14 +1116,8 @@ rels *encode_rel(sokoban_screen *screen) //left relation tl = create_single_rel(screen, LEFT); - - //up relation trans_t *tu = create_single_rel(screen, UP); - - //right relation trans_t *tr = create_single_rel(screen, RIGHT); - - //down relation trans_t *td = create_single_rel(screen, DOWN); rels *rls = NULL; @@ -1256,46 +1129,3 @@ rels *encode_rel(sokoban_screen *screen) return rls; } - -int -test_relprod() -{ - LACE_ME; - - BDDVAR vars[] = {0,2,4}; - BDDVAR all_vars[] = {0,1,2,3,4,5}; - BDDVAR all_vars2[] = {0,1}; - //BDDVAR short_vars[] = {0,1}; - /*BDDVAR short_vars2[] = {2,3}; - BDDVAR short_vars3[] = {0,1,2,3};*/ - - BDDSET vars_set = sylvan_set_fromarray(vars, 3); - BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 6); - BDDSET all_vars_set2 = sylvan_set_fromarray(all_vars2, 2); - //BDDSET short_vars_set = sylvan_set_fromarray(short_vars, 2); - /*BDDSET short_vars_set2 = sylvan_set_fromarray(short_vars2, 2); - BDDSET short_vars_set3 = sylvan_set_fromarray(short_vars3, 4);*/ - - BDD s, t, next, prev; - BDD zeroes, ones; - - // transition relation: 000 --> 111 and !000 --> 000 - t = sylvan_false; - t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){0,1})); - //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0})); - t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){1,0})); - // t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1})); - - s = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); - zeroes = sylvan_cube(vars_set, (uint8_t[]){1,0,0}); - ones = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); - - next = sylvan_relnext(s, t, all_vars_set); - prev = sylvan_relprev(t, next, all_vars_set); - if (next == zeroes) printf("Pass 1\n"); - if (prev == ones) printf("Pass 2\n"); - //trans *ts; - //ts = NULL; - - return 0; -}