repositories / mc1516pa.git / blob
? search:


9f179c659448499b7e8be162066858b18d3c0c80
[mc1516pa.git] / modelchecker / coord.c
1 #include <argp.h>
2 #include <stdio.h>
3 #include <stdlib.h>
4 #include <sylvan.h>
5 #include <lace.h>
6
7 #include "coord.h"
8 #include "sokoban.h"
9 #include "deque.h"
10
11
12 typedef struct {
13 int x;
14 int y;
15 } xy;
16
17 typedef struct {
18 int var[3];
19 } bddvar;
20
21 typedef struct {
22 xy key;
23 bddvar value;
24 UT_hash_handle hh;
25 } xy_bddvar_map;
26
27 typedef struct {
28 int key;
29 xy value;
30 UT_hash_handle hh;
31 } bddvar_xy_map;
32
33 typedef struct {
34 xy_bddvar_map *f;
35 bddvar_xy_map *t;
36 } bimap;
37
38 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
39 {
40 xy_bddvar_map k, *r = NULL;
41 memset(&k, 0, sizeof(xy_bddvar_map));
42 k.key.x = x;
43 k.key.y = y;
44 HASH_FIND(hh, map, &k.key, sizeof(xy), r);
45 return r;
46 }
47
48 bddvar_xy_map *getbdd(int key, bddvar_xy_map *map)
49 {
50 bddvar_xy_map k, *r = NULL;
51 memset(&k, 0, sizeof(bddvar_xy_map));
52 k.key = key;
53 HASH_FIND(hh, map, &k.key, sizeof(int), r);
54 return r;
55 }
56
57
58 bimap *create_bimap_helper(sokoban_screen *screen)
59 {
60 int varcount = 0;
61 sokoban_screen *r;
62 xy_bddvar_map *xybdd = NULL;
63 bddvar_xy_map *bddxy = NULL;
64 for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
65 xy_bddvar_map *f = NULL;
66 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
67 memset(f, 0, sizeof(xy_bddvar_map));
68 f->key.x = r->coord.x;
69 f->key.y = r->coord.y;
70 f->value.var[0] = varcount * 2;
71 f->value.var[1] = (varcount + 1) * 2;
72 f->value.var[2] = (varcount + 2) * 2;
73 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
74
75 for (int i = 0; i <3; i++){
76 bddvar_xy_map *t = NULL;
77 t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
78 memset(t, 0, sizeof(bddvar_xy_map));
79 t->key = (varcount + i) * 2;
80 t->value.x = r->coord.x;
81 t->value.y = r->coord.y;
82 HASH_ADD(hh, bddxy, key, sizeof(int), t);
83 }
84 varcount = varcount + 3;
85 }
86 bimap *bm = NULL;
87 bm = (bimap *)malloc(sizeof(bimap));
88 bm->f = xybdd;
89 bm->t = bddxy;
90 return bm;
91 }
92
93 int check_xy_exists(int x, int y, bimap *bm)
94 {
95 int res = 0;
96 if (getxy(x, y, bm->f) != NULL) res = 1;
97 return res;
98 }
99
100 int check_space(int x, int y, direction d, int delta, bimap *bm)
101 {
102 switch(d){
103 case LEFT: x = x - delta; break;
104 case UP: y = y - delta; break;
105 case RIGHT: x = x + delta; break;
106 case DOWN: y = y + delta; break;
107 }
108 return check_xy_exists(x, y, bm);
109 }
110
111 /*
112 * Each coordinate has three related boolean variables. The combination of those boolean variables
113 * defines tiles:
114 * 000: Wall
115 * 001: Free
116 * 010: Box
117 * 100: Box on target
118 * 011: Target
119 * 101: Agent
120 * 110: Agent on target
121 * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
122 * tiles in the shrinked screen.
123 * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
124 * directly in transition relations.
125 */
126
127 state *encode_screen(sokoban_screen *screen)
128 {
129 LACE_ME;
130
131 BDDVAR vars[HASH_COUNT(screen) * 3];
132 for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
133 vars[i] = i * 2;
134 }
135
136 uint8_t st_enc[HASH_COUNT(screen) * 3];
137
138 BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
139 BDD s;
140 state *fullState = NULL;
141 fullState = (state *)malloc(sizeof(state));
142 fullState->vars.varset = varset;
143 fullState->vars.size = HASH_COUNT(screen) * 3;
144 int tile_index = 0;
145 sokoban_screen *r;
146 for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
147 switch(r->tile){
148 case FREE: //001
149 st_enc[tile_index] = 0;
150 tile_index++;
151 st_enc[tile_index] = 0;
152 tile_index++;
153 st_enc[tile_index] = 1;
154 tile_index++;
155 break;
156 case WALL: //000
157 st_enc[tile_index] = 0;
158 tile_index++;
159 st_enc[tile_index] = 0;
160 tile_index++;
161 st_enc[tile_index] = 0;
162 tile_index++;
163 break;
164 case BOX: //010
165 st_enc[tile_index] = 0;
166 tile_index++;
167 st_enc[tile_index] = 1;
168 tile_index++;
169 st_enc[tile_index] = 0;
170 tile_index++;
171 break;
172 case TARGET: //011
173 st_enc[tile_index] = 0;
174 tile_index++;
175 st_enc[tile_index] = 1;
176 tile_index++;
177 st_enc[tile_index] = 1;
178 tile_index++;
179 break;
180 case AGENT: //101
181 st_enc[tile_index] = 1;
182 tile_index++;
183 st_enc[tile_index] = 0;
184 tile_index++;
185
186 st_enc[tile_index] = 1;
187 tile_index++;
188 break;
189 case TARGAGENT: //110
190 st_enc[tile_index] = 1;
191 tile_index++;
192 st_enc[tile_index] = 1;
193 tile_index++;
194 st_enc[tile_index] = 0;
195 tile_index++;
196 break;
197 case TARGBOX: //100
198 st_enc[tile_index] = 1;
199 tile_index++;
200 st_enc[tile_index] = 0;
201 tile_index++;
202 st_enc[tile_index] = 0;
203 tile_index++;
204 break;
205 }
206 }
207 s = sylvan_cube(varset, st_enc);
208 fullState->bdd = s;
209 printf("Initial state encoded\n");
210 return fullState;
211 }
212
213 lurd_t *lappend(lurd_t *l, char c){
214 lurd_t *temp_lrd = NULL;
215 if (l == NULL){
216 temp_lrd = (lurd_t *)malloc(sizeof(lurd_t));
217 temp_lrd->c = c;
218 temp_lrd->next = NULL;
219 l = temp_lrd;
220 }
221 else {
222 temp_lrd = l;
223 while (temp_lrd->next != NULL){
224 temp_lrd = temp_lrd->next;
225 }
226 temp_lrd->next = (lurd_t *)malloc(sizeof(lurd_t));
227 temp_lrd->next->c = c;
228 temp_lrd->next->next = NULL;
229 }
230 return l;
231 }
232
233 int check_goal(BDD s, BDD g, BDDSET vars){
234 LACE_ME;
235 if(sylvan_satcount(sylvan_and(s, g), vars) > 0) return 1;
236 else return 0;
237 }
238
239 int check_visited(BDD s, BDD v, BDDSET vars){
240 LACE_ME;
241 if(sylvan_satcount(sylvan_and(s, v), vars) > 0) return 1;
242 else return 0;
243 }
244
245 state_t *explstate(state *init, rels *rls, state *g){
246 LACE_ME;
247 deque *state_queue = create();
248 trans_t *t = NULL;
249 state_t *tmp_state = (state_t *)malloc(sizeof(state_t));
250 lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
251 //state_t *new_state = (state_t *)malloc(sizeof(state_t));
252 BDD visited = init->bdd;
253 BDD new;
254 tmp_state->bdd = init->bdd;
255 tmp_state->vars = init->vars;
256 tmp_state->lrd = lrd;
257 state_queue = enq(tmp_state, state_queue);
258
259 while (isEmpty(state_queue) == 0){
260 tmp_state = get_front(state_queue);
261 state_queue = deq(state_queue);
262 new = tmp_state->bdd;
263 t = rls->rell;
264 while (t != NULL){
265 new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
266 if (new != sylvan_false && new != tmp_state->bdd) break;
267 t = t->next_rel;
268 }
269 if (new != sylvan_false && new != tmp_state->bdd){
270 if (check_visited(new, visited, init->vars.varset) == 0){
271 if (check_goal(new, g->bdd, init->vars.varset) == 0){
272 lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
273 state_t *new_state = (state_t *)malloc(sizeof(state_t));
274 printf("here1\n");
275 memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
276 printf("here2\n");
277 new_state->bdd = new;
278 new_state->vars = init->vars;
279 lrd = lappend(lrd, 'l');
280 new_state->lrd = lrd;
281 state_queue = enq(new_state, state_queue);
282 visited = sylvan_or(new, visited);
283 }
284 else {
285 printf("GOAL\n");
286 lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
287 state_t *new_state = (state_t *)malloc(sizeof(state_t));
288 memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
289 new_state->bdd = new;
290 new_state->vars = init->vars;
291 lrd = lappend(lrd, 'l');
292 new_state->lrd = lrd;
293 return new_state;
294 }
295 }
296 }
297
298 t = rls->relu;
299 while (t != NULL){
300 new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
301 if (new != sylvan_false && new != tmp_state->bdd) break;
302 t = t->next_rel;
303 }
304 if (new != sylvan_false && new != tmp_state->bdd){
305 if (check_visited(new, visited, init->vars.varset) == 0){
306 if (check_goal(new, g->bdd, init->vars.varset) == 0){
307 lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
308 state_t *new_state = (state_t *)malloc(sizeof(state_t));
309 memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
310 new_state->bdd = new;
311 new_state->vars = init->vars;
312 lrd = lappend(lrd, 'u');
313 new_state->lrd = lrd;
314 state_queue = enq(new_state, state_queue);
315 visited = sylvan_or(new, visited);
316 }
317 else {
318 printf("GOAL\n");
319 lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
320 state_t *new_state = (state_t *)malloc(sizeof(state_t));
321 memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
322 new_state->bdd = new;
323 new_state->vars = init->vars;
324 lrd = lappend(lrd, 'u');
325 new_state->lrd = lrd;
326 return new_state;
327 }
328 }
329 }
330
331 t = rls->relr;
332 while (t != NULL){
333 new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
334 if (new != sylvan_false && new != tmp_state->bdd) break;
335 t = t->next_rel;
336 }
337 if (new != sylvan_false && new != tmp_state->bdd){
338 if (check_visited(new, visited, init->vars.varset) == 0){
339 if (check_goal(new, g->bdd, init->vars.varset) == 0){
340 printf("Here1\n");
341 lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
342 state_t *new_state = (state_t *)malloc(sizeof(state_t));
343 memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
344 printf("Here2\n");
345
346 new_state->bdd = new;
347 new_state->vars = init->vars;
348 lrd = lappend(lrd, 'r');
349 new_state->lrd = lrd;
350 state_queue = enq(new_state, state_queue);
351 visited = sylvan_or(new, visited);
352 }
353 else {
354 printf("GOAL\n");
355 lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
356 state_t *new_state = (state_t *)malloc(sizeof(state_t));
357 memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
358
359 new_state->bdd = new;
360 new_state->vars = init->vars;
361 lrd = lappend(lrd, 'r');
362 new_state->lrd = lrd;
363 return new_state;
364 }
365 }
366 }
367
368
369 t = rls->reld;
370 while (t != NULL){
371 new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
372 if (new != sylvan_false && new != tmp_state->bdd) break;
373 t = t->next_rel;
374 }
375 if (new != sylvan_false && new != tmp_state->bdd){
376 if (check_visited(new, visited, init->vars.varset) == 0){
377 if (check_goal(new, g->bdd, init->vars.varset) == 0){
378
379 lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
380 state_t *new_state = (state_t *)malloc(sizeof(state_t));
381 memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
382
383 new_state->bdd = new;
384 new_state->vars = init->vars;
385 lrd = lappend(lrd, 'd');
386 new_state->lrd = lrd;
387 state_queue = enq(new_state, state_queue);
388 visited = sylvan_or(new, visited);
389 }
390 else {
391 printf("GOAL\n");
392 lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
393 state_t *new_state = (state_t *)malloc(sizeof(state_t));
394 memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
395
396 new_state->bdd = new;
397 new_state->vars = init->vars;
398 lrd = lappend(lrd, 'd');
399 new_state->lrd = lrd;
400 return new_state;
401 }
402 }
403 }
404
405
406 }
407
408 return NULL;
409 }
410
411 state *encode_goal(sokoban_screen *screen){
412 int boxes = 0;
413 int targets = 0;
414
415 LACE_ME;
416
417 BDDVAR vars[HASH_COUNT(screen) * 3];
418 for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
419 vars[i] = i * 2;
420 }
421
422 uint8_t st_enc[HASH_COUNT(screen) * 3];
423
424 BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
425 BDD s;
426 state *fullState = NULL;
427 fullState = (state *)malloc(sizeof(state));
428 fullState->vars.varset = varset;
429 fullState->vars.size = HASH_COUNT(screen) * 3;
430 int tile_index = 0;
431 sokoban_screen *r;
432 for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
433 switch(r->tile){
434 case FREE: //001 -> any
435 st_enc[tile_index] = 2;
436 tile_index++;
437 st_enc[tile_index] = 2;
438 tile_index++;
439 st_enc[tile_index] = 2;
440 tile_index++;
441 break;
442 case WALL: //000 -> stays the same
443 st_enc[tile_index] = 0;
444 tile_index++;
445 st_enc[tile_index] = 0;
446 tile_index++;
447 st_enc[tile_index] = 0;
448 tile_index++;
449 break;
450 case BOX: //010 -> any
451 boxes++;
452 st_enc[tile_index] = 2;
453 tile_index++;
454 st_enc[tile_index] = 2;
455 tile_index++;
456 st_enc[tile_index] = 2;
457 tile_index++;
458 break;
459 case TARGET: //011 -> targbox
460 targets++;
461 st_enc[tile_index] = 1;
462 tile_index++;
463 st_enc[tile_index] = 0;
464 tile_index++;
465 st_enc[tile_index] = 0;
466 tile_index++;
467 break;
468 case AGENT: //101 -> any
469 st_enc[tile_index] = 2;
470 tile_index++;
471 st_enc[tile_index] = 2;
472 tile_index++;
473 st_enc[tile_index] = 2;
474 tile_index++;
475 break;
476 case TARGAGENT: //110 -> targbox
477 targets++;
478 st_enc[tile_index] = 1;
479 tile_index++;
480 st_enc[tile_index] = 0;
481 tile_index++;
482 st_enc[tile_index] = 0;
483 tile_index++;
484 break;
485 case TARGBOX: //100 -> stays the same
486 targets++;
487 boxes++;
488 st_enc[tile_index] = 1;
489 tile_index++;
490 st_enc[tile_index] = 0;
491 tile_index++;
492 st_enc[tile_index] = 0;
493 tile_index++;
494 break;
495 }
496 }
497 s = sylvan_cube(varset, st_enc);
498 fullState->bdd = s;
499 printf("Goal state encoded\n");
500 if (targets == 0 || (boxes != targets)) return NULL;
501 else return fullState;
502
503 }
504
505 //test
506 //int countTrans(trans_t *trs);
507
508 trans_t *create_single_rel(sokoban_screen *screen, direction dir)
509 {
510 LACE_ME;
511 trans_t *trs, *trs_current;
512 bimap *bm = create_bimap_helper(screen);
513 int x = 0;
514 int y = 0;
515 bddvar_xy_map *bddxy = NULL;
516 int xdelta = 0;
517 int ydelta = 0;
518 int xgamma = 0;
519 int ygamma = 0;
520 trs = NULL;
521 switch(dir){
522 case LEFT:
523 xdelta = -1;
524 ydelta = 0;
525 xgamma = -2;
526 ygamma = 0;
527 break;
528 case UP:
529 xdelta = 0;
530 ydelta = -1;
531 xgamma = 0;
532 ygamma = -2;
533 break;
534 case RIGHT:
535 xdelta = 1;
536 ydelta = 0;
537 xgamma = 2;
538 ygamma = 0;
539 break;
540 case DOWN:
541 xdelta = 0;
542 ydelta = 1;
543 xgamma = 0;
544 ygamma = 2;
545 break;
546 }
547
548 for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
549 bddxy = getbdd(i*6, bm->t);
550 x = bddxy->value.x;
551 y = bddxy->value.y;
552 if (check_space(x, y, dir, 1, bm) == 0){
553 //Agent -> Agent
554 //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
555 BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5};
556 BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
557 uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
558 trs_current = (trans_t *)malloc(sizeof(trans_t));
559 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
560 trs_current->varset.varset = relvarset;
561 trs_current->varset.size = 6;
562 trs_current->next_rel = trs;
563 trs = trs_current;
564
565 //Targagent -> Targagent
566 //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
567 relvarset = sylvan_set_fromarray(relvars, 6);
568 uint8_t rel_enc1[6] = {1, 1, 1, 1, 0, 0};
569 memcpy(rel_enc, rel_enc1, 6*sizeof(uint8_t));
570
571 trs_current = (trans_t *)malloc(sizeof(trans_t));
572 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
573 trs_current->varset.varset = relvarset;
574 trs_current->varset.size = 6;
575 trs_current->next_rel = trs;
576 trs = trs_current;
577
578 }
579
580 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
581 xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
582 unsigned int deltai = bddvar->value.var[0];
583 //Agent Free -> Free Agent
584 //(1 0 0 0 1 1 0 1 0 0 1 1)
585 //or
586 //(0 1 0 0 1 1 1 0 0 0 1 1)
587 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};
588 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
589 uint8_t rel_enc[12];
590 if (i*6 < deltai){
591 uint8_t rel_enc0[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
592 memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
593 }
594 else {
595 uint8_t rel_enc0[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
596 memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
597 }
598 trs_current = (trans_t *)malloc(sizeof(trans_t));
599 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
600 trs_current->varset.varset = relvarset;
601 trs_current->varset.size = 12;
602 trs_current->next_rel = trs;
603 trs = trs_current;
604
605 //Agent Target -> Free Targagent
606 //(1 0 0 0 1 1 0 1 1 1 1 0)
607 //or
608 //(0 1 1 1 1 0 1 0 0 0 1 1)
609 relvarset = sylvan_set_fromarray(relvars, 12);
610 if (i*6 < deltai){
611 uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
612 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
613 }
614 else {
615 uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
616 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
617 }
618 trs_current = (trans_t *)malloc(sizeof(trans_t));
619 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
620 trs_current->varset.varset = relvarset;
621 trs_current->varset.size = 12;
622 trs_current->next_rel = trs;
623 trs = trs_current;
624
625 //Targagent Free -> Target Agent
626 //(1 0 1 1 0 1 0 1 0 0 1 1)
627 //or
628 //(0 1 0 0 1 1 1 0 1 1 0 1)
629 relvarset = sylvan_set_fromarray(relvars, 12);
630 if (i*6 < deltai){
631 uint8_t rel_enc3[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
632 memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
633 }
634 else {
635 uint8_t rel_enc3[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
636 memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
637 }
638 trs_current = (trans_t *)malloc(sizeof(trans_t));
639 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
640 trs_current->varset.varset = relvarset;
641 trs_current->varset.size = 12;
642 trs_current->next_rel = trs;
643 trs = trs_current;
644
645 //Targagent Target -> Target Targagent
646 //(1 0 1 1 0 1 0 1 1 1 1 0)
647 //or
648 //(0 1 1 1 1 0 1 0 1 1 0 1)
649 relvarset = sylvan_set_fromarray(relvars, 12);
650 if (i*6 < deltai){
651 uint8_t rel_enc4[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
652 memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
653 }
654 else {
655 uint8_t rel_enc4[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
656 memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
657 }
658 trs_current = (trans_t *)malloc(sizeof(trans_t));
659 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
660 trs_current->varset.varset = relvarset;
661 trs_current->varset.size = 12;
662 trs_current->next_rel = trs;
663 trs = trs_current;
664
665 //Agent Box -> Agent Box
666 //(1 1 0 0 1 1 0 0 1 1 0 0)
667 //or
668 //(0 0 1 1 0 0 1 1 0 0 1 1)
669 relvarset = sylvan_set_fromarray(relvars, 12);
670 if (i*6 < deltai){
671 uint8_t rel_enc5[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
672 memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
673 }
674 else {
675 uint8_t rel_enc5[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
676 memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
677 }
678 trs_current = (trans_t *)malloc(sizeof(trans_t));
679 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
680 trs_current->varset.varset = relvarset;
681 trs_current->varset.size = 12;
682 trs_current->next_rel = trs;
683 trs = trs_current;
684
685 //Agent Targbox -> Agent Targbox
686 //(1 1 0 0 1 1 1 1 0 0 0 0)
687 //
688 //(1 1 0 0 0 0 1 1 0 0 1 1)
689 relvarset = sylvan_set_fromarray(relvars, 12);
690 if (i*6 < deltai){
691 uint8_t rel_enc6[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
692 memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
693 }
694 else {
695 uint8_t rel_enc6[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
696 memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
697 }
698 trs_current = (trans_t *)malloc(sizeof(trans_t));
699 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
700 trs_current->varset.varset = relvarset;
701 trs_current->varset.size = 12;
702 trs_current->next_rel = trs;
703 trs = trs_current;
704
705 //Targagent Box -> Targagent Box
706 //(1 1 1 1 0 0 0 0 1 1 0 0)
707 //or
708 //(0 0 1 1 0 0 1 1 1 1 0 0)
709 relvarset = sylvan_set_fromarray(relvars, 12);
710 if (i*6 < deltai){
711 uint8_t rel_enc7[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
712 memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
713 }
714 else {
715 uint8_t rel_enc7[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
716 memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
717 }
718 trs_current = (trans_t *)malloc(sizeof(trans_t));
719 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
720 trs_current->varset.varset = relvarset;
721 trs_current->varset.size = 12;
722 trs_current->next_rel = trs;
723 trs = trs_current;
724
725 //Targagent Targbox -> Targagent Targbox
726 //(1 1 1 1 0 0 1 1 0 0 0 0)
727 //or
728 //(1 1 0 0 0 0 1 1 1 1 0 0)
729 relvarset = sylvan_set_fromarray(relvars, 12);
730 if (i*6 < deltai){
731 uint8_t rel_enc8[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
732 memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
733 }
734 else {
735 uint8_t rel_enc8[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
736 memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
737 }
738 trs_current = (trans_t *)malloc(sizeof(trans_t));
739 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
740 trs_current->varset.varset = relvarset;
741 trs_current->varset.size = 12;
742 trs_current->next_rel = trs;
743 trs = trs_current;
744
745
746 }
747
748 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
749 xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
750 unsigned int deltai = bddvar->value.var[0];
751 bddvar = getxy(x + xgamma, y + ygamma, bm->f);
752 unsigned int gammai = bddvar->value.var[0];
753 //Agent Free -> Free Agent
754 //(1 0 0 0 1 1 0 1 0 0 1 1)
755 //or
756 //(0 1 0 0 1 1 1 0 0 0 1 1)
757 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};
758 BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
759 uint8_t rel_enc[12];
760 if (i*6 < deltai){
761 uint8_t rel_enc_[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
762 memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
763 }
764 else {
765 uint8_t rel_enc_[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
766 memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
767 }
768 trs_current = (trans_t *)malloc(sizeof(trans_t));
769 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
770 trs_current->varset.varset = relvarset;
771 trs_current->varset.size = 12;
772 trs_current->next_rel = trs;
773 trs = trs_current;
774
775 //Agent Target -> Free Targagent
776 //(1 0 0 0 1 1 0 1 1 1 1 0)
777 //or
778 //(0 1 1 1 1 0 1 0 0 0 1 1)
779 relvarset = sylvan_set_fromarray(relvars, 12);
780 if (i*6 < deltai){
781 uint8_t rel_enc9[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
782 memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
783 }
784 else {
785 uint8_t rel_enc9[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
786 memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
787 }
788 trs_current = (trans_t *)malloc(sizeof(trans_t));
789 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
790 trs_current->varset.varset = relvarset;
791 trs_current->varset.size = 12;
792 trs_current->next_rel = trs;
793 trs = trs_current;
794
795 //Targagent Free -> Target Agent (LEFT || UP)
796 //(1 0 1 1 0 1 0 1 0 0 1 1)
797 //or
798 //(0 1 0 0 1 1 1 0 1 1 0 1)
799 relvarset = sylvan_set_fromarray(relvars, 12);
800 if (i*6 < deltai){
801 uint8_t rel_enc10[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
802 memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
803 }
804 else {
805 uint8_t rel_enc10[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
806 memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
807 }
808 trs_current = (trans_t *)malloc(sizeof(trans_t));
809 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
810 trs_current->varset.varset = relvarset;
811 trs_current->varset.size = 12;
812 trs_current->next_rel = trs;
813 trs = trs_current;
814
815 //Targagent Target -> Target Targagent (LEFT || UP)
816 //(1 0 1 1 0 1 0 1 1 1 1 0)
817 //or
818 //(0 1 1 1 1 0 1 0 1 1 0 1)
819 relvarset = sylvan_set_fromarray(relvars, 12);
820 if (i*6 < deltai){
821 uint8_t rel_enc11[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
822 memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
823 }
824 else {
825 uint8_t rel_enc11[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
826 memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
827 }
828 trs_current = (trans_t *)malloc(sizeof(trans_t));
829 trs_current->bdd = sylvan_cube(relvarset, rel_enc);
830 trs_current->varset.varset = relvarset;
831 trs_current->varset.size = 12;
832 trs_current->next_rel = trs;
833 trs = trs_current;
834
835 //Agent Box Box -> Agent Box Box
836 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
837 //or
838 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
839 //or
840 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
841 //or
842 //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
843 //or
844 //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
845 //or
846 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
847 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};
848 BDD relvarset1 = sylvan_set_fromarray(relvars1, 18);
849 uint8_t rel_enc1[18];
850 if (i*6 < deltai && deltai < gammai){
851 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
852 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
853 }
854 else if (deltai < gammai && gammai < i*6){
855 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
856 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
857 }
858 else if (gammai < i*6 && i*6 < deltai){
859 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
860 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
861 }
862 else if (i*6 < gammai && gammai < deltai){
863 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
864 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
865 }
866 else if (deltai < i*6 && i*6 < gammai){
867 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
868 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
869 }
870 else {
871 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
872 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
873 }
874
875 trs_current = (trans_t *)malloc(sizeof(trans_t));
876 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
877 trs_current->varset.varset = relvarset1;
878 trs_current->varset.size = 18;
879 trs_current->next_rel = trs;
880 trs = trs_current;
881
882 //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
883 //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
884 //or
885 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
886 //or
887 //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
888 //or
889 //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
890 //or
891 //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
892 //or
893 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
894 relvarset1 = sylvan_set_fromarray(relvars1, 18);
895 if (i*6 < deltai && deltai < gammai){
896 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
897 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
898 }
899 else if (deltai < gammai && gammai < i*6){
900 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
901 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
902 }
903 else if (gammai < i*6 && i*6 < deltai){
904 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
905 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
906 }
907 else if (i*6 < gammai && gammai < deltai){
908 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
909 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
910 }
911 else if (deltai < i*6 && i*6 < gammai){
912 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
913 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
914 }
915 else {
916 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
917 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
918 }
919 trs_current = (trans_t *)malloc(sizeof(trans_t));
920 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
921 trs_current->varset.varset = relvarset1;
922 trs_current->varset.size = 18;
923 trs_current->next_rel = trs;
924 trs = trs_current;
925
926 //Targagent Box Box -> Targagent Box Box
927 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
928 //or
929 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
930 //or
931 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
932 //or
933 //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
934 //or
935 //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
936 //or
937 //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
938 relvarset1 = sylvan_set_fromarray(relvars1, 18);
939 if (i*6 < deltai && deltai < gammai){
940 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
941 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
942 }
943 else if (deltai < gammai && gammai < i*6){
944 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
945 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
946 }
947 else if (gammai < i*6 && i*6 < deltai){
948 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
949 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
950 }
951 else if (i*6 < gammai && gammai < deltai){
952 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
953 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
954 }
955 else if (deltai < i*6 && i*6 < gammai){
956 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
957 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
958 }
959 else {
960 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
961 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
962 }
963 trs_current = (trans_t *)malloc(sizeof(trans_t));
964 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
965 trs_current->varset.varset = relvarset1;
966 trs_current->varset.size = 18;
967 trs_current->next_rel = trs;
968 trs = trs_current;
969
970 //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
971 //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
972 //or
973 //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
974 //or
975 //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
976 //or
977 //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
978 //or
979 //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
980 //or
981 //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
982 relvarset1 = sylvan_set_fromarray(relvars1, 18);
983 if (i*6 < deltai && deltai < gammai){
984 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
985 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
986 }
987 else if (deltai < gammai && gammai < i*6){
988 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
989 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
990 }
991 else if (gammai < i*6 && i*6 < deltai){
992 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
993 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
994 }
995 else if (i*6 < gammai && gammai < deltai){
996 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
997 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
998 }
999 else if (deltai < i*6 && i*6 < gammai){
1000 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
1001 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1002 }
1003 else {
1004 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
1005 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1006 }
1007 trs_current = (trans_t *)malloc(sizeof(trans_t));
1008 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1009 trs_current->varset.varset = relvarset1;
1010 trs_current->varset.size = 18;
1011 trs_current->next_rel = trs;
1012 trs = trs_current;
1013
1014 //Agent Box Free -> Free Agent Box
1015 //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
1016 //or
1017 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
1018 //or
1019 //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
1020 //or
1021 //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
1022 //or
1023 //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
1024 //or
1025 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1026 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1027 if (i*6 < deltai && deltai < gammai){
1028 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1029 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1030 }
1031
1032 else if (deltai < gammai && gammai < i*6){
1033 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1034 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1035 }
1036
1037 else if (gammai < i*6 && i*6 < deltai){
1038 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1039 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1040 }
1041
1042 else if (i*6 < gammai && gammai < deltai){
1043 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1044 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1045 }
1046 else if (deltai < i*6 && i*6 < gammai){
1047 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1048 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1049 }
1050 else {
1051 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1052 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1053 }
1054
1055 trs_current = (trans_t *)malloc(sizeof(trans_t));
1056
1057 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1058 trs_current->varset.varset = relvarset1;
1059 trs_current->varset.size = 18;
1060 trs_current->next_rel = trs;
1061 trs = trs_current;
1062
1063 //Agent Targbox Free -> Free Targagent Box
1064 //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
1065 //or
1066 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
1067 //or
1068 //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1069 //or
1070 //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
1071 //or
1072 //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
1073 //or
1074 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1075 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1076 if (i*6 < deltai && deltai < gammai){
1077 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1078 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1079 }
1080 else if (deltai < gammai && gammai < i*6){
1081 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1082 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1083 }
1084 else if (gammai < i*6 && i*6 < deltai){
1085 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1086 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1087 }
1088 else if (i*6 < gammai && gammai < deltai){
1089 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1090 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1091 }
1092 else if (deltai < i*6 && i*6 < gammai){
1093 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1094 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1095 }
1096 else {
1097 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1098 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1099 }
1100 trs_current = (trans_t *)malloc(sizeof(trans_t));
1101 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1102 trs_current->varset.varset = relvarset1;
1103 trs_current->varset.size = 18;
1104 trs_current->next_rel = trs;
1105 trs = trs_current;
1106
1107 //Agent Box Target -> Free Agent Targbox
1108 //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
1109 //or
1110 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
1111 //or
1112 //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
1113 //or
1114 //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
1115 //or
1116 //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
1117 //or
1118 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1119 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1120 if (i*6 < deltai && deltai < gammai){
1121 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1122 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1123 }
1124 else if (deltai < gammai && gammai < i*6){
1125 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1126 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1127 }
1128 else if (gammai < i*6 && i*6 < deltai){
1129 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1130 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1131 }
1132 else if (i*6 < gammai && gammai < deltai){
1133 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1134 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1135 }
1136 else if (deltai < i*6 && i*6 < gammai){
1137 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1138 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1139 }
1140 else {
1141 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1142 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1143 }
1144 trs_current = (trans_t *)malloc(sizeof(trans_t));
1145 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1146 trs_current->varset.varset = relvarset1;
1147 trs_current->varset.size = 18;
1148 trs_current->next_rel = trs;
1149 trs = trs_current;
1150
1151 //Agent Targbox Target -> Free Targagent Targbox
1152 //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
1153 //or
1154 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
1155 //or
1156 //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1157 //or
1158 //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
1159 //or
1160 //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
1161 //or
1162 //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1163 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1164 if (i*6 < deltai && deltai < gammai){
1165 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1166 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1167 }
1168 else if (deltai < gammai && gammai < i*6){
1169 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1170 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1171 }
1172 else if (gammai < i*6 && i*6 < deltai){
1173 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1174 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1175 }
1176 else if (i*6 < gammai && gammai < deltai){
1177 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1178 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1179 }
1180 else if (deltai < i*6 && i*6 < gammai){
1181 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1182 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1183 }
1184 else {
1185 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1186 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1187 }
1188 trs_current = (trans_t *)malloc(sizeof(trans_t));
1189 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1190 trs_current->varset.varset = relvarset1;
1191 trs_current->varset.size = 18;
1192 trs_current->next_rel = trs;
1193 trs = trs_current;
1194
1195 //Targagent Box Free -> Target Agent Box
1196 //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
1197 //or
1198 //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
1199 //or
1200 //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1201 //or
1202 //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
1203 //or
1204 //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
1205 //or
1206 //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1207 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1208 if (i*6 < deltai && deltai < gammai){
1209 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1210 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1211 }
1212 else if (deltai < gammai && gammai < i*6){
1213 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1214 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1215 }
1216 else if (gammai < i*6 && i*6 < deltai){
1217 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1218 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1219 }
1220 else if (i*6 < gammai && gammai < deltai){
1221 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1222 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1223 }
1224 else if (deltai < i*6 && i*6 < gammai){
1225 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
1226 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1227 }
1228 else {
1229 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1230 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1231 }
1232 trs_current = (trans_t *)malloc(sizeof(trans_t));
1233 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1234 trs_current->varset.varset = relvarset1;
1235 trs_current->varset.size = 18;
1236 trs_current->next_rel = trs;
1237 trs = trs_current;
1238
1239 //Targagent Targbox Free -> Target Targagent Box
1240 //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
1241 //or
1242 //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
1243 //or
1244 //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1245 //or
1246 //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
1247 //or
1248 //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
1249 //or
1250 //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1251 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1252 if (i*6 < deltai && deltai < gammai){
1253 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1254 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1255 }
1256 else if (deltai < gammai && gammai < i*6){
1257 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1258 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1259 }
1260 else if (gammai < i*6 && i*6 < deltai){
1261 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1262 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1263 }
1264 else if (i*6 < gammai && gammai < deltai){
1265 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1266 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1267 }
1268 else if (deltai < i*6 && i*6 < gammai){
1269 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0};
1270 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1271 }
1272 else {
1273 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1274 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1275 }
1276 trs_current = (trans_t *)malloc(sizeof(trans_t));
1277 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1278 trs_current->varset.varset = relvarset1;
1279 trs_current->varset.size = 18;
1280 trs_current->next_rel = trs;
1281 trs = trs_current;
1282
1283 //Targagent Box Target -> Target Agent Targbox
1284 //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1285 //or
1286 //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1287 //or
1288 //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1289 //or
1290 //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1291 //or
1292 //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1293 //or
1294 //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1295 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1296 if (i*6 < deltai && deltai < gammai){
1297 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1298 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1299 }
1300 else if (deltai < gammai && gammai < i*6){
1301 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1302 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1303 }
1304 else if (gammai < i*6 && i*6 < deltai){
1305 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1306 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1307 }
1308 else if (i*6 < gammai && gammai < deltai){
1309 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1310 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1311 }
1312 else if (deltai < i*6 && i*6 < gammai){
1313 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1314 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1315 }
1316 else {
1317 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1318 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1319 }
1320 trs_current = (trans_t *)malloc(sizeof(trans_t));
1321 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1322 trs_current->varset.varset = relvarset1;
1323 trs_current->varset.size = 18;
1324 trs_current->next_rel = trs;
1325 trs = trs_current;
1326
1327 //Targagent Targbox Target -> Target Targagent Targbox
1328 //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1329 //or
1330 //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1331 //or
1332 //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1333 //or
1334 //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1335 //or
1336 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1337 //or
1338 //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1339 relvarset1 = sylvan_set_fromarray(relvars1, 18);
1340 if (i*6 < deltai && deltai < gammai){
1341 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1342 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1343 }
1344 else if (deltai < gammai && gammai < i*6){
1345 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1346 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1347 }
1348 else if (gammai < i*6 && i*6 < deltai){
1349 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1350 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1351 }
1352 else if (i*6 < gammai && gammai < deltai){
1353 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1354 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1355 }
1356 else if (deltai < i*6 && i*6 < gammai){
1357 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1358 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1359 }
1360 else {
1361 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1362 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1363 }
1364 trs_current = (trans_t *)malloc(sizeof(trans_t));
1365 trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1366 trs_current->varset.varset = relvarset1;
1367 trs_current->varset.size = 18;
1368 trs_current->next_rel = trs;
1369 trs = trs_current;
1370 }
1371
1372 }
1373 trs_current = trs;
1374
1375 //test
1376 /*
1377 switch(dir){
1378 case LEFT:
1379 if (trs_current != NULL) printf("LEFT ok!\n");
1380 else printf ("LEFT is empty\n");
1381 printf("Num of trans relations:%d\n", countTrans(trs));
1382 break;
1383 case UP:
1384 if (trs_current != NULL) printf("UP ok!\n");
1385 else printf ("UP is empty\n");
1386 printf("Num of trans relations:%d\n", countTrans(trs));
1387 break;
1388 case RIGHT:
1389 if (trs_current != NULL) printf("RIGHT ok!\n");
1390 else printf ("RIGHT is empty\n");
1391 printf("Num of trans relations:%d\n", countTrans(trs));
1392 break;
1393 case DOWN:
1394 if (trs_current != NULL) printf("DOWN ok!\n");
1395 else printf ("DOWN is empty\n");
1396 printf("Num of trans relations:%d\n", countTrans(trs));
1397 break;
1398 }
1399 */
1400 return trs;
1401 }
1402
1403 //test
1404 /*
1405 int countTrans(trans_t *trs)
1406 {
1407 int counter = 0;
1408 while (trs != NULL){
1409 counter++;
1410 trs = trs->next_rel;
1411 }
1412 return counter;
1413 }
1414 */
1415 rels *encode_rel(sokoban_screen *screen)
1416 {
1417 LACE_ME;
1418
1419 trans_t *tl = sylvan_false;
1420
1421 //left relation
1422 tl = create_single_rel(screen, LEFT);
1423
1424 //up relation
1425 trans_t *tu = create_single_rel(screen, UP);
1426
1427 //right relation
1428 trans_t *tr = create_single_rel(screen, RIGHT);
1429
1430 //down relation
1431 trans_t *td = create_single_rel(screen, DOWN);
1432
1433 rels *rls = NULL;
1434 rls = (rels *)malloc(sizeof(rels));
1435 rls->rell = tl;
1436 rls->relu = tu;
1437 rls->relr = tr;
1438 rls->reld = td;
1439
1440 return rls;
1441 }
1442
1443 int test_trans(state *s, trans_t *t)
1444 {
1445 LACE_ME;
1446 BDD next = sylvan_false;
1447 while (t != NULL){
1448 next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset);
1449 if (next == s->bdd) printf("Same\n");
1450 if (next != s->bdd && next != sylvan_false) printf("Different\n");
1451 if (next == sylvan_false) printf("False\n");
1452 t = t->next_rel;
1453 }
1454 return 1;
1455 }
Unnamed repository; edit this file 'description' to name the repository.