12b428d8d62b0fd92781ed8d2683d35938ab1350
10 #include <gperftools/profiler.h>
46 xy_bddvar_map
*getxy(int x
, int y
, xy_bddvar_map
*map
)
48 xy_bddvar_map k
, *r
= NULL
;
49 memset(&k
, 0, sizeof(xy_bddvar_map
));
52 HASH_FIND(hh
, map
, &k
.key
, sizeof(xy
), r
);
56 bddvar_xy_map
*getbdd(int key
, bddvar_xy_map
*map
)
58 bddvar_xy_map k
, *r
= NULL
;
59 memset(&k
, 0, sizeof(bddvar_xy_map
));
61 HASH_FIND(hh
, map
, &k
.key
, sizeof(int), r
);
65 xy_bddvar_map
*create_xy_bddvar_map(sokoban_screen
*screen
)
69 xy_bddvar_map
*xybdd
= NULL
;
70 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
71 xy_bddvar_map
*f
= NULL
;
72 //bddvar_xy_map *t = NULL;
74 f
= (xy_bddvar_map
*)malloc(sizeof(xy_bddvar_map
));
75 memset(f
, 0, sizeof(xy_bddvar_map
));
76 f
->key
.x
= r
->coord
.x
;
77 f
->key
.y
= r
->coord
.y
;
78 printf("test!: %d %d\n", r
->coord
.x
, r
->coord
.y
);
79 f
->value
.var
[0] = varcount
;
80 f
->value
.var
[1] = varcount
+ 1;
81 f
->value
.var
[2] = varcount
+ 2;
82 HASH_ADD(hh
, xybdd
, key
, sizeof(xy
), f
);
83 varcount
= varcount
+ 3;
88 bddvar_xy_map
*create_bddvar_xy_map(sokoban_screen
*screen
)
92 bddvar_xy_map
*bddxy
= NULL
;
93 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
94 for (int i
= 0; i
<3; i
++){
95 bddvar_xy_map
*f
= NULL
;
96 //bddvar_xy_map *t = NULL;
98 f
= (bddvar_xy_map
*)malloc(sizeof(bddvar_xy_map
));
99 memset(f
, 0, sizeof(bddvar_xy_map
));
100 f
->key
= varcount
+ i
;
101 f
->value
.x
= r
->coord
.x
;
102 f
->value
.y
= r
->coord
.y
;
103 HASH_ADD(hh
, bddxy
, key
, sizeof(int), f
);
105 varcount
= varcount
+ 3;
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 BDD
encode_screen(sokoban_screen
*screen
)
128 BDD state
= sylvan_false
;
132 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
135 if (state
== sylvan_false
){
136 state
= sylvan_not(sylvan_ithvar(tile_index
));
138 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
140 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
144 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
146 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
148 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
153 if (state
== sylvan_false
){
154 state
= sylvan_not(sylvan_ithvar(tile_index
));
156 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
158 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
162 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
164 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
166 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
171 if (state
== sylvan_false
){
172 state
= sylvan_not(sylvan_ithvar(tile_index
));
174 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
176 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
180 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
182 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
184 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
189 if (state
== sylvan_false
){
190 state
= sylvan_not(sylvan_ithvar(tile_index
));
192 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
194 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
198 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
200 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
202 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
207 if (state
== sylvan_false
){
208 state
= sylvan_ithvar(tile_index
);
210 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
212 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
216 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
218 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
220 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
225 if (state
== sylvan_false
){
226 state
= sylvan_ithvar(tile_index
);
228 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
230 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
234 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
236 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
238 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
243 if (state
== sylvan_false
){
244 state
= sylvan_ithvar(tile_index
);
246 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
248 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
252 state
= sylvan_and(state
, sylvan_ithvar(tile_index
));
254 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
256 state
= sylvan_and(state
, sylvan_not(sylvan_ithvar(tile_index
)));
263 xy_bddvar_map *map = NULL;
264 map = create_xy_bddvar_map(screen);
265 xy_bddvar_map *m = getxy(1, 1, map);
266 bddvar_xy_map *map2 = NULL;
267 map2 = create_bddvar_xy_map(screen);
268 bddvar_xy_map *m2 = getbdd(2, map2);
269 printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]);
270 printf("Test2: %d %d\n", m2->value.x, m2->value.y);
272 printf("%d tiles were encoded\n", tile_index
);
276 BDD
encode_rel(sokoban_screen
*screen
)
279 num_tiles
= HASH_COUNT(screen
);
280 printf("Number of tiles: %d\n", num_tiles
);
289 BDD b
= sylvan_not(a
);
290 if (b
== sylvan_false
){
291 printf("BDD works!\n");
293 printf("BDD does not work!\n");
296 BDD c
= sylvan_ithvar(1);
297 if (sylvan_high(c
) == sylvan_true
&& sylvan_low(c
) == sylvan_false
) printf("VAR works 1\n");
298 if (sylvan_var(c
) == 1) printf("Var works 2\n");