+void solve(FILE *inputstream)
+{
+ clock_t time_start_read, time_end_read;
+ clock_t time_start_encode, time_end_encode;
+
+ time_start_read = clock();
+ sokoban_screen *screen = parse_screen(inputstream);
+ if (screen == NULL) printf("Something went wrong...\n");
+ //sokoban_print(screen);
+ time_end_read = clock();
+
+ time_start_encode = clock();
+
+ lace_init(0, 1000000);
+ lace_startup(0, NULL, NULL);
+ LACE_ME;
+ sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
+ sylvan_init_bdd(6);
+ switch(strat){
+ case COORD:
+ DPRINT("Encoding coordinate based\n");
+ encode_screen(screen);
+ //test_relprod();
+ break;
+ case OBJECT:
+ DPRINT("Encoding object based\n");
+ solve_object(screen);
+ break;
+ case HYBRID:
+ DPRINT("Encoding hybrid based\n");
+ DPRINT("Not implemented yet...\n");
+ break;
+ default:
+ ERRPRINT("Huh?");
+ exit(2);