#include <stdio.h>
#include <stdbool.h>
#include <ctype.h>
+#include <time.h>
+#include <unistd.h>
#include <sylvan.h>
-#include "mc.h"
-//#include <sokoban.h>
-//#include <object.h>
-//#include <coord.h>
+#include "sokoban.h"
+#include "coord.h"
+#include "object.h"
-bool DEBUG = false;
+#define DPRINT(fmt, as...) if(VERBOSE) fprintf(stderr, fmt, ## as);
+#define REPORT(s, end, start) DPRINT(s, ((double)(end-start))/CLOCKS_PER_SEC);
-void usage(char *prg){
- fprintf(stderr,
- "Usage:\n"
- "\t%s [opts] [FILE [FILE [...]]]\n"
+//Global variables
+bool VERBOSE = false;
+
+void usage(char *prg)
+{
+ 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"
- "\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);
+}
+
+BDD subsolve(trans_t *t, BDD new){
+ LACE_ME;
+ while (t != NULL){
+ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+ t = t->next_rel;
+ }
+ return new;
}
-void solve(FILE *inputstream){
- int buffer;
- while((buffer = fgetc(inputstream)) != EOF){
- printf("%c", buffer);
+int solve(FILE *inputstream, char *lurd)
+{
+ 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 encoding the screen\n");
+ return 2;
+ }
+ time_end_read = 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);
+
+ //Encode screen
+ time_start_scr = clock();
+ state *init = encode_screen(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);
+ 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 lurd: '%c'\n", *lurd);
+ exit(2);
+ }
+ lurd++;
+ }
+ int iteration = 0;
+ 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;
+ }
+
+ //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);
}
- // Alex:
- // Screen reading
- // - Removing outside walls
- // - Bucket fill
- // - [tile]
- // - tile = structure {int, int, enumtile}
-
- // Both: Encoding in both schemes
-
- // Future: SMC
+ time_end_solve = clock();
+
+ //Free and print stats
+ sokoban_free(screen);
+ 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){
- strategy strat = HYBRID;
+int main(int argc, char **argv)
+{
int optchar;
+ char *lurd = "";
- while((optchar = getopt(argc, argv, "cdhoy")) != -1){
+ while((optchar = getopt(argc, argv, "vhl:")) != -1){
switch(optchar){
- case 'c':
- strat = COORD;
- if(DEBUG) fprintf(stderr, "Strategy changed to Coordinate based\n");
+ case 'l':
+ DPRINT("Lurd detected: `%s'\n", optarg);
+ lurd = optarg;
break;
- case 'd':
- DEBUG = true;
- if(DEBUG) fprintf(stderr, "Debug enabled\n");
+ case 'v':
+ VERBOSE = true;
+ DPRINT("Debug enabled\n");
break;
case 'h':
usage(argv[0]);
return 0;
- case 'o':
- strat = OBJECT;
- if(DEBUG) fprintf(stderr, "Strategy changed to Object based\n");
- break;
- case 'y':
- strat = HYBRID;
- if(DEBUG) fprintf(stderr, "Strategy changed to Hybrid\n");
- break;
case '?':
if(isprint(optopt)){
- fprintf(stderr, "Unknown option `-%c'.\n", optopt);
+ DPRINT("Skipping unknown option `-%c'.\n", optopt);
} else {
- fprintf(stderr, "Unknown option char `-\\x%x'.\n", optopt);
+ DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt);
}
return 2;
default:
}
if(optind == argc){
- fprintf(stderr, "You have not specified a file, reading from stdin\n");
- solve(stdin);
- }
-
- for(int filepathindex = optind; filepathindex < argc; filepathindex++){
- char *currentfilepath = argv[filepathindex];
- fprintf(stderr, "Processing: %s\n", currentfilepath);
- if(DEBUG) fprintf(stderr, "Strategy: %d\n", strat);
- FILE *currentfile = fopen(currentfilepath, "r");
- if(DEBUG) fprintf(stderr, "Opening file\n");
- solve(currentfile);
- if(DEBUG) fprintf(stderr, "Closing file\n");
+ DPRINT("You have not specified a file, reading from stdin\n");
+ return solve(stdin, lurd);
+ } else {
+ DPRINT("Processing: %s\n", argv[optind]);
+ FILE *currentfile = fopen(argv[optind], "r");
+ DPRINT("Opening file\n");
+ return solve(currentfile, lurd);
+ DPRINT("Closing file\n");
fclose(currentfile);
}
- return 0;
}