initial state encoding done, I think

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 02cda40..e954c07 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -48,9 +48,9 @@ void solve(FILE *inputstream)
        time_start_read = clock();
        sokoban_screen *screen = parse_screen(inputstream);
        if (screen == NULL) printf("Something went wrong...\n");
-       sokoban_print(screen);
-
+       //sokoban_print(screen);
        time_end_read = clock();
+
        time_start_encode = clock();
 
        lace_init(0, 1000000);

diff --git a/modelchecker/object.c b/modelchecker/object.c
index 5829ed3..769163f 100644 (file)
--- a/modelchecker/object.c
+++ b/modelchecker/object.c
@@ -1,11 +1,99 @@
 #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)
+
+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 = (sokoban_screen *)(r->hh.next)){
+               *mx = r->coord.x > *mx ? r->coord.x : *mx;
+               *my = r->coord.x > *mx ? r->coord.x : *mx;
+               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:;
+               }
+       }
+}
+
+BDD encode_int(BDD state, int x, int bx, int *variablenum)
+{
+       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));
+               } else {
+                       state = sylvan_and(state, sylvan_nithvar(*variablenum));
+               }
+               *variablenum += 1;
+       }
+       free(encoding);
+       return state;
+}
+
+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);
+}
+
+/*
+ * 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)
 {
-       BDD state = sylvan_false;
+       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 state = sylvan_true;
+       state = encode_position(state, agentx, agenty, wx, wy, &varnum);
+       for(int i = 0; i<nboxes; i++){
+               state = encode_position(state, boxx[i], boxy[i], wx, wy, &varnum);
+       }
+       
        return state;
-       (void) screen; //To avoid not used error
 }