added minimum boxamount, check for crappy file

[mc1516pa.git] / modelchecker / main.c

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 5e89211..06729b1 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -1,8 +1,183 @@
 #include <stdio.h>
+#include <stdbool.h>
+#include <ctype.h>
+#include <time.h>
+#include <unistd.h>
 
 #include <sylvan.h>
 
-int main(void){
-       printf("Hello world!\n");
+#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);
+
+//Global variables
+bool VERBOSE = false;
+
+void usage(char *prg)
+{
+       printf("Usage:\n"
+               "\t%s [opts] [FILE]\n"
+               "\n"
+               "Options:\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 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;
+}
+
+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, true);
+       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
+       for(unsigned int i = 0; i<strlen(lurd); i++){
+               switch(lurd[i]){
+               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[i]);
+                       exit(2);
+               }
+       }
+       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);
+       }
+       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)
+{
+       int optchar;
+       char *lurd = "";
+
+       while((optchar = getopt(argc, argv, "vhl:")) != -1){
+               switch(optchar){
+               case 'l':
+                       DPRINT("Lurd detected: `%s'\n", optarg);
+                       lurd = optarg;
+                       break;
+               case 'v':
+                       VERBOSE = true;
+                       DPRINT("Debug enabled\n");
+                       break;
+               case 'h':
+                       usage(argv[0]);
+                       return 0;
+               case '?':
+                       if(isprint(optopt)){
+                               DPRINT("Skipping unknown option `-%c'.\n", optopt);
+                       } else {
+                               DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt);
+                       }
+                       return 2;
+               default:
+                       break;
+               }
+       }
+
+       if(optind == argc){
+               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");
+               if(currentfile == NULL){
+                       printf("File could not be opened\n");
+                       return 2;
+               }
+               DPRINT("Opening file\n");
+               return solve(currentfile, lurd);
+               DPRINT("Closing file\n");
+               fclose(currentfile);
+       }
+}