#include <argp.h>
-#include <inttypes.h>
-#include <locale.h>
#include <stdio.h>
#include <stdlib.h>
-#include <string.h>
-#include <sys/time.h>
-
-#ifdef HAVE_PROFILER
-#include <gperftools/profiler.h>
-#endif
-
#include <sylvan.h>
-#include <llmsset.h>
#include <lace.h>
#include "coord.h"
#include "sokoban.h"
+#include "deque.h"
+
+
+typedef struct {
+ int x;
+ int y;
+} xy;
+
+typedef struct {
+ int var[3];
+} bddvar;
+
+typedef struct {
+ xy key;
+ bddvar value;
+ UT_hash_handle hh;
+} xy_bddvar_map;
+
+typedef struct {
+ int key;
+ xy value;
+ UT_hash_handle hh;
+} bddvar_xy_map;
+
+typedef struct {
+ xy_bddvar_map *f;
+ bddvar_xy_map *t;
+} bimap;
+
+xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
+{
+ xy_bddvar_map k, *r = NULL;
+ memset(&k, 0, sizeof(xy_bddvar_map));
+ k.key.x = x;
+ k.key.y = y;
+ HASH_FIND(hh, map, &k.key, sizeof(xy), r);
+ return r;
+}
+
+bddvar_xy_map *getbdd(int key, bddvar_xy_map *map)
+{
+ bddvar_xy_map k, *r = NULL;
+ memset(&k, 0, sizeof(bddvar_xy_map));
+ k.key = key;
+ HASH_FIND(hh, map, &k.key, sizeof(int), r);
+ return r;
+}
+
+
+bimap *create_bimap_helper(sokoban_screen *screen)
+{
+ int varcount = 0;
+ sokoban_screen *r;
+ xy_bddvar_map *xybdd = NULL;
+ bddvar_xy_map *bddxy = NULL;
+ for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
+ xy_bddvar_map *f = NULL;
+ f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
+ memset(f, 0, sizeof(xy_bddvar_map));
+ f->key.x = r->coord.x;
+ f->key.y = r->coord.y;
+ 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) * 2;
+ t->value.x = r->coord.x;
+ t->value.y = r->coord.y;
+ HASH_ADD(hh, bddxy, key, sizeof(int), t);
+ }
+ varcount = varcount + 3;
+ }
+ bimap *bm = NULL;
+ bm = (bimap *)malloc(sizeof(bimap));
+ bm->f = xybdd;
+ bm->t = bddxy;
+ return bm;
+}
+
+int check_xy_exists(int x, int y, bimap *bm)
+{
+ int res = 0;
+ if (getxy(x, y, bm->f) != NULL) res = 1;
+ return res;
+}
+
+int check_space(int x, int y, direction d, int delta, bimap *bm)
+{
+ switch(d){
+ case LEFT: x = x - delta; break;
+ case UP: y = y - delta; break;
+ case RIGHT: x = x + delta; break;
+ case DOWN: y = y + delta; break;
+ }
+ return check_xy_exists(x, y, bm);
+}
/*
* Each coordinate has three related boolean variables. The combination of those boolean variables
* directly in transition relations.
*/
-BDD encode_screen(sokoban_screen *screen)
+state *encode_screen(sokoban_screen *screen)
{
- BDD state = sylvan_false;
- //int tile_index = 0;
+ 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;
sokoban_screen *r;
for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
switch(r->tile){
- case FREE:
- if (state == sylvan_false){
-
- }
- else {
+ case FREE: //001
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 1;
+ tile_index++;
+ 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++;
+ 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++;
+ 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++;
+ break;
+ case AGENT: //101
+ st_enc[tile_index] = 1;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
- }
- printf("x = %d y = %d FREE\n", r->coord.x, r->coord.y);
+ st_enc[tile_index] = 1;
+ tile_index++;
break;
- case WALL:
- if (state == sylvan_false){
+ case TARGAGENT: //110
+ st_enc[tile_index] = 1;
+ tile_index++;
+ st_enc[tile_index] = 1;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ 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++;
+ break;
+ }
+ }
+ s = sylvan_cube(varset, st_enc);
+ fullState->bdd = s;
+ printf("Initial state encoded\n");
+ return fullState;
+}
- }
- else {
+lurd_t *lappend(lurd_t *l, char c){
+ lurd_t *temp_lrd = NULL;
+ if (l == NULL){
+ temp_lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ temp_lrd->c = c;
+ temp_lrd->next = NULL;
+ l = temp_lrd;
+ }
+ else {
+ temp_lrd = l;
+ while (temp_lrd->next != NULL){
+ temp_lrd = temp_lrd->next;
+ }
+ temp_lrd->next = (lurd_t *)malloc(sizeof(lurd_t));
+ temp_lrd->next->c = c;
+ temp_lrd->next->next = NULL;
+ }
+ return l;
+}
- }
- printf("x = %d y = %d WALL\n", r->coord.x, r->coord.y);
- break;
- case BOX:
- if (state == sylvan_false){
+int check_goal(BDD s, BDD g, BDDSET vars){
+ LACE_ME;
+ if(sylvan_satcount(sylvan_and(s, g), vars) > 0) return 1;
+ else return 0;
+}
- }
- else {
+int check_visited(BDD s, BDD v, BDDSET vars){
+ LACE_ME;
+ if(sylvan_satcount(sylvan_and(s, v), vars) > 0) return 1;
+ else return 0;
+}
- }
- printf("x = %d y = %d BOX\n", r->coord.x, r->coord.y);
- break;
- case TARGET:
- if (state == sylvan_false){
+state_t *explstate(state *init, rels *rls, state *g){
+ LACE_ME;
+ deque *state_queue = create();
+ trans_t *t = NULL;
+ state_t *tmp_state = (state_t *)malloc(sizeof(state_t));
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ //state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ BDD visited = init->bdd;
+ BDD new;
+ tmp_state->bdd = init->bdd;
+ tmp_state->vars = init->vars;
+ tmp_state->lrd = lrd;
+ state_queue = enq(tmp_state, state_queue);
- }
- else {
+ while (isEmpty(state_queue) == 0){
+ tmp_state = get_front(state_queue);
+ state_queue = deq(state_queue);
+ new = tmp_state->bdd;
+ t = rls->rell;
+ while (t != NULL){
+ new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+ if (new != sylvan_false && new != tmp_state->bdd) break;
+ t = t->next_rel;
+ }
+ if (new != sylvan_false && new != tmp_state->bdd){
+ if (check_visited(new, visited, init->vars.varset) == 0){
+ if (check_goal(new, g->bdd, init->vars.varset) == 0){
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ printf("here1\n");
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+ printf("here2\n");
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'l');
+ new_state->lrd = lrd;
+ state_queue = enq(new_state, state_queue);
+ visited = sylvan_or(new, visited);
+ }
+ else {
+ printf("GOAL\n");
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'l');
+ new_state->lrd = lrd;
+ return new_state;
+ }
+ }
+ }
- }
- printf("x = %d y = %d TARGET\n", r->coord.x, r->coord.y);
- break;
- case AGENT:
- if (state == sylvan_false){
+ t = rls->relu;
+ while (t != NULL){
+ new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+ if (new != sylvan_false && new != tmp_state->bdd) break;
+ t = t->next_rel;
+ }
+ if (new != sylvan_false && new != tmp_state->bdd){
+ if (check_visited(new, visited, init->vars.varset) == 0){
+ if (check_goal(new, g->bdd, init->vars.varset) == 0){
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'u');
+ new_state->lrd = lrd;
+ state_queue = enq(new_state, state_queue);
+ visited = sylvan_or(new, visited);
+ }
+ else {
+ printf("GOAL\n");
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'u');
+ new_state->lrd = lrd;
+ return new_state;
+ }
+ }
+ }
- }
- else {
+ t = rls->relr;
+ while (t != NULL){
+ new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+ if (new != sylvan_false && new != tmp_state->bdd) break;
+ t = t->next_rel;
+ }
+ if (new != sylvan_false && new != tmp_state->bdd){
+ if (check_visited(new, visited, init->vars.varset) == 0){
+ if (check_goal(new, g->bdd, init->vars.varset) == 0){
+ printf("Here1\n");
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+ printf("Here2\n");
- }
- printf("x = %d y = %d AGENT\n", r->coord.x, r->coord.y);
- break;
- case TARGAGENT:
- if (state == sylvan_false){
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'r');
+ new_state->lrd = lrd;
+ state_queue = enq(new_state, state_queue);
+ visited = sylvan_or(new, visited);
+ }
+ else {
+ printf("GOAL\n");
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
- }
- else {
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'r');
+ new_state->lrd = lrd;
+ return new_state;
+ }
+ }
+ }
- }
- printf("x = %d y = %d TARGAGENT\n", r->coord.x, r->coord.y);
- break;
- case TARGBOX:
- if (state == sylvan_false){
- }
- else {
+ t = rls->reld;
+ while (t != NULL){
+ new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+ if (new != sylvan_false && new != tmp_state->bdd) break;
+ t = t->next_rel;
+ }
+ if (new != sylvan_false && new != tmp_state->bdd){
+ if (check_visited(new, visited, init->vars.varset) == 0){
+ if (check_goal(new, g->bdd, init->vars.varset) == 0){
+
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'd');
+ new_state->lrd = lrd;
+ state_queue = enq(new_state, state_queue);
+ visited = sylvan_or(new, visited);
+ }
+ else {
+ printf("GOAL\n");
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'd');
+ new_state->lrd = lrd;
+ return new_state;
+ }
+ }
+ }
+
+
+ }
+
+ return NULL;
+}
+
+state *encode_goal(sokoban_screen *screen){
+ int boxes = 0;
+ int targets = 0;
+
+ 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];
- }
- printf("x = %d y = %d TARGBOX\n", r->coord.x, r->coord.y);
+ 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;
+ sokoban_screen *r;
+ for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
+ switch(r->tile){
+ case FREE: //001 -> any
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ break;
+ case WALL: //000 -> stays the same
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ break;
+ case BOX: //010 -> any
+ boxes++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ break;
+ case TARGET: //011 -> targbox
+ targets++;
+ st_enc[tile_index] = 1;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ break;
+ case AGENT: //101 -> any
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ st_enc[tile_index] = 2;
+ tile_index++;
+ break;
+ case TARGAGENT: //110 -> targbox
+ targets++;
+ st_enc[tile_index] = 1;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ break;
+ case TARGBOX: //100 -> stays the same
+ targets++;
+ boxes++;
+ st_enc[tile_index] = 1;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
+ st_enc[tile_index] = 0;
+ tile_index++;
break;
}
}
- return state;
-}
+ s = sylvan_cube(varset, st_enc);
+ fullState->bdd = s;
+ printf("Goal state encoded\n");
+ if (targets == 0 || (boxes != targets)) return NULL;
+ else return fullState;
-BDD encode_rel(sokoban_screen *screen)
-{
- int num_tiles;
- num_tiles = HASH_COUNT(screen);
- printf("Number of tiles: %d\n", num_tiles);
- return sylvan_true;
}
-void test()
+//test
+//int countTrans(trans_t *trs);
+
+trans_t *create_single_rel(sokoban_screen *screen, direction dir)
{
+ LACE_ME;
+ trans_t *trs, *trs_current;
+ bimap *bm = create_bimap_helper(screen);
+ int x = 0;
+ int y = 0;
+ bddvar_xy_map *bddxy = NULL;
+ int xdelta = 0;
+ int ydelta = 0;
+ int xgamma = 0;
+ int ygamma = 0;
+ trs = NULL;
+ switch(dir){
+ case LEFT:
+ xdelta = -1;
+ ydelta = 0;
+ xgamma = -2;
+ ygamma = 0;
+ break;
+ case UP:
+ xdelta = 0;
+ ydelta = -1;
+ xgamma = 0;
+ ygamma = -2;
+ break;
+ case RIGHT:
+ xdelta = 1;
+ ydelta = 0;
+ xgamma = 2;
+ ygamma = 0;
+ break;
+ case DOWN:
+ xdelta = 0;
+ ydelta = 1;
+ xgamma = 0;
+ ygamma = 2;
+ break;
+ }
+
+ for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
+ 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 * 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;
+ trs_current->varset.size = 6;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //Targagent -> Targagent
+ //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
+ relvarset = sylvan_set_fromarray(relvars, 6);
+ 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);
+ trs_current->varset.varset = relvarset;
+ trs_current->varset.size = 6;
+ 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){
+ xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
+ 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];
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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){
+ xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
+ unsigned int deltai = bddvar->value.var[0];
+ bddvar = getxy(x + xgamma, y + ygamma, bm->f);
+ 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];
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 12;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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];
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+
+ //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);
+ 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;
+ trs_current->varset.size = 18;
+ trs_current->next_rel = trs;
+ trs = trs_current;
+ }
- printf("Test!\n");
- BDD a = sylvan_true;
- BDD b = sylvan_not(a);
- if (b == sylvan_false){
- printf("BDD works!\n");
- } else {
- printf("BDD does not work!\n");
}
+ trs_current = trs;
+
+ //test
+ /*
+ switch(dir){
+ case LEFT:
+ if (trs_current != NULL) printf("LEFT ok!\n");
+ else printf ("LEFT is empty\n");
+ printf("Num of trans relations:%d\n", countTrans(trs));
+ break;
+ case UP:
+ if (trs_current != NULL) printf("UP ok!\n");
+ else printf ("UP is empty\n");
+ printf("Num of trans relations:%d\n", countTrans(trs));
+ break;
+ case RIGHT:
+ if (trs_current != NULL) printf("RIGHT ok!\n");
+ else printf ("RIGHT is empty\n");
+ printf("Num of trans relations:%d\n", countTrans(trs));
+ break;
+ case DOWN:
+ if (trs_current != NULL) printf("DOWN ok!\n");
+ else printf ("DOWN is empty\n");
+ printf("Num of trans relations:%d\n", countTrans(trs));
+ break;
+ }
+ */
+ return trs;
+}
+
+//test
+/*
+int countTrans(trans_t *trs)
+{
+ int counter = 0;
+ while (trs != NULL){
+ counter++;
+ trs = trs->next_rel;
+ }
+ return counter;
+}
+*/
+rels *encode_rel(sokoban_screen *screen)
+{
LACE_ME;
- BDD c = sylvan_ithvar(1);
- if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n");
- if (sylvan_var(c) == 1) printf("Var works 2\n");
+
+ trans_t *tl = sylvan_false;
+
+ //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;
+ rls = (rels *)malloc(sizeof(rels));
+ rls->rell = tl;
+ rls->relu = tu;
+ rls->relr = tr;
+ rls->reld = td;
+
+ return rls;
+}
+
+int test_trans(state *s, trans_t *t)
+{
+ LACE_ME;
+ BDD next = sylvan_false;
+ while (t != NULL){
+ next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset);
+ if (next == s->bdd) printf("Same\n");
+ if (next != s->bdd && next != sylvan_false) printf("Different\n");
+ if (next == sylvan_false) printf("False\n");
+ t = t->next_rel;
+ }
+ return 1;
}