38 xy_bddvar_map
*getxy(int x
, int y
, xy_bddvar_map
*map
)
40 xy_bddvar_map k
, *r
= NULL
;
41 memset(&k
, 0, sizeof(xy_bddvar_map
));
44 HASH_FIND(hh
, map
, &k
.key
, sizeof(xy
), r
);
48 bddvar_xy_map
*getbdd(int key
, bddvar_xy_map
*map
)
50 bddvar_xy_map k
, *r
= NULL
;
51 memset(&k
, 0, sizeof(bddvar_xy_map
));
53 HASH_FIND(hh
, map
, &k
.key
, sizeof(int), r
);
58 bimap
*create_bimap_helper(sokoban_screen
*screen
)
62 xy_bddvar_map
*xybdd
= NULL
;
63 bddvar_xy_map
*bddxy
= NULL
;
64 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
65 xy_bddvar_map
*f
= NULL
;
66 f
= (xy_bddvar_map
*)malloc(sizeof(xy_bddvar_map
));
67 memset(f
, 0, sizeof(xy_bddvar_map
));
68 f
->key
.x
= r
->coord
.x
;
69 f
->key
.y
= r
->coord
.y
;
70 f
->value
.var
[0] = varcount
* 2;
71 f
->value
.var
[1] = (varcount
+ 1) * 2;
72 f
->value
.var
[2] = (varcount
+ 2) * 2;
73 HASH_ADD(hh
, xybdd
, key
, sizeof(xy
), f
);
75 for (int i
= 0; i
<3; i
++){
76 bddvar_xy_map
*t
= NULL
;
77 t
= (bddvar_xy_map
*)malloc(sizeof(bddvar_xy_map
));
78 memset(t
, 0, sizeof(bddvar_xy_map
));
79 t
->key
= (varcount
+ i
) * 2;
80 t
->value
.x
= r
->coord
.x
;
81 t
->value
.y
= r
->coord
.y
;
82 HASH_ADD(hh
, bddxy
, key
, sizeof(int), t
);
84 varcount
= varcount
+ 3;
87 bm
= (bimap
*)malloc(sizeof(bimap
));
93 int check_xy_exists(int x
, int y
, bimap
*bm
)
96 if (getxy(x
, y
, bm
->f
) != NULL
) res
= 1;
100 int check_space(int x
, int y
, direction d
, int delta
, bimap
*bm
)
103 case LEFT
: x
= x
- delta
; break;
104 case UP
: y
= y
- delta
; break;
105 case RIGHT
: x
= x
+ delta
; break;
106 case DOWN
: y
= y
+ delta
; break;
108 return check_xy_exists(x
, y
, bm
);
112 * Each coordinate has three related boolean variables. The combination of those boolean variables
120 * 110: Agent on target
121 * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
122 * tiles in the shrinked screen.
123 * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
124 * directly in transition relations.
127 state
*encode_screen(sokoban_screen
*screen
)
131 BDDVAR vars
[HASH_COUNT(screen
) * 3];
132 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
136 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
138 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
140 state
*fullState
= NULL
;
141 fullState
= (state
*)malloc(sizeof(state
));
142 fullState
->vars
.varset
= varset
;
143 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
146 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
149 st_enc
[tile_index
] = 0;
151 st_enc
[tile_index
] = 0;
153 st_enc
[tile_index
] = 1;
157 st_enc
[tile_index
] = 0;
159 st_enc
[tile_index
] = 0;
161 st_enc
[tile_index
] = 0;
165 st_enc
[tile_index
] = 0;
167 st_enc
[tile_index
] = 1;
169 st_enc
[tile_index
] = 0;
173 st_enc
[tile_index
] = 0;
175 st_enc
[tile_index
] = 1;
177 st_enc
[tile_index
] = 1;
181 st_enc
[tile_index
] = 1;
183 st_enc
[tile_index
] = 0;
186 st_enc
[tile_index
] = 1;
189 case TARGAGENT
: //110
190 st_enc
[tile_index
] = 1;
192 st_enc
[tile_index
] = 1;
194 st_enc
[tile_index
] = 0;
198 st_enc
[tile_index
] = 1;
200 st_enc
[tile_index
] = 0;
202 st_enc
[tile_index
] = 0;
207 s
= sylvan_cube(varset
, st_enc
);
209 printf("Initial state encoded\n");
213 lurd_t
*lappend(lurd_t
*l
, char c
){
214 lurd_t
*temp_lrd
= NULL
;
216 temp_lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
218 temp_lrd
->next
= NULL
;
223 while (temp_lrd
->next
!= NULL
){
224 temp_lrd
= temp_lrd
->next
;
226 temp_lrd
->next
= (lurd_t
*)malloc(sizeof(lurd_t
));
227 temp_lrd
->next
->c
= c
;
228 temp_lrd
->next
->next
= NULL
;
233 int check_goal(BDD s
, BDD g
, BDDSET vars
){
235 if(sylvan_satcount(sylvan_and(s
, g
), vars
) > 0) return 1;
239 int check_visited(BDD s
, BDD v
, BDDSET vars
){
241 if(sylvan_satcount(sylvan_and(s
, v
), vars
) > 0) return 1;
245 state_t
*explstate(state
*init
, rels
*rls
, state
*g
){
247 deque
*state_queue
= create();
249 state_t
*tmp_state
= (state_t
*)malloc(sizeof(state_t
));
250 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
251 //state_t *new_state = (state_t *)malloc(sizeof(state_t));
252 BDD visited
= init
->bdd
;
254 tmp_state
->bdd
= init
->bdd
;
255 tmp_state
->vars
= init
->vars
;
256 tmp_state
->lrd
= lrd
;
257 state_queue
= enq(tmp_state
, state_queue
);
259 while (isEmpty(state_queue
) == 0){
260 tmp_state
= get_front(state_queue
);
261 state_queue
= deq(state_queue
);
262 new = tmp_state
->bdd
;
265 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
266 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
269 if (new != sylvan_false
&& new != tmp_state
->bdd
){
270 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
271 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
272 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
273 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
275 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
277 new_state
->bdd
= new;
278 new_state
->vars
= init
->vars
;
279 lrd
= lappend(lrd
, 'l');
280 new_state
->lrd
= lrd
;
281 state_queue
= enq(new_state
, state_queue
);
282 visited
= sylvan_or(new, visited
);
286 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
287 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
288 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
289 new_state
->bdd
= new;
290 new_state
->vars
= init
->vars
;
291 lrd
= lappend(lrd
, 'l');
292 new_state
->lrd
= lrd
;
300 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
301 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
304 if (new != sylvan_false
&& new != tmp_state
->bdd
){
305 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
306 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
307 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
308 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
309 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
310 new_state
->bdd
= new;
311 new_state
->vars
= init
->vars
;
312 lrd
= lappend(lrd
, 'u');
313 new_state
->lrd
= lrd
;
314 state_queue
= enq(new_state
, state_queue
);
315 visited
= sylvan_or(new, visited
);
319 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
320 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
321 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
322 new_state
->bdd
= new;
323 new_state
->vars
= init
->vars
;
324 lrd
= lappend(lrd
, 'u');
325 new_state
->lrd
= lrd
;
333 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
334 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
337 if (new != sylvan_false
&& new != tmp_state
->bdd
){
338 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
339 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
341 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
342 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
343 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
346 new_state
->bdd
= new;
347 new_state
->vars
= init
->vars
;
348 lrd
= lappend(lrd
, 'r');
349 new_state
->lrd
= lrd
;
350 state_queue
= enq(new_state
, state_queue
);
351 visited
= sylvan_or(new, visited
);
355 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
356 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
357 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
359 new_state
->bdd
= new;
360 new_state
->vars
= init
->vars
;
361 lrd
= lappend(lrd
, 'r');
362 new_state
->lrd
= lrd
;
371 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
372 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
375 if (new != sylvan_false
&& new != tmp_state
->bdd
){
376 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
377 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
379 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
380 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
381 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
383 new_state
->bdd
= new;
384 new_state
->vars
= init
->vars
;
385 lrd
= lappend(lrd
, 'd');
386 new_state
->lrd
= lrd
;
387 state_queue
= enq(new_state
, state_queue
);
388 visited
= sylvan_or(new, visited
);
392 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
393 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
394 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
396 new_state
->bdd
= new;
397 new_state
->vars
= init
->vars
;
398 lrd
= lappend(lrd
, 'd');
399 new_state
->lrd
= lrd
;
411 state
*encode_goal(sokoban_screen
*screen
){
417 BDDVAR vars
[HASH_COUNT(screen
) * 3];
418 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
422 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
424 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
426 state
*fullState
= NULL
;
427 fullState
= (state
*)malloc(sizeof(state
));
428 fullState
->vars
.varset
= varset
;
429 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
432 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
434 case FREE
: //001 -> any
435 st_enc
[tile_index
] = 2;
437 st_enc
[tile_index
] = 2;
439 st_enc
[tile_index
] = 2;
442 case WALL
: //000 -> stays the same
443 st_enc
[tile_index
] = 0;
445 st_enc
[tile_index
] = 0;
447 st_enc
[tile_index
] = 0;
450 case BOX
: //010 -> any
452 st_enc
[tile_index
] = 2;
454 st_enc
[tile_index
] = 2;
456 st_enc
[tile_index
] = 2;
459 case TARGET
: //011 -> targbox
461 st_enc
[tile_index
] = 1;
463 st_enc
[tile_index
] = 0;
465 st_enc
[tile_index
] = 0;
468 case AGENT
: //101 -> any
469 st_enc
[tile_index
] = 2;
471 st_enc
[tile_index
] = 2;
473 st_enc
[tile_index
] = 2;
476 case TARGAGENT
: //110 -> targbox
478 st_enc
[tile_index
] = 1;
480 st_enc
[tile_index
] = 0;
482 st_enc
[tile_index
] = 0;
485 case TARGBOX
: //100 -> stays the same
488 st_enc
[tile_index
] = 1;
490 st_enc
[tile_index
] = 0;
492 st_enc
[tile_index
] = 0;
497 s
= sylvan_cube(varset
, st_enc
);
499 printf("Goal state encoded\n");
500 if (targets
== 0 || (boxes
!= targets
)) return NULL
;
501 else return fullState
;
506 //int countTrans(trans_t *trs);
508 trans_t
*create_single_rel(sokoban_screen
*screen
, direction dir
)
511 trans_t
*trs
, *trs_current
;
512 bimap
*bm
= create_bimap_helper(screen
);
515 bddvar_xy_map
*bddxy
= NULL
;
548 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
549 bddxy
= getbdd(i
*6, bm
->t
);
552 if (check_space(x
, y
, dir
, 1, bm
) == 0){
554 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
555 BDDVAR relvars
[6] = {i
* 6, i
* 6 + 1, i
* 6 + 2, i
* 6 + 3, i
* 6 + 4, i
* 6 + 5};
556 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
557 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
558 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
559 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
560 trs_current
->varset
.varset
= relvarset
;
561 trs_current
->varset
.size
= 6;
562 trs_current
->next_rel
= trs
;
565 //Targagent -> Targagent
566 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
567 relvarset
= sylvan_set_fromarray(relvars
, 6);
568 uint8_t rel_enc1
[6] = {1, 1, 1, 1, 0, 0};
569 memcpy(rel_enc
, rel_enc1
, 6*sizeof(uint8_t));
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
= 6;
575 trs_current
->next_rel
= trs
;
580 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
581 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
582 unsigned int deltai
= bddvar
->value
.var
[0];
583 //Agent Free -> Free Agent
584 //(1 0 0 0 1 1 0 1 0 0 1 1)
586 //(0 1 0 0 1 1 1 0 0 0 1 1)
587 BDDVAR relvars
[12] = {i
*6, i
*6+1, i
*6+2, i
*6+3, i
*6+4, i
*6+5, deltai
, deltai
+1, deltai
+2, deltai
+3, deltai
+4, deltai
+5};
588 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
591 uint8_t rel_enc0
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
592 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
595 uint8_t rel_enc0
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
596 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
598 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
599 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
600 trs_current
->varset
.varset
= relvarset
;
601 trs_current
->varset
.size
= 12;
602 trs_current
->next_rel
= trs
;
605 //Agent Target -> Free Targagent
606 //(1 0 0 0 1 1 0 1 1 1 1 0)
608 //(0 1 1 1 1 0 1 0 0 0 1 1)
609 relvarset
= sylvan_set_fromarray(relvars
, 12);
611 uint8_t rel_enc2
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
612 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
615 uint8_t rel_enc2
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
616 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
618 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
619 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
620 trs_current
->varset
.varset
= relvarset
;
621 trs_current
->varset
.size
= 12;
622 trs_current
->next_rel
= trs
;
625 //Targagent Free -> Target Agent
626 //(1 0 1 1 0 1 0 1 0 0 1 1)
628 //(0 1 0 0 1 1 1 0 1 1 0 1)
629 relvarset
= sylvan_set_fromarray(relvars
, 12);
631 uint8_t rel_enc3
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
632 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
635 uint8_t rel_enc3
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
636 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
638 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
639 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
640 trs_current
->varset
.varset
= relvarset
;
641 trs_current
->varset
.size
= 12;
642 trs_current
->next_rel
= trs
;
645 //Targagent Target -> Target Targagent
646 //(1 0 1 1 0 1 0 1 1 1 1 0)
648 //(0 1 1 1 1 0 1 0 1 1 0 1)
649 relvarset
= sylvan_set_fromarray(relvars
, 12);
651 uint8_t rel_enc4
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
652 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
655 uint8_t rel_enc4
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
656 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
658 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
659 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
660 trs_current
->varset
.varset
= relvarset
;
661 trs_current
->varset
.size
= 12;
662 trs_current
->next_rel
= trs
;
665 //Agent Box -> Agent Box
666 //(1 1 0 0 1 1 0 0 1 1 0 0)
668 //(0 0 1 1 0 0 1 1 0 0 1 1)
669 relvarset
= sylvan_set_fromarray(relvars
, 12);
671 uint8_t rel_enc5
[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
672 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
675 uint8_t rel_enc5
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
676 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
678 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
679 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
680 trs_current
->varset
.varset
= relvarset
;
681 trs_current
->varset
.size
= 12;
682 trs_current
->next_rel
= trs
;
685 //Agent Targbox -> Agent Targbox
686 //(1 1 0 0 1 1 1 1 0 0 0 0)
688 //(1 1 0 0 0 0 1 1 0 0 1 1)
689 relvarset
= sylvan_set_fromarray(relvars
, 12);
691 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
692 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
695 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
696 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
698 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
699 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
700 trs_current
->varset
.varset
= relvarset
;
701 trs_current
->varset
.size
= 12;
702 trs_current
->next_rel
= trs
;
705 //Targagent Box -> Targagent Box
706 //(1 1 1 1 0 0 0 0 1 1 0 0)
708 //(0 0 1 1 0 0 1 1 1 1 0 0)
709 relvarset
= sylvan_set_fromarray(relvars
, 12);
711 uint8_t rel_enc7
[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
712 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
715 uint8_t rel_enc7
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
716 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
718 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
719 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
720 trs_current
->varset
.varset
= relvarset
;
721 trs_current
->varset
.size
= 12;
722 trs_current
->next_rel
= trs
;
725 //Targagent Targbox -> Targagent Targbox
726 //(1 1 1 1 0 0 1 1 0 0 0 0)
728 //(1 1 0 0 0 0 1 1 1 1 0 0)
729 relvarset
= sylvan_set_fromarray(relvars
, 12);
731 uint8_t rel_enc8
[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
732 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
735 uint8_t rel_enc8
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
736 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
738 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
739 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
740 trs_current
->varset
.varset
= relvarset
;
741 trs_current
->varset
.size
= 12;
742 trs_current
->next_rel
= trs
;
748 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
749 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
750 unsigned int deltai
= bddvar
->value
.var
[0];
751 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
752 unsigned int gammai
= bddvar
->value
.var
[0];
753 //Agent Free -> Free Agent
754 //(1 0 0 0 1 1 0 1 0 0 1 1)
756 //(0 1 0 0 1 1 1 0 0 0 1 1)
757 BDDVAR relvars
[12] = {i
*6, i
*6+1, i
*6+2, i
*6+3, i
*6+4, i
*6+5, deltai
, deltai
+1, deltai
+2, deltai
+3, deltai
+4, deltai
+5};
758 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
761 uint8_t rel_enc_
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
762 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
765 uint8_t rel_enc_
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
766 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
768 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
769 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
770 trs_current
->varset
.varset
= relvarset
;
771 trs_current
->varset
.size
= 12;
772 trs_current
->next_rel
= trs
;
775 //Agent Target -> Free Targagent
776 //(1 0 0 0 1 1 0 1 1 1 1 0)
778 //(0 1 1 1 1 0 1 0 0 0 1 1)
779 relvarset
= sylvan_set_fromarray(relvars
, 12);
781 uint8_t rel_enc9
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
782 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
785 uint8_t rel_enc9
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
786 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
788 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
789 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
790 trs_current
->varset
.varset
= relvarset
;
791 trs_current
->varset
.size
= 12;
792 trs_current
->next_rel
= trs
;
795 //Targagent Free -> Target Agent (LEFT || UP)
796 //(1 0 1 1 0 1 0 1 0 0 1 1)
798 //(0 1 0 0 1 1 1 0 1 1 0 1)
799 relvarset
= sylvan_set_fromarray(relvars
, 12);
801 uint8_t rel_enc10
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
802 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
805 uint8_t rel_enc10
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
806 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
808 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
809 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
810 trs_current
->varset
.varset
= relvarset
;
811 trs_current
->varset
.size
= 12;
812 trs_current
->next_rel
= trs
;
815 //Targagent Target -> Target Targagent (LEFT || UP)
816 //(1 0 1 1 0 1 0 1 1 1 1 0)
818 //(0 1 1 1 1 0 1 0 1 1 0 1)
819 relvarset
= sylvan_set_fromarray(relvars
, 12);
821 uint8_t rel_enc11
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
822 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
825 uint8_t rel_enc11
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
826 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
828 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
829 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
830 trs_current
->varset
.varset
= relvarset
;
831 trs_current
->varset
.size
= 12;
832 trs_current
->next_rel
= trs
;
835 //Agent Box Box -> Agent Box Box
836 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
838 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
840 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
842 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
844 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
846 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
847 BDDVAR relvars1
[18] = {i
*6, i
*6+1, i
*6+2, i
*6+3, i
*6+4, i
*6+5, deltai
, deltai
+1, deltai
+2, deltai
+3, deltai
+4, deltai
+5, gammai
, gammai
+1, gammai
+2, gammai
+3, gammai
+4, gammai
+5};
848 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
849 uint8_t rel_enc1
[18];
850 if (i
*6 < deltai
&& deltai
< gammai
){
851 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
852 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
854 else if (deltai
< gammai
&& gammai
< i
*6){
855 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
856 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
858 else if (gammai
< i
*6 && i
*6 < deltai
){
859 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
860 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
862 else if (i
*6 < gammai
&& gammai
< deltai
){
863 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
864 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
866 else if (deltai
< i
*6 && i
*6 < gammai
){
867 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
868 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
871 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
872 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
875 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
876 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
877 trs_current
->varset
.varset
= relvarset1
;
878 trs_current
->varset
.size
= 18;
879 trs_current
->next_rel
= trs
;
882 //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
883 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
885 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
887 //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
889 //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
891 //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
893 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
894 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
895 if (i
*6 < deltai
&& deltai
< gammai
){
896 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
897 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
899 else if (deltai
< gammai
&& gammai
< i
*6){
900 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
901 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
903 else if (gammai
< i
*6 && i
*6 < deltai
){
904 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
905 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
907 else if (i
*6 < gammai
&& gammai
< deltai
){
908 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
909 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
911 else if (deltai
< i
*6 && i
*6 < gammai
){
912 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
913 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
916 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
917 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
919 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
920 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
921 trs_current
->varset
.varset
= relvarset1
;
922 trs_current
->varset
.size
= 18;
923 trs_current
->next_rel
= trs
;
926 //Targagent Box Box -> Targagent Box Box
927 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
929 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
931 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
933 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
935 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
937 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
938 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
939 if (i
*6 < deltai
&& deltai
< gammai
){
940 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
941 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
943 else if (deltai
< gammai
&& gammai
< i
*6){
944 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
945 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
947 else if (gammai
< i
*6 && i
*6 < deltai
){
948 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
949 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
951 else if (i
*6 < gammai
&& gammai
< deltai
){
952 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
953 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
955 else if (deltai
< i
*6 && i
*6 < gammai
){
956 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
957 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
960 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
961 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
963 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
964 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
965 trs_current
->varset
.varset
= relvarset1
;
966 trs_current
->varset
.size
= 18;
967 trs_current
->next_rel
= trs
;
970 //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
971 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
973 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
975 //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
977 //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
979 //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
981 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
982 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
983 if (i
*6 < deltai
&& deltai
< gammai
){
984 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
985 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
987 else if (deltai
< gammai
&& gammai
< i
*6){
988 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
989 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
991 else if (gammai
< i
*6 && i
*6 < deltai
){
992 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
993 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
995 else if (i
*6 < gammai
&& gammai
< deltai
){
996 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
997 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
999 else if (deltai
< i
*6 && i
*6 < gammai
){
1000 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
1001 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1004 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
1005 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1007 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1008 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1009 trs_current
->varset
.varset
= relvarset1
;
1010 trs_current
->varset
.size
= 18;
1011 trs_current
->next_rel
= trs
;
1014 //Agent Box Free -> Free Agent Box
1015 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
1017 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
1019 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
1021 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
1023 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
1025 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1026 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1027 if (i
*6 < deltai
&& deltai
< gammai
){
1028 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1029 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1032 else if (deltai
< gammai
&& gammai
< i
*6){
1033 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1034 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1037 else if (gammai
< i
*6 && i
*6 < deltai
){
1038 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1039 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1042 else if (i
*6 < gammai
&& gammai
< deltai
){
1043 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1044 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1046 else if (deltai
< i
*6 && i
*6 < gammai
){
1047 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1048 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1051 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1052 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1055 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1057 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1058 trs_current
->varset
.varset
= relvarset1
;
1059 trs_current
->varset
.size
= 18;
1060 trs_current
->next_rel
= trs
;
1063 //Agent Targbox Free -> Free Targagent Box
1064 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
1066 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
1068 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1070 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
1072 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
1074 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1075 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1076 if (i
*6 < deltai
&& deltai
< gammai
){
1077 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1078 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1080 else if (deltai
< gammai
&& gammai
< i
*6){
1081 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1082 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1084 else if (gammai
< i
*6 && i
*6 < deltai
){
1085 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1086 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1088 else if (i
*6 < gammai
&& gammai
< deltai
){
1089 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1090 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1092 else if (deltai
< i
*6 && i
*6 < gammai
){
1093 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1094 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1097 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1098 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1100 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1101 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1102 trs_current
->varset
.varset
= relvarset1
;
1103 trs_current
->varset
.size
= 18;
1104 trs_current
->next_rel
= trs
;
1107 //Agent Box Target -> Free Agent Targbox
1108 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
1110 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
1112 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
1114 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
1116 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
1118 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1119 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1120 if (i
*6 < deltai
&& deltai
< gammai
){
1121 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1122 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1124 else if (deltai
< gammai
&& gammai
< i
*6){
1125 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1126 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1128 else if (gammai
< i
*6 && i
*6 < deltai
){
1129 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1130 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1132 else if (i
*6 < gammai
&& gammai
< deltai
){
1133 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1134 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1136 else if (deltai
< i
*6 && i
*6 < gammai
){
1137 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1138 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1141 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1142 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1144 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1145 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1146 trs_current
->varset
.varset
= relvarset1
;
1147 trs_current
->varset
.size
= 18;
1148 trs_current
->next_rel
= trs
;
1151 //Agent Targbox Target -> Free Targagent Targbox
1152 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
1154 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
1156 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1158 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
1160 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
1162 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1163 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1164 if (i
*6 < deltai
&& deltai
< gammai
){
1165 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1166 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1168 else if (deltai
< gammai
&& gammai
< i
*6){
1169 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1170 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1172 else if (gammai
< i
*6 && i
*6 < deltai
){
1173 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1174 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1176 else if (i
*6 < gammai
&& gammai
< deltai
){
1177 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1178 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1180 else if (deltai
< i
*6 && i
*6 < gammai
){
1181 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1182 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1185 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1186 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1188 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1189 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1190 trs_current
->varset
.varset
= relvarset1
;
1191 trs_current
->varset
.size
= 18;
1192 trs_current
->next_rel
= trs
;
1195 //Targagent Box Free -> Target Agent Box
1196 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
1198 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
1200 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1202 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
1204 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
1206 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1207 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1208 if (i
*6 < deltai
&& deltai
< gammai
){
1209 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1210 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1212 else if (deltai
< gammai
&& gammai
< i
*6){
1213 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1214 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1216 else if (gammai
< i
*6 && i
*6 < deltai
){
1217 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1218 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1220 else if (i
*6 < gammai
&& gammai
< deltai
){
1221 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1222 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1224 else if (deltai
< i
*6 && i
*6 < gammai
){
1225 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
1226 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1229 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1230 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1232 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1233 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1234 trs_current
->varset
.varset
= relvarset1
;
1235 trs_current
->varset
.size
= 18;
1236 trs_current
->next_rel
= trs
;
1239 //Targagent Targbox Free -> Target Targagent Box
1240 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
1242 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
1244 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1246 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
1248 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
1250 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1251 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1252 if (i
*6 < deltai
&& deltai
< gammai
){
1253 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1254 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1256 else if (deltai
< gammai
&& gammai
< i
*6){
1257 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1258 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1260 else if (gammai
< i
*6 && i
*6 < deltai
){
1261 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1262 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1264 else if (i
*6 < gammai
&& gammai
< deltai
){
1265 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1266 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1268 else if (deltai
< i
*6 && i
*6 < gammai
){
1269 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0};
1270 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1273 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1274 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1276 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1277 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1278 trs_current
->varset
.varset
= relvarset1
;
1279 trs_current
->varset
.size
= 18;
1280 trs_current
->next_rel
= trs
;
1283 //Targagent Box Target -> Target Agent Targbox
1284 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1286 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1288 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1290 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1292 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1294 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1295 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1296 if (i
*6 < deltai
&& deltai
< gammai
){
1297 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1298 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1300 else if (deltai
< gammai
&& gammai
< i
*6){
1301 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1302 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1304 else if (gammai
< i
*6 && i
*6 < deltai
){
1305 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1306 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1308 else if (i
*6 < gammai
&& gammai
< deltai
){
1309 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1310 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1312 else if (deltai
< i
*6 && i
*6 < gammai
){
1313 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1314 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1317 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1318 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1320 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1321 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1322 trs_current
->varset
.varset
= relvarset1
;
1323 trs_current
->varset
.size
= 18;
1324 trs_current
->next_rel
= trs
;
1327 //Targagent Targbox Target -> Target Targagent Targbox
1328 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1330 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1332 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1334 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1336 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1338 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1339 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1340 if (i
*6 < deltai
&& deltai
< gammai
){
1341 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1342 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1344 else if (deltai
< gammai
&& gammai
< i
*6){
1345 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1346 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1348 else if (gammai
< i
*6 && i
*6 < deltai
){
1349 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1350 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1352 else if (i
*6 < gammai
&& gammai
< deltai
){
1353 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1354 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1356 else if (deltai
< i
*6 && i
*6 < gammai
){
1357 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1358 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1361 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1362 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1364 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1365 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1366 trs_current
->varset
.varset
= relvarset1
;
1367 trs_current
->varset
.size
= 18;
1368 trs_current
->next_rel
= trs
;
1379 if (trs_current != NULL) printf("LEFT ok!\n");
1380 else printf ("LEFT is empty\n");
1381 printf("Num of trans relations:%d\n", countTrans(trs));
1384 if (trs_current != NULL) printf("UP ok!\n");
1385 else printf ("UP is empty\n");
1386 printf("Num of trans relations:%d\n", countTrans(trs));
1389 if (trs_current != NULL) printf("RIGHT ok!\n");
1390 else printf ("RIGHT is empty\n");
1391 printf("Num of trans relations:%d\n", countTrans(trs));
1394 if (trs_current != NULL) printf("DOWN ok!\n");
1395 else printf ("DOWN is empty\n");
1396 printf("Num of trans relations:%d\n", countTrans(trs));
1405 int countTrans(trans_t *trs)
1408 while (trs != NULL){
1410 trs = trs->next_rel;
1415 rels
*encode_rel(sokoban_screen
*screen
)
1419 trans_t
*tl
= sylvan_false
;
1422 tl
= create_single_rel(screen
, LEFT
);
1425 trans_t
*tu
= create_single_rel(screen
, UP
);
1428 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1431 trans_t
*td
= create_single_rel(screen
, DOWN
);
1434 rls
= (rels
*)malloc(sizeof(rels
));
1443 int test_trans(state
*s
, trans_t
*t
)
1446 BDD next
= sylvan_false
;
1448 next
= sylvan_relnext(s
->bdd
, t
->bdd
, t
->varset
.varset
);
1449 if (next
== s
->bdd
) printf("Same\n");
1450 if (next
!= s
->bdd
&& next
!= sylvan_false
) printf("Different\n");
1451 if (next
== sylvan_false
) printf("False\n");