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 BDD visited
= init
->bdd
;
252 tmp_state
->bdd
= init
->bdd
;
253 tmp_state
->vars
= init
->vars
;
254 tmp_state
->lrd
= NULL
;
255 state_queue
= enq(tmp_state
, state_queue
);
257 while (isEmpty(state_queue
) == 0){
258 tmp_state
= get_front(state_queue
);
259 state_queue
= deq(state_queue
);
260 new = tmp_state
->bdd
;
263 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
264 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
267 if (new != sylvan_false
&& new != tmp_state
->bdd
){
268 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
269 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
270 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
271 lrd
= tmp_state
->lrd
;
272 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
273 new_state
->bdd
= new;
274 new_state
->vars
= init
->vars
;
275 lrd
= lappend(lrd
, 'l');
276 new_state
->lrd
= lrd
;
277 state_queue
= enq(new_state
, state_queue
);
278 visited
= sylvan_or(new, visited
);
282 lurd_t
*lrd
= tmp_state
->lrd
;
283 state_t
*new_state
= NULL
;
284 new_state
= (state_t
*)malloc(sizeof(state_t
));
285 new_state
->bdd
= new;
286 new_state
->vars
= init
->vars
;
287 lrd
= lappend(lrd
, 'l');
288 new_state
->lrd
= lrd
;
296 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
297 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
300 if (new != sylvan_false
&& new != tmp_state
->bdd
){
301 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
302 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
303 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
304 lrd
= tmp_state
->lrd
;
305 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
306 new_state
->bdd
= new;
307 new_state
->vars
= init
->vars
;
308 lrd
= lappend(lrd
, 'u');
309 new_state
->lrd
= lrd
;
310 state_queue
= enq(new_state
, state_queue
);
311 visited
= sylvan_or(new, visited
);
315 lurd_t
*lrd
= tmp_state
->lrd
;
316 state_t
*new_state
= NULL
;
317 new_state
= (state_t
*)malloc(sizeof(state_t
));
318 new_state
->bdd
= new;
319 new_state
->vars
= init
->vars
;
320 lrd
= lappend(lrd
, 'u');
321 new_state
->lrd
= lrd
;
329 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
330 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
333 if (new != sylvan_false
&& new != tmp_state
->bdd
){
334 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
335 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
336 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
337 lrd
= tmp_state
->lrd
;
338 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
339 new_state
->bdd
= new;
340 new_state
->vars
= init
->vars
;
341 lrd
= lappend(lrd
, 'r');
342 new_state
->lrd
= lrd
;
343 state_queue
= enq(new_state
, state_queue
);
344 visited
= sylvan_or(new, visited
);
348 lurd_t
*lrd
= tmp_state
->lrd
;
349 state_t
*new_state
= NULL
;
350 new_state
= (state_t
*)malloc(sizeof(state_t
));
351 new_state
->bdd
= new;
352 new_state
->vars
= init
->vars
;
353 lrd
= lappend(lrd
, 'r');
354 new_state
->lrd
= lrd
;
363 new = sylvan_relnext(tmp_state
->bdd
, t
->bdd
, t
->varset
.varset
);
364 if (new != sylvan_false
&& new != tmp_state
->bdd
) break;
367 if (new != sylvan_false
&& new != tmp_state
->bdd
){
368 if (check_visited(new, visited
, init
->vars
.varset
) == 0){
369 if (check_goal(new, g
->bdd
, init
->vars
.varset
) == 0){
370 lurd_t
*lrd
= (lurd_t
*)malloc(sizeof(lurd_t
));
371 lrd
= tmp_state
->lrd
;
372 state_t
*new_state
= (state_t
*)malloc(sizeof(state_t
));
373 new_state
->bdd
= new;
374 new_state
->vars
= init
->vars
;
375 lrd
= lappend(lrd
, 'd');
376 new_state
->lrd
= lrd
;
377 state_queue
= enq(new_state
, state_queue
);
378 visited
= sylvan_or(new, visited
);
382 lurd_t
*lrd
= tmp_state
->lrd
;
383 state_t
*new_state
= NULL
;
384 new_state
= (state_t
*)malloc(sizeof(state_t
));
385 new_state
->bdd
= new;
386 new_state
->vars
= init
->vars
;
387 lrd
= lappend(lrd
, 'd');
388 new_state
->lrd
= lrd
;
400 state
*encode_goal(sokoban_screen
*screen
){
406 BDDVAR vars
[HASH_COUNT(screen
) * 3];
407 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
411 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
413 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
415 state
*fullState
= NULL
;
416 fullState
= (state
*)malloc(sizeof(state
));
417 fullState
->vars
.varset
= varset
;
418 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
421 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
423 case FREE
: //001 -> any
424 st_enc
[tile_index
] = 2;
426 st_enc
[tile_index
] = 2;
428 st_enc
[tile_index
] = 2;
431 case WALL
: //000 -> stays the same
432 st_enc
[tile_index
] = 0;
434 st_enc
[tile_index
] = 0;
436 st_enc
[tile_index
] = 0;
439 case BOX
: //010 -> any
441 st_enc
[tile_index
] = 2;
443 st_enc
[tile_index
] = 2;
445 st_enc
[tile_index
] = 2;
448 case TARGET
: //011 -> targbox
450 st_enc
[tile_index
] = 1;
452 st_enc
[tile_index
] = 0;
454 st_enc
[tile_index
] = 0;
457 case AGENT
: //101 -> any
458 st_enc
[tile_index
] = 2;
460 st_enc
[tile_index
] = 2;
462 st_enc
[tile_index
] = 2;
465 case TARGAGENT
: //110 -> targbox
467 st_enc
[tile_index
] = 1;
469 st_enc
[tile_index
] = 0;
471 st_enc
[tile_index
] = 0;
474 case TARGBOX
: //100 -> stays the same
477 st_enc
[tile_index
] = 1;
479 st_enc
[tile_index
] = 0;
481 st_enc
[tile_index
] = 0;
486 s
= sylvan_cube(varset
, st_enc
);
488 printf("Goal state encoded\n");
489 if (targets
== 0 || (boxes
!= targets
)) return NULL
;
490 else return fullState
;
495 //int countTrans(trans_t *trs);
497 trans_t
*create_single_rel(sokoban_screen
*screen
, direction dir
)
500 trans_t
*trs
, *trs_current
;
501 bimap
*bm
= create_bimap_helper(screen
);
504 bddvar_xy_map
*bddxy
= NULL
;
537 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
538 bddxy
= getbdd(i
*6, bm
->t
);
541 if (check_space(x
, y
, dir
, 1, bm
) == 0){
543 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
544 BDDVAR relvars
[6] = {i
* 6, i
* 6 + 1, i
* 6 + 2, i
* 6 + 3, i
* 6 + 4, i
* 6 + 5};
545 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
546 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
547 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
548 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
549 trs_current
->varset
.varset
= relvarset
;
550 trs_current
->varset
.size
= 6;
551 trs_current
->next_rel
= trs
;
554 //Targagent -> Targagent
555 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
556 relvarset
= sylvan_set_fromarray(relvars
, 6);
557 uint8_t rel_enc1
[6] = {1, 1, 1, 1, 0, 0};
558 memcpy(rel_enc
, rel_enc1
, 6*sizeof(uint8_t));
560 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
561 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
562 trs_current
->varset
.varset
= relvarset
;
563 trs_current
->varset
.size
= 6;
564 trs_current
->next_rel
= trs
;
569 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
570 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
571 unsigned int deltai
= bddvar
->value
.var
[0];
572 //Agent Free -> Free Agent
573 //(1 0 0 0 1 1 0 1 0 0 1 1)
575 //(0 1 0 0 1 1 1 0 0 0 1 1)
576 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};
577 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
580 uint8_t rel_enc0
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
581 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
584 uint8_t rel_enc0
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
585 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
587 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
588 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
589 trs_current
->varset
.varset
= relvarset
;
590 trs_current
->varset
.size
= 12;
591 trs_current
->next_rel
= trs
;
594 //Agent Target -> Free Targagent
595 //(1 0 0 0 1 1 0 1 1 1 1 0)
597 //(0 1 1 1 1 0 1 0 0 0 1 1)
598 relvarset
= sylvan_set_fromarray(relvars
, 12);
600 uint8_t rel_enc2
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
601 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
604 uint8_t rel_enc2
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
605 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
607 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
608 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
609 trs_current
->varset
.varset
= relvarset
;
610 trs_current
->varset
.size
= 12;
611 trs_current
->next_rel
= trs
;
614 //Targagent Free -> Target Agent
615 //(1 0 1 1 0 1 0 1 0 0 1 1)
617 //(0 1 0 0 1 1 1 0 1 1 0 1)
618 relvarset
= sylvan_set_fromarray(relvars
, 12);
620 uint8_t rel_enc3
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
621 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
624 uint8_t rel_enc3
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
625 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
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 //Targagent Target -> Target Targagent
635 //(1 0 1 1 0 1 0 1 1 1 1 0)
637 //(0 1 1 1 1 0 1 0 1 1 0 1)
638 relvarset
= sylvan_set_fromarray(relvars
, 12);
640 uint8_t rel_enc4
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
641 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
644 uint8_t rel_enc4
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
645 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
647 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
648 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
649 trs_current
->varset
.varset
= relvarset
;
650 trs_current
->varset
.size
= 12;
651 trs_current
->next_rel
= trs
;
654 //Agent Box -> Agent Box
655 //(1 1 0 0 1 1 0 0 1 1 0 0)
657 //(0 0 1 1 0 0 1 1 0 0 1 1)
658 relvarset
= sylvan_set_fromarray(relvars
, 12);
660 uint8_t rel_enc5
[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
661 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
664 uint8_t rel_enc5
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
665 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
667 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
668 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
669 trs_current
->varset
.varset
= relvarset
;
670 trs_current
->varset
.size
= 12;
671 trs_current
->next_rel
= trs
;
674 //Agent Targbox -> Agent Targbox
675 //(1 1 0 0 1 1 1 1 0 0 0 0)
677 //(1 1 0 0 0 0 1 1 0 0 1 1)
678 relvarset
= sylvan_set_fromarray(relvars
, 12);
680 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
681 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
684 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
685 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
687 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
688 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
689 trs_current
->varset
.varset
= relvarset
;
690 trs_current
->varset
.size
= 12;
691 trs_current
->next_rel
= trs
;
694 //Targagent Box -> Targagent Box
695 //(1 1 1 1 0 0 0 0 1 1 0 0)
697 //(0 0 1 1 0 0 1 1 1 1 0 0)
698 relvarset
= sylvan_set_fromarray(relvars
, 12);
700 uint8_t rel_enc7
[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
701 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
704 uint8_t rel_enc7
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
705 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
707 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
708 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
709 trs_current
->varset
.varset
= relvarset
;
710 trs_current
->varset
.size
= 12;
711 trs_current
->next_rel
= trs
;
714 //Targagent Targbox -> Targagent Targbox
715 //(1 1 1 1 0 0 1 1 0 0 0 0)
717 //(1 1 0 0 0 0 1 1 1 1 0 0)
718 relvarset
= sylvan_set_fromarray(relvars
, 12);
720 uint8_t rel_enc8
[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
721 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
724 uint8_t rel_enc8
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
725 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
727 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
728 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
729 trs_current
->varset
.varset
= relvarset
;
730 trs_current
->varset
.size
= 12;
731 trs_current
->next_rel
= trs
;
737 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
738 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
739 unsigned int deltai
= bddvar
->value
.var
[0];
740 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
741 unsigned int gammai
= bddvar
->value
.var
[0];
742 //Agent Free -> Free Agent
743 //(1 0 0 0 1 1 0 1 0 0 1 1)
745 //(0 1 0 0 1 1 1 0 0 0 1 1)
746 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};
747 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
750 uint8_t rel_enc_
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
751 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
754 uint8_t rel_enc_
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
755 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
757 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
758 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
759 trs_current
->varset
.varset
= relvarset
;
760 trs_current
->varset
.size
= 12;
761 trs_current
->next_rel
= trs
;
764 //Agent Target -> Free Targagent
765 //(1 0 0 0 1 1 0 1 1 1 1 0)
767 //(0 1 1 1 1 0 1 0 0 0 1 1)
768 relvarset
= sylvan_set_fromarray(relvars
, 12);
770 uint8_t rel_enc9
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
771 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
774 uint8_t rel_enc9
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
775 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
777 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
778 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
779 trs_current
->varset
.varset
= relvarset
;
780 trs_current
->varset
.size
= 12;
781 trs_current
->next_rel
= trs
;
784 //Targagent Free -> Target Agent (LEFT || UP)
785 //(1 0 1 1 0 1 0 1 0 0 1 1)
787 //(0 1 0 0 1 1 1 0 1 1 0 1)
788 relvarset
= sylvan_set_fromarray(relvars
, 12);
790 uint8_t rel_enc10
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
791 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
794 uint8_t rel_enc10
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
795 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
797 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
798 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
799 trs_current
->varset
.varset
= relvarset
;
800 trs_current
->varset
.size
= 12;
801 trs_current
->next_rel
= trs
;
804 //Targagent Target -> Target Targagent (LEFT || UP)
805 //(1 0 1 1 0 1 0 1 1 1 1 0)
807 //(0 1 1 1 1 0 1 0 1 1 0 1)
808 relvarset
= sylvan_set_fromarray(relvars
, 12);
810 uint8_t rel_enc11
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
811 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
814 uint8_t rel_enc11
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
815 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
817 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
818 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
819 trs_current
->varset
.varset
= relvarset
;
820 trs_current
->varset
.size
= 12;
821 trs_current
->next_rel
= trs
;
824 //Agent Box Box -> Agent Box Box
825 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
827 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
829 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
831 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
833 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
835 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
836 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};
837 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
838 uint8_t rel_enc1
[18];
839 if (i
*6 < deltai
&& deltai
< gammai
){
840 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
841 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
843 else if (deltai
< gammai
&& gammai
< i
*6){
844 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
845 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
847 else if (gammai
< i
*6 && i
*6 < deltai
){
848 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
849 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
851 else if (i
*6 < gammai
&& gammai
< deltai
){
852 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
853 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
855 else if (deltai
< i
*6 && i
*6 < gammai
){
856 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
857 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
860 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
861 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
864 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
865 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
866 trs_current
->varset
.varset
= relvarset1
;
867 trs_current
->varset
.size
= 18;
868 trs_current
->next_rel
= trs
;
871 //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
872 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
874 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
876 //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
878 //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
880 //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
882 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
883 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
884 if (i
*6 < deltai
&& deltai
< gammai
){
885 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
886 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
888 else if (deltai
< gammai
&& gammai
< i
*6){
889 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
890 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
892 else if (gammai
< i
*6 && i
*6 < deltai
){
893 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
894 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
896 else if (i
*6 < gammai
&& gammai
< deltai
){
897 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
898 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
900 else if (deltai
< i
*6 && i
*6 < gammai
){
901 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
902 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
905 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
906 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
908 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
909 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
910 trs_current
->varset
.varset
= relvarset1
;
911 trs_current
->varset
.size
= 18;
912 trs_current
->next_rel
= trs
;
915 //Targagent Box Box -> Targagent Box Box
916 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
918 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
920 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
922 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
924 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
926 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
927 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
928 if (i
*6 < deltai
&& deltai
< gammai
){
929 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
930 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
932 else if (deltai
< gammai
&& gammai
< i
*6){
933 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
934 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
936 else if (gammai
< i
*6 && i
*6 < deltai
){
937 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
938 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
940 else if (i
*6 < gammai
&& gammai
< deltai
){
941 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
942 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
944 else if (deltai
< i
*6 && i
*6 < gammai
){
945 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
946 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
949 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
950 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
952 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
953 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
954 trs_current
->varset
.varset
= relvarset1
;
955 trs_current
->varset
.size
= 18;
956 trs_current
->next_rel
= trs
;
959 //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
960 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
962 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
964 //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
966 //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
968 //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
970 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
971 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
972 if (i
*6 < deltai
&& deltai
< gammai
){
973 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
974 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
976 else if (deltai
< gammai
&& gammai
< i
*6){
977 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
978 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
980 else if (gammai
< i
*6 && i
*6 < deltai
){
981 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
982 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
984 else if (i
*6 < gammai
&& gammai
< deltai
){
985 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
986 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
988 else if (deltai
< i
*6 && i
*6 < gammai
){
989 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
990 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
993 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
994 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
996 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
997 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
998 trs_current
->varset
.varset
= relvarset1
;
999 trs_current
->varset
.size
= 18;
1000 trs_current
->next_rel
= trs
;
1003 //Agent Box Free -> Free Agent Box
1004 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
1006 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
1008 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
1010 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
1012 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
1014 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1015 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1016 if (i
*6 < deltai
&& deltai
< gammai
){
1017 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1018 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1021 else if (deltai
< gammai
&& gammai
< i
*6){
1022 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1023 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1026 else if (gammai
< i
*6 && i
*6 < deltai
){
1027 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1028 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1031 else if (i
*6 < gammai
&& gammai
< deltai
){
1032 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1033 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1035 else if (deltai
< i
*6 && i
*6 < gammai
){
1036 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1037 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1040 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1041 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1044 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1046 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1047 trs_current
->varset
.varset
= relvarset1
;
1048 trs_current
->varset
.size
= 18;
1049 trs_current
->next_rel
= trs
;
1052 //Agent Targbox Free -> Free Targagent Box
1053 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
1055 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
1057 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1059 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
1061 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
1063 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1064 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1065 if (i
*6 < deltai
&& deltai
< gammai
){
1066 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1067 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1069 else if (deltai
< gammai
&& gammai
< i
*6){
1070 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1071 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1073 else if (gammai
< i
*6 && i
*6 < deltai
){
1074 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1075 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1077 else if (i
*6 < gammai
&& gammai
< deltai
){
1078 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1079 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1081 else if (deltai
< i
*6 && i
*6 < gammai
){
1082 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1083 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1086 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1087 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1089 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1090 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1091 trs_current
->varset
.varset
= relvarset1
;
1092 trs_current
->varset
.size
= 18;
1093 trs_current
->next_rel
= trs
;
1096 //Agent Box Target -> Free Agent Targbox
1097 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
1099 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
1101 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
1103 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
1105 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
1107 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1108 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1109 if (i
*6 < deltai
&& deltai
< gammai
){
1110 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1111 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1113 else if (deltai
< gammai
&& gammai
< i
*6){
1114 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1115 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1117 else if (gammai
< i
*6 && i
*6 < deltai
){
1118 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1119 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1121 else if (i
*6 < gammai
&& gammai
< deltai
){
1122 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1123 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1125 else if (deltai
< i
*6 && i
*6 < gammai
){
1126 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1127 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1130 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1131 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1133 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1134 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1135 trs_current
->varset
.varset
= relvarset1
;
1136 trs_current
->varset
.size
= 18;
1137 trs_current
->next_rel
= trs
;
1140 //Agent Targbox Target -> Free Targagent Targbox
1141 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
1143 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
1145 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1147 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
1149 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
1151 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1152 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1153 if (i
*6 < deltai
&& deltai
< gammai
){
1154 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1155 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1157 else if (deltai
< gammai
&& gammai
< i
*6){
1158 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1159 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1161 else if (gammai
< i
*6 && i
*6 < deltai
){
1162 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1163 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1165 else if (i
*6 < gammai
&& gammai
< deltai
){
1166 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1167 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1169 else if (deltai
< i
*6 && i
*6 < gammai
){
1170 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1171 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1174 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1175 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1177 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1178 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1179 trs_current
->varset
.varset
= relvarset1
;
1180 trs_current
->varset
.size
= 18;
1181 trs_current
->next_rel
= trs
;
1184 //Targagent Box Free -> Target Agent Box
1185 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
1187 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
1189 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1191 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
1193 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
1195 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1196 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1197 if (i
*6 < deltai
&& deltai
< gammai
){
1198 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1199 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1201 else if (deltai
< gammai
&& gammai
< i
*6){
1202 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1203 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1205 else if (gammai
< i
*6 && i
*6 < deltai
){
1206 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1207 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1209 else if (i
*6 < gammai
&& gammai
< deltai
){
1210 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1211 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1213 else if (deltai
< i
*6 && i
*6 < gammai
){
1214 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
1215 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1218 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1219 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1221 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1222 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1223 trs_current
->varset
.varset
= relvarset1
;
1224 trs_current
->varset
.size
= 18;
1225 trs_current
->next_rel
= trs
;
1228 //Targagent Targbox Free -> Target Targagent Box
1229 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
1231 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
1233 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1235 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
1237 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
1239 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1240 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1241 if (i
*6 < deltai
&& deltai
< gammai
){
1242 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1243 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1245 else if (deltai
< gammai
&& gammai
< i
*6){
1246 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1247 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1249 else if (gammai
< i
*6 && i
*6 < deltai
){
1250 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1251 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1253 else if (i
*6 < gammai
&& gammai
< deltai
){
1254 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1255 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1257 else if (deltai
< i
*6 && i
*6 < gammai
){
1258 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0};
1259 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1262 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1263 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1265 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1266 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1267 trs_current
->varset
.varset
= relvarset1
;
1268 trs_current
->varset
.size
= 18;
1269 trs_current
->next_rel
= trs
;
1272 //Targagent Box Target -> Target Agent Targbox
1273 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1275 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1277 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1279 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1281 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1283 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1284 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1285 if (i
*6 < deltai
&& deltai
< gammai
){
1286 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1287 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1289 else if (deltai
< gammai
&& gammai
< i
*6){
1290 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1291 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1293 else if (gammai
< i
*6 && i
*6 < deltai
){
1294 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1295 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1297 else if (i
*6 < gammai
&& gammai
< deltai
){
1298 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1299 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1301 else if (deltai
< i
*6 && i
*6 < gammai
){
1302 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1303 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1306 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1307 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1309 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1310 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1311 trs_current
->varset
.varset
= relvarset1
;
1312 trs_current
->varset
.size
= 18;
1313 trs_current
->next_rel
= trs
;
1316 //Targagent Targbox Target -> Target Targagent Targbox
1317 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1319 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1321 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1323 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1325 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1327 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1328 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1329 if (i
*6 < deltai
&& deltai
< gammai
){
1330 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1331 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1333 else if (deltai
< gammai
&& gammai
< i
*6){
1334 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1335 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1337 else if (gammai
< i
*6 && i
*6 < deltai
){
1338 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1339 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1341 else if (i
*6 < gammai
&& gammai
< deltai
){
1342 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1343 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1345 else if (deltai
< i
*6 && i
*6 < gammai
){
1346 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1347 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1350 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1351 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1353 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1354 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1355 trs_current
->varset
.varset
= relvarset1
;
1356 trs_current
->varset
.size
= 18;
1357 trs_current
->next_rel
= trs
;
1368 if (trs_current != NULL) printf("LEFT ok!\n");
1369 else printf ("LEFT is empty\n");
1370 printf("Num of trans relations:%d\n", countTrans(trs));
1373 if (trs_current != NULL) printf("UP ok!\n");
1374 else printf ("UP is empty\n");
1375 printf("Num of trans relations:%d\n", countTrans(trs));
1378 if (trs_current != NULL) printf("RIGHT ok!\n");
1379 else printf ("RIGHT is empty\n");
1380 printf("Num of trans relations:%d\n", countTrans(trs));
1383 if (trs_current != NULL) printf("DOWN ok!\n");
1384 else printf ("DOWN is empty\n");
1385 printf("Num of trans relations:%d\n", countTrans(trs));
1394 int countTrans(trans_t *trs)
1397 while (trs != NULL){
1399 trs = trs->next_rel;
1404 rels
*encode_rel(sokoban_screen
*screen
)
1408 trans_t
*tl
= sylvan_false
;
1411 tl
= create_single_rel(screen
, LEFT
);
1414 trans_t
*tu
= create_single_rel(screen
, UP
);
1417 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1420 trans_t
*td
= create_single_rel(screen
, DOWN
);
1423 rls
= (rels
*)malloc(sizeof(rels
));
1432 int test_trans(state
*s
, trans_t
*t
)
1435 BDD next
= sylvan_false
;
1437 next
= sylvan_relnext(s
->bdd
, t
->bdd
, t
->varset
.varset
);
1438 if (next
== s
->bdd
) printf("Same\n");
1439 if (next
!= s
->bdd
&& next
!= sylvan_false
) printf("Different\n");
1440 if (next
== sylvan_false
) printf("False\n");