13 #define DPRINT(fmt, as...) if(VERBOSE) fprintf(stderr, fmt, ## as);
14 #define REPORT(s, end, start) DPRINT(s, ((double)(end-start))/CLOCKS_PER_SEC);
22 "\t%s [opts] [FILE]\n"
25 "\t-l LURD lURD verification strategy\n"
26 "\t-v enable verbose output\n"
27 "\t-h show this help\n"
29 "Positional arguments:\n"
30 "\tFILE zero or one sokoban screens\n"
31 "\t when no file is specified stdin will be used\n", prg
);
34 BDD
subsolve(trans_t
*t
, BDD
new){
37 new = sylvan_or(new, sylvan_relnext(new, t
->bdd
, t
->varset
.varset
));
43 int solve(FILE *inputstream
, char *lurd
)
45 clock_t time_start_read
, time_end_read
, time_start_scr
, time_end_scr
,
46 time_start_goal
, time_end_goal
, time_start_rel
, time_end_rel
,
47 time_start_solve
, time_end_solve
;
50 time_start_read
= clock();
51 sokoban_screen
*screen
= parse_screen(inputstream
, true);
53 printf("Something went wrong encoding the screen\n");
56 time_end_read
= clock();
58 //Lace and sylvan blork
59 lace_init(0, 1000000);
60 lace_startup(0, NULL
, NULL
);
62 sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
66 time_start_scr
= clock();
67 state
*init
= encode_screen(screen
);
68 time_end_scr
= clock();
71 time_start_goal
= clock();
72 state
*goal
= encode_goal(screen
);
73 time_end_goal
= clock();
76 time_start_rel
= clock();
77 rels
*rls
= encode_rel(screen
);
78 time_end_rel
= clock();
82 time_start_solve
= clock();
83 BDD old
= sylvan_false
;
86 for(unsigned int i
= 0; i
<strlen(lurd
); i
++){
89 new = subsolve(rls
->rell
, new);
92 new = subsolve(rls
->relu
, new);
95 new = subsolve(rls
->relr
, new);
98 new = subsolve(rls
->reld
, new);
101 printf("Unknown character in lucd: '%c'\n", lurd
[i
]);
108 DPRINT("Iteration %d\n", iteration
++);
110 if(sylvan_satcount(sylvan_and(goal
->bdd
, new), init
->vars
.varset
) > 0){
115 //Left, Up, Right, Down moves
116 new = subsolve(rls
->rell
, new);
117 new = subsolve(rls
->relu
, new);
118 new = subsolve(rls
->relr
, new);
119 new = subsolve(rls
->reld
, new);
121 time_end_solve
= clock();
123 //Free and print stats
124 sokoban_free(screen
);
125 REPORT("Reading: %fs\n", time_end_read
, time_start_read
);
126 REPORT("Screen encoding: %fs\n", time_end_scr
, time_start_scr
);
127 REPORT("Goal encoding: %fs\n", time_end_goal
, time_start_goal
);
128 REPORT("Relation encoding: %fs\n", time_end_rel
, time_start_rel
);
129 REPORT("Solving encoding: %fs\n", time_end_solve
, time_start_solve
);
132 printf("no solution\n");
138 int main(int argc
, char **argv
)
143 while((optchar
= getopt(argc
, argv
, "vhl:")) != -1){
146 DPRINT("Lurd detected: `%s'\n", optarg
);
151 DPRINT("Debug enabled\n");
158 DPRINT("Skipping unknown option `-%c'.\n", optopt
);
160 DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt
);
169 DPRINT("You have not specified a file, reading from stdin\n");
170 return solve(stdin
, lurd
);
172 DPRINT("Processing: %s\n", argv
[optind
]);
173 FILE *currentfile
= fopen(argv
[optind
], "r");
174 if(currentfile
== NULL
){
175 printf("File could not be opened\n");
178 DPRINT("Opening file\n");
179 return solve(currentfile
, lurd
);
180 DPRINT("Closing file\n");