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
;
43 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
46 if (state
== sylvan_false
){
47 state
= sylvan_not(sylvan_ithvar(tile_index
));
49 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
51 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
55 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
57 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
59 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
62 printf("x = %d y = %d FREE\n", r
->coord
.x
, r
->coord
.y
);
65 if (state
== sylvan_false
){
66 state
= sylvan_not(sylvan_ithvar(tile_index
));
68 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
70 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
74 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
76 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
78 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
81 printf("x = %d y = %d WALL\n", r
->coord
.x
, r
->coord
.y
);
84 if (state
== sylvan_false
){
85 state
= sylvan_not(sylvan_ithvar(tile_index
));
87 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
89 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
93 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
95 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
97 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
100 printf("x = %d y = %d BOX\n", r
->coord
.x
, r
->coord
.y
);
103 if (state
== sylvan_false
){
104 state
= sylvan_not(sylvan_ithvar(tile_index
));
106 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
108 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
112 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
114 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
116 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
119 printf("x = %d y = %d TARGET\n", r
->coord
.x
, r
->coord
.y
);
122 if (state
== sylvan_false
){
123 state
= sylvan_ithvar(tile_index
);
125 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
127 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
131 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
133 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
135 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
138 printf("x = %d y = %d AGENT\n", r
->coord
.x
, r
->coord
.y
);
141 if (state
== sylvan_false
){
142 state
= sylvan_ithvar(tile_index
);
144 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
146 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
150 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
152 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
154 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
157 printf("x = %d y = %d TARGAGENT\n", r
->coord
.x
, r
->coord
.y
);
160 if (state
== sylvan_false
){
161 state
= sylvan_ithvar(tile_index
);
163 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
165 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
169 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
171 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
173 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
176 printf("x = %d y = %d TARGBOX\n", r
->coord
.x
, r
->coord
.y
);
183 BDD
encode_rel(sokoban_screen
*screen
)
186 num_tiles
= HASH_COUNT(screen
);
187 printf("Number of tiles: %d\n", num_tiles
);
196 BDD b
= sylvan_not(a
);
197 if (b
== sylvan_false
){
198 printf("BDD works!\n");
200 printf("BDD does not work!\n");
203 BDD c
= sylvan_ithvar(1);
204 if (sylvan_high(c
) == sylvan_true
&& sylvan_low(c
) == sylvan_false
) printf("VAR works 1\n");
205 if (sylvan_var(c
) == 1) printf("Var works 2\n");