+ //Lace and sylvan blork
+ 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);
+
+ //Encode screen
+ time_start_scr = clock();
+ state *init = encode_screen(screen);
+ time_end_scr = clock();
+
+ //Encode goal
+ time_start_goal = clock();
+ state *goal = encode_goal(screen);
+ time_end_goal = clock();
+
+ //Encode transitions
+ time_start_rel = clock();
+ rels *rls = encode_rel(screen);
+ time_end_rel = clock();
+
+
+ //Actually solve
+ time_start_solve = clock();
+ BDD old = sylvan_false;
+ BDD new = init->bdd;
+ //Do lurd
+ for(unsigned int i = 0; i<strlen(lurd); i++){
+ switch(lurd[i]){
+ case 'l':
+ new = subsolve(rls->rell, new);
+ break;
+ case 'u':
+ new = subsolve(rls->relu, new);
+ break;
+ case 'r':
+ new = subsolve(rls->relr, new);
+ break;
+ case 'd':
+ new = subsolve(rls->reld, new);
+ break;
+ default:
+ printf("Unknown character in lucd: '%c'\n", lurd[i]);
+ exit(2);
+ }
+ }
+ int iteration = 0;
+ bool found = false;
+ 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);