10 #include <gperftools/profiler.h>
21 * Global TODOs for now:
22 * - update the helper maps so it is a single bimap
23 * - make a data structure for relations
24 * - encode relations as a set of four relations for each move
60 xy_bddvar_map
*getxy(int x
, int y
, xy_bddvar_map
*map
)
62 xy_bddvar_map k
, *r
= NULL
;
63 memset(&k
, 0, sizeof(xy_bddvar_map
));
66 HASH_FIND(hh
, map
, &k
.key
, sizeof(xy
), r
);
70 bddvar_xy_map
*getbdd(int key
, bddvar_xy_map
*map
)
72 bddvar_xy_map k
, *r
= NULL
;
73 memset(&k
, 0, sizeof(bddvar_xy_map
));
75 HASH_FIND(hh
, map
, &k
.key
, sizeof(int), r
);
80 xy_bddvar_map *create_xy_bddvar_map(sokoban_screen *screen)
84 xy_bddvar_map *xybdd = NULL;
85 for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
86 xy_bddvar_map *f = NULL;
87 //bddvar_xy_map *t = NULL;
89 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
90 memset(f, 0, sizeof(xy_bddvar_map));
91 f->key.x = r->coord.x;
92 f->key.y = r->coord.y;
93 f->value.var[0] = varcount;
94 f->value.var[1] = varcount + 1;
95 f->value.var[2] = varcount + 2;
96 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
97 varcount = varcount + 3;
102 bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen)
106 bddvar_xy_map *bddxy = NULL;
107 for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
108 for (int i = 0; i <3; i++){
109 bddvar_xy_map *f = NULL;
110 //bddvar_xy_map *t = NULL;
112 f = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
113 memset(f, 0, sizeof(bddvar_xy_map));
114 f->key = varcount + i;
115 f->value.x = r->coord.x;
116 f->value.y = r->coord.y;
117 HASH_ADD(hh, bddxy, key, sizeof(int), f);
119 varcount = varcount + 3;
125 bimap
*create_bimap_helper(sokoban_screen
*screen
)
129 xy_bddvar_map
*xybdd
= NULL
;
130 bddvar_xy_map
*bddxy
= NULL
;
131 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
132 xy_bddvar_map
*f
= NULL
;
133 f
= (xy_bddvar_map
*)malloc(sizeof(xy_bddvar_map
));
134 memset(f
, 0, sizeof(xy_bddvar_map
));
135 f
->key
.x
= r
->coord
.x
;
136 f
->key
.y
= r
->coord
.y
;
137 f
->value
.var
[0] = varcount
;
138 f
->value
.var
[1] = varcount
+ 1;
139 f
->value
.var
[2] = varcount
+ 2;
140 HASH_ADD(hh
, xybdd
, key
, sizeof(xy
), f
);
142 for (int i
= 0; i
<3; i
++){
143 bddvar_xy_map
*t
= NULL
;
144 t
= (bddvar_xy_map
*)malloc(sizeof(bddvar_xy_map
));
145 memset(t
, 0, sizeof(bddvar_xy_map
));
146 t
->key
= varcount
+ i
;
147 t
->value
.x
= r
->coord
.x
;
148 t
->value
.y
= r
->coord
.y
;
149 HASH_ADD(hh
, bddxy
, key
, sizeof(int), t
);
151 varcount
= varcount
+ 3;
154 bm
= (bimap
*)malloc(sizeof(bimap
));
160 int check_xy_exists(int x
, int y
, bimap
*bm
)
163 if (getxy(x
, y
, bm
->f
) != NULL
) res
= 1;
167 int check_space(int x
, int y
, direction d
, int delta
, bimap
*bm
)
170 case LEFT
: x
= x
- delta
; break;
171 case UP
: y
= y
- delta
; break;
172 case RIGHT
: x
= x
+ delta
; break;
173 case DOWN
: y
= y
+ delta
; break;
175 return check_xy_exists(x
, y
, bm
);
179 * Each coordinate has three related boolean variables. The combination of those boolean variables
187 * 110: Agent on target
188 * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
189 * tiles in the shrinked screen.
190 * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
191 * directly in transition relations.
194 state
*encode_screen(sokoban_screen
*screen
)
198 BDDVAR vars
[HASH_COUNT(screen
) * 3];
199 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
203 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
205 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
207 state
*fullState
= NULL
;
208 fullState
= (state
*)malloc(sizeof(state
));
209 fullState
->vars
.varset
= varset
;
210 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
213 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
216 st_enc
[tile_index
] = 0;
218 st_enc
[tile_index
] = 0;
220 st_enc
[tile_index
] = 1;
224 st_enc
[tile_index
] = 0;
226 st_enc
[tile_index
] = 0;
228 st_enc
[tile_index
] = 0;
232 st_enc
[tile_index
] = 0;
234 st_enc
[tile_index
] = 1;
236 st_enc
[tile_index
] = 0;
240 st_enc
[tile_index
] = 0;
242 st_enc
[tile_index
] = 1;
244 st_enc
[tile_index
] = 1;
248 st_enc
[tile_index
] = 1;
250 st_enc
[tile_index
] = 0;
252 st_enc
[tile_index
] = 1;
255 case TARGAGENT
: //110
256 st_enc
[tile_index
] = 1;
258 st_enc
[tile_index
] = 1;
260 st_enc
[tile_index
] = 0;
264 st_enc
[tile_index
] = 1;
266 st_enc
[tile_index
] = 0;
268 st_enc
[tile_index
] = 0;
273 s
= sylvan_cube(varset
, st_enc
);
275 printf("Initial state encoded\n");
284 BDDVAR vars
[] = {0,2,4};
285 BDDVAR all_vars
[] = {4,5};
287 BDDSET vars_set
= sylvan_set_fromarray(vars
, 3);
288 BDDSET all_vars_set
= sylvan_set_fromarray(all_vars
, 2);
290 BDD s
, t
, next
, prev
;
293 // transition relation: 000 --> 111 and !000 --> 000
295 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1,0,1,0,1}));
296 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0}));
297 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){2,0,1,0,2,0}));
298 t
= sylvan_union_cube(t
, all_vars_set
, ((uint8_t[]){1,0}));
300 s
= sylvan_cube(vars_set
, (uint8_t[]){0,0,1});
301 zeroes
= sylvan_cube(vars_set
, (uint8_t[]){0,0,0});
302 ones
= sylvan_cube(vars_set
, (uint8_t[]){0,0,1});
304 next
= sylvan_relnext(s
, t
, all_vars_set
);
305 prev
= sylvan_relprev(t
, next
, all_vars_set
);
306 if (next
== zeroes
) printf("Pass 1\n");
307 if (prev
== ones
|| prev
== zeroes
) printf("Pass 2\n");
312 BDD
encode_rel(sokoban_screen
*screen
)
315 BDD t
= sylvan_false
;
319 bimap
*bm
= create_bimap_helper(screen
);
322 bddvar_xy_map
*bddxy
= NULL
;
323 tmp_scr
*screen
= NULL
;
324 tmp_scr_d
*screen
= NULL
;
325 tmp_scr_g
*screen
= NULL
;
328 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
330 bddxy
= getbdd(i
*3, bm
->t
);
333 if (check_space(x
, y
, LEFT
, 1, bm
) == 0){
334 tmp_scr
= get_coord(x
, y
, screen
);
335 if (tmp_scr
->tile
== AGENT
){
338 if (tmp_scr
->tile
== TARGAGENT
){
342 else if (check_space(x
, y
, LEFT
, 1, bm
) == 1 && check_space(x
, y
, LEFT
, 2, bm
) == 0){
343 tmp_scr
= get_coord(x
, y
, screen
);
344 tmp_scr_d
= get_coord(x
- 1, y
, screen
);
345 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== FREE
){
348 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGET
){
351 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== FREE
){
354 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGET
){
357 if (tmp_scr
->tile
== AGENT
&& (tmp_scr_d
->tile
== BOX
|| tmp_scr_d
->tile
== TARGBOX
)){
360 if (tmp_scr
->tile
== TARGAGENT
&& (tmp_scr_d
->tile
== BOX
|| tmp_scr_d
->tile
== TARGBOX
)){
364 else if (check_space(x
, y
, LEFT
, 1, bm
) == 1 && check_space(x
, y
, LEFT
, 2, bm
) == 1){
365 tmp_scr
= get_coord(x
, y
, screen
);
366 tmp_scr_d
= get_coord(x
- 1, y
, screen
);
367 tmp_scr_g
= get_coord(x
- 2, y
, screen
);
368 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== FREE
){
371 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGET
){
374 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== FREE
){
377 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGET
){
380 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
-> tile
== BOX
&& (tmp_scr_g
->tile
== BOX
|| tmp_scr_g
== TARGBOX
)){
383 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
-> tile
== BOX
&& (tmp_scr_g
->tile
== BOX
|| tmp_scr_g
== TARGBOX
)){
386 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== FREE
){
389 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== FREE
){
392 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== TARGET
){
395 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== TARGET
){
398 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== FREE
){
401 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== FREE
){
404 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== TARGET
){
407 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== TARGET
){
411 printf("x:%d y:%d\n", x
, y
);