12 #define DPRINT(fmt, as...) if(VERBOSE) fprintf(stderr, fmt, ## as);
13 #define REPORT(s, end, start) DPRINT(s, ((double)(end-start))/CLOCKS_PER_SEC);
21 "\t%s [opts] [FILE]\n"
24 "\t-l LURD initial LURD\n"
25 "\t-v enable verbose output\n"
26 "\t-h show this help\n"
28 "Positional arguments:\n"
29 "\tFILE zero or one sokoban screens\n"
30 "\t when no file is specified stdin will be used\n", prg
);
33 BDD
subsolve(trans_t
*t
, BDD
new){
36 new = sylvan_or(new, sylvan_relnext(new, t
->bdd
, t
->varset
.varset
));
42 int solve(FILE *inputstream
, char *lurd
)
44 clock_t time_start_read
, time_end_read
, time_start_scr
, time_end_scr
,
45 time_start_goal
, time_end_goal
, time_start_rel
, time_end_rel
,
46 time_start_solve
, time_end_solve
;
49 time_start_read
= clock();
50 sokoban_screen
*screen
= parse_screen(inputstream
, true);
52 printf("Something went wrong encoding the screen\n");
55 time_end_read
= clock();
57 //Lace and sylvan blork
58 lace_init(0, 1000000);
59 lace_startup(0, NULL
, NULL
);
61 sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
65 time_start_scr
= clock();
66 state
*init
= encode_screen(screen
);
67 time_end_scr
= clock();
70 time_start_goal
= clock();
71 state
*goal
= encode_goal(screen
);
72 time_end_goal
= clock();
75 time_start_rel
= clock();
76 rels
*rls
= encode_rel(screen
);
77 time_end_rel
= clock();
80 time_start_solve
= clock();
81 BDD old
= sylvan_false
;
87 new = subsolve(rls
->rell
, new);
90 new = subsolve(rls
->relu
, new);
93 new = subsolve(rls
->relr
, new);
96 new = subsolve(rls
->reld
, new);
99 printf("Unknown character in lurd: '%c'\n", *lurd
);
109 DPRINT("Iteration %d\n", iteration
++);
111 if(sylvan_satcount(sylvan_and(goal
->bdd
, new), init
->vars
.varset
) > 0){
116 //Left, Up, Right, Down moves
117 new = subsolve(rls
->rell
, new);
118 new = subsolve(rls
->relu
, new);
119 new = subsolve(rls
->relr
, new);
120 new = subsolve(rls
->reld
, new);
123 time_end_solve
= clock();
125 //Free and print stats
126 sokoban_free(screen
);
127 REPORT("Reading: %fs\n", time_end_read
, time_start_read
);
128 REPORT("Screen encoding: %fs\n", time_end_scr
, time_start_scr
);
129 REPORT("Goal encoding: %fs\n", time_end_goal
, time_start_goal
);
130 REPORT("Relation encoding: %fs\n", time_end_rel
, time_start_rel
);
131 REPORT("Solving encoding: %fs\n", time_end_solve
, time_start_solve
);
132 DPRINT("Iterations needed: %d\n", iteration
);
135 printf("no solution\n");
142 int main(int argc
, char **argv
)
147 while((optchar
= getopt(argc
, argv
, "vhl:")) != -1){
150 DPRINT("Lurd detected: `%s'\n", optarg
);
155 DPRINT("Debug enabled\n");
162 DPRINT("Skipping unknown option `-%c'.\n", optopt
);
164 DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt
);
173 DPRINT("You have not specified a file, reading from stdin\n");
174 return solve(stdin
, lurd
);
176 DPRINT("Processing: %s\n", argv
[optind
]);
177 FILE *currentfile
= fopen(argv
[optind
], "r");
178 DPRINT("Opening file\n");
179 return solve(currentfile
, lurd
);
180 DPRINT("Closing file\n");