+BDD encode_transition(sokoban_screen *scr, BDD state, int bx, int by, int *varnum, direction dir)
+{
+ LACE_ME;
+ //Increase the position
+ int oldvarnum = *varnum;
+
+ //RIGHT
+ if(dir == RIGHT){
+ state = sylvan_and(state,
+ sylvan_xor(sylvan_ithvar(*varnum*2), sylvan_ithvar(*varnum*2+1)));
+ *varnum += 1;
+ for(int i = 1; i<bx; i++){
+ state = sylvan_and(state,
+ sylvan_xor(sylvan_ithvar(*varnum*2-1),
+ sylvan_xor(sylvan_ithvar(*varnum*2),
+ sylvan_ithvar(*varnum*2+1))));
+ *varnum += 1;
+ }
+ } else if(dir == LEFT){
+ //TODO
+ *varnum += bx;
+ }else {
+ *varnum += bx;
+ }
+
+ //DOWN
+ if(dir == DOWN){
+ state = sylvan_and(state,
+ sylvan_xor(sylvan_ithvar(*varnum*2), sylvan_ithvar(*varnum*2+1)));
+ *varnum += 1;
+ for(int i = 1; i<by; i++){
+ state = sylvan_and(state,
+ sylvan_xor(sylvan_ithvar(*varnum*2-1),
+ sylvan_xor(sylvan_ithvar(*varnum*2),
+ sylvan_ithvar(*varnum*2+1))));
+ *varnum += 1;
+ }
+ } else if(dir == UP){
+ //TODO
+ *varnum += by;
+ } else {
+ *varnum += by;
+ }
+
+ //Check wether it is a valid position
+ BDD legalpos = sylvan_false;
+ for(sokoban_screen *r=scr; r != NULL; r = r->hh.next){
+ int x = r->coord.x;
+ int y = r->coord.y;
+ *varnum = oldvarnum;
+
+ BDD currentx = sylvan_true;
+ for(int i = 0; i<bx; i++){
+ if((x & (1<<i)) > 0){
+ currentx = sylvan_and(currentx, sylvan_ithvar(*varnum*2+1));
+ } else {
+ currentx = sylvan_and(currentx, sylvan_nithvar(*varnum*2+1));
+ }
+ *varnum += 1;
+ }
+
+ BDD currenty = sylvan_true;
+ for(int i = 0; i<by; i++){
+ if((y & (1<<i)) > 0){
+ currenty = sylvan_and(currenty, sylvan_ithvar(*varnum*2+1));
+ } else {
+ currenty = sylvan_and(currenty, sylvan_nithvar(*varnum*2+1));
+ }
+ *varnum += 1;
+ }
+ legalpos = sylvan_or(legalpos,
+ sylvan_and(currentx, currenty));
+ }
+
+ return sylvan_and(state, legalpos);
+}
+