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  lURD verification strategy\n"
  26 //              "\t-r      show all positions that are a valid solution\n"
  27                 "\n"
  28                 "\t-v      enable verbose output\n"
  29                 "\t-h      show this help\n"
  30                 "\n"
  31                 "Positional arguments:\n"
  32                 "\tFILE  zero or one sokoban screens\n"
  33                 "\t              when no file is specified stdin will be used\n", prg);
  34 }
  35
  36 BDD subsolve(trans_t *t, BDD new){
  37         LACE_ME;
  38         while (t != NULL){
  39                 new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
  40                 t = t->next_rel;
  41         }
  42         return new;
  43 }
  44
  45 int solve(FILE *inputstream)
  46 {
  47         clock_t time_start_read, time_end_read, time_start_scr, time_end_scr,
  48                 time_start_goal, time_end_goal, time_start_rel, time_end_rel,
  49                 time_start_solve, time_end_solve;
  50
  51         //Read screen
  52         time_start_read = clock();
  53         sokoban_screen *screen = parse_screen(inputstream, false);
  54         if (screen == NULL) {
  55                 printf("Something went wrong encoding the screen\n");
  56                 return 2;
  57         }
  58         time_end_read = clock();
  59
  60         //Lace and sylvan blork
  61         lace_init(0, 1000000);
  62         lace_startup(0, NULL, NULL);
  63         LACE_ME;
  64         sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
  65         sylvan_init_bdd(6);
  66
  67         //Encode screen
  68         time_start_scr = clock();
  69         state *init = encode_screen(screen);
  70         time_end_scr = clock();
  71
  72         //Encode goal
  73         time_start_goal = clock();
  74         state *goal = encode_goal(screen);
  75         time_end_goal = clock();
  76
  77         //Encode transitions
  78         time_start_rel = clock();
  79         rels *rls = encode_rel(screen);
  80         time_end_rel = clock();
  81
  82         //Actually solve
  83         time_start_solve = clock();
  84         BDD old = sylvan_false;
  85         BDD new = init->bdd;
  86         int iteration = 0;
  87         bool found = false;
  88         while(new != old){
  89                 DPRINT("Iteration %d\n", iteration++);
  90                 old = new;
  91                 if(sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset) > 0){
  92                         found = true;
  93                         break;
  94                 }
  95
  96                 //Left, Up, Right, Down moves
  97                 new = subsolve(rls->rell, new);
  98                 new = subsolve(rls->relu, new);
  99                 new = subsolve(rls->relr, new);
 100                 new = subsolve(rls->reld, new);
 101         }
 102         time_end_solve = clock();
 103
 104         //Free and print stats
 105         sokoban_free(screen);
 106         REPORT("Reading: %fs\n", time_end_read, time_start_read);
 107         REPORT("Screen encoding: %fs\n", time_end_scr, time_start_scr);
 108         REPORT("Goal encoding: %fs\n", time_end_goal, time_start_goal);
 109         REPORT("Relation encoding: %fs\n", time_end_rel, time_start_rel);
 110         REPORT("Solving encoding: %fs\n", time_end_solve, time_start_solve);
 111
 112         if(!found){
 113                 printf("no solution\n");
 114                 return 1;
 115         }
 116         return 0;
 117 }
 118
 119 int main(int argc, char **argv)
 120 {
 121         int optchar;
 122
 123         while((optchar = getopt(argc, argv, "vh")) != -1){
 124                 switch(optchar){
 125                 case 'v':
 126                         VERBOSE = true;
 127                         DPRINT("Debug enabled\n");
 128                         break;
 129                 case 'h':
 130                         usage(argv[0]);
 131                         return 0;
 132                 case '?':
 133                         if(isprint(optopt)){
 134                                 DPRINT("Skipping unknown option `-%c'.\n", optopt);
 135                         } else {
 136                                 DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt);
 137                         }
 138                         return 2;
 139                 default:
 140                         break;
 141                 }
 142         }
 143
 144         if(optind == argc){
 145                 DPRINT("You have not specified a file, reading from stdin\n");
 146                 return solve(stdin);
 147         } else {
 148                 DPRINT("Processing: %s\n", argv[optind]);
 149                 DPRINT("Thus skipping the other %d files\n", argc-optind);
 150                 FILE *currentfile = fopen(argv[optind], "r");
 151                 DPRINT("Opening file\n");
 152                 return solve(currentfile);
 153                 DPRINT("Closing file\n");
 154                 fclose(currentfile);
 155         }
 156 }