d9a924a5bffe263c9feae12ced853e09df901401
37 xy_bddvar_map
*getxy(int x
, int y
, xy_bddvar_map
*map
)
39 xy_bddvar_map k
, *r
= NULL
;
40 memset(&k
, 0, sizeof(xy_bddvar_map
));
43 HASH_FIND(hh
, map
, &k
.key
, sizeof(xy
), r
);
47 bddvar_xy_map
*getbdd(int key
, bddvar_xy_map
*map
)
49 bddvar_xy_map k
, *r
= NULL
;
50 memset(&k
, 0, sizeof(bddvar_xy_map
));
52 HASH_FIND(hh
, map
, &k
.key
, sizeof(int), r
);
57 bimap
*create_bimap_helper(sokoban_screen
*screen
)
61 xy_bddvar_map
*xybdd
= NULL
;
62 bddvar_xy_map
*bddxy
= NULL
;
63 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
64 xy_bddvar_map
*f
= NULL
;
65 f
= (xy_bddvar_map
*)malloc(sizeof(xy_bddvar_map
));
66 memset(f
, 0, sizeof(xy_bddvar_map
));
67 f
->key
.x
= r
->coord
.x
;
68 f
->key
.y
= r
->coord
.y
;
69 f
->value
.var
[0] = varcount
;
70 f
->value
.var
[1] = varcount
+ 1;
71 f
->value
.var
[2] = varcount
+ 2;
72 HASH_ADD(hh
, xybdd
, key
, sizeof(xy
), f
);
74 for (int i
= 0; i
<3; i
++){
75 bddvar_xy_map
*t
= NULL
;
76 t
= (bddvar_xy_map
*)malloc(sizeof(bddvar_xy_map
));
77 memset(t
, 0, sizeof(bddvar_xy_map
));
78 t
->key
= varcount
+ i
;
79 t
->value
.x
= r
->coord
.x
;
80 t
->value
.y
= r
->coord
.y
;
81 HASH_ADD(hh
, bddxy
, key
, sizeof(int), t
);
83 varcount
= varcount
+ 3;
86 bm
= (bimap
*)malloc(sizeof(bimap
));
92 int check_xy_exists(int x
, int y
, bimap
*bm
)
95 if (getxy(x
, y
, bm
->f
) != NULL
) res
= 1;
99 int check_space(int x
, int y
, direction d
, int delta
, bimap
*bm
)
102 case LEFT
: x
= x
- delta
; break;
103 case UP
: y
= y
- delta
; break;
104 case RIGHT
: x
= x
+ delta
; break;
105 case DOWN
: y
= y
+ delta
; break;
107 return check_xy_exists(x
, y
, bm
);
111 * Each coordinate has three related boolean variables. The combination of those boolean variables
119 * 110: Agent on target
120 * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
121 * tiles in the shrinked screen.
122 * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
123 * directly in transition relations.
126 state
*encode_screen(sokoban_screen
*screen
)
130 BDDVAR vars
[HASH_COUNT(screen
) * 3];
131 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
135 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
137 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
139 state
*fullState
= NULL
;
140 fullState
= (state
*)malloc(sizeof(state
));
141 fullState
->vars
.varset
= varset
;
142 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
145 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
148 st_enc
[tile_index
] = 0;
150 st_enc
[tile_index
] = 0;
152 st_enc
[tile_index
] = 1;
156 st_enc
[tile_index
] = 0;
158 st_enc
[tile_index
] = 0;
160 st_enc
[tile_index
] = 0;
164 st_enc
[tile_index
] = 0;
166 st_enc
[tile_index
] = 1;
168 st_enc
[tile_index
] = 0;
172 st_enc
[tile_index
] = 0;
174 st_enc
[tile_index
] = 1;
176 st_enc
[tile_index
] = 1;
180 st_enc
[tile_index
] = 1;
182 st_enc
[tile_index
] = 0;
185 st_enc
[tile_index
] = 1;
188 case TARGAGENT
: //110
189 st_enc
[tile_index
] = 1;
191 st_enc
[tile_index
] = 1;
193 st_enc
[tile_index
] = 0;
197 st_enc
[tile_index
] = 1;
199 st_enc
[tile_index
] = 0;
201 st_enc
[tile_index
] = 0;
206 s
= sylvan_cube(varset
, st_enc
);
208 printf("Initial state encoded\n");
213 int countTrans(trans_t
*trs
);
215 trans_t
*create_single_rel(sokoban_screen
*screen
, direction dir
)
218 trans_t
*trs
, *trs_current
;
219 bimap
*bm
= create_bimap_helper(screen
);
222 bddvar_xy_map
*bddxy
= NULL
;
255 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
256 bddxy
= getbdd(i
*3, bm
->t
);
259 if (check_space(x
, y
, dir
, 1, bm
) == 0){
261 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
262 BDDVAR relvars
[6] = {i
* 6, i
* 6 + 1, i
* 6 + 2, i
* 6 + 3, i
* 6 + 4, i
* 6 + 5};
263 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
264 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
266 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
267 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
268 trs_current
->varset
.varset
= relvarset
;
269 trs_current
->varset
.size
= 6;
270 trs_current
->next_rel
= trs
;
273 //Targagent -> Targagent
274 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
275 relvarset
= sylvan_set_fromarray(relvars
, 6);
283 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
284 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
285 trs_current
->varset
.varset
= relvarset
;
286 trs_current
->varset
.size
= 6;
287 trs_current
->next_rel
= trs
;
291 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
293 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
294 int deltai
= bddvar
->value
.var
[0];
296 //Agent Free -> Free Agent
297 //(1 0 0 0 1 1 0 1 0 0 1 1)
298 BDDVAR relvars
[12] = {i
*6, i
*6+1, i
*6+2, i
*6+3, i
*6+4, i
*6+5, 2*deltai
, 2*deltai
+1, 2*deltai
+2, 2*deltai
+3, 2*deltai
+4, 2*deltai
+5};
299 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
300 uint8_t rel_enc
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
301 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
302 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
303 trs_current
->varset
.varset
= relvarset
;
304 trs_current
->varset
.size
= 12;
305 trs_current
->next_rel
= trs
;
308 //Agent Target -> Free Targagent
309 //(1 0 0 0 1 1 0 1 1 1 1 0)
310 relvarset
= sylvan_set_fromarray(relvars
, 12);
323 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
324 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
325 trs_current
->varset
.varset
= relvarset
;
326 trs_current
->varset
.size
= 12;
327 trs_current
->next_rel
= trs
;
330 //Targagent Free -> Target Agent
331 //(1 0 1 1 0 1 0 1 0 0 1 1)
332 relvarset
= sylvan_set_fromarray(relvars
, 12);
345 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
346 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
347 trs_current
->varset
.varset
= relvarset
;
348 trs_current
->varset
.size
= 12;
349 trs_current
->next_rel
= trs
;
352 //Targagent Target -> Target Targagent
353 //(1 0 1 1 0 1 0 1 1 1 1 0)
354 relvarset
= sylvan_set_fromarray(relvars
, 12);
367 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
368 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
369 trs_current
->varset
.varset
= relvarset
;
370 trs_current
->varset
.size
= 12;
371 trs_current
->next_rel
= trs
;
374 //Agent Box -> Agent Box
375 //(1 1 0 0 1 1 0 0 1 1 0 0)
376 relvarset
= sylvan_set_fromarray(relvars
, 12);
389 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
390 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
391 trs_current
->varset
.varset
= relvarset
;
392 trs_current
->varset
.size
= 12;
393 trs_current
->next_rel
= trs
;
396 //Agent Targbox -> Agent Targbox
397 //(1 1 0 0 1 1 1 1 0 0 0 0)
398 relvarset
= sylvan_set_fromarray(relvars
, 12);
411 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
412 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
413 trs_current
->varset
.varset
= relvarset
;
414 trs_current
->varset
.size
= 12;
415 trs_current
->next_rel
= trs
;
418 //Targagent Box -> Targagent Box
419 //(1 1 1 1 0 0 0 0 1 1 0 0)
420 relvarset
= sylvan_set_fromarray(relvars
, 12);
433 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
434 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
435 trs_current
->varset
.varset
= relvarset
;
436 trs_current
->varset
.size
= 12;
437 trs_current
->next_rel
= trs
;
440 //Targagent Targbox -> Targagent Targbox
441 //(1 1 1 1 0 0 1 1 0 0 0 0)
442 relvarset
= sylvan_set_fromarray(relvars
, 12);
455 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
456 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
457 trs_current
->varset
.varset
= relvarset
;
458 trs_current
->varset
.size
= 12;
459 trs_current
->next_rel
= trs
;
463 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
465 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
466 int deltai
= bddvar
->value
.var
[0];
467 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
468 int gammai
= bddvar
->value
.var
[0];
470 //Agent Free -> Free Agent
471 //(1 0 0 0 1 1 0 1 0 0 1 1)
472 BDDVAR relvars
[12] = {i
*6, i
*6+1, i
*6+2, i
*6+3, i
*6+4, i
*6+5, 2*deltai
, 2*deltai
+1, i
*deltai
+2, 2*deltai
+3, 2*deltai
+4, 2*deltai
+5};
473 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
474 uint8_t rel_enc
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
475 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
476 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
477 trs_current
->varset
.varset
= relvarset
;
478 trs_current
->varset
.size
= 12;
479 trs_current
->next_rel
= trs
;
482 //Agent Target -> Free Targagent
483 //(1 0 0 0 1 1 0 1 1 1 1 0)
484 relvarset
= sylvan_set_fromarray(relvars
, 12);
497 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
498 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
499 trs_current
->varset
.varset
= relvarset
;
500 trs_current
->varset
.size
= 12;
501 trs_current
->next_rel
= trs
;
504 //Targagent Free -> Target Agent
505 //(1 0 1 1 0 1 0 1 0 0 1 1)
506 relvarset
= sylvan_set_fromarray(relvars
, 12);
519 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
520 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
521 trs_current
->varset
.varset
= relvarset
;
522 trs_current
->varset
.size
= 12;
523 trs_current
->next_rel
= trs
;
526 //Targagent Target -> Target Targagent
527 //(1 0 1 1 0 1 0 1 1 1 1 0)
528 relvarset
= sylvan_set_fromarray(relvars
, 12);
541 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
542 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
543 trs_current
->varset
.varset
= relvarset
;
544 trs_current
->varset
.size
= 12;
545 trs_current
->next_rel
= trs
;
548 //Agent Box Box -> Agent Box Box
549 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
550 BDDVAR relvars1
[18] = {i
*6, i
*6+1, i
*6+2, i
*6+3, i
*6+4, i
*6+5, 2*deltai
, 2*deltai
+1, 2*deltai
+2, 2*deltai
+3, 2*deltai
+4, 2*deltai
+5, 2*gammai
, 2*gammai
+1, 2*gammai
+2, 2*gammai
+3, 2*gammai
+4, 2*gammai
+5};
551 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
552 uint8_t rel_enc1
[18];
571 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
572 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
573 trs_current
->varset
.varset
= relvarset1
;
574 trs_current
->varset
.size
= 18;
575 trs_current
->next_rel
= trs
;
578 //Agent Box Targbox -> Agent Box Targbox
579 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0)
580 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
599 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
600 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
601 trs_current
->varset
.varset
= relvarset1
;
602 trs_current
->varset
.size
= 18;
603 trs_current
->next_rel
= trs
;
606 //Targagent Box Box -> Targagent Box Box
607 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
608 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
627 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
628 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
629 trs_current
->varset
.varset
= relvarset1
;
630 trs_current
->varset
.size
= 18;
631 trs_current
->next_rel
= trs
;
634 //Targagent Box Targbox -> Targagent Box Targbox
635 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
636 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
655 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
656 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
657 trs_current
->varset
.varset
= relvarset1
;
658 trs_current
->varset
.size
= 18;
659 trs_current
->next_rel
= trs
;
662 //Agent Box Free -> Free Agent Box
663 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
664 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
683 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
684 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
685 trs_current
->varset
.varset
= relvarset1
;
686 trs_current
->varset
.size
= 18;
687 trs_current
->next_rel
= trs
;
690 //Agent Targbox Free -> Free Targagent Box
691 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
692 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
711 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
712 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
713 trs_current
->varset
.varset
= relvarset1
;
714 trs_current
->varset
.size
= 18;
715 trs_current
->next_rel
= trs
;
718 //Agent Box Target -> Free Agent Targbox
719 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
720 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
739 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
740 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
741 trs_current
->varset
.varset
= relvarset1
;
742 trs_current
->varset
.size
= 18;
743 trs_current
->next_rel
= trs
;
746 //Agent Targbox Target -> Free Targagent Targbox
747 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
748 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
767 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
768 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
769 trs_current
->varset
.varset
= relvarset1
;
770 trs_current
->varset
.size
= 18;
771 trs_current
->next_rel
= trs
;
774 //Targagent Box Free -> Target Agent Box
775 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
776 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
795 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
796 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
797 trs_current
->varset
.varset
= relvarset1
;
798 trs_current
->varset
.size
= 18;
799 trs_current
->next_rel
= trs
;
802 //Targagent Targbox Free -> Target Targagent Box
803 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
804 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
823 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
824 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
825 trs_current
->varset
.varset
= relvarset1
;
826 trs_current
->varset
.size
= 18;
827 trs_current
->next_rel
= trs
;
830 //Targagent Box Target -> Target Agent Targbox
831 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
832 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
851 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
852 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
853 trs_current
->varset
.varset
= relvarset1
;
854 trs_current
->varset
.size
= 18;
855 trs_current
->next_rel
= trs
;
858 //Targagent Targbox Target -> Target Targagent Targbox
859 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
860 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
879 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
880 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
881 trs_current
->varset
.varset
= relvarset1
;
882 trs_current
->varset
.size
= 18;
883 trs_current
->next_rel
= trs
;
892 if (trs_current
!= NULL
) printf("LEFT ok!\n");
893 else printf ("LEFT is empty\n");
894 printf("Num of trans relations:%d\n", countTrans(trs
));
897 if (trs_current
!= NULL
) printf("UP ok!\n");
898 else printf ("UP is empty\n");
899 printf("Num of trans relations:%d\n", countTrans(trs
));
902 if (trs_current
!= NULL
) printf("RIGHT ok!\n");
903 else printf ("RIGHT is empty\n");
904 printf("Num of trans relations:%d\n", countTrans(trs
));
907 if (trs_current
!= NULL
) printf("DOWN ok!\n");
908 else printf ("DOWN is empty\n");
909 printf("Num of trans relations:%d\n", countTrans(trs
));
917 int countTrans(trans_t
*trs
)
927 rels
*encode_rel(sokoban_screen
*screen
)
931 trans_t
*tl
= sylvan_false
;
934 tl
= create_single_rel(screen
, LEFT
);
937 trans_t
*tu
= create_single_rel(screen
, UP
);
940 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
943 trans_t
*td
= create_single_rel(screen
, DOWN
);
946 rls
= (rels
*)malloc(sizeof(rels
));
955 int test_trans(state
*s
, trans_t
*t
)
959 BDD next
= sylvan_false
;
961 next
= sylvan_relnext(s
->bdd
, t
->bdd
, t
->varset
.varset
);
962 if (next
== s
->bdd
) printf("Same\n");
963 if (next
!= s
->bdd
&& next
!= sylvan_false
) printf("Different\n");
964 if (next
== sylvan_false
) printf("False\n");
967 printf("Trans:%d\n", counter
);