85b1867ea6c93533bb37d76710dbbca4a3b9743b
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
53 xy_bddvar_map
*getxy(int x
, int y
, xy_bddvar_map
*map
)
55 xy_bddvar_map k
, *r
= NULL
;
56 memset(&k
, 0, sizeof(xy_bddvar_map
));
59 HASH_FIND(hh
, map
, &k
.key
, sizeof(xy
), r
);
63 bddvar_xy_map
*getbdd(int key
, bddvar_xy_map
*map
)
65 bddvar_xy_map k
, *r
= NULL
;
66 memset(&k
, 0, sizeof(bddvar_xy_map
));
68 HASH_FIND(hh
, map
, &k
.key
, sizeof(int), r
);
73 xy_bddvar_map *create_xy_bddvar_map(sokoban_screen *screen)
77 xy_bddvar_map *xybdd = NULL;
78 for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
79 xy_bddvar_map *f = NULL;
80 //bddvar_xy_map *t = NULL;
82 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
83 memset(f, 0, sizeof(xy_bddvar_map));
84 f->key.x = r->coord.x;
85 f->key.y = r->coord.y;
86 f->value.var[0] = varcount;
87 f->value.var[1] = varcount + 1;
88 f->value.var[2] = varcount + 2;
89 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
90 varcount = varcount + 3;
95 bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen)
99 bddvar_xy_map *bddxy = NULL;
100 for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
101 for (int i = 0; i <3; i++){
102 bddvar_xy_map *f = NULL;
103 //bddvar_xy_map *t = NULL;
105 f = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
106 memset(f, 0, sizeof(bddvar_xy_map));
107 f->key = varcount + i;
108 f->value.x = r->coord.x;
109 f->value.y = r->coord.y;
110 HASH_ADD(hh, bddxy, key, sizeof(int), f);
112 varcount = varcount + 3;
118 bimap
*create_bimap_helper(sokoban_screen
*screen
)
122 xy_bddvar_map
*xybdd
= NULL
;
123 bddvar_xy_map
*bddxy
= NULL
;
124 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
125 xy_bddvar_map
*f
= NULL
;
126 f
= (xy_bddvar_map
*)malloc(sizeof(xy_bddvar_map
));
127 memset(f
, 0, sizeof(xy_bddvar_map
));
128 f
->key
.x
= r
->coord
.x
;
129 f
->key
.y
= r
->coord
.y
;
130 f
->value
.var
[0] = varcount
;
131 f
->value
.var
[1] = varcount
+ 1;
132 f
->value
.var
[2] = varcount
+ 2;
133 HASH_ADD(hh
, xybdd
, key
, sizeof(xy
), f
);
135 for (int i
= 0; i
<3; i
++){
136 bddvar_xy_map
*t
= NULL
;
137 t
= (bddvar_xy_map
*)malloc(sizeof(bddvar_xy_map
));
138 memset(t
, 0, sizeof(bddvar_xy_map
));
139 t
->key
= varcount
+ i
;
140 t
->value
.x
= r
->coord
.x
;
141 t
->value
.y
= r
->coord
.y
;
142 HASH_ADD(hh
, bddxy
, key
, sizeof(int), t
);
144 varcount
= varcount
+ 3;
147 bm
= (bimap
*)malloc(sizeof(bimap
));
153 int check_xy_exists(int x
, int y
, bimap
*bm
)
156 if (getxy(x
, y
, bm
->f
) != NULL
) res
= 1;
160 int check_space(int x
, int y
, direction d
, int delta
, bimap
*bm
)
163 case LEFT
: x
= x
- delta
; break;
164 case UP
: y
= y
- delta
; break;
165 case RIGHT
: x
= x
+ delta
; break;
166 case DOWN
: y
= y
+ delta
; break;
168 return check_xy_exists(x
, y
, bm
);
172 * Each coordinate has three related boolean variables. The combination of those boolean variables
180 * 110: Agent on target
181 * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
182 * tiles in the shrinked screen.
183 * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
184 * directly in transition relations.
187 state
*encode_screen(sokoban_screen
*screen
)
191 BDDVAR vars
[HASH_COUNT(screen
) * 3];
192 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
196 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
198 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
200 state
*fullState
= NULL
;
201 fullState
= (state
*)malloc(sizeof(state
));
202 fullState
->vars
.varset
= varset
;
203 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
206 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
209 st_enc
[tile_index
] = 0;
211 st_enc
[tile_index
] = 0;
213 st_enc
[tile_index
] = 1;
217 st_enc
[tile_index
] = 0;
219 st_enc
[tile_index
] = 0;
221 st_enc
[tile_index
] = 0;
225 st_enc
[tile_index
] = 0;
227 st_enc
[tile_index
] = 1;
229 st_enc
[tile_index
] = 0;
233 st_enc
[tile_index
] = 0;
235 st_enc
[tile_index
] = 1;
237 st_enc
[tile_index
] = 1;
241 st_enc
[tile_index
] = 1;
243 st_enc
[tile_index
] = 0;
245 st_enc
[tile_index
] = 1;
248 case TARGAGENT
: //110
249 st_enc
[tile_index
] = 1;
251 st_enc
[tile_index
] = 1;
253 st_enc
[tile_index
] = 0;
257 st_enc
[tile_index
] = 1;
259 st_enc
[tile_index
] = 0;
261 st_enc
[tile_index
] = 0;
266 s
= sylvan_cube(varset
, st_enc
);
268 printf("Initial state encoded\n");
277 BDDVAR vars
[] = {0,2,4};
278 BDDVAR all_vars
[] = {4,5};
280 BDDSET vars_set
= sylvan_set_fromarray(vars
, 3);
281 BDDSET all_vars_set
= sylvan_set_fromarray(all_vars
, 2);
283 BDD s
, t
, next
, prev
;
286 // transition relation: 000 --> 111 and !000 --> 000
288 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1,0,1,0,1}));
289 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0}));
290 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){2,0,1,0,2,0}));
291 t
= sylvan_union_cube(t
, all_vars_set
, ((uint8_t[]){1,0}));
293 s
= sylvan_cube(vars_set
, (uint8_t[]){0,0,1});
294 zeroes
= sylvan_cube(vars_set
, (uint8_t[]){0,0,0});
295 ones
= sylvan_cube(vars_set
, (uint8_t[]){0,0,1});
297 next
= sylvan_relnext(s
, t
, all_vars_set
);
298 prev
= sylvan_relprev(t
, next
, all_vars_set
);
299 if (next
== zeroes
) printf("Pass 1\n");
300 if (prev
== ones
|| prev
== zeroes
) printf("Pass 2\n");
305 BDD
create_single_rel(sokoban_screen
*screen
, direction dir
)
308 BDD t
= sylvan_false
;
309 bimap
*bm
= create_bimap_helper(screen
);
312 bddvar_xy_map
*bddxy
= NULL
;
344 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
345 bddxy
= getbdd(i
*3, bm
->t
);
348 if (check_space(x
, y
, dir
, 1, bm
) == 0){
349 sokoban_screen
*tmp_scr
= get_coord(x
, y
, screen
);
350 if (tmp_scr
->tile
== AGENT
){
351 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
352 BDDVAR relvars
[6] = {i
* 3, i
* 3 + 1, i
* 3 + 2, i
* 3 + 3, i
* 3 + 4, i
* 3 + 5};
353 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
354 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
355 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
357 if (tmp_scr
->tile
== TARGAGENT
){
358 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
359 BDDVAR relvars
[6] = {i
* 3, i
* 3 + 1, i
* 3 + 2, i
* 3 + 3, i
* 3 + 4, i
* 3 + 5};
360 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
361 uint8_t rel_enc
[6] = {1, 1, 1, 1, 0, 0};
362 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
365 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
366 sokoban_screen
*tmp_scr
= get_coord(x
, y
, screen
);
367 sokoban_screen
*tmp_scr_d
= get_coord(x
+ xdelta
, y
+ ydelta
, screen
);
368 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
369 int deltai
= bddvar
->value
.var
[0];
370 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== FREE
){
371 //(0 1 0 0 1 1 1 0 0 0 1 1)
372 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};
373 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
374 uint8_t rel_enc
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
375 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
377 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGET
){
378 //(0 1 1 0 1 1 1 0 0 1 1 1)
379 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};
380 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
381 uint8_t rel_enc
[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
382 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
384 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== FREE
){
385 //(0 1 0 1 1 0 1 0 1 0 0 1)
386 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};
387 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
388 uint8_t rel_enc
[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
389 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
391 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGET
){
392 //(0 1 1 1 1 0 1 0 1 1 0 1)
393 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};
394 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
395 uint8_t rel_enc
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
396 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
398 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== BOX
){
399 //(0 0 1 1 0 0 1 1 0 0 1 1)
400 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};
401 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
402 uint8_t rel_enc
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
403 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
405 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGBOX
){
406 //(1 1 0 0 0 0 1 1 0 0 1 1)
407 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};
408 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
409 uint8_t rel_enc
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
410 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
412 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== BOX
){
413 //(0 0 1 1 0 0 1 1 1 1 0 0)
414 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};
415 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
416 uint8_t rel_enc
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
417 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
419 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGBOX
){
420 //(1 1 0 0 0 0 1 1 1 1 0 0)
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] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
424 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
427 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
428 sokoban_screen
*tmp_scr
= get_coord(x
, y
, screen
);
429 sokoban_screen
*tmp_scr_d
= get_coord(x
+ xdelta
, y
+ ydelta
, screen
);
430 sokoban_screen
*tmp_scr_g
= get_coord(x
+ xgamma
, y
+ ygamma
, screen
);
431 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
432 int deltai
= bddvar
->value
.var
[0];
433 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
434 int gammai
= bddvar
->value
.var
[0];
435 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== FREE
){
436 //(0 1 0 0 1 1 1 0 0 0 1 1)
437 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};
438 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
439 uint8_t rel_enc
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
440 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
442 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGET
){
443 //(0 1 1 0 1 1 1 0 0 1 1 1)
444 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};
445 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
446 uint8_t rel_enc
[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
447 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
449 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== FREE
){
450 //(0 1 0 1 1 0 1 0 1 0 0 1)
451 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};
452 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
453 uint8_t rel_enc
[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
454 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
456 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGET
){
457 //(0 1 1 1 1 0 1 0 1 1 0 1)
458 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};
459 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
460 uint8_t rel_enc
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
461 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
463 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
-> tile
== BOX
&& tmp_scr_g
->tile
== BOX
){
464 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
465 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
466 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
467 uint8_t rel_enc
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
468 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
470 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
-> tile
== BOX
&& tmp_scr_g
->tile
== TARGBOX
){
471 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
472 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
473 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
474 uint8_t rel_enc
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
475 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
477 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
-> tile
== BOX
&& tmp_scr_g
->tile
== BOX
){
478 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
479 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
480 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
481 uint8_t rel_enc
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
482 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
484 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
-> tile
== BOX
&& tmp_scr_g
->tile
== TARGBOX
){
485 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
486 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
487 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
488 uint8_t rel_enc
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
489 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
491 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== FREE
){
492 //free box agent -> box agent free
493 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
494 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
495 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
496 uint8_t rel_enc
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
497 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
499 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== FREE
){
500 //(free targbox agent -> box targagent free)
501 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
502 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
503 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
504 uint8_t rel_enc
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
505 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
507 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== TARGET
){
508 //(target box agent -> targbox agent free)
509 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
510 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
511 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
512 uint8_t rel_enc
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
513 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
515 if (tmp_scr
->tile
== AGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== TARGET
){
516 //(target targbox agent -> targbox targagent free)
517 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
518 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
519 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
520 uint8_t rel_enc
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
521 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
523 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== FREE
){
524 //(free box targagent -> box agent target)
525 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
526 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
527 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
528 uint8_t rel_enc
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
529 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
531 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== FREE
){
532 //(free targbox targagent -> box targagent target)
533 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
534 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
535 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
536 uint8_t rel_enc
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
537 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
539 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== BOX
&& tmp_scr_g
->tile
== TARGET
){
540 //(target box targagent -> targbox agent target)
541 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
542 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
543 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
544 uint8_t rel_enc
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
545 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
547 if (tmp_scr
->tile
== TARGAGENT
&& tmp_scr_d
->tile
== TARGBOX
&& tmp_scr_g
->tile
== TARGET
){
548 //(target targbox targagent -> targbox targagent target)
549 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
550 BDDVAR relvars
[18] = {gammai
*3, gammai
*3+1, gammai
*3+2, gammai
*3+3, gammai
*3+4, gammai
*3+5, 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};
551 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 18);
552 uint8_t rel_enc
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
553 t
= sylvan_union_cube(t
, relvarset
, rel_enc
);
560 rels
*encode_rel(sokoban_screen
*screen
)
564 BDD tl
= sylvan_false
;
567 tl
= create_single_rel(screen
, LEFT
);
569 for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
571 bddxy = getbdd(i*3, bm->t);
574 if (check_space(x, y, LEFT, 1, bm) == 0){
575 sokoban_screen *tmp_scr = get_coord(x, y, screen);
576 if (tmp_scr->tile == AGENT){
577 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
578 BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
579 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
580 uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
581 t = sylvan_union_cube(t, relvarset, rel_enc);
583 if (tmp_scr->tile == TARGAGENT){
584 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
585 BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
586 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
587 uint8_t rel_enc[6] = {1, 1, 1, 1, 0, 0};
588 t = sylvan_union_cube(t, relvarset, rel_enc);
591 else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 0){
592 sokoban_screen *tmp_scr = get_coord(x, y, screen);
593 sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
594 xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f);
595 int deltai = bddvar->value.var[0];
596 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
597 //(0 1 0 0 1 1 1 0 0 0 1 1)
598 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};
599 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
600 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
601 t = sylvan_union_cube(t, relvarset, rel_enc);
603 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
604 //(0 1 1 0 1 1 1 0 0 1 1 1)
605 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};
606 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
607 uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
608 t = sylvan_union_cube(t, relvarset, rel_enc);
610 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
611 //(0 1 0 1 1 0 1 0 1 0 0 1)
612 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};
613 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
614 uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
615 t = sylvan_union_cube(t, relvarset, rel_enc);
617 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
618 //(0 1 1 1 1 0 1 0 1 1 0 1)
619 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};
620 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
621 uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
622 t = sylvan_union_cube(t, relvarset, rel_enc);
624 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX){
625 //(0 0 1 1 0 0 1 1 0 0 1 1)
626 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};
627 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
628 uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
629 t = sylvan_union_cube(t, relvarset, rel_enc);
631 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX){
632 //(1 1 0 0 0 0 1 1 0 0 1 1)
633 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};
634 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
635 uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
636 t = sylvan_union_cube(t, relvarset, rel_enc);
638 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX){
639 //(0 0 1 1 0 0 1 1 1 1 0 0)
640 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};
641 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
642 uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
643 t = sylvan_union_cube(t, relvarset, rel_enc);
645 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX){
646 //(1 1 0 0 0 0 1 1 1 1 0 0)
647 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};
648 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
649 uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
650 t = sylvan_union_cube(t, relvarset, rel_enc);
653 else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 1){
654 sokoban_screen *tmp_scr = get_coord(x, y, screen);
655 sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
656 sokoban_screen *tmp_scr_g = get_coord(x - 2, y, screen);
657 xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f);
658 int deltai = bddvar->value.var[0];
659 bddvar = getxy(x - 2, y, bm->f);
660 int gammai = bddvar->value.var[0];
661 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
662 //(0 1 0 0 1 1 1 0 0 0 1 1)
663 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};
664 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
665 uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
666 t = sylvan_union_cube(t, relvarset, rel_enc);
668 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
669 //(0 1 1 0 1 1 1 0 0 1 1 1)
670 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};
671 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
672 uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
673 t = sylvan_union_cube(t, relvarset, rel_enc);
675 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
676 //(0 1 0 1 1 0 1 0 1 0 0 1)
677 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};
678 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
679 uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
680 t = sylvan_union_cube(t, relvarset, rel_enc);
682 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
683 //(0 1 1 1 1 0 1 0 1 1 0 1)
684 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};
685 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
686 uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
687 t = sylvan_union_cube(t, relvarset, rel_enc);
689 if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
690 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
691 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
692 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
693 uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
694 t = sylvan_union_cube(t, relvarset, rel_enc);
696 if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
697 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
698 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
699 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
700 uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
701 t = sylvan_union_cube(t, relvarset, rel_enc);
703 if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
704 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
705 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
706 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
707 uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
708 t = sylvan_union_cube(t, relvarset, rel_enc);
710 if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
711 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
712 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
713 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
714 uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
715 t = sylvan_union_cube(t, relvarset, rel_enc);
717 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
718 //free box agent -> box agent free
719 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
720 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
721 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
722 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
723 t = sylvan_union_cube(t, relvarset, rel_enc);
725 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
726 //(free targbox agent -> box targagent free)
727 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
728 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
729 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
730 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
731 t = sylvan_union_cube(t, relvarset, rel_enc);
733 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
734 //(target box agent -> targbox agent free)
735 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
736 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
737 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
738 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
739 t = sylvan_union_cube(t, relvarset, rel_enc);
741 if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
742 //(target targbox agent -> targbox targagent free)
743 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
744 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
745 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
746 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
747 t = sylvan_union_cube(t, relvarset, rel_enc);
749 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
750 //(free box targagent -> box agent target)
751 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
752 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
753 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
754 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
755 t = sylvan_union_cube(t, relvarset, rel_enc);
757 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
758 //(free targbox targagent -> box targagent target)
759 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
760 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
761 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
762 uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
763 t = sylvan_union_cube(t, relvarset, rel_enc);
765 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
766 //(target box targagent -> targbox agent target)
767 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
768 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
769 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
770 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
771 t = sylvan_union_cube(t, relvarset, rel_enc);
773 if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
774 //(target targbox targagent -> targbox targagent target)
775 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
776 BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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};
777 BDDSET relvarset = sylvan_set_fromarray(relvars, 18);
778 uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
779 t = sylvan_union_cube(t, relvarset, rel_enc);
786 BDD tu
= create_single_rel(screen
, UP
);
789 BDD tr
= create_single_rel(screen
, RIGHT
);
792 BDD td
= create_single_rel(screen
, DOWN
);
795 rls
= (rels
*)malloc(sizeof(rels
));