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);
22 "\t%s [opts] [FILE]\n"
25 "\t-l LURD initial LURD\n"
26 "\t-v enable verbose output\n"
27 "\t-h show this help\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
);
34 BDD
subsolve(trans_t
*t
, BDD
new){
37 new = sylvan_or(new, sylvan_relnext(new, t
->bdd
, t
->varset
.varset
));
43 int solve(FILE *inputstream
, char *lurd
)
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
;
50 time_start_read
= clock();
51 sokoban_screen
*screen
= parse_screen(inputstream
, false);
53 printf("Something went wrong encoding the screen\n");
56 time_end_read
= clock();
58 //Lace and sylvan blork
59 lace_init(0, 1000000);
60 lace_startup(0, NULL
, NULL
);
62 sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
66 time_start_scr
= clock();
67 state
*init
= encode_screen(screen
);
68 time_end_scr
= clock();
71 time_start_goal
= clock();
72 state
*goal
= encode_goal(screen
);
73 time_end_goal
= clock();
76 time_start_rel
= clock();
77 rels
*rls
= encode_rel(screen
);
78 time_end_rel
= clock();
81 time_start_solve
= clock();
82 //BDD old = sylvan_false;
88 new = subsolve(rls
->rell
, new);
91 new = subsolve(rls
->relu
, new);
94 new = subsolve(rls
->relr
, new);
97 new = subsolve(rls
->reld
, new);
100 printf("Unknown character in lurd: '%c'\n", *lurd
);
107 //bool found = false;
110 DPRINT("Iteration %d\n", iteration++);
112 if(sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset) > 0){
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);
125 state
*cont
= (state
*)malloc(sizeof(cont
));
127 cont
->vars
= init
->vars
;
128 res
= explstate(cont
, rls
, goal
);
130 if (res
->lrd
== NULL
) printf("wrong\n");
131 lurd_t
*l
= res
->lrd
;
140 time_end_solve
= clock();
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
);
152 printf("no solution\n");
159 int main(int argc
, char **argv
)
164 while((optchar
= getopt(argc
, argv
, "vhl:")) != -1){
167 DPRINT("Lurd detected: `%s'\n", optarg
);
172 DPRINT("Debug enabled\n");
179 DPRINT("Skipping unknown option `-%c'.\n", optopt
);
181 DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt
);
190 DPRINT("You have not specified a file, reading from stdin\n");
191 return solve(stdin
, lurd
);
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");