- while(new != old){
- ERRPRINT("Iteration %d\n", iteration++);
- old = new;
- //WRONG! each trans relation (LEFT,UP,RIGHT,DOWN) contains a linked list of trans relations (not just
- //only one), so to compute a transition for a single direction, we need to iterate through a relevant linked list
- //taking disjunction of results (for a single direction there will be falses and only one screen change among the
- //results)
- 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));
- }
- //sylvan_printdot_nc(old);
- //switch(strat){
- // case COORD:
- // DPRINT("Encoding coordinate based\n");
- // 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);
- //}
+ if (goal != NULL){
+ while(new != old){
+ old = new;
+ ERRPRINT("Iteration %d\n", iteration++);
+ trans_t *t = rls->rell;
+
+ //for testing
+ /*
+ BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9);
+ BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0});
+ BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0}));
+ BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1}));
+ if (new == teststate2) printf("Wrong!\n");
+ */
+ while (t != NULL){
+ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+ t = t->next_rel;
+ //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
+ }
+
+ t = rls->relu;
+ while (t != NULL){
+ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+ t = t->next_rel;
+ //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
+ }
+
+
+ t = rls->relr;
+ while (t != NULL){
+ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+ t = t->next_rel;
+ //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
+ }
+
+
+ t = rls->reld;
+ while (t != NULL){
+ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+ t = t->next_rel;
+ //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
+ }
+ double check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset);
+ if (check > 0){
+ printf("Solution is found after %d iteration(s)!\n", iteration);
+ break;
+ }
+ }
+ printf("Solution is not found after %d iteration(s)\n", iteration);
+ }
+ else printf("No solution found!\n");
+ //ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
+// sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);
+// sylvan_printdot_nc(old);