- switch(strat){
- case COORD:
- DPRINT("Encoding coordinate based\n");
- state *s = encode_screen(screen);
- //test_relprod();
- rels *rls = encode_rel(screen);
- test_trans(s, rls->relr);
- 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);
+
+ 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));