- //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));
+ 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);