void usage(char *prg)
{
- ERRPRINT("Usage:\n"
- "\t%s [opts] [FILE [FILE [...]]]\n"
+ printf("Usage:\n"
+ "\t%s [opts] [FILE]\n"
"\n"
"Options:\n"
- "\tAll strategies are mutually exclusive\n"
- "\t-c coordinate based strategy\n"
- "\t-o object based strategy\n"
- "\t-y hybrid strategy\n"
--// "\t-l LURD lURD verification strategy\n"
- // "\t-r show all positions that are a valid solution\n"
-// "\t-r show all positions that are a valid solution\n"
-- "\n"
- "\t-d enable verbose debug output\n"
- "\t-h show this help\n"
++ "\t-l LURD lURD verification strategy\n"
+ "\t-v enable verbose output\n"
+ "\t-h show this help\n"
"\n"
"Positional arguments:\n"
- "\tFILE zero or more sokoban screens\n"
- "\t when no file is specified stdin will be used\n", prg);
+ "\tFILE zero or one sokoban screens\n"
+ "\t when no file is specified stdin will be used\n", prg);
}
-int lurd_solve(FILE *inputstream, char *lurd){
-
- sokoban_screen *screen = parse_screen(inputstream, false);
- if (screen == NULL) printf("Something went wrong...\n");
-
- lace_init(0, 1000000);
- lace_startup(0, NULL, NULL);
+BDD subsolve(trans_t *t, BDD new){
LACE_ME;
- sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
- sylvan_init_bdd(6);
-
- state *init = encode_screen(screen);
- state *goal = encode_goal(screen);
- if (goal == NULL) printf("WRONG\n");
- rels *rls = encode_rel(screen);
- BDD new = init->bdd;
- trans_t *t = NULL;
-
- while (*lurd != '\n'){
- printf("We're here1\n");
- switch(*lurd){
- case 'l':
- printf("We're here2\n");
- t = rls->rell;
- while (t != NULL){
- new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
- t = t->next_rel;
- }
- lurd++;
- break;
- case 'u':
- t = rls->relu;
- while (t != NULL){
- new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
- t = t->next_rel;
- }
- lurd++;
- break;
- case 'r':
- t = rls->relr;
- while (t != NULL){
- new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
- t = t->next_rel;
- }
- lurd++;
- break;
- case 'd':
- t = rls->reld;
- while (t != NULL){
- new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
- t = t->next_rel;
- }
- lurd++;
- break;
- default: lurd++;
- }
-
- }
-
- double check = 0;
- if (goal != NULL) {
- check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset);
- }
- if (check > 0) return 1;
- else return 0;
+ while (t != NULL){
+ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+ t = t->next_rel;
+ }
+ return new;
}
- int solve(FILE *inputstream)
-void solve(FILE *inputstream)
++int solve(FILE *inputstream, char *lurd)
{
- clock_t time_start_read, time_end_read;
- clock_t time_start_encode, time_end_encode;
+ clock_t time_start_read, time_end_read, time_start_scr, time_end_scr,
+ time_start_goal, time_end_goal, time_start_rel, time_end_rel,
+ time_start_solve, time_end_solve;
+ //Read screen
time_start_read = clock();
sokoban_screen *screen = parse_screen(inputstream, false);
- if (screen == NULL) printf("Something went wrong...\n");
- //sokoban_print(screen);
+ if (screen == NULL) {
+ printf("Something went wrong encoding the screen\n");
+ return 2;
+ }
time_end_read = clock();
- time_start_encode = clock();
-
+ //Lace and sylvan blork
lace_init(0, 1000000);
lace_startup(0, NULL, NULL);
LACE_ME;
- sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
- sylvan_init_bdd(6);
+ sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
+ sylvan_init_bdd(6);
+ //Encode screen
+ time_start_scr = clock();
state *init = encode_screen(screen);
- state *goal = encode_goal(screen);
+ time_end_scr = clock();
+
+ //Encode goal
+ time_start_goal = clock();
+ state *goal = encode_goal(screen);
+ time_end_goal = clock();
+
+ //Encode transitions
+ time_start_rel = clock();
rels *rls = encode_rel(screen);
- /*
- printf("Doing left\n");
- test_trans(init, rls->rell);
- printf("Doing up\n");
- test_trans(init, rls->relu);
- printf("Doing right\n");
- test_trans(init, rls->relr);
- printf("Doing down\n");
- test_trans(init, rls->reld);
- */
+ time_end_rel = clock();
+
+
+ //Actually solve
+ time_start_solve = clock();
BDD old = sylvan_false;
BDD new = init->bdd;
++ //Do lurd
++ while(*lurd != '\0'){
++ switch(*lurd){
++ case 'l':
++ new = subsolve(rls->rell, new);
++ break;
++ case 'u':
++ new = subsolve(rls->relu, new);
++ break;
++ case 'r':
++ new = subsolve(rls->relr, new);
++ break;
++ case 'd':
++ new = subsolve(rls->reld, new);
++ break;
++ default:
++ printf("Unknown character in lucd: '%c'\n", *lurd);
++ exit(2);
++ }
++ lurd++;
++ }
int iteration = 0;
- if (goal != NULL){
- while(new != old){
- old = new;
- ERRPRINT("Iteration %d\n", iteration++);
- trans_t *t = rls->rell;
-
- //for testing
- /*
- BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9);
- BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0});
- BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0}));
- BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1}));
- if (new == teststate2) printf("Wrong!\n");
- */
- while (t != NULL){
- new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
- t = t->next_rel;
- //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
- }
-
- t = rls->relu;
- while (t != NULL){
- new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
- t = t->next_rel;
- //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
- }
-
-
- t = rls->relr;
- while (t != NULL){
- new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
- t = t->next_rel;
- //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
- }
-
-
- t = rls->reld;
- while (t != NULL){
- new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
- t = t->next_rel;
- //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
- }
- double check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset);
- if (check > 0){
- printf("Solution is found after %d iteration(s)!\n", iteration);
- break;
- }
- }
- }
- else printf("No solution found!\n");
- //ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
-// sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);
-// sylvan_printdot_nc(old);
- time_end_encode = clock();
+ bool found = false;
+ while(new != old){
+ DPRINT("Iteration %d\n", iteration++);
+ old = new;
+ if(sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset) > 0){
+ found = true;
+ break;
+ }
- //SOLVE???
+ //Left, Up, Right, Down moves
+ new = subsolve(rls->rell, new);
+ new = subsolve(rls->relu, new);
+ new = subsolve(rls->relr, new);
+ new = subsolve(rls->reld, new);
+ }
+ time_end_solve = clock();
+ //Free and print stats
sokoban_free(screen);
- ERRPRINT("Reading: %fs\n",
- ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
- ERRPRINT("Encoding: %fs\n",
- ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
+ REPORT("Reading: %fs\n", time_end_read, time_start_read);
+ REPORT("Screen encoding: %fs\n", time_end_scr, time_start_scr);
+ 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);
+
+ if(!found){
+ printf("no solution\n");
+ return 1;
+ }
+ return 0;
}
int main(int argc, char **argv)
{
int optchar;
++ char *lurd = "";
- while((optchar = getopt(argc, argv, "vh")) != -1){
- while((optchar = getopt(argc, argv, "cdhoy")) != -1){
++ while((optchar = getopt(argc, argv, "vhl:")) != -1){
switch(optchar){
- case 'c':
- strat = COORD;
- DPRINT("Strategy changed to Coordinate based\n");
++ case 'l':
++ DPRINT("Lurd detected: `%s'\n", optarg);
++ lurd = optarg;
+ break;
- case 'd':
- DEBUG = true;
+ case 'v':
+ VERBOSE = true;
DPRINT("Debug enabled\n");
break;
case 'h':
}
if(optind == argc){
- ERRPRINT("You have not specified a file, reading from stdin\n");
- //solve(stdin);
- char lrd[] = "ll\n";
- if (lurd_solve(stdin, lrd) == 1) printf ("The given lurd solves the given screen\n");
- else printf ("The given lurd can not solve the given screen\n");
- }
-
- for(int filepathindex = optind; filepathindex < argc; filepathindex++){
- char *currentfilepath = argv[filepathindex];
- ERRPRINT("Processing: %s\n", currentfilepath);
- FILE *currentfile = fopen(currentfilepath, "r");
+ DPRINT("You have not specified a file, reading from stdin\n");
- return solve(stdin);
++ return solve(stdin, lurd);
+ } else {
+ DPRINT("Processing: %s\n", argv[optind]);
- DPRINT("Thus skipping the other %d files\n", argc-optind);
+ FILE *currentfile = fopen(argv[optind], "r");
DPRINT("Opening file\n");
- return solve(currentfile);
- solve(currentfile);
++ return solve(currentfile, lurd);
DPRINT("Closing file\n");
fclose(currentfile);
}
repositories / mc1516pa.git / commitdiff