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