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
));
274 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
275 new_state
->bdd
= new;
276 new_state
->vars
= init
->vars
;
277 lrd
= lappend(lrd
, 'l');
278 new_state
->lrd
= lrd
;
279 state_queue
= enq(new_state
, state_queue
);
280 visited
= sylvan_or(new, visited
);
284 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
285 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
286 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
287 new_state
->bdd
= new;
288 new_state
->vars
= init
->vars
;
289 lrd
= lappend(lrd
, 'l');
290 new_state
->lrd
= lrd
;
298 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
299 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
302 if (new != sylvan_false
&& new != tmp_state
->bdd
){
303 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
304 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
305 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
306 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
307 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
308 new_state
->bdd
= new;
309 new_state
->vars
= init
->vars
;
310 lrd
= lappend(lrd
, 'u');
311 new_state
->lrd
= lrd
;
312 state_queue
= enq(new_state
, state_queue
);
313 visited
= sylvan_or(new, visited
);
317 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
318 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
319 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
320 new_state
->bdd
= new;
321 new_state
->vars
= init
->vars
;
322 lrd
= lappend(lrd
, 'u');
323 new_state
->lrd
= lrd
;
331 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
332 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
335 if (new != sylvan_false
&& new != tmp_state
->bdd
){
336 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
337 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
338 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
339 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
340 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
342 new_state
->bdd
= new;
343 new_state
->vars
= init
->vars
;
344 lrd
= lappend(lrd
, 'r');
345 new_state
->lrd
= lrd
;
346 state_queue
= enq(new_state
, state_queue
);
347 visited
= sylvan_or(new, visited
);
351 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
352 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
353 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
355 new_state
->bdd
= new;
356 new_state
->vars
= init
->vars
;
357 lrd
= lappend(lrd
, 'r');
358 new_state
->lrd
= lrd
;
367 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
368 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
371 if (new != sylvan_false
&& new != tmp_state
->bdd
){
372 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
373 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
375 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
376 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
377 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
379 new_state
->bdd
= new;
380 new_state
->vars
= init
->vars
;
381 lrd
= lappend(lrd
, 'd');
382 new_state
->lrd
= lrd
;
383 state_queue
= enq(new_state
, state_queue
);
384 visited
= sylvan_or(new, visited
);
388 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
389 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
390 memcpy(lrd
, tmp_state
->lrd
, sizeof(lurd_t
));
392 new_state
->bdd
= new;
393 new_state
->vars
= init
->vars
;
394 lrd
= lappend(lrd
, 'd');
395 new_state
->lrd
= lrd
;
407 state
*encode_goal(sokoban_screen
*screen
){
413 BDDVAR vars
[HASH_COUNT(screen
) * 3];
414 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
418 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
420 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
422 state
*fullState
= NULL
;
423 fullState
= (state
*)malloc(sizeof(state
));
424 fullState
->vars
.varset
= varset
;
425 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
428 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
430 case FREE
: //001 -> any
431 st_enc
[tile_index
] = 2;
433 st_enc
[tile_index
] = 2;
435 st_enc
[tile_index
] = 2;
438 case WALL
: //000 -> stays the same
439 st_enc
[tile_index
] = 0;
441 st_enc
[tile_index
] = 0;
443 st_enc
[tile_index
] = 0;
446 case BOX
: //010 -> any
448 st_enc
[tile_index
] = 2;
450 st_enc
[tile_index
] = 2;
452 st_enc
[tile_index
] = 2;
455 case TARGET
: //011 -> targbox
457 st_enc
[tile_index
] = 1;
459 st_enc
[tile_index
] = 0;
461 st_enc
[tile_index
] = 0;
464 case AGENT
: //101 -> any
465 st_enc
[tile_index
] = 2;
467 st_enc
[tile_index
] = 2;
469 st_enc
[tile_index
] = 2;
472 case TARGAGENT
: //110 -> targbox
474 st_enc
[tile_index
] = 1;
476 st_enc
[tile_index
] = 0;
478 st_enc
[tile_index
] = 0;
481 case TARGBOX
: //100 -> stays the same
484 st_enc
[tile_index
] = 1;
486 st_enc
[tile_index
] = 0;
488 st_enc
[tile_index
] = 0;
493 s
= sylvan_cube(varset
, st_enc
);
495 printf("Goal state encoded\n");
496 if (targets
== 0 || (boxes
!= targets
)) return NULL
;
497 else return fullState
;
502 //int countTrans(trans_t *trs);
504 trans_t
*create_single_rel(sokoban_screen
*screen
, direction dir
)
507 trans_t
*trs
, *trs_current
;
508 bimap
*bm
= create_bimap_helper(screen
);
511 bddvar_xy_map
*bddxy
= NULL
;
544 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
545 bddxy
= getbdd(i
*6, bm
->t
);
548 if (check_space(x
, y
, dir
, 1, bm
) == 0){
550 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
551 BDDVAR relvars
[6] = {i
* 6, i
* 6 + 1, i
* 6 + 2, i
* 6 + 3, i
* 6 + 4, i
* 6 + 5};
552 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
553 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
554 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
555 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
556 trs_current
->varset
.varset
= relvarset
;
557 trs_current
->varset
.size
= 6;
558 trs_current
->next_rel
= trs
;
561 //Targagent -> Targagent
562 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
563 relvarset
= sylvan_set_fromarray(relvars
, 6);
564 uint8_t rel_enc1
[6] = {1, 1, 1, 1, 0, 0};
565 memcpy(rel_enc
, rel_enc1
, 6*sizeof(uint8_t));
567 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
568 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
569 trs_current
->varset
.varset
= relvarset
;
570 trs_current
->varset
.size
= 6;
571 trs_current
->next_rel
= trs
;
576 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
577 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
578 unsigned int deltai
= bddvar
->value
.var
[0];
579 //Agent Free -> Free Agent
580 //(1 0 0 0 1 1 0 1 0 0 1 1)
582 //(0 1 0 0 1 1 1 0 0 0 1 1)
583 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};
584 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
587 uint8_t rel_enc0
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
588 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
591 uint8_t rel_enc0
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
592 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
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 //Agent Target -> Free Targagent
602 //(1 0 0 0 1 1 0 1 1 1 1 0)
604 //(0 1 1 1 1 0 1 0 0 0 1 1)
605 relvarset
= sylvan_set_fromarray(relvars
, 12);
607 uint8_t rel_enc2
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
608 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
611 uint8_t rel_enc2
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
612 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
614 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
615 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
616 trs_current
->varset
.varset
= relvarset
;
617 trs_current
->varset
.size
= 12;
618 trs_current
->next_rel
= trs
;
621 //Targagent Free -> Target Agent
622 //(1 0 1 1 0 1 0 1 0 0 1 1)
624 //(0 1 0 0 1 1 1 0 1 1 0 1)
625 relvarset
= sylvan_set_fromarray(relvars
, 12);
627 uint8_t rel_enc3
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
628 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
631 uint8_t rel_enc3
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
632 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
634 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
635 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
636 trs_current
->varset
.varset
= relvarset
;
637 trs_current
->varset
.size
= 12;
638 trs_current
->next_rel
= trs
;
641 //Targagent Target -> Target Targagent
642 //(1 0 1 1 0 1 0 1 1 1 1 0)
644 //(0 1 1 1 1 0 1 0 1 1 0 1)
645 relvarset
= sylvan_set_fromarray(relvars
, 12);
647 uint8_t rel_enc4
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
648 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
651 uint8_t rel_enc4
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
652 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
654 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
655 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
656 trs_current
->varset
.varset
= relvarset
;
657 trs_current
->varset
.size
= 12;
658 trs_current
->next_rel
= trs
;
661 //Agent Box -> Agent Box
662 //(1 1 0 0 1 1 0 0 1 1 0 0)
664 //(0 0 1 1 0 0 1 1 0 0 1 1)
665 relvarset
= sylvan_set_fromarray(relvars
, 12);
667 uint8_t rel_enc5
[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
668 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
671 uint8_t rel_enc5
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
672 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
674 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
675 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
676 trs_current
->varset
.varset
= relvarset
;
677 trs_current
->varset
.size
= 12;
678 trs_current
->next_rel
= trs
;
681 //Agent Targbox -> Agent Targbox
682 //(1 1 0 0 1 1 1 1 0 0 0 0)
684 //(1 1 0 0 0 0 1 1 0 0 1 1)
685 relvarset
= sylvan_set_fromarray(relvars
, 12);
687 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
688 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
691 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
692 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
694 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
695 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
696 trs_current
->varset
.varset
= relvarset
;
697 trs_current
->varset
.size
= 12;
698 trs_current
->next_rel
= trs
;
701 //Targagent Box -> Targagent Box
702 //(1 1 1 1 0 0 0 0 1 1 0 0)
704 //(0 0 1 1 0 0 1 1 1 1 0 0)
705 relvarset
= sylvan_set_fromarray(relvars
, 12);
707 uint8_t rel_enc7
[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
708 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
711 uint8_t rel_enc7
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
712 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
714 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
715 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
716 trs_current
->varset
.varset
= relvarset
;
717 trs_current
->varset
.size
= 12;
718 trs_current
->next_rel
= trs
;
721 //Targagent Targbox -> Targagent Targbox
722 //(1 1 1 1 0 0 1 1 0 0 0 0)
724 //(1 1 0 0 0 0 1 1 1 1 0 0)
725 relvarset
= sylvan_set_fromarray(relvars
, 12);
727 uint8_t rel_enc8
[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
728 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
731 uint8_t rel_enc8
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
732 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
734 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
735 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
736 trs_current
->varset
.varset
= relvarset
;
737 trs_current
->varset
.size
= 12;
738 trs_current
->next_rel
= trs
;
744 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
745 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
746 unsigned int deltai
= bddvar
->value
.var
[0];
747 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
748 unsigned int gammai
= bddvar
->value
.var
[0];
749 //Agent Free -> Free Agent
750 //(1 0 0 0 1 1 0 1 0 0 1 1)
752 //(0 1 0 0 1 1 1 0 0 0 1 1)
753 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};
754 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
757 uint8_t rel_enc_
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
758 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
761 uint8_t rel_enc_
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
762 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
764 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
765 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
766 trs_current
->varset
.varset
= relvarset
;
767 trs_current
->varset
.size
= 12;
768 trs_current
->next_rel
= trs
;
771 //Agent Target -> Free Targagent
772 //(1 0 0 0 1 1 0 1 1 1 1 0)
774 //(0 1 1 1 1 0 1 0 0 0 1 1)
775 relvarset
= sylvan_set_fromarray(relvars
, 12);
777 uint8_t rel_enc9
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
778 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
781 uint8_t rel_enc9
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
782 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
784 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
785 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
786 trs_current
->varset
.varset
= relvarset
;
787 trs_current
->varset
.size
= 12;
788 trs_current
->next_rel
= trs
;
791 //Targagent Free -> Target Agent (LEFT || UP)
792 //(1 0 1 1 0 1 0 1 0 0 1 1)
794 //(0 1 0 0 1 1 1 0 1 1 0 1)
795 relvarset
= sylvan_set_fromarray(relvars
, 12);
797 uint8_t rel_enc10
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
798 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
801 uint8_t rel_enc10
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
802 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
804 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
805 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
806 trs_current
->varset
.varset
= relvarset
;
807 trs_current
->varset
.size
= 12;
808 trs_current
->next_rel
= trs
;
811 //Targagent Target -> Target Targagent (LEFT || UP)
812 //(1 0 1 1 0 1 0 1 1 1 1 0)
814 //(0 1 1 1 1 0 1 0 1 1 0 1)
815 relvarset
= sylvan_set_fromarray(relvars
, 12);
817 uint8_t rel_enc11
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
818 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
821 uint8_t rel_enc11
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
822 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
824 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
825 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
826 trs_current
->varset
.varset
= relvarset
;
827 trs_current
->varset
.size
= 12;
828 trs_current
->next_rel
= trs
;
831 //Agent Box Box -> Agent Box Box
832 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
834 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
836 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
838 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
840 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
842 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
843 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};
844 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
845 uint8_t rel_enc1
[18];
846 if (i
*6 < deltai
&& deltai
< gammai
){
847 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
848 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
850 else if (deltai
< gammai
&& gammai
< i
*6){
851 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
852 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
854 else if (gammai
< i
*6 && i
*6 < deltai
){
855 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
856 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
858 else if (i
*6 < gammai
&& gammai
< deltai
){
859 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
860 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
862 else if (deltai
< i
*6 && i
*6 < gammai
){
863 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
864 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
867 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
868 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
871 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
872 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
873 trs_current
->varset
.varset
= relvarset1
;
874 trs_current
->varset
.size
= 18;
875 trs_current
->next_rel
= trs
;
878 //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
879 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
881 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
883 //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
885 //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
887 //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
889 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
890 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
891 if (i
*6 < deltai
&& deltai
< gammai
){
892 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
893 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
895 else if (deltai
< gammai
&& gammai
< i
*6){
896 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
897 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
899 else if (gammai
< i
*6 && i
*6 < deltai
){
900 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
901 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
903 else if (i
*6 < gammai
&& gammai
< deltai
){
904 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
905 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
907 else if (deltai
< i
*6 && i
*6 < gammai
){
908 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
909 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
912 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
913 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
915 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
916 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
917 trs_current
->varset
.varset
= relvarset1
;
918 trs_current
->varset
.size
= 18;
919 trs_current
->next_rel
= trs
;
922 //Targagent Box Box -> Targagent Box Box
923 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
925 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
927 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
929 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
931 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
933 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
934 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
935 if (i
*6 < deltai
&& deltai
< gammai
){
936 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
937 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
939 else if (deltai
< gammai
&& gammai
< i
*6){
940 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
941 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
943 else if (gammai
< i
*6 && i
*6 < deltai
){
944 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
945 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
947 else if (i
*6 < gammai
&& gammai
< deltai
){
948 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
949 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
951 else if (deltai
< i
*6 && i
*6 < gammai
){
952 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
953 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
956 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
957 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
959 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
960 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
961 trs_current
->varset
.varset
= relvarset1
;
962 trs_current
->varset
.size
= 18;
963 trs_current
->next_rel
= trs
;
966 //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
967 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
969 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
971 //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
973 //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
975 //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
977 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
978 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
979 if (i
*6 < deltai
&& deltai
< gammai
){
980 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
981 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
983 else if (deltai
< gammai
&& gammai
< i
*6){
984 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
985 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
987 else if (gammai
< i
*6 && i
*6 < deltai
){
988 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
989 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
991 else if (i
*6 < gammai
&& gammai
< deltai
){
992 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
993 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
995 else if (deltai
< i
*6 && i
*6 < gammai
){
996 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
997 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1000 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
1001 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1003 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1004 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1005 trs_current
->varset
.varset
= relvarset1
;
1006 trs_current
->varset
.size
= 18;
1007 trs_current
->next_rel
= trs
;
1010 //Agent Box Free -> Free Agent Box
1011 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
1013 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
1015 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
1017 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
1019 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
1021 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1022 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1023 if (i
*6 < deltai
&& deltai
< gammai
){
1024 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1025 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1028 else if (deltai
< gammai
&& gammai
< i
*6){
1029 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1030 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1033 else if (gammai
< i
*6 && i
*6 < deltai
){
1034 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1035 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1038 else if (i
*6 < gammai
&& gammai
< deltai
){
1039 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1040 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1042 else if (deltai
< i
*6 && i
*6 < gammai
){
1043 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1044 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1047 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1048 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1051 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1053 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1054 trs_current
->varset
.varset
= relvarset1
;
1055 trs_current
->varset
.size
= 18;
1056 trs_current
->next_rel
= trs
;
1059 //Agent Targbox Free -> Free Targagent Box
1060 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
1062 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
1064 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1066 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
1068 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
1070 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1071 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1072 if (i
*6 < deltai
&& deltai
< gammai
){
1073 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1074 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1076 else if (deltai
< gammai
&& gammai
< i
*6){
1077 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1078 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1080 else if (gammai
< i
*6 && i
*6 < deltai
){
1081 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1082 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1084 else if (i
*6 < gammai
&& gammai
< deltai
){
1085 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1086 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1088 else if (deltai
< i
*6 && i
*6 < gammai
){
1089 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1090 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1093 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1094 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1096 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1097 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1098 trs_current
->varset
.varset
= relvarset1
;
1099 trs_current
->varset
.size
= 18;
1100 trs_current
->next_rel
= trs
;
1103 //Agent Box Target -> Free Agent Targbox
1104 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
1106 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
1108 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
1110 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
1112 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
1114 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1115 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1116 if (i
*6 < deltai
&& deltai
< gammai
){
1117 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1118 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1120 else if (deltai
< gammai
&& gammai
< i
*6){
1121 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1122 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1124 else if (gammai
< i
*6 && i
*6 < deltai
){
1125 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1126 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1128 else if (i
*6 < gammai
&& gammai
< deltai
){
1129 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1130 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1132 else if (deltai
< i
*6 && i
*6 < gammai
){
1133 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1134 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1137 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1138 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1140 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1141 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1142 trs_current
->varset
.varset
= relvarset1
;
1143 trs_current
->varset
.size
= 18;
1144 trs_current
->next_rel
= trs
;
1147 //Agent Targbox Target -> Free Targagent Targbox
1148 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
1150 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
1152 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1154 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
1156 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
1158 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1159 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1160 if (i
*6 < deltai
&& deltai
< gammai
){
1161 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1162 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1164 else if (deltai
< gammai
&& gammai
< i
*6){
1165 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1166 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1168 else if (gammai
< i
*6 && i
*6 < deltai
){
1169 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1170 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1172 else if (i
*6 < gammai
&& gammai
< deltai
){
1173 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1174 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1176 else if (deltai
< i
*6 && i
*6 < gammai
){
1177 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1178 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1181 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1182 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1184 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1185 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1186 trs_current
->varset
.varset
= relvarset1
;
1187 trs_current
->varset
.size
= 18;
1188 trs_current
->next_rel
= trs
;
1191 //Targagent Box Free -> Target Agent Box
1192 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
1194 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
1196 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1198 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
1200 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
1202 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1203 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1204 if (i
*6 < deltai
&& deltai
< gammai
){
1205 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1206 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1208 else if (deltai
< gammai
&& gammai
< i
*6){
1209 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1210 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1212 else if (gammai
< i
*6 && i
*6 < deltai
){
1213 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1214 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1216 else if (i
*6 < gammai
&& gammai
< deltai
){
1217 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1218 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1220 else if (deltai
< i
*6 && i
*6 < gammai
){
1221 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
1222 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1225 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1226 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1228 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1229 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1230 trs_current
->varset
.varset
= relvarset1
;
1231 trs_current
->varset
.size
= 18;
1232 trs_current
->next_rel
= trs
;
1235 //Targagent Targbox Free -> Target Targagent Box
1236 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
1238 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
1240 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1242 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
1244 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
1246 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1247 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1248 if (i
*6 < deltai
&& deltai
< gammai
){
1249 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1250 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1252 else if (deltai
< gammai
&& gammai
< i
*6){
1253 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1254 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1256 else if (gammai
< i
*6 && i
*6 < deltai
){
1257 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1258 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1260 else if (i
*6 < gammai
&& gammai
< deltai
){
1261 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1262 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1264 else if (deltai
< i
*6 && i
*6 < gammai
){
1265 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0};
1266 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1269 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1270 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1272 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1273 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1274 trs_current
->varset
.varset
= relvarset1
;
1275 trs_current
->varset
.size
= 18;
1276 trs_current
->next_rel
= trs
;
1279 //Targagent Box Target -> Target Agent Targbox
1280 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1282 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1284 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1286 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1288 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1290 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1291 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1292 if (i
*6 < deltai
&& deltai
< gammai
){
1293 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1294 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1296 else if (deltai
< gammai
&& gammai
< i
*6){
1297 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1298 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1300 else if (gammai
< i
*6 && i
*6 < deltai
){
1301 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1302 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1304 else if (i
*6 < gammai
&& gammai
< deltai
){
1305 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1306 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1308 else if (deltai
< i
*6 && i
*6 < gammai
){
1309 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1310 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1313 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1314 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1316 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1317 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1318 trs_current
->varset
.varset
= relvarset1
;
1319 trs_current
->varset
.size
= 18;
1320 trs_current
->next_rel
= trs
;
1323 //Targagent Targbox Target -> Target Targagent Targbox
1324 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1326 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1328 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1330 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1332 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1334 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1335 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1336 if (i
*6 < deltai
&& deltai
< gammai
){
1337 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1338 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1340 else if (deltai
< gammai
&& gammai
< i
*6){
1341 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1342 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1344 else if (gammai
< i
*6 && i
*6 < deltai
){
1345 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1346 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1348 else if (i
*6 < gammai
&& gammai
< deltai
){
1349 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1350 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1352 else if (deltai
< i
*6 && i
*6 < gammai
){
1353 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1354 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1357 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1358 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1360 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1361 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1362 trs_current
->varset
.varset
= relvarset1
;
1363 trs_current
->varset
.size
= 18;
1364 trs_current
->next_rel
= trs
;
1375 if (trs_current != NULL) printf("LEFT ok!\n");
1376 else printf ("LEFT is empty\n");
1377 printf("Num of trans relations:%d\n", countTrans(trs));
1380 if (trs_current != NULL) printf("UP ok!\n");
1381 else printf ("UP is empty\n");
1382 printf("Num of trans relations:%d\n", countTrans(trs));
1385 if (trs_current != NULL) printf("RIGHT ok!\n");
1386 else printf ("RIGHT is empty\n");
1387 printf("Num of trans relations:%d\n", countTrans(trs));
1390 if (trs_current != NULL) printf("DOWN ok!\n");
1391 else printf ("DOWN is empty\n");
1392 printf("Num of trans relations:%d\n", countTrans(trs));
1401 int countTrans(trans_t *trs)
1404 while (trs != NULL){
1406 trs = trs->next_rel;
1411 rels
*encode_rel(sokoban_screen
*screen
)
1415 trans_t
*tl
= sylvan_false
;
1418 tl
= create_single_rel(screen
, LEFT
);
1421 trans_t
*tu
= create_single_rel(screen
, UP
);
1424 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1427 trans_t
*td
= create_single_rel(screen
, DOWN
);
1430 rls
= (rels
*)malloc(sizeof(rels
));
1439 int test_trans(state
*s
, trans_t
*t
)
1442 BDD next
= sylvan_false
;
1444 next
= sylvan_relnext(s
->bdd
, t
->bdd
, t
->varset
.varset
);
1445 if (next
== s
->bdd
) printf("Same\n");
1446 if (next
!= s
->bdd
&& next
!= sylvan_false
) printf("Different\n");
1447 if (next
== sylvan_false
) printf("False\n");