f9dd7e5c7abe754af61a6b1dc2795bdb86c2b767
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)
872 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0
874 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
876 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
878 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
880 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
882 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
883 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
884 if ((i
< deltai
) < gammai
){
885 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
886 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
888 else if ((deltai
< gammai
) < i
){
889 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
890 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
892 else if ((gammai
< i
) < deltai
){
893 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
894 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
896 else if ((i
< gammai
) < deltai
){
897 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
898 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
900 else if ((deltai
< i
) < gammai
){
901 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
902 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
905 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
906 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
908 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
909 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
910 trs_current
->varset
.varset
= relvarset1
;
911 trs_current
->varset
.size
= 18;
912 trs_current
->next_rel
= trs
;
915 //Targagent Box Free -> Target Agent Box
916 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
917 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0
919 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
920 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1
922 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
923 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1
925 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
926 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1
928 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
929 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0
931 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
932 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1
933 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
934 if ((i
< deltai
) < gammai
){
935 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
936 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
938 else if ((deltai
< gammai
) < i
){
939 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
940 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
942 else if ((gammai
< i
) < deltai
){
943 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
944 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
946 else if ((i
< gammai
) < deltai
){
947 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
948 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
950 else if ((deltai
< i
) < gammai
){
951 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
952 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
955 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
956 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
958 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
959 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
960 trs_current
->varset
.varset
= relvarset1
;
961 trs_current
->varset
.size
= 18;
962 trs_current
->next_rel
= trs
;
965 //Targagent Targbox Free -> Target Targagent Box
966 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
967 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0
969 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
970 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1
972 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
973 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0
975 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
976 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0
978 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
979 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0
981 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
982 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1
983 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
984 if ((i
< deltai
) < gammai
){
985 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
986 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
988 else if ((deltai
< gammai
) < i
){
989 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
990 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
992 else if ((gammai
< i
) < deltai
){
993 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
994 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
996 else if ((i
< gammai
) < deltai
){
997 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
998 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1000 else if ((deltai
< i
) < gammai
){
1001 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, ,1 ,1, 0};
1002 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1005 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1006 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1008 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1009 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1010 trs_current
->varset
.varset
= relvarset1
;
1011 trs_current
->varset
.size
= 18;
1012 trs_current
->next_rel
= trs
;
1015 //Targagent Box Target -> Target Agent Targbox
1016 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1018 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1020 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1022 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1024 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1026 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1027 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1028 if ((i
< deltai
) < gammai
){
1029 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1030 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1032 else if ((deltai
< gammai
) < i
){
1033 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1034 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1036 else if ((gammai
< i
) < deltai
){
1037 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1038 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1040 else if ((i
< gammai
) < deltai
){
1041 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1042 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1044 else if ((deltai
< i
) < gammai
){
1045 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1046 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1049 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1050 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1052 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1053 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1054 trs_current
->varset
.varset
= relvarset1
;
1055 trs_current
->varset
.size
= 18;
1056 trs_current
->next_rel
= trs
;
1059 //Targagent Targbox Target -> Target Targagent Targbox
1060 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1062 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1064 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1066 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1068 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1070 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1071 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1072 if ((i
< deltai
) < gammai
){
1073 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1074 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1076 else if ((deltai
< gammai
) < i
){
1077 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1078 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1080 else if ((gammai
< i
) < deltai
){
1081 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1082 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1084 else if ((i
< gammai
) < deltai
){
1085 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1086 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1088 else if ((deltai
< i
) < gammai
){
1089 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1090 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1093 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1094 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1096 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1097 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1098 trs_current
->varset
.varset
= relvarset1
;
1099 trs_current
->varset
.size
= 18;
1100 trs_current
->next_rel
= trs
;
1110 if (trs_current != NULL) printf("LEFT ok!\n");
1111 else printf ("LEFT is empty\n");
1112 printf("Num of trans relations:%d\n", countTrans(trs));
1115 if (trs_current != NULL) printf("UP ok!\n");
1116 else printf ("UP is empty\n");
1117 printf("Num of trans relations:%d\n", countTrans(trs));
1120 if (trs_current != NULL) printf("RIGHT ok!\n");
1121 else printf ("RIGHT is empty\n");
1122 printf("Num of trans relations:%d\n", countTrans(trs));
1125 if (trs_current != NULL) printf("DOWN ok!\n");
1126 else printf ("DOWN is empty\n");
1127 printf("Num of trans relations:%d\n", countTrans(trs));
1135 int countTrans(trans_t
*trs
)
1138 while (trs
!= NULL
){
1140 trs
= trs
->next_rel
;
1145 rels
*encode_rel(sokoban_screen
*screen
)
1149 trans_t
*tl
= sylvan_false
;
1152 tl
= create_single_rel(screen
, LEFT
);
1155 trans_t
*tu
= create_single_rel(screen
, UP
);
1158 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1161 trans_t
*td
= create_single_rel(screen
, DOWN
);
1164 rls
= (rels
*)malloc(sizeof(rels
));
1173 int test_trans(state
*s
, trans_t
*t
)
1177 BDD next
= sylvan_false
;
1179 next
= sylvan_relnext(s
->bdd
, t
->bdd
, t
->varset
.varset
);
1180 if (next
== s
->bdd
) printf("Same\n");
1181 if (next
!= s
->bdd
&& next
!= sylvan_false
) printf("Different\n");
1182 if (next
== sylvan_false
) printf("False\n");
1185 printf("Trans:%d\n", counter
);