#include "coord.h"
#include "sokoban.h"
+#include "deque.h"
typedef struct {
return fullState;
}
+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;
+}
+
+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;
+}
+
+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;
+}
+
+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);
+
+ 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));
+ 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;
+ 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;
+ }
+ }
+ }
+
+ 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;
+ }
+ }
+ }
+
+ 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){
+ 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, '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));
+
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'r');
+ new_state->lrd = lrd;
+ return new_state;
+ }
+ }
+ }
+
+
+ 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];
+
+ 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;
+ }
+ }
+ s = sylvan_cube(varset, st_enc);
+ fullState->bdd = s;
+ printf("Goal state encoded\n");
+ if (targets == 0 || (boxes != targets)) return NULL;
+ else return fullState;
+
+}
+
//test
-int countTrans(trans_t *trs);
+//int countTrans(trans_t *trs);
trans_t *create_single_rel(sokoban_screen *screen, direction dir)
{
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 = 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];
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 < deltai){
+ 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));
}
trs = trs_current;
//Agent Target -> Free Targagent
- //(1 0 0 0 1 1 - 0 1 1 1 1 0)
+ //(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)
+ //(0 1 1 1 1 0 1 0 0 0 1 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
//or
//(0 1 0 0 1 1 1 0 1 1 0 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
//or
//(0 1 1 1 1 0 1 0 1 1 0 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
//or
//(0 0 1 1 0 0 1 1 0 0 1 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
//
//(1 1 0 0 0 0 1 1 0 0 1 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
//or
//(0 0 1 1 0 0 1 1 1 1 0 0)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
//or
//(1 1 0 0 0 0 1 1 1 1 0 0)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
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 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 < deltai){
+ 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));
}
//or
//(0 1 1 1 1 0 1 0 0 0 1 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
//or
//(0 1 0 0 1 1 1 0 1 1 0 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
//or
//(0 1 1 1 1 0 1 0 1 1 0 1)
relvarset = sylvan_set_fromarray(relvars, 12);
- if (i < deltai){
+ 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));
}
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)
+ //(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)
+ //(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)
+ //(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)
+ //(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)
+ //(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)
+ //(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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
- uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
+ 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] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+ 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 = 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)
+ //(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)
+ //(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)
+ //(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)
+ //(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)
+ //(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)
+ //(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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
+ 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));
}
//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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
+ 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));
}
//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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
+ 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));
}
//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 < deltai) < gammai){
+ 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) < i){
+
+ 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) < deltai){
+
+ 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 < gammai) < deltai){
+
+ 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) < gammai){
+ 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));
}
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;
//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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
+ 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));
}
//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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
+ 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));
}
//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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
+ 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));
}
//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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
+ 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));
}
//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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
- uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
+ 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 {
//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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
+ 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));
}
//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 < deltai) < gammai){
+ 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) < i){
+ 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) < deltai){
+ 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 < gammai) < deltai){
+ 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) < gammai){
+ 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] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
+ 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->next_rel = trs;
trs = trs_current;
}
+
}
trs_current = trs;
}
//test
+/*
int countTrans(trans_t *trs)
{
int counter = 0;
}
return counter;
}
-
+*/
rels *encode_rel(sokoban_screen *screen)
{
LACE_ME;
int test_trans(state *s, trans_t *t)
{
LACE_ME;
- int counter = 0;
BDD next = sylvan_false;
while (t != NULL){
next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset);
if (next == sylvan_false) printf("False\n");
t = t->next_rel;
}
- printf("Trans:%d\n", counter);
return 1;
}
repositories / mc1516pa.git / blobdiff