modelchecker/main.c

   1 #include <stdio.h>
   2 #include <stdbool.h>
   3 #include <ctype.h>
   4 #include <time.h>
   5 #include <unistd.h>
   6
   7 #include <sylvan.h>
   8
   9 #include "sokoban.h"
  10 #include "coord.h"
  11
  12 #define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
  13 #define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
  14
  15 typedef enum {OBJECT, COORD, HYBRID} strategy;
  16
  17 //Global variables
  18 bool DEBUG = false;
  19 strategy strat = HYBRID;
  20
  21 void usage(char *prg)
  22 {
  23         ERRPRINT("Usage:\n"
  24                 "\t%s [opts] [FILE [FILE [...]]]\n"
  25                 "\n"
  26                 "Options:\n"
  27                 "\tAll strategies are mutually exclusive\n"
  28                 "\t-c       coordinate based strategy\n"
  29                 "\t-o       object based strategy\n"
  30                 "\t-y       hybrid strategy\n"
  31 //              "\t-l LURD  lURD verification strategy\n"
  32 //              "\t-r       show all positions that are a valid solution\n"
  33                 "\n"
  34                 "\t-d       enable verbose debug output\n"
  35                 "\t-h       show this help\n"
  36                 "\n"
  37                 "Positional arguments:\n"
  38                 "\tFILE     zero or more sokoban screens\n"
  39                 "\t         when no file is specified stdin will be used\n", prg);
  40 }
  41
  42 void solve(FILE *inputstream)
  43 {
  44         clock_t time_start_read, time_end_read;
  45         clock_t time_start_encode, time_end_encode;
  46
  47         time_start_read = clock();
  48         sokoban_screen *screen = parse_screen(inputstream);
  49         if (screen == NULL) printf("Something went wrong...\n");
  50         sokoban_print(screen);
  51
  52         time_end_read = clock();
  53         time_start_encode = clock();
  54
  55         lace_init(0, 1000000);
  56         lace_startup(0, NULL, NULL);
  57         LACE_ME;
  58     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
  59     sylvan_init_bdd(6);
  60
  61         encode_screen(screen);
  62
  63         sokoban_free(screen);
  64
  65         switch(strat){
  66                 case COORD:
  67                         DPRINT("Encoding coordinate based\n");
  68                         break;
  69                 case OBJECT:
  70                         DPRINT("Encoding object based\n");
  71                         break;
  72                 case HYBRID:
  73                         DPRINT("Encoding hybrid based\n");
  74                         break;
  75                 default:
  76                         ERRPRINT("Huh?");
  77                         exit(2);
  78         }
  79         time_end_encode = clock();
  80
  81         //SOLVE???
  82
  83         ERRPRINT("Reading: %fs\n",
  84                 ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
  85         ERRPRINT("Encoding: %fs\n",
  86                 ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
  87 }
  88
  89 int main(int argc, char **argv)
  90 {
  91         int optchar;
  92
  93         while((optchar = getopt(argc, argv, "cdhoy")) != -1){
  94                 switch(optchar){
  95                 case 'c':
  96                         strat = COORD;
  97                         DPRINT("Strategy changed to Coordinate based\n");
  98                         break;
  99                 case 'd':
 100                         DEBUG = true;
 101                         DPRINT("Debug enabled\n");
 102                         break;
 103                 case 'h':
 104                         usage(argv[0]);
 105                         return 0;
 106                 case 'o':
 107                         strat = OBJECT;
 108                         DPRINT("Strategy changed to Object based\n");
 109                         break;
 110                 case 'y':
 111                         strat = HYBRID;
 112                         DPRINT("Strategy changed to Hybrid\n");
 113                         break;
 114                 case '?':
 115                         if(isprint(optopt)){
 116                                 ERRPRINT("Unknown option `-%c'.\n", optopt);
 117                         } else {
 118                                 ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
 119                         }
 120                         return 2;
 121                 default:
 122                         break;
 123                 }
 124         }
 125
 126         if(optind == argc){
 127                 ERRPRINT("You have not specified a file, reading from stdin\n");
 128                 solve(stdin);
 129         }
 130
 131         for(int filepathindex = optind; filepathindex < argc; filepathindex++){
 132                 char *currentfilepath = argv[filepathindex];
 133                 ERRPRINT("Processing: %s\n", currentfilepath);
 134                 FILE *currentfile = fopen(currentfilepath, "r");
 135                 DPRINT("Opening file\n");
 136                 solve(currentfile);
 137                 DPRINT("Closing file\n");
 138                 fclose(currentfile);
 139         }
 140         return 0;
 141 }