-lurd_t *lappend(lurd_t *l, char c){
- lurd_t *temp_lrd = NULL;
- if (l == NULL){
- temp_lrd = (lurd_t *)malloc(sizeof(lurd_t));
- temp_lrd->c = c;
- temp_lrd->next = NULL;
- l = temp_lrd;
- }
- else {
- temp_lrd = l;
- while (temp_lrd->next != NULL){
- temp_lrd = temp_lrd->next;
- }
- temp_lrd->next = (lurd_t *)malloc(sizeof(lurd_t));
- temp_lrd->next->c = c;
- temp_lrd->next->next = NULL;
- }
- return l;
-}
-
-int check_goal(BDD s, BDD g, BDDSET vars){
- LACE_ME;
- if(sylvan_satcount(sylvan_and(s, g), vars) > 0) return 1;
- else return 0;
-}
-
-int check_visited(BDD s, BDD v, BDDSET vars){
- LACE_ME;
- if(sylvan_satcount(sylvan_and(s, v), vars) > 0) return 1;
- else return 0;
-}
-
-state_t *explstate(state *init, rels *rls, state *g){
- LACE_ME;
- deque *state_queue = create();
- trans_t *t = NULL;
- state_t *tmp_state = (state_t *)malloc(sizeof(state_t));
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- //state_t *new_state = (state_t *)malloc(sizeof(state_t));
- BDD visited = init->bdd;
- BDD new;
- tmp_state->bdd = init->bdd;
- tmp_state->vars = init->vars;
- tmp_state->lrd = lrd;
- state_queue = enq(tmp_state, state_queue);
-
- while (isEmpty(state_queue) == 0){
- tmp_state = get_front(state_queue);
- state_queue = deq(state_queue);
- new = tmp_state->bdd;
- t = rls->rell;
- while (t != NULL){
- new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
- if (new != sylvan_false && new != tmp_state->bdd) break;
- t = t->next_rel;
- }
- if (new != sylvan_false && new != tmp_state->bdd){
- if (check_visited(new, visited, init->vars.varset) == 0){
- if (check_goal(new, g->bdd, init->vars.varset) == 0){
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'l');
- new_state->lrd = lrd;
- state_queue = enq(new_state, state_queue);
- visited = sylvan_or(new, visited);
- }
- else {
- printf("GOAL\n");
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'l');
- new_state->lrd = lrd;
- return new_state;
- }
- }
- }
-
- t = rls->relu;
- while (t != NULL){
- new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
- if (new != sylvan_false && new != tmp_state->bdd) break;
- t = t->next_rel;
- }
- if (new != sylvan_false && new != tmp_state->bdd){
- if (check_visited(new, visited, init->vars.varset) == 0){
- if (check_goal(new, g->bdd, init->vars.varset) == 0){
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'u');
- new_state->lrd = lrd;
- state_queue = enq(new_state, state_queue);
- visited = sylvan_or(new, visited);
- }
- else {
- printf("GOAL\n");
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'u');
- new_state->lrd = lrd;
- return new_state;
- }
- }
- }
-
- t = rls->relr;
- while (t != NULL){
- new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
- if (new != sylvan_false && new != tmp_state->bdd) break;
- t = t->next_rel;
- }
- if (new != sylvan_false && new != tmp_state->bdd){
- if (check_visited(new, visited, init->vars.varset) == 0){
- if (check_goal(new, g->bdd, init->vars.varset) == 0){
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
-
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'r');
- new_state->lrd = lrd;
- state_queue = enq(new_state, state_queue);
- visited = sylvan_or(new, visited);
- }
- else {
- printf("GOAL\n");
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
-
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'r');
- new_state->lrd = lrd;
- return new_state;
- }
- }
- }
-
-
- t = rls->reld;
- while (t != NULL){
- new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
- if (new != sylvan_false && new != tmp_state->bdd) break;
- t = t->next_rel;
- }
- if (new != sylvan_false && new != tmp_state->bdd){
- if (check_visited(new, visited, init->vars.varset) == 0){
- if (check_goal(new, g->bdd, init->vars.varset) == 0){
-
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
-
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'd');
- new_state->lrd = lrd;
- state_queue = enq(new_state, state_queue);
- visited = sylvan_or(new, visited);
- }
- else {
- printf("GOAL\n");
- lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
- state_t *new_state = (state_t *)malloc(sizeof(state_t));
- memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
-
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'd');
- new_state->lrd = lrd;
- return new_state;
- }
- }
- }
-
-
- }
-
- return NULL;
-}
-