#include "sokoban.h"
#include "coord.h"
-#include "object.h"
#define DPRINT(fmt, as...) if(VERBOSE) fprintf(stderr, fmt, ## as);
#define REPORT(s, end, start) DPRINT(s, ((double)(end-start))/CLOCKS_PER_SEC);
"\t%s [opts] [FILE]\n"
"\n"
"Options:\n"
- "\t-l LURD lURD verification strategy\n"
+ "\t-l LURD initial LURD\n"
"\t-v enable verbose output\n"
"\t-h show this help\n"
"\n"
rels *rls = encode_rel(screen);
time_end_rel = clock();
-
//Actually solve
time_start_solve = clock();
BDD old = sylvan_false;
BDD new = init->bdd;
//Do lurd
- for(unsigned int i = 0; i<strlen(lurd); i++){
- switch(lurd[i]){
+ while(*lurd != '\0'){
+ switch(*lurd){
case 'l':
new = subsolve(rls->rell, new);
break;
new = subsolve(rls->reld, new);
break;
default:
- printf("Unknown character in lucd: '%c'\n", lurd[i]);
+ printf("Unknown character in lurd: '%c'\n", *lurd);
exit(2);
}
+ lurd++;
}
int iteration = 0;
+
bool found = false;
+
while(new != old){
DPRINT("Iteration %d\n", iteration++);
old = new;
new = subsolve(rls->relr, new);
new = subsolve(rls->reld, new);
}
+
time_end_solve = clock();
//Free and print stats
REPORT("Goal encoding: %fs\n", time_end_goal, time_start_goal);
REPORT("Relation encoding: %fs\n", time_end_rel, time_start_rel);
REPORT("Solving encoding: %fs\n", time_end_solve, time_start_solve);
+ DPRINT("Iterations needed: %d\n", iteration);
if(!found){
printf("no solution\n");
return 1;
}
+ DPRINT("Solution found\n");
return 0;
}