X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fobject.c;h=362802d9f2a9c1ce8ac3f1c8adeade8b26e96ac9;hb=0212b386d85354399a194538538c0da541e987ea;hp=5829ed3331f4f69a32ea1ebf60dd0ef1815c25e7;hpb=b29982e8181d823142ce12b6d582181937fba7ad;p=mc1516pa.git

diff --git a/modelchecker/object.c b/modelchecker/object.c
index 5829ed3..362802d 100644
--- a/modelchecker/object.c
+++ b/modelchecker/object.c
@@ -1,11 +1,202 @@
 #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;
 }