e54fe568c428c2f6818ec9a16abd94fd50f3c0fb
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){
267 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
268 BDDVAR relvars
[6] = {i
* 3, i
* 3 + 1, i
* 3 + 2, i
* 3 + 3, i
* 3 + 4, i
* 3 + 5};
269 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
270 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
272 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
273 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
274 trs_current
->varset
.varset
= relvarset
;
275 trs_current
->varset
.size
= 6;
276 trs_current
->next_rel
= trs
;
279 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
281 relvars
[1] = i
* 3 + 1;
282 relvars
[2] = i
* 3 + 2;
283 relvars
[3] = i
* 3 + 3;
284 relvars
[4] = i
* 3 + 4;
285 relvars
[5] = i
* 3 + 5;
286 relvarset
= sylvan_set_fromarray(relvars
, 6);
294 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
295 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
296 trs_current
->varset
.varset
= relvarset
;
297 trs_current
->varset
.size
= 6;
298 trs_current
->next_rel
= trs
;
302 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
304 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
305 int deltai
= bddvar
->value
.var
[0];
307 //(0 1 0 0 1 1 1 0 0 0 1 1)
308 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};
309 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
310 uint8_t rel_enc
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
311 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
312 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
313 trs_current
->varset
.varset
= relvarset
;
314 trs_current
->varset
.size
= 12;
315 trs_current
->next_rel
= trs
;
318 //(0 1 1 0 1 1 1 0 0 1 1 1)
319 relvars
[0] = deltai
*3;
320 relvars
[1] = deltai
*3+1;
321 relvars
[2] = deltai
*3+2;
322 relvars
[3] = deltai
*3+3;
323 relvars
[4] = deltai
*3+4;
324 relvars
[5] = deltai
*3+5;
331 relvarset
= sylvan_set_fromarray(relvars
, 12);
344 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
345 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
346 trs_current
->varset
.varset
= relvarset
;
347 trs_current
->varset
.size
= 12;
348 trs_current
->next_rel
= trs
;
351 //(0 1 0 1 1 0 1 0 1 0 0 1)
352 relvars
[0] = deltai
*3;
353 relvars
[1] = deltai
*3+1;
354 relvars
[2] = deltai
*3+2;
355 relvars
[3] = deltai
*3+3;
356 relvars
[4] = deltai
*3+4;
357 relvars
[5] = deltai
*3+5;
364 relvarset
= sylvan_set_fromarray(relvars
, 12);
377 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
378 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
379 trs_current
->varset
.varset
= relvarset
;
380 trs_current
->varset
.size
= 12;
381 trs_current
->next_rel
= trs
;
384 //(0 1 1 1 1 0 1 0 1 1 0 1)
385 relvars
[0] = deltai
*3;
386 relvars
[1] = deltai
*3+1;
387 relvars
[2] = deltai
*3+2;
388 relvars
[3] = deltai
*3+3;
389 relvars
[4] = deltai
*3+4;
390 relvars
[5] = deltai
*3+5;
397 relvarset
= sylvan_set_fromarray(relvars
, 12);
410 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
411 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
412 trs_current
->varset
.varset
= relvarset
;
413 trs_current
->varset
.size
= 12;
414 trs_current
->next_rel
= trs
;
417 //(0 0 1 1 0 0 1 1 0 0 1 1)
418 relvars
[0] = deltai
*3;
419 relvars
[1] = deltai
*3+1;
420 relvars
[2] = deltai
*3+2;
421 relvars
[3] = deltai
*3+3;
422 relvars
[4] = deltai
*3+4;
423 relvars
[5] = deltai
*3+5;
430 relvarset
= sylvan_set_fromarray(relvars
, 12);
443 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
444 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
445 trs_current
->varset
.varset
= relvarset
;
446 trs_current
->varset
.size
= 12;
447 trs_current
->next_rel
= trs
;
450 //(1 1 0 0 0 0 1 1 0 0 1 1)
451 relvars
[0] = deltai
*3;
452 relvars
[1] = deltai
*3+1;
453 relvars
[2] = deltai
*3+2;
454 relvars
[3] = deltai
*3+3;
455 relvars
[4] = deltai
*3+4;
456 relvars
[5] = deltai
*3+5;
463 relvarset
= sylvan_set_fromarray(relvars
, 12);
476 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
477 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
478 trs_current
->varset
.varset
= relvarset
;
479 trs_current
->varset
.size
= 12;
480 trs_current
->next_rel
= trs
;
483 //(0 0 1 1 0 0 1 1 1 1 0 0)
484 relvars
[0] = deltai
*3;
485 relvars
[1] = deltai
*3+1;
486 relvars
[2] = deltai
*3+2;
487 relvars
[3] = deltai
*3+3;
488 relvars
[4] = deltai
*3+4;
489 relvars
[5] = deltai
*3+5;
496 relvarset
= sylvan_set_fromarray(relvars
, 12);
509 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
510 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
511 trs_current
->varset
.varset
= relvarset
;
512 trs_current
->varset
.size
= 12;
513 trs_current
->next_rel
= trs
;
516 //(1 1 0 0 0 0 1 1 1 1 0 0)
517 relvars
[0] = deltai
*3;
518 relvars
[1] = deltai
*3+1;
519 relvars
[2] = deltai
*3+2;
520 relvars
[3] = deltai
*3+3;
521 relvars
[4] = deltai
*3+4;
522 relvars
[5] = deltai
*3+5;
529 relvarset
= sylvan_set_fromarray(relvars
, 12);
542 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
543 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
544 trs_current
->varset
.varset
= relvarset
;
545 trs_current
->varset
.size
= 12;
546 trs_current
->next_rel
= trs
;
550 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
552 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
553 int deltai
= bddvar
->value
.var
[0];
554 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
555 int gammai
= bddvar
->value
.var
[0];
557 //(0 1 0 0 1 1 1 0 0 0 1 1)
558 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};
559 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
560 uint8_t rel_enc
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
561 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
562 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
563 trs_current
->varset
.varset
= relvarset
;
564 trs_current
->varset
.size
= 12;
565 trs_current
->next_rel
= trs
;
568 //(0 1 1 0 1 1 1 0 0 1 1 1)
569 relvars
[0] = deltai
*3;
570 relvars
[1] = deltai
*3+1;
571 relvars
[2] = deltai
*3+2;
572 relvars
[3] = deltai
*3+3;
573 relvars
[4] = deltai
*3+4;
574 relvars
[5] = deltai
*3+5;
581 relvarset
= sylvan_set_fromarray(relvars
, 12);
594 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
595 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
596 trs_current
->varset
.varset
= relvarset
;
597 trs_current
->varset
.size
= 12;
598 trs_current
->next_rel
= trs
;
601 //(0 1 0 1 1 0 1 0 1 0 0 1)
602 relvars
[0] = deltai
*3;
603 relvars
[1] = deltai
*3+1;
604 relvars
[2] = deltai
*3+2;
605 relvars
[3] = deltai
*3+3;
606 relvars
[4] = deltai
*3+4;
607 relvars
[5] = deltai
*3+5;
614 relvarset
= sylvan_set_fromarray(relvars
, 12);
627 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
628 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
629 trs_current
->varset
.varset
= relvarset
;
630 trs_current
->varset
.size
= 12;
631 trs_current
->next_rel
= trs
;
634 //(0 1 1 1 1 0 1 0 1 1 0 1)
635 relvars
[0] = deltai
*3;
636 relvars
[1] = deltai
*3+1;
637 relvars
[2] = deltai
*3+2;
638 relvars
[3] = deltai
*3+3;
639 relvars
[4] = deltai
*3+4;
640 relvars
[5] = deltai
*3+5;
647 relvarset
= sylvan_set_fromarray(relvars
, 12);
660 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
661 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
662 trs_current
->varset
.varset
= relvarset
;
663 trs_current
->varset
.size
= 12;
664 trs_current
->next_rel
= trs
;
667 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
668 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};
669 relvars1
[0] = gammai
*3;
670 relvars1
[1] = gammai
*3+1;
671 relvars1
[2] = gammai
*3+2;
672 relvars1
[3] = gammai
*3+3;
673 relvars1
[4] = gammai
*3+4;
674 relvars1
[5] = gammai
*3+5;
675 relvars1
[6] = deltai
*3;
676 relvars1
[7] = deltai
*3+1;
677 relvars1
[8] = deltai
*3+2;
678 relvars1
[9] = deltai
*3+3;
679 relvars1
[10] = deltai
*3+4;
680 relvars1
[11] = deltai
*3+5;
682 relvars1
[13] = i
*3+1;
683 relvars1
[14] = i
*3+2;
684 relvars1
[15] = i
*3+3;
685 relvars1
[16] = i
*3+4;
686 relvars1
[17] = i
*3+5;
687 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
688 uint8_t rel_enc1
[18];
707 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
708 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
709 trs_current
->varset
.varset
= relvarset1
;
710 trs_current
->varset
.size
= 18;
711 trs_current
->next_rel
= trs
;
714 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
715 relvars1
[0] = gammai
*3;
716 relvars1
[1] = gammai
*3+1;
717 relvars1
[2] = gammai
*3+2;
718 relvars1
[3] = gammai
*3+3;
719 relvars1
[4] = gammai
*3+4;
720 relvars1
[5] = gammai
*3+5;
721 relvars1
[6] = deltai
*3;
722 relvars1
[7] = deltai
*3+1;
723 relvars1
[8] = deltai
*3+2;
724 relvars1
[9] = deltai
*3+3;
725 relvars1
[10] = deltai
*3+4;
726 relvars1
[11] = deltai
*3+5;
728 relvars1
[13] = i
*3+1;
729 relvars1
[14] = i
*3+2;
730 relvars1
[15] = i
*3+3;
731 relvars1
[16] = i
*3+4;
732 relvars1
[17] = i
*3+5;
733 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
752 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
753 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
754 trs_current
->varset
.varset
= relvarset1
;
755 trs_current
->varset
.size
= 18;
756 trs_current
->next_rel
= trs
;
759 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
760 relvars1
[0] = gammai
*3;
761 relvars1
[1] = gammai
*3+1;
762 relvars1
[2] = gammai
*3+2;
763 relvars1
[3] = gammai
*3+3;
764 relvars1
[4] = gammai
*3+4;
765 relvars1
[5] = gammai
*3+5;
766 relvars1
[6] = deltai
*3;
767 relvars1
[7] = deltai
*3+1;
768 relvars1
[8] = deltai
*3+2;
769 relvars1
[9] = deltai
*3+3;
770 relvars1
[10] = deltai
*3+4;
771 relvars1
[11] = deltai
*3+5;
773 relvars1
[13] = i
*3+1;
774 relvars1
[14] = i
*3+2;
775 relvars1
[15] = i
*3+3;
776 relvars1
[16] = i
*3+4;
777 relvars1
[17] = i
*3+5;
778 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
779 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
798 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
799 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
800 trs_current
->varset
.varset
= relvarset1
;
801 trs_current
->varset
.size
= 18;
802 trs_current
->next_rel
= trs
;
805 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
806 relvars1
[0] = gammai
*3;
807 relvars1
[1] = gammai
*3+1;
808 relvars1
[2] = gammai
*3+2;
809 relvars1
[3] = gammai
*3+3;
810 relvars1
[4] = gammai
*3+4;
811 relvars1
[5] = gammai
*3+5;
812 relvars1
[6] = deltai
*3;
813 relvars1
[7] = deltai
*3+1;
814 relvars1
[8] = deltai
*3+2;
815 relvars1
[9] = deltai
*3+3;
816 relvars1
[10] = deltai
*3+4;
817 relvars1
[11] = deltai
*3+5;
819 relvars1
[13] = i
*3+1;
820 relvars1
[14] = i
*3+2;
821 relvars1
[15] = i
*3+3;
822 relvars1
[16] = i
*3+4;
823 relvars1
[17] = i
*3+5;
824 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
825 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
844 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
845 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
846 trs_current
->varset
.varset
= relvarset1
;
847 trs_current
->varset
.size
= 18;
848 trs_current
->next_rel
= trs
;
851 //free box agent -> box agent free
852 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
853 relvars1
[0] = gammai
*3;
854 relvars1
[1] = gammai
*3+1;
855 relvars1
[2] = gammai
*3+2;
856 relvars1
[3] = gammai
*3+3;
857 relvars1
[4] = gammai
*3+4;
858 relvars1
[5] = gammai
*3+5;
859 relvars1
[6] = deltai
*3;
860 relvars1
[7] = deltai
*3+1;
861 relvars1
[8] = deltai
*3+2;
862 relvars1
[9] = deltai
*3+3;
863 relvars1
[10] = deltai
*3+4;
864 relvars1
[11] = deltai
*3+5;
866 relvars1
[13] = i
*3+1;
867 relvars1
[14] = i
*3+2;
868 relvars1
[15] = i
*3+3;
869 relvars1
[16] = i
*3+4;
870 relvars1
[17] = i
*3+5;
871 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
872 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
891 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
892 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
893 trs_current
->varset
.varset
= relvarset1
;
894 trs_current
->varset
.size
= 18;
895 trs_current
->next_rel
= trs
;
898 //(free targbox agent -> box targagent free)
899 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
900 relvars1
[0] = gammai
*3;
901 relvars1
[1] = gammai
*3+1;
902 relvars1
[2] = gammai
*3+2;
903 relvars1
[3] = gammai
*3+3;
904 relvars1
[4] = gammai
*3+4;
905 relvars1
[5] = gammai
*3+5;
906 relvars1
[6] = deltai
*3;
907 relvars1
[7] = deltai
*3+1;
908 relvars1
[8] = deltai
*3+2;
909 relvars1
[9] = deltai
*3+3;
910 relvars1
[10] = deltai
*3+4;
911 relvars1
[11] = deltai
*3+5;
913 relvars1
[13] = i
*3+1;
914 relvars1
[14] = i
*3+2;
915 relvars1
[15] = i
*3+3;
916 relvars1
[16] = i
*3+4;
917 relvars1
[17] = i
*3+5;
918 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
919 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
938 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
939 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
940 trs_current
->varset
.varset
= relvarset1
;
941 trs_current
->varset
.size
= 18;
942 trs_current
->next_rel
= trs
;
945 //(target box agent -> targbox agent free)
946 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
947 relvars1
[0] = gammai
*3;
948 relvars1
[1] = gammai
*3+1;
949 relvars1
[2] = gammai
*3+2;
950 relvars1
[3] = gammai
*3+3;
951 relvars1
[4] = gammai
*3+4;
952 relvars1
[5] = gammai
*3+5;
953 relvars1
[6] = deltai
*3;
954 relvars1
[7] = deltai
*3+1;
955 relvars1
[8] = deltai
*3+2;
956 relvars1
[9] = deltai
*3+3;
957 relvars1
[10] = deltai
*3+4;
958 relvars1
[11] = deltai
*3+5;
960 relvars1
[13] = i
*3+1;
961 relvars1
[14] = i
*3+2;
962 relvars1
[15] = i
*3+3;
963 relvars1
[16] = i
*3+4;
964 relvars1
[17] = i
*3+5;
965 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
966 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
985 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
986 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
987 trs_current
->varset
.varset
= relvarset1
;
988 trs_current
->varset
.size
= 18;
989 trs_current
->next_rel
= trs
;
992 //(target targbox agent -> targbox targagent free)
993 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
994 relvars1
[0] = gammai
*3;
995 relvars1
[1] = gammai
*3+1;
996 relvars1
[2] = gammai
*3+2;
997 relvars1
[3] = gammai
*3+3;
998 relvars1
[4] = gammai
*3+4;
999 relvars1
[5] = gammai
*3+5;
1000 relvars1
[6] = deltai
*3;
1001 relvars1
[7] = deltai
*3+1;
1002 relvars1
[8] = deltai
*3+2;
1003 relvars1
[9] = deltai
*3+3;
1004 relvars1
[10] = deltai
*3+4;
1005 relvars1
[11] = deltai
*3+5;
1007 relvars1
[13] = i
*3+1;
1008 relvars1
[14] = i
*3+2;
1009 relvars1
[15] = i
*3+3;
1010 relvars1
[16] = i
*3+4;
1011 relvars1
[17] = i
*3+5;
1012 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1013 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1032 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1033 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1034 trs_current
->varset
.varset
= relvarset1
;
1035 trs_current
->varset
.size
= 18;
1036 trs_current
->next_rel
= trs
;
1039 //(free box targagent -> box agent target)
1040 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1041 relvars1
[0] = gammai
*3;
1042 relvars1
[1] = gammai
*3+1;
1043 relvars1
[2] = gammai
*3+2;
1044 relvars1
[3] = gammai
*3+3;
1045 relvars1
[4] = gammai
*3+4;
1046 relvars1
[5] = gammai
*3+5;
1047 relvars1
[6] = deltai
*3;
1048 relvars1
[7] = deltai
*3+1;
1049 relvars1
[8] = deltai
*3+2;
1050 relvars1
[9] = deltai
*3+3;
1051 relvars1
[10] = deltai
*3+4;
1052 relvars1
[11] = deltai
*3+5;
1054 relvars1
[13] = i
*3+1;
1055 relvars1
[14] = i
*3+2;
1056 relvars1
[15] = i
*3+3;
1057 relvars1
[16] = i
*3+4;
1058 relvars1
[17] = i
*3+5;
1059 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1060 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1079 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1080 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1081 trs_current
->varset
.varset
= relvarset1
;
1082 trs_current
->varset
.size
= 18;
1083 trs_current
->next_rel
= trs
;
1086 //(free targbox targagent -> box targagent target)
1087 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1088 relvars1
[0] = gammai
*3;
1089 relvars1
[1] = gammai
*3+1;
1090 relvars1
[2] = gammai
*3+2;
1091 relvars1
[3] = gammai
*3+3;
1092 relvars1
[4] = gammai
*3+4;
1093 relvars1
[5] = gammai
*3+5;
1094 relvars1
[6] = deltai
*3;
1095 relvars1
[7] = deltai
*3+1;
1096 relvars1
[8] = deltai
*3+2;
1097 relvars1
[9] = deltai
*3+3;
1098 relvars1
[10] = deltai
*3+4;
1099 relvars1
[11] = deltai
*3+5;
1101 relvars1
[13] = i
*3+1;
1102 relvars1
[14] = i
*3+2;
1103 relvars1
[15] = i
*3+3;
1104 relvars1
[16] = i
*3+4;
1105 relvars1
[17] = i
*3+5;
1106 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1107 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1126 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1127 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1128 trs_current
->varset
.varset
= relvarset1
;
1129 trs_current
->varset
.size
= 18;
1130 trs_current
->next_rel
= trs
;
1133 //(target box targagent -> targbox agent target)
1134 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1135 relvars1
[0] = gammai
*3;
1136 relvars1
[1] = gammai
*3+1;
1137 relvars1
[2] = gammai
*3+2;
1138 relvars1
[3] = gammai
*3+3;
1139 relvars1
[4] = gammai
*3+4;
1140 relvars1
[5] = gammai
*3+5;
1141 relvars1
[6] = deltai
*3;
1142 relvars1
[7] = deltai
*3+1;
1143 relvars1
[8] = deltai
*3+2;
1144 relvars1
[9] = deltai
*3+3;
1145 relvars1
[10] = deltai
*3+4;
1146 relvars1
[11] = deltai
*3+5;
1148 relvars1
[13] = i
*3+1;
1149 relvars1
[14] = i
*3+2;
1150 relvars1
[15] = i
*3+3;
1151 relvars1
[16] = i
*3+4;
1152 relvars1
[17] = i
*3+5;
1153 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1154 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1173 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1174 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1175 trs_current
->varset
.varset
= relvarset1
;
1176 trs_current
->varset
.size
= 18;
1177 trs_current
->next_rel
= trs
;
1180 //(target targbox targagent -> targbox targagent target)
1181 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1182 relvars1
[0] = gammai
*3;
1183 relvars1
[1] = gammai
*3+1;
1184 relvars1
[2] = gammai
*3+2;
1185 relvars1
[3] = gammai
*3+3;
1186 relvars1
[4] = gammai
*3+4;
1187 relvars1
[5] = gammai
*3+5;
1188 relvars1
[6] = deltai
*3;
1189 relvars1
[7] = deltai
*3+1;
1190 relvars1
[8] = deltai
*3+2;
1191 relvars1
[9] = deltai
*3+3;
1192 relvars1
[10] = deltai
*3+4;
1193 relvars1
[11] = deltai
*3+5;
1195 relvars1
[13] = i
*3+1;
1196 relvars1
[14] = i
*3+2;
1197 relvars1
[15] = i
*3+3;
1198 relvars1
[16] = i
*3+4;
1199 relvars1
[17] = i
*3+5;
1200 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1201 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1220 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1221 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1222 trs_current
->varset
.varset
= relvarset1
;
1223 trs_current
->varset
.size
= 18;
1224 trs_current
->next_rel
= trs
;
1232 rels
*encode_rel(sokoban_screen
*screen
)
1236 trans_t
*tl
= sylvan_false
;
1239 tl
= create_single_rel(screen
, LEFT
);
1242 trans_t
*tu
= create_single_rel(screen
, UP
);
1245 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1248 trans_t
*td
= create_single_rel(screen
, DOWN
);
1251 rls
= (rels
*)malloc(sizeof(rels
));
1265 BDDVAR vars
[] = {0,2,4};
1266 BDDVAR all_vars
[] = {0,1,2,3,4,5};
1267 BDDVAR all_vars2
[] = {0,1};
1268 //BDDVAR short_vars[] = {0,1};
1269 /*BDDVAR short_vars2[] = {2,3};
1270 BDDVAR short_vars3[] = {0,1,2,3};*/
1272 BDDSET vars_set
= sylvan_set_fromarray(vars
, 3);
1273 BDDSET all_vars_set
= sylvan_set_fromarray(all_vars
, 6);
1274 BDDSET all_vars_set2
= sylvan_set_fromarray(all_vars2
, 2);
1275 //BDDSET short_vars_set = sylvan_set_fromarray(short_vars, 2);
1276 /*BDDSET short_vars_set2 = sylvan_set_fromarray(short_vars2, 2);
1277 BDDSET short_vars_set3 = sylvan_set_fromarray(short_vars3, 4);*/
1279 BDD s
, t
, next
, prev
;
1282 // transition relation: 000 --> 111 and !000 --> 000
1284 t
= sylvan_union_cube(t
, all_vars_set2
, ((uint8_t[]){0,1}));
1285 //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0}));
1286 t
= sylvan_union_cube(t
, all_vars_set2
, ((uint8_t[]){1,0}));
1287 // t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1}));
1289 s
= sylvan_cube(vars_set
, (uint8_t[]){0,0,0});
1290 zeroes
= sylvan_cube(vars_set
, (uint8_t[]){1,0,0});
1291 ones
= sylvan_cube(vars_set
, (uint8_t[]){0,0,0});
1293 next
= sylvan_relnext(s
, t
, all_vars_set
);
1294 prev
= sylvan_relprev(t
, next
, all_vars_set
);
1295 if (next
== zeroes
) printf("Pass 1\n");
1296 if (prev
== ones
) printf("Pass 2\n");