modelchecker/object.c

   1 #include <sylvan.h>
   2 #include <stdbool.h>
   3
   4 #include "object.h"
   5 #include "sokoban.h"
   6
   7 #define MAX_BOX 50
   8 #define EPRINTF(fmt, as...) fprintf(stderr, fmt, ##as)
   9
  10 typedef enum {UP, DOWN, LEFT, RIGHT} direction;
  11
  12 int ilog2(int x)
  13 {
  14         int l = 1;
  15         while((x >>= 1) >= 1)
  16                 l++;
  17         return l;
  18 }
  19
  20 void get_screen_metrics(sokoban_screen *screen,
  21                 int *boxes,
  22                 int *mx, int *my,
  23                 int *agentx, int *agenty,
  24                 int *boxxes, int *boxyes)
  25 {
  26         *boxes = 0;
  27         *mx = 0;
  28         *my = 0;
  29         *agentx = 0;
  30         *agenty = 0;
  31         sokoban_screen *r;
  32         for(r=screen; r != NULL; r = r->hh.next){
  33                 *mx = r->coord.x > *mx ? r->coord.x : *mx;
  34                 *my = r->coord.y > *my ? r->coord.x : *my;
  35                 switch(r->tile){
  36                 case TARGAGENT:
  37                 case AGENT:
  38                         *agentx = r->coord.x;
  39                         *agenty = r->coord.y;
  40                         break;
  41                 case TARGBOX:
  42                 case BOX:
  43                         boxxes[*boxes] = r->coord.x;
  44                         boxyes[*boxes] = r->coord.y;
  45                         *boxes += 1;
  46                         break;
  47                 default:;
  48                 }
  49         }
  50 }
  51
  52 //LSB first
  53 BDD encode_int(BDD state, int x, int bx, int *variablenum)
  54 {
  55         LACE_ME;
  56         char *encoding = malloc(bx);
  57         for(int i = 0; i<bx; i++){
  58                 if((x & (1<<i)) > 0){
  59                         state = sylvan_and(state, sylvan_ithvar(*variablenum*2));
  60                 } else {
  61                         state = sylvan_and(state, sylvan_nithvar(*variablenum*2));
  62                 }
  63                 *variablenum += 1;
  64         }
  65         free(encoding);
  66         return state;
  67 }
  68
  69 BDD encode_position(BDD state, int x, int y, int bx, int by, int *variablenum)
  70 {
  71         state = encode_int(state, x, bx, variablenum);
  72         return encode_int(state, y, by, variablenum);
  73 }
  74
  75 BDD encode_transition(sokoban_screen *scr, BDD state, int bx, int by, int *varnum, direction dir)
  76 {
  77         LACE_ME;
  78         //Increase the position
  79         int oldvarnum = *varnum;
  80
  81         //RIGHT
  82         if(dir == RIGHT){
  83                 state = sylvan_and(state,
  84                         sylvan_xor(sylvan_ithvar(*varnum*2), sylvan_ithvar(*varnum*2+1)));
  85                 *varnum += 1;
  86                 for(int i = 1; i<bx; i++){
  87                         state = sylvan_and(state,
  88                                 sylvan_xor(sylvan_ithvar(*varnum*2-1),
  89                                         sylvan_xor(sylvan_ithvar(*varnum*2),
  90                                                 sylvan_ithvar(*varnum*2+1))));
  91                         *varnum += 1;
  92                 }
  93         } else if(dir == LEFT){
  94                 //TODO
  95                 *varnum += bx;
  96         }else {
  97                 *varnum += bx;
  98         }
  99
 100         //DOWN
 101         if(dir == DOWN){
 102                 state = sylvan_and(state,
 103                         sylvan_xor(sylvan_ithvar(*varnum*2), sylvan_ithvar(*varnum*2+1)));
 104                 *varnum += 1;
 105                 for(int i = 1; i<by; i++){
 106                         state = sylvan_and(state,
 107                                 sylvan_xor(sylvan_ithvar(*varnum*2-1),
 108                                         sylvan_xor(sylvan_ithvar(*varnum*2),
 109                                                 sylvan_ithvar(*varnum*2+1))));
 110                         *varnum += 1;
 111                 }
 112         } else if(dir == UP){
 113                 //TODO
 114                 *varnum += by;
 115         } else {
 116                 *varnum += by;
 117         }
 118
 119         //Check wether it is a valid position
 120         BDD legalpos = sylvan_false;
 121         for(sokoban_screen *r=scr; r != NULL; r = r->hh.next){
 122                 int x = r->coord.x;
 123                 int y = r->coord.y;
 124                 *varnum = oldvarnum;
 125
 126                 BDD currentx = sylvan_true;
 127                 for(int i = 0; i<bx; i++){
 128                         if((x & (1<<i)) > 0){
 129                                 currentx = sylvan_and(currentx, sylvan_ithvar(*varnum*2+1));
 130                         } else {
 131                                 currentx = sylvan_and(currentx, sylvan_nithvar(*varnum*2+1));
 132                         }
 133                         *varnum += 1;
 134                 }
 135
 136                 BDD currenty = sylvan_true;
 137                 for(int i = 0; i<by; i++){
 138                         if((y & (1<<i)) > 0){
 139                                 currenty = sylvan_and(currenty, sylvan_ithvar(*varnum*2+1));
 140                         } else {
 141                                 currenty = sylvan_and(currenty, sylvan_nithvar(*varnum*2+1));
 142                         }
 143                         *varnum += 1;
 144                 }
 145                 legalpos = sylvan_or(legalpos,
 146                         sylvan_and(currentx, currenty));
 147         }
 148
 149         return sylvan_and(state, legalpos);
 150 }
 151
 152 /*
 153  * We have variables numbered 1...
 154  * Per coordinate we need k=bitsx+bitsy variables
 155  *
 156  * agent: 0     till k
 157  * box_i: k+k*i till k+k*(i+1)
 158  * We start with the agent
 159  */
 160 BDD solve_object(sokoban_screen *scr)
 161 {
 162         LACE_ME;
 163         int nboxes, mx, my, wx, wy, agentx, agenty;
 164         int varnum = 0;
 165         int boxx[MAX_BOX];
 166         int boxy[MAX_BOX];
 167
 168         get_screen_metrics(scr, &nboxes, &mx, &my, &agentx, &agenty, boxx, boxy);
 169
 170         EPRINTF("Max x: %d, thus %d bits\n", mx, (wx = ilog2(mx)));
 171         EPRINTF("Max y: %d, thus %d bits\n", my, (wy = ilog2(my)));
 172         EPRINTF("%d boxes\n", nboxes);
 173
 174         BDD init = encode_position(sylvan_true, agentx, agenty, wx, wy, &varnum);
 175         for(int i = 0; i<nboxes; i++){
 176                 init = encode_position(init, boxx[i], boxy[i], wx, wy, &varnum);
 177         }
 178
 179         varnum = 0;
 180         BDD trans_r = encode_transition(scr, sylvan_true, mx, my, &varnum, RIGHT);
 181         varnum = 0;
 182         BDD trans_l = encode_transition(scr, sylvan_true, mx, my, &varnum, LEFT);
 183         varnum = 0;
 184         BDD trans_d = encode_transition(scr, sylvan_true, mx, my, &varnum, DOWN);
 185         varnum = 0;
 186         BDD trans_u = encode_transition(scr, sylvan_true, mx, my, &varnum, UP);
 187
 188         BDD old = sylvan_false;
 189         BDD new = init;
 190         int iteration = 0;
 191         while(new != old){
 192                 EPRINTF("Iteration %d\n", iteration++);
 193                 old = new;
 194                 new = sylvan_or(new, sylvan_relnext(new, trans_d, false));
 195                 new = sylvan_or(new, sylvan_relnext(new, trans_r, false));
 196                 new = sylvan_or(new, sylvan_relnext(new, trans_u, false));
 197                 new = sylvan_or(new, sylvan_relnext(new, trans_l, false));
 198                 sylvan_printdot_nc(old);
 199         }
 200
 201         return init;
 202 }