#include <sylvan.h>
+#include <stdbool.h>
#include "object.h"
#include "sokoban.h"
-BDD solve_object(sokoban_screen *screen)
+#define MAX_BOX 50
+#define EPRINTF(fmt, as...) fprintf(stderr, fmt, ##as)
+
+typedef enum {UP, DOWN, LEFT, RIGHT} direction;
+
+int ilog2(int x)
+{
+ int l = 1;
+ while((x >>= 1) >= 1)
+ l++;
+ return l;
+}
+
+void get_screen_metrics(sokoban_screen *screen,
+ int *boxes,
+ int *mx, int *my,
+ int *agentx, int *agenty,
+ int *boxxes, int *boxyes)
+{
+ *boxes = 0;
+ *mx = 0;
+ *my = 0;
+ *agentx = 0;
+ *agenty = 0;
+ sokoban_screen *r;
+ for(r=screen; r != NULL; r = r->hh.next){
+ *mx = r->coord.x > *mx ? r->coord.x : *mx;
+ *my = r->coord.y > *my ? r->coord.x : *my;
+ switch(r->tile){
+ case TARGAGENT:
+ case AGENT:
+ *agentx = r->coord.x;
+ *agenty = r->coord.y;
+ break;
+ case TARGBOX:
+ case BOX:
+ boxxes[*boxes] = r->coord.x;
+ boxyes[*boxes] = r->coord.y;
+ *boxes += 1;
+ break;
+ default:;
+ }
+ }
+}
+
+//LSB first
+BDD encode_int(BDD state, int x, int bx, int *variablenum)
{
- BDD state = sylvan_false;
+ LACE_ME;
+ char *encoding = malloc(bx);
+ for(int i = 0; i<bx; i++){
+ if((x & (1<<i)) > 0){
+ state = sylvan_and(state, sylvan_ithvar(*variablenum*2));
+ } else {
+ state = sylvan_and(state, sylvan_nithvar(*variablenum*2));
+ }
+ *variablenum += 1;
+ }
+ free(encoding);
return state;
- (void) screen; //To avoid not used error
+}
+
+BDD encode_position(BDD state, int x, int y, int bx, int by, int *variablenum)
+{
+ state = encode_int(state, x, bx, variablenum);
+ return encode_int(state, y, by, variablenum);
+}
+
+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);
+}
+
+/*
+ * We have variables numbered 1...
+ * Per coordinate we need k=bitsx+bitsy variables
+ *
+ * agent: 0 till k
+ * box_i: k+k*i till k+k*(i+1)
+ * We start with the agent
+ */
+BDD solve_object(sokoban_screen *scr)
+{
+ LACE_ME;
+ int nboxes, mx, my, wx, wy, agentx, agenty;
+ int varnum = 0;
+ int boxx[MAX_BOX];
+ int boxy[MAX_BOX];
+
+ get_screen_metrics(scr, &nboxes, &mx, &my, &agentx, &agenty, boxx, boxy);
+
+ EPRINTF("Max x: %d, thus %d bits\n", mx, (wx = ilog2(mx)));
+ EPRINTF("Max y: %d, thus %d bits\n", my, (wy = ilog2(my)));
+ EPRINTF("%d boxes\n", nboxes);
+
+ BDD init = encode_position(sylvan_true, agentx, agenty, wx, wy, &varnum);
+ for(int i = 0; i<nboxes; i++){
+ init = encode_position(init, boxx[i], boxy[i], wx, wy, &varnum);
+ }
+
+ varnum = 0;
+ BDD trans_r = encode_transition(scr, sylvan_true, mx, my, &varnum, RIGHT);
+ varnum = 0;
+ BDD trans_l = encode_transition(scr, sylvan_true, mx, my, &varnum, LEFT);
+ varnum = 0;
+ BDD trans_d = encode_transition(scr, sylvan_true, mx, my, &varnum, DOWN);
+ varnum = 0;
+ BDD trans_u = encode_transition(scr, sylvan_true, mx, my, &varnum, UP);
+
+ BDD old = sylvan_false;
+ BDD new = init;
+ int iteration = 0;
+ while(new != old){
+ EPRINTF("Iteration %d\n", iteration++);
+ old = new;
+ new = sylvan_or(new, sylvan_relnext(new, trans_d, false));
+ new = sylvan_or(new, sylvan_relnext(new, trans_r, false));
+ new = sylvan_or(new, sylvan_relnext(new, trans_u, false));
+ new = sylvan_or(new, sylvan_relnext(new, trans_l, false));
+ sylvan_printdot_nc(old);
+ }
+
+ return init;
}
repositories / mc1516pa.git / blobdiff