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 int ilog2(int x)
  11 {
  12         int l = 1;
  13         while((x >>= 1) >= 1)
  14                 l++;
  15         return l;
  16 }
  17
  18 void get_screen_metrics(sokoban_screen *screen,
  19                 int *boxes,
  20                 int *mx, int *my,
  21                 int *agentx, int *agenty,
  22                 int *boxxes, int *boxyes)
  23 {
  24         *boxes = 0;
  25         *mx = 0;
  26         *my = 0;
  27         *agentx = 0;
  28         *agenty = 0;
  29         sokoban_screen *r;
  30         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
  31                 *mx = r->coord.x > *mx ? r->coord.x : *mx;
  32                 *my = r->coord.x > *mx ? r->coord.x : *mx;
  33                 switch(r->tile){
  34                 case TARGAGENT:
  35                 case AGENT:
  36                         *agentx = r->coord.x;
  37                         *agenty = r->coord.y;
  38                         break;
  39                 case TARGBOX:
  40                 case BOX:
  41                         boxxes[*boxes] = r->coord.x;
  42                         boxyes[*boxes] = r->coord.y;
  43                         *boxes += 1;
  44                         break;
  45                 default:;
  46                 }
  47         }
  48 }
  49
  50 BDD encode_int(BDD state, int x, int bx, int *variablenum)
  51 {
  52         LACE_ME;
  53         char *encoding = malloc(bx);
  54         for(int i = 0; i<bx; i++){
  55                 if((x & (1<<i)) > 0){
  56                         state = sylvan_and(state, sylvan_ithvar(*variablenum));
  57                 } else {
  58                         state = sylvan_and(state, sylvan_nithvar(*variablenum));
  59                 }
  60                 *variablenum += 1;
  61         }
  62         free(encoding);
  63         return state;
  64 }
  65
  66 BDD encode_position(BDD state, int x, int y, int bx, int by, int *variablenum)
  67 {
  68         state = encode_int(state, x, bx, variablenum);
  69         return encode_int(state, y, by, variablenum);
  70 }
  71
  72 /*
  73  * We have variables numbered 1...
  74  * Per coordinate we need k=bitsx+bitsy variables
  75  *
  76  * agent: 0     till k
  77  * box_i: k+k*i till k+k*(i+1)
  78  * We start with the agent
  79  */
  80 BDD solve_object(sokoban_screen *scr)
  81 {
  82         int nboxes, mx, my, wx, wy, agentx, agenty;
  83         int varnum = 0;
  84         int boxx[MAX_BOX];
  85         int boxy[MAX_BOX];
  86         get_screen_metrics(scr, &nboxes, &mx, &my, &agentx, &agenty, boxx, boxy);
  87
  88         EPRINTF("Max x: %d, thus %d bits\n", mx, (wx = ilog2(mx)));
  89         EPRINTF("Max y: %d, thus %d bits\n", my, (wy = ilog2(my)));
  90         EPRINTF("%d boxes\n", nboxes);
  91
  92         BDD state = sylvan_true;
  93         state = encode_position(state, agentx, agenty, wx, wy, &varnum);
  94         for(int i = 0; i<nboxes; i++){
  95                 state = encode_position(state, boxx[i], boxy[i], wx, wy, &varnum);
  96         }
  97
  98         return state;
  99 }