8 #define EPRINTF(fmt, as...) fprintf(stderr, fmt, ##as)
10 typedef enum {UP
, DOWN
, LEFT
, RIGHT
} direction
;
20 void get_screen_metrics(sokoban_screen
*screen
,
23 int *agentx
, int *agenty
,
24 int *boxxes
, int *boxyes
)
32 for(r
=screen
; r
!= NULL
; r
= r
->hh
.next
){
33 *mx
= r
->coord
.x
> *mx
? r
->coord
.x
: *mx
;
34 *my
= r
->coord
.y
> *my
? r
->coord
.x
: *my
;
43 boxxes
[*boxes
] = r
->coord
.x
;
44 boxyes
[*boxes
] = r
->coord
.y
;
53 BDD
encode_int(BDD state
, int x
, int bx
, int *variablenum
)
56 char *encoding
= malloc(bx
);
57 for(int i
= 0; i
<bx
; i
++){
59 state
= sylvan_and(state
, sylvan_ithvar(*variablenum
*2));
61 state
= sylvan_and(state
, sylvan_nithvar(*variablenum
*2));
69 BDD
encode_position(BDD state
, int x
, int y
, int bx
, int by
, int *variablenum
)
71 state
= encode_int(state
, x
, bx
, variablenum
);
72 return encode_int(state
, y
, by
, variablenum
);
75 BDD
encode_transition(sokoban_screen
*scr
, BDD state
, int bx
, int by
, int *varnum
, direction dir
)
78 //Increase the position
79 int oldvarnum
= *varnum
;
83 state
= sylvan_and(state
,
84 sylvan_xor(sylvan_ithvar(*varnum
*2), sylvan_ithvar(*varnum
*2+1)));
86 for(int i
= 1; i
<bx
; i
++){
87 state
= sylvan_and(state
,
88 sylvan_xor(sylvan_ithvar(*varnum
*2-1),
89 sylvan_xor(sylvan_ithvar(*varnum
*2),
90 sylvan_ithvar(*varnum
*2+1))));
93 } else if(dir
== LEFT
){
102 state
= sylvan_and(state
,
103 sylvan_xor(sylvan_ithvar(*varnum
*2), sylvan_ithvar(*varnum
*2+1)));
105 for(int i
= 1; i
<by
; i
++){
106 state
= sylvan_and(state
,
107 sylvan_xor(sylvan_ithvar(*varnum
*2-1),
108 sylvan_xor(sylvan_ithvar(*varnum
*2),
109 sylvan_ithvar(*varnum
*2+1))));
112 } else if(dir
== UP
){
119 //Check wether it is a valid position
120 BDD legalpos
= sylvan_false
;
121 for(sokoban_screen
*r
=scr
; r
!= NULL
; r
= r
->hh
.next
){
126 BDD currentx
= sylvan_true
;
127 for(int i
= 0; i
<bx
; i
++){
128 if((x
& (1<<i
)) > 0){
129 currentx
= sylvan_and(currentx
, sylvan_ithvar(*varnum
*2+1));
131 currentx
= sylvan_and(currentx
, sylvan_nithvar(*varnum
*2+1));
136 BDD currenty
= sylvan_true
;
137 for(int i
= 0; i
<by
; i
++){
138 if((y
& (1<<i
)) > 0){
139 currenty
= sylvan_and(currenty
, sylvan_ithvar(*varnum
*2+1));
141 currenty
= sylvan_and(currenty
, sylvan_nithvar(*varnum
*2+1));
145 legalpos
= sylvan_or(legalpos
,
146 sylvan_and(currentx
, currenty
));
149 return sylvan_and(state
, legalpos
);
153 * We have variables numbered 1...
154 * Per coordinate we need k=bitsx+bitsy variables
157 * box_i: k+k*i till k+k*(i+1)
158 * We start with the agent
160 BDD
solve_object(sokoban_screen
*scr
)
163 int nboxes
, mx
, my
, wx
, wy
, agentx
, agenty
;
168 get_screen_metrics(scr
, &nboxes
, &mx
, &my
, &agentx
, &agenty
, boxx
, boxy
);
170 EPRINTF("Max x: %d, thus %d bits\n", mx
, (wx
= ilog2(mx
)));
171 EPRINTF("Max y: %d, thus %d bits\n", my
, (wy
= ilog2(my
)));
172 EPRINTF("%d boxes\n", nboxes
);
174 BDD init
= encode_position(sylvan_true
, agentx
, agenty
, wx
, wy
, &varnum
);
175 for(int i
= 0; i
<nboxes
; i
++){
176 init
= encode_position(init
, boxx
[i
], boxy
[i
], wx
, wy
, &varnum
);
180 BDD trans_r
= encode_transition(scr
, sylvan_true
, mx
, my
, &varnum
, RIGHT
);
182 BDD trans_l
= encode_transition(scr
, sylvan_true
, mx
, my
, &varnum
, LEFT
);
184 BDD trans_d
= encode_transition(scr
, sylvan_true
, mx
, my
, &varnum
, DOWN
);
186 BDD trans_u
= encode_transition(scr
, sylvan_true
, mx
, my
, &varnum
, UP
);
188 BDD old
= sylvan_false
;
192 EPRINTF("Iteration %d\n", iteration
++);
194 new = sylvan_or(new, sylvan_relnext(new, trans_d
, false));
195 new = sylvan_or(new, sylvan_relnext(new, trans_r
, false));
196 new = sylvan_or(new, sylvan_relnext(new, trans_u
, false));
197 new = sylvan_or(new, sylvan_relnext(new, trans_l
, false));
198 sylvan_printdot_nc(old
);