bimap helper added

[mc1516pa.git] / modelchecker / main.c

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 00f8b32..e954c07 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -1,36 +1,141 @@
 #include <stdio.h>
+#include <stdbool.h>
+#include <ctype.h>
+#include <time.h>
+#include <unistd.h>
 
 #include <sylvan.h>
 
-//#include <sokoban.h>
-//#include <object.h>
-//#include <coord.h>
-//#include <mc.h>
-
-int main(void){
-       // Mart:
-       // Argument parsing
-       // ./main [opts] [FILEPATH [FILEPATH ...]]
-       // -o         Objectbased
-       // -c         Coordinatebased
-       // -y         hYbrid
-       // -h         Help
-       //
-       // FUTURE:
-       // -r         Also compute the set of all reachable solution states
-       // -l LURD    Check if LURD is a valid path
-       //
-       // FILEPATH   Optional input file(s)
-       
-       // Alex:
-       // Screen reading
-       // - Removing outside walls
-       // - Bucket fill
-       // - [tile]
-       // - tile = structure {int, int, enumtile}
-       
-       // Both: Encoding in both schemes
-       
-       // Future: SMC
+#include "sokoban.h"
+#include "coord.h"
+#include "object.h"
+
+#define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
+#define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
+
+typedef enum {OBJECT, COORD, HYBRID} strategy;
+
+//Global variables
+bool DEBUG = false;
+strategy strat = HYBRID;
+
+void usage(char *prg)
+{
+       ERRPRINT("Usage:\n"
+               "\t%s [opts] [FILE [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"
+               "\n"
+               "Positional arguments:\n"
+               "\tFILE     zero or more sokoban screens\n"
+               "\t         when no file is specified stdin will be used\n", prg);
+}
+
+void solve(FILE *inputstream)
+{
+       clock_t time_start_read, time_end_read;
+       clock_t time_start_encode, time_end_encode;
+
+       time_start_read = clock();
+       sokoban_screen *screen = parse_screen(inputstream);
+       if (screen == NULL) printf("Something went wrong...\n");
+       //sokoban_print(screen);
+       time_end_read = clock();
+
+       time_start_encode = clock();
+
+       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);
+       switch(strat){
+               case COORD:
+                       DPRINT("Encoding coordinate based\n");
+                       encode_screen(screen);
+                       break;
+               case OBJECT:
+                       DPRINT("Encoding object based\n");
+                       solve_object(screen);
+                       break;
+               case HYBRID:
+                       DPRINT("Encoding hybrid based\n");
+                       DPRINT("Not implemented yet...\n");
+                       break;
+               default:
+                       ERRPRINT("Huh?");
+                       exit(2);
+       }
+       sokoban_free(screen);
+       time_end_encode = clock();
+
+       //SOLVE???
+
+       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);
+}
+
+int main(int argc, char **argv)
+{
+       int optchar;
+
+       while((optchar = getopt(argc, argv, "cdhoy")) != -1){
+               switch(optchar){
+               case 'c':
+                       strat = COORD;
+                       DPRINT("Strategy changed to Coordinate based\n");
+                       break;
+               case 'd':
+                       DEBUG = true;
+                       DPRINT("Debug enabled\n");
+                       break;
+               case 'h':
+                       usage(argv[0]);
+                       return 0;
+               case 'o':
+                       strat = OBJECT;
+                       DPRINT("Strategy changed to Object based\n");
+                       break;
+               case 'y':
+                       strat = HYBRID;
+                       DPRINT("Strategy changed to Hybrid\n");
+                       break;
+               case '?':
+                       if(isprint(optopt)){
+                               ERRPRINT("Unknown option `-%c'.\n", optopt);
+                       } else {
+                               ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
+                       }
+                       return 2;
+               default:
+                       break;
+               }
+       }
+
+       if(optind == argc){
+               ERRPRINT("You have not specified a file, reading from stdin\n");
+               solve(stdin);
+       }
+
+       for(int filepathindex = optind; filepathindex < argc; filepathindex++){
+               char *currentfilepath = argv[filepathindex];
+               ERRPRINT("Processing: %s\n", currentfilepath);
+               FILE *currentfile = fopen(currentfilepath, "r");
+               DPRINT("Opening file\n");
+               solve(currentfile);
+               DPRINT("Closing file\n");
+               fclose(currentfile);
+       }
        return 0;
 }