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 // int tile_count = 0;
316 BDD t
= sylvan_false
;
321 bimap
*bm
= create_bimap_helper(screen
);
324 bddvar_xy_map
*bddxy
= NULL
;
327 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
329 bddxy
= getbdd(i
*3, bm
->t
);
332 if (check_space(x
, y
, LEFT
, 1, bm
) == 0){
333 sokoban_screen
*tmp_scr
= get_coord(x
, y
, screen
);
334 if (tmp_scr
->tile
== AGENT
){
335 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
336 BDDVAR relvars
[6] = {i
* 3, i
* 3 + 1, i
* 3 + 2, i
* 3 + 3, i
* 3 + 4, i
* 3 + 5};
337 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
338 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
339 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
341 if (tmp_scr
->tile
== TARGAGENT
){
342 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
343 BDDVAR relvars
[6] = {i
* 3, i
* 3 + 1, i
* 3 + 2, i
* 3 + 3, i
* 3 + 4, i
* 3 + 5};
344 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
345 uint8_t rel_enc
[6] = {1, 1, 1, 1, 0, 0};
346 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
349 else if (check_space(x
, y
, LEFT
, 1, bm
) == 1 && check_space(x
, y
, LEFT
, 2, bm
) == 0){
350 sokoban_screen
*tmp_scr
= get_coord(x
, y
, screen
);
351 sokoban_screen
*tmp_scr_d
= get_coord(x
- 1, y
, screen
);
352 xy_bddvar_map
*bddvar
= getxy(x
- 1, y
, bm
->f
);
353 int deltai
= bddvar
->value
.var
[0];
354 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== FREE
){
355 //(0 1 0 0 1 1 1 0 0 0 1 1)
356 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
357 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
358 uint8_t rel_enc
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
359 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
361 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGET
){
362 //(0 1 1 0 1 1 1 0 0 1 1 1)
363 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
364 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
365 uint8_t rel_enc
[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
366 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
368 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== FREE
){
369 //(0 1 0 1 1 0 1 0 1 0 0 1)
370 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
371 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
372 uint8_t rel_enc
[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
373 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
375 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGET
){
376 //(0 1 1 1 1 0 1 0 1 1 0 1)
377 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
378 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
379 uint8_t rel_enc
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
380 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
382 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== BOX
){
383 //(0 0 1 1 0 0 1 1 0 0 1 1)
384 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
385 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
386 uint8_t rel_enc
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
387 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
389 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGBOX
){
390 //(1 1 0 0 0 0 1 1 0 0 1 1)
391 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
392 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
393 uint8_t rel_enc
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
394 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
396 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== BOX
){
397 //(0 0 1 1 0 0 1 1 1 1 0 0)
398 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
399 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
400 uint8_t rel_enc
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
401 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
403 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGBOX
){
404 //(1 1 0 0 0 0 1 1 1 1 0 0)
405 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
406 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
407 uint8_t rel_enc
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
408 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
411 else if (check_space(x
, y
, LEFT
, 1, bm
) == 1 && check_space(x
, y
, LEFT
, 2, bm
) == 1){
412 sokoban_screen
*tmp_scr
= get_coord(x
, y
, screen
);
413 sokoban_screen
*tmp_scr_d
= get_coord(x
- 1, y
, screen
);
414 sokoban_screen
*tmp_scr_g
= get_coord(x
- 2, y
, screen
);
415 xy_bddvar_map
*bddvar
= getxy(x
- 1, y
, bm
->f
);
416 int deltai
= bddvar
->value
.var
[0];
417 // bddvar = getxy(x - 2, y, bm->f);
418 // int gammai = bddvar->value.var[0];
419 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== FREE
){
420 //(0 1 0 0 1 1 1 0 0 0 1 1)
421 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
422 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
423 uint8_t rel_enc
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
424 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
426 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGET
){
427 //(0 1 1 0 1 1 1 0 0 1 1 1)
428 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
429 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
430 uint8_t rel_enc
[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
431 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
433 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== FREE
){
434 //(0 1 0 1 1 0 1 0 1 0 0 1)
435 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
436 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
437 uint8_t rel_enc
[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
438 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
440 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGET
){
441 //(0 1 1 1 1 0 1 0 1 1 0 1)
442 BDDVAR relvars
[12] = {deltai
*3, deltai
*3+1, deltai
*3+2, deltai
*3+3, deltai
*3+4, deltai
*3+5, i
*3, i
*3+1, i
*3+2, i
*3+3, i
*3+4, i
*3+5};
443 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
444 uint8_t rel_enc
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
445 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
447 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
-> tile
== BOX
&& tmp_scr_g
->tile
== BOX
){
450 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
-> tile
== BOX
&& tmp_scr_g
->tile
== TARGBOX
){
453 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
-> tile
== BOX
&& tmp_scr_g
->tile
== BOX
){
456 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
-> tile
== BOX
&& tmp_scr_g
->tile
== TARGBOX
){
459 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== FREE
){
462 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== FREE
){
465 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== TARGET
){
468 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== TARGET
){
471 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== FREE
){
474 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== FREE
){
477 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== TARGET
){
480 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== TARGET
){
484 printf("x:%d y:%d\n", x
, y
);