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 DPRINT(fmt, as...) if(VERBOSE) fprintf(stderr, fmt, ## as);
  13 #define REPORT(s, end, start) DPRINT(s, ((double)(end-start))/CLOCKS_PER_SEC);
  14
  15 //Global variables
  16 bool VERBOSE = false;
  17
  18 void usage(char *prg)
  19 {
  20         printf("Usage:\n"
  21                 "\t%s [opts] [FILE]\n"
  22                 "\n"
  23                 "Options:\n"
  24                 "\t-l LURD initial LURD\n"
  25                 "\t-v      enable verbose output\n"
  26                 "\t-h      show this help\n"
  27                 "\n"
  28                 "Positional arguments:\n"
  29                 "\tFILE  zero or one sokoban screens\n"
  30                 "\t              when no file is specified stdin will be used\n", prg);
  31 }
  32
  33 BDD subsolve(trans_t *t, BDD new){
  34         LACE_ME;
  35         while (t != NULL){
  36                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
  37                 t = t->next_rel;
  38         }
  39         return new;
  40 }
  41
  42 int solve(FILE *inputstream, char *lurd)
  43 {
  44         clock_t time_start_read, time_end_read, time_start_scr, time_end_scr,
  45                 time_start_goal, time_end_goal, time_start_rel, time_end_rel,
  46                 time_start_solve, time_end_solve;
  47
  48         //Read screen
  49         time_start_read = clock();
  50         sokoban_screen *screen = parse_screen(inputstream, true);
  51         if (screen == NULL) {
  52                 printf("Something went wrong encoding the screen\n");
  53                 return 2;
  54         }
  55         time_end_read = clock();
  56
  57         //Lace and sylvan blork
  58         lace_init(0, 1000000);
  59         lace_startup(0, NULL, NULL);
  60         LACE_ME;
  61         sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
  62         sylvan_init_bdd(6);
  63
  64         //Encode screen
  65         time_start_scr = clock();
  66         state *init = encode_screen(screen);
  67         time_end_scr = clock();
  68
  69         //Encode goal
  70         time_start_goal = clock();
  71         state *goal = encode_goal(screen);
  72         time_end_goal = clock();
  73
  74         //Encode transitions
  75         time_start_rel = clock();
  76         rels *rls = encode_rel(screen);
  77         time_end_rel = clock();
  78
  79         //Actually solve
  80         time_start_solve = clock();
  81         BDD old = sylvan_false;
  82         BDD new = init->bdd;
  83         //Do lurd
  84         while(*lurd != '\0'){
  85                 switch(*lurd){
  86                 case 'l':
  87                         new = subsolve(rls->rell, new);
  88                         break;
  89         case 'u':
  90                         new = subsolve(rls->relu, new);
  91                         break;
  92                 case 'r':
  93                         new = subsolve(rls->relr, new);
  94                         break;
  95                 case 'd':
  96                         new = subsolve(rls->reld, new);
  97                         break;
  98                 default:
  99                         printf("Unknown character in lurd: '%c'\n", *lurd);
 100                         exit(2);
 101                 }
 102                 lurd++;
 103         }
 104         int iteration = 0;
 105
 106         bool found = false;
 107
 108         while(new != old){
 109                 DPRINT("Iteration %d\n", iteration++);
 110                 old = new;
 111                 if(sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset) > 0){
 112                         found = true;
 113                         break;
 114                 }
 115
 116                 //Left, Up, Right, Down moves
 117                 new = subsolve(rls->rell, new);
 118                 new = subsolve(rls->relu, new);
 119                 new = subsolve(rls->relr, new);
 120                 new = subsolve(rls->reld, new);
 121         }
 122
 123         time_end_solve = clock();
 124
 125         //Free and print stats
 126         sokoban_free(screen);
 127         REPORT("Reading: %fs\n", time_end_read, time_start_read);
 128         REPORT("Screen encoding: %fs\n", time_end_scr, time_start_scr);
 129         REPORT("Goal encoding: %fs\n", time_end_goal, time_start_goal);
 130         REPORT("Relation encoding: %fs\n", time_end_rel, time_start_rel);
 131         REPORT("Solving encoding: %fs\n", time_end_solve, time_start_solve);
 132         DPRINT("Iterations needed: %d\n", iteration);
 133
 134         if(!found){
 135                 printf("no solution\n");
 136                 return 1;
 137         }
 138
 139         return 0;
 140 }
 141
 142 int main(int argc, char **argv)
 143 {
 144         int optchar;
 145         char *lurd = "";
 146
 147         while((optchar = getopt(argc, argv, "vhl:")) != -1){
 148                 switch(optchar){
 149                 case 'l':
 150                         DPRINT("Lurd detected: `%s'\n", optarg);
 151                         lurd = optarg;
 152                         break;
 153                 case 'v':
 154                         VERBOSE = true;
 155                         DPRINT("Debug enabled\n");
 156                         break;
 157                 case 'h':
 158                         usage(argv[0]);
 159                         return 0;
 160                 case '?':
 161                         if(isprint(optopt)){
 162                                 DPRINT("Skipping unknown option `-%c'.\n", optopt);
 163                         } else {
 164                                 DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt);
 165                         }
 166                         return 2;
 167                 default:
 168                         break;
 169                 }
 170         }
 171
 172         if(optind == argc){
 173                 DPRINT("You have not specified a file, reading from stdin\n");
 174                 return solve(stdin, lurd);
 175         } else {
 176                 DPRINT("Processing: %s\n", argv[optind]);
 177                 FILE *currentfile = fopen(argv[optind], "r");
 178                 DPRINT("Opening file\n");
 179                 return solve(currentfile, lurd);
 180                 DPRINT("Closing file\n");
 181                 fclose(currentfile);
 182         }
 183 }