dec0a284c7ecc095c512c0d097cff9e00ba941ad
10 #include <gperftools/profiler.h>
22 * Each coordinate has three related boolean variables. The combination of those boolean variables
30 * 110: Agent on target
31 * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
32 * tiles in the shrinked screen.
33 * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
34 * directly in transition relations.
37 BDD
encode_screen(sokoban_screen
*screen
)
39 BDD state
= sylvan_false
;
42 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
45 if (state
== sylvan_false
){
51 printf("x = %d y = %d FREE\n", r
->coord
.x
, r
->coord
.y
);
54 if (state
== sylvan_false
){
60 printf("x = %d y = %d WALL\n", r
->coord
.x
, r
->coord
.y
);
63 if (state
== sylvan_false
){
69 printf("x = %d y = %d BOX\n", r
->coord
.x
, r
->coord
.y
);
72 if (state
== sylvan_false
){
78 printf("x = %d y = %d TARGET\n", r
->coord
.x
, r
->coord
.y
);
81 if (state
== sylvan_false
){
87 printf("x = %d y = %d AGENT\n", r
->coord
.x
, r
->coord
.y
);
90 if (state
== sylvan_false
){
96 printf("x = %d y = %d TARGAGENT\n", r
->coord
.x
, r
->coord
.y
);
99 if (state
== sylvan_false
){
105 printf("x = %d y = %d TARGBOX\n", r
->coord
.x
, r
->coord
.y
);
112 BDD
encode_rel(sokoban_screen
*screen
)
115 num_tiles
= HASH_COUNT(screen
);
116 printf("Number of tiles: %d\n", num_tiles
);
125 BDD b
= sylvan_not(a
);
126 if (b
== sylvan_false
){
127 printf("BDD works!\n");
129 printf("BDD does not work!\n");
132 BDD c
= sylvan_ithvar(1);
133 if (sylvan_high(c
) == sylvan_true
&& sylvan_low(c
) == sylvan_false
) printf("VAR works 1\n");
134 if (sylvan_var(c
) == 1) printf("Var works 2\n");