From 313c58c1cd85852f33ff7ca7c638ccb3066d5069 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 21 Apr 2016 20:57:54 +0200 Subject: [PATCH] cleaned up code --- modelchecker/Makefile | 4 +- modelchecker/coord.c | 414 +++++------------------------------------- modelchecker/coord.h | 14 -- modelchecker/deque.c | 71 -------- modelchecker/deque.h | 28 --- modelchecker/main.c | 5 +- modelchecker/object.c | 202 --------------------- modelchecker/object.h | 10 - 8 files changed, 51 insertions(+), 697 deletions(-) delete mode 100644 modelchecker/deque.c delete mode 100644 modelchecker/deque.h delete mode 100644 modelchecker/object.c delete mode 100644 modelchecker/object.h diff --git a/modelchecker/Makefile b/modelchecker/Makefile index e284a57..2463f37 100644 --- a/modelchecker/Makefile +++ b/modelchecker/Makefile @@ -1,7 +1,7 @@ PROGRAM:=main -OBJS:=sokoban.o coord.o object.o deque.o +OBJS:=sokoban.o coord.o -CFLAGS:=-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11\ +CFLAGS:=-O3 -g -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11\ -I./sylvan/src LDLIBS:=-lm -lpthread -lrt LDFLAGS:=./sylvan/src/libsylvan.a diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 6325091..42ad6ce 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -6,7 +6,6 @@ #include "coord.h" #include "sokoban.h" -#include "deque.h" typedef struct { @@ -123,7 +122,6 @@ int check_space(int x, int y, direction d, int delta, bimap *bm) * It seems that the move variable is not necessary since non-deterministic moves can be emvedded * directly in transition relations. */ - state *encode_screen(sokoban_screen *screen) { LACE_ME; @@ -142,272 +140,51 @@ state *encode_screen(sokoban_screen *screen) fullState->vars.varset = varset; fullState->vars.size = HASH_COUNT(screen) * 3; int tile_index = 0; - sokoban_screen *r; - for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ + for(sokoban_screen *r=screen; r != NULL; r = r->hh.next){ switch(r->tile){ case FREE: //001 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; break; case WALL: //000 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; case BOX: //010 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; break; case TARGET: //011 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 1; break; case AGENT: //101 - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - - st_enc[tile_index] = 1; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; break; case TARGAGENT: //110 - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; break; case TARGBOX: //100 - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; } } s = sylvan_cube(varset, st_enc); fullState->bdd = s; - printf("Initial state encoded\n"); return fullState; } -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; -} - state *encode_goal(sokoban_screen *screen){ - int boxes = 0; - int targets = 0; - LACE_ME; BDDVAR vars[HASH_COUNT(screen) * 3]; @@ -424,83 +201,50 @@ state *encode_goal(sokoban_screen *screen){ fullState->vars.varset = varset; fullState->vars.size = HASH_COUNT(screen) * 3; int tile_index = 0; - sokoban_screen *r; - for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ + for(sokoban_screen *r=screen; r != NULL; r=r->hh.next){ switch(r->tile){ case FREE: //001 -> any - st_enc[tile_index] = 2; - tile_index++; - st_enc[tile_index] = 2; - tile_index++; - st_enc[tile_index] = 2; - tile_index++; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; break; case WALL: //000 -> stays the same - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; case BOX: //010 -> any - boxes++; - st_enc[tile_index] = 2; - tile_index++; - st_enc[tile_index] = 2; - tile_index++; - st_enc[tile_index] = 2; - tile_index++; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; break; case TARGET: //011 -> targbox - targets++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; case AGENT: //101 -> any - st_enc[tile_index] = 2; - tile_index++; - st_enc[tile_index] = 2; - tile_index++; - st_enc[tile_index] = 2; - tile_index++; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; break; case TARGAGENT: //110 -> targbox - targets++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; case TARGBOX: //100 -> stays the same - targets++; - boxes++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; } } s = sylvan_cube(varset, st_enc); fullState->bdd = s; - printf("Goal state encoded\n"); - if (targets == 0 || (boxes != targets)) return NULL; - else return fullState; - + return fullState; } -//test -//int countTrans(trans_t *trs); - trans_t *create_single_rel(sokoban_screen *screen, direction dir) { LACE_ME; @@ -571,9 +315,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - } - - else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){ + } else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){ xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); unsigned int deltai = bddvar->value.var[0]; //Agent Free -> Free Agent @@ -737,11 +479,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->varset.size = 12; trs_current->next_rel = trs; trs = trs_current; - - - } - - else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){ + } else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){ xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); unsigned int deltai = bddvar->value.var[0]; bddvar = getxy(x + xgamma, y + ygamma, bm->f); @@ -1367,47 +1105,9 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) } trs_current = trs; - - //test - /* - switch(dir){ - case LEFT: - if (trs_current != NULL) printf("LEFT ok!\n"); - else printf ("LEFT is empty\n"); - printf("Num of trans relations:%d\n", countTrans(trs)); - break; - case UP: - if (trs_current != NULL) printf("UP ok!\n"); - else printf ("UP is empty\n"); - printf("Num of trans relations:%d\n", countTrans(trs)); - break; - case RIGHT: - if (trs_current != NULL) printf("RIGHT ok!\n"); - else printf ("RIGHT is empty\n"); - printf("Num of trans relations:%d\n", countTrans(trs)); - break; - case DOWN: - if (trs_current != NULL) printf("DOWN ok!\n"); - else printf ("DOWN is empty\n"); - printf("Num of trans relations:%d\n", countTrans(trs)); - break; - } - */ return trs; } -//test -/* -int countTrans(trans_t *trs) -{ - int counter = 0; - while (trs != NULL){ - counter++; - trs = trs->next_rel; - } - return counter; -} -*/ rels *encode_rel(sokoban_screen *screen) { LACE_ME; @@ -1416,14 +1116,8 @@ rels *encode_rel(sokoban_screen *screen) //left relation tl = create_single_rel(screen, LEFT); - - //up relation trans_t *tu = create_single_rel(screen, UP); - - //right relation trans_t *tr = create_single_rel(screen, RIGHT); - - //down relation trans_t *td = create_single_rel(screen, DOWN); rels *rls = NULL; @@ -1435,17 +1129,3 @@ rels *encode_rel(sokoban_screen *screen) return rls; } - -int test_trans(state *s, trans_t *t) -{ - LACE_ME; - BDD next = sylvan_false; - while (t != NULL){ - next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset); - if (next == s->bdd) printf("Same\n"); - if (next != s->bdd && next != sylvan_false) printf("Different\n"); - if (next == sylvan_false) printf("False\n"); - t = t->next_rel; - } - return 1; -} diff --git a/modelchecker/coord.h b/modelchecker/coord.h index 014579f..15f6c76 100644 --- a/modelchecker/coord.h +++ b/modelchecker/coord.h @@ -40,21 +40,7 @@ typedef struct { typedef enum { LEFT, UP, RIGHT, DOWN } direction; state *encode_screen(sokoban_screen *screen); - rels *encode_rel(sokoban_screen *screen); - -int test_trans(state *s, trans_t *t); - state *encode_goal(sokoban_screen *screen); -int check_goal(BDD s, BDD g, BDDSET vars); - -int check_visited(BDD s, BDD v, BDDSET vars); - -lurd_t *lappend(lurd_t *l, char c); - -state_t *explstate(state *init, rels *rls, state *g); - -int test_relprod(); - #endif diff --git a/modelchecker/deque.c b/modelchecker/deque.c deleted file mode 100644 index 12ad6fc..0000000 --- a/modelchecker/deque.c +++ /dev/null @@ -1,71 +0,0 @@ -#include -#include -#include -#include -#include - -#include "deque.h" - -deque *create() -{ - deque *d; - d = (deque *)malloc(sizeof(deque)); - d->front = NULL; - d->rear = NULL; - d->count = 0; - - return d; -} - -deque *enq(state_t *s, deque *d) -{ - if (d->rear == NULL){ - d->rear = (node_t *)malloc(sizeof(node_t)); - d->rear->ptr = NULL; - d->rear->s = s; - d->front = d->rear; - } - else { - node_t *temp = (node_t *)malloc(sizeof(node_t)); - d->rear->ptr = temp; - temp->s = s; - temp->ptr = NULL; - d->rear = temp; - } - d->count++; - - return d; -} - -deque *deq(deque *d) -{ - node_t *front_tmp = d->front; - - if (front_tmp == NULL){ - return d; - } - else if (front_tmp->ptr != NULL){ - front_tmp = front_tmp->ptr; - free(d->front); - d->front = front_tmp; - } - else { - free(d->front); - d->front = NULL; - d->rear = NULL; - } - d->count--; - return d; -} - -int isEmpty(deque *d) -{ - if (d->front != NULL && d->rear != NULL) return 0; - else return 1; -} - -state_t *get_front(deque *d) -{ - if (isEmpty(d) == 0) return d->front->s; - else return NULL; -} diff --git a/modelchecker/deque.h b/modelchecker/deque.h deleted file mode 100644 index 16125ea..0000000 --- a/modelchecker/deque.h +++ /dev/null @@ -1,28 +0,0 @@ -#ifndef DEQUE_H -#define DEQUE_H -#include -#include -#include "coord.h" - -typedef struct node { - state_t *s; - struct node *ptr; -} node_t; - -typedef struct { - node_t *front; - node_t *rear; - int count; -} deque; - -deque *create(); - -deque *enq(state_t *s, deque *d); - -deque *deq(deque *d); - -int isEmpty(deque *d); - -state_t *get_front(deque *d); - -#endif diff --git a/modelchecker/main.c b/modelchecker/main.c index 79bb46d..07a665c 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -8,7 +8,6 @@ #include "sokoban.h" #include "coord.h" -#include "object.h" #define DPRINT(fmt, as...) if(VERBOSE) fprintf(stderr, fmt, ## as); #define REPORT(s, end, start) DPRINT(s, ((double)(end-start))/CLOCKS_PER_SEC); @@ -48,7 +47,7 @@ int solve(FILE *inputstream, char *lurd) //Read screen time_start_read = clock(); - sokoban_screen *screen = parse_screen(inputstream, false); + sokoban_screen *screen = parse_screen(inputstream, true); if (screen == NULL) { printf("Something went wrong encoding the screen\n"); return 2; @@ -130,7 +129,7 @@ int solve(FILE *inputstream, char *lurd) REPORT("Goal encoding: %fs\n", time_end_goal, time_start_goal); REPORT("Relation encoding: %fs\n", time_end_rel, time_start_rel); REPORT("Solving encoding: %fs\n", time_end_solve, time_start_solve); - + DPRINT("Iterations needed: %d\n", iteration); if(!found){ printf("no solution\n"); diff --git a/modelchecker/object.c b/modelchecker/object.c deleted file mode 100644 index 362802d..0000000 --- a/modelchecker/object.c +++ /dev/null @@ -1,202 +0,0 @@ -#include -#include - -#include "object.h" -#include "sokoban.h" - -#define MAX_BOX 50 -#define EPRINTF(fmt, as...) fprintf(stderr, fmt, ##as) - -typedef enum {UP, DOWN, LEFT, RIGHT} direction; - -int ilog2(int x) -{ - int l = 1; - while((x >>= 1) >= 1) - l++; - return l; -} - -void get_screen_metrics(sokoban_screen *screen, - int *boxes, - int *mx, int *my, - int *agentx, int *agenty, - int *boxxes, int *boxyes) -{ - *boxes = 0; - *mx = 0; - *my = 0; - *agentx = 0; - *agenty = 0; - sokoban_screen *r; - for(r=screen; r != NULL; r = r->hh.next){ - *mx = r->coord.x > *mx ? r->coord.x : *mx; - *my = r->coord.y > *my ? r->coord.x : *my; - switch(r->tile){ - case TARGAGENT: - case AGENT: - *agentx = r->coord.x; - *agenty = r->coord.y; - break; - case TARGBOX: - case BOX: - boxxes[*boxes] = r->coord.x; - boxyes[*boxes] = r->coord.y; - *boxes += 1; - break; - default:; - } - } -} - -//LSB first -BDD encode_int(BDD state, int x, int bx, int *variablenum) -{ - LACE_ME; - char *encoding = malloc(bx); - for(int i = 0; i 0){ - state = sylvan_and(state, sylvan_ithvar(*variablenum*2)); - } else { - state = sylvan_and(state, sylvan_nithvar(*variablenum*2)); - } - *variablenum += 1; - } - free(encoding); - return state; -} - -BDD encode_position(BDD state, int x, int y, int bx, int by, int *variablenum) -{ - state = encode_int(state, x, bx, variablenum); - return encode_int(state, y, by, variablenum); -} - -BDD encode_transition(sokoban_screen *scr, BDD state, int bx, int by, int *varnum, direction dir) -{ - LACE_ME; - //Increase the position - int oldvarnum = *varnum; - - //RIGHT - if(dir == RIGHT){ - state = sylvan_and(state, - sylvan_xor(sylvan_ithvar(*varnum*2), sylvan_ithvar(*varnum*2+1))); - *varnum += 1; - for(int i = 1; ihh.next){ - int x = r->coord.x; - int y = r->coord.y; - *varnum = oldvarnum; - - BDD currentx = sylvan_true; - for(int i = 0; i 0){ - currentx = sylvan_and(currentx, sylvan_ithvar(*varnum*2+1)); - } else { - currentx = sylvan_and(currentx, sylvan_nithvar(*varnum*2+1)); - } - *varnum += 1; - } - - BDD currenty = sylvan_true; - for(int i = 0; i 0){ - currenty = sylvan_and(currenty, sylvan_ithvar(*varnum*2+1)); - } else { - currenty = sylvan_and(currenty, sylvan_nithvar(*varnum*2+1)); - } - *varnum += 1; - } - legalpos = sylvan_or(legalpos, - sylvan_and(currentx, currenty)); - } - - return sylvan_and(state, legalpos); -} - -/* - * We have variables numbered 1... - * Per coordinate we need k=bitsx+bitsy variables - * - * agent: 0 till k - * box_i: k+k*i till k+k*(i+1) - * We start with the agent - */ -BDD solve_object(sokoban_screen *scr) -{ - LACE_ME; - int nboxes, mx, my, wx, wy, agentx, agenty; - int varnum = 0; - int boxx[MAX_BOX]; - int boxy[MAX_BOX]; - - get_screen_metrics(scr, &nboxes, &mx, &my, &agentx, &agenty, boxx, boxy); - - EPRINTF("Max x: %d, thus %d bits\n", mx, (wx = ilog2(mx))); - EPRINTF("Max y: %d, thus %d bits\n", my, (wy = ilog2(my))); - EPRINTF("%d boxes\n", nboxes); - - BDD init = encode_position(sylvan_true, agentx, agenty, wx, wy, &varnum); - for(int i = 0; i - -#include "sokoban.h" - -BDD solve_object(sokoban_screen *screen); - -#endif -- 2.20.1