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 #include "object.h"
  12
  13 #define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
  14 #define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
  15
  16 typedef enum {OBJECT, COORD, HYBRID} strategy;
  17
  18 //Global variables
  19 bool DEBUG = false;
  20 strategy strat = HYBRID;
  21
  22 void usage(char *prg)
  23 {
  24         ERRPRINT("Usage:\n"
  25                 "\t%s [opts] [FILE [FILE [...]]]\n"
  26                 "\n"
  27                 "Options:\n"
  28                 "\tAll strategies are mutually exclusive\n"
  29                 "\t-c       coordinate based strategy\n"
  30                 "\t-o       object based strategy\n"
  31                 "\t-y       hybrid strategy\n"
  32 //              "\t-l LURD  lURD verification strategy\n"
  33 //              "\t-r       show all positions that are a valid solution\n"
  34                 "\n"
  35                 "\t-d       enable verbose debug output\n"
  36                 "\t-h       show this help\n"
  37                 "\n"
  38                 "Positional arguments:\n"
  39                 "\tFILE     zero or more sokoban screens\n"
  40                 "\t         when no file is specified stdin will be used\n", prg);
  41 }
  42
  43 void solve(FILE *inputstream)
  44 {
  45         clock_t time_start_read, time_end_read;
  46         clock_t time_start_encode, time_end_encode;
  47
  48         time_start_read = clock();
  49         sokoban_screen *screen = parse_screen(inputstream, false);
  50         if (screen == NULL) printf("Something went wrong...\n");
  51         //sokoban_print(screen);
  52         time_end_read = clock();
  53
  54         time_start_encode = clock();
  55
  56         lace_init(0, 1000000);
  57         lace_startup(0, NULL, NULL);
  58         LACE_ME;
  59     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
  60     sylvan_init_bdd(6);
  61
  62         state *init = encode_screen(screen);
  63     state *goal = encode_goal(screen);
  64         rels *rls = encode_rel(screen);
  65     /*
  66     printf("Doing left\n");
  67     test_trans(init, rls->rell);
  68     printf("Doing up\n");
  69     test_trans(init, rls->relu);
  70     printf("Doing right\n");
  71     test_trans(init, rls->relr);
  72     printf("Doing down\n");
  73     test_trans(init, rls->reld);
  74     */
  75
  76         BDD old = sylvan_false;
  77         BDD new = init->bdd;
  78         int iteration = 0;
  79     if (goal != NULL){
  80         while(new != old){
  81             old = new;
  82             ERRPRINT("Iteration %d\n", iteration++);
  83             trans_t *t = rls->rell;
  84
  85             //for testing
  86             /*
  87               BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9);
  88               BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0});
  89               BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0}));
  90               BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1}));
  91               if (new == teststate2) printf("Wrong!\n");
  92             */
  93             while (t != NULL){
  94                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
  95                 t = t->next_rel;
  96                 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
  97             }
  98
  99             t = rls->relu;
 100             while (t != NULL){
 101                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 102                 t = t->next_rel;
 103                 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
 104             }
 105
 106
 107             t = rls->relr;
 108             while (t != NULL){
 109                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 110                 t = t->next_rel;
 111                 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
 112             }
 113
 114
 115             t = rls->reld;
 116             while (t != NULL){
 117                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 118                 t = t->next_rel;
 119                 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
 120             }
 121             double check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset);
 122             if (check > 0){
 123                 printf("Solution is found after %d iteration(s)!\n", iteration);
 124                 break;
 125             }
 126         }
 127         printf("Solution is not found after %d iteration(s)\n", iteration);
 128     }
 129     else printf("No solution found!\n");
 130         //ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
 131 //      sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);
 132 //      sylvan_printdot_nc(old);
 133         time_end_encode = clock();
 134
 135         //SOLVE???
 136
 137         sokoban_free(screen);
 138         ERRPRINT("Reading: %fs\n",
 139                 ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
 140         ERRPRINT("Encoding: %fs\n",
 141                 ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
 142 }
 143
 144 int main(int argc, char **argv)
 145 {
 146         int optchar;
 147
 148         while((optchar = getopt(argc, argv, "cdhoy")) != -1){
 149                 switch(optchar){
 150                 case 'c':
 151                         strat = COORD;
 152                         DPRINT("Strategy changed to Coordinate based\n");
 153                         break;
 154                 case 'd':
 155                         DEBUG = true;
 156                         DPRINT("Debug enabled\n");
 157                         break;
 158                 case 'h':
 159                         usage(argv[0]);
 160                         return 0;
 161                 case 'o':
 162                         strat = OBJECT;
 163                         DPRINT("Strategy changed to Object based\n");
 164                         break;
 165                 case 'y':
 166                         strat = HYBRID;
 167                         DPRINT("Strategy changed to Hybrid\n");
 168                         break;
 169                 case '?':
 170                         if(isprint(optopt)){
 171                                 ERRPRINT("Unknown option `-%c'.\n", optopt);
 172                         } else {
 173                                 ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
 174                         }
 175                         return 2;
 176                 default:
 177                         break;
 178                 }
 179         }
 180
 181         if(optind == argc){
 182                 ERRPRINT("You have not specified a file, reading from stdin\n");
 183                 solve(stdin);
 184         }
 185
 186         for(int filepathindex = optind; filepathindex < argc; filepathindex++){
 187                 char *currentfilepath = argv[filepathindex];
 188                 ERRPRINT("Processing: %s\n", currentfilepath);
 189                 FILE *currentfile = fopen(currentfilepath, "r");
 190                 DPRINT("Opening file\n");
 191                 solve(currentfile);
 192                 DPRINT("Closing file\n");
 193                 fclose(currentfile);
 194         }
 195         return 0;
 196 }