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");
213 int countTrans(trans_t
*trs
);
215 trans_t
*create_single_rel(sokoban_screen
*screen
, direction dir
)
218 trans_t
*trs
, *trs_current
;
219 bimap
*bm
= create_bimap_helper(screen
);
222 bddvar_xy_map
*bddxy
= NULL
;
255 for (unsigned int i
= 0; i
< HASH_COUNT(screen
); i
++){
256 bddxy
= getbdd(i
*6, bm
->t
);
259 if (check_space(x
, y
, dir
, 1, bm
) == 0){
261 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
262 BDDVAR relvars
[6] = {i
* 6, i
* 6 + 1, i
* 6 + 2, i
* 6 + 3, i
* 6 + 4, i
* 6 + 5};
263 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 6);
264 uint8_t rel_enc
[6] = {1, 1, 0, 0, 1, 1};
266 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
267 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
268 trs_current
->varset
.varset
= relvarset
;
269 trs_current
->varset
.size
= 6;
270 trs_current
->next_rel
= trs
;
273 //Targagent -> Targagent
274 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
275 relvarset
= sylvan_set_fromarray(relvars
, 6);
276 uint8_t rel_enc1
[6] = {1, 1, 1, 1, 0, 0};
277 memcpy(rel_enc
, rel_enc1
, 6*sizeof(uint8_t));
279 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
280 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
281 trs_current
->varset
.varset
= relvarset
;
282 trs_current
->varset
.size
= 6;
283 trs_current
->next_rel
= trs
;
287 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 0){
288 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
289 unsigned int deltai
= bddvar
->value
.var
[0];
290 //Agent Free -> Free Agent
291 //(1 0 0 0 1 1 0 1 0 0 1 1)
293 //(0 1 0 0 1 1 1 0 0 0 1 1)
294 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};
295 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
298 uint8_t rel_enc0
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
299 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
302 uint8_t rel_enc0
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
303 memcpy(rel_enc
, rel_enc0
, 12*sizeof(uint8_t));
305 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
306 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
307 trs_current
->varset
.varset
= relvarset
;
308 trs_current
->varset
.size
= 12;
309 trs_current
->next_rel
= trs
;
312 //Agent Target -> Free Targagent
313 //(1 0 0 0 1 1 0 1 1 1 1 0)
315 //(0 1 1 1 1 0 1 0 0 0 1 1)
316 relvarset
= sylvan_set_fromarray(relvars
, 12);
318 uint8_t rel_enc2
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
319 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
322 uint8_t rel_enc2
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
323 memcpy(rel_enc
, rel_enc2
, 12*sizeof(uint8_t));
325 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
326 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
327 trs_current
->varset
.varset
= relvarset
;
328 trs_current
->varset
.size
= 12;
329 trs_current
->next_rel
= trs
;
332 //Targagent Free -> Target Agent
333 //(1 0 1 1 0 1 0 1 0 0 1 1)
335 //(0 1 0 0 1 1 1 0 1 1 0 1)
336 relvarset
= sylvan_set_fromarray(relvars
, 12);
338 uint8_t rel_enc3
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
339 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
342 uint8_t rel_enc3
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
343 memcpy(rel_enc
, rel_enc3
, 12*sizeof(uint8_t));
345 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
346 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
347 trs_current
->varset
.varset
= relvarset
;
348 trs_current
->varset
.size
= 12;
349 trs_current
->next_rel
= trs
;
352 //Targagent Target -> Target Targagent
353 //(1 0 1 1 0 1 0 1 1 1 1 0)
355 //(0 1 1 1 1 0 1 0 1 1 0 1)
356 relvarset
= sylvan_set_fromarray(relvars
, 12);
358 uint8_t rel_enc4
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
359 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
362 uint8_t rel_enc4
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
363 memcpy(rel_enc
, rel_enc4
, 12*sizeof(uint8_t));
365 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
366 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
367 trs_current
->varset
.varset
= relvarset
;
368 trs_current
->varset
.size
= 12;
369 trs_current
->next_rel
= trs
;
372 //Agent Box -> Agent Box
373 //(1 1 0 0 1 1 0 0 1 1 0 0)
375 //(0 0 1 1 0 0 1 1 0 0 1 1)
376 relvarset
= sylvan_set_fromarray(relvars
, 12);
378 uint8_t rel_enc5
[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
379 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
382 uint8_t rel_enc5
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
383 memcpy(rel_enc
, rel_enc5
, 12*sizeof(uint8_t));
385 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
386 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
387 trs_current
->varset
.varset
= relvarset
;
388 trs_current
->varset
.size
= 12;
389 trs_current
->next_rel
= trs
;
392 //Agent Targbox -> Agent Targbox
393 //(1 1 0 0 1 1 1 1 0 0 0 0)
395 //(1 1 0 0 0 0 1 1 0 0 1 1)
396 relvarset
= sylvan_set_fromarray(relvars
, 12);
398 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
399 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
402 uint8_t rel_enc6
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
403 memcpy(rel_enc
, rel_enc6
, 12*sizeof(uint8_t));
405 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
406 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
407 trs_current
->varset
.varset
= relvarset
;
408 trs_current
->varset
.size
= 12;
409 trs_current
->next_rel
= trs
;
412 //Targagent Box -> Targagent Box
413 //(1 1 1 1 0 0 0 0 1 1 0 0)
415 //(0 0 1 1 0 0 1 1 1 1 0 0)
416 relvarset
= sylvan_set_fromarray(relvars
, 12);
418 uint8_t rel_enc7
[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
419 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
422 uint8_t rel_enc7
[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
423 memcpy(rel_enc
, rel_enc7
, 12*sizeof(uint8_t));
425 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
426 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
427 trs_current
->varset
.varset
= relvarset
;
428 trs_current
->varset
.size
= 12;
429 trs_current
->next_rel
= trs
;
432 //Targagent Targbox -> Targagent Targbox
433 //(1 1 1 1 0 0 1 1 0 0 0 0)
435 //(1 1 0 0 0 0 1 1 1 1 0 0)
436 relvarset
= sylvan_set_fromarray(relvars
, 12);
438 uint8_t rel_enc8
[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
439 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
442 uint8_t rel_enc8
[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
443 memcpy(rel_enc
, rel_enc8
, 12*sizeof(uint8_t));
445 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
446 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
447 trs_current
->varset
.varset
= relvarset
;
448 trs_current
->varset
.size
= 12;
449 trs_current
->next_rel
= trs
;
453 else if (check_space(x
, y
, dir
, 1, bm
) == 1 && check_space(x
, y
, dir
, 2, bm
) == 1){
454 xy_bddvar_map
*bddvar
= getxy(x
+ xdelta
, y
+ ydelta
, bm
->f
);
455 unsigned int deltai
= bddvar
->value
.var
[0];
456 bddvar
= getxy(x
+ xgamma
, y
+ ygamma
, bm
->f
);
457 unsigned int gammai
= bddvar
->value
.var
[0];
458 //Agent Free -> Free Agent
459 //(1 0 0 0 1 1 0 1 0 0 1 1)
461 //(0 1 0 0 1 1 1 0 0 0 1 1)
462 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};
463 BDDSET relvarset
= sylvan_set_fromarray(relvars
, 12);
466 uint8_t rel_enc_
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
467 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
470 uint8_t rel_enc_
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
471 memcpy(rel_enc
, rel_enc_
, 12*sizeof(uint8_t));
473 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
474 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
475 trs_current
->varset
.varset
= relvarset
;
476 trs_current
->varset
.size
= 12;
477 trs_current
->next_rel
= trs
;
480 //Agent Target -> Free Targagent
481 //(1 0 0 0 1 1 0 1 1 1 1 0)
483 //(0 1 1 1 1 0 1 0 0 0 1 1)
484 relvarset
= sylvan_set_fromarray(relvars
, 12);
486 uint8_t rel_enc9
[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
487 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
490 uint8_t rel_enc9
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
491 memcpy(rel_enc
, rel_enc9
, 12*sizeof(uint8_t));
493 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
494 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
495 trs_current
->varset
.varset
= relvarset
;
496 trs_current
->varset
.size
= 12;
497 trs_current
->next_rel
= trs
;
500 //Targagent Free -> Target Agent (LEFT || UP)
501 //(1 0 1 1 0 1 0 1 0 0 1 1)
503 //(0 1 0 0 1 1 1 0 1 1 0 1)
504 relvarset
= sylvan_set_fromarray(relvars
, 12);
506 uint8_t rel_enc10
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
507 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
510 uint8_t rel_enc10
[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
511 memcpy(rel_enc
, rel_enc10
, 12*sizeof(uint8_t));
513 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
514 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
515 trs_current
->varset
.varset
= relvarset
;
516 trs_current
->varset
.size
= 12;
517 trs_current
->next_rel
= trs
;
520 //Targagent Target -> Target Targagent (LEFT || UP)
521 //(1 0 1 1 0 1 0 1 1 1 1 0)
523 //(0 1 1 1 1 0 1 0 1 1 0 1)
524 relvarset
= sylvan_set_fromarray(relvars
, 12);
526 uint8_t rel_enc11
[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
527 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
530 uint8_t rel_enc11
[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
531 memcpy(rel_enc
, rel_enc11
, 12*sizeof(uint8_t));
533 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
534 trs_current
->bdd
= sylvan_cube(relvarset
, rel_enc
);
535 trs_current
->varset
.varset
= relvarset
;
536 trs_current
->varset
.size
= 12;
537 trs_current
->next_rel
= trs
;
540 //Agent Box Box -> Agent Box Box
541 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
542 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
544 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
546 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
548 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
550 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
552 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
553 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};
554 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
555 uint8_t rel_enc1
[18];
556 if ((i
< deltai
) < gammai
){
557 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
558 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
560 else if ((deltai
< gammai
) < i
){
561 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
562 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
564 else if ((gammai
< i
) < deltai
){
565 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
566 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
568 else if ((i
< gammai
) < deltai
){
569 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
570 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
572 else if ((deltai
< i
) < gammai
){
573 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
574 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
577 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
578 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
581 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
582 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
583 trs_current
->varset
.varset
= relvarset1
;
584 trs_current
->varset
.size
= 18;
585 trs_current
->next_rel
= trs
;
588 //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
589 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
591 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
593 //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
595 //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
597 //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
599 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
600 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
601 if ((i
< deltai
) < gammai
){
602 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
603 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
605 else if ((deltai
< gammai
) < i
){
606 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
607 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
609 else if ((gammai
< i
) < deltai
){
610 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
611 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
613 else if ((i
< gammai
) < deltai
){
614 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
615 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
617 else if ((deltai
< i
) < gammai
){
618 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
619 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
622 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
623 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
625 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
626 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
627 trs_current
->varset
.varset
= relvarset1
;
628 trs_current
->varset
.size
= 18;
629 trs_current
->next_rel
= trs
;
632 //Targagent Box Box -> Targagent Box Box
633 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
635 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
637 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
639 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
641 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
643 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
644 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
645 if ((i
< deltai
) < gammai
){
646 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
647 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
649 else if ((deltai
< gammai
) < i
){
650 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
651 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
653 else if ((gammai
< i
) < deltai
){
654 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
655 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
657 else if ((i
< gammai
) < deltai
){
658 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
659 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
661 else if ((deltai
< i
) < gammai
){
662 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
663 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
666 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
667 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
669 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
670 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
671 trs_current
->varset
.varset
= relvarset1
;
672 trs_current
->varset
.size
= 18;
673 trs_current
->next_rel
= trs
;
676 //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
677 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
679 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
681 //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
683 //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
685 //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
687 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
688 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
689 if ((i
< deltai
) < gammai
){
690 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
691 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
693 else if ((deltai
< gammai
) < i
){
694 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
695 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
697 else if ((gammai
< i
) < deltai
){
698 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
699 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
701 else if ((i
< gammai
) < deltai
){
702 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
703 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
705 else if ((deltai
< i
) < gammai
){
706 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
707 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
710 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
711 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
713 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
714 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
715 trs_current
->varset
.varset
= relvarset1
;
716 trs_current
->varset
.size
= 18;
717 trs_current
->next_rel
= trs
;
720 //Agent Box Free -> Free Agent Box
721 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
722 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
724 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
725 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1
727 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
728 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1
730 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
731 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1
733 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
734 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0
736 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
737 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1
738 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
739 if ((i
< deltai
) < gammai
){
740 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
741 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
743 else if ((deltai
< gammai
) < i
){
744 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
745 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
747 else if ((gammai
< i
) < deltai
){
748 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
749 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
751 else if ((i
< gammai
) < deltai
){
752 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
753 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
755 else if ((deltai
< i
) < gammai
){
756 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
757 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
760 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
761 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
763 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
764 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
765 trs_current
->varset
.varset
= relvarset1
;
766 trs_current
->varset
.size
= 18;
767 trs_current
->next_rel
= trs
;
770 //Agent Targbox Free -> Free Targagent Box
771 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
772 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0
774 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
775 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1
777 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
778 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0
780 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
781 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0
783 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
784 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0
786 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
787 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1
788 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
789 if ((i
< deltai
) < gammai
){
790 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
791 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
793 else if ((deltai
< gammai
) < i
){
794 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
795 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
797 else if ((gammai
< i
) < deltai
){
798 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
799 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
801 else if ((i
< gammai
) < deltai
){
802 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
803 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
805 else if ((deltai
< i
) < gammai
){
806 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
807 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
810 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
811 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
813 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
814 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
815 trs_current
->varset
.varset
= relvarset1
;
816 trs_current
->varset
.size
= 18;
817 trs_current
->next_rel
= trs
;
820 //Agent Box Target -> Free Agent Targbox
821 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
822 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0
824 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
825 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1
827 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
828 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1
830 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
831 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1
833 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
834 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0
836 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
837 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1
838 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
839 if ((i
< deltai
) < gammai
){
840 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
841 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
843 else if ((deltai
< gammai
) < i
){
844 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
845 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
847 else if ((gammai
< i
) < deltai
){
848 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
849 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
851 else if ((i
< gammai
) < deltai
){
852 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
853 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
855 else if ((deltai
< i
) < gammai
){
856 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
857 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
860 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
861 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
863 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
864 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
865 trs_current
->varset
.varset
= relvarset1
;
866 trs_current
->varset
.size
= 18;
867 trs_current
->next_rel
= trs
;
870 //Agent Targbox Target -> Free Targagent Targbox
871 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
873 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
875 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
877 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
879 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
881 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
882 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
883 if ((i
< deltai
) < gammai
){
884 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
885 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
887 else if ((deltai
< gammai
) < i
){
888 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
889 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
891 else if ((gammai
< i
) < deltai
){
892 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
893 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
895 else if ((i
< gammai
) < deltai
){
896 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
897 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
899 else if ((deltai
< i
) < gammai
){
900 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
901 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
904 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
905 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
907 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
908 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
909 trs_current
->varset
.varset
= relvarset1
;
910 trs_current
->varset
.size
= 18;
911 trs_current
->next_rel
= trs
;
914 //Targagent Box Free -> Target Agent Box
915 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
917 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
919 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
921 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
923 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
925 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
926 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
927 if ((i
< deltai
) < gammai
){
928 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
929 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
931 else if ((deltai
< gammai
) < i
){
932 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
933 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
935 else if ((gammai
< i
) < deltai
){
936 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
937 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
939 else if ((i
< gammai
) < deltai
){
940 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
941 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
943 else if ((deltai
< i
) < gammai
){
944 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
945 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
948 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
949 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
951 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
952 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
953 trs_current
->varset
.varset
= relvarset1
;
954 trs_current
->varset
.size
= 18;
955 trs_current
->next_rel
= trs
;
958 //Targagent Targbox Free -> Target Targagent Box
959 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
961 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
963 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
965 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
967 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
969 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
970 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
971 if ((i
< deltai
) < gammai
){
972 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
973 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
975 else if ((deltai
< gammai
) < i
){
976 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
977 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
979 else if ((gammai
< i
) < deltai
){
980 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
981 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
983 else if ((i
< gammai
) < deltai
){
984 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
985 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
987 else if ((deltai
< i
) < gammai
){
988 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
989 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
992 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
993 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
995 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
996 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
997 trs_current
->varset
.varset
= relvarset1
;
998 trs_current
->varset
.size
= 18;
999 trs_current
->next_rel
= trs
;
1002 //Targagent Box Target -> Target Agent Targbox
1003 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1005 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1007 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1009 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1011 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1013 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1014 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1015 if ((i
< deltai
) < gammai
){
1016 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1017 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1019 else if ((deltai
< gammai
) < i
){
1020 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1021 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1023 else if ((gammai
< i
) < deltai
){
1024 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1025 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1027 else if ((i
< gammai
) < deltai
){
1028 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1029 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1031 else if ((deltai
< i
) < gammai
){
1032 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1033 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1036 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1037 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1039 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1040 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1041 trs_current
->varset
.varset
= relvarset1
;
1042 trs_current
->varset
.size
= 18;
1043 trs_current
->next_rel
= trs
;
1046 //Targagent Targbox Target -> Target Targagent Targbox
1047 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1049 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1051 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1053 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1055 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1057 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1058 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1059 if ((i
< deltai
) < gammai
){
1060 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1061 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1063 else if ((deltai
< gammai
) < i
){
1064 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1065 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1067 else if ((gammai
< i
) < deltai
){
1068 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1069 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1071 else if ((i
< gammai
) < deltai
){
1072 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1073 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1075 else if ((deltai
< i
) < gammai
){
1076 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1077 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1080 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1081 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1083 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1084 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1085 trs_current
->varset
.varset
= relvarset1
;
1086 trs_current
->varset
.size
= 18;
1087 trs_current
->next_rel
= trs
;
1097 if (trs_current != NULL) printf("LEFT ok!\n");
1098 else printf ("LEFT is empty\n");
1099 printf("Num of trans relations:%d\n", countTrans(trs));
1102 if (trs_current != NULL) printf("UP ok!\n");
1103 else printf ("UP is empty\n");
1104 printf("Num of trans relations:%d\n", countTrans(trs));
1107 if (trs_current != NULL) printf("RIGHT ok!\n");
1108 else printf ("RIGHT is empty\n");
1109 printf("Num of trans relations:%d\n", countTrans(trs));
1112 if (trs_current != NULL) printf("DOWN ok!\n");
1113 else printf ("DOWN is empty\n");
1114 printf("Num of trans relations:%d\n", countTrans(trs));
1122 int countTrans(trans_t
*trs
)
1125 while (trs
!= NULL
){
1127 trs
= trs
->next_rel
;
1132 rels
*encode_rel(sokoban_screen
*screen
)
1136 trans_t
*tl
= sylvan_false
;
1139 tl
= create_single_rel(screen
, LEFT
);
1142 trans_t
*tu
= create_single_rel(screen
, UP
);
1145 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1148 trans_t
*td
= create_single_rel(screen
, DOWN
);
1151 rls
= (rels
*)malloc(sizeof(rels
));
1160 int test_trans(state
*s
, trans_t
*t
)
1164 BDD next
= sylvan_false
;
1166 next
= sylvan_relnext(s
->bdd
, t
->bdd
, t
->varset
.varset
);
1167 if (next
== s
->bdd
) printf("Same\n");
1168 if (next
!= s
->bdd
&& next
!= sylvan_false
) printf("Different\n");
1169 if (next
== sylvan_false
) printf("False\n");
1172 printf("Trans:%d\n", counter
);