10 #include <gperftools/profiler.h>
47 xy_bddvar_map
*getxy(int x
, int y
, xy_bddvar_map
*map
)
49 xy_bddvar_map k
, *r
= NULL
;
50 memset(&k
, 0, sizeof(xy_bddvar_map
));
53 HASH_FIND(hh
, map
, &k
.key
, sizeof(xy
), r
);
57 bddvar_xy_map
*getbdd(int key
, bddvar_xy_map
*map
)
59 bddvar_xy_map k
, *r
= NULL
;
60 memset(&k
, 0, sizeof(bddvar_xy_map
));
62 HASH_FIND(hh
, map
, &k
.key
, sizeof(int), r
);
67 bimap
*create_bimap_helper(sokoban_screen
*screen
)
71 xy_bddvar_map
*xybdd
= NULL
;
72 bddvar_xy_map
*bddxy
= NULL
;
73 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
74 xy_bddvar_map
*f
= NULL
;
75 f
= (xy_bddvar_map
*)malloc(sizeof(xy_bddvar_map
));
76 memset(f
, 0, sizeof(xy_bddvar_map
));
77 f
->key
.x
= r
->coord
.x
;
78 f
->key
.y
= 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
);
84 for (int i
= 0; i
<3; i
++){
85 bddvar_xy_map
*t
= NULL
;
86 t
= (bddvar_xy_map
*)malloc(sizeof(bddvar_xy_map
));
87 memset(t
, 0, sizeof(bddvar_xy_map
));
88 t
->key
= varcount
+ i
;
89 t
->value
.x
= r
->coord
.x
;
90 t
->value
.y
= r
->coord
.y
;
91 HASH_ADD(hh
, bddxy
, key
, sizeof(int), t
);
93 varcount
= varcount
+ 3;
96 bm
= (bimap
*)malloc(sizeof(bimap
));
102 int check_xy_exists(int x
, int y
, bimap
*bm
)
105 if (getxy(x
, y
, bm
->f
) != NULL
) res
= 1;
109 int check_space(int x
, int y
, direction d
, int delta
, bimap
*bm
)
112 case LEFT
: x
= x
- delta
; break;
113 case UP
: y
= y
- delta
; break;
114 case RIGHT
: x
= x
+ delta
; break;
115 case DOWN
: y
= y
+ delta
; break;
117 return check_xy_exists(x
, y
, bm
);
121 * Each coordinate has three related boolean variables. The combination of those boolean variables
129 * 110: Agent on target
130 * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
131 * tiles in the shrinked screen.
132 * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
133 * directly in transition relations.
136 state
*encode_screen(sokoban_screen
*screen
)
140 BDDVAR vars
[HASH_COUNT(screen
) * 3];
141 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
145 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
147 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
149 state
*fullState
= NULL
;
150 fullState
= (state
*)malloc(sizeof(state
));
151 fullState
->vars
.varset
= varset
;
152 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
155 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
158 st_enc
[tile_index
] = 0;
160 st_enc
[tile_index
] = 0;
162 st_enc
[tile_index
] = 1;
166 st_enc
[tile_index
] = 0;
168 st_enc
[tile_index
] = 0;
170 st_enc
[tile_index
] = 0;
174 st_enc
[tile_index
] = 0;
176 st_enc
[tile_index
] = 1;
178 st_enc
[tile_index
] = 0;
182 st_enc
[tile_index
] = 0;
184 st_enc
[tile_index
] = 1;
186 st_enc
[tile_index
] = 1;
190 st_enc
[tile_index
] = 1;
192 st_enc
[tile_index
] = 0;
194 st_enc
[tile_index
] = 1;
197 case TARGAGENT
: //110
198 st_enc
[tile_index
] = 1;
200 st_enc
[tile_index
] = 1;
202 st_enc
[tile_index
] = 0;
206 st_enc
[tile_index
] = 1;
208 st_enc
[tile_index
] = 0;
210 st_enc
[tile_index
] = 0;
215 s
= sylvan_cube(varset
, st_enc
);
217 printf("Initial state encoded\n");
221 trans_t
*create_single_rel(sokoban_screen
*screen
, direction dir
)
224 trans_t
*trs
, *trs_current
;
225 bimap
*bm
= create_bimap_helper(screen
);
228 bddvar_xy_map
*bddxy
= NULL
;
261 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
262 bddxy
= getbdd(i
*3, bm
->t
);
265 if (check_space(x
, y
, dir
, 1, bm
) == 0){
268 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
269 BDDVAR relvars
[6] = {i
* 3, i
* 3 + 1, i
* 3 + 2, i
* 3 + 3, i
* 3 + 4, i
* 3 + 5};
270 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
271 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
273 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
274 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
275 trs_current
->varset
.varset
= relvarset
;
276 trs_current
->varset
.size
= 6;
277 trs_current
->next_rel
= trs
;
280 //Targagent -> Targagent
281 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
283 relvars
[1] = i
* 3 + 1;
284 relvars
[2] = i
* 3 + 2;
285 relvars
[3] = i
* 3 + 3;
286 relvars
[4] = i
* 3 + 4;
287 relvars
[5] = i
* 3 + 5;
288 relvarset
= sylvan_set_fromarray(relvars
, 6);
296 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
297 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
298 trs_current
->varset
.varset
= relvarset
;
299 trs_current
->varset
.size
= 6;
300 trs_current
->next_rel
= trs
;
304 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
306 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
307 int deltai
= bddvar
->value
.var
[0];
309 //Free Agent -> Agent Free
310 //(0 1 0 0 1 1 1 0 0 0 1 1)
311 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};
312 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
313 uint8_t rel_enc
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
314 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
315 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
316 trs_current
->varset
.varset
= relvarset
;
317 trs_current
->varset
.size
= 12;
318 trs_current
->next_rel
= trs
;
321 //Target Agent -> Targagent Free
322 //(0 1 1 1 1 0 1 0 0 0 1 1)
323 relvars
[0] = deltai
*3;
324 relvars
[1] = deltai
*3+1;
325 relvars
[2] = deltai
*3+2;
326 relvars
[3] = deltai
*3+3;
327 relvars
[4] = deltai
*3+4;
328 relvars
[5] = deltai
*3+5;
335 relvarset
= sylvan_set_fromarray(relvars
, 12);
348 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
349 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
350 trs_current
->varset
.varset
= relvarset
;
351 trs_current
->varset
.size
= 12;
352 trs_current
->next_rel
= trs
;
355 //REPAIR! Must be: Free Targagent -> Agent Target
356 //(0 1 0 0 1 1 1 0 1 1 0 1)
357 relvars
[0] = deltai
*3;
358 relvars
[1] = deltai
*3+1;
359 relvars
[2] = deltai
*3+2;
360 relvars
[3] = deltai
*3+3;
361 relvars
[4] = deltai
*3+4;
362 relvars
[5] = deltai
*3+5;
369 relvarset
= sylvan_set_fromarray(relvars
, 12);
382 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
383 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
384 trs_current
->varset
.varset
= relvarset
;
385 trs_current
->varset
.size
= 12;
386 trs_current
->next_rel
= trs
;
389 //Target Targagent -> Targagent Target
390 //(0 1 1 1 1 0 1 0 1 1 0 1)
391 relvars
[0] = deltai
*3;
392 relvars
[1] = deltai
*3+1;
393 relvars
[2] = deltai
*3+2;
394 relvars
[3] = deltai
*3+3;
395 relvars
[4] = deltai
*3+4;
396 relvars
[5] = deltai
*3+5;
403 relvarset
= sylvan_set_fromarray(relvars
, 12);
416 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
417 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
418 trs_current
->varset
.varset
= relvarset
;
419 trs_current
->varset
.size
= 12;
420 trs_current
->next_rel
= trs
;
423 //Box Agent -> Box Agent
424 //(0 0 1 1 0 0 1 1 0 0 1 1)
425 relvars
[0] = deltai
*3;
426 relvars
[1] = deltai
*3+1;
427 relvars
[2] = deltai
*3+2;
428 relvars
[3] = deltai
*3+3;
429 relvars
[4] = deltai
*3+4;
430 relvars
[5] = deltai
*3+5;
437 relvarset
= sylvan_set_fromarray(relvars
, 12);
450 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
451 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
452 trs_current
->varset
.varset
= relvarset
;
453 trs_current
->varset
.size
= 12;
454 trs_current
->next_rel
= trs
;
457 //Targbox Agent -> Targbox Agent
458 //(1 1 0 0 0 0 1 1 0 0 1 1)
459 relvars
[0] = deltai
*3;
460 relvars
[1] = deltai
*3+1;
461 relvars
[2] = deltai
*3+2;
462 relvars
[3] = deltai
*3+3;
463 relvars
[4] = deltai
*3+4;
464 relvars
[5] = deltai
*3+5;
471 relvarset
= sylvan_set_fromarray(relvars
, 12);
484 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
485 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
486 trs_current
->varset
.varset
= relvarset
;
487 trs_current
->varset
.size
= 12;
488 trs_current
->next_rel
= trs
;
491 //Box Targagent -> Box Targagent
492 //(0 0 1 1 0 0 1 1 1 1 0 0)
493 relvars
[0] = deltai
*3;
494 relvars
[1] = deltai
*3+1;
495 relvars
[2] = deltai
*3+2;
496 relvars
[3] = deltai
*3+3;
497 relvars
[4] = deltai
*3+4;
498 relvars
[5] = deltai
*3+5;
505 relvarset
= sylvan_set_fromarray(relvars
, 12);
518 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
519 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
520 trs_current
->varset
.varset
= relvarset
;
521 trs_current
->varset
.size
= 12;
522 trs_current
->next_rel
= trs
;
525 //Targbox Targagent -> Targbox Targagent
526 //(1 1 0 0 0 0 1 1 1 1 0 0)
527 relvars
[0] = deltai
*3;
528 relvars
[1] = deltai
*3+1;
529 relvars
[2] = deltai
*3+2;
530 relvars
[3] = deltai
*3+3;
531 relvars
[4] = deltai
*3+4;
532 relvars
[5] = deltai
*3+5;
539 relvarset
= sylvan_set_fromarray(relvars
, 12);
552 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
553 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
554 trs_current
->varset
.varset
= relvarset
;
555 trs_current
->varset
.size
= 12;
556 trs_current
->next_rel
= trs
;
560 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
562 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
563 int deltai
= bddvar
->value
.var
[0];
564 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
565 int gammai
= bddvar
->value
.var
[0];
567 //(0 1 0 0 1 1 1 0 0 0 1 1)
568 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};
569 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
570 uint8_t rel_enc
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
571 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
572 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
573 trs_current
->varset
.varset
= relvarset
;
574 trs_current
->varset
.size
= 12;
575 trs_current
->next_rel
= trs
;
578 //(0 1 1 0 1 1 1 0 0 1 1 1)
579 relvars
[0] = deltai
*3;
580 relvars
[1] = deltai
*3+1;
581 relvars
[2] = deltai
*3+2;
582 relvars
[3] = deltai
*3+3;
583 relvars
[4] = deltai
*3+4;
584 relvars
[5] = deltai
*3+5;
591 relvarset
= sylvan_set_fromarray(relvars
, 12);
604 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
605 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
606 trs_current
->varset
.varset
= relvarset
;
607 trs_current
->varset
.size
= 12;
608 trs_current
->next_rel
= trs
;
611 //(0 1 0 1 1 0 1 0 1 0 0 1)
612 relvars
[0] = deltai
*3;
613 relvars
[1] = deltai
*3+1;
614 relvars
[2] = deltai
*3+2;
615 relvars
[3] = deltai
*3+3;
616 relvars
[4] = deltai
*3+4;
617 relvars
[5] = deltai
*3+5;
624 relvarset
= sylvan_set_fromarray(relvars
, 12);
637 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
638 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
639 trs_current
->varset
.varset
= relvarset
;
640 trs_current
->varset
.size
= 12;
641 trs_current
->next_rel
= trs
;
644 //(0 1 1 1 1 0 1 0 1 1 0 1)
645 relvars
[0] = deltai
*3;
646 relvars
[1] = deltai
*3+1;
647 relvars
[2] = deltai
*3+2;
648 relvars
[3] = deltai
*3+3;
649 relvars
[4] = deltai
*3+4;
650 relvars
[5] = deltai
*3+5;
657 relvarset
= sylvan_set_fromarray(relvars
, 12);
670 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
671 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
672 trs_current
->varset
.varset
= relvarset
;
673 trs_current
->varset
.size
= 12;
674 trs_current
->next_rel
= trs
;
677 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
678 BDDVAR relvars1
[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};
679 relvars1
[0] = gammai
*3;
680 relvars1
[1] = gammai
*3+1;
681 relvars1
[2] = gammai
*3+2;
682 relvars1
[3] = gammai
*3+3;
683 relvars1
[4] = gammai
*3+4;
684 relvars1
[5] = gammai
*3+5;
685 relvars1
[6] = deltai
*3;
686 relvars1
[7] = deltai
*3+1;
687 relvars1
[8] = deltai
*3+2;
688 relvars1
[9] = deltai
*3+3;
689 relvars1
[10] = deltai
*3+4;
690 relvars1
[11] = deltai
*3+5;
692 relvars1
[13] = i
*3+1;
693 relvars1
[14] = i
*3+2;
694 relvars1
[15] = i
*3+3;
695 relvars1
[16] = i
*3+4;
696 relvars1
[17] = i
*3+5;
697 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
698 uint8_t rel_enc1
[18];
717 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
718 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
719 trs_current
->varset
.varset
= relvarset1
;
720 trs_current
->varset
.size
= 18;
721 trs_current
->next_rel
= trs
;
724 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
725 relvars1
[0] = gammai
*3;
726 relvars1
[1] = gammai
*3+1;
727 relvars1
[2] = gammai
*3+2;
728 relvars1
[3] = gammai
*3+3;
729 relvars1
[4] = gammai
*3+4;
730 relvars1
[5] = gammai
*3+5;
731 relvars1
[6] = deltai
*3;
732 relvars1
[7] = deltai
*3+1;
733 relvars1
[8] = deltai
*3+2;
734 relvars1
[9] = deltai
*3+3;
735 relvars1
[10] = deltai
*3+4;
736 relvars1
[11] = deltai
*3+5;
738 relvars1
[13] = i
*3+1;
739 relvars1
[14] = i
*3+2;
740 relvars1
[15] = i
*3+3;
741 relvars1
[16] = i
*3+4;
742 relvars1
[17] = i
*3+5;
743 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
762 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
763 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
764 trs_current
->varset
.varset
= relvarset1
;
765 trs_current
->varset
.size
= 18;
766 trs_current
->next_rel
= trs
;
769 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
770 relvars1
[0] = gammai
*3;
771 relvars1
[1] = gammai
*3+1;
772 relvars1
[2] = gammai
*3+2;
773 relvars1
[3] = gammai
*3+3;
774 relvars1
[4] = gammai
*3+4;
775 relvars1
[5] = gammai
*3+5;
776 relvars1
[6] = deltai
*3;
777 relvars1
[7] = deltai
*3+1;
778 relvars1
[8] = deltai
*3+2;
779 relvars1
[9] = deltai
*3+3;
780 relvars1
[10] = deltai
*3+4;
781 relvars1
[11] = deltai
*3+5;
783 relvars1
[13] = i
*3+1;
784 relvars1
[14] = i
*3+2;
785 relvars1
[15] = i
*3+3;
786 relvars1
[16] = i
*3+4;
787 relvars1
[17] = i
*3+5;
788 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
789 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
808 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
809 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
810 trs_current
->varset
.varset
= relvarset1
;
811 trs_current
->varset
.size
= 18;
812 trs_current
->next_rel
= trs
;
815 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
816 relvars1
[0] = gammai
*3;
817 relvars1
[1] = gammai
*3+1;
818 relvars1
[2] = gammai
*3+2;
819 relvars1
[3] = gammai
*3+3;
820 relvars1
[4] = gammai
*3+4;
821 relvars1
[5] = gammai
*3+5;
822 relvars1
[6] = deltai
*3;
823 relvars1
[7] = deltai
*3+1;
824 relvars1
[8] = deltai
*3+2;
825 relvars1
[9] = deltai
*3+3;
826 relvars1
[10] = deltai
*3+4;
827 relvars1
[11] = deltai
*3+5;
829 relvars1
[13] = i
*3+1;
830 relvars1
[14] = i
*3+2;
831 relvars1
[15] = i
*3+3;
832 relvars1
[16] = i
*3+4;
833 relvars1
[17] = i
*3+5;
834 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
835 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
854 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
855 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
856 trs_current
->varset
.varset
= relvarset1
;
857 trs_current
->varset
.size
= 18;
858 trs_current
->next_rel
= trs
;
861 //free box agent -> box agent free
862 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
863 relvars1
[0] = gammai
*3;
864 relvars1
[1] = gammai
*3+1;
865 relvars1
[2] = gammai
*3+2;
866 relvars1
[3] = gammai
*3+3;
867 relvars1
[4] = gammai
*3+4;
868 relvars1
[5] = gammai
*3+5;
869 relvars1
[6] = deltai
*3;
870 relvars1
[7] = deltai
*3+1;
871 relvars1
[8] = deltai
*3+2;
872 relvars1
[9] = deltai
*3+3;
873 relvars1
[10] = deltai
*3+4;
874 relvars1
[11] = deltai
*3+5;
876 relvars1
[13] = i
*3+1;
877 relvars1
[14] = i
*3+2;
878 relvars1
[15] = i
*3+3;
879 relvars1
[16] = i
*3+4;
880 relvars1
[17] = i
*3+5;
881 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
882 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
901 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
902 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
903 trs_current
->varset
.varset
= relvarset1
;
904 trs_current
->varset
.size
= 18;
905 trs_current
->next_rel
= trs
;
908 //(free targbox agent -> box targagent free)
909 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
910 relvars1
[0] = gammai
*3;
911 relvars1
[1] = gammai
*3+1;
912 relvars1
[2] = gammai
*3+2;
913 relvars1
[3] = gammai
*3+3;
914 relvars1
[4] = gammai
*3+4;
915 relvars1
[5] = gammai
*3+5;
916 relvars1
[6] = deltai
*3;
917 relvars1
[7] = deltai
*3+1;
918 relvars1
[8] = deltai
*3+2;
919 relvars1
[9] = deltai
*3+3;
920 relvars1
[10] = deltai
*3+4;
921 relvars1
[11] = deltai
*3+5;
923 relvars1
[13] = i
*3+1;
924 relvars1
[14] = i
*3+2;
925 relvars1
[15] = i
*3+3;
926 relvars1
[16] = i
*3+4;
927 relvars1
[17] = i
*3+5;
928 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
929 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
948 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
949 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
950 trs_current
->varset
.varset
= relvarset1
;
951 trs_current
->varset
.size
= 18;
952 trs_current
->next_rel
= trs
;
955 //(target box agent -> targbox agent free)
956 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
957 relvars1
[0] = gammai
*3;
958 relvars1
[1] = gammai
*3+1;
959 relvars1
[2] = gammai
*3+2;
960 relvars1
[3] = gammai
*3+3;
961 relvars1
[4] = gammai
*3+4;
962 relvars1
[5] = gammai
*3+5;
963 relvars1
[6] = deltai
*3;
964 relvars1
[7] = deltai
*3+1;
965 relvars1
[8] = deltai
*3+2;
966 relvars1
[9] = deltai
*3+3;
967 relvars1
[10] = deltai
*3+4;
968 relvars1
[11] = deltai
*3+5;
970 relvars1
[13] = i
*3+1;
971 relvars1
[14] = i
*3+2;
972 relvars1
[15] = i
*3+3;
973 relvars1
[16] = i
*3+4;
974 relvars1
[17] = i
*3+5;
975 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
976 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
995 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
996 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
997 trs_current
->varset
.varset
= relvarset1
;
998 trs_current
->varset
.size
= 18;
999 trs_current
->next_rel
= trs
;
1002 //(target targbox agent -> targbox targagent free)
1003 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1004 relvars1
[0] = gammai
*3;
1005 relvars1
[1] = gammai
*3+1;
1006 relvars1
[2] = gammai
*3+2;
1007 relvars1
[3] = gammai
*3+3;
1008 relvars1
[4] = gammai
*3+4;
1009 relvars1
[5] = gammai
*3+5;
1010 relvars1
[6] = deltai
*3;
1011 relvars1
[7] = deltai
*3+1;
1012 relvars1
[8] = deltai
*3+2;
1013 relvars1
[9] = deltai
*3+3;
1014 relvars1
[10] = deltai
*3+4;
1015 relvars1
[11] = deltai
*3+5;
1017 relvars1
[13] = i
*3+1;
1018 relvars1
[14] = i
*3+2;
1019 relvars1
[15] = i
*3+3;
1020 relvars1
[16] = i
*3+4;
1021 relvars1
[17] = i
*3+5;
1022 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1023 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1042 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1043 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1044 trs_current
->varset
.varset
= relvarset1
;
1045 trs_current
->varset
.size
= 18;
1046 trs_current
->next_rel
= trs
;
1049 //(free box targagent -> box agent target)
1050 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1051 relvars1
[0] = gammai
*3;
1052 relvars1
[1] = gammai
*3+1;
1053 relvars1
[2] = gammai
*3+2;
1054 relvars1
[3] = gammai
*3+3;
1055 relvars1
[4] = gammai
*3+4;
1056 relvars1
[5] = gammai
*3+5;
1057 relvars1
[6] = deltai
*3;
1058 relvars1
[7] = deltai
*3+1;
1059 relvars1
[8] = deltai
*3+2;
1060 relvars1
[9] = deltai
*3+3;
1061 relvars1
[10] = deltai
*3+4;
1062 relvars1
[11] = deltai
*3+5;
1064 relvars1
[13] = i
*3+1;
1065 relvars1
[14] = i
*3+2;
1066 relvars1
[15] = i
*3+3;
1067 relvars1
[16] = i
*3+4;
1068 relvars1
[17] = i
*3+5;
1069 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1070 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1089 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1090 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1091 trs_current
->varset
.varset
= relvarset1
;
1092 trs_current
->varset
.size
= 18;
1093 trs_current
->next_rel
= trs
;
1096 //(free targbox targagent -> box targagent target)
1097 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1098 relvars1
[0] = gammai
*3;
1099 relvars1
[1] = gammai
*3+1;
1100 relvars1
[2] = gammai
*3+2;
1101 relvars1
[3] = gammai
*3+3;
1102 relvars1
[4] = gammai
*3+4;
1103 relvars1
[5] = gammai
*3+5;
1104 relvars1
[6] = deltai
*3;
1105 relvars1
[7] = deltai
*3+1;
1106 relvars1
[8] = deltai
*3+2;
1107 relvars1
[9] = deltai
*3+3;
1108 relvars1
[10] = deltai
*3+4;
1109 relvars1
[11] = deltai
*3+5;
1111 relvars1
[13] = i
*3+1;
1112 relvars1
[14] = i
*3+2;
1113 relvars1
[15] = i
*3+3;
1114 relvars1
[16] = i
*3+4;
1115 relvars1
[17] = i
*3+5;
1116 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1117 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1136 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1137 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1138 trs_current
->varset
.varset
= relvarset1
;
1139 trs_current
->varset
.size
= 18;
1140 trs_current
->next_rel
= trs
;
1143 //(target box targagent -> targbox agent target)
1144 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1145 relvars1
[0] = gammai
*3;
1146 relvars1
[1] = gammai
*3+1;
1147 relvars1
[2] = gammai
*3+2;
1148 relvars1
[3] = gammai
*3+3;
1149 relvars1
[4] = gammai
*3+4;
1150 relvars1
[5] = gammai
*3+5;
1151 relvars1
[6] = deltai
*3;
1152 relvars1
[7] = deltai
*3+1;
1153 relvars1
[8] = deltai
*3+2;
1154 relvars1
[9] = deltai
*3+3;
1155 relvars1
[10] = deltai
*3+4;
1156 relvars1
[11] = deltai
*3+5;
1158 relvars1
[13] = i
*3+1;
1159 relvars1
[14] = i
*3+2;
1160 relvars1
[15] = i
*3+3;
1161 relvars1
[16] = i
*3+4;
1162 relvars1
[17] = i
*3+5;
1163 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1164 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1183 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1184 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1185 trs_current
->varset
.varset
= relvarset1
;
1186 trs_current
->varset
.size
= 18;
1187 trs_current
->next_rel
= trs
;
1190 //(target targbox targagent -> targbox targagent target)
1191 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1192 relvars1
[0] = gammai
*3;
1193 relvars1
[1] = gammai
*3+1;
1194 relvars1
[2] = gammai
*3+2;
1195 relvars1
[3] = gammai
*3+3;
1196 relvars1
[4] = gammai
*3+4;
1197 relvars1
[5] = gammai
*3+5;
1198 relvars1
[6] = deltai
*3;
1199 relvars1
[7] = deltai
*3+1;
1200 relvars1
[8] = deltai
*3+2;
1201 relvars1
[9] = deltai
*3+3;
1202 relvars1
[10] = deltai
*3+4;
1203 relvars1
[11] = deltai
*3+5;
1205 relvars1
[13] = i
*3+1;
1206 relvars1
[14] = i
*3+2;
1207 relvars1
[15] = i
*3+3;
1208 relvars1
[16] = i
*3+4;
1209 relvars1
[17] = i
*3+5;
1210 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1211 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1230 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1231 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1232 trs_current
->varset
.varset
= relvarset1
;
1233 trs_current
->varset
.size
= 18;
1234 trs_current
->next_rel
= trs
;
1242 rels
*encode_rel(sokoban_screen
*screen
)
1246 trans_t
*tl
= sylvan_false
;
1249 tl
= create_single_rel(screen
, LEFT
);
1252 trans_t
*tu
= create_single_rel(screen
, UP
);
1255 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1258 trans_t
*td
= create_single_rel(screen
, DOWN
);
1261 rls
= (rels
*)malloc(sizeof(rels
));
1275 BDDVAR vars
[] = {0,2,4};
1276 BDDVAR all_vars
[] = {0,1,2,3,4,5};
1277 BDDVAR all_vars2
[] = {0,1};
1278 //BDDVAR short_vars[] = {0,1};
1279 /*BDDVAR short_vars2[] = {2,3};
1280 BDDVAR short_vars3[] = {0,1,2,3};*/
1282 BDDSET vars_set
= sylvan_set_fromarray(vars
, 3);
1283 BDDSET all_vars_set
= sylvan_set_fromarray(all_vars
, 6);
1284 BDDSET all_vars_set2
= sylvan_set_fromarray(all_vars2
, 2);
1285 //BDDSET short_vars_set = sylvan_set_fromarray(short_vars, 2);
1286 /*BDDSET short_vars_set2 = sylvan_set_fromarray(short_vars2, 2);
1287 BDDSET short_vars_set3 = sylvan_set_fromarray(short_vars3, 4);*/
1289 BDD s
, t
, next
, prev
;
1292 // transition relation: 000 --> 111 and !000 --> 000
1294 t
= sylvan_union_cube(t
, all_vars_set2
, ((uint8_t[]){0,1}));
1295 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0}));
1296 t
= sylvan_union_cube(t
, all_vars_set2
, ((uint8_t[]){1,0}));
1297 // t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1}));
1299 s
= sylvan_cube(vars_set
, (uint8_t[]){0,0,0});
1300 zeroes
= sylvan_cube(vars_set
, (uint8_t[]){1,0,0});
1301 ones
= sylvan_cube(vars_set
, (uint8_t[]){0,0,0});
1303 next
= sylvan_relnext(s
, t
, all_vars_set
);
1304 prev
= sylvan_relprev(t
, next
, all_vars_set
);
1305 if (next
== zeroes
) printf("Pass 1\n");
1306 if (prev
== ones
) printf("Pass 2\n");