8 #define EPRINTF(fmt, as...) fprintf(stderr, fmt, ##as)
18 void get_screen_metrics(sokoban_screen
*screen
,
21 int *agentx
, int *agenty
,
22 int *boxxes
, int *boxyes
)
30 for(r
=screen
; r
!= NULL
; r
= (sokoban_screen
*)(r
->hh
.next
)){
31 *mx
= r
->coord
.x
> *mx
? r
->coord
.x
: *mx
;
32 *my
= r
->coord
.x
> *mx
? r
->coord
.x
: *mx
;
41 boxxes
[*boxes
] = r
->coord
.x
;
42 boxyes
[*boxes
] = r
->coord
.y
;
50 BDD
encode_int(BDD state
, int x
, int bx
, int *variablenum
)
53 char *encoding
= malloc(bx
);
54 for(int i
= 0; i
<bx
; i
++){
56 state
= sylvan_and(state
, sylvan_ithvar(*variablenum
));
58 state
= sylvan_and(state
, sylvan_nithvar(*variablenum
));
66 BDD
encode_position(BDD state
, int x
, int y
, int bx
, int by
, int *variablenum
)
68 state
= encode_int(state
, x
, bx
, variablenum
);
69 return encode_int(state
, y
, by
, variablenum
);
73 * We have variables numbered 1...
74 * Per coordinate we need k=bitsx+bitsy variables
77 * box_i: k+k*i till k+k*(i+1)
78 * We start with the agent
80 BDD
solve_object(sokoban_screen
*scr
)
82 int nboxes
, mx
, my
, wx
, wy
, agentx
, agenty
;
86 get_screen_metrics(scr
, &nboxes
, &mx
, &my
, &agentx
, &agenty
, boxx
, boxy
);
88 EPRINTF("Max x: %d, thus %d bits\n", mx
, (wx
= ilog2(mx
)));
89 EPRINTF("Max y: %d, thus %d bits\n", my
, (wy
= ilog2(my
)));
90 EPRINTF("%d boxes\n", nboxes
);
92 BDD state
= sylvan_true
;
93 state
= encode_position(state
, agentx
, agenty
, wx
, wy
, &varnum
);
94 for(int i
= 0; i
<nboxes
; i
++){
95 state
= encode_position(state
, boxx
[i
], boxy
[i
], wx
, wy
, &varnum
);