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 int lurd_solve(FILE *inputstream, char *lurd){
  44
  45         sokoban_screen *screen = parse_screen(inputstream, false);
  46         if (screen == NULL) printf("Something went wrong...\n");
  47
  48         lace_init(0, 1000000);
  49         lace_startup(0, NULL, NULL);
  50         LACE_ME;
  51     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
  52     sylvan_init_bdd(6);
  53
  54         state *init = encode_screen(screen);
  55     state *goal = encode_goal(screen);
  56     if (goal == NULL) printf("WRONG\n");
  57         rels *rls = encode_rel(screen);
  58         BDD new = init->bdd;
  59     trans_t *t = NULL;
  60
  61     while (*lurd != '\n'){
  62         printf("We're here1\n");
  63         switch(*lurd){
  64         case 'l':
  65             printf("We're here2\n");
  66             t = rls->rell;
  67             while (t != NULL){
  68                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
  69                 t = t->next_rel;
  70             }
  71             lurd++;
  72             break;
  73         case 'u':
  74             t = rls->relu;
  75             while (t != NULL){
  76                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
  77                 t = t->next_rel;
  78             }
  79             lurd++;
  80             break;
  81         case 'r':
  82             t = rls->relr;
  83             while (t != NULL){
  84                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
  85                 t = t->next_rel;
  86             }
  87             lurd++;
  88             break;
  89         case 'd':
  90             t = rls->reld;
  91             while (t != NULL){
  92                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
  93                 t = t->next_rel;
  94             }
  95             lurd++;
  96             break;
  97         default: lurd++;
  98         }
  99
 100     }
 101
 102     double check = 0;
 103     if (goal != NULL) {
 104         check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset);
 105     }
 106     if (check > 0) return 1;
 107     else return 0;
 108 }
 109
 110 void solve(FILE *inputstream)
 111 {
 112         clock_t time_start_read, time_end_read;
 113         clock_t time_start_encode, time_end_encode;
 114
 115         time_start_read = clock();
 116         sokoban_screen *screen = parse_screen(inputstream, false);
 117         if (screen == NULL) printf("Something went wrong...\n");
 118         //sokoban_print(screen);
 119         time_end_read = clock();
 120
 121         time_start_encode = clock();
 122
 123         lace_init(0, 1000000);
 124         lace_startup(0, NULL, NULL);
 125         LACE_ME;
 126     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
 127     sylvan_init_bdd(6);
 128
 129         state *init = encode_screen(screen);
 130     state *goal = encode_goal(screen);
 131         rels *rls = encode_rel(screen);
 132     /*
 133     printf("Doing left\n");
 134     test_trans(init, rls->rell);
 135     printf("Doing up\n");
 136     test_trans(init, rls->relu);
 137     printf("Doing right\n");
 138     test_trans(init, rls->relr);
 139     printf("Doing down\n");
 140     test_trans(init, rls->reld);
 141     */
 142
 143         BDD old = sylvan_false;
 144         BDD new = init->bdd;
 145         int iteration = 0;
 146     if (goal != NULL){
 147         while(new != old){
 148             old = new;
 149             ERRPRINT("Iteration %d\n", iteration++);
 150             trans_t *t = rls->rell;
 151
 152             //for testing
 153             /*
 154               BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9);
 155               BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0});
 156               BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0}));
 157               BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1}));
 158               if (new == teststate2) printf("Wrong!\n");
 159             */
 160             while (t != NULL){
 161                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 162                 t = t->next_rel;
 163                 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
 164             }
 165
 166             t = rls->relu;
 167             while (t != NULL){
 168                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 169                 t = t->next_rel;
 170                 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
 171             }
 172
 173
 174             t = rls->relr;
 175             while (t != NULL){
 176                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 177                 t = t->next_rel;
 178                 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
 179             }
 180
 181
 182             t = rls->reld;
 183             while (t != NULL){
 184                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 185                 t = t->next_rel;
 186                 //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
 187             }
 188             double check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset);
 189             if (check > 0){
 190                 printf("Solution is found after %d iteration(s)!\n", iteration);
 191                 break;
 192             }
 193         }
 194     }
 195     else printf("No solution found!\n");
 196         //ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
 197 //      sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);
 198 //      sylvan_printdot_nc(old);
 199         time_end_encode = clock();
 200
 201         //SOLVE???
 202
 203         sokoban_free(screen);
 204         ERRPRINT("Reading: %fs\n",
 205                 ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
 206         ERRPRINT("Encoding: %fs\n",
 207                 ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
 208 }
 209
 210 int main(int argc, char **argv)
 211 {
 212         int optchar;
 213
 214         while((optchar = getopt(argc, argv, "cdhoy")) != -1){
 215                 switch(optchar){
 216                 case 'c':
 217                         strat = COORD;
 218                         DPRINT("Strategy changed to Coordinate based\n");
 219                         break;
 220                 case 'd':
 221                         DEBUG = true;
 222                         DPRINT("Debug enabled\n");
 223                         break;
 224                 case 'h':
 225                         usage(argv[0]);
 226                         return 0;
 227                 case 'o':
 228                         strat = OBJECT;
 229                         DPRINT("Strategy changed to Object based\n");
 230                         break;
 231                 case 'y':
 232                         strat = HYBRID;
 233                         DPRINT("Strategy changed to Hybrid\n");
 234                         break;
 235                 case '?':
 236                         if(isprint(optopt)){
 237                                 ERRPRINT("Unknown option `-%c'.\n", optopt);
 238                         } else {
 239                                 ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
 240                         }
 241                         return 2;
 242                 default:
 243                         break;
 244                 }
 245         }
 246
 247         if(optind == argc){
 248                 ERRPRINT("You have not specified a file, reading from stdin\n");
 249                 //solve(stdin);
 250         char lrd[] = "ll\n";
 251         if (lurd_solve(stdin, lrd) == 1) printf ("The given lurd solves the given screen\n");
 252         else printf ("The given lurd can not solve the given screen\n");
 253         }
 254
 255         for(int filepathindex = optind; filepathindex < argc; filepathindex++){
 256                 char *currentfilepath = argv[filepathindex];
 257                 ERRPRINT("Processing: %s\n", currentfilepath);
 258                 FILE *currentfile = fopen(currentfilepath, "r");
 259                 DPRINT("Opening file\n");
 260                 solve(currentfile);
 261                 DPRINT("Closing file\n");
 262                 fclose(currentfile);
 263         }
 264         return 0;
 265 }