37 xy_bddvar_map
*getxy(int x
, int y
, xy_bddvar_map
*map
)
39 xy_bddvar_map k
, *r
= NULL
;
40 memset(&k
, 0, sizeof(xy_bddvar_map
));
43 HASH_FIND(hh
, map
, &k
.key
, sizeof(xy
), r
);
47 bddvar_xy_map
*getbdd(int key
, bddvar_xy_map
*map
)
49 bddvar_xy_map k
, *r
= NULL
;
50 memset(&k
, 0, sizeof(bddvar_xy_map
));
52 HASH_FIND(hh
, map
, &k
.key
, sizeof(int), r
);
57 bimap
*create_bimap_helper(sokoban_screen
*screen
)
61 xy_bddvar_map
*xybdd
= NULL
;
62 bddvar_xy_map
*bddxy
= NULL
;
63 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
64 xy_bddvar_map
*f
= NULL
;
65 f
= (xy_bddvar_map
*)malloc(sizeof(xy_bddvar_map
));
66 memset(f
, 0, sizeof(xy_bddvar_map
));
67 f
->key
.x
= r
->coord
.x
;
68 f
->key
.y
= r
->coord
.y
;
69 f
->value
.var
[0] = varcount
* 2;
70 f
->value
.var
[1] = (varcount
+ 1) * 2;
71 f
->value
.var
[2] = (varcount
+ 2) * 2;
72 HASH_ADD(hh
, xybdd
, key
, sizeof(xy
), f
);
74 for (int i
= 0; i
<3; i
++){
75 bddvar_xy_map
*t
= NULL
;
76 t
= (bddvar_xy_map
*)malloc(sizeof(bddvar_xy_map
));
77 memset(t
, 0, sizeof(bddvar_xy_map
));
78 t
->key
= (varcount
+ i
) * 2;
79 t
->value
.x
= r
->coord
.x
;
80 t
->value
.y
= r
->coord
.y
;
81 HASH_ADD(hh
, bddxy
, key
, sizeof(int), t
);
83 varcount
= varcount
+ 3;
86 bm
= (bimap
*)malloc(sizeof(bimap
));
92 int check_xy_exists(int x
, int y
, bimap
*bm
)
95 if (getxy(x
, y
, bm
->f
) != NULL
) res
= 1;
99 int check_space(int x
, int y
, direction d
, int delta
, bimap
*bm
)
102 case LEFT
: x
= x
- delta
; break;
103 case UP
: y
= y
- delta
; break;
104 case RIGHT
: x
= x
+ delta
; break;
105 case DOWN
: y
= y
+ delta
; break;
107 return check_xy_exists(x
, y
, bm
);
111 * Each coordinate has three related boolean variables. The combination of those boolean variables
119 * 110: Agent on target
120 * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
121 * tiles in the shrinked screen.
122 * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
123 * directly in transition relations.
126 state
*encode_screen(sokoban_screen
*screen
)
130 BDDVAR vars
[HASH_COUNT(screen
) * 3];
131 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
135 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
137 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
139 state
*fullState
= NULL
;
140 fullState
= (state
*)malloc(sizeof(state
));
141 fullState
->vars
.varset
= varset
;
142 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
145 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
148 st_enc
[tile_index
] = 0;
150 st_enc
[tile_index
] = 0;
152 st_enc
[tile_index
] = 1;
156 st_enc
[tile_index
] = 0;
158 st_enc
[tile_index
] = 0;
160 st_enc
[tile_index
] = 0;
164 st_enc
[tile_index
] = 0;
166 st_enc
[tile_index
] = 1;
168 st_enc
[tile_index
] = 0;
172 st_enc
[tile_index
] = 0;
174 st_enc
[tile_index
] = 1;
176 st_enc
[tile_index
] = 1;
180 st_enc
[tile_index
] = 1;
182 st_enc
[tile_index
] = 0;
185 st_enc
[tile_index
] = 1;
188 case TARGAGENT
: //110
189 st_enc
[tile_index
] = 1;
191 st_enc
[tile_index
] = 1;
193 st_enc
[tile_index
] = 0;
197 st_enc
[tile_index
] = 1;
199 st_enc
[tile_index
] = 0;
201 st_enc
[tile_index
] = 0;
206 s
= sylvan_cube(varset
, st_enc
);
208 printf("Initial state encoded\n");
212 state
*encode_goal(sokoban_screen
*screen
){
218 BDDVAR vars
[HASH_COUNT(screen
) * 3];
219 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
223 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
225 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
227 state
*fullState
= NULL
;
228 fullState
= (state
*)malloc(sizeof(state
));
229 fullState
->vars
.varset
= varset
;
230 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
233 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
235 case FREE
: //001 -> any
236 st_enc
[tile_index
] = 2;
238 st_enc
[tile_index
] = 2;
240 st_enc
[tile_index
] = 2;
243 case WALL
: //000 -> stays the same
244 st_enc
[tile_index
] = 0;
246 st_enc
[tile_index
] = 0;
248 st_enc
[tile_index
] = 0;
251 case BOX
: //010 -> any
253 st_enc
[tile_index
] = 2;
255 st_enc
[tile_index
] = 2;
257 st_enc
[tile_index
] = 2;
260 case TARGET
: //011 -> targbox
262 st_enc
[tile_index
] = 1;
264 st_enc
[tile_index
] = 0;
266 st_enc
[tile_index
] = 0;
269 case AGENT
: //101 -> any
270 st_enc
[tile_index
] = 2;
272 st_enc
[tile_index
] = 2;
274 st_enc
[tile_index
] = 2;
277 case TARGAGENT
: //110 -> targbox
279 st_enc
[tile_index
] = 1;
281 st_enc
[tile_index
] = 0;
283 st_enc
[tile_index
] = 0;
286 case TARGBOX
: //100 -> stays the same
289 st_enc
[tile_index
] = 1;
291 st_enc
[tile_index
] = 0;
293 st_enc
[tile_index
] = 0;
298 s
= sylvan_cube(varset
, st_enc
);
300 printf("Goal state encoded\n");
301 if (targets
== 0 || (boxes
!= targets
)) return NULL
;
302 else return fullState
;
307 //int countTrans(trans_t *trs);
309 trans_t
*create_single_rel(sokoban_screen
*screen
, direction dir
)
312 trans_t
*trs
, *trs_current
;
313 bimap
*bm
= create_bimap_helper(screen
);
316 bddvar_xy_map
*bddxy
= NULL
;
349 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
350 bddxy
= getbdd(i
*6, bm
->t
);
353 if (check_space(x
, y
, dir
, 1, bm
) == 0){
355 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
356 BDDVAR relvars
[6] = {i
* 6, i
* 6 + 1, i
* 6 + 2, i
* 6 + 3, i
* 6 + 4, i
* 6 + 5};
357 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
358 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
359 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
360 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
361 trs_current
->varset
.varset
= relvarset
;
362 trs_current
->varset
.size
= 6;
363 trs_current
->next_rel
= trs
;
366 //Targagent -> Targagent
367 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
368 relvarset
= sylvan_set_fromarray(relvars
, 6);
369 uint8_t rel_enc1
[6] = {1, 1, 1, 1, 0, 0};
370 memcpy(rel_enc
, rel_enc1
, 6*sizeof(uint8_t));
372 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
373 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
374 trs_current
->varset
.varset
= relvarset
;
375 trs_current
->varset
.size
= 6;
376 trs_current
->next_rel
= trs
;
381 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
382 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
383 unsigned int deltai
= bddvar
->value
.var
[0];
384 //Agent Free -> Free Agent
385 //(1 0 0 0 1 1 0 1 0 0 1 1)
387 //(0 1 0 0 1 1 1 0 0 0 1 1)
388 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};
389 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
392 uint8_t rel_enc0
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
393 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
396 uint8_t rel_enc0
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
397 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
399 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
400 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
401 trs_current
->varset
.varset
= relvarset
;
402 trs_current
->varset
.size
= 12;
403 trs_current
->next_rel
= trs
;
406 //Agent Target -> Free Targagent
407 //(1 0 0 0 1 1 0 1 1 1 1 0)
409 //(0 1 1 1 1 0 1 0 0 0 1 1)
410 relvarset
= sylvan_set_fromarray(relvars
, 12);
412 uint8_t rel_enc2
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
413 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
416 uint8_t rel_enc2
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
417 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
419 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
420 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
421 trs_current
->varset
.varset
= relvarset
;
422 trs_current
->varset
.size
= 12;
423 trs_current
->next_rel
= trs
;
426 //Targagent Free -> Target Agent
427 //(1 0 1 1 0 1 0 1 0 0 1 1)
429 //(0 1 0 0 1 1 1 0 1 1 0 1)
430 relvarset
= sylvan_set_fromarray(relvars
, 12);
432 uint8_t rel_enc3
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
433 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
436 uint8_t rel_enc3
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
437 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
439 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
440 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
441 trs_current
->varset
.varset
= relvarset
;
442 trs_current
->varset
.size
= 12;
443 trs_current
->next_rel
= trs
;
446 //Targagent Target -> Target Targagent
447 //(1 0 1 1 0 1 0 1 1 1 1 0)
449 //(0 1 1 1 1 0 1 0 1 1 0 1)
450 relvarset
= sylvan_set_fromarray(relvars
, 12);
452 uint8_t rel_enc4
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
453 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
456 uint8_t rel_enc4
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
457 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
459 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
460 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
461 trs_current
->varset
.varset
= relvarset
;
462 trs_current
->varset
.size
= 12;
463 trs_current
->next_rel
= trs
;
466 //Agent Box -> Agent Box
467 //(1 1 0 0 1 1 0 0 1 1 0 0)
469 //(0 0 1 1 0 0 1 1 0 0 1 1)
470 relvarset
= sylvan_set_fromarray(relvars
, 12);
472 uint8_t rel_enc5
[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
473 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
476 uint8_t rel_enc5
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
477 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
479 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
480 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
481 trs_current
->varset
.varset
= relvarset
;
482 trs_current
->varset
.size
= 12;
483 trs_current
->next_rel
= trs
;
486 //Agent Targbox -> Agent Targbox
487 //(1 1 0 0 1 1 1 1 0 0 0 0)
489 //(1 1 0 0 0 0 1 1 0 0 1 1)
490 relvarset
= sylvan_set_fromarray(relvars
, 12);
492 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
493 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
496 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
497 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
499 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
500 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
501 trs_current
->varset
.varset
= relvarset
;
502 trs_current
->varset
.size
= 12;
503 trs_current
->next_rel
= trs
;
506 //Targagent Box -> Targagent Box
507 //(1 1 1 1 0 0 0 0 1 1 0 0)
509 //(0 0 1 1 0 0 1 1 1 1 0 0)
510 relvarset
= sylvan_set_fromarray(relvars
, 12);
512 uint8_t rel_enc7
[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
513 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
516 uint8_t rel_enc7
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
517 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
519 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
520 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
521 trs_current
->varset
.varset
= relvarset
;
522 trs_current
->varset
.size
= 12;
523 trs_current
->next_rel
= trs
;
526 //Targagent Targbox -> Targagent Targbox
527 //(1 1 1 1 0 0 1 1 0 0 0 0)
529 //(1 1 0 0 0 0 1 1 1 1 0 0)
530 relvarset
= sylvan_set_fromarray(relvars
, 12);
532 uint8_t rel_enc8
[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
533 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
536 uint8_t rel_enc8
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
537 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
539 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
540 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
541 trs_current
->varset
.varset
= relvarset
;
542 trs_current
->varset
.size
= 12;
543 trs_current
->next_rel
= trs
;
549 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
550 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
551 unsigned int deltai
= bddvar
->value
.var
[0];
552 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
553 unsigned int gammai
= bddvar
->value
.var
[0];
554 //Agent Free -> Free Agent
555 //(1 0 0 0 1 1 0 1 0 0 1 1)
557 //(0 1 0 0 1 1 1 0 0 0 1 1)
558 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};
559 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
562 uint8_t rel_enc_
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
563 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
566 uint8_t rel_enc_
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
567 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
569 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
570 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
571 trs_current
->varset
.varset
= relvarset
;
572 trs_current
->varset
.size
= 12;
573 trs_current
->next_rel
= trs
;
576 //Agent Target -> Free Targagent
577 //(1 0 0 0 1 1 0 1 1 1 1 0)
579 //(0 1 1 1 1 0 1 0 0 0 1 1)
580 relvarset
= sylvan_set_fromarray(relvars
, 12);
582 uint8_t rel_enc9
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
583 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
586 uint8_t rel_enc9
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
587 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
589 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
590 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
591 trs_current
->varset
.varset
= relvarset
;
592 trs_current
->varset
.size
= 12;
593 trs_current
->next_rel
= trs
;
596 //Targagent Free -> Target Agent (LEFT || UP)
597 //(1 0 1 1 0 1 0 1 0 0 1 1)
599 //(0 1 0 0 1 1 1 0 1 1 0 1)
600 relvarset
= sylvan_set_fromarray(relvars
, 12);
602 uint8_t rel_enc10
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
603 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
606 uint8_t rel_enc10
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
607 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
609 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
610 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
611 trs_current
->varset
.varset
= relvarset
;
612 trs_current
->varset
.size
= 12;
613 trs_current
->next_rel
= trs
;
616 //Targagent Target -> Target Targagent (LEFT || UP)
617 //(1 0 1 1 0 1 0 1 1 1 1 0)
619 //(0 1 1 1 1 0 1 0 1 1 0 1)
620 relvarset
= sylvan_set_fromarray(relvars
, 12);
622 uint8_t rel_enc11
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
623 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
626 uint8_t rel_enc11
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
627 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
629 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
630 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
631 trs_current
->varset
.varset
= relvarset
;
632 trs_current
->varset
.size
= 12;
633 trs_current
->next_rel
= trs
;
636 //Agent Box Box -> Agent Box Box
637 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
639 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
641 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
643 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
645 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
647 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
648 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};
649 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
650 uint8_t rel_enc1
[18];
651 if (i
*6 < deltai
&& deltai
< gammai
){
652 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
653 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
655 else if (deltai
< gammai
&& gammai
< i
*6){
656 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
657 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
659 else if (gammai
< i
*6 && i
*6 < deltai
){
660 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
661 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
663 else if (i
*6 < gammai
&& gammai
< deltai
){
664 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
665 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
667 else if (deltai
< i
*6 && i
*6 < gammai
){
668 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
669 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
672 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
673 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
676 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
677 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
678 trs_current
->varset
.varset
= relvarset1
;
679 trs_current
->varset
.size
= 18;
680 trs_current
->next_rel
= trs
;
683 //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
684 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
686 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
688 //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
690 //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
692 //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
694 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
695 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
696 if (i
*6 < deltai
&& deltai
< gammai
){
697 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
698 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
700 else if (deltai
< gammai
&& gammai
< i
*6){
701 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
702 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
704 else if (gammai
< i
*6 && i
*6 < deltai
){
705 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
706 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
708 else if (i
*6 < gammai
&& gammai
< deltai
){
709 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
710 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
712 else if (deltai
< i
*6 && i
*6 < gammai
){
713 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
714 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
717 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
718 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
720 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
721 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
722 trs_current
->varset
.varset
= relvarset1
;
723 trs_current
->varset
.size
= 18;
724 trs_current
->next_rel
= trs
;
727 //Targagent Box Box -> Targagent Box Box
728 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
730 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
732 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
734 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
736 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
738 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
739 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
740 if (i
*6 < deltai
&& deltai
< gammai
){
741 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
742 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
744 else if (deltai
< gammai
&& gammai
< i
*6){
745 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
746 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
748 else if (gammai
< i
*6 && i
*6 < deltai
){
749 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
750 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
752 else if (i
*6 < gammai
&& gammai
< deltai
){
753 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
754 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
756 else if (deltai
< i
*6 && i
*6 < gammai
){
757 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
758 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
761 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
762 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
764 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
765 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
766 trs_current
->varset
.varset
= relvarset1
;
767 trs_current
->varset
.size
= 18;
768 trs_current
->next_rel
= trs
;
771 //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
772 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
774 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
776 //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
778 //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
780 //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
782 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
783 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
784 if (i
*6 < deltai
&& deltai
< gammai
){
785 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
786 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
788 else if (deltai
< gammai
&& gammai
< i
*6){
789 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
790 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
792 else if (gammai
< i
*6 && i
*6 < deltai
){
793 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
794 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
796 else if (i
*6 < gammai
&& gammai
< deltai
){
797 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
798 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
800 else if (deltai
< i
*6 && i
*6 < gammai
){
801 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
802 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
805 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
806 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
808 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
809 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
810 trs_current
->varset
.varset
= relvarset1
;
811 trs_current
->varset
.size
= 18;
812 trs_current
->next_rel
= trs
;
815 //Agent Box Free -> Free Agent Box
816 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
818 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
820 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
822 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
824 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
826 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
827 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
828 if (i
*6 < deltai
&& deltai
< gammai
){
829 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
830 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
833 else if (deltai
< gammai
&& gammai
< i
*6){
834 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
835 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
838 else if (gammai
< i
*6 && i
*6 < deltai
){
839 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
840 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
843 else if (i
*6 < gammai
&& gammai
< deltai
){
844 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
845 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
847 else if (deltai
< i
*6 && i
*6 < gammai
){
848 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
849 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
852 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
853 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
856 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
858 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
859 trs_current
->varset
.varset
= relvarset1
;
860 trs_current
->varset
.size
= 18;
861 trs_current
->next_rel
= trs
;
864 //Agent Targbox Free -> Free Targagent Box
865 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
867 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
869 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
871 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
873 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
875 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
876 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
877 if (i
*6 < deltai
&& deltai
< gammai
){
878 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
879 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
881 else if (deltai
< gammai
&& gammai
< i
*6){
882 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
883 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
885 else if (gammai
< i
*6 && i
*6 < deltai
){
886 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
887 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
889 else if (i
*6 < gammai
&& gammai
< deltai
){
890 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
891 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
893 else if (deltai
< i
*6 && i
*6 < gammai
){
894 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
895 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
898 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
899 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
901 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
902 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
903 trs_current
->varset
.varset
= relvarset1
;
904 trs_current
->varset
.size
= 18;
905 trs_current
->next_rel
= trs
;
908 //Agent Box Target -> Free Agent Targbox
909 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
911 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
913 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
915 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
917 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
919 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
920 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
921 if (i
*6 < deltai
&& deltai
< gammai
){
922 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
923 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
925 else if (deltai
< gammai
&& gammai
< i
*6){
926 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
927 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
929 else if (gammai
< i
*6 && i
*6 < deltai
){
930 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
931 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
933 else if (i
*6 < gammai
&& gammai
< deltai
){
934 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
935 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
937 else if (deltai
< i
*6 && i
*6 < gammai
){
938 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
939 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
942 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
943 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
945 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
946 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
947 trs_current
->varset
.varset
= relvarset1
;
948 trs_current
->varset
.size
= 18;
949 trs_current
->next_rel
= trs
;
952 //Agent Targbox Target -> Free Targagent Targbox
953 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
955 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
957 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
959 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
961 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
963 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
964 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
965 if (i
*6 < deltai
&& deltai
< gammai
){
966 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
967 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
969 else if (deltai
< gammai
&& gammai
< i
*6){
970 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
971 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
973 else if (gammai
< i
*6 && i
*6 < deltai
){
974 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
975 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
977 else if (i
*6 < gammai
&& gammai
< deltai
){
978 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
979 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
981 else if (deltai
< i
*6 && i
*6 < gammai
){
982 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
983 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
986 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
987 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
989 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
990 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
991 trs_current
->varset
.varset
= relvarset1
;
992 trs_current
->varset
.size
= 18;
993 trs_current
->next_rel
= trs
;
996 //Targagent Box Free -> Target Agent Box
997 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
999 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
1001 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1003 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
1005 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
1007 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1008 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1009 if (i
*6 < deltai
&& deltai
< gammai
){
1010 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1011 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1013 else if (deltai
< gammai
&& gammai
< i
*6){
1014 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1015 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1017 else if (gammai
< i
*6 && i
*6 < deltai
){
1018 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1019 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1021 else if (i
*6 < gammai
&& gammai
< deltai
){
1022 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1023 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1025 else if (deltai
< i
*6 && i
*6 < gammai
){
1026 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
1027 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1030 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1031 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1033 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1034 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1035 trs_current
->varset
.varset
= relvarset1
;
1036 trs_current
->varset
.size
= 18;
1037 trs_current
->next_rel
= trs
;
1040 //Targagent Targbox Free -> Target Targagent Box
1041 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
1043 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
1045 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1047 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
1049 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
1051 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1052 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1053 if (i
*6 < deltai
&& deltai
< gammai
){
1054 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1055 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1057 else if (deltai
< gammai
&& gammai
< i
*6){
1058 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1059 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1061 else if (gammai
< i
*6 && i
*6 < deltai
){
1062 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1063 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1065 else if (i
*6 < gammai
&& gammai
< deltai
){
1066 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1067 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1069 else if (deltai
< i
*6 && i
*6 < gammai
){
1070 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0};
1071 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1074 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1075 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1077 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1078 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1079 trs_current
->varset
.varset
= relvarset1
;
1080 trs_current
->varset
.size
= 18;
1081 trs_current
->next_rel
= trs
;
1084 //Targagent Box Target -> Target Agent Targbox
1085 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1087 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1089 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1091 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1093 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1095 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1096 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1097 if (i
*6 < deltai
&& deltai
< gammai
){
1098 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1099 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1101 else if (deltai
< gammai
&& gammai
< i
*6){
1102 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1103 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1105 else if (gammai
< i
*6 && i
*6 < deltai
){
1106 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1107 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1109 else if (i
*6 < gammai
&& gammai
< deltai
){
1110 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1111 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1113 else if (deltai
< i
*6 && i
*6 < gammai
){
1114 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1115 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1118 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1119 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1121 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1122 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1123 trs_current
->varset
.varset
= relvarset1
;
1124 trs_current
->varset
.size
= 18;
1125 trs_current
->next_rel
= trs
;
1128 //Targagent Targbox Target -> Target Targagent Targbox
1129 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1131 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1133 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1135 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1137 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1139 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1140 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1141 if (i
*6 < deltai
&& deltai
< gammai
){
1142 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1143 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1145 else if (deltai
< gammai
&& gammai
< i
*6){
1146 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1147 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1149 else if (gammai
< i
*6 && i
*6 < deltai
){
1150 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1151 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1153 else if (i
*6 < gammai
&& gammai
< deltai
){
1154 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1155 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1157 else if (deltai
< i
*6 && i
*6 < gammai
){
1158 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1159 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1162 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1163 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1165 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1166 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1167 trs_current
->varset
.varset
= relvarset1
;
1168 trs_current
->varset
.size
= 18;
1169 trs_current
->next_rel
= trs
;
1180 if (trs_current != NULL) printf("LEFT ok!\n");
1181 else printf ("LEFT is empty\n");
1182 printf("Num of trans relations:%d\n", countTrans(trs));
1185 if (trs_current != NULL) printf("UP ok!\n");
1186 else printf ("UP is empty\n");
1187 printf("Num of trans relations:%d\n", countTrans(trs));
1190 if (trs_current != NULL) printf("RIGHT ok!\n");
1191 else printf ("RIGHT is empty\n");
1192 printf("Num of trans relations:%d\n", countTrans(trs));
1195 if (trs_current != NULL) printf("DOWN ok!\n");
1196 else printf ("DOWN is empty\n");
1197 printf("Num of trans relations:%d\n", countTrans(trs));
1206 int countTrans(trans_t *trs)
1209 while (trs != NULL){
1211 trs = trs->next_rel;
1216 rels
*encode_rel(sokoban_screen
*screen
)
1220 trans_t
*tl
= sylvan_false
;
1223 tl
= create_single_rel(screen
, LEFT
);
1226 trans_t
*tu
= create_single_rel(screen
, UP
);
1229 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1232 trans_t
*td
= create_single_rel(screen
, DOWN
);
1235 rls
= (rels
*)malloc(sizeof(rels
));
1244 int test_trans(state
*s
, trans_t
*t
)
1247 BDD next
= sylvan_false
;
1249 next
= sylvan_relnext(s
->bdd
, t
->bdd
, t
->varset
.varset
);
1250 if (next
== s
->bdd
) printf("Same\n");
1251 if (next
!= s
->bdd
&& next
!= sylvan_false
) printf("Different\n");
1252 if (next
== sylvan_false
) printf("False\n");