-void solve(FILE *inputstream){
- clock_t time_start, time_file_read;
- int buffer;
-
- time_start = clock();
- while((buffer = fgetc(inputstream)) != EOF){
- printf("%c", buffer);
- // Alex:
- // Screen reading
- // - Removing outside walls
- // - Bucket fill
- // - [tile]
- // - tile = structure {int, int, enumtile}
+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);
+
+ state *init = encode_screen(screen);
+ rels *rls = encode_rel(screen);
+
+ BDD old = sylvan_false;
+ BDD new = init->bdd;
+ int iteration = 0;
+ while(new != old){
+ ERRPRINT("Iteration %d\n", iteration++);
+ old = new;
+ new = sylvan_or(new, sylvan_relnext(new, rls->rell->bdd, rls->rell->varset.varset));
+ new = sylvan_or(new, sylvan_relnext(new, rls->relu->bdd, rls->relu->varset.varset));
+ new = sylvan_or(new, sylvan_relnext(new, rls->relr->bdd, rls->relr->varset.varset));
+ new = sylvan_or(new, sylvan_relnext(new, rls->reld->bdd, rls->reld->varset.varset));