bimap helper added

[mc1516pa.git] / modelchecker / main.c

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 16dd229..e954c07 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -2,19 +2,26 @@
 #include <stdbool.h>
 #include <ctype.h>
 #include <time.h>
+#include <unistd.h>
 
 #include <sylvan.h>
 
-#include "mc.h"
 #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){
-       fprintf(stderr, 
-               "Usage:\n"
+void usage(char *prg)
+{
+       ERRPRINT("Usage:\n"
                "\t%s [opts] [FILE [FILE [...]]]\n"
                "\n"
                "Options:\n"
@@ -33,68 +40,82 @@ void usage(char *prg){
                "\t         when no file is specified stdin will be used\n", prg);
 }
 
-void solve(FILE *inputstream){
+void solve(FILE *inputstream)
+{
        clock_t time_start_read, time_end_read;
        clock_t time_start_encode, time_end_encode;
 
        time_start_read = clock();
-       //struct sokoban_screen *screen = parse_screen(inputstream);
-       parse_screen(inputstream);
+       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:
-               if(DEBUG) fprintf(stderr, "Encoding coordinate based\n");
-               break;
-       case OBJECT:
-               if(DEBUG) fprintf(stderr, "Encoding object based\n");
-               break;
-       case HYBRID:
-               if(DEBUG) fprintf(stderr, "Encoding hybrid based\n");
-               break;
-       default:
-               fprintf(stderr, "Huh?");
-               exit(2);
+               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();
-       
-       // Future: SMC
-       fprintf(stderr, "Reading: %fs\n",
+
+       //SOLVE???
+
+       ERRPRINT("Reading: %fs\n",
                ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
-       fprintf(stderr, "Encoding: %fs\n",
+       ERRPRINT("Encoding: %fs\n",
                ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
 }
 
-int main(int argc, char **argv){
+int main(int argc, char **argv)
+{
        int optchar;
 
        while((optchar = getopt(argc, argv, "cdhoy")) != -1){
                switch(optchar){
                case 'c':
                        strat = COORD;
-                       if(DEBUG) fprintf(stderr, "Strategy changed to Coordinate based\n");
+                       DPRINT("Strategy changed to Coordinate based\n");
                        break;
                case 'd':
                        DEBUG = true;
-                       if(DEBUG) fprintf(stderr, "Debug enabled\n");
+                       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");
+                       DPRINT("Strategy changed to Object based\n");
                        break;
                case 'y':
                        strat = HYBRID;
-                       if(DEBUG) fprintf(stderr, "Strategy changed to Hybrid\n");
+                       DPRINT("Strategy changed to Hybrid\n");
                        break;
                case '?':
                        if(isprint(optopt)){
-                               fprintf(stderr, "Unknown option `-%c'.\n", optopt);
+                               ERRPRINT("Unknown option `-%c'.\n", optopt);
                        } else {
-                               fprintf(stderr, "Unknown option char `-\\x%x'.\n", optopt);
+                               ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
                        }
                        return 2;
                default:
@@ -103,17 +124,17 @@ int main(int argc, char **argv){
        }
 
        if(optind == argc){
-               fprintf(stderr, "You have not specified a file, reading from stdin\n");
+               ERRPRINT("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);
+               ERRPRINT("Processing: %s\n", currentfilepath);
                FILE *currentfile = fopen(currentfilepath, "r");
-               if(DEBUG) fprintf(stderr, "Opening file\n");
+               DPRINT("Opening file\n");
                solve(currentfile);
-               if(DEBUG) fprintf(stderr, "Closing file\n");
+               DPRINT("Closing file\n");
                fclose(currentfile);
        }
        return 0;