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.
125 state
*encode_screen(sokoban_screen
*screen
)
129 BDDVAR vars
[HASH_COUNT(screen
) * 3];
130 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
134 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
136 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
138 state
*fullState
= NULL
;
139 fullState
= (state
*)malloc(sizeof(state
));
140 fullState
->vars
.varset
= varset
;
141 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
143 for(sokoban_screen
*r
=screen
; r
!= NULL
; r
= r
->hh
.next
){
146 st_enc
[tile_index
++] = 0;
147 st_enc
[tile_index
++] = 0;
148 st_enc
[tile_index
++] = 1;
151 st_enc
[tile_index
++] = 0;
152 st_enc
[tile_index
++] = 0;
153 st_enc
[tile_index
++] = 0;
156 st_enc
[tile_index
++] = 0;
157 st_enc
[tile_index
++] = 1;
158 st_enc
[tile_index
++] = 0;
161 st_enc
[tile_index
++] = 0;
162 st_enc
[tile_index
++] = 1;
163 st_enc
[tile_index
++] = 1;
166 st_enc
[tile_index
++] = 1;
167 st_enc
[tile_index
++] = 0;
168 st_enc
[tile_index
++] = 1;
170 case TARGAGENT
: //110
171 st_enc
[tile_index
++] = 1;
172 st_enc
[tile_index
++] = 1;
173 st_enc
[tile_index
++] = 0;
176 st_enc
[tile_index
++] = 1;
177 st_enc
[tile_index
++] = 0;
178 st_enc
[tile_index
++] = 0;
182 s
= sylvan_cube(varset
, st_enc
);
187 state
*encode_goal(sokoban_screen
*screen
){
190 BDDVAR vars
[HASH_COUNT(screen
) * 3];
191 for (uint8_t i
= 0; i
< HASH_COUNT(screen
) * 3; i
++){
195 uint8_t st_enc
[HASH_COUNT(screen
) * 3];
197 BDDSET varset
= sylvan_set_fromarray(vars
, HASH_COUNT(screen
) * 3);
199 state
*fullState
= NULL
;
200 fullState
= (state
*)malloc(sizeof(state
));
201 fullState
->vars
.varset
= varset
;
202 fullState
->vars
.size
= HASH_COUNT(screen
) * 3;
204 for(sokoban_screen
*r
=screen
; r
!= NULL
; r
=r
->hh
.next
){
206 case FREE
: //001 -> any
207 st_enc
[tile_index
++] = 2;
208 st_enc
[tile_index
++] = 2;
209 st_enc
[tile_index
++] = 2;
211 case WALL
: //000 -> stays the same
212 st_enc
[tile_index
++] = 0;
213 st_enc
[tile_index
++] = 0;
214 st_enc
[tile_index
++] = 0;
216 case BOX
: //010 -> any
217 st_enc
[tile_index
++] = 2;
218 st_enc
[tile_index
++] = 2;
219 st_enc
[tile_index
++] = 2;
221 case TARGET
: //011 -> targbox
222 st_enc
[tile_index
++] = 1;
223 st_enc
[tile_index
++] = 0;
224 st_enc
[tile_index
++] = 0;
226 case AGENT
: //101 -> any
227 st_enc
[tile_index
++] = 2;
228 st_enc
[tile_index
++] = 2;
229 st_enc
[tile_index
++] = 2;
231 case TARGAGENT
: //110 -> targbox
232 st_enc
[tile_index
++] = 1;
233 st_enc
[tile_index
++] = 0;
234 st_enc
[tile_index
++] = 0;
236 case TARGBOX
: //100 -> stays the same
237 st_enc
[tile_index
++] = 1;
238 st_enc
[tile_index
++] = 0;
239 st_enc
[tile_index
++] = 0;
243 s
= sylvan_cube(varset
, st_enc
);
248 trans_t
*create_single_rel(sokoban_screen
*screen
, direction dir
)
251 trans_t
*trs
, *trs_current
;
252 bimap
*bm
= create_bimap_helper(screen
);
255 bddvar_xy_map
*bddxy
= NULL
;
288 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
289 bddxy
= getbdd(i
*6, bm
->t
);
292 if (check_space(x
, y
, dir
, 1, bm
) == 0){
294 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
295 BDDVAR relvars
[6] = {i
* 6, i
* 6 + 1, i
* 6 + 2, i
* 6 + 3, i
* 6 + 4, i
* 6 + 5};
296 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
297 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
298 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
299 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
300 trs_current
->varset
.varset
= relvarset
;
301 trs_current
->varset
.size
= 6;
302 trs_current
->next_rel
= trs
;
305 //Targagent -> Targagent
306 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
307 relvarset
= sylvan_set_fromarray(relvars
, 6);
308 uint8_t rel_enc1
[6] = {1, 1, 1, 1, 0, 0};
309 memcpy(rel_enc
, rel_enc1
, 6*sizeof(uint8_t));
311 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
312 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
313 trs_current
->varset
.varset
= relvarset
;
314 trs_current
->varset
.size
= 6;
315 trs_current
->next_rel
= trs
;
318 } else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
319 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
320 unsigned int deltai
= bddvar
->value
.var
[0];
321 //Agent Free -> Free Agent
322 //(1 0 0 0 1 1 0 1 0 0 1 1)
324 //(0 1 0 0 1 1 1 0 0 0 1 1)
325 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};
326 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
329 uint8_t rel_enc0
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
330 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
333 uint8_t rel_enc0
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
334 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
336 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
337 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
338 trs_current
->varset
.varset
= relvarset
;
339 trs_current
->varset
.size
= 12;
340 trs_current
->next_rel
= trs
;
343 //Agent Target -> Free Targagent
344 //(1 0 0 0 1 1 0 1 1 1 1 0)
346 //(0 1 1 1 1 0 1 0 0 0 1 1)
347 relvarset
= sylvan_set_fromarray(relvars
, 12);
349 uint8_t rel_enc2
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
350 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
353 uint8_t rel_enc2
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
354 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
356 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
357 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
358 trs_current
->varset
.varset
= relvarset
;
359 trs_current
->varset
.size
= 12;
360 trs_current
->next_rel
= trs
;
363 //Targagent Free -> Target Agent
364 //(1 0 1 1 0 1 0 1 0 0 1 1)
366 //(0 1 0 0 1 1 1 0 1 1 0 1)
367 relvarset
= sylvan_set_fromarray(relvars
, 12);
369 uint8_t rel_enc3
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
370 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
373 uint8_t rel_enc3
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
374 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
376 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
377 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
378 trs_current
->varset
.varset
= relvarset
;
379 trs_current
->varset
.size
= 12;
380 trs_current
->next_rel
= trs
;
383 //Targagent Target -> Target Targagent
384 //(1 0 1 1 0 1 0 1 1 1 1 0)
386 //(0 1 1 1 1 0 1 0 1 1 0 1)
387 relvarset
= sylvan_set_fromarray(relvars
, 12);
389 uint8_t rel_enc4
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
390 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
393 uint8_t rel_enc4
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
394 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
396 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
397 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
398 trs_current
->varset
.varset
= relvarset
;
399 trs_current
->varset
.size
= 12;
400 trs_current
->next_rel
= trs
;
403 //Agent Box -> Agent Box
404 //(1 1 0 0 1 1 0 0 1 1 0 0)
406 //(0 0 1 1 0 0 1 1 0 0 1 1)
407 relvarset
= sylvan_set_fromarray(relvars
, 12);
409 uint8_t rel_enc5
[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
410 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
413 uint8_t rel_enc5
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
414 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
416 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
417 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
418 trs_current
->varset
.varset
= relvarset
;
419 trs_current
->varset
.size
= 12;
420 trs_current
->next_rel
= trs
;
423 //Agent Targbox -> Agent Targbox
424 //(1 1 0 0 1 1 1 1 0 0 0 0)
426 //(1 1 0 0 0 0 1 1 0 0 1 1)
427 relvarset
= sylvan_set_fromarray(relvars
, 12);
429 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
430 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
433 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
434 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
436 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
437 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
438 trs_current
->varset
.varset
= relvarset
;
439 trs_current
->varset
.size
= 12;
440 trs_current
->next_rel
= trs
;
443 //Targagent Box -> Targagent Box
444 //(1 1 1 1 0 0 0 0 1 1 0 0)
446 //(0 0 1 1 0 0 1 1 1 1 0 0)
447 relvarset
= sylvan_set_fromarray(relvars
, 12);
449 uint8_t rel_enc7
[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
450 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
453 uint8_t rel_enc7
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
454 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
456 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
457 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
458 trs_current
->varset
.varset
= relvarset
;
459 trs_current
->varset
.size
= 12;
460 trs_current
->next_rel
= trs
;
463 //Targagent Targbox -> Targagent Targbox
464 //(1 1 1 1 0 0 1 1 0 0 0 0)
466 //(1 1 0 0 0 0 1 1 1 1 0 0)
467 relvarset
= sylvan_set_fromarray(relvars
, 12);
469 uint8_t rel_enc8
[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
470 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
473 uint8_t rel_enc8
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
474 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
476 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
477 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
478 trs_current
->varset
.varset
= relvarset
;
479 trs_current
->varset
.size
= 12;
480 trs_current
->next_rel
= trs
;
482 } else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
483 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
484 unsigned int deltai
= bddvar
->value
.var
[0];
485 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
486 unsigned int gammai
= bddvar
->value
.var
[0];
487 //Agent Free -> Free Agent
488 //(1 0 0 0 1 1 0 1 0 0 1 1)
490 //(0 1 0 0 1 1 1 0 0 0 1 1)
491 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};
492 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
495 uint8_t rel_enc_
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
496 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
499 uint8_t rel_enc_
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
500 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
502 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
503 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
504 trs_current
->varset
.varset
= relvarset
;
505 trs_current
->varset
.size
= 12;
506 trs_current
->next_rel
= trs
;
509 //Agent Target -> Free Targagent
510 //(1 0 0 0 1 1 0 1 1 1 1 0)
512 //(0 1 1 1 1 0 1 0 0 0 1 1)
513 relvarset
= sylvan_set_fromarray(relvars
, 12);
515 uint8_t rel_enc9
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
516 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
519 uint8_t rel_enc9
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
520 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
522 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
523 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
524 trs_current
->varset
.varset
= relvarset
;
525 trs_current
->varset
.size
= 12;
526 trs_current
->next_rel
= trs
;
529 //Targagent Free -> Target Agent (LEFT || UP)
530 //(1 0 1 1 0 1 0 1 0 0 1 1)
532 //(0 1 0 0 1 1 1 0 1 1 0 1)
533 relvarset
= sylvan_set_fromarray(relvars
, 12);
535 uint8_t rel_enc10
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
536 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
539 uint8_t rel_enc10
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
540 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
542 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
543 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
544 trs_current
->varset
.varset
= relvarset
;
545 trs_current
->varset
.size
= 12;
546 trs_current
->next_rel
= trs
;
549 //Targagent Target -> Target Targagent (LEFT || UP)
550 //(1 0 1 1 0 1 0 1 1 1 1 0)
552 //(0 1 1 1 1 0 1 0 1 1 0 1)
553 relvarset
= sylvan_set_fromarray(relvars
, 12);
555 uint8_t rel_enc11
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
556 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
559 uint8_t rel_enc11
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
560 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
562 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
563 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
564 trs_current
->varset
.varset
= relvarset
;
565 trs_current
->varset
.size
= 12;
566 trs_current
->next_rel
= trs
;
569 //Agent Box Box -> Agent Box Box
570 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
572 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
574 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
576 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
578 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
580 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
581 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};
582 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
583 uint8_t rel_enc1
[18];
584 if (i
*6 < deltai
&& deltai
< gammai
){
585 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
586 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
588 else if (deltai
< gammai
&& gammai
< i
*6){
589 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
590 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
592 else if (gammai
< i
*6 && i
*6 < deltai
){
593 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
594 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
596 else if (i
*6 < gammai
&& gammai
< deltai
){
597 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
598 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
600 else if (deltai
< i
*6 && i
*6 < gammai
){
601 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
602 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
605 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
606 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
609 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
610 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
611 trs_current
->varset
.varset
= relvarset1
;
612 trs_current
->varset
.size
= 18;
613 trs_current
->next_rel
= trs
;
616 //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
617 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
619 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
621 //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
623 //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
625 //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
627 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
628 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
629 if (i
*6 < deltai
&& deltai
< gammai
){
630 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
631 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
633 else if (deltai
< gammai
&& gammai
< i
*6){
634 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
635 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
637 else if (gammai
< i
*6 && i
*6 < deltai
){
638 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
639 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
641 else if (i
*6 < gammai
&& gammai
< deltai
){
642 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
643 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
645 else if (deltai
< i
*6 && i
*6 < gammai
){
646 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
647 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
650 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
651 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
653 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
654 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
655 trs_current
->varset
.varset
= relvarset1
;
656 trs_current
->varset
.size
= 18;
657 trs_current
->next_rel
= trs
;
660 //Targagent Box Box -> Targagent Box Box
661 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
663 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
665 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
667 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
669 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
671 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
672 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
673 if (i
*6 < deltai
&& deltai
< gammai
){
674 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
675 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
677 else if (deltai
< gammai
&& gammai
< i
*6){
678 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
679 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
681 else if (gammai
< i
*6 && i
*6 < deltai
){
682 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
683 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
685 else if (i
*6 < gammai
&& gammai
< deltai
){
686 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
687 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
689 else if (deltai
< i
*6 && i
*6 < gammai
){
690 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
691 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
694 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
695 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
697 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
698 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
699 trs_current
->varset
.varset
= relvarset1
;
700 trs_current
->varset
.size
= 18;
701 trs_current
->next_rel
= trs
;
704 //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
705 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
707 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
709 //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
711 //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
713 //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
715 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
716 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
717 if (i
*6 < deltai
&& deltai
< gammai
){
718 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
719 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
721 else if (deltai
< gammai
&& gammai
< i
*6){
722 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
723 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
725 else if (gammai
< i
*6 && i
*6 < deltai
){
726 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
727 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
729 else if (i
*6 < gammai
&& gammai
< deltai
){
730 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
731 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
733 else if (deltai
< i
*6 && i
*6 < gammai
){
734 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
735 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
738 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
739 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
741 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
742 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
743 trs_current
->varset
.varset
= relvarset1
;
744 trs_current
->varset
.size
= 18;
745 trs_current
->next_rel
= trs
;
748 //Agent Box Free -> Free Agent Box
749 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
751 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
753 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
755 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
757 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
759 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
760 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
761 if (i
*6 < deltai
&& deltai
< gammai
){
762 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
763 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
766 else if (deltai
< gammai
&& gammai
< i
*6){
767 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
768 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
771 else if (gammai
< i
*6 && i
*6 < deltai
){
772 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
773 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
776 else if (i
*6 < gammai
&& gammai
< deltai
){
777 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
778 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
780 else if (deltai
< i
*6 && i
*6 < gammai
){
781 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
782 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
785 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
786 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
789 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
791 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
792 trs_current
->varset
.varset
= relvarset1
;
793 trs_current
->varset
.size
= 18;
794 trs_current
->next_rel
= trs
;
797 //Agent Targbox Free -> Free Targagent Box
798 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
800 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
802 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
804 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
806 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
808 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
809 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
810 if (i
*6 < deltai
&& deltai
< gammai
){
811 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
812 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
814 else if (deltai
< gammai
&& gammai
< i
*6){
815 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
816 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
818 else if (gammai
< i
*6 && i
*6 < deltai
){
819 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
820 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
822 else if (i
*6 < gammai
&& gammai
< deltai
){
823 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
824 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
826 else if (deltai
< i
*6 && i
*6 < gammai
){
827 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
828 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
831 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
832 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
834 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
835 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
836 trs_current
->varset
.varset
= relvarset1
;
837 trs_current
->varset
.size
= 18;
838 trs_current
->next_rel
= trs
;
841 //Agent Box Target -> Free Agent Targbox
842 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
844 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
846 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
848 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
850 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
852 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
853 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
854 if (i
*6 < deltai
&& deltai
< gammai
){
855 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
856 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
858 else if (deltai
< gammai
&& gammai
< i
*6){
859 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
860 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
862 else if (gammai
< i
*6 && i
*6 < deltai
){
863 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
864 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
866 else if (i
*6 < gammai
&& gammai
< deltai
){
867 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
868 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
870 else if (deltai
< i
*6 && i
*6 < gammai
){
871 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
872 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
875 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
876 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
878 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
879 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
880 trs_current
->varset
.varset
= relvarset1
;
881 trs_current
->varset
.size
= 18;
882 trs_current
->next_rel
= trs
;
885 //Agent Targbox Target -> Free Targagent Targbox
886 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
888 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
890 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
892 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
894 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
896 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
897 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
898 if (i
*6 < deltai
&& deltai
< gammai
){
899 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
900 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
902 else if (deltai
< gammai
&& gammai
< i
*6){
903 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
904 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
906 else if (gammai
< i
*6 && i
*6 < deltai
){
907 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
908 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
910 else if (i
*6 < gammai
&& gammai
< deltai
){
911 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
912 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
914 else if (deltai
< i
*6 && i
*6 < gammai
){
915 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
916 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
919 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
920 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
922 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
923 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
924 trs_current
->varset
.varset
= relvarset1
;
925 trs_current
->varset
.size
= 18;
926 trs_current
->next_rel
= trs
;
929 //Targagent Box Free -> Target Agent Box
930 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
932 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
934 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
936 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
938 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
940 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
941 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
942 if (i
*6 < deltai
&& deltai
< gammai
){
943 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
944 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
946 else if (deltai
< gammai
&& gammai
< i
*6){
947 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
948 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
950 else if (gammai
< i
*6 && i
*6 < deltai
){
951 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
952 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
954 else if (i
*6 < gammai
&& gammai
< deltai
){
955 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
956 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
958 else if (deltai
< i
*6 && i
*6 < gammai
){
959 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
960 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
963 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
964 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
966 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
967 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
968 trs_current
->varset
.varset
= relvarset1
;
969 trs_current
->varset
.size
= 18;
970 trs_current
->next_rel
= trs
;
973 //Targagent Targbox Free -> Target Targagent Box
974 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
976 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
978 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
980 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
982 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
984 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
985 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
986 if (i
*6 < deltai
&& deltai
< gammai
){
987 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
988 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
990 else if (deltai
< gammai
&& gammai
< i
*6){
991 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
992 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
994 else if (gammai
< i
*6 && i
*6 < deltai
){
995 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
996 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
998 else if (i
*6 < gammai
&& gammai
< deltai
){
999 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1000 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1002 else if (deltai
< i
*6 && i
*6 < gammai
){
1003 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0};
1004 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1007 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1008 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1010 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1011 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1012 trs_current
->varset
.varset
= relvarset1
;
1013 trs_current
->varset
.size
= 18;
1014 trs_current
->next_rel
= trs
;
1017 //Targagent Box Target -> Target Agent Targbox
1018 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1020 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1022 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1024 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1026 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1028 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1029 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1030 if (i
*6 < deltai
&& deltai
< gammai
){
1031 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1032 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1034 else if (deltai
< gammai
&& gammai
< i
*6){
1035 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1036 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1038 else if (gammai
< i
*6 && i
*6 < deltai
){
1039 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1040 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1042 else if (i
*6 < gammai
&& gammai
< deltai
){
1043 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1044 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1046 else if (deltai
< i
*6 && i
*6 < gammai
){
1047 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1048 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1051 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1052 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1054 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1055 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1056 trs_current
->varset
.varset
= relvarset1
;
1057 trs_current
->varset
.size
= 18;
1058 trs_current
->next_rel
= trs
;
1061 //Targagent Targbox Target -> Target Targagent Targbox
1062 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1064 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1066 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1068 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1070 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1072 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1073 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1074 if (i
*6 < deltai
&& deltai
< gammai
){
1075 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1076 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1078 else if (deltai
< gammai
&& gammai
< i
*6){
1079 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1080 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1082 else if (gammai
< i
*6 && i
*6 < deltai
){
1083 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1084 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1086 else if (i
*6 < gammai
&& gammai
< deltai
){
1087 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1088 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1090 else if (deltai
< i
*6 && i
*6 < gammai
){
1091 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1092 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1095 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1096 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1098 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1099 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1100 trs_current
->varset
.varset
= relvarset1
;
1101 trs_current
->varset
.size
= 18;
1102 trs_current
->next_rel
= trs
;
1111 rels
*encode_rel(sokoban_screen
*screen
)
1115 trans_t
*tl
= sylvan_false
;
1118 tl
= create_single_rel(screen
, LEFT
);
1119 trans_t
*tu
= create_single_rel(screen
, UP
);
1120 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1121 trans_t
*td
= create_single_rel(screen
, DOWN
);
1124 rls
= (rels
*)malloc(sizeof(rels
));