13 #define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
14 #define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
16 typedef enum {OBJECT
, COORD
, HYBRID
} strategy
;
20 strategy strat
= HYBRID
;
25 "\t%s [opts] [FILE [FILE [...]]]\n"
28 "\tAll strategies are mutually exclusive\n"
29 "\t-c coordinate based strategy\n"
30 "\t-o object based strategy\n"
31 "\t-y hybrid strategy\n"
32 // "\t-l LURD lURD verification strategy\n"
33 // "\t-r show all positions that are a valid solution\n"
35 "\t-d enable verbose debug output\n"
36 "\t-h show this help\n"
38 "Positional arguments:\n"
39 "\tFILE zero or more sokoban screens\n"
40 "\t when no file is specified stdin will be used\n", prg
);
43 void solve(FILE *inputstream
)
45 clock_t time_start_read
, time_end_read
;
46 clock_t time_start_encode
, time_end_encode
;
48 time_start_read
= clock();
49 sokoban_screen
*screen
= parse_screen(inputstream
, false);
50 if (screen
== NULL
) printf("Something went wrong...\n");
51 //sokoban_print(screen);
52 time_end_read
= clock();
54 time_start_encode
= clock();
56 lace_init(0, 1000000);
57 lace_startup(0, NULL
, NULL
);
59 sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
62 state
*init
= encode_screen(screen
);
63 state
*goal
= encode_goal(screen
);
64 rels
*rls
= encode_rel(screen
);
66 printf("Doing left\n");
67 test_trans(init, rls->rell);
69 test_trans(init, rls->relu);
70 printf("Doing right\n");
71 test_trans(init, rls->relr);
72 printf("Doing down\n");
73 test_trans(init, rls->reld);
76 BDD old
= sylvan_false
;
82 ERRPRINT("Iteration %d\n", iteration
++);
83 trans_t
*t
= rls
->rell
;
87 BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9);
88 BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0});
89 BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0}));
90 BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1}));
91 if (new == teststate2) printf("Wrong!\n");
94 new = sylvan_or(new, sylvan_relnext(new, t
->bdd
, t
->varset
.varset
));
96 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
101 new = sylvan_or(new, sylvan_relnext(new, t
->bdd
, t
->varset
.varset
));
103 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
109 new = sylvan_or(new, sylvan_relnext(new, t
->bdd
, t
->varset
.varset
));
111 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
117 new = sylvan_or(new, sylvan_relnext(new, t
->bdd
, t
->varset
.varset
));
119 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
121 double check
= sylvan_satcount(sylvan_and(goal
->bdd
, new), init
->vars
.varset
);
123 printf("Solution is found after %d iteration(s)!\n", iteration
);
128 else printf("No solution found!\n");
129 ERRPRINT("Satcount: %f\n", sylvan_satcount(old
, init
->vars
.varset
));
130 // sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);
131 // sylvan_printdot_nc(old);
132 time_end_encode
= clock();
136 sokoban_free(screen
);
137 ERRPRINT("Reading: %fs\n",
138 ((double) (time_end_read
-time_start_read
))/CLOCKS_PER_SEC
);
139 ERRPRINT("Encoding: %fs\n",
140 ((double) (time_end_encode
-time_start_encode
))/CLOCKS_PER_SEC
);
143 int main(int argc
, char **argv
)
147 while((optchar
= getopt(argc
, argv
, "cdhoy")) != -1){
151 DPRINT("Strategy changed to Coordinate based\n");
155 DPRINT("Debug enabled\n");
162 DPRINT("Strategy changed to Object based\n");
166 DPRINT("Strategy changed to Hybrid\n");
170 ERRPRINT("Unknown option `-%c'.\n", optopt
);
172 ERRPRINT("Unknown option char `-\\x%x'.\n", optopt
);
181 ERRPRINT("You have not specified a file, reading from stdin\n");
185 for(int filepathindex
= optind
; filepathindex
< argc
; filepathindex
++){
186 char *currentfilepath
= argv
[filepathindex
];
187 ERRPRINT("Processing: %s\n", currentfilepath
);
188 FILE *currentfile
= fopen(currentfilepath
, "r");
189 DPRINT("Opening file\n");
191 DPRINT("Closing file\n");