- // Future: SMC
- fprintf(stderr, "Reading: %fs\n",
- ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
- fprintf(stderr, "Encoding: %fs\n",
- ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
+ while(new != old){
+ DPRINT("Iteration %d\n", iteration++);
+ old = new;
+ if(sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset) > 0){
+ found = true;
+ break;
+ }
+
+ //Left, Up, Right, Down moves
+ new = subsolve(rls->rell, new);
+ new = subsolve(rls->relu, new);
+ new = subsolve(rls->relr, new);
+ new = subsolve(rls->reld, new);
+ }
+
+ time_end_solve = clock();
+
+ //Free and print stats
+ sokoban_free(screen);
+ REPORT("Reading: %fs\n", time_end_read, time_start_read);
+ REPORT("Screen encoding: %fs\n", time_end_scr, time_start_scr);
+ REPORT("Goal encoding: %fs\n", time_end_goal, time_start_goal);
+ REPORT("Relation encoding: %fs\n", time_end_rel, time_start_rel);
+ REPORT("Solving encoding: %fs\n", time_end_solve, time_start_solve);
+
+
+ if(!found){
+ printf("no solution\n");
+ return 1;
+ }
+
+ return 0;