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)
543 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
545 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
547 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
549 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
551 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
552 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};
553 BDD relvarset1
= sylvan_set_fromarray(relvars1
, 18);
554 uint8_t rel_enc1
[18];
555 if ((i
< deltai
) < gammai
){
556 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
557 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
559 else if ((deltai
< gammai
) < i
){
560 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
561 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
563 else if ((gammai
< i
) < deltai
){
564 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
565 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
567 else if ((i
< gammai
) < deltai
){
568 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
569 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
571 else if ((deltai
< i
) < gammai
){
572 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
573 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
576 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
577 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
580 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
581 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
582 trs_current
->varset
.varset
= relvarset1
;
583 trs_current
->varset
.size
= 18;
584 trs_current
->next_rel
= trs
;
587 //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
588 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0)
590 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1)
592 //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
594 //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0)
596 //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0)
598 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
599 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
600 if ((i
< deltai
) < gammai
){
601 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
602 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
604 else if ((deltai
< gammai
) < i
){
605 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
606 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
608 else if ((gammai
< i
) < deltai
){
609 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
610 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
612 else if ((i
< gammai
) < deltai
){
613 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
614 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
616 else if ((deltai
< i
) < gammai
){
617 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
618 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
621 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
622 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
624 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
625 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
626 trs_current
->varset
.varset
= relvarset1
;
627 trs_current
->varset
.size
= 18;
628 trs_current
->next_rel
= trs
;
631 //Targagent Box Box -> Targagent Box Box
632 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
634 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
636 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
638 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
640 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
642 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
643 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
644 if ((i
< deltai
) < gammai
){
645 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
646 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
648 else if ((deltai
< gammai
) < i
){
649 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
650 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
652 else if ((gammai
< i
) < deltai
){
653 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
654 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
656 else if ((i
< gammai
) < deltai
){
657 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
658 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
660 else if ((deltai
< i
) < gammai
){
661 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
662 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
665 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
666 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
668 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
669 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
670 trs_current
->varset
.varset
= relvarset1
;
671 trs_current
->varset
.size
= 18;
672 trs_current
->next_rel
= trs
;
675 //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
676 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
678 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
680 //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
682 //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
684 //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
686 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
687 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
688 if ((i
< deltai
) < gammai
){
689 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
690 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
692 else if ((deltai
< gammai
) < i
){
693 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
694 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
696 else if ((gammai
< i
) < deltai
){
697 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
698 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
700 else if ((i
< gammai
) < deltai
){
701 uint8_t rel_enc__
[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
702 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
704 else if ((deltai
< i
) < gammai
){
705 uint8_t rel_enc__
[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
706 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
709 uint8_t rel_enc__
[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
710 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
712 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
713 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
714 trs_current
->varset
.varset
= relvarset1
;
715 trs_current
->varset
.size
= 18;
716 trs_current
->next_rel
= trs
;
719 //Agent Box Free -> Free Agent Box
720 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
722 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
724 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
726 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
728 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
730 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
731 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
732 if ((i
< deltai
) < gammai
){
733 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
734 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
736 else if ((deltai
< gammai
) < i
){
737 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
738 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
740 else if ((gammai
< i
) < deltai
){
741 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
742 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
744 else if ((i
< gammai
) < deltai
){
745 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
746 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
748 else if ((deltai
< i
) < gammai
){
749 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
750 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
753 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
754 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
756 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
757 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
758 trs_current
->varset
.varset
= relvarset1
;
759 trs_current
->varset
.size
= 18;
760 trs_current
->next_rel
= trs
;
763 //Agent Targbox Free -> Free Targagent Box
764 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
766 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
768 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
770 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
772 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
774 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
775 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
776 if ((i
< deltai
) < gammai
){
777 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
778 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
780 else if ((deltai
< gammai
) < i
){
781 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
782 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
784 else if ((gammai
< i
) < deltai
){
785 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
786 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
788 else if ((i
< gammai
) < deltai
){
789 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
790 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
792 else if ((deltai
< i
) < gammai
){
793 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
794 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
797 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
798 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
800 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
801 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
802 trs_current
->varset
.varset
= relvarset1
;
803 trs_current
->varset
.size
= 18;
804 trs_current
->next_rel
= trs
;
807 //Agent Box Target -> Free Agent Targbox
808 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
810 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
812 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
814 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
816 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
818 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
819 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
820 if ((i
< deltai
) < gammai
){
821 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
822 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
824 else if ((deltai
< gammai
) < i
){
825 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
826 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
828 else if ((gammai
< i
) < deltai
){
829 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
830 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
832 else if ((i
< gammai
) < deltai
){
833 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
834 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
836 else if ((deltai
< i
) < gammai
){
837 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
838 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
841 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
842 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
844 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
845 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
846 trs_current
->varset
.varset
= relvarset1
;
847 trs_current
->varset
.size
= 18;
848 trs_current
->next_rel
= trs
;
851 //Agent Targbox Target -> Free Targagent Targbox
852 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
854 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
856 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
858 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
860 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
862 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
863 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
864 if ((i
< deltai
) < gammai
){
865 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
866 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
868 else if ((deltai
< gammai
) < i
){
869 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
870 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
872 else if ((gammai
< i
) < deltai
){
873 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
874 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
876 else if ((i
< gammai
) < deltai
){
877 uint8_t rel_enc__
[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
878 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
880 else if ((deltai
< i
) < gammai
){
881 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
882 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
885 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
886 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
888 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
889 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
890 trs_current
->varset
.varset
= relvarset1
;
891 trs_current
->varset
.size
= 18;
892 trs_current
->next_rel
= trs
;
895 //Targagent Box Free -> Target Agent Box
896 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
898 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
900 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
902 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
904 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
906 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
907 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
908 if ((i
< deltai
) < gammai
){
909 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
910 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
912 else if ((deltai
< gammai
) < i
){
913 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
914 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
916 else if ((gammai
< i
) < deltai
){
917 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
918 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
920 else if ((i
< gammai
) < deltai
){
921 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
922 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
924 else if ((deltai
< i
) < gammai
){
925 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
926 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
929 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
930 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
932 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
933 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
934 trs_current
->varset
.varset
= relvarset1
;
935 trs_current
->varset
.size
= 18;
936 trs_current
->next_rel
= trs
;
939 //Targagent Targbox Free -> Target Targagent Box
940 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
942 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
944 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
946 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
948 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
950 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
951 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
952 if ((i
< deltai
) < gammai
){
953 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
954 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
956 else if ((deltai
< gammai
) < i
){
957 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
958 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
960 else if ((gammai
< i
) < deltai
){
961 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
962 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
964 else if ((i
< gammai
) < deltai
){
965 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
966 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
968 else if ((deltai
< i
) < gammai
){
969 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
970 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
973 uint8_t rel_enc__
[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
974 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
976 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
977 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
978 trs_current
->varset
.varset
= relvarset1
;
979 trs_current
->varset
.size
= 18;
980 trs_current
->next_rel
= trs
;
983 //Targagent Box Target -> Target Agent Targbox
984 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
986 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
988 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
990 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
992 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
994 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
995 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
996 if ((i
< deltai
) < gammai
){
997 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
998 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1000 else if ((deltai
< gammai
) < i
){
1001 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1002 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1004 else if ((gammai
< i
) < deltai
){
1005 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1006 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1008 else if ((i
< gammai
) < deltai
){
1009 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1010 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1012 else if ((deltai
< i
) < gammai
){
1013 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1014 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1017 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1018 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1020 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1021 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1022 trs_current
->varset
.varset
= relvarset1
;
1023 trs_current
->varset
.size
= 18;
1024 trs_current
->next_rel
= trs
;
1027 //Targagent Targbox Target -> Target Targagent Targbox
1028 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1030 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1032 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1034 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1036 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1038 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1039 relvarset1
= sylvan_set_fromarray(relvars1
, 18);
1040 if ((i
< deltai
) < gammai
){
1041 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1042 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1044 else if ((deltai
< gammai
) < i
){
1045 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1046 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1048 else if ((gammai
< i
) < deltai
){
1049 uint8_t rel_enc__
[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1050 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1052 else if ((i
< gammai
) < deltai
){
1053 uint8_t rel_enc__
[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1054 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1056 else if ((deltai
< i
) < gammai
){
1057 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1058 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1061 uint8_t rel_enc__
[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1062 memcpy(rel_enc1
, rel_enc__
, 18*sizeof(uint8_t));
1064 trs_current
= (trans_t
*)malloc(sizeof(trans_t
));
1065 trs_current
->bdd
= sylvan_cube(relvarset1
, rel_enc1
);
1066 trs_current
->varset
.varset
= relvarset1
;
1067 trs_current
->varset
.size
= 18;
1068 trs_current
->next_rel
= trs
;
1078 if (trs_current != NULL) printf("LEFT ok!\n");
1079 else printf ("LEFT is empty\n");
1080 printf("Num of trans relations:%d\n", countTrans(trs));
1083 if (trs_current != NULL) printf("UP ok!\n");
1084 else printf ("UP is empty\n");
1085 printf("Num of trans relations:%d\n", countTrans(trs));
1088 if (trs_current != NULL) printf("RIGHT ok!\n");
1089 else printf ("RIGHT is empty\n");
1090 printf("Num of trans relations:%d\n", countTrans(trs));
1093 if (trs_current != NULL) printf("DOWN ok!\n");
1094 else printf ("DOWN is empty\n");
1095 printf("Num of trans relations:%d\n", countTrans(trs));
1103 int countTrans(trans_t
*trs
)
1106 while (trs
!= NULL
){
1108 trs
= trs
->next_rel
;
1113 rels
*encode_rel(sokoban_screen
*screen
)
1117 trans_t
*tl
= sylvan_false
;
1120 tl
= create_single_rel(screen
, LEFT
);
1123 trans_t
*tu
= create_single_rel(screen
, UP
);
1126 trans_t
*tr
= create_single_rel(screen
, RIGHT
);
1129 trans_t
*td
= create_single_rel(screen
, DOWN
);
1132 rls
= (rels
*)malloc(sizeof(rels
));
1141 int test_trans(state
*s
, trans_t
*t
)
1145 BDD next
= sylvan_false
;
1147 next
= sylvan_relnext(s
->bdd
, t
->bdd
, t
->varset
.varset
);
1148 if (next
== s
->bdd
) printf("Same\n");
1149 if (next
!= s
->bdd
&& next
!= sylvan_false
) printf("Different\n");
1150 if (next
== sylvan_false
) printf("False\n");
1153 printf("Trans:%d\n", counter
);