- 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;
- }
- }
- }
- 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);
- time_end_encode = clock();
-
- //SOLVE???